WilliamHamilton[ WilliamHamilton[ WilliamHamilton[ --- Day changed Fri Sep 01 2017 hi all, I'd like some help in understanding how I could write something in Agda 01/09 13:49 There is this datatype, data Tm : Con → Ty → Set where, which models the terms in a STLC 01/09 13:50 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 Types 01/09 13:51 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 list 01/09 13:52 * WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-01_13:03:56.txt 01/09 14:03 but I'm having problems with membership 01/09 14:12 * WilliamHamilton[ sent a long message: WilliamHamilton[_2017-09-01_13:25:17.txt 01/09 14:25 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 for 01/09 14:25 (Dec) so how should I turn the ≡ equality into decidable equality? 01/09 14:28 I'll stop my rambling pinging mietek 01/09 14:28 WilliamHamilton[: you want a list of triples 01/09 15:19 or pairs, where the first element is a pair -- a context and a type... 01/09 15:20 and that's essentially the encoding with (Σ Con (λ c → Σ Ty (λ t → Tm c t))) I did before, right? 01/09 15:20 isomorphic, yes 01/09 15:21 I must have a dependent product 01/09 15:21 oh 01/09 15:21 no this is good enough 01/09 15:21 what's your isomorphic version? 01/09 15:21 Con \times Ty 01/09 15:21 i mean, what you did is fine 01/09 15:21 i'm suggesting a stylistic difference 01/09 15:21 but I didn't see you got this 01/09 15:22 so what is your issue again? 01/09 15:22 my issue is how do I check that one of these terms is in a list of these terms 01/09 15:22 basically, how do I use the module 01/09 15:22 https://agda.github.io/agda-stdlib/Data.List.Any.Membership.html 01/09 15:23 I'd like to have a binary answer to the question "is this element in the list?" 01/09 15:23 can you try answering this question without using the stdlib? 01/09 15:24 i don't think using it is helpful at this stage 01/09 15:24 or to be honest at any stage except detour research 01/09 15:24 s/detour/setoid/ 01/09 15:24 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 01/09 15:25 that's a datatypes 01/09 15:26 datatype* 01/09 15:26 oh, I'm dumb, I can just write the function like I'd do in haskell 01/09 15:27 I got lost thinking about Decidability 01/09 15:27 well, you probably do want to have a Dec (x % L) 01/09 15:27 where % stands for something 01/09 15:28 and you will probably only be able to get here if the type of x is equipped with a decidable equality 01/09 15:28 why should I want a Dec? Doesn't a function of type A -> List A -> Bool suffice? 01/09 15:29 moreover, I'd like the decidable equality for my type to do what ≡ does, and I'm not sure how 01/09 15:30 Bool is a projection of Dec 01/09 15:32 https://gist.github.com/mietek/a40dbb19e05fc2fe368f8ee6dbcd4f9f 01/09 15:32 here's a small example of a decidable equality 01/09 15:32 note it is distinct from propositional equality 01/09 15:32 we are making a decision that propositional equality holds 01/09 15:32 sure, we could just be returning Bool, if that's all you want 01/09 15:33 but that's less information 01/09 15:33 for example, in your list membership case 01/09 15:33 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 if we return Bool, all we know is that the list either contains or does not contain an the element 01/09 15:34 but if we return a value of a hypothetical IsMemberOf type 01/09 15:34 we can pinpoint exactly where that element is, in a type safe manner 01/09 15:34 we know the position 01/09 15:34 https://mietek.github.io/research/html/PreludeList.html#5404 01/09 15:35 example 01/09 15:36 there is no deriving in Agda 01/09 15:36 you could maybe hack something together with the reflection facility 01/09 15:36 no, I still haven't read about reflection, but it seems to advanced for my immediate concerns here 01/09 15:37 thanks for the examples, I'll define a decidible equality now! 01/09 15:37 yeah, i wouldn't recommend it 01/09 15:38 oh, moreover, the stylistical difference you were mentioning before: could you expand upon it? 01/09 15:38 I'm not sure I understood the point 01/09 15:38 well, the term type depends on two things 01/09 15:38 a context and a type 01/09 15:39 oh, making it depend on a pair? 01/09 15:39 yes 01/09 15:39 because neither element of the pair needs to depend on each other 01/09 15:39 ok than, that's a good suggestion, I wanted to be sure that there wasn't another part to it 01/09 15:39 s/than/then 01/09 15:39 it's conceivable that you could also want a list of terms that *all* depend on the same context 01/09 15:40 or that are all of the same type; why not 01/09 15:40