--- Day changed Fri Mar 31 2017
sleffyHey guys! I'm trying to use https://agda.github.io/agda-stdlib/Data.Vec.Properties.html#11166. But, I can't figure out for the life of me how to get the `to` function out of there. This is probably trivial, but I don't know enough about records to get this right.31/03 00:26
sleffyI think the main problem is that I've got an `↔` here, and I don't know how to get a one-way function (from left to right) out of it.31/03 00:31
sleffyReally don't need all this Setoid baggage. Is there a nice way to take an `A ↔ B`, and get an `A → B` out of it? Nice and simple.31/03 00:39
glguysleffy: to-fun : ∀ {a b} {A : Set a} {B : Set b} → A ↔ B → A → B31/03 00:57
glguyto-fun inv x = Inverse.to inv ⟨$⟩ x31/03 00:57
sleffyglguy, thank you!31/03 00:57
sleffyShows where the pattern is there, too.31/03 00:57
--- Log closed Fri Mar 31 01:54:20 2017
--- Log opened Fri Mar 31 02:00:38 2017
-!- Irssi: #agda: Total of 127 nicks [0 ops, 0 halfops, 0 voices, 127 normal]31/03 02:00
-!- Irssi: Join to #agda was synced in 126 secs31/03 02:02
sleffyI need Agda to temporarily ignore the fact that two things are not definitionally equal, and generate a propositional equality instead. Is there a way to do so?31/03 02:47
sleffyI have a problem w.r.t. delaying a check of definitional equality. I have a solution to it, but I'd like to know if there's another solution.31/03 03:47
lpastesleffy pasted “PropositionalNotDefinitional.agda” at http://lpaste.net/35412131/03 03:47
comieteksleffy: have you considered John Major equality?31/03 06:05
comietek~== in the std lib31/03 06:05
comietek(single character)31/03 06:05
sleffycomietek, unfortunately I don't think heterogeneous equality would have helped31/03 06:06
sleffyThe issue was preventing Agda from requiring definitional equality, and instead generating a propositional equality31/03 06:06
sleffyI didn't need an equality between two inhabitants of different types; I needed a convenient way to "relax" the pattern matching rules, which I suspect doesn't exist31/03 06:07
comietekI'll look at the code in a bit31/03 06:12
sleffycomietek, don't worry too much about it - I found a solution. If you're still curious though, I did list it in the paste.31/03 06:13
sleffyI think I got disconnected the first time I tried to send this. So, I'll try again. Agda is complaining about getting stuck on a unification problem when I try to C-c C-c in Emacs. I can't see any reason why it would get stuck - everything looks trivially unifiable. The only thing I can think of is that it might be choking on the built-in function type, but that would be ridiculous, wouldn't it? http://lpaste.net/35414831/03 17:19
mieteksleffy: please paste the actual code that has a problem31/03 17:29
sleffymietek, okay. There's a total of five files involved here. The problem itself occurs here on line 156 of `Lemmas.agda`: http://lpaste.net/3134623143012859904#line15631/03 17:34
sleffyOther dependencies include `Typing.agda` which contains the typing judgement family (http://lpaste.net/6818550003066208256), `Eval.agda` the small-step reduction (http://lpaste.net/3790771533115293696), `Syntax.agda` the actual abstract syntax along with substitution using `Data.Fin.Substitution`. (http://lpaste.net/6364785763351003136)31/03 17:35
sleffy`Ctx n` here is just `Vec (Maybe Type) n`, but there are some other lemmas and such in a module of their own. I can paste that if need be.31/03 17:36
mietekuh.31/03 17:37
sleffyThe issue is that if I try to split `x` (I want to be able to pattern-match `tlam` on it, because it's clearly typed using the lambda typing rule from `Typing.agda`) then Agda refuses to unify with the error I pasted above.31/03 17:37
mietekdebugging 101: try to isolate a self-contained minimal test case31/03 17:38
mietekwhile talking to a rubber duck31/03 17:38
sleffyThis is part of why I wanted to try and avoid posting the whole problem. :P31/03 17:38
sleffyYeah, I wasn't quite sure how to isolate this one, because I'm really not sure what's causing it.31/03 17:38
sleffyUnification with function types themselves have worked just fine in other places in this project31/03 17:38
mietekyou could at least post 1 file with only the dependencies needed for this 1 function that has a hole31/03 17:38
sleffyI've been able to pattern-match on these judgements just fine as well31/03 17:39
sleffy...yeah that probably would have been a better idea. I'll try to reformat the mess, then31/03 17:39
mietekthen I could easily load it in Agda and see what’s wrong31/03 17:39
lpastesleffy pasted “Linear/Core.agda” at http://lpaste.net/35414931/03 17:46
sleffymietek, done ^ that was a lot smaller than I thought it would be...31/03 17:46
sleffyTo reproduce the problem, try to pattern-match on `tlam` either directly on `x` on line 85, or try to pattern-match `tlam` against `jf` on line 93.31/03 17:47
sleffyOr, you can try `C-c C-c x` in the hole on 85, which produces the most puzzling error message so far.31/03 17:48
mieteksleffy: I think the problem is "green slime"31/03 18:52
mieteksleffy: sorry, was AFK31/03 18:52
mieteksleffy:   lam t     / ρ = lam (t / ρ ↑)31/03 18:53
mieteksleffy: https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf31/03 18:53
mieteksleffy: >> The presence of ‘green slime’— defined functions in the return types of constructors—is a danger sign.31/03 18:53
sleffymietek, knowing McBride, I tried to google "green slime" in an attempt to figure out what reference he was making this time. But the only two things I can come up with are a two-star sci-fi film from the '60s and a DnD monster...31/03 19:09
mieteksleffy: I think it’s just that his syntax highlighting does functions in green31/03 19:09
mietekor did at some point31/03 19:09
sleffyhaha, oh man, that's even better31/03 19:09
dolioYeah, it's that.31/03 19:09
dolioI think it was epigram that did that?31/03 19:10
sleffyAnyways, I switched from embedding my types into Agda's type system to using an inductive `Type` datatype. That solved the problem.31/03 19:10
dolioThe code comments of one of the versions of epigram 2 makes reference to "blue" and "green" things, too, and there's no explanation; you just have to know what color the epigram emacs mode uses for things.31/03 19:11
mietekoh doh31/03 19:11
mietekI pasted the wrong line when I tried to explain31/03 19:12
mietekI should have pasted31/03 19:12
mietek    → c ⊢ lam e ∈ (t1 → t2)31/03 19:12
mietekso it was choking on the built-in function type31/03 19:12
sleffyYeah, that's kinda what I figured was going on31/03 19:13
sleffyBut it feels fishy to me that it couldn't unify `a → b` with `c → d`31/03 19:13
sleffyWhy would that be impossible?31/03 19:14
mietekdo you mean, unify these types, or unify some _values_ of these types?31/03 19:14
sleffyUnify the types.31/03 19:17
sleffyThat's what it needed to do to make things work. There weren't any values involved31/03 19:17
sleffyI was using those types strictly to annotate things. For example, `(lam (var zero))` in the system I was trying to build would be the identity function, and you could build a typing judgement for it which says it's from `a → a` for some a.31/03 19:18
sleffyNot that `lam (var zero) : a → a`, but that you could build an instance of `Γ ⊢ lam (var zero) ∈ a → a`31/03 19:19
sleffyWhich wouldn't actually contain an `a → a`.31/03 19:19
sleffyEventually I was going to write a `compile` function which would turn it into an `a → a`...31/03 19:20

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