/home/laney/.irssi/irclogs/Freenode/2011/#epigram/July.log

--- Log opened Fri Jul 01 00:00:57 2011
pigworkeragundry: ping01/07 12:43
agundrypigworker: pong01/07 12:45
pigworkerwhere shall we meet? what resources do we need? (it's a nice day, so far...)01/07 12:46
pigworkerif it's mostly chat, we could get some vitamin D, perhaps01/07 12:47
agundryI think that's a very good idea01/07 12:48
agundryI don't have any particular need for technology01/07 12:48
pigworkerI'll get my shoes on, then head for the north side of the Clyde and turn left.01/07 12:49
agundryCan you give me about 10 minutes? I'm halfway though lunch01/07 12:50
pigworkersure; ping when ready01/07 12:50
agundrypigworker: I'm just about to leave01/07 13:04
pigworkercool, I'll head Clydewards now01/07 13:04
agundrysee you shortly01/07 13:06
augurpigworker: what a peculiar way of saying that. "we could get some vitamin D"01/07 16:47
pigworkeraugur: the vitamin D thing - you wouldn't find it peculiar if you lived in Glasgow01/07 17:54
pigworkerthe Sun does not visit often01/07 17:55
augurpigworker: you know they have supplements for that01/07 18:07
pigworkerstill, the real thing is good when available01/07 18:08
--- Day changed Mon Jul 04 2011
molerispigworker: ping04/07 13:57
pigworkermoleris: sorry to be slow...04/07 14:24
molerisNo worries04/07 14:26
pigworkerWhat's up? (I guess we should confirm our plans...)04/07 14:26
molerisI had a technical question - but yeah we should organise for the 18th too04/07 14:28
pigworkerif you're still on for 18-22, let's say that's definite?04/07 14:28
molerisI am04/07 14:29
pigworkerok; that's a plan (stevan, grab those tickets if they're still going)04/07 14:30
pigworkerwhat's the question?04/07 14:30
* pigworker does a darcs pull04/07 14:31
molerisThe eta-quotation (and therefore def equality) is broken when it comes to Definitions04/07 14:32
pigworkerurk... where should I look?04/07 14:32
molerisEvidences/EtaQuote.lhs 04/07 14:33
molerisand Tm.lhs I guess04/07 14:33
pigworkeris it my imagination, or is that a missing case?04/07 14:34
molerisIt's not so missing at my end, but just a broken04/07 14:35
molerisIf the def doesn't have a Case in it then there's no problem04/07 14:36
pigworkerif it doesn't have a Case, then it doesn't even show up, right? it gets fully applied by eta-expansion and fires away04/07 14:37
molerisprecisely04/07 14:38
pigworkerwhat does rewindStk do again?04/07 14:38
molerisit reconstructs the original spine that the def was applied to04/07 14:39
pigworkersounds useful04/07 14:39
molerisThats what I've been attempting to use04/07 14:40
molerisglad I'm not being totally dumb04/07 14:40
pigworkersounds like the right sort of plan; what's cocking up?04/07 14:40
pigworkerI think the plan should be "rewind the stack to get the spine; use the type to figure out how to etaQuote the spine; rebuild the application"04/07 14:43
molerisErr, right - so we can etaQuote the spine Ok, but then we need to rebuild the term04/07 14:43
molerisbut the original operator definition is a Body and we can't put it at the head04/07 14:45
pigworkerbecause it could compute to that stuck state, right?04/07 14:45
molerisWell we can't do evaluation at that point anyway because we've got open terms04/07 14:50
pigworkercoming out of etaQuote, yes04/07 14:51
pigworkerI suspect our best bet is to try something simpler.04/07 14:53
molerisSimple is good04/07 14:53
pigworkerCan we set things up so we can have a normal form which is just a def with a spine? We'll just have to maintain the invariant ourselves that the operator doesn't get to Emit when fed the spine.04/07 14:55
molerisCould work -will have a play04/07 15:01
pigworkermaybe Ds should just be ordinary heads, then04/07 15:06
molerisThat might actually be the simplest way todo it04/07 15:08
pigworkerthe code that runs ops could be yanked out as something that tries to reach Emit, but if it fails, just rebuild; looks like apply gets simpler but applys gets some stuff for running Ds04/07 15:10
--- Day changed Tue Jul 05 2011
* edwinb gives Idris the ability to overload lambdas05/07 15:30
edwinbI can't decide if this is the most evil or most useful feature I've added in ages05/07 15:31
molerisedwinb: Can't it be both?05/07 15:31
edwinbI think 'or' allows both ;)05/07 15:33
edwinbhttps://github.com/edwinb/ResIO/blob/master/linlang.idr -- skip to the end05/07 15:33
Saizani know i've wanted that a lot in haskell05/07 15:35
edwinbSomehow being able to overload bindings makes writing DSELs a lot easier. Especially functional stuff with weird type systems.05/07 15:36
edwinbyou could do type class evilness to some extent in Haskell... but I suppose it's not quite the same thing05/07 15:37
Saizanafaict the Arrow class is more or less about this, though it's quite ugly to write code in that style05/07 15:41
quicksilverby 'being able to override bindings' you mean 'being able to write custom operators which bind names' ?05/07 15:44
edwinbyes, that's more like it05/07 15:44
quicksilverthat is roughly what I envy lisp, if I understand you correctly.05/07 15:45
edwinbeverything we do was done in Lisp 50 years ago :)05/07 15:45
quicksilverin a way. But in an important way, no.05/07 15:46
quicksilverThere are reasons we don't choose to program in lisp.05/07 15:47
edwinbWell indeed05/07 15:47
--- Day changed Sat Jul 09 2011
pequalsnphi, i'm trying to install SHE and I'm having this issue http://code.google.com/p/epigram/issues/detail?id=11409/07 13:40
pequalsnpany help appreciated09/07 13:40
Saizanshe is meant for an earlier version of mtl09/07 13:43
pequalsnpSaizan: so I should downgrade mtl?09/07 13:44
Saizanor comment out those instances09/07 13:44
pequalsnpSaizan: ok, thanks for your help! :)09/07 13:45
Saizanhttp://code.haskell.org/~Saizan/she-0.3.tar.gz <- like i've done here09/07 13:45
pequalsnpSaizan: nice, thanks09/07 13:45
--- Day changed Tue Jul 12 2011
molerisagundry: Ping12/07 13:41
agundrymoleris: pong12/07 13:41
molerisHola12/07 13:41
molerisI just pulled your patches from Thursday12/07 13:41
molerisand they fixed a bug that I spent all yesterday hunting12/07 13:41
molerisI think I might need a holiday12/07 13:42
molerisThanks though12/07 13:42
agundryglad I could help, though it's a shame you didn't darcs pull earlier...12/07 13:42
agundrywhich bug, out of curiosity?12/07 13:43
molerisIndeed12/07 13:43
molerisErr, presumably the Env composition bug12/07 13:43
molerisI need to do a more thorough investigation though12/07 13:43
molerisI was convinced the problem I had was with elim12/07 13:44
agundryit's always possible there are multiple bugs 12/07 13:45
molerisit's certain there are12/07 13:45
molerisBut I'm no longer blocked in the way I was yesterday12/07 13:46
agundrygood12/07 13:46
molerisI'm trying to get the thing in a good state for next week12/07 13:47
molerisor at least less of a state12/07 13:48
agundrythat would be useful12/07 13:48
agundryI'm looking forward to a bit of hacking next week12/07 13:49
molerisGood (:12/07 13:51
agundrythis might already be on your radar, but I noticed when doing propsimp that the equality unfolding machinery in TypeCheckRules is missing quite a few cases12/07 13:52
molerisnot surprised12/07 13:53
agundryI've put in errors for the time being12/07 13:53
agundrywe used to be able to do this cheaply using HalfZip, I think12/07 13:53
molerisYeah, we have to do a bit more work these days12/07 13:54
molerisswings and roundabouts12/07 13:54
--- Day changed Wed Jul 13 2011
* edwinb feels his ears burning and finds reddit13/07 01:15
edwinbI should probably contribute to that discussion13/07 01:16
edwinbbut not right now13/07 01:16
pigworkeredwinb: I hope I didn't overstep.13/07 09:26
edwinbpigworker: it all seemed accurate to me, so no...13/07 10:51
pigworkeredwinb: how's next week looking for you?13/07 16:37
augurpigworker: would epigram2's levitation be capable of transparently forgetting ornamentation?13/07 16:39
pigworkerdepends what you mean by transparently13/07 16:39
augurwell, supposising you defined fins as an ornamented nat, transparently enough for you to use fins for nat-taking functions without a case13/07 16:40
edwinbpigworker: I'm around but possibly busy13/07 16:40
augurwithout an explicit cast, i mean13/07 16:40
edwinbthat said, I do intend to pop over at some point13/07 16:40
pigworkeredwinb: that'd be nice (my hotel is a bit full, but it can always get fuller if you're happy with padded floor)13/07 16:42
edwinbI would probably come over with the best intention of doing a day trip then end up on the floor anyway13/07 16:42
edwinbis it next week moleris is about?13/07 16:43
pigworkeraugur: I don't know whether it makes sense to make the forgetful maps silent, but we can arrange for them to be operationally inexpensive13/07 16:43
pigworkeredwinb: yes13/07 16:43
augurpigworker: someone in #agda (dont remember who) commented that with constructor overloading, cast functions look like explicit identity functions defined as homomorphisms. toNat :: Fin -> Nat ; toNat 0 = 0 ; toNat (suc n) = suc (toNat n)13/07 16:45
edwinbpigworker: right then. I can probably definitely head over on Tuesday.13/07 16:45
augurand that its really an unfortunate thing that you're forced to define it at all, given this fact13/07 16:46
pigworkeredwinb: cool13/07 16:46
augurand i figured that ornamentation would make it extraordinarily easy to make such a thing completely silent13/07 16:46
pigworkeraugur: be careful what you wish for -- subtyping and implicit argument synthesis are not good friends13/07 16:47
augurhmm!13/07 16:47
pigworkerbut there are good things that we can do13/07 16:48
augurwell, i suppose if the forgetful functor is free with the ornamentation, the definition process is removed, so theres that13/07 16:48
augurtoNat :: Fin n -> Nat ; toNat = forget13/07 16:48
augurthats cheap enough i guess..13/07 16:48
edwinbit's quite easy to make it operationally free13/07 16:49
augurcan i just say, btw, that the whole levitaton thing was hard to understand at first but once i got it it was the most amazing thing ever13/07 16:49
pigworkerindeed, and we can arrange for an ornamented structure to be implemented behind the scenes as a dependent pair of plain data and extra stuff13/07 16:49
edwinbbut I'm not sure I want it completely implicit13/07 16:49
pigworkerso as edwinb says, for free13/07 16:50
auguri like pictures. there were no pictures. :( you should get ezyang to illustrate your papers lol13/07 16:50
auguryeah complete implicitness might not be so good13/07 16:50
augurornamentation would at least mean you wouldnt have to hand-write an identity-like traverser13/07 16:50
pigworkerindeed, never again13/07 16:53
--- Day changed Thu Jul 14 2011
molerisagundry: You about?14/07 13:20
agundrymoleris: I am indeed14/07 13:21
agundrywhat's up?14/07 13:21
molerisI'm just trying to wire the Problem simplification to the Prop simplifier14/07 13:21
molerisBut I'm getting confused14/07 13:21
molerisAre the prfs you get back from the simplifier all open terms?14/07 13:22
agundryit depends on the proof in question14/07 13:24
agundrysorry, I should have integrated the simplifer for propositional hypotheses as well as goals14/07 13:24
molerisOk, so for instance: Simply _P0 prfPImpP0 prfP0ImpP14/07 13:26
agundryOkay, the data structure has changed slightly so Simply has two arguments14/07 13:26
molerisSimplyOne wven14/07 13:26
moleriseven14/07 13:27
agundryah, right14/07 13:27
agundryso _P0 is a Prop (not a Set, which it used to be)14/07 13:27
molerisOk14/07 13:27
agundryprfPImpP0 is a closed* proof of P => _P0, where P is the original proposition14/07 13:28
agundryand by closed, I mean it only contains level variables referring to parameters in the original context14/07 13:28
molerisright14/07 13:28
agundryprfP0ImpP is a proof of P with one extra level parameter (at the next fresh level)14/07 13:29
agundryand a proof of P0 should be substituted for that level parameter14/07 13:30
molerisOk, this probably explains my problem14/07 13:30
agundryit's not actually an implication14/07 13:30
molerisI guess thats because if P decomposes to more than one part, it's easier this way?14/07 13:31
agundryyes, it generalises so that in the Simply case, you still get a proof of P but with more free level variables14/07 13:31
molerisOK, cheers14/07 13:31
agundryif you want a function with multiple arguments, you can construct one (and somewhere in the propsimp code it does that)14/07 13:32
molerisI think I have all the bits I need now14/07 13:32
agundrygood14/07 13:32
molerisSimplyOne is just a pattern synonym right? so I only have to write a case for Simply?14/07 13:33
agundryyep14/07 13:33
agundrythere's also a SimplyTrivial pattern synonym14/07 13:33
agundryyell when you find all the bugs I've missed...14/07 13:34
--- Day changed Mon Jul 18 2011
roconnortypes are blue?18/07 13:25
pigworkerroconnor: yeah18/07 13:39
pigworkercanonical type constructors are blue, anyway18/07 13:39
roconnorpigworker: and they are blue because they are Tory, right?18/07 14:11
pigworkeryes18/07 14:12
pigworkerof the old-fashioned paternalistic variety18/07 14:14
* edwinb looks around for a pigworker 18/07 16:13
pigworkeredwinb: I'm around and about18/07 17:42
augurpigworker: so who is agundry18/07 17:48
augurit seems you know each other in the real world18/07 17:48
pigworkeraugur: agundry is one of my PhD students18/07 17:55
auguraha!18/07 17:55
auguri wish my profs were on irc18/07 17:59
edwinbpigworker: oh, sorry, I went. Just wanted to check if turning up tomorrow around lunch time was still okay18/07 19:53
edwinbit can only be a day trip but I expect I can stay quite late...18/07 19:54
augurpigworker: why is [] : * not * -> *?18/07 20:15
pigworkeredwinb: yes, that's good -- let us know when you're on your way and I'll advise the venue18/07 21:53
pigworkeraugur: in what context?18/07 21:53
edwinbpigworker: righto18/07 21:54
--- Day changed Tue Jul 19 2011
augurpigworker: is your family the first plt dynasty?19/07 04:30
pigworkeraugur: I think Goguen and Goguen might be earlier19/07 09:06
agundrymoleris, pigworker, stevan: morning19/07 10:25
pigworkermorning, we're at the coffee stage...19/07 10:25
edwinbthat's good, so am I...19/07 10:27
edwinbright, looks like I'll get to Glasgow just in time for you all to have had lunch19/07 11:04
pigworkerdon't bet on it19/07 11:08
edwinbno, I suppose not19/07 11:09
edwinbI'll be there about 2 anyway19/07 11:09
agundryJust in case anyone other than me is hacking on the Pig, I've just pushed a patch fixing the Monad fail problem19/07 11:10
pigworkerthanks; this may yet happen19/07 11:27
edwinbit turns out a 0 minute change at Haymarket is only just impossible19/07 13:20
agundryedwinb: what's your ETA?19/07 13:58
edwinbI'm in pigworker's office now...19/07 14:07
--- Day changed Wed Jul 20 2011
pigworkeragundry: morning!20/07 09:52
agundrypigworker: good morning20/07 09:52
agundrywhat's the plan for this morning?20/07 09:54
pigworkerseems to be a slow start... just making coffee now, no sign of my guests yet; but I've shipped a resit20/07 09:55
pigworkerwe should probably meet here, to avoid network nonsense20/07 09:56
agundryrightyo20/07 09:56
agundryI'm at school now, so I can come over whenever20/07 09:56
pigworkerI think the plan is to investigate nixed definitions and fix the sodding occur check.20/07 09:56
pigworkerYou're welcome whenever, as long as you don't mind bleary people.20/07 09:58
agundryokay, I'll pop by in a bit20/07 09:58
--- Day changed Fri Jul 22 2011
* pigworker is happily pulling a bunch of patches22/07 12:09
--- Day changed Wed Jul 27 2011
Saizanwhen epigram will get universes, in which one will (A : Set) == (B : Set) be? Set or Set1?27/07 23:22
--- Day changed Thu Jul 28 2011
augurSaizan: when you will get grammar, in which one will "when epigram will get universes, ..." be? grammatical or ungrammatical?28/07 10:22
molerispigworker: Good news, I've fixed the bug that stopped the recursive call to plus elaborating28/07 11:30
pigworkeryay!28/07 11:30
molerisBad news, |plus two two| only elaborates to |'s (plus ('s 'z) ('s ('s 'z)))|28/07 11:31
pigworkerha! whnf!28/07 11:31
molerisMaybe, I tried to wire the eager evaluator up to the front end and still got the same result28/07 11:33
molerisBut that could mean any number of things28/07 11:33
pigworkeryeah, the recursive call might not be elaborating successfully to an ih call (check the term?), or the induction operator might have a glitch, or we might not be delta-ing aggressively enough, or...28/07 11:35
pigworkerSaizan: I think it goes like this (and we should do this anyway, before we stratify)... each level is closed under set-equivalence, so if A and B are in Set0, A <-> B is in Prop0, meanwhile, the value equality (A : Set0) == (B : Set0) : Prop1 unpacks to A <-> B, which is ok by cumulativity.28/07 11:39
Saizanoh, i had forgotten about <->. A <-> B : Prop0 for A, B : Set0 should fit my use of free theorems so i like it :)28/07 11:54
pigworkerto be fair, so had we, but it seems right that A <-> B is morally a special case of (A -> B) * (B -> A) and so is small; the Agda model of OTT agrees, and we don't need to quantify over Set to explain what it means for two particular sets to be equal28/07 12:22
Saizannice to know there doesn't seem to be a fundamental reason to push type equality one level up, agda's stdlib made me worry28/07 12:30
pigworkerYeah, it's kind of a cusp. I'd expect equations between things in, say (Set0 -> Set0) to live in Prop1. Arguably, small-indexed set families can be equated in Prop0 as they involve only small quantification, but I'm unhappy about defining a Prop0 by recursion over Set128/07 12:33
pigworkerIt reminds me of the universe hierarchy two-step. Starting from some base universe (U, T), construct a universe (U', T') by closure under Pi, Sigma, etc; then build (U'^, T'^) by adding just a code for U'; repeat ad nauseam.28/07 12:36
Saizanso you wouldn't like A <-> B : Prop0 for A, B : Nat -> Set0 ?28/07 12:38
Saizani guess that doesn't even typecheck28/07 12:39
pigworkersomething like that would have to be heterogenously defined by recursion over a (benevolent?) fragment of Set1, rather than fixed for Set0; makes me nervous, but I accept that (m n : Nat) -> (m : Nat) == (n : Nat) -> F m <-> G n is small28/07 12:42
pigworkerI guess we'll see where we get bitten.28/07 12:43
Saizanalways on the edge :)28/07 12:45
molerispigworker: "... or the induction operator might have a glitch"  Indeed28/07 14:33
moleris> elab plus two two28/07 14:33
moleris's ('s ('s ('s 'z)))28/07 14:34
pigworkerfour!28/07 15:22

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