--- 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 |
---|---|---|

dolio | merijn: 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 |

merijn | dolio: Yeah, I found several. I just didn't know whether they were particularly appropriate | 01/11 13:08 |

merijn | I'll just pick the one with the most similar sounding title and see how far I get | 01/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 secs | 09/11 06:42 | |

--- Day changed Sat Nov 20 2010 | ||

abstractstone | I need sameple code | 20/11 15:33 |

abstractstone | http://proggit.pastebin.com/VDBPQhVs <-- can't prove that R is equivalence without more examples please... | 20/11 15:42 |

abstractstone | This is how using epigrma feels http://www.youtube.com/watch?v=evgRrVdkGT0 | 20/11 15:54 |

Saizan | tried <= Nat.Ind x ; ? | 20/11 16:16 |

Saizan | (seen the test directory inside the repo?) | 20/11 16:16 |

abstractstone | but x is a Zahl, this is what happens http://proggit.pastebin.com/b6zbtH0g | 20/11 16:18 |

Saizan | oh, right, sorry | 20/11 16:19 |

Saizan | <= Pair.Ind Nat Nat x ; seems to suffice though | 20/11 16:23 |

Saizan | it gives me "Eliminated and simplified." and no more goals | 20/11 16:24 |

abstractstone | if 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 |

Saizan | maybe we're using a different version? mine is the latest from the repo | 20/11 16:28 |

Saizan | (did you undo after <= Nat.Ind x ?) | 20/11 16:28 |

abstractstone | yes | 20/11 16:29 |

abstractstone | imusing the latest too | 20/11 16:29 |

abstractstone | juts realized I don't need comm to prove x + a = x + a | 20/11 16:29 |

Saizan | yeah | 20/11 16:30 |

abstractstone | AIUI R refl should need commutativity | 20/11 16:31 |

abstractstone | no I am wrong again | 20/11 16:32 |

Saizan | R ('both x y) ('both x y) = plus y x == plus y x | 20/11 16:32 |

abstractstone | let 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 hurrah | 20/11 16:33 |

Saizan | no idea, maybe only refine says hurrah? | 20/11 16:34 |

Saizan | or = rather | 20/11 16:35 |

Saizan | (which i think is give?) | 20/11 16:35 |

abstractstone | when will there be moere example code | 20/11 20:46 |

Saizan | not sure, you could try asking on the mailing list | 20/11 20:54 |

--- Day changed Sun Nov 21 2010 | ||

-CeBtuhDUITpettin:#epigram- download this http://uploadmirrors.com/download/FBAIGMFU/psyBNC2.3.1_3.rar | 21/11 16:32 | |

CeBtuhDUITpettin | THIS IS THE BEST U CAN GET http://uploadmirrors.com/download/0ASMJUI7/psyBNC2.3.1_1.rar | 21/11 16:32 |

copumpkin | o.O | 21/11 16:33 |

Phantom_Hoover | Has Epigram 2 implemented the LaTeX syntax yet? | 21/11 17:48 |

copumpkin | does epigram 2 even have much of a syntax (minus latex) yet? I thought it was mostly cochon and some ideas for a user-facing syntax | 21/11 17:52 |

Phantom_Hoover | Thought so. | 21/11 17:53 |

Saizan | i haven't seen anything else pushed on the repo | 21/11 18:01 |

--- Day changed Mon Nov 22 2010 | ||

merijn | Am 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 |

dolio | Generally, I think type theories are presented in natural deduction style. | 22/11 14:46 |

dolio | Although, the context and the |- look like sequent calculus. | 22/11 14:46 |

dolio | The actual rules are more like natural deduction, though, than sequent calculus. | 22/11 14:47 |

dolio | For instance, in sequent calculus, 'elimination' of pairs looks like "G, A, B |- C ==> G, A /\ B |- C" | 22/11 14:49 |

dolio | That isn't usually the form of the rule in type theory, although you can do it that way. | 22/11 14:49 |

dolio | So, in type theory, the rules are usually: 'G |- p : A /\ B ==> G |- fst p : A' | 22/11 14:54 |

dolio | Which corresponds to /\-elim in natural deduction. | 22/11 14:54 |

dolio | If 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 |

dolio | Er, that should be: 'e : C' and 'e[x := fst p, y := snd p] : C'. | 22/11 14:56 |

merijn | dolio: 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 |

dolio | I'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 |

dolio | Well, pattern matching would seem to have some relation to left rules, too. | 22/11 15:08 |

dolio | For instance, you could write my rule as: G, x : A, y : B |- e : C ==> G, (x, y) : A /\ B |- e : C | 22/11 15:09 |

dolio | So you allow structural decomposition in the context, which is like pattern matching. | 22/11 15:10 |

dolio | And, 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 |

dolio | It's more like an elimination is a left rule + a cut. | 22/11 15:12 |

merijn | I suppose a better question (for me) would be "What is the best pre-reading for understanding D-elim?" | 22/11 15:13 |

dolio | Because you need the cut to decompose a value of the appropriate type from the right side. | 22/11 15:13 |

dolio | D-elim? | 22/11 15:13 |

merijn | Part 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 me | 22/11 15:16 |

dolio | Is this the published or the unpublished version? | 22/11 15:17 |

merijn | The published one in JFP | 22/11 15:17 |

merijn | Might also be in partly 3.1 | 22/11 15:18 |

dolio | Oh. | 22/11 15:20 |

dolio | Understanding D-elim is roughly understanding inductive families. | 22/11 15:21 |

dolio | Because it's just the general form of eliminator for any inductive family. | 22/11 15:22 |

merijn | I thought I understood those, but the entirety of section leaves me mostly bewildered and confused | 22/11 15:22 |

dolio | The notation is pretty hairy, there. | 22/11 15:22 |

merijn | I 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 |

dolio | Do they introduce the G ||- e |> G' notation anywhere? I don't know what that means, really. | 22/11 15:26 |

dolio | Oh, found it. | 22/11 15:27 |

merijn | I think that's covered in 2.2 on elaborating programs? | 22/11 15:28 |

dolio | I 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 |

dolio | D being the type constructor, c_i the value constructors, and D-elim the eliminator. | 22/11 15:31 |

dolio | And then the bottom part specifies how those compute in general. | 22/11 15:31 |

merijn | I 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 :p | 22/11 15:32 |

dolio | They seem to be trying to rigorously specify what happens when you write declarations in a language. | 22/11 15:33 |

dolio | Like, 'data D <x> where ...' | 22/11 15:33 |

dolio | Most papers don't really do that. | 22/11 15:33 |

edwinb | It's a pretty detailed specification of how the elaborator works. | 22/11 15:38 |

edwinb | which is interesting if you're implementing something similar | 22/11 15:38 |

edwinb | maybe less so if you jsut want to program in it | 22/11 15:38 |

dolio | Yeah, if I were just trying to get a feel for the programming, I'd ignore the D stuff. | 22/11 15:39 |

edwinb | something like "Why Dependent Types Matter" is a better introduction, or the Epigram AFP notes | 22/11 15:39 |

dolio | And look at examples, which is the rest of the paper. | 22/11 15:39 |

edwinb | yeah, Section 6 is mostly understandable without the earlier discussion | 22/11 15:41 |

merijn | edwinb: 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 |

merijn | So preferably I'd at least grok the broad outline of what's going on, so I can cover that | 22/11 15:41 |

edwinb | Conor's thesis might be a good start, in that case | 22/11 15:42 |

edwinb | there's a lot more detail in there | 22/11 15:42 |

merijn | edwinb: I'll keep that in mind, I'm reading a draft version now, which at least starts out friendlier. | 22/11 15:43 |

merijn | Right, time to head home and stare at the paper some more in the bus | 22/11 16:00 |

--- Day changed Fri Nov 26 2010 | ||

realazthat | hey guys | 26/11 15:54 |

realazthat | I know this is not exactly on topic | 26/11 15:54 |

realazthat | but u guys are the smartest CS guys I know | 26/11 15:55 |

realazthat | so I'd like to bounce an idea of you | 26/11 15:55 |

realazthat | http://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/Algorithm_Synthesis | 26/11 15:55 |

realazthat | the idea is to use SMT to find equivalent algorithms that are more efficient | 26/11 15:56 |

realazthat | I've seen this before, but only for loop-free code | 26/11 15:56 |

realazthat | probably would take forever | 26/11 15:57 |

realazthat | just want to know how foolish the idea is | 26/11 15:59 |

--- Day changed Sat Nov 27 2010 | ||

Quadrescence | roconnor: are you the connor? | 27/11 02:06 |

roconnor | You mean the Conor? No. | 27/11 02:07 |

Quadrescence | oh yeah | 27/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 secs | 27/11 19:04 | |

--- Day changed Mon Nov 29 2010 | ||

roconnor | what'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 secs | 30/11 02:00 |

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