--- Log opened Thu Jul 01 00:00:56 2010
-!- mode/#epigram [+v dolio] by ChanServ01/07 01:35
-!- mode/#epigram [+v dolio] by ChanServ01/07 02:18
-!- mode/#epigram [+v Saizan] by ChanServ01/07 02:31
-!- mode/#epigram [+v dolio] by ChanServ01/07 03:18
-!- mode/#epigram [+v Saizan] by ChanServ01/07 06:37
-!- mode/#epigram [+v dolio] by ChanServ01/07 08:18
-!- mode/#epigram [+v Saizan] by ChanServ01/07 14:39
-!- mode/#epigram [+v Saizan] by ChanServ01/07 14:41
-!- mode/#epigram [+v Saizan_] by ChanServ01/07 15:26
-!- Saizan_ is now known as Saizan01/07 15:26
-!- mode/#epigram [+v dolio] by ChanServ01/07 16:22
-!- mode/#epigram [+v dolio] by ChanServ01/07 17:18
-!- mode/#epigram [+v dolio] by ChanServ01/07 18:18
-!- mode/#epigram [+v Saizan] by ChanServ01/07 18:55
-!- mode/#epigram [+v Saizan] by ChanServ01/07 19:28
-!- mode/#epigram [+v Saizan] by ChanServ01/07 19:29
-!- mode/#epigram [+v soupdragon] by ChanServ01/07 21:27
-!- mode/#epigram [+v soupdragon] by ChanServ01/07 21:51
--- Day changed Fri Jul 02 2010
-!- mode/#epigram [+v dolio] by ChanServ02/07 03:21
-!- mode/#epigram [+v dolio] by ChanServ02/07 05:49
-!- mode/#epigram [+v Saizan] by ChanServ02/07 06:30
-!- mode/#epigram [+v dolio] by ChanServ02/07 06:50
-!- mode/#epigram [+v dolio] by ChanServ02/07 08:50
-!- mode/#epigram [+v pigworker_] by ChanServ02/07 10:08
-!- pigworker_ is now known as pigworker02/07 10:11
-!- mode/#epigram [+v Saizan] by ChanServ02/07 10:30
-!- mode/#epigram [+v Saizan] by ChanServ02/07 10:54
-!- mode/#epigram [+v pigworker_] by ChanServ02/07 10:58
-!- mode/#epigram [+v pigworker] by ChanServ02/07 11:00
-!- mode/#epigram [+v dolio] by ChanServ02/07 11:50
-!- mode/#epigram [+v Saizan] by ChanServ02/07 12:59
-!- mode/#epigram [+v soupdragon] by ChanServ02/07 13:16
-!- mode/#epigram [+v Saizan] by ChanServ02/07 13:18
-!- mode/#epigram [+v Saizan] by ChanServ02/07 13:55
-!- mode/#epigram [+v Saizan] by ChanServ02/07 14:32
-!- mode/#epigram [+v Saizan] by ChanServ02/07 14:50
-!- mode/#epigram [+v dolio] by ChanServ02/07 14:50
-!- mode/#epigram [+v Saizan] by ChanServ02/07 15:07
-!- mode/#epigram [+v Saizan] by ChanServ02/07 17:04
-!- mode/#epigram [+v Saizan] by ChanServ02/07 17:11
-!- mode/#epigram [+v Saizan] by ChanServ02/07 19:29
-!- mode/#epigram [+v Saizan] by ChanServ02/07 20:37
-!- mode/#epigram [+v Saizan] by ChanServ02/07 20:41
-!- koninkje1away is now known as koninkje_away02/07 22:25
--- Day changed Sat Jul 03 2010
-!- mode/#epigram [+v pigworker] by ChanServ03/07 00:23
-!- mode/#epigram [+v Saizan] by ChanServ03/07 06:37
-!- mode/#epigram [+v codolio] by ChanServ03/07 06:49
-!- codolio is now known as dolio03/07 07:12
-!- mode/#epigram [+v dolio] by ChanServ03/07 07:47
-!- mode/#epigram [+v Saizan] by ChanServ03/07 08:40
-!- mode/#epigram [+v Saizan] by ChanServ03/07 10:10
-!- mode/#epigram [+v Saizan] by ChanServ03/07 11:12
-!- mode/#epigram [+v Saizan] by ChanServ03/07 19:24
--- Day changed Sun Jul 04 2010
-!- mode/#epigram [+v Saizan] by ChanServ04/07 00:06
-!- mode/#epigram [+v dolio] by ChanServ04/07 01:46
-!- mode/#epigram [+v dolio] by ChanServ04/07 03:50
-!- mode/#epigram [+v dolio] by ChanServ04/07 04:50
-!- mode/#epigram [+v Saizan] by ChanServ04/07 06:44
-!- mode/#epigram [+v dolio] by ChanServ04/07 08:49
-!- mode/#epigram [+v dolio] by ChanServ04/07 16:46
-!- mode/#epigram [+v soupdragon] by ChanServ04/07 20:14
-!- mode/#epigram [+v dolio] by ChanServ04/07 20:50
-!- mode/#epigram [+v dolio] by ChanServ04/07 22:46
--- Day changed Mon Jul 05 2010
-!- mode/#epigram [+v dolio] by ChanServ05/07 05:46
-!- mode/#epigram [+v dolio] by ChanServ05/07 13:49
-!- mode/#epigram [+v dolio] by ChanServ05/07 16:45
-!- mode/#epigram [+v soupdragon] by ChanServ05/07 16:56
-!- mode/#epigram [+v dolio] by ChanServ05/07 17:50
-!- mode/#epigram [+v soupdragon] by ChanServ05/07 17:54
-!- mode/#epigram [+v codolio] by ChanServ05/07 19:49
--- Day changed Tue Jul 06 2010
-!- mode/#epigram [+v dolio] by ChanServ06/07 00:45
-!- mode/#epigram [+v dolio] by ChanServ06/07 01:49
-!- mode/#epigram [+v dolio] by ChanServ06/07 03:49
-!- mode/#epigram [+v dolio] by ChanServ06/07 05:49
-!- mode/#epigram [+v dolio] by ChanServ06/07 12:08
-!- mode/#epigram [+v soupdragon] by ChanServ06/07 14:21
-!- mode/#epigram [+v dolio] by ChanServ06/07 16:45
-!- mode/#epigram [+v dolio] by ChanServ06/07 18:48
-!- mode/#epigram [+v soupdragon] by ChanServ06/07 20:46
-!- mode/#epigram [+v dolio] by ChanServ06/07 20:48
--- Day changed Wed Jul 07 2010
-!- mode/#epigram [+v dolio] by ChanServ07/07 01:48
-!- mode/#epigram [+v dolio] by ChanServ07/07 02:45
-!- mode/#epigram [+v dolio] by ChanServ07/07 12:48
-!- mode/#epigram [+v dolio] by ChanServ07/07 13:48
-!- mode/#epigram [+v soupdragon] by ChanServ07/07 14:38
-!- mode/#epigram [+v Saizan_] by ChanServ07/07 15:59
-!- Saizan_ is now known as Saizan07/07 15:59
-!- mode/#epigram [+v pigworker] by ChanServ07/07 20:09
tsapievening pigworker07/07 20:09
+pigworkerevening tsapi07/07 20:09
+pigworkerI don't know of James McKinna is on -dev; he was fiddling with makefiles earlier07/07 20:38
+pigworkerI forwarded tsapi's message, just in case07/07 20:38
tsapiI should have cc'ed him07/07 20:39
tsapiI think rolling back the repo might be the only option but I'm not sure.07/07 20:40
tsapistill can't pull from blinky. I think my repo is broken. I'll try getting a new one.07/07 21:01
tsapithat worked. I guess it's not stupid enough to pull them one at a time :)07/07 21:05
tsapipigworker: is your repo ok?07/07 21:05
+pigworkerhaven't tried07/07 21:06
+pigworkerI might stay a few patches behind until it's sorted.07/07 21:06
tsapiI got a new repo successfully.07/07 21:07
+pigworkerccasin, if you're interested in normalization, you might find http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf has a little to offer (for evaluation at least); chop off filename for darcs repo07/07 21:54
ccasinpigworker: thanks, this is interesting07/07 22:01
+pigworkerbet you can't prove it terminates with natural number induction07/07 22:02
ccasin:)07/07 22:03
ccasinof course, I could win that battle if I could just figure out how to do this metatheory07/07 22:04
+pigworkerproof theoretically, metatheory isn't any heavier than metaprogramming, and we wanna do that, right?07/07 22:05
ccasinthat's my argument07/07 22:05
ccasinthe current response is that we'll still be able to write generic programs, just not reason about them07/07 22:05
ccasinwhich is... unsatisfying07/07 22:05
+pigworkeryes: you want to use generic programs in types07/07 22:06
ccasinI agree in theory, but I confess I'm having trouble coming up with examples that are "practical" enough to win the argument07/07 22:08
+pigworkerat this point, I'd offer a large bet07/07 22:10
+pigworkerdata Reader = Stop | Read (Nat -> Reader)07/07 22:11
+pigworkercombine :: Reader -> Reader -> Reader07/07 22:12
+pigworkercombine Stop next = next07/07 22:12
+pigworkercombine (Read f) next = Read (\ x -> combine (f x) next)07/07 22:13
+pigworkerlooks a bit ordinal, if you ask me07/07 22:13
+pigworkerhard to prove monad laws for the >>= of interactive processes without transfinite induction07/07 22:16
+pigworkerI wonder if that's practical.07/07 22:17
ccasinnat indexed trees like that are nice examples07/07 22:17
ccasinthe question is what does Joe Programmer want to use them for07/07 22:17
+Saizanoleg's iteratee is not far from that07/07 22:18
+pigworkerIt was Hancock's long before...07/07 22:18
ccasinI should think harder about interactive processes, thanks07/07 22:19
+pigworkerWho speaks for Joe Programmer?07/07 22:20
ccasinsurely not oleg07/07 22:20
+pigworkerQuite a lot of Joes root for Oleg07/07 22:20
ccasinyeah, it's a good question07/07 22:21
+pigworkerIn my time, I've been Joe-bashed rather a lot.07/07 22:21
+pigworkerMany things I've been told Joe didn't want to know about are now much in demand.07/07 22:22
ccasinyes07/07 22:22
ccasinanyway, it seems silly - I know what sort of programs I want to write, and they use this stuff.  And I'm not such a brilliant theorist07/07 22:23
ccasinas to make it pointless07/07 22:23
+pigworker"Why should Joe spoil my fun?" is always the key question.07/07 22:24
+pigworkerIt's faintly insulting. They say "no one will ever want this". I say "I want this." They say "you're no one."07/07 22:25
ccasinyes07/07 22:25
ccasinbut, I'm hopeful that once things get a little more concrete with trellys it won't be too hard to make the case07/07 22:26
+pigworkeryeah; fun vs no fun is much easier once systems are actually going07/07 22:27
ccasinI've got to run - thanks for the kipling link though, it's really neat.  I've consistently failed in attempts to usably embed languages this complicated in agda07/07 22:32
-!- mode/#epigram [+v soupdragon] by ChanServ07/07 22:49
-!- mode/#epigram [+v pigworker] by ChanServ07/07 22:53
+soupdragonhow is epigram going ? :)07/07 23:09
-!- mode/#epigram [+v pigworker] by ChanServ07/07 23:23
+pigworkersoupdragon, we're all a bit distracted at the moment, but we might manage some more next week07/07 23:24
+pigworkerit's the season to finish papers07/07 23:26
pedagandsoupdragon, I've been writing and deleting a fair amount of code lately to get a usable interface07/07 23:26
pedagandbut don't say anything to my boss, I'm supposed to finish papers07/07 23:27
+pigworkertwo can play at that game...07/07 23:28
pedagandwhen I say "deleting code", it's deleting the code I wrote, obviously. That's an old Greek tradition07/07 23:28
+soupdragon:)07/07 23:28
+soupdragonI can keep quiet07/07 23:28
+pigworkercode is ephemeral; deleting it is a form of progress07/07 23:29
pedagandpigworker, :-)07/07 23:30
-!- mode/#epigram [+v dolio] by ChanServ07/07 23:48
--- Day changed Thu Jul 08 2010
-!- mode/#epigram [+v dolio] by ChanServ08/07 02:08
+doliopigworker: So, I glanced at my hurkens file, and it doesn't look to me like an EPTS-style annotation system would actually make higher impredicativity safe.08/07 02:10
+pigworkerdolio: just checking...if I add "biggish intersections" S : Set_{i+1}, T : S -> Set_i |- (x : S)- -> T : Set_i at each level, do things break?08/07 08:26
+doliopigworker: That'd be my guess.08/07 08:27
+pigworkerI'd like to confirm that, just to cut off that line of enquiry.08/07 08:29
+dolioI might get around to actually coding up such a type theory. I've been trying to decide whether or not to try bidirectional type checking.08/07 08:31
+pigworkerMeanwhile, for anxious largeness enthusiasts (such as myself), there's always the question of which appeals to impredicativity you can shrink by coding the big with a universe.08/07 08:32
+pigworkerLike when you code lambda terms with a set of free variables by indexing over natural numbers which suc under binders, instead of over sets which Maybe.08/07 08:35
+pigworkerI don't know how widely applicable that trick is: I'm really curious to see which monsters are invulnerable to the I-R incredible shrinking ray...08/07 08:39
tsapiif anyone is interested I have a draft of a paper entitled "relative monads formalised" at http://www.cs.ioc.ee/~james/papers/AssistedMonads2.pdf the code is up there too08/07 08:39
tsapideadline is on Sunday so there's still a bit to do08/07 08:40
+dolioIs that a followup to "Monads Need Not Be Endofunctors"?08/07 08:40
agundryI know that feeling...08/07 08:40
tsapidolio: more of a follow behind :)08/07 08:40
tsapidolio: it covers less stuff in more detail08/07 08:41
+dolioAh.08/07 08:41
tsapidolio: although, there is some stuff about models of lambda calculus as relative em algebras which wasn't in the original paper.08/07 08:44
+doliopigworker: Do you know off hand if there's much work on union types? I think it may have been the Mishra-Linger thesis that gave semantics for part of the work in some theory with intersections, but mentioned that the theory wasn't (known to be?) well-behaved when unions were added.08/07 08:44
+dolioBut you get unions straight-forwardly when you have the erasure stuff with inductive types.08/07 08:45
+pigworkerI don't know much about union types, but I can see you've got the ability to code static-only tagging.08/07 08:49
+dolioYeah. Erase the left side of the pair.08/07 08:50
+dolioRight side gets you subset types.08/07 08:50
+dolioI believe.08/07 08:50
+pigworkerusual caveats about erasure and proof irrelevance08/07 08:50
+dolioSure.08/07 08:51
+pigworkerHere's a question about intersections and unions...08/07 09:00
+pigworkerAre they "just an optimization"? I mean, do we get extra strength, as well as leaner-running Pi and Sigma. If so, what?08/07 09:04
+pigworkerI'm hoping for a stronger definitional equality, and some theorems-for-free.08/07 09:05
+dolioI think you get better parametricity.08/07 09:05
+dolioAt least, they capture the intuitive notion of "parametric", I think.08/07 09:06
+pigworkerI'm wondering if there's a systematic method to prove the theorems for pi-and-sigma programs that correspond to the free theorems for intersection-union programs.08/07 09:07
+dolioAt least, if you have an inductive(-recursive) universe U, I'd expect an intersection (t : U) => ... to have similar results as (t : Set) -> ...08/07 09:07
+dolioSomeone had a paper on parametricty in pure type systems, and they noted toward the end that if you restrict what observations you can make on data, you can get stronger theorems.08/07 09:08
+dolioAnd that's exactly what intersections and unions do.08/07 09:08
+pigworkerThat's my question: is it *exactly* what intersections and unions do? or *at least* what intersections and unions do?08/07 09:09
+dolioWell, certainly at least. :)08/07 09:10
+dolioStronger definitional equality maybe.08/07 09:10
+dolioAs you know, the EPTS folks have an alternate rule that erases before checking equality.08/07 09:10
+dolioAnd that gets you some things you otherwise wouldn't have.08/07 09:11
+pigworkerbroken typechecker?08/07 09:11
+dolioWas it broken?08/07 09:11
+pigworkerdepends which proofs you erase08/07 09:11
+dolioThe ones marked compile-time-only.08/07 09:11
+pigworkerso, not equality or termination, then08/07 09:12
+dolioDon't think so.08/07 09:13
+dolioYou erase the parametric stuff, more or less.08/07 09:13
+pigworkerbut not as much as you can erase at run time08/07 09:14
+pigworkerone level of erasure is not enough to manage open-vs-closed computation08/07 09:16
+pigworkerthat's why edwinb and I considered multiple levels in that "lightning" scribble we wrote on a virtual beermat in 200508/07 09:16
+dolioYeah, the intersection/union type stuff seems like erasing all the stuff that people don't ever need to look at, so to speak.08/07 09:17
+pigworkergotta run just now - incoming visitor08/07 09:18
+dolioWhereas equality you might have to look at, but there's only one possibility, or some such.08/07 09:18
+dolioAll right.08/07 09:18
+pigworker(yeah the distinction bites when you have to be strict in "...or bust")08/07 09:19
-!- mode/#epigram [+v Saizan] by ChanServ08/07 09:40
-!- mode/#epigram [+v dolio] by ChanServ08/07 10:44
* edwinb is running out of punctuation again08/07 11:06
* edwinb considers switching back to an untyped language where this sort of thing isn't a problem08/07 11:07
-!- mode/#epigram [+v dolio] by ChanServ08/07 13:45
-!- mode/#epigram [+v soupdragon] by ChanServ08/07 16:00
-!- mode/#epigram [+v Saizan] by ChanServ08/07 16:41
-!- shapr[ is now known as shapr08/07 19:21
-!- mode/#epigram [+v pigworker] by ChanServ08/07 22:06
-!- mode/#epigram [+v dolio] by ChanServ08/07 23:48
--- Day changed Fri Jul 09 2010
-!- mode/#epigram [+v pigworker] by ChanServ09/07 00:26
-!- mode/#epigram [+v dolio] by ChanServ09/07 01:48
-!- mode/#epigram [+v dolio] by ChanServ09/07 03:44
-!- mode/#epigram [+v dolio] by ChanServ09/07 04:49
-!- mode/#epigram [+v dolio] by ChanServ09/07 05:44
-!- mode/#epigram [+v pigworker] by ChanServ09/07 06:25
-!- mode/#epigram [+v dolio] by ChanServ09/07 11:47
-!- mode/#epigram [+v soupdragon] by ChanServ09/07 13:42
-!- mode/#epigram [+v dolio] by ChanServ09/07 15:47
-!- mode/#epigram [+v soupdragon] by ChanServ09/07 16:36
-!- mode/#epigram [+v dolio] by ChanServ09/07 16:47
-!- mode/#epigram [+v dolio] by ChanServ09/07 18:48
-!- mode/#epigram [+v dolio] by ChanServ09/07 23:44
--- Day changed Sat Jul 10 2010
-!- mode/#epigram [+v dolio] by ChanServ10/07 00:44
-!- mode/#epigram [+v dolio] by ChanServ10/07 02:47
-!- mode/#epigram [+v dolio] by ChanServ10/07 08:47
-!- mode/#epigram [+v soupdragon] by ChanServ10/07 14:08
--- Day changed Sun Jul 11 2010
-!- mode/#epigram [+v soupdragon] by ChanServ11/07 00:27
-!- mode/#epigram [+v dolio] by ChanServ11/07 02:43
-!- mode/#epigram [+v codolio] by ChanServ11/07 08:47
-!- codolio is now known as dolio11/07 10:13
-!- mode/#epigram [+v dolio] by ChanServ11/07 10:47
-!- mode/#epigram [+v dolio] by ChanServ11/07 12:47
-!- mode/#epigram [+v soupdragon] by ChanServ11/07 15:37
-!- mode/#epigram [+v dolio] by ChanServ11/07 16:43
-!- mode/#epigram [+v dolio] by ChanServ11/07 19:47
--- Day changed Mon Jul 12 2010
-!- mode/#epigram [+v dolio] by ChanServ12/07 00:43
-!- mode/#epigram [+v dolio] by ChanServ12/07 05:47
-!- mode/#epigram [+v dolio] by ChanServ12/07 09:30
-!- mode/#epigram [+v dolio] by ChanServ12/07 11:46
-!- mode/#epigram [+v dolio] by ChanServ12/07 12:46
-!- mode/#epigram [+v edwinb] by ChanServ12/07 15:55
tsapimoleris ping12/07 16:23
moleristsapi: pong12/07 16:36
-!- mode/#epigram [+v soupdragon] by ChanServ12/07 16:38
-!- mode/#epigram [+v dolio] by ChanServ12/07 23:46
--- Day changed Tue Jul 13 2010
-!- mode/#epigram [+v dolio] by ChanServ13/07 00:46
-!- mode/#epigram [+v Saizan] by ChanServ13/07 01:30
-!- mode/#epigram [+v Saizan] by ChanServ13/07 01:42
-!- mode/#epigram [+v dolio] by ChanServ13/07 02:46
-!- mode/#epigram [+v dolio] by ChanServ13/07 04:46
-!- mode/#epigram [+v dolio] by ChanServ13/07 15:46
-!- mode/#epigram [+v soupdragon] by ChanServ13/07 16:17
-!- mode/#epigram [+v dolio] by ChanServ13/07 19:43
-!- mode/#epigram [+v dolio] by ChanServ13/07 20:46
-!- shapr[ is now known as shapr13/07 23:42
--- Day changed Wed Jul 14 2010
-!- mode/#epigram [+v soupdragon] by ChanServ14/07 00:17
-!- koninkje_away is now known as koninkje14/07 03:00
-!- mode/#epigram [+v dolio] by ChanServ14/07 07:46
-!- mode/#epigram [+v Saizan] by ChanServ14/07 09:19
-!- mode/#epigram [+v Saizan] by ChanServ14/07 19:49
-!- mode/#epigram [+v dolio] by ChanServ14/07 20:12
-!- mode/#epigram [+v soupdragon] by ChanServ14/07 20:54
-!- mode/#epigram [+v soupdragon] by ChanServ14/07 21:40
-!- mode/#epigram [+v dolio] by ChanServ14/07 23:42
--- Day changed Thu Jul 15 2010
-!- mode/#epigram [+v dolio] by ChanServ15/07 00:46
-!- mode/#epigram [+v dolio] by ChanServ15/07 02:42
-!- mode/#epigram [+v dolio] by ChanServ15/07 06:45
-!- ServerMode/#epigram [+v edwinb] by holmes.freenode.net15/07 10:18
-!- mode/#epigram [+v soupdragon] by ChanServ15/07 18:56
-!- mode/#epigram [+v dolio] by ChanServ15/07 21:41
-!- mode/#epigram [+v dolio] by ChanServ15/07 23:45
--- Day changed Fri Jul 16 2010
-!- mode/#epigram [+v codolio] by ChanServ16/07 02:44
-!- codolio is now known as dolio16/07 02:45
-!- mode/#epigram [+v dolio] by ChanServ16/07 04:41
-!- mode/#epigram [+v dolio] by ChanServ16/07 05:46
-!- mode/#epigram [+v dolio] by ChanServ16/07 11:41
-!- mode/#epigram [+v dolio] by ChanServ16/07 15:44
-!- mode/#epigram [+v dolio] by ChanServ16/07 16:45
-!- mode/#epigram [+v dolio] by ChanServ16/07 17:44
-!- mode/#epigram [+v Saizan] by ChanServ16/07 18:15
-!- mode/#epigram [+v soupdragon] by ChanServ16/07 18:16
-!- mode/#epigram [+v Saizan] by ChanServ16/07 18:29
-!- mode/#epigram [+v Saizan] by ChanServ16/07 19:00
-!- mode/#epigram [+v Saizan] by ChanServ16/07 20:18
-!- mode/#epigram [+v dolio] by ChanServ16/07 23:45
--- Day changed Sat Jul 17 2010
-!- mode/#epigram [+v dolio] by ChanServ17/07 02:44
-!- mode/#epigram [+v codolio] by ChanServ17/07 05:44
-!- mode/#epigram [+v dolio] by ChanServ17/07 16:44
-!- mode/#epigram [+v dolio] by ChanServ17/07 17:41
-!- mode/#epigram [+v soupdragon] by ChanServ17/07 18:02
-!- mode/#epigram [+v dolio] by ChanServ17/07 20:41
-!- mode/#epigram [+v dolio] by ChanServ17/07 21:45
--- Day changed Sun Jul 18 2010
-!- mode/#epigram [+v dolio] by ChanServ18/07 01:41
-!- mode/#epigram [+v dolio] by ChanServ18/07 02:41
-!- mode/#epigram [+v Saizan] by ChanServ18/07 03:04
-!- mode/#epigram [+v dolio] by ChanServ18/07 03:13
-!- koninkje is now known as world18/07 03:23
-!- world is now known as koninkje18/07 03:23
-!- mode/#epigram [+v dolio] by ChanServ18/07 03:40
-!- mode/#epigram [+v soupdragon] by ChanServ18/07 04:31
-!- mode/#epigram [+v dolio] by ChanServ18/07 04:41
-!- koninkje is now known as koninkje_away18/07 05:12
-!- koninkje_away is now known as koninkje18/07 07:52
-!- koninkje is now known as koninkje_away18/07 08:25
-!- mode/#epigram [+v dolio] by ChanServ18/07 14:44
pedagandmoleris, historically, where does the induction principle of IDesc come from?18/07 19:24
pedagandI was surprised to see that it exactly fits Jacobs' fibrational definition of induction principles, although I suspect that this is not a coincidence...18/07 19:26
pedagandbut noticing how much pain it was (for me) to instantiate Jacobs' scheme to IDesc, I'm wondering where you got it from and if it was easier18/07 19:26
* soupdragon bets it came from Dybjer 18/07 19:27
+soupdragonproblem is his site's down but there's a link to 'Indexed Induction-Recursion' from Anton Setzers page.. which looks related18/07 19:29
* soupdragon is just regurgitating things I read a while ago since nobody else seems to be here18/07 19:29
pedagandI've it here and, indeed, that's similar. I actually wrote that in the ICFP paper: "induction principle, don't look at me, it's all Dybjer's fault"18/07 19:30
+soupdragonhehe18/07 19:31
pedagandbut I can help thinking that the nottinghamers had something in mind. Hence my curiosity :-)18/07 19:31
pedagandbut thanks for your help, Dybjer's paper might answer my question as well18/07 19:32
* soupdragon really doesn't know anything about fibers other than the definition (which is not even close to half the battle) - but it seems to be very important18/07 19:33
+soupdragonwith all this fibred homotopy lambda calculus (I can just about spell the words...)18/07 19:33
+soupdragonsomething I'd like to understand eventually18/07 19:33
pedagandI don't understand anything of those things, but I've a colleague working on it who feels horribly alone. So, I've kind of funded the Fibrations Anonymous association and I patiently listen to his tortured stories.18/07 19:36
+soupdragonI should start one! maybe I could pick some of it up18/07 19:38
pedagandas for fibrations alone, Bart Jacobs has written the Bible of Fibrationalogy: "Categorical logic and type theory"18/07 19:38
pedagandfibrations seem good for modelling a type theory in category theory18/07 19:38
+soupdragonmmaybe this is gentler than his PhD thesis18/07 19:41
+soupdragonI've got to check it out ty!18/07 19:42
pedagandif you look for yet-another-crazy-model-of-type-theory-in-cat, you can look at the first chapter of Michael Abbott PhD thesis. I don't know if it's gentler either, but it is heavily inspired by Jacobs, claiming some improvements18/07 19:43
pedagandpersonally, I prefer to stay clear of these things, because it seems never ending18/07 19:44
+soupdragonlater18/07 19:55
-!- mode/#epigram [+v codolio] by ChanServ18/07 20:43
-!- codolio is now known as dolio18/07 22:58
--- Day changed Mon Jul 19 2010
-!- mode/#epigram [+v soupdragon] by ChanServ19/07 04:45
-!- mode/#epigram [+v dolio] by ChanServ19/07 05:44
-!- mode/#epigram [+v dolio] by ChanServ19/07 08:40
-!- mode/#epigram [+v pigworker] by ChanServ19/07 13:31
-!- mode/#epigram [+v dolio] by ChanServ19/07 14:44
+pigworkermoleris: is blinky on the blinky, by any chance?19/07 17:47
-!- mode/#epigram [+v dolio] by ChanServ19/07 18:43
-!- mode/#epigram [+v pigworker] by ChanServ19/07 19:08
-!- mode/#epigram [+v dolio] by ChanServ19/07 19:40
-!- mode/#epigram [+v soupdragon] by ChanServ19/07 20:16
-!- mode/#epigram [+v dolio] by ChanServ19/07 21:43
--- Day changed Tue Jul 20 2010
-!- mode/#epigram [+v dolio] by ChanServ20/07 07:00
-!- mode/#epigram [+v dolio] by ChanServ20/07 07:39
-!- mode/#epigram [+v pigworker_] by ChanServ20/07 10:27
-!- pigworker_ is now known as pigworker20/07 10:28
-!- mode/#epigram [+v pigworker_] by ChanServ20/07 12:05
-!- pigworker_ is now known as pigworker20/07 12:05
-!- mode/#epigram [+v dolio] by ChanServ20/07 12:40
-!- mode/#epigram [+v soupdragon] by ChanServ20/07 13:26
-!- mode/#epigram [+v dolio] by ChanServ20/07 13:44
molerispigworker: indeed it was, fixed now20/07 14:16
molerispedagand: ping20/07 14:17
-!- mode/#epigram [+v pigworker_] by ChanServ20/07 14:42
-!- pigworker_ is now known as pigworker20/07 14:42
+pigworkermoleris: Much ta. Uncle James and I have been exchanging patches via local network, but he just got on the train.20/07 14:53
-!- mode/#epigram [+v pigworker] by ChanServ20/07 14:59
pedagandmoleris, pong, sorry for the lag20/07 15:32
-!- mode/#epigram [+v dolio] by ChanServ20/07 19:40
-!- mode/#epigram [+v dolio] by ChanServ20/07 23:43
--- Day changed Wed Jul 21 2010
-!- mode/#epigram [+v soupdragon] by ChanServ21/07 00:53
-!- mode/#epigram [+v dolio] by ChanServ21/07 02:40
-!- mode/#epigram [+v dolio] by ChanServ21/07 04:43
-!- mode/#epigram [+v pigworker] by ChanServ21/07 09:32
-!- ServerMode/#epigram [+v Saizan] by holmes.freenode.net21/07 09:36
-!- mode/#epigram [+v pigworker] by ChanServ21/07 10:32
-!- mode/#epigram [+v codolio] by ChanServ21/07 10:42
pedagandpigworker, the Hinze-Cheney paper you had in mind is "First-Class Phantom Types", right? There only is a samizdat edition (cornell techreport) of it, afaik.21/07 11:24
+pigworkerpedagand: that's the paper; will see if I can find a more advanced version...21/07 11:29
pedagandalright. Meanwhile, I'll use this one.21/07 11:37
-!- mode/#epigram [+v dolio] by ChanServ21/07 11:39
+pigworkerlooks like the tech report is what there is21/07 12:00
+pigworkersurely there's an earlier GADT paper by Tim Sheard than LotF..?21/07 12:01
pedagandI'll look that up21/07 12:05
+edwinbHmm, I thought that one was the first21/07 12:06
+pigworkerjust looked; seems so21/07 12:10
+pigworkerXi/Chen/Chen POPL 2003 is probably also something to mention in that line21/07 12:12
pedagandok21/07 12:14
--- Log closed Wed Jul 21 14:28:16 2010
--- Log opened Wed Jul 21 14:52:22 2010
-!- Irssi: #epigram: Total of 10 nicks [0 ops, 0 halfops, 5 voices, 5 normal]21/07 14:52
-!- Irssi: Join to #epigram was synced in 77 secs21/07 14:53
-!- mode/#epigram [+v dolio] by ChanServ21/07 15:44
-!- mode/#epigram [+v Saizan] by ChanServ21/07 17:29
-!- mode/#epigram [+v dolio] by ChanServ21/07 17:39
pedagandpigworker, I've removed the table 1 in Section 5 and removed Section 6.1. Let me know if it would cause conflict, I will take care of the merge.21/07 17:59
pedagandout of curiosity, did someone cared to implement "summer" in Scotland? If so, which Service Pack disabled it?21/07 18:07
+edwinbwe've implemented it in the east21/07 18:10
+edwinbit was really warm yesterday. 18 degrees.21/07 18:10
pedagandI see: we don't have the same standards of "summerness" :-)21/07 18:12
+edwinbI even went out without a coat21/07 18:12
+edwinbI think your other problem is that all the rain tends to get dumped on Glasgow21/07 18:13
pedagandthe glaswegian monsoon...21/07 18:21
-!- mode/#epigram [+v dolio] by ChanServ21/07 19:39
pedagandpigworker, something frightening happens when levitating Desc in Coq21/07 22:18
+pigworkerpedagand: what sort of frightening?21/07 22:18
pedagandI mean, apart from the very fact of using Coq21/07 22:18
pedagandthe levitated Desc ends up in Type(0)21/07 22:19
pedagandthe Matthes trick gives a lot of impredicativity, enough to remove all mention of "Type" in DescD21/07 22:20
pedagandI might have cocked up the model, tho. Wouldn't be surprising. I copy it on the web in a sec.21/07 22:21
pedagandhttp://coq.pastebin.com/qbruakFL21/07 22:24
pedagandanyway, it's nothing urgent. Just curiosity.21/07 22:26
pedagandnote that I could use "Set" as the target of Mu, but then it is limited to taking things in Type(1) down to Type(0).21/07 22:27
pedagandthis does not work for the levitation21/07 22:28
pedagandafter some thinking, blaming Matthes is incorrect. I probably made a mistake. Sorry for the noise.21/07 22:32
+pigworkerthis does sound worrying, in an interesting way21/07 22:48
+pigworker(btw, I was interrupted by my phone)21/07 22:49
pedagandno problem21/07 23:00
+dolioThat's weird.21/07 23:03
+dolioShouldn't 'Sigma Type ...' require the Desc in DescCases to be Desc : Type_2 (I think)?21/07 23:05
+dolioSigma Type_0 ... : Desc_1 : Type_221/07 23:05
pedagandassuming the existence of a Desc(n+1) in Type(n+2) 21/07 23:20
pedagandwe have the existence of a constructor Sigma : (S : Type(n+1)) -> ... -> Desc(n+1)21/07 23:21
pedagandwe also have a fix-point operator Mu(n+1) : Desc(n+1) -> Type(n+1)21/07 23:22
pedagandwe then write DescD(n) of type Desc(n+1) using "Sigma (Type(n)) (\s -> ...)" in several places21/07 23:22
pedagandtaking Desc'(n) to be Mu(n+1) DescD(n) should give something of type Type(n+1)21/07 23:23
pedagandright? or I'm losing my mind maybe :-)21/07 23:24
pedagand( in the Coq file, Desc' happens to be a Type(0) )21/07 23:26
pedagandmy suspicion is that MuU is not the Mu we want. But I don't understand where is my mistake.21/07 23:29
+Saizana random feeling i have is MuU needs to be interpreted21/07 23:30
+pigworkerOnce you've built Desc', does it still say Desc lives in Type(0)?21/07 23:40
+pigworkerBut even so, I don't get how Desc' can be in Type_0.21/07 23:41
+pigworkerSorry. Brain damage. I meant: is  Desc still in Type(1)?21/07 23:42
pedagandyes it is still in (at least) Type(1)21/07 23:42
+pigworkerBut this Desc is perhaps polymorphic in Coq these days...and yet Desc' should be big!21/07 23:46
+pigworkerI can't remember, offhand, how to construct Thierry Coquand's "paradox of trees", but it's worth trying...21/07 23:48
pedagandhttp://coq.pastebin.com/utWM9vf8   (I'm double-triple-checking what I'm seeing)21/07 23:55
pedagandanother possibility is that I'm mis-reading the Print Universes output. That's a possibility.21/07 23:56
pedagandyeah, that's the thing21/07 23:57
pedagandI got to understand the output of Print Universes first :-)21/07 23:58
--- Day changed Thu Jul 22 2010
pedagandtest2 is ok actually.22/07 00:07
+pigworkerv weird22/07 00:07
pedagandwhen I say, "is ok" I mean "it is of the right type"22/07 00:09
pedagandwell, I suspect I made a silly mistake in my Desc code. Will find out tomorrow. I will explore Saizan's suggestion as well (thanks btw).22/07 00:14
pedagandgood night folks, don't lose sleep, Coq is correct :-)22/07 00:16
-!- mode/#epigram [+v dolio] by ChanServ22/07 01:40
-!- mode/#epigram [+v dolio] by ChanServ22/07 02:02
+dolioI translated to Agda and got Desc : Set122/07 02:03
+dolioSo the Coq output must just be weird.22/07 02:03
+dolioOr wrong.22/07 02:03
+dolioDesc' : Set1, even.22/07 02:03
pedaganddolio, yeah, that's why I'm back: I made a mistake, that's alright22/07 02:04
pedagandI missed a bunch of constraints in Coq's output22/07 02:04
pedagandsorry to have wasted your time22/07 02:04
+dolioThe code itself seems all right.22/07 02:04
pedagandyes, I'm kind of convinced that it's doing the right thing. Doing the right thing and "set polymorphising" to the right type. Gorgeous :-)22/07 02:07
+dolioI'm not really a fan of isConst, and ConstSet, and so on.22/07 02:07
+dolioBut, I thought about indexing directly, and realized it couldn't be done.22/07 02:08
pedagandyou can do it without them?22/07 02:08
+dolioNo.22/07 02:08
+dolioconst would have to quantify over too large a type, for instance.22/07 02:10
pedagandI don't know if it's what you call "indexing directly" but you could write, say, "Sigma : forall S : Type, forall T : S -> Desc, IMu (Sigma S T)" but the size of Mu goes up then22/07 02:11
pedagandyeah, so we're talking of the same thing indeed22/07 02:11
+dolioYes, that's what I mean.22/07 02:11
+dolioI thought I was successful in doing that once, but maybe it was when I was fooling around with inductive-recursive universes.22/07 02:15
pedagandwhen your universe is "big" enough, you can fearlessly replace "Set" with a code in the universe, then interpret the code before use.  Kind of stuff pigworker is very keen on doing :-)22/07 02:26
pedagandhopefully, codes are small, so you don't get into troubles22/07 02:27
+dolioSomewhere around here I wrote an inductive-recursive universe closed under his induction-recursion desc.22/07 02:27
+dolioWhich makes me kind of suspicious.22/07 02:28
+dolioI also have an old copy of the agda executable which says his I-R desc isn't strictly positive, but the latest agda doesn't agree.22/07 02:29
pedagandIR is self-describing, isn't it? so, why would that be suspicious to achieve self-description?22/07 02:30
+dolioI guess Coq could break the tie.22/07 02:30
-!- mode/#epigram [+v soupdragon] by ChanServ22/07 02:32
+dolioWell, in the paper I read on induction-recursion, they described two different setups. One was an "external" Mahlo universe, and one was "internal".22/07 02:33
+dolioAnd I thought the difference was that the external one was like Set allowing inductive-recursive definitions, and the internal one was having some other T : Set being closed under induction-recursion somehow.22/07 02:33
+dolioAnd further, I thought they said that the internal Mahlo universe was more powerful in some sense.22/07 02:34
+dolioSo, having a U : Set closed under induction-recursion (via a desc) seems like being able to define an internal Mahlo universe, while Agda's Set is externally Mahlo.22/07 02:36
+dolioBut it's quite possible that I don't really understand all this.22/07 02:37
+dolioLikely, in fact.22/07 02:39
pedagandI see. Surely, you've seen pigworker's levitating IIR?22/07 02:39
-!- mode/#epigram [+v dolio] by ChanServ22/07 02:39
pedagandI said: "surely, you've seen pigworker's levitating IIR?"22/07 02:40
pedagandI don't know if it would address your worries22/07 02:40
+dolioI'm pretty sure that's where I got it from.22/07 02:40
+dolioHaving thought about it since I did it, it occurred to me that Set1 is involved.22/07 02:40
+dolioSo Set might qualify as an internal Mahlo universe in Set1.22/07 02:41
+dolioSo my worries may be invalid.22/07 02:41
pedaganddunno, but I promise, if I were to find out, I'll tell you :-)22/07 02:42
+doliohttp://code.haskell.org/~dolio/agda-share/universes/html/IRDataHierarchy.html22/07 02:43
+dolioThat's the code, in case you're interested.22/07 02:43
pedagandthanks, bookmarked22/07 02:43
pedagandout of curiosity, I've seen you're into categorical stuffs, and also participating to stuff like ncatlab22/07 02:44
pedagandwhat is your point of view on "type theory"?22/07 02:44
pedagandI mean, category theory seems extremely rich22/07 02:44
+soupdragonI heard that higher category theory was too complex to use as a foundation... don't really know myself if that's a reasonable statement22/07 02:45
pedagandfor example, there are so many things on ncat, it's very active, with people making deep connections into various fields of maths (and physics, and CS)22/07 02:45
pedagandI cannot find (maybe simply because I'm not looking at the right place) the same kind of "energy" in type theory22/07 02:46
+dolioMy knowledge of category theory is significantly weaker than that of type theory, I think.22/07 02:46
+dolioThe homotopy identity types seems like it might be a interesting cross-over.22/07 02:47
+dolioI don't know. I guess, off the top of my head, type theory doesn't seem as widely reaching as category theory.22/07 02:50
+dolioType theory seems like a nicer (to me, perhaps from a computational perspective) alternative to set theory.22/07 02:51
pedagandok, same feeling. Having discussed that with a colleague, he argued that type theory being constructive, we're doomed to such fate22/07 02:51
+dolioIn that you can probably build everything up out of it.22/07 02:52
pedagandindeed22/07 02:52
+dolioWhereas category theory grew out of abstracting common structure useful in various fields of mathematics.22/07 02:53
+dolioSo it tends to have more of a feel of capturing the essence of various applications.22/07 02:53
+dolioAs opposed to "you can do all of mathematics this way, but it may not be nice."22/07 02:54
+Saizanit seems to me that that CT is about discovering structure while type theory is about writing it down22/07 02:54
+dolioBut, a lot of category theory isn't foundational, either.22/07 02:54
+dolioI'm not that familiar with the foundational stuff.22/07 02:54
pedagandso, you would say that type theory cannot live on its own, while category theory provides some kind of universal language?22/07 02:54
pedagandSaizan, makes sense, yeah22/07 02:56
+soupdragonwhat about effective topos and internal logic22/07 02:56
+soupdragonAIUI category theory has an internal dependent types theory and vice versa22/07 02:57
+soupdragonI only get the CCC case with simple types though. because I can't understand these advanced constructions22/07 02:58
pedagandsoupdragon, that's the case in point I think: those category theorists can talk about stuffs, abstract them away. Modelling category theory in Agda requires Petabytes of ram.22/07 02:58
pedagands/about stuffs/about our stuffs/22/07 02:58
+soupdragonwell the problem I had was  when are two objects/morphisms/categories equal22/07 02:58
pedagandyou might want to look at [http://www.citeulike.org/user/pedagand/article/405068]. Haven't read it yet, tho, but looks roughly gentle. Glodblatt on Topoi might be a good start too, quite gentle.22/07 03:00
+soupdragonty!22/07 03:01
pedagands/Glodblatt/Goldblatt/   I should really go to sleep :-)22/07 03:01
+dolioAnyhow, Agda takes gigabytes of memory to load Data.Nat.Properties.22/07 03:01
+Saizan(is Coq as much memory hungry?)22/07 03:02
+soupdragonCheck 999999999 : nat. crashes Coq :P22/07 03:02
+soupdragonbut I don't think there are really the same problems as in Agda22/07 03:03
pedagandI won't blame anybody for eating up memory :-D22/07 03:03
+soupdragonwell not the same memory problem.. we still can't prove K or anything22/07 03:03
+dolioAnd category theory seems to naturally have some conceptually dependent types.22/07 03:05
+dolioLike, you have Hom(A,B) as a family parameterized by objects.22/07 03:05
+soupdragonyeah  Hom : Obj -> Obj -> *22/07 03:06
+dolioWhen you formulate category theory in set theory, you do ugly stuff like having a set (or class) of all arrows, and then partial functions for composition of arrows, which test equality of the relevant objects.22/07 03:06
+soupdragonI like the idea of axiomatizing SET but I'm only about half way through this book22/07 03:07
pedagandI have been told that this leads to issues on some cases and that, in the end, both approaches have their strength and weakness22/07 03:07
+dolioI have some book that I haven't read yet about formulating category theory from the ground up, and it describes what it calls 'first-order logic with dependent sorts' for doing it.22/07 03:08
pedagandI had been given a very precise example but I cannot remember22/07 03:08
+dolioFOLDS.22/07 03:08
+soupdragonyeah read a little about FOLDS on n-cat22/07 03:08
+dolioI believe it tries to stick to constructivism, too.22/07 03:08
pedagandmmh, interesting. I should get my hand on it.22/07 03:09
+dolioI'm not sure that a category-theoretic foundation is that much different from a type-theoretic one, though.22/07 03:11
+dolioAnd presumably you can make in constructive.22/07 03:11
+dolioInstead of saying "these types and functions exist" you say "these categories and functors exist."22/07 03:11
+dolioAnd given the homotopy type theory stuff, I guess the former might end up being a special case of the latter.22/07 03:13
+soupdragonwhat does homotopy identity type do ? :)22/07 03:13
+dolioIf you go on to "these n-categories exist", then n-groupoids are special cases of n-categories, and if types are n-groupoids...22/07 03:14
+dolioI don't fully understand the homotopy stuff, though.22/07 03:16
pedagand(thanks for the chat folks, very instructive. I have to leave, sadly.)22/07 03:20
-!- mode/#epigram [+v dolio] by ChanServ22/07 03:39
-!- ServerMode/#epigram [+v edwinb] by holmes.freenode.net22/07 04:31
-!- ServerMode/#epigram [+v edwinb] by holmes.freenode.net22/07 05:30
-!- mode/#epigram [+v dolio] by ChanServ22/07 06:43
-!- mode/#epigram [+v dolio] by ChanServ22/07 07:39
-!- mode/#epigram [+v dolio] by ChanServ22/07 13:43
-!- mode/#epigram [+v dolio] by ChanServ22/07 14:39
+pigworkerpedagand, moleris, tsapi: I've just noticed that we're not so consistent about \mapsto versus = for definitions.22/07 16:05
-!- mode/#epigram [+v dolio] by ChanServ22/07 16:39
pedagandpigworker, ha, indeed22/07 17:04
+pigworkerI'm also a bit nervous about thin/fat horizontal/vertical space in tuples.22/07 17:04
+pigworkerMore moreover, I'm troubled by either the presence or the absence of trailing 'const 1 in IDesc 1 descriptions.22/07 17:06
+pigworkerWe need to sort our LISP out!22/07 17:06
pedagandas for const 1 in IDesc, we already knew that22/07 17:06
pedagandI took on me to write something slightly incorrect, for the sake of simplicity22/07 17:07
+pigworkerI've just written the upgrade : Desc -> IDesc 1 function.22/07 17:08
+pigworkerI think I'm a little less troubled if we *do* have const 1 at the end (with const a=b for indexed things)22/07 17:09
pedagandno problem, that's fine with me22/07 17:09
+pigworkerI'll push what I've got (start of sec 5) and keep going.22/07 17:10
pedagandok22/07 17:11
+pigworkerdone22/07 17:11
+pigworkerThis sunshine is tempting me to go out, though...22/07 17:12
pedagandas for tuples, I had checked them some time ago, they looked coherent, but I didn't noticed a thin/fat distinction, and for me horizontal/vertical has no semantics difference22/07 17:12
+pigworkerwe have things like   ['const 1   'var []], where thin and fat are different22/07 17:13
pedagandbleh22/07 17:14
pedagandso, the empty tuple is typeseted "[]" in fat, all right. Why would any other bracket by typeseted in fat? what's the meaning of fatness?22/07 17:16
pedagandif Ms Tolles were reading this discussion, she would freak out and send another row of emails :-D22/07 17:17
pedagandbtw, please do go enjoy sunshine, it won't reappear before next year, maybe22/07 17:18
+pigworkerI mean that the gap between 1 and 'var is different from the gap after 'var22/07 17:19
pedagandha.....22/07 17:19
pedagandwho got this bright idea of giving semantical importance to space? ACM will be delighted to know that our paper is written in Whitespace.22/07 17:22
pedagandanyway, I'll take care of that and =/\mapsto22/07 17:23
+edwinbFundamenta Informaticae decided that the whitespace in one of our haskell code samples wasn't important...22/07 17:23
+pigworker[(`const 1) (`var [])] might do it22/07 17:24
+pigworker' not `22/07 17:24
+pigworkerWadler's Law strikes again...22/07 17:24
pedagandpigworker, I'm kidding, no worry :-) it's rather interesting to see differences in people's perceptions of "symbols"22/07 17:27
+pigworkeryeah, but ultimately it comes down to machine perception of symbols, and they're a bit less telepathic; people aren't usually as good at telepathy as they are at delusion22/07 17:29
pedagandwell, it never comes down to a machine. It comes down to the brave human implementing a parser. With Epigram's hieroglyphic syntax, we have a proof that computer are better than humans when it comes to perception of symbols...22/07 17:39
-!- mode/#epigram [+v dolio] by ChanServ22/07 17:39
pedagandor maybe that's where your discussion about delusion kicks in :-)22/07 17:39
+pigworkeryeah, but our paper notation seems to require a space-measuring-and-comparing parser, where brackets or punctuation might be clearer22/07 17:47
pedagandI completely agree. Good ol' brackets.22/07 17:50
+pigworkeroh yeah, let's drop brackets on rightmost lambdas, so 'sigma S \s -> T, not 'sigma S (\s -> T); we do it often but not always22/07 17:57
pedagandI did a pass to check that. I'll do another one.22/07 17:58
pedagandI've pushed my changes on first sections22/07 17:58
pedagandbtw, the paper we submit is a \MonochromeEpigram, or a color one?22/07 18:00
+pigworker\MonochromeEpigram22/07 18:01
+pigworkerI'm contemplating 'k for 'const; the ACM are making that hard to resist.22/07 18:35
pedagandfeel free22/07 18:44
+pigworkerjust pushed a patch with some of this reorganisation22/07 18:58
-!- mode/#epigram [+v dolio] by ChanServ22/07 19:42
+pigworkerand some more adjustments along the same lines22/07 20:00
pedagandtransformed the = to \mapsto22/07 20:14
pedagandstarring at whitespaces right now22/07 20:14
-!- mode/#epigram [+v dolio] by ChanServ22/07 20:42
pedagandwhen you need red square brackets, it's \sqr{...}. I'm fixing the one you missed, no need to go back.22/07 20:47
pedagandyou will want to update the free monad presentation of IDesc to include 'k 1 as well22/07 21:02
--- Day changed Fri Jul 23 2010
-!- mode/#epigram [+v dolio] by ChanServ23/07 01:42
-!- mode/#epigram [+v dolio] by ChanServ23/07 03:39
-!- koninkje_away is now known as koninkje23/07 03:49
-!- mode/#epigram [+v soupdragon] by ChanServ23/07 05:27
-!- mode/#epigram [+v dolio] by ChanServ23/07 05:42
-!- mode/#epigram [+v pigworker] by ChanServ23/07 09:26
pedagand(pushed a few things on Section 5, currently fixing colours in Section 5)23/07 09:31
pedaganddamnit, I've a brit' ispell version. Forbidden to write 'color'.23/07 09:31
-!- mode/#epigram [+v dolio] by ChanServ23/07 09:35
+pigworkerquite right too; this paper will have British spelling; I wouldn't make you write in Belgian23/07 09:47
pedagand:-)23/07 09:51
+pigworkeror is it your IRC client which moans?23/07 09:51
pedagandyeah, IRC client. But same ispell in emacs, so the paper gets the same treatment. I'll follow your suggestion and make an #epigram-be, where my ispell will be switched to 'dict-us' :-)23/07 09:57
+pigworkerawesome!23/07 09:58
pedagandI went through the Section 5 todo list. Only remaining item: merging Discussion and Conclusion. Do you want to take it, or should I go for it?23/07 10:05
pedagandwe need to make plenty of space, too23/07 10:05
+pigworkerI'm happy to do it. I need to work through that stuff anyway. We need to do a bit of boiling, but we might also edit the .bib file to produce more abbreviated entries (another thing I learned from James McKinna).23/07 10:09
pedagandok, I take the bibtex boiling23/07 10:11
+pigworkerevery para whose last line is less than half a column gets some hard staring!23/07 10:16
pedagandgot a tvlicensing ordeal, yeah! But it's not really mine: my address, not my name. I'm a bit sad :-(23/07 10:49
pedagandboiling the bibtex bring us to 7 lines over the page limit. That was quite effective.23/07 10:50
pedagandplus your patch, we're in the 12 pages zone again. Fear not Lisa, we will make it!23/07 10:52
+pigworkerthose tv licensing people just don't listen or learn23/07 11:17
+pigworkerdo you have a tv?23/07 11:17
pedagandnop, I've many perversions but not this one :-)23/07 11:18
+pigworkerthen ignore the spam; if by freak chance they do show up, tell them you're not the person they have on their records, you don't have a tv, and they can't come in without a warrant23/07 11:19
+pigworkerthey're like vampires, basically23/07 11:20
pedagandyeah, after visiting their website, I really feel like a criminal23/07 11:20
pedagandanyway, that's an interesting bit of British culture, imo23/07 11:21
pedagandI mean, not that you guys are all vampires :-D I should stop there, I won't make a living in social studies with such analogies23/07 11:24
+pigworkerbut indeed, we have to be invited in23/07 11:25
+pigworkerI'm not sure the free monad counts as a "type-indexed datatype" because the construction is parametric in the functor. That makes things shorter!23/07 11:36
+pigworkerJust pushed and pulled. We'll soon have enough space to expand your skyhook footnotes.23/07 11:40
pedagandpigworker, shall I mention the Coq model when talking about set polymorphism in the skyhook subsection?23/07 13:29
+pigworkerthat just builds the types, right?23/07 13:30
+pigworkerbut Coq makes it polymorphic?23/07 13:31
+pigworkeryes, it's worth saying that Coq admits layers of the construction with the levels we claim23/07 13:32
pedagandyes23/07 13:32
pedagandfeel free to ditch skyhooks, I'm checking that we can indeed type-check from Desc42 to Desc0 (before the heat death of the Universe)23/07 14:19
-!- mode/#epigram [+v dolio] by ChanServ23/07 14:38
pedagandheat death of the Universe looks like a more plausible outcome :-(23/07 14:56
+pigworkeriz in ur huttonzrazr flattening ur tuples23/07 14:56
+pigworkerwill 5 do?23/07 14:57
+pigworkerheat death of Universe passes termination check but fails positivity23/07 14:57
pedagand:-)23/07 15:01
pedagandChecked! 23/07 15:11
pedagandDesc42 hardcoded, walked down to Desc0. Yes, I know, I've strange hobbies.23/07 15:12
+pigworkerGordon Bennett!23/07 15:19
+pigworkerI'm still shaving bits off the HR example. I think we have enough room to give the type of cataI now.23/07 15:20
-!- mode/#epigram [+v pigworker_] by ChanServ23/07 15:26
-!- pigworker_ is now known as pigworker23/07 15:26
pedagandI can write the type of cataI. Or you've already done that?23/07 15:28
+pigworkergo ahead!23/07 15:29
pedagandjust the type, right? not the full implementation23/07 15:30
+pigworkerjust the type23/07 15:32
+pigworkerbtw, did you ever try the HR example using the free monad just to add variables, leaving the values as part of the signature?23/07 15:33
-!- mode/#epigram [+v dolio] by ChanServ23/07 15:39
pedagandnop23/07 15:45
pedagandwhat would be the benefit?23/07 15:45
+pigworkerI suspect it's cleaner as a program. As an explanation, we could say "free monad adds variables - here's what we had before, now there are variables"; we might not need to renegotiate the original signature.23/07 15:49
pedagandcould do. I start updating the model and if it goes well, we can update the text23/07 15:56
+pigworkerworth a try, I think23/07 15:58
+pigworkerI'll pop over, if only to get a printout.23/07 15:58
-!- mode/#epigram [+v dolio] by ChanServ23/07 16:42
-!- mode/#epigram [+v pigworker] by ChanServ23/07 17:44
-!- koninkje is now known as koninkje_away23/07 18:38
-!- mode/#epigram [+v pigworker] by ChanServ23/07 21:34
-!- mode/#epigram [+v dolio] by ChanServ23/07 21:42
pedagandpigworker, with values part of the signature, the definition of a "closed term" becomes a bit strange: it needs to be a free monad of something23/07 21:57
pedagandin what I pushed, it is the free monad over Empty _ = Void23/07 21:57
+pigworkera free monad with an empty variable set23/07 21:57
+pigworkerclosed term is term with no variables; strange?23/07 21:58
pedagandok, so I did it right23/07 21:58
+pigworkeryes23/07 21:58
+pigworkerAs my old mathematics teacher says "a mathematician is someone who knows that x is x+0"23/07 21:59
pedagandnot strange, but I was scared of introducing new material23/07 22:00
pedagandshall I update the text now wrt. the new model, or wait you're done shaking it?23/07 22:01
+pigworkerif you're still active, don't let me stop you; I'm done for the day23/07 22:03
+pigworkerI can also stay away from that bit in the morning...23/07 22:03
pedagandI'll be glad to be done with that paper, so I'm going to finish this tonight. After that, my todo list is empty. I'll do the Sheridan clean up when you call it a day.23/07 22:12
pedagandobviously, if you see stuff I can help with, let me know23/07 22:12
-!- mode/#epigram [+v dolio] by ChanServ23/07 22:38
pedagandpigworker, how would you like the empty set to be represented today, sir?23/07 23:23
pedagandwe have "1" for Unit, I could pick "0"23/07 23:25
pedagandbut 0 is already taken by the 0 constructor of EnumT. Gosh.23/07 23:25
pedagandhey, "()" almost looks like "0". Here I go. It's \Zero in pig.sty, feel free to change it.23/07 23:27
--- Day changed Sat Jul 24 2010
-!- mode/#epigram [+v dolio] by ChanServ24/07 00:42
-!- mode/#epigram [+v pigworker] by ChanServ24/07 01:31
-!- mode/#epigram [+v dolio] by ChanServ24/07 01:39
-!- mode/#epigram [+v soupdragon] by ChanServ24/07 02:53
-!- mode/#epigram [+v dolio] by ChanServ24/07 03:02
-!- mode/#epigram [+v dolio] by ChanServ24/07 09:38
-!- mode/#epigram [+v dolio] by ChanServ24/07 11:38
-!- mode/#epigram [+v pigworker] by ChanServ24/07 13:06
-!- mode/#epigram [+v dolio] by ChanServ24/07 13:38
-!- mode/#epigram [+v pigworker] by ChanServ24/07 17:14
-!- mode/#epigram [+v pigworker] by ChanServ24/07 23:36
--- Day changed Sun Jul 25 2010
-!- mode/#epigram [+v codolio] by ChanServ25/07 05:41
-!- codolio is now known as dolio25/07 05:56
-!- mode/#epigram [+v soupdragon] by ChanServ25/07 06:00
-!- mode/#epigram [+v pigworker] by ChanServ25/07 10:13
pedagandpigworker, do you have any edition pending in your repos?25/07 14:17
+pigworkernot at the moment; hopefully that will change later today25/07 14:18
pedagandok25/07 14:23
pedagandyou like tight deadlines, do you? it's your way to get that adrenaline rush :-)25/07 14:26
pedagandyou know, Livi tower is 13/14th floor, you could do base jumping from there, that's excellent for adrenaline too25/07 14:27
+pigworkerI'm just exhausted.25/07 15:07
+pigworkerOK, I'm going to merge sections 6 and 7 now.25/07 15:24
pedagandjust pushed a few fixes, pull before that25/07 15:26
+pigworkerok; by the way, should we just use #[] for the empty type here, rather than inventing something else?25/07 15:40
pedagandha, makes sense, indeed25/07 16:08
pedagandI fix that25/07 16:08
pedagandpushed25/07 16:10
-!- mode/#epigram [+v dolio] by ChanServ25/07 16:42
+pigworkerJust one back section now "Discussion", but with more subsections: I've pushed.25/07 18:49
pedagandthanks25/07 18:51
pedagandlooks very nice25/07 18:52
+pigworkerJust pushed a small tweak to the abstract, too.25/07 18:52
+pigworkerwe need our ACM classifiers now...25/07 18:53
pedagandgoodo25/07 18:53
pedagandyeah, this is so extraordinarily annoying to do25/07 18:54
+pigworkerI've got another two to do, so I'd be glad if you made a first attempt...25/07 18:55
+pigworkerI must confess, I'm thinking of permuting the examples again, although your new version is a big improvement. I'm mindful of time, though.25/07 18:56
pedagandyep, sure25/07 18:56
pedagandpermuting which examples? all of them? or moving Hutton earlier?25/07 18:57
+pigworker5.2 and 5.3 examples; specifically, introducing HR before freemo; then 5.3 freemo, freemo for Hutton, freemo for IDesc25/07 18:58
+pigworkerso HR-with-no-var acts as an example for tagged indexed descriptions, then no-var motivates freemo25/07 19:01
+pigworkerour "VERY HARD" deadline is 2pm tomorrow; I'm keen to stop thinking tonight, then print and tidy in the morning25/07 19:04
pedagandyep. You don't have to tell me twice to stop thinking :-) I do these keywords and so on.25/07 19:05
+pigworkershould I try that permutation of examples?25/07 19:05
pedagandI had a version with HR as you suggest it, just wasn't pleased with the redundancy I was supposed to be removing with the re-shaping25/07 19:06
pedagandnop, I can do it, that's fine25/07 19:06
pedagandI'll submit it as a standalone patch, rollback will be easy anyway25/07 19:06
+pigworkerhow easy is it to write a generic operation from "open terms with no variables" to "closed terms"?25/07 19:09
pedagandit ought to be rather easy: take the constructor tag, add one, done.25/07 19:12
pedagandnow, let me verify this bold claim with my Swedish fellow..25/07 19:12
+pigworkersounds very plausible25/07 19:13
+pigworkerso many ways to skin that cat...25/07 19:16
pedagandso, it takes 2 lines, one for the type, one for the cata+algebra25/07 19:21
pedagand4 lines if you use pattern matching and a where clause25/07 19:22
pedagandI guess, I can play it this way. Will see what happens space-wise...25/07 19:23
+pigworkerother possibility is to show how to extend an alg for (de D) to one for (de (D * X)) by providing a "var case"25/07 19:24
pedagandso, a generalisation of "turning open with no variable" to "closed", where the provide the behavior in the var case, right?25/07 19:31
+pigworkeryeah, effectively fusing subst-to-no-var, no-var-to-closed, eval-closed25/07 19:32
-!- mode/#epigram [+v dolio] by ChanServ25/07 19:38
+pigworkergot to step away a moment; back soon25/07 19:52
-!- mode/#epigram [+v pigworker] by ChanServ25/07 20:27
pedagand(sorry, got a phone call. I'm still in General Terms with ACM.)25/07 20:30
+pigworkerI know, it's torture. Moreover, google...25/07 20:52
+pigworkerI'm adding level annotations to Desc levitation.25/07 20:53
pedagandall right, kicked general terms out of the door25/07 20:57
pedagandyou'll end up in a strange situation when annotating the switchD part. But if you have a good story for it, well, have fun.25/07 20:58
+pigworkerI was wondering where the mines were...25/07 20:59
+pigworkerI've pushed a patch. I think it's ok, but I'm tired. We're almost there, I think. The ACM metadata seems fine. Let's make up some keywords (levitation!) in the morning.25/07 22:08
pedagandjust in case: keywords are not mandatory25/07 22:13
pedagandI'm still in the reshaping of freemo. We can check that tomorrow.25/07 22:16
+doliopigworker: So, I glanced at the levitation paper after pulling from the epigram repository, and seeing some of the discussion in the patches...25/07 22:34
+dolioAnd was wondering: is induction-recursion still considered suspicious?25/07 22:34
+pigworkerit depends who you're trying to convince25/07 22:35
+pigworkerthere's a set-theoretic model, but no SN proof25/07 22:35
+dolioAh, okay.25/07 22:35
+dolioI guess the fact that it's a wacky set-theoretic model doesn't help.25/07 22:36
+pigworkerno doubt25/07 22:36
+pigworkerand we're very much in the territory of needing to swallow the dog to catch the cat...25/07 22:37
+pigworkerhow do we know this ordinal exists? because we can think of a bigger one!25/07 22:38
+soupdragongentzen: the man who proved induction using induction25/07 22:43
+pigworkerlittle fleas nead bigger fleas, for nutrition, if nothing else25/07 22:49
pedagandpushing freemo re-re-shaping25/07 22:53
pedagandstill 12 pages, I cannot believe. Aleluia.25/07 22:53
pedagandthe question of "making sense" is of very little importance, especially at this time of the day, with a fire alarm ringing in the facing building.25/07 22:54
+pigworkergood luck!25/07 22:54
pedagandoh that happens every now and then. Otherwise, it's people trying to break into the building next to mine, under work.25/07 22:56
pedagandI live in a very lively place, never boring25/07 22:56
+pigworkerfree entertainment is sometimes a good thing25/07 22:59
+pigworkerI've pulled your patch. It's flowing well now: I think it was worth doing. Thanks.25/07 22:59
pedagandmade a mistake in \update, fixing it now25/07 22:59
pedagandfree entertainment is good, excepted when they want to break into *your* building, or *your* flat. They tried both... :-)25/07 23:01
+pigworkerI might tweak the words a little. You have an "Obviously". We don't use that word. We're Not Allowed.25/07 23:02
pedagandhaha, true. Go ahead, no offence taken.25/07 23:02
+pigworkerNone intended. "Obviously" is an intimidation word: we get all the intimidation we need from the actual content.25/07 23:04
+dolioWow, you guys really do have a file with Desc copy-pasted 43 times.25/07 23:08
pedagandthat's true, especially in monochrome, that's pretty scary, looks very serious and clever. Ha, if only people knew... :-)25/07 23:09
pedaganddolio, look at DescStrat.lhs25/07 23:09
+dolioYeah, I am right now. :)25/07 23:09
pedagandI suspect it's even worse to look at the haskell file than the result :-)25/07 23:09
+dolioI didn't read the foot note before. I figured you started at something like 4, just to prove the point.25/07 23:09
+dolioStuff like Lift37 is unfortunate.25/07 23:11
pedagandyou mean, all the Lift* or there is something peculiar about Lift37?25/07 23:12
+dolioI guess that's the difficult half of universe polymorphism.25/07 23:12
+dolioLift in general.25/07 23:12
pedagandha, yeah25/07 23:12
pedagandfear not, we are on the case! Hem.. Maybe. One day.25/07 23:13
+dolioYeah, I skimmed Stratisfaction, too.25/07 23:13
pedagandpoor of you...25/07 23:13
+pigworkerbut we certainly need to put some breathing space between the two25/07 23:13
+dolioThe Agda folks had discussed something along those lines back when universe polymorphism first appeared, as I recall. But it's still not here yet.25/07 23:14
+doliopedagand: Well, I kind of stopped reading once the pages got especially colorful.25/07 23:14
+pigworkerIt's clear that lack of lifting promotes abstraction over multiple levels, hence some fairly gory Agda.25/07 23:17
+dolioYes.25/07 23:17
+dolioCategory theory is especially fun.25/07 23:17
+pigworkerI'll bet.25/07 23:18
+dolioYou need two indices for categories (objects and arrows). Then functors go over two categories, so they have four levels.25/07 23:18
+dolioNatural transformations may have 8. I forget.25/07 23:18
+dolioActually, no, the functors would have to have the same 4.25/07 23:19
+soupdragonbut what about when you make new categories out of old ones?25/07 23:19
+soupdragonso 'natural transforms' are just arrows25/07 23:19
+pigworkerGaah! We're hoping to abstract the base level, but fix the gaps between levels. For that, you need lifting to work as well.25/07 23:19
+soupdragonoh it's not levels like I was thinking 25/07 23:20
+soupdragonlevels like Type[0] : Type[1] : Type[2] : ..25/07 23:20
+pigworkeryeah, predicative hierarchy misery25/07 23:20
+dolioFunctor {i j k l} (C : Category {i} {j}) (D : Category {k} {l}) : Set (i \lub j \lub k \lub l) ...25/07 23:21
+pigworkerand i \lub lucy isn't lucy \lub i ?25/07 23:21
+dolioI think it is. Agda has a special solver/reducer for levels.25/07 23:22
+pigworkeranother colostomy bag on the kernel?25/07 23:22
+dolioSo 'suc j \lub j' gets reduced to 'suc j' even though j is a variable.25/07 23:22
+pigworkernot too bad if it's a reducer25/07 23:23
+dolioWell, it isn't just a reducer, I think.25/07 23:23
+dolioYou can fill in certain bad signatures and it won't error out, but generate unsolved meta-constraints or something..25/07 23:24
+pigworkerI think they're getting it cheap from Andreas Abel's sized type stuff.25/07 23:25
+dolioOr it used to...25/07 23:26
+dolioMy initial test didn't work.25/07 23:26
+dolioMaybe it doesn't do that anymore.25/07 23:26
+dolioI think you used to be able to do something like: 'record Foo {i j} (A : Set i) (B : Set j) : Set i where field { a : A ; b : B }'...25/07 23:27
+dolioAnd at the bottom of the emacs mode, you'd get something like 'j <= i', but not an error.25/07 23:28
+pigworkerThat looks like it could get hairy.25/07 23:28
+dolioOh, I got one.25/07 23:29
+dolioIf you add an extra level k, and C : Set k, and have the record : Set (i \lub j) with a field c : C...25/07 23:29
+dolioYou get Set k <= Set (i \lub j).25/07 23:29
+dolioSo I guess it only fails to reject when a \lub is involved or something.25/07 23:30
+pigworkersounds plausible, if a bit arbitrary25/07 23:30
+dolioYeah, you'd think that'd be a straight forward inference to k =< i or k =< j, both of which it rejects on its own.25/07 23:31
+pigworkerI can't help thinking it's too much polymorphism in the wrong place. I think it's work applying some thought. Thanks, pedagand.25/07 23:32
pedagandpigworker, have you been compiling the paper with latex or you used the pdflatex-based makefile?25/07 23:45
+pigworkerI've been doing the make thing.25/07 23:46
pedagandokidoki25/07 23:46
pedagandgosh, I scared myself to death... I thought the postscript was broken, it's actually my viewer which is fancy. Sorry for the noise.25/07 23:50
pedagandno worry Lisa, you will get it T1 encoded, all right25/07 23:51
pedagandas for set polymorphism, Hank convinced me that it's not polymorphism we need, but a reflection principle (that we might have in Stratisfaction). Anyway, I'm far from done right now...25/07 23:54
pedagandwell, I call it a day for today. See you tomorrow!25/07 23:59
--- Day changed Mon Jul 26 2010
pedagand(bad luck, we are already tomorrow)26/07 00:00
-!- mode/#epigram [+v pigworker] by ChanServ26/07 00:40
-!- mode/#epigram [+v pigworker] by ChanServ26/07 01:51
-!- mode/#epigram [+v dolio] by ChanServ26/07 02:41
-!- mode/#epigram [+v dolio] by ChanServ26/07 04:41
-!- mode/#epigram [+v dolio] by ChanServ26/07 06:41
-!- mode/#epigram [+v dolio] by ChanServ26/07 08:38
-!- mode/#epigram [+v pigworker] by ChanServ26/07 09:24
-!- mode/#epigram [+v dolio] by ChanServ26/07 09:41
pedagand(I've catched a few belgianism with ispell, just pushed)26/07 09:52
+pigworkerthanks; just finishing my second coffee; there in 3026/07 10:01
pedagandnot a good day for base jumping, don't bother taking your equipment :-)26/07 10:06
-!- mode/#epigram [+v soupdragon] by ChanServ26/07 11:31
-!- mode/#epigram [+v pigworker] by ChanServ26/07 12:15
pedagandgoddammit, finally done with icfp! Ha, if I can get my hand on this reviewer #2 that made us rewrite the paper, I will.. I will.. I will offer him a beer! :-)26/07 13:46
ccasinI'm looking at your icfp paper again today, so if there is a new version I'd love to see it :)26/07 13:51
pedagand;-)26/07 13:55
ccasinof course, I am not responsible for any of the reviews26/07 13:55
pedagandof course26/07 13:56
pedagandthat goes without saying :-)26/07 13:57
ccasin:) I would love to have a look at the final version though, if it's done26/07 13:57
ccasinor perhaps the version on your website is the final one?26/07 13:58
pedagandI'm putting in on my website, in a sec26/07 13:59
ccasinI don't mean to imply it is deficient :)26/07 13:59
pedagandhere you go: http://personal.cis.strath.ac.uk/~dagand/stuffs/levitation.pdf26/07 14:00
pedagandsorry, I've to run away. Talk right now.26/07 14:00
ccasinwonderful, thanks26/07 14:00
pedagandsee you later26/07 14:00
ccasinlater26/07 14:00
-!- mode/#epigram [+v dolio] by ChanServ26/07 15:37
-!- mode/#epigram [+v dolio] by ChanServ26/07 17:41
-!- koninkje_away is now known as koninkje26/07 19:47
-!- mode/#epigram [+v pigworker] by ChanServ26/07 21:22
-!- mode/#epigram [+v pigworker_] by ChanServ26/07 21:24
-!- pigworker_ is now known as pigworker26/07 21:24
--- Day changed Tue Jul 27 2010
-!- koninkje is now known as koninkje_away27/07 00:28
-!- mode/#epigram [+v dolio] by ChanServ27/07 00:53
-!- mode/#epigram [+v pigworker] by ChanServ27/07 01:00
-!- mode/#epigram [+v dolio] by ChanServ27/07 01:04
-!- mode/#epigram [+v dolio] by ChanServ27/07 02:05
-!- mode/#epigram [+v dolio] by ChanServ27/07 04:04
-!- mode/#epigram [+v codolio] by ChanServ27/07 04:29
-!- mode/#epigram [+v dolio] by ChanServ27/07 05:02
-!- ServerMode/#epigram [+v dolio] by holmes.freenode.net27/07 05:14
-!- ServerMode/#epigram [+v dolio] by holmes.freenode.net27/07 05:19
-!- mode/#epigram [+v dolio] by ChanServ27/07 06:04
-!- mode/#epigram [+v dolio] by ChanServ27/07 07:04
-!- mode/#epigram [+v soupdragon] by ChanServ27/07 08:43
-!- moleris_ is now known as moleris27/07 10:51
-!- mode/#epigram [+v soupdragon] by ChanServ27/07 11:35
-!- mode/#epigram [+v dolio] by ChanServ27/07 15:01
-!- mode/#epigram [+v soupdragon] by ChanServ27/07 18:01
-!- mode/#epigram [+v pigworker] by ChanServ27/07 20:14
copumpkinoh my!27/07 20:36
-!- koninkje_away is now known as koninkje27/07 20:42
-!- mode/#epigram [+v dolio] by ChanServ27/07 21:04
-!- koninkje is now known as koninkje_away27/07 22:46
--- Day changed Wed Jul 28 2010
-!- mode/#epigram [+v dolio] by ChanServ28/07 00:04
-!- mode/#epigram [+v dolio] by ChanServ28/07 02:04
-!- koninkje_away is now known as koninkje28/07 06:18
-!- koninkje is now known as koninkje_away28/07 06:55
-!- mode/#epigram [+v soupdragon] by ChanServ28/07 07:33
-!- mode/#epigram [+v pigworker] by ChanServ28/07 09:56
-!- mode/#epigram [+v dolio] by ChanServ28/07 10:04
-!- mode/#epigram [+v dolio] by ChanServ28/07 16:04
pedagandmoleris, "Epigram Prime: A Demonstration" at MSFP'10? what??28/07 16:16
pedagandor maybe didn't till five minutes ago that you were giving a demo of *Epigram*28/07 16:18
pedagands/didn't/didn't knew/28/07 16:19
molerispedagand: Heh, err yeah tsapi asked me a while back28/07 16:40
molerisscary stuff28/07 16:40
pedagandyou've already thought about what to demo? 28/07 16:40
molerisnope28/07 16:42
pedagandI mean, that's a good ordeal, so that we get our act together and finally do this high-level language. I've some snippets of code, but it's nowhere near something usable28/07 16:42
molerisI was kinda hoping Epigram would be in a better state by then28/07 16:43
molerishow was your summer looking before I said that? ;)28/07 16:43
agundryhooray for optimism28/07 16:43
pedagandho, my summer was doomed anyway :-) Just, I'm always hesitating between investing myself in Epigram or focusing more onto "theoretical" stuffs28/07 16:44
molerisagundry: When's the camera ready version of your paper due?28/07 16:44
agundrymoleris: monday, but hopefully it will be shipped sooner28/07 16:44
molerisEpigram Epigram Epigram28/07 16:45
pedagandbut that Epigram guy won't get me a PhD :-) that's what I'm scared of..28/07 16:45
molerisplenty of time for that28/07 16:46
pedagandlooking at my progress so far, I really doubt it, but anyway.. Maybe you should set some milestones, stuff you would like to be able to demonstrate28/07 16:48
pedagandthis would give some incentive to "get things done"28/07 16:48
pedagandbtw, pigworker was talking of changing completely the term representation and introducing stratification at the same time28/07 16:49
agundryIt has been a long time since we last implemented the lambda calculus...28/07 16:50
moleriseurgh, not again ;)28/07 16:50
molerisI should come visit you guys soon anyway - see if we can't come up with a plan28/07 16:51
pedagandsummer sales, 70% off on your term representation28/07 16:51
agundrymoleris: that would be good28/07 16:52
pedagandyep, definitely28/07 16:52
agundrypigworker is officially on holiday, but I suspect Epigram counts as having fun as far as he's concerned28/07 16:52
molerisas long as he doesn't show his face in the dept. or something... 28/07 16:53
molerisWell when he's around we should see if we can't arrange something28/07 16:54
-!- mode/#epigram [+v pigworker] by ChanServ28/07 18:05
+pigworkeragundry: I just pushed a patch that gets us back down to 12 pages...28/07 18:05
agundrypigworker: thanks, I'm sure I can break the limit again soon ;-)28/07 18:06
agundryone conflict but it's easy to fix28/07 18:06
+pigworkercool28/07 18:06
agundryI like 'dependent' generalisation28/07 18:06
+pigworkeranything to save a line28/07 18:10
agundryI've just pushed a few changes because I'm worried about getting too far from the main tree28/07 18:14
agundrysection 9 isn't coherent yet28/07 18:14
+pigworkeryou have the token28/07 18:14
-!- mode/#epigram [+v dolio] by ChanServ28/07 19:04
-!- mode/#epigram [+v dolio] by ChanServ28/07 22:04

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