/home/laney/.irssi/irclogs/Freenode/2010/#epigram/June.log

--- Log opened Thu Jun 03 14:33:47 2010
-!- Irssi: #epigram: Total of 7 nicks [0 ops, 0 halfops, 0 voices, 7 normal]03/06 14:33
-!- Irssi: Join to #epigram was synced in 0 secs03/06 14:33
Laneyevening03/06 14:33
molerisLaney: How are the logs coming along?03/06 14:36
Laneyall good boss: http://epigram.orangesquash.org.uk/2010/June.log.html03/06 14:38
molerisAnother day, another strictness bug to squash03/06 14:52
pedagandmoleris, I'm curious: what do you do that triggers them so easily? is it something in the Data tactics?03/06 15:10
molerispedagand: Using induction or iinduction specialised to EnumD, DescD, IDescD03/06 15:36
molerisin order to do some generic programming basically03/06 15:37
moleristhis time it was a canTy rule from Enum.lhs03/06 15:38
molerisI was trying to write tabulate, the inverse of switch03/06 15:38
pedagandmoleris, ok03/06 17:19
pigworkermoleris: if you can make sense of the new OpTree machinery, you can write operators without strictness bugs03/06 20:26
pigworkerLaney: thanks very much for the lovely logging03/06 20:27
* edwinb waves at the people reading the logs03/06 20:39
shapryou screamt?03/06 23:23
soupdragonlook there's 11 people here03/06 23:24
soupdragonwtf!03/06 23:24
shaprThat's awesome!03/06 23:24
shaprpigworker: If you'll register your irc nick, I'll add you to the ops list03/06 23:25
shaprToo long since I've used chanserv, I'm trying to figure out how templates work.03/06 23:27
Saizanshapr: so you continue the tradition of founding irc channels for functional languages?:)03/06 23:27
pigworkershapr: I'm kinda new to IRC; where do I need to poke something?03/06 23:27
shaprI started #concatenative too :-)03/06 23:28
soupdragonwhat03/06 23:28
shaprpigworker: /msg nickserv help register03/06 23:28
shaprpigworker: That'll give you the directions for registering your account.03/06 23:28
shaprI started a bunch of channels, but only a few of them have gone places.03/06 23:29
* shapr shrugs03/06 23:29
shaprThese days I do more meatspace organizing, my time is going into being a makerspace cofounder.03/06 23:29
shaprMe and ybit03/06 23:29
pigworkershapr: done; thanks for that03/06 23:31
shaprOk, as soon as I figure out how priv assignment has changed, you get as much ops power as I can give you.03/06 23:32
-!- mode/#epigram [+o shapr] by ChanServ03/06 23:33
-!- shapr changed the topic of #epigram to: http://www.e-pig.org/ | Epigram - Programming Language with Dependent Types03/06 23:34
@shaprpigworker: visited #haskell already?03/06 23:47
pigworkerlurked briefly, but it whizzes by so fast!03/06 23:48
edwinbI can't keep up with #haskell...03/06 23:49
pigworkeron a completely unrelated topic, was code golf invented because of ACM 2-column format?03/06 23:52
edwinbheh03/06 23:54
edwinbghc is irritating me by producing inexplicably fast code that epic can't get near03/06 23:59
--- Day changed Fri Jun 04 2010
edwinbI think it might be being much cleverer at memory allocation04/06 00:01
pedagandedwinb, I've a linux machine at hand and a week-end starting in 24 hours: if you need an oprofiling, let me know :-)04/06 00:12
edwinbit's more what it's not doing that I'd like to know, than what it is doing...04/06 00:14
pedagandyou could pinpoint the source of the performance loss I think04/06 00:14
pedagandare you doing lot of function calls? or indirect function calls?04/06 00:15
edwinbit's spending 30% of its time in GC related functions04/06 00:15
pedagandin my old days, 30% of GC was good04/06 00:16
edwinbyeah, but ghc does better and we can't have that ;)04/06 00:17
pedagandwell, GHC has an upper-class GC, at the same time :-)04/06 00:17
edwinbbetter GC would help, but I suspect knowing when not to allocate at all would be good04/06 00:18
edwinbi.e. when it's okay to use the stack rather than heap, or when it's okay to reuse something04/06 00:18
edwinbI've tried a really simple allocator which just moves a pointer along and never frees04/06 00:18
-!- mode/#epigram [+v dolio] by ChanServ04/06 00:18
edwinbwhich of course makes things much faster, at least for a short time...04/06 00:18
pedagandI see04/06 00:19
pedagandcan't you benchmark your stuff without GC and GHC without GC?04/06 00:21
edwinbI think I'd need to poke about GHC internals a bit more to do that04/06 00:22
pedagandbecause, it'll always be unfair to compare your boehm-ian GC with any other clever stuff04/06 00:22
edwinbbut I may have to do that anyway if I want to know what's going on04/06 00:22
edwinbif there's clever stuff that lives happily alongside boehm then I want it!04/06 00:22
edwinbmind, this isn't actually that important. I think epic is fast enough for most purposes at the moment.04/06 00:22
edwinbIt just annoys me ;)04/06 00:23
Saizanor you could steal GHC's RTS? assuming the evaluation models are compatible enough..04/06 00:26
pedagandSaizan, you mean, spitting some Core code and sending that to GHC?04/06 00:28
+dolioThat might be tough, since I think GHC core is still typed.04/06 00:29
edwinbthat's the biggest problem with it, yes04/06 00:30
Saizanpedagand: it was more like stealing the RTS (which i think is in C) and link it with code generated separately by epic04/06 00:30
edwinbI tried it a while back, and it sort of worked, but the optimiser broke things04/06 00:30
edwinbI'd prefer to know why it works so well though, rather than just stealing it04/06 00:31
edwinbalthough I'm not averse to stealing it ;)04/06 00:31
+dolioWhat kind of code are you comparing?04/06 00:31
Saizansome mercury guy is already doing that, iiuc04/06 00:31
edwinbthis is a contrived program which tree sorts some integers 04/06 00:32
edwinbso lots of cosntructing things which don't live very long04/06 00:33
+dolioI see.04/06 00:33
Saizanah, the case a generational gc is designed for04/06 00:34
+dolioNot just that, a copying collector. How does Boehm work?04/06 00:34
edwinbBoehn is mark/sweep04/06 00:34
edwinbIt is possible that it is simply because GHC's GC is better suited to it04/06 00:35
edwinband I'm just getting horribly fragmented memory04/06 00:35
edwinbmaybe this is where I need pedagand's profiling skills...04/06 00:35
pedagandha, see, I've skillz! I call my mother right away, thanks Edwin! :-)04/06 00:36
edwinbhehe04/06 00:37
-!- mode/#epigram [+v dolio] by ChanServ04/06 02:18
-!- koninkje_away is now known as koninkje04/06 03:21
-!- koninkje is now known as koninkje_away04/06 06:45
-!- koninkje_away is now known as koninkje04/06 06:58
-!- koninkje is now known as koninkje_away04/06 07:10
-!- mode/#epigram [+v dolio] by ChanServ04/06 08:22
-!- koninkje_away is now known as koninkje04/06 08:58
-!- mode/#epigram [+v pigworker] by ChanServ04/06 09:20
-!- mode/#epigram [+v dolio] by ChanServ04/06 09:21
molerispigworker: This wasn't in an operator, but I'm keen to understand that stuff anyway. I might change the PAIR pattern synonym to a smart constructor, put a stop to these bugs once and for all :)04/06 10:20
+pigworkergood plan: it's a bum steer04/06 10:20
+pigworkerthat patsy04/06 10:20
+pigworkermy wicked plot is to rework the VV vs TT distinction so VV means "you can match here if you're of positive type"04/06 10:21
+pigworkerarguably, that's a job for newtype, though04/06 10:23
+pigworkerprevent matching by hiding the constructor...04/06 10:23
molerisThe lazy vs Strict distinction does seem like it would be useful04/06 10:24
molerisin other news I've almost written the rec gadget in epigram04/06 10:26
+pigworkerbonzer04/06 10:54
+pigworkeranyhow, time to occupy a different spot in the Glasgow skyline...04/06 10:55
-!- koninkje is now known as koninkje_away04/06 11:26
-!- mode/#epigram [+v dolio] by ChanServ04/06 14:18
-!- mode/#epigram [+v pigworker] by ChanServ04/06 14:49
-!- mode/#epigram [+v pigworker] by ChanServ04/06 14:51
-!- mode/#epigram [+v dolio] by ChanServ04/06 15:21
-!- mode/#epigram [+v Saizan] by ChanServ04/06 16:50
-!- mode/#epigram [+v dolio] by ChanServ04/06 18:22
* soupdragon feels like I missed out on something04/06 18:24
soupdragonsomeone do /topic http://www.e-pig.org/ | Epigram - Programming Language with Dependent Types  | logs: http://epigram.orangesquash.org.uk/04/06 18:25
soupdragondon't seem to have privs.04/06 18:25
* soupdragon tries to hit the chandeliers and fails04/06 18:27
+pigworkerI gave it a whirl, but I don't see any effect.04/06 18:28
soupdragonguess one has to be +o to set topic04/06 18:28
soupdragondidn't used to be like that04/06 18:28
+pigworkerI'm clueless about these IRC mechanisms.04/06 18:29
soupdragonshapr?04/06 18:29
soupdragonhttp://www.spacex.com/webcast.php 10 seconds till liftoff04/06 18:30
soupdragonengine shutdown just after ignition nvm -_-04/06 18:30
+pigworkerI'm having too much fun watching my computer grind to a standstill trying to check a proof...04/06 18:32
soupdragongrinding to a standstill sounds about right04/06 18:32
+pigworkerghc about 30% CPU, emacs totally locked up, the sun blazing down04/06 18:33
soupdragonthat's the life!04/06 18:34
soupdragonis this the proof for the linear containers stuff?04/06 18:34
+pigworkerif only... I'm not convinced I've got the definitions right for that yet04/06 18:34
+pigworkercrikey, something happened!04/06 18:35
+pigworkerI'm trying to prove that the recursively defined equality on Nat is transitive...04/06 18:35
soupdragonin epigram ?04/06 18:36
shaprYow!04/06 18:36
soupdragonhey shapr :)04/06 18:36
shaprhiya!04/06 18:36
soupdragonI want to set the topic04/06 18:36
soupdragonsince it's polite (policy) to put the place for the logs in there04/06 18:36
+pigworkersoupdragon: no, in a type theory I implemented in Agda04/06 18:36
shaprawright04/06 18:36
soupdragonI wonder when should I get the courage to try coding basic category theory into the pig?04/06 18:36
soupdragonthere is a feeling my whole approach of doing it with quotients inside records might be wrong (that's what I'd do in coq if it has quotients.. which might happen not sure)04/06 18:37
+pigworkerthe epigram engines cannae take it, but it's always interesting to see where the failure kicks in04/06 18:38
soupdragonhehe04/06 18:39
shaprwill you guys be doing the ICFPc in Epigram?04/06 18:40
+pigworkerIt's really amazing watching Agda behave like an interactive assistant for an encoded theory04/06 18:40
soupdragonIt's a lot of fun to see the type inference/term inference thing switching over04/06 18:40
+pigworkershapr: not unless the competition is to implement Epigram04/06 18:40
shaprhah04/06 18:40
soupdragonI've never done ICFP.. I just cheer on roconnor04/06 18:41
soupdragonwell I wrote some lisp macros for a team once04/06 18:42
+pigworkerI'll probably spend most of that time over the Atlantic, anyhow04/06 18:43
shaprComing to the USA?04/06 18:53
+pigworkeryeah, teaching at the school in Eugene, OR04/06 19:02
shaprnifty04/06 19:06
+pigworkertrouble is, these days, "dependently typed programming" could really touch on a lot of material; editorial choice is required04/06 19:09
+pigworkerI wonder if Agda would speed up if it did edwinb optimization on open terms.04/06 19:15
+pigworkerEpigram gets to really not store index info in data if it comes from the type.04/06 19:16
-!- mode/#epigram [+v dolio] by ChanServ04/06 19:21
soupdragonhttp://www.spacex.com/webcast.php04/06 19:45
soupdragonthis time it's going04/06 19:45
+pigworkerghc has stopped and emacs is going (either my term has checked or agda has dies)04/06 19:52
soupdragonnot a good sign04/06 19:53
+pigworkerit normally works a bit when it's colouring in04/06 19:54
+pigworkerbut that was death04/06 19:55
+pigworkerok, it's time I went home04/06 19:57
-!- ChanServ changed the topic of #epigram to: http://www.e-pig.org/ | Epigram - Programming Language with Dependent Types | logs: http://epigram.orangesquash.org.uk/04/06 19:58
soupdragonty shapr04/06 20:00
edwinbI suspect the answer to pigworker's question is "Yes, but not as much as it should."04/06 21:31
edwinbas I understand it a lot of Agda's slowness is caused by loss of sharing04/06 21:32
edwinbalthough I may be out of date04/06 21:32
+Saizanit'd be nice if there was some intro for wannabe agda hackers, the 200 modules are a bit intimidating04/06 21:35
soupdragonidk04/06 21:38
soupdragonnewbies can learn Coq04/06 21:38
soupdragonI think Agda (at this point) is for reseachy people04/06 21:38
soupdragonstill ironing out the details and exploring and such04/06 21:39
soupdragononce they fix the theory that would be the time to start writing manuals and so on04/06 21:39
+Saizanby "agda hackers" i meant people that might like to work on the implementation04/06 21:39
soupdragonoh sorry04/06 21:39
soupdragonyeah I totally couldn't get into the agda source code at all04/06 21:39
soupdragona lot of weird stuff going on in there04/06 21:39
-!- mode/#epigram [+v Saizan] by ChanServ04/06 22:13
-!- mode/#epigram [+v Saizan] by ChanServ04/06 22:23
-!- mode/#epigram [+v pigworker] by ChanServ04/06 23:42
--- Day changed Sat Jun 05 2010
soupdragonFetching a hashed repository would be faster.  Perhaps you could persuade05/06 00:30
soupdragonthe maintainer to run darcs optimize --upgrade with darcs 2.4.0 or higher?05/06 00:30
soupdragon<darcs get http://www.e-pig.org/darcs/Pig09>05/06 00:30
pedagandsoupdragon, please do harass pigworker when he is back :-)05/06 00:35
soupdragonokay ill try :)05/06 00:35
pedagandhe and his mac G4 are our only to keep that obsolete stuff05/06 00:35
soupdragoneverything 'looks alright' except [DISABLED] Fin.pig is disabled and some vec thing05/06 00:35
soupdragonthings*05/06 00:35
pedagandindeed, these are disabled, no worry05/06 00:36
soupdragonit's so cool how there's all this agda stuff along with epigram :)05/06 00:37
pedagandand on Monday, there will be some Coq stuff as well probably :)05/06 00:38
soupdragonooh what's happening?05/06 00:39
soupdragonI saw that old OTT.v thing05/06 00:39
soupdragonbut that was a while back05/06 00:39
pedagandreviewers are not convinced by "with have implemented that stuff in our wacky Epigram language", so we use Agda (and it's useful for us to, truth to be said)05/06 00:39
pedagandI've made yet another model of Desc in Coq, nothing really exciting05/06 00:40
+dolioThe (I)Desc stuff in Agda is certainly more convincing than "it doesn't seem to loop anymore". :)05/06 00:41
+dolioAlthough I suppose the looping stuff might not quite be modeled in Agda.05/06 00:41
pedagandapparently, not everybody trusts the "set polymorphism" option of Agda :-)05/06 00:42
+dolioYou mean, the stuff with Level and Set i?05/06 00:43
pedagandyes05/06 00:43
+dolioWell, it's hard to blame them for that.05/06 00:44
pedagandindeed05/06 00:45
+dolioI've tried a couple times making something inductive-recursive work, but haven't gotten anywhere yet.05/06 00:51
pedagandto "work" toward which end? Set polymorphism?05/06 00:53
+dolioMaking a universe (or hierarchy) with something desc-like in it.05/06 00:53
pedagandif you give yourself a Mu at each level and a code+interpreter at "some" level, then you walk down the stairs, building a Desc at each level05/06 00:54
pedagandthat's probably unhealthy but I thought we could put the code at some level Omega (transfinite) and do the descent from there05/06 00:55
pedagandbut that's rather contrived...05/06 00:56
+dolioWell, I even ran into negative types trying to have a Desc type mutually defined with U, and where Mu d lives in U.05/06 00:58
+dolioWhich is disappointing.05/06 00:58
nappingHave you read "The Gentle Art of Levitation"?05/06 01:00
pedagandthe codes for Desc should live one level higher than the corresponding Mu05/06 01:00
pedagandI guess you did that right, but just checking05/06 01:00
nappingIt seems to be Conor's shot at a self-describing universe05/06 01:00
pedagandI've an Agda model in which I hard-coded Desc_42, then go down, go down, go down, ... My EPSRC funding is well used, I tell you :-D05/06 01:01
+dolio:)05/06 01:01
pedagandnapping, worse than that... I was part of the gang who wrote it :-)05/06 01:01
soupdragonand I first heard about this stuff from Peter Morris' thesis05/06 01:02
pedagandindeed, that's his baby05/06 01:03
+dolioAnyhow, yes, the levitation paper had some of the stuff that didn't seem modeled by the Agda to me, and which struck me as not obviously correct.05/06 01:06
+dolioLike "we can replace Desc by a Desc description of Desc in a certain way".05/06 01:06
+dolioThe Agda is bootstrapped by an Agda type Desc.05/06 01:07
+Saizanit seems in the end you've to assume something named Desc exists to be able to typecheck the definition of Desc05/06 01:08
pedagandthat's entirely true05/06 01:09
pedagandthe whole collapsing of Desc onto itself is due to switchD05/06 01:10
pedagandwithout resorting to an embedded model of a type-theory with Desc inside Agda, it wasn't possible to model switchD05/06 01:11
pedagandI reckon that it's what you've been trying to get to, right?05/06 01:12
+dolioNo, so far I'd just been trying to make an inductive-recursive universe closed under Mu for a mutually defined Desc type.05/06 01:13
+dolioWhich would be analogous to the Desc type in Agda, I think. Or the tower of descs using universe polymorphism.05/06 01:14
pedagandha, ok05/06 01:16
-!- mode/#epigram [+v dolio] by ChanServ05/06 01:21
-!- mode/#epigram [+v dolio] by ChanServ05/06 04:21
-!- mode/#epigram [+v dolio] by ChanServ05/06 06:18
-!- mode/#epigram [+v dolio] by ChanServ05/06 07:21
-!- mode/#epigram [+v dolio] by ChanServ05/06 08:21
-!- mode/#epigram [+v dolio] by ChanServ05/06 09:21
-!- mode/#epigram [+v pigworker] by ChanServ05/06 09:51
-!- mode/#epigram [+v dolio] by ChanServ05/06 11:18
-!- mode/#epigram [+v pigworker_] by ChanServ05/06 11:30
-!- pigworker_ is now known as pigworker05/06 11:31
tsapihello05/06 11:52
pedagandhi, james? what are you doing on 9grid.fr?? You're a plan9 user???05/06 11:55
tsapia closet one :)05/06 11:57
pedagandhaha05/06 11:58
tsapiis this channel logged by the way?05/06 11:58
pedagandyep, as written in the status bar up there ^05/06 11:58
tsapiI know Laney keeps logs for #agda05/06 11:59
pedagandhttp://epigram.orangesquash.org.uk/05/06 11:59
tsapihttp://epigram.orangesquash.org.uk/05/06 11:59
tsapii see05/06 11:59
-!- mode/#epigram [+v dolio] by ChanServ05/06 15:21
-!- mode/#epigram [+v Saizan] by ChanServ05/06 16:04
-!- mode/#epigram [+v dolio] by ChanServ05/06 16:21
-!- mode/#epigram [+v codolio] by ChanServ05/06 18:21
-!- mode/#epigram [+v dolio] by ChanServ05/06 19:21
pedagand(./test/Syntax.pig has landed in the repos. That's a short tour of Epigram's syntax. Feel free to add your cheatcodes.)05/06 21:56
tsapicool!05/06 22:08
tsapiI guess the green equality shouldn't really be used, it's an implementation detail05/06 22:08
tsapiand refl1 and refl2 are identical right?05/06 22:10
pedagandI had the impression that we could use greenEq to compute stuffs for us, while the blue would just get stuck with the thing we give. I don't know.05/06 22:19
pedagandha yes, refl1 and refl2 are the same : I've removed something I tried05/06 22:20
pedagand(I've removed refl2)05/06 22:21
pedagandactually, you're right: to get the green, you'd write a blue and Out it (with %)05/06 22:29
molerispedagand: Good stuff05/06 22:49
pedagandthanks :-)05/06 22:50
molerisWhile you might not write greenEq, you're certainly going to get it appearing as a goal (after an %), so I think we should probably give it a better syntax05/06 22:50
molerisI think (<->) was suggested at some point -- not that I'm particularly attached to it05/06 22:51
molerisAlso, using con to split sigmas is getting very old (does it also eliminate still Mu as well?)05/06 22:52
pedagandwhat would you use to split a sigma?05/06 22:53
molerismatching pairs on the left of lambdas would be really nice :)05/06 22:54
molerisi.e. having |\ [ x , y ] -> t| instead of |con \ x y -> t|05/06 22:55
molerisnot sure how difficult that would be in the current setup though05/06 22:55
pedagandha, yes, so: con for splitting sigma is old *but* implemented :-)05/06 22:58
molerisOK, but con is still misleading05/06 22:58
molerisI realise that keywords are at a premium, but con already does a number of things, and spliting sigmas isn't really in the same class of jobs05/06 22:59
molerisI vote for adding a keyword `split'05/06 23:00
pedagandI entirely agree with you...05/06 23:01
pedagandyep, we can do that05/06 23:02
pedagandbut, assuming we can implement "\ [x , y] -> ...", would we need "split" as well?05/06 23:05
pedagandhum, yes, split ? might still be useful I guess05/06 23:05
molerisit would still be useful, afterall anonymous functions aren't the end of the story05/06 23:07
+pigworkerwhy not go for the fancy lambda? you only need it in the display syntax, which is now something else05/06 23:10
-!- mode/#epigram [+v dolio] by ChanServ05/06 23:21
pedagandyou mean: we should just do fancy lambda, or both split and fancy lambda? I think both are just display artifacts 05/06 23:25
+pigworkersplit's a no brainer, so warm up with that; then try fancy lambda?05/06 23:33
+pigworkeron the earlier topic, I'm beginning to think green equality isn't worth it05/06 23:35
pedagandok05/06 23:37
+pigworkerwe could just make the con constructor for blue equality do one step of expansion, with blue equality for the bits05/06 23:37
+pigworkerwe don't really make use of the way green equality computes lots of steps at once05/06 23:38
pedagandI turn these into feature requests, sir05/06 23:41
+doliopedagand: This is what I was talking about yesterday: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25931#a2593105/06 23:43
pedagandas for me, I've a much more basic request: propsimp should stop to unpack my carefully crafted sigma types! Damn it!05/06 23:43
pedagand:-)05/06 23:43
+dolioAgda doesn't like it because Fix D ~ Fix D' -> ....05/06 23:44
pedaganddolio, ha, yes, thanks for that discussion btw05/06 23:44
+dolioEven though it's probably okay.05/06 23:44
+dolioDue to structural decrease of the descriptions (not that I've proved that or anything).05/06 23:45
pedagandhave you tried to manually unfold Fix?05/06 23:45
+dolioI'm not sure what you mean by that.05/06 23:46
+dolioI thought about not making Fix a datatype, but then I realized I didn't really know of any other possibilities.05/06 23:47
+dolioI did find a way to sort of do it, by moving Desc and U into Set1, and having Desc quantify over Set instead of U. So it'd be totally separate from U.05/06 23:49
+dolioBut that isn't really correct, because then U contains datatypes over Set, not just over other types in U.05/06 23:49
pedagand"Meta" is a module of yours, right? Or it's in the stdlib?05/06 23:54
+dolioOh. Yeah. I think the only thing I'm using it for in there is top and sigma.05/06 23:54
pedagandI hpaste what I meant by unfolding, but it's ugly, in Coq, and I'm not sure it's your problem here05/06 23:55
pedagandhere you go: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25932#a2593205/06 23:57
pedagandintuitively, you bring [| . |] into Fix05/06 23:58
+dolioOh, so you give Fix several constructors mirroring Desc.05/06 23:58
+dolioHmm...05/06 23:58
pedagandso, here it's particularly disgusting because we use the impredicativity of Prop to avoid size issues05/06 23:58
+dolioHeh.05/06 23:59
pedagandthat's a Matthes-style encoding05/06 23:59
--- Day changed Sun Jun 06 2010
+pigworkerare you sure? it's late; I don't see where impredicativity kicks in (but maybe I'm blind)06/06 00:02
pedagandhem.06/06 00:02
+pigworkerIt's possible Venanzio Capretta has already invented this trick; we are always inventing each other's tricks.06/06 00:03
pedagandthe fact is MuU is in Set right, not Set106/06 00:04
pedagands/Set1/Type/06/06 00:05
pedagandwe abuse Prop with the Is_true, getting the proof to run e.g. SigmaHd and SigmaTl06/06 00:05
pedagandwell, I should try writing it directly and see if the size change06/06 00:06
+pigworkerbut Is_true takes a tiny wee Bool to a tiny wee Prop; do we ever make bloody big Props?06/06 00:08
pedagandwhat is a big Prop? There is no hierarchy of Props, isn't it?06/06 00:10
pedagandI mean, there is no hierarchy of Prop, period. :-)06/06 00:10
pedagandyes, so writing it "directly" (I hpaste in a sec) gives you: "Error: Large non-propositional inductive types must be in Type."06/06 00:15
pedagandhere you go: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25932#a2593306/06 00:17
+pigworkerI mean a Prop which is made by equating things in big sets06/06 00:18
pedaganddolio, so the definition above is what you could write as a one step unfolding, however Mu is "too big" now, you cannot build your hierarchy downward06/06 00:18
pedagandpigworker, mmh ok. So, you don't call that trick "abusing impredicativity of Prop"?06/06 00:21
+pigworkernot if it's just reflecting Bool06/06 00:21
+doliopedagand: Is it just me, or does pi look exactl like sigma?06/06 00:22
+dolioAlso, I assume instead of Fix D you use MuU D D?06/06 00:23
+dolioThis appears to actually work in Agda.06/06 00:23
pedaganddolio, hehe, no it's not just you, I'm seeing this too :-)06/06 00:24
pedagandpigworker, ok. I'm mystified by the fact that we can save a size by going to and fro Prop without magic...06/06 00:25
pedaganddolio, yes, MuU is Fix in your case06/06 00:26
+dolioOh, I spoke too soon. I still had --no-positivity-check on.06/06 00:26
+dolioThis also fails.06/06 00:26
+dolioWhich is the less surprising result.06/06 00:27
pedagandoh well...06/06 00:27
-!- mode/#epigram [+v pigworker] by ChanServ06/06 00:27
+dolioIt would have been somewhat odd if that had solved the positivity problems.06/06 00:28
+dolioIf U = f U is negative, I'd expect expanding f U to have the same problem.06/06 00:29
pedagandI'll look into that, that's definitely something to clarify.06/06 00:31
pedagandI'm afraid that my induction-recursion-fu is very low, so don't expect immediate returns on investment...06/06 00:33
-!- mode/#epigram [+v pigworker] by ChanServ06/06 00:35
+dolioI'm no expert, either.06/06 00:35
+dolioI really have no reason to expect that you could actually have an inductive-recursive universe closed under descriptions, either. I just thought it'd be cool if you could.06/06 00:36
+dolioW-types are easy, of course, but I think observational equality is also hard.06/06 00:36
+dolioFor different reasons than Desc, though.06/06 00:37
-!- mode/#epigram [+v pigworker] by ChanServ06/06 01:08
+Saizandolio: what about a two-step encoding like this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25931#a2593406/06 02:02
+dolioThat might work.06/06 02:05
+dolioYeah, that seems kosher.06/06 02:06
pedagandthat's intriguing06/06 02:08
+Saizanfound it almost by accident :) 06/06 02:12
pedagandwhat is your intuition of this external notion Desc' and its link with the encoded one?06/06 02:13
+Saizanwell, Desc' is larger in principle, but it's also what Fix easily digests, while Desc is what we really want to describe06/06 02:23
+Saizanso \[[_\]] is sort of like translating to a lower level unsafer language06/06 02:24
+Saizanbut the Desc' values that are in its image are ok06/06 02:25
pedagandok, I see06/06 02:26
+dolioDesc' is descriptions over Set, Desc is descriptions over U, and you interpret the latter into the former.06/06 02:27
+dolioSince U is being interpeted into Set.06/06 02:27
+Saizani've proved [[ `Prf` ! `INu` I F i > inn (out x) == `INu` I F i > x ! ]], postulating coe, where == is bisimulation, but if i fill in the definition of !_>_==_>_! for `IMu' types it turns yellow :\06/06 02:31
+doliopedagand: http://code.haskell.org/~dolio/agda-share/universes/html/DataHierarchy.html06/06 02:48
pedagandthanks for the pointer06/06 02:49
pedagandI keep it carefully, but for now... must... sleep... :-)06/06 02:50
+dolio:)06/06 02:50
pedagandg'd night06/06 02:51
-!- mode/#epigram [+v pigworker] by ChanServ06/06 10:58
tsapipedagand: I linked your Syntax.pig file from our embrionic website06/06 12:08
pedagandgoodo :-)06/06 12:36
tsapi 06/06 12:56
pedagandhaha, Pig just ate all my ram. I've 4gigs...06/06 16:02
pedagandI restarted it with top nearby. 1.1G resident, and counting...06/06 16:04
pedagandoh well... 2.2G06/06 16:05
pedagandI'll sneakily put that in the test repos, hehe :-)06/06 16:06
tsapinice :) we're catching up with agda 06/06 16:11
pedagandhehe, I've some huge proof term left open, this might be the cause of the problem06/06 16:16
pedagandis it me or http://www.e-pig.org/epilogue/ is "blank"?06/06 16:35
molerispedagand: Not just you06/06 16:41
pedagandok, I hope it's nothing bad. I don't "need" it, ignore my message and don't ruin your week-end :-)06/06 16:43
molerisI think it's probably my fault. In fact, since I switched the main website to the new one earier06/06 16:46
molerisNo idea what bad I made. But, the data is safe, so no need to panic :-/06/06 16:50
pedagandtsapi, btw, do you use Plan9 or Inferno?06/06 16:52
tsapipedagand plan906/06 16:52
tsapipedagand, it's one of my many bad habits :)06/06 16:53
pedagandwell, using an ageing Unix system such as Linux, *that's* a bad habit (shame on me). Plan9, on the other hand, makes you a Good Kid :-)06/06 16:58
pedagandand you have all the software to "work" (read, emacs) there? or you've to use Acme, for instance?06/06 16:59
tsapiI don't have emacs, just acme and sam which are nice in different ways. But, work is not really possible for that I'd at least need latex (which I tried and failed to install this afternoon)06/06 17:08
tsapiIt's fun to play with and has some interesting ideas, particulary about the filesystem/namespaces etc.06/06 17:09
pedagandyes, I read a few papers about it, it looks really cool06/06 17:14
molerispedagand: Epilogue is back06/06 17:25
pedagandoooooh :-) And I see tsapi's web page at e-pig.org. Great06/06 17:27
pedagandis anyone planning to give it a CSS brush? If no, I could do that tonight if you want06/06 17:28
pedagandI mean: "I could do that, if you want" (and that would probably be tonight)06/06 17:31
molerisI'd be very happy for you to do it is you want :)06/06 17:32
pedagandok ;-)06/06 17:33
molerisis tomorrow the moment of truth for Levitation?06/06 17:35
pedagandhehe06/06 17:41
pedagandyep, tomorrow ;-)06/06 17:43
pedagandwhy do we want pairs to be lazy in Epigram?06/06 17:56
pedagandto retain sharing?06/06 17:56
-!- mode/#epigram [+v dolio] by ChanServ06/06 18:20
tsapiepilogue has lost its darcs feed06/06 19:38
pedagand(I've pushed web/index.alt.html, feel free to move it to index.html when it's satisfying)06/06 19:40
pedagandI think there is no more darcsweb behind, anyway, isn't it?06/06 19:40
tsapipedagand, very nice :)06/06 19:45
pedagandthat's very easy when you've the right CSS, the most difficult is to get the content: and you did that :-)06/06 19:45
tsapiI kind of liked having different pages for the different sections but perhaps there isn't so much point if they aren't very big06/06 19:52
pedagandyeah, I hesitated before merging all in one page. Right now it's as little as one page, with some very small sections so I gave it a try.06/06 19:56
pedagandI think that putting the Download section at the bottom would give a better balance06/06 19:57
tsapiyeah, and we should have quick link to the epilogue06/06 19:59
pedagandha, indeed!06/06 20:00
moleristsapi: rss feed fixed, cheers for the heads up06/06 20:01
tsapimoleris, cool06/06 20:01
molerispedagand: Have you got a copy of the images in your quotation post handy? They seem to have gone walkabout06/06 20:02
pedagandyep, I've them on my hd, I'll fix that06/06 20:03
molerista06/06 20:03
moleriswebpage looks good06/06 20:04
tsapii moved the downloads and added an epilogue link06/06 20:18
pedagandok, I did it here but go ahead, feel free to push06/06 20:23
tsapipedagand, sorry, i already did06/06 20:25
pedagandsure, no problem06/06 20:25
tsapiI think we should absorb the contents of INSTALL into the web docs and remove it. Better not to maintain two sets of instructions06/06 20:29
pedagandI quite like to "more INSTALL" when I'm walking through a new source code but I admit being old fashioned06/06 20:37
pedagandI've change the style of <ul> so that they are slightly padded on the right06/06 20:47
pedagandmaybe we could "mv index.alt.html to index.html" now?06/06 20:48
pedagandI do it, we can still bikeshed it later on06/06 21:11
pedagandhop, e-pig.org updated :-)06/06 21:18
tsapipedagand good work :)06/06 21:19
tsapipedagand, fair point about INSTALL, but we should synchronise it somehow.06/06 21:20
tsapimaybe just be a direct copy of what is in downloads section with the html formatting removed06/06 21:21
pedagandwell, you're convincing me of the advantage of the html: there is no extra-work to be done :-)06/06 21:25
tsapiin that case we could just put a note in the INSTALL saying to point your web browser at the local copy of the html instructions06/06 21:27
pedagandexactly06/06 21:28
tsapiI'll do it then06/06 21:29
pedagandperfect, thanks06/06 21:30
tsapipedagand, done.06/06 21:49
pedagandthat looks good06/06 21:52
-!- mode/#epigram [+v soupdragon] by ChanServ06/06 22:02
Laneyit's common to link right into a $vcs-web interface for such things06/06 22:07
tsapiLaney: what things?06/06 22:16
Laneyre: INSTALL06/06 22:17
tsapiok, good06/06 22:18
-!- mode/#epigram [+v dolio] by ChanServ06/06 23:20
--- Day changed Mon Jun 07 2010
-!- mode/#epigram [+v dolio] by ChanServ07/06 00:17
+soupdragonany webologists around? this is 404ing http://www.e-pig.org/test/Syntax.pig07/06 00:31
+pigworkerno clue about the 40407/06 01:29
+pigworkerhave been working on this steaming pile of ex....ment http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf07/06 01:30
+soupdragonpigworker on page 2 is * meant to be Ty?07/06 01:43
+soupdragoninside that mutual definition07/06 01:43
+pigworkeryeah. botched alpha conversion. not real agda...07/06 01:44
+pigworkerthanks for the catch07/06 01:45
+pigworkerI just can't get this stuff right unless I'm typechecking the source for the paper.07/06 01:47
+soupdragongosh!! that was a fun read07/06 02:04
+soupdragonISTR you mentioning something like this idea on agda mailing list but without s & k?07/06 02:05
+soupdragonI wonder if you could implement a linear dependent type calculus in this same way07/06 02:10
-!- mode/#epigram [+v dolio] by ChanServ07/06 02:17
+pigworkerThe s and k thing just had to happen: it's the ancient way of good plumbing.07/06 02:51
+pigworkerLinearity might work out, in the style of the DSL for rearrangements. But it's important to distinguish type-level usage (cost free) from run-time usage (resource bound).07/06 02:53
-!- mode/#epigram [+v codolio] by ChanServ07/06 08:20
-!- mode/#epigram [+v Saizan] by ChanServ07/06 08:54
-!- mode/#epigram [+v pigworker] by ChanServ07/06 08:55
molerispedagand: It's official then :) Congratulations!07/06 09:58
edwinbOur ICFP was accepted!!!!!07/06 09:58
* edwinb dances a happy, if astonished, dance07/06 09:58
molerisedwinb: Congrats, you and us both!07/06 09:59
edwinbCongratulations to you chaps too :)07/06 10:00
edwinbI get the impression, from the modified reviews, we just sneaked in07/06 10:03
edwinbpigworker: any update on the SPLS title, or should I go with the proposed?07/06 10:05
+pigworkeredwinb: fantastic!07/06 10:06
+pigworkerpedagand, moleris, tsapi: quality!07/06 10:07
pedagandoh, I got an "accepter paper #23". Lovely07/06 10:07
+pigworkeredwinb: I think a little jocularity isn't a big problem07/06 10:08
pedagandpigworker, you seem delighted this morning: I just arrived, what happened? :-)07/06 10:08
+pigworkerdelight!07/06 10:08
pedagand:-)07/06 10:09
edwinbpigworker: splendid07/06 10:10
edwinbpedagand: congratulations on the paper.07/06 10:11
edwinbLots of dependent types at ICFP this year then...07/06 10:12
-!- mode/#epigram [+v dolio] by ChanServ07/06 10:20
pedagandedwinb, ha, reading the logs, I understand the reason of the euphoria: congrat's too!07/06 10:22
molerisI noticed some bugs in the Gentle Arts code while I was in Glasgow last. I guess I should fix those now :)07/06 10:29
+pigworkeradam__: well done! good mood around here today...07/06 10:30
agundryso I see, congratulations on getting in to ICFP07/06 10:30
agundrysorry for the join/part nonsense07/06 10:30
+pigworkernow I just have to get myself a gig07/06 10:31
+doliopigworker: So, for some reason, I was under the impression that Peter Dybjer's work on inductive types/families allowed for types defined by mutual induction. Is that not correct?07/06 10:32
+pigworkerI can't remember if mutual induction is explicitly present, but it's always codable by indexing with a flag07/06 10:33
+dolioIs that different somehow from the induction-induction in your paper?07/06 10:34
+pigworkerinduction-induction involves fixpoints in Sigma Set \ X -> Set, not just 2 -> Set07/06 10:35
pedagandagundry, and I saw a tweet on getting to MSFP: congrats! :-)07/06 10:35
+pigworkerindexing one branch over another is new/strange/weird/harder to encode07/06 10:35
agundrypedagand: thanks!07/06 10:36
+pigworkerToni Setzer has a new story about induction-induction. I think the LICS submission...ended up at CSL.07/06 10:36
+pigworkerLong ago, he and I tried to code induction-induction by giving first flat mutually defined preterms, then flat mutually defined goodness-predicates. The induction principles failed to hold, but only for want of proof irrelevance.07/06 10:38
tsapihello #epigram, today seems to be a good day :)07/06 10:47
edwinbpigworker: SPLS programme is up at http://www.cs.st-andrews.ac.uk/~eb/SPLS-June10/ but as you see I don't have abstracts from many people...07/06 10:56
edwinbcould you send me one please? Although I'm sure we can all roughly guess what's in it.07/06 10:56
+pigworkeredwinb: will do, when I get to school07/06 11:02
edwinbrighto. As you see, from the absence of others, there is no serious hurry.07/06 11:08
-!- mode/#epigram [+v Saizan] by ChanServ07/06 12:41
-!- mode/#epigram [+v Saizan] by ChanServ07/06 13:08
-!- mode/#epigram [+v soupdragon] by ChanServ07/06 17:43
-!- mode/#epigram [+v Saizan] by ChanServ07/06 19:23
-!- mode/#epigram [+v dolio] by ChanServ07/06 20:20
pedagandtsapi, out of curiosity, in your formalization of category theory, what representation did you use for objects and for morphisms?07/06 21:24
-!- mode/#epigram [+v pigworker] by ChanServ07/06 21:25
tsapipedagand: I'm just using sets for both and propositional equality for the laws07/06 21:27
pedagandha, ok. In test/Cat, I used Objects in Set, Arrows in Objs -> Objs -> Set. How wicked is that in your opinion?07/06 21:28
pedagandthis is nothing but curiosity, I'm definitely not the right person to play these games. So, don't be afraid to be brutal in your judgement :-)07/06 21:29
tsapijust the same as me, I'm also using type in type07/06 21:29
pedagandok, good07/06 21:29
pedagandI started with a "dom : Arrows -> Objects, cod : Arrows -> Object, compos : Arrows -> Arrows -> (pf that cod = dom) -> Arrows"07/06 21:30
pedagandso, that's probably what was crazy, I became reasonable after :-)07/06 21:30
tsapirecord Cat : Set where07/06 21:32
tsapithat didn't work...07/06 21:32
pedagandok, thanks07/06 21:33
tsapihttp://www.cs.ioc.ee/~james/Categories.agda07/06 21:34
tsapimore sensible people than myself use setoids for the homset and hence the equations07/06 21:35
+soupdragonI got mired when I tried to use setoids07/06 21:36
tsapiI thin having dom and cod introduces more equalities than necessary but I haven't really tried it that way07/06 21:36
+soupdragonso quotients look like a magic wand to me 07/06 21:36
pedagandyeah, ok, I did the same thing than you, that's reassuring07/06 21:36
tsapiit's really a different definition of a category I think, not just a different formalisation with dom and cod07/06 21:36
pedagandas far as I understood, there is a problem with quotient. pigworker will correct me, that was a story about representing real numbres07/06 21:37
pedagandtsapi, on ncatlab (link written in the Cat file), someone was arguing that the Hom(x,y) representation was the right one07/06 21:38
pedagandI mean, the "right" one :-)07/06 21:38
pedagandanyway, I'm reassured, thanks07/06 21:39
tsapipedagand, sounds interesting, i'll take a look07/06 21:44
+soupdragonregarding real numbers in quotients - http://www.reddit.com/r/dependent_types/comments/azl8r/quotients_epigram2/07/06 21:45
+soupdragonI guess that's not the only problem though07/06 21:46
tsapisoupdragon, thanks for the link07/06 21:52
+pigworkerat meetings, you actually hear people say, in all seriousness, "but those are not the real real numbers"07/06 21:52
pedagandto be honest, I cannot tell whether the "problem" discussed there and the one that pigworker once told us are the same. I make a very bad Apostle, sorry :-)07/06 21:52
tsapiin the fragment of category theory I'm working in, I haven't come across such problems07/06 21:52
+pigworkerroconnor raised important questions about choice functions; if I have a function from (X/R) -> (Y/S), do I have a function f : X -> Y such that R a b -> S (f a) f b)?07/06 21:55
+soupdragonand what's the answer ?:)07/06 21:58
pedagandif you say "yes", you break 'quotientness' by a carefully engineered S?07/06 22:01
pedagandby "breaking quotientness" I mean: you can access the "physical" representation of your objects, while you wanted to abstract it away07/06 22:01
tsapipigworker, I'd have thought absolutely yes, it basically the definition of a function on setoids.07/06 22:02
+pigworkeryes it is the definition of a function on setoids, but setoids don't hide information, they just demand evidence that you don't abuse information07/06 22:04
+soupdragonoh so maybe we only get the respectfulness proof from a sort of parametricity?07/06 22:04
+pigworkeryep07/06 22:04
+pigworkerbut what sort of parametricity?07/06 22:05
+pigworkerat the moment, I don't know good conditions for the existence of choice functions, only good and bad examples07/06 22:05
+pigworkerconsider a universe operator which closes some (U, El) under Pi and quotients; calculate the free theorems07/06 22:12
-!- mode/#epigram [+v dolio] by ChanServ07/06 22:17
+soupdragoncan't see it.. (q,q') \in X/R <=> ???07/06 22:27
+soupdragonwe have things like  ((x,y),(x',y')) \in AxB <=> (x,x') \in A and (y,y') \in B.  (f,f') \in A->B <=> forall (x,x') \in A, (f x, f' x') \in B07/06 22:28
+soupdragonso it seems that the relation for quotients needs to use qelim07/06 22:28
+pigworkerperhaps, but is that a problem?07/06 23:45
+pigworkerif you unpack (X/R) to get elements of X which you then use by R'ing them, you do respect the quotient07/06 23:46
+soupdragonhi shapr!07/06 23:49
+soupdragonpigworker, not a problem just that I don't know what it shoudl be07/06 23:49
+doliopedagand: I've seen a genuine category theorist argue that Arrows : Obj -> Obj -> Set is the Right Way to do it. And that dom, cod : Arrow -> Obj, and f . g being a partial function defined when dom f = cod g is an artifact of encoding the conceptually dependent type in set theory.07/06 23:50
+pigworkerit's all terribly start-a-fight equality-sensitive07/06 23:51
+dolioOh, you mentioned that. I missed it in my skimming.07/06 23:51
pedagandyeah, this matches the commentary of the ncat-lab person. I suspect we're talking of the same discussion: "In praise of dep. types", in which you intervened :-)07/06 23:52
+dolioYes.07/06 23:52
pedagandand you're convinced by that too?07/06 23:52
pedagand(out of curiosity)07/06 23:52
+pigworkerhankovian mischief-merchants would consider Obj -> Sigma Set \ X -> Obj07/06 23:53
+dolioWell, I certainly tend to think about hom sets as being families ala type theory. But that may be due to my working mostly in type theory.07/06 23:54
+dolioBut, if a mathematician does as well, that's probably a good sign.07/06 23:54
pedagandok, thanks07/06 23:54
+soupdragonI'd like to have a category theory text which defines everything using category theory07/06 23:54
pedagandpigworker, the benefit of this encoding lies in the implementation? or it captures more definitions? or something else?07/06 23:55
+soupdragonI haven't yet found one, which is frustrating.. closest is probably Sets for Mathematics which axiomatizes SET using categories07/06 23:55
+dolioDoes that go into Lawvere's ETCS?07/06 23:56
+soupdragonthat's what it is, I think07/06 23:57
+pigworkerpedagand: it's almost certainly idiotic, but with a naive attitude to equality, isomorphic to the other two07/06 23:57
+dolioHe worked on another foundation, too, as I understand. I don't know if it's in any books, though.07/06 23:57
+dolioHis thesis goes into it a little, though.07/06 23:57
+dolioWhere you axiomatize the category of categories.07/06 23:58
+dolioHardcore categorists would probably tell you that's wrong, though, because the collection of all categories is naturally a 2-category.07/06 23:59
+soupdragonhuh07/06 23:59
pedagandpigworker, ok. I always feel better when I do it the Hank way, so I'll give it a go :-)07/06 23:59
+soupdragon2-category is different form Set-2 right?07/06 23:59
+soupdragonyou are saying something different than it's Big?07/06 23:59
pedagandsoupdragon, morphisms form a category in a 2-cat07/06 23:59
--- Day changed Tue Jun 08 2010
+pigworkerpedagand: I'm not saying it's the Hank way. Unless it's the Hank way of taking the piss.08/06 00:00
+dolioIn the case of Cat, 2-category means it talks about categories, functors and natural transformations in the definition.08/06 00:00
pedagandpigworker, hehe08/06 00:01
+dolioIn general you have 0-cells, 1-cells and 2-cells, with 0 and 1-cells being like objects and morphisms, and 2-cells going between 1-cells, and composable in ways similar to natural transformations.08/06 00:01
+pigworkerid X = (1 , \_ -> X)08/06 00:01
shaprhiya soupdragon 08/06 00:02
+pigworkerPow : Set a -> Set (suc a); Pow X = X -> Set a; Fam : Set -> Set (suc a); Fam X = Sg (Set a) \I -> I -> X; Hank's names for competing notions of power set; where you see one, you may expect to find the other; they are equivalent only if equality on X makes sense.08/06 00:16
+pigworkersorry, Fam : Set a -> Set (suc a)08/06 00:18
* dolio sighs a little every time he sees Sg X \\x -> ....08/06 00:22
+pigworkerI'd like to write (x : X) * but what gives?08/06 00:33
+pigworkerI note you've picked up nervous double backslash syndrome from spending too much time in Agda mode.08/06 00:36
+dolioI have?08/06 00:42
+dolioAnyhow, my point was that it'd be nice if Agda had some way to introduce new binding syntax. Not that that's easy.08/06 00:44
+dolioSomehow what I don't mind in "callCC (\k -> ...)" seems especially ugly when it's Sigma or Pi or W.08/06 00:45
edwinbHmm. That would be nice.08/06 00:46
edwinbBut possibly a nightmare to parse...08/06 00:46
+dolioOr "shift (\k -> ...)". I guess the very name of callCC suggests that you're passing a function.08/06 00:46
+pigworkerIt is simultaneously desirable that really only lambda binds and that on the surface, you can make anything vaguely functional bind.08/06 00:46
+dolioYeah, Coq seems to manage by allowing you to rewrite at an almost token stream level it seems.08/06 00:48
+dolioBut I don't really know how their parser works.08/06 00:48
+pigworkerI'm profoundly grateful that it's Sg S \ x -> T, not Sg S (\ x -> T).08/06 00:48
+pigworkerI wish Haskell did that.08/06 00:49
+dolioThat is handy. Although it looks wrong to me from years of Haskell training.08/06 00:50
+Saizanif all the binders were highlighted in a peculiar way it wouldn't be much of a problem to have custom ones08/06 00:51
+pigworkerLEGO did it, which is why I'm used to it.08/06 00:52
+pigworkerPeculiarly, I learned LEGO in 1995 and Haskell in 2000.08/06 00:54
+soupdragonyeah I always wondered why haskell had that restriction08/06 00:54
pedagandpigworker, I think I've fully automated stratisfaction here. So, now, I'm going to bed, have an happy night of sleep, and will find where the bug is tomorrow :-)08/06 01:02
pedagandit is not like "it is working, don't know why": I have some sort of story for it. It is in 3 colors, so it must be true.08/06 01:03
+pigworkerpedagand: I await with interest; but bughunting in the morning is definitely the best policy08/06 01:03
pedagandyeah, will see. Hopefully it's really working... 08/06 01:06
pedagandg'd night folks08/06 01:07
+pigworkerNight all!08/06 02:46
-!- mode/#epigram [+v Saizan] by ChanServ08/06 03:05
-!- mode/#epigram [+v dolio] by ChanServ08/06 06:27
-!- mode/#epigram [+v dolio] by ChanServ08/06 08:16
-!- mode/#epigram [+v edwinb] by ChanServ08/06 09:10
-!- mode/#epigram [+v pigworker] by ChanServ08/06 10:56
tsapimorning pigworker08/06 10:56
+pigworkermorning tsapi, how do?08/06 10:56
tsapinot bad thanks. How's the refactoring going?08/06 10:58
+pigworkerI stepped away for a few days to write a paper, but it's in a stable position just now.08/06 11:02
moleristsapi, pigworker: I have just pushed a patch migrating the new levitated IDesc to the new OpTree lang08/06 11:08
moleriscouple more HFs to kill, but it shouldn't be a problem08/06 11:08
+pigworkermoleris: cool; how was it? tsapi: just got your email08/06 11:09
molerismuch better than last time around, the cheap emb of values in to terms is a life saver as far as I'm concerned. Just hope the type checking uncertainty is not too high a price :)08/06 11:11
agundryHooray, I've proved that flip plus == plus08/06 11:11
agundrypedagand and I are giving a demo on Epigram tomorrow to a general compsci audience08/06 11:12
agundryany suggestions for better examples than commutativity of plus?08/06 11:13
+pigworkeragundry: flip plus == plus  is key! not true in Coq!08/06 11:14
agundryYes, that's why I thought I should check we can actually prove it08/06 11:14
tsapiagundry, simple examples are good I think. I think it's a bad idea to try to think of different ones because you're bored of the old ones.08/06 11:15
tsapiEg. Maybe is a very helpful example for understanding monads.08/06 11:15
+pigworkeragundry so, vzip? (or rather, vectorized application?)08/06 11:16
agundrytsapi: that's certainly true08/06 11:16
agundrypigworker: vzip/vapp could work, it will be interesting to see how bad the coercion woes get08/06 11:17
+pigworkeragundry: quite; I'm still curious to know if lazy defs help, but maybe now is not the time to find out08/06 11:19
+edwinbHmm, I wonder if I can sneak in to the SICSA conference tomorrow08/06 11:19
agundrypigworker: so am I, though perhaps I should wait until after tomorrow08/06 11:19
+pigworkeryes, see what's already workable08/06 11:21
+pigworkeralthough recompiling the thing with an experimental hack just before the demo is traditional...08/06 11:21
agundryedwinb: our demo is at the SICSA conference around 19.00; I don't think we will go to much else08/06 11:21
+edwinboh, apparently there's only you and Lars doing demos08/06 11:26
agundryyep, that could be amusing08/06 11:26
pedagandmmh, looks like if I want to go to work today, I've to give up on bike-to-work. Or people will say that I'm a "mud" man when I arrive.08/06 13:31
molerisIDesc: Now with 100% fewer higher order scopes08/06 13:44
agundrymoleris: nice work08/06 13:45
tsapimoleris: nice work :)08/06 13:46
molerista08/06 13:47
agundryI am experimenting with Fin at the moment, will re-enable the test case shortly08/06 13:48
+pigworkerI imagine that I have finished the DepRep paper, http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf but I suppose I should print it out and pretend to read it before I send it to WGP.08/06 14:17
tsapipigworker: cool! P.S. you can update the reference to the gentle art of levitation :)08/06 14:27
-!- mode/#epigram [+v soupdragon] by ChanServ08/06 14:33
+pigworker'deed I can!08/06 14:55
+pigworkerwill also add a bit more related work (McKinna/Pollack, Barras, Benton et al, Sheard)08/06 14:55
+soupdragon what's Benton et al ?08/06 14:57
+pigworker"Strongly typed term representations in Coq" (submitted to JAR)08/06 15:00
+soupdragonooh it's even in color08/06 15:00
+pigworkerI coloured it in during the exam board, yesterday afternoon.08/06 15:00
+pigworkertime for school...08/06 15:01
pedagandmoleris, do you have a data tactics for IDesc?08/06 15:15
molerispedagand: Sorry, no - I have plenty of bits n pieces but nothing ready for a demo :-(08/06 15:31
pedagandno problem, that was just curiosity. I'm myself in bits'n'pieces and am not ready for a demo either :-)08/06 15:32
agundryMaybe we should just fake it for Vec and Fin ;-)08/06 15:32
molerisI think it would be unwise to expose a general audience to the true horror IDesc, so I'd be tempted to fake it08/06 15:34
-!- mode/#epigram [+v dolio] by ChanServ08/06 16:03
-!- mode/#epigram [+v pigworker] by ChanServ08/06 16:12
-!- mode/#epigram [+v dolio] by ChanServ08/06 16:19
-!- mode/#epigram [+v Saizan] by ChanServ08/06 16:20
-!- mode/#epigram [+v Saizan] by ChanServ08/06 19:57
-!- mode/#epigram [+v pigworker] by ChanServ08/06 20:21
-!- mode/#epigram [+v dolio] by ChanServ08/06 20:43
-!- mode/#epigram [+v dolio] by ChanServ08/06 21:08
-!- mode/#epigram [+v soupdragon] by ChanServ08/06 22:24
-!- mode/#epigram [+v soupdragon] by ChanServ08/06 23:12
--- Day changed Wed Jun 09 2010
-!- mode/#epigram [+v dolio] by ChanServ09/06 01:08
-!- mode/#epigram [+v dolio] by ChanServ09/06 05:12
+soupdragonhttp://video.google.com/videoplay?docid=2717941286977874486#09/06 10:09
+soupdragonRussian animation: Cat Who Walked by Herself 09/06 10:09
+soupdragonnice version of the rudyard kipling story09/06 10:09
+soupdragonalso everyone probably picks up on this stuff long before me but this is very neat http://www.chargueraud.org/arthur/research/2010/cfml/09/06 10:10
+soupdragonProgram Verification Through Characteristic Formulae09/06 10:10
+soupdragonbringing Dijkstra back09/06 10:10
+soupdragonto pure functional programs09/06 10:10
tsapipigworker: the Forsberg & Setzer paper has been published at CSL by the way, I found a list of accpepted papers09/06 10:14
+pigworkertsapi: yeah, Hank told me; Toni hasn't updated his .bib09/06 10:15
roconnoris there a name for a conversion rule that would say that x = if b then x else x, or more generally allow convertability between any x and a match statement whose branches are all x?09/06 10:32
roconnorI don't even know if such a converability rule is sound.09/06 10:33
+edwinbThe problem would surely be that if you don't know b, you don't know it's not _|_, so the rule isn't sound?09/06 10:38
roconnoredwinb: I mean in a stronglly normalizing system, such as coq, agda or epigram09/06 10:38
roconnoredwinb: in coq we have && defined on bool such that (true && x) and x are convertable, but wouldn't it be so awesome if (x && true) and x were convertable as well!09/06 10:40
+soupdragonroconnor, you could probably hack that into CoqMT (I tried to do somethign a bit like that an failed, though)09/06 10:40
roconnorMT?09/06 10:41
+soupdragonright now it's got some arithmetic that lets you do stuff like   refl : x + y = y + x09/06 10:41
+soupdragonhttp://pierre-yves.strub.nu/research/coqmt/09/06 10:41
pedagandmodulo theory, he has a paper at CSL too09/06 10:41
roconnoroh right09/06 10:41
+soupdragonwhat is this CSL?09/06 10:41
roconnoris modulo theory less hacky than it sounds?09/06 10:42
+soupdragonI keep forgetting you just add 'dependent types' to any of these terms to google it09/06 10:42
+soupdragonroconnor, well it adds new decision procedures to the conversion rule - you have to prove the axioms for them in Coq09/06 10:42
+soupdragonnot sure if that makes it okay09/06 10:42
pedagandCSL: http://mfcsl2010.fi.muni.cz/csl/social-program  , look at the stuffs in *bold* :-)09/06 10:43
+edwinbroconnor: but even if it's strongly normalising, b might arise from, say, a proof of false09/06 10:50
roconnorhmm09/06 10:51
+pigworkerroconnor: if b then x else x would need to be invoked during head-normalization, to be sure that everything equal to a canonical form computes to a canonical form09/06 11:05
+pigworkerit's also not obviously type preserving for dependent if09/06 11:06
agundrywow, the Pig becomes much faster if one partially disables the scheduler09/06 11:07
agundrythis may help lessen my embarrasment at the demo tonight...09/06 11:07
+pigworkeragundry: doesn't surprise me; I'm quite sure Epigram 1 spent much of it's time checking that there wasn't anything important to do09/06 11:08
+pigworkerit's -> its09/06 11:08
agundryyes, somehow we need to keep track of that information, rather than searching the whole proof state09/06 11:09
+pigworkerspotting saturated regions would be a good start09/06 11:09
+pigworkerconsider P b = if b then (if b then Nat else Bool) else Nat09/06 11:11
+pigworkerobserve zero : P true, zero : P false, but zero not in P b if b a variable09/06 11:11
agundryhmm, I guess we are interested in two things: whether there any holes in a region, and whether there are any elaboration problems09/06 11:12
+pigworkerso if b then x else x = x needs its Sam Lindley friends to have a chance of being sound09/06 11:12
+pigworkeragundry: yes, no-orange-here, and the weaker no-orange-to-automate here would be useful09/06 11:14
+edwinbit's the sort of thing I'd quite happily do in the compiler since by then we know that either b is canonical, or we've crashed already09/06 11:21
+pigworkeredwinb: on another top, I'm wondering about projectors for next Wednesday...09/06 11:54
+pigworkerinsert ic09/06 11:54
+edwinbI assume you are going to use more traditional methods?09/06 11:55
+edwinbI think we have a steam powered projector in the room09/06 11:55
+pigworkerI'm going to do lots of live Agda09/06 11:56
+edwinboh, okay09/06 11:56
+pigworkerideal situation -- simultaneous projection; if I have to pick one, it'll have to be the computer09/06 11:56
+edwinbbut this could still mean live Agda on OHP ;)09/06 11:56
+edwinbit might be possible09/06 11:57
+pigworkertrue, but it's fun to actually run this code, even though it goes slower on a computer than on a handwritten slide09/06 11:57
+edwinbbut the layout of the room is such that if too many turn up, there is another half of the room with a second screen09/06 11:57
+edwinband I think it's only possible to project one thing twice, if that makes sense09/06 11:58
+pigworkeryes, but one with data and one with steam would work?09/06 11:59
+edwinbshould do, but I'd have to go to the room and check09/06 11:59
+edwinbwhich is not so easy since I'm at home at the minute09/06 11:59
+edwinbI'll go and look later09/06 12:00
+pigworkerwhat I'll probably do is write some acetate, but make sure I have digital photos, just in case; thanks for scoping it out!09/06 12:00
+pigworkerUnrelatedly, "Strongly Typed Term Representations in Coq" just got accepted by JAR. I am profoundly grateful to my coauthors for putting my name on the front.09/06 12:02
+edwinbOh splendid. I don't think I've seen that one.09/06 12:18
* edwinb finds it on the internets09/06 12:19
tsapipedagand, are the stratified model for the gentle art in the Pig09 repo?09/06 12:23
pedagandyes, anything which is not "TT" as a suffix of the filename09/06 12:24
pedagandthat is, Desc.agda and IDesc.agda09/06 12:24
tsapipedagand, cool, thanks09/06 12:24
roconnorpigworker: isn't if b then x else x impossible in the dependent case?  Each branch of the if statement has a different type in for the dependent if so it must be the case that each branch has a different term.09/06 12:36
+pigworkerroconnor: check the example!09/06 12:37
roconnoredwinb: I haven't quite figured how why having b arise from a proof of false would be problematic.  Granted you did make me feel nervous09/06 12:37
roconnorpigworker: oh, sorry I see now you wrote more09/06 12:38
+pigworkerthe point is that the branch types get to compute even if the return type is stuck09/06 12:38
roconnorheh, dependent type theory is so complicated :)09/06 12:39
roconnorwho is Sam Lindley?09/06 12:40
+pigworkeryeah, very sensitive to details of computation09/06 12:40
+pigworkerSam did a PhD in Edinburgh, amongst other things giving a reduction-based proof that beta-eta equality for simply typed lambda calculus with *coproducts* is decidable.09/06 12:42
+pigworkerHe was Phil Wadler's researcher for a bit, and now he works for a spin-out company.09/06 12:43
+pigworkerLike most people who have worked with eta-equality for coproducts, he never wants to work with eta-equality for coproducts again.09/06 12:43
tsapihehe09/06 12:44
roconnorbtw, what is a good reference for idiom brackets? The applicative functor's paper, or do you have a newer paper describing idiom brackets in SHE?09/06 12:48
+pigworkerthe applicative functor paper is the good reference09/06 12:48
+pigworkerI haven't written a SHE paper yet, and it's not going to happen by Monday.09/06 12:50
+pigworkerI still need a better story about what SHE's type system would be if you didn't turn all the {..} kinds into *.09/06 12:51
+pigworkerAnd besides, I'm supposed to be writing a grant proposal about SHE by Monday.09/06 12:52
roconnorsounds unfun09/06 12:52
+pigworkerIt's made me extraordinarily productive at almost everything else. I'm thinking of doing the dishes.09/06 12:53
+edwinbpigworker: we do appear to have a cardboard and string projector available. I imagine we can set it up to point to a useful bit of wall.09/06 14:54
+pigworkeredwinb: splendid!09/06 14:55
+pigworkeragundry, pedagand: do you want any more input from me for tonight?09/06 15:26
agundryhmm, I think we have a reasonable plan09/06 15:27
agundryif you are around we could chat about the demo file, but it's not too urgent09/06 15:28
+pigworkerI'm barely able to stay awake, but you could send me the file...09/06 15:28
agundryokay, but don't look at it for too long if sleep would be more useful!09/06 15:31
agundryemail away09/06 15:32
+pigworkerta09/06 15:32
agundryafter the demo I will tidy the file up and stick it somewhere visible to reddit ;-)09/06 15:32
+pigworkerlooks good (but we really must make more constraint solving happen mechanically)09/06 15:36
agundryyes, that is on my list of things to think about09/06 15:36
agundrymostly I have just hidden the ships in separate files09/06 15:36
+pigworkerok, but you should be in a position to say "these bits will eventually look after themselves"09/06 15:37
agundrythat is the intended semantics of "load" in the demo file... mostly09/06 15:38
+pigworkerfine09/06 15:38
tsapiagundry: good luck with your demo. I'd like to absorb what you've done into the manual/tutorial when you're done.09/06 15:39
agundrytsapi: thanks. That sounds like a good plan.09/06 15:41
-!- mode/#epigram [+v dolio] by ChanServ09/06 16:12
-!- mode/#epigram [+v dolio] by ChanServ09/06 17:08
-!- mode/#epigram [+v dolio] by ChanServ09/06 18:08
-!- mode/#epigram [+v dolio] by ChanServ09/06 19:12
-!- mode/#epigram [+v dolio] by ChanServ09/06 20:08
-!- mode/#epigram [+v Saizan] by ChanServ09/06 22:39
-!- mode/#epigram [+v Saizan] by ChanServ09/06 23:29
--- Day changed Thu Jun 10 2010
-!- mode/#epigram [+v Saizan] by ChanServ10/06 00:28
-!- mode/#epigram [+v Saizan] by ChanServ10/06 01:24
-!- mode/#epigram [+v pigworker] by ChanServ10/06 08:08
molerisMorning10/06 09:45
molerisagundry pedagand: How was the gig?10/06 09:46
agundrymoleris: okay, some people were mildly interested in what we are doing, others were completely bemused10/06 09:48
agundrypretty much as expected really10/06 09:48
agundryit was very amusing to have a huge TV screen on which to display a couple of emacs buffers10/06 09:49
moleris:)10/06 09:52
molerisas long as it didn't break too spectacularly10/06 09:52
agundryit didn't, not that we tried anything very adventurous10/06 09:53
agundrythough pedagand did open the category theory file at one point10/06 09:53
molerisyou do well to avoid going too far off script at these types of things10/06 09:53
agundryunfortunately the compiler seems not to be working at the moment10/06 09:53
agundryso we couldn't demonstrate that10/06 09:54
molerishmm, it what way is it broken?10/06 09:54
agundryit doesn't cope with operator primitives (but a cheap fix is to add them to support.e)10/06 09:55
agundrymoreover, plus two two evalues to two10/06 09:55
agundry*evaluates10/06 09:55
molerisirk10/06 09:55
agundryI'm not sure what is going on with the operator DSEL, otherwise I would have spent more time debugging10/06 09:56
molerisI'm not sure what state the code is in that generates support.e code from OTrees10/06 09:56
agundryI couldn't find it, though I didn't look very hard10/06 09:57
molerisand there are still a number of operators with legacy code10/06 09:57
molerisno, it shouldn't be10/06 09:57
molerisI have a meeting this morning (possibly) but after that I might get my hands dirty porting a few more operators10/06 09:58
agundrythanks10/06 09:59
-!- mode/#epigram [+v pigworker] by ChanServ10/06 11:32
molerispigworker: the green equality - is it going?10/06 11:45
agundrypigworker says we should get rid of it, and I agree10/06 11:45
molerisporting it to OpTree is going to be a big deal, so I also agree :)10/06 11:46
-!- mode/#epigram [+v dolio] by ChanServ10/06 15:01
-!- mode/#epigram [+v Saizan] by ChanServ10/06 15:24
-!- mode/#epigram [+v Saizan] by ChanServ10/06 17:04
-!- mode/#epigram [+v pigworker] by ChanServ10/06 17:16
-!- mode/#epigram [+v Saizan] by ChanServ10/06 17:36
-!- mode/#epigram [+v dolio] by ChanServ10/06 20:08
-!- mode/#epigram [+v Saizan] by ChanServ10/06 21:54
--- Day changed Fri Jun 11 2010
-!- mode/#epigram [+v dolio] by ChanServ11/06 00:11
-!- mode/#epigram [+v Saizan] by ChanServ11/06 02:50
-!- mode/#epigram [+v Saizan] by ChanServ11/06 03:01
-!- mode/#epigram [+v pigworker] by ChanServ11/06 09:15
-!- mode/#epigram [+v pigworker] by ChanServ11/06 14:26
-!- mode/#epigram [+v dolio] by ChanServ11/06 15:11
-!- mode/#epigram [+v dolio] by ChanServ11/06 16:11
+edwinbHmm. Things I didn't expect to be doing this afternoon: Explaining monads to the head of school11/06 16:18
-!- mode/#epigram [+v Saizan] by ChanServ11/06 16:49
-!- mode/#epigram [+v Saizan] by ChanServ11/06 17:46
-!- mode/#epigram [+v Saizan] by ChanServ11/06 17:57
-!- mode/#epigram [+v dolio] by ChanServ11/06 18:11
shaprYow!11/06 18:13
tsapishapr: only tumbleweed in here today :)11/06 18:14
shapraww11/06 18:14
shaprIt's so quiet!11/06 18:14
-!- mode/#epigram [+v dolio] by ChanServ11/06 20:07
-!- mode/#epigram [+v dolio] by ChanServ11/06 20:15
-!- mode/#epigram [+v Saizan] by ChanServ11/06 21:25
-!- mode/#epigram [+v pigworker] by ChanServ11/06 21:33
-!- mode/#epigram [+v pigworker_] by ChanServ11/06 22:27
-!- pigworker_ is now known as pigworker11/06 22:27
-!- mode/#epigram [+v Saizan] by ChanServ11/06 22:34
-!- mode/#epigram [+v Saizan] by ChanServ11/06 23:02
--- Day changed Sat Jun 12 2010
-!- mode/#epigram [+v Saizan] by ChanServ12/06 00:00
-!- mode/#epigram [+v dolio] by ChanServ12/06 00:07
-!- mode/#epigram [+v Saizan] by ChanServ12/06 02:37
-!- mode/#epigram [+v dolio] by ChanServ12/06 03:11
-!- mode/#epigram [+v Saizan] by ChanServ12/06 05:14
+pigworkerhttp://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/models/Alg-IIR.agda12/06 11:38
+pigworkerIt's a more "algebraic" presentation of indexed induction recursion, with examples (Nat, freshlists, a universe).12/06 11:39
+dolioSo, descriptions of indexed induction-recursion only require induction-recursion for their definition?12/06 12:32
-!- pigworker_ is now known as pigworker12/06 12:35
+dolioSo, descriptions of indexed induction-recursion only require induction-recursion for their definition?12/06 12:37
+dolio(That'll look weird in the logs, probably.)12/06 12:39
+dolioOh, descriptions of indexed families were just an inductive type, too.12/06 12:42
-!- mode/#epigram [+v codolio] by ChanServ12/06 14:10
+codolioHere's something: Agda accepts your code fine, but when I go to generate html, it complains about DATA not being strictly positive.12/06 14:36
-!- codolio is now known as dolio12/06 14:36
+doliopigworker ^^12/06 14:37
+dolioAlthough it's a strange version of the error. It's not complaining about anything that's obviously to the left of an arrow.12/06 14:42
+dolioPerhaps it's related to decode not termination checking as written?12/06 14:42
-!- mode/#epigram [+v pigworker] by ChanServ12/06 15:02
+pigworkerdolio: that's weird12/06 15:03
+pigworkermostly, when I do that sort of construction, I expect termination to moan and positivity to grumble; it's *size* I'm watching12/06 15:04
+dolioWell, I don't really understand what it's complaining about. The alleged problem is 'DATA occurs in the 4th argument to Func in the type of <_> in the definition of DATA which occurs in the 4th argument to deco in an argument to a bound variable in the first clause of in the definition of decode, which occurs in the 5th argument to Func in the type of the constructor <_> in the definition of DATA'.12/06 15:06
-!- mode/#epigram [+v dolio] by ChanServ12/06 15:10
+doliopigworker: I guess it's ultimately complaining that the 'd' in decode might introduce negativity (I think that's right).12/06 15:13
+dolioI don't understand why it works fine in the emacs mode and not for generating html. Maybe my versions are mismatched or something.12/06 15:13
+dolioAnyhow: http://code.haskell.org/~dolio/agda-share/universes/IRDataHierarchy.agda12/06 15:30
+dolioThat's an attempt at a hierarchy of inductive-recursive universes closed under induction-recursion.12/06 15:31
+dolioI'm not sure if I've got everything, though.12/06 15:31
-!- mode/#epigram [+v Saizan] by ChanServ12/06 15:43
-!- mode/#epigram [+v dolio] by ChanServ12/06 15:56
* dolio remembered something that makes him skeptical that he did his IR universes right.12/06 18:22
-!- mode/#epigram [+v Saizan] by ChanServ12/06 18:27
+dolioWell, that actually worked out much better than expected.12/06 19:21
-!- mode/#epigram [+v dolio] by ChanServ12/06 20:10
-!- mode/#epigram [+v pigworker] by ChanServ12/06 22:46
-!- shapr` is now known as shapr12/06 23:27
--- Day changed Sun Jun 13 2010
-!- mode/#epigram [+v dolio] by ChanServ13/06 00:11
-!- mode/#epigram [+v codolio] by ChanServ13/06 01:10
-!- mode/#epigram [+v Saizan] by ChanServ13/06 01:14
-!- mode/#epigram [+v dolio] by ChanServ13/06 02:07
-!- mode/#epigram [+v Saizan] by ChanServ13/06 03:07
-!- mode/#epigram [+v dolio] by ChanServ13/06 07:10
-!- mode/#epigram [+v Saizan] by ChanServ13/06 07:18
-!- mode/#epigram [+v dolio] by ChanServ13/06 08:07
-!- mode/#epigram [+v Saizan] by ChanServ13/06 10:06
-!- mode/#epigram [+v dolio] by ChanServ13/06 11:07
-!- mode/#epigram [+v dolio] by ChanServ13/06 14:11
-!- mode/#epigram [+v Saizan] by ChanServ13/06 14:15
-!- mode/#epigram [+v Saizan] by ChanServ13/06 14:19
tsapiI wonder if we should follow this advice to make our webservers display agda files nicely: http://www.w3.org/International/questions/qa-htaccess-charset13/06 20:42
tsapiby defaulting to utf-8 encoding13/06 20:43
tsapithanks to pedagand for another informative weekly summary!13/06 20:59
pedagandglad you like, really13/06 20:59
pedagandit's good to know that some people actually look at it :-)13/06 21:00
+dolioAm I missing out on epigram action somewhere?13/06 21:00
tsapidolio: aren't you subscribed to epigram-discuss?13/06 21:01
+dolioI guess not.13/06 21:02
+dolioJust to the old epigram list that no one uses anymore.13/06 21:02
tsapihttp://www.e-pig.org/darcs/Pig09/web/#community13/06 21:02
tsapithe old durham one is dead i think13/06 21:03
+dolioIt's the place to look if  you want to learn about filling in impossible cases of total functions with junk, though.13/06 21:05
-!- mode/#epigram [+v dolio] by ChanServ13/06 21:06
pedaganddolio, your subscription is approved, welcome ;-)13/06 21:08
+dolioSweet.13/06 21:08
+dolioSo, pigworker displayed a Desc for induction recursion in Agda yesterday...13/06 21:11
+dolioAnd I did my thing and put it in a hierarchy of inductive-recursive universes.13/06 21:11
+dolioBut that leaves me with a conundrum:13/06 21:11
+dolioI thought that the Dybjer & Setzer paper on induction-recursion mentioned that having an internal Mahlo universe was stronger than one having an external universe.13/06 21:12
+dolioBut the thing I defined sort of seems like an internal one, but defined using an external one.13/06 21:13
+dolioPerhaps it's just an illusion, though.13/06 21:13
+dolioOr perhaps I just don't understand the distinction.13/06 21:15
stevanhi, could the mailing list be added to gmane (http://gmane.org/subscribe.php)? they provide rss feeds, which is nice for people like me who mostly read. thanks!13/06 21:49
pedagandI'm doing it13/06 22:00
stevanawesome!13/06 22:01
pedaganddone, it's awaiting moderation13/06 22:12
pedagandthere already was an epigram mailing list, so I asked for epigram213/06 22:14
pedagandI'm having a thought for the next generation of PhD students, trying "epigram", then "epigram2", to settle for "epigram3"13/06 22:14
+edwinbI thought we were onto 'suc epigram' by now13/06 22:16
pedagand:-)13/06 22:29
+Saizannice post13/06 22:43
pedagandSaizan, I'll try to watch Italy-Paraguay and make a silly joke out of it. I won't promise it, tho, I'm quite busy these days ;-)13/06 22:56
pedagandyou're in what looks like a rather easy group, lucky Italians!13/06 22:56
+edwinbyou'll do well to beat English goalkeeper comedy13/06 22:57
pedagandI was in a pub in Edinburgh watching it: it is surprising to see people delighted to see their own "country" take a goal13/06 22:58
+edwinbScotsmen will be cheering for Anyone But England13/06 23:00
+edwinbas a substitute for having a team worth supporting13/06 23:00
pedagandit looks like a French striker such as Henry is more able of his hands than your goalkeeper :-)13/06 23:00
+edwinbheh13/06 23:01
pedagandstrange country indeed ;-)13/06 23:01
+edwinbtoo right13/06 23:01
+Saizanhah, i wonder if some people in the so-called "Padania" do the same here, i think they have a team in some alternative world cup too :)13/06 23:07
+edwinbSometimes Scotland qualify, but they always go out early13/06 23:08
+Saizanplus_11.impl_2.makeE_2.m_1.s_0.e_0.xf_0.u_0.u_0 >  <- the component names here are not meant to be readable, right?13/06 23:14
pedagandsome people have this ability, the rest of us don't13/06 23:16
pedagandI've a patch that gives you the first and last component, putting the remaining in ellipsis when necessary13/06 23:16
pedagandhere, I can see that you define plus in a let, you called elimination with a motive, you're working on a subgoal, I suspect the second one, and misery ensued13/06 23:17
pedagandif the last name is a "hole_xxx", this tells you that an elaboration problem is stuck (often, something wrong happened)13/06 23:18
+Saizanimpl_2 is the elimination?13/06 23:19
pedagandimpl is, I think, generated by the "let" construction13/06 23:20
pedagand"makeE" is generated by elimination with a motive13/06 23:20
+Saizanah, yeah13/06 23:20
+Saizanpaying attention while stepping through the script helps :)13/06 23:20
pedagandCochon prints these details for debugging purposes, these things ought to be hidden in a high-level language13/06 23:21
+Saizanah btw, what's the relation between UI/ and DisplayLang/ ?13/06 23:30
pedagandin UI/, we define interfaces to the theorem prover13/06 23:32
pedagandright now, DisplayLang is considered as a part of the theorem prover, like ProofState13/06 23:33
pedagandthat's an interesting question, thanks for asking13/06 23:36
+dolioHere's a probably less interesting one: where do the names "green" and "blue" equality come from?13/06 23:37
+dolioSyntax coloring somewhere?13/06 23:37
tsapidolio: epigram syntax colouring - blue is a type constructor, green is a function13/06 23:38
+dolioAh.13/06 23:38
+dolioThat's what I'd have guessed, except the other way around.13/06 23:39
+Saizanbtw, HsColour does a decent job on .pig files13/06 23:39
+dolioSince Agda is backwards (actually, I can't think of what color type constructors are...).13/06 23:40
+dolioApparently they're also blue, same as functions.13/06 23:40
pedagandSaizan, actually, DisplayLang ought to be in UI/ as well. I'm opening a ticket, thanks13/06 23:43
+Saizanpedagand: ah :), though modules like ProofState import it, but not for any good reason?13/06 23:48
pedagandthat's where the rat nest starts... It will be politically correct to import from UI/Lib. So, I'm hoping to share bits of the DisplayLang in UI/Lib, while specializing others in UI/Cochon13/06 23:50
pedagandfor example, I would really love to get DisplayLang/Lexer and DisplayLang/TmParse out of the way, in UI/Cochon13/06 23:50
pedaganda stripped-down version of the display language is probably a good start for any interface. Then, you would have "interface-specific" constructions in your UI/YourStuff13/06 23:52
+Saizantrue13/06 23:54
--- Day changed Mon Jun 14 2010
+Saizanand it's also needed for Features.* currently14/06 00:00
pedagandwonderful :-)14/06 00:03
+Saizanprogramming goals are messing with my brain, i'm used to only seeing types in goals, from Agda, so i try to interpret e.g. "max^1 x y" in "Programming: < max^1 x y : Nat >" as a type, so i end up thinking of twelf where max would actually be a data family (except with 3 arguments) ..14/06 00:31
-!- mode/#epigram [+v dolio] by ChanServ14/06 04:10
-!- mode/#epigram [+v dolio] by ChanServ14/06 05:06
-!- mode/#epigram [+v pigworker] by ChanServ14/06 08:06
-!- mode/#epigram [+v Saizan] by ChanServ14/06 12:34
-!- mode/#epigram [+v pigworker] by ChanServ14/06 13:40
-!- mode/#epigram [+v dolio] by ChanServ14/06 14:06
+pigworkeredwinb: just to confirm that, bar further unforeseen calamities, I'm on for Wednesday14/06 18:25
+edwinbpigworker: okay, thanks for letting me know14/06 18:25
-!- mode/#epigram [+v pigworker_] by ChanServ14/06 18:38
-!- pigworker_ is now known as pigworker14/06 18:40
-!- mode/#epigram [+v dolio] by ChanServ14/06 19:10
-!- mode/#epigram [+v Saizan] by ChanServ14/06 19:47
pedagandpigworker, got hurkens paradox in my system: doesn't type-check with stratification On, does with stratification Off.14/06 20:38
pedagandhowever, the way it doesn't type-check is rather disappointing: it is very early on, with one of the helper function14/06 20:40
+dolioI don't think that's unusual.14/06 20:49
+doliocode.haskell.org doesn't seem to be responding...14/06 20:52
+dolioAnyhow, I have the paradox encoded for a system U interpeter there.14/06 20:52
+dolioBut I think it would blow up early there, too, because otherwise U would be too large to pass to itself.14/06 20:53
pedagandhaskell.org being down is not unusual as well ;-) 14/06 20:53
+dolioYeah.14/06 20:53
pedagandyep, that's the thing: I take s : U and do "s U" in one of the early term14/06 20:54
pedagandwhat is system U, btw?14/06 20:54
+dolioIt's similar to the calculus of constructions, but with 3 levels, and impredicativity on the second level.14/06 20:55
+dolioIt's what Hurkens uses in his paper.14/06 20:55
+dolioActually, I think he uses U-, which has impredicative quantification over the third level in the second level, but not the first level.14/06 20:56
+dolioBecause the latter isn't used at all.14/06 20:56
pedagandha, indeed. I'm really struggling with his notation and terminology...14/06 20:57
+dolioYeah, it's rough.14/06 20:58
+dolioI actually cribbed from the Agda encoding.14/06 20:58
+dolioAnd only looked at his paper to fix up the types.14/06 20:58
+dolioI actually had to rewrite a portion of my interpreter while doing that.14/06 20:58
+dolioBecause it revealed serious variable capture issues.14/06 20:59
+doliohttp://code.haskell.org/~dolio/pts/hurkens.pts14/06 21:54
+dolioThere it is.14/06 21:54
pedagandthanks14/06 22:00
pedagandout of curiosity, which language is that?14/06 22:01
pedagandha, I see, that's pts, your language :-)14/06 22:04
+dolioYes.14/06 22:09
+dolioIt's a rudimentary interpreter for pure type systems, and I've been adding more and more systems over time.14/06 22:10
+dolioAs you can probably tell, it doesn't do anything very fancy. In fact, it's pretty much entirely based around the REPL. Even the files just contain lists of REPL commands.14/06 22:12
+dolioAnyhow, if [] weren't impredicative, U would have type triangle, I think.14/06 22:32
+dolioAnd it would be inelligible to be an X.14/06 22:32
-!- mode/#epigram [+v dolio] by ChanServ14/06 23:10
-!- shapr` is now known as shapr[14/06 23:14
-!- mode/#epigram [+v Saizan] by ChanServ14/06 23:19
--- Day changed Tue Jun 15 2010
-!- mode/#epigram [+v pigworker] by ChanServ15/06 07:48
-!- mode/#epigram [+v pigworker] by ChanServ15/06 11:00
-!- mode/#epigram [+v dolio] by ChanServ15/06 13:06
-!- mode/#epigram [+v Saizan] by ChanServ15/06 14:32
--- Day changed Wed Jun 16 2010
-!- mode/#epigram [+v dolio] by ChanServ16/06 04:06
-!- mode/#epigram [+v dolio] by ChanServ16/06 04:21
-!- mode/#epigram [+v dolio] by ChanServ16/06 07:09
-!- mode/#epigram [+v codolio] by ChanServ16/06 08:09
-!- mode/#epigram [+v dolio] by ChanServ16/06 09:06
-!- mode/#epigram [+v dolio] by ChanServ16/06 13:09
-!- mode/#epigram [+v codolio] by ChanServ16/06 17:09
-!- mode/#epigram [+v dolio] by ChanServ16/06 18:05
-!- mode/#epigram [+v dolio] by ChanServ16/06 20:09
--- Day changed Thu Jun 17 2010
-!- mode/#epigram [+v dolio] by ChanServ17/06 00:09
-!- mode/#epigram [+v Saizan] by ChanServ17/06 00:40
-!- mode/#epigram [+v pigworker] by ChanServ17/06 08:38
-!- mode/#epigram [+v dolio] by ChanServ17/06 09:05
-!- mode/#epigram [+v pigworker] by ChanServ17/06 13:24
molerispigworker: Don't suppose you've had a thoughts about TELescopes and the new 1st order terms have you?17/06 13:46
+pigworkerwhere do we use them? I wonder if we need them now17/06 13:48
molerisMainly for opTypes, I can't see them being much use now17/06 13:53
moleriswill be a labourious job to get rid, but it's just grind17/06 13:54
+pigworkerthe alternative is to have HO telescopes and quote them to make types17/06 14:02
+pigworkerthat might be cheaper for now17/06 14:03
+pigworkernobody ever updates a TEL, right?17/06 14:05
molerisdon't think so17/06 14:07
molerispity is cheap at the moment, though - if we go that way it'll need to be lifted to ((->) NameSuppy)17/06 14:12
+pigworkerwe'd need a name supply to do the quotation, aye17/06 14:19
-!- mode/#epigram [+v Saizan] by ChanServ17/06 14:46
-!- mode/#epigram [+v dolio] by ChanServ17/06 15:09
-!- mode/#epigram [+v dolio] by ChanServ17/06 16:09
-!- mode/#epigram [+v codolio] by ChanServ17/06 18:09
shaprYow!17/06 18:14
shapr@quote epigram17/06 18:14
lambdabotdolio says: Perhaps he's an epigram guy and frowns on Turing completeness.17/06 18:14
+codolioOh, there's a bot in here.17/06 18:24
-!- mode/#epigram [+v dolio] by ChanServ17/06 19:08
-!- mode/#epigram [+v dolio] by ChanServ17/06 20:04
-!- mode/#epigram [+v codolio] by ChanServ17/06 21:09
-!- codolio is now known as dolio17/06 21:44
--- Day changed Fri Jun 18 2010
-!- mode/#epigram [+v dolio] by ChanServ18/06 01:09
-!- mode/#epigram [+v dolio] by ChanServ18/06 06:08
-!- mode/#epigram [+v codolio] by ChanServ18/06 10:20
-!- mode/#epigram [+v pigworker] by ChanServ18/06 11:00
-!- mode/#epigram [+v dolio] by ChanServ18/06 11:20
-!- mode/#epigram [+v dolio] by ChanServ18/06 12:16
+pigworkerpedagand: in your stratified system, does Pi bind a variable itself, or is it parametrized by a function?18/06 12:33
pedagandright now, it is a function18/06 12:34
pedagandI mean, parameterized by a function18/06 12:35
+pigworkerYeah, that's what the implementation suggests.18/06 12:35
pedagandI chose that one because it's the one we use in the implem, but as we know, it led to issues in the past. So this might change if the proof barfs on it18/06 12:37
+pigworkerI'm trying to check the (GFTP) property that bigging-up types preserves judgments, and I don't seem to get it if Pi takes a function.18/06 12:37
pedagandthat's the good old issue18/06 12:39
+pigworkerthat's why I thought I'd check18/06 12:39
+pigworkerthe bind-a-var way might go through; I'll try it18/06 12:40
pedagandif you bind, you can use the context-part of the GFTP and you ought to be safe18/06 12:43
+pigworkerthat's what I hope will happen18/06 12:43
+pigworkerhmm, what's the easiest way to get a whiteboard on IRC?18/06 12:45
+pigworkerI mean, a photo of a whiteboard18/06 12:45
pedagandthe same than what you do on tweeter?18/06 12:46
+pigworkeryeah, I suppose I could just use twitter18/06 12:47
pedaganddid the STLC part make any sort of sense? 18/06 12:55
pedagand*made18/06 12:56
+pigworkerIt's very weird, because it's not obvious why one wants a lambda calculus with a hierarchy of Set levels but no quantifiers.18/06 13:08
pedagandas mentioned in the intro, nobody wants that :-) but it's easier to explain the machinery in that setting. 18/06 13:10
pedagandbecause, in the dependent case, the weird thing is that the machinery makes no sense18/06 13:10
pedagand(or very little)18/06 13:11
+pigworkerI'd rather find the sense the machinery makes, than explain the machinery in a context where the application doesn't really motivate it. If the former is an option...18/06 13:28
pedagandI'm working on it18/06 13:29
pedagandthis "pigworker has quit" is like a David Lynch movie for me: it's innocent, but hides a cruel question18/06 14:38
pedagandhas Conor left for the pub? Or for supervision?18/06 14:38
pedagandlife is tough :-)18/06 14:39
-!- mode/#epigram [+v dolio] by ChanServ18/06 15:16
-!- mode/#epigram [+v dolio] by ChanServ18/06 16:20
-!- mode/#epigram [+v Saizan] by ChanServ18/06 17:36
-!- mode/#epigram [+v Saizan] by ChanServ18/06 19:41
-!- mode/#epigram [+v soupdragon] by ChanServ18/06 19:59
-!- mode/#epigram [+v dolio] by ChanServ18/06 21:16
--- Day changed Sat Jun 19 2010
-!- mode/#epigram [+v dolio] by ChanServ19/06 01:16
-!- mode/#epigram [+v dolio] by ChanServ19/06 05:19
pedagandhow does the TYPES workshop "works"? it is not clear from the website what is the dependency between "giving a talk" and "getting a paper in the post-proceedings". Anybody familiar with this scheme?19/06 10:54
tsapipedegand: there isn't any the the post-proceedings are an open call. There is not usually an obligation to give a talk (at all or on the same topic)19/06 10:56
tsapipedagand19/06 10:56
pedagandha, ok, thanks19/06 10:57
tsapiactually it says this on the website http://types10.mimuw.edu.pl/19/06 10:58
pedagandindeed, but that sounded so strange I couldn't believe it :-)19/06 10:59
tsapipedagand: :) has the deadline recently passed?19/06 10:59
pedagandI've no clue19/06 10:59
pedagandI cannot find any deadline, that's my other problem19/06 11:00
pedagandnor can I find an indication of the page limit19/06 11:00
tsapiI now found the one for the types 2009, the deadline for the post proceedings was in 26th May 2010. The next types meeting is in October.19/06 11:29
pedagandtsapi, thanks19/06 14:08
-!- mode/#epigram [+v codolio] by ChanServ19/06 16:18
-!- mode/#epigram [+v dolio] by ChanServ19/06 17:16
pedaganddid Randy Pollack wrote a paper on implementing records in a dependent type-theory? dblp doesn't give anything19/06 17:48
pedagandI know from pigworker and a mention in the Coq'art that he worked quite a lot on this topic19/06 17:49
tsapihttp://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf has a reference: Dependently typed records in type theory (Pollack 2002)19/06 17:54
pedagandhaha, interesting coincidence. Thanks again19/06 17:56
tsapi:)19/06 17:56
-!- mode/#epigram [+v dolio] by ChanServ19/06 18:20
-!- mode/#epigram [+v dolio] by ChanServ19/06 19:15
-!- mode/#epigram [+v codolio] by ChanServ19/06 20:19
pedagandwhy did we abandoned the Features.Container file? Was it just too difficult to implement, or we stumbled on a theoretical limit?19/06 20:52
molerispedagand: I think we changed our minds about how we wanted that stuff to be implemented.19/06 21:58
pedagandfor no particular reason? :-)19/06 22:00
molerisprobably19/06 22:00
molerisI think there's a neater way to deal with the indexing19/06 22:01
pedagandok, fair enough19/06 22:01
molerisThe stuff in models/Containers.agda would work well enough19/06 22:02
molerisbut it's also a real headf*ck to write that stuff in a fully explicit TT19/06 22:02
pedagandyou write "there's a neater ...": you mean, the current one is not perfect and you have a better story?19/06 22:03
molerisI have another version of that file somewhere19/06 22:04
pedagandindeed, I've just implemented records and that was already too much headf* for me :-)19/06 22:04
pedagandok19/06 22:04
molerisif you look at that file there's a function called rearrange which is just one part of a dumb isomorphism19/06 22:05
moleristhat we need to define it suggests that the pieces of the jigsaw are not quite sliding into place properly19/06 22:06
molerisI really want to internalise Mu/Nu in the Desc universe soon though19/06 22:08
pedagandha... long ago, the plan was to sort out "language with binders", so that the internal fix-points come easily19/06 22:08
pedagandI mean, as we wrote in the conclusion of the Desc paper19/06 22:09
pedagandI think the idea was that free monadic IDesc + a bit of machinery, we would get real substitution on IDesc19/06 22:11
-!- mode/#epigram [+v dolio] by ChanServ19/06 22:16
pedagandactually, models/FMSB is precisely about that19/06 22:17
molerisBinding not the whole of the story19/06 22:19
moleris*is19/06 22:19
molerisand since we haven't sorted binding out either ;)19/06 22:19
pedagandoh, I trust you on that 19/06 22:20
molerisI can't find that file, must have hidden it somewhere19/06 22:20
moleristo protect myself from the horrors contained within19/06 22:21
pedagand:-)19/06 22:24
-!- mode/#epigram [+v Saizan] by ChanServ19/06 23:17
--- Day changed Sun Jun 20 2010
-!- mode/#epigram [+v dolio] by ChanServ20/06 00:16
-!- mode/#epigram [+v Saizan] by ChanServ20/06 07:39
-!- mode/#epigram [+v dolio] by ChanServ20/06 10:18
-!- mode/#epigram [+v dolio] by ChanServ20/06 12:15
tsapiI also copied xclock, hoping to use it to test if equis is working but I don't know how to invoke it20/06 12:47
tsapi(wrong window)20/06 12:47
pedagandin models/Records.agda (just pushed), I've been trying to play the "embedding a post-fix language" (Okasaki) in Agda20/06 13:29
pedagandI fake polymorphism with an implicit {a : Set}20/06 13:29
pedagandhowever, if I go into dependant arguments, Agda rightfully goes nuts on the resulting unification problem (I think)20/06 13:29
pedagandis there a "dependant" trick to achieve a similar effect?20/06 13:30
+Saizanpedagand: this typechecks here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26398#a2639820/06 13:49
pedagandbrilliant!20/06 13:50
pedagandthat was the trick...20/06 13:51
pedagandthanks20/06 13:51
+Saizanyou're welcome :)20/06 13:52
pedagandsadly, Epigram doesn't solve this kind of constraint apparently. Oh, well...20/06 14:17
-!- mode/#epigram [+v codolio] by ChanServ20/06 15:19
scriptdevilI am reading the paper "Why Dependent Types Matter". In it, in the very first code snippet, there is order x y <= rec x20/06 18:31
scriptdevilWhat does the rec x mean herE?20/06 18:31
scriptdevil Does it mean that we apply the recursive expansion of x? i.e. (1+x)?20/06 18:35
scriptdevilOk. Reading onwards answered the question. :)20/06 18:37
ccasinI think it means "I am going to define this by structural induction on x"20/06 18:43
ccasinwhich you can see they then go on to do20/06 18:43
pedagandscriptdevil, "<=" is called the "by" gadget: it is given an elimination principle (rec x here) and it applies "elimination with a motive" strategy20/06 18:52
pedagandmost of them, for datatypes, it's a call to an induction principle20/06 18:52
pedagandin Agda, for example, this machinery is hidden behind the pattern-matching abstraction. Here it's explicit.20/06 18:52
pedagandit also means that we don't have/don't need an external "termination checker": when definition your function, you give the proof that it terminates20/06 18:53
ccasinpedagand: forgive my ignorance, but are the elimination principles defined within epigram or are a fixed set of them hard-wired in?20/06 18:59
ccasin(I really need to read that paper)20/06 18:59
pedagandignorance forgiven, otherwise how would I deal with myself? :-) you have "basic" induction principles, such as the generic one for data-types, or for Sigma-types, etc.20/06 19:00
pedagandbut you can also define your own20/06 19:00
pedagandfor example, there is "ship", the function doing substitution of equal for equal20/06 19:01
pedagandalso, from the basic induction principle of data-types, you can define others20/06 19:01
pedagandfor example, for Nat, we give you "simple induction" (H(0), H(n) -> H(n+1))20/06 19:02
ccasinyes, sounds nifty20/06 19:02
pedagandbut you can go on defining "strong induction"20/06 19:02
pedagandactually, Adam has defined strong induction "generically" for an inductive data-type (I think)20/06 19:02
ccasinusing your levitation stuff?  that sounds very cool20/06 19:02
pedagandyes, but you can do it anywhere. That's Gimenez strong induction principles, or Conor's memoization technique20/06 19:03
pedagandjust that, in this case, we can do it inside the type theory20/06 19:04
ccasinyes, well, that's the cool part20/06 19:04
ccasinnow, the "basic" one for datatypes, that must be built in? (I mean, could you define it within epigram?)20/06 19:04
pedagandyes, indeed20/06 19:04
ccasinI can't wait to start playing with epigram2... maybe after the popl deadline I'll have time20/06 19:06
pedagandyes (I re-convinced myself): you need somewhere to start: to define an operation on Desc (such as the induction principle), well, you need something to induct on Desc 20/06 19:07
pedagand:-)20/06 19:07
pedagandthis is not good for mental health to have such self-definition :-)20/06 19:07
ccasinpedagand: that's what I figured, but sometimes I'm confused by where the levitation technique bottoms out20/06 19:07
pedagandme too, I'm afraid 20/06 19:08
ccasin:)20/06 19:08
+Saizanthere's this UI/Haskell though, how much does that intend to cover? since to desugar a normal haskell recursive definition into induction principles you'd need something like a termination checker, no?20/06 19:11
pedagandbut actually, it doesn't "bottom out", it "tops up", I would say: you define Desc and its induction principle at some level Set(n). Then we can build it inside Set(n-1), Set(n-2), etc. 20/06 19:12
pedagand(provided you give yourself a Mu at each level, and so on)20/06 19:12
pedagandSaizan, that's something Adam is into, I think. As for me, I just know that, for this interface, they will add an axiom of general recursion20/06 19:13
pedagandI heard a discussion, but I'm not really a proponent on that story20/06 19:13
pedagandthe idea seems to be that currently Haskell is being developed over some more and more System-F-ish system20/06 19:14
pedagandConor's idea is to express Haskell's concepts in Martin-Lof type theory20/06 19:14
pedagandI hope I'm not spoiling any industrial secret! :-)20/06 19:14
+Saizanhehe :)20/06 19:14
ccasina cool idea - though a pain for the implementor, considering how often the haskell core changes!20/06 19:15
pedagandI think it's more meant toward "formalising Haskell", and having some confidence when you add features to it20/06 19:15
pedagandlike what your boss is currently doing, I heard ;-)20/06 19:16
ccasinYes :)  Well, it seems someone is always doing it, for the current definition of "Haskell"20/06 19:17
ccasinan embedding into a more expressive language would be very nice, though20/06 19:17
pedagandthat would also be great fun to write Haskell interactively! that's what hooked me20/06 19:18
ccasinneat20/06 19:19
ccasinthough I'll believe it's faster to write haskell from inside a type theory when I see it :)20/06 19:20
pedagand:-)20/06 19:23
scriptdevilOk. Next question. I kinda wanna start learning type theory. I started with TTFP by Simon Thompson. Still in it. Then read this paper when I wanted to understand the uses of dependent function types. Am I going the right path or is any other book better? I know classical logic quite well. 20/06 19:29
pedagandthere is also Nordgstrom [http://www.citeulike.org/user/pedagand/article/2310446]20/06 19:32
pedagand*Nordstrom20/06 19:32
pedagandbut I couldn't tell if Thompson is better than Nordstrom, they are just "different"20/06 19:33
pedagandare you having fun reading the "Why dependant types matter"? Or it's a painful agony? (bits of it are doing this to me)20/06 19:34
ccasinI have read (most of) Nordstrom - it's good if what you want to know is how to express some programs in a very explicit type theory, but less good if what you want to know is "what is type theory"20/06 19:35
tsapithis one is also good: http://www.cs.nott.ac.uk/~txa/lof.pdf20/06 19:37
tsapibut there is nothing /really good/ I don't think20/06 19:38
ccasinscriptdevil: what is your level of familiarity with reasoning about basic functional languages?  You might want to start with something simpler like Pierce's "Types and Programming Languages" or similar.  Most of these papers about fancier theories assume that stuff as background knowledge20/06 19:38
pedagandtsapi, you're really proud of your warez copy of Martin-Lof, aren't you? :-)20/06 19:38
tsapisomebody should write a type theory textbook20/06 19:38
tsapi:)20/06 19:38
tsapinothing to do with me :)20/06 19:39
tsapiI just know a guy...20/06 19:39
pedagand;-)20/06 19:40
scriptdevilOk. I got those books. Thank you :)20/06 20:09
-!- mode/#epigram [+v dolio] by ChanServ20/06 21:19
--- Day changed Mon Jun 21 2010
-!- mode/#epigram [+v dolio] by ChanServ21/06 02:18
-!- mode/#epigram [+v dolio] by ChanServ21/06 05:19
-!- mode/#epigram [+v Saizan] by ChanServ21/06 06:03
-!- mode/#epigram [+v pigworker] by ChanServ21/06 07:31
-!- mode/#epigram [+v pigworker_] by ChanServ21/06 07:43
-!- pigworker_ is now known as pigworker21/06 07:43
-!- mode/#epigram [+v dolio] by ChanServ21/06 08:19
-!- mode/#epigram [+v codolio] by ChanServ21/06 09:18
pedagandmoleris, have you read the literature on Joyal's "analytic functors" and other "species"? 21/06 11:40
molerispedagand: I have21/06 11:50
pedagandha, great! Do you have a recommended reference to get into that? 21/06 11:51
pedaganddo you recommend reading this sort of stuff, btw? Or you had the feeling of "wasting your time"?21/06 11:52
pedagandas you might have noticed, we are writing a Containers for dummies, so I try to embrace the literature (smack-down may be a more appropriate word)21/06 11:55
molerisThe book "Combinatorial Species and Tree-like Structures" is a reasonable place to start, if you can find it on the shelves of a colleague21/06 12:07
molerisit's not a waste of time, but at the same time it's not the easiest thing to wrap your head around.21/06 12:08
pedagandok, thanks21/06 12:15
molerispedagand: Btw, you give me too much credit there are plenty of HF terms left to kill21/06 12:43
pedagandI did not checked actually, I trusted my misinterpretation of your commit message :-) 21/06 12:48
pedagandbut, well, greping for HF tells me that you eradicated most of them21/06 12:49
pedagandthere is one in Prop, the others are not really problematic. In particular, Problem is not connected to the system, FreeMonad is bound to disappear21/06 12:50
pedagandso, no, you deserve a round of applause :-)21/06 12:51
pedagandha, I missed OpDef and Elab: one HF each.21/06 12:52
molerisI see more than that21/06 12:55
molerisWhat about PropSimp.lhs?21/06 12:56
molerisAlso, as I discussed with pigworker there's a problem with Telescopes21/06 12:56
pedagandoops, missed that one too :-) Do like me, stare at your terminal very quickly, life is much better at high-glaring speed21/06 12:57
pedagandwhat's wrong with Hubble again? 21/06 12:58
molerisPropSimp, looked like a big change so I left it. Maybe I should have filed a issue in the bug tracker instead21/06 12:59
pedagandyep, you should: this World cup is too much of a pain, I'd rather fix bugs than watching it :-)21/06 13:02
agundrypedagand: I don't blame you...21/06 13:02
agundryPropSimp needs some thought, preferably by someone other than me21/06 13:03
molerisHeh, at least France's pain is almost over, I have a feeling England could conspire to make our hell last a few days longer21/06 13:03
molerisTelescopes are inescapably higher order at them moment21/06 13:05
molerisThere's a question about how much we really need them now, too... It is not a coincidence they were introduced soon after the HF constructor21/06 13:07
pedagandagundry, hehe. Btw, what kind of thought does PropSimp need?21/06 13:11
pedagandmoleris, yes, that's true21/06 13:12
agundrypedagand: it would be nice if the simplification rules were clearer and more obviously terminating21/06 13:13
pedagandha, ok, sure.21/06 13:14
agundryI also suspect it could be made a lot more efficient by removing all the discharges21/06 13:14
agundrymaybe this relates to figuring out how to remove the HFs21/06 13:14
molerisagundry: I should hope that would be the case21/06 13:14
molerisor at least that process can be made a lot cheaper21/06 13:15
agundryI've been experimenting with having problem simplification invoke elimination to substitute out equations21/06 13:16
agundrythis seems to work but it is incredibly slow21/06 13:16
-!- agundry is now known as agundry_away21/06 14:24
-!- agundry_away is now known as agundry21/06 15:25
+pigworkerafternoon all! (it's bloody early here, but that's jetlag)21/06 15:41
agundrypigworker: good afternoon, modulo timezones21/06 15:42
+pigworkerIf telescopes are just used for op types, we might just write those as terms, yeah? If they're all nice and toplevel, could you slurp them in from the parser?21/06 15:46
agundryHmm, you mean we could write operator types in Epigram and parse them at runtime?21/06 15:49
+pigworkermeanwhile, do we have a clear on-paper characterization of what PropSimp does?21/06 15:49
agundrynot really, that's part of the problem21/06 15:49
agundryI tried to find a nice way of writing down simplification rules, but didn't succeed21/06 15:50
+pigworkeragundry: parse at run time, or translate Epigram-with-Haskell-bits to Haskell in preprocessing21/06 15:50
+pigworkerFor PropSimp, I'd try a sequent calculus presentation.21/06 15:51
+pigworkertricky to demo in IRC21/06 15:52
agundrythat was roughly what I tried: there are a few scribblings in the PropSimp.lhs file 21/06 15:54
+pigworkerA, B, Delta |- P  <=>  A /\ B, Delta |- P21/06 15:54
agundrythe problem is finding a notation for the isomorphisms between proofs21/06 15:55
+pigworkerit's be a start to know what the rules are at the problem level, then refine them with realizers21/06 15:56
+pigworkerit'd21/06 15:56
agundrytrue21/06 15:56
agundryfor operator types, runtime parsing could work; we would either need to resurrect a parser for the evidence language, or be very careful that elaboration didn't use any of the operators we were defining21/06 15:57
+pigworkersomething of the sort; I'd rather we did it at compile-time, of course, but I realise that complicates the build process21/06 16:00
agundryI guess we could use quasi-quotation or similar trickery21/06 16:02
+pigworkeryeah; or maybe we can just improve the brevity of working with terms in Haskell21/06 16:03
agundrythat would be useful elsewhere as well, I suspect21/06 16:04
+pigworkera lot of the turgid wrappering can be hidden with typeclass tomfoolery21/06 16:05
+pigworkera challenge --- implement lambda calculus in Haskell with properly scoped de Bruijn terms; show how to implement variables as overloaded functions which figure out how to shift themselves from the type info21/06 16:07
+pigworkergotta get clean and face the day; more later21/06 16:10
agundryokay, bye for now21/06 16:12
pedagandmoleris, do you confirm that IDesc code is a completely canonical object? Or there is some operator in the picture that I'm not seeing?21/06 17:02
pedagandI guess, sumilike, although being applied late during distillation, still counts as an operator in the definition21/06 17:06
pedagand(I'm trying to stratify Desc or IDesc in my system. If I can remember my name at the end of the day, that will be a miracle)21/06 17:07
agundrypedagand: sumilike is only used for elaborating and distilling tags with arguments21/06 17:11
agundryso I don't see why it would cause you problems21/06 17:11
pedagandis that "distill es (IMU l _I s i :>: CON (PAIR t x))" what you call "tags with arguments"?21/06 17:12
pedagandjust to check21/06 17:13
agundryyes21/06 17:14
agundrythe idea is that t will be distilled to a tag (an element of UId) applied to the list that x distills to21/06 17:17
pedagandhehe, goodo21/06 17:18
pedagandthanks21/06 17:20
agundryno problem21/06 17:21
-!- mode/#epigram [+v Saizan] by ChanServ21/06 19:26
-!- mode/#epigram [+v Saizan_] by ChanServ21/06 22:34
-!- Saizan_ is now known as Saizan21/06 22:34
--- Day changed Tue Jun 22 2010
-!- mode/#epigram [+v Saizan] by ChanServ22/06 01:10
-!- mode/#epigram [+v Saizan] by ChanServ22/06 05:05
-!- mode/#epigram [+v Saizan] by ChanServ22/06 13:24
-!- mode/#epigram [+v soupdragon] by ChanServ22/06 17:58
-!- mode/#epigram [+v Saizan_] by ChanServ22/06 18:26
-!- Saizan_ is now known as Saizan22/06 18:26
--- Day changed Wed Jun 23 2010
pedagandedwinb, so England qualified finally?23/06 17:08
+edwinbyes. They were rubbish though.23/06 17:10
pedagandha, well. I can hardly blame any team for being rubbish, my nationality prevents that :-)23/06 17:13
+edwinbwell. indeed.23/06 17:15
+edwinbit doesn't stop the Scots ;)23/06 17:15
pedagand:-)23/06 17:17
-!- mode/#epigram [+v Saizan] by ChanServ23/06 19:36
--- Day changed Thu Jun 24 2010
-!- mode/#epigram [+v Saizan] by ChanServ24/06 09:29
pizza_building cabal's 'she' fails for me; anyone else have this problem?24/06 19:06
ccasinjust tried and got a compiler panic, though I'm running an ancient version of ghc (6.10.3)24/06 19:08
pizza_i'm running ghc-6.8.2, which is the latest mainstream ubuntu package, apparently24/06 19:09
ccasinconsidering that she is all about fancy type hacks, a new version is probably required24/06 19:09
ccasinalso I just checked and ghc 6.12.1 is in apt on ubuntu lucid24/06 19:10
pizza_hmm i'll have to figure out how to get that24/06 19:11
ccasinubuntu's bad for this sort of thing though - ghc changes fast and ubuntu keeps packages at the same version for the duration of a release24/06 19:12
ccasinbetter off just downloading and installing ghc binaries directly24/06 19:12
pizza_ok24/06 19:15
ccasinon 6.12.1 she seems to build fine - just tried on a different computer24/06 19:15
pizza_thanks for the info24/06 19:17
pizza_does epigram aim to eventual self-hosting?24/06 19:18
pizza_hmm building ghc from source requires a new ghc binary than i already have. curiouser and curiouser24/06 19:21
ccasinit also takes hours - binaries highly recommended24/06 19:22
pizza_the main challenge as a haskell programmer i can tell so far seems to be setting up the environment :/24/06 19:25
ccasinit's usually pretty painless!  Though the current transition to the "haskell platform" may be confusing things24/06 19:28
ccasinyour best bet is probably just installing the 6.12.1 binary and then building the platform from source24/06 19:30
ccasinhttp://hackage.haskell.org/platform/linux.html24/06 19:30
pizza_thanks24/06 19:41
pizza_hmmm, building from source breaks. time to try 6.12 binary...24/06 19:50
pizza_6.12.1 binaries installed; now to build haskellplatform which should replace my old cabal and friends...24/06 20:10
pizza_Registering she-0.1... \o/24/06 20:22
pizza_pizza@ubuntu:~/src/Pig09/src$ make dep24/06 20:30
pizza_ghc: could not execute: she24/06 20:30
ccasinwhere did she get installed and is it on your path?24/06 20:31
ccasin.cabal/bin is a common place24/06 20:31
pizza_ah24/06 20:31
pizza_there we go24/06 20:31
-!- mode/#epigram [+v Saizan] by ChanServ24/06 20:35
pizza_im doing the "two plus two" example; what does the "^1" in Programming: < plus^1 m n : Nat > mean?24/06 20:40
pedagandI'm always a bit afraid when I see someone compiling Epigram. The source code is already enough of a misery. I hope you're not expecting it to work better when compiled :-)24/06 20:40
pizza_ha :)24/06 20:41
pedagandfor example, the following are equivalent: \x -> \y -> x   and \ x -> \ x -> x^124/06 20:41
pedagandthe "^i" gives you the De Bruijn index when there is shadowing in the context24/06 20:41
pedagandin this case, this comes from the way "plus" as a labelled type has been defined in the proof state.24/06 20:42
pedagandput otherwise, you're observing an implementation artifact24/06 20:43
pedagandsorry about that. I warned you: it's the bleeding edge as in "gosh, it cuts!" :-)24/06 20:44
+SaizanVec.Ind from the demo seems to be even sharper! :)24/06 20:46
pedagandha, don't tell me about this demo. If it were just me, I would have called it "public humiliation session"24/06 20:47
pedagandimagine, we struggled half an hour to define "+"24/06 20:47
pizza_why is that humiliating?24/06 20:47
pedagandI ruined all my chances to get by with the good looking girl which got attracted by our emacs buffer :-)24/06 20:48
pizza_lol24/06 20:48
+Saizanah, you didn't have the script ready?24/06 20:48
pedagandpizza_, I'm kidding ;-)24/06 20:48
pedagandSaizan, have seen the part where we define plus in the script? Conor and Adam wanted to make the point that programming is "interactive"24/06 20:49
pedagandso, if you follow the intermediary steps and explain this interactive elaboration 1/ the girl falls asleep; 2/ she reckon that half an hour ago we were already defining plus24/06 20:50
pedagandand the Java guy next to you suddenly looks like a promising mate24/06 20:50
pedaganddamnit! :-)24/06 20:50
+Saizanahahahah :D24/06 20:50
+Saizani can understand why there's no explanation for vhead then :)24/06 20:53
pedagandthe funny bit was a person patiently listening to this "+" definition and then asking "ok, mmh, could you show an application you developed with that language?"24/06 21:01
pedagandI suddenly remembered that many languages had been invented for the sole purpose of building applications. Gosh :-)24/06 21:01
ccasin:)24/06 21:03
ccasinwas this a demo at the oregon summer school?24/06 21:03
pedagandno, a local event here in Edinburgh24/06 21:03
ccasinah24/06 21:04
pedagandlong ago, Conor expressed the desire to do his lecture with Epigram24/06 21:05
ccasinI saw conor is giving dependently typed programming lecture there - are they in epigram?24/06 21:05
pedagandbut reality caught up :-)24/06 21:05
ccasinalas24/06 21:05
ccasinso much cool stuff there this year24/06 21:05
pedagandI believe his lecture is based on some induction recursion madness. So, Epigram is out of the game anyway24/06 21:05
pedagand(that's the politically correct reason, anyway)24/06 21:06
ccasin:)24/06 21:06
ccasinis he using agda?24/06 21:07
pedagandwell, I don't know, he alluded that his lectures would be based on his recent "type theory in itself" paper24/06 21:08
pedagandbut he wrote the lecture in the plane to Oregon apparently, so I can't say for sure24/06 21:08
pizza_Epitome.pdf S1.2 "This is all very tenative."24/06 22:19
pedagandis it a quote from the text? I cannot find it. Or it's your opinion about it? :-)24/06 22:40
pizza_copy-and-pasted from the pdf24/06 22:42
pedagandHu24/06 22:42
pizza_bottom of p.724/06 22:42
pedagandI recompile the pdf, might take a few hours24/06 22:43
pedagandha, got it24/06 22:44
pedagandthe syntax... I suspect that your friend to get into this maze is to look at Syntax.pig in the test directory24/06 22:47
pedagandif you haven't already24/06 22:47
pizza_i did, it was a bit overwhelming24/06 22:47
pizza_hard for me as a programmer to differentiate between built-in stuff and stuff being defined24/06 22:48
pedagandwell, this syntax is overwhelming *by design*, anyway. 24/06 22:48
pizza_:)24/06 22:48
pedagandthere is not many built-in stuffs, that's one of the (many) craziness of the language.24/06 22:49
pedagandare you familiar with Agda for instance?24/06 22:49
pedagandor Coq maybe?24/06 22:50
pedagandI wrote Syntax.pig to be some kind of Rosetta stone for someone coming from these languages. (I agree it could be improved, tho)24/06 22:50
pizza_I've played a bit with Isabelle/HOL; I am more of a programmer exploring functional languages and learning concepts at the moment than someone with a serious FP background, so dont mind me24/06 22:51
pedagandwell, I'm afraid Epigram is not the ideal tool for learning: Agda is much more polished and will put less silly barriers to entry than we do have24/06 22:53
pizza_yup ok24/06 22:55
pedagandbut don't misread me: I'm not bothered to answer questions :-)24/06 22:55
pizza_you have been most kind and helpful24/06 22:57
pedagandyou're welcome24/06 22:57
--- Day changed Fri Jun 25 2010
-!- mode/#epigram [+v Saizan] by ChanServ25/06 01:55
-!- mode/#epigram [+v Saizan] by ChanServ25/06 02:00
-!- mode/#epigram [+v soupdragon] by ChanServ25/06 18:33
--- Day changed Sat Jun 26 2010
tsapisometimes a deadline extension is the last thing you want...26/06 00:30
pedagandwhat you need is a good spam filter then :-)26/06 00:48
pedagandso that you don't know that there has been an extension and you just ship this damned paper 26/06 00:48
pedagandwhich workshop is it?26/06 00:49
tsapihttp://www.cs.unibo.it/~asperti/mscs26/06 00:52
pedagandwell, good luck with that! it's about a comonadic story?26/06 00:55
tsapirelative monads in agda26/06 00:55
tsapithanks :)26/06 00:56
pedagandho, interesting. Let us know when you've a draft, it could accidentally on reddit :-)26/06 00:57
tsapiok :)26/06 01:00
-!- mode/#epigram [+v Saizan] by ChanServ26/06 02:13
-!- mode/#epigram [+v Saizan] by ChanServ26/06 13:24
--- Day changed Sun Jun 27 2010
-!- mode/#epigram [+v Saizan] by ChanServ27/06 14:10
-!- mode/#epigram [+v Saizan] by ChanServ27/06 15:27
-!- mode/#epigram [+v Saizan] by ChanServ27/06 16:26
-!- mode/#epigram [+v Saizan] by ChanServ27/06 17:12
pedagandtsapi, do you have a definition of relative monads in Agda, by any chance? 27/06 19:10
pedagandif not, no problem, it's just me being lazy. I would need one in Epigram27/06 19:10
tsapipedagand: I do it's a question of where to put it27/06 19:31
tsapithe repo isn't online27/06 19:31
tsapipedagand: I'll mail you a tarball of the repo (including the paper). I plan to put a draft and the formalisation online later in the week27/06 19:32
pedagandok, thanks27/06 19:33
pedagandbut if you're busy with other things, don't le me distract you, that's not urgent27/06 19:35
pedagands/le/let/27/06 19:36
tsapinot busy, spent the cycling27/06 19:43
tsapispent the day cycling27/06 19:43
+edwinbthat sounds quite busy27/06 19:44
pedagandtsapi, got your mail, thanks27/06 21:23
--- Day changed Mon Jun 28 2010
-!- mode/#epigram [+v Saizan] by ChanServ28/06 03:16
-!- mode/#epigram [+v Saizan] by ChanServ28/06 05:21
-!- mode/#epigram [+v Saizan] by ChanServ28/06 05:45
-!- mode/#epigram [+v Saizan] by ChanServ28/06 09:18
-!- mode/#epigram [+v Saizan] by ChanServ28/06 19:05
-!- mode/#epigram [+v soupdragon] by ChanServ28/06 22:43
--- Day changed Tue Jun 29 2010
-!- mode/#epigram [+v dolio] by ChanServ29/06 00:45
-!- mode/#epigram [+v dolio] by ChanServ29/06 01:15
-!- shapr[ is now known as shapr29/06 02:34
-!- mode/#epigram [+v Saizan] by ChanServ29/06 05:12
-!- mode/#epigram [+v dolio] by ChanServ29/06 06:23
-!- mode/#epigram [+v Saizan] by ChanServ29/06 07:23
-!- mode/#epigram [+v dolio] by ChanServ29/06 08:19
-!- mode/#epigram [+v Saizan] by ChanServ29/06 08:38
-!- mode/#epigram [+v Saizan] by ChanServ29/06 09:44
-!- mode/#epigram [+v dolio] by ChanServ29/06 10:19
-!- mode/#epigram [+v Saizan] by ChanServ29/06 10:47
-!- mode/#epigram [+v Saizan] by ChanServ29/06 11:19
-!- mode/#epigram [+v pigworker] by ChanServ29/06 13:37
-!- mode/#epigram [+v soupdragon] by ChanServ29/06 15:46
-!- mode/#epigram [+v dolio] by ChanServ29/06 17:22
-!- mode/#epigram [+v pigworker] by ChanServ29/06 18:14
-!- mode/#epigram [+v dolio] by ChanServ29/06 19:19
-!- mode/#epigram [+v dolio] by ChanServ29/06 20:23
+doliopigworker: So, I heard you already know how to turn induction-induction into just induction (or, inductive families).29/06 20:39
+dolioAlthough, I'm not super convinced the translation someone gave me covers everything.29/06 20:43
+pigworkerThere's something like a preterms and goodness-judgments translation (which relies on proof-irrelevance for goodness).29/06 21:03
+pigworkerCan't say I've defined it formally, though.29/06 21:04
-!- mode/#epigram [+v codolio] by ChanServ29/06 21:22
-!- codolio is now known as dolio29/06 21:36
+doliopigworker: That kind of surprised me, because I tend to think of induction-recursion as allowing you to write bigger types (so to speak) than you'd otherwise be able to. So I kind of expected induction-induction to be similar.29/06 21:44
+dolioWhereas that translation looks like it's just a way of carving out parts of things you could write anyway.29/06 21:45
+pigworkerI-I can't do "big" like I-R can, it's true.29/06 22:04
+pigworkerI wonder, if we had intersections as well as products, could we allow big intersections for constructor arguments, given that the data will not store the large things?29/06 22:08
+dolioYeah, that's kind of been on my mind, along with the erasure stuff.29/06 22:08
+dolioI seem to recall hearing that one of the ideas behind parametricity is "when is it okay to be impredicative?"29/06 22:09
+pigworkerIt might be ok to have data Foo : Set where foo : /\ X : Set -> Foo, for a silly example.29/06 22:10
+dolioBut, I've been lazily avoiding working on my implementation of the EPTS (and associated) stuff.29/06 22:11
+pigworkerBut if intersection erases only at run-time, that might just affect which phases one can screw up at.29/06 22:11
+dolioSo I can't, say, put together a type system where forall is impredicative, but pi isn't, and see if Hurkens' paradox still goes through.29/06 22:12
+pigworkerLots of variables to tweak there.29/06 22:13
+pigworkerI wonder if Alexandre Miquel already knows what works.29/06 22:15
-!- mode/#epigram [+v dolio] by ChanServ29/06 22:23
-!- mode/#epigram [+v pigworker] by ChanServ29/06 23:18
--- Day changed Wed Jun 30 2010
-!- mode/#epigram [+v dolio] by ChanServ30/06 00:22
-!- mode/#epigram [+v dolio] by ChanServ30/06 01:55
-!- mode/#epigram [+v dolio] by ChanServ30/06 02:22
-!- mode/#epigram [+v pigworker] by ChanServ30/06 03:14
-!- mode/#epigram [+v dolio] by ChanServ30/06 05:19
-!- mode/#epigram [+v Saizan] by ChanServ30/06 05:39
-!- mode/#epigram [+v dolio] by ChanServ30/06 06:19
-!- mode/#epigram [+v Saizan] by ChanServ30/06 09:10
-!- mode/#epigram [+v dolio] by ChanServ30/06 10:19
-!- mode/#epigram [+v pigworker] by ChanServ30/06 10:32
-!- mode/#epigram [+v Saizan] by ChanServ30/06 11:37
+pigworkerpedagand: hi, how are you?30/06 12:05
+pigworkerIt's time I went to school.30/06 12:14
-!- mode/#epigram [+v codolio] by ChanServ30/06 13:21
-!- mode/#epigram [+v dolio] by ChanServ30/06 14:22
-!- mode/#epigram [+v pigworker] by ChanServ30/06 19:00
-!- mode/#epigram [+v dolio] by ChanServ30/06 21:23
-!- mode/#epigram [+v dolio] by ChanServ30/06 22:19

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