--- Day changed Mon Sep 04 2017
kyagrdHas Agda user's mailing list homepage moved from https://lists.chalmers.se/mailman/listinfo/agda ? (getting 403 Forbidden)04/09 04:53
WilliamHamiltonWhy is the inspect module in the standard library deprecated? Is that not useful anymore in new versions of Agda?04/09 10:53
WilliamHamilton(oh I see, there's inspect on steroids)04/09 10:54
WilliamHamiltonmietek, in the end I was able to costruct an inductive representation of the normal terms I'm interested in and I'm trying to adapt the semantics04/09 11:06
WilliamHamiltonbut I'd still appreciate if someone could take a look at this function http://lpaste.net/358196#line101 and suggest me how to proceed (or how to get Agda to accept my with clause)04/09 11:07
WilliamHamiltonthe thing is, this should be a very simple task, there's no profound reason for me not managing to write that code other than my clumsiness with agda04/09 11:07
WilliamHamiltonanyways, I commented the parts in which I'm interested in, and tried to clean up the clauses as best as I could04/09 11:08
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) with τ₁ ≟ τ₂ | σ₁ ≟ σ₂04/09 11:19
pgiarrusso... | yes refl | yes refl = yes refl04/09 11:19
pgiarrussoWilliamHamilton: to fix ≟ on Type, it's easiest to ask Agda to do the case split04/09 11:19
pgiarrussoyou write, after the with,  ... | p | q = {!!} , case split, and get a better result:04/09 11:21
pgiarrussosplitting on p gives you (τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) | yes p | q = {!!} -- and another line which is boring04/09 11:22
pgiarrussoand splitting on the new p gives (τ₁ ⇒ σ₁) ≟ (.τ₁ ⇒ σ₂) | yes refl | q = {!!} --, where τ₂ becomes .τ₁04/09 11:22
pgiarrussoWilliamHamilton: given the amount of code you wrote after that point, it seems you're using a very non-interactive development style — have you a chance to see (live or video) somebody experience code in Agda with its interactive code-editing support?04/09 11:25
pgiarrusso(can't point to a good video, also I really dislike videos, but might be worth here. I've learned it from people and docs)04/09 11:25
WilliamHamiltonpgiarrusso: for the first part, unfortunately I did not get the point you were trying to make for the ≟ function. It seems that you were suggesting a better way to write it, in that case could you show me the final result?04/09 11:26
WilliamHamiltonI did the refining of that function using mostly the refine command and the give command04/09 11:27
pgiarrussoWilliamHamilton: you need to use case-split to also modify the left-hand side04/09 11:27
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) with τ₁ ≟ τ₂ | σ₁ ≟ σ₂04/09 11:27
pgiarrusso(τ₁ ⇒ σ₁) ≟ (.τ₁ ⇒ σ₂) | yes refl | q = {!!}04/09 11:27
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) | no ¬p | q = {!!}04/09 11:27
pgiarrussothat is what I have now here (I haven't finished that code here) but it is progress04/09 11:28
pgiarrussoyou're right there is something I'm not explaining well — matching on refl modifies the context because it says that tau1 and tau2 are equal, right?04/09 11:30
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-04_10:31:09.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/oCxISJoPQGdKIqIWooRuwptk>04/09 11:31
WilliamHamiltonthen I tidied up this version using `...` and `_` to hide irrelevant details and variables04/09 11:31
pgiarrussono no no no no, that's forbidden04/09 11:32
pgiarrusso... means "copy the line above unchanged"04/09 11:32
pgiarrussoI mean, does the code keep typechecking after you do that refactoring?04/09 11:32
WilliamHamiltonyes it does, but I get the point now04/09 11:33
pgiarrussoI mean, ... | yes refl | yes refl = yes refl means 04/09 11:33
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) | yes refl | yes refl = yes refl04/09 11:33
pgiarrussomeans (τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) | yes refl | yes refl = yes refl , which should not type check 04/09 11:33
WilliamHamiltonI see, but so, as agda never puts `...` by itself, does that mean that I will have only complete lines in my code?04/09 11:33
pgiarrussobecause refl does not have type τ₁ ≡ τ₂04/09 11:34
pgiarrussowell, you can only use ... if the lines can be equal04/09 11:34
pgiarrussobut if pattern matching modifies the LHS, you can't replace it by ...04/09 11:34
WilliamHamiltonI see, that makes sense (there's still the point that it typechecks for some reason, and I would be interested in knowing why - but I won't do that manually anymore)04/09 11:35
pgiarrussothat *is* confusing and doesn't work here04/09 11:35
pgiarrussothere  *are* bugs in Emacs with stale typechecking results and undo04/09 11:35
pgiarrussofor instance, this code fails:04/09 11:35
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂) with τ₁ ≟ τ₂ | σ₁ ≟ σ₂04/09 11:36
pgiarrusso... | yes refl | yes refl = yes refl04/09 11:36
pgiarrusso(τ₁ ⇒ σ₁) ≟ (.τ₁ ⇒ σ₂)  | yes refl | no ¬p    = no (¬p Function.∘ ⇒-≡-inj₂)04/09 11:36
pgiarrusso(τ₁ ⇒ σ₁) ≟ (τ₂ ⇒ σ₂)   | no ¬p    | q        =  no (¬p Function.∘ ⇒-≡-inj₁)04/09 11:36
pgiarrussojust because of that ...04/09 11:36
pgiarrussoBTW, ... is fine for the line with two "no"s, because the context is refined04/09 11:36
WilliamHamiltonI see, just to be sure, does the code I pasted in that hpaste compile for you?04/09 11:36
pgiarrussoalso, for reference, I'm using Agda 11:37
WilliamHamiltoni mean, it also has the ... | yes refl | yes refl line04/09 11:37
WilliamHamilton(I'm using agda 2.5.2)04/09 11:37
pgiarrussoWilliamHamilton: doesn't work with my Agda, I started answering on the first error I got04/09 11:37
WilliamHamiltonoooh, I see, thanks (I was presupposing that it compiled, as it does on my computer)04/09 11:38
WilliamHamiltonnow I understand what's going on here, ok04/09 11:38
WilliamHamiltonso, let's me rewrite those function without my edits, so that you'll be able to load them without errors04/09 11:38
WilliamHamiltonI'll paste it again in a moment04/09 11:39
pgiarrussoso either they changed things in 2.5.2 (surprising), or sth. else is wrong04/09 11:39
pgiarrussoOK04/09 11:39
pgiarrussodoh, I find my code but it just does dec. equality for types and contexts (also got much simpler terms, for STLC)—it's https://github.com/inc-lc/ilc-agda/blob/master/Thesis/SIRelBigStep/Types.agda, but not sure it helps04/09 11:40
WilliamHamiltoneh, I understand how to do it on types and contexts, the problem I'm having is on the terms; and as I said what's bugging me is that it's matematically a very simple operation, I get stuck in the formalization04/09 11:42
pgiarrussoWilliamHamilton: let me face palm a second since 2.5.2 changed exactly what we discussed, sorry04/09 11:43
pgiarrussohttps://github.com/agda/agda/blob/master/CHANGELOG.md#pattern-matching04/09 11:43
WilliamHamiltonso what was happening in my code was that `.` was inserted automatically in my lhs?04/09 11:45
pgiarrussowell, it wasn't being inserted where needed here... and after reading the changelog carefully, I'm still confused why it works for you.04/09 11:47
WilliamHamiltonpgiarrusso: so, if I understood correctly the problem, http://lpaste.net/358197 should work on your version04/09 11:54
pgiarrussoWilliamHamilton: got it to work (with a couple smaller changes), trying to understand the problem... trying to install the new version meanwhile04/09 11:57
pgiarrussoLOL, your commented out 2nd case works here (with the old version of ...)04/09 11:59
pgiarrussoWhat about04/09 11:59
pgiarrusso((Γ₁ , (σ ⇒ τ)) , λt t₁) ≟ᵗ (_ , λt t₂) | yes refl | yes refl with ((Γ₁ < σ , τ) , t₁) ≟ᵗ ((Γ₁ < σ , τ) , t₂)04/09 11:59
pgiarrusso((Γ₁ , (σ ⇒ τ)) , λt t₁) ≟ᵗ (_ , λt t₂) | yes refl | yes refl | a = {!!}04/09 11:59
pgiarrussothat works here, and hopefully means the same for you?04/09 12:00
WilliamHamiltonperfect, so the point is that I'd like to prove decidable equality for two terms, but I cannot directly compare two terms with different contexts or types, so instead I want the decidable equality for what I called ATm in the code, which is a term with explicitly stated context and type04/09 12:00
WilliamHamiltonlol, let me try that04/09 12:00
WilliamHamiltonthat's very strange:04/09 12:03
WilliamHamiltonyour version works, but the strange part is that04/09 12:03
WilliamHamiltonmy version also works (because I changed the definition before?)04/09 12:03
WilliamHamiltonwait, let me do some more experiments04/09 12:05
pgiarrussoon your approach: the idea makes sense, not sure if comparing terms with the *same* context and type would work04/09 12:05
WilliamHamiltonthat's the problem I'm having: why do you think it could not work?04/09 12:06
pgiarrussowell, I'm not sure if subcalls keep having the same context/type04/09 12:07
pgiarrussomore precisely: I think all cases should work, *except for* _[_] where I'm not sure04/09 12:07
WilliamHamiltonok, there should be an analogue function ≟ˢ which checks substitutions, and those should be mutually defined04/09 12:08
WilliamHamiltonbut I'd be happy to do the application case, or the lambda one, which are easier, first04/09 12:09
WilliamHamiltonin the meantime04/09 12:09
WilliamHamiltonI understood where my error came from:04/09 12:09
pgiarrussoOK: if the substitutions are decidably equal, then you should be able to invoke the function recursively04/09 12:09
WilliamHamiltonin the first version of the code you saw, the clauses for when the context or types are different were:04/09 12:10
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-04_11:10:24.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/XGwyevpKVOHCdKCjghMlRKUo>04/09 12:10
WilliamHamiltonthis caused the error in the second clause to explode04/09 12:10
WilliamHamiltonif instead I write04/09 12:10
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-04_11:11:05.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/FsUwiQbybgbvBqjPHEUuTbjv>04/09 12:11
WilliamHamiltonnot using the `...`, then I don't have an error there04/09 12:11
WilliamHamiltonso lesson learned, never manually use `...` :D04/09 12:11
pgiarrussowell, use it carefully04/09 12:11
pgiarrussoin this case, which LHS should it copy?04/09 12:11
WilliamHamiltonright, the one a lot of lines before:04/09 12:12
WilliamHamilton```04/09 12:12
WilliamHamilton_≟ᵗ_ ((Γ₁ , τ₁) , t₁) ((Γ₂ , τ₂) , t₂) with Γ₁ ≟ᶜ Γ₂ | τ₁ ≟ τ₂04/09 12:12
WilliamHamilton```04/09 12:12
WilliamHamiltonthis one, so I get what I was doing wrong04/09 12:12
WilliamHamiltonbetter just to rewrite it04/09 12:13
pgiarrussoyeah, I'm trying to guess which one it is copying here, honestly not sure, but *that* reproduces the error you see04/09 12:13
pgiarrussobecause sometimes it *does* copy a line from earlier I think, not sure what the rules are04/09 12:14
pgiarrussoWilliamHamilton: are you implementing explicit substitutions? is your Agda code online?04/09 12:34
pgiarrussobecause I've never seen explicit substitutions formalized, let alone in this "intrinsically typed" style04/09 12:34
WilliamHamiltonwell, in that gist there are also the definitions of explicit substitution, but you should take a look at the original work this is based on, Chapman's thesis; for comparison, Chapman's code is at https://github.com/jmchapman/Big-step-Normalisation/blob/master/LambdaCalculus/BasicSystem/Syntax.agda04/09 12:35
WilliamHamilton(to be clear: I just began writing code based on Chapman's one, so I don't have much of my own)04/09 12:40
pgiarrussoThanks for the pointer! People keep recommending his thesis04/09 12:54
WilliamHamiltonyou have to thank mietek as he was the one suggesting it to me, but I found it very well written, and also has the code on his github page which is a huge plus. Well structured code, also04/09 12:59
WilliamHamiltonpgiarrusso: speaking of interactive workflow, the thing that really slows me down is that I don't know how to handle the errors that make yellow part of the buffer (lol, I mean those in which typechecking leaves some holes). For example, I completed most of line 128 in http://lpaste.net/358198#line128 , but when I refine with proj2, the holes are not informative and I don't know how to complete that04/09 13:16
WilliamHamiltoncould you illustrate what your workflow might be in this case, and how to  arrive to a solution?04/09 13:17
pgiarrussoquick answer: yellow things are arguments that can't be deduced, often implicits arguments (as there), so in general I add implicit arguments and fill them in via {?}... but proj\_2 is different04/09 13:19
pgiarrussofor that sort of case, I usually add more stuff before refining04/09 13:19
WilliamHamiltonwhat makes it different? And what stuff do you add?04/09 13:19
pgiarrussowell, refining a hole of type tau with proj\_2 means creating a hole of type alpha, tau, where alpha is completely undetermined04/09 13:20
pgiarrussoso importantly: alpha will become a yellow thing, but that will usually be automatically solved when you add an argument to proj_204/09 13:21
pgiarrussoif you know what the argument of proj_2 should be, I'd start writing proj_2 (your-stuff) and checking the type matches04/09 13:22
pgiarrussodoes that answer?04/09 13:23
pgiarrusso(sorry, multi-tasking with ICFP talks)04/09 13:23
WilliamHamiltonI'm trying to follow along, np; the thing is that I would write `proj2 x`, and I have to understand first why that doesn't typecheck04/09 13:24
pgiarrussoC-c , or C-c . should show you relevant info04/09 13:24
pgiarrussolook at the context—either x isn't a pair, or its 2nd component doesn't match the expected type04/09 13:25
WilliamHamiltonsorry, I meant proj_2-==04/09 13:26
pgiarrussolooking at its type and nothing else: {B : A → Set} looks hard to infer04/09 13:32
pgiarrussobecause it's a function and higher-order unification in general is undecidable04/09 13:32
pgiarrussothe local fix is to add {B = ?} and try to figure out what argument you want for B04/09 13:32
pgiarrussobut I suspect your B should just *not* be implicit04/09 13:33
pgiarrussowhich is why the corresponding argument of subst in the stdlib is not implicit04/09 13:33
pgiarrussoI'm *not* sure though, because maybe the later arguments help04/09 13:34
pgiarrussoWilliamHamilton, aah I see what's happening:04/09 13:37
pgiarrussoGoal: λt t₁ ≡ λt t₂04/09 13:37
pgiarrussoHave: λt t₁ ≡04/09 13:37
pgiarrusso      subst (λ gt → Tm (proj₁ gt) (proj₂ gt)) (sym (proj₁-≡ x)) (λt t₂)04/09 13:37
WilliamHamiltonright, that's literally for how the definition of proj_2-== is04/09 13:38
pgiarrussoso you can fill in `P.trans (proj₂-≡ x)`, but now you have a subst in there04/09 13:38
WilliamHamiltonwait, first, where did you see Goal:... Have:...?04/09 13:39
WilliamHamiltonok, I'm on board with goal04/09 13:39
pgiarrussoI used C-c .04/09 13:39
pgiarrussoput `proj₂-≡ x` in the goal, since you said that's what you wanted, and used C-c .04/09 13:40
WilliamHamiltoncould you give me the name of the command corresponding to `C-c .`?04/09 13:40
pgiarrusso(or well, I'm using Spacemacs so I use , .)04/09 13:40
WilliamHamiltonok, I'm using spacemacs too, ok04/09 13:40
WilliamHamiltonjust give me the spacemacs version of things :)04/09 13:40
pgiarrusso, .04/09 13:40
pgiarrussoIIUC Emacs C-c generally becomes ,04/09 13:41
pgiarrussoFWIW, the full name is agda2-goal-and-context-inferred04/09 13:41
WilliamHamiltonohh! That command is extremely useful!04/09 13:41
WilliamHamiltonI don't know how I could miss it till now04/09 13:42
WilliamHamiltonok! Now I see what you mean04/09 13:42
pgiarrussoagda2-goal-and-context shows everything but the stuff you're filling in, useful if you don't have sth that type checks04/09 13:42
pgiarrussosee https://github.com/syl20bnr/spacemacs/tree/master/layers/%2Blang/agda04/09 13:42
pgiarrussothat writes `SPC m` instead of `,`, but `,` is a standard abbreviation04/09 13:42
pgiarrusso(and to clarify: I use `` everywhere as in Markdown, you're not supposed to type those)04/09 13:43
pgiarrussoback to subst: are you familiar with Agda's reduction behavior?04/09 13:43
WilliamHamiltonyes, I'm familiar enough with spacemacs, and the ` ` convention is fine; perfect, now I have to understand how to get rid of subst04/09 13:43
WilliamHamiltonunfortunately not04/09 13:43
pgiarrussoso, subst is defined by equation04/09 13:44
pgiarrussosubst P refl p = p04/09 13:44
pgiarrussoso Agda has a small-step reduction rule subst P refl p -> p04/09 13:44
pgiarrusso(I am *not* going to write the congruence rules)04/09 13:44
WilliamHamiltonok, that makes sense04/09 13:45
pgiarrussowhat's confusing to most (me included) is that Agda does not have a rule subst P x p -> p04/09 13:45
pgiarrussobecause the second rule is unsound if x is open04/09 13:45
pgiarrussox might depend on some assumption in context that cannot be realized (say, Int = Bool)04/09 13:46
pgiarrussoso, in general, adding such rules could violate type soundness when reducing open terms04/09 13:46
pgiarrussoto get an actual example, take04/09 13:47
pgiarrussocast : ∀ {a b : Set} → a ≡ b → a → b04/09 13:47
pgiarrussoabsurdTerm = λ (prf : ℕ ≡ Bool) → cast prf 3 ∨ false04/09 13:47
pgiarrussocast refl x = x04/09 13:47
pgiarrussoand now imagine Agda reduced cast eq x -> x04/09 13:47
WilliamHamiltonright, so I have to make sure that the eq in subst is indeed refl04/09 13:48
pgiarrussothe body of absurdTerm would then reduce to 3 ∨ false, then to a core dump04/09 13:48
pgiarrussoexactly04/09 13:48
pgiarrussoI'd try having a separate lemma04/09 13:49
WilliamHamiltonin my case at hand that would be `sym (proj₁-≡ x)`04/09 13:49
WilliamHamiltonright?04/09 13:49
WilliamHamiltonif I prove that this is refl, the subst rewrite starts and I complete the lemma04/09 13:50
pgiarrussocorrect04/09 13:50
pgiarrussohowever, often (and maybe here) one can try to avoid the subst04/09 13:51
WilliamHamiltonhow would one do that? I'd have to change the definition of proj_2-== right?04/09 13:52
pgiarrussoI mean, that term `sym (proj₁-≡ x)` has type (Γ₁ , σ ⇒ τ) ≡ (Γ₁ , σ ⇒ τ)04/09 13:52
pgiarrussofor this case, I'd try adding a variant of proj_2-== for this case... let me try a second04/09 13:53
pgiarrussoproj₂-≡2 : ∀{A : Set} {B : A → Set} → {a : A} → {p₁ p₂ : B a} → (eq : _≡_ {A = Σ A B} (a , p₁) (a , p₂)) → p₁ ≡ p₂04/09 13:55
pgiarrussoproj₂-≡2 refl = refl04/09 13:55
pgiarrusso(name's silly)04/09 13:55
WilliamHamiltonI can see this works but I have to think more about how I could have thought this definition04/09 13:56
WilliamHamiltonI see, postulating that the first component is already equal, I free myself from the need of proving the substitution; that's a very smart solution, thank you!04/09 13:59
pgiarrussoWilliamHamilton, thanks!04/09 13:59
pgiarrussoI'm trying to use it here but running into confusing trouble...04/09 13:59
WilliamHamilton```04/09 13:59
WilliamHamilton  = no (λ x → ¬p (pair-≡ (refl , λ-≡-inj (proj₂-≡2 x))))04/09 13:59
WilliamHamilton```04/09 13:59
WilliamHamiltonthis typechecks ^. Are there some troubles in other parts?04/09 14:00
pgiarrussoI was having trouble with that, not sure what's up04/09 14:02
pgiarrussoOK, works now, as expected, so go ahead04/09 14:03
WilliamHamiltonyeah, I'm already doing the app case; I'm probably able to do this by myself with the lessons learned, I'll ping if I run in something unexpected or when I get the solution04/09 14:04
WilliamHamiltonthanks again for the help!04/09 14:04
pgiarrussoBTW, last thing I forgot:04/09 14:04
pgiarrusso_≟ᵗ2_ : ∀ Γ τ → (t₁ t₂ : Tm Γ τ) → Dec (t₁ ≡ t₂)04/09 14:04
pgiarrusso_≟ᵗ2_ = {!!}04/09 14:04
pgiarrussoearlier I was suggesting *this* definition *should* work04/09 14:04
WilliamHamiltonthis works only if they have the same type, oooh04/09 14:04
WilliamHamiltonI can use this as a lemma for my version04/09 14:05
pgiarrussoif you need the extended version, yes04/09 14:05
pgiarrussoyes. earlier it sounded like you were trying to use two Gamma and two taus, which is indeed much more painful04/09 14:05
WilliamHamiltonnono! in fact the right thing to do is probably prove this last lemma you said, and the extended version is only a wrapper around it once I get to unify the contexts and the types04/09 14:06
pgiarrusso+104/09 14:27
pgiarrussoHas anybody compiled Agda (2.5.2) with Happy 1.19.6 (from 2 days ago)? I'm trying to pin down some compile failures and separate operator errors from real problems04/09 18:08
pgiarrussoat least I installed 2.5.2 with Stackage LTS 8.24 (using happy 1.19.5). Retrying with the newer happy version04/09 18:14
pgiarrusso... and it fails!04/09 18:14
WilliamHamiltonpgiarrusso: if you're you're only interested in the latest version, I usually install agda via nix, to not pollute my haskell installation04/09 18:15
pgiarrussoI just got 2.5.2 version installed, right now I'm debugging what's going on for a report04/09 18:16
pgiarrussoFWIW I filed https://github.com/agda/agda/issues/273104/09 19:23

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!