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

--- Log opened Tue Feb 01 00:00:42 2011
--- Day changed Wed Feb 02 2011
copumpkinvery quiet in here lately :(02/02 21:11
ccasinwhat would you like to talk about?02/02 21:20
copumpkinhow awesome epigram is!02/02 21:20
copumpkinand where e-pig.org went02/02 21:21
copumpkinoh it's loading now02/02 21:21
ccasinI can't wait for a proper release02/02 21:21
ccasinI am too scared to try the repository version, but really want to play with OTT02/02 21:21
ccasinI suppose I should just stop whining and implement it myself :)02/02 21:22
copumpkinlol02/02 21:22
--- Day changed Thu Feb 03 2011
pigworkerdrifting along with the tumbling tumbleweeds, ccasin wonders about a release version; I wonder if I'll ever get near the thing again03/02 09:01
Saizanlack of time or of interest?03/02 09:05
pigworkerlack of time03/02 09:08
pigworkerI never seem to leave getting-the-next-act-together-just-in-time mode.03/02 09:14
--- Day changed Fri Feb 04 2011
molerisn/window 304/02 11:10
molerisd'oh04/02 11:10
pigworkerfunny how that happens04/02 11:11
molerispigworker: Hey, how are things?04/02 11:12
pigworkerbonkers, as usual04/02 11:13
pigworkertoday's tasks include filling in my annual review form and having lunch with Kostas's family04/02 11:13
molerisgood luck with both04/02 11:14
pigworkerwhat you up to, week 14-18 Feb?04/02 11:14
molerispretty much nothing -- yet04/02 11:15
molerisEpigram?04/02 11:16
pigworkerif you were in Bonnie Scotland, we might manage a thing or two04/02 11:16
pigworkerI teach Agda of a Monday afternoon, and we have Gambino on Voevodsky on the Thursday. Then my birthday.04/02 11:17
molerisIt is probably the best week for me for a while -- I think we should go for it04/02 11:24
pigworkermoleris: ok, let's do that04/02 12:24
--- Log opened Thu Feb 10 15:52:12 2011
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]10/02 15:52
!holmes.freenode.net [freenode-info] channel flooding and no channel staff around to help? Please check with freenode support: http://freenode.net/faq.shtml#gettinghelp10/02 15:52
-!- Irssi: Join to #epigram was synced in 0 secs10/02 15:52
brixenis there a tarball of the source code for Epigram?10/02 18:38
brixenor could someone please make me one who has a current repo clone10/02 18:38
brixenI've tried for hours to darcs get http://www.e-pig.org/darcs/Pig09/10/02 18:39
Saizanhours? it completed in ~1 minute here10/02 18:42
dolioI've had pulls from the epigram repository hang for a very long time before.10/02 18:42
dolioEspecially if I haven't pulled in a while.10/02 18:43
brixenSaizan: I've been trying since last night, it continually fails10/02 18:44
brixenI had it in a sh while look trying to get the damn thing :(10/02 18:44
brixena tarball would be so very much appreciated 10/02 18:44
copumpkinbrixen: I'll send you one for $10010/02 18:44
brixencan I send you $100 monopoly bucks? :)10/02 18:45
copumpkinsure!10/02 18:45
brixenis there a paypall for monopoly bucks?10/02 18:45
Saizanhttp://saizan.ath.cx/Pig09.tar.gz <- does that link work?10/02 18:45
brixenSaizan: thank you!10/02 18:45
brixenany chance whatsoever this project would consider hosting on github.com?10/02 18:46
copumpkinpeople are so used to darcs around here10/02 18:46
copumpkinI wouldn't mind either way10/02 18:46
brixenyeah, I assumed as much10/02 18:46
copumpkinbut darcs is quite nice10/02 18:46
brixenwell, perhaps it's the host, but I constantly got timeouts that caused darcs to fail10/02 18:47
Saizanmaybe it always worked well for me because i'm in europe :)10/02 18:48
Saizanis patch-tag reliable these days? it would be easy to keep a mirror there10/02 18:49
brixenSaizan: thanks for the tar, it's building now!10/02 18:49
Saizannp :)10/02 18:50
copumpkinI never got too much of a good vibe from patch-tag10/02 18:50
copumpkinI dunno10/02 18:50
copumpkinhave you tried darcsden?10/02 18:50
Saizanno10/02 18:52
brixenSaizan: I'm going to try to make a git mirror with http://www.sanityinc.com/articles/converting-darcs-repositories-to-git10/02 19:13
brixenSaizan: I'll let ya know if I succeed10/02 19:13
copumpkinbrixen: I think fastconvert is the more accepted approach these days10/02 19:16
copumpkinhttp://hackage.haskell.org/package/darcs-fastconvert10/02 19:16
copumpkinI may be wrong though10/02 19:16
brixenI'll try it10/02 19:17
brixencopumpkin: thanks, worked like a charm10/02 20:27
brixenhttps://github.com/brixen/Epigram if anyone is interested10/02 20:28
copumpkin:)10/02 20:28
brixenI'll do my best to keep it current10/02 20:28
brixenis it correct that the last commit was 26-10-2010 ?10/02 20:28
Saizanyes10/02 20:35
--- Log closed Sat Feb 12 00:19:37 2011
--- Log opened Sat Feb 12 00:19:45 2011
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]12/02 00:19
-!- Irssi: Join to #epigram was synced in 85 secs12/02 00:21
--- Day changed Sun Feb 13 2011
j-invariantdarcs is the worst thing ever13/02 17:22
j-invariantwhy doesn't it just die?13/02 18:06
--- Day changed Wed Feb 16 2011
roconnoris normalization by evaluation how systems really work to decide convertablilty?16/02 17:53
roconnorit seems that you'd expect to be able to decide convertability in a lot of cases with just a bit of evaluation, if any at all.16/02 17:54
dolioNot all systems use NBE.16/02 18:11
dolioI think my interpreters just use 'normalize t == normalize u' during checking, but other places I only reduce to WHNF, and one could write a more complex decider for equality that worked that way.16/02 18:14
dolioReduce to WHNF and compare head constructors, then compare components.16/02 18:15
roconnordolio: I'm thinking that you could compare syntatic equality and if that fails then reduce to WHNF and compare head constructors and then recurse16/02 18:17
dolioYeah, there's that too.16/02 18:17
roconnorthat seems like it would often be fast16/02 18:17
roconnorbut I have no experience.16/02 18:17
roconnor(faster than NBE or normalize t == normalize u)16/02 18:17
dolioAgda may do something like that, but I don't feel like blowing up my computer to check.16/02 18:18
roconnorso I'm wondering if this NbE paper by Abel Coquand and Pagano is useful16/02 18:18
roconnoror just academic (not that that is a bad thing)16/02 18:19
pigworkerour new implementation (in progress this week) uses head-normalization, and is first-order16/02 19:06
pigworkerwe'll implement definitional equality as evaluate, eta-expand, compare for reference purposes, but it's clear that we can choose to do less evaluation at the cost of a more complex, less obviously complete algorithm16/02 19:09
merijnI think I've started to grok this thing. If the goal is to view programming as searching the space of well-typed programs then elimination with a motive is the way to construct valid searches in the space of well-typed programs given a well-typed partial program and a desired solution?16/02 19:36
pigworkerEWAM is one way to refine a programming problem, yes.16/02 19:50
roconnorpigworker: I would have though always delta expanding would cause an exponential blow up in evaluation time that would then render type checking impractical.16/02 21:09
pigworkerI've never found that to be the bottleneck.16/02 21:11
pigworkerOf course, it could be that the other bottlenecks prevented examples being interesting enough to expose the problem.16/02 21:16
pigworkerNote, by the way, that us Epigram folks have a secret weapon: labelled types.16/02 21:17
pigworkerWhen you define a function f : X -> Y, say, that induces a type family Computation_f : X -> Set with constructor return_f : Y -> Computation_f x and eliminator call_f : (x : X) -> Computation_f x -> Y such that call_f x (return_f y) = y16/02 21:24
pigworkerBy restricting access to this type, we ensure that call_f x1 c1 = call_f x2 c2 iff x1 = x2. We never compare the huge ugly eliminator terms which implement f.16/02 21:25
dolioI suppose it's conceivable that avoiding delta expansion could save a lot of time.16/02 21:30
pigworkerOf course, that's not enough to ensure that checking refl : ack 100 = ack 100 is cheap. resp ack (refl 100) is a more sensible proof of same...16/02 21:30
dolion = ack 6 6 ; n == n?16/02 21:30
pigworkerIt can and does. But it also takes time.16/02 21:30
pigworkerMostly, I'm just reluctant to optimize the implementation of equality before I know what I want it to mean.16/02 21:32
pigworkerWe're now whnf based, so more cheap syntactic yesses defo on the the cards.16/02 21:33
pigworkerWhat's significantly different in Agda and Epigram is that normalization is not just rewriting. We both do type-directed eta-expansion. Epigram does proof irrelevance and certain algebraic simplifications (e.g. monad laws).16/02 21:37
pigworkerdolio: The whole thing goes much quicker if you use lambda-abstraction (it doesn't matter what n is, it's itself) rather than let-abstraction in that example. The real question is what kind of trouble you get into even when you're not asking for it.16/02 21:40
pigworkerI accept, however, that it's churlish of the machine to ignore the heavy hint given by the let.16/02 21:41
pigworkerWhat I think is really dodgy is testing (f a) = (f b) by testing full definitional equality of a and b, before trying to compute (f a) and (f b). That "shortcut" can easily turn into a wild goose chase. A cheap sound test of a = b might well be a good idea. I propose to test if a and b are the same variable.16/02 21:49
dolioYeah, I fully testing a = b doesn't sound good.16/02 21:50
dolioEr, minus the I.16/02 21:50
dolioThat sounds like the opposite of what roconnor was suggesting in general. :)16/02 21:52
dolioQuick heuristic tests before you run the real thing.16/02 21:52
pigworkerIf we play it right, we ensure that you can always use a let-abstraction to point out a coincidence, and we make that trick stable with respect to lambda-lifting.16/02 21:52
roconnordolio: I'd be inclined to test a and b for syntactic equality and if that fails then reduce (f a) and (f b).16/02 22:12
dolioRight.16/02 22:12
roconnorof course, if conversion isn't a bottleneck, then I wouldn't do any of this fancy stuff.16/02 22:13
roconnorI'm just a surprised that it isn't16/02 22:13
roconnor*a bit surprised16/02 22:13
Saizanwhat is the bottleneck then?16/02 22:14
pigworkervarious whole-term traversal operations, e.g. metavariable update, discharging parameters to make de Bruijn indices16/02 22:16
pigworkerI think we've just figured out how to make the former a lot cheaper, and (fingers crossed) we've eliminated the latter.16/02 22:18
pigworkerImplement the lambda calculus a different way once a fortnight, and you too can discover the formula for going nowhere.16/02 22:19
--- Day changed Fri Feb 18 2011
agundrymoleris: ping18/02 10:26
--- Day changed Mon Feb 21 2011
auguroh hello21/02 05:37
augurlots of people i recognize21/02 05:37
auguranyone know anything about the class of data types that are inductively definable?21/02 05:38
auguror the type classes? like, are the monoids inductive? etc?21/02 05:39
augurmoleris: im apparently reading your thesis. this better be interesting. >|21/02 21:21
copumpkinI thought it was21/02 21:22
augur:D21/02 21:22
augurim going to blame you if its not, copumpkin21/02 21:22
copumpkinif you do, avoid doing so in here21/02 21:22
copumpkinit'll just be awkward21/02 21:22
augurawkward soup21/02 21:22
--- Day changed Tue Feb 22 2011
augurgod you people are so quiet :|22/02 23:58
--- Day changed Wed Feb 23 2011
molerisaugur: Let me know how you get on with my thesis, if you have any questions I'd be happy to help.. (:23/02 11:24
auguroh wow, hey moleris23/02 17:58
auguruh, yeah, your thesis went a bit over my head quite quickly23/02 17:59

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