--- Day changed Sat Jan 05 2013
augurbitonic: i can honestly say i dont know how pattern matching would work without using eliminators05/01 00:05
bitonicaugur: what do you mean?  Most other languages simply have the notion of pattern matching in the core calculus (e.g. GHC Core, Agda, Idris...)05/01 00:14
augurno i mean, i know THAT they have it05/01 00:14
augursyntactically05/01 00:14
augurbut i dont know how you'd implement it. epigram implements it more or less as sugar for eliminators05/01 00:15
augurafaik05/01 00:15
bitonicaugur: ?  you mean what are the semantics for pattern matching or how do you actually compile it?05/01 00:15
augurwhat the haskell for pattern matching with dependent types looks like.05/01 00:15
auguror whatever you want to implement it in05/01 00:16
augurfor elims, its just an axiom with some equations05/01 00:16
augurfor pattern matching, i have no idea05/01 00:16
bitonicaugur: you just refine your context with the information gained for each constructor, some unification is involved05/01 00:17
bitonicaugur: without the dependent pattern matching a-la Agda it should be relatively simple...  but I have a vague idea only too.  what I’m sure of is that TVftL seems very complicated05/01 00:19
bitonicthe whole process of reducing everything to eliminators05/01 00:19
augurhm05/01 00:19
augureliminators seem easy to me05/01 00:19
augurthe tricky part is the representation05/01 00:19
augurbut you also need some theorem stuff too apparently05/01 00:19
augurhence the addendum paper for it05/01 00:20
bitonicaugur: the elaboration seems easy to you?05/01 00:20
bitonicthe details look pretty hairy05/01 00:20
bitonicaugur: what’s the addendum paper?05/01 00:20
auguri dont remember the elaboration stuff, actually, i only understood bits of it, because i didnt know quite what certain things meant, but yeah it seemed reasonably easy05/01 00:21
augurthe addendum paper was uh ..05/01 00:21
augura few constructions on constructors, i think?05/01 00:21
augurfrom what i remember of the elaboration stuff, it was just a whole bunch of crap to turn concrete syntax into contexts05/01 00:21
auguri should re-read the constructions paper. i dont remember the motivation for it but im sure it made lots of sense05/01 00:22
augurim going to ask conor05/01 00:23
bitonicaugur: I’m referring to the elaboration on page 24, for example05/01 00:23
bitonicthere’s quite a lot of stuff going on of stuff going on05/01 00:23
augurgimme a sec05/01 00:24
augurwell05/01 00:24
augurwhy dont you link me to your version05/01 00:24
augurbecause theres like three05/01 00:24
auguris it the long version, the silly version, or the published version05/01 00:24
bitonicaugur: <http://strictlypositive.org/view.ps.gz>, first hit on google05/01 00:26
bitonicit’s the same as the “Final Version” here <http://www.cs.ru.nl/~james/RESEARCH/research.html>05/01 00:27
augurok ill look05/01 00:30
augurgimme a sec05/01 00:30
augurok lemme look05/01 00:40
augurpage 2405/01 00:41
auguroh that stuff, bitonic05/01 00:41
bitonicyeah, *that* stuff ehe05/01 00:41
augurno i never quite grokked that meta-operation stuff fully05/01 00:41
augurthe paper doesnt explain it very well, tho.05/01 00:42
bitonicagreed05/01 00:42
auguri suspect there's a lot of presupposed knowledge there05/01 00:42
augurall of this SPLIT and so forth05/01 00:42
bitonicwell yeah there are a lot of meta operations05/01 00:42
auguri would've written that stuff differently05/01 00:43
augurmore dumb examples to ease people into it05/01 00:43
augurok i need to sleep05/01 00:43
augurnight!05/01 00:43
bitonicyeah, me too, night!05/01 00:43
augur(also, tweet at conor for insights!)05/01 00:43
augurnight05/01 00:48
xplatbitonic: if you want the dirt on the 'by' rule i think you want to read 'elimination with a motive'?05/01 14:36
augurbitonic: so conor says05/01 14:36
augurEWAM shows how eliminators (used prudently) introduce constraints; AFCOC builds kit to solve 'em. Together, the kit for EDPM.05/01 14:36
bitonicxplat, augur: well, I wasn’t that much into the technicalities of the elaboration but more into finding out why it’s convenient to use eliminators05/01 14:39
augurbitonic: see those papers probably :)05/01 14:39
auguri think conor's big point tho is that having first-class eliminators lets you use different elimination schemes05/01 14:39
bitonicaugur: I guess you are psygnisfive on twitter05/01 14:50
auguryes :p05/01 14:50
dolioIf you're worried about the complexity of elaborating pattern matching into eliminators, you should be worried about baking that complexity into your core calculus without any bugs.05/01 16:09
dolioAlso, epigram conceivably allows you to use your own derived eliminators that allow you to decompose problems by things other than just straight induction, while still using pattern matching.05/01 16:11
augurdolio! \o/05/01 16:14
augurdolio: what i havent fully grokked about the custom elims thing tho is how you actually achieve it without just building everything on other elims05/01 16:15
auguror maybe you do but thats ok because its not quite the same05/01 16:15
xplataugur: you do eventually build everything on the 'natural' elims for your types, it just means your custom patterns that you built are first-class05/01 18:30
augurhm05/01 18:31
xplatagda handles this by just using 'with' and not 'by' and having you actually make a view type that has your custom patterns as constructors, but the epigram way has less weight for the user05/01 18:31
xplatand it has more of a 'feature' and less of an 'idiom/design pattern' feel, which ... well, how you might feel about that is a matter of taste05/01 18:33
augurxplat: hm hm!05/01 18:35
augurwell im off to read EWAM05/01 18:35
augurxplat: you're familiar with EWAM no05/01 22:38
xplataugur: a bit05/01 22:38
augurtheres a typo in 2.3 isnt there?05/01 22:38
augurwhere he says05/01 22:38
augurif the goal is05/01 22:38
augur? : forall m | N. m <= 0 -> m = 005/01 22:39
augurthe phi is not clear05/01 22:39
augurso we replace that with05/01 22:39
augur? : forall m, n | N. m <= n -> n = 0 -> m = 005/01 22:39
augurso now we can define05/01 22:39
augurphi = \m,n | N. m <= n -> n = 0 -> m = 005/01 22:40
augurbut earlier he says05/01 22:42
augurif ? : forall m, n | N. m <= n -> P[m,n]05/01 22:42
augurthen phi = \m,n.P[m,n]05/01 22:42
augurso i presume what he meant was that when we replace the original m <= 0 goal, we take phi to be phi = \m,n | N. n = 0 -> m = 005/01 22:43
xplat... let me take a look05/01 22:44
xplatthe version i'm looking at is a little different05/01 22:49
augurok05/01 22:49
augurlink?05/01 22:49
xplathttp://citeseerx.ist.psu.edu/viewdoc/download?doi= 22:49
augurthats the one im looking at!05/01 22:51
xplatanyway, yeah i think you're right, leaving the m ≤ n -> in was a brain fart or whatever05/01 22:53
augurcopy and paste error05/01 22:53
xplatalso likely, yes05/01 22:54
augurxplat: i think if i use spines for internal representations of applications, it should be ok, right?05/01 22:55
augurisnt that a common thing?05/01 22:55
augurrepresenting f x y z as App f [x,y,z]05/01 22:56
augurinstead of as App (App (App f x) y) z05/01 22:56
auguri think that would make evaluation a lot simpler, because identifying reducible elim apps is easier i think05/01 22:57
augurApp (Elim ...) [...]05/01 22:58
xplatyeah, this is fine05/01 22:59
auguralso im not sure i should actually use a dependently typed language for my little linguistic toolkit or not05/01 23:00
xplatagda does it, not sure what epigram is using (but if epilog is still up you can see it there)05/01 23:00
augurim thinking i might just want to use a decidable, sorted, first order system05/01 23:00
augurdecidable in that the propositions are all values not props05/01 23:01
xplatnot sure what you mean by 'sorted'.  just 'multi-sorted'?05/01 23:01
augurso like forall x. P is just any xs p05/01 23:01
auguryeah, the values have types05/01 23:01
augursimple types05/01 23:01
augurthe reason is, im not sure that dependent types are really beneficial for this05/01 23:02
auguri mean, they're nice in that they provide all sorts of rich structures05/01 23:02
xplat'forall x. P' is 'any xs p' sounds like a HOL-style system05/01 23:03
augurbut at the same time, im not sure that amount of structure is useful05/01 23:03
augurwell, what i mean is that it's just the same sort of value-level quantification as in haskell's any05/01 23:03
augurnot a propositional quantification as in agda05/01 23:03
xplatthat's what i mean too05/01 23:03
auguroh ok05/01 23:03
xplatpossibly you should look up isabelle and hol-light if you're interested in that direction05/01 23:04
augurwell see thats the thing05/01 23:04
augurim not even sure i need a rich proof theoretic system05/01 23:04
augurmost of the interesting work will be in testing, not proving05/01 23:04
augurmodel checking, essentially05/01 23:04
auguron finite models05/01 23:04
augursmall models, even05/01 23:05
augurso model checking wont be at all costly05/01 23:05
augurmy main desire is to avoid forcing a type-level distinction between elements of different sets05/01 23:05
auguri could use predicates as sets, but then we get into a nasty representational problem05/01 23:06
augurwhere theres types and theres sets and the two arent quite the same05/01 23:06
xplataugur: the HOL/LCF-school approach seems to be relatively amenable to plugging in different decision procedures05/01 23:07
auguri think i'd do best to avoid a built-in type system just because then i'd have to figure out what it means to fuse or split types, etc etc05/01 23:07
auguri dont really know HOL05/01 23:07
augurill have to give it a look05/01 23:07
auguri really like the look of ExtendedML actually05/01 23:08
auguri like signatures, conceptually05/01 23:08
augursignatures and theories05/01 23:08
auguri dont think ill need higherorder signatures tho05/01 23:10
augurbecause what sane theory of natural language is going to quantifier over the whole universe of functions05/01 23:10
augurbut then what if you want to employ generic mathematical concepts05/01 23:11
augurD:05/01 23:11

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