--- Log opened Mon Nov 01 00:00:26 2010
merijn"The View From the Left" mentions inductive families of data types referring to work by Dybjer in the book Logical Frameworks. Any recommendations of papers/whatever covering the same subject since buying books is a bit to pricey for me?01/11 10:34
doliomerijn: A lot of Dybjer's papers are available online, including a bunch on induction. I don't know how good they'd be to learn from, though.01/11 12:49
merijndolio: Yeah, I found several. I just didn't know whether they were particularly appropriate01/11 13:08
merijnI'll just pick the one with the most similar sounding title and see how far I get01/11 13:08
--- Log closed Tue Nov 09 06:34:19 2010
--- Log opened Tue Nov 09 06:40:59 2010
-!- Irssi: #epigram: Total of 12 nicks [0 ops, 0 halfops, 0 voices, 12 normal]09/11 06:40
-!- Irssi: Join to #epigram was synced in 95 secs09/11 06:42
--- Day changed Sat Nov 20 2010
abstractstoneI need sameple code20/11 15:33
abstractstonehttp://proggit.pastebin.com/VDBPQhVs <-- can't prove that R is equivalence without more examples please...20/11 15:42
abstractstoneThis is how using epigrma feels http://www.youtube.com/watch?v=evgRrVdkGT020/11 15:54
Saizantried <= Nat.Ind x ; ?20/11 16:16
Saizan(seen the test directory inside the repo?)20/11 16:16
abstractstonebut x is a Zahl, this is what happens http://proggit.pastebin.com/b6zbtH0g20/11 16:18
Saizanoh, right, sorry20/11 16:19
Saizan<= Pair.Ind Nat Nat x ;  seems to suffice though20/11 16:23
Saizanit gives me "Eliminated and simplified." and no more goals20/11 16:24
abstractstoneif I do that then  show context  it says  pig : (a : Nat)(x : Sig (a : Nat ;)) -> Sig () -> < _ : :- (plus (x !) a) == (plus (x !) a) >20/11 16:26
abstractstone give plusComm ;  just errors though :20/11 16:26
Saizanmaybe we're using a different version? mine is the latest from the repo20/11 16:28
Saizan(did you undo after <= Nat.Ind x ?)20/11 16:28
abstractstoneyes20/11 16:29
abstractstoneimusing the latest too20/11 16:29
abstractstonejuts realized I don't need comm to prove x + a = x + a20/11 16:29
Saizanyeah20/11 16:30
abstractstoneAIUI R refl should need commutativity20/11 16:31
abstractstoneno I am wrong again20/11 16:32
SaizanR ('both x y) ('both x y) = plus y x == plus y x 20/11 16:32
abstractstonelet Rrefl (x : Zahl) : :- R x x ;20/11 16:33
abstractstone<= Pair.Ind Nat Nat x ;20/11 16:33
abstractstone^ once you do this... why doesn't it say hurrah20/11 16:33
Saizanno idea, maybe only refine says hurrah?20/11 16:34
Saizanor = rather20/11 16:35
Saizan(which i think is give?)20/11 16:35
abstractstonewhen will there be moere example code20/11 20:46
Saizannot sure, you could try asking on the mailing list20/11 20:54
--- Day changed Sun Nov 21 2010
-CeBtuhDUITpettin:#epigram- download this http://uploadmirrors.com/download/FBAIGMFU/psyBNC2.3.1_3.rar21/11 16:32
CeBtuhDUITpettinTHIS IS THE BEST U CAN GET http://uploadmirrors.com/download/0ASMJUI7/psyBNC2.3.1_1.rar21/11 16:32
copumpkino.O21/11 16:33
Phantom_HooverHas Epigram 2 implemented the LaTeX syntax yet?21/11 17:48
copumpkindoes epigram 2 even have much of a syntax (minus latex) yet? I thought it was mostly cochon and some ideas for a user-facing syntax21/11 17:52
Phantom_HooverThought so.21/11 17:53
Saizani haven't seen anything else pushed on the repo21/11 18:01
--- Day changed Mon Nov 22 2010
merijnAm I right that it might be enlightening to read up on sequent calculus in addition to the lambda cube for understanding epigram?22/11 14:00
dolioGenerally, I think type theories are presented in natural deduction style.22/11 14:46
dolioAlthough, the context and the |- look like sequent calculus.22/11 14:46
dolioThe actual rules are more like natural deduction, though, than sequent calculus.22/11 14:47
dolioFor instance, in sequent calculus, 'elimination' of pairs looks like "G, A, B |- C  ==> G, A /\ B |- C"22/11 14:49
dolioThat isn't usually the form of the rule in type theory, although you can do it that way.22/11 14:49
dolioSo, in type theory, the rules are usually: 'G |- p : A /\ B ==> G |- fst p : A'22/11 14:54
dolioWhich corresponds to /\-elim in natural deduction.22/11 14:54
dolioIf you want to make a sequent-alike type theory, your rule is something like: 'G, x : A, y : B |- C ==> G, p : A /\ B |- C[x := fst p, y := snd p]'22/11 14:55
dolioEr, that should be: 'e : C' and 'e[x := fst p, y := snd p] : C'.22/11 14:56
merijndolio: I got stuck reading the view from the left so I was going over a draft version of it with more notes and that made quite a few references to sequent calculus. So I figured that might provide some insight I was missing. But apparently the referenced paper by Gentzen is only available behind a paywall :\22/11 15:01
dolioI've read that reduction of sequent-calculus-style type theory derivations by eliminating cuts corresponds to eta-long beta normalization, though, so that's interesting.22/11 15:02
dolioWell, pattern matching would seem to have some relation to left rules, too.22/11 15:08
dolioFor instance, you could write my rule as: G, x : A, y : B |- e : C ==> G, (x, y) : A /\ B |- e : C22/11 15:09
dolioSo you allow structural decomposition in the context, which is like pattern matching.22/11 15:10
dolioAnd, I don't think it's quite precise to say that elimination rules in natural deduction correspond to left rules in sequent calculus.22/11 15:12
dolioIt's more like an elimination is a left rule + a cut.22/11 15:12
merijnI suppose a better question (for me) would be "What is the best pre-reading for understanding D-elim?"22/11 15:13
dolioBecause you need the cut to decompose a value of the appropriate type from the right side.22/11 15:13
dolioD-elim?22/11 15:13
merijnPart of the data declaration elaboration discussed in 3.2 of The View from the Left. Because I'm basically arbitrarily selecting important papers from the reference list and reading until it (hopefully) magically makes sense to me22/11 15:16
dolioIs this the published or the unpublished version?22/11 15:17
merijnThe published one in JFP22/11 15:17
merijnMight also be in partly 3.122/11 15:18
dolioOh.22/11 15:20
dolioUnderstanding D-elim is roughly understanding inductive families.22/11 15:21
dolioBecause it's just the general form of eliminator for any inductive family.22/11 15:22
merijnI thought I understood those, but the entirety of section leaves me mostly bewildered and confused22/11 15:22
dolioThe notation is pretty hairy, there.22/11 15:22
merijnI mean, inductive families are basically just datatypes defined by a set of constructors which may recursively refer to each other, thereby allowing things like heterogeneous lists, right?22/11 15:26
dolioDo they introduce the G ||- e |> G' notation anywhere? I don't know what that means, really.22/11 15:26
dolioOh, found it.22/11 15:27
merijnI think that's covered in 2.2 on elaborating programs?22/11 15:28
dolioI guess what the top part is saying is that the data declaration there introduces D, c_i and D-elim of the appropriate types.22/11 15:31
dolioD being the type constructor, c_i the value constructors, and D-elim the eliminator.22/11 15:31
dolioAnd then the bottom part specifies how those compute in general.22/11 15:31
merijnI swear I'm keeping a copy of this paper for the rest of my live so I can look at it every time I get uppity and be remorselessly crushed :p22/11 15:32
dolioThey seem to be trying to rigorously specify what happens when you write declarations in a language.22/11 15:33
dolioLike, 'data D <x> where ...'22/11 15:33
dolioMost papers don't really do that.22/11 15:33
edwinbIt's a pretty detailed specification of how the elaborator works.22/11 15:38
edwinbwhich is interesting if you're implementing something similar22/11 15:38
edwinbmaybe less so if you jsut want to program in it22/11 15:38
dolioYeah, if I were just trying to get a feel for the programming, I'd ignore the D stuff.22/11 15:39
edwinbsomething like "Why Dependent Types Matter" is a better introduction, or the Epigram AFP notes22/11 15:39
dolioAnd look at examples, which is the rest of the paper.22/11 15:39
edwinbyeah, Section 6 is mostly understandable without the earlier discussion22/11 15:41
merijnedwinb: I'm not so much aiming to program in it as I want to understand it. Doing a literature study on programming with dependent types and the research group is kinda interested in Epigram so my supervisor and me decided to do that.22/11 15:41
merijnSo preferably I'd at least grok the broad outline of what's going on, so I can cover that22/11 15:41
edwinbConor's thesis might be a good start, in that case22/11 15:42
edwinbthere's a lot more detail in there22/11 15:42
merijnedwinb: I'll keep that in mind, I'm reading a draft version now, which at least starts out friendlier.22/11 15:43
merijnRight, time to head home and stare at the paper some more in the bus22/11 16:00
--- Day changed Fri Nov 26 2010
realazthathey guys26/11 15:54
realazthatI know this is not exactly on topic26/11 15:54
realazthatbut u guys are the smartest CS guys I know26/11 15:55
realazthatso I'd like to bounce an idea of you26/11 15:55
realazthathttp://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/Algorithm_Synthesis26/11 15:55
realazthatthe idea is to use SMT to find equivalent algorithms that are more efficient26/11 15:56
realazthatI've seen this before, but only for loop-free code26/11 15:56
realazthatprobably would take forever26/11 15:57
realazthatjust want to know how foolish the idea is26/11 15:59
--- Day changed Sat Nov 27 2010
Quadrescenceroconnor: are you the connor?27/11 02:06
roconnorYou mean the Conor?  No.27/11 02:07
Quadrescenceoh yeah27/11 02:07
--- Log closed Sat Nov 27 19:02:37 2010
--- Log opened Sat Nov 27 19:02:49 2010
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]27/11 19:02
-!- Irssi: Join to #epigram was synced in 99 secs27/11 19:04
--- Day changed Mon Nov 29 2010
roconnorwhat's the difference between convertability and definitional equality in type theory?  Or do different schools use these terms differently?29/11 15:22
--- Log closed Tue Nov 30 01:58:43 2010
--- Log opened Tue Nov 30 01:58:51 2010
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]30/11 01:58
-!- Irssi: Join to #epigram was synced in 88 secs30/11 02:00

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