--- Log opened Wed Jun 01 00:00:16 2011
molerisagundry: Morning01/06 09:11
agundrymoleris: good morning01/06 09:11
molerisHow's things?01/06 09:11
agundrygood thanks01/06 09:12
agundryI started working on schemes, but still have a few issues to resolve before I push01/06 09:12
molerisHeh, how did you guess my question ;)01/06 09:13
agundryhe he01/06 09:14
agundryI notice that you got some approximation to matching working01/06 09:14
molerisHm, yeah - I kinda gave in and got the old one working again01/06 09:14
agundryah okay01/06 09:15
agundryOne question about schemes: I'm not sure which representation to use for binders01/06 09:16
agundryIt seems like levels are nicer than indices01/06 09:16
molerisOk01/06 09:18
agundryDoes that seem reasonable? I'm just worried that I'm missing something01/06 09:18
agundryIt makes turning a scheme into a type harder, but I don't think we generally do that without elaborating01/06 09:19
molerisYeah, I think it's reasonable01/06 09:20
molerisEither way you go is a compromise I suppose01/06 09:21
agundryhmm, should the name resolution code for schemes be working?01/06 09:26
molerisNope01/06 09:28
agundryThat might be why I can't see them01/06 09:28
molerisI broke it quite badly - I might go in and fix that now01/06 09:29
molerisSaves you having to trawl through my awful code01/06 09:29
agundryI tweaked it in a few places to extract schemes from entries01/06 09:29
agundrybut perhaps they are getting lost along the way01/06 09:29
molerisRight01/06 09:29
molerisSo I need your patches01/06 09:29
agundryI was just about to suggest that, hang on01/06 09:29
agundrypushed01/06 09:32
molerisTa01/06 09:33
molerisshouldn't take long01/06 09:33
agundrythanks01/06 09:34
agundry'let f (A : Set) : A' fails in name resolution, but I'm not sure if that's a bug in there or in the elaboration of schemes01/06 09:34
agundryInitially I was just trying to get 'let f : Set ; scheme f' tell me that f had a scheme01/06 09:36
molerisFailed to load interface for `DisplayLang.Scheme':01/06 09:38
molerisIn what way am I being dumb?01/06 09:38
molerisAh, got it01/06 09:39
moleris> scheme f01/06 09:41
moleris: Set01/06 09:41
agundrygood01/06 09:41
molerisI'll push this, then see if I can find the bug with 'let f (A : Set) : A'01/06 09:43
molerispushed01/06 09:44
agundryas I say, that could well be my fault01/06 09:45
molerislooks like the A gets introduced in the wrong place01/06 09:46
molerisso yeah - you (:01/06 09:46
molerisyou can see it if you do 'f (A : Set) : Set ; show state'01/06 09:47
moleris'A' is inside 'tau'01/06 09:47
molerisThe name resolver shouldn't crash though01/06 09:47
molerisSo I'll fix that01/06 09:47
agundryokay, I'll check it out01/06 09:48
molerishmm, I guess 'A' should be in 'tau' but it also should be in the main module01/06 09:49
molerisor something01/06 09:49
molerisNo, what am I talking about01/06 09:50
molerisSorry01/06 09:50
molerisIgnore everything I just said01/06 09:50
molerisOk, I've pushed a second patch with fixes the pattern match fail in findParam 01/06 09:54
molerisif you get that, you can see what goes wrong01/06 09:54
agundryta, I think I see the problem in scheme elaboration01/06 09:55
molerisI have done some Label stuff which we can add to the mix soon, I think I need a coffee though - back in a sec01/06 09:57
agundrymoleris: I've pushed some patches with a bit more progress, though schemes under shared parameters are broken at the moment01/06 11:44
molerisagundry: Thanks (:01/06 11:49
molerisHow much of a hassle are shared parameters?01/06 11:50
agundryI don't know, I haven't really figured out why they aren't working01/06 11:52
agundryIt probably is nothing particularly deep01/06 11:53
molerisFair enough01/06 11:54
molerisWhat is it that goes wrong?01/06 12:00
agundryIf you do 'module M ; lambda A : Set ; let x : A' then x gets given the scheme (A : Set) : A^101/06 12:03
agundrywhich I think means the A is referring to the lambda-bound rather than scheme-bound copy01/06 12:04
agundryalso elaborating such a thing (e.g. with 'infer') gives an error, but I think I see why that is01/06 12:05
molerisInside M should 'scheme x' say ': A'?01/06 12:14
agundryyes, I think so01/06 12:15
agundryactually no, wait01/06 12:15
agundry'scheme' doesn't remove shared parameters at the moment01/06 12:15
agundryI think I've just fixed part of the problem01/06 12:16
agundryMaybe I'm worrying too much; what does A^1 mean these days?01/06 12:26
agundryWhich way does the numbering go?01/06 12:26
molerisHat counts backwards01/06 12:27
agundrythat's what I thought01/06 12:27
agundryso the scheme (A : Set) : A^1 is probably wrong01/06 12:27
molerisIt's not quite right, no01/06 12:29
molerisBut it may just be a display problem 01/06 12:30
agundrybrb01/06 12:30
agundryokay, so I think it's actually storing the correct scheme, it's just pretty-printing it without removing the shared parameters01/06 12:41
molerisYup01/06 12:41
molerisI think it only makes sense if you remove them01/06 12:42
agundryFortunately that's very easy to do with the level representation01/06 12:42
molerisGood01/06 12:44
agundryFix pushed01/06 12:44
molerisThat was quick (:01/06 12:46
moleris'let f {A : Set} (a : A) : A ; lam A ; lam a ; give a' ...01/06 12:51
moleris(assuming we have some B : Set, b : B for the following)01/06 12:51
moleris'elab f b' gives 'b'. Yay!01/06 12:52
moleris'infer f b' gives 'A'. Boooo01/06 12:52
molerisalso 'infer f' is way off the mark with 'a : !!!.A_0) -> a'01/06 12:53
agundryyep, looks like infer f results in some dangling levels01/06 12:54
molerisStill, we're getting there01/06 12:54
agundryI should probably get on with something else, but good luck with the bug-hunting01/06 13:06
molerista01/06 13:07
molerisagundry: Starting to suspect the bug I'm looking for has nothing to with Schemes after all01/06 15:08
agundrythat's possible, have you made much progress?01/06 15:10
molerisWell, I've just come up with an example that goes wrong without invoking any of your code01/06 15:11
moleriswhich is progress of sorts :)01/06 15:11
agundryhmm, it's gratifying to know that I'm not the only source of bugs ;-)01/06 15:13
molerisNot by a long chalk01/06 15:14
agundrythough I was expecting the problem to be in the elaboration code for things with schemes01/06 15:14
agundrywhat's your example?01/06 15:14
moleris> make T : Set ; pi A : Set ; pi a : A ; give A01/06 15:18
moleris> make f : T ; lam A ; lam a ; give a01/06 15:18
moleris> infer f Set01/06 15:19
moleris(a : !!!.A_0) -> A01/06 15:19
molerisSo the same example, basically :)01/06 15:19
agundryhow puzzling01/06 15:23
molerisI suspect the piLifting mechanism01/06 15:25
agundryit certainly could be that one of the P-variables in the type of f is not getting turned into a V01/06 15:27
--- Day changed Mon Jun 06 2011
agundrymoleris: ping06/06 13:41
molerisagundry: Pong06/06 13:42
agundryI've been enhancing the ugly-printer and I think I made some progress on your buy06/06 13:43
agundry*bug06/06 13:43
molerisAh, OK - what have you found?06/06 13:44
agundryThe faulty type has a level-open term appearing in an index environment06/06 13:44
agundrybut environment concatenation seems to assume that index environments are level-closed06/06 13:44
agundry(and enforces that they are index-closed)06/06 13:44
molerisI think I'd come to conclusion it was a problem with environments06/06 13:47
molerisso thats good06/06 13:47
molerisor bad, depending on which way you look at it06/06 13:47
agundryPresumably index environments ought to be level-closed?06/06 13:49
agundryThe trouble is, I'm not sure how to track down the code that is violating that assumption06/06 13:49
molerisNo idea how the faulty env arises either06/06 13:49
moleristhe pi-lifter, the likely source of the error, uses envs to capture some Ps as Vs06/06 13:50
agundryit doesn't create an index env, though, just a level one06/06 13:52
molerisTrue06/06 13:52
molerisActually I don't see why IEnvs should be L closed06/06 13:54
agundryI can't see how to write level concatenation if they are open06/06 13:55
molerisThat might be the reason (:06/06 13:56
agundryIt's also possible that I'm missing something...06/06 13:56
agundryIn the cons case of (<<<) on Tm.lhs line 319, we are assuming e doesn't contain any levels from gl06/06 13:57
molerisAh, OK06/06 13:57
agundryI tried to insert an extra closure, but then you get a term with m index variables rather than an index-closed one06/06 13:58
molerisWe're assuming that in an Env (gl, gi) that gi is closed wrt to gl06/06 14:01
molerisWhich makes sense06/06 14:01
agundryyes06/06 14:01
agundrycareful, though, in the code gl and gi are separate envs06/06 14:02
molerisha06/06 14:02
moleristhe name choice isn't great there, then06/06 14:02
agundryoh no, sorry, I'm being stupid06/06 14:03
agundryyou're right06/06 14:03
agundrythe envs are (gl, gi) and (gl', gi')06/06 14:03
agundrybut the point is that gi' is not closed wrt gl06/06 14:03
molerisRight06/06 14:04
molerisOK, we might be in business06/06 14:18
molerisLet me just run the test06/06 14:18
molerisagundry: Still there?06/06 14:24
agundryyep, have you worked it out?06/06 14:25
agundryI'm still confused06/06 14:25
molerisI have, I think06/06 14:25
molerisThe fix that you already tried, to close e over gl works06/06 14:26
molerisbut only if (<+<) :: Env {Z} {n} -> Env {n} {o} -> Env {Z} {o}06/06 14:26
molerisWhich, luckily, is all we need06/06 14:26
agundryah ha06/06 14:26
agundryI didn't think about restricting the type of (<+<)06/06 14:26
agundryof course that makes sense06/06 14:26
molerisPushing a patch - can you just check that it works for you06/06 14:26
agundrysure06/06 14:27
molerisI really should try to be better with versioning - I've got about three things on the go in my repo - all with unrecorded changes06/06 14:28
agundryouch06/06 14:28
agundrypatch looks good at this end06/06 14:28
agundryI'll push my improved uglyprinter shortly, in case it is useful in other debugging efforts06/06 14:28
agundryone thing I have discovered is that we generated a lot of pointless closures06/06 14:29
molerisIt will certainly06/06 14:29
molerisIt happens06/06 14:29
molerisCheers for spotting that - I was struggling06/06 14:31
molerisCase of wood for the tress maybe06/06 14:31
agundryyou're welcome06/06 14:32
agundryMaking the ugly printer go under closures meant I had a much better chance of seeing what was happening06/06 14:32
agundrypatch pushed, in case you want to have a look yourself06/06 14:34
molerisTa06/06 14:34
molerisagundry: Don't suppose you're up for having a look at a new propogation bug are you06/06 15:01
molerisnews, not new06/06 15:01
agundryoh goody06/06 15:03
agundrygo on then06/06 15:03
molerisI don't think it's a bad one, but I'd hope you'd be able to spot it quicker than me (I did have look, honest)06/06 15:03
molerisSo, news about a definition's children doesn't seem to be being told to the definition06/06 15:04
molerisFor insatnce:06/06 15:04
molerismake X : Set ; make Y : Set ; out ; give Y ; give Set ; out ; elab X06/06 15:05
agundryI see06/06 15:06
molerisIt works if Y isn't a child of X though06/06 15:06
agundryI simplified the relevant bit of news propagation when updating it, but I must have introduced a new bug06/06 15:06
agundryaargggh06/06 15:34
agundryit was a stupid typo06/06 15:34
agundryfix pushed06/06 15:38
molerisThanks (:06/06 15:39
--- Day changed Wed Jun 08 2011
molerisquit08/06 16:49
--- Day changed Thu Jun 09 2011
augurholy crap conor's a hardcore twitterer09/06 07:38
--- Day changed Fri Jun 10 2011
molerisagundry: Ping10/06 12:56
agundrymoleris: pong10/06 13:57
agundryI just generated a picture of the module dependency graph for Epigram, it's quite amazing10/06 14:02
moleris:D10/06 14:05
agundryhow's you?10/06 14:05
molerisGoing mad - but I've almost got Pierre's ewam code working again10/06 14:06
molerisI want to change the term rep slightly though - and just need a sanity check10/06 14:06
agundryhaving ewam would be great, especially if I don't have to implement any of it...10/06 14:07
molerisIt turns out that having to explain all of the Levels or none of them in an Env is a pain in the backside10/06 14:07
agundrythat's true10/06 14:07
agundrydo you have a better proposal?10/06 14:07
molerisSo I propose |type LEnv {n} = [(Int,Tm {Body, Exp, n})]|10/06 14:09
agundryassociation list?10/06 14:09
agundrysounds good10/06 14:09
molerisWith the semantics that if the lookup fails then it's the identity on that P10/06 14:10
agundryI think that makes sense, and would make various lifting things much less painful10/06 14:11
molerisOk, I think I'll move to another branch get implement this change10/06 14:12
molerisWill save a lot of faff in Elimination.lhs10/06 14:12
agundryrightyo10/06 14:14
molerisYou up to anythign interesting?10/06 14:14
agundryin other news, I was feeling in need of some boredom so I decided to fix the Epitome so it builds again10/06 14:14
molerisAh10/06 14:14
molerisexcellent10/06 14:15
agundryDo you want me to push a patch? It touches rather a lot of the codebase (mostly changing comments into lhs2TeX-friendly ones)10/06 14:15
molerisErm10/06 14:15
molerisYou can do10/06 14:15
agundryIt's no trouble to wait if you want to push some changes first and let me merge them10/06 14:16
agundryI've also got a plan for simplifying the ProofState hierarchy, but that could be similarly invasive10/06 14:16
molerisGo for the Epitome patches - maybe hold off on the Hierachy ones though10/06 14:20
agundryokay, will do10/06 14:21
agundryI haven't started on the hierarchy anyway10/06 14:21
agundrydone10/06 14:25
agundryanything else I can usefully get on with?10/06 14:32
molerisProbably :)10/06 14:34
molerisHere's a question - what is supposed to solve hoping equations? Is it the ProblemSimplifier10/06 14:35
agundryThere's a thing in Elaboration.RunElab called simplifyProof10/06 14:37
agundrythat tries the propositional simplifier and looks for solvable equations10/06 14:38
molerisSo there is10/06 14:38
agundryit then leaves solutions lying around for the scheduler to find10/06 14:38
agundry(of course, none of this is switched on at the moment)10/06 14:38
molerisno10/06 14:39
molerisI had a look at the Prop simplifier10/06 14:39
molerisIt scared me more than the EWAM code so I decided to fix that instead10/06 14:39
agundrythat's understandable10/06 14:40
molerisDid you write it?10/06 14:40
* agundry blushes10/06 14:41
molerisHah, I didn't mean it like that10/06 14:41
agundryI can take a look if you like, a lot of the complexity is scope management pain10/06 14:41
agundryso that will certainly be different now (if not necessarily easier)10/06 14:41
molerisI think easier10/06 14:41
molerisor should I say hope10/06 14:42
agundryWe'll see; your new notion of level environment might be useful10/06 14:42
molerisIt needs fixing sooner or later, if you want to do it then great - otherwise I'll get round to it at some point10/06 14:42
agundryI'll have a go10/06 14:43
molerisCool - new environments will be with you soon I hope10/06 14:44
agundrymoleris: how do we eliminate proofs of false these days?10/06 16:21
molerisif you look in Evidences/Tm.lhs there's a bunch of primitive definitions10/06 16:33
moleristhere should be one call zeroElimDEF or something, i forget exactly10/06 16:34
agundryoh ta10/06 16:35
molerisI pushed a patch with the new envs btw, then I realised that they are broken wrt schemes, and probably more10/06 16:36
molerisSo be wary before pulling10/06 16:37
agundryI think I pulled that already, oh well10/06 16:40
molerisI think I found it10/06 16:42
molerisA fix will be out before knocking off time ;)10/06 16:43
molerisIt is just Schemes as far as I can see10/06 16:43
molerisFix pushed (though this by no means guarantees the new Envs work)10/06 16:49
agundrythanks10/06 16:51
--- Day changed Tue Jun 14 2011
molerisagundry: About?14/06 10:37
agundrymoleris: indeed14/06 10:37
agundryand thinking propositional simplification thoughts14/06 10:37
molerisGood good (: I don't like to feel alone in the Epigram darkness 14/06 10:38
molerisWe're almost in a position to have some fun with the thing again though14/06 10:38
auguro.o14/06 10:39
agundryyes, I see some EWAM patches have emerged14/06 10:39
augurso is Epigram 2 out yet14/06 10:39
augur:P14/06 10:39
molerisaugur: It's as close as it's ever been14/06 10:40
agundryI'm not sure that's saying much...14/06 10:41
molerissshhh14/06 10:41
agundryIn the simplifier, I'm having trouble building proofs that can be re-typechecked14/06 10:45
moleris:|14/06 10:46
molerisWhat sort of errors are you getting from the type checker?14/06 10:46
agundryI need to make a term like \ x -> falseElim (f x) (t x)14/06 10:47
agundrywhere f and t are closed expressions14/06 10:47
moleriso I c14/06 10:48
agundryI can weaken them (using wk) but I end up making a redex that breaks the typechecker14/06 10:48
agundrysince sometimes (but not always) f and t will be canonical14/06 10:49
molerisReally? What sort of Cans?14/06 10:51
agundrywell, lambdas14/06 10:51
agundryso not Cans in an epigram sense14/06 10:52
molerisno, I see what you mean now though14/06 10:53
agundrythe trouble is the typechecker doesn't like beta-redexes, but I can't evaluate them away because I'm under a binder14/06 10:53
molerisYep, so I think the type checker needs a slight rethink14/06 10:59
molerisIf you can't do evaluaion under a binder it needs to be a bit smarter when it goes under one14/06 11:01
agundrywhat do you mean?14/06 11:02
molerisI don't know14/06 11:02
moleris:)14/06 11:02
molerisSo we can't type check (_G :/ L ...) :$ as14/06 11:09
molerisis that the problem?14/06 11:09
agundryyes, I think so14/06 11:09
molerisIs it too much hassle to make definitions of f and t?14/06 11:12
agundryhmm, I guess I could thread a name supply14/06 11:17
molerisMaybe we should address the real problem instead14/06 11:18
agundrymaybe, I'm not sure how though14/06 11:24
molerisnope14/06 11:25
agundrymaking definitions seems to work (though I've just made up names rather than threading the name supply so far)14/06 11:25
molerisTrouble is - I just ran into the same problem14/06 11:35
molerisagundry: I've had a thought14/06 16:36
molerisah, actually - no I haven't. As you were14/06 16:38
agundryfair enough14/06 16:39
molerisMuch progress?14/06 16:39
agundryI've been avoiding thinking by working on propositional simplification 14/06 16:39
agundryand simple cases now work14/06 16:39
agundrythe new representation seems to make it a bit cheaper (just insert closures rather than traverse terms) but no more comprehensible14/06 16:40
agundryHow about you?14/06 16:41
molerisI persuaded some bits of the problem simplifier to go14/06 16:41
moleristhe bits that don't rely on the propositional simplifier 14/06 16:42
agundrygood14/06 16:44
agundryI wonder if we ought to think about redesigning some of the problem simplifier / relabelling machinery14/06 16:44
agundryrather than simplifying aggressively (and introducing too much strictness), then renaming everything, we should let the user supply a problem decomposition14/06 16:46
molerisWe should give the user control over what happens to pattern variables you mean?14/06 16:46
agundryyes14/06 16:46
agundryI think that was always the plan, we just never quite got there before14/06 16:47
agundryright, I'm off, see you later14/06 17:03
molerisyup, byee14/06 17:03
--- Day changed Mon Jun 20 2011
pigworkeragundry: how do?20/06 12:44
agundrypigworker: okay thanks, though I seem to be the only one in the office20/06 12:45
pigworkerI've started wondering about integer types for Epigram...20/06 12:46
agundryWhat about them in particular?20/06 12:46
agundryWe've vaguely talked about them in the past, but never quite got there20/06 12:47
pigworkerI was wondering if it was worth making them a special case.20/06 12:47
pigworkergotta go -- delivery man just arrived, back in a bit20/06 12:48
agundryhmm, you mean something like adding magic elaboration/constraint solving rules?20/06 12:50
agundrySounds like a good idea20/06 12:52
agundryIt might be a good way to figure out how to fit this stuff into System FC and get some kind of proof automation, because you'd probably want a similar bunch of axioms and an induction principle20/06 12:54
pigworkerDelivery amusingly fails to deliver the thing we went to IKEA to buy. We got our 100 tea lights, though.20/06 12:59
pigworkerBut anyway.20/06 12:59
agundryI probably shouldn't ask what you are planning to do with 100 tea lights...20/06 13:00
pigworkerI was wondering whether ranges with optional bottom and top ends would be good.20/06 13:00
agundryAs in your ordered data structures stuff? Quite possibly20/06 13:01
pigworkerThe 100 tea lights are a metaphor for a large quantity of random tat that seemed like a good idea at the time. In this instance, I think they are actually a hat rack.20/06 13:01
pigworkerYeah, so types Z, Z(a..), Z(..b), Z(a..b)20/06 13:02
agundryah, my metaphor spotting fails again; that makes more sense20/06 13:03
agundryWould you want those all to be types? Couldn't you just add a type (<=)?20/06 13:03
pigworkerwe did get some candles, but we're still ok for tea lights from last time20/06 13:03
pigworkerThey'd be types, one way or another. We like Nat and Fin. I'm wondering whether we should leave it all to Prop-wrangling or if there's an advantage to baking ranges in.20/06 13:06
pigworkerSomewhat nervously, I'm wondering if there's scope for (gasp!) subtyping.20/06 13:07
pigworkerWorse, I'm fed up with + having rubbish definitional equality, when we know its equational theory is rather rich and relatively tractable.20/06 13:09
agundryI wasn't expecting you to suggest subtyping... but a better definitional equality for + would certainly be nice20/06 13:10
agundryWhat does subtyping buy you over Z(a..) := Sig (n : Z ; a <= n) and a few projections? A bit less clutter, I guess?20/06 13:11
pigworkersucs to the front, associativity, commutativity; it could just work20/06 13:11
agundryit ought to; perhaps we could even get symmetry in a few naughty special cases, though maybe that's too hackish20/06 13:13
pigworkerwe could think about what's relatively straightforward20/06 13:14
pigworkersubtyping would only be worth it if we jacked it up structurally Tm Z(0..n) <= Tm Z(0..n+1)20/06 13:16
agundryah of course20/06 13:16
pigworkersubtyping does play havoc with implicit syntax, though20/06 13:17
pigworkerWe should also think about subset types, more generally.20/06 13:18
agundryby subset types you mean sigmas with proof components?20/06 13:20
pigworker{x : S | P x}, used like elements of S, but with silent management of propositional baggage20/06 13:20
pigworkerso yes, sigmas with one piece of data, plus proofs, with less noise about wrapping and unwrapping20/06 13:21
pigworkerlike in Matthieu Sozeau's thesis20/06 13:22
agundryI regret that my French isn't good enough to read Sozeau's thesis...20/06 13:25
agundrysubset types + proof irrelevance definitely sounds like a combination worth pursuing20/06 13:26
agundrythough I worry that it's a trade off with how much implicit argument synthesis we can get20/06 13:26
pigworkerSubset types would work like functions with implicit arguments: they have default silent eliminations (projections here, not applications), but with some sort of manual override.20/06 13:32
agundryokay, I see, so under the hypothesis (y : {x : S | P x}) we infer the type S for y but have manual overrides for y ! and y -20/06 13:48
agundryI presume this happens at the elaboration level rather than being baked into the evidence language?20/06 13:49
pigworkeryep20/06 13:58
--- Log closed Mon Jun 20 18:39:37 2011
--- Log opened Mon Jun 20 19:01:03 2011
-!- Irssi: #epigram: Total of 15 nicks [0 ops, 0 halfops, 0 voices, 15 normal]20/06 19:01
-!- Irssi: Join to #epigram was synced in 152 secs20/06 19:02
--- Log closed Tue Jun 21 01:08:31 2011
--- Log opened Tue Jun 21 01:08:36 2011
-!- Irssi: #epigram: Total of 14 nicks [0 ops, 0 halfops, 0 voices, 14 normal]21/06 01:08
-!- Irssi: Join to #epigram was synced in 76 secs21/06 01:09
--- Day changed Wed Jun 22 2011
pigworkeragundry: sorry not in yet; sorting out my trip to London is proving more complex than I had expected22/06 13:26
augurpigworker: just be glad you have a working train network to be miffed about when its not working right22/06 13:37
pigworkerin this case, the overnight trains are working, but fully booked; will need a different plan22/06 13:39
pigworkeragundry: you about?22/06 14:42
agundrypigworker: I'm back22/06 14:56
agundryI can leave now and meet you for a brief chat, if you like?22/06 14:57
pigworkeryes please! I have to pack!22/06 14:59
agundryon my way22/06 15:00
--- Log opened Wed Jun 22 20:24:41 2011
-!- Irssi: #epigram: Total of 16 nicks [0 ops, 0 halfops, 0 voices, 16 normal]22/06 20:24
-!- Irssi: Join to #epigram was synced in 74 secs22/06 20:25
--- Day changed Tue Jun 28 2011
pigworkermoleris: how do?28/06 10:08
molerispigworker: No bad, yerself?28/06 10:10
pigworkernothing more sleep wouldn't cure28/06 10:10
pigworkerhow was Glasto?28/06 10:10
molerisheh, I know that feeling.28/06 10:11
molerisVery good - despite the mud28/06 10:11
pigworkerone of M's pals was having a last night in Nice'n'Sleazy before flying back to Australia; I was the oldest person in the pub28/06 10:12
pigworkerbut we should probably plot some activity28/06 10:13
pigworkerhow's July looking? wk beginning 11th or 18th look ok just now28/06 10:16
molerisYes, we should indeed28/06 10:17
moleristhe 18th is probably better for me at the moment28/06 10:17
molerisTravelling on the Monday28/06 10:19
pigworkerok, Mon-Thu's good; need to jump on a train on Fri28/06 10:19
edwinbhello world28/06 10:20
molerisedwinb: hallo28/06 10:21
pigworkeredwinb: wotcher28/06 10:21
pigworkerhow about a bit of piggery-jokery?28/06 10:22
edwinbI was thinking I haven't come over to play for a while28/06 10:22
* pigworker could use a nice day at the seaside, also28/06 10:22
molerispigworker: In that case either week would involve travel on Monday and Friday for me28/06 10:23
molerisso no strong preference28/06 10:23
agundryI see the game is afoot28/06 10:24
agundryeither week works for me28/06 10:24
pigworkerstevan: how about you?28/06 10:25
pigworkerprobably, the week of the 18th is better (M will be in Wales, so we can use her study as a bedroom without too much disruption)28/06 10:26
molerisSounds good28/06 10:27
pigworkerthere might even be an actual bed in it, if IKEA get their act together...28/06 10:28
pigworkerlet's pencil that week (18-22 July) in and see what we can make of it28/06 10:31
molerisYup28/06 10:33
agundrysounds good28/06 10:33
pigworkerwhere are we at just now, anyhow?28/06 10:35
* pigworker runs make28/06 10:36
molerisWe're getting there28/06 10:38
molerisI had just rebuild the EWAM code, and was looking at data when I ran into the P bug28/06 10:39
molerisI just implemented your suggested fix, and it gets rid of my blocker - which is good28/06 10:39
pigworkercool, so we might reach 4 soon?28/06 10:40
molerisvery soon28/06 10:40
molerisagundry was looking at propsimplify, which needs fixing for unification to happen - not sure where he is with that28/06 10:41
agundryI've been making progress, but having issues with the inability to re-typecheck terms28/06 10:42
agundryI hope your fix will help28/06 10:42
pigworkerin what way? ah, that way28/06 10:42
pigworkeragundry: is your retypecheck really necessary?28/06 10:42
agundrywell, that's an interesting question28/06 10:43
pigworker(yes might well be the right answer)28/06 10:43
agundryit is useful to detect bugs in the propositional simplifier28/06 10:43
molerisah, in that case I should record a patch28/06 10:43
agundryI've also been running into other issues with the typechecker which I have been trying to understand28/06 10:43
pigworkerhave we got a switch for extra assertions?28/06 10:44
agundryI'll try things out again when moleris pushes a patch, and see what still doesn't work28/06 10:44
agundrypigworker: not at the moment28/06 10:44
molerisagundry: pushed28/06 10:44
agundrymoleris: ta28/06 10:45
pigworkerafter all, a big part of the plan was geared around avoiding eval-quote cycles28/06 10:46
agundryonce we are confident the simplifier worked correctly, we could certainly turn off the check, but it would be nice to be able to check in the first place28/06 10:49
pigworkersure; I just wanted to clarify the role the check was playing; we certainly need that diagnostic facility28/06 10:50
pigworkergotta step away; back in a bit28/06 10:51
molerisagundry: patch help much?28/06 11:02
agundrya little, but I'm still getting headTySpine failures because of other redexes28/06 11:04
agundryI'm trying to work out how to do more evaluation when constructing simplified propositions28/06 11:04
agundrybut I might have to just stop typechecking the results of simplification28/06 11:05
molerishopefully we won't write too many bugs into that code (:28/06 11:07
molerisoo, a fire alarm28/06 11:11
molerishow exciting28/06 11:11
* edwinb ponders linear types again28/06 12:48
edwinbI wonder what breaks...28/06 12:48
pigworkeredwinb: if you manage phase properly, not much, I bet28/06 12:51
edwinbit seems that sticking them in their own corner of the type hierarchy makes lots of problems go away28/06 12:52
edwinbthen you control carefully how values can move between those bits of the hieararchy28/06 12:52
edwinbthen you don't spend days writing resource managing DSLs, you just write functions...28/06 12:53
edwinbit seems so simple that something must go wrong...28/06 12:53
pigworkerit does sound plausible; might be worth checking out works of Pym and Ishtiaq28/06 12:56
edwinbadding a universe of linear types would be much easier if Idris knew anything about universes28/06 13:55
pigworkerhave you already got "irrelevant Pi"? (i.e. intersection?)28/06 14:07
edwinbno, nothing clever at all28/06 14:10
* edwinb will bodge it as usual for the sake of experimentation28/06 14:10
pigworkerI'm just thinking that in a linear (x:S) -o T x, you might need to write \ x -> t where x occurs more than once, but only once in a place that survives to run time.28/06 14:18
edwinbyou might, which makes things interesting28/06 14:20
edwinbalthough not for the application I'm interested in at the minute28/06 14:21
edwinbbut at least that is more restrictive than it needs to be, rather than less28/06 14:22
pigworkerI also wonder how far you can get with nondependent -o28/06 14:22
pigworkerI've just had a daft idea...28/06 14:24
pigworkerOnce upon a time, we had this plan to adapt System F style Church-to-Curry erasure to dependent type theory.28/06 14:25
edwinbthere is a question of when to allow aliasing, with resources. (x:S) -o T x where x is clearly shared safely, is a place where you'd want to allow it28/06 14:25
* edwinb remembers this plan28/06 14:26
pigworkerThe basic idea (if you're not edwinb and weren't there (in the Cask and Barrel iirc)) is to label the colons with some notion of phase or region, then have a variable rule  ..., x :i S, ... |- x :j S  if  i <= j  where the order somehow reflects "staticness".28/06 14:28
edwinbhang on, got to go, will be back and read up...28/06 14:29
pigworkerlambda, pi, application are similarly region sensitive; you can use dynamic stuff statically (that's the whole point of dependent types) but static stuff can't be used in dynamic places28/06 14:30
pigworkeryou can then erase everything above any given level28/06 14:31
pigworkerthis allows to mediate one notion of erasure to optimise open-term computation in typechecking, and a more aggressive erasure for closed-term computation at run-time28/06 14:32
pigworkerbut there is no reason to make <= a total order!28/06 14:33
pigworkerI wonder if we could set up a calculus in this style with two incomparable regions, such that programs can be disentangled into two separately executable components.28/06 14:36
pigworkerof course, we'd want the two components to communicate somehow, but over some sort of restricted channel...28/06 14:39
edwinbhmm, that took longer than I expected28/06 17:47
edwinbThis erasure calculus plan seems like it'd be a good idea some time. As does optimising open term type checking.28/06 17:52
edwinbI'd quite like to set up epic to be able to compile open terms28/06 17:52
dolioErasure calculus plan/28/06 17:53
edwinbmaybe calling it a "plan" is premature28/06 17:53
dolioI was really more interested in the erasure calculus part. :)28/06 17:54
* edwinb wonders where the logs live so he doesn't have to repeat what pigworker just said28/06 17:55
pigworkerhttp://epigram.orangesquash.org.uk/28/06 17:55
edwinbaha. http://epigram.orangesquash.org.uk/2011/June.log.html28/06 17:55
pigworkerreminds me of FlowCamL28/06 17:58
dolioI'm a bit unhappy at how the erasure stuff ended up in Agda.28/06 18:01
dolioThe actual dependent uses are still not allowed, and Andreas has examples where it'd cause weird behavior.28/06 18:02
dolioAnd I don't know how to solve them.28/06 18:02
pigworkerI can't remember how it's done in Agda (are there rules?), so I don't know if we get bitten the same way.28/06 18:06
dolioI think it's fairly close to the Mishra-Linger and Sheard stuff, although it's superficially different.28/06 18:07
pigworkerI realise it's rich to ask for rules, of course.28/06 18:07
dolioBut Agda has type-directed stuff in its definitional equality, while the EPTS stuff doesn't.28/06 18:08
dolioSo, you end up wondering if you should eta expand f : _28/06 18:08
dolioWhere _ is an erased type or something.28/06 18:09
dolioI think that's more or less the nub.28/06 18:10
pigworkerdoesn't sound too friendly, but we love eta28/06 18:10
pigworkeryeah, equality for neutral terms is type-reconstructing28/06 18:11
dolioThe EPTS stuff doesn't do eta and such, so they don't need to keep types around to decide equality.28/06 18:11
pigworkerI see.28/06 18:11
pigworkerI also see a (pricey?) fix.28/06 18:12
dolioSo, if you wanted to do eta, you probably have to eschew open-term, during-checking erasure. At least prima facie.28/06 18:12
pigworkerDon't actually do the erasure, just mark the "erasables"; don't compare marked terms for equality, but do use them in type reconstruction.28/06 18:13
pigworkerI'm trying to write some rules down at the moment.28/06 18:19
pigworker(not for erasure, just now) but the game (in a sort of a Bob Constable way) is to present definitional equality as a PER28/06 18:20
dolioOh, I should note, you can actually do '.(x : A) -> ...' in Agda now.28/06 18:22
pigworkerwhat happens?28/06 18:22
dolioBut '.(x : A) -> B x' is not allowed unless B : .A -> Set28/06 18:22
pigworkerbooo!28/06 18:22
dolioBut the only such Bs are constant functions.28/06 18:22
dolioAnd it isn't even useful as a phantom type, because the equality knows that B x = B y for all x and y.28/06 18:23
pigworkerif you take being well-typed to mean being def-equal to itself, you get a clue that you can't throw away for equality info that you expect to need in typechecking28/06 18:26
pigworkerbut maybe that model doesn't fit so well with erasure28/06 18:29
--- Day changed Wed Jun 29 2011
pigworkerhttp://www.e-pig.org/epilogue/?p=914  and  http://www.e-pig.org/epilogue/?p=955  for the beginnings of some technology which might help us formalise the Epigram kernel29/06 17:13
--- Day changed Thu Jun 30 2011
* Saizan would have guessed DepRep to be that technology30/06 00:25
pigworkerSaizan: I don't want to predicate the existence of a formal spec on figuring out how to give every feature the DepRep treatment.30/06 02:01
pigworkerliyang: how's tricks?30/06 02:04
liyangmorning!30/06 02:05
pigworkerwell, I was thinking of crashing, but then you appeared30/06 02:05
liyangback in the office after Glasto.30/06 02:05
liyangawfully warm these last couple of days in the UK...30/06 02:06
pigworkerI can see that's something of a comedown30/06 02:06
liyangHow's Glasgae30/06 02:06
pigworkernot as warm, but still too warm30/06 02:06
pigworkerwhat's the opposite of hibernation?30/06 02:07
liyangAnything in particular keeping you up?30/06 02:08
pigworkernope; net chat; a full bottle in front of me30/06 02:08
pigworkeroh, and the Soft Boys doing a ridiculous cover of Astronomy Domine30/06 02:10
liyang(opposite of hibernum?)30/06 02:10
pigworkerI mean being put into a stupor by summer30/06 02:10
pigworkeraestivation?30/06 02:11
liyang"Aestivation (from Latin aestas, summer) is a state of animal dormancy[1], characterized by inactivity and a lowered metabolic rate, that is entered in response to high temperatures and arid conditions."30/06 02:13
liyangSounds right.30/06 02:13
pigworkerthe only cure is czech lager30/06 02:13
pigworkeror just rolling with it30/06 02:14
* Saizan wonders if there's a smart way to do induction over Go EqC eqf (ze & _ !- T :> t === t) _30/06 02:17
pigworkerno chance30/06 02:18
pigworkerbut x & G !- T :> t === t for suitably x-compliant T and t, perhaps30/06 02:19
Saizantrue, but my problem was more that i need to pattern match on T and t to make eqf compute30/06 02:20
Saizanrather than getting the derivation to tell me what they are30/06 02:21
pigworkerthat's the state of play, just now30/06 02:21
pigworkersomehow it'd be good to capture derivable case analyses30/06 02:22
pigworkerI wonder if anyone has ever thought about that30/06 02:22
Saizanderivable case analyses?30/06 02:25
pigworkeryeah, datatypes are born with a notion of constructor case analysis; but a given telescope can have many splittings into cases by composite eliminations30/06 02:27
pigworkerand when you write a function, you generate such a composite case analysis; it should not be hard to record it and re-invoke it in a proof30/06 02:28
pigworkerCheck travaux de Balaa et Bertot.30/06 02:29
Saizani've thought that with some powerful reflection one could create a datatype out of a function by essentially an Agda -> Twelf conversion30/06 02:31
pigworkerIt shouldn't be that hard. Given levitation-style data, we should be computing the code for the datatype as part of the process of elaborating the function.30/06 02:33
pigworkerHence Go, as it happens.30/06 02:34
Saizanah, yes, since you still have access to the source of the function30/06 02:40
pigworkerindeed -- and the free monad nicely exposes the call structure30/06 02:43
Saizanbut the  "Sigma S T -> IDest (Sigma S T)" we can manage to build out of a "(s : S) -> Prog A B S T (T s)" in agda won't give us a nicer induction principle for free, afaiu30/06 02:58
Saizans/IDest/IDesc/30/06 02:58
pigworkerYes. To know the representation is not to known the reasoning method (type is more than representation; type isomorphism should not be equality). It's worth studying what it is to be a case analysis of S, especially given a presentation of S as a finite sum.30/06 03:09
agundrypigworker: are you likely to be in the office today or tomorrow?30/06 12:06
agundryit would be useful to chat30/06 12:06
pigworkergotta stay home just now (awaiting delivery), but could be in tomorrow30/06 12:07
agundryokay, I'm unconstrained tomorrow and you know where to find me30/06 12:12
pigworkercool30/06 12:17

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