abstractstone abstractstone abstractstone --- Log opened Wed Dec 01 00:00:20 2010 I need to solve this: 01/12 00:04 data Nat := ('zero : Nat) ; ('suc  : Nat -> Nat); 01/12 00:04 let foo : :- (: Nat) ('zero) == (: Nat) ('zero) ; 01/12 00:04 give refl ; 01/12 00:04 it gives the error: I'm sorry, Dave. I'm afraid I can't do that. 01/12 00:04 Error: elabGive: only possible for incomplete goals. 01/12 00:04 but if you go root ; elab foo ; it prints _ 01/12 00:05 In a situation like this: 01/12 00:06 foo_1.impl_2 > show context 01/12 00:06 Nat : Set 01/12 00:06 foo-type : Set 01/12 00:06 foo : (c : < _ : :- ((: Nat) 'zero) == ((: Nat) 'zero) >) -> :- ((: Nat) 'zero) == ((: Nat) 'zero) 01/12 00:06 what do you do? 01/12 00:06 make foo := refl Nat 'zero : :- (: Nat) ('zero) == (: Nat) ('zero) ; 01/12 00:07 works 01/12 00:07 what does elab foo gives after that? 01/12 00:08 oh it still gives _ 01/12 00:08 that's weird 01/12 00:08 oh maybe it does that for all props 01/12 00:09 it's just that (: Nat) ('zero) == (: Nat) ('zero) reduces to TT (or however the unit type is called, i'm not sure), and _ is how the inhabitant gets pretty printed 01/12 00:09 so, "let foo : :- (: Nat) ('zero) == (: Nat) ('zero) ;" was a complete definition of foo, because _ was filled in directly 01/12 00:10 ah thank you 01/12 00:10 how can you tell when a complete definition has been given? 01/12 00:11 if it doesn't give you the type of the next goal, i guess 01/12 00:13 let R_trans (z : Zahl) (w : Zahl) (y : Zahl) : :- R z w => R w y => R z y ; 01/12 00:21 <= Pair.Ind Nat Nat z ; 01/12 00:21 <= Pair.Ind Nat Nat w ; 01/12 00:21 <= Pair.Ind Nat Nat y ; 01/12 00:21 gives this goal: 01/12 00:22 let R_trans (z : Zahl) (w : Zahl) (y : Zahl) : :- R z w => R w y => R z y ; 01/12 00:22 <= Pair.Ind Nat Nat z ; 01/12 00:22 <= Pair.Ind Nat Nat w ; 01/12 00:22 <= Pair.Ind Nat Nat y ; 01/12 00:22 oops 01/12 00:22 Programming: < R_trans ('both a^1 a) ('both a^3 a^2) ('both a^5 a^4) : R_trans-type.h14 ('both a^1 a) ('both a^3 a^2) ('both a^5 a^4) > 01/12 00:22 I need to unfold the definition of R_trans-type.h14 somehow? 01/12 00:23 I want to get something like  :- a^1 + a^2 == a^3 + a => ... 01/12 00:24 http://proggit.pastebin.com/tQuBZHiH 01/12 00:28 I will need the lemmas X=Y & Z=W -> X+Z=Y+W, as well as a+d+c+f=c+b+e+d -> a+f = b+e 01/12 00:29 but right now I just want to get R_trans into a state where I can apply these lemmas (assuming I had them) 01/12 00:30 really difficult to get started on this language with so little example code 01/12 00:42 http://proggit.pastebin.com/spCzsns4 - How do I name a^i in this? 01/12 00:44 lambda a ;  doesn't work 01/12 00:44 --- Day changed Fri Dec 03 2010 dead channel is dead? 03/12 20:41 nope 03/12 20:48 oh goody 03/12 20:50 There hasn't been much activity on the darcs repo either. I was wondering if things were still progressing? 03/12 20:50 I haven't actually tried it, mostly because the SHE requirement is scary? 03/12 20:50 * roconnor hasn't used epigram 03/12 20:51 :D 03/12 20:51 Taral: the epigram developers are probably mostly in BST or maybe a few in CEST. 03/12 20:51 I know. :( 03/12 20:52 All the fun stuff happens in Europe. 03/12 20:52 Taral: she is not that scary 03/12 21:35 it doesn't even eat all your ram if you use the darcs version :) 03/12 21:35 where's the darcs version? 03/12 21:48 aha 03/12 21:48 how long before we have epigram on epigram? 03/12 21:49 http://personal.cis.strath.ac.uk/~conor/pub/she <- in case you haven't found it 03/12 22:01 * Saizan_ doesn't know 03/12 22:01 I got it. 03/12 22:01 Compiling darcs first :D 03/12 22:02 i've seen pigworker write that the missing piece to implement a dep. typed language in itself is some good tech for constraint solving 03/12 22:04 http://pastebin.com/nTAxGGiq 03/12 22:07 # 03/12 22:07 I have to prove:  let thmZahlthing (a : Nat) (b : Nat) (c : Nat) (d : Nat) (e : Nat) (f : Nat) (p1 : :- plus a d == plus c b) (p2 : :- plus c f == plus e d) : :- plus a d == plus e b ; 03/12 22:07 there is too much commutativity and associativity,  I can't write it out the in usual way: any ideas? 03/12 22:08 I started writing the proof but it doesn't check the validity as you go: It adds coercions whenever you put X instead of Y 03/12 22:12 What is ? 03/12 22:12 refine thmplusCancel 'zero a b = ? ; 03/12 22:12 it's a hole, simpl fills it in 03/12 22:12 interesting. 03/12 22:13 simpl isn't in the manual yet 03/12 22:13 help simpl  in the Epigram prompt 03/12 22:18 and help lists commands 03/12 22:18 mhm! 03/12 22:19 I don't see how this theorem is true. 03/12 22:19 oh, I see. 03/12 22:19 a+d = c+b,c+f=e+d 03/12 22:21 (a+d)+(c+f) = (c+b)+(e+f) 03/12 22:21 ... 03/12 22:21 (c+f)+(a+d) = (c+f)+(e+b) 03/12 22:21 a+d=e+b 03/12 22:21 each line is one use of 'trans' 03/12 22:22 I don't know the most efficient way to fill the ... part - that's why I am stuck 03/12 22:22 trans is a no-op 03/12 22:22 I mean efficiency in terms of how much I have to type :P 03/12 22:23 what I wrote above is wrong 03/12 22:26 well 03/12 22:27 thmZahlthing_10.impl_2 > = thmplusCancel (plus c f) (plus a d) (plus e b) ? 03/12 22:27 Ta. 03/12 22:27 Goal: :- (plus (plus c f) (plus a d)) == (plus (plus c f) (plus e b)) 03/12 22:27 if you want to use backwards reasoning 03/12 22:27 annoying that it won't infer holes from types 03/12 22:28 I have been trying to prove the wrong thing, it should be :- plus a f == plus e b 03/12 22:31 oho 03/12 22:32 what would be ideal is if I could just operate directly on the goal equation 03/12 22:35 looking... 03/12 22:35 that mgiht ahve to be a feature though 03/12 22:35 I wish I understood what a "programming problem" really is. 03/12 22:39 you mean the angle brackets thing? 03/12 22:39 Programming: < thmZahlthing a b c d e f p1 p2 : :- (plus a d) == (plus e b) > 03/12 22:40 yeah 03/12 22:40 it's kind of interesting 03/12 22:40 interesting question 03/12 22:41 I think part of it is to make sure you do recursion properly (no infinnite loops) 03/12 22:42 infer equalFun Nat Nat (\ (x : Nat) -> plus x c) (plus b a) (plus a b) (thmplusComm b a) ; 03/12 22:51 it's not parsing my (\ (x : Nat) -> plus x c) part 03/12 22:51 er 03/12 22:52 ah it works without the : 03/12 22:52 : Nat 03/12 22:52 Hm. 03/12 22:54 Looks like much of this machinery is not implemented. 03/12 22:55 http://proggit.pastebin.com/xYXqYhWL 03/12 22:56 that's where I am at now: just have to put those equations together 03/12 22:56 what's equalFun? 03/12 22:57 let equalFun (X : Set) (Y : Set) (f : X -> Y) (a : X) (b : X) (P1 : :- a == b) : :- f a == f b ; 03/12 22:57 root ; 03/12 22:57 oh 03/12 22:57 lots of basic facts about equality seem to get proved automatically (I don't really know how ...) 03/12 22:57 :) 03/12 22:58 magic. 03/12 22:58 using the rules: 03/12 23:22 { X+Y == Y+X } { X+(Y+Z) == (X+Y)+Z } 03/12 23:22 best I can do so far is (a+b)+(c+f) = a+(b+(c+f)) = b+(a+(c+f)) = b+((a+c)+f) = b+(f+(a+c)) = b+((f+a)+c) = b+(c+(f+a)) = (b+c)+(f+a) = (c+b)+(f+a) = (b+c)+(a+f) 03/12 23:22 I don't think I can get epigram to accept that 03/12 23:23 I think I need a better set of rules 03/12 23:24 programming with Epigram right now is a pain 03/12 23:24 it might be a bit painful but it should be straightforward if you first define transitivity and congruence for == 03/12 23:24 those exist already 03/12 23:24 have you written much Taral ? 03/12 23:26 no 03/12 23:27 because it's a pain 03/12 23:28 most of the infrastructure is missing 03/12 23:28 what infrastructure? 03/12 23:28 backwards reasoning, for one. 03/12 23:29 there's "apply", but it only works if you do crazy things with the proof state. 03/12 23:29 and is very specific 03/12 23:29 and doesn't work on programming problems 03/12 23:29 can you give an example? 03/12 23:31 what, apply? 03/12 23:32 of some infrastructure for backwards reasoning, how/when it'd be useful 03/12 23:33 i've only used Agda and Twelf as theorem provers, afaiu they don't have things like that? 03/12 23:34 So if your goal is T and you have x :  S -> T in the environment, you don't have "apply x"? 03/12 23:35 ah, i see, in Agda you'd write (x ?) as the term you want to use to prove T, ? is the placeholder for a new goal 03/12 23:39 sure, you can try that here. 03/12 23:39 yeah 03/12 23:39 it makes a mess 03/12 23:39 really? 03/12 23:39 yes 03/12 23:39 for one, there's little to no inference in the system 03/12 23:40 so you have to do (x Abigthing Bbigthing ?) 03/12 23:40 and second, that doesn't make a new programming problem 03/12 23:40 it makes a hole which is a standard propositional thing 03/12 23:40 and thus your environment gets hidden in an upper layer 03/12 23:40 i see, i didn't notice those problems 03/12 23:41 what were you trying to do? 03/12 23:42 try abstractstone's problem, you'll see 03/12 23:43 I've been working on this for wees 03/12 23:43 weeks 03/12 23:43 i've only played at little with the cofree comonad in the past, where there wasn't even refine :) 03/12 23:44 *when 03/12 23:44 --- Day changed Sat Dec 04 2010 http://pastebin.com/gkY4w9wP 04/12 00:03 doing this kind of arithmetic is annoying. 04/12 00:04 I bet there's quite a lot of things here that could be improved 04/12 00:04 in coq there are tactics to auto-solve these things 04/12 00:04 Taral: there is a thing for automatically solving prop proofs 04/12 00:04 so you could probably add arithmetic as a feature too 04/12 00:05 I wouldn't. 04/12 00:05 wuoldn't what? 04/12 00:05 They're separate tactics in coq for a reason. 04/12 00:05 You don't want to add that to the simplifier. 04/12 00:05 I'm out for a bit. 04/12 00:09 ttyl 04/12 00:09 --- Day changed Mon Dec 06 2010 Good morning. 06/12 18:08 --- Day changed Thu Dec 09 2010 Just passing through... will probably have to get back to shovelling shortly. 09/12 09:51 --- Day changed Fri Dec 10 2010 * edwinb wonders if anyone here has any ideas about the evilness he wants to do with Epic 10/12 14:22 it seems to me it ought to be possible to steal Haskell syntax 10/12 14:23 especially if what you want to do is write your own operators 10/12 14:23 but to do this, and write out actual code, I need to convert arbitrary top level haskell identifiers to strings 10/12 14:23 there must be some evilness in the libraries somewhere that lets me do this... 10/12 14:23 from within haskell? 10/12 15:12 TemplateHaskell has 'foo (or ''Foo for types) which gives you a Name that you can convert to String with show 10/12 15:13 Hmm, I wonder if that might do it 10/12 15:18 * edwinb has a look, cheers 10/12 15:18 though you have to use it on the identifier directly 10/12 15:20 ooh! I think that's exactly what I'm after 10/12 15:20 thanks :) 10/12 15:20 np :) 10/12 15:21 --- Day changed Sat Dec 11 2010 Has there still been no sign of soupdragon? 11/12 23:48 no signs 11/12 23:59 --- Day changed Sun Dec 12 2010 When or why did s?he disappear? 12/12 00:03 I just pushed another patch to http://personal.cis.strath.ac.uk/~conor/fooling/Spiny.lhs 12/12 18:38 Now, any old crap like  la$\f -> f (la$ \x -> f x x)  just evaluates to the relevant de Bruijn term. 12/12 18:40 I just hope ghc's inliner gets busy with code like that... 12/12 18:42 maybe an INLINE pragma for la would help, though one should check the core first 12/12 18:47 Funny that someone asked on stackoverflow today about the impact of changing your data structures on your code base... 12/12 18:47 Saizan: from the little I understand, it's a good candidate anyway, unless its type is just too scary 12/12 18:48 it's small and non-recursive, so that's true 12/12 18:56 Gaaah. I was hoping to use more typeclass voodoo to iterate the lambda, but I'm not allowed polytypes in constraints. 12/12 19:05 The overall plan is to remove the deep separation of terms and values which causes so much of a headache in the Epigram 2 source. 12/12 19:33 values would be things of type Nm here? 12/12 19:43 yeah, but they're only head-normal 12/12 20:01 crucially, you can use that type to ensure that head-normalisation happens -- it's a type error to forget (I need that) 12/12 20:03 moleris: I forget; was there a way to persuade Epilogue to do the right thing with Haskell code? 12/12 20:11 I seem to get [lhs2TeX] happening sometimes. 12/12 20:12 First instalment of the blogged code http://www.e-pig.org/epilogue/?p=706 12/12 23:34 pigworker: that's great, thanks :D 12/12 23:40 --- Day changed Mon Dec 13 2010 * Saizan wonders when one would use Nix 13/12 00:30 Saizan: not sure about Nix; I seem to have built its main use case into the type of W (embedding closed whnfs as open heads). 13/12 10:05 pigworker: Ping 13/12 14:41 wotcher 13/12 14:42 Just reading through the blog post - I see you got the blog to do the haskell thing 13/12 14:42 yeah, cut into small enough lumps, it kind of works; weird arrows... 13/12 14:43 if you ever feel like writing agda in a blog post, I have the world's worst highlighter of agda for you (which will eventually improve when I finish moving) 13/12 14:43 copumpkin: that does sometimes happen... 13/12 14:44 good luck with the move, and... don't fret about unicode on my account! 13/12 14:44 hah, that much already works :P 13/12 14:44 https://github.com/pumpkin/agda-highlight and some of its output is at http://pumpkinpat.ch/moo.html 13/12 14:45 I'll get there eventually. 13/12 14:45 Three lectures left this term, but a big pile of labs as well. 13/12 14:46 ack :) 13/12 14:46 Snow expected on Thursday, so it's panic stations now. 13/12 14:47 Snow is good for pigs but bad for young goats. 13/12 14:47 :| 13/12 14:47 when I said I was reading the blog post, in fact I was fixinging the horrid font and arrows - results now up for all to appreciate 13/12 14:48 Sweet! 13/12 14:49 still a few oddities - like the spacing between * and where 13/12 14:49 yeah, I usually just redefine where to have a bit of leading space 13/12 14:49 the antialiasing on the text looks odd 13/12 14:50 can't really put my finger on it 13/12 14:50 have you come across mathjax by the way? 13/12 14:50 it was worse before :) 13/12 14:50 http://www.mathjax.org/ native (hinted) font rendering 13/12 14:50 I noticed that cartazio had been fiddling with it. 13/12 14:51 it's very attractive! 13/12 14:51 oh yeah 13/12 14:51 Gonna have to disappear in a moment. Committee meeting. Better swap the other brain back in, if I can persuade the dog to stop chewing it. 13/12 14:54 pigworker: Shan't keep you then - we should deffo try to book some time to bash the new term rep into the Pig though 13/12 14:55 back from meeting; need to write notes for my class, but I'm relatively interruptable 13/12 16:43 is e-pig.org down? 13/12 18:02 I guess so, http://downforeveryoneorjustme.com/e-pig.org 13/12 18:03 :( 13/12 18:12 I want to read the reddit link 13/12 18:12 epic + that blog post = roll your own dependently typed language (minus syntax) 13/12 18:13 syntax is overrated 13/12 18:14 I agree 13/12 18:14 hmm, I thought I had that blog post cached, but apparently not 13/12 18:15 join #oasis 13/12 18:35 edwinb: do you have any guides on using epic beyond the sample you put up? 13/12 20:30 Anyone know what happened to www.e-pig.org? 13/12 20:57 Taral: I hope someone in Nottingham can kick something at some point. 13/12 22:45 --- Day changed Tue Dec 14 2010 copumpkin: not yet, but I hope to have one quite soon 14/12 00:34 excellent! :D 14/12 00:34 thanks 14/12 00:34 I decided (coincidentally...) the other day that it was about time I wrote it up 14/12 00:34 what with it being more than 4 years old now 14/12 00:35 Dear Lord, please may I be forgiven for grinning when people who are not at all my stooges appear on the Coq list and make innocent remarks like "I have a type T : Set and equivalence relation R : T -> T -> Prop and I would like to form the new type T/R : Set. I could not find any way to form this new type."? 14/12 09:42 heh 14/12 22:23 --- Day changed Wed Dec 15 2010 I wonder if I will get to write more blog today. epilogue is still unhappy... 15/12 10:12 was that on sneezy? 15/12 11:34 we had some, ahem, problems there... 15/12 11:34 forgive me if I manage not to faint with amazement 15/12 11:59 pigworker copumpkin: e-pig.org is back 15/12 14:42 sorry for the interruption 15/12 14:42 yay! 15/12 14:42 thanks :) 15/12 14:42 moleris: many thanks! 15/12 16:04 pigworker: Still in the mood to blog more today? 15/12 16:04 I'm half asleep, but otherwise yes. 15/12 16:05 okay, done with the conf call -- probably too late in the UK now 15/12 17:29 If a random collection of mid-keyboard characters appears from me on IRC, phone me to wake me up. 15/12 18:18 Does anyone have a link to the version of the levitation paper with stratified Set? 15/12 21:01 Taral: I see Pierre still has the earlier version in his publications section. Cough. http://personal.cis.strath.ac.uk/~conor/levitation.pdf 15/12 22:06 Yeah, that's the one I have. 15/12 22:08 But it's not stratified. :/ 15/12 22:08 Which kind of messes with my plans to make a distilled-down dependent core based on epigram. 15/12 22:08 :P 15/12 22:08 o wait 15/12 22:10 that's not a link to pierre's web :) 15/12 22:11 is there an easy way to distinguish the old and the new paper? 15/12 22:12 pigworker: What are your thoughts on universe (Set^n) polymorphism? 15/12 22:13 Ah, you want the version of the paper which doesn't exist. Pierre did build an Agda model with Agda universe polymorphism. 15/12 22:14 No, the one you gave me is the one I wanted. I try not to request non-existent things. 15/12 22:15 I think I have all the stratification rules done, just wanted to check the Desc stratification. 15/12 22:15 (well, IDesc technically) 15/12 22:15 Are they plans to add universe polymorphism to Epigram2? 15/12 22:16 The newer version has indices which should fit a suitably stratified system (and were instantiated by a script Pierre wrote, up to level 42, relying on no polymorphism). 15/12 22:17 *nod* 15/12 22:17 I do want to have universe polymorphism in Epigram 2, but I think the way it's done in Agda is too complex. 15/12 22:18 * Taral goes to read about Agda's universe polymorphism. 15/12 22:18 I tried something involving encodings... but didn't get far. 15/12 22:18 If you find anything to read, let me know. 15/12 22:18 and coq's Set^n \subset Set^{n+1} bothers me 15/12 22:18 "Persuading these programs to perform was a perilous pedagogical peregrination for the protagonist." 15/12 22:19 ow. 15/12 22:19 I love it 15/12 22:19 something hurts in my brain every time I see that sentence. 15/12 22:19 I pretty much nicked it out of Doctor Who. 15/12 22:20 heh 15/12 22:22 okay, agda's universe polymorphism is icky 15/12 22:22 The single-quantifier restriction is... odd, and there's no lifting. 15/12 22:22 Then again, I'm not sure if lifting is requisite 15/12 22:23 Lack of lifting is what makes it necessary to consider multiple universe variables, equipped with successor and max. 15/12 22:24 yuk 15/12 22:24 but then again, if you do have lifting, you end up with problems on the elim side... 15/12 22:24 Bah, nevermind. I leave it alone for now. 15/12 22:24 pigworker: I like your recent blog post on a better way to type terms in Epigram2's implementation. Is there code on the way? 15/12 22:25 I plan to try polymorphism in the "base level", but otherwise allow only constant levels above base. 15/12 22:25 "base level"? 15/12 22:26 what seems most icky to me (as a non-expert) about agda's universe polymorphism is that you can pattern match on universe levels 15/12 22:27 or could up until recently 15/12 22:27 Ew. 15/12 22:27 Universe levels should be non-informative. 15/12 22:27 Everything you can do at Set^0, Set^1, Set^2..., you can redo at Set^1, Set^2, Set^3...  You might as well replace 0 by a variable standing for the lowest level you are locally considering. 15/12 22:28 I agree, but I'm not quite sure what could go wrong with the current system. It just makes me feel uncomfortable/unparametric :P 15/12 22:28 pigworker: Oh, that's neat. 15/12 22:28 That assumes you have x \in Set^0 -> x \in Set^1, though 15/12 22:28 which implies Set^0 \subset Set^1 15/12 22:28 mini agda already has that 15/12 22:29 iirc 15/12 22:29 and coq has that. 15/12 22:29 I don't know how implicit this polymorphism can be. But it's not hard to see how the fully explicit system ought to be. x{0} : Set^0, x{1} : Set^1, etc.. 15/12 22:31 hm 15/12 22:31 nat{0}, nat{1}? 15/12 22:31 I suppose. 15/12 22:31 ah, now add bidirectional typechecking 15/12 22:32 heh "boxy types" :D 15/12 22:32 So, I reckon Set^n accepts (x : S) -> T if Set^n accepts S and x : S |- Set^n accepts T. The Pi syntax need not mention the n. 15/12 22:34 not mentioning n is nice, if I understand you correctly 15/12 22:35 If you add an operator, lift^n : Set^n -> Set^{n+1}, you discover that lift^n ((x : S) -> T) = (x : lift^n S) -> lift^n T, and so on: lift does exactly nothing. 15/12 22:35 For canonical sets, it actually becomes true that Set^n \subset Set^{n+1}. 15/12 22:36 :( "canonical sets"? 15/12 22:36 canonical sets are sets formed by canonical set constructors (Pi, Sigma, etc) 15/12 22:37 ah 15/12 22:37 * Taral is trying to follow this logic. This stuff is hard. x.x 15/12 22:38 Still kicking it around. I could go with a fully explicit core language, abstracting over levels and making lift compute by recursion on types. The fact that lift does nothing makes me reluctant. 15/12 22:43 If you want it to be complete, don't you have to add the ability to raise the level at every lambda? 15/12 23:34 s/raise/set/ 15/12 23:34 I'm not sure what you mean. 15/12 23:35 er 15/12 23:36 f x = case x of { A -> \y -> y; B -> ... } the inner \y -> y needs to be polymorphic 15/12 23:37 what's the type of f? 15/12 23:37 mmm 15/12 23:38 I'm expecting the type of f to determine the type of that inner lambda. 15/12 23:39 f {l} Obj l -> {T : Set l} T -> T 15/12 23:39 but what you want is 15/12 23:39 f {l} Obj l -> {l'} {T : Set l'} T -> T 15/12 23:39 s/^f/f :/g 15/12 23:41 I guess it's a question of where generalisation over levels happens. I don't know. 15/12 23:46 *nod* 15/12 23:46 There's a paper in there somewhere. 15/12 23:46 one of these days, when the rest of the bits have turned up 15/12 23:48 Anyway, I'm still working on trying to distill a dependently-typed core out of this. 15/12 23:49 Something separable from the language aspect, so it can be reused. 15/12 23:49 With universe levels, the question is what goes in the explicit syntax of the core: some stuff may be useful information (even if it's concealed in high-level syntax); other stuff may be more of a nuisance. 15/12 23:51 At least that's a question. 15/12 23:51 Yeah, I'm inclined to just set that particular brand down for now before I get burned. :) 15/12 23:51 * edwinb is having far too much fun with epic. It's almost like it's nearly holiday time or something. 15/12 23:52 edwinb: implementing the lambda calculus is just so festive 15/12 23:53 Today's fun was implementing a LOGO like thingy 15/12 23:53 I have enough trouble keeping track of all the pieces that have to dance (Set, Pi, Lambda, Sigma, (,), 1, nat (En), fin (#), hlist (branches), mu, desc, con, out, ind, all, All, switch 15/12 23:53 etc.) 15/12 23:53 I probably missed some. 15/12 23:53 perhaps I'll give it some syntax and write a program to draw a Christmas tree 15/12 23:54 So why does Pig export to epic instead of extracting haskell or something? 15/12 23:55 Extraction is a bit limiting 15/12 23:56 it is? 15/12 23:56 I'd be tempted to export open computational behaviour to Haskell, to link it in to the typechecker. 15/12 23:56 You don't get to control evaluation strategy, or do any clever optimisations 15/12 23:56 it's quite hard work even to convince GHC to compile your output since it's full of coerces 15/12 23:56 and that limits with the optimiser can do 15/12 23:57 and, really, we ought to do much better 15/12 23:57 But for run-time code, generating haskell is throwing away hard-won information. 15/12 23:57 I wonder if you could compile to GHC Core instead of Haskell? 15/12 23:57 you can do pretty well with extraction, but I'd hope we can do a lot better 15/12 23:57 GHC core has too many types 15/12 23:57 boo :( 15/12 23:57 None of the existing intermediate languages really work right 15/12 23:58 I know because I've looked ;) 15/12 23:58 It's a shame to re-implement all those optimizations. 15/12 23:58 It's not very hard 15/12 23:58 Fortunately they've been very kind and written them up ;) 15/12 23:58 You could maybe work with the jhc guy :) 15/12 23:59 GHC output isn't ideal for my current favoured application domain, which is bit level systems hacking 15/12 23:59 Of course, Pig is different in that you have things like termination guarantees. 15/12 23:59 that's a domain where a dependently typed language can really win, I think 15/12 23:59 copumpkin: There's no point masking your host if you join the channel before the mask takes effect. :) 15/12 23:59 --- Day changed Thu Dec 16 2010 and you have to put some thought into exactly what code you're generating. You don't get much flexibility if you just generate Haskell with evil hacks. 16/12 00:00 True. 16/12 00:00 Taral: yeah, too lazy to make that work right, besides I usually don't care 16/12 00:00 lol 16/12 00:00 Anyway, my current thinking with epic is that it would be nice to make the interface available to others 16/12 00:00 since it isn't limited to just Epigram, or dependent types 16/12 00:01 *nod* 16/12 00:01 Also, I'd quite like to write a paper that doesn't have the phrase "dependent type" in anywhere. Just for once. 16/12 00:01 I recommend writing papers which aren't about dependent types. 16/12 00:01 * Taral laughs. 16/12 00:02 Got me through the lean years. 16/12 00:02 I tried writing a paper once. 16/12 00:02 It didn't go well. :( 16/12 00:02 I leave paper-writing to other people now. 16/12 00:02 When I'm not doing dependent types I'm usually perpertrating dirty hacks... they tend to be less publishab;e. 16/12 00:03 Although that doesn't seem to stop some people. 16/12 00:04 I've just spent a term teaching. I've written a 100 page tome about first-year digital logic. I'm desperate to write a paper about something more fun, but I fear I'll just fall asleep on FGHJ. 16/12 00:05 You have a very linear face. 16/12 00:05 edwinb: a dirty hack, hammed up, is always floggable 16/12 00:05 pigworker: Is that why there's been little activity on the Pig codebaes? 16/12 00:05 er, codebase 16/12 00:05 I'm guessing VBN and space will get caught in crossfire 16/12 00:05 Taral: yes; no human resource directed at problem means no progress 16/12 00:06 I'd help, but I only barely understand what's already there. 16/12 00:06 And the rate at which fundamental things (like term representations) change makes me reluctant to do anything with it. 16/12 00:07 If there was a reasonable core, I could at least hack at making a usable programming language which parses to that core. 16/12 00:07 (no, cochon is not a usable core) 16/12 00:07 It's a moving target, true. The history of this project is the history of gradually improving representational choices resulting in differently positioned obstacles. 16/12 00:08 Yes, and watching it is fascinating. :) I don't feel competent to contribute, is all. 16/12 00:09 Isn't it awfully late over there? 16/12 00:09 it's only midnight 16/12 00:09 I quite understand. People volunteer, but it's hard to identify things to suggest. 16/12 00:11 It takes some getting used to: code that was a sweat to think through just getting shredded six months later. 16/12 00:28 I'm a bit behind where it's at at the minute... 16/12 00:31 Hopefully worth resynching in the New Year. 16/12 01:12 I'm hoping we can switch to the new term representation, leaving the rest of the structure standing. Translation to Epic won't change much. 16/12 01:15 Good morning. 16/12 16:39 pigworker: Did you get any sleep yet? 16/12 16:39 stayed up until the cricket started (in Australia) then conked out 16/12 16:43 it was worth not sleeping for 16/12 17:03 * edwinb disputes "Distribution.Simple" as a name for the cabal module hierarchy 16/12 17:07 I was woken up by Ponting and stayed awake until lunch. Good times. 16/12 17:13 edwinb: It's relative. 16/12 17:13 To be fair I am trying to do something a bit weird. 16/12 17:15 pigworker: I waited until I'd got a full line at Boycott Bingo 16/12 17:15 can't have taken long 16/12 17:16 It was about 4am before he started talking about his grandmother 16/12 17:17 I dimly recall, also Aggers prompting with a stick of rooobarb 16/12 17:17 * pigworker has just blogged about the cheeky typeclass hack Saizan helped sort out the other day. 16/12 21:09 pigworker: is there an advantage to writing o ~ (S n) as a superclass constraint for Leq instead of just substituting it into the class head? 16/12 21:17 oh 16/12 21:17 man, I'm dumb 16/12 21:18 ignore me :) 16/12 21:18 a sufficiently sensible question that I felt obliged to answer it 16/12 21:18 man, that's quite elegant 16/12 21:19 makes me want to go write my own dependently typed language using your last two blog posts as starting points 16/12 21:20 I like to give the game away. 16/12 21:20 it's a type level irrefutable pattern: "instance (o ~ S n, Leq m n) => Leq m o" ~~ "leq m ~(S n) = leq m n" 16/12 22:56 --- Log closed Sun Dec 19 14:36:01 2010 --- Log opened Sun Dec 19 14:36:10 2010 -!- Irssi: #epigram: Total of 10 nicks [0 ops, 0 halfops, 0 voices, 10 normal] 19/12 14:36 -!- Irssi: Join to #epigram was synced in 86 secs 19/12 14:37 anyone here use PiSigma? 19/12 22:10 --- Day changed Mon Dec 20 2010 anyone here use PiSigma? 20/12 15:26 I haven't tried it. I don't really understand how it's supposed to work. 20/12 16:48 pigworker: interesting use of Maybe () there :) 20/12 21:30 I guess it's strictly more useful than Bool 20/12 21:30 I'm a big fan of Maybe (). Optimism at work. 20/12 21:44 I also get to write   pattern True = Just ()   pattern False = Nothing 20/12 21:45 Of course, I should really be using Either, with a suitable monoid. 20/12 21:46 that's nice 20/12 21:51 does chev keep as much sharing as a call-by-need evaluator? 20/12 21:52 No. There's a tension with chev. You can write chev as the primitive, instead of chk, with the aim of maximising sharing. You end up baking in a copy of //, and I'm reluctant to do that too early, for fear that // will get out of sync with its copy. Later, fuse chev. 20/12 22:00 i thought it'd be more complicated than that, but i see now that you always update the environment with the result of evaluation 20/12 22:06 I've experimented with working in State Environment, rather than Reader Environment, updating thunks on evaluation, but if it's going to be that complicated, you may as well use actual mutable state and get it right. 20/12 22:09 heh, true 20/12 22:11 (i end up in StateT Heap (Reader Environment) actually) 20/12 22:14 --- Day changed Tue Dec 21 2010 as a side remark, it is my understanding that silent cumlativity is what destroy's coq's ability to have eta-conversion. 21/12 02:17 --- Day changed Wed Dec 22 2010 yay, ornamental algebras 22/12 04:42 I should probably finish the damn thing. 22/12 04:47 * pigworker had better get some sleep. 22/12 04:58 pigworker: Your Spiny type checker doesn't terminate on ill-typed terms :( 22/12 21:01 oh, I see the bit about "contain no beta-redexes" 22/12 21:02 boooooo 22/12 21:02 what about let-forms? 22/12 21:02 global defs currently available, locals not hard to add 22/12 21:02 Via the Dfn constructor? 22/12 21:03 yes 22/12 21:03 I wondered why that was there :) 22/12 21:03 It's a shame you still need a name supply to do type checking. 22/12 21:03 But I tried to make it nameless and failed. 22/12 21:03 you can go nuts doing that 22/12 21:03 I'm already nuts. I work on this stuff, yes? 22/12 21:04 nuts is relative 22/12 21:04 :) 22/12 21:05 going totally nameless means facing the dark side of de Bruijn indexing 22/12 21:06 I'm a mutant -- I can code in indexes. 22/12 21:06 What do I do if the input program contains beta-redexes? Insist on typing? 22/12 21:06 syntax error 22/12 21:07 Or convert them to let-forms. 22/12 21:07 which require types. 22/12 21:07 bah, syntax error. 22/12 21:07 Be nice if the W constructor wouldn't admit lambdas. 22/12 21:08 then you couldn't build a beta redex. 22/12 21:08 the elaborator can be more liberal, but there's no reason for the kernel to be 22/12 21:08 ah, but the point is to allow lambdas there, so that it's possible to implement operators 22/12 21:09 ah, so long as you can guarantee that they're well-typed? 22/12 21:10 Because I can W (B La Nil (V0 :$(A (V0 :$ B0)))) 22/12 21:10 s/V0/V 0/g 22/12 21:11 yes, operator implementations are inside the kernel 22/12 21:11 sounds good to me. 22/12 21:11 onward! 22/12 21:11 might need to be even more liberal than W, and allow any old (in scope) rubbish, but I'll worry about that when it happens 22/12 21:12 --- Day changed Tue Dec 28 2010 pigworker: I noticed long ago that you were talking about slice categories in haskell as a way of deriving indexed monads. Can you elaborate on what part of that is actually the slice category? The comment is here: http://blog.sigfpe.com/2009/02/beyond-monads.html 28/12 18:12 pigworker: all I can really see there is a natural transformation and a generalized functor and monad class using it 28/12 18:12 Given a suitable equality (ha ha ha) for I : Set, the I -> Set category (Pow I, whose morphisms X -> Y are functions in (i : I) -> X i -> Y i) behaves just like the slice category (Fam I), whose objects are pairs A : Set, f : A -> I and whose morphisms (A, f) -> (B, g) are functions h : A -> B such that f = g o h. Take X i = Sg A \a -> f a == i to go one way, and (A, f) = (Sg I X, fst) for the other. 28/12 18:17 You can kind of do Pow in Haskell, but Fam is rather harder to get at. 28/12 18:18 yeah. is it even possible? I implemented slice categories in agda a while back, but couldn't really think of a good way of doing it in haskell 28/12 18:19 some shenanigans with type functions and a wrapper type? 28/12 18:19 Has there been much change between Epigram 1 and 2? (On the underlying theory level, that is?) 28/12 18:22 ok, I've been trying to install Epigram, but cabal keeps failing on installing SHE. Any suggestions? 28/12 19:32 merijn: the underlying theory is completely different 28/12 19:35 install SHE from darcs? (cabal should work, but maybe I have to update something...) 28/12 19:36 In that case I should probably first figure out whether the papers I was reading refer to 1 or 2 before installing the wrong version :p 28/12 19:37 Epigram 1 is the wrong version. 28/12 19:37 if you're checking out old Epigram papers, better to try hacking the examples in Agda 28/12 19:38 pigworker: Yes, but these papers are assigned material I have to read. I was just hoping playing around with actual implementation might lessen my confusion 28/12 19:40 which papers are they? 28/12 19:41 "The View from the left" and "Towards Observational Type Theory" 28/12 19:43 VfL corresponds closely to Epigram 1 (which isn't on Hackage but is on e-pig.org and needs xemacs); TOTT is an early plan for the type theory of Epigram 2 (but Observation Equality, Now! might help clarify what's going on) 28/12 19:45 Ah, goody. So the theory I've been struggling through is mostly outdated anyway, joy! 28/12 19:48 Theory moves fast around here, but the key ideas of VfL and TOTT are still in play. Details (e.g. how datatypes are defined) evolve, but it's certainly not a waste of effort to get to grips with the concepts. 28/12 19:51 Its mostly the core concepts which are important to me right now anyway, VfL is rather dense unfortunately. 28/12 19:58 they made us do that 28/12 20:00 I noticed, I also have a draft version which has considerably less terrifying diagrams than the final version. 28/12 20:05 the half-as-long version? it contains essentially the same ideas about programming on top of a proof assistant, without the disguise 28/12 20:06 --- Day changed Wed Dec 29 2010 So... I noticed today that I can't create inductive datatypes in Prop like coq has. 29/12 19:54 What's the substitute? 29/12 19:54 --- Day changed Thu Dec 30 2010 I see Taral's not about, but hopefully he'll pick this up from the logs... 30/12 12:24 There should be (is?) a Prop-former called something like Inh : Set -> Prop, which forms the proposition that a set is inhabited. 30/12 12:25 It's left-adjoint to :- I think. The prop Inh S => P and the set S -> :- P correspond appropriately. :- . Inh is a monad. 30/12 12:27 But here's the but. Inh eliminates only over Prop. 30/12 12:28 The standard (malheureux, à mon avis) use of Prop for termination proofs is thus excluded. 30/12 12:30 I say "he'll pick this up". I don't know Taral's gender and should not have presumed. 30/12 12:34 Termination evidence is distinctly relevant for open computation, and thus belongs in Set. It tends to inhabit the sort of set that edwinb erases at run time anyway. Panic over, I hope. 30/12 12:35 they tend (more or less by definition) to translate to the pattern matching function you would have written in the first place... 30/12 13:57 pigworker: does epigram have any specific plans about record types and records in general? 30/12 20:29 copumpkin: not yet; I had a thought about allowing a field name in the sigma type and supporting friendlier elaboration with named projection, but I'm not sure 30/12 21:54 I always meant to do some work with Zhaohui Luo and Randy Pollack on that topic. 30/12 21:55 my main use case is to build up algebraic structures by combinations of fields stating their operations and properties on them, but I'm not sure how much work there is on dependent record types that would allow me to do what I want 30/12 22:12 copumpkin: that's also Randy's primary concern, and he's written quite a bit on the subject, but nobody has implemented the technology he modelled as a native feature 30/12 23:31 --- Day changed Fri Dec 31 2010 pigworker: randy what? 31/12 03:33 Pollack 31/12 03:37 aha, thanks 31/12 03:37

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