dolio dolio vixey --- Log opened Thu Oct 01 00:00:52 2009 universe> :t \(l : Level) (A : Type[l]) (x : A) -> x 01/10 00:14 (l : Level) -> (A : Type[l]) -> (x : A) -> A 01/10 00:14 is that Type part of the theory now? 01/10 00:14 :t (l : Level) -> (A : Type[l]) -> (x : A) -> A  ==> Type[omega] 01/10 00:14 of a function? 01/10 00:14 or** 01/10 00:15 It's part of the type theory of the universe polymorphism I hacked onto my pure type system interpreter. 01/10 00:15 aha cool 01/10 00:15 Which 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 interpreter?? does that mean you actually run code??? 01/10 00:20 Well, yeah, if you consider normalizing lambda terms "running code". 01/10 00:20 Seems I've done something wrong, though. 01/10 00:22 :t \(l : Level) (C : (k : Level) -> Type[k] -> Type[k]) -> C (Suc l) (Type[l]) 01/10 00:23 Gives: 01/10 00:23 (l : Level) -> (C : (k : Level) -> Type[k] -> Type[k]) -> (k : Level) -> Type[k] -> Type[k] 01/10 00:23 Which isn't right. 01/10 00:23 It should be: 01/10 00:23 (l : Level) -> (C : (k : Level) -> Type[k] -> Type[k]) -> Type[Suc l] 01/10 00:23 -!- ksf is now known as TheHunter 01/10 01:15 -!- TheHunter is now known as ksf 01/10 01:15 Ah hah. Seems to be a parsing error. 01/10 01:19 you shoudl proof your parser XD 01/10 01:20 Yeah. I'll just whip up a total interpreter for a dependently typed language. 01/10 01:22 oh?? 01/10 01:22 And use that well-developed library of parser combinators. 01/10 01:22 did you read James Chapmans thesis?? 01/10 01:22 No. Did someone finally manage something impressive in that area? 01/10 01:23 oh yeah! 01/10 01:23 Are we talking total parser combinators or total language interpreters? 01/10 01:23 http://cs.ioc.ee/~james/PUBLICATION_files/thesis.pdf 01/10 01:23 I knew about the parser combinators. 01/10 01:23 I did parsers with proofs too 01/10 01:23 it's really difficult 01/10 01:23 Agda folks have been working on that. 01/10 01:24 well I don't see them doing proofs 01/10 01:24 just making parsers that are total 01/10 01:24 Yes. 01/10 01:24 yes ? to what 01/10 01:24 They don't do proofs. Just make combinators that can be used at all in Agda. 01/10 01:25 ah ok 01/10 01:25 You have to walk before you can run, though. 01/10 01:25 I think the proofs have to be part of the libarary really -- obviously it's a starting point ... yeah walk before run 01/10 01:26 fwiw I got the proofs working but mine is hideous to actually use :P 01/10 01:26 getting 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 thought 01/10 01:27 :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 though 01/10 01:27 Success. 01/10 01:27 nice 01/10 01:27 Level is nat? 01/10 01:27 or something conat? or else 01/10 01:27 Level is sort of the extended naturals. 01/10 01:28 It's built-in, though. 01/10 01:28 I have Level : Type[0] right now. 01/10 01:28 The idea is that quantifying over Level ranges over naturals. 01/10 01:29 And then things of the form (l : Level) -> ... Type[l] live in Type[Omega]. 01/10 01:29 So maybe, technically, Level is just the naturals, and there's an extra universe above everything. 01/10 01:30 I think I have Omega : Level type checking right now, though. 01/10 01:30 Thanks for that thesis, by the way. Ground-breaking stuff. 01/10 01:32 dolio all of his work it excellent! I have been waiting for that thesis to be released for some time 01/10 01:35 he uses techicolor!! 01/10 01:35 I think we must thank Conor for this new trend 01/10 01:36 (?) 01/10 01:36 Yeah, it's lie most Epigram papers. 01/10 01:36 Like, even. 01/10 01:36 Quite nice. 01/10 01:36 I wonder if they have a tool that automatically converts the Epigram source to nicely colored latex like that. 01/10 01:37 dolio does your thing do inductives and/or coinductives? 01/10 01:52 Hah, no. 01/10 01:52 I think it's really easy to add inductives but um, adding coinductives is way beyond my knowledge 01/10 01:52 It's just does straight lambda calculi with pure type systems. 01/10 01:53 I'm guessing that one wants OTT if they are adding coinductives but really just don't know anything verly clearly in that area 01/10 01:53 Although 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 It just won't do anything during normalization. 01/10 01:54 oh but you need normalization don't you :S 01/10 01:55 Running code is so 90s. 01/10 01:55 folds 01/10 01:55 lol 01/10 01:55 -!- opdolio is now known as dolio 01/10 02:03 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10096#a10096 01/10 02:39 cool 01/10 02:40 http://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 list 02/10 06:35 about the Raw* distinction 02/10 06:35 I don't really, either. 02/10 06:36 he sort of repeated the obvious at me :) 02/10 06:37 The RawFoos in the algebra modules aren't even used for representing the operator set. 02/10 06:37 There'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 yeah 02/10 06:38 there's so much duplication in there 02/10 06:38 I've started a new algebra module that I hope will be nicer, but haven't had much time 02/10 06:38 Going the other way around wouldn't be great either, though. 02/10 06:39 You'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 yeah 02/10 06:40 Because you can only open them after the fields. 02/10 06:41 what bothers me is how deep you sometimes have to go to pull out properties 02/10 06:41 unless I missed something about how the modules work 02/10 06:41 (well, that and all the duplication) 02/10 06:42 -!- koninkje is now known as koninkje_away 02/10 08:56 -!- opdolio is now known as dolio 02/10 15:44 wow, it looks like nobody's touched this luo type theory book since it was purchased in 94 02/10 16:13 I suppose that isn't surprising. 02/10 16:17 guess not, but it's nice to have a brand new book 02/10 16:19 the TAPL I checked out looked like a car had run over it 02/10 16:19 --- Day changed Sat Oct 03 2009 -!- byorgey_ is now known as byorgey 03/10 20:43 --- Day changed Sun Oct 04 2009 hey there 04/10 19:26 anyone awake? :) 04/10 19:27 yeah 04/10 19:36 :) 04/10 19:42 I'm trying to figure out on how to access some implicit arguments 04/10 19:43 if you have 04/10 19:44 f : Set -> {P : Set} -> ... 04/10 19:44 then you use: 04/10 19:44 f A {P} ... = ... 04/10 19:44 can I pattern match on P? 04/10 19:44 even so..  I have this: 04/10 19:45 if it's an inductive 04/10 19:45 small-to-big : ? {a v} -> a ?* value v -> a ? v 04/10 19:45 ah.. no unicode here of course :) 04/10 19:45 fist ? is forall, the other one just ctor 04/10 19:46 if you use UTF-8 is should be finea 04/10 19:46 small-t-big : forall {a v} -> a -->* value v -> a => v 04/10 19:46 [] is one ctor for the _-->*_ type 04/10 19:47 and this works fine: 04/10 19:47 small-to-big [] = ? 04/10 19:47 but to write the term I need to access .v (the instance of v) 04/10 19:47 I tried small-to-big {a} {v} [] = ? 04/10 19:47 but then it complains 04/10 19:47 that it cannot verify that [] is of the correct type 04/10 19:48 what is the type of []? 04/10 19:48 _-->*_ 04/10 19:48 (disclaimer: I'm working on a problem set in Ulf's course at Chalmers) 04/10 19:49 I think that is not a type 04/10 19:49 data _-->*_ : Term -> Term -> Set where ... 04/10 19:49 it is just the list type over _-->_ (which is another type we have) 04/10 19:50 Arnar_: you've to use . to allow 'a' and 'v' to be constrained by the pattern matching on the constructor 04/10 19:50 Arnar: yeah so _-->*_ isn't a type then 04/10 19:50 Arnar_: small-to-big {.a} {.v} [] = ? 04/10 19:50 Saizan was getting to that... 04/10 19:50 fax: sorry :) 04/10 19:51 Saizan_: hmm.. it just says  a is not in scope 04/10 19:51 Saizan_: if it's not a type, what then? :) 04/10 19:51 Arnar you could ask Agda what the type of [] is 04/10 19:51 ok, hang on 04/10 19:51 only put the . at v then, it actually depends on how [] is defined 04/10 19:52 fax: it says _495 -->* _495   (when I ask about the type of []) 04/10 19:53 oh that's interesting 04/10 19:53 that means that a = v 04/10 19:53 Saizan_: just says v is not in scope then :/ 04/10 19:53 fax: yes.. well 04/10 19:53 they are different types 04/10 19:53 I guess there's too many things goin on at once for you to concentrate 04/10 19:53 but the ctors are overlapping 04/10 19:54 a = v means they are the same type 04/10 19:54 fax: a is a Term, and v is a Value 04/10 19:54 "value" lifts values from terms 04/10 19:55 and here  a = value v 04/10 19:55 doesn't look that way to me 04/10 19:55 http://www.cs.chalmers.se/ComputingScience/Education/Courses/types/agda-lecture/Bool.html 04/10 19:55 okay yeah what you said is true 04/10 19:57 still, what I really want now is what Saizan suggested, i.e. small-to-big {a} {.v} [] = ... 04/10 19:58 [] tells you that a = v 04/10 19:58 so try {a} {.a} or {.v} {v} or something like that 04/10 19:59 right, but they can be either true or false 04/10 19:59 hang on 04/10 19:59 ah 04/10 19:59 now we're getting somewhere 04/10 19:59 a != value v of type Term 04/10 19:59 when I do {v} {.v} 04/10 19:59 hmm 04/10 20:00 if I do {.v} {v} --- it says Value !=< Term of type Set 04/10 20:00 which I guess means Value is not a subtype of Term? 04/10 20:01 I have it 04/10 20:01 small-to-big {.(value v)} {v} [] = ? 04/10 20:02 then C-c C-c on v does the trick 04/10 20:02 :D 04/10 20:02 -!- byorgey_ is now known as byorgey 04/10 20:02 thanks fax, Saizan_ 04/10 20:02 why did I keep insisting that a = v :/   yeah it's a = value v 04/10 20:03 hehe :) 04/10 20:03 C-SPC is not a good key to use on OS-X :/ 04/10 20:05 Arnar_: btw, C-c C-e over an hole shows you the context 04/10 20:38 Saizan_: thanks. I've been using C-c C-, for the same result 04/10 20:42 agda2-give is C-c C-SPC... which I rebound to C-c Ent 04/10 20:43 --- Day changed Mon Oct 05 2009 -!- Saizan__ is now known as Saizan 05/10 02:19 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 It might be too higher order for the unification algorithm to figure out. 05/10 05:19 Oh, maybe it's ambiguous what type the first argument is, too. 05/10 05:22 No, I guess not. 05/10 05:23 well, the first argument to _$_\equiv_ needs to be (tvar -> type tvar) 05/10 05:23 coq can infer it without the annotation, it seems 05/10 05:23 If you do "t1 : _ -> _ -> _" which part turns yellow? 05/10 05:25 none 05/10 05:26 But it turns yellow if you don't put a type annotation in? 05/10 05:27 yes 05/10 05:27 if i just use _ it turns yellow 05/10 05:27 Weird. 05/10 05:28 What if it's just _ -> _? :) 05/10 05:28 yeah, it can't conclude it's a function of two argument? 05/10 05:28 That's hard to believe with "t1 v v'" in there. 05/10 05:28 no yellow with _ -> _ 05/10 05:29 Well, that's definitely weird. 05/10 05:30 I don't know if that's worth reporting or not. 05/10 05:31 I guess you might as well. 05/10 05:33 i wonder if it's small enough as it is 05/10 05:34 Well, you can remove most of the constructors, at least, I guess. 05/10 05:35 You can remove the \all part, too. 05/10 05:36 http://upload.wikimedia.org/wikipedia/commons/5/5c/TooManyPigeons.jpg 05/10 18:00 hi, 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 Are "yes" and "no" in scope? 05/10 18:56 Anyhow, I don't see anything obviously wrong there. 05/10 18:57 ah! 05/10 18:59 i always bump in some universe problem 05/10 21:06 it seems i can only embed the predicative subset of System F in agda, which is not that surprising actually 05/10 21:06 Fixed 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 Less is more: Coq is a complex beast 05/10 21:09 Saizan: You mean, embedding the language like an interpreter? 05/10 21:10 I suppose that wouldn't be too surprising. 05/10 21:10 dolio: yeah 05/10 21:10 though they don't seem to have this problem in coq 05/10 21:11 Are you doing it the same way? 05/10 21:11 Also, they have a sort of universe polymorphism in Coq, so that may make a difference. 05/10 21:11 Coq even has a flag to make Set impredicative, I think. 05/10 21:12 i think i'm doing it like here http://adam.chlipala.net/papers/PhoasICFP08/ , but i might be missing something 05/10 21:15 oh yeah that wont work in Agda 05/10 21:15 but the universe subtyping of Coq still keeps everything free of paradoxes? 05/10 21:16 nice http://www.cse.chalmers.se/~wouter/Talks/AIM%20X.pdf 05/10 21:26 Are they encoding an impredicative System F? I can't really tell. 05/10 21:26 well, foralled types are not in a distinct type 05/10 21:27 Yeah. But predicativity is about whether you can have 'forall a. T' and instantiate a to 'forall b. U'. 05/10 21:31 I guess you can do that? 05/10 21:31 Since you can substitute a type(T) in for a T? And 'forall b. U' is a type(T)? 05/10 21:32 well it seems like it allows 'a' to be instantiated by any SystemF's type, so also foralled ones 05/10 21:32 It's been a long time since I read this paper. 05/10 21:32 if i had a working coq installation i could try 05/10 21:33 the problem seems to be that typeDenote's result is of type Set here http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10465#a10465 05/10 21:34 while in agda i need Set1 because of the forall 05/10 21:34 I have Coq not Agda 05/10 21:35 T : Set? 05/10 21:35 in TAll? 05/10 21:35 yes 05/10 21:35 Maybe it uses impredicative Set? 05/10 21:35 it could be, yeah, i don't know much about coq 05/10 21:37 Adam always uses impredicative Set 05/10 21:37 I don't really understand how impredicative Set doesn't lead to the same paradoxes as Type : Type? 05/10 21:38 * Saizan neither 05/10 21:38 Or does it, and that's why they got rid of it (with the flag for turning it back on)? 05/10 21:38 well I think there are type theory experts that are not comfortable with it :) 05/10 21:39 Oh, looking at some faq, I guess that impredicativity does let you construct Hurkens' paradox. 05/10 21:40 So, there you go. 05/10 21:40 huh? 05/10 21:42 Saizan: 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 I don't think so 05/10 21:43 or just use Coq 05/10 21:43 Don't think what? 05/10 21:43 that impredicativity gives you hurkens 05/10 21:44 "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 Oh, I guess that's about something else. 05/10 21:46 You can't model classical mathematics soundly in Coq if it also has impredicative set, or something. 05/10 21:46 yes I beleive that's why they made it optional 05/10 21:46 Isn't double-negation of excluded middle always provable, though? 05/10 21:49 aha! I see what you're saying 05/10 21:50 classical logic is a fragment of intuitionistic: So if we can't model classical then intuitionistic should break down too 05/10 21:50 Well, that wasn't what I was thinking, but that certainly sounds good. :) 05/10 21:51 ~~(P \/ ~P) is a theorem in Coq 05/10 21:51 Right. And if impredicativity implies ~(P \/ ~P)... 05/10 21:51 well the thing is: I haven't really understood this Hurkens stuff properly... just skimmed it years ago 05/10 21:51 but anyway that file you mentioned is not impredicative Set so much as having a bijection from Prop to bool 05/10 21:52 (maybe I should have said ~~(P \/ ~P) is a theorem in CoC) 05/10 21:56 Yeah, I don't really understand how to use that file, either. 05/10 21:57 Oh, but... 05/10 21:59 That file assumes {A} + {~ A} and proves False. 05/10 21:59 Which gets you ~ ({A} + {~ A}), right? So if you have ~~({A} + {~ A}), those two get you False? 05/10 22:00 "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 Is that equivalent to impredicative set? 05/10 23:29 since you can then instantiate the A with "(A : U) -> T(A)" it looks like it to me 05/10 23:33 Yeah. 05/10 23:33 where is that cited from? 05/10 23:35 The article on types (I think) on plato.stanford.edu. 05/10 23:36 http://plato.stanford.edu/entries/type-theory/ 05/10 23:36 Toward the end. 05/10 23:36 Searching for Hurkens is an easy way to find it. 05/10 23:37 found it, thanks 05/10 23:38 I'm a bit confused by their wording, though. 05/10 23:38 It says Girard "obtained his paradox" from that system, but also proved normalization for the type system. 05/10 23:39 maybe the paradox is only there in classical type theory? if there's one 05/10 23:46 crushed.. 05/10 23:50 Hurkens' paper on the subject seems to be behind a pay wall. 05/10 23:52 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3153 05/10 23:53 And I got Coquand's, but the mathematical symbols are all jumbled together. 05/10 23:53 this is good but very hard going 05/10 23:53 www.cs.chalmers.se/~coquand/paradox.ps 05/10 23:53 Same with that one. 05/10 23:54 which paywall? 05/10 23:55 Springer link or ACM. 05/10 23:55 --- Day changed Tue Oct 06 2009 no pdf link on ACM, sadly 06/10 00:00 http://www-cgi.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/hurkens95tlca.pdf <- from google scholar 06/10 00:02 Ah, nice. 06/10 00:03 (in the process i found that the first result for type theory is about typography, on google) 06/10 00:15 hehe 06/10 00:15 "Type Theory is a journal of contemporary typography" 06/10 00:15 Man, Hurkens' PTS rules only have two elements instead of three. 06/10 00:34 Apparently all the rules are of the form (s,t,t). 06/10 01:02 Oh, I guess that's what makes it impredicative. 06/10 01:16 So, fiddling with the Hurkens stuff, it seems like you need one more level of impredicativity before you get inconsistency. 06/10 07:34 one more level? 06/10 07:36 so, e.g. not just impredicativity for Set but also Set1? 06/10 07:37 Yes. 06/10 07:37 I mean, that should certainly be sufficient, because that's what they have in the paper. 06/10 07:40 The paper has star, box and triangle. 06/10 07:40 With the rules (*,*,*) ([],[],[]) and ([],*,*), the last one being impredicative (I think). 06/10 07:42 And that's consistent. 06/10 07:42 And they get inconsistency when they add (tri,[],[]). 06/10 07:42 The hierarchy being * : [] : tri, incidentally. 06/10 07:43 i see, and this is all without inductive types, right? 06/10 07:43 Yeah, it's just a pure type system. 06/10 07:44 So, it would seem that you can have impredicative rules for Set, as long as everything above set is stratified appropriately. 06/10 07:44 Unless there's some undiscovered paradox out there. 06/10 07:45 -!- jfredett_ is now known as jfredett 06/10 07:45 heh 06/10 07:47 another interesting thing would be an explanation of the inconsistency while keeping strong normalization bit 06/10 07:48 Yeah, 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 Er, rule, not axiom. 06/10 07:52 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 types 06/10 07:53 Well, that's good to know. 06/10 07:55 (it's a bit unsatisfactory that the chapter itself is not much more than an overview on the subject) 06/10 07:56 I was kind of disappointed that existential types had to live in Set1 in Agda when I first found it out. 06/10 07:56 by existentials you mean like in System F, right? 06/10 07:58 Like in haskell. 06/10 07:59 k, i was also surprised by polymorphic types being in Set1, today 06/10 08:00 If Set were impredicative, you could define it as: ∃ P = ∀(r : Set) → (∀ a → P a → r) → r 06/10 08:01 ∃ : (Set → Set) → Set 06/10 08:01 where are the rules for this universe hierarchy written down? 06/10 08:04 And, of course, you can't have the equivalent of 'data Foo = Foo (forall a. P a)' either. 06/10 08:05 Which? 06/10 08:05 agda ones 06/10 08:05 Agda'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 "∃ 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) -> Set2 06/10 08:07 The lambda cube's rules for function spaces look like: (*,*,*) (*,[],[]) ([],*,[]) ([],[],[]). 06/10 08:08 Where * : []. 06/10 08:08 So, 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 ah, i see, so in this case i'd get the maximum of Set1 and Set1 06/10 08:10 So, there (∀ a → P a → r) : Set1, and r : Set, so (∀ a → P a → r) -> r : max(Set1,Set) = Set1. 06/10 08:10 And then, yeah, max(Set1,Set1). 06/10 08:10 But (Set -> Set) -> Set1 : Set2. 06/10 08:10 -!- opdolio is now known as dolio 06/10 18:53 copumpkin: FYI, NAD informed me that using "True (coprime ...)" isn't just for making '4 % 5' easy. 06/10 20:17 oh? 06/10 20:17 Apparently it makes the representation unique, whereas "Coprime num den" wouldn't. 06/10 20:18 Provably unique, that is. 06/10 20:18 hrm 06/10 20:18 Which lets you use _==_ instead of an extensional, setoid equality. 06/10 20:18 oh 06/10 20:19 I can sort of see that, I think 06/10 20:19 * Saizan needs an hoogle for agda 06/10 20:40 where is True from? 06/10 20:40 Relation.Nullary.Decidable 06/10 20:45 thanks 06/10 20:46 fax: What do you use to write Coq? 06/10 20:50 Proof General 06/10 20:51 (3 window mode & electric terminator) 06/10 20:51 I'd recommend it to people too if there wasn't this stupid vim/emacs thing people can't seem to get around 06/10 20:52 Oh, proof general is emacs? 06/10 20:54 it runs inside emacs 06/10 20:54 Okay. Well, that'll probably work out well. 06/10 20:55 I tried coqide once before, and it confused the hell out of me. 06/10 20:55 oh no, we're losing dolio to coq 06/10 21:03 Well, I was trying to figure out that Hurkens stuff yesterday. 06/10 21:03 Agda has nothing comparable to -impredicative-set. 06/10 21:04 And programming directly in coqtop isn't very nice. 06/10 21:04 :/ 06/10 21:12 worse than the emacs/vim is the "My language" thing 06/10 21:12 Well, quite frankly, I can't stand Coq's syntax. 06/10 21:19 That may be superficial, but whatever. 06/10 21:19 it feels very old-school 06/10 21:19 maybe we should make an agda-to-coq compiler 06/10 21:19 I have the same problem with MLs. 06/10 21:20 syntax doesn't matter 06/10 21:23 It does to me. 06/10 21:23 fax: there are definitely more important things, but bad syntax is off-putting 06/10 21:24 --- Day changed Wed Oct 07 2009 what do you use as constructor name instead of \lambda when embedding some LC? 07/10 02:03 -- inferred, id : term (Π (λ x → inj (Var x) ⇒ inj (Var x))) id = Λ λ a -> Lam {inj (Var a)} λ x -> Var x 07/10 02:36 yay for predicative System F2 phoas style 07/10 02:36 Which part got inferred? 07/10 02:38 The Pi part? 07/10 02:39 oh, irssi put it on a line, the signature above however 07/10 02:39 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10515#a10515 07/10 02:41 i should test type application before declaring victory, i guess 07/10 02:42 Nice. 07/10 02:49 Is this PHOAS style? 07/10 02:50 yeah, terms are parametric in the representation of variables 07/10 02:50 i've just realized that i need something at the value level to convert between terms of type "inj x" and "x" though 07/10 02:51 People 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 and cast/cast' look like there should be a better way 07/10 02:52 Namely that a naive HOAS type has values that don't correspond to lambda terms. 07/10 02:52 yeah 07/10 02:52 and it's also easier to do some kinds of conversions 07/10 02:53 Yeah, and they gave the impression that the two facts are related, but I don't really grok how that is. :) 07/10 02:54 aside from the fact that you get both by parametricity? 07/10 02:55 and you also have an explicit Var constructor 07/10 02:55 Well, 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 Even 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 A 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 And 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 ah, i see, the question is if you could have one without the other, somehow 07/10 03:10 having 1-to-1 without analysis, since the other case is known 07/10 03:12 it'd need to be a non-computable bijection, basically 07/10 03:13 I 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 Although, you can't really analyze the exotic terms. 07/10 03:13 Because 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 So your analysis may be wrong. 07/10 03:14 true 07/10 03:14 He 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 Which you could probably do for the completely opaque version, too. 07/10 03:15 But it'd still be useless. 07/10 03:15 it'd be nice if the compiler could use agda proofs to help it optimize code 07/10 05:32 sounds hard though 07/10 05:32 hi 07/10 16:51 i got a problem with the following code which i don't understand how to solve: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10524#a10524 07/10 16:52 i'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 secs 07/10 17:07 -!- pumpkin_ is now known as copumpkin 07/10 20:05 -!- opdolio is now known as dolio 07/10 22:22 --- Day changed Thu Oct 08 2009 seanmcl: what happens if you leave out what's after the =? 08/10 01:13 -!- copumpkin is now known as pumpkin 08/10 01:54 i wonder if i can code a phoas HM where the types of the terms get inferred 08/10 02:08 That'd be pretty impressive, but I wouldn't bet on it. 08/10 02:15 yeah, even though i can omit some annotations required in normal Church style for my system F2 08/10 02:17 -!- Saizan__ is now known as Saizan 08/10 07:00 * Saizan wants pattern matching under lambda 08/10 07:14 hey there 08/10 13:11 is there any way the agda parser can parse y into <_>_? I mean, without having all the whitespace in < x > y ? 08/10 13:12 Arnar: how would it know that y should be parsed that way, and not just as a single identifier? 08/10 13:17 IIUC Agda doesn't make a distinction (like Haskell does) between operator and non-operator symbols. 08/10 13:17 byorgey: 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 ah, not that I am aware of 08/10 13:29 byorgey: 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 Arnar: heh, that would be super-duper confusing. =) 08/10 17:45 --- Day changed Fri Oct 09 2009 -!- opdolio is now known as dolio 09/10 02:22 -!- copumpkin is now known as c0w 09/10 03:37 twelf is rather different than I was expecting. 09/10 03:43 how so? 09/10 03:43 Well, it's an implementation of the LF logical framework, which is a dependently typed lambda calculus. 09/10 03:44 But, it doesn't use lambda calculus-like computation. 09/10 03:44 Instead, it uses LF for defining term languages, and logic programming with induction over that term structure for computation. 09/10 03:45 So 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 At least, from what little I know of lambda prolog. 09/10 03:46 hmm, /me doesn't know prolog 09/10 03:49 I keep meaning to learn it 09/10 03:49 -!- c0w is now known as copumpkin 09/10 03:49 Not prolog, lambda prolog. 09/10 03:49 Prolog doesn't have types. 09/10 03:49 well, I don't know that one either :) 09/10 03:49 :) 09/10 03:50 Anyhow, 't -> o' is the type of a unary prediate on ts. Etc. 09/10 03:50 And, say, plus would have the type 'nat -> nat -> nat -> o'. 09/10 03:51 plus(z,n,n). plus(s m,n,s o) :- plus(m,n,o). 09/10 03:52 Or something like that. 09/10 03:52 o 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 plus(s M, N, s O) :- plus(M,N,O). 09/10 03:53 lambda prolog has higher order unification built into it 09/10 03:54 You'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 Unless you're formalizing arithmetic. 09/10 03:56 -!- elliottt_ is now known as elliottt 09/10 18:21 -!- opdolio is now known as dolio 09/10 21:06 -!- kosmikus_ is now known as kosmikus 09/10 21:49 hey dolio 09/10 23:32 --- Day changed Sat Oct 10 2009 Yes? 10/10 00:51 here is a book on predicative arithmetic http://www.math.princeton.edu/~nelson/books/pa.pdf 10/10 00:51 Does it explain where the word "predicative" came from? 10/10 00:52 not the etymology no 10/10 00:56 Ah well. 10/10 00:56 Someone asked me that the other day, and I have no idea what the answer is. 10/10 00:56 maybe it comes from early set theory 10/10 00:57 -!- opdolio is now known as dolio 10/10 08:23 http://www.cs.chalmers.se/~miquel/lect1.ps -- http://www.cs.chalmers.se/~miquel/lect[234].ps 10/10 16:31 Type Theory: Impredicative Part 10/10 16:31 nice 10/10 17:15 --- Day changed Sun Oct 11 2009 Is it just me, or are those slide upside-down? 11/10 01:00 just you 11/10 01:00 to me, they are sideways 11/10 01:00 Heh. 11/10 01:00 -!- koninkje1away is now known as koninkje_away 11/10 02:46 -!- Smurfen_ is now known as Smurfen 11/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 secs 11/10 18:03 --- Day changed Mon Oct 12 2009 -!- eelco_ is now known as eelco 12/10 07:34 -!- pumpkin_ is now known as pumpkin 12/10 19:15 -!- pumpkin is now known as copumpkin 12/10 21:21 dolio: 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 constructions 12/10 21:26 turned out the problem was indeed eta-expansion of record types 12/10 21:27 after replacing all records with equivalent data definitions and custom eliminators, type checking finally became feasible again 12/10 21:28 Huh. 12/10 23:30 The problem with mine ended up being pretty weird. 12/10 23:30 from the logs i jugde you began coding your own type theory system? 12/10 23:34 Oh, 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 from the logs i jugde you began coding your own type theory system? 12/10 23:36 uh, sorry for the double post 12/10 23:42 :) 12/10 23:42 anyway, now i can typecheck horizontal composition of natural transformations in 10s as opposed to a heap overflow after 10 min 12/10 23:43 Wow. 12/10 23:43 i wonder if it would be hard to hack the agda source to disable eta expansion for record types 12/10 23:44 it is a bit awkwards defining all those custom datatypes 12/10 23:44 Well, possibly. That could possibly screw up type checking, though. 12/10 23:46 Assuming you're proving equalities that rely on eta for records. 12/10 23:47 well, that i would not, of course 12/10 23:49 I just mean it might not be easy to avoid that. 12/10 23:50 Since you can't inspect records by matching to see if they're equal, like data. 12/10 23:50 i am using setoids anyway 12/10 23:51 Oh right. 12/10 23:51 Never mind, then. :) 12/10 23:51 e. 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 equivalent 12/10 23:52 and their maps are equal, if they are extensionally equal 12/10 23:52 and so on 12/10 23:52 equal -> equivalent 12/10 23:52 Right. 12/10 23:52 --- Day changed Tue Oct 13 2009 -!- ksf_ is now known as ksf 13/10 06:07 -!- kosmikus_ is now known as kosmikus 13/10 08:47 -!- Smurfen_ is now known as Smurfen 13/10 10:10 -!- opdolio is now known as dolio 13/10 11:03 --- Day changed Wed Oct 14 2009 -!- pumpkin is now known as anapumpkin 14/10 00:17 -!- anapumpkin is now known as pumpkin 14/10 00:52 -!- ksf_ is now known as ksf 14/10 06:06 -!- opdolio is now known as dolio 14/10 11:20 hi 14/10 20:50 hi stevan 14/10 21:17 this new rewrite construct looks interesting 14/10 21:18 oh my god! they're adding MORE complications to Agda 14/10 21:19 'magic with' wasn't bad enough! 14/10 21:19 yes, I'm a bit sceptic as well 14/10 21:20 admittedly looks interesting, but I'm not sure if we need more ad-hoc constructs 14/10 21:21 what's new? 14/10 21:53 http://permalink.gmane.org/gmane.comp.lang.agda/1154 14/10 21:53 ok, now being back to runtime and memory problems (when typechecking setoid composition for comma categories) 14/10 22:14 ;S 14/10 22:15 i know agda uses normalization by evaluation, which automatically generates eta-long forms 14/10 22:20 but i think i do not need eta-expansion for dependent function types at all 14/10 22:20 i wonder if there would be a more efficient type checking strategy 14/10 22:21 ecst Coq doesn't have eta-expansion :P 14/10 22:21 It's really irritating 14/10 22:21 it matters to me 14/10 22:21 yeah, but i find the impredicative metatheory of coq a bit strange 14/10 22:21 I would love to find it strange but I still don't understand the meaning of predicativity etc well enough 14/10 22:22 been trying to read a bit into it 14/10 22:22 ok, i meant not strange but rather constructively less appealing 14/10 22:23 oh why is that? 14/10 22:23 only Prop is impredicative in coq 14/10 22:28 Set isn't anymore 14/10 22:28 ah, that is nice 14/10 22:28 fax: for example, you cannot have the (standard) set model in an impredicative calculus 14/10 22:29 what does that mean? 14/10 22:29 a model is an assignment of "real" mathematical objects to given syntax 14/10 22:30 you mean can't interpret set theory into impredicative? 14/10 22:30 or interpret the impredicative calculus into set theory? 14/10 22:30 latter 14/10 22:31 curious 14/10 22:37 -!- Saizan_ is now known as Saizan 14/10 22:46 -!- byorgey_ is now known as byorgey 14/10 22:48 --- Day changed Thu Oct 15 2009 -!- codolio is now known as dolio 15/10 01:14 -!- FunctorSalad_ is now known as FunctorSalad 15/10 12:03 An impredicative type-level is quite handy when you're working with just lambda terms. 15/10 13:20 i guess it let you do things you'd need explicitly recursive types for instead? 15/10 13:21 Church encoding anything bumps it up a level. 15/10 13:22 So, like Bool ends up in Set1, even. And then you can't write "not b = b Bool false true". 15/10 13:23 ah, right 15/10 13:23 Of 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 http://code.haskell.org/~dolio/pts/itower.pts 15/10 14:19 Woo! 15/10 14:19 dolio: what's that? 15/10 15:07 oh, a PTS implementation? 15/10 15:08 neat. 15/10 15:08 --- Day changed Fri Oct 16 2009 -!- eelco_ is now known as eelco 16/10 12:24 --- Day changed Sat Oct 17 2009 can anyone point me to the syntax for mutually inductive data types (if that is possible)? 17/10 00:07 mutual 17/10 00:08 data A ... 17/10 00:08 data B ... 17/10 00:08 you can also have recursive functions in there 17/10 00:08 so Agda has induction recursion? 17/10 00:08 (ind-rec I mean, as well as non ind-rec) 17/10 00:09 roconnor, 17/10 00:09 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers 17/10 00:09 look at the bottom has a nice example 17/10 00:09 THE example :P 17/10 00:10 so you don't have to say mutual for mutual data types? 17/10 00:12 I think you do ? 17/10 00:13 ah 17/10 00:14 ok 17/10 00:14 should I install emacs or xemacs? 17/10 00:16 roconnor 17/10 00:17 hmm, xemacs doesn't appear to be packaged for me, so emacs it is I guess 17/10 00:17 is this about SillyTree? 17/10 00:17 :P 17/10 00:17 yes 17/10 00:17 I bet I can do it in Agda 17/10 00:18 what's the value of that 17/10 00:18 ? 17/10 00:18 But I suppose I should verify this claim 17/10 00:18 oh right 17/10 00:18 to prove that coq sucks and they should make it better or everyone will move to Agda 17/10 00:18 you're kidding? 17/10 00:19 or to prove that Agda is unsound and everyone should move to coq 17/10 00:19 lol 17/10 00:19 I exagerate 17/10 00:19 *sigh* I have to learn emacs and agda 17/10 00:23 btw 17/10 00:24 Inductive SillyTree (p : bool) : Type := 17/10 00:24 | leaf : p = true -> SillyTree p 17/10 00:24 | node : p = false -> forall b, SillyTreePair b -> SillyTree p 17/10 00:24 with SillyTreePair (p : bool) : Type := 17/10 00:24 | stp : SillyTree p -> SillyTree p -> SillyTreePair p. 17/10 00:24 maybe that's not ussble though 17/10 00:24 I'm ont very sure 17/10 00:24 lots of subst. needed to use it probablyars 17/10 00:25 er, does Agda not have type families? 17/10 00:25 roconnor that was Coq :P 17/10 00:25 oh ya, good idea, but doesn't scale to my actual problem unfortunately 17/10 00:26 :( 17/10 00:26 Adga has type families 17/10 00:27 I thought so 17/10 00:27 damn it why dosn't this agda mode go 17/10 00:27 roconnor I don't know a lot about syntax but I'm just curious what you're actually doing ? 17/10 00:28 I'm trying to define the sytax for this logic langauge called Chiron developed for the MathScheme project at McMaster 17/10 00:28 well define the syntax and semantics 17/10 00:28 starting with the syntax 17/10 00:29 dammmn I never heard of this 17/10 00:29 It is very new 17/10 00:29 woow looks really interesting 17/10 00:32 best thing to read to start is: Chiron: A Multi-Paradigm Logic ? 17/10 00:33 probably 17/10 00:33 it's a bit fuzzy 17/10 00:33 but maybe I good start 17/10 00:34 File mode specification error: (file-error "Cannot open load file" "haskell-indent") 17/10 00:35 what's that formal math wiki ? 17/10 00:37 the one with your calculator on it 17/10 00:37 I don't know ... mathwiki? 17/10 00:37 thanks 17/10 00:37 agda mode requires haskell-indent? weird 17/10 00:38 GRRR 17/10 00:39 mathwiki doesn't have agda 17/10 00:39 or maybe it's something else you've in .emacs? 17/10 00:39 ya, that would save me a bunch of trouble 17/10 00:39 Saizan_: I think it requires haskell-indent 17/10 00:39 "agda-mode setup" made it work out of the box for me, but i had haskell-mode already installed 17/10 00:42 how did you get haskell-mode installed? 17/10 00:43 i installed emacs-haskell-mode from my distro 17/10 00:44 roconnor 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 yes 17/10 00:44 er 17/10 00:44 classical set theory 17/10 00:44 http://haskell.org/haskellwiki/Haskell-mode <- but you can get it from the repo too 17/10 00:45 oh use Benjamin Werners work? 17/10 00:45 I have it installed 17/10 00:45 fax: yes 17/10 00:45 awesome!!!!!!!!!!!!!! 17/10 00:45 but presumably I have to do something to my .emacs file 17/10 00:45 roconner danm you get the really interesting stuff to do 17/10 00:45 that part -> (load "/path/to/haskell-mode/haskell-site-file") 17/10 00:45 no, wait 17/10 00:46 well, maybe it's enough 17/10 00:46 ugh 17/10 00:47 * roconnor searches his nix store for a haskell-site-file 17/10 00:47 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 (load "haskell-site-file") might be enough, it's in the load-path 17/10 00:48 and i'd expect a distro package to make it so 17/10 00:49 I've learned not to expect too much from nix yet 17/10 00:51 hmm, somehow I didn't manage to install it 17/10 00:52 s/it's in the load-path/if it's in the load-path/ -- tbc 17/10 00:53 it is in .nix-profile/share/emacs/site-lisp/ 17/10 00:53 now 17/10 00:53 load it giving the full path then :) 17/10 00:55 oooh, pretty colours 17/10 00:56 yeah! 17/10 00:56 and latex-like unicode input 17/10 00:56 type theory: Now in glorious technicolor 17/10 00:56 (there are some shortcuts) 17/10 00:56 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput 17/10 00:57 curly braces for forall? 17/10 00:59 roconnor so you index by a bool to say if the term contains eval or not? 17/10 00:59 roconnor: curly braces are for implicit arguments 17/10 01:00 I think it is better to count the evals in some fashion 17/10 01:00 and forall is for when you don't want to give the type 17/10 01:00 oh?? 17/10 01:00 i.e forall a -> t, is the same as (a : _) -> t, where _ is filled by inference 17/10 01:01 ah needed more spaces 17/10 01:01 heh 17/10 01:03 Agda insists that it knows one of my parameters is true 17/10 01:03 done 17/10 01:04 comment syntax is like Haskell? 17/10 01:05 yes 17/10 01:05 does Agda extract to Haskell? 17/10 01:06 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo <- it seems so 17/10 01:07 It is tempting to do this in Agda 17/10 01:08 it seems much nicer for dependently typed programming than Coq 17/10 01:09 well of course ... it has K and eta 17/10 01:09 even if it didn't have K or eta 17/10 01:09 it'd be awful if it didn't :P 17/10 01:09 like how it insisted that my parameter was actually the value true. 17/10 01:10 that was nice 17/10 01:10 you mean in coq you don't get refinements when you pattern match on a gadt? 17/10 01:10 I call it dependent case analysis 17/10 01:11 it's basically case but you can fiddle a bit 17/10 01:11 not proper pattern matching in any case 17/10 01:12 Saizan_: let me check 17/10 01:12 fax: uhm, what would be proper pattern matching? 17/10 01:13 Saizan_: Just like Agda or Epigram 17/10 01:13 ah, ok, i misread 17/10 01:13 maybe I should have said dependent pattern matching 17/10 01:13 Saizan_: well, coq at least lets me put impossible patterns into my analysis 17/10 01:14 I'm trying to check if it requires me to put in impossible patterns, but I think it does 17/10 01:14 ya I think it will 17/10 01:15 because nested patterns presumably are translated into nested non-dependent case statement 17/10 01:15 you put () 17/10 01:15 so the dependent parameters are simply generalized away into to new free variables 17/10 01:16 fax: sometimes the depedent types don't allow you to put even () 17/10 01:17 oh I don't know exactly the situation you mean 17/10 01:17 fax: and you are forced to instead put in a proof that the case is impossible. 17/10 01:17 oh right yes 17/10 01:17 False_rec (...) 17/10 01:17 that is a general theorem though 17/10 01:17 I mean dependent pattern matching can't always know 17/10 01:17 sure 17/10 01:18 but intrestingly when Agda does know it makes you 17/10 01:18 from my 10 min experience with Agda so far 17/10 01:18 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 you 17/10 01:21 how do I make a goal? 17/10 01:25 you put a "?" and reload 17/10 01:26 where the proof should go 17/10 01:27 oh, maybe that doesn't work for patter 17/10 01:27 eh, no 17/10 01:27 only in expressions, afaiu 17/10 01:27 ah 17/10 01:28 getting it now 17/10 01:28 sillyFunction (node true (stp .true leaf leaf)) = true 17/10 01:30 what does the . mean in .true ? 17/10 01:30 mean that it's inferred from the rest of the patterns 17/10 01:30 s/mean/it means/ 17/10 01:30 i.e, given the other patterns it has to be true 17/10 01:31 wierd 17/10 01:31 heh, I can move the dot around 17/10 01:31 but I can't remove it 17/10 01:31 I can even dot both trues 17/10 01:32 okay, that was fun 17/10 01:32 Coq sucks 17/10 01:32 you could declare those arguments as implicit maybe, so they don't have to appear 17/10 01:33 probably 17/10 01:33 lol 17/10 01:34 heh Coq sucks :) 17/10 01:34 can interesting programs, not just proofs, be written in agda? like a compiler for a simple language 17/10 01:37 jlaire: it's the programs you can write -- the proofs you cant :P 17/10 01:38 fax: why not? 17/10 01:38 no tactics make it too difficult 17/10 01:38 hmm, ok :P 17/10 01:38 ah, i guess 17/10 01:38 there's a separate tool that does proof search, but it's quite new it seems 17/10 01:39 I presumed we were supposed to do all proofs in Adga via reflection 17/10 01:39 does reflection means "write down the proof terms"? 17/10 01:40 well theer is that and there is also some really nice modules for program derivations and equational proofs 17/10 01:40 no it means write a little dsl and write a program to solve your program and then intepret that dsl into your semantic domain 17/10 01:41 solve your problem 17/10 01:41 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 way 17/10 01:43 that doesn't solve the problem of needing to write proofs in agda 17/10 01:43 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 this 17/10 01:45 that would be the idea 17/10 01:45 I don't think this is actually done 17/10 01:45 i'd like to see some examples of that 17/10 01:46 me too 17/10 01:46 there's some in the standard library 17/10 01:46 I'd be cool 17/10 01:46 Ring solver or something 17/10 01:47 it proves stuff like x + y = y + x 17/10 01:47 /nick SillyTree 17/10 05:04 ;) 17/10 05:04 :o 17/10 05:05 -!- opdolio is now known as dolio 17/10 06:39 weird everyone is using agda these days.. 17/10 19:58 :O 17/10 19:59 can I call into Haskell libraries from Agda? 17/10 20:01 yes byorgey 17/10 20:01 there is a good example of this, 17/10 20:01 http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/ 17/10 20:02 thanks fax. 17/10 20:02 --- Day changed Sun Oct 18 2009 is it possible to do PHOAS in Agda 2 now? 18/10 01:12 what's the P? 18/10 01:13 http://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf 18/10 01:13 that name sounds familiar 18/10 01:13 isn't he smerdyakov or something? 18/10 01:13 has anyone done this in Agda? 18/10 01:13 dammit why the hell can't I use ∀ :/ 18/10 02:12 ∃ 18/10 02:13 fax: i've done the predicative System F in that style 18/10 02:30 cool what did you do with it? 18/10 02:30 nothing :D 18/10 02:30 can you post it please? 18/10 02:31 k 18/10 02:31 it's a bit messy maybe: http://code.haskell.org/~Saizan/SystemFpred.agda 18/10 02:33 I wrote this much btw http://pastie.org/659143 18/10 02:33 i managed to write the interpretation into agda types 18/10 02:34 well you have proved strong normalization of F :P 18/10 02:34 heh 18/10 02:34 yeah :) 18/10 02:35 i had to use cast/cast' as a way to avoid an extensionality axiom 18/10 02:35 it'd be nice if we could find a cleaner way 18/10 02:35 oh, also "inj" is something i'd like to avoid 18/10 02:36 huuughhh 18/10 02:36 I have to install the agda lib 18/10 02:36 well, you can define the standard Boolean and equality types instead 18/10 02:37 and T 18/10 02:37 it's not hard to install the lib though :) 18/10 02:38 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 hope 18/10 02:41 -!- pumpkin is now known as copumpkin 18/10 04:44 -!- opdolio is now known as dolio 18/10 09:29 -!- Saizan_ is now known as Saizan 18/10 09:54 -!- opdolio is now known as dolio 18/10 19:58 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 following 18/10 20:35 locations: ~/lib-0.2/src/Data/Nat.agda ~/lib-0.2/src/Data/Nat.lagda 18/10 20:35 have you downloaded the standard library? 18/10 20:35 but if I do: less ~/lib-0.2/src/Data I can see Nat.agda . Is this a known problem? 18/10 20:36 yes 18/10 20:36 try expanding the ~ 18/10 20:36 Hm. That's an improvement. Now it just complains Nat is not in scope. 18/10 20:38 I'm working through "Dependently Typed Programming in Agda". Is this pre-agda2? 18/10 20:40 no 18/10 20:41 Hm. It mentions the summer school library module Data.Nat. Perhaps the standard library has changed since then? 18/10 20:42 ohh 18/10 20:42 I think they changed to use ? instead of Nat 18/10 20:42 I'll browse the source 18/10 20:42 ℕ 18/10 20:42 Thanks FunctorSalad - that does the trick 18/10 20:43 nobody got my joke -_- 18/10 20:43 Is that supposed to pun a face with an infix underscore operator? 18/10 20:44 --- Day changed Mon Oct 19 2009 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10903#a10903 19/10 04:31 * dolio goes to get some much-needed sleep. 19/10 04:32 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 what's the message? 19/10 14:41 Failed to infer the value of dotted pattern when checking the pattern .n has type \Bbb{N} 19/10 14:42 Well, it didn't say \Bbb{N} 19/10 14:42 I'm trying to do exercise 3.1 19/10 14:50 Is there a way I can post my attempt so far, so someone can explain what I'm doing wrong? 19/10 14:51 Perhaps i should try joinging the mailing list, and ask there? 19/10 14:54 use hpaste.org 19/10 14:55 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10913#a10913 19/10 14:57 colin_: I think those should be ".(n + suc k)" based on the constructors of Compare. 19/10 15:12 Also, you need an n that isn't dotted in each case, I believe. 19/10 15:13 Thanks dolio - I understand now, and I have got it pass the type checker. 19/10 15:16 Since a .e that contains a variable is expected to have that variable matched elsewhere. 19/10 15:16 How do I write a main function to print a Nat to stdout? 19/10 16:54 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 I vaguely remember that there are two IOs 19/10 19:42 If I import IO.Primitive instead of IO, then it doesn't type check. 19/10 19:45 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 I'd like to know how to use the IO standard library instead. 19/10 19:53 I do remember having the same problem as you, but can't remember what to do to fix it 19/10 19:53 Oh well, I'll learn - slowly. 19/10 19:56 -!- English_Gent is now known as EnglishGent 19/10 20:35 So, what do we think about types like { i : Level, A : Type[i] | A }? 19/10 20:51 I am not sure what that syntax is supposed to mean 19/10 20:53 something like { i : Level | { A : Type[i] | A } } ? 19/10 20:53 Yeah, right-nested dependent sum. 19/10 20:54 so you must have cumulativity for that type to be inhabited? 19/10 20:54 What do you mean by that? 19/10 20:56 oh no I am talking nonsense 19/10 20:56 sorry yeah I understand the type now: shouldn't it be a type error? 19/10 20:57 oh, actually Type[i] : Type[i+1] 19/10 20:57 { i : Level | { A : Type[i] | A } } : Type[?] 19/10 20:57 Its type is Type[omega], which is outside the quantification power of Level. 19/10 20:58 are you allowed to do that? :P 19/10 20:58 That's how I've been typing Pi types like '(i : Level) -> Type[i]' as well. 19/10 20:58 There's one extra level above the predicative hierarchy, kind of like box in the CoC. 19/10 20:59 So I thought: why not have it for strong sums, too? 19/10 20:59 sounds a bit scary 19/10 21:00 { i : Level | { A : Type[i] | A } } is roughly the disjoint union of all types except Type[omega], I think. 19/10 21:00 Yeah, it does sound scary. :) 19/10 21:01 For instance, skimping on the notation (which is really verbose for dependent tuples)... 19/10 21:04 < 0, List Nat, [1,2,3] > is an element. 19/10 21:04 And < 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 RichardO 20/10 06:50 i'm having some trubles solving a problem im having can anyone help? 20/10 07:57 is anyone on here? 20/10 07:57 let's hear the question :) 20/10 07:57 Let F:B->C and G:A->B be functions 20/10 07:58 prove that if F is injective and G is injective then F o G is Injective 20/10 07:58 any idea? 20/10 07:58 So far i got 20/10 07:58 (F o G)(X)=F(G(x)) 20/10 07:59 (F o G)(X1) isn't equal to (F o G)(x2) 20/10 07:59 cause X1,X2 are elements of A: X1 isn't equal to X2, F(x1) isn't equal to F(x2) 20/10 08:01 am i on somewhat the right track? 20/10 08:01 I'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 sense 20/10 08:04 ... 20/10 08:04 there's an Injective in the standard libraries? 20/10 08:19 nope, but I gotta say, that's a pretty trivial proof 20/10 08:20 unless I messed something up 20/10 08:20 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10934#a10934 20/10 08:23 I guess it is 20/10 08:23 -!- eelco_ is now known as eelco 20/10 10:08 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10934#a10934 20/10 16:31 that's very nice 20/10 16:31 fax: thank you! 20/10 17:06 That's an unusual definition of Injective. 20/10 17:15 I don't think injective is worthwhile in constructive math 20/10 17:21 You mean the idea in general, or that formulation. 20/10 17:22 as a general concept 20/10 17:22 (do prove me wrong :P) 20/10 17:25 Well, I have no idea. 20/10 17:25 I 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 Only a doubly-negated version. 20/10 17:26 aha 20/10 17:26 that makes sense 20/10 17:26 we don't get f^-1 from a (f x == f y -> x == y) proof though 20/10 17:26 I was debating which of the two to use and the one I wrote seemed to fit what the original dude was asking 20/10 17:27 I started writing it for him but then he disappeared 20/10 17:27 http://code.haskell.org/~dolio/agda-share/injective/html/Functional.html 20/10 17:28 zomg 20/10 17:29 whatever I do dolio has already done! 20/10 17:29 (and better) 20/10 17:30 Heh. I did that in response to some blog post by someone a while back. 20/10 17:30 That's how I discovered that all functions were provably injective in agda at the time. 20/10 17:30 oh :) 20/10 17:30 hm 20/10 17:41 can you actually prove something injective without producing an inverse function?? 20/10 17:46 (yes) 20/10 17:48 I wonder what they do in constructive category theory 20/10 18:01 (partial setoids) 20/10 18:06 zomg I proved composition of injectiveness dolio's way too! 20/10 20:09 so l33t 20/10 20:09 (I need to prove simple things because I'm incapable of proving more complicated ones) 20/10 20:11 what? 20/10 20:12 I proved composition of injective functions is injective the other way around too 20/10 20:13 totally uninteresting 20/10 20:13 hey that's interesting someones using Injective on the agda mailing list 20/10 20:16 I wonder whey because I can do the proof about ++ assoc without injectivity 20/10 20:19 would be interesting to see the actual usage 20/10 20:19 if I have x -> y, and I have ¬ y, how can I get to ¬ x? 20/10 20:28 oh wait, I think I know 20/10 20:29 there we go 20/10 20:31 what are some other simple statements I can prove? 20/10 20:36 I don't think there's any point in proving simple statements 20/10 20:38 pick an interesting non-trivial proof to do and there will be lots of drugdery to go along with the interesting proofs 20/10 20:39 the point would be "getting a feeling" for it, really. I'm still at the point where I rejoice if my code typechecks 20/10 20:40 any suggestions for interesting non-trivial proofs then? 20/10 20:40 we all are :D 20/10 20:40 well, I rejoice when my injectivity proof typechecks :P 20/10 20:40 copumpkin: 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 Just compose the proofs? 20/10 20:47 almost identical :P 20/10 20:47 yeah 20/10 20:47 hrrmpf, belittle me all you want! 20/10 20:47 Heh. 20/10 20:48 I also converted from your definition of injectivity to the other one I used 20/10 20:48 do you know any uses of injectivity in type theory? 20/10 20:49 not me, I'm a layperson 20/10 20:49 Injectivity of constructors is occasionally useful for fiddling around with equalities. 20/10 20:50 Like 's m == s n -> m == n' or 'x :: xs == y :: ys -> (x == y) * (xs == ys)'. 20/10 20:50 I mean proofs of f x = f y -> x = y 20/10 20:50 Those are proofs of that. Just that f is a constructor. 20/10 20:51 I know I've used those two above before. 20/10 20:52 parthian shot! 20/10 20:52 http://code.haskell.org/~dolio/agda-share/sorting/html/Natural.html 20/10 20:53 There, that uses injectivity of succ to prove that succ respects inequality. 20/10 20:54 Only I called it ==-pred instead of succ-injective. 20/10 20:54 There are similar theorems in the vector module, only I called them ==-head and ==-tail. 20/10 20:56 What 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 theory 20/10 21:01 Well, that may be. I can't say I've had much use for injectivity of arbitrary functions. 20/10 21:03 The use of Injective in those mailing list posts is probably to be used with (type) constructors. 20/10 21:05 did anyone recognize the original guy asking the question in here? 20/10 21:05 montes89 20/10 21:05 Nope. 20/10 21:06 I wonder if that's being taken as an axiom :| 20/10 21:06 to prove type constructor injectivity is quite involved 20/10 21:06 (for each specific case...) 20/10 21:07 (in general it doesn't hold) 20/10 21:07 I'm pretty sure Agda just gives it to you. 20/10 21:08 Both type and value constructors are just defined to be injective. 20/10 21:08 heh it does 20/10 21:10 that's bizarre 20/10 21:10 (well it's derivible in general for constructors given K but doesn't make sense for type constructors) 20/10 21:11 can you prove pigeonhole from Fin injectivity? 20/10 21:14 if I wrote ackermann in agda, it would be pink, right? 20/10 21:21 no 20/10 21:21 That might depend on how you write it. 20/10 21:21 With higher-order functions, ackermann is primitive recursive, though. 20/10 21:22 oh 20/10 21:22 I see 20/10 21:22 that higher-order form is so much more elegant than the other form I saw 20/10 21:23 I'm kind of annoyed at the phoas syntax for sys F 20/10 23:13 I don't like the relation 20/10 23:14 (used for type application) 20/10 23:14 --- Day changed Wed Oct 21 2009 James Chapman defines everything mutually 21/10 01:21 syntax, context etc.. and the congurences are mutually defined too 21/10 01:21 Wild. 21/10 01:25 I'm not really familiar with the issues that keep everything from being mutual in Agda and such. 21/10 01:26 well it works.. I can't decide if that's what I should do too 21/10 01:26 I seem to recall augustss being pro- everything being mutual, but Ulf had some reasons for not wanting that. 21/10 01:27 oh he's got a new paper! http://cs.ioc.ee/~james/PUBLICATION_files/Relative_Monads.pdf 21/10 01:29 not read it yet 21/10 01:29 I still need to read his thesis so I can rewrite my type theory in Agda. :) 21/10 01:29 Then we'll know it doesn't cause non-termination. 21/10 01:29 http://cs.ioc.ee/~james/PUBLICATION.html 21/10 01:29 Big step normalisation might be worth reading first 21/10 01:30 I actually have two copies of his thesis somehow. 21/10 01:30 I named one with an 's', and one with a 'z'. 21/10 01:30 :S 21/10 01:31 (See also Piponi [7] for this and other interesting uses of vector spaces in functional programming.) 21/10 01:31 heh just watched his talk the other day 21/10 01:32 way over my head 21/10 01:38 that paper about relative monads 21/10 01:38 I 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 I 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 dolio 21/10 15:20 -!- copumpkin is now known as TheHunter 21/10 18:16 -!- TheHunter is now known as copumpkin 21/10 18:16 --- Day changed Thu Oct 22 2009 I attempted to subscribe to the mailing list on Monday. Still no confirmation from the moderator. Is this normal? 22/10 12:38 I had no problems subscribing a couple of weeks ago 22/10 12:40 --- Day changed Fri Oct 23 2009 I'm getting an error message that doesn't seem right to me: 23/10 11:24 IO \top !=< Set1 when checking that the exporession putStrLn "Hello World!" has type Set1 23/10 11:24 IO has type Set -> Set1 and \top has type Set so i don't see the problem. 23/10 11:25 if (putStrLn "Hello World!" : IO \top) it can't also have type Set1 23/10 11:44 it seems like you're using "putStrLn "Hello World!"" as a type somewhere 23/10 11:45 I'm trying to sequence two such calls in a row, using >>, but I can't get it right. 23/10 11:53 My attempt is here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11091#a11091 23/10 12:02 i think you've to use ♯₁ instead of ∞₁ there 23/10 12:21 the former is the value constructor for the latter family 23/10 12:21 i've never used IO, but this one typechecks http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11091#a11092 23/10 12:23 -!- opdolio is now known as dolio 23/10 16:35 how do I do coq-section like stuff? Do I use let? 23/10 19:58 Local module? 23/10 19:58 I'm not sure what all sections get for you, though. 23/10 19:59 in coq I declaire a series of variables and hypothesis 23/10 20:00 which I get to use in my definitions 23/10 20:00 then when I close my section these definition are automagically parameterized by those variables and hypothesis 23/10 20:01 I think you could do that by parameterizing the module by those. 23/10 20:01 Opening a module without supplying the parameters brings the things inside into scope parameterized by the module's parameters. 23/10 20:03 how do I make a hole? 23/10 20:10 Hole? 23/10 20:10 ? perhaps, if that's what you mean. 23/10 20:11 ah ? 23/10 20:11 yes 23/10 20:11 {! !} might also work, but why would you type all that? 23/10 20:11 Agda doesn't seem to like my nested recursion definition either 23/10 20:21 I'd have to see it to comment. 23/10 20:24 what's the usual paste site people use here? 23/10 20:25 hpaste :) 23/10 20:25 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11098#a11098 23/10 20:27 Hmm, yeah. 23/10 20:33 I don't know much about the termination checker, to be honest. 23/10 20:33 I'm not sure if the simpler nested recursion problem works. 23/10 20:33 It works if you define Z in a where clause. 23/10 20:34 Not parameterized by treeInd. 23/10 20:34 oh, you have to do that? 23/10 20:34 Just using it. 23/10 20:34 ooh 23/10 20:35 nice 23/10 20:36 I guess Z is out of scope 23/10 20:36 but still, not bad. 23/10 20:36 You might be able to define them together in a mutual block, too. 23/10 20:38 If you want both in scope. 23/10 20:38 certainly better than I can do in Coq at the moment 23/10 20:38 yep, mutual seems to work 23/10 20:39 I wonder if Agda catches Burnos non-terminating example. 23/10 20:39 is Agda impredicative? 23/10 20:40 I think the "Z treeInd y y'" isnt' obviously structurally recursive, though, so it doesn't do any additional work. 23/10 20:40 No. 23/10 20:40 well, that rules out even stating Bruno's example :) 23/10 20:40 There's a --type-in-type flag, but of course, that's inconsistent. :) 23/10 20:41 dolio: I'm not sure I understood your structural recursive comment 23/10 20:41 ah 23/10 20:41 in Coq, reduction will occur (and has to) before guards are checked 23/10 20:42 so the Z gets inlined and reduced and the treeInd now appears applied to structurally smaller elements and it is happy. 23/10 20:42 at least in the simple 1 list parameter nested fixpoint case 23/10 20:43 I can't get this 2 list parameter example to work in Coq yet 23/10 20:43 Well, 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 I think there's been talk of rewriting it. 23/10 20:50 dolio: that seems strange. I sort of thought it was essential to do reduction before checking guardedness 23/10 21:02 it seems a bit odd to have two converable terms where one passes the checker but the other one does not 23/10 21:03 it seems like that would cause problems 23/10 21:03 Yeah, as I said, I don't really know how it works. 23/10 21:03 I mean, it must do some reduction to be able to see that it works with the where/mutual case. 23/10 21:04 I suppose it might just track the size of arguments through function calls. 23/10 21:10 there don't seem to be any notes on the wiki about how to install the emacs mode, especially after installing from hackage 23/10 23:45 agda-mode setup 23/10 23:45 aha, thanks 23/10 23:52 --- Day changed Sat Oct 24 2009 ok, apparently emacs can't find the agda-mode executable, and ~/.cabal/bin being in both .bashrc and emacs's load-path doesn't help 24/10 00:09 right, have to setenv "PATH" in .emacs to add agda-mode's location. 24/10 00:30 -!- koninkje_away is now known as koninkje 24/10 02:54 -!- Saizan_ is now known as Saizan 24/10 15:58 -!- opdolio is now known as dolio 24/10 21:13 --- Day changed Sun Oct 25 2009 no news with epigram since that short spell :( 25/10 20:47 Not much has happened, alas 25/10 20:48 Conor's teaching, others have been doing their own thing... 25/10 20:48 I expect there'll be another spurt soon enough 25/10 20:49 I need to think up something to do 25/10 20:49 hey edwinb so what are you working on ? :) 25/10 20:50 any cool new Idris stuff or what 25/10 20:51 I'm just writing some slides about it now 25/10 20:51 for a talk tomorrow aimed at newcomers to dependent types 25/10 20:51 I've been trying to make it efficient, which is always entertaining 25/10 20:51 spreading the good word! 25/10 20:52 indeed 25/10 20:52 * edwinb idly wonders if he knows who fax is 25/10 20:52 nah I'm just kid 25/10 20:52 heh 25/10 20:52 I don't study any of this stuff (yet?) 25/10 20:52 undergrad? 25/10 20:52 yeah 25/10 20:52 It's good to have interested undergrads, certainly! 25/10 20:53 all the good stuff is drying out like fplunch and so on -_- 25/10 21:21 Good 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 you actually want to run code? 25/10 23:18 there's an evaluate menu item I believe 25/10 23:18 ISTR a repl too 25/10 23:21 "unsupported" 25/10 23:21 kippetje: what do you plan to do with it? most of the time you'll just want C-c C-l 25/10 23:22 I 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 but i guess ill try to make it haskell code and do it in haskell, emacs is too complicated 25/10 23:26 C-c C-n can normalize things. 25/10 23:28 kippetje what's complicated? 25/10 23:30 kippetje well if you show the code maybe it can be explained 25/10 23:30 I already made it haskell which im looking at now :) 25/10 23:35 how? 25/10 23:36 Its just a simple function nothing special with types, just bool and nat 25/10 23:36 what about that isn't clear? 25/10 23:37 use what dolio said to find out values it gives for particular input 25/10 23:38 when i do that it gives "compile error:" and nothing more 25/10 23:38 make sure your file loaded correctly first 25/10 23:38 we'd be happy to try to explain some code to you if you have any specific questions, too 25/10 23:38 you actually want to run code? 25/10 23:38 this made me laugh out loud 25/10 23:39 :) 25/10 23:39 I 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 agda 25/10 23:40 Saizan: given the lack of anything useful in the Rational module in the standard library, I doubt anyone's tried yet :) 25/10 23:41 but maybe 25/10 23:41 kippetje: (I got this feeling like converting to haskell to understand is a bad idea for a few different reasons) 25/10 23:41 roconnor: Who runs code anymore? Except inasmuch as type checking involves running code. :) 25/10 23:41 it's the ultimate laziness 25/10 23:42 I know my answer is right, but don't need it right now 25/10 23:42 copumpkin: heh, i'm not even sure if Rationals would be sufficient to start or i'd need Reals 25/10 23:43 Saizan: yeah, depends what you're after really... it'd be nice to get reals into agda thouh 25/10 23:43 Saizan: you probably need integration, which mean reals 25/10 23:43 well, i'm after something i can do my prob. theory exercises in :) 25/10 23:44 if i want to cover continuous variables i'd need integration, yeah 25/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 else 25/10 23:45 Saizan you are aware that formal math is a billion times harder than doing it on paper? :) 25/10 23:47 like fixing the rationals? 25/10 23:47 Saizan just incase you hadn't noticed ... 25/10 23:47 Saizan: for a while that too, but then I saw something else shiny :) 25/10 23:47 it's only on the order of 10x harder 25/10 23:47 fax: i wasn't aware of the scale factor :) 25/10 23:47 maybe 100x harder for beginners 25/10 23:47 fax: has anyone proved that multiplier? 25/10 23:47 One-jillion times harder! 25/10 23:48 damn 25/10 23:48 http://code.haskell.org/~dolio/agda-share/html/ExistentialCoinduction.html 25/10 23:50 (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 dolio 26/10 01:12 -!- seanmcl_ is now known as seanmcl 26/10 15:58 Huh, Agda blows up on the last part of James Chapman's simply typed SK normalizer. 26/10 20:49 Oh, I missed some dots, apparently. 26/10 21:07 --- Day changed Tue Oct 27 2009 The code at the end of this thesis is lying to me. 27/10 00:04 give it some truth serum 27/10 00:04 In any case, I have one simply typed SK normalizer, minus a soundness theorem. 27/10 00:06 S = lam (lam (lam ((∅ [ ↑ _ ] [ ↑ _ ])$ ∅ $((∅ [ ↑ _ ])$ ∅)))) 27/10 01:14 -!- opdolio is now known as dolio 27/10 03:27 -!- opdolio is now known as dolio 27/10 06:33 hey 27/10 16:43 I'm getting something from Agda.. ehrm.. which I don't know if it is an error or not 27/10 16:43 cannot 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 yellow 27/10 16:45 what does this mean? 27/10 16:45 it means it couldn't infer some of the types 27/10 16:45 try making implicit arguments explicit on that call 27/10 16:46 the _N are metavariables the the type checker couldn't resolve 27/10 16:46 aha 27/10 16:47 hang on 27/10 16:47 right.. works if I make everything explicit 27/10 16:48 you can put {_} as arguments and reload, it'll hilight in yellow only the problematic ones 27/10 16:48 I did have implicit arguments in the definitions.. 27/10 16:48 but it wasn't highlighting any of them 27/10 16:48 oh wait 27/10 16:48 I need to pass the implicit args in the recursive call I guess 27/10 16:48 you use foo {a} to pass a as an implicit argument to foo 27/10 16:49 ah yes 27/10 16:49 Saizan_: thanks.. 27/10 16:49 np 27/10 16:49 I was actually pattern matching on an implicit Nat argument 27/10 16:49 had to pass it to the recursive call 27/10 16:49 well, that depends on the shape of the other arguments, however it's not unusual 27/10 16:51 would Agda be suitable for solving/creating a proof for this problem, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11217#a11217 27/10 20:00 it's be rather painful for now 27/10 20:01 or do I need something more specialized/different ? 27/10 20:01 so far everything is painful for me in Agda :) 27/10 20:01 would Coq be any better? 27/10 20:01 stepcut what is it??? 27/10 20:01 Lots of 40 components each are called acceptable if they contain no more than 3 defectives. 27/10 20:01 The 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 What is the probability that exactly 1 defective is found in the sample if there are 3 defectives in the entire lot 27/10 20:01 just a simple probability question... 27/10 20:02 well I can't read all that but why donot you just compute it in a thingy like maxima? 27/10 20:02 did you want a certified program to compute it? 27/10 20:02 yeah.. I want some sort of 'proof' that I did it right... 27/10 20:03 mostly trying to get more experience with proofs 27/10 20:03 though maybe that is not the type of thing you prove? 27/10 20:03 I don't do probability theory :P 27/10 20:05 me neither. I had to take that class twice... 27/10 20:05 Coq has computable real lib (thanks to roconnor) and theory of integration etc 27/10 20:05 hence my desire for a stronger assertion of correctness ;) 27/10 20:05 if you can't prove it on paper you can't prove it formally 27/10 20:05 I mean it's a LOT harder inside the computer 27/10 20:06 yeah, I have noticed that 27/10 20:06 it is surely to do with the subject being in infancy 27/10 20:06 (and all of us beginners etc) 27/10 20:06 oh 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 Seems like the same problem but with defective/non-defective parts 27/10 20:07 I 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 ???? 27/10 20:10 calculus is the most practical mathematics  other than sumsing and timesing 27/10 20:10 practical in what way? 27/10 20:11 nobody turns real life situations into probability theory, we fly by intuition - that doesn't make sense 27/10 20:11 that's because most people don't know probabity theory ;) 27/10 20:11 stepcut people that balance poles on the nose and juggle don't know control theory :P 27/10 20:14 :p 27/10 20:15 (some of them might.. but anyway, they aren't (conciously) approximation solustions to the ODE for inverted pendulum) 27/10 20:16 but imagine if they *were*! But you didn't think of that! 27/10 20:16 ok, the first step is to prove the Basic Counting Principle 27/10 20:26 Yes, 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 zomg 27/10 20:27 dolio I don't find that true in general... 27/10 20:27 sort of  the fundamental thing about mathematics? 27/10 20:28 Well, I think it's true when you're a neophyte at the subject. 27/10 20:28 I 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 oh sure I agree 27/10 20:29 well the whole structure of mathematical education is based on not understanding anything you do 27/10 20:29 that's quite possible to combat though 27/10 20:29 On a tangent, have you read James Chapman's thesis yet? 27/10 20:30 yes 27/10 20:30 I'm not sure what to think about the dependently typed normalizer. 27/10 20:31 why? 27/10 20:32 what abot it? 27/10 20:32 It 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 dolio I find his technique in general very elaborate:   I think that is why he does the smaller case studies though 27/10 20:32 But, 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 I don't beleive you need to say "if it's well typed" since every syntax is well typed by construction 27/10 20:32 isn't it? 27/10 20:33 It's well typed in the LF by construction, yes. 27/10 20:33 I guess the same can be said of Luo's UTT. 27/10 20:35 no  ?? 27/10 20:35 You 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 Which may be easier than proving normalization directly. 27/10 20:36 I guess that's what the twelf folks call "adequacy". 27/10 20:36 dolio I think I better re-read it to be follow you properly 27/10 20:38 you mean the stuff in Chapter 5 - Dependently typed λ-calculi? 27/10 20:38 Yeah. 27/10 20:38 ok. 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.htm 27/10 20:39 surely I can prove this in Agda? 27/10 20:40 fax: 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 I've also seen the proof done as 2 dimensional array of tuples 27/10 20:41 You'd need some kind of axioms of probability, at least. 27/10 20:49 dolio: I'm not understanding your statements about LF and such 27/10 20:51 seems I also need to rebuild agda against a newer libffi :-/ 27/10 20:51 dolio: I've not understood what you say about LF and so forth 27/10 20:56 LF is a dependently typed lambda calculus used as a meta-language for defining object languages. 27/10 20:57 Where the object language is the language you want to actually work in. 27/10 20:58 yes but are you calling Agda LF? 27/10 20:58 No. Chapman defines models the LF in Agda, and the object language in the LF at the same time, sort of. 27/10 21:00 I didn't notice that :S 27/10 21:00 His Type type is the type of LF types. 27/10 21:00 Or, in Twelf they call them kinds, I think, to keep from getting confused. 27/10 21:01 So, 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 And there are meta-level pi types, too. 27/10 21:03 Then you define your object language by listing things that are in U, and El(s) and so on. 27/10 21:04 So 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 Oh, and application. 27/10 21:07 you said   the object language *in* the LF 27/10 21:07 but I think that is not what is happening 27/10 21:07 the object language is the "LF" 27/10 21:09 (I find calling it LF extremely confusing btw) 27/10 21:09 do you refer to a part of the actual .agda implementation? 27/10 21:11 Well, 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 Which 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 Defining 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 dolio: In 5.6 that's adding impredicative set isn't it? 27/10 21:20 whereas every quantification you had before was in Type[2], this lets you have a quantification in Type[1] 27/10 21:20 I don't think it's impredicative. 27/10 21:21 I think the split  Term/Type  is not really saying 'these are different languages' but lets every presentation follow a single technique 27/10 21:22 to me it reads like: 27/10 21:23 Gamma |- sigma : *,     Gamma, sigma : * |- tau : * 27/10 21:23 ------------------------------------ 27/10 21:23 Gamma |- Pi_u sigma tau : * 27/10 21:23 No, 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 However, 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 Yes, I know. 27/10 21:27 so that is why I think Pi_u is impredicative 27/10 21:28 Luo introduces a similar object-level pi on 177 of Computation and Reasoning. 27/10 21:28 Luo does use the LF approach to define his type theory 27/10 21:28 Pi : (A:Type)((A)Type)Type 27/10 21:29 I think it's a quite different approach in James' Thesis -- although he uses Type Theory (epigram/agda) instead of Set Theory 27/10 21:29 But that translates to Chapman's LF-embedded in Agda. 27/10 21:29 Pi : (sigma : Type G U) (tau : Type (G ; El sigma) U) -> Type G U 27/10 21:30 Er, those should be Term G U 27/10 21:31 I've still not really understood what you mean when you say LF in reference to James' development 27/10 21:31 dolio do correct me if I say something nonsensical there's a big chance I have misunderstood parts of his thesis :P 27/10 21:33 I 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 Luo takes the LF as a starting point, Chapman encodes it as Agda datatypes. 27/10 21:36 I 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 The judgment S : Type in Luo is analogous to S : Term G U in Chapman. 27/10 21:38 I think. 27/10 21:38 F : (x:A)B  ~ F : Term G (Pi A B) 27/10 21:40 And Luo adding object-language Pi is analogous to Chapman adding a Pi constructor to the Term type. 27/10 21:41 yeah that does make sense, I see 27/10 21:43 Chapman 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 when he says "we both formalise Martin-Lof ’s logical framework,"? 27/10 21:45 Yes. 27/10 21:47 I think he is referring to the entire calculus, not just Type? 27/10 21:47 Yes, Terms are part of LF, too. 27/10 21:48 in 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 But 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 At least, that's how I understand it. 27/10 21:50 I saw them as separate but I am not very sure anymore :) 27/10 21:50 for example the syntax (terms and types and kinds) of UTT is self contained 27/10 21:51 ok, 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 what am I doing wrong? 27/10 21:51 I'm trying to write up some of the early parts of Luo's stuff Chapman style, to illustrate. 27/10 21:51 stepcut when I said that stuff about Coq having reals and integration etc... I mentioned it because I don't think such libraries exist in Agda 27/10 21:52 fax: I don't think I need reals or integration to prove the Fundamental Theory of Counting ? 27/10 21:53 sure 27/10 21:53 dolio btw I think with the Type in UTT is stratified implicitly (like in Coq 27/10 21:59 Well, the Type in UTT is a meta-language entity. 27/10 22:00 He gets around later to talking about object-language universes, which are cumulative. 27/10 22:00 Or, predicative, or whatever. 27/10 22:01 It's kind of a weird system. Different than Coq or Agda. 27/10 22:01 what is the differenc from Coq? 27/10 22:02 Well, I think people call the difference Russel-style universes vs. Tarski-style. 27/10 22:03 In Coq, you have A : Type[i], and Type[i] : Type[j] for i < j and so on. 27/10 22:03 Which is Russel style. 27/10 22:04 that is also what UTT uses though 27/10 22:05 Hold on, phone call. 27/10 22:06 I think they're essentially the same except for UTT has this nice sum type 27/10 22:06 In Tarski-style, like LF/UTT, you have the Type kind/universe, which contains names as values. 27/10 22:07 hello 27/10 22:07 Then, for each name A in Type, you have El(A) is also a kind. 27/10 22:07 That's what Plastic does 27/10 22:07 hi yakov 27/10 22:08 And each object language term has a type El(A) in the meta theory, independent of types in the object theory. 27/10 22:08 silly question but anyway is it possible to print values from emacs? 27/10 22:09 yakov you can compute values and have them displayed if that's what you mean 27/10 22:10 But then he goes on to define universes in the object theory, which have names Type_i : Type. 27/10 22:11 yes, this is what i want 27/10 22:11 C-c C-n in emacs probably? 27/10 22:11 So each predicative universe has a name in Type, and its elements a : El(Type_i) are also names. 27/10 22:11 aha. thanks copumpkin 27/10 22:13 :) 27/10 22:13 And 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 dolio what section is that because that's not how the normal presentation went 27/10 22:14 And there's always type_i : El(Type_i+1), specifying the hierarchy. 27/10 22:14 "9.2.3 Predicative Universes" in his book. 27/10 22:14 Anyhow, I've got to grab some dinner. I'll be back in a while. 27/10 22:15 fax: 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 I was thinking of ECC -_- 27/10 23:38 Which he describes directly, instead of working in the logical framework. 27/10 23:38 yeah 27/10 23:38 Which 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 But, all terms are typed in LF, and I guess you prove strong normalization based on typing in LF. 27/10 23:40 But, how does that translate to saying that a well-typed ECC term is strongly normalizing? 27/10 23:40 I'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 But I'm not really sure. 27/10 23:46 Instead 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 Where 2 is a De Bruijn index. 27/10 23:50 Oh, actually, that should be a 0, I guess. 27/10 23:51 --- Day changed Wed Oct 28 2009 Incidentally, I looked this back up today: https://lists.chalmers.se/pipermail/agda/2008/000640.html 28/10 00:23 It seems to make a lot more sense having read Luo's book. 28/10 00:23 -!- copumpkin is now known as Xah 28/10 00:56 -!- Xah is now known as copumpkin 28/10 00:58 hello 28/10 11:57 hi 28/10 12:30 http://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 ones 28/10 15:13 mh, but context-sensitive ones are turing complete, though maybe you can do that in a non-termination monad 28/10 15:23 yeah, so where does it fall? there's a distinction of "mildly context-sensitive" 28/10 15:24 that one feels too restrictive 28/10 15:24 indexed? 28/10 15:25 I dunno :) 28/10 15:25 it'd be nice to get some more formal intuition on that, though, especially given how many monadic parsing libs there are out there :P 28/10 15:26 heh 28/10 15:27 Saizan_: I thought "context-sensitive" has the requirement that the RHS is not longer than the LHS 28/10 16:20 which makes them decidable 28/10 16:20 (equivalent to "linearly-bounded" turing machines or some such) 28/10 16:20 FunctorSalad: ah, true 28/10 16:24 however monadic parser combinators in haskell can parse turing complete grammars i'd imagine 28/10 16:26 can you write a nonterminating monadic parser? 28/10 16:26 I guess you could just put fix id in it 28/10 16:26 can'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 FunctorSalad: the pure function can't report a failure 28/10 16:48 with monads you can write "do input <- many anyChar; if turingCompleteP input then return () else mzero" 28/10 16:49 is this defining a Haskell-style tuple, or something else? 28/10 17:48 data Σ (A : Set) (B : A → Set) : Set where 28/10 17:48 _,_ : (x : A) (y : B x) → Σ A B 28/10 17:48 28/10 17:48 stepcut: not quite 28/10 17:49 although it can be a haskell-style tuple 28/10 17:49 a normal haskell tuple would be more like: 28/10 17:50 data Tuple ( A : Set ) ( B : Set ) : Set where 28/10 17:50 _,_ : (x : A) (y : B) -> Tuple A B 28/10 17:50 ? 28/10 17:50 yeah, but you can use the other one as a regular tuple too 28/10 17:50 how do you do that ? 28/10 17:50 http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#213 28/10 17:51 Tuple A B = Σ A (const B) 28/10 17:52 oh well you just stick the second value in there such that its type doesn't depend on it 28/10 17:52 *on the first value 28/10 17:52 oh the  x function ? 28/10 17:52 looks like I also have an older version of lib 28/10 17:53 yeah 28/10 17:53 _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b) 28/10 17:53 that one's using the new fancy level stuff 28/10 17:53 but you get the idea 28/10 17:53 I have the latest Agda from darcs, so perhaps I should upgrade? 28/10 17:53 you mean upgrade the standard library? 28/10 17:54 how 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 approach 28/10 17:55 in emacs there are shortcuts if you type \ 28/10 17:55 \r gives you the right arrow for example 28/10 17:55 \lambda is a lambda 28/10 17:55 copumpkin: where can I find that list of shortcuts? 28/10 17:55 \bn is the Nat symbol 28/10 17:55 \ 28/10 17:55 or there's a webpage somewhere on the agda wiki with a few 28/10 17:56 ok 28/10 17:56 maybe I can just look in agda-mode.el ? or is it not agda specific? 28/10 17:56 regarding 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/Agda 28/10 17:57 darcs get --lazy http://www.cs.nott.ac.uk/~nad/repos/lib/ 28/10 17:58 http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.UnicodeInput <- for the shortcuts 28/10 17:59 how 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 that's it 28/10 18:00 ok 28/10 18:01 ok, I tried this: 28/10 18:03 f : Σ ℕ ℕ 28/10 18:03 f = ( zero × zero ) 28/10 18:03 28/10 18:03 but I got this error, 28/10 18:03 Set !=< (ℕ → Set) of type Set₁ 28/10 18:03 when checking that the expression ℕ has type ℕ → Set 28/10 18:03 what does !=< mean ? 28/10 18:04 is it a frowny face with a baseball cap? 28/10 18:04 the type is \bn x \bn 28/10 18:04 Σ ℕ ℕ   is a type error 28/10 18:04 so deal with that first 28/10 18:04 that _×_ is a type thing 28/10 18:04 stepcut: make sense? 28/10 18:05 OT: shouldn't theorem-provers be EDSLs in haskell rather than stand-alone apps? 28/10 18:05 Σ ℕ (\ _ -> ℕ) 28/10 18:05 FunctorSalad: only if you're trying to sell us something ;) 28/10 18:05 then you could use all the power of runtime haskell to combine proofs 28/10 18:05 FunctorSalad: Ivor is 28/10 18:05 fax: yeah but it seems to be in disrepair somewhat :( 28/10 18:06 I looked at ivor but couldn't make much sense of it 28/10 18:06 but that's the idea yes 28/10 18:06 copumpkin: I don't get it what am I selling...? 28/10 18:06 I thought you were leading into your type-level proving stuff in haskell that you were working on the other day :) 28/10 18:07 stepcut: !=< means "not less than or equal" 28/10 18:07 copumpkin: no, actually after working on it I reappreciated how powerfully expressive the *value*-level is ;) 28/10 18:08 FunctorSalad: lol 28/10 18:08 fax: Σ ℕ ℕ 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 but it did somewhat make me appreciate the "fluidity"of set theory more *runs before being burned at the stake* 28/10 18:09 stepcut, 28/10 18:09 data Σ (A : Set) (B : A → Set) : Set where 28/10 18:09    _,_ : (x : A) (y : B x) → Σ A B 28/10 18:09 talking about this one? 28/10 18:09 stepcut: yes, it wants a function and you gave it a type 28/10 18:09 fax: yeah, though I added to the 28/10 18:09 stepcut: so your type needs to be \bn × \bn 28/10 18:09 quite simply ℕ : Set, is okay but the next ℕ : ℕ -> Set is wrong 28/10 18:09 latest version. so now it is data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where 28/10 18:09 okay 28/10 18:09 why do you want to use this one? 28/10 18:10 with ⊔ 28/10 18:10 that's the new default one in the std lib 28/10 18:10 fax: because newer is better I guess ? 28/10 18:10 fax: it's just whatever is in darcs head for lib 28/10 18:10 f :  ℕ × ℕ; f = zero , zero 28/10 18:11 its probably just confusing and worse 28/10 18:11 what is Set 28/10 18:11 a? 28/10 18:11 it's a type 28/10 18:11 is that in the new thing got an explicit level 28/10 18:12 yeah 28/10 18:12 Set is the type of types, Set_1 is the type of type of types, and so on 28/10 18:12 I mean this one though 28/10 18:12 latest version. so now it is data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where 28/10 18:12 Set didn't used to have a parameter 28/10 18:12 yeah, the parameter is the explicit level 28/10 18:13 to avoid the subscript levels we used to have 28/10 18:13 so no more Set\_1 Set\_2 and so on 28/10 18:13 stepcut: make sense? 28/10 18:19 copumpkin: yes-ish 28/10 18:19 opdolio gave me a good explanation for all this a few weeks ago 28/10 18:20 copumpkin: too much Haskell polluting my brain mostly... 28/10 18:20 stepcut: but basically that sigma is called a dependent sum 28/10 18:20 meaning that the _type_ of the right element depends on the _value_ of the left 28/10 18:21 you can make that dependency constant 28/10 18:21 and get yourself a regular haskell 2-tuple 28/10 18:21 crazy 28/10 18:21 you can also get arbitrary sums for example though 28/10 18:22 types like Either can be represented easily 28/10 18:22 you 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 y 28/10 18:23 sorry, that's not very elegantly phrased 28/10 18:23 ah, I think I get it. Neat. 28/10 18:24 ok, so I am trying to do a cartesian product thing now using the tuple. I wrote this: 28/10 18:25 cartesian : ∀ {a b m n} -> Vec a m -> Vec b n -> Vec (a × b) (m * n) 28/10 18:25 cartesian [] _ = [] 28/10 18:25 cartesian (x ∷ xs) ys = (map (\y -> x × y) ys) ++ cartesian xs ys 28/10 18:25 but I get this error: .a !=< Set  for the x in (\y -> x × y) 28/10 18:25 yeah, you want _,_ there 28/10 18:25 so, that means that a is not less than or equal to Set. 28/10 18:25 it's a value-level thing 28/10 18:25 you'll always use the , constructor 28/10 18:26 what does it mean that a is not less than or equal to Set though ? 28/10 18:26 ah 28/10 18:26 not even sure what the right language for this is 28/10 18:26 :p 28/10 18:26 but you're saying that you're mapping from your vec to a type 28/10 18:27 you're sticking a type into your vec with that × 28/10 18:27 in 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 expected 28/10 18:28 or that to any level 28/10 18:28 ok, 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 yeah 28/10 18:33 stepcut 28/10 18:33 Tuple A B = Σ A (const B) 28/10 18:33 I 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 fax: yeah, that makes sense now 28/10 18:33 http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1048 28/10 18:34 this works: 28/10 18:43 Tuple : (A : Set) (B : Set) → Set 28/10 18:43 Tuple A B = Σ A (λ _ → B) 28/10 18:43 yep, that's pretty much how that x is defined 28/10 18:43 but if I use const I get: Set !=< (_12 A B) 28/10 18:43 except it's dealing with multiple type levels 28/10 18:43 (on the last B) 28/10 18:43 which seems odd because const is: 28/10 18:44 const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A 28/10 18:44 const x = λ _ → x 28/10 18:44 now 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 how do you intend to express that? 28/10 18:52 that's what I am working on. Though I am wondering if maybe I should have used sets. 28/10 18:53 I can tell you how I'd do it, but there may be a more elegant way 28/10 18:53 I'm pretty new to this too :) 28/10 18:54 actually, I also need to prove that the cartesian product does not include any other elements as well.. 28/10 18:57 yep, you can do those separately 28/10 18:57 well, 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 together 28/10 18:57 yep 28/10 18:58 so, one part is to prove that, ∀ a b, if a ∈ A and b ∈ B, then (a, b) ∈ A × B 28/10 18:59 yep 28/10 19:00 so written as a type...? 28/10 19:00 I was thinking something like this: 28/10 19:02 lemma1 : ∀ {a b m n} → (a ∈ Vec a m) → (b ∈ Vec b n) → ((a × b) ∈ (Vec (a × b) (m * n))) 28/10 19:02 but ∈ is not defined for Vec that I saw 28/10 19:02 I guess I need to write it ? 28/10 19:04 it is 28/10 19:07 well 28/10 19:07 data _∈_ {a : Set} : a → {n : ℕ} → Vec a n → Set where 28/10 19:07 oh, duh. 28/10 19:08 its constructors may be a bit of a pain though 28/10 19:08 how can I get agda to check my type signature before I implement the function bodies. is that possible ? 28/10 19:09 oh. maybe its just, lemma1 : : lemma1 = _ 28/10 19:10 just type ? 28/10 19:21 it'll put a "hole" there 28/10 19:21 like f : aType 28/10 19:24 f = ? 28/10 19:24 then C-c C-l 28/10 19:24 and it'll convert the question mark into a fancy hole 28/10 19:24 and allow you to ask for the type of that hole and other things 28/10 19:24 cool 28/10 19:26 ok, 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 oh wait, I misread the type for 'there' 28/10 19:28 so you get how it works? 28/10 19:40 very slowly 28/10 19:40 I think my first step is to prove: 28/10 19:40 lemma1a  : ∀ {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 why are you doing x \in x \:: xs ? 28/10 19:41 instead of just, x \in xs ? 28/10 19:42 yeah 28/10 19:42 hrm, do to an earlier error I made I think 28/10 19:43 I am not really clear on how to prove implement this, test :  ∀ {a} {n} {x} {xs : Vec a n} → x ∈ xs 28/10 19:44 maybe I don't need to ... 28/10 19:46 ok, so now I have this: 28/10 19:46 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 19:46 this does seem better :) 28/10 19:46 now I have my first case: 28/10 19:48 lemma1a here here = here 28/10 19:48 cool, how's it going? 28/10 19:55 second case not so well 28/10 19:56 I want something like: 28/10 19:56 lemma1a here (there ys) = lemma1a here ys 28/10 19:56 but I have not got it quite right yet 28/10 19:56 yeah, I don't get this part ;) 28/10 20:05 maybe I need a with 28/10 20:06 you might :) 28/10 20:08 do you get the basic meaning of here vs. there? 28/10 20:08 yeah. here say that if you have an element x and you append it to the head of a vector, then the vector contains x 28/10 20:09 there 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 member 28/10 20:10 ooo... 28/10 20:12 ? 28/10 20:12 hrm, still not right 28/10 20:13 I guess I don't understand what is wrong with this yet, 28/10 20:15 lemma1a here (there ys) = lemma1a here ys 28/10 20:15 what does it say? 28/10 20:16 here 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 which is not quite right because that is showing the cartesian of xs ys' not xs ys 28/10 20:19 stepcut: make any progress? 28/10 21:43 copumpkin: no, I had to do something else for a bit, but I am looking at it again now 28/10 21:52 though I'm currently at a lose as to what to do 28/10 21:53 in fact, now I don't even understand why the part that works, works, 28/10 21:59 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 21:59 lemma1a here here = here 28/10 21:59 I'll be back in a little while, going home 28/10 21:59 matching against "here" refines xs to "x :: zs" in the first case, and similarly for ys. 28/10 22:00 stepcut what are you tring to write? 28/10 22:00 fax: proof that, ∀ a b, if a ∈ A and b ∈ B, then (a, b) ∈ A × B 28/10 22:02 So 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 stepcut just as a test or for something else? 28/10 22:02 And presumably cartesian (x :: xs') (y :: ys') = (x , y) :: whatever 28/10 22:02 fax: 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 together 28/10 22:04 oh heh 28/10 22:04 yeah.. I still have no idea what to do for the second case 28/10 22:14 stepcut got a nice proof of this on paper? 28/10 22:16 or web or whatever 28/10 22:16 fax: no sir 28/10 22:16 step 1 ^ 28/10 22:16 * stepcut never learned how to do proofs 28/10 22:17 hello 28/10 22:19 hi 28/10 22:20 I 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 hm I've read that 28/10 22:21 as much as I like Troelstra, I don't think I got much out of it, I preferred  Proof Theory - Takeuti 28/10 22:22 I don't think it has much to do with agda 28/10 22:23 either of them,a 28/10 22:23 fax: 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 stepcut what exactly to prove? 28/10 22:33 I missed a lot of whatever was happening 28/10 22:33 I wrote a function: cartesian : ∀ {a b m n} -> Vec a m -> Vec b n -> Vec (a × b) (m * n) 28/10 22:33 which is supposed to do the cartesian product 28/10 22:34 so 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 or 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 stepcut I can't think of any nice way to format this all 28/10 23:14 heh 28/10 23:14 only the obvious thing about length and drop etc 28/10 23:14 there must be a better way 28/10 23:14 * stepcut knows no ways, much less a better one 28/10 23:14 what is the obvious thing about length and drop? 28/10 23:15 if cartesian was something like 28/10 23:15 x (y::ys) --> map (y:) xs ++ cartesian xs ys 28/10 23:15 you've mentioned OTT yesterday. what does this acronym mean? 28/10 23:15 then drop (length xs) (map (y:) xs ++ cartesian xs ys) = cartesian xs ys 28/10 23:15 and yo ucan rewrite that in the recursive step of the proof for lemma1a 28/10 23:16 fax: I have,  cartesian (x ∷ xs) ys = (map (\y -> x , y) ys) ++ cartesian xs ys 28/10 23:16 (this is slightly hideous) 28/10 23:16 Observational type theory. 28/10 23:16 stepcut, that's what I mean 28/10 23:16 h 28/10 23:17 hm 28/10 23:17 stepcut do yu have join for vectors? 28/10 23:22 um 28/10 23:24 I am using Data.Vec, so if it's not there, I don't have it. 28/10 23:25 concat 28/10 23:25 by join do you mean, Vec (Vec a n) m -> Vec a (m * n) ? 28/10 23:26 yes 28/10 23:26 nope. 28/10 23:26 I remember seeing that 28/10 23:26 somewhere, I thought 28/10 23:26 ah well, it wouldn't be hard to write 28/10 23:26 concat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m) 28/10 23:27 concat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m) 28/10 23:27 concat []         = [] 28/10 23:27 concat (xs ∷ xss) = xs ++ concat xss 28/10 23:27 28/10 23:27 ? 28/10 23:27 sure, if that works 28/10 23:31 stepcut: are you formalizing prob. theory to do your homework? i was going to attempt that too :) 28/10 23:32 Saizan: yes, but it is not homework 28/10 23:35 --- Day changed Thu Oct 29 2009 stepcut I am attempting to prove this in the normal way and it is awful :P 29/10 00:02 I hope someone comes up with a better way 29/10 00:04 fax: heh 29/10 00:11 if you want to read it here, http://pastie.org/674305 29/10 00:14 everything up to "proof" seems fine 29/10 00:14 but then it turns horrible and we realize it was all a mistake 29/10 00:14 purrty 29/10 00:15 it 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 pointless 29/10 00:17 fax: don't like implicit parameters for that proof? 29/10 00:20 no 29/10 00:26 stepcut next you show   < a , b > in A * B --> (a in A x b in B) ? 29/10 00:53 where does that vector product thing place in the whole scheme? 29/10 00:53 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11256#a11256 29/10 01:02 I think most of that stuff is in the standard library. 29/10 01:03 oh purty 29/10 01:05 dolio: not a fan of the std lib? 29/10 01:05 I wanted to see if I could rewrite it without looking. 29/10 01:05 :) 29/10 01:05 much better 29/10 01:06 Now I'm not finding it, though... 29/10 01:07 stepcut: !!! 29/10 01:07 copumpkin: !!! 29/10 01:10 :) 29/10 01:11 stepcut: did you see master dolio's masterful proof? 29/10 01:11 Oh, it's only defined for lists. 29/10 01:11 copumpkin: I am seeing it now. 29/10 01:11 Data.List.Any.Properties has lots of stuff in this area. 29/10 01:11 yeah, I got frustrated at how much more Data.List had than Vec 29/10 01:11 I'll have to study it tomorrow though 29/10 01:11 looks nice 29/10 01:16 hello 29/10 08:56 double negation monad :o 29/10 17:23 :o 29/10 17:27 isn't that Cont Void? 29/10 17:27 (don't know if there's Cont in Agda?) 29/10 17:27 I thought one of dolio's experiments involved that 29/10 17:28 maybe not 29/10 17:29 is ./example/lib in the darcs source tree the current stdlib? 29/10 17:44 ("example") 29/10 17:44 nope 29/10 18:06 it's a separate repo 29/10 18:06 do you think the double negation in the latest email on the agda list was intentional? 29/10 18:36 But it is not 29/10 18:36 not OK for a corresponding theory of countably branching 29/10 18:36 well-founded trees. 29/10 18:36 sorry newb question... what does the dot in patterns mean? 29/10 20:03 something about absurdity I reckon 29/10 20:04 another question: is there any global indexing mechanism for theorems? 29/10 20:05 FunctorSalad: it's the dependent pattern matching refinement 29/10 20:05 (where matching on one thing tells you something about another thing) 29/10 20:05 revealing existentials by pattern matching, like in haskell? 29/10 20:06 if you have a constructor    X : T Foo 29/10 20:10 then  f : i -> T i -> ... 29/10 20:10 the pattern    X for T i refines i into 'Foo' 29/10 20:10 so you can write   f .Foo X = ... 29/10 20:10 * FunctorSalad really likes the haskell mode so far 29/10 20:10 err emacs mode 29/10 20:11 (I've independently wished for this 'holes' thing in haskell actually) 29/10 20:11 it's pretty nice 29/10 20:12 fax: indexed families are the same thing as existentials really or not? at least in haskell they are 29/10 20:12 X : T Foo can be written as X : i = Foo -> T i 29/10 20:13 (don't know if that's correct in agda) 29/10 20:13 I just started using it rather than just hearing about it ;) 29/10 20:13 (the i is existential there) 29/10 20:14 fax: what?  I thought that happened automatically, and the dot is to mark *inaccessible* patterns 29/10 20:14 unless I am confused 29/10 20:14 maybe I should write what I mean in haskell: 29/10 20:16 no I don't think so FunctorSalad 29/10 20:16 data T :: (* -> *) where X : T Foo 29/10 20:16 is equivalent to 29/10 20:16 that is not useful 29/10 20:16 data T j = (j ~ Foo) => T j 29/10 20:17 (I find that to be conceptually somewhat simpler than the indexed families) 29/10 20:17 correction: 29/10 20:18 data T j = (j ~ Foo) => X 29/10 20:18 FunctorSalad I don't think this has any interesting content 29/10 20:18 fax: it eliminates index families as primitives... 29/10 20:18 *indexed 29/10 20:18 but you need some built-in equality, as haskell has 29/10 20:19 is there some builtin for dependent pairs? 29/10 20:28 -!- opdolio is now known as dolio 29/10 21:14 You can mimic the Haskell version by storing the propositional equality. 29/10 21:17 data T (j : ?) : Set where X : j ≡ Foo → T j 29/10 21:17 Although that's rarely nicer than indexing directly. 29/10 21:19 "Not a valid let-declaration 29/10 21:26 when scope checking" 29/10 21:26 what could that mean? 29/10 21:26 Uh... Your 'let' is invalid somehow? 29/10 21:27 And it happened during the phase where it was resolving the scope of names. 29/10 21:27 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11282#a11282 29/10 21:27 yes but how is it invalid ;) 29/10 21:28 No pattern matching in let function definitions. 29/10 21:28 Which is a bizarre restriction, but... 29/10 21:28 is there any other way to do an inline pattern match or do I need a toplevel decl? 29/10 21:29 Top level, I'm afraid. 29/10 21:29 Or a where. 29/10 21:29 That looks like it'd be fine in a where. 29/10 21:30 ah, I inferred from "not in let" that "not in where" either 29/10 21:31 thanks 29/10 21:31 Nope, let and where are different for some reason. :) 29/10 21:32 where is sugar (or something) for a local module, whereas let is something else. 29/10 21:32 Oh, lets can't be recursive, either. I guess it just inlines everything in the let, essentially. 29/10 21:34 ah 29/10 21:35 According to the AIM10 notes, there was talk about making let more like where, though. 29/10 21:36 (can anyone *ever* remember which direction of the adjunction is ♯ and which is ♭? ;)) 29/10 21:36 I think Hom(A,UB) ---> Hom(FA,B) should be ♯ 29/10 21:37 because it "extends" a function to the whole free gadget 29/10 21:37 but I think I've seen it the other way 29/10 21:38 Adjunction? 29/10 21:38 the adjoint functors kind 29/10 21:38 Hmm, I hadn't thought of that as an adjunction. 29/10 21:39 Then again, they're one of the weak areas of my basic category theory knowledge. 29/10 21:40 ♯ and ♭ are just names sometimes used for the two directions of the adjunction isomorphism 29/10 21:42 I think it's better than φ ;) 29/10 21:42 What are the two functors? F and \inf F? Or I and \inf? 29/10 21:43 ah you mean this specific case of set union? 29/10 21:45 (with "that") 29/10 21:45 I hadn't thought of \inf as being part of/defined by an adjunction. 29/10 21:46 \inf? 29/10 21:47 Are we talking about some \sharp and \flat that are unrelated to codata? 29/10 21:47 I don't know the usage of ♯ and ♭ with codata 29/10 21:48 maybe it's a special case of the usage for adjunctions 29/10 21:48 Oh, well, nevermind me, then. :) 29/10 21:48 (pretty much anything in structure math is an adjunction ;)) 29/10 21:48 Oh, I see what you're saying now. 29/10 21:48 in 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 which can be expressed as an adjunction if you take the category "sets ordered by inclusion" 29/10 21:50 I find myself preferring the epsilon/eta definition of adjunctions. 29/10 21:53 Possibly because I feel all dirty and concrete talking about hom-sets. :) 29/10 21:54 Maybe if I only worked in enriched categories, I'd feel better. :) 29/10 21:55 hmm never thought about it like that 29/10 21:56 but yes it seems to involve your background set theory 29/10 21:56 Although, 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 Which is nice. 29/10 22:02 the minibuffer should use the agda input-method too 29/10 22:27 It does sometimes. 29/10 22:28 Like for C-c C-d/n. 29/10 22:28 But not C-s. 29/10 22:28 I can M-x set-input-method in the minibuffer but it won't remember 29/10 22:30 can't I insert holes in a hole? 29/10 22:31 (with manual question marks, not 'refine') 29/10 22:31 You can. 29/10 22:32 { foo ? }0 29/10 22:32 apparently the two question marks are assumed to be the same type 29/10 22:32 or I have some other bug :) 29/10 22:35 you can put things in the holes? i never tried that 29/10 23:14 What do you do? Delete the hole and fill it in yourself? 29/10 23:28 I use _ and then fill it in 29/10 23:28 --- Day changed Fri Oct 30 2009 you can also fill it in yourself and press C-c C-space ;) 30/10 00:23 That was such a surprise you knocked fax off the internet. 30/10 00:24 FunctorSalad_: how do universe levels work in agda? 30/10 15:59 roconnor_: no idea I'm a newbie myself 30/10 15:59 roconnor_: up until recently, you had Set, Set\_1 Set\_2 and so on 30/10 15:59 I just realized I probably can't give you the level of answer you're looking for :) 30/10 16:00 how do you find stuff in the stdlib? 30/10 16:03 I browse the Everything file, or use grep -R 30/10 16:03 but it's a real pain, in general 30/10 16:03 data Ens : Set\_1 where 30/10 16:04 sup : (I : Set) -> (I -> Ens) -> Ens 30/10 16:04 how do I get that to go? 30/10 16:04 ah Set1 30/10 16:05 roconnor_: I can't seem to get powersets to work with it 30/10 16:05 yeah, I was just using the \_ for the emacs input thing 30/10 16:05 you can put I : Set1, then you can use I -> Set as index set 30/10 16:05 *but* I can't get elementhood in Set 30/10 16:05 didn't try that much though 30/10 16:05 well, as of recently, you can explicitly work with arbitrary levels 30/10 16:05 but I think you'll need the darcs version for that 30/10 16:06 So instead of Set\_1 you have Set 1 (where 1 is a built-in level type) 30/10 16:06 Set (suc zero) ;) 30/10 16:06 it doesn't have syntactic sugar yet? 30/10 16:06 maybe I didn't enable it 30/10 16:06 maybe you're right :) 30/10 16:06 don't have the latest agda on this computer and am too lazy to compile it now to check :P 30/10 16:07 can you axiomatize classical set theory with: postulate S : Set 30/10 16:07 postulate _∈_ : S -> S -> Bool 30/10 16:07 ? 30/10 16:07 seems much more computational than S -> S -> Set 30/10 16:07 um 30/10 16:08 how do I write an anonymous function in Agda? 30/10 16:08 haskell syntax 30/10 16:08 (\lambda x \r moo x) 30/10 16:08 ugh 30/10 16:08 so much typing 30/10 16:08 :P 30/10 16:08 that doesn't work in emacs 30/10 16:09 I type \ 30/10 16:09 and the next character goes crazy 30/10 16:09 ah 30/10 16:09 anyhow 30/10 16:09 must go to lunch now 30/10 16:09 it needs to go through various other things 30/10 16:09 before hitting lambda 30/10 16:09 will deal with this later 30/10 16:09 funcompo should be universe polymorphic right? 30/10 17:05 FunctorSalad_: okay, I can define a "Power set" but I doubt I can prove it's defining property. 30/10 18:26 FunctorSalad_: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a11344 30/10 18:26 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 why shouldn't it work? 30/10 18:29 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 at least Martin Lof type theory doesn't have enough strength to prove Z is consistent. 30/10 18:30 FunctorSalad_: but you are exactly right. 30/10 18:31 If I try to prove a mem Power b <-> a subset` b, I don't think it will were 30/10 18:31 because I have only Set valued predicates, and I would need something like Set2 valued predicates as you say. 30/10 18:32 roconnor what is Z? 30/10 18:35 ZFC without the FC? 30/10 18:35 maye spoil the fun but you can find defiinitions and proofs in Benjamin Werners paper 30/10 18:36 god damn wireless 30/10 18:39 roconnor did you read my ? question 30/10 18:39 what is Z? 30/10 18:39 nope 30/10 18:40 Z is Zermelo set theory 30/10 18:40 okay 30/10 18:40 essentially ZF without the replacement axiom 30/10 18:40 techincally Z also has no foundation axiom, but no one cares about that. 30/10 18:40 why not?? 30/10 18:40 because only set theoriests care if sets are well-founded 30/10 18:41 heh 30/10 18:41 everyone else is using sets to do encoding. 30/10 18:41 to do real math 30/10 18:41 they don't care about the structure of their codes. 30/10 18:41 I think real math should stop using logical foundations 30/10 18:42 category theory is in fashion 30/10 18:42 heh did you write that wikipedia line that foundation is "arguably the least useful axiom in ZFC"? 30/10 18:42 nope 30/10 18:42 -!- roconnor__ is now known as roconnor 30/10 18:42 I was simply repeating it here. 30/10 18:42 :) 30/10 18:42 wikipedia is my source for all of what I am saying 30/10 18:42 FunctorSalad_: I go my member predicate to be in Set1 instead of Set2 30/10 18:44 but that still isn't low enough. 30/10 18:44 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a11346 30/10 18:45 hmm 30/10 18:46 this is wrong 30/10 18:46 is the model good for anything except showing that the axiomatic approach is consistent in agda? 30/10 18:47 I mean, good for using the resulting set theory 30/10 18:48 well, I was given the semantics of a logic in set theory 30/10 18:48 I'm trying to formalize it. 30/10 18:48 is ~ not? 30/10 18:49 FunctorSalad which model ? 30/10 18:49 fax: this Ens model I / FunctorSalad_ are writing. 30/10 18:49 roconnor: I mean, does constructing a model for set theory help you with that formalization, compared to postulating the axioms of set theory 30/10 18:50 ya 30/10 18:50 probably not 30/10 18:51 other than giving evidence that the axioms are sound. 30/10 18:51 I don't have much justification beyond wanting to do this. 30/10 18:51 ah finally got to the crux of the matter 30/10 18:53 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a11349 30/10 18:54 in Coq, forall (A : Type (*1*)), Prop  has type Prop, but in agda it has Type (*1*). 30/10 18:55 so 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 which is the impredicativity of Coq. 30/10 18:56 roconnor can't you just duplicate the def. of negation on different levels to define this in Agda? 30/10 18:56 ero 30/10 18:56 forall (A : Type) (something in prop) ... 30/10 18:56 oh no you couldn't 30/10 18:57 fax: 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 er 30/10 18:58 I mean to change mem, subset and equiv to return Set. 30/10 18:58 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=11344#a11350 30/10 18:59 Result for command Check forall (A:Type), True . : 30/10 19:00 Type (* Top.4183 *) -> True 30/10 19:00 : Prop 30/10 19:00 Result for command Check forall (A:Type), unit . : 30/10 19:00 Type (* Top.4184 *) -> unit 30/10 19:00 : Type (* max(0, (Top.4184)+1) *) 30/10 19:00 -!- roconnor_ is now known as roconnor 30/10 21:16 -!- Saizan_ is now known as Saizan 30/10 21:31 --- Day changed Sat Oct 31 2009 Huh, updating to the new version of ubuntu changed a lot of the unicode characters in emacs. 31/10 09:41 Hi. 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 byorgey 31/10 13:47 what does it mean when agsy says "Meta variable kind not supported: Sort (Type (Var 0 []))"? 31/10 15:22 hmm does agda automagically resolve the ambiguity between Data.List and Data.Vec symbols? 31/10 16:05 I have imported both and [] works 31/10 16:05 are there type synonyms? 31/10 16:15 oh right they are just plain definitions =) 31/10 16:19 FunctorSalad: yeah, you get overloading for constructors 31/10 16:47 how can I do this? foo = ..... (\n -> case elimFin1 n of refl -> ....) .... ? 31/10 17:28 (the notation if there was case) 31/10 17:28 use a with 31/10 17:28 inside the lambda? 31/10 17:30 not sure how you'd use it with a lambda 31/10 17:31 guess I'll have to mess with subst instead of pattern matching on the refl? 31/10 17:48 that might be easier 31/10 17:48