--- Day changed Fri Sep 01 2017
WilliamHamilton[hi all, I'd like some help in understanding how I could write something in Agda01/09 13:49
WilliamHamilton[There is this datatype, `data Tm : Con → Ty → Set where`, which models the terms in a STLC01/09 13:50
WilliamHamilton[now, I want an algorithm that takes as an input a list of these terms, but I want this list to store heterogeneous Contexts and Types01/09 13:51
WilliamHamilton[so, to be clearer, I want a list of terms, irrespective of the context and types I'm using, and moreover I'd like to check whether a term I have is in this list01/09 13:52
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-01_13:03:56.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/kbYajgEGXeUNeaXHIFGhYYyz>01/09 14:03
WilliamHamilton[but I'm having problems with membership01/09 14:12
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-01_13:25:17.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/heYPNGhXtKUkxyAlYZQOVgGM>01/09 14:25
WilliamHamilton[what I really wanted to ask agda is a yes/no question. I understood that the `yes/no` questions should be what the `Decidable` class is for01/09 14:25
WilliamHamilton[(`Dec`) so how should I turn the `≡` equality into decidable equality?01/09 14:28
WilliamHamilton[I'll stop my rambling pinging mietek01/09 14:28
comietekWilliamHamilton[: you want a list of triples01/09 15:19
comietekor pairs, where the first element is a pair -- a context and a type...01/09 15:20
WilliamHamilton[and that's essentially the encoding with `(Σ Con (λ c → Σ Ty (λ t → Tm c t)))` I did before, right?01/09 15:20
comietekisomorphic, yes01/09 15:21
WilliamHamilton[I must have a dependent product01/09 15:21
WilliamHamilton[oh01/09 15:21
comietekno this is good enough01/09 15:21
WilliamHamilton[what's your isomorphic version?01/09 15:21
comietekCon \times Ty01/09 15:21
comieteki mean, what you did is fine01/09 15:21
comieteki'm suggesting a stylistic difference01/09 15:21
comietekbut I didn't see you got this01/09 15:22
comietekso what is your issue again?01/09 15:22
WilliamHamilton[my issue is how do I check that one of these terms is in a list of these terms01/09 15:22
WilliamHamilton[basically, how do I use the module01/09 15:22
WilliamHamilton[https://agda.github.io/agda-stdlib/Data.List.Any.Membership.html01/09 15:23
WilliamHamilton[I'd like to have a binary answer to the question "is this element in the list?"01/09 15:23
comietekcan you try answering this question without using the stdlib?01/09 15:24
comieteki don't think using it is helpful at this stage01/09 15:24
comietekor to be honest at any stage except detour research01/09 15:24
comieteks/detour/setoid/01/09 15:24
WilliamHamilton[the thing I would write by myself if something isomorphic to:01/09 15:25
* WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-01_14:25:59.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/DmwMSgazlyPJVpCmIqwBOfYS>01/09 15:25
comietekthat's a datatypes01/09 15:26
comietekdatatype*01/09 15:26
WilliamHamilton[oh, I'm dumb, I can just write the function like I'd do in haskell01/09 15:27
WilliamHamilton[I got lost thinking about Decidability01/09 15:27
comietekwell, you probably do want to have a Dec (x % L)01/09 15:27
comietekwhere % stands for something01/09 15:28
comietekand you will probably only be able to get here if the type of x is equipped with a decidable equality01/09 15:28
WilliamHamilton[why should I want a Dec? Doesn't a function of type A -> List A -> Bool suffice?01/09 15:29
WilliamHamilton[moreover, I'd like the decidable equality for my type to do what ≡ does, and I'm not sure how01/09 15:30
comietekBool is a projection of Dec01/09 15:32
comietekhttps://gist.github.com/mietek/a40dbb19e05fc2fe368f8ee6dbcd4f9f01/09 15:32
comietekhere's a small example of a decidable equality01/09 15:32
comieteknote it is distinct from propositional equality01/09 15:32
comietekwe are making a decision that propositional equality holds01/09 15:32
comieteksure, we could just be returning Bool, if that's all you want01/09 15:33
comietekbut that's less information01/09 15:33
comietekfor example, in your list membership case01/09 15:33
WilliamHamilton[I see, and there is no way to generate automatically a decidable equality, in the way `deriving Eq` works in haskell, right?01/09 15:33
comietekif we return Bool, all we know is that the list either contains or does not contain an the element01/09 15:34
comietekbut if we return a value of a hypothetical IsMemberOf type01/09 15:34
comietekwe can pinpoint exactly where that element is, in a type safe manner01/09 15:34
WilliamHamilton[we know the position01/09 15:34
comietekhttps://mietek.github.io/research/html/PreludeList.html#540401/09 15:35
comietekexample01/09 15:36
comietekthere is no deriving in Agda01/09 15:36
comietekyou could maybe hack something together with the reflection facility01/09 15:36
WilliamHamilton[no, I still haven't read about reflection, but it seems to advanced for my immediate concerns here01/09 15:37
WilliamHamilton[thanks for the examples, I'll define a decidible equality now!01/09 15:37
comietekyeah, i wouldn't recommend it01/09 15:38
WilliamHamilton[oh, moreover, the stylistical difference you were mentioning before: could you expand upon it?01/09 15:38
WilliamHamilton[I'm not sure I understood the point01/09 15:38
comietekwell, the term type depends on two things01/09 15:38
comieteka context and a type01/09 15:39
WilliamHamilton[oh, making it depend on a pair?01/09 15:39
comietekyes01/09 15:39
comietekbecause neither element of the pair needs to depend on each other01/09 15:39
WilliamHamilton[ok than, that's a good suggestion, I wanted to be sure that there wasn't another part to it01/09 15:39
WilliamHamilton[s/than/then01/09 15:39
comietekit's conceivable that you could also want a list of terms that *all* depend on the same context01/09 15:40
comietekor that are all of the same type; why not01/09 15:40

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