--- Log opened Thu Oct 01 00:00:52 2009
doliouniverse> :t \(l : Level) (A : Type[l]) (x : A) -> x01/10 00:14
dolio(l : Level) -> (A : Type[l]) -> (x : A) -> A01/10 00:14
vixeyis that Type part of the theory now?01/10 00:14
dolio:t (l : Level) -> (A : Type[l]) -> (x : A) -> A  ==> Type[omega]01/10 00:14
vixeyof a function?01/10 00:14
vixeyor**01/10 00:15
dolioIt's part of the type theory of the universe polymorphism I hacked onto my pure type system interpreter.01/10 00:15
vixeyaha cool01/10 00:15
dolioWhich isn't very sophisticated yet. It'll just blow up if I try to use multiple universe parameters, because I haven't done anything with constraint solving and whatnot.01/10 00:16
copumpkininterpreter?? does that mean you actually run code???01/10 00:20
dolioWell, yeah, if you consider normalizing lambda terms "running code".01/10 00:20
dolioSeems I've done something wrong, though.01/10 00:22
dolio:t \(l : Level) (C : (k : Level) -> Type[k] -> Type[k]) -> C (Suc l) (Type[l])01/10 00:23
dolioGives:01/10 00:23
dolio(l : Level) -> (C : (k : Level) -> Type[k] -> Type[k]) -> (k : Level) -> Type[k] -> Type[k]01/10 00:23
dolioWhich isn't right.01/10 00:23
dolioIt should be:01/10 00:23
dolio(l : Level) -> (C : (k : Level) -> Type[k] -> Type[k]) -> Type[Suc l]01/10 00:23
-!- ksf is now known as TheHunter01/10 01:15
-!- TheHunter is now known as ksf01/10 01:15
dolioAh hah. Seems to be a parsing error.01/10 01:19
vixeyyou shoudl proof your parser XD01/10 01:20
dolioYeah. I'll just whip up a total interpreter for a dependently typed language.01/10 01:22
vixeyoh??01/10 01:22
dolioAnd use that well-developed library of parser combinators.01/10 01:22
vixeydid you read James Chapmans thesis??01/10 01:22
dolioNo. Did someone finally manage something impressive in that area?01/10 01:23
vixeyoh yeah!01/10 01:23
dolioAre we talking total parser combinators or total language interpreters?01/10 01:23
vixeyhttp://cs.ioc.ee/~james/PUBLICATION_files/thesis.pdf01/10 01:23
dolioI knew about the parser combinators.01/10 01:23
vixeyI did parsers with proofs too01/10 01:23
vixeyit's really difficult01/10 01:23
dolioAgda folks have been working on that.01/10 01:24
vixeywell I don't see them doing proofs01/10 01:24
vixeyjust making parsers that are total01/10 01:24
dolioYes.01/10 01:24
vixeyyes ? to what01/10 01:24
dolioThey don't do proofs. Just make combinators that can be used at all in Agda.01/10 01:25
vixeyah ok01/10 01:25
dolioYou have to walk before you can run, though.01/10 01:25
vixeyI think the proofs have to be part of the libarary really -- obviously it's a starting point ... yeah walk before run01/10 01:26
vixeyfwiw I got the proofs working but mine is hideous to actually use :P01/10 01:26
vixeygetting all the well foundeded whatever it is together takes loads of book keeping, I think all that stuff can be automated once and for all thought01/10 01:27
dolio:t \(l : Level) (C : (k : Level) -> Type[k] -> Type[k]) -> C (Suc l) Type[l] ==> (l : Level) -> (C : (k : Level) -> Type[k] -> Type[k]) -> Type[l + 1]01/10 01:27
vixeythough01/10 01:27
dolioSuccess.01/10 01:27
vixeynice01/10 01:27
vixeyLevel is nat?01/10 01:27
vixeyor something conat? or else01/10 01:27
dolioLevel is sort of the extended naturals.01/10 01:28
dolioIt's built-in, though.01/10 01:28
dolioI have Level : Type[0] right now.01/10 01:28
dolioThe idea is that quantifying over Level ranges over naturals.01/10 01:29
dolioAnd then things of the form (l : Level) -> ... Type[l] live in Type[Omega].01/10 01:29
dolioSo maybe, technically, Level is just the naturals, and there's an extra universe above everything.01/10 01:30
dolioI think I have Omega : Level type checking right now, though.01/10 01:30
dolioThanks for that thesis, by the way. Ground-breaking stuff.01/10 01:32
vixeydolio all of his work it excellent! I have been waiting for that thesis to be released for some time01/10 01:35
vixeyhe uses techicolor!!01/10 01:35
vixeyI think we must thank Conor for this new trend01/10 01:36
vixey(?)01/10 01:36
dolioYeah, it's lie most Epigram papers.01/10 01:36
dolioLike, even.01/10 01:36
dolioQuite nice.01/10 01:36
dolioI wonder if they have a tool that automatically converts the Epigram source to nicely colored latex like that.01/10 01:37
vixeydolio does your thing do inductives and/or coinductives?01/10 01:52
opdolioHah, no.01/10 01:52
vixeyI think it's really easy to add inductives but um, adding coinductives is way beyond my knowledge01/10 01:52
opdolioIt's just does straight lambda calculi with pure type systems.01/10 01:53
vixeyI'm guessing that one wants OTT if they are adding coinductives but really just don't know anything verly clearly in that area01/10 01:53
opdolioAlthough I'm adding an "assume" command, so I can add names with types to the environment, which I think will let me experiment with types as if there were actual inductive types in the environment.01/10 01:54
opdolioIt just won't do anything during normalization.01/10 01:54
vixeyoh but you need normalization don't you :S01/10 01:55
opdolioRunning code is so 90s.01/10 01:55
vixeyfolds01/10 01:55
vixeylol01/10 01:55
-!- opdolio is now known as dolio01/10 02:03
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=10096#a1009601/10 02:39
vixeycool01/10 02:40
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=10096#a10101 Woo.01/10 16:39
--- Day changed Fri Oct 02 2009
* copumpkin didn't really get Nils' explanation on the mailing list02/10 06:35
copumpkinabout the Raw* distinction02/10 06:35
dolioI don't really, either.02/10 06:36
copumpkinhe sort of repeated the obvious at me :)02/10 06:37
dolioThe RawFoos in the algebra modules aren't even used for representing the operator set.02/10 06:37
dolioThere's a Foo with a declaration of all the operators, and then it defines a RawFoo as a consequence, copying all the operators to it.02/10 06:38
copumpkinyeah02/10 06:38
copumpkinthere's so much duplication in there02/10 06:38
copumpkinI've started a new algebra module that I hope will be nicer, but haven't had much time02/10 06:38
dolioGoing the other way around wouldn't be great either, though.02/10 06:39
dolioYou'd end up with "record Foo : Set1 where field raw-foo : RawFoo ; is-foo : IsFoo (RawFoo.op1 raw-foo) (RawFoo.op2 raw-foo) ..."02/10 06:40
copumpkinyeah02/10 06:40
dolioBecause you can only open them after the fields.02/10 06:41
copumpkinwhat bothers me is how deep you sometimes have to go to pull out properties02/10 06:41
copumpkinunless I missed something about how the modules work02/10 06:41
copumpkin(well, that and all the duplication)02/10 06:42
-!- koninkje is now known as koninkje_away02/10 08:56
-!- opdolio is now known as dolio02/10 15:44
copumpkinwow, it looks like nobody's touched this luo type theory book since it was purchased in 9402/10 16:13
dolioI suppose that isn't surprising.02/10 16:17
copumpkinguess not, but it's nice to have a brand new book02/10 16:19
copumpkinthe TAPL I checked out looked like a car had run over it02/10 16:19
--- Day changed Sat Oct 03 2009
-!- byorgey_ is now known as byorgey03/10 20:43
--- Day changed Sun Oct 04 2009
Arnar_hey there04/10 19:26
Arnar_anyone awake? :)04/10 19:27
faxyeah04/10 19:36
Arnar_:)04/10 19:42
Arnar_I'm trying to figure out on how to access some implicit arguments04/10 19:43
faxif you have04/10 19:44
faxf : Set -> {P : Set} -> ...04/10 19:44
faxthen you use:04/10 19:44
faxf A {P} ... = ...04/10 19:44
Arnar_can I pattern match on P?04/10 19:44
Arnar_even so..  I have this:04/10 19:45
faxif it's an inductive04/10 19:45
Arnar_small-to-big : ? {a v} -> a ?* value v -> a ? v04/10 19:45
Arnar_ah.. no unicode here of course :)04/10 19:45
Arnar_fist ? is forall, the other one just ctor04/10 19:46
faxif you use UTF-8 is should be finea04/10 19:46
Arnar_small-t-big : forall {a v} -> a -->* value v -> a => v04/10 19:46
Arnar_[] is one ctor for the _-->*_ type04/10 19:47
Arnar_and this works fine:04/10 19:47
Arnar_small-to-big [] = ?04/10 19:47
Arnar_but to write the term I need to access .v (the instance of v)04/10 19:47
Arnar_I tried small-to-big {a} {v} [] = ?04/10 19:47
Arnar_but then it complains04/10 19:47
Arnar_that it cannot verify that [] is of the correct type04/10 19:48
faxwhat is the type of []?04/10 19:48
Arnar__-->*_04/10 19:48
Arnar_(disclaimer: I'm working on a problem set in Ulf's course at Chalmers)04/10 19:49
faxI think that is not a type04/10 19:49
Arnar_data _-->*_ : Term -> Term -> Set where ...04/10 19:49
Arnar_it is just the list type over _-->_ (which is another type we have)04/10 19:50
Saizan_Arnar_: you've to use . to allow 'a' and 'v' to be constrained by the pattern matching on the constructor04/10 19:50
faxArnar: yeah so _-->*_ isn't a type then04/10 19:50
Saizan_Arnar_: small-to-big {.a} {.v} [] = ?04/10 19:50
faxSaizan was getting to that...04/10 19:50
Saizan_fax: sorry :)04/10 19:51
Arnar_Saizan_: hmm.. it just says  a is not in scope04/10 19:51
Arnar_Saizan_: if it's not a type, what then? :)04/10 19:51
faxArnar you could ask Agda what the type of [] is04/10 19:51
Arnar_ok, hang on04/10 19:51
Saizan_only put the . at v then, it actually depends on how [] is defined04/10 19:52
Arnar_fax: it says _495 -->* _495   (when I ask about the type of [])04/10 19:53
faxoh that's interesting04/10 19:53
faxthat means that a = v04/10 19:53
Arnar_Saizan_: just says v is not in scope then :/04/10 19:53
Arnar_fax: yes.. well04/10 19:53
Arnar_they are different types04/10 19:53
faxI guess there's too many things goin on at once for you to concentrate04/10 19:53
Arnar_but the ctors are overlapping04/10 19:54
faxa = v means they are the same type04/10 19:54
Arnar_fax: a is a Term, and v is a Value04/10 19:54
Arnar_"value" lifts values from terms04/10 19:55
Arnar_and here  a = value v04/10 19:55
faxdoesn't look that way to me04/10 19:55
Arnar_http://www.cs.chalmers.se/ComputingScience/Education/Courses/types/agda-lecture/Bool.html04/10 19:55
faxokay yeah what you said is true04/10 19:57
Arnar_still, what I really want now is what Saizan suggested, i.e. small-to-big {a} {.v} [] = ...04/10 19:58
fax[] tells you that a = v04/10 19:58
faxso try {a} {.a} or {.v} {v} or something like that04/10 19:59
Arnar_right, but they can be either true or false04/10 19:59
Arnar_hang on04/10 19:59
Arnar_ah04/10 19:59
Arnar_now we're getting somewhere04/10 19:59
Arnar_a != value v of type Term04/10 19:59
Arnar_when I do {v} {.v}04/10 19:59
Arnar_hmm04/10 20:00
Arnar_if I do {.v} {v} --- it says Value !=< Term of type Set04/10 20:00
Arnar_which I guess means Value is not a subtype of Term?04/10 20:01
Arnar_I have it04/10 20:01
Arnar_small-to-big {.(value v)} {v} [] = ?04/10 20:02
Arnar_then C-c C-c on v does the trick04/10 20:02
Arnar_:D04/10 20:02
-!- byorgey_ is now known as byorgey04/10 20:02
Arnar_thanks fax, Saizan_04/10 20:02
faxwhy did I keep insisting that a = v :/   yeah it's a = value v04/10 20:03
Arnar_hehe :)04/10 20:03
Arnar_C-SPC is not a good key to use on OS-X :/04/10 20:05
Saizan_Arnar_: btw, C-c C-e over an hole shows you the context04/10 20:38
Arnar_Saizan_: thanks. I've been using C-c C-, for the same result04/10 20:42
Arnar_agda2-give is C-c C-SPC... which I rebound to C-c Ent04/10 20:43
--- Day changed Mon Oct 05 2009
-!- Saizan__ is now known as Saizan05/10 02:19
Saizan_http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10452#a10452 <- is there good explanation to why i need to give a signature to t1 in S\Pi ?05/10 05:09
dolioIt might be too higher order for the unification algorithm to figure out.05/10 05:19
dolioOh, maybe it's ambiguous what type the first argument is, too.05/10 05:22
dolioNo, I guess not.05/10 05:23
Saizan_well, the first argument to _$_\equiv_ needs to be (tvar -> type tvar)05/10 05:23
Saizan_coq can infer it without the annotation, it seems05/10 05:23
dolioIf you do "t1 : _ -> _ -> _" which part turns yellow?05/10 05:25
Saizan_none05/10 05:26
dolioBut it turns yellow if you don't put a type annotation in?05/10 05:27
Saizan_yes05/10 05:27
Saizan_if i just use _ it turns yellow05/10 05:27
dolioWeird.05/10 05:28
dolioWhat if it's just _ -> _? :)05/10 05:28
Saizan_yeah, it can't conclude it's a function of two argument?05/10 05:28
dolioThat's hard to believe with "t1 v v'" in there.05/10 05:28
Saizan_no yellow with _ -> _05/10 05:29
dolioWell, that's definitely weird.05/10 05:30
dolioI don't know if that's worth reporting or not.05/10 05:31
dolioI guess you might as well.05/10 05:33
Saizan_i wonder if it's small enough as it is05/10 05:34
dolioWell, you can remove most of the constructors, at least, I guess.05/10 05:35
dolioYou can remove the \all part, too.05/10 05:36
faxhttp://upload.wikimedia.org/wikipedia/commons/5/5c/TooManyPigeons.jpg05/10 18:00
stevanhi, i got problems with \?= (decidable)... i get parse / scope errors when i try to use it, clearly i'm doing something wrong... here's an example: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10460#a10460   how do i use it properly? thanks.05/10 18:54
dolioAre "yes" and "no" in scope?05/10 18:56
dolioAnyhow, I don't see anything obviously wrong there.05/10 18:57
stevanah!05/10 18:59
Saizani always bump in some universe problem05/10 21:06
Saizanit seems i can only embed the predicative subset of System F in agda, which is not that surprising actually05/10 21:06
faxFixed system: Coq is a (reasonably) fixed and theoretically described system – it is an implementation of the Calculus of Inductive Constructions. Agda is more experimental. There is no pen-and-paper description of the underlying theory. As a result, Agda is a bit more open to less established ideas (universe polymorphism, different termination checkers, coinduction, etc.).05/10 21:08
faxLess is more: Coq is a complex beast05/10 21:09
dolioSaizan: You mean, embedding the language like an interpreter?05/10 21:10
dolioI suppose that wouldn't be too surprising.05/10 21:10
Saizandolio: yeah05/10 21:10
Saizanthough they don't seem to have this problem in coq05/10 21:11
dolioAre you doing it the same way?05/10 21:11
dolioAlso, they have a sort of universe polymorphism in Coq, so that may make a difference.05/10 21:11
dolioCoq even has a flag to make Set impredicative, I think.05/10 21:12
Saizani think i'm doing it like here http://adam.chlipala.net/papers/PhoasICFP08/ , but i might be missing something05/10 21:15
faxoh yeah that wont work in Agda05/10 21:15
Saizanbut the universe subtyping of Coq still keeps everything free of paradoxes?05/10 21:16
faxnice http://www.cse.chalmers.se/~wouter/Talks/AIM%20X.pdf05/10 21:26
dolioAre they encoding an impredicative System F? I can't really tell.05/10 21:26
Saizanwell, foralled types are not in a distinct type05/10 21:27
dolioYeah. But predicativity is about whether you can have 'forall a. T' and instantiate a to 'forall b. U'.05/10 21:31
dolioI guess you can do that?05/10 21:31
dolioSince you can substitute a type(T) in for a T? And 'forall b. U' is a type(T)?05/10 21:32
Saizanwell it seems like it allows 'a' to be instantiated by any SystemF's type, so also foralled ones05/10 21:32
dolioIt's been a long time since I read this paper.05/10 21:32
Saizanif i had a working coq installation i could try05/10 21:33
Saizanthe problem seems to be that typeDenote's result is of type Set here http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10465#a1046505/10 21:34
Saizanwhile in agda i need Set1 because of the forall05/10 21:34
faxI have Coq not Agda05/10 21:35
dolioT : Set?05/10 21:35
dolioin TAll?05/10 21:35
Saizanyes05/10 21:35
dolioMaybe it uses impredicative Set?05/10 21:35
Saizanit could be, yeah, i don't know much about coq05/10 21:37
faxAdam always uses impredicative Set05/10 21:37
dolioI don't really understand how impredicative Set doesn't lead to the same paradoxes as Type : Type?05/10 21:38
* Saizan neither05/10 21:38
dolioOr does it, and that's why they got rid of it (with the flag for turning it back on)?05/10 21:38
faxwell I think there are type theory experts that are not comfortable with it :)05/10 21:39
dolioOh, looking at some faq, I guess that impredicativity does let you construct Hurkens' paradox.05/10 21:40
dolioSo, there you go.05/10 21:40
faxhuh?05/10 21:42
dolioSaizan: Anyhow, if the code in that paper relies on impredicativity of Set, you can probably use {-# OPTIONS --type-in-type #-} to make things work in Agda.05/10 21:43
faxI don't think so05/10 21:43
faxor just use Coq05/10 21:43
dolioDon't think what?05/10 21:43
faxthat impredicativity gives you hurkens05/10 21:44
dolio"see file ClassicalDescription.v for a proof that excluded-middle and description implies the double negation of excluded-middle in Set and file Hurkens_Set.v from the user contribution Rocq/PARADOXES for a proof that impredicativity of Set implies the simple negation of excluded-middle in Set"05/10 21:45
dolioOh, I guess that's about something else.05/10 21:46
dolioYou can't model classical mathematics soundly in Coq if it also has impredicative set, or something.05/10 21:46
faxyes I beleive that's why they made it optional05/10 21:46
dolioIsn't double-negation of excluded middle always provable, though?05/10 21:49
faxaha! I see what you're saying05/10 21:50
faxclassical logic is a fragment of intuitionistic: So if we can't model classical then intuitionistic should break down too05/10 21:50
dolioWell, that wasn't what I was thinking, but that certainly sounds good. :)05/10 21:51
fax~~(P \/ ~P) is a theorem in Coq05/10 21:51
dolioRight. And if impredicativity implies ~(P \/ ~P)...05/10 21:51
faxwell the thing is: I haven't really understood this Hurkens stuff properly... just skimmed it years ago05/10 21:51
faxbut anyway that file you mentioned <http://coq.inria.fr/contribs/Paradoxes.Hurkens_Set.html> is not impredicative Set so much as having a bijection from Prop to bool05/10 21:52
fax(maybe I should have said ~~(P \/ ~P) is a theorem in CoC)05/10 21:56
dolioYeah, I don't really understand how to use that file, either.05/10 21:57
dolioOh, but...05/10 21:59
dolioThat file assumes {A} + {~ A} and proves False.05/10 21:59
dolioWhich gets you ~ ({A} + {~ A}), right? So if you have ~~({A} + {~ A}), those two get you False?05/10 22:00
dolio"Instead of the axiom U: U one assumes only '(A: U) → T(A) : U' if T(A) : U [A: U]. Notice the circularity, indeed of the same kind as the one that is rejected by the ramified hierarchy"05/10 23:29
dolioIs that equivalent to impredicative set?05/10 23:29
Saizan_since you can then instantiate the A with "(A : U) -> T(A)" it looks like it to me05/10 23:33
dolioYeah.05/10 23:33
Saizan_where is that cited from?05/10 23:35
dolioThe article on types (I think) on plato.stanford.edu.05/10 23:36
doliohttp://plato.stanford.edu/entries/type-theory/05/10 23:36
dolioToward the end.05/10 23:36
dolioSearching for Hurkens is an easy way to find it.05/10 23:37
Saizan_found it, thanks05/10 23:38
dolioI'm a bit confused by their wording, though.05/10 23:38
dolioIt says Girard "obtained his paradox" from that system, but also proved normalization for the type system.05/10 23:39
Saizan_maybe the paradox is only there in classical type theory? if there's one05/10 23:46
Saizancrushed..05/10 23:50
dolioHurkens' paper on the subject seems to be behind a pay wall.05/10 23:52
faxhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi= 23:53
dolioAnd I got Coquand's, but the mathematical symbols are all jumbled together.05/10 23:53
faxthis is good but very hard going05/10 23:53
faxwww.cs.chalmers.se/~coquand/paradox.ps05/10 23:53
dolioSame with that one.05/10 23:54
Saizanwhich paywall?05/10 23:55
dolioSpringer link or ACM.05/10 23:55
--- Day changed Tue Oct 06 2009
Saizanno pdf link on ACM, sadly06/10 00:00
Saizanhttp://www-cgi.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/hurkens95tlca.pdf <- from google scholar06/10 00:02
dolioAh, nice.06/10 00:03
Saizan(in the process i found that the first result for type theory is about typography, on google)06/10 00:15
faxhehe06/10 00:15
fax"Type Theory is a journal of contemporary typography"06/10 00:15
dolioMan, Hurkens' PTS rules only have two elements instead of three.06/10 00:34
dolioApparently all the rules are of the form (s,t,t).06/10 01:02
dolioOh, I guess that's what makes it impredicative.06/10 01:16
dolioSo, fiddling with the Hurkens stuff, it seems like you need one more level of impredicativity before you get inconsistency.06/10 07:34
Saizan_one more level?06/10 07:36
Saizan_so, e.g. not just impredicativity for Set but also Set1?06/10 07:37
dolioYes.06/10 07:37
dolioI mean, that should certainly be sufficient, because that's what they have in the paper.06/10 07:40
dolioThe paper has star, box and triangle.06/10 07:40
dolioWith the rules (*,*,*) ([],[],[]) and ([],*,*), the last one being impredicative (I think).06/10 07:42
dolioAnd that's consistent.06/10 07:42
dolioAnd they get inconsistency when they add (tri,[],[]).06/10 07:42
dolioThe hierarchy being * : [] : tri, incidentally.06/10 07:43
Saizan_i see, and this is all without inductive types, right?06/10 07:43
dolioYeah, it's just a pure type system.06/10 07:44
dolioSo, it would seem that you can have impredicative rules for Set, as long as everything above set is stratified appropriately.06/10 07:44
dolioUnless there's some undiscovered paradox out there.06/10 07:45
-!- jfredett_ is now known as jfredett06/10 07:45
Saizan_heh06/10 07:47
Saizan_another interesting thing would be an explanation of the inconsistency while keeping strong normalization bit06/10 07:48
dolioYeah, I don't know what that was about. Maybe he showed the inconsistency when you have that one axiom, but proved strong normalization for the system without it, which is still impredicative.06/10 07:49
dolioEr, rule, not axiom.06/10 07:52
Saizan_btw, i've skimmed attapl chapter on dep. types and it seems you get another source of inconsistencies from impredicativity + strong sums, and even there all is fine if the strong sums are only on small types06/10 07:53
dolioWell, that's good to know.06/10 07:55
Saizan_(it's a bit unsatisfactory that the chapter itself is not much more than an overview on the subject)06/10 07:56
dolioI was kind of disappointed that existential types had to live in Set1 in Agda when I first found it out.06/10 07:56
Saizan_by existentials you mean like in System F, right?06/10 07:58
dolioLike in haskell.06/10 07:59
Saizan_k, i was also surprised by polymorphic types being in Set1, today06/10 08:00
dolioIf Set were impredicative, you could define it as: ∃ P = ∀(r : Set) → (∀ a → P a → r) → r06/10 08:01
dolio∃ : (Set → Set) → Set06/10 08:01
Saizan_where are the rules for this universe hierarchy written down?06/10 08:04
dolioAnd, of course, you can't have the equivalent of 'data Foo = Foo (forall a. P a)' either.06/10 08:05
dolioWhich?06/10 08:05
Saizan_agda ones06/10 08:05
dolioAgda's is relatively simple. If you go read about basic pure type systems, or the lambda cube, it's a pretty natural extension of that.06/10 08:07
Saizan_"∃ P = ∀(r : Set) → (∀ a → P a → r) → r" was confusing me since (∀ a → P a → r) : Set1 and that made me think it'd make ∃ : (Set -> Set) -> Set206/10 08:07
dolioThe lambda cube's rules for function spaces look like: (*,*,*) (*,[],[]) ([],*,[]) ([],[],[]).06/10 08:08
dolioWhere * : [].06/10 08:08
dolioSo, you can see that you always take the maximum. So Agda's rules for spaces look like (Set_i,Set_j,Set_max(i,j)).06/10 08:08
Saizan_ah, i see, so in this case i'd get the maximum of Set1 and Set106/10 08:10
dolioSo, there (∀ a → P a → r) : Set1, and r : Set, so (∀ a → P a → r) -> r : max(Set1,Set) = Set1.06/10 08:10
dolioAnd then, yeah, max(Set1,Set1).06/10 08:10
dolioBut (Set -> Set) -> Set1 : Set2.06/10 08:10
-!- opdolio is now known as dolio06/10 18:53
doliocopumpkin: FYI, NAD informed me that using "True (coprime ...)" isn't just for making '4 % 5' easy.06/10 20:17
copumpkinoh?06/10 20:17
dolioApparently it makes the representation unique, whereas "Coprime num den" wouldn't.06/10 20:18
dolioProvably unique, that is.06/10 20:18
copumpkinhrm06/10 20:18
dolioWhich lets you use _==_ instead of an extensional, setoid equality.06/10 20:18
copumpkinoh06/10 20:19
copumpkinI can sort of see that, I think06/10 20:19
* Saizan needs an hoogle for agda06/10 20:40
Saizanwhere is True from?06/10 20:40
copumpkinRelation.Nullary.Decidable06/10 20:45
Saizanthanks06/10 20:46
doliofax: What do you use to write Coq?06/10 20:50
faxProof General06/10 20:51
fax(3 window mode & electric terminator)06/10 20:51
faxI'd recommend it to people too if there wasn't this stupid vim/emacs thing people can't seem to get around06/10 20:52
dolioOh, proof general is emacs?06/10 20:54
faxit runs inside emacs06/10 20:54
dolioOkay. Well, that'll probably work out well.06/10 20:55
dolioI tried coqide once before, and it confused the hell out of me.06/10 20:55
copumpkinoh no, we're losing dolio to coq06/10 21:03
dolioWell, I was trying to figure out that Hurkens stuff yesterday.06/10 21:03
dolioAgda has nothing comparable to -impredicative-set.06/10 21:04
dolioAnd programming directly in coqtop isn't very nice.06/10 21:04
fax:/06/10 21:12
faxworse than the emacs/vim is the "My language" thing06/10 21:12
dolioWell, quite frankly, I can't stand Coq's syntax.06/10 21:19
dolioThat may be superficial, but whatever.06/10 21:19
copumpkinit feels very old-school06/10 21:19
copumpkinmaybe we should make an agda-to-coq compiler06/10 21:19
dolioI have the same problem with MLs.06/10 21:20
faxsyntax doesn't matter06/10 21:23
dolioIt does to me.06/10 21:23
copumpkinfax: there are definitely more important things, but bad syntax is off-putting06/10 21:24
--- Day changed Wed Oct 07 2009
Saizan_what do you use as constructor name instead of \lambda when embedding some LC?07/10 02:03
Saizan_ -- inferred, id : term (Π (λ x → inj (Var x) ⇒ inj (Var x)))                                                                                 id = Λ λ a -> Lam {inj (Var a)} λ x -> Var x07/10 02:36
Saizan_yay for predicative System F2 phoas style07/10 02:36
dolioWhich part got inferred?07/10 02:38
dolioThe Pi part?07/10 02:39
Saizan_oh, irssi put it on a line, the signature above however07/10 02:39
Saizan_http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10515#a1051507/10 02:41
Saizan_i should test type application before declaring victory, i guess07/10 02:42
dolioNice.07/10 02:49
dolioIs this PHOAS style?07/10 02:50
Saizan_yeah, terms are parametric in the representation of variables07/10 02:50
Saizan_i've just realized that i need something at the value level to convert between terms of type "inj x" and "x" though07/10 02:51
dolioPeople were talking about HOAS in the most recent LTU posting, and I didn't realize, but PHOAS clears up a significant problem with the more naive HOAS.07/10 02:52
Saizan_and cast/cast' look like there should be a better way07/10 02:52
dolioNamely that a naive HOAS type has values that don't correspond to lambda terms.07/10 02:52
Saizan_yeah07/10 02:52
Saizan_and it's also easier to do some kinds of conversions07/10 02:53
dolioYeah, and they gave the impression that the two facts are related, but I don't really grok how that is. :)07/10 02:54
Saizan_aside from the fact that you get both by parametricity?07/10 02:55
Saizan_and you also have an explicit Var constructor07/10 02:55
dolioWell, the extremely naive HOAS example they gave was 'data Term = App Term Term | Lam (Term -> Term)', which, you can't do much at all with that.07/10 02:59
dolioEven if you make it a well-typed GADT sort of thing, about the only thing you can do is extract it into the meta-language.07/10 02:59
dolioA refinement was 'data Term a = App (Term a) (Term a) | Lam (Term a -> Term a) | Hole a', which lets you do analysis, but still has exotic terms.07/10 03:00
dolioAnd then if you replace Lam with 'Lam (a -> Term a)', you're back in 1-to-1 correspondence, but that's PHOAS.07/10 03:01
Saizan_ah, i see, the question is if you could have one without the other, somehow07/10 03:10
Saizan_having 1-to-1 without analysis, since the other case is known07/10 03:12
Saizan_it'd need to be a non-computable bijection, basically07/10 03:13
dolioI guess I may have over-interpreted the correspondence, since he clearly mentions a type with exotic terms that you can analyze.07/10 03:13
dolioAlthough, you can't really analyze the exotic terms.07/10 03:13
dolioBecause one of the things that makes a term exotic is that if you pass in a Hole, it may respond differently than if you pass in a Lam or an App.07/10 03:14
dolioSo your analysis may be wrong.07/10 03:14
Saizan_true07/10 03:14
dolioHe also talks about authors that make ad-hoc extensions to the type sytem (or something) to prevent people from constructing terms that would otherwise be allowed in the naive representations.07/10 03:15
dolioWhich you could probably do for the completely opaque version, too.07/10 03:15
dolioBut it'd still be useless.07/10 03:15
copumpkinit'd be nice if the compiler could use agda proofs to help it optimize code07/10 05:32
copumpkinsounds hard though07/10 05:32
stevanhi07/10 16:51
stevani got a problem with the following code which i don't understand how to solve: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10524#a1052407/10 16:52
stevani'd like to think that p can't be an object of add <= st and that it should be the absurd pattern there instead of p... but the typechecker says it isn't obvious... and when i try to case split on p i get an error which i don't understand saying something about not being able to unify some indices...07/10 16:54
--- Log closed Wed Oct 07 17:05:48 2009
--- Log opened Wed Oct 07 17:05:59 2009
-!- Irssi: Join to #agda was synced in 106 secs07/10 17:07
-!- pumpkin_ is now known as copumpkin07/10 20:05
-!- opdolio is now known as dolio07/10 22:22
--- Day changed Thu Oct 08 2009
copumpkinseanmcl: what happens if you leave out what's after the =?08/10 01:13
-!- copumpkin is now known as pumpkin08/10 01:54
Saizani wonder if i can code a phoas HM where the types of the terms get inferred08/10 02:08
dolioThat'd be pretty impressive, but I wouldn't bet on it.08/10 02:15
Saizanyeah, even though i can omit some annotations required in normal Church style for my system F208/10 02:17
-!- Saizan__ is now known as Saizan08/10 07:00
* Saizan wants pattern matching under lambda08/10 07:14
Arnarhey there08/10 13:11
Arnaris there any way the agda parser can parse <x>y into <_>_? I mean, without having all the whitespace in < x > y ?08/10 13:12
byorgeyArnar: how would it know that <x>y should be parsed that way, and not just as a single identifier?08/10 13:17
byorgeyIIUC Agda doesn't make a distinction (like Haskell does) between operator and non-operator symbols.08/10 13:17
Arnarbyorgey: I realize it wouldn't, was just wondering if there was a way to tell it that < and > were operator symbols (should be simple, just a pre-tokenizing step that surrounds them with whitespace)08/10 13:24
byorgeyah, not that I am aware of08/10 13:29
Arnarbyorgey: hmm.. emacs renders zero-width spaces as spaces, but "Word joiner" U+2060 is renderd as a very thin space, if only Agda parsed that as whitespace, code such as I descrbied above might become more readable :)08/10 16:08
byorgeyArnar: heh, that would be super-duper confusing. =)08/10 17:45
--- Day changed Fri Oct 09 2009
-!- opdolio is now known as dolio09/10 02:22
-!- copumpkin is now known as c0w09/10 03:37
doliotwelf is rather different than I was expecting.09/10 03:43
c0whow so?09/10 03:43
dolioWell, it's an implementation of the LF logical framework, which is a dependently typed lambda calculus.09/10 03:44
dolioBut, it doesn't use lambda calculus-like computation.09/10 03:44
dolioInstead, it uses LF for defining term languages, and logic programming with induction over that term structure for computation.09/10 03:45
dolioSo when you define type families 't -> u -> type' it's more like you're defining a, say, lambda prolog predicate of type 't -> u -> o'.09/10 03:46
dolioAt least, from what little I know of lambda prolog.09/10 03:46
c0whmm, /me doesn't know prolog09/10 03:49
c0wI keep meaning to learn it09/10 03:49
-!- c0w is now known as copumpkin09/10 03:49
dolioNot prolog, lambda prolog.09/10 03:49
dolioProlog doesn't have types.09/10 03:49
copumpkinwell, I don't know that one either :)09/10 03:49
dolio:)09/10 03:50
dolioAnyhow, 't -> o' is the type of a unary prediate on ts. Etc.09/10 03:50
dolioAnd, say, plus would have the type 'nat -> nat -> nat -> o'.09/10 03:51
dolioplus(z,n,n). plus(s m,n,s o) :- plus(m,n,o).09/10 03:52
dolioOr something like that.09/10 03:52
dolioo in that second case not being the o the codomain of predicates. I guess prologs usually use uppercase for variables, so...09/10 03:53
dolioplus(s M, N, s O) :- plus(M,N,O).09/10 03:53
faxlambda prolog has higher order unification built into it09/10 03:54
dolioYou'd define addition in about the same way in twelf, although it's primarily a language for describing and proving things about other languages, so maybe you wouldn't worry about that.09/10 03:56
dolioUnless you're formalizing arithmetic.09/10 03:56
-!- elliottt_ is now known as elliottt09/10 18:21
-!- opdolio is now known as dolio09/10 21:06
-!- kosmikus_ is now known as kosmikus09/10 21:49
faxhey dolio09/10 23:32
--- Day changed Sat Oct 10 2009
dolioYes?10/10 00:51
faxhere is a book on predicative arithmetic http://www.math.princeton.edu/~nelson/books/pa.pdf10/10 00:51
dolioDoes it explain where the word "predicative" came from?10/10 00:52
faxnot the etymology no10/10 00:56
dolioAh well.10/10 00:56
dolioSomeone asked me that the other day, and I have no idea what the answer is.10/10 00:56
faxmaybe it comes from early set theory10/10 00:57
-!- opdolio is now known as dolio10/10 08:23
faxhttp://www.cs.chalmers.se/~miquel/lect1.ps -- http://www.cs.chalmers.se/~miquel/lect[234].ps10/10 16:31
faxType Theory: Impredicative Part10/10 16:31
Saizannice10/10 17:15
--- Day changed Sun Oct 11 2009
dolioIs it just me, or are those slide upside-down?11/10 01:00
faxjust you11/10 01:00
faxto me, they are sideways11/10 01:00
dolioHeh.11/10 01:00
-!- koninkje1away is now known as koninkje_away11/10 02:46
-!- Smurfen_ is now known as Smurfen11/10 12:07
--- Log closed Sun Oct 11 17:58:47 2009
--- Log opened Sun Oct 11 18:02:12 2009
-!- Irssi: #agda: Total of 18 nicks [0 ops, 0 halfops, 0 voices, 18 normal]11/10 18:02
-!- Irssi: Join to #agda was synced in 97 secs11/10 18:03
--- Day changed Mon Oct 12 2009
-!- eelco_ is now known as eelco12/10 07:34
-!- pumpkin_ is now known as pumpkin12/10 19:15
-!- pumpkin is now known as copumpkin12/10 21:21
ecstdolio: fwiw, after a break of some weeks i took a closer look at what was causing those agda performance problems with my (partially setoid) category theory constructions12/10 21:26
ecstturned out the problem was indeed eta-expansion of record types12/10 21:27
ecstafter replacing all records with equivalent data definitions and custom eliminators, type checking finally became feasible again12/10 21:28
dolioHuh.12/10 23:30
dolioThe problem with mine ended up being pretty weird.12/10 23:30
ecstfrom the logs i jugde you began coding your own type theory system?12/10 23:34
dolioOh, well, I wrote a type checker/normalizer for pure type systems a while back, so I modified it to support universe polymorphism.12/10 23:36
ecstfrom the logs i jugde you began coding your own type theory system?12/10 23:36
ecstuh, sorry for the double post12/10 23:42
dolio:)12/10 23:42
ecstanyway, now i can typecheck horizontal composition of natural transformations in 10s as opposed to a heap overflow after 10 min12/10 23:43
dolioWow.12/10 23:43
ecsti wonder if it would be hard to hack the agda source to disable eta expansion for record types12/10 23:44
ecstit is a bit awkwards defining all those custom datatypes12/10 23:44
dolioWell, possibly. That could possibly screw up type checking, though.12/10 23:46
dolioAssuming you're proving equalities that rely on eta for records.12/10 23:47
ecstwell, that i would not, of course12/10 23:49
dolioI just mean it might not be easy to avoid that.12/10 23:50
dolioSince you can't inspect records by matching to see if they're equal, like data.12/10 23:50
ecsti am using setoids anyway12/10 23:51
dolioOh right.12/10 23:51
dolioNever mind, then. :)12/10 23:51
ecste. g., natural transformations, which are pseudo-records consisting of a map and a proof of the coherence condition, in the functor category are equivalent, if only their maps are equivalent12/10 23:52
ecstand their maps are equal, if they are extensionally equal12/10 23:52
ecstand so on12/10 23:52
ecstequal -> equivalent12/10 23:52
dolioRight.12/10 23:52
--- Day changed Tue Oct 13 2009
-!- ksf_ is now known as ksf13/10 06:07
-!- kosmikus_ is now known as kosmikus13/10 08:47
-!- Smurfen_ is now known as Smurfen13/10 10:10
-!- opdolio is now known as dolio13/10 11:03
--- Day changed Wed Oct 14 2009
-!- pumpkin is now known as anapumpkin14/10 00:17
-!- anapumpkin is now known as pumpkin14/10 00:52
-!- ksf_ is now known as ksf14/10 06:06
-!- opdolio is now known as dolio14/10 11:20
stevanhi14/10 20:50
kosmikushi stevan14/10 21:17
stevanthis new rewrite construct looks interesting14/10 21:18
faxoh my god! they're adding MORE complications to Agda14/10 21:19
fax'magic with' wasn't bad enough!14/10 21:19
kosmikusyes, I'm a bit sceptic as well14/10 21:20
kosmikusadmittedly looks interesting, but I'm not sure if we need more ad-hoc constructs14/10 21:21
FunctorSaladwhat's new?14/10 21:53
stevanhttp://permalink.gmane.org/gmane.comp.lang.agda/115414/10 21:53
ecstok, now being back to runtime and memory problems (when typechecking setoid composition for comma categories)14/10 22:14
fax`;S14/10 22:15
ecsti know agda uses normalization by evaluation, which automatically generates eta-long forms14/10 22:20
ecstbut i think i do not need eta-expansion for dependent function types at all14/10 22:20
ecsti wonder if there would be a more efficient type checking strategy14/10 22:21
faxecst Coq doesn't have eta-expansion :P14/10 22:21
faxIt's really irritating14/10 22:21
faxit matters to me14/10 22:21
ecstyeah, but i find the impredicative metatheory of coq a bit strange14/10 22:21
faxI would love to find it strange but I still don't understand the meaning of predicativity etc well enough14/10 22:22
faxbeen trying to read a bit into it14/10 22:22
ecstok, i meant not strange but rather constructively less appealing14/10 22:23
faxoh why is that?14/10 22:23
FunctorSaladonly Prop is impredicative in coq14/10 22:28
FunctorSaladSet isn't anymore14/10 22:28
ecstah, that is nice14/10 22:28
ecstfax: for example, you cannot have the (standard) set model in an impredicative calculus14/10 22:29
faxwhat does that mean?14/10 22:29
ecsta model is an assignment of "real" mathematical objects to given syntax14/10 22:30
faxyou mean can't interpret set theory into impredicative?14/10 22:30
faxor interpret the impredicative calculus into set theory?14/10 22:30
FunctorSaladlatter14/10 22:31
faxcurious14/10 22:37
-!- Saizan_ is now known as Saizan14/10 22:46
-!- byorgey_ is now known as byorgey14/10 22:48
--- Day changed Thu Oct 15 2009
-!- codolio is now known as dolio15/10 01:14
-!- FunctorSalad_ is now known as FunctorSalad15/10 12:03
dolioAn impredicative type-level is quite handy when you're working with just lambda terms.15/10 13:20
Saizani guess it let you do things you'd need explicitly recursive types for instead?15/10 13:21
dolioChurch encoding anything bumps it up a level.15/10 13:22
dolioSo, like Bool ends up in Set1, even. And then you can't write "not b = b Bool false true".15/10 13:23
Saizanah, right15/10 13:23
dolioOf course "not b R t f = b R f t" isn't that much worse, but it probably gets worse in general.15/10 13:25
doliohttp://code.haskell.org/~dolio/pts/itower.pts15/10 14:19
dolioWoo!15/10 14:19
byorgeydolio: what's that?15/10 15:07
byorgeyoh, a PTS implementation?15/10 15:08
byorgeyneat.15/10 15:08
--- Day changed Fri Oct 16 2009
-!- eelco_ is now known as eelco16/10 12:24
--- Day changed Sat Oct 17 2009
roconnorcan anyone point me to the syntax for mutually inductive data types (if that is possible)?17/10 00:07
faxmutual17/10 00:08
fax data A ...17/10 00:08
fax data B ...17/10 00:08
faxyou can also have recursive functions in there17/10 00:08
roconnorso Agda has induction recursion?17/10 00:08
fax(ind-rec I mean, as well as non ind-rec)17/10 00:09
faxroconnor,17/10 00:09
faxhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers17/10 00:09
faxlook at the bottom has a nice example17/10 00:09
faxTHE example :P17/10 00:10
roconnorso you don't have to say mutual for mutual data types?17/10 00:12
faxI think you do ?17/10 00:13
roconnorah17/10 00:14
roconnorok17/10 00:14
roconnorshould I install emacs or xemacs?17/10 00:16
faxroconnor17/10 00:17
roconnorhmm, xemacs doesn't appear to be packaged for me, so emacs it is I guess17/10 00:17
faxis this about SillyTree?17/10 00:17
fax:P17/10 00:17
roconnoryes17/10 00:17
roconnorI bet I can do it in Agda17/10 00:18
faxwhat's the value of that17/10 00:18
fax?17/10 00:18
roconnorBut I suppose I should verify this claim17/10 00:18
faxoh right17/10 00:18
roconnorto prove that coq sucks and they should make it better or everyone will move to Agda17/10 00:18
faxyou're kidding?17/10 00:19
roconnoror to prove that Agda is unsound and everyone should move to coq17/10 00:19
faxlol17/10 00:19
roconnorI exagerate17/10 00:19
roconnor*sigh* I have to learn emacs and agda17/10 00:23
faxbtw17/10 00:24
faxInductive SillyTree (p : bool) : Type :=17/10 00:24
fax| leaf : p = true -> SillyTree p17/10 00:24
fax| node : p = false -> forall b, SillyTreePair b -> SillyTree p17/10 00:24
faxwith SillyTreePair (p : bool) : Type :=17/10 00:24
fax| stp : SillyTree p -> SillyTree p -> SillyTreePair p.17/10 00:24
faxmaybe that's not ussble though17/10 00:24
faxI'm ont very sure17/10 00:24
faxlots of subst. needed to use it probablyars17/10 00:25
roconnorer, does Agda not have type families?17/10 00:25
faxroconnor that was Coq :P17/10 00:25
roconnoroh ya, good idea, but doesn't scale to my actual problem unfortunately17/10 00:26
fax:(17/10 00:26
faxAdga has type families17/10 00:27
roconnorI thought so17/10 00:27
roconnordamn it why dosn't this agda mode go17/10 00:27
faxroconnor I don't know a lot about syntax but I'm just curious what you're actually doing ?17/10 00:28
roconnorI'm trying to define the sytax for this logic langauge called Chiron developed for the MathScheme project at McMaster17/10 00:28
roconnorwell define the syntax and semantics17/10 00:28
roconnorstarting with the syntax17/10 00:29
faxdammmn I never heard of this17/10 00:29
roconnorIt is very new17/10 00:29
faxwoow looks really interesting17/10 00:32
faxbest thing to read to start is:  Chiron: A Multi-Paradigm Logic ?17/10 00:33
roconnorprobably17/10 00:33
roconnorit's a bit fuzzy17/10 00:33
roconnorbut maybe I good start17/10 00:34
roconnorFile mode specification error: (file-error "Cannot open load file" "haskell-indent")17/10 00:35
faxwhat's that formal math wiki ?17/10 00:37
faxthe one with your calculator on it17/10 00:37
roconnorI don't know ... mathwiki?17/10 00:37
faxthanks17/10 00:37
Saizan_agda mode requires haskell-indent? weird17/10 00:38
faxGRRR17/10 00:39
faxmathwiki doesn't have agda17/10 00:39
Saizan_or maybe it's something else you've in .emacs?17/10 00:39
roconnorya, that would save me a bunch of trouble17/10 00:39
roconnorSaizan_: I think it requires haskell-indent17/10 00:39
Saizan_"agda-mode setup" made it work out of the box for me, but i had haskell-mode already installed17/10 00:42
roconnorhow did you get haskell-mode installed?17/10 00:43
Saizan_i installed emacs-haskell-mode from my distro17/10 00:44
faxroconnor should probably stop buggin you about this stuff: BUt are you planning on implementing a constructive set theory and then interpreting this language into it?17/10 00:44
roconnoryes17/10 00:44
roconnorer17/10 00:44
roconnorclassical set theory17/10 00:44
Saizan_http://haskell.org/haskellwiki/Haskell-mode <- but you can get it from the repo too17/10 00:45
faxoh use Benjamin Werners work?17/10 00:45
roconnorI have it installed17/10 00:45
roconnorfax: yes17/10 00:45
faxawesome!!!!!!!!!!!!!!17/10 00:45
roconnorbut presumably I have to do something to my .emacs file17/10 00:45
faxroconner danm you get the really interesting stuff to do17/10 00:45
Saizan_that part -> (load "/path/to/haskell-mode/haskell-site-file")17/10 00:45
Saizan_no, wait17/10 00:46
Saizan_well, maybe it's enough17/10 00:46
roconnorugh17/10 00:47
* roconnor searches his nix store for a haskell-site-file17/10 00:47
Saizan_you might also have to add the directory to the load-path with (add-to-list 'load-path "/path/to/haskell-mode/")17/10 00:47
Saizan_(load "haskell-site-file") might be enough, it's in the load-path17/10 00:48
Saizan_and i'd expect a distro package to make it so17/10 00:49
roconnorI've learned not to expect too much from nix yet17/10 00:51
roconnorhmm, somehow I didn't manage to install it17/10 00:52
Saizan_s/it's in the load-path/if it's in the load-path/ -- tbc17/10 00:53
roconnorit is in .nix-profile/share/emacs/site-lisp/17/10 00:53
roconnornow17/10 00:53
Saizan_load it giving the full path then :)17/10 00:55
roconnoroooh, pretty colours17/10 00:56
Saizan_yeah!17/10 00:56
Saizan_and latex-like unicode input17/10 00:56
faxtype theory: Now in glorious technicolor17/10 00:56
Saizan_(there are some shortcuts)17/10 00:56
Saizan_http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput17/10 00:57
roconnorcurly braces for forall?17/10 00:59
faxroconnor so you index by a bool to say if the term contains eval or not?17/10 00:59
Saizan_roconnor: curly braces are for implicit arguments17/10 01:00
roconnorI think it is better to count the evals in some fashion17/10 01:00
Saizan_and forall is for when you don't want to give the type17/10 01:00
faxoh??17/10 01:00
Saizan_i.e forall a -> t, is the same as (a : _) -> t, where _ is filled by inference17/10 01:01
roconnorah needed more spaces17/10 01:01
roconnorheh17/10 01:03
roconnorAgda insists that it knows one of my parameters is true17/10 01:03
roconnordone17/10 01:04
roconnorcomment syntax is like Haskell?17/10 01:05
Saizan_yes17/10 01:05
roconnordoes Agda extract to Haskell?17/10 01:06
Saizan_http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo <- it seems so17/10 01:07
roconnorIt is tempting to do this in Agda17/10 01:08
roconnorit seems much nicer for dependently typed programming than Coq17/10 01:09
faxwell of course ... it has K and eta17/10 01:09
roconnoreven if it didn't have K or eta17/10 01:09
faxit'd be awful if it didn't :P17/10 01:09
roconnorlike how it insisted that my parameter was actually the value true.17/10 01:10
roconnorthat was nice17/10 01:10
Saizan_you mean in coq you don't get refinements when you pattern match on a gadt?17/10 01:10
faxI call it  dependent case analysis17/10 01:11
faxit's basically case but you can fiddle a bit17/10 01:11
faxnot proper pattern matching in any case17/10 01:12
roconnorSaizan_: let me check17/10 01:12
Saizan_fax: uhm, what would be proper pattern matching?17/10 01:13
faxSaizan_: Just like Agda or Epigram17/10 01:13
Saizan_ah, ok, i misread17/10 01:13
faxmaybe I should have said  dependent pattern matching17/10 01:13
roconnorSaizan_: well, coq at least lets me put impossible patterns into my analysis17/10 01:14
roconnorI'm trying to check if it requires me to put in impossible patterns, but I think it does17/10 01:14
roconnorya I think it will17/10 01:15
roconnorbecause nested patterns presumably are translated into nested non-dependent case statement17/10 01:15
faxyou put ()17/10 01:15
roconnorso the dependent parameters are simply generalized away into to new free variables17/10 01:16
roconnorfax: sometimes the depedent types don't allow you to put even ()17/10 01:17
faxoh I don't know exactly the situation you mean17/10 01:17
roconnorfax: and you are forced to instead put in a proof that the case is impossible.17/10 01:17
faxoh right yes17/10 01:17
roconnorFalse_rec (...)17/10 01:17
faxthat is a general theorem though17/10 01:17
faxI mean dependent pattern matching can't always know17/10 01:17
roconnorsure17/10 01:18
roconnorbut intrestingly when Agda does know it makes you17/10 01:18
roconnorfrom my 10 min experience with Agda so far17/10 01:18
Saizan_yup, sometimes you need to put a (), other times you just avoid writing a clause for that case, and "C-c c" on an hole is quite nice, it writes down the valid cases for a variable in the source for you17/10 01:21
roconnorhow do I make a goal?17/10 01:25
Saizan_you put a "?" and reload17/10 01:26
Saizan_where the proof should go17/10 01:27
roconnoroh, maybe that doesn't work for patter17/10 01:27
Saizan_eh, no17/10 01:27
Saizan_only in expressions, afaiu17/10 01:27
roconnorah17/10 01:28
roconnorgetting it now17/10 01:28
roconnorsillyFunction (node true (stp .true leaf leaf)) = true17/10 01:30
roconnorwhat does the . mean in .true ?17/10 01:30
Saizan_mean that it's inferred from the rest of the patterns17/10 01:30
Saizan_s/mean/it means/17/10 01:30
Saizan_i.e, given the other patterns it has to be true17/10 01:31
roconnorwierd17/10 01:31
roconnorheh, I can move the dot around17/10 01:31
roconnorbut I can't remove it17/10 01:31
roconnorI can even dot both trues17/10 01:32
roconnorokay, that was fun17/10 01:32
roconnorCoq sucks17/10 01:32
Saizan_you could declare those arguments as implicit maybe, so they don't have to appear17/10 01:33
roconnorprobably17/10 01:33
faxlol17/10 01:34
Saizan_heh Coq sucks :)17/10 01:34
jlairecan interesting programs, not just proofs, be written in agda? like a compiler for a simple language17/10 01:37
faxjlaire: it's the programs you can write -- the proofs you cant :P17/10 01:38
Saizan_fax: why not?17/10 01:38
faxno tactics make it too difficult17/10 01:38
jlairehmm, ok :P17/10 01:38
Saizan_ah, i guess17/10 01:38
Saizan_there's a separate tool that does proof search, but it's quite new it seems17/10 01:39
roconnorI presumed we were supposed to do all proofs in Adga via reflection17/10 01:39
Saizan_does reflection means "write down the proof terms"?17/10 01:40
faxwell theer is that and there is also some really nice modules for program derivations and equational proofs17/10 01:40
roconnorno it means write a little dsl and write a program to solve your program and then intepret that dsl into your semantic domain17/10 01:41
roconnorsolve your problem17/10 01:41
Saizan_you can also just write your functions as you would in haskell and then prove separate properties about them, but maybe it doesn't scale well that way17/10 01:43
roconnorthat doesn't solve the problem of needing to write proofs in agda17/10 01:43
Saizan_you mean that by reflection you could use agda as a metalanguage to generate the proofs?17/10 01:45
* Saizan_ is quite a noob in all of this17/10 01:45
roconnorthat would be the idea17/10 01:45
roconnorI don't think this is actually done17/10 01:45
Saizan_i'd like to see some examples of that17/10 01:46
roconnorme too17/10 01:46
faxthere's some in the standard library17/10 01:46
roconnorI'd be cool17/10 01:46
faxRing solver or something17/10 01:47
faxit proves stuff like   x + y = y + x17/10 01:47
FunctorSalad /nick SillyTree17/10 05:04
FunctorSalad;)17/10 05:04
copumpkin:o17/10 05:05
-!- opdolio is now known as dolio17/10 06:39
faxweird everyone is using agda these days..17/10 19:58
copumpkin:O17/10 19:59
byorgeycan I call into Haskell libraries from Agda?17/10 20:01
faxyes byorgey17/10 20:01
faxthere is a good example of this,17/10 20:01
faxhttp://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/17/10 20:02
byorgeythanks fax.17/10 20:02
--- Day changed Sun Oct 18 2009
faxis it possible to do PHOAS in Agda 2 now?18/10 01:12
copumpkinwhat's the P?18/10 01:13
faxhttp://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf18/10 01:13
copumpkinthat name sounds familiar18/10 01:13
copumpkinisn't he smerdyakov or something?18/10 01:13
faxhas anyone done this in Agda?18/10 01:13
faxdammit why the hell can't I use ∀ :/18/10 02:12
FunctorSalad18/10 02:13
Saizan_fax: i've done the predicative System F in that style18/10 02:30
faxcool what did you do with it?18/10 02:30
Saizan_nothing :D18/10 02:30
faxcan you post it please?18/10 02:31
Saizan_k18/10 02:31
Saizan_it's a bit messy maybe: http://code.haskell.org/~Saizan/SystemFpred.agda18/10 02:33
faxI wrote this much btw http://pastie.org/65914318/10 02:33
Saizan_i managed to write the interpretation into agda types18/10 02:34
faxwell you have proved strong normalization of F :P18/10 02:34
Saizan_heh18/10 02:34
Saizan_yeah :)18/10 02:35
Saizan_i had to use cast/cast' as a way to avoid an extensionality axiom18/10 02:35
Saizan_it'd be nice if we could find a cleaner way18/10 02:35
Saizan_oh, also "inj" is something i'd like to avoid18/10 02:36
faxhuuughhh18/10 02:36
faxI have to install the agda lib18/10 02:36
Saizan_well, you can define the standard Boolean and equality types instead18/10 02:37
Saizan_and T18/10 02:37
Saizan_it's not hard to install the lib though :)18/10 02:38
Saizan_i've found it horrible that type application requires those huge proof terms like in appflip, i might be missing a way to generate/infer them, i hope18/10 02:41
-!- pumpkin is now known as copumpkin18/10 04:44
-!- opdolio is now known as dolio18/10 09:29
-!- Saizan_ is now known as Saizan18/10 09:54
-!- opdolio is now known as dolio18/10 19:58
colin_I just started looking at agda today. I cannot get emacs to find Data.Nat. It says: Failed to find source of module Data.Nat in any of the following18/10 20:35
colin_locations: ~/lib-0.2/src/Data/Nat.agda ~/lib-0.2/src/Data/Nat.lagda18/10 20:35
faxhave you downloaded the standard library?18/10 20:35
colin_but if I do: less ~/lib-0.2/src/Data I can see Nat.agda . Is this a known problem?18/10 20:36
colin_yes18/10 20:36
faxtry expanding the ~18/10 20:36
colin_Hm. That's an improvement. Now it just complains Nat is not in scope.18/10 20:38
colin_I'm working through "Dependently Typed Programming in Agda". Is this pre-agda2?18/10 20:40
faxno18/10 20:41
colin_Hm. It mentions the summer school library module Data.Nat. Perhaps the standard library has changed since then?18/10 20:42
faxohh18/10 20:42
faxI think they changed to use ? instead of Nat18/10 20:42
colin_I'll browse the source18/10 20:42
FunctorSalad18/10 20:42
colin_Thanks FunctorSalad - that does the trick18/10 20:43
faxnobody got my joke -_-18/10 20:43
colin_Is that supposed to pun a face with an infix underscore operator?18/10 20:44
--- Day changed Mon Oct 19 2009
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=10903#a1090319/10 04:31
* dolio goes to get some much-needed sleep.19/10 04:32
colin_I'm trying to do an example from "Dependently typed programming in Agda" and I'm getting lost with an error message.19/10 14:41
copumpkinwhat's the message?19/10 14:41
colin_Failed to infer the value of dotted pattern when checking the pattern .n has type \Bbb{N}19/10 14:42
colin_Well, it didn't say \Bbb{N}19/10 14:42
colin_I'm trying to do exercise 3.119/10 14:50
colin_Is there a way I can post my attempt so far, so someone can explain what I'm doing wrong?19/10 14:51
colin_Perhaps i should try joinging the mailing list, and ask there?19/10 14:54
jlaireuse hpaste.org19/10 14:55
colin_http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10913#a1091319/10 14:57
doliocolin_: I think those should be ".(n + suc k)" based on the constructors of Compare.19/10 15:12
dolioAlso, you need an n that isn't dotted in each case, I believe.19/10 15:13
colin_Thanks dolio - I understand now, and I have got it pass the type checker.19/10 15:16
dolioSince a .e that contains a variable is expected to have that variable matched elsewhere.19/10 15:16
colin_How do I write a main function to print a Nat to stdout?19/10 16:54
colin_I'm trying to co,pile the example hello world fragment in chapter 4 of "Dependently Typed Programming in Agda". That chapter says the type of main has to be IO Unit, but the type checker only seems to accept IO \top. Furthermore, the compiler complains that the type of main should be .IO.Primitive.IO A for some A. What do I need to do?19/10 19:41
pumpkinI vaguely remember that there are two IOs19/10 19:42
colin_If I import IO.Primitive instead of IO, then it doesn't type check.19/10 19:45
colin_It turns out I can get it to work if I DON'T import IO or anything else, and just put in all the directives myself (it actually does this in the tutorial, but I tried to be too clever :-(19/10 19:53
colin_I'd like to know how to use the IO standard library instead.19/10 19:53
pumpkinI do remember having the same problem as you, but can't remember what to do to fix it19/10 19:53
colin_Oh well, I'll learn - slowly.19/10 19:56
-!- English_Gent is now known as EnglishGent19/10 20:35
dolioSo, what do we think about types like { i : Level, A : Type[i] | A }?19/10 20:51
faxI am not sure what that syntax is supposed to mean19/10 20:53
faxsomething like { i : Level | { A : Type[i] | A } } ?19/10 20:53
dolioYeah, right-nested dependent sum.19/10 20:54
faxso you must have cumulativity for that type to be inhabited?19/10 20:54
dolioWhat do you mean by that?19/10 20:56
faxoh no I am talking nonsense19/10 20:56
faxsorry yeah I understand the type now: shouldn't it be a type error?19/10 20:57
faxoh, actually Type[i] : Type[i+1]19/10 20:57
fax{ i : Level | { A : Type[i] | A } } : Type[?]19/10 20:57
dolioIts type is Type[omega], which is outside the quantification power of Level.19/10 20:58
faxare you allowed to do that? :P19/10 20:58
dolioThat's how I've been typing Pi types like '(i : Level) -> Type[i]' as well.19/10 20:58
dolioThere's one extra level above the predicative hierarchy, kind of like box in the CoC.19/10 20:59
dolioSo I thought: why not have it for strong sums, too?19/10 20:59
faxsounds a bit scary19/10 21:00
dolio{ i : Level | { A : Type[i] | A } } is roughly the disjoint union of all types except Type[omega], I think.19/10 21:00
dolioYeah, it does sound scary. :)19/10 21:01
dolioFor instance, skimping on the notation (which is really verbose for dependent tuples)...19/10 21:04
dolio< 0, List Nat, [1,2,3] > is an element.19/10 21:04
dolioAnd < 1, List Type[0], [Nat, List Nat, List (List Nat) ] >19/10 21:05
--- Day changed Tue Oct 20 2009
-!- RichardO_ is now known as RichardO20/10 06:50
montes89i'm having some trubles solving a problem im having can anyone help?20/10 07:57
montes89is anyone on here?20/10 07:57
copumpkinlet's hear the question :)20/10 07:57
montes89Let F:B->C and G:A->B be functions20/10 07:58
montes89prove that if F is injective and G is injective then F o G is Injective20/10 07:58
montes89any idea?20/10 07:58
montes89So far i got20/10 07:58
montes89(F o G)(X)=F(G(x))20/10 07:59
montes89(F o G)(X1) isn't equal to (F o G)(x2)20/10 07:59
montes89cause X1,X2 are elements of A: X1 isn't equal to X2,  F(x1) isn't equal to F(x2)20/10 08:01
montes89am i on somewhat the right track?20/10 08:01
copumpkinI'd talk about G independently, show that it generates non-equal elements of B given unequal elements of A, and then use those unequal elements of B to make unequal elements of C, if that makes any sense20/10 08:04
copumpkin...20/10 08:04
Saizanthere's an Injective in the standard libraries?20/10 08:19
copumpkinnope, but I gotta say, that's a pretty trivial proof20/10 08:20
copumpkinunless I messed something up20/10 08:20
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=10934#a1093420/10 08:23
copumpkinI guess it is20/10 08:23
-!- eelco_ is now known as eelco20/10 10:08
faxhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=10934#a1093420/10 16:31
faxthat's very nice20/10 16:31
pumpkinfax: thank you!20/10 17:06
dolioThat's an unusual definition of Injective.20/10 17:15
faxI don't think injective is worthwhile in constructive math20/10 17:21
dolioYou mean the idea in general, or that formulation.20/10 17:22
faxas a general concept20/10 17:22
fax(do prove me wrong :P)20/10 17:25
dolioWell, I have no idea.20/10 17:25
dolioI do know that you'd usually use f x == f y -> x == y, though, since that can get you the negated version, but the negated version can't get you back the non-negated version.20/10 17:26
dolioOnly a doubly-negated version.20/10 17:26
pumpkinaha20/10 17:26
pumpkinthat makes sense20/10 17:26
faxwe don't get f^-1 from a (f x == f y -> x == y) proof though20/10 17:26
pumpkinI was debating which of the two to use and the one I wrote seemed to fit what the original dude was asking20/10 17:27
pumpkinI started writing it for him but then he disappeared20/10 17:27
doliohttp://code.haskell.org/~dolio/agda-share/injective/html/Functional.html20/10 17:28
pumpkinzomg20/10 17:29
pumpkinwhatever I do dolio has already done!20/10 17:29
pumpkin(and better)20/10 17:30
dolioHeh. I did that in response to some blog post by someone a while back.20/10 17:30
dolioThat's how I discovered that all functions were provably injective in agda at the time.20/10 17:30
pumpkinoh :)20/10 17:30
faxhm20/10 17:41
faxcan you actually prove something injective without producing an inverse function??20/10 17:46
fax(yes)20/10 17:48
faxI wonder what they do in constructive category theory20/10 18:01
fax(partial setoids)20/10 18:06
copumpkinzomg I proved composition of injectiveness dolio's way too!20/10 20:09
copumpkinso l33t20/10 20:09
copumpkin(I need to prove simple things because I'm incapable of proving more complicated ones)20/10 20:11
faxwhat?20/10 20:12
copumpkinI proved composition of injective functions is injective the other way around too20/10 20:13
copumpkintotally uninteresting20/10 20:13
faxhey that's interesting someones using Injective on the agda mailing list20/10 20:16
faxI wonder whey because I can do the proof about ++ assoc without injectivity20/10 20:19
faxwould be interesting to see the actual usage20/10 20:19
copumpkinif I have x -> y, and I have ¬ y, how can I get to ¬ x?20/10 20:28
copumpkinoh wait, I think I know20/10 20:29
copumpkinthere we go20/10 20:31
copumpkinwhat are some other simple statements I can prove?20/10 20:36
faxI don't think there's any point in proving simple statements20/10 20:38
faxpick an interesting non-trivial proof to do and there will be lots of drugdery to go along with the interesting proofs20/10 20:39
copumpkinthe point would be "getting a feeling" for it, really. I'm still at the point where I rejoice if my code typechecks20/10 20:40
copumpkinany suggestions for interesting non-trivial proofs then?20/10 20:40
faxwe all are :D20/10 20:40
copumpkinwell, I rejoice when my injectivity proof typechecks :P20/10 20:40
doliocopumpkin: Isn't the proof of composition of injectiveness for my definition of injective about the same as the one you originally used?20/10 20:47
dolioJust compose the proofs?20/10 20:47
copumpkinalmost identical :P20/10 20:47
copumpkinyeah20/10 20:47
copumpkinhrrmpf, belittle me all you want!20/10 20:47
dolioHeh.20/10 20:48
copumpkinI also converted from your definition of injectivity to the other one I used20/10 20:48
faxdo you know any uses of injectivity in type theory?20/10 20:49
copumpkinnot me, I'm a layperson20/10 20:49
dolioInjectivity of constructors is occasionally useful for fiddling around with equalities.20/10 20:50
dolioLike 's m == s n -> m == n' or 'x :: xs == y :: ys -> (x == y) * (xs == ys)'.20/10 20:50
faxI mean proofs of  f x = f y -> x = y20/10 20:50
dolioThose are proofs of that. Just that f is a constructor.20/10 20:51
dolioI know I've used those two above before.20/10 20:52
copumpkinparthian shot!20/10 20:52
doliohttp://code.haskell.org/~dolio/agda-share/sorting/html/Natural.html20/10 20:53
dolioThere, that uses injectivity of succ to prove that succ respects inequality.20/10 20:54
dolioOnly I called it ==-pred instead of succ-injective.20/10 20:54
dolioThere are similar theorems in the vector module, only I called them ==-head and ==-tail.20/10 20:56
faxWhat I am trying to say is that I think there isn't much theory about injective functions like there is in category theory or set theory20/10 21:01
dolioWell, that may be. I can't say I've had much use for injectivity of arbitrary functions.20/10 21:03
dolioThe use of Injective in those mailing list posts is probably to be used with (type) constructors.20/10 21:05
copumpkindid anyone recognize the original guy asking the question in here?20/10 21:05
copumpkinmontes8920/10 21:05
dolioNope.20/10 21:06
faxI wonder if that's being taken as an axiom :|20/10 21:06
faxto prove type constructor injectivity is quite involved20/10 21:06
fax(for each specific case...)20/10 21:07
fax(in general it doesn't hold)20/10 21:07
dolioI'm pretty sure Agda just gives it to you.20/10 21:08
dolioBoth type and value constructors are just defined to be injective.20/10 21:08
faxheh it does20/10 21:10
faxthat's bizarre20/10 21:10
fax(well it's derivible in general for constructors given K but doesn't make sense for type constructors)20/10 21:11
faxcan you prove pigeonhole from Fin injectivity?20/10 21:14
copumpkinif I wrote ackermann in agda, it would be pink, right?20/10 21:21
faxno20/10 21:21
dolioThat might depend on how you write it.20/10 21:21
dolioWith higher-order functions, ackermann is primitive recursive, though.20/10 21:22
copumpkinoh20/10 21:22
copumpkinI see20/10 21:22
copumpkinthat higher-order form is so much more elegant than the other form I saw20/10 21:23
faxI'm kind of annoyed at the phoas syntax for sys F20/10 23:13
faxI don't like the relation20/10 23:14
fax(used for type application)20/10 23:14
--- Day changed Wed Oct 21 2009
faxJames Chapman defines everything mutually21/10 01:21
faxsyntax, context etc.. and the congurences are mutually defined too21/10 01:21
dolioWild.21/10 01:25
dolioI'm not really familiar with the issues that keep everything from being mutual in Agda and such.21/10 01:26
faxwell it works.. I can't decide if that's what I should do too21/10 01:26
dolioI seem to recall augustss being pro- everything being mutual, but Ulf had some reasons for not wanting that.21/10 01:27
faxoh he's got a new paper! http://cs.ioc.ee/~james/PUBLICATION_files/Relative_Monads.pdf21/10 01:29
faxnot read it yet21/10 01:29
dolioI still need to read his thesis so I can rewrite my type theory in Agda. :)21/10 01:29
dolioThen we'll know it doesn't cause non-termination.21/10 01:29
faxhttp://cs.ioc.ee/~james/PUBLICATION.html21/10 01:29
faxBig step normalisation might be worth reading first21/10 01:30
dolioI actually have two copies of his thesis somehow.21/10 01:30
dolioI named one with an 's', and one with a 'z'.21/10 01:30
fax:S21/10 01:31
fax(See also Piponi [7] for this and other interesting uses of vector spaces in functional programming.)21/10 01:31
faxheh just watched his talk the other day21/10 01:32
faxway over my head21/10 01:38
faxthat paper about relative monads21/10 01:38
dolioI suspect it's rather over my head, too. I'm not that well versed in the actual mathematical end of monads.21/10 01:43
dolioI couldn't tell you what the Eilenberg-Moore category is, other than it has to do with algebras.21/10 01:43
-!- opdolio is now known as dolio21/10 15:20
-!- copumpkin is now known as TheHunter21/10 18:16
-!- TheHunter is now known as copumpkin21/10 18:16
--- Day changed Thu Oct 22 2009
colin__I attempted to subscribe to the mailing list on Monday. Still no confirmation from the moderator. Is this normal?22/10 12:38
jlaireI had no problems subscribing a couple of weeks ago22/10 12:40
--- Day changed Fri Oct 23 2009
colin_I'm getting an error message that doesn't seem right to me:23/10 11:24
colin_IO \top !=< Set1 when checking that the exporession putStrLn "Hello World!" has type Set123/10 11:24
colin_IO has type Set -> Set1 and \top has type Set so i don't see the problem.23/10 11:25
Saizanif (putStrLn "Hello World!" : IO \top) it can't also have type Set123/10 11:44
Saizanit seems like you're using "putStrLn "Hello World!"" as a type somewhere23/10 11:45
colin_I'm trying to sequence two such calls in a row, using >>, but I can't get it right.23/10 11:53
colin_My attempt is here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11091#a1109123/10 12:02
Saizani think you've to use ♯₁ instead of ∞₁ there23/10 12:21
Saizanthe former is the value constructor for the latter family23/10 12:21
Saizani've never used IO, but this one typechecks http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11091#a1109223/10 12:23
-!- opdolio is now known as dolio23/10 16:35
roconnorhow do I do coq-section like stuff?  Do I use let?23/10 19:58
dolioLocal module?23/10 19:58
dolioI'm not sure what all sections get for you, though.23/10 19:59
roconnorin coq I declaire a series of variables and hypothesis23/10 20:00
roconnorwhich I get to use in my definitions23/10 20:00
roconnorthen when I close my section these definition are automagically parameterized by those variables and hypothesis23/10 20:01
dolioI think you could do that by parameterizing the module by those.23/10 20:01
dolioOpening a module without supplying the parameters brings the things inside into scope parameterized by the module's parameters.23/10 20:03
roconnorhow do I make a hole?23/10 20:10
dolioHole?23/10 20:10
dolio? perhaps, if that's what you mean.23/10 20:11
roconnorah ?23/10 20:11
roconnoryes23/10 20:11
dolio{! !} might also work, but why would you type all that?23/10 20:11
roconnorAgda doesn't seem to like my nested recursion definition either23/10 20:21
dolioI'd have to see it to comment.23/10 20:24
roconnorwhat's the usual paste site people use here?23/10 20:25
doliohpaste :)23/10 20:25
roconnorhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11098#a1109823/10 20:27
dolioHmm, yeah.23/10 20:33
dolioI don't know much about the termination checker, to be honest.23/10 20:33
roconnorI'm not sure if the simpler nested recursion problem works.23/10 20:33
dolioIt works if you define Z in a where clause.23/10 20:34
dolioNot parameterized by treeInd.23/10 20:34
roconnoroh, you have to do that?23/10 20:34
dolioJust using it.23/10 20:34
roconnorooh23/10 20:35
roconnornice23/10 20:36
roconnorI guess Z is out of scope23/10 20:36
roconnorbut still, not bad.23/10 20:36
dolioYou might be able to define them together in a mutual block, too.23/10 20:38
dolioIf you want both in scope.23/10 20:38
roconnorcertainly better than I can do in Coq at the moment23/10 20:38
roconnoryep, mutual seems to work23/10 20:39
roconnorI wonder if Agda catches Burnos non-terminating example.23/10 20:39
roconnoris Agda impredicative?23/10 20:40
dolioI think the "Z treeInd y y'" isnt' obviously structurally recursive, though, so it doesn't do any additional work.23/10 20:40
dolioNo.23/10 20:40
roconnorwell, that rules out even stating Bruno's example :)23/10 20:40
dolioThere's a --type-in-type flag, but of course, that's inconsistent. :)23/10 20:41
roconnordolio: I'm not sure I understood your structural recursive comment23/10 20:41
roconnorah23/10 20:41
roconnorin Coq, reduction will occur (and has to) before guards are checked23/10 20:42
roconnorso the Z gets inlined and reduced and the treeInd now appears applied to structurally smaller elements and it is happy.23/10 20:42
roconnorat least in the simple 1 list parameter nested fixpoint case23/10 20:43
roconnorI can't get this 2 list parameter example to work in Coq yet23/10 20:43
dolioWell, even without the module, it doesn't seem to do any of that sort of inlining. I guess the termination checker doesn't handle that kind of higher-order situation.23/10 20:47
dolioI think there's been talk of rewriting it.23/10 20:50
roconnordolio: that seems strange.  I sort of thought it was essential to do reduction before checking guardedness23/10 21:02
roconnorit seems a bit odd to have two converable terms where one passes the checker but the other one does not23/10 21:03
roconnorit seems like that would cause problems23/10 21:03
dolioYeah, as I said, I don't really know how it works.23/10 21:03
dolioI mean, it must do some reduction to be able to see that it works with the where/mutual case.23/10 21:04
dolioI suppose it might just track the size of arguments through function calls.23/10 21:10
HairyDudethere don't seem to be any notes on the wiki about how to install the emacs mode, especially after installing from hackage23/10 23:45
Laneyagda-mode setup23/10 23:45
HairyDudeaha, thanks23/10 23:52
--- Day changed Sat Oct 24 2009
HairyDudeok, apparently emacs can't find the agda-mode executable, and ~/.cabal/bin being in both .bashrc and emacs's load-path doesn't help24/10 00:09
HairyDuderight, have to setenv "PATH" in .emacs to add agda-mode's location.24/10 00:30
-!- koninkje_away is now known as koninkje24/10 02:54
-!- Saizan_ is now known as Saizan24/10 15:58
-!- opdolio is now known as dolio24/10 21:13
--- Day changed Sun Oct 25 2009
faxno news with epigram since that short spell :(25/10 20:47
edwinbNot much has happened, alas25/10 20:48
edwinbConor's teaching, others have been doing their own thing...25/10 20:48
edwinbI expect there'll be another spurt soon enough25/10 20:49
faxI need to think up something to do25/10 20:49
faxhey edwinb so what are you working on ? :)25/10 20:50
faxany cool new Idris stuff or what25/10 20:51
edwinbI'm just writing some slides about it now25/10 20:51
edwinbfor a talk tomorrow aimed at newcomers to dependent types25/10 20:51
edwinbI've been trying to make it efficient, which is always entertaining25/10 20:51
faxspreading the good word!25/10 20:52
edwinbindeed25/10 20:52
* edwinb idly wonders if he knows who fax is25/10 20:52
faxnah I'm just kid25/10 20:52
edwinbheh25/10 20:52
faxI don't study any of this stuff (yet?)25/10 20:52
edwinbundergrad?25/10 20:52
faxyeah25/10 20:52
edwinbIt's good to have interested undergrads, certainly!25/10 20:53
faxall the good stuff is drying out like fplunch and so on -_-25/10 21:21
kippetjeGood evening, I just downloaded and installed Agda2, I started the emacs editor which came with it and opened a file containing agda code. Now I would like to compile (or load, whatever is needed) this and test it like I would do with Haskell: ghci file.hs and then call the specific function with it's parameters. How do you do that in the agda emacs?25/10 23:18
copumpkinyou actually want to run code?25/10 23:18
copumpkinthere's an evaluate menu item I believe25/10 23:18
SaizanISTR a repl too25/10 23:21
Laney"unsupported"25/10 23:21
copumpkinkippetje: what do you plan to do with it? most of the time you'll just want C-c C-l25/10 23:22
kippetjeI know, but I have a piece of code which I do not understand, so I split it up in several pieces and I want to test each part to see what it exactly does.25/10 23:25
kippetjebut i guess ill try to make it haskell code and do it in haskell, emacs is too complicated25/10 23:26
dolioC-c C-n can normalize things.25/10 23:28
faxkippetje what's complicated?25/10 23:30
faxkippetje well if you show the code maybe it can be explained25/10 23:30
kippetjeI already made it haskell which im looking at now :)25/10 23:35
faxhow?25/10 23:36
kippetjeIts just a simple function nothing special with types, just bool and nat25/10 23:36
faxwhat about that isn't clear?25/10 23:37
faxuse what dolio said to find out values it gives for particular input25/10 23:38
kippetjewhen i do that it gives "compile error:" and nothing more25/10 23:38
faxmake sure your file loaded correctly first25/10 23:38
copumpkinwe'd be happy to try to explain some code to you if you have any specific questions, too25/10 23:38
roconnor<copumpkin> you actually want to run code?25/10 23:38
roconnorthis made me laugh out loud25/10 23:39
copumpkin:)25/10 23:39
kippetjeI know you can help, but i think i got it figured out now :)25/10 23:39
* Saizan wonders if someone has formalized basic probability theory in agda25/10 23:40
copumpkinSaizan: given the lack of anything useful in the Rational module in the standard library, I doubt anyone's tried yet :)25/10 23:41
copumpkinbut maybe25/10 23:41
faxkippetje: (I got this feeling like converting to haskell to understand is a bad idea for a few different reasons)25/10 23:41
dolioroconnor: Who runs code anymore? Except inasmuch as type checking involves running code. :)25/10 23:41
copumpkinit's the ultimate laziness25/10 23:42
copumpkinI know my answer is right, but don't need it right now25/10 23:42
Saizancopumpkin: heh, i'm not even sure if Rationals would be sufficient to start or i'd need Reals25/10 23:43
copumpkinSaizan: yeah, depends what you're after really... it'd be nice to get reals into agda thouh25/10 23:43
roconnorSaizan: you probably need integration, which mean reals25/10 23:43
Saizanwell, i'm after something i can do my prob. theory exercises in :)25/10 23:44
Saizanif i want to cover continuous variables i'd need integration, yeah25/10 23:44
* copumpkin got all excited about porting roconnor's reals from coq to agda, but then I saw something shiny and went and did something else25/10 23:45
faxSaizan you are aware that formal math is a billion times harder than doing it on paper? :)25/10 23:47
Saizanlike fixing the rationals?25/10 23:47
faxSaizan just incase you hadn't noticed ...25/10 23:47
copumpkinSaizan: for a while that too, but then I saw something else shiny :)25/10 23:47
roconnorit's only on the order of 10x harder25/10 23:47
Saizanfax: i wasn't aware of the scale factor :)25/10 23:47
roconnormaybe 100x harder for beginners25/10 23:47
copumpkinfax: has anyone proved that multiplier?25/10 23:47
dolioOne-jillion times harder!25/10 23:48
copumpkindamn25/10 23:48
doliohttp://code.haskell.org/~dolio/agda-share/html/ExistentialCoinduction.html25/10 23:50
Saizan(my problem with probability is that i struggle to not see it as a bunch of distinct cases, i was hoping the connections would be clearer in code)25/10 23:51
--- Day changed Mon Oct 26 2009
-!- opdolio is now known as dolio26/10 01:12
-!- seanmcl_ is now known as seanmcl26/10 15:58
dolioHuh, Agda blows up on the last part of James Chapman's simply typed SK normalizer.26/10 20:49
dolioOh, I missed some dots, apparently.26/10 21:07
--- Day changed Tue Oct 27 2009
dolioThe code at the end of this thesis is lying to me.27/10 00:04
copumpkingive it some truth serum27/10 00:04
dolioIn any case, I have one simply typed SK normalizer, minus a soundness theorem.27/10 00:06
dolioS = lam (lam (lam ((∅ [ ↑ _ ] [ ↑ _ ]) $ ∅ $ ((∅ [ ↑ _ ]) $ ∅))))27/10 01:14
-!- opdolio is now known as dolio27/10 03:27
-!- opdolio is now known as dolio27/10 06:33
Arnarhey27/10 16:43
ArnarI'm getting something from Agda.. ehrm.. which I don't know if it is an error or not27/10 16:43
Arnarcannot post the code as it is a solution to an ongoing exam.. but I get a bunch of _51 : Set, _52 : Some type ... messages in the information buffer, and one recursive call in my code (which looks correct) is highlighted in yellow27/10 16:45
Arnarwhat does this mean?27/10 16:45
Saizan_it means it couldn't infer some of the types27/10 16:45
Saizan_try making implicit arguments explicit on that call27/10 16:46
Saizan_the _N are metavariables the the type checker couldn't resolve27/10 16:46
Arnaraha27/10 16:47
Arnarhang on27/10 16:47
Arnarright.. works if I make everything explicit27/10 16:48
Saizan_you can put {_} as arguments and reload, it'll hilight in yellow only the problematic ones27/10 16:48
ArnarI did have implicit arguments in the definitions..27/10 16:48
Arnarbut it wasn't highlighting any of them27/10 16:48
Arnaroh wait27/10 16:48
ArnarI need to pass the implicit args in the recursive call I guess27/10 16:48
Saizan_you use foo {a} to pass a as an implicit argument to foo27/10 16:49
Arnarah yes27/10 16:49
ArnarSaizan_: thanks..27/10 16:49
Saizan_np27/10 16:49
ArnarI was actually pattern matching on an implicit Nat argument27/10 16:49
Arnarhad to pass it to the recursive call27/10 16:49
Saizan_well, that depends on the shape of the other arguments, however it's not unusual27/10 16:51
stepcutwould Agda be suitable for solving/creating a proof for this problem, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11217#a1121727/10 20:00
copumpkinit's be rather painful for now27/10 20:01
stepcutor do I need something more specialized/different ?27/10 20:01
stepcutso far everything is painful for me in Agda :)27/10 20:01
stepcutwould Coq be any better?27/10 20:01
faxstepcut what is it???27/10 20:01
faxLots of 40 components each are called acceptable if they contain no more than 3 defectives.27/10 20:01
faxThe procedure for sampling the lot is to select 5 components at random and to reject the lot if a defective is found.27/10 20:01
faxWhat is the probability that exactly 1 defective is found in the sample if there are 3 defectives in the entire lot27/10 20:01
stepcutjust a simple probability question...27/10 20:02
faxwell I can't read all that but why donot you just compute it in a thingy like maxima?27/10 20:02
faxdid you want a certified program to compute it?27/10 20:02
stepcutyeah.. I want some sort of 'proof' that I did it right...27/10 20:03
stepcutmostly trying to get more experience with proofs27/10 20:03
stepcutthough maybe that is not the type of thing you prove?27/10 20:03
faxI don't do probability theory :P27/10 20:05
stepcutme neither. I had to take that class twice...27/10 20:05
faxCoq has computable real lib (thanks to roconnor) and theory of integration etc27/10 20:05
stepcuthence my desire for a stronger assertion of correctness ;)27/10 20:05
faxif you can't prove it on paper you can't prove it formally27/10 20:05
faxI mean it's a LOT harder inside the computer27/10 20:06
stepcutyeah, I have noticed that27/10 20:06
faxit is surely to do with the subject being in infancy27/10 20:06
fax(and all of us beginners etc)27/10 20:06
stepcutoh well, I'll look it up in my book. I remember they were always talking about things such as, You have 4 blue balls and 3 red balls, what are the odds of drawing exactly 2 red balls.27/10 20:07
stepcutSeems like the same problem but with defective/non-defective parts27/10 20:07
stepcutI once saw an interesting presentation which claimed that the (pre-college) math education system was all wrong. The whole thing leads up to learning calculus, which no one uses much in daily life, and that it should lead up to learn probability -- which is a lot more useful in daily life...27/10 20:09
fax????27/10 20:10
faxcalculus is the most practical mathematics  other than sumsing and timesing27/10 20:10
stepcutpractical in what way?27/10 20:11
faxnobody turns real life situations into probability theory, we fly by intuition - that doesn't make sense27/10 20:11
stepcutthat's because most people don't know probabity theory ;)27/10 20:11
faxstepcut people that balance poles on the nose and juggle don't know control theory :P27/10 20:14
stepcut:p27/10 20:15
fax(some of them might.. but anyway, they aren't (conciously) approximation solustions to the ODE for inverted pendulum)27/10 20:16
stepcutbut imagine if they *were*! But you didn't think of that!27/10 20:16
stepcutok, the first step is to prove the Basic Counting Principle27/10 20:26
dolioYes, but if you 'prove' it on paper, you won't know whether you're proof is right. That's the frustrating thing about paper.27/10 20:27
copumpkinzomg27/10 20:27
faxdolio I don't find that true in general...27/10 20:27
faxsort of  the fundamental thing about mathematics?27/10 20:28
dolioWell, I think it's true when you're a neophyte at the subject.27/10 20:28
dolioI remember proving things for homework early during an abstract algebra course where I wasn't really confident with what I'd written down.27/10 20:29
faxoh sure I agree27/10 20:29
faxwell the whole structure of mathematical education is based on not understanding anything you do27/10 20:29
faxthat's quite possible to combat though27/10 20:29
dolioOn a tangent, have you read James Chapman's thesis yet?27/10 20:30
faxyes27/10 20:30
dolioI'm not sure what to think about the dependently typed normalizer.27/10 20:31
faxwhy?27/10 20:32
faxwhat abot it?27/10 20:32
dolioIt seems like the goal is to show that normalization of the object language is terminating if it's well typed in the logical framework.27/10 20:32
faxdolio I find his technique in general very elaborate:   I think that is why he does the smaller case studies though27/10 20:32
dolioBut, that doesn't tell you whether being well typed in the object language confers the same property. You'd have to show that every object-well-typed term is LF-well-typed.27/10 20:32
faxI don't beleive you need to say "if it's well typed" since every syntax is well typed by construction27/10 20:32
faxisn't it?27/10 20:33
dolioIt's well typed in the LF by construction, yes.27/10 20:33
dolioI guess the same can be said of Luo's UTT.27/10 20:35
faxno  ??27/10 20:35
dolioYou have to show that there's a translation from your language into the language encoded in LF, if your original concept of your language isn't embedded in the LF.27/10 20:35
dolioWhich may be easier than proving normalization directly.27/10 20:36
dolioI guess that's what the twelf folks call "adequacy".27/10 20:36
faxdolio I think I better re-read it to be follow you properly27/10 20:38
faxyou mean the stuff in Chapter 5 - Dependently typed λ-calculi?27/10 20:38
dolioYeah.27/10 20:38
stepcutok. The fundamental princple of counting is that if event 1 has m possible outcomes, and event 2 has n possible outcomes, then together they have m*n possible outcomes. The proofs I have seen so far are 'graphical', such as a graph, like, http://www.aaamath.com/g5-sta-basic-cntg.htm27/10 20:39
stepcutsurely I can prove this in Agda?27/10 20:40
doliofax: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11218#a11218 <-- there's an incomplete encoding of my language with universe polymorphism in his style, I think.27/10 20:41
stepcutI've also seen the proof done as 2 dimensional array of tuples27/10 20:41
dolioYou'd need some kind of axioms of probability, at least.27/10 20:49
faxdolio: I'm not understanding your statements about LF and such27/10 20:51
stepcutseems I also need to rebuild agda against a newer libffi :-/27/10 20:51
faxdolio: I've not understood what you say about LF and so forth27/10 20:56
dolioLF is a dependently typed lambda calculus used as a meta-language for defining object languages.27/10 20:57
dolioWhere the object language is the language you want to actually work in.27/10 20:58
faxyes but are you calling Agda LF?27/10 20:58
dolioNo. Chapman defines models the LF in Agda, and the object language in the LF at the same time, sort of.27/10 21:00
faxI didn't notice that :S27/10 21:00
dolioHis Type type is the type of LF types.27/10 21:00
dolioOr, in Twelf they call them kinds, I think, to keep from getting confused.27/10 21:01
dolioSo, U is a kind, the kind of names of types. Then, if s : U, El(s) is a kind, the kind of values of s. Or something like that.27/10 21:02
dolioAnd there are meta-level pi types, too.27/10 21:03
dolioThen you define your object language by listing things that are in U, and El(s) and so on.27/10 21:04
dolioSo for just a vanilla logical framework, you'd have U, El, Pi (meta) and lambda in the terms, I think (plus whatever coercion stuff he needs for proving things).27/10 21:06
dolioOh, and application.27/10 21:07
faxyou said   the object language *in* the LF27/10 21:07
faxbut I think that is not what is happening27/10 21:07
faxthe object language is the "LF"27/10 21:09
fax(I find calling it LF extremely confusing btw)27/10 21:09
faxdo you refer to a part of the actual .agda implementation?27/10 21:11
dolioWell, in his thesis, he mainly talks about the vanilla LF I described above, but if you look on page 94, he talks about adding Pi types 'in the universe'.27/10 21:14
dolioWhich would be object-language pi types if you were defining an object language using the LF as a base in Luo style, for instacne.27/10 21:14
dolioDefining languages "in" the LF, if I understand correctly, is done by extending the rules of LF with extra constants and computation rules.27/10 21:16
faxdolio: In 5.6 that's adding impredicative set isn't it?27/10 21:20
faxwhereas every quantification you had before was in Type[2], this lets you have a quantification in Type[1]27/10 21:20
dolioI don't think it's impredicative.27/10 21:21
faxI think the split  Term/Type  is not really saying 'these are different languages' but lets every presentation follow a single technique27/10 21:22
faxto me it reads like:27/10 21:23
faxGamma |- sigma : *,     Gamma, sigma : * |- tau : *27/10 21:23
fax------------------------------------27/10 21:23
fax     Gamma |- Pi_u sigma tau : *27/10 21:23
faxNo, the sort Set lying at the bottom of the hierarchy of computational types is predicative in the basic Coq system. This means that a family of types in Set, e.g. ∀ A:Set, A → A, is not a type in Set and it cannot be applied on itself.27/10 21:26
faxHowever, the sort Set was impredicative in the original versions of Coq. For backward compatibility, or for experiments by knowledgeable users, the logic of Coq can be set impredicative for Set by calling Coq with the option -impredicative-set.27/10 21:26
dolioYes, I know.27/10 21:27
faxso that is why I think Pi_u is impredicative27/10 21:28
dolioLuo introduces a similar object-level pi on 177 of Computation and Reasoning.27/10 21:28
faxLuo does use the LF approach to define his type theory27/10 21:28
dolioPi : (A:Type)((A)Type)Type27/10 21:29
faxI think it's a quite different approach in James' Thesis -- although he uses Type Theory (epigram/agda) instead of Set Theory27/10 21:29
dolioBut that translates to Chapman's LF-embedded in Agda.27/10 21:29
dolioPi : (sigma : Type G U) (tau : Type (G ; El sigma) U) -> Type G U27/10 21:30
dolioEr, those should be Term G U27/10 21:31
faxI've still not really understood what you mean when you say LF in reference to James' development27/10 21:31
faxdolio do correct me if I say something nonsensical there's a big chance I have misunderstood parts of his thesis :P27/10 21:33
dolioI mean that Chapman's thesis could be seen as formalizing (parts of) the LF chapters of Luo's book in Agda.27/10 21:36
dolioLuo takes the LF as a starting point, Chapman encodes it as Agda datatypes.27/10 21:36
faxI don't see much similarity:  My understanding was that Luo uses LF to define the UTT,   Chapman just defines his calculus straight away (as dependently typed syntax)27/10 21:38
dolioThe judgment S : Type in Luo is analogous to S : Term G U in Chapman.27/10 21:38
dolioI think.27/10 21:38
dolioF : (x:A)B  ~ F : Term G (Pi A B)27/10 21:40
dolioAnd Luo adding object-language Pi is analogous to Chapman adding a Pi constructor to the Term type.27/10 21:41
faxyeah that does make sense, I see27/10 21:43
dolioChapman actually mentions the LF at the beginning of that chapter when he's comparing it to someone else's work in agda-light.27/10 21:44
faxwhen he says "we both formalise Martin-Lof ’s logical framework,"?27/10 21:45
dolioYes.27/10 21:47
faxI think he is referring to the entire calculus, not just Type?27/10 21:47
dolioYes, Terms are part of LF, too.27/10 21:48
faxin UTT he uses the LF approach to formalize the object languag, but that object language isn't part of LF - is it?27/10 21:49
dolioBut the way Luo defines the object language in the LF is to declare new terms as part of the LF, so what you end up with looks like the LF + a bunch of extra terms.27/10 21:49
dolioAt least, that's how I understand it.27/10 21:50
faxI saw them as separate but I am not very sure anymore :)27/10 21:50
faxfor example the syntax (terms and types and kinds) of UTT is self contained27/10 21:51
stepcutok, I loaded my .agda file, and it is all syntax highlighted. When I do C-c C-l, it says 'Wrote /tmp/agda2-mode3923pnb' in the Message buffer, and then nothing happens...27/10 21:51
stepcutwhat am I doing wrong?27/10 21:51
dolioI'm trying to write up some of the early parts of Luo's stuff Chapman style, to illustrate.27/10 21:51
faxstepcut when I said that stuff about Coq having reals and integration etc... I mentioned it because I don't think such libraries exist in Agda27/10 21:52
stepcutfax: I don't think I need reals or integration to prove the Fundamental Theory of Counting ?27/10 21:53
faxsure27/10 21:53
faxdolio btw I think with the Type in UTT is stratified implicitly (like in Coq27/10 21:59
dolioWell, the Type in UTT is a meta-language entity.27/10 22:00
dolioHe gets around later to talking about object-language universes, which are cumulative.27/10 22:00
dolioOr, predicative, or whatever.27/10 22:01
dolioIt's kind of a weird system. Different than Coq or Agda.27/10 22:01
faxwhat is the differenc from Coq?27/10 22:02
dolioWell, I think people call the difference Russel-style universes vs. Tarski-style.27/10 22:03
dolioIn Coq, you have A : Type[i], and Type[i] : Type[j] for i < j and so on.27/10 22:03
dolioWhich is Russel style.27/10 22:04
faxthat is also what UTT uses though27/10 22:05
dolioHold on, phone call.27/10 22:06
faxI think they're essentially the same except for UTT has this nice sum type27/10 22:06
dolioIn Tarski-style, like LF/UTT, you have the Type kind/universe, which contains names as values.27/10 22:07
yakovhello27/10 22:07
dolioThen, for each name A in Type, you have El(A) is also a kind.27/10 22:07
faxThat's what Plastic does27/10 22:07
faxhi yakov27/10 22:08
dolioAnd each object language term has a type El(A) in the meta theory, independent of types in the object theory.27/10 22:08
yakovsilly question but anyway is it possible to print values from emacs?27/10 22:09
faxyakov you can compute values and have them displayed if that's what you mean27/10 22:10
dolioBut then he goes on to define universes in the object theory, which have names Type_i : Type.27/10 22:11
yakovyes, this is what i want27/10 22:11
copumpkinC-c C-n in emacs probably?27/10 22:11
dolioSo each predicative universe has a name in Type, and its elements a : El(Type_i) are also names.27/10 22:11
yakovaha. thanks copumpkin27/10 22:13
copumpkin:)27/10 22:13
dolioAnd there's a meta-language function T_i from El(Type_i) to Type that associate the names in El(Type_i) to the names in Type, which in turn associates the names from Type_i with the datatypes that have been defined independently in the meta-theory.27/10 22:14
faxdolio what section is that because that's not how the normal presentation went27/10 22:14
dolioAnd there's always type_i : El(Type_i+1), specifying the hierarchy.27/10 22:14
dolio"9.2.3 Predicative Universes" in his book.27/10 22:14
dolioAnyhow, I've got to grab some dinner. I'll be back in a while.27/10 22:15
doliofax: So, it occurred to me that you might be thinking of ECC, which has a Coq-like type hierarchy, and impredicative Prop level and such.27/10 23:37
faxI was thinking of ECC -_-27/10 23:38
dolioWhich he describes directly, instead of working in the logical framework.27/10 23:38
faxyeah27/10 23:38
dolioWhich sort of illustrates my original point. The UTT he talks about later is a definition of (an extended version of) ECC in the logical framework.27/10 23:39
dolioBut, all terms are typed in LF, and I guess you prove strong normalization based on typing in LF.27/10 23:40
dolioBut, how does that translate to saying that a well-typed ECC term is strongly normalizing?27/10 23:40
dolioI'm also not sure my description of Chapman's stuff as being analogous to the LF stuff is completely on-target, because Chapman deals explicitly with contexts, whereas Luo's LF formulation uses the meta-level pi types for that, I think.27/10 23:43
dolioBut I'm not really sure.27/10 23:46
dolioInstead of "Piu : (A : Term G U) (B : Term (G , El A) U) -> Type G U" a Luo definition might translate as "Piu : Term G (Pi U (Pi (Pi (El 2) U) U))", or something like that.27/10 23:50
dolioWhere 2 is a De Bruijn index.27/10 23:50
dolioOh, actually, that should be a 0, I guess.27/10 23:51
--- Day changed Wed Oct 28 2009
dolioIncidentally, I looked this back up today: https://lists.chalmers.se/pipermail/agda/2008/000640.html28/10 00:23
dolioIt seems to make a lot more sense having read Luo's book.28/10 00:23
-!- copumpkin is now known as Xah28/10 00:56
-!- Xah is now known as copumpkin28/10 00:58
yakovhello28/10 11:57
Saizanhi28/10 12:30
copumpkinhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=271 seems interesting. I wonder how hard it would be to prove the intuition that applicative parsers can recognize exactly context-free languages and that monadic ones can do context-sensitive ones28/10 15:13
Saizanmh, but context-sensitive ones are turing complete, though maybe you can do that in a non-termination monad28/10 15:23
copumpkinyeah, so where does it fall? there's a distinction of "mildly context-sensitive"28/10 15:24
copumpkinthat one feels too restrictive28/10 15:24
copumpkinindexed?28/10 15:25
copumpkinI dunno :)28/10 15:25
copumpkinit'd be nice to get some more formal intuition on that, though, especially given how many monadic parsing libs there are out there :P28/10 15:26
Saizanheh28/10 15:27
FunctorSaladSaizan_: I thought "context-sensitive" has the requirement that the RHS is not longer than the LHS28/10 16:20
FunctorSaladwhich makes them decidable28/10 16:20
FunctorSalad(equivalent to "linearly-bounded" turing machines or some such)28/10 16:20
Saizan_FunctorSalad: ah, true28/10 16:24
Saizan_however monadic parser combinators in haskell can parse turing complete grammars i'd imagine28/10 16:26
copumpkincan you write a nonterminating monadic parser?28/10 16:26
copumpkinI guess you could just put fix id in it28/10 16:26
FunctorSaladcan't even an applicative parser just read in the whole stuff as a string and then do the parsing in a pure function...?28/10 16:29
Saizan_FunctorSalad: the pure function can't report a failure28/10 16:48
Saizan_with monads you can write "do input <- many anyChar; if turingCompleteP input then return () else mzero"28/10 16:49
stepcutis this defining a Haskell-style tuple, or something else?28/10 17:48
stepcutdata Σ (A : Set) (B : A → Set) : Set where28/10 17:48
stepcut  _,_ : (x : A) (y : B x) → Σ A B28/10 17:48
stepcut 28/10 17:48
copumpkinstepcut: not quite28/10 17:49
copumpkinalthough it can be a haskell-style tuple28/10 17:49
stepcuta normal haskell tuple would be more like:28/10 17:50
stepcutdata Tuple ( A : Set ) ( B : Set ) : Set where28/10 17:50
stepcut  _,_ : (x : A) (y : B) -> Tuple A B28/10 17:50
stepcut?28/10 17:50
copumpkinyeah, but you can use the other one as a regular tuple too28/10 17:50
stepcuthow do you do that ?28/10 17:50
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#21328/10 17:51
faxTuple A B = Σ A (const B)28/10 17:52
copumpkinoh well you just stick the second value in there such that its type doesn't depend on it28/10 17:52
copumpkin*on the first value28/10 17:52
stepcutoh the  x function ?28/10 17:52
stepcutlooks like I also have an older version of lib28/10 17:53
copumpkinyeah28/10 17:53
copumpkin_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)28/10 17:53
copumpkinthat one's using the new fancy level stuff28/10 17:53
copumpkinbut you get the idea28/10 17:53
stepcutI have the latest Agda from darcs, so perhaps I should upgrade?28/10 17:53
copumpkinyou mean upgrade the standard library?28/10 17:54
stepcuthow do you go about entering all the unicode symbols. I just open up the library and copy and paste in the characters -- but that doesn't seem like a reasonable long term approach28/10 17:55
copumpkinin emacs there are shortcuts if you type \28/10 17:55
copumpkin\r gives you the right arrow for example28/10 17:55
copumpkin\lambda is a lambda28/10 17:55
stepcutcopumpkin: where can I find that list of shortcuts?28/10 17:55
copumpkin\bn is the Nat symbol28/10 17:55
copumpkin\<tab>28/10 17:55
copumpkinor there's a webpage somewhere on the agda wiki with a few28/10 17:56
stepcutok28/10 17:56
stepcutmaybe I can just look in agda-mode.el ? or is it not agda specific?28/10 17:56
stepcutregarding upgrading the starndard lib: yes, I think so? The standard lib is distribution separately from the compiler right ? i.e. it's not found in http://code.haskell.org/Agda28/10 17:57
stepcutdarcs get --lazy http://www.cs.nott.ac.uk/~nad/repos/lib/28/10 17:58
Saizan_http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.UnicodeInput <- for the shortcuts28/10 17:59
stepcuthow do I tell agda where to find the standard library? So far I have just been setting this emacs variable,  '(agda2-include-dirs (quote ("." "/home/stepcut/n-heptane/projects/agda/lib/src")))28/10 18:00
copumpkinthat's it28/10 18:00
stepcutok28/10 18:01
stepcutok, I tried this:28/10 18:03
stepcutf : Σ ℕ ℕ28/10 18:03
stepcutf = ( zero × zero )28/10 18:03
stepcut 28/10 18:03
stepcutbut I got this error,28/10 18:03
stepcutSet !=< (ℕ → Set) of type Set₁28/10 18:03
stepcutwhen checking that the expression ℕ has type ℕ → Set28/10 18:03
stepcutwhat does !=< mean ?28/10 18:04
stepcutis it a frowny face with a baseball cap?28/10 18:04
copumpkinthe type is \bn x \bn28/10 18:04
faxΣ ℕ ℕ   is a type error28/10 18:04
faxso deal with that first28/10 18:04
copumpkinthat _×_ is a type thing28/10 18:04
copumpkinstepcut: make sense?28/10 18:05
FunctorSaladOT: shouldn't theorem-provers be EDSLs in haskell rather than stand-alone apps?28/10 18:05
Saizan_Σ ℕ (\ _ -> ℕ)28/10 18:05
copumpkinFunctorSalad: only if you're trying to sell us something ;)28/10 18:05
FunctorSaladthen you could use all the power of runtime haskell to combine proofs28/10 18:05
faxFunctorSalad: Ivor is28/10 18:05
FunctorSaladfax: yeah but it seems to be in disrepair somewhat :(28/10 18:06
copumpkinI looked at ivor but couldn't make much sense of it28/10 18:06
FunctorSaladbut that's the idea yes28/10 18:06
FunctorSaladcopumpkin: I don't get it what am I selling...?28/10 18:06
copumpkinI thought you were leading into your type-level proving stuff in haskell that you were working on the other day :)28/10 18:07
Saizan_stepcut: !=< means "not less than or equal"28/10 18:07
FunctorSaladcopumpkin: no, actually after working on it I reappreciated how powerfully expressive the *value*-level is ;)28/10 18:08
copumpkinFunctorSalad: lol28/10 18:08
stepcutfax: Σ ℕ ℕ is a type error because the first argument has the type Set a (with ℕ does), but the second one has the type (A -> Set b), and ℕ does not have that type ?28/10 18:08
FunctorSaladbut it did somewhat make me appreciate the "fluidity"of set theory more *runs before being burned at the stake*28/10 18:09
faxstepcut,28/10 18:09
fax <stepcut> data Σ (A : Set) (B : A → Set) : Set where28/10 18:09
fax <stepcut>   _,_ : (x : A) (y : B x) → Σ A B28/10 18:09
faxtalking about this one?28/10 18:09
copumpkinstepcut: yes, it wants a function and you gave it a type28/10 18:09
stepcutfax: yeah, though I added to the28/10 18:09
copumpkinstepcut: so your type needs to be \bn × \bn28/10 18:09
faxquite simply ℕ : Set, is okay but the next ℕ : ℕ -> Set is wrong28/10 18:09
stepcutlatest version. so now it is data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where28/10 18:09
faxokay28/10 18:09
faxwhy do you want to use this one?28/10 18:10
faxwith ⊔28/10 18:10
copumpkinthat's the new default one in the std lib28/10 18:10
stepcutfax: because newer is better I guess ?28/10 18:10
stepcutfax: it's just whatever is in darcs head for lib28/10 18:10
copumpkinf :  ℕ × ℕ; f = zero , zero28/10 18:11
faxits probably just confusing and worse28/10 18:11
faxwhat is Set28/10 18:11
faxa?28/10 18:11
copumpkinit's a type28/10 18:11
faxis that in the new thing got an explicit level28/10 18:12
copumpkinyeah28/10 18:12
copumpkinSet is the type of types, Set_1 is the type of type of types, and so on28/10 18:12
faxI mean this one though28/10 18:12
fax <stepcut> latest version. so now it is data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where28/10 18:12
faxSet didn't used to have a parameter28/10 18:12
copumpkinyeah, the parameter is the explicit level28/10 18:13
copumpkinto avoid the subscript levels we used to have28/10 18:13
copumpkinso no more Set\_1 Set\_2 and so on28/10 18:13
copumpkinstepcut: make sense?28/10 18:19
stepcutcopumpkin: yes-ish28/10 18:19
copumpkinopdolio gave me a good explanation for all this a few weeks ago28/10 18:20
stepcutcopumpkin: too much Haskell polluting my brain mostly...28/10 18:20
copumpkinstepcut: but basically that sigma is called a dependent sum28/10 18:20
copumpkinmeaning that the _type_ of the right element depends on the _value_ of the left28/10 18:21
copumpkinyou can make that dependency constant28/10 18:21
copumpkinand get yourself a regular haskell 2-tuple28/10 18:21
stepcutcrazy28/10 18:21
copumpkinyou can also get arbitrary sums for example though28/10 18:22
copumpkintypes like Either can be represented easily28/10 18:22
copumpkinyou can think of data Either x y = Left x | Right y as just being a dependent sum with an index of data Side = Left | Right, and then you have fst as an element of Side, and snd as a function that takes Left to x and Right to y28/10 18:23
copumpkinsorry, that's not very elegantly phrased28/10 18:23
stepcutah, I think I get it. Neat.28/10 18:24
stepcutok, so I am trying to do a cartesian product thing now using the tuple. I wrote this:28/10 18:25
stepcutcartesian : ∀ {a b m n} -> Vec a m -> Vec b n -> Vec (a × b) (m * n)28/10 18:25
stepcutcartesian [] _ = []28/10 18:25
stepcutcartesian (x ∷ xs) ys = (map (\y -> x × y) ys) ++ cartesian xs ys28/10 18:25
stepcutbut I get this error: .a !=< Set  for the x in (\y -> x × y)28/10 18:25
copumpkinyeah, you want _,_ there28/10 18:25
stepcutso, that means that a is not less than or equal to Set.28/10 18:25
copumpkinit's a value-level thing28/10 18:25
copumpkinyou'll always use the , constructor28/10 18:26
stepcutwhat does it mean that a is not less than or equal to Set though ?28/10 18:26
stepcutah28/10 18:26
copumpkinnot even sure what the right language for this is28/10 18:26
stepcut:p28/10 18:26
copumpkinbut you're saying that you're mapping from your vec to a type28/10 18:27
copumpkinyou're sticking a type into your vec with that ×28/10 18:27
copumpkinin general saying that it's not less than or equal to Set, it means that you're trying to stick a type where a value is expected, or the type of a type where a type is expected28/10 18:28
copumpkinor that to any level28/10 18:28
stepcutok, so at the most basic level I can define a haskellish tuple like, g : Σ ℕ (λ _ → ℕ) ; g = zero , zero ; But that type siganture is annoying. So we have a function _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b) ; A × B = Σ A (λ _ → B) ; so that I can instead write, f :  ℕ × ℕ28/10 18:32
copumpkinyeah28/10 18:33
faxstepcut28/10 18:33
faxTuple A B = Σ A (const B)28/10 18:33
stepcutI am not used to look at functions and thinking that I might like to use them in my type signature yet ;)28/10 18:33
stepcutfax: yeah, that makes sense now28/10 18:33
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#104828/10 18:34
stepcutthis works:28/10 18:43
stepcutTuple : (A : Set) (B : Set) → Set28/10 18:43
stepcutTuple A B = Σ A (λ _ → B)28/10 18:43
copumpkinyep, that's pretty much how that x is defined28/10 18:43
stepcutbut if I use const I get: Set !=< (_12 A B)28/10 18:43
copumpkinexcept it's dealing with multiple type levels28/10 18:43
stepcut(on the last B)28/10 18:43
stepcutwhich seems odd because const is:28/10 18:44
stepcutconst : ∀ {a b} {A : Set a} {B : Set b} → A → B → A28/10 18:44
stepcutconst x = λ _ → x28/10 18:44
stepcutnow for the tricky part ... how to prove that the cartesian product includes every combination of elements from Vec a m and Vec b n :-/28/10 18:52
copumpkinhow do you intend to express that?28/10 18:52
stepcutthat's what I am working on. Though I am wondering if maybe I should have used sets.28/10 18:53
copumpkinI can tell you how I'd do it, but there may be a more elegant way28/10 18:53
copumpkinI'm pretty new to this too :)28/10 18:54
stepcutactually, I also need to prove that the cartesian product does not include any other elements as well..28/10 18:57
copumpkinyep, you can do those separately28/10 18:57
stepcutwell, what I really want to prove is the rule of product. If event 1 can happen m ways and event 2 can happen n ways, then there are exactly m*n ways that both can occur together28/10 18:57
copumpkinyep28/10 18:58
stepcutso, one part is to prove that, ∀ a b, if a ∈ A and b ∈ B, then (a, b) ∈ A × B28/10 18:59
copumpkinyep28/10 19:00
copumpkinso written as a type...?28/10 19:00
stepcutI was thinking something like this:28/10 19:02
stepcutlemma1 : ∀ {a b m n} → (a ∈ Vec a m) → (b ∈ Vec b n) → ((a × b) ∈ (Vec (a × b) (m * n)))28/10 19:02
stepcutbut ∈ is not defined for Vec that I saw28/10 19:02
stepcutI guess I need to write it ?28/10 19:04
copumpkinit is28/10 19:07
copumpkinwell28/10 19:07
copumpkindata _∈_ {a : Set} : a → {n : ℕ} → Vec a n → Set where28/10 19:07
stepcutoh, duh.28/10 19:08
copumpkinits constructors may be a bit of a pain though28/10 19:08
stepcuthow can I get agda to check my type signature before I implement the function bodies. is that possible ?28/10 19:09
stepcutoh. maybe its just, lemma1 : <type> : lemma1 = _28/10 19:10
copumpkinjust type ?28/10 19:21
copumpkinit'll put a "hole" there28/10 19:21
copumpkinlike f : aType28/10 19:24
copumpkinf = ?28/10 19:24
copumpkinthen C-c C-l28/10 19:24
copumpkinand it'll convert the question mark into a fancy hole28/10 19:24
copumpkinand allow you to ask for the type of that hole and other things28/10 19:24
stepcutcool28/10 19:26
stepcutok, so with the member thing I can only express the types, x ∈ x ∷ xs and x ∈ y ∷ xs right? (via here and there)28/10 19:27
stepcutoh wait, I misread the type for 'there'28/10 19:28
copumpkinso you get how it works?28/10 19:40
stepcutvery slowly28/10 19:40
stepcutI think my first step is to prove:28/10 19:40
stepcutlemma1a  : ∀ {a b : Set}{m n : ℕ }{x : a}{y : b} {xs : Vec a n}{ys : Vec b m} → (x ∈ x ∷ xs) → (y ∈ y ∷ ys) → ((x , y) ∈ (x , y) ∷ cartesian xs ys)28/10 19:40
copumpkinwhy are you doing x \in x \:: xs ?28/10 19:41
stepcutinstead of just, x \in xs ?28/10 19:42
copumpkinyeah28/10 19:42
stepcuthrm, do to an earlier error I made I think28/10 19:43
stepcutI am not really clear on how to prove implement this, test :  ∀ {a} {n} {x} {xs : Vec a n} → x ∈ xs28/10 19:44
stepcutmaybe I don't need to ...28/10 19:46
stepcutok, so now I have this:28/10 19:46
stepcutlemma1a  : ∀ {a b : Set}{m n : ℕ }{x : a}{y : b} {xs : Vec a n}{ys : Vec b m} → (x ∈ xs) → (y ∈ ys) → ((x , y) ∈ cartesian xs ys)28/10 19:46
stepcutthis does seem better :)28/10 19:46
stepcutnow I have my first case:28/10 19:48
stepcutlemma1a here here = here28/10 19:48
copumpkincool, how's it going?28/10 19:55
stepcutsecond case not so well28/10 19:56
stepcutI want something like:28/10 19:56
stepcutlemma1a here (there ys) = lemma1a here ys28/10 19:56
stepcutbut I have not got it quite right yet28/10 19:56
stepcutyeah, I don't get this part ;)28/10 20:05
stepcutmaybe I need a with28/10 20:06
copumpkinyou might :)28/10 20:08
copumpkindo you get the basic meaning of here vs. there?28/10 20:08
stepcutyeah. here say that if you have an element x and you append it to the head of a vector, then the vector contains x28/10 20:09
stepcutthere says that if you know that x is a member of xs, then if you append an element to the head of the vector x is still a member28/10 20:10
stepcutooo...28/10 20:12
copumpkin?28/10 20:12
stepcuthrm, still not right28/10 20:13
stepcutI guess I don't understand what is wrong with this yet,28/10 20:15
stepcutlemma1a here (there ys) = lemma1a here ys28/10 20:15
copumpkinwhat does it say?28/10 20:16
stepcuthere is the proof that (x ∈ xs) and there is the proof that (y ∈ ys) it contains a proof that (y ∈ y' : ys'), = lemma1 here ys proves that, (x, y) ∈ cartesian xs ys'28/10 20:18
stepcutwhich is not quite right because that is showing the cartesian of xs ys' not xs ys28/10 20:19
copumpkinstepcut: make any progress?28/10 21:43
stepcutcopumpkin: no, I had to do something else for a bit, but I am looking at it again now28/10 21:52
stepcutthough I'm currently at a lose as to what to do28/10 21:53
stepcutin fact, now I don't even understand why the part that works, works,28/10 21:59
stepcutlemma1a  : ∀ {a b : Set}{m n : ℕ }{x : a}{y : b} {xs : Vec a n}{ys : Vec b m} → (x ∈ xs) → (y ∈ ys) → ((x , y) ∈ cartesian xs ys)28/10 21:59
stepcutlemma1a here here = here28/10 21:59
copumpkinI'll be back in a little while, going home28/10 21:59
doliomatching against "here" refines xs to "x :: zs" in the first case, and similarly for ys.28/10 22:00
faxstepcut what are you tring to write?28/10 22:00
stepcutfax: proof that, ∀ a b, if a ∈ A and b ∈ B, then (a, b) ∈ A × B28/10 22:02
dolioSo you end up with "lemma1a {xs = x :: xs'} {ys = y :: ys'} here here : (x , y) \in cartesian (x :: xs') (y :: ys')28/10 22:02
faxstepcut just as a test or for something else?28/10 22:02
dolioAnd presumably cartesian (x :: xs') (y :: ys') = (x , y) :: whatever28/10 22:02
stepcutfax: the eventual goal is to prove that if you have event a which can happen m ways and event b which can happen n ways that there are m*n ways that a and b can happen together28/10 22:04
faxoh heh28/10 22:04
stepcutyeah.. I still have no idea what to do for the second case28/10 22:14
faxstepcut got a nice proof of this on paper?28/10 22:16
faxor web or whatever28/10 22:16
stepcutfax: no sir28/10 22:16
faxstep 1 ^28/10 22:16
* stepcut never learned how to do proofs 28/10 22:17
yakovhello28/10 22:19
faxhi28/10 22:20
yakovI want to buy Basic Proof Theory to catch up with proof-assistant side of Agda :-) is it a good book for agda programmer?28/10 22:20
faxhm I've read that28/10 22:21
faxas much as I like Troelstra, I don't think I got much out of it, I preferred  Proof Theory - Takeuti28/10 22:22
faxI don't think it has much to do with agda28/10 22:23
faxeither of them,a28/10 22:23
stepcutfax: I am having difficult proving this on paper, because the definition of a cartesian product is, X x Y = { (x, y) | x ∈ X, y Y ∈ Y }. So the thing I am trying to prove is the definition.. :-/28/10 22:32
faxstepcut what exactly to prove?28/10 22:33
faxI missed a lot of whatever was happening28/10 22:33
stepcutI wrote a function: cartesian : ∀ {a b m n} -> Vec a m -> Vec b n -> Vec (a × b) (m * n)28/10 22:33
stepcutwhich is supposed to do the cartesian product28/10 22:34
stepcutso I am trying to so that for my implementation, ∀ a b, if a ∈ A and b ∈ B, then (a, b) ∈ A × B.28/10 22:34
stepcutor more specifically, lemma1a  : ∀ {a b : Set}{m n : ℕ }{x : a}{y : b} {xs : Vec a n}{ys : Vec b m} → (x ∈ xs) → (y ∈ ys) → ((x , y) ∈ cartesian xs ys)28/10 22:35
faxstepcut I can't think of any nice way to format this all28/10 23:14
stepcutheh28/10 23:14
faxonly the obvious thing about length and drop etc28/10 23:14
faxthere must be a better way28/10 23:14
* stepcut knows no ways, much less a better one28/10 23:14
stepcutwhat is the obvious thing about length and drop?28/10 23:15
faxif cartesian was something like28/10 23:15
faxx (y::ys) --> map (y:) xs ++ cartesian xs ys28/10 23:15
yakovyou've mentioned OTT yesterday. what does this acronym mean?28/10 23:15
faxthen drop (length xs) (map (y:) xs ++ cartesian xs ys) = cartesian xs ys28/10 23:15
faxand yo ucan rewrite that in the recursive step of the proof for lemma1a28/10 23:16
stepcutfax: I have,  cartesian (x ∷ xs) ys = (map (\y -> x , y) ys) ++ cartesian xs ys28/10 23:16
fax(this is slightly hideous)28/10 23:16
dolioObservational type theory.28/10 23:16
faxstepcut, that's what I mean28/10 23:16
faxh28/10 23:17
faxhm28/10 23:17
faxstepcut do yu have join for vectors?28/10 23:22
stepcutum28/10 23:24
stepcutI am using Data.Vec, so if it's not there, I don't have it.28/10 23:25
copumpkinconcat28/10 23:25
stepcutby join do you mean, Vec (Vec a n) m -> Vec a (m * n) ?28/10 23:26
faxyes28/10 23:26
stepcutnope.28/10 23:26
copumpkinI remember seeing that28/10 23:26
copumpkinsomewhere, I thought28/10 23:26
copumpkinah well, it wouldn't be hard to write28/10 23:26
stepcutconcat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m)28/10 23:27
stepcutconcat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m)28/10 23:27
stepcutconcat []         = []28/10 23:27
stepcutconcat (xs ∷ xss) = xs ++ concat xss28/10 23:27
stepcut 28/10 23:27
stepcut ?28/10 23:27
copumpkinsure, if that works28/10 23:31
Saizanstepcut: are you formalizing prob. theory to do your homework? i was going to attempt that too :)28/10 23:32
stepcutSaizan: yes, but it is not homework28/10 23:35
--- Day changed Thu Oct 29 2009
faxstepcut I am attempting to prove this in the normal way and it is awful :P29/10 00:02
faxI hope someone comes up with a better way29/10 00:04
stepcutfax: heh29/10 00:11
faxif you want to read it here, http://pastie.org/67430529/10 00:14
faxeverything up to "proof" seems fine29/10 00:14
faxbut then it turns horrible and we realize it was all a mistake29/10 00:14
stepcutpurrty29/10 00:15
faxit could probably be neatened up a bit by making more functions and pretending to develop some 'theory' about dropping and so on.. I think it's only application would be the single proof though - so kinda pointless29/10 00:17
copumpkinfax: don't like implicit parameters for that proof?29/10 00:20
faxno29/10 00:26
faxstepcut next you show   < a , b > in A * B --> (a in A x b in B) ?29/10 00:53
faxwhere does that vector product thing place in the whole scheme?29/10 00:53
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11256#a1125629/10 01:02
dolioI think most of that stuff is in the standard library.29/10 01:03
copumpkinoh purty29/10 01:05
copumpkindolio: not a fan of the std lib?29/10 01:05
dolioI wanted to see if I could rewrite it without looking.29/10 01:05
copumpkin:)29/10 01:05
faxmuch better29/10 01:06
dolioNow I'm not finding it, though...29/10 01:07
copumpkinstepcut: !!!29/10 01:07
stepcutcopumpkin: !!!29/10 01:10
copumpkin:)29/10 01:11
copumpkinstepcut: did you see master dolio's masterful proof?29/10 01:11
dolioOh, it's only defined for lists.29/10 01:11
stepcutcopumpkin: I am seeing it now.29/10 01:11
dolioData.List.Any.Properties has lots of stuff in this area.29/10 01:11
copumpkinyeah, I got frustrated at how much more Data.List had than Vec29/10 01:11
stepcutI'll have to study it tomorrow though29/10 01:11
stepcutlooks nice29/10 01:16
yakovhello29/10 08:56
copumpkindouble negation monad :o29/10 17:23
FunctorSalad:o29/10 17:27
FunctorSaladisn't that Cont Void?29/10 17:27
FunctorSalad(don't know if there's Cont in Agda?)29/10 17:27
copumpkinI thought one of dolio's experiments involved that29/10 17:28
copumpkinmaybe not29/10 17:29
FunctorSaladis ./example/lib in the darcs source tree the current stdlib?29/10 17:44
FunctorSalad("example")29/10 17:44
copumpkinnope29/10 18:06
copumpkinit's a separate repo29/10 18:06
copumpkindo you think the double negation in the latest email on the agda list was intentional?29/10 18:36
copumpkinBut it is not29/10 18:36
copumpkinnot OK for a corresponding theory of countably branching29/10 18:36
copumpkinwell-founded trees.29/10 18:36
FunctorSaladsorry newb question... what does the dot in patterns mean?29/10 20:03
FunctorSaladsomething about absurdity I reckon29/10 20:04
FunctorSaladanother question: is there any global indexing mechanism for theorems?29/10 20:05
faxFunctorSalad: it's the dependent pattern matching refinement29/10 20:05
fax(where matching on one thing tells you something about another thing)29/10 20:05
FunctorSaladrevealing existentials by pattern matching, like in haskell?29/10 20:06
faxif you have a constructor    X : T Foo29/10 20:10
faxthen  f : i -> T i -> ...29/10 20:10
faxthe pattern    X for T i refines i into 'Foo'29/10 20:10
faxso you can write   f .Foo X = ...29/10 20:10
* FunctorSalad really likes the haskell mode so far29/10 20:10
FunctorSaladerr emacs mode29/10 20:11
FunctorSalad(I've independently wished for this 'holes' thing in haskell actually)29/10 20:11
copumpkinit's pretty nice29/10 20:12
FunctorSaladfax: indexed families are the same thing as existentials really or not? at least in haskell they are29/10 20:12
FunctorSaladX : T Foo can be written as X : i = Foo -> T i29/10 20:13
FunctorSalad(don't know if that's correct in agda)29/10 20:13
FunctorSaladI just started using it rather than just hearing about it ;)29/10 20:13
FunctorSalad(the i is existential there)29/10 20:14
byorgeyfax: what?  I thought that happened automatically, and the dot is to mark *inaccessible* patterns29/10 20:14
byorgeyunless I am confused29/10 20:14
FunctorSaladmaybe I should write what I mean in haskell:29/10 20:16
faxno I don't think so FunctorSalad29/10 20:16
FunctorSaladdata T :: (* -> *) where X : T Foo29/10 20:16
FunctorSaladis equivalent to29/10 20:16
faxthat is not useful29/10 20:16
FunctorSaladdata T j = (j ~ Foo) => T j29/10 20:17
FunctorSalad(I find that to be conceptually somewhat simpler than the indexed families)29/10 20:17
FunctorSaladcorrection:29/10 20:18
FunctorSaladdata T j = (j ~ Foo) => X29/10 20:18
faxFunctorSalad I don't think this has any interesting content29/10 20:18
FunctorSaladfax: it eliminates index families as primitives...29/10 20:18
FunctorSalad*indexed29/10 20:18
FunctorSaladbut you need some built-in equality, as haskell has29/10 20:19
FunctorSaladis there some builtin for dependent pairs?29/10 20:28
-!- opdolio is now known as dolio29/10 21:14
dolioYou can mimic the Haskell version by storing the propositional equality.29/10 21:17
doliodata T (j : ?) : Set where X : j ≡ Foo → T j29/10 21:17
dolioAlthough that's rarely nicer than indexing directly.29/10 21:19
FunctorSalad"Not a valid let-declaration29/10 21:26
FunctorSaladwhen scope checking"29/10 21:26
FunctorSalad what could that mean?29/10 21:26
dolioUh... Your 'let' is invalid somehow?29/10 21:27
dolioAnd it happened during the phase where it was resolving the scope of names.29/10 21:27
FunctorSaladhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11282#a1128229/10 21:27
FunctorSaladyes but how is it invalid ;)29/10 21:28
dolioNo pattern matching in let function definitions.29/10 21:28
dolioWhich is a bizarre restriction, but...29/10 21:28
FunctorSaladis there any other way to do an inline pattern match or do I need a toplevel decl?29/10 21:29
dolioTop level, I'm afraid.29/10 21:29
dolioOr a where.29/10 21:29
dolioThat looks like it'd be fine in a where.29/10 21:30
FunctorSaladah, I inferred from "not in let" that "not in where" either29/10 21:31
FunctorSaladthanks29/10 21:31
dolioNope, let and where are different for some reason. :)29/10 21:32
doliowhere is sugar (or something) for a local module, whereas let is something else.29/10 21:32
dolioOh, lets can't be recursive, either. I guess it just inlines everything in the let, essentially.29/10 21:34
FunctorSaladah29/10 21:35
dolioAccording to the AIM10 notes, there was talk about making let more like where, though.29/10 21:36
FunctorSalad(can anyone *ever* remember which direction of the adjunction is ♯ and which is ♭? ;))29/10 21:36
FunctorSaladI think Hom(A,UB) ---> Hom(FA,B) should be ♯29/10 21:37
FunctorSaladbecause it "extends" a function to the whole free gadget29/10 21:37
FunctorSaladbut I think I've seen it the other way29/10 21:38
dolioAdjunction?29/10 21:38
FunctorSaladthe adjoint functors kind29/10 21:38
dolioHmm, I hadn't thought of that as an adjunction.29/10 21:39
dolioThen again, they're one of the weak areas of my basic category theory knowledge.29/10 21:40
FunctorSalad♯ and ♭ are just names sometimes used for the two directions of the adjunction isomorphism29/10 21:42
FunctorSaladI think it's better than φ ;)29/10 21:42
dolioWhat are the two functors? F and \inf F? Or I and \inf?29/10 21:43
FunctorSaladah you mean this specific case of set union?29/10 21:45
FunctorSalad(with "that")29/10 21:45
dolioI hadn't thought of \inf as being part of/defined by an adjunction.29/10 21:46
FunctorSalad\inf?29/10 21:47
dolioAre we talking about some \sharp and \flat that are unrelated to codata?29/10 21:47
FunctorSaladI don't know the usage of ♯ and ♭ with codata29/10 21:48
FunctorSaladmaybe it's a special case of the usage for adjunctions29/10 21:48
dolioOh, well, nevermind me, then. :)29/10 21:48
FunctorSalad(pretty much anything in structure math is an adjunction ;))29/10 21:48
dolioOh, I see what you're saying now.29/10 21:48
FunctorSaladin my case I have that \bigcup is defined by the property: ⋃ Y ⊆ Z  if and only if (∀ X ∈ Y.   X ⊆ Z)29/10 21:49
FunctorSaladwhich can be expressed as an adjunction if you take the category "sets ordered by inclusion"29/10 21:50
dolioI find myself preferring the epsilon/eta definition of adjunctions.29/10 21:53
dolioPossibly because I feel all dirty and concrete talking about hom-sets. :)29/10 21:54
dolioMaybe if I only worked in enriched categories, I'd feel better. :)29/10 21:55
FunctorSaladhmm never thought about it like that29/10 21:56
FunctorSaladbut yes it seems to involve your background set theory29/10 21:56
dolioAlthough, working through the adjunction for exponentials with solidsnack this morning, the hom set version is the one that shows you currying immediately.29/10 22:02
dolioWhich is nice.29/10 22:02
FunctorSaladthe minibuffer should use the agda input-method too29/10 22:27
dolioIt does sometimes.29/10 22:28
dolioLike for C-c C-d/n.29/10 22:28
dolioBut not C-s.29/10 22:28
FunctorSaladI can M-x set-input-method in the minibuffer but it won't remember29/10 22:30
FunctorSaladcan't I insert holes in a hole?29/10 22:31
FunctorSalad(with manual question marks, not 'refine')29/10 22:31
dolioYou can.29/10 22:32
dolio{ foo ? }029/10 22:32
FunctorSaladapparently the two question marks are assumed to be the same type29/10 22:32
FunctorSalador I have some other bug :)29/10 22:35
Saizanyou can put things in the holes? i never tried that29/10 23:14
dolioWhat do you do? Delete the hole and fill it in yourself?29/10 23:28
faxI use _ and then fill it in29/10 23:28
--- Day changed Fri Oct 30 2009
FunctorSaladyou can also fill it in yourself and press C-c C-space ;)30/10 00:23
dolioThat was such a surprise you knocked fax off the internet.30/10 00:24
roconnor_FunctorSalad_: how do universe levels work in agda?30/10 15:59
FunctorSalad_roconnor_: no idea I'm a newbie myself30/10 15:59
copumpkinroconnor_: up until recently, you had Set, Set\_1 Set\_2 and so on30/10 15:59
copumpkinI just realized I probably can't give you the level of answer you're looking for :)30/10 16:00
FunctorSalad_how do you find stuff in the stdlib?30/10 16:03
copumpkinI browse the Everything file, or use grep -R30/10 16:03
copumpkinbut it's a real pain, in general30/10 16:03
roconnor_data Ens : Set\_1 where30/10 16:04
roconnor_  sup : (I : Set) -> (I -> Ens) -> Ens30/10 16:04
roconnor_how do I get that to go?30/10 16:04
roconnor_ah Set130/10 16:05
FunctorSalad_roconnor_: I can't seem to get powersets to work with it30/10 16:05
copumpkinyeah, I was just using the \_ for the emacs input thing30/10 16:05
FunctorSalad_you can put I : Set1, then you can use I -> Set as index set30/10 16:05
FunctorSalad_*but* I can't get elementhood in Set30/10 16:05
FunctorSalad_didn't try that much though30/10 16:05
copumpkinwell, as of recently, you can explicitly work with arbitrary levels30/10 16:05
copumpkinbut I think you'll need the darcs version for that30/10 16:06
copumpkinSo instead of Set\_1 you have Set 1 (where 1 is a built-in level type)30/10 16:06
FunctorSalad_Set (suc zero) ;)30/10 16:06
copumpkinit doesn't have syntactic sugar yet?30/10 16:06
FunctorSalad_maybe I didn't enable it30/10 16:06
copumpkinmaybe you're right :)30/10 16:06
copumpkindon't have the latest agda on this computer and am too lazy to compile it now to check :P30/10 16:07
FunctorSalad_can you axiomatize classical set theory with: postulate S : Set30/10 16:07
FunctorSalad_postulate _∈_ : S -> S -> Bool30/10 16:07
FunctorSalad_?30/10 16:07
FunctorSalad_seems much more computational than S -> S -> Set30/10 16:07
roconnor_um30/10 16:08
roconnor_how do I write an anonymous function in Agda?30/10 16:08
FunctorSalad_haskell syntax30/10 16:08
copumpkin(\lambda x \r moo x)30/10 16:08
roconnor_ugh30/10 16:08
roconnor_so much typing30/10 16:08
copumpkin:P30/10 16:08
roconnor_that doesn't work in emacs30/10 16:09
roconnor_I type \30/10 16:09
roconnor_and the next character goes crazy30/10 16:09
roconnor_ah30/10 16:09
roconnor_anyhow30/10 16:09
roconnor_must go to lunch now30/10 16:09
copumpkinit needs to go through various other things30/10 16:09
copumpkinbefore hitting lambda30/10 16:09
roconnor_will deal with this later30/10 16:09
FunctorSalad_funcompo should be universe polymorphic right?30/10 17:05
roconnor_FunctorSalad_: okay, I can define a "Power set" but I doubt I can prove it's defining property.30/10 18:26
roconnor_FunctorSalad_: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a1134430/10 18:26
FunctorSalad_roconnor_: oh, you unwrapped everything... I tried to use my ∈ type, which didn't work because ∈ is Set2 or something (with Ens : Set2)30/10 18:28
FunctorSalad_why shouldn't it work?30/10 18:29
roconnor_well, it shouldn't work because I don't think Agda has enough proof theoretic strength to prove Z is consistent.30/10 18:30
roconnor_at least Martin Lof type theory doesn't have enough strength to prove Z is consistent.30/10 18:30
roconnor_FunctorSalad_: but you are exactly right.30/10 18:31
roconnor_If I try to prove a `mem` Power b <-> a `subset` b, I don't think it will were30/10 18:31
roconnor_because I have only Set valued predicates, and I would need something like Set2 valued predicates as you say.30/10 18:32
faxroconnor what is Z?30/10 18:35
faxZFC without the FC?30/10 18:35
faxmaye spoil the fun but you can find defiinitions and proofs in Benjamin Werners paper30/10 18:36
roconnor__god damn wireless30/10 18:39
faxroconnor did you read my ? question30/10 18:39
faxwhat is Z?30/10 18:39
roconnor__nope30/10 18:40
roconnor__Z is Zermelo set theory30/10 18:40
faxokay30/10 18:40
roconnor__essentially ZF without the replacement axiom30/10 18:40
roconnor__techincally Z also has no foundation axiom, but no one cares about that.30/10 18:40
faxwhy not??30/10 18:40
roconnor__because only set theoriests care if sets are well-founded30/10 18:41
faxheh30/10 18:41
roconnor__everyone else is using sets to do encoding.30/10 18:41
roconnor__to do real math30/10 18:41
roconnor__they don't care about the structure of their codes.30/10 18:41
faxI think real math should stop using logical foundations30/10 18:42
roconnor__category theory is in fashion30/10 18:42
FunctorSalad_heh did you write that wikipedia line that foundation is "arguably the least useful axiom in ZFC"?30/10 18:42
roconnor__nope30/10 18:42
-!- roconnor__ is now known as roconnor30/10 18:42
roconnorI was simply repeating it here.30/10 18:42
roconnor:)30/10 18:42
roconnorwikipedia is my source for all of what I am saying30/10 18:42
roconnorFunctorSalad_: I go my member predicate to be in Set1 instead of Set230/10 18:44
roconnorbut that still isn't low enough.30/10 18:44
roconnorhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a1134630/10 18:45
roconnorhmm30/10 18:46
roconnorthis is wrong30/10 18:46
FunctorSalad_is the model good for anything except showing that the axiomatic approach is consistent in agda?30/10 18:47
FunctorSalad_I mean, good for using the resulting set theory30/10 18:48
roconnorwell, I was given the semantics of a logic in set theory30/10 18:48
roconnorI'm trying to formalize it.30/10 18:48
roconnoris ~ not?30/10 18:49
faxFunctorSalad which model ?30/10 18:49
roconnorfax: this Ens model I / FunctorSalad_ are writing.30/10 18:49
FunctorSalad_roconnor: I mean, does constructing a model for set theory help you with that formalization, compared to postulating the axioms of set theory30/10 18:50
roconnorya30/10 18:50
roconnorprobably not30/10 18:51
roconnorother than giving evidence that the axioms are sound.30/10 18:51
roconnorI don't have much justification beyond wanting to do this.30/10 18:51
roconnorah finally got to the crux of the matter30/10 18:53
roconnorhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a1134930/10 18:54
roconnorin Coq, forall (A : Type (*1*)), Prop  has type Prop, but in agda it has Type (*1*).30/10 18:55
roconnorso that line I marked as doesn't type check is the difference that makes this work in Coq but not in Agda.30/10 18:56
roconnorwhich is the impredicativity of Coq.30/10 18:56
faxroconnor can't you just duplicate the def. of negation on different levels to define this in Agda?30/10 18:56
roconnorero30/10 18:56
roconnorforall (A : Type) (something in prop) ...30/10 18:56
faxoh no you couldn't30/10 18:57
roconnorfax: my goal is to define that exists to return something of type Set, so I can use it in my power set.30/10 18:57
roconnorer30/10 18:58
roconnorI mean to change mem, subset and equiv to return Set.30/10 18:58
roconnorhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a1135030/10 18:59
roconnorResult for command Check forall (A:Type), True . :30/10 19:00
roconnorType (* Top.4183 *) -> True30/10 19:00
roconnor     : Prop30/10 19:00
roconnorResult for command Check forall (A:Type), unit . :30/10 19:00
roconnorType (* Top.4184 *) -> unit30/10 19:00
roconnor     : Type (* max(0, (Top.4184)+1) *)30/10 19:00
-!- roconnor_ is now known as roconnor30/10 21:16
-!- Saizan_ is now known as Saizan30/10 21:31
--- Day changed Sat Oct 31 2009
dolioHuh, updating to the new version of ubuntu changed a lot of the unicode characters in emacs.31/10 09:41
rhzHi. Why would I get this error: Failed to find source of module Data.Nat in any of the following locations: ..... when scope checking the declaration open import Data.Nat, even if the file Nat.agda is in the location given by .....? This is in Emacs btw. Furthermore if I try to load a file from the standard library itself that includes Data.Nat then there is no problem. I'm stumped.31/10 12:01
-!- byorgey_ is now known as byorgey31/10 13:47
FunctorSaladwhat does it mean when agsy says "Meta variable kind not supported: Sort (Type (Var 0 []))"?31/10 15:22
FunctorSaladhmm does agda automagically resolve the ambiguity between Data.List and Data.Vec symbols?31/10 16:05
FunctorSaladI have imported both and [] works31/10 16:05
FunctorSaladare there type synonyms?31/10 16:15
FunctorSaladoh right they are just plain definitions =)31/10 16:19
Saizan_FunctorSalad: yeah, you get overloading for constructors31/10 16:47
FunctorSaladhow can I do this? foo = ..... (\n -> case elimFin1 n of refl -> ....) .... ?31/10 17:28
FunctorSalad(the notation if there was case)31/10 17:28
copumpkinuse a with31/10 17:28
FunctorSaladinside the lambda?31/10 17:30
copumpkinnot sure how you'd use it with a lambda31/10 17:31
FunctorSaladguess I'll have to mess with subst instead of pattern matching on the refl?31/10 17:48
copumpkinthat might be easier31/10 17:48

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