--- Log opened Sat Jan 01 00:00:58 2011
Phantom_Hooverroconnor, which dev is in St. Andrews.01/01 01:41
Phantom_HooverI'm sure there's one in St. Andrews.01/01 01:41
Phantom_HooverYOUR SILENCE SPEAKS VOLUMES01/01 01:42
roconnorI don't know01/01 01:45
Phantom_Hooverroconnor, LIES01/01 01:46
--- Day changed Sun Jan 02 2011
elliottwould questions pertaining to she be out of place here?02/01 22:35
copumpkinpeople might miss out on the silence if you asked a question02/01 22:36
elliottsorry to deprive, then — but has there been much development since 0.1? i.e. is it worth using darcs she?02/01 22:37
copumpkinnot sure, I've always just used the darcs version02/01 22:37
elliotti'm using the release but I feel like I'm missing out on all sorts of bugs02/01 22:38
--- Day changed Mon Jan 03 2011
pigworkerer um, still awake for some vaguely cricket-related reason03/01 02:23
pigworkerquestions about SHE are certainly fair game; not so sure about answers03/01 02:24
pigworkerLeastways, I'm not sure I have time or energy to fix anything. But I'm sure there's plenty to worry about.03/01 02:26
elliotthehe03/01 02:26
pigworkerMr Shotgun is looking my way and shaking his head.03/01 02:26
elliott0.1 seems to be working.03/01 02:26
elliottwell. apart from the thing where my design is totally broken03/01 02:26
elliottas i discover that, in fact, {[Type]} is not really sufficient to carry around a dependent type context. ho hum. i should probably actually learn this stuff rather than trying to beat haskell code into submission03/01 02:27
pigworkerDependent contexts are trickier than that, yeah...03/01 02:27
pigworkerBut the Singleton construction for polytypes is kind of in a twist, too.03/01 02:28
elliottpigworker: "Nonsense! It's all so simple that I can do it in 50 lines of elegant Haskell."03/01 02:28
pigworkerNonsense usually requires less effort than that!03/01 02:28
elliottIt's very _advanced_ nonsense.03/01 02:29
elliottI believe it is called "type theory".03/01 02:29
pigworkerGo on then.03/01 02:30
elliottBy "It's all so simple that I can do it in 50 lines of elegant Haskell", I mean "it's not".03/01 02:30
copumpkinelliott: are you building off pigworker's recent blogpost?03/01 02:30
elliottcopumpkin: I was actually trying to see how simple I could get it before reading an Epilogue post that neatly demonstrates why my whole model is broken.03/01 02:31
elliottI think I've given up for now. :)03/01 02:31
pigworkerI was thinking of hacking Jón Fairbairn's superclass instance proposal into SHE, but Mr Shotgun demands paradigm-shifting articles.03/01 02:39
elliottI suggest you add syntax for unsafeCoerce!03/01 02:40
elliottThat would be great!03/01 02:40
pigworkerI think the existing syntax for that is ok.03/01 02:41
elliottpigworker: But it's so /verbose/.03/01 02:42
elliottWhat if I want to unsafeCoerce every other value?03/01 02:42
pigworkerI only said it's "ok". Actually, it's not nearly demeaning enough, but one must make allowances.03/01 02:43
dolioSuperclass instances as in, I can declare fmap in conjuction with my Monad instance?03/01 02:43
dolioOr declare defaults for it in the Monad class?03/01 02:43
pigworkerdolio: yep03/01 02:43
elliottI would support something like "unsafeCoerceAndYesIKnowI'mABadPerson x $$ PrettyPlease %% SOMEONE_SHOULD_REMOVE_THIS (())((IAmSoSoSorry))(())"03/01 02:43
pigworkerelliott: That's more like it.03/01 02:44
elliottpigworker: And every syntax highlighting mode is obligated, by law, to render it in red 72pt Impact, bold, italic, underline, and blinking.03/01 02:44
elliottWith a bright green background.03/01 02:44
doliopigworker: I don't know if that's wise. If you did that, you might develop an actual user base that you'd have to support. :)03/01 02:45
elliottThat would be really nice for a proper algebraic-structure numeric hierarchy. :p03/01 02:45
pigworkerdolio: The proposal, specifically, is to allow classes to declare default instances for their superclasses, and instances to override them.03/01 02:46
dolioThe whole shebang, then.03/01 02:46
pigworkerIt's funny. The question "what could I do with just a shitty preprocessor?" concentrates the mind.03/01 02:47
elliottEvery time I use she I'm *convinced* it won't be able to do what I want it to do, and then like magic it manages to completely fool me into believing I'm using a language with Real Dependent Types.03/01 02:48
dolioProbably seems less daunting than getting intimate with the relevant parts of GHC.03/01 02:48
elliottAt least until it complains about :@$()$#$#$#$#$#@@.03/01 02:49
pigworkerelliott: I was inspired by Asterix-style swearing.03/01 02:49
dolioI was expecting not to be able to partially apply pattern synonyms a while back, but I was pleasantly surprised at my being wrong.03/01 02:50
elliottpigworker: It certainly encourages me to bring out ghc -E -o /dev/stdout | less.03/01 02:50
elliottAnd gawp, in horror.03/01 02:50
pigworkerLet me assure you: not only is it nasty, it is also cheap.03/01 02:50
elliottAnd nasty.03/01 02:51
pigworkerdolio: I am also surprised, but perhaps I had a moment of enthusiasm.03/01 02:52
elliottI prefer to think it has features you don't even know about. Sort of like bugs, only more benign.03/01 02:53
pigworkerOf course it has features I don't know about. I am Goldfish.03/01 02:53
pigworkerIt would be awfully worrying if SHE acquired functionality people actually wanted.03/01 02:57
pigworkerBut I am comforted by the thought that I would not be the person most worried by such circumstances.03/01 02:57
elliottAs it stands, isn't she basically only useful for obsoleting she? "Oh, we have a fancy dependently-typed language implemented in Haskell/she now; guess we can forget about it."03/01 02:59
pigworkerThat's only one possible outcome, and it's very long term.03/01 03:00
pigworkerI'm very much in favour of stuffing as many dependently typed goodies as possible into Haskell as she stands.03/01 03:02
pigworkerNo point in being a snob. Far better to be infectious.03/01 03:03
elliottI was kidding really. She is a neat hack. Scares me though.03/01 03:04
elliottKeep preprocessing the code to check it's actually working.03/01 03:04
pigworkerSHE reminds me of synchronized swimming, shot from below.03/01 03:05
elliottThat analogy is like an analogy that makes perfect sense, shifted sideways slightly.03/01 03:07
copumpkinanyone know of an elegant way of ensuring in a datastructure that no duplicate names (I don't really care how these are represented, as long as they're unique) are defined?03/01 04:56
pigworkercopumpkin: maybe you could adapt the standard IR freshlist example03/01 13:29
--- Day changed Tue Jan 04 2011
TaralOkay, I think I'm *finally* understanding how this stuff all works.04/01 19:07
TaralCute how eliminators are fundamentally untyped, so you can apply them to all sorts of things (e.g. proofs)04/01 19:08
elliotti didn't know you did epigram :)04/01 19:09
TaralI do all sorts of things. :)04/01 19:09
TaralBeen trying to write a dependently-typed embeddable core in C for a work project.04/01 19:10
TaralI'm using Conor's stuff as a base.04/01 19:10
elliottTaral: in /C/? :D04/01 19:11
TaralYes.04/01 19:11
TaralWell, C++ technically, but I don't like shooting myself in the foot.04/01 19:11
elliottyou're trying to do practical things with dependent types and you're trying to do them in C, that's like, breaking two laws of the universe04/01 19:11
* Taral laughs.04/01 19:11
TaralYes.04/01 19:11
elliottwell ... good luck :P04/01 19:12
Taral:D04/01 19:13
elliottit'd probably be easier to Greenspun yourself half of GHC and do the rest inside that04/01 19:14
TaralGreenspun?04/01 19:23
edwinbhttp://en.wikipedia.org/wiki/Greenspun's_Tenth_Rule04/01 19:24
TaralOh.04/01 19:24
TaralYeah, I did that once.04/01 19:24
edwinbPlenty of practical things to do with dependent types, anyway!04/01 19:25
Taralmachine2.c, implementing a lisp machine with native continuations in C.04/01 19:25
edwinbIn as much as I understand "practical"04/01 19:25
TaralIt was designed to run in bounded stack and heap.04/01 19:25
edwinbthe point of the rule isn't so much that you actually implement lisp, but that you might as well have04/01 19:25
Taral(where bounded was in the single-digit KB)04/01 19:25
Taraler, double-digit, actually.04/01 19:25
TaralAnyway, it was for embedding in an OS kernel.04/01 19:25
TaralDoesn't everyone want a lisp machine in their kernel?04/01 19:25
edwinbIt's similar to the one pigworker taught me once, that if you want to write a program, best to start by writing the language that program is best written in04/01 19:26
TaralYeah.04/01 19:26
TaralSo the depcore is first written using dependent types, then manually "compiled" to C.04/01 19:26
edwinband that if you look at any program of any reasonable size, that's what the programmer has done whether they know it or not04/01 19:26
TaralI wish there were more verification tools for C.04/01 19:26
Taral:(04/01 19:26
edwinbwhy manually compiled? Do you need the C to be readable and maintainable?04/01 19:27
elliottTaral: frama-c? :p04/01 19:27
Taraledwinb: Because writing a compiler is harder.04/01 19:27
elliottHey, I want a lisp machine in my kernel. Well, okay, actually a lazy specialiser, but close enough.04/01 19:28
edwinbMay be harder but you only have to do it once...04/01 19:28
Taralframa-c isn't what I want. I want a full "program satisfies specification" verifier.04/01 19:28
edwinbof course, you have to convince your boss it's worth it I suppose04/01 19:28
TaralYeah, not likely.04/01 19:28
TaralBecause it's not.04/01 19:28
Taral:D04/01 19:28
edwinboh well then ;)04/01 19:28
elliottwhat about "why"? related to frama-c somehow i think04/01 19:29
elliottoutputs to Coq04/01 19:29
TaralThe biggest problem is that no matter what I do, there's chance of error.04/01 19:29
elliottvorpal in #esoteric used it once that's all i know :-D04/01 19:29
TaralOh god, why.04/01 19:29
TaralI never got that monstrosity to work.04/01 19:29
TaralAh, why's C verifier is caduceus, and "Caduceus is now obsolete and fully subsumed by Frama-C.:04/01 19:30
Taral"04/01 19:30
elliottit seems that frama-c can use why as a backend.04/01 19:30
elliott"jessie: to verify properties in a deductive manner. Jessie relies on the Why back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Coq. Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications."04/01 19:30
Taraloh! it does have specifications!04/01 19:30
TaralI'll give frama-c a go.04/01 19:30
Taral(wtb dependently-typed c)04/01 19:32
elliottTaral: My recollection of frama-c is the unicode char for blackboard N in a C comment, and thinking that was really really wrong. :-)04/01 19:32
TaralLOL04/01 19:32
TaralEpigram 2 only allows recursion by induction. But what if the termination proof of my function is by appeal to, for example, well-ordering?04/01 19:34
elliotthmm does it?04/01 19:34
elliottcoq allows well-ordered recursion i know that04/01 19:34
SaizanTaral: you do induction over an accessibility proof04/01 19:35
TaralHm.04/01 19:35
edwinbas you'd do it in Coq, basically, yes04/01 19:35
TaralBut inductive types in E2 aren't in Prop.04/01 19:35
edwinbthey are erasable though04/01 19:35
TaralHow do you decide if a Set is erasable?04/01 19:36
edwinbyou don't want them in Prop if you want to do computation over them04/01 19:36
TaralHm.04/01 19:36
* edwinb tries to think of a short answer that isn't just "Chapter 4 of my thesis"04/01 19:36
Tarallol04/01 19:36
TaralYeah, this is my problem. I keep getting confused.04/01 19:36
pigworkerThe word "erasable" should be forbidden unless qualified by "for open computation" or "for closed computation".04/01 19:36
Saizanwhen they're type determines their value :)04/01 19:37
Saizan*their04/01 19:37
edwinbwith a termination predicate, you can look at the indices and decide exactly what the constructor has to be, and exactly what the arguments have to be04/01 19:37
TaralAh, single-constructor after decomposition.04/01 19:37
edwinbso you don't need to look at the concrete instance of the predicate at all04/01 19:37
pigworkerin closed computation04/01 19:37
edwinbso you just throw it away and end up with the function you'd have written in the first place04/01 19:37
TaralOkay. The rule in Coq was that erasable things had to be in Prop.04/01 19:37
edwinbpigworker: thank you, yes ;)04/01 19:38
Taralpigworker: What does "for open computation" mean?04/01 19:38
pigworkerin the presence of hypotheses04/01 19:38
TaralYou mean . |-  vs \Gamma |-?04/01 19:38
pigworkeryep04/01 19:38
TaralOkay.04/01 19:38
pigworkerin open computation, lies are true04/01 19:38
TaralI usually reason in closed computation.04/01 19:38
edwinbalthough in open computation you can still throw away quite a bit04/01 19:39
edwinband we don't do open computation at run-time anyway04/01 19:39
TaralSo, for example, the standard accessibility predicate type (x : T) -> ((y : T) -> R y x -> Acc y) -> Acc x -- this is erasable in closed computation?04/01 19:41
edwinbyes04/01 19:41
TaralWoot.04/01 19:41
TaralOkay, I have to go spend a week grokking this now.04/01 19:41
Taral:D04/01 19:41
TaralLunch time, bbiab.04/01 19:41
TaralIs there a better way to do this?04/01 21:04
Taralmake AccID := \ T R x -> 'piD T (\ y -> 'piD (:- R y x) (\ _ -> 'varD y)) : (T : Set) -> (T -> T -> Prop) -> T -> IDesc T;04/01 21:04
Taralmake Acc := \ T R i -> IMu T (AccID T R) i : (T : Set) -> (T -> T -> Prop) -> T -> Set;04/01 21:04
Taral(I note that IMu is special and can't be partially applied, hence the eta-expansion.)04/01 21:04
pigworkersomeone might know how to use the idata tactic, or whatever it's called04/01 21:05
TaralAlso, Pig's implementation of IDesc differs from the paper. Are you planning to document this somewhere?04/01 21:06
Taral('fsigmaD and 'fpiD)04/01 21:06
pigworkeryes, we'll document it just before we change it again04/01 21:06
Taraloh, dear.04/01 21:07
Taralwell, your latest work on term representations will probably require extensive rewrites anyway...04/01 21:07
Taralthe Pig is dead! Long live the Pig.04/01 21:07
pigworkeryeah, there's an idata thing; I found an example04/01 21:09
pigworkeridata Va : (Sig (G : Cx ; T : Ty ;)) -> Set := ('top : (G : Cx) -> (T : Ty) -> Va [('sn G T) T ]) ; ('pop : (G : Cx) -> (S : Ty) -> (T : Ty) -> Va [G T] -> Va [('sn G S) T ]) ;04/01 21:09
TaralOh. Acc doesn't have constructors.04/01 21:10
TaralI could put in a single one, a la coq.04/01 21:10
pigworkeryeah04/01 21:10
Taral:(04/01 21:10
pigworkeranother nuisance is that idata doesn't let you analyse the index before you offer a constructor choice04/01 21:12
Taral*nod*04/01 21:12
TaralNo GADTs for you?04/01 21:12
TaralHow do I specify the difference between parameters and indices?04/01 21:12
pigworkerit's just trying to offer the old functionality, baking in the equational constraints04/01 21:12
TaralAcc has parameters T and R, with index i.04/01 21:12
pigworkeryou put parameters left of the : and you get one index right of it04/01 21:12
Taral(wtb implicit args)04/01 21:12
TaralAh, ok.04/01 21:13
pigworkerI hope04/01 21:13
Taralwait04/01 21:13
Taralah04/01 21:13
Taralmake AccID := \ T R x -> 'piD T (\ y -> 'piD (:- R y x) (\ _ -> 'varD y)) : (T : Set) -> (T -> T -> Prop) -> T -> IDesc T;04/01 21:14
Taralmake Acc := \ T R i -> IMu T (AccID T R) i : (T : Set) -> (T -> T -> Prop) -> T -> Set;04/01 21:14
Taralidata Acc (T : Set) (R : T -> T - Prop) : (x : T) -> Set := ('acc : ((y : T) -> (:- R y x) -> Acc T R y) -> Acc T R x04/01 21:14
Taraloops04/01 21:14
Taraljust the last line there. :)04/01 21:15
pigworkeryour (x : T) isn't in scope, I'm afraid04/01 21:15
Taral:(04/01 21:15
TaralHow do I name the index?04/01 21:15
pigworkerit should be, of course04/01 21:16
TaralYour G and T were in scope.04/01 21:16
Taraloh, you had them in the... curses.04/01 21:16
pigworkerno they weren't 04/01 21:16
pigworkerexactly04/01 21:16
Taralok04/01 21:16
pigworkercurses04/01 21:16
Taralidata Acc (T : Set) (R : T -> T -> Prop) : T -> Set := ('acc : (x : T) -> ((y : T) -> (:- R y x) -> Acc T R y) -> Acc T R x);04/01 21:16
pigworkerlooks more like it... does it buy that?04/01 21:16
TaralData'd.04/01 21:17
TaralInteresting.04/01 21:17
Taral > infer Acc;04/01 21:17
Taral(T : Set)(R : T -> T -> Prop) -> T -> Set04/01 21:17
Taralthat looks right.04/01 21:17
pigworkertry infer Acc.acc04/01 21:17
Taraldoesn't exist.04/01 21:18
Taralthere's an accTy...04/01 21:18
pigworkerI thought the constructors got chucked into the module, too, but what do I know?04/01 21:18
Taral      ConDescs04/01 21:19
Taral        [ \ i : T ->04/01 21:19
Taral        ] [((: indTy -> IDesc indTy) (\ i -> 'sigmaD T (\ x -> 'prodD 'xf ('piD T (\ y -> 'piD (:- R y x) (\ xf -> 'varD y))) ('constD (:- i == x)))) i)] : Sig (IDesc T ;) ;04/01 21:19
pigworkeryep04/01 21:19
Taralthrowing in a useless equality there, but otherwise looks right.04/01 21:19
pigworkercompulsory catholicism!04/01 21:20
TaralI'll stick with my hand-crafted one.04/01 21:20
TaralMore likely to be inferred as erasable in closed computation.04/01 21:20
TaralIn indexed types without equalities, inversion and other such advanced tactics are all implicit. It's so PRETTY.04/01 21:21
pigworkerYes, obviously so04/01 21:21
pigworker(I meant obviously erasable, not obviously pretty)04/01 21:21
Taralif I could write this, it would be awesome:04/01 21:21
Taralidata Acc (T : Set) (R : T -> T -> Prop) : (x : T) -> Set := ((y : T) -> (:- R y x) -> Acc T R y) -> Acc T R x;04/01 21:21
Taralor move the (x : T) if necessary.04/01 21:22
TaralI guess what I really want is to be able to "quote" the contents, so I can write A -> B -> C and get 'piD A ...04/01 21:22
pigworkertotal rethink required anyway04/01 21:22
Taralk :D04/01 21:22
TaralYou are much much smarter at this than I am.04/01 21:22
pigworkerI've just stepped on more of the mines already.04/01 21:23
Taral?04/01 21:23
Saizantotal rethink of what? IDesc's constructors?04/01 21:23
pigworkerrethink of how to declare a datatype04/01 21:24
pigworkerIDesc won't change much for a while (until we figure out how to internalise Mu and Nu nicely)04/01 21:24
TaralWhat's the advantage to internalized Mu/Nu?04/01 21:25
pigworkermuch neater mutual datatypes04/01 21:26
pigworkerBut we need to treat data declaration as a programming problem, allowing analysis of the index.04/01 21:28
TaralI'm still confused as to how to work with programming problems. All too often I end up just using ? and reverting to non-programming...04/01 21:31
TaralIt's all very clumsy right now.04/01 21:31
pigworkersure, but it will get less so, eventually04/01 21:32
TaralWhat I really like about Epigram2 is that I feel like I can *trust* the core. coq's dependent pattern match always struck me as too complex to verify.04/01 21:34
pigworkerThat's certainly an objective. Small, closed kernel. Elaboration, outside.04/01 21:35
TaralIs it possible to do quotient types?04/01 21:39
TaralMy brain locks when I try to work out the answer to that question.04/01 21:40
pigworkerhttp://www.e-pig.org/epilogue/?p=31904/01 21:40
pigworkeris at least a start04/01 21:41
Taraloh, I forgot about that.04/01 21:41
pigworkerI don't know how to do "choice functions" yet.04/01 21:41
Taral"STUFF YOUR SETOIDS" yes.04/01 21:41
TaralAh, quotients would have to be added as a feature.04/01 21:43
pigworkeryeah04/01 21:43
TaralStill, that's something.04/01 21:43
TaralWhat about ocaml-style polymorphic variants?04/01 21:44
TaralI think that requires subtyping, and subtyping is evil.04/01 21:44
pigworkersubtyping certainly makes me nervous04/01 21:45
TaralEVIL.04/01 21:45
Taralsubtyping in the absence of type inference is at least manageable.04/01 21:45
Taralsubtyping + inference = your brain explode.04/01 21:45
pigworkertoo many variables, not enough constraints04/01 21:45
TaralYup.04/01 21:46
TaralOh! I know how I can do it without subtyping.04/01 21:47
TaralI can have the elaborator do the work for me. :D04/01 21:47
TaralYou lose some dynamic features, but I don't care.04/01 21:47
pigworkerIt's certainly plausible to compute the required coercions: what's trickier is arranging for those coercions to have no runtime cost.04/01 21:50
Taral*nod*04/01 21:52
TaralThe other person on my project wants to put object-oriented programming in.04/01 21:52
TaralWhich requires subtyping.04/01 21:52
TaralWhich I told him is scary.04/01 21:52
TaralHe wants objects to have type ['method1 'method2] -> switch ...04/01 21:52
TaralBut that requires that sets of tags have a subtyping relation.04/01 21:52
TaralAnd I don't like duck typing in this context.04/01 21:53
TaralNeeds more thinking on my part.04/01 21:53
pigworkerat the moment, inclusion between enumerations can be free only if the small enumeration is a prefix of the big one04/01 21:55
TaralYeah, these don't have to be the same enumerations as are used for descriptions, though.04/01 21:56
TaralBut... no. I think I'm going to have to think about this more. My feeling is that there's a better way to do it.04/01 21:57
TaralOkay, meeting time. bbl.04/01 21:57
pigworkercheers!04/01 21:57
--- Day changed Wed Jan 05 2011
j-invariantAre modules parametric?05/01 11:31
j-invariantif I have an isomorphism between X and X', and I instantiate the module M in two different ways to get M(X) and M(X') I know there's a relation between the two but can it be proved?05/01 11:39
agundryj-invariant: Epigram doesn't have a proper module system (yet)05/01 11:47
j-invariantoh yes I look to the future05/01 11:47
agundryI'm not sure what the future plan for the module system is, gazing into the future is more pigworker's area of expertise than mine ;-)05/01 11:49
j-invariantmodules look like natural transformations - I'm curious if that's going to become a reality05/01 11:49
pigworkerj-invariant: it boils down to whether type-formers can be persuaded to respect isomorphism (in a necessarily proof-relevant way)05/01 12:00
j-invariantI guess that's been proved for the whole scheme of SPTs05/01 12:01
pigworkerreally?05/01 12:01
j-invariantoh I thought that was the case with the generic map/fold stuff - must have misunderstood05/01 12:02
pigworkerI mean, I expect it's somehow doable, by a construction a bit like observational equality, but isomorphism is more liberal than OTT equality on sets05/01 12:04
j-invariantif I understand type formers just means any F : * -> *, and just means when ij = 1, map_F i o map_F j = map_F 1?05/01 12:12
j-invariantrespecting isomorphism just means**05/01 12:13
j-invariantnot sure what I've mixed up05/01 12:20
doliopigworker: Hah! So you did it.05/01 12:39
pigworkercouldn't not, really05/01 12:53
pigworkerit took a day05/01 12:53
j-invariantand what will happne about induction-recursion?05/01 13:46
pigworkerj-invariant: not just for functors F05/01 13:48
pigworkerj-invariant: also, if f : S ~= S', then we need to derive some lifting to Pi S T ~= Pi S' (T . f^-1), and so on05/01 13:50
pigworkerre induction-recursion, I have a levitation-style coding, awaiting implementation05/01 13:51
j-invariantwow!05/01 13:51
merijnAre there any other papers/explanations of the BasicElim tactic or is "Elimination with a motive" the only one?05/01 14:28
pigworkermerijn: it shows up in my thesis; it's also present in some form in the View from the Left05/01 14:40
j-invariantpigworker: when you say you have a coding, is that like a PDF?05/01 14:43
pigworkerno, it's a lump of Agda05/01 14:44
merijnI'll take a look at your thesis. I encountered it in View from the Left too, but got stuck there (which is mostly why I grabbed "Elimination with a motive" to begin with). I think my background in type theory is just insufficient at the moment.05/01 14:45
pigworkerj-invariant: specifically, this lump of Agda http://www.e-pig.org/darcsweb?r=Pig09;a=plainblob;f=/models/Alg-IIR.agda05/01 14:48
pigworkerready for a levitated implementation05/01 14:49
pigworkermerijn: it works in two phases, constructing a motive with heterogeneous equality constraints, then solving the constraints05/01 14:50
pigworkerthe latter is also treated in "A Few Constructions on Constructors"05/01 14:51
pigworkeroh yeah, and the whole thing is revisited again again in "Eliminating Dependent Pattern Matching"05/01 14:51
pigworkerSee folks? You are doomed to keep writing your thesis until enough people understand it.05/01 14:51
merijnBetter either pick a trivially explainable thesis or an incredibly fun topic, then :p05/01 14:53
Saizanbtw, is there an algorithm to transform definitions accepted by agda's termination checker to ones that use only eliminators? for the inductive case at least05/01 14:54
j-invariantThat's what "Eliminating Dependent Pattern Matching" is about: AN algorithm exists (in theory) but nobody implements it05/01 14:54
j-invariantmaybe this is changing05/01 14:55
pigworkerI didn't make it fully automatic, but I made all the necessary pieces.05/01 14:58
dolioI guess Epigram doesn't quite count?05/01 15:00
pigworkerThe search space for splitting trees that correspond to a set of equations and refutations is finite, and there are good heuristics, but there are still corner cases where backtracking becomes necessary.05/01 15:01
dolioSince you can write several equations in Agda that wouldn't fit into the splitting trees that Epigram makes you write?05/01 15:01
pigworkerEpigram makes you choose the eliminations, but lets you define eliminators.05/01 15:01
merijnThe abstract of your thesis leads me to believe I could have saved a bunch of time by starting there directly instead of my mentor sending me on a wild goose chase through the references of various papers...05/01 15:02
pigworkerdolio: Do you mean that Agda allows fall-thtough?05/01 15:02
pigworkermerijn: Ah, but once you have found my thesis, the wild goose chase has just begun...05/01 15:03
doliopigworker: I mean, Agda would probably let you write the implementation of the majority function that you used to get in big arguments about on the epigram list.05/01 15:03
pigworkeryes, but not with the (open) operational semantics Berry wanted05/01 15:04
merijnpigworker: There goes my cause for optimism...05/01 15:04
pigworkerbehind the scenes, Agda also constructs splitting trees05/01 15:05
pigworkerIn fact, Agda's splitting tree construction is quite naive (in a reassuringly predictable way -- Ulf opted for predictability rather than cleverness, to make it easier to fight).05/01 15:08
pigworkerIf, in Agda, you write something like  suc x >= suc y = x >= y ; zero >= suc y = false ; x >= zero = true  it'll be strict in the first argument (so x >= zero = true will not hold for neutral x).05/01 15:11
dolioYeah. That is a little inconvenient.05/01 15:12
dolioAlthough, it doesn't seem easily avoidable.05/01 15:12
Saizanwhich epigram list?05/01 15:13
dolioThe old one.05/01 15:13
pigworkerit's avoidable if you can ask to split the second argument before the first (and then split the first only when the second is a suc)05/01 15:14
doliohttp://dir.gmane.org/gmane.comp.lang.epigram05/01 15:14
dolioYes, but then you have the same problem for zero >= x05/01 15:15
pigworkerbut that has to be strict in x!05/01 15:15
dolioOr, I guess that isn't a problem.05/01 15:15
dolioWell, in that example, then, you can rewrite it to behave nicely.05/01 15:16
pigworkerdolio: you can rewrite all of them to behave nicely, with helper functions etc05/01 15:16
dolioI guess the point of the majority function is that you can never split it such that you don't run into the problem?05/01 15:17
pigworkerthat's right05/01 15:17
Saizanan open computation evaluation strategy that looked at all the branches in "parallel", modulo overlapping ones, is going to be unsound wrt the normal evaluation for closed computation?05/01 15:48
copumpkinwhat do you guys think of http://snapplr.com/kd8w ?05/01 17:11
copumpkinregarding keeping exists/forall separate from sigma and pi05/01 17:11
j-invariantloss of parametricity?05/01 17:11
j-invariantwhy not make a language with parametricity built in05/01 17:11
TaralGood morning.05/01 17:19
doliocopumpkin: Have you heard of erasure pure type systems?05/01 17:27
copumpkinnope05/01 17:35
dolioReally?05/01 17:35
dolioThat's hard to believe, considering I talk about them so often.05/01 17:35
dolioAnyhow, they have annotated pis, which is essentially the same as having both pi and forall.05/01 17:37
dolioAnd you can extend that to inductive types to get sigma and exists.05/01 17:37
Taralpigworker: Why is your stuff still in ps.gz? Nobody uses that anymore. :P05/01 17:38
dolioPi actually has some non-trivial parametricity properties in many theories, though.05/01 17:39
pigworkerWhile I'm at it, why is my whole website hideously out of date? And why haven't I finished six papers? And where's my bloody Epigram 2?05/01 17:39
dolioLike, the theorems that would hold in Haskell would hold for the corresponding types in a dependent type theory.05/01 17:40
dolioJust not for other pi types that might not exist in haskell.05/01 17:40
dolioAssuming the dependent theory doesn't also have type case or something.05/01 17:40
TaralBasicElim looks a lot like coq "apply"05/01 17:43
j-invariantwhat do you mean by non-trivial dolio ?05/01 17:43
Taralpigworker: Clearly you need minions.05/01 17:43
dolioj-invariant: Bool has a 'parametricity theorem' but it's like 'forall b : Bool. b = b'.05/01 17:44
dolioThat's trivial.05/01 17:44
dolioforall a. a -> a, meanwhile, has a theorem that implies that it's inhabited only by the identity function.05/01 17:45
dolioWhich isn't trivial.05/01 17:45
pigworkerUnfortunately, the kind of people I can sometimes get the cash to hire are too clever to waste on wiping my arse for me.05/01 17:45
copumpkindolio: neat05/01 17:50
copumpkinso wait, is forall restricted to quantifying over Sets?05/01 17:50
copumpkinthe parametric one05/01 17:50
dolioErasure type systems do more than that.05/01 17:50
dolioThey let you quantify with forall over arbitrary types (including kinds), but they restrict the way you can use such variables.05/01 17:51
dolioSo if you do 'forall (n : Nat) ...', you would be prevented from inspecting n to do different things depending on what number it is.05/01 17:52
dolioAnd thus be parametric in n.05/01 17:52
j-invariantwhy not just write  pi (Nat : *). pi (n : Nat). ?05/01 17:53
copumpkinI see05/01 17:55
copumpkinthat's kind of neat05/01 17:55
dolioBecause the rest of the type may depend on n being a particular natural number type, not any type at all.05/01 17:55
j-invariantI don't get it, at all. As usual05/01 17:55
copumpkinso are there any plans for a "rally to restore parametricity" in any of the actual languages out there?05/01 17:55
j-invariantdolio: doesn'ot that just contradict parametricity again?05/01 17:56
dolioLike reverse : forall A n. Vec A n -> Vec A n05/01 17:56
dolioNo.05/01 17:56
dolioA function is parametric in an argument if its value is the same regardless of the value of that argument.05/01 17:57
dolioNot if it has an arbitrary type.05/01 17:57
j-invariantpumpkin: interested in uAgda?O maybe you can help me :P05/01 17:58
pumpkinunfortunately, I've only glanced at it05/01 17:58
pumpkinnot written any code in it :(05/01 17:58
dolioIn forall (a : *). a -> a, a has a particular type *, but values of that type are parametric in a.05/01 17:58
Taralpigworker: You don't PAY minions. That's silly.05/01 17:58
pumpkinhow about universe levels and parametricity over those?05/01 17:58
pumpkinwould you disallow pi over Level?05/01 17:58
dolioI've been meaning to write an interpreter that does that.05/01 17:59
dolioAlthough, I'm not sure there's anything wrong with universe dependence instead of universe parametricity.05/01 17:59
dolioAside from the fact that people are expecting the latter.05/01 18:00
pumpkinyeah, it just feels odd05/01 18:00
Taralwe were talking about erasure yesterday05/01 18:00
j-invariantuAgda has a way to reify the parametricity conditions05/01 18:00
Taralpigworker insisted we qualify "erasure" with "in closed/open computation"05/01 18:00
Taralwait, I'm confused again.05/01 18:01
TaralThis happens a lot to me in here.05/01 18:01
Taral:(05/01 18:01
dolioEPTSes are concerned with erasure on open terms.05/01 18:02
Taralah05/01 18:05
Taralso they restrict the ability to compute on values?05/01 18:06
dolioYes?05/01 18:06
TaralCool.05/01 18:06
dolioIf /\ is parametric lambda, then '/\(n : Nat) -> elimNat z s n' is a type error.05/01 18:07
pigworkerI'm certainly interested in adding forall to Epigram. Parametricity is a far better motivation than erasure (much of which can happen anyway, without introducing finer type distinctions).05/01 18:07
j-invariantI still don't understand why this gives you something that \(Nat : *)(n : Nat) .. doesn't05/01 18:07
Taralj-invariant: \(Nat : *)(n : Nat)(l : list n) doesn't type check.05/01 18:08
Taralbecause list is Nat -> *, not (Nat : *) -> Nat -> *05/01 18:08
pumpkinj-invariant: we want to explicitly disallow pattern matching on the n05/01 18:08
pigworkerindeed, one may write  append : forall m n. Vec m -> Vec n -> Vec (m+n)  and note that append doesn't need to compute with m and n, even though its type does05/01 18:09
j-invariantso it's like an explicit version of not needing to store indices?05/01 18:10
j-invariantdone by hand rather than the compiler05/01 18:10
pumpkinwell, it also gives you other guarantees about the function05/01 18:10
pumpkinthat it won't go do weird things if you pass it a Vec 16 and a Vec 1905/01 18:10
pumpkinfor example, currently, you could return a reversed list for that case05/01 18:11
pumpkinor maybe just replicate 35 . head05/01 18:11
pigworkeredwinb's index erasure mechanism relies on the index value being available elsewhere -- you don't store lengths in vectors because you *do* pass them to functions which manipulate vectors; no information is lost, but duplicates are avoided05/01 18:13
pigworkerforall gives the power to throw things away, even if you don't have a spare; you gain regularity by knowing you don't use that information05/01 18:16
Taralgrr parser05/01 18:31
Taralmake pf1 := :- (n : Nat) => FF : Set; fails05/01 18:31
Taralmake pf1 := :- ((n : Nat) => FF) : Set; is ok05/01 18:31
Taralmake t1 := ('zero == 'suc 'zero) : Prop; also fails05/01 18:34
j-invariantwhy?05/01 18:34
TaralI dunno!05/01 18:34
TaralParser is dumb.05/01 18:34
Taralmake t1 := ('zero == 'zero) : Prop; fails05/01 18:35
pigworkerI don't think the former is ambiguous. Parser is dumb.05/01 18:35
pigworker'zero, on the other hand, is meaningless without a type05/01 18:35
Taralah, point05/01 18:35
j-invariantahh05/01 18:35
Taralmake t1 := ((: Nat) 'zero == (: Nat) 'zero) : Prop; works05/01 18:35
Taralelaborator fail: let zero_not_suc : :- ((n : Nat) => ((: Nat) 'zero == (: Nat) 'suc n) => FF);05/01 18:37
Taral[ElabTrace] Hole zero_not_suc_3.zero_not_suc-type_0.h3_0.h4_1 started crying:05/01 18:37
TaralError: canTy: the proposed value  []  is not of type  Sig (xf : Nat ;)05/01 18:37
Taral[ElabTrace] Hole zero_not_suc_3.zero_not_suc-type_0.h3_0.h5_2 started crying:05/01 18:37
TaralError: elimTy: failed to eliminate 'suc h4 with n05/01 18:37
j-invariant(: Nat) 'suc n <--05/01 18:38
j-invariantthat could be (: Nat) ('suc n) maybe05/01 18:39
Taralugh05/01 18:39
Taralyes05/01 18:39
Taralmore parser fail then :(05/01 18:39
pigworker(: Nat) is treated like a function05/01 18:39
j-invariantwhat?05/01 18:39
Tarallet zero_not_suc : :- ((n : Nat) => (Nat.zero == Nat.suc n) => FF);05/01 18:39
pigworkerwhether that's a good idea is another matter05/01 18:39
Taralmuch better05/01 18:39
Taralwow05/01 18:40
Taralit auto-solved it05/01 18:40
Taralthat's neat.05/01 18:40
pigworkerNat.zero == Nat.suc n  is, by construction, a wrapper around FF05/01 18:43
Taralyeah05/01 18:43
Taralthat's what I was trying to see05/01 18:43
Taralturns out it's :- FF && FF05/01 18:43
TaralYou know how much shenanigans you have to go through to prove that in coq?05/01 18:43
TaralAnd in Pig it's FREE!05/01 18:43
pumpkinoink05/01 18:43
Saizancoq doesn't see that zero == suc n is empty?05/01 18:44
pigworkerTaral: I remember those shenanigans only too well.05/01 18:44
Taralinfo inversion was enough to make babies cry05/01 18:45
TaralSaizan: Not without some help.05/01 18:45
pumpkinthat's kind of sad05/01 18:45
pigworkerthe Discriminate tactic gets it easily enough05/01 18:46
Taralhttp://pastebin.com/mTk6jd1c05/01 18:46
Taralah, better proof there.05/01 18:46
j-invariantTaral: much easier way, just make a function f 0 = True, f 1 = False05/01 18:47
Taralhttp://pastebin.com/QNNqAK8Y05/01 18:47
Taralj-invariant: That's what discriminate does05/01 18:47
Taralit's still not as easy as "false by definition"05/01 18:47
pigworkeryeah, but it just relies on the usual eliminator05/01 18:48
pigworkerEpigram's == is hardwired specially (for extensionality)05/01 18:49
TaralI know :D :D :D05/01 18:49
TaralIt gets even better when you look at inversion05/01 18:50
--- Day changed Thu Jan 06 2011
pumpkinis it even conceivable for a type system to be able to determine automatically that moo : {f : Set -> Set} -> {a : Set} -> f a -> f a is extensionally equal to id ?06/01 21:25
pumpkinis this yet another of those cases where dolio will tell me to look at erasable PTSs? :P06/01 21:27
* pumpkin hangs head in shame06/01 21:27
Saizannot sure if they are enough for that06/01 21:30
doliocopumpkin: I think for something like that, you'd need a system that incorporated its own parametricity theorems.06/01 23:36
dolioThat's something Jean-Philippe Bernardy is trying to do, I think.06/01 23:47
dolioAlthough, I don't really like his approach to ensuring that parametricity.06/01 23:49
copumpkinwhat is it?06/01 23:50
dolioIt's essentially the same as Coq, have a separate Prop universe for irrelevant things. But he wants to be able to have universe polymorphism include that universe so you don't have to duplicate definitions.06/01 23:52
dolioThe contention of the EPTS folk, by contrast, is that irrelevance shouldn't be based on what universe a type lives in, but how it's used in a particular situation.06/01 23:55
dolioWhich also eliminates duplicate definitions.06/01 23:55
copumpkinah06/01 23:55
dolioBut the second one feels like a sound principle to me, and the former just seems like a scheme for getting rid of duplicate definitions.06/01 23:56
dolioEven if the former actually covers all the irrelevance/parametricity situations of the latter.06/01 23:57
copumpkinhm, ok06/01 23:58
dolioIt seems like, consider GHC's static-dynamic divide.06/01 23:59
--- Day changed Fri Jan 07 2011
dolioEven if you added facilities for you to make one declaration for both static and dynamic stuff, it'd still feel artificially divided compared to a system that didn't have two separate systems, but instead tracked all the individual things that are used statically versus dynamically.07/01 00:01
TaralMany of the types people want to erase are inherently non-informative, so you don't need anything special there.07/01 00:02
TaralThe rest are things like indices.07/01 00:02
TaralIf you can see the value, you can infer the erasability, but that doesn't help anyone who is trying to *use* the value.07/01 00:03
TaralHence EPTS, right?07/01 00:03
dolioLike, SHE can automatically generate type definitions from data definitions.07/01 00:03
Taraldolio: SHE is a horrid hack for adding pseudo-dependent types to Haskell.07/01 00:03
dolioBut (forgive me), C++ just tracks which ints (and so on) are statically known. There's no separate template-level int.07/01 00:04
TaralCorrect.07/01 00:05
dolioSo, C++ is better in that sense.07/01 00:05
Taralew.07/01 00:05
Taralso wrong.07/01 00:05
TaralAh.07/01 00:06
TaralC++ won't let you *compute* with ints at the type-level.07/01 00:06
TaralIf you want to do that, you have to add a type-level int "type" (= template) and do computation with that.07/01 00:06
Taralsame as Haskell.07/01 00:06
dolioI can't write 'f<m + n>()' if m and n are static?07/01 00:06
dolioOr f<g(m,n)>()?07/01 00:07
dolioAnyhow, if not, then consider Dependent ML instead.07/01 00:07
dolioAlthough it's limited.07/01 00:07
TaralNo, you can't write f<m+n>07/01 00:07
TaralYou can write f<plus<m,n>> if m and n are types that you want to "add".07/01 00:07
Taralbut C++ is strictly non-dependent.07/01 00:08
dolioI guess you can't really allow arbitrary C++ functions on integer template parameters.07/01 00:10
dolioSince they may do arbitrary side effects that don't make sense at compile time.07/01 00:10
Taral:)07/01 00:14
dolioLack of basic arithmetic is a little surprising, though.07/01 00:15
TaralIt was never the intention to allow any kind of arbitrary computation with templates.07/01 00:15
TaralThe fact that they are turing complete is an accident.07/01 00:15
dolioOkay, I can do this:07/01 00:46
doliotemplate<int m> void f() { const int n = m - 1; if(m > 0) { f<n>(); } }07/01 00:47
dolioAlthough it blows the template instantiation stack for some reason.07/01 00:47
dolioIt instantiates the function for negative values even though they'd never be used.07/01 00:48
dolioStupid C++.07/01 00:48
dolioI guess I'd probably need to use some kind of template-level conditional, if that even exists.07/01 00:49
Taraldolio: You can do that, but none of the logic is being used. You've basically said this:07/01 01:24
Taralwell07/01 01:25
Taralreplace f<n> with f<int>, if you will...07/01 01:25
Taralthe value isn't inspected, only the type07/01 01:25
Taraland things statically known about the value I suppose07/01 01:26
Taralbut not like you're doing it :D07/01 01:26
dolioEh?07/01 01:26
TaralSorry, it's been a while.07/01 01:26
Taralin the case you gave, there's nothing stopping someone calling f<-1>()07/01 01:26
Taralso... no termination for you :D07/01 01:26
dolioRight.07/01 01:27
TaralI dunno.07/01 01:27
TaralTemplates are voodoo.07/01 01:27
TaralI know you can't actually build dependent types out of them though.07/01 01:27
dolioRight. It's a static versus dynamic divide, and you can't cross from the latter to the former.07/01 01:27
dolioBut, there's no (even conceptual) duplication. Just some values are static and some are dynamic.07/01 01:28
dolioAlthough, you can't use most functions on static stuff, presumably.07/01 01:29
dolioIf you want to do certain fancy dependent-type-like stuff with such a system, you have to resort back to duplication, though.07/01 01:32
dolioBecause you can't talk about dynamic things in the static area.07/01 01:32
TaralHm.07/01 01:32
dolioSo you need to create dynamic types indexed by the static things to establish a correspondence.07/01 01:33
Taralbleh07/01 01:33
dolioWhich is what ATS does.07/01 01:33
TaralATS?07/01 01:33
dolioThere's static ints, and then a dynamic family of singleton types indexed by the static ints.07/01 01:33
dolio1 : int(1)07/01 01:34
Taralew07/01 01:34
dolioand then you work with exists n. int(n).07/01 01:34
dolioWhich is isomorphic to the regular ints, but lets you inspect them to refine types.07/01 01:34
dolioOr something of that sort.07/01 01:34
TaralAh, index extraction. :D07/01 01:35
dolioAnyhow, it's rather disappointing once you've worked with something like Coq or Agda.07/01 01:35
Taral*nod*07/01 01:35
copumpkinpigworker: I don't suppose you're still awake07/01 03:23
* copumpkin converts a huge chunk of code to use her idiom brackets07/01 05:13
pigworkercopumpkin: thanks to England's bowlers, I got a relatively early night07/01 10:10
quicksilverwell, there you go.07/01 13:30
copumpkinwhere??07/01 15:05
quicksilverI was looking for pigworker, and I found him.07/01 15:10
quicksilverso, here.07/01 15:10
copumpkinoho!07/01 15:10
copumpkin#agda, too07/01 15:10
quicksilverI'm not leet enough for #agda.07/01 15:13
copumpkinyeah, didn't think so07/01 15:14
copumpkin:P07/01 15:14
copumpkinpigworker: do you have a magic idiom bracket for a non-pure function too, in SHE?07/01 15:57
copumpkinwhere I have (baa <*> moo <*> oink)07/01 15:58
pigworker(|id baa moo oink|) should work07/01 16:01
pigworkerunless I'm losing the plot07/01 16:02
pigworkerI think I also added a (crappy) syntax for join.07/01 16:03
copumpkinoh, of course07/01 16:05
copumpkinyeah, I saw the syntax for join, but I don't have any monadic thingies for now07/01 16:05
--- Day changed Sat Jan 08 2011
j-invariantis a typed programming language like untyped lambda calculus with ornaments08/01 11:32
pigworkerj-invariant: fundamentally not; a typed programming language can have program inference08/01 12:33
pigworkeror do you mean, as an exercise in data representation? typed syntax can be presented as an ornament on untyped syntax08/01 12:35
j-invariantI just meant for data representation, but now I'm wondering what that is about program inference?08/01 12:41
pigworkertype classes provide an example of program inference08/01 12:42
pigworkertypes, as a high level document of structure are a good cue to program generation08/01 12:43
pigworkerthe people who talk of types solely in terms of error-policing are selling them massively short08/01 12:44
pigworkerThe text under a type signature need not be a mechanism in itself: it need merely describe the refinement of the type to a mechanism.08/01 12:47
j-invariantnice point of view - like logic programming08/01 12:47
pigworkeryes, I suppose it is08/01 12:47
j-invariantThe best kind of programming :D08/01 12:48
j-invariant(except for that all incarnations of it to date are useless)08/01 12:48
pigworkerMy beef with logic programming is that the mechanism is, by contrast, too well hidden.08/01 12:49
dolioYou don't have to worry about the mechanism. Except that you do.08/01 12:50
pigworkerI do envy the all-modes-at-once aspect.08/01 12:51
j-invarianthey I wonder if Kanren is monadic08/01 12:52
j-invariantthen you could fit it inside epigram and have your cake08/01 12:52
pigworkerI guess I should learn about Kanren08/01 12:52
j-invariantpigworker: it's a bit like prolog, but redesinged with the benefit of hindsight -- if you like elephants have a look at http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=1066308/01 12:53
pigworkerI'm certainly keen to "write functional programs that behave like relations".08/01 12:55
j-invariantone more thing I was curious about was what about large scale programming? It always seems to collapse in agda and coq (unless you're one of those amazing people that develop 4 color theorem)08/01 12:55
j-invariantI am worried about having to do reduction while typechecking: settings thins "opaque" in coq just does not work at all.  but if you don't do that you can sometimes get to a point where typechecking needs to evaluate a massive computaion08/01 12:57
pigworkerThere's a need to figure out how to renegotiate computational behaviour across modlue boundaries. To do that, you need extensionality...08/01 12:58
pigworkermudule, not modole08/01 12:59
j-invariantmaybe category theory (the way that abstract universal properties containing all the information of a concrete implementation) will become an important tool08/01 13:00
pigworkerit's central, in any case08/01 13:01
pigworkerthe computational behaviour of things, however, is how we separate machine work from people work08/01 13:02
--- Day changed Sun Jan 09 2011
* pigworker will be offline for a couple of hours, then on the train to Doncaster, Grantham, Nottingham; might manage some packets...09/01 11:10
--- Log closed Mon Jan 10 14:16:53 2011
--- Log opened Mon Jan 10 14:17:48 2011
-!- Irssi: #epigram: Total of 12 nicks [0 ops, 0 halfops, 0 voices, 12 normal]10/01 14:17
-!- Irssi: Join to #epigram was synced in 89 secs10/01 14:19
--- Log closed Wed Jan 12 11:10:25 2011
--- Log opened Wed Jan 12 11:10:33 2011
-!- Irssi: #epigram: Total of 14 nicks [0 ops, 0 halfops, 0 voices, 14 normal]12/01 11:10
-!- Irssi: Join to #epigram was synced in 93 secs12/01 11:12
TaralGood morning.12/01 17:17
TaralBeen awfully quiet in here the past few days.12/01 17:18
--- Day changed Thu Jan 13 2011
* roconnor wonders about combining patch theory with epigram's refinement of types approach to defining functions13/01 00:20
Taral*brain explode*13/01 00:25
roconnor:)13/01 00:25
--- Log closed Sat Jan 15 20:38:48 2011
--- Log opened Sat Jan 15 20:38:56 2011
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]15/01 20:38
-!- Irssi: Join to #epigram was synced in 96 secs15/01 20:40
--- Day changed Sun Jan 16 2011
pequalsnphi, there seems to be a typo in the epigram manual:16/01 17:52
pequalsnp... > refine plus ('suc m) n := 'suc (plus m n)16/01 17:52
pequalsnpshould be ... > refine plus ('suc m) n = 'suc (plus m n) , i think16/01 17:52
--- Day changed Wed Jan 19 2011
copumpkinwere GADTs based off of inductive families, or developed independently of them19/01 04:23
copumpkin?19/01 04:23
dolioI'd be surprised if it weren't the former.19/01 04:45
dolioI think GADTs + Extensible Kinds = Dependent Programming is the first GADTs paper.19/01 04:50
dolioAnd it cites inductive families, among other stuff.19/01 04:50
dolioMaybe I'm wrong, though.19/01 04:51
dolioI guess wobbly types predates that paper.19/01 04:52
dolioAnyhow, inductive families are mid-90s at latest.19/01 04:56
dolioAnd GADT-related stuff looks early-to-mid naughties.19/01 04:56
dolioIt looks like "guarded recursive datatype constructors" were invented without reference to inductive families, though.19/01 04:59
dolioAnd the wobbly types paper states that those are another name for GADTs.19/01 04:59
copumpkinI see19/01 05:16
copumpkinthanks19/01 05:16
copumpkinfreudian slip? :)19/01 05:16
--- Day changed Thu Jan 20 2011
Taral > idata le (n : Nat) : Nat -> Set := ('le_N : (n : Nat) -> le n n); ('le_S : (n : nat) (m : nat) -> le n m -> le n ('suc m));20/01 23:20
TaralI'm sorry, Dave. I'm afraid I can't do that.20/01 23:20
TaralError: C doesn't target T20/01 23:20
Taralah20/01 23:23
dolioC? T?20/01 23:23
Taralwhat a useless error message20/01 23:23
Taralthe problem is that the parameters are in-scope, and I'm overwriting them with un-needed foralls.20/01 23:24
Taral > idata le (n : Nat) : Nat -> Set := ('le_N : le n n); ('le_S : (m : Nat) -> le n m -> le n ('suc m));20/01 23:24
TaralData'd.20/01 23:24
TaralAnd... stuck again because programming problems are weird20/01 23:29
Taral:(20/01 23:29
Taral*sigh*20/01 23:29
Taralthere's nothing like "apply" or "constructor" in here.20/01 23:41
Taralusing = 'le_S ? works... until I want to call the IH, whereupon it fails because the IH returns a programming problem.20/01 23:41
Taralno, I'm an idiot.20/01 23:58
TaralI keep forgetting that you don't call those programming problems directly.20/01 23:58
TaralSo even though you have: \ eqfh : ((eq : Nat)(eqy : le eq y) -> < leTrans eq y m eqy xf : le eq m >) ->20/01 23:58
Taralyou refer to (leTrans eq y m eqy xf), not (eqfh eq eqy)20/01 23:58
--- Log closed Tue Jan 25 00:29:55 2011
--- Log opened Tue Jan 25 00:30:04 2011
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]25/01 00:30
-!- Irssi: Join to #epigram was synced in 96 secs25/01 00:31
--- Day changed Wed Jan 26 2011
dolioThought: A universe defined by induction-recursion is not the same as Martin-Loef's universe a la Tarski.26/01 00:43
Mathnerd314dolio: I have no idea what you just said.26/01 00:50
Mathnerd314*of what26/01 00:51
dolioAt least you've confirmed that it got sent.26/01 00:51
dolioOh, but pigworker isn't here, so he can't comment.26/01 00:54
Mathnerd314dolio: any idea of why it's not in the logs yet?26/01 01:10
dolioWhat?26/01 01:10
Mathnerd314your message(s)26/01 01:11
dolioI don't know.26/01 01:12
dolioMaybe that page is only generated at intervals.26/01 01:16
Saizanyeah, it takes a while to refresh26/01 01:24

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