/home/laney/.irssi/irclogs/Freenode/2010/#epigram/September.log

--- Log opened Wed Sep 01 00:00:16 2010
-!- mode/#epigram [+v dolio] by ChanServ01/09 00:54
-!- mode/#epigram [+v pigworker] by ChanServ01/09 01:51
-!- mode/#epigram [+v dolio] by ChanServ01/09 01:54
-!- mode/#epigram [+v dolio] by ChanServ01/09 03:51
-!- mode/#epigram [+v dolio] by ChanServ01/09 05:51
-!- mode/#epigram [+v dolio] by ChanServ01/09 06:20
-!- mode/#epigram [+v pigworker] by ChanServ01/09 07:37
-!- mode/#epigram [+v dolio] by ChanServ01/09 08:54
agundrypigworker: ping01/09 13:16
+pigworkerhi01/09 13:16
agundryare you about this afternoon?01/09 13:16
agundryit would be good to chat01/09 13:17
+pigworkerI was planning on not being about, and struggling with cgi scripting.01/09 13:17
agundryah okay, I can amuse myself then01/09 13:18
+pigworkerIs there a pressing dilemma? I can be in tomorrow.01/09 13:19
agundrynot really, and I'm not in tomorrow...01/09 13:19
+pigworkerAh, yes. I remember you saying so, now.01/09 13:20
agundryjust out of curiosity, which library are you using for CGI?01/09 13:20
+pigworkerI'm using Network.CGI, but that's just a random choice. I'm more than willing to learn better.01/09 13:20
+edwinbI looked around CGI libraries once, and didn't find anything better that wasn't really heavyweight...01/09 13:22
agundryI don't know any better, since I've not done any web programming in Haskell. It would be interesting to try though.01/09 13:22
+pigworkerI'm not doing anything wild. Just now, I'm trying to configure my local server to run .cgi executables...01/09 13:23
+pigworkeragundry: Friday ok? Or would a slot later today be useful, if I could dig myself out..?01/09 13:24
agundryFriday's okay with me, and any time is fine01/09 13:25
+pigworkerAim for 11am and see what happens?01/09 13:26
agundryokay, see you then01/09 13:26
+edwinbpigworker: don't you just need to put them in /Library/WebServer/CGI-Executables?01/09 13:29
+edwinbor are you doing something slightly more wild?01/09 13:29
+pigworkerI'm working under ~/SItes/01/09 13:30
+edwinbI've only ever managed to do it in the top level cgi-bin directory01/09 13:30
+pigworkerI've just added a ScriptAlias to my apache .conf file, hitting ~/Sites/cgi-bin/   seems to work01/09 13:30
+pigworkerdon't know what I've broken by doing that, of course01/09 13:31
+edwinbtoday I'm mostly trying to make my computer work well enough to run agda again01/09 13:31
+edwinbI seem to be having a bad computer week01/09 13:31
+edwinbI can have macports command line tools working, or ghc working, but not both at once01/09 13:32
+edwinbpity agda needs both01/09 13:32
+pigworkeredwinb: I understand your pain.01/09 13:35
+edwinbI can have both if I stick with ghc 6.10 from macports of course...01/09 13:36
+edwinbbut then I can't compile... anything interesting.01/09 13:36
+edwinbso, now for ghc 6.12.3 from source to see if that helps01/09 13:36
+edwinbgood job I have papers to review ;)01/09 13:36
+edwinbmy CPU isn't going to be much use today after all01/09 13:36
+pigworkergood luck!01/09 13:37
+edwinb"cabal: cannot configure base-3.0.3.2. It requires base >=4.0 && <4.3"01/09 13:48
+edwinbthat's almost funny01/09 13:49
molerisagundry: ping01/09 14:38
agundrymoleris: pong01/09 14:39
moleriswe were wondering if you could have a quick look at a bug for us :)01/09 14:39
agundrycertainly01/09 14:39
molerisI've pushed test/recbug.pig01/09 14:39
agundryprovided it's an Epigram bug ;-)01/09 14:39
molerisheh01/09 14:39
molerisdamn..01/09 14:39
molerisTis a tiny (in fact, empty) universe construction01/09 14:40
molerisI would expect it to be a complete definition, but we're left with a goal to justify the recursive call to |el|01/09 14:41
agundrythat's not surprising, the recursion spotter is not very clever01/09 14:41
molerisSo you think it's just not spotting the justification in the context?01/09 14:44
agundryyep01/09 14:45
molerisrather than not being able to infer the args?01/09 14:45
agundrypretty much anything other than variables or canonical forms confuse it01/09 14:45
agundrythe problem here is the application01/09 14:45
molerisyup01/09 14:45
agundryextending it to deal with application of identical functions shouldn't be too hard01/09 14:45
molerisok, we'll have a go :)01/09 14:46
molerisunless you want to01/09 14:46
agundryI'd rather you had a look at my code and possibly figured out a better way to do it ;-)01/09 14:47
agundryyou want to look at the section "Hoping for labelled types" in Elaboration.RunElab01/09 14:48
molerisfair01/09 14:48
molerischeers01/09 14:48
agundryor rather, you don't want to look at it, as pedagand can tell you01/09 14:48
agundrygood luck ;-)01/09 14:50
molerisIt's a good thing pedagand can't get on irc right now..01/09 14:52
agundryI bet01/09 14:53
agundrymeanwhile, I am trying to figure out what pigworker's notion of an .epi file should look like in Haskell01/09 14:54
molerisagundry: Something approximating a fix has emanated from pedagands laptop01/09 15:56
agundryhmm, I see a slightly uncertain patch01/09 15:57
agundrylooks plausible01/09 15:58
molerisit's the next approximation to the right answer01/09 16:01
agundrygood01/09 16:04
pedagandwow, tsapi, you've caught an impressive tan :-)01/09 23:55
--- Day changed Thu Sep 02 2010
-!- mode/#epigram [+v pigworker] by ChanServ02/09 08:36
-!- mode/#epigram [+v pigworker] by ChanServ02/09 08:55
tsapipedagand: it's just dirt :)02/09 09:48
pedagandtsapi, :-)02/09 09:57
tsapiwhy should I write "define plus 'zero n := n" instead of just "= n"?02/09 10:37
tsapialso, the name choices have got worse again, it chooses xf^1 as the name of the first argument to plus now.02/09 10:40
tsapidefine plus ('suc xf^1) n := 'suc (plus xf^1 n)02/09 10:43
tsapiI'm sorry, Dave. I'm afraid I can't do that.02/09 10:43
tsapiError: relabel: can't match xf^1 with xf^102/09 10:43
tsapi= 'suc (plus xf^1 n)02/09 10:43
tsapiTa.02/09 10:43
pedagandyou would "define plus ..." to give the nice name 'n' instead of suffering with the Pig generated one02/09 10:55
pedagandas for the "can't do that" problem, you could report a bug02/09 10:55
pedagandprobably, there is shadowing of xf from the left to the right side02/09 10:56
pedagandwhat happens if you write xf^2 on the right?02/09 10:56
tsapipedegand: ah, I see. I'll check xf^2. 02/09 10:58
tsapidefine plus ('suc xf^1) n := 'suc (plus xf^2 n)02/09 11:00
tsapiI'm sorry, Dave. I'm afraid I can't do that.02/09 11:00
tsapiError: relabel: can't match xf^1 with xf^102/09 11:00
pedagandwell, that was a wild guess anyway02/09 11:03
pedagandwhenever you've time, please report this bug02/09 11:04
tsapii will02/09 11:04
pedagandyesterday, we did some pretty sick changes to the unifier, so this might be related02/09 11:04
tsapidefine plus ('suc m) n := 'suc (plus m n)02/09 11:07
tsapithat works :)02/09 11:07
tsapibug reported02/09 11:13
pedagandthanks!02/09 11:35
-!- mode/#epigram [+v pigworker] by ChanServ02/09 12:26
tsapimoleris: you there?02/09 13:40
-!- mode/#epigram [+v pigworker_] by ChanServ02/09 13:53
* pigworker_ is just testing a new client02/09 13:54
moleristsapi: here02/09 14:08
molerispigworker: hola02/09 14:13
+pigworkerarternoon02/09 14:13
tsapimoleris: your subject descriptors are mangled: "D [3]: m"02/09 14:13
molerisI've just squashed the last HF occurence02/09 14:13
+pigworkeryay!02/09 14:13
tsapiMs. Tolles can't fix them.02/09 14:14
moleriswe are, 9 months later, first order again02/09 14:14
tsapican you send an updated abstract to me and her?02/09 14:14
molerisWill push in a sec02/09 14:14
moleristsapi: Oh crap, I hate those things02/09 14:14
tsapiD.3.2 [Programming techniques]: Applicative (Functional) Programming;02/09 14:14
tsapiD.3.3 [Programming languages]: Language Constructs and Features---Data02/09 14:14
tsapitypes and structures.02/09 14:14
tsapishould do the trick02/09 14:14
tsapiI guess she only has a pdf02/09 14:15
+pigworkerwhy in these days of google we need to put up with this crap is beyond me...02/09 14:15
tsapiand me... I'm not sure if anyone cares. Sheridan don't. She proposed just replacing it with "D.3.2, D.3.3"02/09 14:16
tsapimoleris: (re. HF) yay!02/09 14:18
-!- mode/#epigram [+v pigworker] by ChanServ02/09 14:22
* pigworker had a peculiar network glitch there...02/09 14:24
molerisNow I have to remember the particular tool chain that produces acceptable pdfs, I got this wrong last time around02/09 14:27
+pigworkerIt was roughly at that point that I found my dirty libiconv redirect did have consequences...02/09 14:28
+pigworkerI made bad .pdf but ok .ps, so they coped.02/09 14:29
* pigworker is downloading short films about a short person from Estonia02/09 14:31
+pigworkerMeanwhile, I wonder if we can identify the places where we need to be strict about head-normal forms.02/09 14:33
tsapipigworker :)02/09 14:37
+pigworkertsapi: I reckon he's got your eyes!02/09 14:38
tsapipigworker: poor chap!02/09 14:38
tsapipigworker: By the way, this is the film Aive was working as a set designer on: http://news.err.ee/culture/042f2d7a-fd55-4214-915f-5ac7d45bc064. In case you stumble upon it...02/09 14:39
+pigworker"manor house on stilts"? cool02/09 14:41
moleristsapi: email address for Ms. Tolles?02/09 14:44
tsapilisatolles@sheridanprinting.com02/09 14:47
molerista02/09 14:48
molerissent02/09 14:53
molerispigworker: You think you could put up with me visting Glasgow before/after the IR meeting02/09 14:54
+pigworkersounds good to me02/09 14:54
+pigworkerI gotta fly to the USA on the 19th, though, so before is probably better02/09 14:55
molerisrighto02/09 14:56
+pigworkerMeanwhile, I'm thinking about heading to Beeston this Sunday, northbound on Wednesday. House gets priority, but I'm sure I'll manage at least the extracurricular parts of AIM.02/09 15:11
molerissounds good02/09 15:13
tsapimoleris: sorry Peter! I was suggesting to have both subject descriptors (3.2 and 3.3)02/09 15:23
tsapimoleris: the whole thing is an anachronism02/09 15:24
tsapimoleris: but, if it is there it should be correct02/09 15:25
moleristsapi: Hah, I think my brain has melted02/09 15:51
-!- mode/#epigram [+v pigworker] by ChanServ02/09 17:15
-!- mode/#epigram [+v pigworker] by ChanServ02/09 19:00
-!- pumpkin is now known as copumpkin02/09 22:18
--- Day changed Fri Sep 03 2010
-!- mode/#epigram [+v pigworker] by ChanServ03/09 09:01
pedagandagundry: pushed the patch for issue #7403/09 09:50
agundrypedagand: thank you03/09 09:50
agundryI will investigate03/09 09:51
agundryAre you planning to change seekLabel any more?03/09 09:51
agundryah03/09 09:52
pedagandhell, no! :-D03/09 09:52
agundryOkay, I have a plan that might result in a simpler version, will experiment and see if it works.03/09 09:52
pedagandgoodo03/09 09:53
agundrypf-Sigma is not getting lambdas introduced because problem simplification doesn't introduce them inside PRF03/09 09:53
pedagand"them"? lambdas? I just want pf-Sigma in the context, as a whole. Isn't that possible?03/09 09:55
agundryoh sorry, I was misreading the term, nevermind03/09 09:55
agundrytoo many brackets...03/09 09:55
agundryyup, it's a bug03/09 09:56
pedagandis it serious doc?03/09 10:00
agundryThe problem simplifier is generating a term that doesn't typecheck03/09 10:00
agundryand I can't immediately see why.03/09 10:00
pedagandlet me know when I shall start digging the grave :-)03/09 10:09
tsapidoes idata currently only support one parameter and one index?03/09 10:28
tsapiidata Vec (X : Set) : Nat -> Set. We can't have idata List (X : Set) : Set ?03/09 10:29
agundrytsapi: I think so, at the moment03/09 10:30
agundryas I understand it, the labelling scheme/anchors needed to be sorted out first03/09 10:30
agundrymoleris?03/09 10:30
+pigworkeragundry: on my way in a minute...03/09 10:45
agundrypigworker: okay, see you soon03/09 10:45
molerisagundry: problem?03/09 10:49
molerisoh, idata03/09 10:49
agundrymoleris: lots of problems, but I was just checking with you about my answer to tsapi's question03/09 10:50
molerisindeed should have read the msg history (:03/09 10:50
moleristhe idata tactic supports any number of parameters, but only one index03/09 10:51
molerispedagand keeps sighing in the seat beside me, which suggests that his porting of anchors to idesc is causing problems, but hopefully that will lift the index restriction03/09 10:52
tsapimoleris: any number except zero? or is this the parser?03/09 10:53
tsapigotta go, I have to go sing happy birthday to my office.03/09 10:53
tsapior, more likely, listen to some more nostalgic speaches03/09 10:56
moleristsapi: you there?03/09 11:37
-!- mode/#epigram [+v pigworker] by ChanServ03/09 12:30
pedagandanyone in Strathclyde HQ?03/09 16:01
agundrypedagand: hello03/09 16:01
pedagandwhat's the situation wrt. Epigram there?03/09 16:01
agundryI showed pigworker the demo and we had a long conversation about elaboration03/09 16:02
agundryno progress on your bug so far, I'm afraid03/09 16:02
pedaganddiscussion leading to a conclusion, or just to even more discussion?03/09 16:03
agundrydiscussion is always coinductive ;-)03/09 16:03
pedagandthe "elaboration" of the source language (or whatever we call it), right?03/09 16:03
agundryelaboration of anything, really03/09 16:03
+pigworkerRe bug: I'm worried about where that quantified equation is coming from. I wouldn't expect it to be useful.03/09 16:03
agundrywe have a couple of proposals which I am writing up03/09 16:03
agundryas issues03/09 16:04
agundrythat equation is clearly not useful, but the simplifier is still broken03/09 16:04
pedagandagundry: goodo, would be great if we could know about that, we might work a bit this week end here03/09 16:04
pedagandpigworker, agundry: which equation stuff are you talking about? the bug?03/09 16:05
agundrypedagand: that would be good03/09 16:05
agundrypedagand: yes03/09 16:05
agundryyour test case has a hypothetical equation that simplifies to false03/09 16:06
pedagandok. It comes from Peter's writing real code in Epigram. This man is frightening.03/09 16:06
pedagandthere is a qui proquo then: you seem to be talking about #74, I was thinking of #7003/09 16:07
agundryyes, issue #74, sorry for the confusion03/09 16:08
agundrywe haven't discussed #70 but I might have a plan anyway03/09 16:09
+pigworkermust remember where the bug tracker is...03/09 16:09
pedagandall right03/09 16:09
agundrypigworker: http://code.google.com/p/epigram/issues/03/09 16:09
pedagandor you click up there on e-pig.org, everything is listed there03/09 16:10
pedagandanyway, I might get the IDesc anchoring working in a few03/09 16:11
pedagandit's disgusting tho03/09 16:11
+pigworkerta03/09 16:11
pedagandon my side, moleris is exploding probsimp, after having slaughtered Cochon so that it eats a Prelude03/09 16:17
agundrysounds exciting03/09 16:17
agundryI think fixing #74 will involve modifying the probsimp case for |PI (PRF p) t|, at least I guess that's where the problem is.03/09 16:18
agundryI can happily wait until moleris pushes some patches, though.03/09 16:18
pedagandhe is not playing in that some, so you can go ahead03/09 16:19
pedagandthe merge will be easy03/09 16:19
pedagands/some/zone/ (strange typo indeed)03/09 16:20
agundryOh okay, what is he modifying then?03/09 16:20
molerisagundry: About to abandon a misguided foray into ProbSimp03/09 16:24
molerisso no danger of conflict03/09 16:25
+pigworkerI need to go home and worry about things.03/09 16:27
tsapimoleris: I'm here now03/09 16:36
-!- mode/#epigram [+v pigworker] by ChanServ03/09 16:45
moleristsapi: Whats your problem with Fin?03/09 16:50
molerisidata Fin : Nat -> Set := (zero : (n : Nat) -> Fin ('succ n)) ; (succ : (n : Nat) -> Fin n -> Fin ('succ n)) 03/09 16:51
molerisshould work03/09 16:51
tsapioh! I thought you needed to have one type parameter03/09 16:52
molerisno, any number, including zero03/09 16:53
tsapiexcellent03/09 16:54
-!- Irssi: #epigram: Total of 14 nicks [0 ops, 0 halfops, 3 voices, 11 normal]03/09 16:54
tsapibut the type has to be 'something -> Set' right?03/09 16:55
molerisfor the moment03/09 16:55
molerisI'd love for it to be zero or one, which might happen imminently03/09 16:56
moleris(zero or one indexes)03/09 16:57
tsapithat'd be nice03/09 16:57
+pigworkerI'd propose a right-nested record of indices, which you could sneakily curry out.03/09 16:57
tsapioh, you can overload constructor names?03/09 16:57
molerisyup03/09 16:58
+pigworker'cos they're not names!03/09 16:58
+pigworkerat least, not in the sense of "identifiers with scope"03/09 16:58
molerispigworker: right nested records, yes.03/09 17:01
molerisneed to work out how to get the currying, uncurrying to happen03/09 17:02
moleriswith pedagand's anchors03/09 17:02
--- Day changed Sat Sep 04 2010
tsapiis there something like lambda that works inside a programming problem?04/09 18:12
tsapidata Nat := (zero : Nat) ; (suc : Nat -> Nat)04/09 18:12
tsapidata Nat := (zero : Nat) ; (suc : Nat -> Nat)04/09 18:13
tsapilet plus (m : Nat) : Nat -> Nat04/09 18:13
tsapilambda n04/09 18:13
tsapiI'm sorry, Dave. I'm afraid I can't do that.04/09 18:13
tsapiError: lambdaParam: goal is not a pi-type or all-proof.04/09 18:13
tsapianyone there? I think I found a bug with Fin.Ind04/09 20:24
tsapihttp://code.google.com/p/epigram/issues/detail?id=7804/09 20:31
moleristsapi: Not a bug04/09 20:40
moleristhe index to i is ('suc m)04/09 20:41
molerisso you should say <= Fin.Ind ('suc m) i04/09 20:41
pedagandI've been walking on Losehill all day long, it's pretty much like coding Epigram:04/09 21:37
pedagandyou know there is Winhill on the other side, with Hope in the middle04/09 21:37
tsapi:)04/09 21:37
pedagandsorry for the interlude :-)04/09 21:37
tsapiI just filed another bug04/09 21:38
pedagandexcellent04/09 21:38
pedagandhaha, memalloc FAILED...04/09 21:39
pedagandI'm going to push the Anchors on IDesc. If it blows things up, don't be afraid to roll it back.04/09 22:04
pedagandit's a disgusting hack, I'm flagellating myself for having committed such horror04/09 22:06
molerispedagand: You still there?04/09 22:50
pedagandyep04/09 22:59
pedagandmoleris: I'm not going to implement any form of Prelude tonight tho :-)04/09 23:00
molerisfair enough04/09 23:04
molerisjust wondering if there were any plans for tomorrow?04/09 23:05
pedagandnop, no plan04/09 23:15
+edwinboh, hello. Nice walk today?04/09 23:15
moleriswouldn't be able to tell you04/09 23:16
pedagandthat was good04/09 23:16
molerisglad you appreciated the place names04/09 23:16
pedagandUlf "overslept" just as you did, apparently :-)04/09 23:17
molerishah04/09 23:17
molerislazy, lazy people04/09 23:17
+edwinbI woke up early enough but decided not to go anywhere...04/09 23:17
+edwinbI expect I'll do the same tomorrow ;)04/09 23:17
LaneyThe P&J is a very comfortable place, clearly…04/09 23:18
pedagandedwinb: fair enough :-)04/09 23:18
+edwinbsounds like nobody has made any plans anyway...04/09 23:19
moleriswell, if you want to do anything low key04/09 23:19
molerislike, lunch, for instance04/09 23:19
+edwinbI did explore Nottingham today, which is good, because I don't have to do that again now04/09 23:19
pedagandLaney: not quite, I don't have a table in my room. So, I'll be probably be forced to spend the day in a Cafe. Oh, too bad :-)04/09 23:20
molerisand edwinb isn't in the P&J (:04/09 23:20
+edwinbnot even a sofa in the lobby?04/09 23:20
+edwinbI'm on a sofa in the hotel bar now...04/09 23:21
+edwinbthere are two people with laptops here, and a woman at the bar who is selling no beer and probably extremely bored04/09 23:21
pedaganddunno if there is a sofa, but I won't stay all day in the sofa, or people will think I'm the clerk or something04/09 23:23
pedagandanyway, if you guys makes plans, I'll be delighted to join04/09 23:23
+edwinbI'm unlikely to make a plan, but I could well join if one develops...04/09 23:23
pedagandbut if you want to enjoy a quiet sunday, I'll cope04/09 23:23
+edwinbI'll probably sit on a sofa and fix bugs04/09 23:24
LaneyI recommend Lee Rosy's tea rooms, there are worse places to spend an afternoon than there04/09 23:24
Laneyfree wifi too. :)04/09 23:25
+edwinbsounds ideal ;)04/09 23:25
pedagandindeed, thanks04/09 23:25
LaneyI could be tempted to join you for some time too04/09 23:26
pedagandfor writing bugs or for drinking tea? :-D04/09 23:26
moleriswriting bugs isn't exactly the aim now is it?04/09 23:26
pedagandI guess, both are reasonable things to do in the end..04/09 23:27
pedagandho, sorry, then I misread our Mission Statement04/09 23:27
moleriseasily done04/09 23:27
pedagandsince the beginning, I write bug, fix correct codes, and reduce sharing04/09 23:28
pedagandsounds like we're consensusing for Lee Rosy? Around which time should we meet there?04/09 23:29
moleris11am?04/09 23:30
pedagandthat's fine by me04/09 23:30
pedagandI can't find on google maps tho, do you the approx. address?04/09 23:31
pedagand*have04/09 23:31
molerisyeah, odd that it doesn't show - I was just checking that04/09 23:32
molerisit's opposite the broadway cinema, on broad street04/09 23:32
pedagandta04/09 23:32
--- Day changed Sun Sep 05 2010
tsapipedagand: you'll pleased to know I still get the same mem alloc FAIl with anchors05/09 08:41
pedagandtsapi, gorgeous :-)05/09 09:13
pedagandI've written new bugs without removing the old ones, I'm proud of myself05/09 09:14
tsapipedagand: :)05/09 09:19
pedagandI'll take a look at that this afternoon I think05/09 09:25
tsapicool, thanks05/09 09:30
+pigworker_Anybody alive and well and living in Nottingham?05/09 10:51
+pigworker_I'll arrive somewhere in the area, 9ish, if I'm lucky. Is there a pub plan?05/09 10:55
molerispigworker: No pub plan as yet05/09 12:04
molerisWe'll keep you informed though05/09 12:04
pedagandedwinb: we're at Lee Rosy (17 Broad street), if you feel like leaving your sofa ;-)05/09 12:14
+edwinbpedagand: still there? might join you in a bit if so05/09 15:11
molerisedwinb: we aren't right now butwe are still about05/09 15:26
+pigworkerNow that HF is gone, is there ever any reason to bquote?05/09 15:30
* edwinb watches pedagand try to get his Linux box to talk to the wireless05/09 16:32
* edwinb just connected his Mac to demonstrate how it works05/09 16:32
tsapi:)05/09 16:34
+edwinbserves him right for mocking Mac users the other day ;)05/09 16:38
+edwinbHoorah! He did it.05/09 16:41
pedagandedwinb: stop that!05/09 16:41
* pigworker is hoping that his MCO connection will work.05/09 18:15
--- Day changed Mon Sep 06 2010
pedagandtsapi, if I told you how many bugs are behind your issue #79, you wouldn't believe it...06/09 00:11
pedagandI mean "how many" as far as I can tell06/09 00:12
pedagandagundry: the 'tm' in solveHole' of Unification is supposed to be lambda-lifted or not?06/09 11:40
agundrygood question, let me have a look06/09 11:40
pedagandright, it's given lambda-lifted while the type expects a fully applied thing. Then, misery happens, as you would expect06/09 11:41
pedagand*right now06/09 11:41
agundryI think it should be given non-lifted06/09 11:42
agundrybut might well be buggy in this regard06/09 11:42
pedagandall right, then that's our bug. Thanks06/09 11:43
pedaganddo you have a few minutes to look at it? I've a small test case06/09 11:44
agundrysure06/09 11:44
agundrywas just making handleSchemeArgs use the error-reporting combinators properly, in the hope of dealing with that space leak06/09 11:45
pedagandI've pushed the test case06/09 11:48
agundrythank you06/09 11:48
pedagandif you fill '?' with 'f', that would go through06/09 11:48
pedagandbut having question mark leads to making a hole (of the right type), but the giveOutBelow in Unification is called on the ref of the goal (alone, not fully applied)06/09 11:49
pedagandand it blows up06/09 11:50
agundryyep, that definitely looks like a lambda-lifting bug06/09 11:50
pedagandto summarize: in RunElab, on the EWait corresponding to the question mark, we do the right thing, get the right reference06/09 11:51
pedagand(applied to its scope, therefore lifted)06/09 11:51
pedagandin Unification, we just have the reference of the goal, not applied its spine, and we (try to) give it06/09 11:52
pedagands/therefore lifted/therefore fully-applied/ (sorry)06/09 11:53
pedagandit was already so in 'resume' in the Scheduler06/09 11:58
agundryperhaps the news update mechanism is at fault?06/09 12:00
pedagandwhat I see is that we are moving the lambda-lifted object around (in solveHole, in resume, etc.) while we are supposed to manipulate/give the fully applied thing instead06/09 12:01
agundryyes06/09 12:04
agundrywhere does the lambda-lifted thing get introduced in the first place?06/09 12:05
pedagandI'm tracing it, Doctor Watson06/09 12:05
pedagandso far, I went back to 'makeWait' in RunElab06/09 12:06
agundryI really need to rewrite the seekLabel/makeWait stuff06/09 12:06
pedagandI wouldn't complain if you did so :-)06/09 12:08
pedagandso, I'm in seekIn now and I'm sinking as well06/09 12:08
pedagandha, the call of makeWait in seekIn is correct (fully applied)06/09 12:09
agundryhuh?06/09 12:10
agundrythere was me thinking the problem was in matchParams/valueMatch06/09 12:10
agundryAre the values in the substitution given to makeWait correct?06/09 12:11
pedagandthe term we giveOutBelow un-applied comes from the WaitSolve that is made by makeWait06/09 12:11
moleris[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[A[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B[B06/09 12:12
pedagandthe term that is given is the fully-applied one06/09 12:12
molerisI think a cat fell asleep on my keyboard06/09 12:12
molerissorry bout that06/09 12:12
pedagandI'm not very clear, sorry: 'g' is the fully applied object06/09 12:13
pedagandbut the 'v' we put in WaitSolve is lambda-lifted apparently06/09 12:13
agundrythat's the problem06/09 12:14
pedagandtherefore, I suspect that the thing making subst is buggy wrt. lifting (?)06/09 12:14
agundryyep, I think matchParams is generating a list with lambda-lifted values06/09 12:14
agundrywhen they should be fully applied06/09 12:14
pedagandElementary, my dear Watson, elementary. I try that, see what happens06/09 12:17
agundrywow, this code is confusing06/09 12:17
agundryhigherMatch is wrong06/09 12:18
agundryit's returning |pval gRef| which is lambda-lifted06/09 12:19
pedagandwell, I cannot make sense of any of this..06/09 12:20
agundrymea culpa, mea culpa, mea maxima culpa06/09 12:21
pedagandif you know how to fix it, go ahead06/09 12:21
agundryI'm trying something06/09 12:22
agundrywhat was I thinking when I wrote this?06/09 12:23
pedagandthat code is all right for a first draft. But we should not pile up drafts on top of each other. Usual rumbling..06/09 12:33
agundryindeed06/09 12:33
agundryI'm trying a quick hack to get things working06/09 12:33
agundrybut I need to refactor this lot properly06/09 12:34
pedagandok, thanks06/09 12:34
agundryright, I have a quick fix that appears to solve the problem, and the other test cases still pass06/09 12:44
molerisagundry: Thx (:06/09 14:00
molerisAnnoyingly, tsapi's original bug still doesn't go through in one go06/09 14:00
agundrywhich one, #79?06/09 14:01
molerismaybe this was never going to fix that, but I'm still annoyed (;06/09 14:01
molerisyeah, that code06/09 14:03
agundryI've not investigated that, but was under the impression from the bug reports that there were a few contributing factors06/09 14:04
agundryI am currently rewriting the recursive call search and matching stuff06/09 14:04
molerisI personally suspect that code for the error06/09 14:05
molerisSo I won't attempt a fix06/09 14:05
pedagandagundry: great, thanks06/09 14:21
agundrypedagand: do you have any interesting examples for which label lookup currently fails?06/09 16:57
agundrynevermind06/09 17:08
tsapiare Conor's comments on page 15 of the epitome about scopes still relevant? This plan has been enacted right? Should they be removed?06/09 23:08
pedagandtsapi: why on earth are you having such sinful thoughts at midnight? What's wrong with you? ;-)06/09 23:10
pedagandI'm compiling the Epitome but I suspect that it's about first-order things06/09 23:11
pedagandand that's a sensible topic these days :-)06/09 23:12
tsapitime has little meaning :)06/09 23:12
pedagandall right, it's about Yuk function application... Very sensible thing, indeed06/09 23:12
tsapinot that one, the next two comments06/09 23:13
pedagandoh, sorry06/09 23:13
pedagandsadly, my remark will be the same. So it goes:06/09 23:13
pedagandyou would have thought that the plan has been enacted06/09 23:14
pedagandbut actually, look at BetaQuotation.lhs06/09 23:14
pedagandbquote is a nice identity function06/09 23:14
pedaganda mangler would do its job if there wasn't a TT/VV distinction06/09 23:15
tsapiah06/09 23:15
pedagandso, you guessed it: change of term representation is in the air06/09 23:15
tsapiok, i just thought the prose was out of step with the code, but i guess it's not worth fixing if the code is about to get changed anyway...06/09 23:16
pedagandyeah, the code itself is out of step with the code06/09 23:17
tsapi:)06/09 23:17
* edwinb squelches back to his hotel06/09 23:19
* pedagand waits 10 minutes, for edwinb phone's battery to run out before criticizing edwinb (for having a Mac for instance)06/09 23:19
+edwinbpedagand: I'm on my Mac in the hotel bar ;)06/09 23:20
+edwinbon the wireless06/09 23:20
pedagandgotcha :-(06/09 23:20
+edwinb(it worked instantly, as you'd expect)06/09 23:20
pedagandshut up now!06/09 23:20
pedagand:-)06/09 23:20
+edwinbhehe06/09 23:20
pedagandI had to modprobe -r, modprobe, ifconfig, iwconfig, dhclient06/09 23:21
pedagandand it just worked as well06/09 23:21
pedagandLinux is user-friendly, simply that it chooses more carefully its friends than other OSes06/09 23:22
pedagands/simply that it/it simply/06/09 23:22
+edwinbyes, well, my Mac gets upset with my router at home06/09 23:22
+edwinbit won't talk to cheap hardware06/09 23:22
pedaganddamned posh thing, I just hate 'em :-)06/09 23:25
pedagandanyway, tsapi, I think it's faire to say that we're all fairly depressed here in Nottingham06/09 23:25
pedagand*fair06/09 23:25
pedagandspent last week shuffling sh*t around, had to threw it away today06/09 23:26
tsapiwhy so?06/09 23:26
pedagandthought we would start other things, but already know they will have to be thrown away06/09 23:26
pedagandand spent days tracking disgusting bugs, writing disgusting workaround code06/09 23:27
+pigworkerdelete it all now06/09 23:28
pedagandno way06/09 23:28
+pigworkerI can't deal with the fact that "delete it all now" doesn't follow from "it's disgusting"06/09 23:29
pedagandwhat would that change? 06/09 23:31
pedagandthere is no technical mistake in the code06/09 23:31
+edwinbif I did that, I don't think I'd ever have made anything...06/09 23:31
pedagandjust tactical mistakes in my opinion06/09 23:31
pedagandedwinb: you definitely have a point here, imho06/09 23:32
+pigworkerwhat's worth keeping?06/09 23:36
+pigworkerI am prepared to accept that there might be something worth keeping. I just want to hear it, that's all.06/09 23:37
pedagandI don't feel like playing this game, now and here06/09 23:38
pedagandwill chat that IRL tomorrow if you want too06/09 23:39
pedagand*to06/09 23:39
+pigworkerFair. I don't want to delete it all now. I do want to try to identify something positive to work from and towards.06/09 23:45
pedagandhopefully, we can sort this out tomorrow or when Peter comes in Glasgow06/09 23:50
+pigworkeryeah, I'm just depressed about neglect on my part06/09 23:51
pedagandin the meantime, I'm tired in a way that edwinb would describe as 'so French', so I will go to sleep :-)06/09 23:51
+pigworkerg'night06/09 23:51
+edwinbnight night06/09 23:52
--- Day changed Tue Sep 07 2010
tsapigood morning people of epigram07/09 07:43
+pigworkermorning!07/09 07:51
+edwinbmorning07/09 08:10
pedagandmorning07/09 08:10
+pigworkerthe radio tells me there's a big strike in France today07/09 08:11
pedaganddunno, but if they start chopping off royal and presidential heads, let me know, I don't want to miss that07/09 08:15
+pigworkersadly, there's no word of such festivities07/09 08:20
+pigworkermeanwhile, the big broken computer system in today's news is the one which calculates British tax07/09 08:21
+pigworkertheir mistake was to do arithmetic in binary07/09 08:22
+pigworkerhas just done the Epigram 1 name hack... (\ xs x -> f x xs) ys = \ y -> f y ys07/09 18:58
+pigworkermake test := \ X x -> _ : (P : Prop) -> :- P -> :- P;    works nicely07/09 19:52
pedagandcute07/09 20:19
+pigworkerYeah, but the real example fails mysteriously. Usual story. Need food just now, though...07/09 20:29
pedagandif I can remotely be of remote help, let me know.. I promise, I won't grumble, Laney told me how naughty a boy I am when I do that :-)07/09 20:32
pedagandbon appetit, btw07/09 20:34
pedagandfor type-level programming in Haskell, what is the 'sanest' way? Type families?07/09 20:34
+pigworkeroften, but not always07/09 20:35
pedagandwhat is the other one?07/09 20:37
pedagandnevermind, this is not urgent matter, stay focused on the epigram plumbing07/09 20:42
shaprright!07/09 21:45
shaprpigworker: Is your house haunted?07/09 21:46
+edwinbI heard there were some restless spirits in it07/09 22:13
* pedagand feels dirty: doing type-level "programming" in Haskell07/09 22:36
+pigworkerpedagand: the other (older) way to do type-level Haskell programming is with type classes and functional dependencies07/09 23:42
+Saizanwhich have the distinct advantage of OverlappingInstances and also allow bidirectionality07/09 23:44
+pigworkerI've definitely had examples which work better in one than the other, both ways around. Can't remember any just now, though.07/09 23:46
+pigworkeredwinb: the courvoisier isn't going anywhere07/09 23:50
--- Day changed Wed Sep 08 2010
+pigworkeragundry: ping08/09 11:06
agundrypigworker: pong08/09 11:07
+pigworkergot a(nother) mystery for you...08/09 11:07
+pigworkerit's a proof search thing08/09 11:07
agundryfire away08/09 11:07
+pigworkerI'll just push the patch with the file...08/09 11:08
+pigworkerI've just pushed the patch. It's an experiment with proof search.08/09 11:11
agundrypulled; investigating08/09 11:11
+pigworkerI'm trying to write an eliminator to compare two numbers, (x and y, say), adding a proof of either Le x y or Le y x to the context.08/09 11:12
+pigworkerGiven that I've defined Le ('suc x) ('suc y) = Le x y, I'm expecting the proof management in the two step cases to happen by search.08/09 11:14
agundryI see08/09 11:15
agundrybut search is failing, and giving xf seems not to terminate08/09 11:16
+pigworkerdoesn't terminate? or keeps asking for more?08/09 11:19
agundrysorry, that's what I mean08/09 11:19
agundrygive xf just leaves you at a new goal asking for a proof of the same proposition08/09 11:20
+pigworkeryeah, that's what happened to me08/09 11:20
+pigworkerit's just that I had tried adding some dumb tracing, using show, which caused a standstill: I wanted to be sure that I hadn't put that in my patch08/09 11:21
agundrySomething seems to be inserting an unnecessary coercion between (:- Le fx^5 fx^4) and itself, then trying to prove the reflexive equation by stupid means08/09 11:21
+pigworkerI was wondering if for some reason, def eq was rejecting that equation.08/09 11:22
agundryit feels like that might be the case08/09 11:22
agundrybut I don't know why it would08/09 11:23
+pigworkerhence my attempt at tracing (I wanted def eq to show me any two Props it was comparing); I suppose a cheaper trace would just report the result of the eq check in the searc process08/09 11:24
+pigworkersearch08/09 11:24
agundryand that just left you in a spin?08/09 11:28
+pigworkerI was just using show, which is asking for it, really08/09 11:29
agundrywe need to come up with a cheap way to print bits of terms (maybe a show-like gadget that takes a nesting limit)08/09 11:30
agundryyep, the definitional equality check performed by the elaborator for that type is failing08/09 11:44
+pigworkerI was thinking of writing an uglyprinter with much detail skippage08/09 11:44
+pigworkerit it somehow falling off the bottom? uncovered case, default False?08/09 11:45
agundryhmm, maybe08/09 11:45
agundryit seems we have Le ('suc x) ('suc y) reducing to Le x y but not definitionally equal to it08/09 12:05
agundryI wonder if a label is being left lying around somewhere and compared by the syntactic equality08/09 12:05
agundrycuriouser and curiouser08/09 12:34
agundrypigworker, you should find that if you replace |<= Nat.Ind y;| with |<= [y] Nat.Ind y;| then everything is fine08/09 12:34
agundrywithout the comma, elimination chooses a motive that includes a programming problem hypothesis08/09 12:36
agundryand somehow that makes Le ('suc x) ('suc y) store its original arguments somewhere in the stuck induction with label Le x y08/09 12:37
agundrycausing the definitional equality failure08/09 12:38
agundry...and with that, ttfn08/09 12:44
+pigworkerso, agundry's investigations reveal that we need to fix EWAM to spot and exclude prog hyps08/09 12:48
--- Day changed Thu Sep 09 2010
pedagandmoleris: when doing 'show state' of a data-ed data-type, you prefer to see the nice name or the code? I reckon that during the demo, you would have liked to show the 'Mu (Sigma ...)' thing09/09 00:00
copumpkindo Containers "reveal" the similarity between List and Vec?09/09 00:02
copumpkinor is there some kind of analysis that would show them having similar structure, despite different type indices09/09 00:02
pedagandcopumpkin: I think that this will answer your question: http://www.e-pig.org/epilogue/?p=57709/09 00:04
copumpkinoh, perfect :)09/09 00:04
copumpkinthanks09/09 00:04
copumpkinfascinating! Do you know what happened (if anything, yet) with "It’d be lovely to figure out how to lift ornaments to functions over data (how to get ++ from + ?). To do that, we really need to build a universe of ornaments for algebras, compatible with these ornaments for functors." ?09/09 00:15
moleriscopumpkin: Funny, pigworker reiterated his desire to find the answer to that question only last night09/09 00:54
copumpkinwow, I need to pay more attention to this channel :)09/09 00:55
copumpkinassuming it happened in here09/09 00:55
molerisactually it was over a pint09/09 00:55
molerisand the pub shut soon after, so we never found out (:09/09 00:57
copumpkindamn :)09/09 00:59
pedagandis anyone else having issues type-checking 'vec' defined here: http://personal.cis.strath.ac.uk/~conor/pub/she/pi.html09/09 12:56
pedagandin my version of She, it looks like 'deriving SheSingleton' does nothing09/09 12:56
pedagand(my version of She is the 'darcs' one, plus some speed-improvement hacks)09/09 12:58
pedagandsame problem with the official 'darcs' version09/09 13:01
pedagandsame problem with the released version... I'm puzzled...09/09 13:05
agundryI've not tried playing with the pi-type stuff she provides09/09 13:08
agundrybut are you sure your file is free from syntax errors?09/09 13:09
agundryshe has a habit of doing confusing things when one, say, omits a bracket09/09 13:09
agundryhurrah, I can now write  |refine plus m n <= Nat.Ind m| followed by |refine plus 'zero n = n|09/09 13:11
agundrybut I can't decide whether the second one should be = or := 09/09 13:11
pedagandhaha, that's ridiculous: the 'deriving' was written two *spaces* to the left and therefore She ignore it and removed it09/09 13:12
molerisagundry: One suggestion, from the AIM Demo is to overload |(x : X) ->| for Prop -- freeing up => for |refine plus 'zero n => n|09/09 13:13
moleris\`a la Epigam 109/09 13:13
agundrypedgand: she's like that09/09 13:13
molerisbut if that creates too much surgery on the parser, then don't bother09/09 13:14
agundrymoleris: that could work, but would probably be easiest when we get around to overloading Prop properly09/09 13:14
agundryis = okay for the time being?09/09 13:14
molerisit's fine (:09/09 13:14
agundryI've made the parser a bit more liberal so we can have tactics with the same name as keywords09/09 13:17
pedagandoverloading Prop properly? You mean, in the Evidences language? That's what was discussed last time actually09/09 14:09
pedagandI forgot to write it down, sorry about that09/09 14:09
pedagandhere is my take on it: http://code.google.com/p/epigram/issues/detail?id=10009/09 14:11
tsapino more codata in Agda it seems :(09/09 15:17
tsapiand I didn't know you could define recursive records09/09 15:17
+Saizanas long as we have \inf ..09/09 15:18
pedagandwhat is our situation wrt. EWAM generating re-re-reintroducing hypotheses? Shall I (try to) fix that? or it's a proofstate trick?09/09 16:36
pedagandright now, I'm working with 5 hypothesis and EWAM has introduced them 18 times09/09 16:36
pedagandre-introducing the hypos once, I can understand. But 18, I don't understand how this could happen...09/09 16:38
pedagand(moreover, it takes no less than 1Gig and 5 minutes to do that)09/09 16:39
pedagandI tried to apply another elimination: dead by swapping :-D09/09 16:45
agundrypedagand: pigworker and I discussed this and it is recorded (in clever disguise) as issue 77 in the bug tracker09/09 17:32
agundrythe plan is to make refinements happen out of scope of the parameters, to avoid reabstracting them09/09 17:33
pedagandok, so it's none of my business, good :-)09/09 17:34
agundrywell, I didn't say that...09/09 17:35
pedagandI wish you did :-) jokes apart, if it can help, I could do it. But I don't really understand how this should work right now.09/09 17:38
pedagandmoleris: when you're coming in Glasgow finally?09/09 19:07
molerispedagand: Good question09/09 19:44
molerisPossibly just Monday afternoon and Tuesday09/09 19:46
molerisbefore the IR meeting09/09 19:47
moleriswill have to confirm with pigworker09/09 19:47
pedagandshapr: the command to disable the auto-voice might be: '/msg chanserv flags #epigram * -V'09/09 19:47
pedagandmoleris: okay, I've asked Neil for coming along on IR, but I have no answer yet09/09 19:48
* shapr tries that09/09 19:48
shaprpedagand: You haven't registered your nick?09/09 19:49
pedagandnope09/09 19:49
shaprpourquoi pas?09/09 19:49
pedagandeven myself would like not to be myself, so I find it hard to imagine someone 'stealing my identity'09/09 19:50
pedagandthere is nothing to steal, really :-)09/09 19:50
* shapr svär åt chanserv09/09 19:51
shaprAh, but were you registered and identified, I could delegate the power such that you could fix this sort of problem yourself.09/09 19:51
shaprThus, there are benefits.09/09 19:51
pedagandif it can prevent you from swearing to ChanServ, then I will do :-)09/09 19:52
shaprTalar do svenska också?09/09 19:52
shaprahem, du09/09 19:53
shaprWe had this discussion before, but I forget the outcome... iirc, you do not speak Swedish exactly...09/09 19:54
pedagandas much as google translate does :-)09/09 19:54
shaprhah, of course.09/09 19:54
shaprpas de problem...09/09 19:54
pedagandbut I promise, if I get my PhD, I learn Swedish, I promise09/09 19:54
shaprhaha, good idea!09/09 19:54
shaprAre you aiming for Chalmers then?09/09 19:54
shaprOr perhaps KTH?09/09 19:54
pedagandto get a PhD? I'm not sure :-D09/09 19:54
pedagand(I meant: "I'm not sure (it's a good idea)")09/09 19:55
shaprLots of good stuff happening at Chalmers... I wonder if Aarne Ranta has considered porting GF (Grammatical Framework) to Epigram.09/09 19:55
pedagandI'm aiming at short term survival for now, will see for Chalmers if I haven't gone Postal before the end09/09 19:56
shaprheh, excellent idea :-)09/09 19:59
pedagandJag är registrerad, I think (if that makes any sense..)09/09 20:02
shaprvad bra!09/09 20:11
shaprwhich probably won't clear gtranslate... means "How nice!" or "That's great!"09/09 20:11
pedagandthanks for the translation, my Swedish is getting better and better ;-)09/09 20:18
pedagand(I tried to disable autovoice myself, chanserv says I'm not authorized. Dammit :-) )09/09 21:00
+dolioDid you try on yourself?09/09 21:00
copumpkin@get-shapr09/09 21:01
+Saizanpedagand: you're not even in the access list09/09 21:02
pedagandargh, I'm nothing :-)09/09 21:03
pedaganddon't bother, that was just a test09/09 21:03
+doliopigworker can do it, too, looks like.09/09 21:03
pedagandit doesn't work on myself either09/09 21:03
+dolioYou need either f or F to modify flags, I think.09/09 21:04
shaprwhoops, lemme fix it...09/09 21:05
shaprDangit, now I can't remember how to add access to people :-/09/09 21:06
+dolioThe help says you should be able to manipulate flags you have, but that doesn't seem to be working.09/09 21:06
+dolioI can't -V myself.09/09 21:06
shaprI tried /msg chanserv FLAGS #epigram *!*@*.* -v but it says Channel access to #epigram for *!*@*.* unchanged.09/09 21:07
shaprAny ideas?09/09 21:07
shaprI'm at work, so don't have many CPU cycles to spare...09/09 21:07
+dolioFor one, you want -V, I think. Unless you want to take away all voice privileges.09/09 21:07
pedagandisn't it -V to disable automatic voice?09/09 21:07
shaprI tried that too.09/09 21:08
shaprsame response09/09 21:08
+dolioSeveral of us are listed as the op template. Maybe you can change that?09/09 21:08
shaprI can change anything you like if you'll tell me what command to run...09/09 21:09
+doliotemplate op -V?09/09 21:09
+dolioEr, template #epigram op -V09/09 21:09
shaprok, done09/09 21:10
shaprChanged template op to +voti in #epigram.09/09 21:10
shaprsez chanserv09/09 21:10
+dolioHeh, no, we still have +V, but we're not listed as being the op template anymore. :)09/09 21:10
shaprwot?09/09 21:11
shaprdolio: If you have op template, are you able to change the settings yourself?09/09 21:11
+dolio4     dolio                  +vVoti (op)09/09 21:12
+dolioThat was the old line.09/09 21:12
+dolio4     dolio                  +vVoti09/09 21:12
+dolioThat's the new one.09/09 21:12
+dolioSame permissions, no template listed.09/09 21:12
* shapr svär åt chanserv09/09 21:13
+dolioOkay, try this:09/09 21:13
shaprdolio: Ok, can you give me a line to send to chanserv to give you privs to fix it? :-)09/09 21:14
+doliotemplate #epigram op +V09/09 21:14
shaprdone09/09 21:14
+dolioOkay, now:  template #epigram op !-V09/09 21:15
shapraha - 3 access entries updated accordingly.09/09 21:17
+dolioYep, okay.09/09 21:17
+dolioNow: template #epigram co-founder !-V09/09 21:17
+dolioThat should take care of pigworker.09/09 21:17
shaprroger - 1 access entries updated accordingly.09/09 21:19
+dolioOkay, we're done.09/09 21:19
shapryay, thanks!09/09 21:19
pedagandgeez, thanks guys! For a moment, this looked like an interactive session in Epigram09/09 21:21
+Saizan"denied access to idata, you need +O"09/09 21:24
pedagand:-D09/09 21:25
--- Day changed Fri Sep 10 2010
pigworkershould this work...?10/09 15:32
pigworkerlet Flag : Set ;10/09 15:32
pigworkerrefine Flag = Enum ['help 'main] ;10/09 15:32
agundryyes, doesn't it?10/09 15:33
pigworkershoot me now10/09 15:34
pigworkerafter pulling patches, there's a thing to remember to do...10/09 15:34
agundryindeed10/09 15:34
agundryincidentally, I think I've got elimination with a motive moving its methods correctly10/09 15:35
pigworkersounds promising10/09 15:35
agundryI just need to fix an annoying infinite loop in problem simplification...10/09 15:35
pigworkergood luck!10/09 15:35
pigworkerrecompiled...happy now10/09 15:39
pigworkerwhat still prevents us switching off automatic enum splitting?10/09 15:59
agundrynot much10/09 16:00
agundrywe would need to use idata everywhere and make sure TaggedInduction.pig was loaded so it could generate the nice induction principles10/09 16:01
pigworkerwe should be using idata everywhere anyway!10/09 16:03
molerisagreed10/09 16:03
moleristhe autoloading of TaggedInduction.pig is more of a problem10/09 16:04
agundrywe could replace the data tactic with one that called idata with unit index set, which would make migrating the test cases easier10/09 16:04
moleristhere are plenty of cases that predate the data tactic even, though10/09 16:05
moleris(test cases)10/09 16:05
pigworkermaybe we should have a bit of a cull-or-update mission10/09 16:05
agundrythat's probably not such a bad plan10/09 16:06
* pigworker wishes for rec; might try programming it10/09 16:12
molerisI had an attempt a while ago, which ran in to all sorts of problems10/09 16:13
molerisI think I struggled to almost the finish line, but now it's all broken and out of date10/09 16:14
molerismight be easier now, mind10/09 16:14
pigworkerdid we lose the hieroglyphics for making functions from sigmas?10/09 16:29
agundryno, you can still write |give con ?| if you like10/09 16:29
pigworkerso I can; then something weird happened...10/09 16:30
pigworkerif you issue |lambda| with no var, you get Pig: Prelude.last: empty list10/09 16:32
pigworkeroops10/09 16:32
pigworkerfix pushed10/09 16:38
pigworkeris there any way I can get the nice induction principle for IDesc?10/09 17:20
agundrypigworker: you need to load TaggedInduction.pig, then use idata10/09 17:21
pigworkerah, I see I was ambiguous; it's the datatype IDesc over which I want to do induction, for generic programming purposes10/09 17:22
agundryah, that's a bit trickier10/09 17:23
agundryI don't think the necessary bits are exposed as primitive definitions10/09 17:25
pigworkersomehow, we need to make that stuff available10/09 17:26
agundryno hold on, it seems they are10/09 17:28
pigworkerhow do I get'em?10/09 17:29
agundryIDescConstructors and IDescBranches are primitives10/09 17:29
pedagand there is SimpleInduction as well for inductions on IDesc10/09 17:42
pedagandbut it's not so simple when the proofs are not trivialised..10/09 17:43
pigworkerpedagand: thanks, checking it out10/09 17:44
pigworkerthat file needs a bit of repair now, I think10/09 17:46
agundryit needs more than a bit of repair10/09 17:59
agundryseveral of the hypotheses of idescInduction are absurd10/09 17:59
pigworkercan we hack a nasty piece of kit to turn a file Pig09/src/Prelude.pig into a Haskell file PreludePig.lhs, defining a string with exactly the contents of Prelude.Pig; this string could then be executed when the pig starts..?10/09 18:02
agundrywe could, or even something more principled10/09 18:04
agundrythe problem is referring to prelude things in Haskell code10/09 18:04
agundrythe current solution by moleris is a bit painful but more or less works10/09 18:04
agundrybtw, I'm pushing a patch bomb that avoids excessive accumulation of hypotheses10/09 18:05
pigworkerbonzer10/09 18:05
agundrylooks like Sort.pig goes through10/09 18:05
pigworkersweet! I'll see if I can finish the job10/09 18:17
pigworkerwe could really do with a more ecumenical idata tactic sometime...10/09 18:40
copumpkinpigworker: automatic proof!10/09 19:55
pigworkerdone it! Sort.pig now has insertion sort guaranteeing ordered output10/09 19:55
copumpkinis that public?10/09 19:56
pigworkerall the proofs are by appeal to hyps in the context, which happen automatically; I just pushed it in the repo10/09 19:56
pigworkerhttp://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/test/Sort.pig10/09 19:59
copumpkinyeah, was just looking at that, thanks :)10/09 19:59
copumpkinsorry if I'm being slow, but I can see what owotoNat is doing, but not the etymology of its name :)10/09 20:00
copumpkinI noticed this in another of your modules somewhere (can't remember where)10/09 20:00
dolioOn to permutations.10/09 20:04
pigworkerowoto is "one way or the other"10/09 20:10
pigworkerdolio: yeah, it's just occurred to me that permutation is a job for an indexed monad10/09 20:12
dolioOh yeah?10/09 20:12
pigworkeryeah, index by which elements you've used; make use of an element an effect10/09 20:14
dolioAh.10/09 20:15
pigworkerI'm hoping for lightweight linearity. Probably won't happen.10/09 20:16
dolioWorth a try, I guess.10/09 20:16
copumpkinpigworker: ah! I was trying to pronounce it and couldn't find something meaningful :)10/09 20:17
pigworkerneed to extend the notion of programming problem with "current signature" and "current state"; then program ML-style10/09 20:18
nappingI am wondering about the difficulties in defining a well-typed syntax for a dependently typed language10/09 21:22
nappingIt seems to me the main difficulty is in the appeal to convertability, if we are to represted *term* instead of typing judgements10/09 21:23
nappingbut then, how is the language proved to be strongly normalizing in the first place?10/09 21:24
dolioTrying to do it that way isn't likely to work, I think.10/09 21:26
doliopigworker wrote a paper not long ago about doing such a thing, though.10/09 21:26
nappingor rather, those foundational proofs might show the way to at least representing the syntax10/09 21:26
napping"outrageous coincidences"?10/09 21:27
dolioYou define a universe of types in your meta language, and then index the syntactic terms by those.10/09 21:27
dolioYes.10/09 21:27
dolioAnd then you have a type of well-formed syntactic types indexed by the semantic universe of types.10/09 21:28
nappingDo you know a good reference for the foundational metatheory of some reasonably powerful language?10/09 21:28
dolioOr something along those lines.10/09 21:28
pigworkernapping: Healf Goguen's thesis is a good contribution, there.10/09 22:23
pigworkerInevitably, though, it takes a big theory to prove normalization of a small one. There was an old lady who swallowed a fly...perhaps she'll reach canonical form.10/09 22:24
--- Day changed Sat Sep 11 2010
pigworkerHey, gang! Let's use extensionality to prove case analysis principles for functions!11/09 01:02
Saizanlike that a function from 2 is actually a pair?11/09 01:04
pigworkeryeah, and a function from (A + B) is given by a function from A and a function from B11/09 01:05
pigworkersame deal, if you code + as Sigma 2, of course11/09 01:06
pigworkerit would be fun to demo stuff that just doesn't happen in Agda and Coq11/09 01:09
dolioEh, I postulate extensionality on a regular basis. :)11/09 01:10
Saizani was surprised by Agda not accepting that all proofs of A -> _|_ are equal11/09 01:10
Saizanwhile it works for A -> Unit11/09 01:11
pigworkerdolio: and with it, many new canonical forms of type Bool11/09 01:11
pigworkerthat's a record versus data thing11/09 01:11
pigworkerIn Epigram 2, Enum [] is not proof-irrelevant, but :- FF is.11/09 01:12
pigworkerGenerally speaking, unique inhabitation is a sign of degeneracy in an enumeration...11/09 01:14
dolioDoes Agda just eta-convert everything of type A -> Unit to \_ -> _?11/09 01:14
Saizanwhat's eqGreen for Enum [] though? satisfiable?11/09 01:14
pigworkerSaizan: yeah, everything in Enum [] is provably equal, not to mention distinct.11/09 01:15
pigworkerdolio: yes11/09 01:15
dolioHandy.11/09 01:15
pigworkermoreover, _ makes a perfectly good element11/09 01:15
pigworkerI am a vacuously satisfied lemon, and I'm going to bed. G'night!11/09 01:18
pedagandmoleris: give a look at pigmode.el: multi-line code supported11/09 11:48
pedagandbtw, edwinb, if you want syntax highlighting for Idris, this pigmode will surely be a good start11/09 11:56
edwinbooh11/09 11:56
pedagandit's quite easy actually11/09 11:56
edwinbI have an ivor-mode11/09 11:56
edwinbsyntax highlighting is the easy bit really11/09 11:57
edwinbit's magic indentation I really want11/09 11:57
pedagandyeah, ok, you beat me then :-)11/09 11:57
edwinbI might switch to haskell like syntax so that I can steal their code ;)11/09 12:01
pedagandi've looked at haskell-mode.el: that's frightening11/09 12:03
pigworkerI wonder if we can easily interrogate the shell buffer for the latest programming problem and copy it to a refine command in the script.11/09 12:24
tsapihow do I use Pig mode?11/09 13:10
pigworkershould I be doing cabal install these days? I guess it's time I made sure the binary was in my path (pig mode seems to presume this).11/09 13:30
pedagandtsapi: you can install it like any emacs mode, in theory11/09 13:43
pedagandif you want to test it quickly, you open pigmode in emacs and type meta-x eval-buffer11/09 13:43
pedagandthen it will trigger itself when you open a .pig file11/09 13:43
tsapiI ended up just loading it from .emacs11/09 13:43
pigworkeroddly, when I try using it, it gets pig-win and code-win the wrong way round11/09 13:45
pedagandbleh11/09 13:52
pigworkerI think Aquamacs has a dodgy split-window. Maybe start Pig with (comint-run "Pig") and detect buffer "*Pig*"?11/09 13:53
pedagandas for matching prog problems, it certainly is doable but as we're just playing the script, it won't be very useful11/09 13:54
pigworkerI was thinking about actually supporting the writing of new programs...11/09 13:57
pigworkertsapi: yer wk function seems to work now, but ren seems to cause a lot of trouble11/09 14:04
pigworkeralso, better not to break the ordinary function of M-x shell...11/09 14:10
pigworkerbut it's definitely progress11/09 14:11
pedagandhaha11/09 14:11
pedagandwell, I'm back to pen&paper for today11/09 14:12
tsapipigmode is very nice, thanks Pierre!11/09 14:28
pedagandgrrr.. I'm stuck fiddling with lisp instead of learning what is a subobject classifier. halp! halp!11/09 14:29
pedagandtsapi: you're welcome. It's quite fragile tho, so be careful :-)11/09 14:30
copumpkinsubobject classifiers in lisp!11/09 14:30
pedagandcopumpkin: no thanks :-)11/09 14:32
copumpkinfind a subobject classifier in the category of parentheses (and um, words between them? :P)11/09 14:32
* copumpkin stops making no sense and crawls back into his hole11/09 14:33
tsapipedagand: it'd be nice to flash the executed line like this: http://vimeo.com/12127980 :)11/09 14:34
pedagandI might have solve the shell call11/09 14:46
pedagandtsapi: :-)11/09 14:47
pedagandI've pushed a different handling of windows and use comint-run. Why on earth am I doing that? Quick, subobjects!11/09 14:53
Saizanit still dies on some parse failures11/09 15:17
Saizan(or maybe all?)11/09 15:17
pedagandwhat dies?11/09 15:18
SaizanPig11/09 15:18
pedagandafaik the parser have not changed 11/09 15:19
pedagandso it's not surprising11/09 15:19
Saizanfor example with "let Bounds : Set refine Bounds = Sig (l : BT Nat ; u : BT Nat ; ) ;"11/09 15:19
pedagandI get a "Parse failure", is that unexpected?11/09 15:20
pedagandI mean, this line is not valid, so I'm not surprised if it's rejected11/09 15:21
molerispedagand: It's not just that it gets rejected, but it seems to kill the Pig11/09 15:21
moleriswhich it didn't do before11/09 15:21
molerisperhaps before I complain, I should say "thanks, good work"11/09 15:22
pedagandha ho11/09 15:23
pedaganddon't bother with the formalities, go straight to the complaints :-)11/09 15:23
pedagandI have my idea why it's crashing11/09 15:24
pedagandexitFailure is overrated11/09 15:25
Saizanheh, you can catch it though :)11/09 15:26
pedagandI think I'll just rollback to the previous code11/09 15:27
pedagandfixed11/09 15:32
pedagandpigworker: is the new window handling working better on your playskool(tm) emacs?11/09 15:57
pigworkerpedagand: much better, thanks; would it be too radical to suggest TAB in place of C-c C-r? or is that insufficient suffering?11/09 17:01
pedagandTab is a bit too radical imho: when you're tabulating your file, you do not expect Pig to shout at you (think typing tab in a comment)11/09 17:18
pedagandyou could have C-c C-c, or C-Tab probably11/09 17:18
pigworkerBut it's a mortal sin to use Tab to make spaces!11/09 17:18
pedagandbut indentation modes use Tab to indent (with spaces)11/09 17:20
pedagandsuch as the indent-mode in haskell-mode, for instance11/09 17:20
pigworkerIt always guesses the wrong indentation when I use it, so I don't.11/09 17:21
pigworkerBut I shouldn't impose my habits on others. Except when they're right.11/09 17:21
pigworker(the habits, not the others)11/09 17:22
pedagandhave you enabled this in your .emacs: (add-hook 'haskell-mode-hook 'turn-on-haskell-indent) ?11/09 17:22
pigworkerprobably not11/09 17:22
pedagandthere are several indentation modes, some are definitely broken11/09 17:22
pigworkerI find that the time I spend using the space bar is seldom wasted.11/09 17:23
pedagandbecause most of your code is 24 characters wide/ACM 2-col...11/09 17:24
pigworkerI'm also wondering how much tab-based tabulation we're ever likely to do in a Cochon script. mode-local key-binding?11/09 17:24
pigworkerYeah, it's got to fit on the punch cards, after all.11/09 17:24
pedagandyou could write {- ... -} comments in a Cochon script and hit tab11/09 17:27
pigworkerwhat for?11/09 17:28
pigworkermeanwhile, I'm on the hunt for bquote calls which serve no useful purpose...11/09 17:31
pedagandthat looks much more interesting than defending the right for Tab to exist. I should do something like that as well. :-)11/09 17:32
pigworkerI found one whose result was unused. I commented it out. Probably makes no difference.11/09 17:33
pedagandbut all bquote (except 1) are useless, isn't it?11/09 17:35
pigworkerhope so, but I plan to think about it11/09 17:35
pigworkeralthough actually, just now I'm trying to figure out how to make the tags red11/09 17:37
pedagandhave you looked at bquote's code? it's just an identity function, excepted when you call it with a non empty list of references to bind (in which case it's just a mangler job)11/09 17:37
pedagandthere is a regexp catching 'foo, you can define a custome font-face for it11/09 17:38
pigworkeryes, so it gets interesting when it goes under a binder11/09 17:38
pedagandinstead of applying whatever font-face I chose11/09 17:38
pedagandwhat does the second 'it' refers to? "bquote"? "the mangler"?11/09 17:39
pigworkerbquote... it gets rid of closures; before I replace bquote with the identity, I want to make sure its usages are not afraid to encounter closures11/09 17:40
pigworkerI'd be surprised if that was a problem, but I'd be even more surprised if there was just no problem.11/09 17:41
pedagandoh, this reminds me a question: how is the mangler supposed to deal with closures?11/09 17:52
pigworkerbetter think about that...11/09 17:54
pigworkerthe values stored in environments are all supposed to be closed, so we might need to give an extra field for how to mangle a closed thing11/09 17:55
pigworkerof course, there's also the random lump of term that's wrapped with the environment to worry about...11/09 18:15
pigworkerI'm looking at code which does too much retypechecking. If we know (PI s t) is a Set, then we know s is a Set. Our lack of faith is costing us time.11/09 18:50
pedagandbetter be safe than sorry?11/09 18:59
pedagandat some stage, we will have to remove the Anchor stuff. It's just broken. Well, like most of my contributions anyway..11/09 19:13
pigworkerpossibly, but often we're effectively doing extra checking whose sole purpose is detecting bugs: if EWAM creates ill-typed subgoals for motive and methods, that's a bug; we might want to turn that on and off11/09 19:58
doliopigworker: So, I've been thinking...11/09 21:46
dolioConsider the type/functor: T X = exists Y. X*Y.11/09 21:47
dolioA 'constructor' for that type would have type: C : forall X Y. X -> Y -> T X.11/09 21:48
dolioAnd the free theorem for that is: forall f g x y. map f (C x y) = C (f x) (g y)11/09 21:48
dolioHowever, it seems unlikely that you'd be able to prove that, even in most extensional type theories.11/09 21:49
dolioThe fact that Y is existentially quantified seems to cause quotienting to happen for equality on the terms that use Y.11/09 21:50
dolioSo: can an observational equality be constructed that incorporates these sorts of parametricity-related equations?11/09 21:52
pigworkerdolio: interesting question; under all the wrapping, the point is that g can only be the polymorphic identity function?11/09 23:27
pigworkersomehow, one would hope that it's consistent to add this sort of parametricity; correspondingly, it should be possible to set up an observational equality in which free theorems hold (although Epigram's current observational equality does not give them)11/09 23:32
pigworkerwe do, however, enjoy the property that assuming consistent propositional axioms cannot break canonicity; correspondingly, one could perhaps assert a single, generically-programmed parametricity axiom11/09 23:34
--- Day changed Sun Sep 12 2010
doliopigworker: No. g is not limited to being identity. Adding in types, I believe it's...12/09 01:57
dolioforall (f : X1 -> X2) (g : Y1 -> Y2) (x : X1) (y : Y1). map f (C x y) = C (f x) (g y)12/09 01:58
dolioImplicitly quantifying over the types, as well.12/09 01:59
dolioX1, etc.12/09 01:59
koninkjedolio: following up on my non-pointed functor? :)12/09 01:59
doliokoninkje: I was wondering whether we could have a type theory that would actually allow you to prove the free theorem internally.12/09 02:00
koninkjeIt is an interesting question12/09 02:00
dolioI don't anticipate even most extensional type theories would get you there.12/09 02:00
doliopigworker: A special case for C being the constructor of a type with existential quantification would be that the value produced by the constructor is the same regardless of what the second argument is.12/09 02:02
koninkjepigworker: Actually the problem is that it doesn't have to be the identity function12/09 02:02
koninkjeper se12/09 02:02
koninkjeEssentially, we'd need to show thatany existentially quantified type has only one (observable) inhabitant12/09 02:03
dolioSince you can take g = const y2, for any y2, and then C x y1 = C x y2.12/09 02:03
koninkjeThough, proving that does mean that any function on the existential type is *observably equivalent* to the identity function...12/09 02:04
koninkjeque interesante12/09 02:04
koninkjeI wonder if anyone's worked on a type theory based on bisimulation12/09 02:05
koninkjeThat seems like it'd be the way to go about shoing this kind of thing, and I know Amal Ahmed has been interested in that sort of system12/09 02:06
koninkjeIf only I were doing cs for my phd, then I'd have a thesis topic12/09 02:06
dolio:)12/09 02:06
koninkjeAnd an advisor too :)12/09 02:07
dolioAnyhow, it seems like you could finesse the OTT definition of equality to incorporate some of this.12/09 02:07
koninkjeHow is OTT's equality different from, say, CoC/CIC?12/09 02:08
dolioLike, right now, we have (f : (T : *) -> U) == (g : (T' : *) -> U')  = (T T' : *) -> T = T' -> ...12/09 02:08
dolioWhen instead, you could define it to be talking about relations between T and T'.12/09 02:09
dolioBut I don't know if that'd all work out.12/09 02:09
dolioOTT sort of defines equality by recursion over the structure of types.12/09 02:10
dolioDefining equality for each type to be the natural extensional equality on each type.12/09 02:11
dolioOh, and it's heterogeneous, as well.12/09 02:11
dolioThat may be too vague a description.12/09 02:12
koninkjeI think I get the idea12/09 02:13
dolioAnyhow, it works out that you get a subst : (A : *) (P : A -> *) (x y : A) -> x = y -> P x -> P y, but = is extensional.12/09 02:14
koninkjeI've yet to find any actual reason to limit oneself to homogeneous equality...12/09 02:14
dolioYou have to be somewhat careful, at least.12/09 02:15
koninkjeHow so?12/09 02:15
dolioSomeone used heterogeneous equality in Agda to prove that Bool /= Fin 2.12/09 02:15
dolioWhich is undesirable to some people, I think.12/09 02:16
koninkjeOoh, reference?12/09 02:16
copumpkinlol, I was just looking at that: http://code.google.com/p/agda/issues/detail?id=29212/09 02:16
dolioBut that's because heterogeneous equality in Agda has a slightly different meaning that the OTT one.12/09 02:16
dolioI believe pigworker describes the difference as, in Agda, proofs of heterogeneous equality are "the type are equal AND the values are equal", whereas in OTT, they're "IF the types are equal, THEN the values are equal."12/09 02:19
* koninkje nods12/09 02:20
koninkjeThis looks rather similar to the T X = exists Y. X*Y issue12/09 02:22
koninkjenamely, Bool==Fin 2 only in the case where we're talking about equivalence under observational isomorphisms12/09 02:22
koninkjeOtherwise, clearly they're different types, because one has True and False whereas the other has Zero and One12/09 02:23
koninkjecf. http://ncatlab.org/nlab/show/evil12/09 02:24
dolioIt is kind of a sticky issue.12/09 02:24
dolioAgda used to just hand you a proof of Bool /= Fin 2, I believe.12/09 02:25
dolioBecause it looked at the type constructors, and they were different, so obviously they're not the same type.12/09 02:25
koninkjeWell it's the age old definitional vs observational equivalence issue12/09 02:25
dolioDoing that, though, turns out to allow you to prove the anti-classical theorem 'Not (forall P. P \/ Not P)', though, if I'm remembering correctly.12/09 02:26
koninkjedoing what?12/09 02:28
dolioAllowing injective type constructors.12/09 02:28
dolioOr, taking all type constructors to be injective.12/09 02:28
dolioWhich is what used to provide the easy Bool /= Fin 2 proof.12/09 02:29
* koninkje nods12/09 02:29
dolioAnd of course, the homotopy type theory people want identity types to be inhabited for any two isomorphic types.12/09 02:30
koninkjeThere's nothing wrong with anti-classicism though12/09 02:30
dolioYeah, I agree.12/09 02:31
koninkjeProblematically, (exists t. t) is not a terminal object in standard CCCs, so any theory for proving x*(exists t.t) ~= x is going to have to diverge from normal CCCs12/09 02:37
dolioIt isn't?12/09 02:38
koninkjeThe morphisms from all objects to (exists t.t) aren't unique12/09 02:39
dolioI wasn't aware that (exists t. t) was even a construct in CCCs in general.12/09 02:42
koninkjeIt's not a construct. I'm just saying that if we have a CCC and it has an object (exists t.t) which behaves in the ways we'd expect/like, then (exists t.t) isn't terminal12/09 02:44
dolioWell, then, I'm lost.12/09 02:45
dolioI expect (exists t. t) to be a terminal object.12/09 02:45
koninkjeFix some type X. There are multiple functions from X to (exists t. t); namely one function for each element of X12/09 02:46
koninkjeSo hom(X, exists t.t) isn't unique for any non-singleton X12/09 02:47
copumpkinare those functions observably different?12/09 02:47
copumpkinor does that not matter?12/09 02:47
koninkjeDoesn't matter. Category theory is talking about equality/identity, not observations12/09 02:48
copumpkinfair enough12/09 02:48
dolioYour notion of equality is very weak.12/09 02:49
dolioAnd not, I think, the one typically used even in category theory.12/09 02:49
koninkjeThough, we can define a functor from a "CCC" with existentials to a CCC without them, which maps (exists t.t) to 112/09 02:49
koninkjedolio: I'm pretty sure it is the one commonly used in CT12/09 02:49
dolioI'm not aware of category theorists usually having problems with extensional equality.12/09 02:49
koninkjeextensional equality is different than observable equality12/09 02:50
koninkjeextensionally, (exists t.t) is a product of some type/object T and a value of T12/09 02:50
koninkjeobservably, all such pairs are the same12/09 02:51
koninkjebut not extensionally12/09 02:51
koninkje--well, if you have typecase then they aren't observably equal either12/09 02:51
koninkjePersonally I'm a great fan of extensional equality. It's far better for most tasks than equality by unique identity12/09 02:53
koninkjewhence my link to the n-Lab page on "evil" earlier12/09 02:54
dolioYour argument that hom(X, exists t. t) simply assumes that (exists t. t) has more than one element. If it only has one element, then all the morphisms are extensionally equal.12/09 02:55
koninkjeAnd (exists t.t) isn't isomorphic to unit because, for example, take T to be the empty type. How can you map unit to it?12/09 02:56
dolioAnd all elements of (exists t. t) are extensionally equal, in that you can substitute one for another without changing meaning.12/09 02:56
dolioBecause there's no way to get information out of (exists t. t).12/09 02:56
koninkjeUnless you have typecase, or polymorphic seq, or reflection, or...12/09 02:57
dolioYes, polymorphic seq breaks things.12/09 02:57
koninkjeThat (exists t. t) only has one element must be taken as an axiom. It is not provided by the definition of existential quantification12/09 02:57
dolioI wouldn't necessarily expect type case to even work on something quantified with exists, as opposed to some other sigma, but that's another issue.12/09 02:57
koninkjeThis shows up in the Coq definition of existentials, e.g.12/09 02:58
koninkjeWhy wouldn't typecase work with existentials? (Exists X x) = typecase X of { Unit -> ... ;... }12/09 02:59
dolioBecause exists is parametric quantification, just like forall.12/09 02:59
koninkjeer, that "e.g." didn't mean to reference the following line12/09 02:59
koninkjeBut dependent types screw up parametricity12/09 03:01
koninkje(and if you have typecase at all, then you don't have real parametricity)12/09 03:02
dolioThere's work on parametricity with dependent types.12/09 03:03
koninkjeSure, I'm just saying that dependent types make a mess of things compared to System F, Fomega, etc12/09 03:03
dolioAnd you can have systems with two different varieties of quantifiers, one which is parametric, and one which isn't. And typecase could work only on variables quantified with the non-parametric quantifier.12/09 03:04
koninkjetrue12/09 03:04
koninkjeMy point was that the category we work in doesn't have (exists t. t) be isomorphic with unit. There's a functor from this category to one where (exists t.t) is mapped to a terminal object, but that doesn't make it terminal in the source category12/09 03:06
koninkjethis is the same functor that's used to do Prop erasure since every P:Prop is isomorphic to the terminal object--- but only after erasure12/09 03:07
koninkjeIf they were isomorphic before erasure, then that'd defeat the whoe purpose of having Prop in the first place12/09 03:07
koninkjes/whoe/whole/12/09 03:07
dolioI don't agree with your first sentence. I think, in Haskell minus seq, (exists t. t) is isomorphic to the terminal object, under the usual extensional equality used to talk about things like free theorems.12/09 03:07
koninkjeBut that's already diverging from Haskell itself. 12/09 03:09
koninkjeAnd the free theorems are talking about isomorphisms, not equalities12/09 03:10
dolioThey're talking about equalities.12/09 03:10
dolioI don't even know what isomorphisms you're talking about, to be honest.12/09 03:10
koninkjenot the ones I'm familiar with12/09 03:10
dolioWhat is the category in question, where values are objects, and have morphisms between them?12/09 03:11
koninkjeI dunno. I was talking about the category of types and functions12/09 03:11
dolioFree theorems aren't theorems about types, they're theorems about values with a certain type.12/09 03:12
koninkjeThey're theorems about morphisms; it only happens to be the case that every hom-set has an associated object in CCCs12/09 03:13
koninkjeThough I suppose it depends on which free theorems you're meaning. Since results about morphisms imply the structure of the objects behind them12/09 03:14
dolioOkay, (exists t. t) should be isomorphic to forall r. (forall t. t -> r) -> r = T12/09 03:20
dolioThe free theorem for type T is: forall e : T. forall f h1 h2. (forall g z. f (h1 z) = h2 (g z)) => f (e h1) = e h212/09 03:21
dolioSuppose h : (forall t. t -> r) for a fixed r. The free theorem for that type gives: forall h : (forall t. t -> r). forall f. h = h . f12/09 03:22
dolioA special case of which is: forall h : (forall t. t -> r). forall x y. h x = h y12/09 03:23
dolioIf in the free theorem given by T, we take f = h1 = h2 = h...12/09 03:23
dolioThen forall g z. h (h z) = h (g z) by the free theorem for h.12/09 03:24
dolioAnd so: forall e : T. h (e h) = e h12/09 03:24
dolioSo, now: forall e e' : T. forall h. e h = h (e h) = h (e' h) = e' h12/09 03:25
dolioAnd then, forall e e' : T. e = e', via extensionality.12/09 03:26
dolioSo, parametricity entails that all elements of forall r. (forall t. t -> r) -> r are equal.12/09 03:26
koninkjesc12/09 04:14
pigworkerdolio: morning! it's clear that I didn't understand your question last night, sorry12/09 08:32
dolioNo problem.12/09 08:32
pigworkerpartly, I was failing to figure out what the quantifiers meant, and where there was implicit application, projection, and quantification12/09 08:33
pigworkerIt remains the case that our lazy-Prop setup is amenable to stronger axioms and that we have no typecase, so there might be some parametricity to grab onto that way.12/09 08:35
dolioAnyhow, one thought I've had is that the definitions of equality in OTT are kind of similar to the parametricity propositions.12/09 08:36
dolioOnly in OTT, all the relations are set to equality.12/09 08:36
pigworkerYes, and one could relax that, given enough guarantees of non-inspection.12/09 08:36
pigworkerThat is, I'm not sure if one could safely relax the definition of equality, but one could offer free theorems.12/09 08:38
pigworkerAt that point, it becomes really attractive to offer intersection distinct from product, to allow the voluntary exchange of inspection for theorems.12/09 08:39
dolioYes.12/09 08:41
pigworkerMeanwhile, as currently formulated, OTT's equality on sets is "representational compatibility" rather than "isomorphism", so Fin 2 had better not be Bool...12/09 08:42
dolioWell, I wouldn't expect that. But you can't prove them distinct either, can you?12/09 08:43
pigworkerIt's really more about descriptions of sets than sets per se.12/09 08:43
pigworkeryes you can prove them distinct12/09 08:43
dolioOh.12/09 08:43
pigworkerin the OTT models, types are collected in a universe, and "equality" is for codes not their meanings12/09 08:44
pigworkerit is certainly the case that Fin 2 and Bool are differently described12/09 08:45
pigworkerit is also the case that run-time values of one may not be used, untransformed, where run-time values of the other are expected12/09 08:46
pigworkerIt's a deliberate choice to ensure that coercion between "equal" sets can be erased at run-time (closed computation only), where the more iso-friendly equalities would require the insertion of adaptors.12/09 08:49
* pigworker had better spend the day on planet Teaching.12/09 12:12
--- Day changed Thu Sep 16 2010
Phantom_HooverSo is soupdragon around any more16/09 18:50
Phantom_Hoover*?16/09 18:50
--- Day changed Tue Sep 21 2010
pedagandmoleris: how is life going?21/09 12:58
molerispedagand: Can we talk about something else? ;)21/09 13:05
molerisHow was the 2nd day of IR anyway?21/09 13:06
pedagandhaha, you can still miss your flight21/09 13:13
pedagandthat was good, we got some crazy category theory model of type theory, induction-induction, and a few examples of Hank21/09 13:14
molerisheh, it's not even that - after the AIM demo I'm pretty relaxed and looking forward to it21/09 13:14
pedagandoh, I see, that's even worse :-)21/09 13:15
molerisI just need to stop it with the self sabotage21/09 13:15
molerisAnyway, I'm trying to workout the exact make up of the demo21/09 13:16
molerisCurrently this involves swapping the Nat compare stuff with some Rec for Nat, fibonacci seq.21/09 13:17
molerisAdding an itroduction to Prop, before the equality madness21/09 13:17
molerisintroduction21/09 13:18
molerisand finding some extra time so I can do something with an indexed data type :)21/09 13:18
molerisMaybe Nisse will take pity on me and not ask to see the description of Nat in the first 5 minutes21/09 13:19
moleristhat ought to buy me some time21/09 13:19
molerisany thoughts?21/09 13:27
pedagand:-)21/09 13:28
pedagandI tried some generic programming in Levitation.pig yesterday21/09 13:29
pedagandI think we are stuck with programming with IDesc, so generic prog on IDesc is probably too dangerous21/09 13:29
pedagandyou're program seems exciting, that's good21/09 13:30
pedagands/you're/your/21/09 13:32
molerisSome generics would be good though, and I can always deal with the difficult stuff with a forward pointer to your talk21/09 13:35
moleris(;21/09 13:36
pedagandany free (i)monad?21/09 13:36
molerisThat's not a bad idea. For the MSFP crowd especially21/09 13:37
pedagandor showing off the simplification rules (opSimp.pig)21/09 13:38
molerisfree monad with free monad laws - yes21/09 13:43
pedagandI know you're a vi user, so if you need some duct-tape on pigmode, let us now21/09 13:43
molerisI can get by in emacs, I've even got to the point where I don't type my vi shortcuts in any more21/09 13:44
pedagandI was thinking: if you want to add shortcuts, or if you're not happy with pigmode.el behavior and don't know how to fix it21/09 13:48
pedagandbut, surely, elisp doesn't frighten you ;-)21/09 13:48
molerisah, cheers21/09 14:00
moleriswell, there was one thing (:21/09 14:01
moleristhe syntax hilighting is a bit broken for comments, for instance keywords that happen to be in comment text get coloured in still21/09 14:02
molerisI was also tempted to add a shortcut that prepended the a line with 'refine' to make the "program" text even cleaner - but I have enough elisp to do that myself21/09 14:05
moleriss/prepend the a/prepends a/21/09 14:05
pedagandfor colors, it annoyed me at the time but could fix it in 5 minutes. I'll give another look.21/09 14:30
pedagandgeez, I cannot write... s/could/could not/ (this is semantically important)21/09 14:45
molerisI managed to translate from the pedagandish21/09 14:51
pedagandgot it! that was a silly typo21/09 14:52
molerispedagand: thx21/09 15:18
pedagand(in fact, it wasn't a silly typo. In the meantime, I found the hack I pushed)21/09 15:19
--- Day changed Wed Sep 22 2010
molerisagundry: You about?22/09 13:22
agundrymoleris: yep, hello22/09 13:23
molerisHow you doing?22/09 13:23
agundryokay, thanks, feeling vaguely ready for Baltimore22/09 13:24
molerisGood stuff :)22/09 13:24
agundryyou?22/09 13:24
molerisGetting there22/09 13:24
molerisThanks for some of your bug fixes on the Pig over the last week or so, they've made the demo look almost plausible22/09 13:25
agundryno problem, I've been trying to do things that at least give Pig a veneer of plausibility ;-)22/09 13:25
agundryis there anything else that it would be particularly useful to fix?22/09 13:25
molerisWell, I was wondering - What breaks if we allow the problem simlifier to introduce lambdas for PRF (ALL _ _) goals in the same way as for PI22/09 13:26
molerisThis isn't actually a request for code btw - I've actually wired it up and it :) But it's probably a baad idea somehow22/09 13:27
moleris(... and it seems to be OK :) ...)22/09 13:28
moleristidies up some of the niggles with the flip plus == plus bit of the demo22/09 13:28
agundryI've actually been trying that out; it doesn't appear to break anything22/09 13:30
molerisCool22/09 13:32
agundryI look forward to seeing your patch22/09 13:38
molerisHa22/09 13:40
molerisMy repo is in a bit of a state at the moment - and it's only going to get worse as Saturday approaches22/09 13:41
molerisWill rationalise and push useful things next week I guess22/09 13:42
agundryfair enough22/09 13:47
molerisFor instance I've dumped Desc.lhs completely in my local copy and switched off the Enum splitter22/09 13:49
molerisand there are other (lets say) less principled things mixed in22/09 13:50
--- Day changed Sat Sep 25 2010
Phantom_HooverHas anyone around here seen soupdragon lately?25/09 21:49
--- Day changed Tue Sep 28 2010
ccasin__what's the best reference for epigram 2?28/09 12:36
ccasin__(say, for a related work section)28/09 12:37
--- Day changed Thu Sep 30 2010
pigworkerccasin: reference for Epigram 2, hmmm... aspects of the design are reported in GAOL and ObsEqNow, but there's nothing more comprehensive that's peer-reviewed; of course, there's the website and the EpiTome...30/09 15:05
ccasinpigworker: thanks. I'm citing those two but didn't know if there was a better comprehensive report floating around as well30/09 15:08
pigworkersadly not at the moment... moving target30/09 15:09
ccasinfair enough!  it hardly matters since equality and datatypes are the only parts I know enough about to mention in particular30/09 15:10
ccasinthanks30/09 15:11

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