--- Day changed Sat Sep 02 2017
WilliamHamilton[mietek, in the context of writing decidable equality for data types, `≡` basically means `i will normalize the two terms and check they're literally equal`, right?02/09 09:31
WilliamHamilton[and if so, I wonder why it doesn't suffice that the outermost constructors be different for the two terms to be different02/09 09:32
WilliamHamilton[for example, why the last function here http://lpaste.net/358157 is not obvious at line 66?02/09 09:34
WilliamHamilton[my intent would be to say: they have different outmost constructors, so they are different terms02/09 09:34
WilliamHamilton[I also seem to get stuck in this minor problem:02/09 10:22
WilliamHamilton[```02/09 10:22
WilliamHamilton[tm≡-inj₁ : ∀ {Γ₁ Γ₂ τ₁ τ₂} → Tm Γ₁ τ₁ → Tm Γ₂ τ₂ → Tm Γ₁ τ₁ ≡ Tm Γ₂ τ₂ → Γ₁ ≡ Γ₂02/09 10:22
WilliamHamilton[```02/09 10:22
WilliamHamilton[I realize that my problem is that unification is not working like I naively expect it to do, but cannot understand the details02/09 10:23
WilliamHamilton[Another way to put the question might be: what does the expression `Tm Γ₁ τ₁ ≡ Tm Γ₂ τ₂` mean when I try to use it as an hypothesis?02/09 12:08
WilliamHamilton[my intuition would be that i could pattern match on it to get `refl`, and this would imply the unification of (Γ₁ and Γ₂) and of (τ₁ and τ₂)02/09 12:09
WilliamHamilton[instead, when I try to pattern match on it in agda, I get the error:02/09 12:10
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-02_11:11:09.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/xLKhEHeLLhiZwoGmLiAcRDkD>02/09 12:11
WilliamHamilton[(the relevant example file is always  http://lpaste.net/358157 )02/09 12:11
WilliamHamilton[(or better still http://lpaste.net/358158 - I cleaned it up a bit)02/09 12:14
skiWilliamHamilton[ : replace the `refl' pattern by the "absurd" pattern, `()', and remove the `=' and the definiens02/09 12:53
ski(a `C-c C-c' on the scrutinee would do this, here)02/09 12:53
skithe absurd pattern means "i'm trying to match on actual constructors here, but there's no alternatives (left), so we're in an impossible situation" (and hence no body is required)02/09 12:54
WilliamHamilton[ski: thanks for the help: are you referring to tm≡-inj₂ in  http://lpaste.net/358158 ?02/09 12:55
skireferring to02/09 12:55
ski  _≟ᵗ_ {.(_ < τ₁)} {τ₁} {.(_ < τ₁)} {.τ₁} top (t2 [ x ]) | yes refl | yes refl = no {!!}02/09 12:55
WilliamHamilton[ok, give me a second to try that out02/09 12:56
skiif you had `| yes refl | yes x = {!x!}' there, and do a `C-c C-c' on the `x', it will do this automatically for you, as i mentioned02/09 12:56
skithe point here is that `x' is known to have a type `top ≡ t2 [ x ]', but there's no constructors matching this (because `top' and `t2 [ x ]' are disjoint), so using the absurd pattern amounts to explicitly recognizing this fact in the proof02/09 12:58
ski(er, i should have called it `eq' or something, not `x'. you already had an `x' in scope. sorry)02/09 12:58
skiWilliamHamilton[ : btw, next time, use the "Annotation" button to make updates/additions. that way it'll end up on the same page. "Edit" can be used to make e.g. minor corrections (the edited paste is replaced on the page, though older versions and diffs can be viewed)02/09 13:02
WilliamHamilton[I will, thanks; unfortunately I'm not managing to get the previous suggestion work, although I understand why that is the right direction; I'll try another few times and then ping if I get nowhere, if it's cool02/09 13:04
WilliamHamilton[if I start from:02/09 13:05
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-02_12:05:47.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/lVZcadcMJwnhoJNVerTGyqgm>02/09 13:05
skioh, hm, i'm not paying enough attention02/09 13:06
skiyou're not doing `t1 ≟ t2', but `τ₁ ≟ τ₂'02/09 13:07
WilliamHamilton[right, let me try the other option02/09 13:08
WilliamHamilton[how could I do the comparison between two terms? That's what I'm trying to define (it should be t1 ≟ᵗ t2, which is the function I'm trying to define). Or am I missing something?02/09 13:09
skii'm not quite sure why you're passing `Tm Γ₁ τ₁' and `Tm Γ₂ τ₂' to `_≟ᵗ_', let alone why you're trying to prove `Dec (Tm Γ₁ τ₁ ≡ Tm Γ₂ τ₂)' (decidable equality of two term *types*, not of two terms)02/09 13:10
WilliamHamilton[I was trying to pass those terms because I coudn't manage to do the proof without02/09 13:11
skidid you mean to say02/09 13:11
ski  _≟ᵗ_ : ∀ {Γ₁ τ₁ Γ₂ τ₂} → (t₁ : Tm Γ₁ τ₁) → (t₂ : Tm Γ₂ τ₂) → Dec (t₁ ≡ t₂)02/09 13:11
ski?02/09 13:11
WilliamHamilton[oh, right, that's probably what I was trying to say, yes02/09 13:12
WilliamHamilton[that I can compare two of those terms02/09 13:12
WilliamHamilton[I will try to prove the right version now (sorry!)02/09 13:12
skii'm not sure whether it's possible to prove your `tm≡-inj₂'02/09 13:13
ski(probably someone more experienced could answer that)02/09 13:13
WilliamHamilton[but maybe there will be no need of that in this right version (it could be a more reasonable lemma)02/09 13:14
skiright02/09 13:14
ski(hopefully now the absurd pattern should do the trick)02/09 13:16
WilliamHamilton[let's hope so, I should write the correct thing I want to prove first :D (it's not ≟ᵗ : ∀ {Γ₁ τ₁ Γ₂ τ₂} → (t₁ : Tm Γ₁ τ₁) → (t₂ : Tm Γ₂ τ₂) → Dec (t₁ ≡ t₂) because I want to compare also terms which have different context and type; they shouldn't be equal - but probably I can encode that somehow)02/09 13:17
WilliamHamilton[in the meantime, thanks for the help, it has been very appreciated :)02/09 13:17
skiWilliamHamilton[ : "I want to compare also terms which have different context and type; they shouldn't be equal" -- is there a reason you want this ?02/09 13:22
WilliamHamilton[ski: yes, I'm trying to write a function that checks if a term contains a term from a list I want to `ban`02/09 13:23
WilliamHamilton[for example, let's say I want to notice when some variables appear, and do something in that case02/09 13:23
WilliamHamilton[so, the function checking is recursive on the derivation tree and on the leafs I will check: leaf `elem` forbiddenLeafs02/09 13:25
WilliamHamilton[hope this makes some sense, I've been simplifying something; if you want more details, you can ask for the full version02/09 13:25
skican't you just use weakening on the `forbiddenLeafs', as you enter a lambda ?02/09 13:26
ski(i don't follow the "I want to notice when some variables appear", can you elaborate ?)02/09 13:26
WilliamHamilton[yes, that will part of it (actually I have to do this to do things correctly: the forbiddenLeafs are weakened every time they enter a lambda)02/09 13:27
skiso i'm not sure why you require heterogenous equality02/09 13:28
WilliamHamilton[ok, so, I am trying to prove that STLC (and than Godel T) normalize when I strip of the xi rule02/09 13:28
WilliamHamilton[which is the rule that says that if I know t1 == t2 then I can conclude lambda t1 == lambda t202/09 13:28
WilliamHamilton[and I want to do this with Big Step Normalization (I was going to use Normalization by Evaluation, but I don't know how to formalize that)02/09 13:29
WilliamHamilton[so I recognized that the proof could work with slight changes from the normal one02/09 13:30
WilliamHamilton[if I encoded which application I want to be blocked, which is essentially a syntactic check02/09 13:30
WilliamHamilton[to be more clear I'll do an example02/09 13:30
WilliamHamilton[the term λx . (\y . y) x is already in normal form if I omit the xi rule02/09 13:31
WilliamHamilton[that's because I don't want to reduce this application: (\y . y) x02/09 13:32
WilliamHamilton[because x is bound by a lambda02/09 13:32
WilliamHamilton[so my reasoning is that I could do a preliminary pass, and just mark that application as locked02/09 13:32
WilliamHamilton[and to do that I want to know when a term contains a variable from a list that I will construct from binders02/09 13:33
WilliamHamilton[does this make at least a bit of sense? (as opposed to: pure madness :D)02/09 13:34
WilliamHamilton[(btw I'm totally open to suggestions on how I could do things better)02/09 13:36
skihm02/09 13:44
skii still don't see how you go from this to wanting heterogenous equality02/09 13:45
WilliamHamilton[I'm not sure I want heterogenous equality: probably it will suffice something of a suitable Σ type02/09 13:45
WilliamHamilton[equality on Σ (Con × Ty) (λ (g ,′ t) → Tm g t) maybe02/09 13:45
skiyeah, that's what i was going to try02/09 13:45
skibtw, it might perhaps be useful here to syntactically distinguish between free and bound variables02/09 13:46
skii believe Conor McBride (?) suggests that, in one paper02/09 13:46
WilliamHamilton[that might be useful, I'll think about that02/09 13:47
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-02_12:48:03.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/MMIhfBpIJhNJuxReRtZiUtKv>02/09 13:48
WilliamHamilton[I'm trying a series of variations of this theme but they are all rejected02/09 13:48
WilliamHamilton[while I can say `Σ (Con × Ty) (λ x → Tm ε ι)`02/09 13:49
WilliamHamilton[why can't I pattern match on a product in that way?02/09 13:49
WilliamHamilton[ok, for reference Σ (Con × Ty) (λ {(g , t) → Tm g t}) was the correct form; I had to use a special pattern matching lambda (the { })02/09 14:02
skihm, yea, for some reason, ordinary lambda can't match, even in cases like this where there's only one form02/09 14:06
ski(an alternative would be to use two `Σ's)02/09 14:06
comietekWilliamHamilton[: NbE is far easier than BSN; not sure where are you getting lost, but i showed you complete NbE for STLC earlier02/09 14:07
comietekbbl02/09 14:07
WilliamHamilton[comietek: including the proofs of soundness and completeness?02/09 14:08
WilliamHamilton[or just the algorithm? Because the algorithm is simpler, but I don't recall seeing the formalization of the properties (I hope I'm wrong)02/09 14:09
WilliamHamilton[`{p₁ p₂ : Σ A B} → p₁ ≡ p₂ → proj₁ p₁ ≡ proj₁ p₂` is easily provable02/09 15:38
WilliamHamilton[is there an analog principle for the second component?02/09 15:38
lambda-11235WilliamHamilton[: There is. The type becomes more complicated because you have to show proj2 p1 and proj2 p2 are both of type B (proj1 p1), or B (proj1 p2).02/09 16:02
lambda-11235http://lpaste.net/35816302/09 16:03
WilliamHamilton[thanks lambda-11235, good to know!02/09 16:04
comietekWilliamHamilton[: nbe is composition of soundness and completeness02/09 16:41
comietekunless you mean soundness _of_ nbe, in which case, Coquand 200202/09 16:41
WilliamHamilton[so, probably I mean soundness of nbe, in the sense that I want a theorem stating that t ≃ nf (t) for every t in my language and also one saying that t ≃ t' ⇒ nf t = nf t'02/09 16:47
WilliamHamilton[is that what you mean with the distinction, comietek?02/09 16:47
comieteklikely, yes02/09 16:48
WilliamHamilton[for example, Chapman has the theorems I'm referring to, here https://github.com/jmchapman/Big-step-Normalisation/tree/master/LambdaCalculus/BasicSystem02/09 16:48
comietekcool02/09 16:48
WilliamHamilton[see for example https://github.com/jmchapman/Big-step-Normalisation/blob/master/LambdaCalculus/BasicSystem/Soundness.agda02/09 16:48
comieteki still think that nbe is conceptually simpler02/09 16:49
WilliamHamilton[but comietek I'm very interested in knowing why nbe is simpler02/09 16:49
WilliamHamilton[right02/09 16:49
comietekwell, we already said this just now02/09 16:49
comietekit's a composition of a translation forth, from syntax to semantics, and back, from semantics to syntax02/09 16:49
WilliamHamilton[the thing is, as I read the presentation of both, it seems to me that they are the same thing, only BSN uses a `first order presentation` of the ~kripke argument that at some point you need02/09 16:50
WilliamHamilton[yes, but BSN as presented by chapman is morally the same thing: a translation from a syntax source to a semantic language, and back to a target syntax language02/09 16:50
comietekmorally...02/09 16:51
comietekit's likely that both techniques are close; you will find people saying that everything is nbe02/09 16:51
comietekbbl02/09 16:51
WilliamHamilton[if you happen to find it, I'm very interested in a more detailled discussion of the differences, because for now the only thing that changes is that in nbe you use full kripke relations and in bsn you use a first level presentation02/09 16:51
WilliamHamilton[by the way lambda-11235, is the function you referred to present in the agda standard library, to your knowledge?02/09 16:53
lambda-11235WilliamHamilton[: I have no idea.02/09 17:06
lambda-11235Σ-≡,≡↔≡ in /usr/share/agda/lib/prim/Function/Related/TypeIsomorphisms.agda seems to do the job.02/09 17:10
WilliamHamilton[lambda-11235:  thanks again!02/09 17:13
lambda-11235WilliamHamilton[: np.02/09 17:13
WilliamHamilton[if I need to write some implicit arguments for an infix operator02/09 17:39
WilliamHamilton[is there a way to do that without writing it in the prefix form?02/09 17:39
WilliamHamilton[don't mind that; here's another question:02/09 18:52
WilliamHamilton[I don't understand how to use record in imported modules from the standard library02/09 18:53
WilliamHamilton[I want to use the function https://agda.github.io/agda-stdlib/Function.Related.TypeIsomorphisms.html#%CE%A3-%E2%89%A1,%E2%89%A1%E2%86%94%E2%89%A102/09 18:54
WilliamHamilton[Σ-≡,≡↔≡.to02/09 18:54
WilliamHamilton[`Σ-≡,≡↔≡.to`02/09 18:54
WilliamHamilton[so I'm trying to import it in my module with no avail. I tried02/09 18:55
WilliamHamilton[open import Function.Related.TypeIsomorphisms using (Σ-≡,≡↔≡)02/09 18:55
WilliamHamilton[(and the function Σ-≡,≡↔≡.to appears not to be in scope)02/09 18:56
WilliamHamilton[2.02/09 18:56
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-02_17:57:01.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/rcdkIGgWsjHYviFfozgbFajq>02/09 18:57
WilliamHamilton[(but this doesn't compile because the module is not found)02/09 18:57
WilliamHamilton[what's the right way to import that function?02/09 18:58
Eduard_MunteanuWilliamHamilton[, that's not a record definition, it's just "to" in a "where" clause, so you can't get to it directly.02/09 22:06
glguyYou'll need something like: open import Function.Related.TypeIsomorphisms using (Σ-≡,≡↔≡)02/09 22:06
glguyopen import Function.Inverse as Inv using (module Inverse)02/09 22:06
glguyopen Inverse (Σ-≡,≡↔≡ {p₁ = {!!}} {p₂ = {!!}}) renaming (to to foo)02/09 22:06
Eduard_MunteanuAlso the "to" in the record is part of _↔_02/09 22:08
glguyor easier would be: foo = Inverse.to Σ-≡,≡↔≡02/09 22:08
glguyEduard_Munteanu: _↔_ isn't the underlying record type, Inverse is02/09 22:09
glguyFrom ↔ To = Inverse (P.setoid From) (P.setoid To)02/09 22:10
WilliamHamilton[thanks for the advices; so in this case:02/09 22:11
WilliamHamilton[open Inverse (Σ-≡,≡↔≡ {p₁ = {!!}} {p₂ = {!!}}) renaming (to to foo)02/09 22:11
WilliamHamilton[p1 and p2 should be probably set to the two types that compose the sigma02/09 22:11
WilliamHamilton[but what does the same function in02/09 22:12
WilliamHamilton[foo = Inverse.to Σ-≡,≡↔≡?02/09 22:12
glguyYou'll have to find a way to specify p1 and p2 there, too02/09 22:12
WilliamHamilton[yes, but I tried:02/09 22:12
WilliamHamilton[foo = Inverse.to Σ-≡,≡↔≡ {foo} {bar} and that doesn't work02/09 22:13
WilliamHamilton[oh wait02/09 22:13
glguyyou needs parentheses still02/09 22:13
glguyor Σ-≡,≡↔≡ {p₁ = _} {p₂ = _} .to02/09 22:14
glguycould be a way to get around the parens02/09 22:14
glguyand you'll definitely need the explicit p₁ = and p₂ =02/09 22:14
glguyunless you also want to provide all of the other leading implicit parameters positionally02/09 22:14
WilliamHamilton[could I ask where does the Inverse module come from?02/09 22:17
WilliamHamilton[it's not mentioned anywhere explicitly in Σ-≡,≡↔≡ 's signature02/09 22:18
glguyI pasted the definition of ↔ above02/09 22:18
WilliamHamilton[oh, I see now, thanks02/09 22:19
glguyWilliamHamilton[: The other thing to call out in particular is that your pasted code earlier tried using both open and import on Σ-≡,≡↔≡02/09 22:26
glguyimport is specifically to loading a module from file02/09 22:26
glguyopen is about bringing things into scope02/09 22:26
WilliamHamilton[I see, so once Σ-≡,≡↔≡ gets its arguments and becomes a record, I can open it02/09 22:27
WilliamHamilton[that's the reason for02/09 22:27
WilliamHamilton[open Inverse (Σ-≡,≡↔≡ {p₁ = {!!}} {p₂ = {!!}}) renaming (to to foo)02/09 22:27
glguyIn the case of open Inverse (Σ-≡...02/09 22:27
glguyYou're opening the Inverse module02/09 22:27
glguybut it's not being loaded from Inverse.agda, so you don't include the import02/09 22:28
glguyIt's already loaded from an earlier import02/09 22:28
WilliamHamilton[thanks, this is very useful02/09 22:28
glguyThat part's slightly confused because there's a module Function.Inverse which itself contains another Inverse record, and records introduce new modules themselves02/09 22:28
glguyand we can either open the record's module on its own, or open it as applied to some value02/09 22:30
glguyso: open Inverse02/09 22:30
glguyor: open Inverse value-of-type-Inverse02/09 22:30
WilliamHamilton[what happens in the first case? I'll have a `to` in scope?02/09 22:30
glguyYeah, a to in scope with type Inverse... -> type-of-to-field02/09 22:31
glguyto : {omitted} → Inv.Inverse From To → From ⟶ To02/09 22:34
WilliamHamilton[yes, thanks, I was trying to do a concrete example but I noticed that the arguments for Inverse are setoids,02/09 22:34
WilliamHamilton[so I can't use ℕ and (λ n → n ≡ 2) which are my go-to examples02/09 22:35
WilliamHamilton[just to be sure, does the agda lib have a version of Σ-≡,≡↔≡ not setoid oriented, or is it common to reimplement such simple functions like lambda-11235 suggested?02/09 22:37
WilliamHamilton[(this has been an excellent way to learn about modules, but for my code I just wanted to reason with ≡ and Σ)02/09 22:38
glguyI don’t know; I’ve never needed either.02/09 22:38
glguyBut writing a local definition would seem fine to me.02/09 22:38

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