--- Log opened Wed Dec 01 00:00:20 2010
abstractstoneI need to solve this:01/12 00:04
abstractstonedata Nat := ('zero : Nat) ; ('suc  : Nat -> Nat);01/12 00:04
abstractstonelet foo : :- (: Nat) ('zero) == (: Nat) ('zero) ;01/12 00:04
abstractstonegive refl ;01/12 00:04
abstractstoneit gives the error: I'm sorry, Dave. I'm afraid I can't do that.01/12 00:04
abstractstoneError: elabGive: only possible for incomplete goals.01/12 00:04
abstractstonebut if you go root ; elab foo ; it prints _01/12 00:05
abstractstoneIn a situation like this:01/12 00:06
abstractstonefoo_1.impl_2 > show context01/12 00:06
abstractstoneNat : Set01/12 00:06
abstractstonefoo-type : Set01/12 00:06
abstractstonefoo : (c : < _ : :- ((: Nat) 'zero) == ((: Nat) 'zero) >) -> :- ((: Nat) 'zero) == ((: Nat) 'zero)01/12 00:06
abstractstonewhat do you do?01/12 00:06
abstractstonemake foo := refl Nat 'zero : :- (: Nat) ('zero) == (: Nat) ('zero) ;01/12 00:07
abstractstone works01/12 00:07
Saizanwhat does elab foo gives after that?01/12 00:08
abstractstoneoh it still gives _01/12 00:08
abstractstonethat's weird01/12 00:08
abstractstoneoh maybe it does that for all props01/12 00:09
Saizanit'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 printed01/12 00:09
Saizanso, "let foo : :- (: Nat) ('zero) == (: Nat) ('zero) ;" was a complete definition of foo, because _ was filled in directly01/12 00:10
abstractstoneah thank you01/12 00:10
abstractstonehow can you tell when a complete definition has been given?01/12 00:11
Saizanif it doesn't give you the type of the next goal, i guess01/12 00:13
abstractstonelet R_trans (z : Zahl) (w : Zahl) (y : Zahl) : :- R z w => R w y => R z y ;01/12 00:21
abstractstone<= Pair.Ind Nat Nat z ;01/12 00:21
abstractstone<= Pair.Ind Nat Nat w ;01/12 00:21
abstractstone<= Pair.Ind Nat Nat y ;01/12 00:21
abstractstonegives this goal:01/12 00:22
abstractstonelet R_trans (z : Zahl) (w : Zahl) (y : Zahl) : :- R z w => R w y => R z y ;01/12 00:22
abstractstone<= Pair.Ind Nat Nat z ;01/12 00:22
abstractstone<= Pair.Ind Nat Nat w ;01/12 00:22
abstractstone<= Pair.Ind Nat Nat y ;01/12 00:22
abstractstoneoops01/12 00:22
abstractstoneProgramming: < 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
abstractstoneI need to unfold the definition of R_trans-type.h14 somehow?01/12 00:23
abstractstoneI want to get something like  :- a^1 + a^2 == a^3 + a => ...01/12 00:24
abstractstonehttp://proggit.pastebin.com/tQuBZHiH01/12 00:28
abstractstoneI 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+e01/12 00:29
abstractstonebut 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
abstractstonereally difficult to get started on this language with so little example code 01/12 00:42
abstractstonehttp://proggit.pastebin.com/spCzsns4 - How do I name a^i in this?01/12 00:44
abstractstonelambda a ;  doesn't work01/12 00:44
--- Day changed Fri Dec 03 2010
Taraldead channel is dead?03/12 20:41
roconnornope03/12 20:48
Taraloh goody03/12 20:50
TaralThere hasn't been much activity on the darcs repo either. I was wondering if things were still progressing?03/12 20:50
TaralI haven't actually tried it, mostly because the SHE requirement is scary?03/12 20:50
* roconnor hasn't used epigram03/12 20:51
roconnor:D03/12 20:51
roconnorTaral: the epigram developers are probably mostly in BST or maybe a few in CEST.03/12 20:51
TaralI know. :(03/12 20:52
TaralAll the fun stuff happens in Europe.03/12 20:52
Saizan_Taral: she is not that scary03/12 21:35
Saizan_it doesn't even eat all your ram if you use the darcs version :)03/12 21:35
Taralwhere's the darcs version?03/12 21:48
Taralaha03/12 21:48
Taralhow long before we have epigram on epigram?03/12 21:49
Saizan_http://personal.cis.strath.ac.uk/~conor/pub/she <- in case you haven't found it03/12 22:01
* Saizan_ doesn't know03/12 22:01
TaralI got it.03/12 22:01
TaralCompiling darcs first :D03/12 22:02
Saizan_i've seen pigworker write that the missing piece to implement a dep. typed language in itself is some good tech for constraint solving03/12 22:04
abstractstonehttp://pastebin.com/nTAxGGiq03/12 22:07
abstractstone#03/12 22:07
abstractstoneI 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
abstractstonethere is too much commutativity and associativity,  I can't write it out the in usual way: any ideas?03/12 22:08
abstractstoneI started writing the proof but it doesn't check the validity as you go: It adds coercions whenever you put X instead of Y03/12 22:12
TaralWhat is ?03/12 22:12
Taralrefine thmplusCancel 'zero a b = ? ;03/12 22:12
abstractstoneit's a hole, simpl fills it in03/12 22:12
Taralinteresting.03/12 22:13
Taralsimpl isn't in the manual yet03/12 22:13
abstractstonehelp simpl  in the Epigram prompt03/12 22:18
abstractstoneand help lists commands03/12 22:18
Taralmhm!03/12 22:19
TaralI don't see how this theorem is true.03/12 22:19
Taraloh, I see.03/12 22:19
abstractstonea+d = c+b,c+f=e+d03/12 22:21
abstractstone(a+d)+(c+f) = (c+b)+(e+f)03/12 22:21
abstractstone...03/12 22:21
abstractstone(c+f)+(a+d) = (c+f)+(e+b)03/12 22:21
abstractstonea+d=e+b03/12 22:21
abstractstoneeach line is one use of 'trans'03/12 22:22
abstractstoneI don't know the most efficient way to fill the ... part - that's why I am stuck03/12 22:22
Taraltrans is a no-op03/12 22:22
abstractstoneI mean efficiency in terms of how much I have to type :P03/12 22:23
abstractstonewhat I wrote above is wrong03/12 22:26
Taralwell03/12 22:27
TaralthmZahlthing_10.impl_2 > = thmplusCancel (plus c f) (plus a d) (plus e b) ?03/12 22:27
TaralTa.03/12 22:27
TaralGoal: :- (plus (plus c f) (plus a d)) == (plus (plus c f) (plus e b))03/12 22:27
Taralif you want to use backwards reasoning03/12 22:27
Taralannoying that it won't infer holes from types03/12 22:28
abstractstoneI have been trying to prove the wrong thing, it should be :- plus a f == plus e b03/12 22:31
Taraloho03/12 22:32
abstractstonewhat would be ideal is if I could just operate directly on the goal equation03/12 22:35
Tarallooking...03/12 22:35
abstractstonethat mgiht ahve to be a feature though03/12 22:35
TaralI wish I understood what a "programming problem" really is.03/12 22:39
abstractstoneyou mean the angle brackets thing?03/12 22:39
abstractstoneProgramming: < thmZahlthing a b c d e f p1 p2 : :- (plus a d) == (plus e b) >03/12 22:40
Taralyeah03/12 22:40
Taralit's kind of interesting03/12 22:40
abstractstoneinteresting question03/12 22:41
abstractstoneI think part of it is to make sure you do recursion properly (no infinnite loops)03/12 22:42
abstractstoneinfer equalFun Nat Nat (\ (x : Nat) -> plus x c) (plus b a) (plus a b) (thmplusComm b a) ;03/12 22:51
abstractstoneit's not parsing my (\ (x : Nat) -> plus x c) part03/12 22:51
Taraler03/12 22:52
abstractstoneah it works without the :03/12 22:52
abstractstone: Nat03/12 22:52
TaralHm.03/12 22:54
TaralLooks like much of this machinery is not implemented.03/12 22:55
abstractstonehttp://proggit.pastebin.com/xYXqYhWL03/12 22:56
abstractstonethat's where I am at now: just have to put those equations together03/12 22:56
Taralwhat's equalFun?03/12 22:57
abstractstonelet equalFun (X : Set) (Y : Set) (f : X -> Y) (a : X) (b : X) (P1 : :- a == b) : :- f a == f b ;03/12 22:57
abstractstoneroot ;03/12 22:57
Taraloh03/12 22:57
abstractstonelots of basic facts about equality seem to get proved automatically (I don't really know how ...)03/12 22:57
Taral:)03/12 22:58
Taralmagic.03/12 22:58
abstractstoneusing the rules:03/12 23:22
abstractstone { X+Y == Y+X } { X+(Y+Z) == (X+Y)+Z }03/12 23:22
abstractstonebest 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
abstractstoneI don't think I can get epigram to accept that03/12 23:23
abstractstoneI think I need a better set of rules03/12 23:24
Taralprogramming with Epigram right now is a pain03/12 23:24
Saizanit might be a bit painful but it should be straightforward if you first define transitivity and congruence for ==03/12 23:24
Taralthose exist already03/12 23:24
abstractstonehave you written much Taral ?03/12 23:26
Taralno03/12 23:27
Taralbecause it's a pain03/12 23:28
Taralmost of the infrastructure is missing03/12 23:28
abstractstonewhat infrastructure?03/12 23:28
Taralbackwards reasoning, for one.03/12 23:29
Taralthere's "apply", but it only works if you do crazy things with the proof state.03/12 23:29
Taraland is very specific03/12 23:29
Taraland doesn't work on programming problems03/12 23:29
Saizancan you give an example?03/12 23:31
Taralwhat, apply?03/12 23:32
Saizanof some infrastructure for backwards reasoning, how/when it'd be useful03/12 23:33
Saizani've only used Agda and Twelf as theorem provers, afaiu they don't have things like that?03/12 23:34
TaralSo if your goal is T and you have x :  S -> T in the environment, you don't have "apply x"?03/12 23:35
Saizanah, i see, in Agda you'd write (x ?) as the term you want to use to prove T, ? is the placeholder for a new goal03/12 23:39
Taralsure, you can try that here.03/12 23:39
Saizanyeah03/12 23:39
Taralit makes a mess03/12 23:39
Saizanreally?03/12 23:39
Taralyes03/12 23:39
Taralfor one, there's little to no inference in the system03/12 23:40
Taralso you have to do (x Abigthing Bbigthing ?)03/12 23:40
Taraland second, that doesn't make a new programming problem03/12 23:40
Taralit makes a hole which is a standard propositional thing03/12 23:40
Taraland thus your environment gets hidden in an upper layer03/12 23:40
Saizani see, i didn't notice those problems03/12 23:41
Taralwhat were you trying to do?03/12 23:42
Taraltry abstractstone's problem, you'll see03/12 23:43
abstractstoneI've been working on this for wees03/12 23:43
abstractstoneweeks03/12 23:43
Saizani've only played at little with the cofree comonad in the past, where there wasn't even refine :)03/12 23:44
Saizan*when03/12 23:44
--- Day changed Sat Dec 04 2010
abstractstonehttp://pastebin.com/gkY4w9wP04/12 00:03
Taraldoing this kind of arithmetic is annoying.04/12 00:04
abstractstoneI bet there's quite a lot of things here that could be improved04/12 00:04
Taralin coq there are tactics to auto-solve these things04/12 00:04
abstractstoneTaral: there is a thing for automatically solving prop proofs04/12 00:04
abstractstoneso you could probably add arithmetic as a feature too04/12 00:05
TaralI wouldn't.04/12 00:05
abstractstonewuoldn't what?04/12 00:05
TaralThey're separate tactics in coq for a reason.04/12 00:05
TaralYou don't want to add that to the simplifier.04/12 00:05
TaralI'm out for a bit.04/12 00:09
Taralttyl04/12 00:09
--- Day changed Mon Dec 06 2010
TaralGood morning.06/12 18:08
--- Day changed Thu Dec 09 2010
pigworkerJust 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 Epic10/12 14:22
edwinbit seems to me it ought to be possible to steal Haskell syntax10/12 14:23
edwinbespecially if what you want to do is write your own operators10/12 14:23
edwinbbut to do this, and write out actual code, I need to convert arbitrary top level haskell identifiers to strings10/12 14:23
edwinbthere must be some evilness in the libraries somewhere that lets me do this...10/12 14:23
Saizanfrom within haskell?10/12 15:12
SaizanTemplateHaskell has 'foo (or ''Foo for types) which gives you a Name that you can convert to String with show10/12 15:13
edwinbHmm, I wonder if that might do it10/12 15:18
* edwinb has a look, cheers10/12 15:18
Saizanthough you have to use it on the identifier directly10/12 15:20
edwinbooh! I think that's exactly what I'm after10/12 15:20
edwinbthanks :)10/12 15:20
Saizannp :)10/12 15:21
--- Day changed Sat Dec 11 2010
Phantom_HooverHas there still been no sign of soupdragon?11/12 23:48
Saizanno signs11/12 23:59
--- Day changed Sun Dec 12 2010
Phantom_HooverWhen or why did s?he disappear?12/12 00:03
pigworkerI just pushed another patch to http://personal.cis.strath.ac.uk/~conor/fooling/Spiny.lhs12/12 18:38
pigworkerNow, any old crap like  la$ \f -> f (la$ \x -> f x x)  just evaluates to the relevant de Bruijn term.12/12 18:40
pigworkerI just hope ghc's inliner gets busy with code like that...12/12 18:42
Saizanmaybe an INLINE pragma for la would help, though one should check the core first12/12 18:47
pigworkerFunny that someone asked on stackoverflow today about the impact of changing your data structures on your code base...12/12 18:47
pigworkerSaizan: from the little I understand, it's a good candidate anyway, unless its type is just too scary12/12 18:48
Saizanit's small and non-recursive, so that's true12/12 18:56
pigworkerGaaah. I was hoping to use more typeclass voodoo to iterate the lambda, but I'm not allowed polytypes in constraints.12/12 19:05
pigworkerThe 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
Saizanvalues would be things of type Nm here?12/12 19:43
pigworkeryeah, but they're only head-normal12/12 20:01
pigworkercrucially, 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
pigworkermoleris: I forget; was there a way to persuade Epilogue to do the right thing with Haskell code?12/12 20:11
pigworkerI seem to get [lhs2TeX] happening sometimes.12/12 20:12
pigworkerFirst instalment of the blogged code http://www.e-pig.org/epilogue/?p=70612/12 23:34
copumpkinpigworker: that's great, thanks :D12/12 23:40
--- Day changed Mon Dec 13 2010
* Saizan wonders when one would use Nix13/12 00:30
pigworkerSaizan: 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
molerispigworker: Ping13/12 14:41
pigworkerwotcher13/12 14:42
molerisJust reading through the blog post - I see you got the blog to do the haskell thing13/12 14:42
pigworkeryeah, cut into small enough lumps, it kind of works; weird arrows...13/12 14:43
copumpkinif 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
pigworkercopumpkin: that does sometimes happen...13/12 14:44
pigworkergood luck with the move, and... don't fret about unicode on my account!13/12 14:44
copumpkinhah, that much already works :P13/12 14:44
copumpkinhttps://github.com/pumpkin/agda-highlight and some of its output is at http://pumpkinpat.ch/moo.html13/12 14:45
pigworkerI'll get there eventually.13/12 14:45
pigworkerThree lectures left this term, but a big pile of labs as well.13/12 14:46
copumpkinack :)13/12 14:46
pigworkerSnow expected on Thursday, so it's panic stations now.13/12 14:47
pigworkerSnow is good for pigs but bad for young goats.13/12 14:47
moleris:|13/12 14:47
moleriswhen I said I was reading the blog post, in fact I was fixinging the horrid font and arrows - results now up for all to appreciate13/12 14:48
pigworkerSweet!13/12 14:49
molerisstill a few oddities - like the spacing between * and where13/12 14:49
pigworkeryeah, I usually just redefine where to have a bit of leading space13/12 14:49
copumpkinthe antialiasing on the text looks odd13/12 14:50
copumpkincan't really put my finger on it13/12 14:50
copumpkinhave you come across mathjax by the way?13/12 14:50
molerisit was worse before :)13/12 14:50
copumpkinhttp://www.mathjax.org/ native (hinted) font rendering13/12 14:50
pigworkerI noticed that cartazio had been fiddling with it.13/12 14:51
copumpkinit's very attractive!13/12 14:51
copumpkinoh yeah13/12 14:51
pigworkerGonna 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
molerispigworker: Shan't keep you then - we should deffo try to book some time to bash the new term rep into the Pig though13/12 14:55
pigworkerback from meeting; need to write notes for my class, but I'm relatively interruptable13/12 16:43
copumpkinis e-pig.org down?13/12 18:02
copumpkinI guess so, http://downforeveryoneorjustme.com/e-pig.org13/12 18:03
roconnor:(13/12 18:12
roconnorI want to read the reddit link13/12 18:12
copumpkinepic + that blog post = roll your own dependently typed language (minus syntax)13/12 18:13
edwinbsyntax is overrated13/12 18:14
copumpkinI agree13/12 18:14
edwinbhmm, I thought I had that blog post cached, but apparently not13/12 18:15
roconnorjoin #oasis13/12 18:35
copumpkinedwinb: do you have any guides on using epic beyond the sample you put up?13/12 20:30
TaralAnyone know what happened to www.e-pig.org?13/12 20:57
pigworkerTaral: I hope someone in Nottingham can kick something at some point.13/12 22:45
--- Day changed Tue Dec 14 2010
edwinbcopumpkin: not yet, but I hope to have one quite soon14/12 00:34
copumpkinexcellent! :D14/12 00:34
copumpkinthanks 14/12 00:34
edwinbI decided (coincidentally...) the other day that it was about time I wrote it up14/12 00:34
edwinbwhat with it being more than 4 years old now14/12 00:35
pigworkerDear 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
koninkjeheh14/12 22:23
--- Day changed Wed Dec 15 2010
pigworkerI wonder if I will get to write more blog today. epilogue is still unhappy...15/12 10:12
Laneywas that on sneezy?15/12 11:34
Laneywe had some, ahem, problems there...15/12 11:34
pigworkerforgive me if I manage not to faint with amazement15/12 11:59
molerispigworker copumpkin: e-pig.org is back15/12 14:42
molerissorry for the interruption15/12 14:42
copumpkinyay!15/12 14:42
copumpkinthanks :)15/12 14:42
pigworkermoleris: many thanks!15/12 16:04
molerispigworker: Still in the mood to blog more today?15/12 16:04
pigworkerI'm half asleep, but otherwise yes.15/12 16:05
Taralokay, done with the conf call -- probably too late in the UK now15/12 17:29
pigworkerIf a random collection of mid-keyboard characters appears from me on IRC, phone me to wake me up.15/12 18:18
TaralDoes anyone have a link to the version of the levitation paper with stratified Set?15/12 21:01
pigworkerTaral: I see Pierre still has the earlier version in his publications section. Cough. http://personal.cis.strath.ac.uk/~conor/levitation.pdf15/12 22:06
TaralYeah, that's the one I have.15/12 22:08
TaralBut it's not stratified. :/15/12 22:08
TaralWhich kind of messes with my plans to make a distilled-down dependent core based on epigram.15/12 22:08
Taral:P15/12 22:08
Taralo wait15/12 22:10
Taralthat's not a link to pierre's web :)15/12 22:11
Taralis there an easy way to distinguish the old and the new paper?15/12 22:12
Taralpigworker: What are your thoughts on universe (Set^n) polymorphism?15/12 22:13
pigworkerAh, 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
TaralNo, the one you gave me is the one I wanted. I try not to request non-existent things.15/12 22:15
TaralI think I have all the stratification rules done, just wanted to check the Desc stratification.15/12 22:15
Taral(well, IDesc technically)15/12 22:15
TaralAre they plans to add universe polymorphism to Epigram2?15/12 22:16
pigworkerThe 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
Taral*nod*15/12 22:17
pigworkerI 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
TaralI tried something involving encodings... but didn't get far.15/12 22:18
pigworkerIf you find anything to read, let me know.15/12 22:18
Taraland coq's Set^n \subset Set^{n+1} bothers me15/12 22:18
copumpkin"Persuading these programs to perform was a perilous pedagogical peregrination for the protagonist."15/12 22:19
Taralow.15/12 22:19
copumpkinI love it15/12 22:19
Taralsomething hurts in my brain every time I see that sentence.15/12 22:19
pigworkerI pretty much nicked it out of Doctor Who.15/12 22:20
Taralheh15/12 22:22
Taralokay, agda's universe polymorphism is icky15/12 22:22
TaralThe single-quantifier restriction is... odd, and there's no lifting.15/12 22:22
TaralThen again, I'm not sure if lifting is requisite15/12 22:23
pigworkerLack of lifting is what makes it necessary to consider multiple universe variables, equipped with successor and max.15/12 22:24
Taralyuk15/12 22:24
Taralbut then again, if you do have lifting, you end up with problems on the elim side...15/12 22:24
TaralBah, nevermind. I leave it alone for now.15/12 22:24
Taralpigworker: 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
pigworkerI plan to try polymorphism in the "base level", but otherwise allow only constant levels above base.15/12 22:25
Taral"base level"?15/12 22:26
copumpkinwhat seems most icky to me (as a non-expert) about agda's universe polymorphism is that you can pattern match on universe levels15/12 22:27
copumpkinor could up until recently15/12 22:27
TaralEw.15/12 22:27
TaralUniverse levels should be non-informative.15/12 22:27
pigworkerEverything 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
copumpkinI agree, but I'm not quite sure what could go wrong with the current system. It just makes me feel uncomfortable/unparametric :P15/12 22:28
Taralpigworker: Oh, that's neat.15/12 22:28
TaralThat assumes you have x \in Set^0 -> x \in Set^1, though15/12 22:28
Taralwhich implies Set^0 \subset Set^115/12 22:28
copumpkinmini agda already has that15/12 22:29
copumpkiniirc15/12 22:29
Taraland coq has that.15/12 22:29
pigworkerI 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
Taralhm15/12 22:31
Taralnat{0}, nat{1}?15/12 22:31
TaralI suppose.15/12 22:31
pigworkerah, now add bidirectional typechecking15/12 22:32
Taralheh "boxy types" :D15/12 22:32
pigworkerSo, 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
copumpkinnot mentioning n is nice, if I understand you correctly15/12 22:35
pigworkerIf 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
pigworkerFor canonical sets, it actually becomes true that Set^n \subset Set^{n+1}.15/12 22:36
Taral:( "canonical sets"?15/12 22:36
pigworkercanonical sets are sets formed by canonical set constructors (Pi, Sigma, etc)15/12 22:37
Taralah15/12 22:37
* Taral is trying to follow this logic. This stuff is hard. x.x15/12 22:38
pigworkerStill 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
TaralIf 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
Tarals/raise/set/15/12 23:34
pigworkerI'm not sure what you mean.15/12 23:35
Taraler15/12 23:36
Taralf x = case x of { A -> \y -> y; B -> ... } the inner \y -> y needs to be polymorphic15/12 23:37
pigworkerwhat's the type of f?15/12 23:37
Taralmmm15/12 23:38
pigworkerI'm expecting the type of f to determine the type of that inner lambda.15/12 23:39
Taralf {l} Obj l -> {T : Set l} T -> T15/12 23:39
Taralbut what you want is15/12 23:39
Taralf {l} Obj l -> {l'} {T : Set l'} T -> T15/12 23:39
Tarals/^f/f :/g15/12 23:41
pigworkerI guess it's a question of where generalisation over levels happens. I don't know.15/12 23:46
Taral*nod*15/12 23:46
TaralThere's a paper in there somewhere.15/12 23:46
pigworkerone of these days, when the rest of the bits have turned up15/12 23:48
TaralAnyway, I'm still working on trying to distill a dependently-typed core out of this.15/12 23:49
TaralSomething separable from the language aspect, so it can be reused.15/12 23:49
pigworkerWith 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
pigworkerAt least that's a question.15/12 23:51
TaralYeah, 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
pigworkeredwinb: implementing the lambda calculus is just so festive15/12 23:53
edwinbToday's fun was implementing a LOGO like thingy15/12 23:53
TaralI 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, switch15/12 23:53
Taraletc.)15/12 23:53
TaralI probably missed some.15/12 23:53
edwinbperhaps I'll give it some syntax and write a program to draw a Christmas tree15/12 23:54
TaralSo why does Pig export to epic instead of extracting haskell or something?15/12 23:55
edwinbExtraction is a bit limiting15/12 23:56
Taralit is?15/12 23:56
pigworkerI'd be tempted to export open computational behaviour to Haskell, to link it in to the typechecker.15/12 23:56
edwinbYou don't get to control evaluation strategy, or do any clever optimisations15/12 23:56
edwinbit's quite hard work even to convince GHC to compile your output since it's full of coerces15/12 23:56
edwinband that limits with the optimiser can do15/12 23:57
edwinband, really, we ought to do much better15/12 23:57
pigworkerBut for run-time code, generating haskell is throwing away hard-won information.15/12 23:57
TaralI wonder if you could compile to GHC Core instead of Haskell?15/12 23:57
edwinbyou can do pretty well with extraction, but I'd hope we can do a lot better15/12 23:57
edwinbGHC core has too many types15/12 23:57
Taralboo :(15/12 23:57
edwinbNone of the existing intermediate languages really work right15/12 23:58
edwinbI know because I've looked ;)15/12 23:58
TaralIt's a shame to re-implement all those optimizations.15/12 23:58
edwinbIt's not very hard15/12 23:58
edwinbFortunately they've been very kind and written them up ;)15/12 23:58
TaralYou could maybe work with the jhc guy :)15/12 23:59
edwinbGHC output isn't ideal for my current favoured application domain, which is bit level systems hacking15/12 23:59
TaralOf course, Pig is different in that you have things like termination guarantees.15/12 23:59
edwinbthat's a domain where a dependently typed language can really win, I think15/12 23:59
Taralcopumpkin: 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
edwinband 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
TaralTrue.16/12 00:00
copumpkinTaral: yeah, too lazy to make that work right, besides I usually don't care16/12 00:00
Tarallol16/12 00:00
edwinbAnyway, my current thinking with epic is that it would be nice to make the interface available to others16/12 00:00
edwinbsince it isn't limited to just Epigram, or dependent types16/12 00:01
Taral*nod*16/12 00:01
edwinbAlso, 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
pigworkerI recommend writing papers which aren't about dependent types.16/12 00:01
* Taral laughs.16/12 00:02
pigworkerGot me through the lean years.16/12 00:02
TaralI tried writing a paper once.16/12 00:02
TaralIt didn't go well. :(16/12 00:02
TaralI leave paper-writing to other people now.16/12 00:02
edwinbWhen I'm not doing dependent types I'm usually perpertrating dirty hacks... they tend to be less publishab;e.16/12 00:03
edwinbAlthough that doesn't seem to stop some people.16/12 00:04
pigworkerI'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
TaralYou have a very linear face.16/12 00:05
pigworkeredwinb: a dirty hack, hammed up, is always floggable16/12 00:05
Taralpigworker: Is that why there's been little activity on the Pig codebaes?16/12 00:05
Taraler, codebase16/12 00:05
pigworkerI'm guessing VBN and space will get caught in crossfire16/12 00:05
pigworkerTaral: yes; no human resource directed at problem means no progress16/12 00:06
TaralI'd help, but I only barely understand what's already there.16/12 00:06
TaralAnd the rate at which fundamental things (like term representations) change makes me reluctant to do anything with it.16/12 00:07
TaralIf 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
Taral(no, cochon is not a usable core)16/12 00:07
pigworkerIt'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
TaralYes, and watching it is fascinating. :) I don't feel competent to contribute, is all.16/12 00:09
TaralIsn't it awfully late over there?16/12 00:09
edwinbit's only midnight16/12 00:09
pigworkerI quite understand. People volunteer, but it's hard to identify things to suggest.16/12 00:11
pigworkerIt takes some getting used to: code that was a sweat to think through just getting shredded six months later.16/12 00:28
edwinbI'm a bit behind where it's at at the minute...16/12 00:31
pigworkerHopefully worth resynching in the New Year.16/12 01:12
pigworkerI'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
TaralGood morning.16/12 16:39
Taralpigworker: Did you get any sleep yet?16/12 16:39
pigworkerstayed up until the cricket started (in Australia) then conked out16/12 16:43
edwinbit was worth not sleeping for16/12 17:03
* edwinb disputes "Distribution.Simple" as a name for the cabal module hierarchy16/12 17:07
pigworkerI was woken up by Ponting and stayed awake until lunch. Good times.16/12 17:13
Taraledwinb: It's relative.16/12 17:13
edwinbTo be fair I am trying to do something a bit weird.16/12 17:15
edwinbpigworker: I waited until I'd got a full line at Boycott Bingo16/12 17:15
pigworkercan't have taken long16/12 17:16
edwinbIt was about 4am before he started talking about his grandmother16/12 17:17
pigworkerI dimly recall, also Aggers prompting with a stick of rooobarb16/12 17:17
* pigworker has just blogged about the cheeky typeclass hack Saizan helped sort out the other day.16/12 21:09
pumpkinpigworker: 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
pumpkinoh16/12 21:17
pumpkinman, I'm dumb16/12 21:18
pumpkinignore me :)16/12 21:18
pigworkera sufficiently sensible question that I felt obliged to answer it16/12 21:18
pumpkinman, that's quite elegant16/12 21:19
pumpkinmakes me want to go write my own dependently typed language using your last two blog posts as starting points16/12 21:20
pigworkerI like to give the game away.16/12 21:20
Saizanit'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 secs19/12 14:37
roconnoranyone here use PiSigma?19/12 22:10
--- Day changed Mon Dec 20 2010
roconnoranyone here use PiSigma?20/12 15:26
pigworkerI haven't tried it. I don't really understand how it's supposed to work.20/12 16:48
pumpkinpigworker: interesting use of Maybe () there :)20/12 21:30
pumpkinI guess it's strictly more useful than Bool20/12 21:30
pigworkerI'm a big fan of Maybe (). Optimism at work.20/12 21:44
pigworkerI also get to write   pattern True = Just ()   pattern False = Nothing20/12 21:45
pigworkerOf course, I should really be using Either, with a suitable monoid.20/12 21:46
pumpkinthat's nice20/12 21:51
Saizan_does chev keep as much sharing as a call-by-need evaluator?20/12 21:52
pigworkerNo. 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
Saizan_i thought it'd be more complicated than that, but i see now that you always update the environment with the result of evaluation20/12 22:06
pigworkerI'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
Saizan_heh, true20/12 22:11
Saizan_(i end up in StateT Heap (Reader Environment) actually)20/12 22:14
--- Day changed Tue Dec 21 2010
roconnoras 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
copumpkinyay, ornamental algebras22/12 04:42
pigworkerI should probably finish the damn thing.22/12 04:47
* pigworker had better get some sleep.22/12 04:58
Taralpigworker: Your Spiny type checker doesn't terminate on ill-typed terms :(22/12 21:01
Taraloh, I see the bit about "contain no beta-redexes"22/12 21:02
Taralboooooo22/12 21:02
Taralwhat about let-forms?22/12 21:02
pigworkerglobal defs currently available, locals not hard to add22/12 21:02
TaralVia the Dfn constructor?22/12 21:03
pigworkeryes22/12 21:03
TaralI wondered why that was there :)22/12 21:03
TaralIt's a shame you still need a name supply to do type checking.22/12 21:03
TaralBut I tried to make it nameless and failed.22/12 21:03
pigworkeryou can go nuts doing that22/12 21:03
TaralI'm already nuts. I work on this stuff, yes?22/12 21:04
pigworkernuts is relative22/12 21:04
Taral:)22/12 21:05
pigworkergoing totally nameless means facing the dark side of de Bruijn indexing22/12 21:06
TaralI'm a mutant -- I can code in indexes.22/12 21:06
TaralWhat do I do if the input program contains beta-redexes? Insist on typing?22/12 21:06
pigworkersyntax error22/12 21:07
TaralOr convert them to let-forms.22/12 21:07
Taralwhich require types.22/12 21:07
Taralbah, syntax error.22/12 21:07
TaralBe nice if the W constructor wouldn't admit lambdas.22/12 21:08
Taralthen you couldn't build a beta redex.22/12 21:08
pigworkerthe elaborator can be more liberal, but there's no reason for the kernel to be22/12 21:08
pigworkerah, but the point is to allow lambdas there, so that it's possible to implement operators22/12 21:09
Taralah, so long as you can guarantee that they're well-typed?22/12 21:10
TaralBecause I can W (B La Nil (V0 :$ (A (V0 :$ B0))))22/12 21:10
Tarals/V0/V 0/g22/12 21:11
pigworkeryes, operator implementations are inside the kernel22/12 21:11
Taralsounds good to me.22/12 21:11
Taralonward!22/12 21:11
pigworkermight need to be even more liberal than W, and allow any old (in scope) rubbish, but I'll worry about that when it happens22/12 21:12
--- Day changed Tue Dec 28 2010
copumpkinpigworker: 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.html28/12 18:12
copumpkinpigworker: all I can really see there is a natural transformation and a generalized functor and monad class using it28/12 18:12
pigworkerGiven 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
pigworkerYou can kind of do Pow in Haskell, but Fam is rather harder to get at.28/12 18:18
copumpkinyeah. 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 haskell28/12 18:19
pigworkersome shenanigans with type functions and a wrapper type?28/12 18:19
merijnHas there been much change between Epigram 1 and 2? (On the underlying theory level, that is?)28/12 18:22
merijnok, I've been trying to install Epigram, but cabal keeps failing on installing SHE. Any suggestions?28/12 19:32
pigworkermerijn: the underlying theory is completely different28/12 19:35
pigworkerinstall SHE from darcs? (cabal should work, but maybe I have to update something...)28/12 19:36
merijnIn that case I should probably first figure out whether the papers I was reading refer to 1 or 2 before installing the wrong version :p28/12 19:37
pigworkerEpigram 1 is the wrong version.28/12 19:37
pigworkerif you're checking out old Epigram papers, better to try hacking the examples in Agda28/12 19:38
merijnpigworker: Yes, but these papers are assigned material I have to read. I was just hoping playing around with actual implementation might lessen my confusion28/12 19:40
pigworkerwhich papers are they?28/12 19:41
merijn"The View from the left" and "Towards Observational Type Theory"28/12 19:43
pigworkerVfL 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
merijnAh, goody. So the theory I've been struggling through is mostly outdated anyway, joy!28/12 19:48
pigworkerTheory 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
merijnIts mostly the core concepts which are important to me right now anyway, VfL is rather dense unfortunately.28/12 19:58
pigworkerthey made us do that28/12 20:00
merijnI noticed, I also have a draft version which has considerably less terrifying diagrams than the final version.28/12 20:05
pigworkerthe half-as-long version? it contains essentially the same ideas about programming on top of a proof assistant, without the disguise28/12 20:06
--- Day changed Wed Dec 29 2010
TaralSo... I noticed today that I can't create inductive datatypes in Prop like coq has.29/12 19:54
TaralWhat's the substitute?29/12 19:54
--- Day changed Thu Dec 30 2010
pigworkerI see Taral's not about, but hopefully he'll pick this up from the logs...30/12 12:24
pigworkerThere 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
pigworkerIt'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
pigworkerBut here's the but. Inh eliminates only over Prop.30/12 12:28
pigworkerThe standard (malheureux, à mon avis) use of Prop for termination proofs is thus excluded.30/12 12:30
pigworkerI say "he'll pick this up". I don't know Taral's gender and should not have presumed.30/12 12:34
pigworkerTermination 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
edwinbthey 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
copumpkinpigworker: does epigram have any specific plans about record types and records in general?30/12 20:29
pigworkercopumpkin: 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 sure30/12 21:54
pigworkerI always meant to do some work with Zhaohui Luo and Randy Pollack on that topic.30/12 21:55
copumpkinmy 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 want30/12 22:12
pigworkercopumpkin: 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 feature30/12 23:31
--- Day changed Fri Dec 31 2010
copumpkinpigworker: randy what?31/12 03:33
dolioPollack31/12 03:37
copumpkinaha, thanks31/12 03:37

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