Laney moleris Laney --- 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 secs 03/06 14:33 evening 03/06 14:33 Laney: How are the logs coming along? 03/06 14:36 all good boss: http://epigram.orangesquash.org.uk/2010/June.log.html 03/06 14:38 Another day, another strictness bug to squash 03/06 14:52 moleris, I'm curious: what do you do that triggers them so easily? is it something in the Data tactics? 03/06 15:10 pedagand: Using induction or iinduction specialised to EnumD, DescD, IDescD 03/06 15:36 in order to do some generic programming basically 03/06 15:37 this time it was a canTy rule from Enum.lhs 03/06 15:38 I was trying to write tabulate, the inverse of switch 03/06 15:38 moleris, ok 03/06 17:19 moleris: if you can make sense of the new OpTree machinery, you can write operators without strictness bugs 03/06 20:26 Laney: thanks very much for the lovely logging 03/06 20:27 * edwinb waves at the people reading the logs 03/06 20:39 you screamt? 03/06 23:23 look there's 11 people here 03/06 23:24 wtf! 03/06 23:24 That's awesome! 03/06 23:24 pigworker: If you'll register your irc nick, I'll add you to the ops list 03/06 23:25 Too long since I've used chanserv, I'm trying to figure out how templates work. 03/06 23:27 shapr: so you continue the tradition of founding irc channels for functional languages?:) 03/06 23:27 shapr: I'm kinda new to IRC; where do I need to poke something? 03/06 23:27 I started #concatenative too :-) 03/06 23:28 what 03/06 23:28 pigworker: /msg nickserv help register 03/06 23:28 pigworker: That'll give you the directions for registering your account. 03/06 23:28 I started a bunch of channels, but only a few of them have gone places. 03/06 23:29 * shapr shrugs 03/06 23:29 These days I do more meatspace organizing, my time is going into being a makerspace cofounder. 03/06 23:29 Me and ybit 03/06 23:29 shapr: done; thanks for that 03/06 23:31 Ok, 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 ChanServ 03/06 23:33 -!- shapr changed the topic of #epigram to: http://www.e-pig.org/ | Epigram - Programming Language with Dependent Types 03/06 23:34 pigworker: visited #haskell already? 03/06 23:47 lurked briefly, but it whizzes by so fast! 03/06 23:48 I can't keep up with #haskell... 03/06 23:49 on a completely unrelated topic, was code golf invented because of ACM 2-column format? 03/06 23:52 heh 03/06 23:54 ghc is irritating me by producing inexplicably fast code that epic can't get near 03/06 23:59 --- Day changed Fri Jun 04 2010 I think it might be being much cleverer at memory allocation 04/06 00:01 edwinb, 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 it's more what it's not doing that I'd like to know, than what it is doing... 04/06 00:14 you could pinpoint the source of the performance loss I think 04/06 00:14 are you doing lot of function calls? or indirect function calls? 04/06 00:15 it's spending 30% of its time in GC related functions 04/06 00:15 in my old days, 30% of GC was good 04/06 00:16 yeah, but ghc does better and we can't have that ;) 04/06 00:17 well, GHC has an upper-class GC, at the same time :-) 04/06 00:17 better GC would help, but I suspect knowing when not to allocate at all would be good 04/06 00:18 i.e. when it's okay to use the stack rather than heap, or when it's okay to reuse something 04/06 00:18 I've tried a really simple allocator which just moves a pointer along and never frees 04/06 00:18 -!- mode/#epigram [+v dolio] by ChanServ 04/06 00:18 which of course makes things much faster, at least for a short time... 04/06 00:18 I see 04/06 00:19 can't you benchmark your stuff without GC and GHC without GC? 04/06 00:21 I think I'd need to poke about GHC internals a bit more to do that 04/06 00:22 because, it'll always be unfair to compare your boehm-ian GC with any other clever stuff 04/06 00:22 but I may have to do that anyway if I want to know what's going on 04/06 00:22 if there's clever stuff that lives happily alongside boehm then I want it! 04/06 00:22 mind, this isn't actually that important. I think epic is fast enough for most purposes at the moment. 04/06 00:22 It just annoys me ;) 04/06 00:23 or you could steal GHC's RTS? assuming the evaluation models are compatible enough.. 04/06 00:26 Saizan, you mean, spitting some Core code and sending that to GHC? 04/06 00:28 That might be tough, since I think GHC core is still typed. 04/06 00:29 that's the biggest problem with it, yes 04/06 00:30 pedagand: it was more like stealing the RTS (which i think is in C) and link it with code generated separately by epic 04/06 00:30 I tried it a while back, and it sort of worked, but the optimiser broke things 04/06 00:30 I'd prefer to know why it works so well though, rather than just stealing it 04/06 00:31 although I'm not averse to stealing it ;) 04/06 00:31 What kind of code are you comparing? 04/06 00:31 some mercury guy is already doing that, iiuc 04/06 00:31 this is a contrived program which tree sorts some integers 04/06 00:32 so lots of cosntructing things which don't live very long 04/06 00:33 I see. 04/06 00:33 ah, the case a generational gc is designed for 04/06 00:34 Not just that, a copying collector. How does Boehm work? 04/06 00:34 Boehn is mark/sweep 04/06 00:34 It is possible that it is simply because GHC's GC is better suited to it 04/06 00:35 and I'm just getting horribly fragmented memory 04/06 00:35 maybe this is where I need pedagand's profiling skills... 04/06 00:35 ha, see, I've skillz! I call my mother right away, thanks Edwin! :-) 04/06 00:36 hehe 04/06 00:37 -!- mode/#epigram [+v dolio] by ChanServ 04/06 02:18 -!- koninkje_away is now known as koninkje 04/06 03:21 -!- koninkje is now known as koninkje_away 04/06 06:45 -!- koninkje_away is now known as koninkje 04/06 06:58 -!- koninkje is now known as koninkje_away 04/06 07:10 -!- mode/#epigram [+v dolio] by ChanServ 04/06 08:22 -!- koninkje_away is now known as koninkje 04/06 08:58 -!- mode/#epigram [+v pigworker] by ChanServ 04/06 09:20 -!- mode/#epigram [+v dolio] by ChanServ 04/06 09:21 pigworker: 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 good plan: it's a bum steer 04/06 10:20 that patsy 04/06 10:20 my 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 arguably, that's a job for newtype, though 04/06 10:23 prevent matching by hiding the constructor... 04/06 10:23 The lazy vs Strict distinction does seem like it would be useful 04/06 10:24 in other news I've almost written the rec gadget in epigram 04/06 10:26 bonzer 04/06 10:54 anyhow, time to occupy a different spot in the Glasgow skyline... 04/06 10:55 -!- koninkje is now known as koninkje_away 04/06 11:26 -!- mode/#epigram [+v dolio] by ChanServ 04/06 14:18 -!- mode/#epigram [+v pigworker] by ChanServ 04/06 14:49 -!- mode/#epigram [+v pigworker] by ChanServ 04/06 14:51 -!- mode/#epigram [+v dolio] by ChanServ 04/06 15:21 -!- mode/#epigram [+v Saizan] by ChanServ 04/06 16:50 -!- mode/#epigram [+v dolio] by ChanServ 04/06 18:22 * soupdragon feels like I missed out on something 04/06 18:24 someone do /topic http://www.e-pig.org/ | Epigram - Programming Language with Dependent Types  | logs: http://epigram.orangesquash.org.uk/ 04/06 18:25 don't seem to have privs. 04/06 18:25 * soupdragon tries to hit the chandeliers and fails 04/06 18:27 I gave it a whirl, but I don't see any effect. 04/06 18:28 guess one has to be +o to set topic 04/06 18:28 didn't used to be like that 04/06 18:28 I'm clueless about these IRC mechanisms. 04/06 18:29 shapr? 04/06 18:29 http://www.spacex.com/webcast.php 10 seconds till liftoff 04/06 18:30 engine shutdown just after ignition nvm -_- 04/06 18:30 I'm having too much fun watching my computer grind to a standstill trying to check a proof... 04/06 18:32 grinding to a standstill sounds about right 04/06 18:32 ghc about 30% CPU, emacs totally locked up, the sun blazing down 04/06 18:33 that's the life! 04/06 18:34 is this the proof for the linear containers stuff? 04/06 18:34 if only... I'm not convinced I've got the definitions right for that yet 04/06 18:34 crikey, something happened! 04/06 18:35 I'm trying to prove that the recursively defined equality on Nat is transitive... 04/06 18:35 in epigram ? 04/06 18:36 Yow! 04/06 18:36 hey shapr :) 04/06 18:36 hiya! 04/06 18:36 I want to set the topic 04/06 18:36 since it's polite (policy) to put the place for the logs in there 04/06 18:36 soupdragon: no, in a type theory I implemented in Agda 04/06 18:36 awright 04/06 18:36 I wonder when should I get the courage to try coding basic category theory into the pig? 04/06 18:36 there 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 the epigram engines cannae take it, but it's always interesting to see where the failure kicks in 04/06 18:38 hehe 04/06 18:39 will you guys be doing the ICFPc in Epigram? 04/06 18:40 It's really amazing watching Agda behave like an interactive assistant for an encoded theory 04/06 18:40 It's a lot of fun to see the type inference/term inference thing switching over 04/06 18:40 shapr: not unless the competition is to implement Epigram 04/06 18:40 hah 04/06 18:40 I've never done ICFP.. I just cheer on roconnor 04/06 18:41 well I wrote some lisp macros for a team once 04/06 18:42 I'll probably spend most of that time over the Atlantic, anyhow 04/06 18:43 Coming to the USA? 04/06 18:53 yeah, teaching at the school in Eugene, OR 04/06 19:02 nifty 04/06 19:06 trouble is, these days, "dependently typed programming" could really touch on a lot of material; editorial choice is required 04/06 19:09 I wonder if Agda would speed up if it did edwinb optimization on open terms. 04/06 19:15 Epigram gets to really not store index info in data if it comes from the type. 04/06 19:16 -!- mode/#epigram [+v dolio] by ChanServ 04/06 19:21 http://www.spacex.com/webcast.php 04/06 19:45 this time it's going 04/06 19:45 ghc has stopped and emacs is going (either my term has checked or agda has dies) 04/06 19:52 not a good sign 04/06 19:53 it normally works a bit when it's colouring in 04/06 19:54 but that was death 04/06 19:55 ok, it's time I went home 04/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 ty shapr 04/06 20:00 I suspect the answer to pigworker's question is "Yes, but not as much as it should." 04/06 21:31 as I understand it a lot of Agda's slowness is caused by loss of sharing 04/06 21:32 although I may be out of date 04/06 21:32 it'd be nice if there was some intro for wannabe agda hackers, the 200 modules are a bit intimidating 04/06 21:35 idk 04/06 21:38 newbies can learn Coq 04/06 21:38 I think Agda (at this point) is for reseachy people 04/06 21:38 still ironing out the details and exploring and such 04/06 21:39 once they fix the theory that would be the time to start writing manuals and so on 04/06 21:39 by "agda hackers" i meant people that might like to work on the implementation 04/06 21:39 oh sorry 04/06 21:39 yeah I totally couldn't get into the agda source code at all 04/06 21:39 a lot of weird stuff going on in there 04/06 21:39 -!- mode/#epigram [+v Saizan] by ChanServ 04/06 22:13 -!- mode/#epigram [+v Saizan] by ChanServ 04/06 22:23 -!- mode/#epigram [+v pigworker] by ChanServ 04/06 23:42 --- Day changed Sat Jun 05 2010 Fetching a hashed repository would be faster.  Perhaps you could persuade 05/06 00:30 the maintainer to run darcs optimize --upgrade with darcs 2.4.0 or higher? 05/06 00:30 05/06 00:30 soupdragon, please do harass pigworker when he is back :-) 05/06 00:35 okay ill try :) 05/06 00:35 he and his mac G4 are our only to keep that obsolete stuff 05/06 00:35 everything 'looks alright' except [DISABLED] Fin.pig is disabled and some vec thing 05/06 00:35 things* 05/06 00:35 indeed, these are disabled, no worry 05/06 00:36 it's so cool how there's all this agda stuff along with epigram :) 05/06 00:37 and on Monday, there will be some Coq stuff as well probably :) 05/06 00:38 ooh what's happening? 05/06 00:39 I saw that old OTT.v thing 05/06 00:39 but that was a while back 05/06 00:39 reviewers 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 I've made yet another model of Desc in Coq, nothing really exciting 05/06 00:40 The (I)Desc stuff in Agda is certainly more convincing than "it doesn't seem to loop anymore". :) 05/06 00:41 Although I suppose the looping stuff might not quite be modeled in Agda. 05/06 00:41 apparently, not everybody trusts the "set polymorphism" option of Agda :-) 05/06 00:42 You mean, the stuff with Level and Set i? 05/06 00:43 yes 05/06 00:43 Well, it's hard to blame them for that. 05/06 00:44 indeed 05/06 00:45 I've tried a couple times making something inductive-recursive work, but haven't gotten anywhere yet. 05/06 00:51 to "work" toward which end? Set polymorphism? 05/06 00:53 Making a universe (or hierarchy) with something desc-like in it. 05/06 00:53 if 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 level 05/06 00:54 that's probably unhealthy but I thought we could put the code at some level Omega (transfinite) and do the descent from there 05/06 00:55 but that's rather contrived... 05/06 00:56 Well, 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 Which is disappointing. 05/06 00:58 Have you read "The Gentle Art of Levitation"? 05/06 01:00 the codes for Desc should live one level higher than the corresponding Mu 05/06 01:00 I guess you did that right, but just checking 05/06 01:00 It seems to be Conor's shot at a self-describing universe 05/06 01:00 I'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 :-D 05/06 01:01 :) 05/06 01:01 napping, worse than that... I was part of the gang who wrote it :-) 05/06 01:01 and I first heard about this stuff from Peter Morris' thesis 05/06 01:02 indeed, that's his baby 05/06 01:03 Anyhow, 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 Like "we can replace Desc by a Desc description of Desc in a certain way". 05/06 01:06 The Agda is bootstrapped by an Agda type Desc. 05/06 01:07 it seems in the end you've to assume something named Desc exists to be able to typecheck the definition of Desc 05/06 01:08 that's entirely true 05/06 01:09 the whole collapsing of Desc onto itself is due to switchD 05/06 01:10 without resorting to an embedded model of a type-theory with Desc inside Agda, it wasn't possible to model switchD 05/06 01:11 I reckon that it's what you've been trying to get to, right? 05/06 01:12 No, 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 Which would be analogous to the Desc type in Agda, I think. Or the tower of descs using universe polymorphism. 05/06 01:14 ha, ok 05/06 01:16 -!- mode/#epigram [+v dolio] by ChanServ 05/06 01:21 -!- mode/#epigram [+v dolio] by ChanServ 05/06 04:21 -!- mode/#epigram [+v dolio] by ChanServ 05/06 06:18 -!- mode/#epigram [+v dolio] by ChanServ 05/06 07:21 -!- mode/#epigram [+v dolio] by ChanServ 05/06 08:21 -!- mode/#epigram [+v dolio] by ChanServ 05/06 09:21 -!- mode/#epigram [+v pigworker] by ChanServ 05/06 09:51 -!- mode/#epigram [+v dolio] by ChanServ 05/06 11:18 -!- mode/#epigram [+v pigworker_] by ChanServ 05/06 11:30 -!- pigworker_ is now known as pigworker 05/06 11:31 hello 05/06 11:52 hi, james? what are you doing on 9grid.fr?? You're a plan9 user??? 05/06 11:55 a closet one :) 05/06 11:57 haha 05/06 11:58 is this channel logged by the way? 05/06 11:58 yep, as written in the status bar up there ^ 05/06 11:58 I know Laney keeps logs for #agda 05/06 11:59 http://epigram.orangesquash.org.uk/ 05/06 11:59 http://epigram.orangesquash.org.uk/ 05/06 11:59 i see 05/06 11:59 -!- mode/#epigram [+v dolio] by ChanServ 05/06 15:21 -!- mode/#epigram [+v Saizan] by ChanServ 05/06 16:04 -!- mode/#epigram [+v dolio] by ChanServ 05/06 16:21 -!- mode/#epigram [+v codolio] by ChanServ 05/06 18:21 -!- mode/#epigram [+v dolio] by ChanServ 05/06 19:21 (./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 cool! 05/06 22:08 I guess the green equality shouldn't really be used, it's an implementation detail 05/06 22:08 and refl1 and refl2 are identical right? 05/06 22:10 I 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 ha yes, refl1 and refl2 are the same : I've removed something I tried 05/06 22:20 (I've removed refl2) 05/06 22:21 actually, you're right: to get the green, you'd write a blue and Out it (with %) 05/06 22:29 pedagand: Good stuff 05/06 22:49 thanks :-) 05/06 22:50 While 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 syntax 05/06 22:50 I think (<->) was suggested at some point -- not that I'm particularly attached to it 05/06 22:51 Also, using con to split sigmas is getting very old (does it also eliminate still Mu as well?) 05/06 22:52 what would you use to split a sigma? 05/06 22:53 matching pairs on the left of lambdas would be really nice :) 05/06 22:54 i.e. having |\ [ x , y ] -> t| instead of |con \ x y -> t| 05/06 22:55 not sure how difficult that would be in the current setup though 05/06 22:55 ha, yes, so: con for splitting sigma is old *but* implemented :-) 05/06 22:58 OK, but con is still misleading 05/06 22:58 I 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 jobs 05/06 22:59 I vote for adding a keyword split' 05/06 23:00 I entirely agree with you... 05/06 23:01 yep, we can do that 05/06 23:02 but, assuming we can implement "\ [x , y] -> ...", would we need "split" as well? 05/06 23:05 hum, yes, split ? might still be useful I guess 05/06 23:05 it would still be useful, afterall anonymous functions aren't the end of the story 05/06 23:07 why not go for the fancy lambda? you only need it in the display syntax, which is now something else 05/06 23:10 -!- mode/#epigram [+v dolio] by ChanServ 05/06 23:21 you mean: we should just do fancy lambda, or both split and fancy lambda? I think both are just display artifacts 05/06 23:25 split's a no brainer, so warm up with that; then try fancy lambda? 05/06 23:33 on the earlier topic, I'm beginning to think green equality isn't worth it 05/06 23:35 ok 05/06 23:37 we could just make the con constructor for blue equality do one step of expansion, with blue equality for the bits 05/06 23:37 we don't really make use of the way green equality computes lots of steps at once 05/06 23:38 I turn these into feature requests, sir 05/06 23:41 pedagand: This is what I was talking about yesterday: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25931#a25931 05/06 23:43 as 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 :-) 05/06 23:43 Agda doesn't like it because Fix D ~ Fix D' -> .... 05/06 23:44 dolio, ha, yes, thanks for that discussion btw 05/06 23:44 Even though it's probably okay. 05/06 23:44 Due to structural decrease of the descriptions (not that I've proved that or anything). 05/06 23:45 have you tried to manually unfold Fix? 05/06 23:45 I'm not sure what you mean by that. 05/06 23:46 I thought about not making Fix a datatype, but then I realized I didn't really know of any other possibilities. 05/06 23:47 I 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 But that isn't really correct, because then U contains datatypes over Set, not just over other types in U. 05/06 23:49 "Meta" is a module of yours, right? Or it's in the stdlib? 05/06 23:54 Oh. Yeah. I think the only thing I'm using it for in there is top and sigma. 05/06 23:54 I hpaste what I meant by unfolding, but it's ugly, in Coq, and I'm not sure it's your problem here 05/06 23:55 here you go: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25932#a25932 05/06 23:57 intuitively, you bring [| . |] into Fix 05/06 23:58 Oh, so you give Fix several constructors mirroring Desc. 05/06 23:58 Hmm... 05/06 23:58 so, here it's particularly disgusting because we use the impredicativity of Prop to avoid size issues 05/06 23:58 Heh. 05/06 23:59 that's a Matthes-style encoding 05/06 23:59 --- Day changed Sun Jun 06 2010 are you sure? it's late; I don't see where impredicativity kicks in (but maybe I'm blind) 06/06 00:02 hem. 06/06 00:02 It's possible Venanzio Capretta has already invented this trick; we are always inventing each other's tricks. 06/06 00:03 the fact is MuU is in Set right, not Set1 06/06 00:04 s/Set1/Type/ 06/06 00:05 we abuse Prop with the Is_true, getting the proof to run e.g. SigmaHd and SigmaTl 06/06 00:05 well, I should try writing it directly and see if the size change 06/06 00:06 but Is_true takes a tiny wee Bool to a tiny wee Prop; do we ever make bloody big Props? 06/06 00:08 what is a big Prop? There is no hierarchy of Props, isn't it? 06/06 00:10 I mean, there is no hierarchy of Prop, period. :-) 06/06 00:10 yes, 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 here you go: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25932#a25933 06/06 00:17 I mean a Prop which is made by equating things in big sets 06/06 00:18 dolio, 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 downward 06/06 00:18 pigworker, mmh ok. So, you don't call that trick "abusing impredicativity of Prop"? 06/06 00:21 not if it's just reflecting Bool 06/06 00:21 pedagand: Is it just me, or does pi look exactl like sigma? 06/06 00:22 Also, I assume instead of Fix D you use MuU D D? 06/06 00:23 This appears to actually work in Agda. 06/06 00:23 dolio, hehe, no it's not just you, I'm seeing this too :-) 06/06 00:24 pigworker, 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 dolio, yes, MuU is Fix in your case 06/06 00:26 Oh, I spoke too soon. I still had --no-positivity-check on. 06/06 00:26 This also fails. 06/06 00:26 Which is the less surprising result. 06/06 00:27 oh well... 06/06 00:27 -!- mode/#epigram [+v pigworker] by ChanServ 06/06 00:27 It would have been somewhat odd if that had solved the positivity problems. 06/06 00:28 If U = f U is negative, I'd expect expanding f U to have the same problem. 06/06 00:29 I'll look into that, that's definitely something to clarify. 06/06 00:31 I'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 ChanServ 06/06 00:35 I'm no expert, either. 06/06 00:35 I 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 W-types are easy, of course, but I think observational equality is also hard. 06/06 00:36 For different reasons than Desc, though. 06/06 00:37 -!- mode/#epigram [+v pigworker] by ChanServ 06/06 01:08 dolio: what about a two-step encoding like this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25931#a25934 06/06 02:02 That might work. 06/06 02:05 Yeah, that seems kosher. 06/06 02:06 that's intriguing 06/06 02:08 found it almost by accident :) 06/06 02:12 what is your intuition of this external notion Desc' and its link with the encoded one? 06/06 02:13 well, Desc' is larger in principle, but it's also what Fix easily digests, while Desc is what we really want to describe 06/06 02:23 so $[_$] is sort of like translating to a lower level unsafer language 06/06 02:24 but the Desc' values that are in its image are ok 06/06 02:25 ok, I see 06/06 02:26 Desc' is descriptions over Set, Desc is descriptions over U, and you interpret the latter into the former. 06/06 02:27 Since U is being interpeted into Set. 06/06 02:27 i'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 pedagand: http://code.haskell.org/~dolio/agda-share/universes/html/DataHierarchy.html 06/06 02:48 thanks for the pointer 06/06 02:49 I keep it carefully, but for now... must... sleep... :-) 06/06 02:50 :) 06/06 02:50 g'd night 06/06 02:51 -!- mode/#epigram [+v pigworker] by ChanServ 06/06 10:58 pedagand: I linked your Syntax.pig file from our embrionic website 06/06 12:08 goodo :-) 06/06 12:36 06/06 12:56 haha, Pig just ate all my ram. I've 4gigs... 06/06 16:02 I restarted it with top nearby. 1.1G resident, and counting... 06/06 16:04 oh well... 2.2G 06/06 16:05 I'll sneakily put that in the test repos, hehe :-) 06/06 16:06 nice :) we're catching up with agda 06/06 16:11 hehe, I've some huge proof term left open, this might be the cause of the problem 06/06 16:16 is it me or http://www.e-pig.org/epilogue/ is "blank"? 06/06 16:35 pedagand: Not just you 06/06 16:41 ok, 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 I think it's probably my fault. In fact, since I switched the main website to the new one earier 06/06 16:46 No idea what bad I made. But, the data is safe, so no need to panic :-/ 06/06 16:50 tsapi, btw, do you use Plan9 or Inferno? 06/06 16:52 pedagand plan9 06/06 16:52 pedagand, it's one of my many bad habits :) 06/06 16:53 well, 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 and you have all the software to "work" (read, emacs) there? or you've to use Acme, for instance? 06/06 16:59 I 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 It's fun to play with and has some interesting ideas, particulary about the filesystem/namespaces etc. 06/06 17:09 yes, I read a few papers about it, it looks really cool 06/06 17:14 pedagand: Epilogue is back 06/06 17:25 oooooh :-) And I see tsapi's web page at e-pig.org. Great 06/06 17:27 is anyone planning to give it a CSS brush? If no, I could do that tonight if you want 06/06 17:28 I mean: "I could do that, if you want" (and that would probably be tonight) 06/06 17:31 I'd be very happy for you to do it is you want :) 06/06 17:32 ok ;-) 06/06 17:33 is tomorrow the moment of truth for Levitation? 06/06 17:35 hehe 06/06 17:41 yep, tomorrow ;-) 06/06 17:43 why do we want pairs to be lazy in Epigram? 06/06 17:56 to retain sharing? 06/06 17:56 -!- mode/#epigram [+v dolio] by ChanServ 06/06 18:20 epilogue has lost its darcs feed 06/06 19:38 (I've pushed web/index.alt.html, feel free to move it to index.html when it's satisfying) 06/06 19:40 I think there is no more darcsweb behind, anyway, isn't it? 06/06 19:40 pedagand, very nice :) 06/06 19:45 that'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 I kind of liked having different pages for the different sections but perhaps there isn't so much point if they aren't very big 06/06 19:52 yeah, 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 I think that putting the Download section at the bottom would give a better balance 06/06 19:57 yeah, and we should have quick link to the epilogue 06/06 19:59 ha, indeed! 06/06 20:00 tsapi: rss feed fixed, cheers for the heads up 06/06 20:01 moleris, cool 06/06 20:01 pedagand: Have you got a copy of the images in your quotation post handy? They seem to have gone walkabout 06/06 20:02 yep, I've them on my hd, I'll fix that 06/06 20:03 ta 06/06 20:03 webpage looks good 06/06 20:04 i moved the downloads and added an epilogue link 06/06 20:18 ok, I did it here but go ahead, feel free to push 06/06 20:23 pedagand, sorry, i already did 06/06 20:25 sure, no problem 06/06 20:25 I think we should absorb the contents of INSTALL into the web docs and remove it. Better not to maintain two sets of instructions 06/06 20:29 I quite like to "more INSTALL" when I'm walking through a new source code but I admit being old fashioned 06/06 20:37 I've change the style of
so that they are slightly padded on the right 06/06 20:47 maybe we could "mv index.alt.html to index.html" now? 06/06 20:48 I do it, we can still bikeshed it later on 06/06 21:11 hop, e-pig.org updated :-) 06/06 21:18 pedagand good work :) 06/06 21:19 pedagand, fair point about INSTALL, but we should synchronise it somehow. 06/06 21:20 maybe just be a direct copy of what is in downloads section with the html formatting removed 06/06 21:21 well, you're convincing me of the advantage of the html: there is no extra-work to be done :-) 06/06 21:25 in that case we could just put a note in the INSTALL saying to point your web browser at the local copy of the html instructions 06/06 21:27 exactly 06/06 21:28 I'll do it then 06/06 21:29 perfect, thanks 06/06 21:30 pedagand, done. 06/06 21:49 that looks good 06/06 21:52 -!- mode/#epigram [+v soupdragon] by ChanServ 06/06 22:02 it's common to link right into a $vcs-web interface for such things 06/06 22:07 Laney: what things? 06/06 22:16 re: INSTALL 06/06 22:17 ok, good 06/06 22:18 -!- mode/#epigram [+v dolio] by ChanServ 06/06 23:20 --- Day changed Mon Jun 07 2010 -!- mode/#epigram [+v dolio] by ChanServ 07/06 00:17 any webologists around? this is 404ing http://www.e-pig.org/test/Syntax.pig 07/06 00:31 no clue about the 404 07/06 01:29 have been working on this steaming pile of ex....ment http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf 07/06 01:30 pigworker on page 2 is * meant to be Ty? 07/06 01:43 inside that mutual definition 07/06 01:43 yeah. botched alpha conversion. not real agda... 07/06 01:44 thanks for the catch 07/06 01:45 I just can't get this stuff right unless I'm typechecking the source for the paper. 07/06 01:47 gosh!! that was a fun read 07/06 02:04 ISTR you mentioning something like this idea on agda mailing list but without s & k? 07/06 02:05 I wonder if you could implement a linear dependent type calculus in this same way 07/06 02:10 -!- mode/#epigram [+v dolio] by ChanServ 07/06 02:17 The s and k thing just had to happen: it's the ancient way of good plumbing. 07/06 02:51 Linearity 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 ChanServ 07/06 08:20 -!- mode/#epigram [+v Saizan] by ChanServ 07/06 08:54 -!- mode/#epigram [+v pigworker] by ChanServ 07/06 08:55 pedagand: It's official then :) Congratulations! 07/06 09:58 Our ICFP was accepted!!!!! 07/06 09:58 * edwinb dances a happy, if astonished, dance 07/06 09:58 edwinb: Congrats, you and us both! 07/06 09:59 Congratulations to you chaps too :) 07/06 10:00 I get the impression, from the modified reviews, we just sneaked in 07/06 10:03 pigworker: any update on the SPLS title, or should I go with the proposed? 07/06 10:05 edwinb: fantastic! 07/06 10:06 pedagand, moleris, tsapi: quality! 07/06 10:07 oh, I got an "accepter paper #23". Lovely 07/06 10:07 edwinb: I think a little jocularity isn't a big problem 07/06 10:08 pigworker, you seem delighted this morning: I just arrived, what happened? :-) 07/06 10:08 delight! 07/06 10:08 :-) 07/06 10:09 pigworker: splendid 07/06 10:10 pedagand: congratulations on the paper. 07/06 10:11 Lots of dependent types at ICFP this year then... 07/06 10:12 -!- mode/#epigram [+v dolio] by ChanServ 07/06 10:20 edwinb, ha, reading the logs, I understand the reason of the euphoria: congrat's too! 07/06 10:22 I 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 adam__: well done! good mood around here today... 07/06 10:30 so I see, congratulations on getting in to ICFP 07/06 10:30 sorry for the join/part nonsense 07/06 10:30 now I just have to get myself a gig 07/06 10:31 pigworker: 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 I can't remember if mutual induction is explicitly present, but it's always codable by indexing with a flag 07/06 10:33 Is that different somehow from the induction-induction in your paper? 07/06 10:34 induction-induction involves fixpoints in Sigma Set \ X -> Set, not just 2 -> Set 07/06 10:35 agundry, and I saw a tweet on getting to MSFP: congrats! :-) 07/06 10:35 indexing one branch over another is new/strange/weird/harder to encode 07/06 10:35 pedagand: thanks! 07/06 10:36 Toni Setzer has a new story about induction-induction. I think the LICS submission...ended up at CSL. 07/06 10:36 Long 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 hello #epigram, today seems to be a good day :) 07/06 10:47 pigworker: 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 could you send me one please? Although I'm sure we can all roughly guess what's in it. 07/06 10:56 edwinb: will do, when I get to school 07/06 11:02 righto. As you see, from the absence of others, there is no serious hurry. 07/06 11:08 -!- mode/#epigram [+v Saizan] by ChanServ 07/06 12:41 -!- mode/#epigram [+v Saizan] by ChanServ 07/06 13:08 -!- mode/#epigram [+v soupdragon] by ChanServ 07/06 17:43 -!- mode/#epigram [+v Saizan] by ChanServ 07/06 19:23 -!- mode/#epigram [+v dolio] by ChanServ 07/06 20:20 tsapi, 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 ChanServ 07/06 21:25 pedagand: I'm just using sets for both and propositional equality for the laws 07/06 21:27 ha, 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 this 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 just the same as me, I'm also using type in type 07/06 21:29 ok, good 07/06 21:29 I started with a "dom : Arrows -> Objects, cod : Arrows -> Object, compos : Arrows -> Arrows -> (pf that cod = dom) -> Arrows" 07/06 21:30 so, that's probably what was crazy, I became reasonable after :-) 07/06 21:30 record Cat : Set where 07/06 21:32 that didn't work... 07/06 21:32 ok, thanks 07/06 21:33 http://www.cs.ioc.ee/~james/Categories.agda 07/06 21:34 more sensible people than myself use setoids for the homset and hence the equations 07/06 21:35 I got mired when I tried to use setoids 07/06 21:36 I thin having dom and cod introduces more equalities than necessary but I haven't really tried it that way 07/06 21:36 so quotients look like a magic wand to me 07/06 21:36 yeah, ok, I did the same thing than you, that's reassuring 07/06 21:36 it's really a different definition of a category I think, not just a different formalisation with dom and cod 07/06 21:36 as far as I understood, there is a problem with quotient. pigworker will correct me, that was a story about representing real numbres 07/06 21:37 tsapi, on ncatlab (link written in the Cat file), someone was arguing that the Hom(x,y) representation was the right one 07/06 21:38 I mean, the "right" one :-) 07/06 21:38 anyway, I'm reassured, thanks 07/06 21:39 pedagand, sounds interesting, i'll take a look 07/06 21:44 regarding real numbers in quotients - http://www.reddit.com/r/dependent_types/comments/azl8r/quotients_epigram2/ 07/06 21:45 I guess that's not the only problem though 07/06 21:46 soupdragon, thanks for the link 07/06 21:52 at meetings, you actually hear people say, in all seriousness, "but those are not the real real numbers" 07/06 21:52 to 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 in the fragment of category theory I'm working in, I haven't come across such problems 07/06 21:52 roconnor 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 and what's the answer ?:) 07/06 21:58 if you say "yes", you break 'quotientness' by a carefully engineered S? 07/06 22:01 by "breaking quotientness" I mean: you can access the "physical" representation of your objects, while you wanted to abstract it away 07/06 22:01 pigworker, I'd have thought absolutely yes, it basically the definition of a function on setoids. 07/06 22:02 yes it is the definition of a function on setoids, but setoids don't hide information, they just demand evidence that you don't abuse information 07/06 22:04 oh so maybe we only get the respectfulness proof from a sort of parametricity? 07/06 22:04 yep 07/06 22:04 but what sort of parametricity? 07/06 22:05 at the moment, I don't know good conditions for the existence of choice functions, only good and bad examples 07/06 22:05 consider a universe operator which closes some (U, El) under Pi and quotients; calculate the free theorems 07/06 22:12 -!- mode/#epigram [+v dolio] by ChanServ 07/06 22:17 can't see it.. (q,q') \in X/R <=> ??? 07/06 22:27 we 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 B 07/06 22:28 so it seems that the relation for quotients needs to use qelim 07/06 22:28 perhaps, but is that a problem? 07/06 23:45 if you unpack (X/R) to get elements of X which you then use by R'ing them, you do respect the quotient 07/06 23:46 hi shapr! 07/06 23:49 pigworker, not a problem just that I don't know what it shoudl be 07/06 23:49 pedagand: 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 it's all terribly start-a-fight equality-sensitive 07/06 23:51 Oh, you mentioned that. I missed it in my skimming. 07/06 23:51 yeah, 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 Yes. 07/06 23:52 and you're convinced by that too? 07/06 23:52 (out of curiosity) 07/06 23:52 hankovian mischief-merchants would consider Obj -> Sigma Set \ X -> Obj 07/06 23:53 Well, 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 But, if a mathematician does as well, that's probably a good sign. 07/06 23:54 ok, thanks 07/06 23:54 I'd like to have a category theory text which defines everything using category theory 07/06 23:54 pigworker, the benefit of this encoding lies in the implementation? or it captures more definitions? or something else? 07/06 23:55 I haven't yet found one, which is frustrating.. closest is probably Sets for Mathematics which axiomatizes SET using categories 07/06 23:55 Does that go into Lawvere's ETCS? 07/06 23:56 that's what it is, I think 07/06 23:57 pedagand: it's almost certainly idiotic, but with a naive attitude to equality, isomorphic to the other two 07/06 23:57 He worked on another foundation, too, as I understand. I don't know if it's in any books, though. 07/06 23:57 His thesis goes into it a little, though. 07/06 23:57 Where you axiomatize the category of categories. 07/06 23:58 Hardcore categorists would probably tell you that's wrong, though, because the collection of all categories is naturally a 2-category. 07/06 23:59 huh 07/06 23:59 pigworker, ok. I always feel better when I do it the Hank way, so I'll give it a go :-) 07/06 23:59 2-category is different form Set-2 right? 07/06 23:59 you are saying something different than it's Big? 07/06 23:59 soupdragon, morphisms form a category in a 2-cat 07/06 23:59 --- Day changed Tue Jun 08 2010 pedagand: I'm not saying it's the Hank way. Unless it's the Hank way of taking the piss. 08/06 00:00 In the case of Cat, 2-category means it talks about categories, functors and natural transformations in the definition. 08/06 00:00 pigworker, hehe 08/06 00:01 In 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 id X = (1 , \_ -> X) 08/06 00:01 hiya soupdragon 08/06 00:02 Pow : 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 sorry, 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 I'd like to write (x : X) * but what gives? 08/06 00:33 I note you've picked up nervous double backslash syndrome from spending too much time in Agda mode. 08/06 00:36 I have? 08/06 00:42 Anyhow, 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 Somehow what I don't mind in "callCC (\k -> ...)" seems especially ugly when it's Sigma or Pi or W. 08/06 00:45 Hmm. That would be nice. 08/06 00:46 But possibly a nightmare to parse... 08/06 00:46 Or "shift (\k -> ...)". I guess the very name of callCC suggests that you're passing a function. 08/06 00:46 It is simultaneously desirable that really only lambda binds and that on the surface, you can make anything vaguely functional bind. 08/06 00:46 Yeah, Coq seems to manage by allowing you to rewrite at an almost token stream level it seems. 08/06 00:48 But I don't really know how their parser works. 08/06 00:48 I'm profoundly grateful that it's Sg S \ x -> T, not Sg S (\ x -> T). 08/06 00:48 I wish Haskell did that. 08/06 00:49 That is handy. Although it looks wrong to me from years of Haskell training. 08/06 00:50 if all the binders were highlighted in a peculiar way it wouldn't be much of a problem to have custom ones 08/06 00:51 LEGO did it, which is why I'm used to it. 08/06 00:52 Peculiarly, I learned LEGO in 1995 and Haskell in 2000. 08/06 00:54 yeah I always wondered why haskell had that restriction 08/06 00:54 pigworker, 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 it 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 pedagand: I await with interest; but bughunting in the morning is definitely the best policy 08/06 01:03 yeah, will see. Hopefully it's really working... 08/06 01:06 g'd night folks 08/06 01:07 Night all! 08/06 02:46 -!- mode/#epigram [+v Saizan] by ChanServ 08/06 03:05 -!- mode/#epigram [+v dolio] by ChanServ 08/06 06:27 -!- mode/#epigram [+v dolio] by ChanServ 08/06 08:16 -!- mode/#epigram [+v edwinb] by ChanServ 08/06 09:10 -!- mode/#epigram [+v pigworker] by ChanServ 08/06 10:56 morning pigworker 08/06 10:56 morning tsapi, how do? 08/06 10:56 not bad thanks. How's the refactoring going? 08/06 10:58 I stepped away for a few days to write a paper, but it's in a stable position just now. 08/06 11:02 tsapi, pigworker: I have just pushed a patch migrating the new levitated IDesc to the new OpTree lang 08/06 11:08 couple more HFs to kill, but it shouldn't be a problem 08/06 11:08 moleris: cool; how was it? tsapi: just got your email 08/06 11:09 much 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 Hooray, I've proved that flip plus == plus 08/06 11:11 pedagand and I are giving a demo on Epigram tomorrow to a general compsci audience 08/06 11:12 any suggestions for better examples than commutativity of plus? 08/06 11:13 agundry: flip plus == plus is key! not true in Coq! 08/06 11:14 Yes, that's why I thought I should check we can actually prove it 08/06 11:14 agundry, 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 Eg. Maybe is a very helpful example for understanding monads. 08/06 11:15 agundry so, vzip? (or rather, vectorized application?) 08/06 11:16 tsapi: that's certainly true 08/06 11:16 pigworker: vzip/vapp could work, it will be interesting to see how bad the coercion woes get 08/06 11:17 agundry: quite; I'm still curious to know if lazy defs help, but maybe now is not the time to find out 08/06 11:19 Hmm, I wonder if I can sneak in to the SICSA conference tomorrow 08/06 11:19 pigworker: so am I, though perhaps I should wait until after tomorrow 08/06 11:19 yes, see what's already workable 08/06 11:21 although recompiling the thing with an experimental hack just before the demo is traditional... 08/06 11:21 edwinb: our demo is at the SICSA conference around 19.00; I don't think we will go to much else 08/06 11:21 oh, apparently there's only you and Lars doing demos 08/06 11:26 yep, that could be amusing 08/06 11:26 mmh, 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 IDesc: Now with 100% fewer higher order scopes 08/06 13:44 moleris: nice work 08/06 13:45 moleris: nice work :) 08/06 13:46 ta 08/06 13:47 I am experimenting with Fin at the moment, will re-enable the test case shortly 08/06 13:48 I 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 pigworker: cool! P.S. you can update the reference to the gentle art of levitation :) 08/06 14:27 -!- mode/#epigram [+v soupdragon] by ChanServ 08/06 14:33 'deed I can! 08/06 14:55 will also add a bit more related work (McKinna/Pollack, Barras, Benton et al, Sheard) 08/06 14:55 what's Benton et al ? 08/06 14:57 "Strongly typed term representations in Coq" (submitted to JAR) 08/06 15:00 ooh it's even in color 08/06 15:00 I coloured it in during the exam board, yesterday afternoon. 08/06 15:00 time for school... 08/06 15:01 moleris, do you have a data tactics for IDesc? 08/06 15:15 pedagand: Sorry, no - I have plenty of bits n pieces but nothing ready for a demo :-( 08/06 15:31 no problem, that was just curiosity. I'm myself in bits'n'pieces and am not ready for a demo either :-) 08/06 15:32 Maybe we should just fake it for Vec and Fin ;-) 08/06 15:32 I think it would be unwise to expose a general audience to the true horror IDesc, so I'd be tempted to fake it 08/06 15:34 -!- mode/#epigram [+v dolio] by ChanServ 08/06 16:03 -!- mode/#epigram [+v pigworker] by ChanServ 08/06 16:12 -!- mode/#epigram [+v dolio] by ChanServ 08/06 16:19 -!- mode/#epigram [+v Saizan] by ChanServ 08/06 16:20 -!- mode/#epigram [+v Saizan] by ChanServ 08/06 19:57 -!- mode/#epigram [+v pigworker] by ChanServ 08/06 20:21 -!- mode/#epigram [+v dolio] by ChanServ 08/06 20:43 -!- mode/#epigram [+v dolio] by ChanServ 08/06 21:08 -!- mode/#epigram [+v soupdragon] by ChanServ 08/06 22:24 -!- mode/#epigram [+v soupdragon] by ChanServ 08/06 23:12 --- Day changed Wed Jun 09 2010 -!- mode/#epigram [+v dolio] by ChanServ 09/06 01:08 -!- mode/#epigram [+v dolio] by ChanServ 09/06 05:12 http://video.google.com/videoplay?docid=2717941286977874486# 09/06 10:09 Russian animation: Cat Who Walked by Herself 09/06 10:09 nice version of the rudyard kipling story 09/06 10:09 also 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 Program Verification Through Characteristic Formulae 09/06 10:10 bringing Dijkstra back 09/06 10:10 to pure functional programs 09/06 10:10 pigworker: the Forsberg & Setzer paper has been published at CSL by the way, I found a list of accpepted papers 09/06 10:14 tsapi: yeah, Hank told me; Toni hasn't updated his .bib 09/06 10:15 is 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 I don't even know if such a converability rule is sound. 09/06 10:33 The 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 edwinb: I mean in a stronglly normalizing system, such as coq, agda or epigram 09/06 10:38 edwinb: 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 roconnor, you could probably hack that into CoqMT (I tried to do somethign a bit like that an failed, though) 09/06 10:40 MT? 09/06 10:41 right now it's got some arithmetic that lets you do stuff like refl : x + y = y + x 09/06 10:41 http://pierre-yves.strub.nu/research/coqmt/ 09/06 10:41 modulo theory, he has a paper at CSL too 09/06 10:41 oh right 09/06 10:41 what is this CSL? 09/06 10:41 is modulo theory less hacky than it sounds? 09/06 10:42 I keep forgetting you just add 'dependent types' to any of these terms to google it 09/06 10:42 roconnor, well it adds new decision procedures to the conversion rule - you have to prove the axioms for them in Coq 09/06 10:42 not sure if that makes it okay 09/06 10:42 CSL: http://mfcsl2010.fi.muni.cz/csl/social-program , look at the stuffs in *bold* :-) 09/06 10:43 roconnor: but even if it's strongly normalising, b might arise from, say, a proof of false 09/06 10:50 hmm 09/06 10:51 roconnor: 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 form 09/06 11:05 it's also not obviously type preserving for dependent if 09/06 11:06 wow, the Pig becomes much faster if one partially disables the scheduler 09/06 11:07 this may help lessen my embarrasment at the demo tonight... 09/06 11:07 agundry: doesn't surprise me; I'm quite sure Epigram 1 spent much of it's time checking that there wasn't anything important to do 09/06 11:08 it's -> its 09/06 11:08 yes, somehow we need to keep track of that information, rather than searching the whole proof state 09/06 11:09 spotting saturated regions would be a good start 09/06 11:09 consider P b = if b then (if b then Nat else Bool) else Nat 09/06 11:11 observe zero : P true, zero : P false, but zero not in P b if b a variable 09/06 11:11 hmm, I guess we are interested in two things: whether there any holes in a region, and whether there are any elaboration problems 09/06 11:12 so if b then x else x = x needs its Sam Lindley friends to have a chance of being sound 09/06 11:12 agundry: yes, no-orange-here, and the weaker no-orange-to-automate here would be useful 09/06 11:14 it'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 already 09/06 11:21 edwinb: on another top, I'm wondering about projectors for next Wednesday... 09/06 11:54 insert ic 09/06 11:54 I assume you are going to use more traditional methods? 09/06 11:55 I think we have a steam powered projector in the room 09/06 11:55 I'm going to do lots of live Agda 09/06 11:56 oh, okay 09/06 11:56 ideal situation -- simultaneous projection; if I have to pick one, it'll have to be the computer 09/06 11:56 but this could still mean live Agda on OHP ;) 09/06 11:56 it might be possible 09/06 11:57 true, but it's fun to actually run this code, even though it goes slower on a computer than on a handwritten slide 09/06 11:57 but the layout of the room is such that if too many turn up, there is another half of the room with a second screen 09/06 11:57 and I think it's only possible to project one thing twice, if that makes sense 09/06 11:58 yes, but one with data and one with steam would work? 09/06 11:59 should do, but I'd have to go to the room and check 09/06 11:59 which is not so easy since I'm at home at the minute 09/06 11:59 I'll go and look later 09/06 12:00 what 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 Unrelatedly, "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 Oh splendid. I don't think I've seen that one. 09/06 12:18 * edwinb finds it on the internets 09/06 12:19 pedagand, are the stratified model for the gentle art in the Pig09 repo? 09/06 12:23 yes, anything which is not "TT" as a suffix of the filename 09/06 12:24 that is, Desc.agda and IDesc.agda 09/06 12:24 pedagand, cool, thanks 09/06 12:24 pigworker: 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 roconnor: check the example! 09/06 12:37 edwinb: I haven't quite figured how why having b arise from a proof of false would be problematic. Granted you did make me feel nervous 09/06 12:37 pigworker: oh, sorry I see now you wrote more 09/06 12:38 the point is that the branch types get to compute even if the return type is stuck 09/06 12:38 heh, dependent type theory is so complicated :) 09/06 12:39 who is Sam Lindley? 09/06 12:40 yeah, very sensitive to details of computation 09/06 12:40 Sam 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 He was Phil Wadler's researcher for a bit, and now he works for a spin-out company. 09/06 12:43 Like 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 hehe 09/06 12:44 btw, 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 the applicative functor paper is the good reference 09/06 12:48 I haven't written a SHE paper yet, and it's not going to happen by Monday. 09/06 12:50 I 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 And besides, I'm supposed to be writing a grant proposal about SHE by Monday. 09/06 12:52 sounds unfun 09/06 12:52 It's made me extraordinarily productive at almost everything else. I'm thinking of doing the dishes. 09/06 12:53 pigworker: 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 edwinb: splendid! 09/06 14:55 agundry, pedagand: do you want any more input from me for tonight? 09/06 15:26 hmm, I think we have a reasonable plan 09/06 15:27 if you are around we could chat about the demo file, but it's not too urgent 09/06 15:28 I'm barely able to stay awake, but you could send me the file... 09/06 15:28 okay, but don't look at it for too long if sleep would be more useful! 09/06 15:31 email away 09/06 15:32 ta 09/06 15:32 after the demo I will tidy the file up and stick it somewhere visible to reddit ;-) 09/06 15:32 looks good (but we really must make more constraint solving happen mechanically) 09/06 15:36 yes, that is on my list of things to think about 09/06 15:36 mostly I have just hidden the ships in separate files 09/06 15:36 ok, but you should be in a position to say "these bits will eventually look after themselves" 09/06 15:37 that is the intended semantics of "load" in the demo file... mostly 09/06 15:38 fine 09/06 15:38 agundry: 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 tsapi: thanks. That sounds like a good plan. 09/06 15:41 -!- mode/#epigram [+v dolio] by ChanServ 09/06 16:12 -!- mode/#epigram [+v dolio] by ChanServ 09/06 17:08 -!- mode/#epigram [+v dolio] by ChanServ 09/06 18:08 -!- mode/#epigram [+v dolio] by ChanServ 09/06 19:12 -!- mode/#epigram [+v dolio] by ChanServ 09/06 20:08 -!- mode/#epigram [+v Saizan] by ChanServ 09/06 22:39 -!- mode/#epigram [+v Saizan] by ChanServ 09/06 23:29 --- Day changed Thu Jun 10 2010 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 00:28 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 01:24 -!- mode/#epigram [+v pigworker] by ChanServ 10/06 08:08 Morning 10/06 09:45 agundry pedagand: How was the gig? 10/06 09:46 moleris: okay, some people were mildly interested in what we are doing, others were completely bemused 10/06 09:48 pretty much as expected really 10/06 09:48 it was very amusing to have a huge TV screen on which to display a couple of emacs buffers 10/06 09:49 :) 10/06 09:52 as long as it didn't break too spectacularly 10/06 09:52 it didn't, not that we tried anything very adventurous 10/06 09:53 though pedagand did open the category theory file at one point 10/06 09:53 you do well to avoid going too far off script at these types of things 10/06 09:53 unfortunately the compiler seems not to be working at the moment 10/06 09:53 so we couldn't demonstrate that 10/06 09:54 hmm, it what way is it broken? 10/06 09:54 it doesn't cope with operator primitives (but a cheap fix is to add them to support.e) 10/06 09:55 moreover, plus two two evalues to two 10/06 09:55 *evaluates 10/06 09:55 irk 10/06 09:55 I'm not sure what is going on with the operator DSEL, otherwise I would have spent more time debugging 10/06 09:56 I'm not sure what state the code is in that generates support.e code from OTrees 10/06 09:56 I couldn't find it, though I didn't look very hard 10/06 09:57 and there are still a number of operators with legacy code 10/06 09:57 no, it shouldn't be 10/06 09:57 I have a meeting this morning (possibly) but after that I might get my hands dirty porting a few more operators 10/06 09:58 thanks 10/06 09:59 -!- mode/#epigram [+v pigworker] by ChanServ 10/06 11:32 pigworker: the green equality - is it going? 10/06 11:45 pigworker says we should get rid of it, and I agree 10/06 11:45 porting it to OpTree is going to be a big deal, so I also agree :) 10/06 11:46 -!- mode/#epigram [+v dolio] by ChanServ 10/06 15:01 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 15:24 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 17:04 -!- mode/#epigram [+v pigworker] by ChanServ 10/06 17:16 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 17:36 -!- mode/#epigram [+v dolio] by ChanServ 10/06 20:08 -!- mode/#epigram [+v Saizan] by ChanServ 10/06 21:54 --- Day changed Fri Jun 11 2010 -!- mode/#epigram [+v dolio] by ChanServ 11/06 00:11 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 02:50 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 03:01 -!- mode/#epigram [+v pigworker] by ChanServ 11/06 09:15 -!- mode/#epigram [+v pigworker] by ChanServ 11/06 14:26 -!- mode/#epigram [+v dolio] by ChanServ 11/06 15:11 -!- mode/#epigram [+v dolio] by ChanServ 11/06 16:11 Hmm. Things I didn't expect to be doing this afternoon: Explaining monads to the head of school 11/06 16:18 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 16:49 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 17:46 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 17:57 -!- mode/#epigram [+v dolio] by ChanServ 11/06 18:11 Yow! 11/06 18:13 shapr: only tumbleweed in here today :) 11/06 18:14 aww 11/06 18:14 It's so quiet! 11/06 18:14 -!- mode/#epigram [+v dolio] by ChanServ 11/06 20:07 -!- mode/#epigram [+v dolio] by ChanServ 11/06 20:15 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 21:25 -!- mode/#epigram [+v pigworker] by ChanServ 11/06 21:33 -!- mode/#epigram [+v pigworker_] by ChanServ 11/06 22:27 -!- pigworker_ is now known as pigworker 11/06 22:27 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 22:34 -!- mode/#epigram [+v Saizan] by ChanServ 11/06 23:02 --- Day changed Sat Jun 12 2010 -!- mode/#epigram [+v Saizan] by ChanServ 12/06 00:00 -!- mode/#epigram [+v dolio] by ChanServ 12/06 00:07 -!- mode/#epigram [+v Saizan] by ChanServ 12/06 02:37 -!- mode/#epigram [+v dolio] by ChanServ 12/06 03:11 -!- mode/#epigram [+v Saizan] by ChanServ 12/06 05:14 http://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/models/Alg-IIR.agda 12/06 11:38 It's a more "algebraic" presentation of indexed induction recursion, with examples (Nat, freshlists, a universe). 12/06 11:39 So, descriptions of indexed induction-recursion only require induction-recursion for their definition? 12/06 12:32 -!- pigworker_ is now known as pigworker 12/06 12:35 So, descriptions of indexed induction-recursion only require induction-recursion for their definition? 12/06 12:37 (That'll look weird in the logs, probably.) 12/06 12:39 Oh, descriptions of indexed families were just an inductive type, too. 12/06 12:42 -!- mode/#epigram [+v codolio] by ChanServ 12/06 14:10 Here'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 dolio 12/06 14:36 pigworker ^^ 12/06 14:37 Although 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 Perhaps it's related to decode not termination checking as written? 12/06 14:42 -!- mode/#epigram [+v pigworker] by ChanServ 12/06 15:02 dolio: that's weird 12/06 15:03 mostly, when I do that sort of construction, I expect termination to moan and positivity to grumble; it's *size* I'm watching 12/06 15:04 Well, 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 ChanServ 12/06 15:10 pigworker: I guess it's ultimately complaining that the 'd' in decode might introduce negativity (I think that's right). 12/06 15:13 I 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 Anyhow: http://code.haskell.org/~dolio/agda-share/universes/IRDataHierarchy.agda 12/06 15:30 That's an attempt at a hierarchy of inductive-recursive universes closed under induction-recursion. 12/06 15:31 I'm not sure if I've got everything, though. 12/06 15:31 -!- mode/#epigram [+v Saizan] by ChanServ 12/06 15:43 -!- mode/#epigram [+v dolio] by ChanServ 12/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 ChanServ 12/06 18:27 Well, that actually worked out much better than expected. 12/06 19:21 -!- mode/#epigram [+v dolio] by ChanServ 12/06 20:10 -!- mode/#epigram [+v pigworker] by ChanServ 12/06 22:46 -!- shapr is now known as shapr 12/06 23:27 --- Day changed Sun Jun 13 2010 -!- mode/#epigram [+v dolio] by ChanServ 13/06 00:11 -!- mode/#epigram [+v codolio] by ChanServ 13/06 01:10 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 01:14 -!- mode/#epigram [+v dolio] by ChanServ 13/06 02:07 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 03:07 -!- mode/#epigram [+v dolio] by ChanServ 13/06 07:10 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 07:18 -!- mode/#epigram [+v dolio] by ChanServ 13/06 08:07 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 10:06 -!- mode/#epigram [+v dolio] by ChanServ 13/06 11:07 -!- mode/#epigram [+v dolio] by ChanServ 13/06 14:11 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 14:15 -!- mode/#epigram [+v Saizan] by ChanServ 13/06 14:19 I wonder if we should follow this advice to make our webservers display agda files nicely: http://www.w3.org/International/questions/qa-htaccess-charset 13/06 20:42 by defaulting to utf-8 encoding 13/06 20:43 thanks to pedagand for another informative weekly summary! 13/06 20:59 glad you like, really 13/06 20:59 it's good to know that some people actually look at it :-) 13/06 21:00 Am I missing out on epigram action somewhere? 13/06 21:00 dolio: aren't you subscribed to epigram-discuss? 13/06 21:01 I guess not. 13/06 21:02 Just to the old epigram list that no one uses anymore. 13/06 21:02 http://www.e-pig.org/darcs/Pig09/web/#community 13/06 21:02 the old durham one is dead i think 13/06 21:03 It'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 ChanServ 13/06 21:06 dolio, your subscription is approved, welcome ;-) 13/06 21:08 Sweet. 13/06 21:08 So, pigworker displayed a Desc for induction recursion in Agda yesterday... 13/06 21:11 And I did my thing and put it in a hierarchy of inductive-recursive universes. 13/06 21:11 But that leaves me with a conundrum: 13/06 21:11 I 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 But the thing I defined sort of seems like an internal one, but defined using an external one. 13/06 21:13 Perhaps it's just an illusion, though. 13/06 21:13 Or perhaps I just don't understand the distinction. 13/06 21:15 hi, 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 I'm doing it 13/06 22:00 awesome! 13/06 22:01 done, it's awaiting moderation 13/06 22:12 there already was an epigram mailing list, so I asked for epigram2 13/06 22:14 I'm having a thought for the next generation of PhD students, trying "epigram", then "epigram2", to settle for "epigram3" 13/06 22:14 I thought we were onto 'suc epigram' by now 13/06 22:16 :-) 13/06 22:29 nice post 13/06 22:43 Saizan, 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 you're in what looks like a rather easy group, lucky Italians! 13/06 22:56 you'll do well to beat English goalkeeper comedy 13/06 22:57 I was in a pub in Edinburgh watching it: it is surprising to see people delighted to see their own "country" take a goal 13/06 22:58 Scotsmen will be cheering for Anyone But England 13/06 23:00 as a substitute for having a team worth supporting 13/06 23:00 it looks like a French striker such as Henry is more able of his hands than your goalkeeper :-) 13/06 23:00 heh 13/06 23:01 strange country indeed ;-) 13/06 23:01 too right 13/06 23:01 hah, 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 Sometimes Scotland qualify, but they always go out early 13/06 23:08 plus_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 some people have this ability, the rest of us don't 13/06 23:16 I've a patch that gives you the first and last component, putting the remaining in ellipsis when necessary 13/06 23:16 here, 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 ensued 13/06 23:17 if the last name is a "hole_xxx", this tells you that an elaboration problem is stuck (often, something wrong happened) 13/06 23:18 impl_2 is the elimination? 13/06 23:19 impl is, I think, generated by the "let" construction 13/06 23:20 "makeE" is generated by elimination with a motive 13/06 23:20 ah, yeah 13/06 23:20 paying attention while stepping through the script helps :) 13/06 23:20 Cochon prints these details for debugging purposes, these things ought to be hidden in a high-level language 13/06 23:21 ah btw, what's the relation between UI/ and DisplayLang/ ? 13/06 23:30 in UI/, we define interfaces to the theorem prover 13/06 23:32 right now, DisplayLang is considered as a part of the theorem prover, like ProofState 13/06 23:33 that's an interesting question, thanks for asking 13/06 23:36 Here's a probably less interesting one: where do the names "green" and "blue" equality come from? 13/06 23:37 Syntax coloring somewhere? 13/06 23:37 dolio: epigram syntax colouring - blue is a type constructor, green is a function 13/06 23:38 Ah. 13/06 23:38 That's what I'd have guessed, except the other way around. 13/06 23:39 btw, HsColour does a decent job on .pig files 13/06 23:39 Since Agda is backwards (actually, I can't think of what color type constructors are...). 13/06 23:40 Apparently they're also blue, same as functions. 13/06 23:40 Saizan, actually, DisplayLang ought to be in UI/ as well. I'm opening a ticket, thanks 13/06 23:43 pedagand: ah :), though modules like ProofState import it, but not for any good reason? 13/06 23:48 that'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/Cochon 13/06 23:50 for example, I would really love to get DisplayLang/Lexer and DisplayLang/TmParse out of the way, in UI/Cochon 13/06 23:50 a 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/YourStuff 13/06 23:52 true 13/06 23:54 --- Day changed Mon Jun 14 2010 and it's also needed for Features.* currently 14/06 00:00 wonderful :-) 14/06 00:03 programming 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 ChanServ 14/06 04:10 -!- mode/#epigram [+v dolio] by ChanServ 14/06 05:06 -!- mode/#epigram [+v pigworker] by ChanServ 14/06 08:06 -!- mode/#epigram [+v Saizan] by ChanServ 14/06 12:34 -!- mode/#epigram [+v pigworker] by ChanServ 14/06 13:40 -!- mode/#epigram [+v dolio] by ChanServ 14/06 14:06 edwinb: just to confirm that, bar further unforeseen calamities, I'm on for Wednesday 14/06 18:25 pigworker: okay, thanks for letting me know 14/06 18:25 -!- mode/#epigram [+v pigworker_] by ChanServ 14/06 18:38 -!- pigworker_ is now known as pigworker 14/06 18:40 -!- mode/#epigram [+v dolio] by ChanServ 14/06 19:10 -!- mode/#epigram [+v Saizan] by ChanServ 14/06 19:47 pigworker, got hurkens paradox in my system: doesn't type-check with stratification On, does with stratification Off. 14/06 20:38 however, the way it doesn't type-check is rather disappointing: it is very early on, with one of the helper function 14/06 20:40 I don't think that's unusual. 14/06 20:49 code.haskell.org doesn't seem to be responding... 14/06 20:52 Anyhow, I have the paradox encoded for a system U interpeter there. 14/06 20:52 But I think it would blow up early there, too, because otherwise U would be too large to pass to itself. 14/06 20:53 haskell.org being down is not unusual as well ;-) 14/06 20:53 Yeah. 14/06 20:53 yep, that's the thing: I take s : U and do "s U" in one of the early term 14/06 20:54 what is system U, btw? 14/06 20:54 It's similar to the calculus of constructions, but with 3 levels, and impredicativity on the second level. 14/06 20:55 It's what Hurkens uses in his paper. 14/06 20:55 Actually, 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 Because the latter isn't used at all. 14/06 20:56 ha, indeed. I'm really struggling with his notation and terminology... 14/06 20:57 Yeah, it's rough. 14/06 20:58 I actually cribbed from the Agda encoding. 14/06 20:58 And only looked at his paper to fix up the types. 14/06 20:58 I actually had to rewrite a portion of my interpreter while doing that. 14/06 20:58 Because it revealed serious variable capture issues. 14/06 20:59 http://code.haskell.org/~dolio/pts/hurkens.pts 14/06 21:54 There it is. 14/06 21:54 thanks 14/06 22:00 out of curiosity, which language is that? 14/06 22:01 ha, I see, that's pts, your language :-) 14/06 22:04 Yes. 14/06 22:09 It's a rudimentary interpreter for pure type systems, and I've been adding more and more systems over time. 14/06 22:10 As 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 Anyhow, if [] weren't impredicative, U would have type triangle, I think. 14/06 22:32 And it would be inelligible to be an X. 14/06 22:32 -!- mode/#epigram [+v dolio] by ChanServ 14/06 23:10 -!- shapr is now known as shapr[ 14/06 23:14 -!- mode/#epigram [+v Saizan] by ChanServ 14/06 23:19 --- Day changed Tue Jun 15 2010 -!- mode/#epigram [+v pigworker] by ChanServ 15/06 07:48 -!- mode/#epigram [+v pigworker] by ChanServ 15/06 11:00 -!- mode/#epigram [+v dolio] by ChanServ 15/06 13:06 -!- mode/#epigram [+v Saizan] by ChanServ 15/06 14:32 --- Day changed Wed Jun 16 2010 -!- mode/#epigram [+v dolio] by ChanServ 16/06 04:06 -!- mode/#epigram [+v dolio] by ChanServ 16/06 04:21 -!- mode/#epigram [+v dolio] by ChanServ 16/06 07:09 -!- mode/#epigram [+v codolio] by ChanServ 16/06 08:09 -!- mode/#epigram [+v dolio] by ChanServ 16/06 09:06 -!- mode/#epigram [+v dolio] by ChanServ 16/06 13:09 -!- mode/#epigram [+v codolio] by ChanServ 16/06 17:09 -!- mode/#epigram [+v dolio] by ChanServ 16/06 18:05 -!- mode/#epigram [+v dolio] by ChanServ 16/06 20:09 --- Day changed Thu Jun 17 2010 -!- mode/#epigram [+v dolio] by ChanServ 17/06 00:09 -!- mode/#epigram [+v Saizan] by ChanServ 17/06 00:40 -!- mode/#epigram [+v pigworker] by ChanServ 17/06 08:38 -!- mode/#epigram [+v dolio] by ChanServ 17/06 09:05 -!- mode/#epigram [+v pigworker] by ChanServ 17/06 13:24 pigworker: Don't suppose you've had a thoughts about TELescopes and the new 1st order terms have you? 17/06 13:46 where do we use them? I wonder if we need them now 17/06 13:48 Mainly for opTypes, I can't see them being much use now 17/06 13:53 will be a labourious job to get rid, but it's just grind 17/06 13:54 the alternative is to have HO telescopes and quote them to make types 17/06 14:02 that might be cheaper for now 17/06 14:03 nobody ever updates a TEL, right? 17/06 14:05 don't think so 17/06 14:07 pity is cheap at the moment, though - if we go that way it'll need to be lifted to ((->) NameSuppy) 17/06 14:12 we'd need a name supply to do the quotation, aye 17/06 14:19 -!- mode/#epigram [+v Saizan] by ChanServ 17/06 14:46 -!- mode/#epigram [+v dolio] by ChanServ 17/06 15:09 -!- mode/#epigram [+v dolio] by ChanServ 17/06 16:09 -!- mode/#epigram [+v codolio] by ChanServ 17/06 18:09 Yow! 17/06 18:14 @quote epigram 17/06 18:14 dolio says: Perhaps he's an epigram guy and frowns on Turing completeness. 17/06 18:14 Oh, there's a bot in here. 17/06 18:24 -!- mode/#epigram [+v dolio] by ChanServ 17/06 19:08 -!- mode/#epigram [+v dolio] by ChanServ 17/06 20:04 -!- mode/#epigram [+v codolio] by ChanServ 17/06 21:09 -!- codolio is now known as dolio 17/06 21:44 --- Day changed Fri Jun 18 2010 -!- mode/#epigram [+v dolio] by ChanServ 18/06 01:09 -!- mode/#epigram [+v dolio] by ChanServ 18/06 06:08 -!- mode/#epigram [+v codolio] by ChanServ 18/06 10:20 -!- mode/#epigram [+v pigworker] by ChanServ 18/06 11:00 -!- mode/#epigram [+v dolio] by ChanServ 18/06 11:20 -!- mode/#epigram [+v dolio] by ChanServ 18/06 12:16 pedagand: in your stratified system, does Pi bind a variable itself, or is it parametrized by a function? 18/06 12:33 right now, it is a function 18/06 12:34 I mean, parameterized by a function 18/06 12:35 Yeah, that's what the implementation suggests. 18/06 12:35 I 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 it 18/06 12:37 I'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 that's the good old issue 18/06 12:39 that's why I thought I'd check 18/06 12:39 the bind-a-var way might go through; I'll try it 18/06 12:40 if you bind, you can use the context-part of the GFTP and you ought to be safe 18/06 12:43 that's what I hope will happen 18/06 12:43 hmm, what's the easiest way to get a whiteboard on IRC? 18/06 12:45 I mean, a photo of a whiteboard 18/06 12:45 the same than what you do on tweeter? 18/06 12:46 yeah, I suppose I could just use twitter 18/06 12:47 did the STLC part make any sort of sense? 18/06 12:55 *made 18/06 12:56 It'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 as mentioned in the intro, nobody wants that :-) but it's easier to explain the machinery in that setting. 18/06 13:10 because, in the dependent case, the weird thing is that the machinery makes no sense 18/06 13:10 (or very little) 18/06 13:11 I'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 I'm working on it 18/06 13:29 this "pigworker has quit" is like a David Lynch movie for me: it's innocent, but hides a cruel question 18/06 14:38 has Conor left for the pub? Or for supervision? 18/06 14:38 life is tough :-) 18/06 14:39 -!- mode/#epigram [+v dolio] by ChanServ 18/06 15:16 -!- mode/#epigram [+v dolio] by ChanServ 18/06 16:20 -!- mode/#epigram [+v Saizan] by ChanServ 18/06 17:36 -!- mode/#epigram [+v Saizan] by ChanServ 18/06 19:41 -!- mode/#epigram [+v soupdragon] by ChanServ 18/06 19:59 -!- mode/#epigram [+v dolio] by ChanServ 18/06 21:16 --- Day changed Sat Jun 19 2010 -!- mode/#epigram [+v dolio] by ChanServ 19/06 01:16 -!- mode/#epigram [+v dolio] by ChanServ 19/06 05:19 how 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 pedegand: 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 pedagand 19/06 10:56 ha, ok, thanks 19/06 10:57 actually it says this on the website http://types10.mimuw.edu.pl/ 19/06 10:58 indeed, but that sounded so strange I couldn't believe it :-) 19/06 10:59 pedagand: :) has the deadline recently passed? 19/06 10:59 I've no clue 19/06 10:59 I cannot find any deadline, that's my other problem 19/06 11:00 nor can I find an indication of the page limit 19/06 11:00 I 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 tsapi, thanks 19/06 14:08 -!- mode/#epigram [+v codolio] by ChanServ 19/06 16:18 -!- mode/#epigram [+v dolio] by ChanServ 19/06 17:16 did Randy Pollack wrote a paper on implementing records in a dependent type-theory? dblp doesn't give anything 19/06 17:48 I know from pigworker and a mention in the Coq'art that he worked quite a lot on this topic 19/06 17:49 http://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 haha, interesting coincidence. Thanks again 19/06 17:56 :) 19/06 17:56 -!- mode/#epigram [+v dolio] by ChanServ 19/06 18:20 -!- mode/#epigram [+v dolio] by ChanServ 19/06 19:15 -!- mode/#epigram [+v codolio] by ChanServ 19/06 20:19 why 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 pedagand: I think we changed our minds about how we wanted that stuff to be implemented. 19/06 21:58 for no particular reason? :-) 19/06 22:00 probably 19/06 22:00 I think there's a neater way to deal with the indexing 19/06 22:01 ok, fair enough 19/06 22:01 The stuff in models/Containers.agda would work well enough 19/06 22:02 but it's also a real headf*ck to write that stuff in a fully explicit TT 19/06 22:02 you write "there's a neater ...": you mean, the current one is not perfect and you have a better story? 19/06 22:03 I have another version of that file somewhere 19/06 22:04 indeed, I've just implemented records and that was already too much headf* for me :-) 19/06 22:04 ok 19/06 22:04 if you look at that file there's a function called rearrange which is just one part of a dumb isomorphism 19/06 22:05 that we need to define it suggests that the pieces of the jigsaw are not quite sliding into place properly 19/06 22:06 I really want to internalise Mu/Nu in the Desc universe soon though 19/06 22:08 ha... long ago, the plan was to sort out "language with binders", so that the internal fix-points come easily 19/06 22:08 I mean, as we wrote in the conclusion of the Desc paper 19/06 22:09 I think the idea was that free monadic IDesc + a bit of machinery, we would get real substitution on IDesc 19/06 22:11 -!- mode/#epigram [+v dolio] by ChanServ 19/06 22:16 actually, models/FMSB is precisely about that 19/06 22:17 Binding not the whole of the story 19/06 22:19 *is 19/06 22:19 and since we haven't sorted binding out either ;) 19/06 22:19 oh, I trust you on that 19/06 22:20 I can't find that file, must have hidden it somewhere 19/06 22:20 to protect myself from the horrors contained within 19/06 22:21 :-) 19/06 22:24 -!- mode/#epigram [+v Saizan] by ChanServ 19/06 23:17 --- Day changed Sun Jun 20 2010 -!- mode/#epigram [+v dolio] by ChanServ 20/06 00:16 -!- mode/#epigram [+v Saizan] by ChanServ 20/06 07:39 -!- mode/#epigram [+v dolio] by ChanServ 20/06 10:18 -!- mode/#epigram [+v dolio] by ChanServ 20/06 12:15 I also copied xclock, hoping to use it to test if equis is working but I don't know how to invoke it 20/06 12:47 (wrong window) 20/06 12:47 in models/Records.agda (just pushed), I've been trying to play the "embedding a post-fix language" (Okasaki) in Agda 20/06 13:29 I fake polymorphism with an implicit {a : Set} 20/06 13:29 however, if I go into dependant arguments, Agda rightfully goes nuts on the resulting unification problem (I think) 20/06 13:29 is there a "dependant" trick to achieve a similar effect? 20/06 13:30 pedagand: this typechecks here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26398#a26398 20/06 13:49 brilliant! 20/06 13:50 that was the trick... 20/06 13:51 thanks 20/06 13:51 you're welcome :) 20/06 13:52 sadly, Epigram doesn't solve this kind of constraint apparently. Oh, well... 20/06 14:17 -!- mode/#epigram [+v codolio] by ChanServ 20/06 15:19 I am reading the paper "Why Dependent Types Matter". In it, in the very first code snippet, there is order x y <= rec x 20/06 18:31 What does the rec x mean herE? 20/06 18:31 Does it mean that we apply the recursive expansion of x? i.e. (1+x)? 20/06 18:35 Ok. Reading onwards answered the question. :) 20/06 18:37 I think it means "I am going to define this by structural induction on x" 20/06 18:43 which you can see they then go on to do 20/06 18:43 scriptdevil, "<=" is called the "by" gadget: it is given an elimination principle (rec x here) and it applies "elimination with a motive" strategy 20/06 18:52 most of them, for datatypes, it's a call to an induction principle 20/06 18:52 in Agda, for example, this machinery is hidden behind the pattern-matching abstraction. Here it's explicit. 20/06 18:52 it also means that we don't have/don't need an external "termination checker": when definition your function, you give the proof that it terminates 20/06 18:53 pedagand: 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 (I really need to read that paper) 20/06 18:59 ignorance 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 but you can also define your own 20/06 19:00 for example, there is "ship", the function doing substitution of equal for equal 20/06 19:01 also, from the basic induction principle of data-types, you can define others 20/06 19:01 for example, for Nat, we give you "simple induction" (H(0), H(n) -> H(n+1)) 20/06 19:02 yes, sounds nifty 20/06 19:02 but you can go on defining "strong induction" 20/06 19:02 actually, Adam has defined strong induction "generically" for an inductive data-type (I think) 20/06 19:02 using your levitation stuff? that sounds very cool 20/06 19:02 yes, but you can do it anywhere. That's Gimenez strong induction principles, or Conor's memoization technique 20/06 19:03 just that, in this case, we can do it inside the type theory 20/06 19:04 yes, well, that's the cool part 20/06 19:04 now, the "basic" one for datatypes, that must be built in? (I mean, could you define it within epigram?) 20/06 19:04 yes, indeed 20/06 19:04 I can't wait to start playing with epigram2... maybe after the popl deadline I'll have time 20/06 19:06 yes (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 :-) 20/06 19:07 this is not good for mental health to have such self-definition :-) 20/06 19:07 pedagand: that's what I figured, but sometimes I'm confused by where the levitation technique bottoms out 20/06 19:07 me too, I'm afraid 20/06 19:08 :) 20/06 19:08 there'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 but 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 (provided you give yourself a Mu at each level, and so on) 20/06 19:12 Saizan, 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 recursion 20/06 19:13 I heard a discussion, but I'm not really a proponent on that story 20/06 19:13 the idea seems to be that currently Haskell is being developed over some more and more System-F-ish system 20/06 19:14 Conor's idea is to express Haskell's concepts in Martin-Lof type theory 20/06 19:14 I hope I'm not spoiling any industrial secret! :-) 20/06 19:14 hehe :) 20/06 19:14 a cool idea - though a pain for the implementor, considering how often the haskell core changes! 20/06 19:15 I think it's more meant toward "formalising Haskell", and having some confidence when you add features to it 20/06 19:15 like what your boss is currently doing, I heard ;-) 20/06 19:16 Yes :) Well, it seems someone is always doing it, for the current definition of "Haskell" 20/06 19:17 an embedding into a more expressive language would be very nice, though 20/06 19:17 that would also be great fun to write Haskell interactively! that's what hooked me 20/06 19:18 neat 20/06 19:19 though I'll believe it's faster to write haskell from inside a type theory when I see it :) 20/06 19:20 :-) 20/06 19:23 Ok. 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 there is also Nordgstrom [http://www.citeulike.org/user/pedagand/article/2310446] 20/06 19:32 *Nordstrom 20/06 19:32 but I couldn't tell if Thompson is better than Nordstrom, they are just "different" 20/06 19:33 are 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 I 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 this one is also good: http://www.cs.nott.ac.uk/~txa/lof.pdf 20/06 19:37 but there is nothing /really good/ I don't think 20/06 19:38 scriptdevil: 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 knowledge 20/06 19:38 tsapi, you're really proud of your warez copy of Martin-Lof, aren't you? :-) 20/06 19:38 somebody should write a type theory textbook 20/06 19:38 :) 20/06 19:38 nothing to do with me :) 20/06 19:39 I just know a guy... 20/06 19:39 ;-) 20/06 19:40 Ok. I got those books. Thank you :) 20/06 20:09 -!- mode/#epigram [+v dolio] by ChanServ 20/06 21:19 --- Day changed Mon Jun 21 2010 -!- mode/#epigram [+v dolio] by ChanServ 21/06 02:18 -!- mode/#epigram [+v dolio] by ChanServ 21/06 05:19 -!- mode/#epigram [+v Saizan] by ChanServ 21/06 06:03 -!- mode/#epigram [+v pigworker] by ChanServ 21/06 07:31 -!- mode/#epigram [+v pigworker_] by ChanServ 21/06 07:43 -!- pigworker_ is now known as pigworker 21/06 07:43 -!- mode/#epigram [+v dolio] by ChanServ 21/06 08:19 -!- mode/#epigram [+v codolio] by ChanServ 21/06 09:18 moleris, have you read the literature on Joyal's "analytic functors" and other "species"? 21/06 11:40 pedagand: I have 21/06 11:50 ha, great! Do you have a recommended reference to get into that? 21/06 11:51 do you recommend reading this sort of stuff, btw? Or you had the feeling of "wasting your time"? 21/06 11:52 as 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 The book "Combinatorial Species and Tree-like Structures" is a reasonable place to start, if you can find it on the shelves of a colleague 21/06 12:07 it'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 ok, thanks 21/06 12:15 pedagand: Btw, you give me too much credit there are plenty of HF terms left to kill 21/06 12:43 I did not checked actually, I trusted my misinterpretation of your commit message :-) 21/06 12:48 but, well, greping for HF tells me that you eradicated most of them 21/06 12:49 there is one in Prop, the others are not really problematic. In particular, Problem is not connected to the system, FreeMonad is bound to disappear 21/06 12:50 so, no, you deserve a round of applause :-) 21/06 12:51 ha, I missed OpDef and Elab: one HF each. 21/06 12:52 I see more than that 21/06 12:55 What about PropSimp.lhs? 21/06 12:56 Also, as I discussed with pigworker there's a problem with Telescopes 21/06 12:56 oops, missed that one too :-) Do like me, stare at your terminal very quickly, life is much better at high-glaring speed 21/06 12:57 what's wrong with Hubble again? 21/06 12:58 PropSimp, looked like a big change so I left it. Maybe I should have filed a issue in the bug tracker instead 21/06 12:59 yep, you should: this World cup is too much of a pain, I'd rather fix bugs than watching it :-) 21/06 13:02 pedagand: I don't blame you... 21/06 13:02 PropSimp needs some thought, preferably by someone other than me 21/06 13:03 Heh, at least France's pain is almost over, I have a feeling England could conspire to make our hell last a few days longer 21/06 13:03 Telescopes are inescapably higher order at them moment 21/06 13:05 There's a question about how much we really need them now, too... It is not a coincidence they were introduced soon after the HF constructor 21/06 13:07 agundry, hehe. Btw, what kind of thought does PropSimp need? 21/06 13:11 moleris, yes, that's true 21/06 13:12 pedagand: it would be nice if the simplification rules were clearer and more obviously terminating 21/06 13:13 ha, ok, sure. 21/06 13:14 I also suspect it could be made a lot more efficient by removing all the discharges 21/06 13:14 maybe this relates to figuring out how to remove the HFs 21/06 13:14 agundry: I should hope that would be the case 21/06 13:14 or at least that process can be made a lot cheaper 21/06 13:15 I've been experimenting with having problem simplification invoke elimination to substitute out equations 21/06 13:16 this seems to work but it is incredibly slow 21/06 13:16 -!- agundry is now known as agundry_away 21/06 14:24 -!- agundry_away is now known as agundry 21/06 15:25 afternoon all! (it's bloody early here, but that's jetlag) 21/06 15:41 pigworker: good afternoon, modulo timezones 21/06 15:42 If 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 Hmm, you mean we could write operator types in Epigram and parse them at runtime? 21/06 15:49 meanwhile, do we have a clear on-paper characterization of what PropSimp does? 21/06 15:49 not really, that's part of the problem 21/06 15:49 I tried to find a nice way of writing down simplification rules, but didn't succeed 21/06 15:50 agundry: parse at run time, or translate Epigram-with-Haskell-bits to Haskell in preprocessing 21/06 15:50 For PropSimp, I'd try a sequent calculus presentation. 21/06 15:51 tricky to demo in IRC 21/06 15:52 that was roughly what I tried: there are a few scribblings in the PropSimp.lhs file 21/06 15:54 A, B, Delta |- P <=> A /\ B, Delta |- P 21/06 15:54 the problem is finding a notation for the isomorphisms between proofs 21/06 15:55 it's be a start to know what the rules are at the problem level, then refine them with realizers 21/06 15:56 it'd 21/06 15:56 true 21/06 15:56 for 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 defining 21/06 15:57 something of the sort; I'd rather we did it at compile-time, of course, but I realise that complicates the build process 21/06 16:00 I guess we could use quasi-quotation or similar trickery 21/06 16:02 yeah; or maybe we can just improve the brevity of working with terms in Haskell 21/06 16:03 that would be useful elsewhere as well, I suspect 21/06 16:04 a lot of the turgid wrappering can be hidden with typeclass tomfoolery 21/06 16:05 a 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 info 21/06 16:07 gotta get clean and face the day; more later 21/06 16:10 okay, bye for now 21/06 16:12 moleris, 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 I guess, sumilike, although being applied late during distillation, still counts as an operator in the definition 21/06 17:06 (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 pedagand: sumilike is only used for elaborating and distilling tags with arguments 21/06 17:11 so I don't see why it would cause you problems 21/06 17:11 is that "distill es (IMU l _I s i :>: CON (PAIR t x))" what you call "tags with arguments"? 21/06 17:12 just to check 21/06 17:13 yes 21/06 17:14 the idea is that t will be distilled to a tag (an element of UId) applied to the list that x distills to 21/06 17:17 hehe, goodo 21/06 17:18 thanks 21/06 17:20 no problem 21/06 17:21 -!- mode/#epigram [+v Saizan] by ChanServ 21/06 19:26 -!- mode/#epigram [+v Saizan_] by ChanServ 21/06 22:34 -!- Saizan_ is now known as Saizan 21/06 22:34 --- Day changed Tue Jun 22 2010 -!- mode/#epigram [+v Saizan] by ChanServ 22/06 01:10 -!- mode/#epigram [+v Saizan] by ChanServ 22/06 05:05 -!- mode/#epigram [+v Saizan] by ChanServ 22/06 13:24 -!- mode/#epigram [+v soupdragon] by ChanServ 22/06 17:58 -!- mode/#epigram [+v Saizan_] by ChanServ 22/06 18:26 -!- Saizan_ is now known as Saizan 22/06 18:26 --- Day changed Wed Jun 23 2010 edwinb, so England qualified finally? 23/06 17:08 yes. They were rubbish though. 23/06 17:10 ha, well. I can hardly blame any team for being rubbish, my nationality prevents that :-) 23/06 17:13 well. indeed. 23/06 17:15 it doesn't stop the Scots ;) 23/06 17:15 :-) 23/06 17:17 -!- mode/#epigram [+v Saizan] by ChanServ 23/06 19:36 --- Day changed Thu Jun 24 2010 -!- mode/#epigram [+v Saizan] by ChanServ 24/06 09:29 building cabal's 'she' fails for me; anyone else have this problem? 24/06 19:06 just tried and got a compiler panic, though I'm running an ancient version of ghc (6.10.3) 24/06 19:08 i'm running ghc-6.8.2, which is the latest mainstream ubuntu package, apparently 24/06 19:09 considering that she is all about fancy type hacks, a new version is probably required 24/06 19:09 also I just checked and ghc 6.12.1 is in apt on ubuntu lucid 24/06 19:10 hmm i'll have to figure out how to get that 24/06 19:11 ubuntu's bad for this sort of thing though - ghc changes fast and ubuntu keeps packages at the same version for the duration of a release 24/06 19:12 better off just downloading and installing ghc binaries directly 24/06 19:12 ok 24/06 19:15 on 6.12.1 she seems to build fine - just tried on a different computer 24/06 19:15 thanks for the info 24/06 19:17 does epigram aim to eventual self-hosting? 24/06 19:18 hmm building ghc from source requires a new ghc binary than i already have. curiouser and curiouser 24/06 19:21 it also takes hours - binaries highly recommended 24/06 19:22 the main challenge as a haskell programmer i can tell so far seems to be setting up the environment :/ 24/06 19:25 it's usually pretty painless! Though the current transition to the "haskell platform" may be confusing things 24/06 19:28 your best bet is probably just installing the 6.12.1 binary and then building the platform from source 24/06 19:30 http://hackage.haskell.org/platform/linux.html 24/06 19:30 thanks 24/06 19:41 hmmm, building from source breaks. time to try 6.12 binary... 24/06 19:50 6.12.1 binaries installed; now to build haskellplatform which should replace my old cabal and friends... 24/06 20:10 Registering she-0.1... \o/ 24/06 20:22 pizza@ubuntu:~/src/Pig09/src$ make dep 24/06 20:30 ghc: could not execute: she 24/06 20:30 where did she get installed and is it on your path? 24/06 20:31 .cabal/bin is a common place 24/06 20:31 ah 24/06 20:31 there we go 24/06 20:31 -!- mode/#epigram [+v Saizan] by ChanServ 24/06 20:35 im doing the "two plus two" example; what does the "^1" in Programming: < plus^1 m n : Nat > mean? 24/06 20:40 I'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 ha :) 24/06 20:41 for example, the following are equivalent: \x -> \y -> x   and \ x -> \ x -> x^1 24/06 20:41 the "^i" gives you the De Bruijn index when there is shadowing in the context 24/06 20:41 in this case, this comes from the way "plus" as a labelled type has been defined in the proof state. 24/06 20:42 put otherwise, you're observing an implementation artifact 24/06 20:43 sorry about that. I warned you: it's the bleeding edge as in "gosh, it cuts!" :-) 24/06 20:44 Vec.Ind from the demo seems to be even sharper! :) 24/06 20:46 ha, don't tell me about this demo. If it were just me, I would have called it "public humiliation session" 24/06 20:47 imagine, we struggled half an hour to define "+" 24/06 20:47 why is that humiliating? 24/06 20:47 I ruined all my chances to get by with the good looking girl which got attracted by our emacs buffer :-) 24/06 20:48 lol 24/06 20:48 ah, you didn't have the script ready? 24/06 20:48 pizza_, I'm kidding ;-) 24/06 20:48 Saizan, 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 so, 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 plus 24/06 20:50 and the Java guy next to you suddenly looks like a promising mate 24/06 20:50 damnit! :-) 24/06 20:50 ahahahah :D 24/06 20:50 i can understand why there's no explanation for vhead then :) 24/06 20:53 the 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 I suddenly remembered that many languages had been invented for the sole purpose of building applications. Gosh :-) 24/06 21:01 :) 24/06 21:03 was this a demo at the oregon summer school? 24/06 21:03 no, a local event here in Edinburgh 24/06 21:03 ah 24/06 21:04 long ago, Conor expressed the desire to do his lecture with Epigram 24/06 21:05 I saw conor is giving dependently typed programming lecture there - are they in epigram? 24/06 21:05 but reality caught up :-) 24/06 21:05 alas 24/06 21:05 so much cool stuff there this year 24/06 21:05 I believe his lecture is based on some induction recursion madness. So, Epigram is out of the game anyway 24/06 21:05 (that's the politically correct reason, anyway) 24/06 21:06 :) 24/06 21:06 is he using agda? 24/06 21:07 well, I don't know, he alluded that his lectures would be based on his recent "type theory in itself" paper 24/06 21:08 but he wrote the lecture in the plane to Oregon apparently, so I can't say for sure 24/06 21:08 Epitome.pdf S1.2 "This is all very tenative." 24/06 22:19 is it a quote from the text? I cannot find it. Or it's your opinion about it? :-) 24/06 22:40 copy-and-pasted from the pdf 24/06 22:42 Hu 24/06 22:42 bottom of p.7 24/06 22:42 I recompile the pdf, might take a few hours 24/06 22:43 ha, got it 24/06 22:44 the syntax... I suspect that your friend to get into this maze is to look at Syntax.pig in the test directory 24/06 22:47 if you haven't already 24/06 22:47 i did, it was a bit overwhelming 24/06 22:47 hard for me as a programmer to differentiate between built-in stuff and stuff being defined 24/06 22:48 well, this syntax is overwhelming *by design*, anyway. 24/06 22:48 :) 24/06 22:48 there is not many built-in stuffs, that's one of the (many) craziness of the language. 24/06 22:49 are you familiar with Agda for instance? 24/06 22:49 or Coq maybe? 24/06 22:50 I 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 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 me 24/06 22:51 well, 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 have 24/06 22:53 yup ok 24/06 22:55 but don't misread me: I'm not bothered to answer questions :-) 24/06 22:55 you have been most kind and helpful 24/06 22:57 you're welcome 24/06 22:57 --- Day changed Fri Jun 25 2010 -!- mode/#epigram [+v Saizan] by ChanServ 25/06 01:55 -!- mode/#epigram [+v Saizan] by ChanServ 25/06 02:00 -!- mode/#epigram [+v soupdragon] by ChanServ 25/06 18:33 --- Day changed Sat Jun 26 2010 sometimes a deadline extension is the last thing you want... 26/06 00:30 what you need is a good spam filter then :-) 26/06 00:48 so that you don't know that there has been an extension and you just ship this damned paper 26/06 00:48 which workshop is it? 26/06 00:49 http://www.cs.unibo.it/~asperti/mscs 26/06 00:52 well, good luck with that! it's about a comonadic story? 26/06 00:55 relative monads in agda 26/06 00:55 thanks :) 26/06 00:56 ho, interesting. Let us know when you've a draft, it could accidentally on reddit :-) 26/06 00:57 ok :) 26/06 01:00 -!- mode/#epigram [+v Saizan] by ChanServ 26/06 02:13 -!- mode/#epigram [+v Saizan] by ChanServ 26/06 13:24 --- Day changed Sun Jun 27 2010 -!- mode/#epigram [+v Saizan] by ChanServ 27/06 14:10 -!- mode/#epigram [+v Saizan] by ChanServ 27/06 15:27 -!- mode/#epigram [+v Saizan] by ChanServ 27/06 16:26 -!- mode/#epigram [+v Saizan] by ChanServ 27/06 17:12 tsapi, do you have a definition of relative monads in Agda, by any chance? 27/06 19:10 if not, no problem, it's just me being lazy. I would need one in Epigram 27/06 19:10 pedagand: I do it's a question of where to put it 27/06 19:31 the repo isn't online 27/06 19:31 pedagand: 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 week 27/06 19:32 ok, thanks 27/06 19:33 but if you're busy with other things, don't le me distract you, that's not urgent 27/06 19:35 s/le/let/ 27/06 19:36 not busy, spent the cycling 27/06 19:43 spent the day cycling 27/06 19:43 that sounds quite busy 27/06 19:44 tsapi, got your mail, thanks 27/06 21:23 --- Day changed Mon Jun 28 2010 -!- mode/#epigram [+v Saizan] by ChanServ 28/06 03:16 -!- mode/#epigram [+v Saizan] by ChanServ 28/06 05:21 -!- mode/#epigram [+v Saizan] by ChanServ 28/06 05:45 -!- mode/#epigram [+v Saizan] by ChanServ 28/06 09:18 -!- mode/#epigram [+v Saizan] by ChanServ 28/06 19:05 -!- mode/#epigram [+v soupdragon] by ChanServ 28/06 22:43 --- Day changed Tue Jun 29 2010 -!- mode/#epigram [+v dolio] by ChanServ 29/06 00:45 -!- mode/#epigram [+v dolio] by ChanServ 29/06 01:15 -!- shapr[ is now known as shapr 29/06 02:34 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 05:12 -!- mode/#epigram [+v dolio] by ChanServ 29/06 06:23 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 07:23 -!- mode/#epigram [+v dolio] by ChanServ 29/06 08:19 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 08:38 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 09:44 -!- mode/#epigram [+v dolio] by ChanServ 29/06 10:19 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 10:47 -!- mode/#epigram [+v Saizan] by ChanServ 29/06 11:19 -!- mode/#epigram [+v pigworker] by ChanServ 29/06 13:37 -!- mode/#epigram [+v soupdragon] by ChanServ 29/06 15:46 -!- mode/#epigram [+v dolio] by ChanServ 29/06 17:22 -!- mode/#epigram [+v pigworker] by ChanServ 29/06 18:14 -!- mode/#epigram [+v dolio] by ChanServ 29/06 19:19 -!- mode/#epigram [+v dolio] by ChanServ 29/06 20:23 pigworker: So, I heard you already know how to turn induction-induction into just induction (or, inductive families). 29/06 20:39 Although, I'm not super convinced the translation someone gave me covers everything. 29/06 20:43 There's something like a preterms and goodness-judgments translation (which relies on proof-irrelevance for goodness). 29/06 21:03 Can't say I've defined it formally, though. 29/06 21:04 -!- mode/#epigram [+v codolio] by ChanServ 29/06 21:22 -!- codolio is now known as dolio 29/06 21:36 pigworker: 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 Whereas that translation looks like it's just a way of carving out parts of things you could write anyway. 29/06 21:45 I-I can't do "big" like I-R can, it's true. 29/06 22:04 I 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 Yeah, that's kind of been on my mind, along with the erasure stuff. 29/06 22:08 I seem to recall hearing that one of the ideas behind parametricity is "when is it okay to be impredicative?" 29/06 22:09 It might be ok to have data Foo : Set where foo : /\ X : Set -> Foo, for a silly example. 29/06 22:10 But, I've been lazily avoiding working on my implementation of the EPTS (and associated) stuff. 29/06 22:11 But if intersection erases only at run-time, that might just affect which phases one can screw up at. 29/06 22:11 So 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 Lots of variables to tweak there. 29/06 22:13 I wonder if Alexandre Miquel already knows what works. 29/06 22:15 -!- mode/#epigram [+v dolio] by ChanServ 29/06 22:23 -!- mode/#epigram [+v pigworker] by ChanServ 29/06 23:18 --- Day changed Wed Jun 30 2010 -!- mode/#epigram [+v dolio] by ChanServ 30/06 00:22 -!- mode/#epigram [+v dolio] by ChanServ 30/06 01:55 -!- mode/#epigram [+v dolio] by ChanServ 30/06 02:22 -!- mode/#epigram [+v pigworker] by ChanServ 30/06 03:14 -!- mode/#epigram [+v dolio] by ChanServ 30/06 05:19 -!- mode/#epigram [+v Saizan] by ChanServ 30/06 05:39 -!- mode/#epigram [+v dolio] by ChanServ 30/06 06:19 -!- mode/#epigram [+v Saizan] by ChanServ 30/06 09:10 -!- mode/#epigram [+v dolio] by ChanServ 30/06 10:19 -!- mode/#epigram [+v pigworker] by ChanServ 30/06 10:32 -!- mode/#epigram [+v Saizan] by ChanServ 30/06 11:37 pedagand: hi, how are you? 30/06 12:05 It's time I went to school. 30/06 12:14 -!- mode/#epigram [+v codolio] by ChanServ 30/06 13:21 -!- mode/#epigram [+v dolio] by ChanServ 30/06 14:22 -!- mode/#epigram [+v pigworker] by ChanServ 30/06 19:00 -!- mode/#epigram [+v dolio] by ChanServ 30/06 21:23 -!- mode/#epigram [+v dolio] by ChanServ 30/06 22:19