--- Log opened Mon May 16 11:09:08 2011
-!- Irssi: #epigram: Total of 14 nicks [0 ops, 0 halfops, 0 voices, 14 normal]16/05 11:09
-!- Irssi: Join to #epigram was synced in 0 secs16/05 11:09
molerispigworker: Afternoon16/05 15:44
pigworkerin a rainy Glasgow, yes16/05 15:45
pigworkerhow are things? I pulled some patches this morning16/05 15:45
molerisI've just pushed a rather fat patch16/05 15:46
pigworkerpulled! what should I hope to do?16/05 15:46
molerisUmm, if you pull up an interactive session of Cochon.Cochon16/05 15:47
pigworkermake clean; make just bombed out16/05 15:47
molerisand run 'cochon emptyContext'16/05 15:47
molerisyeah, I need to fix the makey stuff soon :S16/05 15:48
pigworkerI just got a problem in Moonshine.lhs (missing DLK, DTIN)16/05 15:48
molerisoo err16/05 15:49
molerismight be shee related?16/05 15:49
molerisshe16/05 15:49
pigworker'spec so16/05 15:49
molerisrunning ghci again might fix it16/05 15:50
pigworkersure enuff and yes it does (those pesky module chases)16/05 15:50
molerisphew16/05 15:51
pigworkera prompt!16/05 15:51
molerisOK, you should be able to the basic make, lam, give stuff16/05 15:51
pigworkerI think some such thing just happened.16/05 15:53
moleris'show state' and 'inspect [term]' are useful to see what you've done16/05 15:54
pigworkerI'm just reloading inside an emacs shell...16/05 15:54
molerisYou'll quickly establish that the pretty printer needs work16/05 15:54
molerisHeh, yes sensible16/05 15:54
pigworkerI see.16/05 15:55
pigworkerI did some very simple stuff. So far so good.16/05 15:56
molerisGood16/05 15:56
molerisI've implemented some built-ins, but you can't call them at the moment16/05 15:57
pigworkerAnd I see that some sort of update propagation is happening.16/05 15:57
pigworkerAll in good time.16/05 15:58
pigworkerI've been working on stratification. I think I'm onto something. It's not dangerous or radical.16/05 15:59
molerisShouldn't be too difficult actually16/05 15:59
molerisOh, cool16/05 15:59
molerisI was hoping to pick your brain on the Operator language16/05 16:00
pigworkerI think I've found a way to have silent cumulativity but explicit polymorphism. More another time.16/05 16:00
pigworkerOperators, yeah?16/05 16:00
pigworkershould I be looking at Evidences/Tm.lhs or some such?16/05 16:01
molerisSpecifically, if we need to extend it to help us write equality16/05 16:02
pigworkerI see the current data Operator def.16/05 16:02
molerisYup, and underneath the OpMaker stuff, and a few simple examples 16/05 16:03
pigworkerI can't remember where we hid the interpreter.16/05 16:03
molerisIt's all in that file - spread through eval, apply and mkD16/05 16:05
pigworkerok, so we can do cases on any old thing, to see if it's canonical16/05 16:07
pigworkerwhat happens with equality?16/05 16:07
pigworkerbtw, are we dumping green equality?16/05 16:08
molerisI think so yeah16/05 16:08
pigworkerso we need coe to be an operator, but not equality itself16/05 16:10
molerisAh, maybe16/05 16:10
copumpkinomg a pigworker 16/05 16:10
molerisI was wondering what the pieces were16/05 16:10
molerisAre the rules for the blue equality all encoded as canTy rules?16/05 16:11
pigworkerI see we have Eq being a Can. Good.16/05 16:11
pigworkerYes, I think we just blat them all out in canTy. Why try harder?16/05 16:12
pigworkerI suppose we might need to farm it out to a helper function, because more than one thing needs to know how to decompose an equation.16/05 16:14
molerisAha16/05 16:15
molerisOk. Cool. I was thinking that something like the EqGreen operator was still needed16/05 16:16
molerisbut if it isn't then that makes everything much easier16/05 16:16
pigworkerHow about we write eqUnfold :: ((Can, [EXP]) :>: EXP) -> ((Can, [EXP]) :>: EXP) -> Maybe (Can, VAL) taking two things in canonical types and explaining how one would build a canonical proof of the equation?16/05 16:18
pigworkerSo, quite like EqGreen, really, but not an operator.16/05 16:19
molerisyup16/05 16:19
pigworkerThen we canTy a Prf of an Eq, if we get what's expected by eqUnfold16/05 16:22
pigworkerThat leaves the vexed question of how to handle refl.16/05 16:23
molerisah16/05 16:24
molerisI can't even remember what status refl had before16/05 16:25
pigworkerhack, I suspect16/05 16:25
moleris:) 16/05 16:26
pigworkerI fear this is likely to continue.16/05 16:27
pigworkerWe want the coe operator to exploit refl if it's there, but not get stuck if it isn't, so we'll need to be a wee bit canny.16/05 16:28
molerisCannyness is not something the current operator language is set up for16/05 16:30
pigworkernope, and it's a bit left-to-right, too16/05 16:33
molerisit is16/05 16:33
moleristhe ol' coe goes something like this: 16/05 16:33
moleris           oprun :: [VAL] -> Either NEU VAL16/05 16:33
moleris>          oprun [_S, _T, q, v] | partialEq _S _T q = Right v16/05 16:33
moleris>          oprun [C x,C y,q,s] = case halfZip x y of16/05 16:33
moleris>            Nothing  -> Right $ nEOp @@ [q $$ Out, C y]16/05 16:33
pigworkerwhen we have coe S T Q s, we wanna sneak a look at Q16/05 16:33
moleris>            Just fxy -> coerce fxy (q $$ Out) s16/05 16:34
moleriswhere partialEq is a hack to spot the presence of the refl hack16/05 16:36
pigworkerI guess the question is whether we need a more powerful operator language, or to make coe a separate thing16/05 16:36
molerisSame with coh is it?16/05 16:40
pigworkercoh is also a nuisance; you can leave it to snowball, but it's better not to.16/05 16:41
pigworkerwe certainly want coh S T Q refl = refl16/05 16:43
molerisyup16/05 16:44
pigworkerI mean coh S T refl s = refl16/05 16:44
molerisBoth otions seem fairly onerous16/05 16:49
pigworkerAt the moment, I'm inclining towards taking them out of the Operator language. One motivation for Operator is ease of Epic compilation, and we don't do that with coe or coh.16/05 16:51
molerisMakes sense16/05 16:52
molerisSo we add two more Head terms?16/05 16:53
pigworkerpossibly16/05 16:54
pigworkerwe also need to figure out how to project the structural behaviour from an equality proof16/05 16:55
pigworkerthat has an impact on how we handle refl16/05 16:55
pigworkerI think I may need to commune with a whiteboard...16/05 17:01
molerisOK16/05 17:01
molerisThere's plenty of stuff to be done that isn't equality16/05 17:02
molerisshall we chat about it again soon?16/05 17:02
pigworkeryeah; I'll let you know how the going is in a wee while16/05 17:03
molerisCheers16/05 17:06
pigworkerI think I'm getting a clue. We need some new Head terms, I think.16/05 17:44
pigworkermoleris: I think I might have a stab at hacking it in a bit. I have the beginnings of a plan...16/05 17:52
pigworkerI was gonna blog about universes but I might hack on equality instead.16/05 17:54
* pigworker is fickle.16/05 17:54
pigworkermoleris: Do we use Chkd anywhere?16/05 18:20
pigworkerI see, etaQuote uses it to do proof-irrelevance.16/05 18:23
pigworkermoleris: I've done a bit of equality hacking; dunno if it's any good. Will push patch.16/05 22:40
pigworkerPatch pushed.16/05 22:46
--- Day changed Wed May 18 2011
copumpkinpigworker: is your new SHE up somewhere?18/05 23:37
pigworkerWhich new SHE? The one in Kleisli arrows is the one on hackage.18/05 23:53
copumpkinoh, okay18/05 23:53
copumpkinI thought you'd added something to it for some reason :)18/05 23:53
pigworkerI am a bit behind on ghc versions, so a newer SHE is needed, but hasn't happened yet.18/05 23:53
copumpkinI do have a modified darcs SHE right now18/05 23:54
copumpkinjust though there was an even newer one18/05 23:54
copumpkin*thought18/05 23:54
pigworkerThe last thing I added to the hackage version was default superclass instances.18/05 23:54
pigworkerThe darcs version may contain a more recent bugfix (whose nature escapes my dim memory).18/05 23:55
pigworkerI've received patches for compatibility with newer library versions (which now include instances I was explicitly adding). I wish I understood how to make sure I don't break the old toolchain.18/05 23:57
--- Day changed Thu May 19 2011
Saizancabal defines dome CPP macros to check for versions of deps in #ifdefs, check dist/build/autogen/cabal_macros.h after a build19/05 00:03
doliopigworker: ping19/05 04:31
pigworkerdolio: good morning19/05 08:38
molerispigworker: I've wired your equality stuff to the parser, elaborator, pretty printer. About to have a play with it.19/05 14:00
pigworkermoleris: good! I await tales of my stupidity (whilst marking projects)19/05 14:20
molerispigworker: Got one for yer19/05 16:08
moleris> isRefl (Refl _ _ :$ _) = True19/05 16:09
molerisNot always :)19/05 16:09
pigworkermoleris: my bad; that should be isRefl (Refl _ _ :$ B0) = True19/05 19:19
pigworker'night all; on my travels for a week and a bit...19/05 22:43
--- Day changed Sun May 22 2011
augurepipeeps22/05 03:40
augurin Epigram: Practical Programming with Dependent Types section 2.2, mcbride very quickly starts using diamond operators and <...> and such22/05 03:41
augurwhat is all of this22/05 03:41
augurwhere does it come from?22/05 03:41
augurand also, what is rec doing? ive never understood this22/05 03:43
Saizanthe <plus x y : Nat> type is defined right there with the only constructor return<plus x y> : Nat -> <plus x y : Nat>22/05 03:46
Saizanthe \diamond is just part of the name \diamondplus22/05 03:46
augurok22/05 03:47
augurim not understanding this type then22/05 03:47
auguri should probably read gimenez22/05 03:48
Saizanit's mostly a "trick" to make x and y appear in the return type of \diamondplus, in the end it's a Nat packaged up in a fancy type22/05 03:51
augurhm22/05 03:51
Saizansee the type of mz22/05 03:51
Saizanwithout this <..> stuff you'd simply have mz : Nat -> Nat, and it would have been harder to see in which case of the plus definition you are22/05 03:52
Saizaninstead here you can read from the type that mz is supposed to handle the case for which the first argument is zero22/05 03:53
auguroh i see22/05 03:53
augurthe point is to provide a case combinator that takes arguments that know which case they're for22/05 03:53
augur?22/05 03:53
Saizanyeah, you create such a case combinator, more like induction principle actually, by passing (\ x -> (y : Nat) -> < plus x y : Nat >) to the more general NatInd22/05 03:56
augurhm22/05 03:57
augurok im going to order food22/05 03:57
Saizanthis seems the #1 FAQ of this channel btw :)22/05 03:59
augurSaizan: lol22/05 04:38
augurwell that should tell you (and conor) something!22/05 04:38
Saizanyeah, that learn you a epigram should be quite explicit about it :)22/05 05:02
--- Day changed Tue May 24 2011
molerisagundry: You about?24/05 10:45
agundrymoleris: indeed24/05 10:45
molerisHow are things?24/05 10:45
molerisHow was TFP?24/05 10:46
agundryTFP was good, an interesting mix of talks and I think mine went okay24/05 10:46
molerisGood to hear24/05 10:46
agundry(though it was a bit rushed and incomprehensible at the end, as I always seem to manage...)24/05 10:46
molerisThe end is the least important bit (:24/05 10:47
agundryI'm a bit behind on the epigram front as I've been thinking about type-level numbers in Haskell24/05 10:47
molerisWhich is fair enogh24/05 10:48
agundrybut pigworker tells me that progress has been made on equality?24/05 10:48
molerisYeah, he put some stuff together which you might want to look at.24/05 10:48
molerisWe left the Op language as is24/05 10:48
molerisand instead added canTy rules for the equality type24/05 10:49
molerisand extra heads for Refl, Coe and Coh24/05 10:49
molerisIn the mean time I've been putting the rest of the system back together24/05 10:50
agundryhow are you getting on?24/05 10:51
molerisPretty well24/05 10:52
molerisbut today I want to get programming problems to work again24/05 10:52
molerisand this has lead me to the file Tactics/Matching.lhs24/05 10:53
agundryuh oh24/05 10:53
molerisHehe24/05 10:53
molerisHow broken was this code before?24/05 10:54
molerisIs it worth stating afresh?24/05 10:54
agundryfairly; it was a rather half-baked implementation of matching that worked for the sort of higher-order matching problems we tended to encounter24/05 10:55
agundrybut sometimes produced type-incorrect results24/05 10:55
agundrystarting from scratch might well be the best option24/05 10:55
molerisWhat I feared24/05 10:56
molerisI need to stare at it a bit any way to work out what happens with the new Tm24/05 10:57
agundryI always wondered if we could make more consistent use of the unification and matching machinery24/05 10:57
molerisProbably24/05 10:58
molerisI beat the Unification algorithm about to get it to work with the new Tm, made a bit of a mess of it to be honest24/05 10:59
agundryit was a bit of a mess to begin with24/05 10:59
molerisThe occurs check is a bit crazy with explicit substitutions lying around24/05 11:01
agundryah, so I see24/05 11:02
molerisIf you have any time and want to get stuck in there's plenty left to fix (:24/05 11:08
agundryI don't doubt it24/05 11:09
agundryWhat's the best way to get the thing to build at the moment?24/05 11:09
molerismake Pig24/05 11:09
agundryOh, sorry, it wasn't working because my dependencies were out of date, but seems to be going through now24/05 11:11
agundryI'm not sure I'll have much time, but are there any obvious things for me to look at that you won't be working on?24/05 11:12
molerisSchemes?24/05 11:14
molerisWishful thinking on my part there24/05 11:14
moleris(I'd need to fix the NameResolution wrt Schemes I think)24/05 11:16
agundrydo we have holes working?24/05 11:18
agundryhmm, she just ate all my memory trying to compile Cochon/DevLoad.lhs24/05 11:18
molerisOdd, maybe get rid of all her files and try again24/05 11:19
agundryI started from make clean in order to get anywhere24/05 11:20
molerisah24/05 11:20
agundryI'm compiling with ghc-6.12.1, is that still the best option or do we have ghc 7 support yet?24/05 11:21
moleris6.12 is what I use24/05 11:21
molerisStupid thing is that DevLoad is completely commented out (:24/05 11:21
agundryso it is24/05 11:22
molerisif you remove the dependency on it in Main.lhs and 'make depend ; make Pig' do we have lift off?24/05 11:25
agundryI got past it by commenting out all the import statements, but now I'm stuck on Main.lhs24/05 11:26
agundrywow, some of the hers files are huge (several megabytes up to 43Mb for Main)24/05 11:28
moleriscan you get rid of them manually24/05 11:28
molerisI think 'make clean' leaves them in place24/05 11:28
agundryoh, that would be it, I assumed they were deleted24/05 11:29
agundrynow it works24/05 11:29
agundrythanks24/05 11:29
agundryit lives24/05 11:29
molerisyeah, it should really kill them24/05 11:30
agundrylooking at the Makefile, I think it does for those in the $(SRCS) list24/05 11:31
agundrymaybe I had an old one from somewhere else lying around24/05 11:31
molerisah, that would be my fault I think - I fiddled with that list without realising24/05 11:33
agundryI'm rebuilding and it's still very slow, perhaps I have an old she version or something24/05 11:34
molerispass24/05 11:38
molerisI do know that Holes are working though24/05 11:38
molerisso there's some good news24/05 11:38
agundryexcellent24/05 11:40
agundryI've solved my she problem: somehow I had a version of she without pedagand's newline patch from last year24/05 11:54
molerisagundry: OK, Now I understand the old matching code, I'm ready to throw it in the bin24/05 14:27
agundrygood24/05 14:27
molerisIf only I could remember how to do it properly :)24/05 14:28
agundryI wish I knew...24/05 14:31
agundryI guess we want to do something like Miller pattern unification24/05 14:32
--- Log closed Fri May 27 22:19:00 2011
--- Log opened Fri May 27 22:19:11 2011
-!- Irssi: #epigram: Total of 12 nicks [0 ops, 0 halfops, 0 voices, 12 normal]27/05 22:19
-!- Irssi: Join to #epigram was synced in 72 secs27/05 22:20
--- Day changed Tue May 31 2011
tsapimowning31/05 09:02

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