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

--- Log opened Mon Aug 01 00:00:43 2011
--- Day changed Tue Aug 02 2011
pigworkermoleris: ping02/08 11:56
molerispigworker: pong02/08 11:58
pigworkerhi, did you get to see the cricket btw?02/08 11:58
pigworkerI've just added a wee patch (unpushed as yet) to SHE...02/08 11:59
pigworkerit makes Monad yield default Applicative and Functor instances02/08 12:00
molerisI missed out on tickets actually02/08 12:01
molerisoh well02/08 12:01
pigworkerrats02/08 12:01
molerisWould have gone today if there was play :)02/08 12:02
molerisJust had a look at the data stuff you pushed02/08 12:02
pigworkeroh the irony02/08 12:02
molerislooks OK02/08 12:02
pigworkerThe Pig does not compile with my new SHE, but it should just be a matter of deleting instances.02/08 12:03
molerisOK02/08 12:03
molerisI can do that if you want02/08 12:03
pigworkerI'll see if I can it sorted this end, then push changes to both at once.02/08 12:03
molerisFair enough.02/08 12:03
pigworkerHow much trouble do you think the listy levitation would be?02/08 12:04
pigworkerThere seem to be more moving parts.02/08 12:05
molerisI do worry about it a bit02/08 12:06
molerisbut I might get my hands dirty02/08 12:06
pigworkerwe at least have the luxury of adding it alongside the old one, then making a choice02/08 12:07
molerisYup02/08 12:11
moleris1st attempt will also involve hard coding Lists I think02/08 12:11
pigworkerI guess so02/08 12:11
molerisLunch time here, chat more anon02/08 12:12
quicksilverooh, a new version of she02/08 13:02
quicksilverI wish hackage had changelogs02/08 13:02
* quicksilver fails also to find changelog at http://personal.cis.strath.ac.uk/~conor/pub/she/02/08 13:03
augurquicksilver: stop, pigworker's site is full of enough broken links, dont make it worse by asking for a changelog :P02/08 14:14
quicksilver:)02/08 14:14
quicksilverwell maybe she and epigram and similar could live on patchtag or darcsden or github02/08 14:15
quicksilverso the changelogs are easily browseable02/08 14:15
pigworkerI've just added default superclass instances for Monad etc (see the docs on superclasses).02/08 14:15
quicksilverah02/08 14:16
pigworkerCorrespondingly, I commented out a lot of crap from the Epigram source.02/08 14:16
quicksilverthis feature should be more widely exposed and considered for haskell 201x02/08 14:18
quicksilverit's less controversial than idiom brackets and less obscure than pi types :)02/08 14:19
pigworkerquicksilver: see http://hackage.haskell.org/trac/ghc/wiki/KindFact and http://hackage.haskell.org/trac/ghc/wiki/DefaultSuperclassInstances02/08 15:19
quicksilverpigworker++02/08 15:23
pigworkerSHE's a bit of a general purpose cheap prototype...02/08 15:24
quicksilverno haskell-prime proposal yet though02/08 15:24
pigworkerthings pretty much have to be in GHC before they reach haskell-prime (whether that's the official position or not)02/08 15:25
quicksilverdepends what you mean by 'reach haskell-prime' I think02/08 15:26
quicksilverKindFact looks like it might collide - syntactically - with SPJ's DataKind plans.02/08 15:26
pigworkerin that it prevents a datatype called Fact being used as a kind?02/08 15:27
quicksilverpigworker: well, just in the fact that it also creates named kinds, and does so for a slightly different purpose02/08 15:42
quicksilvernot a conflict02/08 15:42
quicksilverjust a collision in the sense of two related but different ideas attaching to the same currently unused syntactical space02/08 15:42
* pigworker is mucking about with mixfix parsing (Agda envy), has tiny prototype implementation02/08 16:00
quicksilverpigworker: do you also break the symbol/character dichotomy?02/08 16:02
quicksilverand the :constructor +operator one?02/08 16:02
quicksilverin my head, at least, they're closely allied with general mixfix.02/08 16:02
pigworkerI'm much in favour of more space and less character classification.02/08 16:03
quicksilverI'm a bit undecided by general mixfix02/08 16:04
quicksilverbut I really really really want outfix02/08 16:04
quicksilverbra custom kets02/08 16:04
quicksilverwhich nest properly without horrific constructor typeclass precedence tricks.02/08 16:05
pigworkermy technology lets you create templates where...02/08 16:05
pigworker...a template is a sequence of (places or punctuation) such that...02/08 16:05
pigworker...there is at least one punctuation mark and no two places are adjacent02/08 16:06
pigworkeryou can then assert grouping rules...02/08 16:07
pigworker... group x + (y * z)    means * binds tighter than +02/08 16:07
pigworker... group x + (y + z)   means + is right-associative02/08 16:08
quicksilverhmm interesting.02/08 16:09
pigworkerI've tried a template  _ ! _ ! _   with  group a ! (b ! c ! d) ! e   which is alarming but unproblematic02/08 16:09
quicksilverthat's a bit like a bracket02/08 16:10
pigworkerI think I'd better allow "operator classes" (e.g. arithmetic, logical, etc) with general this-class-binds-tighter than that class, to save work, but NO MORE F***ING NUMBERS!02/08 16:10
quicksilverit's quite hard without numbers though02/08 16:11
quicksilverisn't there a quadratic explosion02/08 16:12
quicksilverif N libraries define disjoint operators?02/08 16:12
quicksilveror do you conservatively just make it illegal and require explicit parenthesising if operators don't have relative precedence?02/08 16:12
pigworkerIndeed it's conservative in that respect, but also the ordering is closed transitively02/08 16:13
pigworkerif we have generic operator classes, we could do a lot just by assigning an operator to a class02/08 16:14
pigworkere.g., if you invent a new arithmetic operator, you shouldn't have to establish its relationships individually with comparison operators02/08 16:17
dolioIt'd be nice to still have sections, too, incidentally.02/08 16:18
dolioThat's one thing I miss in Agda.02/08 16:18
pigworkersections are plausible (even right-sections, if you're crafty)02/08 16:18
pigworkerif _op_ has type (a : A)(b : B a) -> C a b, then check (. op b) by ensuring b : {a : A} -> B a, and deliver \ a -> _op_ a (b {a}) : C a (b {a})02/08 16:21
pigworkerI don't know whether a placeholder character is necessary for sections in general. Possibly not.02/08 16:23
quicksilversections are remarkably powerful expressively02/08 16:33
quicksilverfrom an "expressivity of syntax" angle, they are one thing that haskell got very very right02/08 16:34
quicksilver(probably more right than anyone realised)02/08 16:34
quicksilverI still remember the awed pause when I first realised you could write map ($x) [f,g,h]02/08 16:34
pigworkerI prefer [f,g,h] <*> [x], myself02/08 16:35
quicksilversure02/08 16:37
quicksilverit's only an example of the power of sections02/08 16:37
pigworkersure, just having fun02/08 16:37
dolioWhat about sequence [f,g,h] x? :)02/08 17:23
pigworkerindeed02/08 17:26
--- Day changed Sun Aug 07 2011
wieczykHi, it is possible to compile epigram by ghc7?07/08 16:52
wieczykI have error: http://hpaste.org/4994307/08 16:52
wieczykI am guessing that code is not compatible with some package, but cabal does not contain packages' versions.07/08 16:54
pigworkerwieczyk: looks like you might have an old version of SHE07/08 18:59
pigworkerI just added default superclass instances for Functor and Foldable (from Traversable), etc, and removed the corresponding hand-rolled duplicates from Epigram.07/08 19:02
pigworkercabal has the upgrade07/08 19:03
--- Day changed Tue Aug 16 2011
roconnorIs there anything I can read about how Epigram denotes and type checks dependent case analysis?16/08 20:56
roconnor!16/08 23:10
roconnorThere are a suprisingly large number of proofs of Absurd16/08 23:11
Saizanwhat do you mean?16/08 23:16
roconnor0 is a proof of Absurd according to the epitome16/08 23:41
copumpkin:o16/08 23:42
copumpkinthat sounds like a useful thing to have!16/08 23:42
copumpkinit makes so many of my proofs easier16/08 23:42
roconnoreveryone switch to epigram!16/08 23:42
roconnorAlso I cannot find where the Elim type constructor is defined.16/08 23:44
roconnormaybe I should look at the sources16/08 23:45
roconnorAh, found it in the sources16/08 23:47
roconnorbut not in the Epitome16/08 23:47
--- Day changed Thu Aug 18 2011
roconnoranyone know what operators are?18/08 03:18
Saizanfrom what i've seen they are primitives and/or glorified definitions which can have special simplification rules18/08 03:21
Saizani.e. if map is an operator you can make map fusion part of definitional equality18/08 03:22
roconnorhmm18/08 03:22
--- Day changed Fri Aug 19 2011
roconnorare there sum types in the Evidence langauge?  I don't see them.19/08 15:10
agundryroconnor: there are Sigma-types but not binary sums (which can be encoded with sigma using a two-element enumeration)19/08 15:13
roconnoragundry: Enumerations sounds like a kind of sum type.19/08 15:14
roconnorhow are they encoded and eliminated in the evidence language?19/08 15:14
* roconnor pull up the pig09 sources19/08 15:16
agundryan element of an enumeration is a natural number19/08 15:16
agundry(encoded in unary form using the Su and Ze canonical constructors)19/08 15:16
roconnorhow are they eliminated?19/08 15:18
agundryusing the builtin switch operator19/08 15:19
agundryhmm, looks like that bit is missing from the Epitome19/08 15:19
roconnoris it in the sources?19/08 15:19
agundrylook in Evidences/Primitives.lhs19/08 15:19
agundryif you really want to19/08 15:20
roconnoror would it be documented in one of the epitome references as well?19/08 15:20
roconnoroh, is switch an operator?19/08 15:20
agundryhmm, it might be in the Desc paper19/08 15:20
agundryyes, check out The Gentle Art of Levitation for a more comprehensible story than the Pig source code19/08 15:22
roconnorthanks this is helpful19/08 15:29
agundryyou're welcome19/08 15:30
--- Day changed Mon Aug 29 2011
copumpkinedwinb: nice slides!29/08 07:42
Saizantruly29/08 08:02
edwinbcopumpkin: thanks :). Now I'm off into hiding to turn them into a paper...29/08 13:31
--- Day changed Wed Aug 31 2011
cayleeSo I built Epigram on my machine, and I tried running examples from Syntax.pig but I got syntax errors on the data declarations and both kinds of equality - is it just out of date?31/08 17:40
pigworkerlet me have a quick look31/08 17:41
augurpigworker!31/08 17:42
augurthank you for pointing me in the right direction :)31/08 17:43
pigworkerSyntax.pig looks like it belongs to the time before we took it all apart again.31/08 17:43
cayleeAhh31/08 17:43
pigworkeraugur: happy to help31/08 17:43
Saizanare there examples that are meant to work with the current version?31/08 17:44
pigworkercaylee: inevitably, we're putting it back together again slightly differently31/08 17:44
pigworkerSaizan: I know a few things have started working, but I don't know if they've been assembled into useful files yet.31/08 17:45
cayleeOkay! So...I suppose I just need to keep reading the Epitome.31/08 17:46
pigworkeryou might have more fun in the short term by rolling back to the tag we put in before we smashed it up31/08 17:46
pigworkermost of the current reorganisations are boring and administrative... there's just a lot of them31/08 17:47
cayleeAh, so there's not a big difference in capabilities between the two? (I also apparently need to look at how to rollback in darcs...)31/08 17:52
pigworkerThere's a big difference in capability: the new version does a lot less, at the moment! The potential is the other way around, though.31/08 17:55
cayleeThat's what I was trying to ask, though clumsily. :-)31/08 17:56

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