--- Log opened Sat Jan 01 00:00:58 2011 | ||

Saizan | is there an algorithm for transforming recursive definitions accepted by the termination checker into definitions that use eliminators? at least for the inductive cases? | 01/01 13:14 |
---|---|---|

dolio | Saizan: Look for Eliminating Dependent Pattern Matching. | 01/01 21:30 |

--- Day changed Mon Jan 03 2011 | ||

stevan | pigworker: hi, you reckon partial refinements a la the "when is a type refinement an inductive type" paper are possible in the ornament setting? the deletion of info you mention in the discussion isn't quite the same thing, or? | 03/01 10:55 |

pigworker | stevan: It's trivial to do partial refinement in the ornament setting. | 03/01 12:12 |

roconnor | Where can I get Simmon's and Licata's Abstraction Theorem code? | 03/01 14:59 |

stevan | hmm | 03/01 21:22 |

stevan | i'll have to give that a try... | 03/01 21:23 |

--- Day changed Tue Jan 04 2011 | ||

sully | does there exist a pastebin with agda syntax highlighting? | 04/01 02:24 |

sully | (I think I know the answer to this question.) | 04/01 02:24 |

pumpkin | no, but one is coming as soon as I get some time to polish up my agda syntax highlighter so chrisdone can put it into hpaste.org | 04/01 02:25 |

pumpkin | I've given up trying to give ETAs on it though | 04/01 02:25 |

sully | oh, cool | 04/01 02:26 |

-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal] | 04/01 10:08 | |

--- Day changed Wed Jan 05 2011 | ||

yrlnry | pigworker: I am intrigued by your very recent tweet "I think it's important to emphasize the extent to which a bit of dependent typing can improve basic hygiene standards, with not much proof." | 05/01 16:15 |

yrlnry | I would be grateful if you could elaborate a bit. | 05/01 16:15 |

pigworker | I just mean that there's plenty of stuff you can do if you just want a little more precision, but maybe not total correctness, without writing much more than the type and the program. | 05/01 16:25 |

Saizan | which is roughly the area haskell gadts try to cover | 05/01 16:29 |

pigworker | yeah, and the benefits are already clear; the static-dynamic separation is annoyingly rigid, though | 05/01 16:35 |

yrlnry | What kind of stuff? | 05/01 16:39 |

Saizan | i'd like some guarantee about forcing/erasure for those gadts values that are known at compile time though, and maybe something like coq modulo theories for type families, so i wouldn't even need to pattern match on proof terms to make things typecheck | 05/01 16:41 |

--- Day changed Thu Jan 06 2011 | ||

copumpkin | http://hpaste.org/42787/data_airty | 06/01 01:22 |

copumpkin | damn typos | 06/01 01:22 |

copumpkin | anyway, is that just crazy talk? | 06/01 01:22 |

copumpkin | I feel like it would be possible for me to write my families manually like that with equality proofs and sigmas | 06/01 01:25 |

copumpkin | without the data notation | 06/01 01:25 |

pigworker | seems a bit lurid to me; can't you parametrize by a universe or something? | 06/01 01:27 |

copumpkin | oh, I don't need it | 06/01 01:28 |

copumpkin | it just occurred to me and was wondering if it was possible | 06/01 01:28 |

pigworker | it takes some heavy staring to see why it might make sense; I'm surprised it's rejected, but pleased | 06/01 01:30 |

copumpkin | would epigram reject it? | 06/01 01:32 |

copumpkin | either of them | 06/01 01:32 |

copumpkin | beware the whore naturals | 06/01 04:10 |

copumpkin | http://snapplr.com/vkbv | 06/01 04:10 |

copumpkin | pigworker: do you know what happened to the 5th part of your lectures on http://www.cs.uoregon.edu/Activities/summerschool/summer10/curriculum.html ? | 06/01 17:14 |

copumpkin | the link is a 404 | 06/01 17:14 |

pigworker | not a clue | 06/01 17:14 |

copumpkin | damn, I've emailed the site maintainer | 06/01 17:15 |

copumpkin | I'll see if they know :) | 06/01 17:15 |

pigworker | my involvement with the video stopped when they pressed stop | 06/01 17:15 |

copumpkin | ah okay | 06/01 17:16 |

djahandarie | Ooh, these are neat | 06/01 17:56 |

copumpkin | they sure are | 06/01 17:57 |

copumpkin | only one missing is pigworker's last though | 06/01 17:57 |

djahandarie | Lunch break is over though, will need to continue this video journey another day :( | 06/01 17:58 |

danten | pumpkin, the forth video contains both lecture 4 and 5 | 06/01 20:32 |

danten | fourth * | 06/01 20:33 |

pumpkin | oh, weird | 06/01 20:38 |

pumpkin | hadn't gotten there yet, so didn't notice :) | 06/01 20:38 |

djahandarie | It is slightly odd when someone joins the room and replies to something they weren't here for, lol | 06/01 20:39 |

danten | hehe, always reads the logs :) | 06/01 20:40 |

pumpkin | :P | 06/01 20:41 |

pumpkin | I've received emails from NAD about things I've said in here | 06/01 20:41 |

pumpkin | and he's never in here | 06/01 20:41 |

pumpkin | speaking of which, I really need to get around to implementing the changes I said I'd make in the agda syntax highlighting support | 06/01 20:42 |

danten | I'm only receiving bug reports from him.. | 06/01 20:42 |

danten | ;) | 06/01 20:42 |

pumpkin | if I didn't know better, I'd think that orangesquash.org.uk domain belonged to me | 06/01 20:43 |

pumpkin | whose is it, anyway? | 06/01 20:43 |

danten | dunno | 06/01 20:43 |

danten | I think Laney | 06/01 20:44 |

jeltsch | Hi, is there a MIME type for Agda source code? | 06/01 21:13 |

sully | hm | 06/01 23:03 |

sully | when I try to load the "lists as polynomial functors" example from "Dependently Typed Programming in Agda" | 06/01 23:03 |

sully | emacs colors it yellow | 06/01 23:03 |

copumpkin | it might be due to universe polymorphism? | 06/01 23:03 |

copumpkin | what are the unresolved metas? | 06/01 23:03 |

sully | how do I determine that? | 06/01 23:04 |

copumpkin | it should print things like _206: Sort | 06/01 23:05 |

copumpkin | in the status window | 06/01 23:05 |

sully | Sort _167 | 06/01 23:05 |

copumpkin | oh yeah | 06/01 23:05 |

sully | _168 : _167 | 06/01 23:05 |

copumpkin | yeah | 06/01 23:05 |

copumpkin | so you probably have a f : {A} -> A -> ... | 06/01 23:05 |

copumpkin | or something like that | 06/01 23:05 |

copumpkin | where you just want to change that to {A : Set} | 06/01 23:05 |

sully | that did it | 06/01 23:06 |

sully | thanks | 06/01 23:06 |

copumpkin | np | 06/01 23:06 |

* sully also a little bit lost at this point in the tutorial | 06/01 23:06 | |

copumpkin | how so? | 06/01 23:06 |

sully | I feel like while the polynomial functor stuff might be great motivating examples for people who know anything at all about category theory | 06/01 23:07 |

copumpkin | oh :P | 06/01 23:07 |

copumpkin | yeah | 06/01 23:07 |

sully | yeah | 06/01 23:07 |

sully | mostly the problem is that I know absolutely nothing about category theory | 06/01 23:07 |

copumpkin | have you used much haskell? | 06/01 23:08 |

sully | except that it involves things like functors and arrow and endofunctors and Zygohistomorphic prepromorphisms | 06/01 23:09 |

sully | no, not much | 06/01 23:09 |

copumpkin | lol | 06/01 23:09 |

copumpkin | alright | 06/01 23:09 |

sully | I've played around with it some | 06/01 23:09 |

copumpkin | the functor-ness of this isn't too essential | 06/01 23:09 |

sully | to get some understanding of typeclasses and monads | 06/01 23:09 |

copumpkin | but have you come across things like nat = mu x. 1 + x ? | 06/01 23:09 |

sully | but I've spent most of my time in Standard ML | 06/01 23:10 |

sully | yeah. | 06/01 23:10 |

copumpkin | that's pretty much what this is about | 06/01 23:10 |

copumpkin | list a = mu x. 1 + a * x | 06/01 23:10 |

copumpkin | mu is the mu they have in there | 06/01 23:10 |

copumpkin | and you get * and + and 1 and 0 | 06/01 23:10 |

sully | well, I guess actually I've spent most of my time in C, but... :P | 06/01 23:10 |

* sully nods | 06/01 23:10 | |

copumpkin | actually no 0 | 06/01 23:10 |

sully | (or maybe C++; every intership I've ever had has involved writing C++) | 06/01 23:11 |

sully | (sigh.) | 06/01 23:11 |

copumpkin | but it's basically arithmetic of that sort, and it turns out any such structure can be mapped generically, which makes it into a functor | 06/01 23:11 |

* sully nods | 06/01 23:11 | |

sully | (a friend of mine took a category theory class so that he could understand the statement "A monad is just a monoid in the category of endofunctors, what's the problem?") | 06/01 23:14 |

copumpkin | :P | 06/01 23:14 |

sully | apparently all of the pieces came together on the last day of class | 06/01 23:15 |

copumpkin | awesome | 06/01 23:15 |

--- Day changed Fri Jan 07 2011 | ||

Saizan | dolio: iirc you said with IR you can embed a whole tower of universes into Set, do you have the code handy? | 07/01 11:18 |

dolio | http://code.haskell.org/~dolio/agda-share/universes/ | 07/01 11:19 |

dolio | Hierarchy, in particular. | 07/01 11:24 |

Saizan | btw, was IRDataHierarchy typechecking as it is? it doesn't pass the positivity check on Fix with darcs Agda | 07/01 11:28 |

dolio | I don't remember. | 07/01 11:29 |

dolio | Is Fix not part of the universes? | 07/01 11:29 |

dolio | Because if so, that's kind of interesting. | 07/01 11:30 |

dolio | Back when Conor first proposed it, when I went to generate html, I had an old version of the agda executable that rejected it due to a positivity check. | 07/01 11:31 |

dolio | But an updated Agda at the time allowed it. | 07/01 11:31 |

Saizan | my current one doesn't, Fix is used in the decoding function of one of the universes there | 07/01 11:32 |

dolio | Yes. But stuff that comes later in the file wouldn't cause it to fail the positivity checker. | 07/01 11:32 |

dolio | It fails here, too. | 07/01 11:33 |

dolio | For whatever version I have. | 07/01 11:33 |

dolio | I actually found it hard to believe that it was accepted. | 07/01 11:33 |

Saizan | anyhow, i see in Hierarchy that the "trick" is to spell it out to agda that the base universe doesn't have a code for U | 07/01 11:34 |

dolio | Well, there's no universe inside it. | 07/01 11:35 |

dolio | If you look at the IRDataHierarchy one, you can see that I use ⊥ as the lowest universe, but then make the eventual U never rever to that. | 07/01 11:36 |

Saizan | yeah, but i was trying to do the same with a single data definition, instead of two, and the positivity checker stopped me | 07/01 11:36 |

dolio | So the lowest universe that you actually use would have a code for a lower universe, but it's just the empty type. | 07/01 11:37 |

dolio | And that way of coding things is a little nicer. | 07/01 11:38 |

dolio | Because you don't have to do case analysis on various 'ns' to figure out whether you're in the lowest universe, and thus need to use different codes. | 07/01 11:39 |

dolio | All U n have the same codes. | 07/01 11:39 |

Saizan | i see | 07/01 11:39 |

dolio | Pi and such over different universes is still a mess, though. | 07/01 11:40 |

dolio | Conceivably you can define any Pi type that Agda will accept with its built-in universes, but all the lifting into lub universes is a lot of busy work. | 07/01 11:41 |

dolio | Especially if you want to parameterize over the levels. | 07/01 11:41 |

dolio | And I've tried writing a Pi combinator that auto-lifts its two arguments into a lub universe, but it ended up being very difficult for reasons I can't really recall. | 07/01 11:42 |

Saizan | what's also maybe suboptimal is that the image of T doesn't give you types like (a : Set) -> a -> a, but (a : U) -> T a -> T a | 07/01 11:44 |

Saizan | though i guess the former would cover too many things | 07/01 11:45 |

dolio | Yeah, the thing is, terms with type T (pi u \a -> a => a) or whatever needn't be parametric. | 07/01 11:53 |

dolio | Since the Us are defined inductively, you can do type case, effectively. | 07/01 11:54 |

dolio | Which kind of trivially guarantees that they don't have a type like (a : Set) -> a -> a, because terms with that type must be parametric. | 07/01 11:55 |

dolio | pigworker: So, it seems that the Agda positivity checker has gone back to rejecting your induction-recursion encoding. | 07/01 12:31 |

dolio | As of early December, at least. | 07/01 12:33 |

pigworker | dolio: I'll investigate. | 07/01 13:05 |

dolio | Apparently you're working in a fragile area. | 07/01 13:07 |

dolio | As you may recall, I have an old copy of the agda executable that also rejects it. | 07/01 13:07 |

dolio | I don't know what tweaks they've been doing to the checker, but it's switched its opinion of your code twice now (at least). | 07/01 13:08 |

dolio | Also, SHE seems not to compile on GHC 7. | 07/01 13:12 |

dolio | Or maybe it's a new mtl thing. | 07/01 13:13 |

dolio | With redundant applicative instances. | 07/01 13:13 |

copumpkin | yeah, I ran into that too yesterday (the SHE not compiling) | 07/01 14:45 |

copumpkin | if you just comment out an alternative instance it works | 07/01 14:45 |

pigworker | copumpkin: which alternative instance? | 07/01 16:07 |

copumpkin | there's one for L, which is StateT, in HaLay.hs | 07/01 16:08 |

pigworker | now derived? | 07/01 16:08 |

pigworker | I mean, supplied? | 07/01 16:08 |

copumpkin | apparently that's already magically an instance | 07/01 16:08 |

copumpkin | yeah | 07/01 16:08 |

pigworker | about time | 07/01 16:08 |

copumpkin | it might be new in mtl 2, assuming you don't have an upper bound on your mtl dependency? | 07/01 16:09 |

copumpkin | yeah, you don't | 07/01 16:09 |

copumpkin | so it was using mtl2 | 07/01 16:09 |

dolio | mtl2 just repackages transformers, which has the applicative instances. | 07/01 16:09 |

pigworker | I'm clueless about this stuff. | 07/01 16:10 |

copumpkin | also, you mentioned in one of those videos that SheSingleton could be a GA data family (I love those, and use them all over the place) | 07/01 16:10 |

pigworker | oh, it is now, I think | 07/01 16:10 |

copumpkin | oh cool | 07/01 16:10 |

copumpkin | hadn't looked | 07/01 16:10 |

copumpkin | GHC should support custom code preprocessors with associated custom error postprocessors! | 07/01 16:11 |

dolio | What's new in 0.3, by the way? | 07/01 16:12 |

copumpkin | the superclass instance stuff that people have been talking about in that huge thread, I think | 07/01 16:12 |

dolio | That was in 0.2. | 07/01 16:12 |

pigworker | 0.3 is a bugfix on 0.2, which added default superclass instances | 07/01 16:12 |

copumpkin | oh | 07/01 16:12 |

dolio | Ah. | 07/01 16:12 |

pigworker | I noticed I'd screwed up the (trivial, non-)treatment of fundeps, and other things like that. | 07/01 16:13 |

pigworker | dolio: is it my Alg-IIR.agda file which no longer positivity-checks? | 07/01 16:14 |

dolio | Right. | 07/01 16:14 |

pigworker | if so, that's an incentive not to upgrade... | 07/01 16:14 |

dolio | Heh. | 07/01 16:15 |

pigworker | but I still have botched record constructors, which is really annoying | 07/01 16:15 |

dolio | I was considering bringing it up on the mailing list. | 07/01 16:15 |

Saizan | the two might be related, does it check if Sg is a data? | 07/01 16:15 |

pigworker | you tell me; I'm not getting the symptoms | 07/01 16:16 |

dolio | Although, I guess the lesser Descs don't require more powerful datatypes than they encode themselves. | 07/01 16:19 |

dolio | And there's no reason for me to suspect that an inductive-recursive definition of codes for inductive-recursive definitions should be less likely to work. | 07/01 16:20 |

pigworker | no, and Func is strictly positive in X, by the looks of things | 07/01 16:21 |

dolio | I think what it comes down to is that part of the definition is too opaque for the checker to see through. | 07/01 16:22 |

dolio | And in those situations, it assumes the worst. | 07/01 16:22 |

pigworker | yeah | 07/01 16:22 |

djahandarie | Whoa, this ala thing is pretty neat | 07/01 17:19 |

djahandarie | ...and it doesn't even need SHE does it? | 07/01 17:24 |

icarroll | I'm wondering how to use records like haskell type classes. Is there any documentation or code I could look at? | 07/01 23:53 |

icarroll | I've done a number of searches and haven't found anything. | 07/01 23:53 |

icarroll | I guess no one's home | 07/01 23:59 |

icarroll | :( | 07/01 23:59 |

--- Day changed Sat Jan 08 2011 | ||

dolio | pigworker: It breaks termination? I wasn't expecting that. | 08/01 00:40 |

pigworker | I was. | 08/01 00:51 |

dolio | pigworker: So, 'progress : {A : Set} {x y : A} -> x == y -> x == y ; progress _ = trustMe' is a problem? | 08/01 15:38 |

dolio | Same as making equality proofs irrelevant? | 08/01 15:38 |

pigworker | The rules are that you only use the unsafe trustMe to define extensionality. After that, no cheating! | 08/01 16:41 |

pigworker | er, sorry, dolio: ping, see above | 08/01 16:42 |

pigworker | But you're right, if that was the unsafeTrustMe, there would be trouble. | 08/01 16:44 |

dolio | pigworker: One part of the original message was about whether it was safe to use trustMe as long as you only added consistent axioms. | 08/01 19:08 |

dolio | Even just adding extensionality will cause non-normalizing terms? | 08/01 19:09 |

pigworker | If you implement extensionality with primUnsafeTrustMe, you get non-normalizing terms. | 08/01 19:32 |

pigworker | dolio: and if you implement extensionality with the safe primTrustMe, you lose canonicity | 08/01 19:36 |

dolio | Well, the latter doesn't surprise me, if I understand canonicity correctly. You'd have values of type f == g that get stuck on primTrustMe because they aren't definitionally equal. | 08/01 19:40 |

dolio | f and g aren't, even. | 08/01 19:40 |

dolio | Is there a simple example of where getting stuck like that prevents a loop? | 08/01 19:41 |

pigworker | you certainly need to get stuck sometimes to prevent loops | 08/01 19:46 |

pigworker | taking refl : f == g is rather unstuck, when f and g are only extensionally equal | 08/01 19:49 |

dolio | Well, yes, it's unstuck. | 08/01 19:53 |

dolio | I guess, if you have a false (forall x. f x == g x) in your context, you can then get an inappropriate refl : f == g? | 08/01 19:53 |

dolio | Which should actually be stuck on the assumed (forall x. f x == g x). | 08/01 19:54 |

dolio | Or something like that. | 08/01 19:54 |

pigworker | you don't even need a false statement of that form | 08/01 19:54 |

pigworker | although you do need a false statement somewhere | 08/01 19:55 |

pigworker | the "only consistent axioms" condition is a red herring, as you can always have a false hypothesis | 08/01 19:55 |

dolio | Right. | 08/01 19:56 |

pigworker | I'd spill the beans, but I'm fed up being a spoilsport. People should learn to spoil their own sport. | 08/01 20:05 |

dolio | :) | 08/01 20:05 |

--- Day changed Sun Jan 09 2011 | ||

pigworker | Does Agda allow irrelevant .(a : A) -> B a these days? | 09/01 16:43 |

Saizan | that's a parse error, even | 09/01 17:02 |

--- Day changed Mon Jan 10 2011 | ||

djahandarie | pigworker, I have a version of your ala with (Newtype n' o | 10/01 04:38 |

djahandarie | Agh | 10/01 04:38 |

copumpkin | aghla? | 10/01 04:38 |

djahandarie | (Newtype n o, Newtype n' o') => and one with just (Newtype n o) => | 10/01 04:39 |

djahandarie | Seems like you decided to switch from one to the other at one point though I'm not sure why :o) | 10/01 04:39 |

pigworker | djahandrie: I can't remember what the issues were. There's no especially good reason to force the inner and outer newtypes to coincide on the nose. | 10/01 08:58 |

djahandarie | Okay. I guess I'll just find out for myself then heh | 10/01 09:04 |

--- Log closed Mon Jan 10 14:16:52 2011 | ||

--- Log opened Mon Jan 10 14:17:47 2011 | ||

-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal] | 10/01 14:17 | |

-!- Irssi: Join to #agda was synced in 79 secs | 10/01 14:19 | |

--- Day changed Tue Jan 11 2011 | ||

copumpkin | I wonder how I'd go about proving that applicative parsers recognize no more than context-free languages | 11/01 19:32 |

dolio | Sounds difficult. | 11/01 19:34 |

dolio | Actually, it might not be as difficult as it sounds at first, I guess. | 11/01 19:35 |

dolio | Because the beauty of applicatives is that the 'T' in 'f T' is superfluous. | 11/01 19:36 |

dolio | You cannot observe the T to decide what kind of parsers to make. | 11/01 19:36 |

copumpkin | I guess I'd need to come up with a convenient (for this proof) definition of what it means to be context-free | 11/01 19:36 |

dolio | So what you need to do, is figure out what recognizer operations the applicative combinators correspond to, and prove that those recognize context free languages. | 11/01 19:37 |

djahandarie | Maybe you could connect it with the SK combinator calculus? *random thought* | 11/01 19:37 |

--- Day changed Wed Jan 12 2011 | ||

djahandarie | pigworker, possibly of interest to you http://althack.org/Data-Newtype.html :) | 12/01 00:31 |

djahandarie | Going to throw it on Hackage later today | 12/01 00:32 |

pigworker | Yes, it is interesting. I can't remember whether the associated type version works better or worse, but fundeps are fine for now... | 12/01 00:34 |

djahandarie | pigworker, I did the associated type version | 12/01 00:34 |

djahandarie | But it blows up on GHC < 7 | 12/01 00:34 |

djahandarie | So I decided to go with this for now | 12/01 00:34 |

pigworker | curious; a bit of a rat's nest, that | 12/01 00:35 |

djahandarie | http://althack.org/Newtype.hs the code | 12/01 00:36 |

copumpkin | noooo | 12/01 00:36 |

copumpkin | who needs GHC < 7 anyway | 12/01 00:36 |

djahandarie | It'd be nice if there was some way to force GHC to automatically write these instances... | 12/01 00:36 |

djahandarie | Maybe I could write an extension? | 12/01 00:37 |

* djahandarie has never ventured into those lands | 12/01 00:37 | |

copumpkin | there's a more general deriving mechanism being written as we speak | 12/01 00:37 |

copumpkin | so with any luck that'll come in the not-too-distant future | 12/01 00:37 |

djahandarie | Doesn't deriving always somehow related to the type that then newtype wraps though? | 12/01 00:37 |

djahandarie | relate* | 12/01 00:37 |

copumpkin | this is a general deriving mechanism for anything, not just newtypes | 12/01 00:38 |

djahandarie | Ah, neat | 12/01 00:38 |

pigworker | generating Newtype instances from newtype declarations would not be so tricky with SHE | 12/01 00:38 |

copumpkin | of course, you wouldn't want these instances unless you ask for them | 12/01 00:38 |

djahandarie | No, make them anyways!! | 12/01 00:38 |

copumpkin | lol | 12/01 00:38 |

pigworker | but it's nicer if it's built in | 12/01 00:38 |

copumpkin | yeah | 12/01 00:38 |

sully | what does BUILTIN LIST do, exactly? | 12/01 03:27 |

sully | does it allow convenient notation for lists, and if so what is the syntax? | 12/01 03:27 |

sully | or, alternately, is any of this documented anywhere? | 12/01 03:28 |

copumpkin | I hadn't even come across that | 12/01 03:28 |

dolio | It makes agda do certain list computations using Haskell lists behind the scenes, I think. | 12/01 03:34 |

dolio | The same is true of built-in pragmas for natural numbers. They're why you can actually do appreciable arithmetic in Agda. | 12/01 03:35 |

dolio | If it were actually doing unary computations something like 10^10 would probably force you to reboot. | 12/01 03:36 |

--- Log closed Wed Jan 12 11:10:25 2011 | ||

--- Log opened Wed Jan 12 11:10:32 2011 | ||

-!- Irssi: #agda: Total of 40 nicks [0 ops, 0 halfops, 0 voices, 40 normal] | 12/01 11:10 | |

-!- Irssi: Join to #agda was synced in 83 secs | 12/01 11:11 | |

--- Day changed Fri Jan 14 2011 | ||

jlouis | That hole thing in Agda2's Emacs mode is badass | 14/01 18:57 |

jlouis | It basically programs the solutions to the exercises for you | 14/01 18:57 |

Saizan | even more so with the auto command | 14/01 19:03 |

ccasin | Are agda's irrelevant arguments basically an implementation of ICC*, or are the something else? | 14/01 19:08 |

ccasin | *they | 14/01 19:08 |

Saizan | ..there are so many -CC | 14/01 19:10 |

ccasin | :) | 14/01 19:20 |

ccasin | Here I'm thinking about the algorithmic variant of the implicit calculus of constructions | 14/01 19:20 |

ccasin | I think the paper was by Barras and Bernardo | 14/01 19:21 |

ccasin | it's also essentially the same system as EPTS, from Nathan Linger's thesis | 14/01 19:21 |

jlouis | Heh, I am in a tutorial where all ASCII is now UTF8. I guess I can as well learn the stdlib :) | 14/01 20:38 |

jlouis | though, where is 'refl' located? | 14/01 20:43 |

jlouis | or rather something that lets me do the equivalent of an ascii == | 14/01 20:46 |

Saizan | Relation.Binary.PropositionalEquality | 14/01 20:46 |

jlouis | Saizan: thank you! | 14/01 20:58 |

dolio | Irrelevant arguments are like EPTS/ICC/etc. | 14/01 21:15 |

dolio | Except you can't be dependent over them yet. | 14/01 21:15 |

dolio | So, .A -> B, but not .(x : A) -> B x | 14/01 21:15 |

dolio | mini agda has the latter, though, I think. | 14/01 21:16 |

copumpkin | oh | 14/01 21:16 |

dolio | Amongst other things. | 14/01 21:16 |

ccasin | dolio: thanks | 14/01 21:39 |

jlouis | Heh, this STLC from the tutorial is around 10 times as large as one in Twelf :P | 14/01 22:43 |

jlouis | line-wise | 14/01 22:43 |

dolio | Twelf has lambda terms as built-in language constructs. | 14/01 22:43 |

jlouis | exactly, it is alsmost cheating | 14/01 22:44 |

jlouis | but I am not sure it will keep being like that as I build larger things | 14/01 22:44 |

jlouis | Twelf has no library for instance | 14/01 22:44 |

dolio | I suppose I should say, twelf has them as a built-in data structure (with very nice properties). | 14/01 22:48 |

dolio | Agda has lambda terms built in, but they're used primarily for computation. | 14/01 22:49 |

--- Day changed Sat Jan 15 2011 | ||

sully | does there exist documentation of what all the BUILTINs are? | 15/01 20:07 |

sully | (I think I already know the answer to most questions beginning with "does there exist documentation" when agda is being discussed, but...) | 15/01 20:08 |

--- Log closed Sat Jan 15 20:38:48 2011 | ||

--- Log opened Sat Jan 15 20:38:55 2011 | ||

-!- Irssi: #agda: Total of 35 nicks [0 ops, 0 halfops, 0 voices, 35 normal] | 15/01 20:38 | |

-!- Irssi: Join to #agda was synced in 85 secs | 15/01 20:40 | |

--- Day changed Sun Jan 16 2011 | ||

freiksenet | is "indexed type" a synonym to "dependent type'? | 16/01 15:53 |

ccasin | sometimes it is used in a more specialized way | 16/01 16:01 |

ccasin | to refer to types that have non-uniform dependent arguments | 16/01 16:02 |

ccasin | for example, vec's natural number argument, but not its type argument | 16/01 16:02 |

freiksenet | aha. | 16/01 16:02 |

freiksenet | ccasin: thanks | 16/01 16:03 |

ccasin | no problem | 16/01 16:04 |

ski | re uniform dependent arguments, i tried to write | 16/01 16:28 |

ski | foo (A : Set) (a : A) : P a -> ... | 16/01 16:28 |

ski | foo A a (...) = ... | 16/01 16:28 |

ski | but it didn't like that type signature :/ | 16/01 16:29 |

ski | (it seemed to me that if that worked in `data' declarations, it would also work in normal bindings) | 16/01 16:29 |

ccasin | in data declarations it has a special meaning though | 16/01 16:29 |

ski | yeah .. but i was wanting "the same" meaning in `foo' above | 16/01 16:29 |

ccasin | fair enough | 16/01 16:30 |

ski | though maybe that's sortof useless .. hm | 16/01 16:30 |

ski | hm, i suppose `foo' is not a good example | 16/01 16:31 |

ski | bar (n : Nat) : ... | 16/01 16:31 |

ski | is better | 16/01 16:31 |

ski | so i was thinking this should enforce `bar' to be "parametric" in the `n' argument | 16/01 16:31 |

ski | so each defining equation would start with `bar n' (not matching on `n') | 16/01 16:32 |

ski | but now that i think on it again, i'm not sure one could stop `n' from being matched on "later" (and if one could, would it be useful ?) | 16/01 16:32 |

ski | (at the time i was playing with alternate definitions for a type. one used `data', another was a plain definition, defining the type to be `Unit' in one case, &c.) | 16/01 16:33 |

ski | fwiw, this was it : | 16/01 16:36 |

ski | trans_=<_<_O : {m n o : Ordinal} -> n >=O m -> n <O o -> m <O o | 16/01 16:36 |

ski | i wanted to say in the type (so that it was statically checked), that the definition didn't (by itself) match on the `n >=O m' argument | 16/01 16:37 |

Saizan | you could use the irrelevant arguments feature there, maybe | 16/01 16:38 |

ski | (it would in the recursive case pass that argument to another (mutually recursive) function which would match on it, however) | 16/01 16:38 |

ski | hm .. how does that work ? | 16/01 16:38 |

Saizan | the syntax would be: trans_=<_<_O : {m n o : Ordinal} -> .(n >=O m) -> n <O o -> m <O o | 16/01 16:39 |

ski | (i mean if you say `data Foo (n : Nat) : Set where F : Bar n -> Foo n', nothing is hindering `Bar' for being indexed on its natural number argument .. only `Foo' is forbidden from that) | 16/01 16:39 |

Saizan | but then you can use that argument only in an irrelevant position | 16/01 16:39 |

ski | ok, so then i couldn't pass it to another function that matches (non-irrelevantly) on it, right ? | 16/01 16:39 |

Saizan | yeah, unless you use the result of that function only in a place marked as irrelevant | 16/01 16:41 |

ski | yeah | 16/01 16:41 |

Saizan | the release notes for 2-2-8 should have the details | 16/01 16:41 |

ski | anyway, you see how with `data Foo (n : Nat) ...' only `Foo' is forbidden to "match" on `n' ? | 16/01 16:42 |

ski | i wanted that, for an ordinary definition | 16/01 16:42 |

Saizan | i don't think there's any support for that | 16/01 16:42 |

ski | ok | 16/01 16:42 |

ski | (another thing i was wanting was to have uniform arguments after non-uniform ones .. but i suppose that's not possible :) | 16/01 16:46 |

ski | (that would allow me to say `m =<O n' instead of `n >=O m' above :) | 16/01 16:46 |

ski | (.. of course i can make a definition, but that doesn't help me when matching, since i can't make "derived constructors/patterns") | 16/01 16:47 |

Saizan | how would you use such a property btw? it doesn't seem like you can derive much from knowing trans_=<_<_O won't match on (n >=O m) | 16/01 16:49 |

ski | well, i'm not sure :) | 16/01 16:51 |

ski | i wanted the `data' and the equality definitions to correspond more to each other | 16/01 16:51 |

ski | (i can't say exactly where uniform arguments of `data'-definitions are used either, btw) | 16/01 16:52 |

Saizan | for data they are mostly useful when quantifying over them in constructors would put the type you're defining in a higher universe, otherwise it's just a syntactical convenience | 16/01 16:57 |

ski | ah, ok | 16/01 16:58 |

ski | interesting | 16/01 16:58 |

Saizan | e.g. data List : Set -> Set where [] :: (A : Set) -> List A would be a type error because ((A : Set) -> List A) : Set1 | 16/01 17:04 |

ski | *nod* | 16/01 17:26 |

dolio | You can make new indexed types using parameterized types and existing indexed types (like the equality type), though. | 16/01 17:32 |

dolio | So parameters for types are somewhat different than irrelevant arguments. | 16/01 17:32 |

dolio | If a type had an irrelevant parameter, that would be even more restrictive. The type would not be able to depend on that argument, so it effectively would be forced to be phantom. | 16/01 17:33 |

dolio | (I think, at least.) | 16/01 17:34 |

--- Day changed Mon Jan 17 2011 | ||

jlouis | Has anybody tried to build something like (List N) where N can be ordered and the list is sorted by force of a dependent type? | 17/01 20:05 |

dolio | Yes. I'm sure that's been done. | 17/01 20:05 |

dolio | I've probably done it at some point. | 17/01 20:05 |

jlouis | I tried with non-empty lists where I have SList N N where the latter N is the minimal element in the list | 17/01 20:06 |

cads | I have a question about agda. | 17/01 20:07 |

cads | I want to try an experiment, to learn it | 17/01 20:07 |

jlouis | dolio: do you have a hint as to what you did? | 17/01 20:07 |

cads | And what I'd like to do is to take the basic definitions and theorems from my calculus course and formalize them in agda | 17/01 20:07 |

jlouis | my stdlib-fu is too weak to be able to grab the right tools in the toolbox unfortunately | 17/01 20:08 |

cads | is it easy to do this, or do I have to work with some nontrivially finitized constructive version of the theory? | 17/01 20:08 |

dolio | Formalizing calculus would be a lot of work. | 17/01 20:08 |

jlouis | you'd need the Reals for starters, right? | 17/01 20:09 |

cads | the definitions are very simple but they almost all rely on quantification over uncountable sets, or infinite sequences and stuff | 17/01 20:09 |

cads | jlouis, definitely | 17/01 20:09 |

cads | dolio, what would be the steps I'd have to take to accomplish it? | 17/01 20:10 |

dolio | It rather depends. | 17/01 20:10 |

cads | could I use some existing analysis framework and specialize it to plain calculus of one variable? | 17/01 20:11 |

dolio | You could try developing constructive reals, and doing calculus with that. | 17/01 20:11 |

dolio | Or you could postulate a bunch of axioms about real numbers that are sufficient to just reason in the way that calculus requires. | 17/01 20:11 |

cads | really I just want to hold something that can prove every problem in my book that has a solution | 17/01 20:11 |

dolio | But I don't expect either one of those options to be very easy. | 17/01 20:12 |

cads | something built from what was available, and provably correct | 17/01 20:12 |

cads | hmm | 17/01 20:12 |

dolio | It's possible there are Coq libraries for this sort of thing. | 17/01 20:12 |

cads | basic caclulus doesn't invoke many of the real strange properties of the reals | 17/01 20:13 |

cads | dolio, that gives me an idea | 17/01 20:15 |

dolio | jlouis: So, playing a bit now, it's a little more of a pain than I thought. | 17/01 20:16 |

cads | I'll write the definitions from the book and see what properties of the real numbers I'm required to postulate for them to make sense | 17/01 20:16 |

dolio | At least, for a 'the head is less than the head of the tail' layout. | 17/01 20:16 |

jlouis | dolio: yeah. Perhaps one should go with the idea of bounds instead | 17/01 20:18 |

Saizan | http://www.e-pig.org/epilogue/?p=690 <- this should be portable to agda | 17/01 20:19 |

dolio | jlouis: There's an easy inductive-recursive formulation using All. | 17/01 20:20 |

jlouis | Saizan: mmm, I considered that as well | 17/01 20:20 |

jlouis | dolio: I still need to grasp what inductive-recursive means :) | 17/01 20:20 |

dolio | _::_ : forall h t -> All (h <) t -> SList | 17/01 20:20 |

jlouis | Just to be clear, All P t means that P(x) forall x in t ? | 17/01 20:22 |

dolio | Right. | 17/01 20:22 |

dolio | So, the head is less than (or equal to) all the elements of the tail. | 17/01 20:22 |

dolio | And All is mutually defined by recursion. | 17/01 20:23 |

jlouis | I can see how one should be able to insert elements based on discriminating on that | 17/01 20:24 |

dolio | http://hpaste.org/43107/sorted_lists | 17/01 20:24 |

dolio | On a side note, why does Data.Unit have a <=? | 17/01 20:25 |

dolio | _ <= _ = True | 17/01 20:25 |

jlouis | the unit element is equal to the unit element? | 17/01 20:25 |

dolio | Right. | 17/01 20:26 |

jlouis | though the < doesn't make much sense | 17/01 20:26 |

dolio | Empty doesn't have one. | 17/01 20:26 |

jlouis | perhaps it is out of convenience | 17/01 20:26 |

jlouis | Empty has no inhabitation? | 17/01 20:26 |

dolio | Right. For all elements e and e', e <= e' vacuously. | 17/01 20:27 |

dolio | _<=_ : E -> E -> Set ; () <= () | 17/01 20:28 |

jlouis | I dunno really, but with () you can at least construct an element (namely ()) whereas that is impossible with Empty. Maybe that is the subtlety of the difference ? | 17/01 20:29 |

jlouis | I've been hacking Agda for... 2-3 days at max, so I can always claim lack of knowledge and innocense :) | 17/01 20:30 |

jlouis | dolio: I've been trying some discrimination against the definition you gave, but this fails: Any clue? http://hpaste.org/paste/43107/sorted_lists_annotation#p43108 | 17/01 21:53 |

jlouis | somehow I don't think x <=? y is the way to go | 17/01 21:53 |

jlouis | in particular, I have a hard time generating a specimen of All | 17/01 21:54 |

dolio | I expect you're going to want to prove a lemma like 'x < y -> All (_<_ y) zs -> All (_<_ x) zs'. | 17/01 21:55 |

jlouis | I've thought about a transitivity lemma of some kind for if All (_<=_ hd) tl and x <= hd, then surely I must be able to show All (_<_ x) tl | 17/01 21:55 |

jlouis | heh, that *almost* agrees modulo notation | 17/01 21:55 |

jlouis | I'll play around with it | 17/01 21:55 |

jlouis | http://hpaste.org/paste/43107/sorted_lists_annotation#p43112 heh that is kind-of a screeching halt I came to | 17/01 23:32 |

jlouis | The problem is mangling of 'All' again. We'd like to use the neg p proof we have been handed to show that _<=_ hd bounds (insert x tl), but.. that must require some mutuality probably | 17/01 23:34 |

jlouis | speaking of which... Twelf has several termination strategies. What does Agda have in that department? | 17/01 23:35 |

Saizan | almost nothing | 17/01 23:38 |

Saizan | there's a flag to disable the termination checker and another to increase the "depth", but other than that you can't control it | 17/01 23:39 |

jlouis | ok | 17/01 23:39 |

Saizan | btw, this SList is supposed to be in decresing order, or am i reading it wrong? | 17/01 23:41 |

Saizan | ah, yeah, it's me, i was reading (_≤_ hd) as a section | 17/01 23:42 |

jlouis | I started with the optimistic idea of defining sparse vectors like this | 17/01 23:47 |

jlouis | but this is a fine stepping stone | 17/01 23:47 |

Saizan | http://hpaste.org/paste/43107/sorted_lists_annotation#p43113 <- seems to work | 17/01 23:58 |

Saizan | the holes would need a ¬ (x ≤ hd) -> hd ≤ x lemma | 17/01 23:59 |

--- Day changed Tue Jan 18 2011 | ||

jlouis | mm | 18/01 00:01 |

jlouis | Saizan: it is interesting how the lemma needs to inspect the top two elements of the list | 18/01 00:05 |

jlouis | I was down that road but stopped it because "that never leads to anything, heh" | 18/01 00:05 |

Saizan | well, insert x tl inspects the first element of tl | 18/01 00:08 |

jlouis | exactly | 18/01 00:09 |

jlouis | Saizan: what is the strategy for showing: ¬ (x ≤ hd) -> hd ≤ x ? I have a hard time arguing around \bot-elim | 18/01 00:32 |

jlouis | with compare x y and eliminate impossible cases? | 18/01 00:33 |

jlouis | with x <=? y and play with yes p / no neg-p instances? | 18/01 00:33 |

jlouis | the latter doesn't seem to work | 18/01 00:34 |

jlouis | split on x , split on y, handle the four cases by deciding on x <=? y ? | 18/01 00:34 |

jlouis | ok, that last thing worked | 18/01 00:37 |

jlouis | only, no decider was needed, thanks rubber duck :) | 18/01 00:37 |

Saizan | :) | 18/01 00:39 |

Saizan | you need only 3 cases actually | 18/01 00:39 |

Saizan | lemma2 : ∀ {x hd} -> ¬ (x ≤ hd) -> hd ≤ x | 18/01 00:40 |

Saizan | lemma2 {x} {zero} ¬p = z≤n | 18/01 00:40 |

Saizan | lemma2 {zero} {suc n} ¬p = ⊥-elim (¬p z≤n) | 18/01 00:40 |

jlouis | ah, yes | 18/01 00:40 |

Saizan | lemma2 {suc n} {suc n'} ¬p = s≤s (lemma2 (λ x → ¬p (s≤s x))) | 18/01 00:40 |

jlouis | if {y = zero} collapses | 18/01 00:40 |

jlouis | The automatic refinement and automatic search is a neat improvment over my Twelf-hacking | 18/01 00:41 |

Saizan | by automatic refinement you mean pattern matching changing the types? | 18/01 00:42 |

jlouis | C-c C-r | 18/01 00:42 |

jlouis | you can basically just go looking for what Agda wants and then slowly let it give things | 18/01 00:43 |

Saizan | ah, yeah, i wish i learned about it earlier | 18/01 00:45 |

ski | jlouis : both `=<' and `<' makes sense for both `Unit' and `Empty' .. | 18/01 07:42 |

dolio | They make sense, but I'm skeptical that they're of use more often than they need to be hidden to avoid conflicting with, say, the Nat versions. | 18/01 07:58 |

ski | hm .. can one associate unique values with types, somehow ? | 18/01 07:59 |

ski | i.e. like type classes, only with a guarantee that the instance is unique | 18/01 07:59 |

ski | .. though i suppose that mightn't be that useful in this circumstance anyway | 18/01 08:00 |

dolio | I don't think so, unless you'd accept defining a set of codes, and then an interpretation into sets and a function that gives the 'instances' for those types. | 18/01 08:02 |

ski | m .. for `Unit' and `Empty' there should be unique "weak"(?) and strict partial orders | 18/01 08:05 |

ski | but obviously not for naturals and more complicated stuff | 18/01 08:05 |

ski | anyway, i was thinking the orders for `Unit' and `Empty' might be useful to (semi- ?)automatically derive orders for more complicated types | 18/01 08:06 |

ski | i suppose they at least could be useful to manually derive orders, in a principled way | 18/01 08:07 |

ski | e.g. you could have combinators combining orders over constituent types into orders over compound types | 18/01 08:07 |

dolio | You could. | 18/01 08:08 |

ski | `lexicographic <A <B : WellOrder (A * B)',&c. | 18/01 08:08 |

dolio | It's far more frequent for me to import both Data.Unit and Data.Nat, though, than it is for me to need the ordering for, say, List Unit. | 18/01 08:09 |

ski | i wouldn't mind writing `=<U' or something like that for the order over `Unit' | 18/01 08:10 |

ski | (and similarly for naturals, &c.) | 18/01 08:10 |

jlouis | ski: how do you justify () < () ? | 18/01 12:34 |

jlouis | I somewhat don't grok its reflexive | 18/01 12:34 |

ski | jlouis : the `() < ()' doesn't prove reflexivity, it only defines `_<_' for `Empty' | 18/01 13:53 |

jlouis | ski: oh! | 18/01 13:53 |

ski | _<_ : Empty -> Empty -> Set | 18/01 13:53 |

ski | () < () | 18/01 13:53 |

ski | there's zero cases to consider, in the definition | 18/01 13:53 |

* jlouis nod | 18/01 13:54 | |

ski | however, this `_<_' still *is* reflexive, yes | 18/01 13:54 |

jlouis | how about the Unit then? | 18/01 13:54 |

jlouis | assuming Unit is the one-element inhabited type | 18/01 13:54 |

ski | `_=<_' as well as `_<_' can be defined, but only the former is reflexive (naturally) | 18/01 13:55 |

ski | in the former, `U =< U' is defined to be `Unit', so reflexivity will give `U' as proof for `U =< U' (the only case) | 18/01 13:56 |

ski | in the latter, `U < U' is defined to be `Empty', so reflexivity would need to prove `U < U' which is `Empty', which shouldn't be possible | 18/01 13:57 |

jlouis | ah, something clicked now | 18/01 13:57 |

ski | in the case of `_<_' for `Empty' (as well as `_=<', of course), there simply is no case to begin with. reflexivity similarly is provable simply because there's no element `e' in `Empty' to prove `e < e' (or `e =< e') for | 18/01 13:58 |

ski | (it's vacuously true) | 18/01 13:59 |

--- Day changed Wed Jan 19 2011 | ||

roconnor | given a least fixed point of a Functor F, we have A ~ F (A). What is the usual names for the two directions of the isormophism? fold and unfold? | 19/01 16:20 |

dolio | in and out | 19/01 16:35 |

roconnor | thanks | 19/01 16:43 |

--- Day changed Thu Jan 20 2011 | ||

copumpkin | jlouis: what's this clever agda code from you I hear of on the twitterverse? | 20/01 17:07 |

jlouis | copumpkin: Ralf defined 'Huttons Razor + an Exit (exception)' and then he asked, among other stuff: Define a function pure : Exp -> Bool. .. but it is so much more fun to do: data Exp : Bool -> Set where... of course :) | 20/01 17:40 |

jlouis | https://gist.github.com/4d2bdfb2d59116d641e6 | 20/01 17:40 |

jlouis | last 5 lines or so | 20/01 17:40 |

copumpkin | cool :) | 20/01 17:45 |

copumpkin | that could be done in haskell too though | 20/01 17:46 |

jlouis | copumpkin: Yes, GADTs right? | 20/01 17:47 |

jlouis | or an indexing trick? | 20/01 17:47 |

copumpkin | yeah, GADTs | 20/01 17:48 |

copumpkin | and type families to do the boolean operation | 20/01 17:48 |

jlouis | It is just that dependent types comes more natural to me than GADTs+families | 20/01 17:48 |

jlouis | for some odd reason | 20/01 17:48 |

djahandarie | Other way around for me :P | 20/01 17:48 |

djahandarie | Then again I still haven't done enough with Agda | 20/01 17:49 |

jlouis | I've been hacking a bit of Twelf and Coq before this | 20/01 17:50 |

copumpkin | does coq have inductive families? | 20/01 17:53 |

copumpkin | probably, I guess | 20/01 17:53 |

Saizan | in haskell you'd actually need a typeclass if you wanted a boolean to pattern match on :) | 20/01 17:54 |

ccasin | copumpkin: yes, but pattern matching on them sucks | 20/01 17:54 |

ccasin | both in the sense that it is terribly inconvenient and in the sense that it is actually a little weaker | 20/01 17:56 |

kosmikus | jlouis: you're at Dagstuhl then? what's the topic of the meeting? | 20/01 17:59 |

jlouis | kosmikus: nope, I am just trying to learn to juggle agda | 20/01 18:05 |

copumpkin | ccasin: ick | 20/01 18:06 |

ccasin | copumpkin: things are getting better though. mattam write a coq plugin that elaborates nicer agda-style pattern matching into coq (plus an assumption of Axiom K, which it the thing it is missing) | 20/01 18:07 |

ccasin | and there is reason to hope both the plugin and the missing axiom will make their way into coq proper | 20/01 18:07 |

copumpkin | what is this axiom K I keep hearing about? | 20/01 18:07 |

ccasin | it's also called the uniqueness of identity proofs | 20/01 18:07 |

ccasin | forall (A B : Set) (P Q : A = B), P = Q | 20/01 18:08 |

copumpkin | ah okay | 20/01 18:08 |

copumpkin | wait, only on sets? | 20/01 18:09 |

ccasin | no, I think any sort | 20/01 18:09 |

copumpkin | or A B : Set, x : A, y : B, p q : x == y, p == q | 20/01 18:09 |

ccasin | oh, right | 20/01 18:09 |

ccasin | that :) | 20/01 18:09 |

copumpkin | I see | 20/01 18:09 |

ccasin | I think maybe with just one Set, and no first assumption of equality | 20/01 18:09 |

ccasin | not sure if it matters | 20/01 18:09 |

ccasin | let me see | 20/01 18:10 |

ccasin | yes, its statement in the coq stdlib is: | 20/01 18:10 |

ccasin | forall (U : Type) (x y : U) (p1 p2 : x = y), p1 = p2 | 20/01 18:11 |

ccasin | http://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html | 20/01 18:11 |

ccasin | Sorry for the slipup :) | 20/01 18:11 |

ccasin | according to that page, Axiom K actually refers to an equivalent variant. I like it because it's quicker to write "Axiom K" than "Uniqueness of identity proofs" | 20/01 18:12 |

ccasin | anyway, this is independent of coq but true in agda, and it is important for "good" pattern matching. There is some push to add it to coq, though | 20/01 18:14 |

copumpkin | ah interesting | 20/01 18:23 |

copumpkin | it's because inductive families carry implicit equalities around a lot? | 20/01 18:23 |

ccasin | yes | 20/01 18:26 |

ccasin | in agda, when you pattern match it does all these substitutions on the types in the context | 20/01 18:27 |

ccasin | to resolve those equalities | 20/01 18:27 |

copumpkin | yeah | 20/01 18:27 |

ccasin | you can use this nice behavior to derive UIP | 20/01 18:28 |

ccasin | in coq, the pattern matching isn't so clean | 20/01 18:28 |

copumpkin | UIP? | 20/01 18:28 |

ccasin | uniqueness of identity proofs :) | 20/01 18:28 |

copumpkin | oh okay :P | 20/01 18:28 |

copumpkin | how computationally meaningful are the implicit arguments to constructors of http://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.html#875 ? | 20/01 19:02 |

copumpkin | cause otherwise a proof of n <= m is basically isomorphic to n | 20/01 19:03 |

copumpkin | even if not, the implicit m argument to s<=s has exactly the same structure as the smaller number | 20/01 19:04 |

ccasin | I'm not sure what "computationally meaningful" means here | 20/01 19:09 |

ccasin | but I agree proofs of n <= m have n constructors | 20/01 19:09 |

ccasin | err, (n+1), counting 0 | 20/01 19:10 |

copumpkin | well, Fin is basically equivalent to Nat, at runtime | 20/01 19:10 |

copumpkin | so could possibly be represented efficiently too | 20/01 19:10 |

ccasin | yes, I think so too for this datatype | 20/01 19:10 |

copumpkin | so Fin, <=, and Nat all look roughly the same at runtime, and any implicit parameters their constructors may have can usually be figured out from context (as far as I can tell) | 20/01 19:11 |

ccasin | I guess, one question to as is | 20/01 19:12 |

ccasin | oops | 20/01 19:12 |

ccasin | ignore that, sorry | 20/01 19:12 |

copumpkin | (it seems like Dec P could also be represented as a Bool at runtime, if P isn't decomposed for computation) | 20/01 19:12 |

ccasin | yes | 20/01 19:13 |

ccasin | Of course, with this representation a proof of (n <= m) doesn't give you enough information to figure out m | 20/01 19:13 |

copumpkin | it seems that any time you have an n <= m, you acquired it by <=?'ing two numbers, so it's non-local, but the information should be available somewhere :P | 20/01 19:14 |

copumpkin | that's pretty sketchy though, I guess | 20/01 19:14 |

ccasin | I agree, in a vague way :) | 20/01 19:14 |

copumpkin | well, n <= m ~~ (n, m) | 20/01 19:14 |

copumpkin | it'd be cute to have a compiler with fancy automated reasoning that for every natural, attempted to automatically prove (using presburger solver or real-closed field solver, or smt of some other sort) that n <= 2^wordsize, and if so, represents the number as a native word | 20/01 19:17 |

* copumpkin dreams on | 20/01 19:17 | |

copumpkin | it'd be nice if the standard library Category could be put into another namespace (Agda.Category.Functor/Monad?) somehow, making room for categories with proofs as the most general namespace version | 20/01 20:21 |

dolio | exists n. n <= m is one possible implementation of Fin (m+1). | 20/01 20:55 |

dolio | And if you use a sigma instead, you have redundant information. | 20/01 20:57 |

dolio | Storing both the n and the proof. | 20/01 20:57 |

copumpkin | yep | 20/01 20:57 |

dolio | Also, from what I gather, I wouldn't hold your breath for K in Coq. | 20/01 20:58 |

dolio | Since it seems to be getting used for work on the models of type theory in which K is inconsistent. | 20/01 20:58 |

ccasin | dolio: I guess that is voevodsky's work? | 20/01 22:08 |

dolio | Him at least. | 20/01 22:08 |

ccasin | I am still vaguely hopeful - mattam has indicated that he wants it and he's on the official coq team now | 20/01 22:08 |

dolio | Although I can't say I know any other folks on the job. | 20/01 22:08 |

ccasin | perhaps we will get it as an optional flag | 20/01 22:08 |

dolio | Yeah, that's a possibility. | 20/01 22:09 |

ccasin | I think these are the people working on the voevodsky stuff: | 20/01 22:09 |

ccasin | http://www.math.ias.edu/sp/univalent | 20/01 22:10 |

ccasin | though, as far as I know, he's the only one hacking in coq | 20/01 22:10 |

ccasin | well, scratch that | 20/01 22:10 |

ccasin | the second name on that site is Coquand | 20/01 22:10 |

dolio | He's the one you see on the mailing list, at least. | 20/01 22:10 |

ccasin | so I guess I'm wrong :) | 20/01 22:10 |

ccasin | yeah, actually, the whole description here is pitched in terms of using proof assistants. I thought they were just doing semantics. Neat! | 20/01 22:11 |

dolio | If you talk to Conor, I think he'll tell you that K isn't necessary for nice matching. What you need is some variety of substitutive heterogeneous equality | 20/01 22:12 |

dolio | And K just allows you to get that. | 20/01 22:12 |

dolio | Of course, I don't think Coq is more likely to adopt that as an alternative to K. | 20/01 22:13 |

ccasin | yeah, that sounds right | 20/01 22:13 |

ccasin | K is just what coq is missing | 20/01 22:13 |

ccasin | it's totally plausible that a different notion of definitional equality will do the same job | 20/01 22:14 |

ccasin | in fact, we're working on one in Trellys :) | 20/01 22:14 |

copumpkin | who the hell called it K? | 20/01 22:15 |

dolio | In Martin-Loef type theory, identity types are I, and identity elimination is J. | 20/01 22:15 |

dolio | So K is next in line. | 20/01 22:15 |

ccasin | interesting | 20/01 22:15 |

ccasin | people call it "Streicher's axiom K" | 20/01 22:16 |

ccasin | so maybe he is to blame | 20/01 22:16 |

dolio | Probably. But I can make up a rationale, at least. :) | 20/01 22:16 |

ccasin | certainly - I totally bought it :) | 20/01 22:17 |

--- Day changed Fri Jan 21 2011 | ||

lpjhjdh | Is it possible to show something like the following? http://hpaste.org/43178/xsxs | 21/01 02:02 |

lpjhjdh | I have no idea how to reduce x ∷ subst (Vec .A) n+0≡n (xs ++ []) | 21/01 02:02 |

lpjhjdh | I know the standard library just uses a more reasonable notion of equivalence | 21/01 02:03 |

Saizan | pattern match on n+0≡n, providing the right implicit n | 21/01 02:03 |

dolio | Yes, it is possible. | 21/01 02:04 |

lpjhjdh | interesting, I'll give it a shot, thanks | 21/01 02:05 |

lpjhjdh | actually I'm uncertain I understand what that grants me, would you mind explicating a bit? | 21/01 02:05 |

Saizan | mh, maybe it doesn't help | 21/01 02:06 |

Saizan | that should reduce the subst away though | 21/01 02:06 |

lpjhjdh | ah, thanks | 21/01 02:07 |

lpjhjdh | so since I know the shape of n to be "suc k" it reduces to "cong suc k" | 21/01 02:11 |

lpjhjdh | Sorry I don't actually quite understand how this is reducing actually. So I have a vector of size "k+1" and match with "n+0=n {m}" | 21/01 02:16 |

lpjhjdh | but then I'm not sure how to match on the result of type "m + 0 = m" | 21/01 02:17 |

lpjhjdh | bleh, sorry keep mixing up notation meatn to say "m+1" | 21/01 02:18 |

* Saizan is not finding a way to solve this either | 21/01 02:19 | |

dolio | I may have been over-zealous. If it is possible, it's likely to be painful. | 21/01 02:20 |

dolio | Because heterogeneous equality handles the non-definitionally-equal indices much better. | 21/01 02:21 |

Saizan | yeah | 21/01 02:22 |

lpjhjdh | I see, an interesting exercise. I'm content letting it go having brilliant folks such as yourselves note that it's painful :) | 21/01 02:23 |

lpjhjdh | thanks for the help | 21/01 02:23 |

dolio | For instance, trying to prove subst P eq Px = Px' | 21/01 02:23 |

dolio | Er. | 21/01 02:23 |

dolio | Trying to prove that in general is hard. | 21/01 02:23 |

dolio | That doesn't type as stated. | 21/01 02:24 |

lpjhjdh | Okay, so in general is it much easier to just come up with a good notion of equivalence and then prove things respect it? | 21/01 02:26 |

dolio | The problem here is that n + 0 and n are provably equal, but not definitionally equal. Heterogeneous equality is approximately the same as the regular homogeneous equality, but it doesn't require the types of the two terms to be definitionally equal. | 21/01 02:28 |

lpjhjdh | Ah, thanks | 21/01 02:29 |

dolio | You could look at the limitation of the homogeneous equality as being a little artificial. | 21/01 02:30 |

dolio | A concession to decidable checking, rather than 'this really should not work.' | 21/01 02:31 |

--- Day changed Sat Jan 22 2011 | ||

BMeph | Just curious, but does anyone see Agda getting to the point where it feels as clunky for an Agda user to work with Haskell, as it feels for a Haskell programmer to work with Ocaml? | 22/01 21:34 |

Saizan | for some things yes | 22/01 21:34 |

Saizan | though agda feels clunkier when termination checking hinders higher order programming | 22/01 21:35 |

Saizan | a simple thing that's quite clunky in haskell is the lack of type application | 22/01 21:36 |

dolio | Actually programming with Haskell already feels klunkier than Agda, tool-wise. | 22/01 21:45 |

BMeph | Saizan: Thanks; looks like I may try moving Agda higher up on my "things to investigate" list. | 22/01 21:46 |

sully | the automatic case splitting is dead sexy. | 22/01 21:50 |

sully | downsides of Agda include: as the type system becomes more expressive, the ability for mortals to understand it decreases drastically | 22/01 21:57 |

sully | for example: http://pastebin.mozilla.org/971818 | 22/01 21:58 |

--- Day changed Mon Jan 24 2011 | ||

napping | Are there any examples of reflection on terms with binders? | 24/01 02:03 |

napping | I don't see how to turn the AST back into typed results | 24/01 02:03 |

* Saizan doesn't remember how binders are represented | 24/01 02:05 | |

napping | It's a DeBruijn notation, but it seems to have very little type information | 24/01 02:06 |

napping | Well, I guess I could target a "Maybe" type | 24/01 02:06 |

Saizan | var : ℕ → List (Arg Term) → Term <- what does that list contain? (taken from the release notes) | 24/01 02:11 |

codolio | The std lib says var is a variable applied to arguments. | 24/01 02:11 |

Saizan | then i see, lambdas are not even annotated | 24/01 02:14 |

dolio | Not in the reflection, at least. | 24/01 02:15 |

dolio | It looks like it has a flag that says whether it's annotated, but not what the annotation is. | 24/01 02:15 |

Saizan | the Explicit? i think that only distinguishes between \ x -> and \ {x} -> | 24/01 02:22 |

dolio | Oh, duh. | 24/01 02:23 |

napping | it seems type annotations are not preserved at all | 24/01 02:23 |

napping | but I don't need them yet | 24/01 02:24 |

dolio | Yeah. I don't remember how this stuff works, really. | 24/01 02:24 |

copumpkin | napping: maybe poke around the terrifying presburger solver? | 24/01 02:24 |

dolio | Interpreting a Term back into Agda is going to be tricky business as written. | 24/01 02:24 |

dolio | In fact, you can't really do it at all, because there's no way to turn 'unknown' into its original form. | 24/01 02:25 |

Saizan | i think you are supposed to have a function Term -> Maybe WhatYourSolverActuallyHandles | 24/01 02:25 |

Saizan | and not work with Term further | 24/01 02:25 |

napping | I want to tern phoas terms into DeBruijn terms | 24/01 02:25 |

dolio | Bwahaha! Voevodsky should switch to Agda. Coq just assumed that he wanted his identity type to be in Prop. :) | 24/01 02:34 |

dolio | Actually, he doesn't want K, though, so I guess he can't. | 24/01 02:35 |

napping | What's he working on? | 24/01 02:35 |

dolio | I'm watching his presentation on univalent foundations of mathematics. | 24/01 02:36 |

dolio | Which is essentially using homotopy types instead of sets as your basis. And it turns out that intuitionistic Martin-Loef type theory is the logic of homotopy types, conveniently. | 24/01 02:37 |

ccasin | dolio: how watchable is that talk for people who don't know anything about homotopy theory? | 24/01 02:37 |

ccasin | I've been too afraid to check it out | 24/01 02:37 |

dolio | I don't know anything about homotopy theory, really. | 24/01 02:38 |

dolio | Seems all right so far. | 24/01 02:38 |

Saizan | the one from that talk about normalizing proofs so we can believe them even if the system is inconsistent was Voevodsky too? | 24/01 02:39 |

dolio | This is a different talk, I think. | 24/01 02:40 |

napping | There is some discussion like that in Luo's book | 24/01 02:40 |

dolio | It was a 3-lecture series. One is by Steve Awodey on the connection between identity types and homotopy... | 24/01 02:40 |

dolio | Another is on how to use Coq, which I'm not planning to watch. | 24/01 02:40 |

ccasin | Saizan: this idea has always seemed a little odd to me | 24/01 02:41 |

dolio | And this third is by Voevodsky about how you'd go about proving stuff in his new foundations using Coq. | 24/01 02:41 |

ccasin | most theorems are functions, and normalizing something of type (x : nat) -> foo x | 24/01 02:41 |

ccasin | doesn't tell you whether every application is normalizing | 24/01 02:41 |

ccasin | which is presumably what one cares about. | 24/01 02:41 |

Saizan | yeah | 24/01 02:42 |

dolio | Yeah, I don't really get what he was driving at in that regard. | 24/01 02:42 |

dolio | Although it occurred to me later that you can normalize things of the form (exists x. foo x) and be confident in them (I think). | 24/01 02:43 |

dolio | And then (forall x. exists y. foo x y) remains useful as a scheme for generating many (exists y. foo e y) that you can be confident about. | 24/01 02:44 |

ccasin | yes | 24/01 02:44 |

dolio | But that's still very limited. | 24/01 02:44 |

ccasin | but still only as many as you can check | 24/01 02:44 |

napping | Is it covered in the talk? | 24/01 02:46 |

napping | Luo was writing in the context of a normalizing calculus | 24/01 02:46 |

dolio | Is what covered? | 24/01 02:46 |

dolio | The point of the other talk was, "assume that pretty much all mathematics are inconsistent. What then?" | 24/01 02:47 |

dolio | And the idea was, if you work in something like type theory, you can normalize your proofs to have confidence in them. | 24/01 02:47 |

dolio | Even if you can prove falsehoods. | 24/01 02:47 |

napping | So Luo was more about cut elimination, and normal forms being obviously sound | 24/01 02:48 |

dolio | I mean, Voevodsky was operating on the premise that even Peano arithmetic is inconsistent. | 24/01 02:50 |

dolio | So whatever system Luo was working in would probably also be inconsistent by consequence. | 24/01 02:50 |

ccasin | unless LEM is to blame :) | 24/01 02:53 |

dolio | But, we can still trust normal forms for propositions that don't involve universal quantification, because bad proofs all loop, presumably. | 24/01 02:54 |

ccasin | yeah | 24/01 02:54 |

dolio | I think if PA is inconsistent, even Heyting arithmetic is in trouble, because you can encode the former into the latter by double negation, and prove all the same theorems. | 24/01 02:58 |

dolio | So if false is a theorem in PA, then not (not false) is a theorem in HA, but that's equivalent to false. | 24/01 02:59 |

ccasin | why is (not (not False)) equivalent to False? | 24/01 03:00 |

dolio | Did I get that wrong? | 24/01 03:00 |

dolio | ((False -> False) -> False) -> False | 24/01 03:00 |

dolio | f k = k id? | 24/01 03:01 |

ccasin | ah, right, sorry | 24/01 03:01 |

ccasin | had too many falses in my head :) | 24/01 03:01 |

ccasin | this makes me a little uncomfortable | 24/01 03:03 |

ccasin | if LEM is so powerful, why is it so easy to show it doesn't break consistency | 24/01 03:03 |

ccasin | well, I guess easy is relative, one has to do the double negation encoding | 24/01 03:04 |

dolio | I don't know how easy it is to show that PA is equivalent to HA. | 24/01 03:04 |

dolio | And you can't do the same for set theory, as far as I know. | 24/01 03:05 |

ccasin | yes, one can prove the consistency of constructive set theory in classical set theory | 24/01 03:06 |

ccasin | so hopefully it shouldn't be so easy to show that the latter's inconsistency implies the former's? | 24/01 03:07 |

ccasin | maybe I am thinking about this wrong, though | 24/01 03:07 |

dolio | Do you mean the reverse? | 24/01 03:08 |

dolio | I don't think showing the consistency of constructive set theory would imply the consistency of classical set theory. | 24/01 03:08 |

ccasin | right, the opposite | 24/01 03:09 |

dolio | If classical set theory proves the consistency of constructive set theory, though, then proving classical set theory consistent would prove constructive set theory consistent, presumably. | 24/01 03:09 |

ccasin | classical ZF proves constructive ZF's consistency | 24/01 03:09 |

ccasin | at least, that's the folklore | 24/01 03:09 |

ccasin | so it seems conceivable that classical set theory is inconsistent but constructive set theory isn't | 24/01 03:10 |

dolio | Anyhow, for propositional logic, you can double negate to turn classical propositions into constructive propositions, and I believe you get all the same theorems. | 24/01 03:11 |

ccasin | yes | 24/01 03:11 |

dolio | This fails for first-order logic. | 24/01 03:11 |

ccasin | OK, I am reassured | 24/01 03:11 |

dolio | So it's interesting that it still works for arithmetic statements. | 24/01 03:11 |

ccasin | hmm | 24/01 03:13 |

ccasin | so, I'm trying to remember my constructive logic class | 24/01 03:14 |

ccasin | I think there is a double negation encoding that works for FO, right? | 24/01 03:14 |

ccasin | it's just a little more complicated than directly double negating everything | 24/01 03:14 |

dolio | I don't know. | 24/01 03:14 |

ccasin | but it probably double negates the atomic formulas, presumably including False | 24/01 03:14 |

ccasin | so we are back where we started | 24/01 03:15 |

ccasin | let me see | 24/01 03:15 |

ccasin | http://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation | 24/01 03:15 |

dolio | I don't know, then. | 24/01 03:20 |

dolio | I'd guess that classical ZF proving constructive ZF consistent is wrong. | 24/01 03:20 |

dolio | Unless constructive ZF gets rid of more than excluded middle. | 24/01 03:21 |

napping | Well, looks like time to try the Agda reflection | 24/01 03:32 |

napping | Finally finished the Coq version with a quoter in Ltac - it's a huge pain working under binders | 24/01 03:32 |

dolio | Hmm, I can see why he wouldn't want to work on this in Agda... | 24/01 03:59 |

Saizan | everything would be of h-level 2? | 24/01 04:00 |

dolio | Well, I can try not to use K. | 24/01 04:00 |

dolio | But, it's disguised in pattern matching. | 24/01 04:00 |

dolio | So, I'm left in a situation where I don't know when I should be allowed to use pattern matching to prove what I want to prove. | 24/01 04:01 |

lpjhjdh | so I'm making a little abstract machine that executes instructions within an environment mapping variables to values and with a stack and was wondering how you suggest I encode a few instructions that require non-empty env and/or stack. | 24/01 07:27 |

copumpkin | represent the stack in the type | 24/01 07:28 |

copumpkin | or ask for a proof of non-emptyness with the instruction | 24/01 07:28 |

lpjhjdh | what would the former entail? Which type I mean to say | 24/01 07:28 |

lpjhjdh | asking for a proof of non-emptiness seems reasonable | 24/01 07:29 |

lpjhjdh | to implement I mean | 24/01 07:29 |

copumpkin | you could do something like an indexed monad, indexed by the size of the stack | 24/01 07:30 |

copumpkin | then | 24/01 07:30 |

copumpkin | data Lang : Nat -> Nat -> Set -> Set where | 24/01 07:31 |

copumpkin | or maybe it'd be parametrized by the type, since there isn't enough information to have multiple types in it | 24/01 07:31 |

copumpkin | but anyway | 24/01 07:31 |

copumpkin | actually | 24/01 07:32 |

lpjhjdh | sorry what would the third index Set be? | 24/01 07:32 |

copumpkin | data Lang (A : Set) : Nat -> Set where | 24/01 07:32 |

copumpkin | Push : forall {n} -> A -> Lang A n -> Lang A (suc n) | 24/01 07:32 |

copumpkin | Pop : forall {n} -> A -> Lang A (suc n) -> Lang A n | 24/01 07:33 |

lpjhjdh | aha, thanks | 24/01 07:33 |

copumpkin | well, pop wouldn't take an A too | 24/01 07:33 |

copumpkin | but you know what I mean | 24/01 07:33 |

lpjhjdh | yeah | 24/01 07:33 |

copumpkin | alternately, you could do something like | 24/01 07:34 |

copumpkin | data Lang : List Set -> Set -> Set where | 24/01 07:34 |

copumpkin | hmm | 24/01 07:35 |

copumpkin | that doesn't work out as cleanly | 24/01 07:35 |

copumpkin | but anyway, parametrize it by the list of types of elements on the stack | 24/01 07:35 |

copumpkin | so you can have a heterogeneous one | 24/01 07:35 |

lpjhjdh | language is so simple it only contains naturals, should try extending it once I work this out | 24/01 07:36 |

copumpkin | cool | 24/01 07:44 |

copumpkin | it's worth thinking of it as a free monad, possibly | 24/01 07:45 |

copumpkin | or a free indexed monad | 24/01 07:45 |

copumpkin | where the index is the state of the stack before the operation and after | 24/01 07:45 |

lpjhjdh | my algebra is quite bad, have to read up on free structures to fully appreciate your suggestion. A few chapters of category theory for the working mathematican. Many thanks. | 24/01 07:51 |

--- Log closed Tue Jan 25 00:29:55 2011 | ||

--- Log opened Tue Jan 25 00:30:04 2011 | ||

-!- Irssi: #agda: Total of 34 nicks [0 ops, 0 halfops, 0 voices, 34 normal] | 25/01 00:30 | |

-!- Irssi: Join to #agda was synced in 86 secs | 25/01 00:31 | |

--- Day changed Wed Jan 26 2011 | ||

stevan | hi, bug or feature: http://hpaste.org/43325/s ? | 26/01 14:45 |

Saizan | usually η x represents a recursive occurrence with index x, rather than representing the current index | 26/01 17:28 |

Saizan | anyhow, not unifying n and suc n sounds like a feature, since Nat is inductive | 26/01 17:29 |

Saizan | stevan: ahah! where strikes again | 26/01 17:52 |

Saizan | so, sorry, i wasn't awake enough to read the -- Works part | 26/01 17:52 |

Saizan | it's a known infelicity, it appears also in "outrageous coincidences .." | 26/01 17:53 |

Saizan | http://code.google.com/p/agda/issues/detail?id=44&q=where | 26/01 17:54 |

Saizan | jlouis: godlike even?:) | 26/01 20:25 |

jlouis | godlike | 26/01 20:25 |

jlouis | I pray to goddess Agda | 26/01 20:25 |

jlouis | that it will type and termination check my terms | 26/01 20:25 |

Saizan | ah, in _that_ sense | 26/01 20:26 |

pumpkin | djahandarie: it may be more productive to ask agda questions in here :P | 26/01 22:32 |

djahandarie | Good point | 26/01 22:32 |

pumpkin | Rel a b = a -> b -> Set | 26/01 22:32 |

pumpkin | so first write Rel (what's its type?) | 26/01 22:35 |

pumpkin | I wouldn't bother making all sorts of category abstractions if you just want to do this | 26/01 22:35 |

pumpkin | just state your axioms | 26/01 22:35 |

djahandarie | Hmm | 26/01 22:35 |

djahandarie | The category axioms? | 26/01 22:36 |

pumpkin | yep | 26/01 22:36 |

pumpkin | so start with Rel : Set -> Set -> Set1; Rel a b = a -> b -> Set | 26/01 22:37 |

pumpkin | id : forall a. Rel a a | 26/01 22:37 |

djahandarie | That was the easy one :P | 26/01 22:39 |

pumpkin | did you write it? | 26/01 22:39 |

pumpkin | you probably need something else | 26/01 22:39 |

djahandarie | No, I was thinking of the type for the associativity axiom | 26/01 22:40 |

dolio | Syntax error. | 26/01 22:40 |

pumpkin | dolio would make a terrible compiler | 26/01 22:42 |

pumpkin | it reminds me of the cmm compiler in ghc | 26/01 22:42 |

dolio | At least I gave you more information than, "problem" | 26/01 22:43 |

pumpkin | you mean that dot? | 26/01 22:43 |

pumpkin | it was a pseudoagda-ey thing :P | 26/01 22:43 |

dolio | Yes. | 26/01 22:44 |

pumpkin | id : forall a -> Rel a a | 26/01 22:44 |

pumpkin | djahandarie: you're going to want equality at some pont | 26/01 22:46 |

pumpkin | point | 26/01 22:46 |

pumpkin | you can define it yourself or pull in Relation.Binary.PropositionalEquality | 26/01 22:46 |

djahandarie | Can you show me a full example of something simpler? | 26/01 22:47 |

Saizan | e.g. to show that (Nat,_+_) is a monoid, you'd have to make defs with the following types: forall n -> n + 0 == n; forall n -> 0 + n == n; forall x y z -> x + | 26/01 22:53 |

Saizan | x + (y + z) == (x + y) + z | 26/01 22:54 |

--- Day changed Fri Jan 28 2011 | ||

Cerulean | hey. I think code.haskell.org is down (surprise surprise..?) -- anywhere other 'canonical' spot to get the repo from? | 28/01 21:46 |

--- Day changed Sat Jan 29 2011 | ||

dolio | Oh shit. --without-K. | 29/01 01:13 |

dolio | Now we can entice Voevodsky. | 29/01 01:13 |

Saizan | :O | 29/01 01:16 |

Saizan | he might like universe polymorphism | 29/01 01:16 |

copumpkin | so what's this stuff about not having K, and why will it attract the guy whose name I can't remember how to spell? | 29/01 23:52 |

dolio | K is uniqueness of identity proofs. | 29/01 23:55 |

copumpkin | yeah | 29/01 23:57 |

dolio | In univalent foundations, identity of sets is actually isomorphism, so only bot and top have unique identity proofs. | 29/01 23:57 |

copumpkin | but why was having K keeping Mr. X away? | 29/01 23:57 |

dolio | K is inconsistent with his work. | 29/01 23:58 |

copumpkin | oh | 29/01 23:58 |

dolio | There's some videos linked in the dependent types reddit. | 29/01 23:58 |

dolio | If you watch, one of the main ideas is that Martin-Loef type theory is the internal language of these certain types of categories of homotopy types, or something like that. | 29/01 23:59 |

dolio | But Martin-Loef + K is not. | 29/01 23:59 |

dolio | They don't mention the latter fact, but K collapses the higher-dimensional structure. | 29/01 23:59 |

--- Day changed Sun Jan 30 2011 | ||

dolio | Everything above level 2 or so. Because you can prove everything happens 'on the nose' instead of just up to higher equivalence levels. | 30/01 00:00 |

copumpkin | hm :o | 30/01 00:02 |

dolio | In essence, it's like: we have the internal language of a category, except we also have an axiom that says all morphisms are the identity. | 30/01 00:07 |

dolio | That limits what categories your language applies to. | 30/01 00:07 |

copumpkin | yeah, I see | 30/01 00:07 |

--- Day changed Mon Jan 31 2011 | ||

rribeiro | Hello... I'm trying to learn a bit of agda... I'm trying to implement a matrix transposition algorithm | 31/01 16:44 |

rribeiro | I'm using the Data.Vec module from the standard library as a base for the implementation of matrix's | 31/01 16:45 |

rribeiro | ranspose : {m n : ℕ} → Matrix m n → Matrix n m | 31/01 16:46 |

rribeiro | transpose [] = [] | 31/01 16:46 |

rribeiro | transpose (ns ∷ nss) = (map head ns) ∷ (transpose nss) | 31/01 16:46 |

rribeiro | when I've typed these code... I've got the error msg | 31/01 16:47 |

rribeiro | zero != .n of type N | 31/01 16:47 |

rribeiro | any clue? | 31/01 16:47 |

ccasin | rribeiro: to start with, .n here is the "n" parameter of your function | 31/01 16:50 |

ccasin | I'm not sure how you implemented matrixes, but here is my guess at what is happening | 31/01 16:50 |

ccasin | in the first case, you pattern match on the empty list | 31/01 16:50 |

ccasin | this means that one dimension of the matrix, the "m" one, must be 0 | 31/01 16:51 |

ccasin | but it doesn't give us any information about the second dimension | 31/01 16:51 |

ccasin | so the input matrix has type "Matrix 0 n" for some arbitrary n | 31/01 16:51 |

ccasin | Now you return another empty vector | 31/01 16:51 |

ccasin | which has type "Matrix 0 n' " for any n' | 31/01 16:51 |

ccasin | but, because of your type, you needed to return something with the type "Matrix n 0" | 31/01 16:52 |

ccasin | does that make sense? | 31/01 16:52 |

rribeiro | ccasin, Ok... | 31/01 16:52 |

rribeiro | ccasin, thank you! | 31/01 16:53 |

ccasin | no problem | 31/01 16:54 |

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