Saizan liyang copumpkin --- Log opened Sun Aug 01 00:00:38 2010 no, that's probably the most annoying thing about universe polymorphism 01/08 00:01 copumpkin: http://www.demotivator.org/index.php/customize/create_image/1280619296 01/08 00:37 hmm that link didn't work, it just took me to a generic page 01/08 00:38 http://liyang.hu/crap/mycode.png 01/08 00:40 MY EYES 01/08 00:40 GIVE THEM BACK 01/08 00:40 what is it? 01/08 00:40 I'm not quite sure yet… :-/ 01/08 00:41 what's the general topic? :P 01/08 00:43 transactional memory. ;_; 01/08 00:45 Was inspired by something you said on #haskell. 01/08 00:45 oh yeah 01/08 00:47 The absurdity of that ↣-READ′ lemma is that the RHS is always ‘r’. >_<;; 01/08 00:55 :O 01/08 00:59 * Saizan now wishes for a "unify as if it were injective" pragma :\ 01/08 09:01 * Saizan has 222 unresolved metas now. 01/08 09:02 wow 01/08 10:06 what are you proving? 01/08 10:06 what is dependently-typed? 01/08 12:25 types with arbitrary expressions in them ;) 01/08 12:26 is coq also dependently-typed? 01/08 12:26 yep 01/08 12:26 some people that dealed with coq said it's a bit difficult to grasp 01/08 12:26 is there an agda tutorial somewhere?:P 01/08 12:27 sort of 01/08 12:27 oh yeah 01/08 12:27 accessing wiki 01/08 12:27 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 01/08 12:27 dark weren't you asking how to do classical logic in coq? 01/08 12:29 yes, I actually asked en passant, my problem was other (how to derive a natural deduction proof for a theorem) 01/08 12:30 I hope you realize that the logic of agda is not close to classical logic either 01/08 12:30 I then learned about those hints and that if I add the law of excluded middle, I get classical logic 01/08 12:30 lol, http://snapplr.com/5032 01/08 12:30 dark: if you want to add LEM, the coq prop/set distinction is probably better for you than agda 01/08 12:31 but agda is fun to play with as a haskell-alike with stronger types :P 01/08 12:31 if_then_else_, o.o 01/08 12:34 illuminating 01/08 12:34 it's cool but I don't think I've ever used that function 01/08 12:34 "the type of non-empty lists" is interesting 01/08 12:40 Eventually Trellys will be done, and you'll get to do classical reasoning in a propositional fragment of the language, and general recursion in another fragment. 01/08 12:40 interesting 01/08 12:41 And unrestricted side effects, too. 01/08 12:42 Which is a little less exciting, perhaps. 01/08 12:42 oh, hm 01/08 12:42 lots of interesting stuff happening in this field 01/08 12:43 we need more people on it to make it happen faster! :P cause if one person takes time T, then two people will take T / 2, duh 01/08 12:44 Maybe you can test that hypothesis, and write a book about it. 01/08 12:45 You could call it... 01/08 12:45 The Mythical Man-Month. 01/08 12:45 That's a pretty good title. 01/08 12:45 something that always puzzled me: can you represent the type of elipses by their characteristic equation? and the type of circles as well 01/08 12:45 when I mention this problem, people come with this soluton: class Elipse { .., class Circle { .., and then make one inherit from the other 01/08 12:46 :P 01/08 12:46 dark: clearly you need dependent subtyping! 01/08 12:47 it's not about what I need but if it can be done at all 01/08 12:47 I'm of course confused about this problem, but it would be something like.. I write a complex expression, the compiler tries to reduce it to some known expression form, say a circle. if it can, then I can pass it as a circle 01/08 12:51 now I have the type of curves, and a subtype of it, that is the type of circles 01/08 12:52 and then I can pass a circle as elipse, but not every elipse as circle 01/08 12:52 That's asking quite a bit. 01/08 12:53 it looks like that type of non-empty list.. 01/08 12:53 if this is possible at all, I think one has to be careful to not let the base type of curves to be too complex, or else checking if a type is a circle is undecidable 01/08 12:54 for example, representing curves as lambdas would not work.. 01/08 12:54 s/is undecidable/would be undecidable/ 01/08 12:55 you can use a dependent pair to model circles 01/08 12:57 circular :: Ellipse -> Set 01/08 12:57 Circle = Sigma Ellipse circular 01/08 12:57 Sigma Ellipse? 01/08 12:58 Sigma is like a haskell pair (a, b), but the _type_ of b depends on the value of a 01/08 12:58 It's also like a sum. 01/08 13:00 yeah 01/08 13:00 Generalized to arbitrary index sets. 01/08 13:00 it's a pretty awesome type, overall 01/08 13:00 Ellipse -> Set is the type of functions that receive an ellipse and returns.. a type? 01/08 13:00 dark: yeah, that type would typically either be the empty type or the unit type 01/08 13:01 empty type for false and unit type for true 01/08 13:01 so it would check if the ellipse is a circle, and if so return unit, which then would make writing the pair trivial (since the second would just contain tt, the only constructor) 01/08 13:01 if instead it isn't a circle, then you couldn't form a pair because you'd need to provide an element of the empty type for the second half of it 01/08 13:02 dark: make sense? 01/08 13:05 no.. there are other types at Set 01/08 13:09 yes, but circular doesn't return them 01/08 13:10 so a definition of circular might be 01/08 13:10 circular (Ellipse x) = if isCircle x then Unit else Empty 01/08 13:10 where data Unit : Set where tt : Unit 01/08 13:11 and data Empty : Set where -- nothing here 01/08 13:11 I was thinking this: if you define a curve as (the roots of) a polynomial on x and y, and define an ellipse as a polynomial that meets some definition (such as http://en.wikipedia.org/wiki/Ellipse#General_ellipse ).. 01/08 13:11 you could then make a function that accepts polynomials that are ellipses. and if you define circles too, you can hopefully show that every curve that passes as ellipses is also accepted as circle 01/08 13:12 without needing to define circle as a special case of an ellipse 01/08 13:12 what does this have to do with dependent types?? 01/08 13:12 soupdragon, I saw "the type of the non-empty list" on that paper 01/08 13:13 it looks like "the type of this arbitrary subset of this more general type" 01/08 13:13 that looks like "the type of this arbitrary subset of polynomials" 01/08 13:13 arbitrary subsets are Sigma 01/08 13:14 dark: say we have a type T, and a proposition, P : T -> Set, then Sigma T P is those t : T such that P t is true (inhabited). 01/08 13:18 dark: so for your example, T = Curve. You would then have propositions Elipse t and Circle t and prove that Circle t -> Elipse t. 01/08 13:19 as a footnote,  he in some part say "Since checking type inhabitation is undecidable.", so it seems that agda can't do this checking in the general case 01/08 13:20 you need proofs :) 01/08 13:20 nothing comes for free 01/08 13:20 the mere existence of a total (+ invertible?) function Circle t -> Ellipse t is sufficient for asserting that all circles are ellipsis? 01/08 13:23 well, forall t. Circle t -> Ellipse t, but pretty much, yes. 01/08 13:24 I was hoping it were something without convertions (like there, where I can have a value that is both a list and a non-empty list) 01/08 13:24 dark: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28467#a28467 01/08 13:25 well the value here is t which is both a circle and ellipse, the Circle t and Ellipse t are the proof of this fact rather than the circle/ellipse itself. (in practice/convenience wise the distinction doesn't make much difference though) 01/08 13:26 ah 01/08 13:27 @.@ 01/08 13:27 ps: unicode, yay=) 01/08 13:27 :P 01/08 13:27 dark: does that code make more sense? 01/08 13:28 yes 01/08 13:29 you could use any inhabited type as "true" but ⊤ carries no additional information 01/08 13:29 so is often what you want 01/08 13:30 how do you type such chars? 01/08 13:32 in agda-mode in emacs, you can type backslash followed by some representation of the character 01/08 13:32 \top = ⊤ 01/08 13:32 \bot = ⊥ 01/08 13:32 \bn = ℕ and so on 01/08 13:32 * copumpkin is going crazy trying to write this arity-generic function 01/08 13:38 oh nice, someone fixed the agda haddock 01/08 15:58 now I can look and it and wonder why there are two semirings in it :) 01/08 15:59 I guess one is a class and the other is a record 01/08 15:59 C-c C-r is handy 01/08 16:05 copumpkin: re what i'm proving:  http://code.haskell.org/~Saizan/bisim/ObsEq.agda <- which i actually did months ago when the injectivity-check bug meant that all those metas were resolved :\ 01/08 16:14 oh my 01/08 16:16 Which bug? 01/08 16:17 A telescope is a sequence of typed bindings. Bound variables are in scope in later types. Or it's the mysterious Thierry-function-telescope. Only it's not. 01/08 16:29 http://code.google.com/p/agda/issues/detail?id=170 <- it's related to this one, but i can't find it 01/08 16:30 (i should probably say "constructor-headed" rather than "injective", since that's apparently what is checked) 01/08 16:30 Ah. 01/08 16:33 the "bug" was that recursive calls were considered constructors for the sake of this check 01/08 16:37 with the effect of making type inference make guesses that were wrong in some cases 01/08 16:39 copumpkin: sounds scary. 01/08 16:41 just found that in the agda source 01/08 16:41 maybe it's not the most scary thing around then :) 01/08 16:43 (A : Set) (P : A -> Set) (x y : A) (eq : x == y) (Px : P x) is a telescope. 01/08 16:45 Or something like that. 01/08 16:45 but Thierry-function-telescope ? 01/08 16:47 I'm not sure how to read those sentences. That might just be another reference for what they're talking about. 01/08 16:48 I'm not sure who coined the name "telescope." It may well have been Thierry Coquand. 01/08 16:49 why are they specifically named? 01/08 16:49 I guess they're useful? :P 01/08 16:49 where might one use them? 01/08 16:49 You can make a telescope datatype, too. 01/08 16:51 data Telescope : Set1 where nil : Telescope ; cons : (S : Set) (S -> Telescope) -> Telescope 01/08 16:52 Or something of that sort. 01/08 16:52 Of course, that has limitations. 01/08 16:54 they are used to represent environments/contexts where the types of later elements can depend on the value of the former ones 01/08 16:55 interesting 01/08 16:56 thanks agsy for inserting  an f = f proof for me 01/08 20:22 :O 01/08 20:23 hmm, I need to prove that equality on my permutations is decidable! 01/08 21:18 this seems tricky 01/08 21:18 "on my permutations"? 01/08 21:18 I branched off my original array stuff and decided to work on the permutations side of things for a bit 01/08 21:19 I think I may be OCD 01/08 21:25 You don't have to be, but it certainly helps. 01/08 21:25 two things that bother me about agda are that the source code contains SemiRing and Semiring, and that the std lib contains Data.Fin.Props and Data.(Nat|Vec|...).Properties 01/08 21:26 :P 01/08 21:26 mmm, I want to prove stuff about decidable equality on Fin-domained functions 01/08 22:08 well the theory of bijections on Fin n can get pretty deep 01/08 22:37 seen .BagAndSetEquality ? 01/08 22:39 has a nice treatment of permutations, imho 01/08 22:40 http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.Any.BagAndSetEquality.html#270 ? 01/08 22:40 yeah, i guess what i was really referring to is http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.Any.html#4828 01/08 22:45 i never used it though, it only looked nicer than my more inductive treatment :) 01/08 22:47 how did you do it? 01/08 22:47 there was an fplunch post about that stuff iirc 01/08 22:49 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28484#a28484 01/08 22:51 --- Day changed Mon Aug 02 2010 I wish I could partially apply implicit variables somehow 02/08 11:43 What does that mean? 02/08 11:47 I have a lot of λ {x} {y} → ⁻¹-cong {n} {x} {y} 02/08 11:48 just writing -1-cong {n} turns yellow 02/08 11:49 because it won't pass the input {x} and {y} to the cong 02/08 11:49 Oh. 02/08 11:49 copumpkin: make the {n} explicit and move it after {x} and {y}? 02/08 12:38 I can't move it after x and y, cause x and y depend on it :/ 02/08 12:39 Sometimes it's just not worth using implicit arguments. :-/ 02/08 12:40 I can't really change this though :( I'm building an algebraic structure from Algebra and it expects a proof in that form 02/08 12:40 k 02/08 15:21 oops sorry 02/08 15:21 http://code.haskell.org/~Saizan/agda-reflection/doc/main.tex 02/08 16:37 I guess that paper is still unreleased? 02/08 16:38 quoteGoal is pretty magical 02/08 17:00 copumpkin: re decidable permutations: would this help? http://acandystore.org/agda/Retract.html 02/08 17:05 (an extension of dolio's http://code.haskell.org/~dolio/agda-share/DecEq.agda) 02/08 17:06 basically, if you can define an embedding of your permutations into sexps then you get decidable equality for free 02/08 17:07 example at the bottom 02/08 17:08 I see! that seems quite nice :) 02/08 17:08 I'll play with that, thanks! 02/08 17:09 just express your perms like (1 3 4 2) and you're all set :P (easier said than done?) 02/08 17:12 gl 02/08 17:12 thanks :) 02/08 17:12 yeah, it should be that easy 02/08 17:13 I already have a transformation to a Vec (Fin n) n 02/08 17:13 ah! excellent 02/08 17:13 not that I really needed decidable equality for anything :P 02/08 17:13 maybe I do 02/08 17:13 (that url is darcs-able, btw) 02/08 17:14 cool! 02/08 17:16 http://code.haskell.org/~Saizan/agda-reflection/rls1/prop_logic/MyReflection.agda is amusing 02/08 17:25 they set up a datatype with a constructor course 02/08 17:25 and a mixfix one _is_of_ 02/08 17:25 and so all the proofs end in of course 02/08 17:26 cute 02/08 17:26 as in, ‘… as a matter of course’? 02/08 17:27 i have a type error "A !=< if b then A else A". what's the right way to deal with this? 02/08 17:47 should i just code up my own eta contraction for Bool? 02/08 17:47 or is there something slicker? 02/08 17:48 danbrown: write a lemma : \all b A \-> if b then A else A \== A, then use rewrite lemma. 02/08 18:08 I think you just need to code up your own 02/08 18:08 where can i read about 'rewrite'? 02/08 18:09 here? http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6 02/08 18:10 yeah 02/08 18:10 it mostly gets rid of the need for subst I think 02/08 18:10 if you have p : x == y and write rewrite p, it'll replace all instances of x with y in your goal and context types 02/08 18:11 dolio said it's equivalent to just pattern matching on refl and filling in the right patterns 02/08 18:11 do i have to use it at top level? 02/08 18:11 yeah, that makes sense 02/08 18:12 you can stick it before any = in a function definition I think 02/08 18:12 so f x with rewrite p x = ? 02/08 18:12 without the "with" 02/08 18:12 f x with moo x \n ... | m rewrite p m = ? 02/08 18:13 With rewrite though, there seems to be less scope for leaving out implicit arguments and letting Agda infer them. 02/08 18:13 you can also rewrite by a bunch of things with pipes between them 02/08 18:13 rewrite p  | q | r = ... 02/08 18:13 cool 02/08 18:14 I love it 02/08 18:14 that should nicely solve my first problem 02/08 18:14 (or you can also write f x rewrite y with g z\n…) 02/08 18:18 ah, hadn't tried that 02/08 18:18 It depends on where/when you want the rewrite to happen. Sometimes you might want to rewrite by the same == proof twice, in which case the ==.inspect idiom is useful too. i.e. f x with g x\n… | c z with-== gx==cz rewrite gx==cz = … and then use another rewrite gx=cz later on. 02/08 18:21 ah yeah, I've used that 02/08 18:22 mysterious failure... oh well. i'll stick to manual eta expansion for now :/ 02/08 18:30 danbrown: rewrite does give the same kind of mysterious error messages as with sometimes 02/08 18:30 mentioning a w variable 02/08 18:30 sometimes I've found that calling sym on it will fix it 02/08 18:30 this was just a "failed to solve constraints" 02/08 18:31 oh :o 02/08 18:31 _1574 w == _1584 w : _1532 w 02/08 18:31 indeed mentioning a w variable ;) 02/08 18:31 oh, did you put a hole in the rewrite expression? 02/08 18:31 yes 02/08 18:31 or does it have implicits that can't be inferred 02/08 18:31 yeah, it won't know what to do if the rewrite expression isn't fully determined I don't think 02/08 18:32 oh 02/08 18:32 when i bottom it out i get a different "failed to solve constriants": if b then _1477 w else _1487 w == _1497 w : Set 02/08 18:32 doesn't look like it made much progress :P 02/08 18:33 Yeah, as annoying as writing ==.subst is, it is often able to infer implicits that you can't leave out with rewrite. 02/08 18:33 well, i do have lots of implicit args flying around 02/08 18:33 Instantiate them one by one until Agda stops complaining. :3 02/08 18:34 lol, I see our workflows have things in common :P 02/08 18:34 yeah, the usual strategy. ;) i don't think it's worth the trouble to track down now, though. manual eta expansion works fine for now and writing this little function wasn't my main goal today. 02/08 18:36 way too easy to get lost in details 02/08 18:36 damn details 02/08 18:37 (this function is quite ugly, though) 02/08 18:37 does anyone know of any work on making a solver for ordered (semi)rings that can figure out inequalities? 02/08 19:32 error message: "Cannot split on the constructor foo when checking the definition of f" 02/08 22:57 what does that mean? 02/08 22:57 i'm starting to write a function matching on a large datatype and gave it a catch-all _ pattern at the bottom 02/08 22:58 well, but the error is actually on another line, so nm that 02/08 22:58 In my experience, that happens when trying to do case analysis on an indexed type, and the index is not a variable. 02/08 22:59 Oh, and possibly when the refined index would involve an arbitrary function. 02/08 23:01 For instance, I have a permutation type where one of the constructors is like: foo : (xs ys) -> (xs ++ ys) ~ (ys ++ xs) 02/08 23:02 So, in a certian proof, you may have (x :: xs) ~ ys. 02/08 23:02 bar with that type, say. 02/08 23:02 copumpkin: presburger can do inequalities, yes? 02/08 23:03 If you try to match on bar, it will give that error. 02/08 23:03 stevan: not sure, don't know much about it, but it's a lot weaker than a general semiring, right? 02/08 23:03 Because the (x :: xs) and the (xs ++ ys) are incompatible. 02/08 23:04 You can't refine the former to get the form of the latter in any reasonable way, I guess. 02/08 23:04 copumpkin: i don't know much about it either :-). you can't have multiplication between variables, so it's weaker i believe 02/08 23:05 stevan: from what I understood, people liked it because everything was decidable in it 02/08 23:05 stevan: but I just need inequalities :) 02/08 23:06 Isn't it complete or something? 02/08 23:06 (btw, Gallais (who is working on the reflection thing in agda you linked to earlier) is working on presburger in agda too, it seems). 02/08 23:07 yeah, I saw that in his reflection folder 02/08 23:08 looks cool :) 02/08 23:08 it seems like the same technique used in the semiring equality solver could be used for inequalities, but maybe not 02/08 23:09 dolio: ok, it might be because i'm trying to sketch something out at a high enough level that it's totally incoherent until i ground out some of the details 02/08 23:12 i'll comment out the bad constructor for now and keep that in mind as i refine my development 02/08 23:13 whats the difference in pattern matching between (.e :: .e0) and .(e :: e0)   ? I see they behave differently in type checking but I'm fuzzy on exactly whats going on 02/08 23:13 Are you sure there's a difference? 02/08 23:14 I get different errors in the emacs mode. 02/08 23:14 so yes. 02/08 23:14 Huh. 02/08 23:14 I don't think there's much difference, in the above case where :: is a constructor. OTOH you could have .(e ++ e') 02/08 23:15 maybe its type checking errors manifesting at different places 02/08 23:15 maybe there are implicits 02/08 23:15 and putting a dot around the entire thing is the same as dotting the implicits too? 02/08 23:15 yeah maybe thats whats ahppening for me 02/08 23:16 i'm not expert, but i read the first as, "once you constrain this to the _::_ constructor, it's determined what e and e0 are", whereas i read the second as, "this input will be a cons of e and e0" 02/08 23:16 *no expert 02/08 23:16 I have a giant pattern with {.e :: .e' :: .v'} in it somewhere which gives a ucn' != suc n of type N 02/08 23:16 but if I change to {.(e :: e' :: v')} that goes away 02/08 23:17 You can write that as .{e :: e' :: v'} , btw. 02/08 23:17 ok 02/08 23:18 * liyang isn't sure he could explain the suc n' != suc n error without a concrete example. 02/08 23:18 #1 "if this is a cons then it's a cons of e and e0", #2 "this is a cons of e and e0" 02/08 23:19 not sure that #1 makes sense, though 02/08 23:19 seems like #1 implies #2 02/08 23:19 The multiple-dots version might do cons-matching first, technically. 02/08 23:20 so I can put .{any expression, not just a constructor pattern}   ? 02/08 23:20 benc___: yeah 02/08 23:20 ok 02/08 23:20 I wouldn't expect that to really make a difference, except for having to write absurd cases. 02/08 23:20 benc___: sometimes you'll see crazy stuff in pattern matches :P 02/08 23:20 benc___: yes, .{any expression} 02/08 23:21 You don't have to fill in anything after a dot though—Agda already knows what goes there—you can just use a wildcard _. 02/08 23:27 It helps you to see what's going on though, of course. 02/08 23:28 So writing ._ instead of .(some expression) makes no difference for Agda, and might make the code easier on the eyes, my previous remark aside. 02/08 23:30 --- Day changed Tue Aug 03 2010 I wish I knew how to fold text in Emacs. :( 03/08 03:43 * liyang misses Vim. 03/08 03:44 * benc___ wakes up again 03/08 08:40 * Saizan never sleeps 03/08 09:59 * Amadiro hi 03/08 17:44 hi 03/08 17:44 hi 03/08 17:45 hi! 03/08 17:50 Hm, I have to remember that. If I feel down next time, I'll just "/amsg hi", and see all the friendly responses :D 03/08 17:51 anything in the standard library for floats,rationals,smething like that? 03/08 19:16 * benc___ wants to play with physical quantities annotated by their SI units, in a scuba dive program 03/08 19:17 rationals 03/08 19:18 right 03/08 19:18 but no operations on them yet 03/08 19:18 where? 03/08 19:18 ok 03/08 19:18 Data.Rational 03/08 19:18 so "no" ;) 03/08 19:18 hey, the basic type is there :P 03/08 19:18 not in my 0.3 that i have here 03/08 19:18 it should be there 03/08 19:18 oh wait 03/08 19:18 it is 03/08 19:18 * benc___ was only looking at subdirectories not files 03/08 19:18 doh 03/08 19:18 else i wouldn't even have asked here 03/08 19:19 data.rational and data.float was there first place i looked! 03/08 19:19 :) NAD said that someone had worked on filling in the Rational code but I'm not sure what happened with that 03/08 19:19 * benc___ doesn't really mind building stuff up from low levels but its frustrating to find someone already did it 03/08 19:20 dolio wrote a useful function for that a while back 03/08 19:20 but I can't remember where it is 03/08 19:20 What? 03/08 19:21 to help definition of rational functions 03/08 19:21 I thought 03/08 19:21 Oh. 03/08 19:21 http://code.haskell.org/~dolio/agda-share/html/Rat.html 03/08 19:21 aha, that's the one 03/08 19:22 truthFromWitness is now a library function 03/08 19:22 toWitness I think 03/08 19:22 Is it? I wrote the thing in there because it was a counterpart to what was in the library. 03/08 19:23 oh 03/08 19:23 yeah, silly me 03/08 19:23 --- Day changed Wed Aug 04 2010 wow, that fp-lunch reflective presburger solver is pretty large 04/08 00:06 yeah. 04/08 00:07 MY EYES 04/08 00:09 liyang: I just found something worse than your picture 04/08 00:09 I've heard of walls of code before, but holy shit: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28526#a28526 04/08 00:09 is that The Matrix? 04/08 00:11 yep 04/08 00:13 it looks more terrifying with wrap on 04/08 00:13 now I really want to ask it to solve me some presburger arithmetic statements 04/08 00:14 ‘lol’. 04/08 00:47 ¯\(°_0)/¯ 04/08 00:48 There's no way to improve that code? 04/08 00:48 What's that from? 04/08 00:48 I'm not sure how that was even written in the first place. 04/08 00:49 The .(fdsjllvkdfml) patterns can be left out by replacing them with ._ 04/08 00:49 Even the type signature is pretty heinous. 04/08 00:51 darcs get http://patch-tag.com/r/gallais/agda 04/08 00:51 who is gallais? 04/08 00:53 INRIA guy. 04/08 00:53 ah 04/08 00:54 (I think. Did he visiting Nottingham? I don't know, I haven't been in the office for months…) 04/08 00:54 I find it a bit strange-looking though, e.g. in the signature: Σ (b ∈ (bset φ)) (λ _ → x ≡ ([| proj₁ b |]e ((+ 0) ● ρ)) ℤ+ (+ toℕ j)) 04/08 00:58 That's just a non-dependent product A × B… 04/08 00:58 yeah, it looks at least partially automated 04/08 00:58 but I'm not sure what would've done that for him 04/08 00:58 agsy can't figure out way simpler stuff than that 04/08 00:58 And a lot of parentheses could have been left out with judicious assignment of operator fixities. 04/08 00:59 (I still have no idea what it does.) 04/08 00:59 cooper's algorithm is apparently one way to decide statements in presburger arithmetic 04/08 01:00 i think the type is probably copy-pasted from a hole's type, and the rest is constructed by C-c C-c 04/08 01:00 * copumpkin just discovered C-c C-r the other day 04/08 01:01 made me quite happy 04/08 01:01 I only know half of what it does though 04/08 01:01 Mmm… but C-c C-c generates quite messy code though. 04/08 01:01 It'll name all the implicit arguments when matching on a constructor purely so they can be used in a .(…) pattern elsewhere. You can do a lot to tidy it up by writing ._ instead and getting rid of the implicits. 04/08 01:03 If you have a whole bunch of implicits, and only need one of the later ones, it'll fill in all the ones before it too… when you could use {x = foo} patterns. 04/08 01:05 Hi, can anyone point me towards a tutorial on Theorem proving with agda please? 04/08 01:34 Introductions to Agda: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation 04/08 01:39 I get the impression Berengal was having connection issues 04/08 11:05 Looks that way. 04/08 11:32 So, I read yesterday that some people consider W-types to be impredicative. 04/08 11:32 W-types being the arbitrarily branching trees? 04/08 11:33 Yes. data W (A : Set) (T : A -> Set) : Set where sup : (x : A) -> (T x -> W A T) -> W A T 04/08 11:33 Apparently some people have decided that "predicative" means "has proof-theoretic ordinal less than or equal to Gamma_0." 04/08 11:35 But theories with W-types have ordinals bigger than that. 04/08 11:35 At least, W-types + a single universe. 04/08 11:39 By contrast, Martin-Loef type theory with infinite universes, but no W-types apparently has a proof-theoretic ordinal of Gamma_0. 04/08 11:39 is there an overview of the universe level rules? 04/08 18:18 With or without universe polymorphism? 04/08 18:28 either, really 04/08 18:29 Well, if it's without, it's easy. 04/08 18:31 let's do without then 04/08 18:31 I have an intuitive understanding of it, but wanted to get a summary 04/08 18:31 in AGDA? 04/08 18:32 If |- A : SetM and x : A |- B : SetN, then |- (x : A) -> B : max(SetM, SetN) 04/08 18:32 And an inductive definition is valid if the types of its constructors have the same size as specified for the datatype. 04/08 18:33 that's it? 04/08 18:34 I think so. 04/08 18:34 There's records, I guess, but you can imagine 'record { ... }' being an appropriate n-ary constructor, and figure out the size of its type. 04/08 18:35 makes sense :) 04/08 18:35 With universe polymorphism, it's almost the same. 04/08 18:36 Except, instead you have 'Set m' and 'Set n'. And if x is free in n, the type of the pi is Set\omega. 04/08 18:37 which agda doesn't allow, right? 04/08 18:38 It's buggy in that area. 04/08 18:38 At least, I kind of consider it buggy. 04/08 18:38 It's more buggy when you try to do inductive types involving Set\omega. 04/08 18:39 It could, I think, allow things that it doesn't. 04/08 18:39 oh, Set\omega is a builtin? cause I looked at Level and there was no third constructor 04/08 18:39 Yes, it is not a constructor. 04/08 18:40 I think naming it 'Set\omega' is a mistake, too. 04/08 18:40 how come? 04/08 18:40 Because it gives the impression that \omega is a Level, and thus that quantification over level should range over it. 04/08 18:40 ah, as I guess happened with me :P 04/08 18:41 In my personal interpreter, I called that universe \Omega. 04/08 18:41 that's your pts? 04/08 18:42 upts. 04/08 18:42 The fork. 04/08 18:42 Which has become a little out of date. It still uses strings and alpha renaming for bound variables, so it's probably broken. 04/08 18:42 ah 04/08 18:43 Not so broken that it won't likely work for whatever small experiments you're doing. 04/08 18:44 But still broken. 04/08 18:45 I didn't discover that pts had problems until I was writing Hurkens' paradox. 04/08 18:45 dolio: isn't it different in CoC? If |- A : SetM and x : A |- B : SetN, then |- (x : A) -> B : SetN 04/08 20:07 dumb question: can someone explain to me how to use C-c C-c ? 04/08 20:24 the documentation isn't particularly helpful 04/08 20:24 you put the cursor over a hole, C-c C-c RET 04/08 20:25 it needs to be just a hole on the RHS 04/08 20:25 sometimes it'll not be able to figure it out 04/08 20:25 so "f x = {! x !}" ? or "f = {! x !}" ? or "f = {! f !}" ? 04/08 20:25 oh, the x needs to be there 04/08 20:25 so you can ask C-c C-c to split it 04/08 20:26 so there you'd type C-c C-c x RET 04/08 20:26 and it would give you all the valid cases for x 04/08 20:26 with one hole each 04/08 20:26 i don't put anything inside the hole 04/08 20:26 I don't think it makes a difference, but yeah, I usually leave it empty too 04/08 20:26 so i have g : ⊤ → ⊤; g x = {! x !}. when i try to split it says "Right hand side must be a single hole when making a case distinction. when checking that the expression ? has type ⊤" 04/08 20:27 hmm, how would one represent inductive families (GADT-style) in a low-level dependent LC? 04/08 20:27 danbrown: what if you leave the hole empty? 04/08 20:27 same 04/08 20:28 then you've probably encountered the bug that I submitted a couple of days ago 04/08 20:28 hrm 04/08 20:28 http://code.google.com/p/agda/issues/detail?id=289 04/08 20:28 so is all case splitting currently broken, or are we trying to do funny splits? 04/08 20:29 mine seems particularly simple :P 04/08 20:29 as do NAD's 04/08 20:30 *does 04/08 20:30 I've had it work for more complex ones 04/08 20:31 it generally works for me 04/08 20:31 not sure under what conditions it breaks 04/08 20:31 how is your T defined? 04/08 20:31 Saizan: from the stdlib: data ⊤ where tt : ⊤ 04/08 20:31 (with : Set something) 04/08 20:32 it's actually a record in the stdlib iirc 04/08 20:32 which might be the source of the problem 04/08 20:32 it works with a data decls 04/08 20:33 ok, that's fair. but data decls still don't work for me: data A : Set where a : A; f : A → A; f a = ? 04/08 20:33 same error 04/08 20:33 my original example was a data decl though 04/08 20:34 using Dec P 04/08 20:34 maybe because 'a' is a pattern? 04/08 20:34 Saizan: err, yes :P 04/08 20:35 it seems error reporting is quite poor :) 04/08 20:35 ok, that "data A" example does indeed work 04/08 20:35 "whatever happens, let's blame the RHS" :) 04/08 20:36 curious. the problem seems to occur when the _codomain_ is a record 04/08 20:38 :O 04/08 20:39 data → data and record → data both work, but data → record and record → record both fail 04/08 20:39 mh, that might make sense if there's some eta-expansion going on wrt the hole 04/08 20:40 oh, mine was using records too 04/08 20:40 just indirectly 04/08 20:40 you should comment on that ticket 04/08 20:41 copumpkin: my original problem (before g : ⊤ → ⊤) was also using Dec 04/08 20:41 i will 04/08 20:41 mine is actually using False and True 04/08 20:41 but those are functions that evaluate to \bot or \top 04/08 20:41 why is 04/08 20:42 \top a record, anyway? 04/08 20:42 because then it gets surjectivity 04/08 20:43 agda implements surjective/eta conversion for all records (since they have a single constructor) 04/08 20:44 just means more things typecheck 04/08 20:44 surjectivity in what sense? 04/08 20:44 when it comes down to it 04/08 20:44 ah 04/08 20:44 like surjective pairing 04/08 20:44 (fst p,snd p) = p 04/08 20:44 if you define pairs as a record ^ will be convertible 04/08 20:44 but if you define them as a data type it wil not be provable 04/08 20:45 in the case of T it's   t = x    (forall x) 04/08 20:45 since t is the only constructor 04/08 20:45 ah 04/08 20:45 in the case of LAMBDA it's  f = \x -> f x 04/08 20:45 which Agda does implement 04/08 20:45 oh and do you have any idea about my earlier question? about how inductive families / GADTs can be represented in a dependent LC? 04/08 20:48 (where the constructors refine the type) 04/08 20:49 you need a primitive equality type, at least 04/08 20:49 afaiu 04/08 20:49 yeah, Leibniz doesn't cut it 04/08 20:49 the reasons why are kind of subtle I can't remember them - Coq'Art covers it 04/08 20:49 hmm 04/08 20:57 is there no pdf of it? 04/08 21:00 I guess it's a real dead tree book 04/08 21:00 so I guess GADT-alikes mean that you can't really decompose ADTs into sums/products etc.? 04/08 21:07 copumpkin you should read Peter Morris' Thesis 04/08 21:07 well except skip the chapters on containers 04/08 21:08 unless you can actually understand that stuff.... (I can't) 04/08 21:08 but the rest is important 04/08 21:08 http://www.cs.nott.ac.uk/~pwm/thesis.pdf, right? 04/08 21:08 es 04/08 21:10 eys 04/08 21:10 yes 04/08 21:10 thanks :) will read 04/08 21:16 "Unlike in the case of strictly positive types there is no generative grammar on which to base the codes of a universe for strictly positive families. " 04/08 21:22 boo 04/08 21:22 danbrown: The CoC only has that rule if SetN is the lowest universe. If you have that rule for arbitrarily high universes, you can encode a paradox. 04/08 21:46 Of course, the basis CoC doesn't have too many universes. 04/08 21:46 so for Set(N+1) universes CoC uses the ITT-style rule? 04/08 21:48 In Coq, that's how Prop works, and Set works that way if you use --impredicative-set, but none of the Type universes work that way. 04/08 21:48 Yes. You must if you care about strong normalization. 04/08 21:49 hmm 04/08 21:50 can you succinctly explain to me the essential difference between ITT and lambda-cube-style type theory (e.g. CoC)? 04/08 21:50 i'm more familiar with the latter 04/08 21:51 and as far as i can tell they're very similar, so i'm wondering what different purposes each serves 04/08 21:52 They are pretty similar. 04/08 21:52 http://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/ 04/08 21:53 Some of the stuff there is pretty good. 04/08 21:53 not succinct :P 04/08 21:54 The Intuitionistic Type Theory article by Martin-Loef himself is really readable. 04/08 21:54 but thanks for the references ;) 04/08 21:54 I have to step out for a while. Maybe I can try to explain later. 04/08 21:54 ok 04/08 21:55 I was surprised how readable the Intuitionistic Type Theory book is. 04/08 21:55 have you read the handbook article? 04/08 21:56 Nordström, et al. 04/08 21:56 confusing problem with magic patterns—any insight? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558 04/08 22:05 it's possible that it's just a bug 04/08 22:06 but i'm not sure 04/08 22:06 if it is empty but agda can't see it, just use \bot-elim 04/08 22:07 what's with your accented letters? 04/08 22:07 ;) 04/08 22:07 hmm 04/08 22:08 oh, I see 04/08 22:09 wait, my agda got confused 04/08 22:09 yeah, ok. i don't see how ⊥-elim helps. 04/08 22:09 what's happening? 04/08 22:09 danbrown: remove the absurd pattern and you get some yellow, too 04/08 22:10 you need to put an accented pi into the implicits 04/08 22:10 ? but it's a constructor 04/08 22:10 oh yeah 04/08 22:11 well, you need to provide its implicits then :P 04/08 22:11 danbrown, that's weird - looks like a bug to me 04/08 22:11 oh, hmm 04/08 22:11 soupdragon: probably. trying to see if giving the implicits works around it... 04/08 22:13 ok, giving the implicit arguments appears to not help: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558#a28562 04/08 22:30 i'll file a bug 04/08 22:30 afaiu, it boils down to not be able to tell that "y ≡ (y + y') × s" should be empty. 04/08 22:32 shouldn't an occurs check be enough? 04/08 22:32 that's what i'd naively expect 04/08 22:33 how would you go about proving that type is empty without dependent pattern matching? 04/08 22:34 uhh... 04/08 22:34 i don't know where to start, formally 04/08 22:35 wait 04/08 22:36 wh does it come down to y ≡ (y + y') × s 04/08 22:36 ? 04/08 22:36 I thought it was just  that   π̀ {s} {t} ∙ M  isn't equal to either of  (ὶ ∙ V) or (ί ∙ V) 04/08 22:36 well, i've tried to convince agda of that by pattern matching on t first 04/08 22:37 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558#a28563 <- so i went down exploring it like this, if you try to pattern match on eq in the { }4 case of foo you get that problem 04/08 22:39 Saizan what about pattern matching on Val in ¬Valπ̀? maybe that would let you avoid having a lemma 04/08 22:40 well you'd get some equations to discharge, not sure if agda would do them automatically or not (hopefully would) 04/08 22:41 it doesn't let me do that 04/08 22:41 Saizan: i just created an issue, feel free to follow up: http://code.google.com/p/agda/issues/detail?id=291 04/08 22:41 I wish agda would install I want to have a look at this :/ 04/08 22:42 * copumpkin doesn't get why it's a bug 04/08 22:46 there are many things that agda can't spot are empty at first glance 04/08 22:46 i'm not sure it's a bug either 04/08 22:47 though i've no idea how to prove "y ≡ (y + y') × s -> \bot" indirectly 04/08 22:48 agsy can spot it's empty :) 04/08 22:50 copumpkin: can it convince agda? ;) 04/08 22:50 nope 04/08 22:50 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558#a28564 04/08 22:50 very nice 04/08 22:51 hehe, good old eliminators :) 04/08 22:51 How are those accented characters typed, by the way? Emacs wouldn't tell me? 04/08 22:52 Is it a separate accent character? 04/08 22:52 Like \^ will put a hat on the previous character? 04/08 22:52 dolio: yeah, they're "combining characters" in unicode. when you enter one they decorate the preceding character 04/08 22:53 dolio: i type them by manually entering a bunch into my .vimrc ;) the agda table for quail could be extended to include them 04/08 22:53 Heh. 04/08 22:53 (still grokking your solution) 04/08 22:55 I used the standard inductive eliminator for Val. 04/08 22:56 on the bottom line, is _ the only thing you can write there? 04/08 22:56 The predicate I was proving was false for pi-left indices, and true for everything else. 04/08 22:56 right 04/08 22:56 But, to prove predicates over Val, you only need to prove them for the iota-cases. 04/08 22:56 Which is trivial. 04/08 22:57 And dependent pattern matching actually works for writing the eliminator. :) 04/08 22:57 hmm 04/08 22:57 I'm not sure it doesn't work directly. I guess we'll see if it's a bug. 04/08 22:58 Not sure *why*, that is. 04/08 22:58 yeah, ok 04/08 22:58 It is somewhat different, though. 04/08 22:58 those _ at the bottom are of type ⊥, right? 04/08 22:59 Type top. 04/08 22:59 err, oh 04/08 22:59 yes 04/08 22:59 The predicate is top for the two iota cases. 04/08 22:59 danbrown: just out of curiosity, why the accents? :P 04/08 22:59 And since it's a record, agda fills it in. 04/08 22:59 dolio: right 04/08 22:59 I guess the manual way would be 'record{}' 04/08 23:00 I never think of that, though. 04/08 23:00 copumpkin: prettier. this is a highly pared-down version of my working code where i like to keep identifiers as short as possible. so π̀ beats π₁ 04/08 23:01 Where did I leave off? 04/08 23:05 manual way was record{} 04/08 23:05 Anyhow, the way that the absurd pattern works, if I remember correctly, is that Agda tries to use its unification algorithm to find a term of the relevant type. 04/08 23:05 dolio: thanks, btw 04/08 23:05 And if the algorithm returns a definite "there are no such terms", the absurd pattern works. 04/08 23:05 But I think that's kind of ad-hoc, so you may have found a corner case that nothing can be done about. 04/08 23:05 Or, not a term of the relevant type, but a constructor that targets the type. 04/08 23:05 I guess "no such terms" reduces to SAT 04/08 23:07 or is it worse than that? 04/08 23:07 I guess it is 04/08 23:08 Well, it might be higher-order unification in general, which is undecidable. 04/08 23:08 yeah, I see 04/08 23:08 This case doesn't look higher-order, though. 04/08 23:08 To me, anyway. I'm certainly no expert, though. 04/08 23:09 danbrown: So, did you find something explaining ITT vs. CoC, or should I still try? 04/08 23:18 dolio: I'd appreciate you trying, if you're still around :) 04/08 23:26 Well, for one, the lambda cube languages usually have impredicative polymorphism. 04/08 23:27 Which allows them to encode lots of inductive types using lambdas, but not their strong induction principles. 04/08 23:28 That doesn't matter in System F and stuff, but it matters in the dependently typed corners. 04/08 23:28 By contrast, ITT has lots of direct type formers. 04/08 23:29 Natural numbers, finite sets, pi, sigma, W, disjoint union and identity types. 04/08 23:30 as in, they're primitive? 04/08 23:30 They're all introduced like rules in natural deduction. 04/08 23:31 ah 04/08 23:31 And I think the usual presentation has judgments describing what things are sets. 04/08 23:32 So, you have 'finite sets are sets' and 'if A is a set, and B(x) is a set when x is in A, then Pi A B is a set'. 04/08 23:33 yeah 04/08 23:33 Which has none of the universe/sort stuff of the lambda cube type languages. 04/08 23:33 But, at the end, you introduce universes, induction-recursion style. 04/08 23:34 So, you say 'U is a set' and give rules for building elements of U, which correspond to all the ways of forming sets, except U itself. 04/08 23:35 And you have an eliminator T, such that 'if s is an element of U, then T s is a set'. 04/08 23:36 And along with all this, there are also eliminators for all the other sets, and judgments of equality, which are the computation rules, essentially. 04/08 23:37 And you're not limited to having just one U. You can have a U0, which has all the previous ways of forming sets (pi, sig, w, ...), and then U1, which has all of those, plus u0 and t0, and then U2 with all of those, plus u1 and t1, and so on. 04/08 23:38 Which is similar to the direct hierarchies of universes that Agda or Coq use. 04/08 23:39 Just presented differently. 04/08 23:39 wait, what are u0 and t0? 04/08 23:40 u0 is the name of U0 in U1. 04/08 23:40 oh ok 04/08 23:40 So u0 : U1, T1 u0 = U0 04/08 23:40 I see, yeah 04/08 23:40 And t0 s is the name of T0 s in U1. 04/08 23:40 I guess T may not be considered an eliminator per-se. 04/08 23:42 Anyhow, generalizing that style of definition is how you get induction-recursion. 04/08 23:43 It also means that Agda could get rid of everything above Set and still have all the power of Martin-Loef type theory, I think. 04/08 23:44 More, probably. 04/08 23:45 so Martin-Loef doesn't have higher universes? 04/08 23:46 The stuff in that short Intuitionistic Type Theory thing doesn't. It only has one U. 04/08 23:47 ah, I see 04/08 23:48 But he had multiple tweaks of the theory over the years. 04/08 23:48 Programming in Martin Lof Type Theory has an infinite heirarchy of universe 04/08 23:48 And I've heard there was one with multiple universes. 04/08 23:48 sorry that's not the correct title 04/08 23:48 I've been trying to figure out a minimal set of primitives for a simple DT normalizer I'm writing 04/08 23:48 Constructive mathematics and computer programming. <-- this  one 04/08 23:49 ah, I'll add that to my reading list 04/08 23:49 In fact, he must have had one with infinite universes and no W-types, considering I mentioned earlier that someone cited that as a theory which was considered predicative, but adding W-types was considered impredicative. 04/08 23:49 ah yes 04/08 23:49 frustrating all these martin lof papers are out there now 04/08 23:50 when I was obsessed with reading everything there is about type theory none of this stuff was available 04/08 23:50 aw 04/08 23:50 is pi, sigma, zero, one, and two sufficient for constructing all non-inductive family types? 04/08 23:51 (I was reluctant to add two, but couldn't figure out how to do it without it) 04/08 23:51 I think you need 2 04/08 23:51 yeah 04/08 23:51 martin lof gives N (which we call Fin) 04/08 23:51 N_0 N_1 .. 04/08 23:51 if I want to use sigma as a non-dependent sum I need two 04/08 23:51 yeah 04/08 23:51 I was reluctant to add that cause it seemed like more than was strictly necessary 04/08 23:52 now I'm trying to figure out that thesis you pointed me at to see how to add the inductive family stuff 04/08 23:52 Thorstin Alterkirch has some lecture note style document re. some of the basics of peter morris' work 04/08 23:53 oh, I'll poke around on his site to see if I can find that, thanks 04/08 23:54 Thorsten Altenkirch 04/08 23:54 copumpkin: You need W-types for all inductive types, I think. 04/08 23:54 http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf - but there's other good stuff there too which is related 04/08 23:54 dolio: what would that give me over the sums/products? 04/08 23:55 oh 04/08 23:55 I guess I can't really get recursion 04/08 23:55 Ordinals, for instance. 04/08 23:55 I think you'll have trouble doing ordinals without W-types. 04/08 23:55 hmm, probably 04/08 23:56 okay, so I should probably add W 04/08 23:56 soupdragon: thanks :) 04/08 23:56 --- Day changed Thu Aug 05 2010 W-types and a universe gets you some set theory, too. 05/08 00:00 You represent sets by W U T. 05/08 00:00 And you can get most all the ways of making a set besides powerset, I think. 05/08 00:00 All the ZF-ways, that is. 05/08 00:01 * copumpkin can't remember where he read about W types 05/08 00:01 maybe type theory and functional programming 05/08 00:01 that book felt like a description of agda 05/08 00:01 * Saizan first met them in the OOT paper 05/08 00:01 *OTT 05/08 00:01 so W, 0, 1, 2, pi, and sigma 05/08 00:06 is that sufficient for all types? 05/08 00:06 uh 05/08 00:06 that's sufficent for all types you can define with that 05/08 00:06 well :P 05/08 00:06 the question doesn't make sense as is 05/08 00:06 if you read Peter Morris' work it classifies types a bit more sharply than just ADT/GADT 05/08 00:07 okay, I'll keep reading :) 05/08 00:07 and also maybe have a look at some of the terrifying stuff from Peter Dybjer 05/08 00:07 :o 05/08 00:08 it sort of leaves out coinductive ones, except that you've pi which is a quite flexible one 05/08 00:08 oh yeah 05/08 00:08 I guess I could throw in # and b as defined in Coinduction, but I'll ignore it for now 05/08 00:09 I can never remember about coinductives 05/08 00:10 copumpkin: That's what OTT takes as primitive. 05/08 00:10 The old stuff, at least. 05/08 00:13 The problem with W-types is that you need extensional-ish equality to prove some of the induction principles for encoded types. 05/08 00:14 Like, you won't be able to prove induction on the naturals encoded as W-types. 05/08 00:15 oh 05/08 00:15 "This reflects the well known fact that the category of finite types is bicartesian closed." of course 05/08 00:38 usually remarks like that are a hint that you should just give up 05/08 00:39 :) 05/08 00:39 I think I actually get it, but it seems weird to remark that offhand 05/08 00:39 my favorite one is "as everyone knows,  1 + 2 + 3 + 4 + ... = -1/12" 05/08 00:39 hmm, I didn't know that ;) 05/08 00:40 "In a short period of less than a year, two distinguished physicists, A. Slavnov and F. Yndurain, gave seminars in Barcelona, about different subjects. It was remarkable that, in both presentations, at some point the speaker addressed the audience with these words: 'As everybody knows, 1 + 1 + 1 + · · · = −1⁄2'. Implying maybe: If you do not know this, it is no use to continue listening." 05/08 00:40 hah 05/08 00:40 -1/2? 05/08 00:40 Bicartesian closed means that it has binary sums and products, and exponentials, I believe. 05/08 00:42 Or maybe it's all finite sums and products. 05/08 00:42 I think exponentials too 05/08 00:43 Anyhow, convincing yourself of that shouldn't be too hard. 05/08 00:43 yeah 05/08 00:43 Yes, I said exponentials. :) 05/08 00:43 oh, I thought your second thing was contradicting your first, so I was contradicting what I thought you were saying :P 05/08 00:44 "A category is bicartesian if it is both cartesian and cocartesian, that is if both it and its opposite may be made into cartesian monoidal categories." 05/08 00:44 "A bicartesian category which is also cartesian closed (but not usually cocartesian closed) is a bicartesian closed category." 05/08 00:44 according to ncatlab 05/08 00:44 iirc if it's both cartesian closed and cocartesian closed it collapses into a category where all objects are isomorphic? 05/08 00:46 Ah. It's all products, then. 05/08 00:46 Bicartesian closed doesn't imply coexponentials. 05/08 00:46 But I seem to recall that being the case, yes. 05/08 00:47 agsy really needs to avoid writing f = f as solutions 05/08 00:57 it can be pretty helpful sometimes for writing simple stuff though 05/08 00:57 case splitting seems way buggier than it used to be 05/08 01:11 sometimes it forgets variables or swaps them 05/08 01:11 soupdragon: http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf is wonderful, thanks 05/08 01:59 btw, does anyone else edit agda code in vim? 05/08 05:37 i made a few improvements to what's on the wiki 05/08 05:37 i should post them at some point... 05/08 05:37 anyone here played with HOL light? 05/08 12:15 I spent some time reading the source code but I didn't get a lot out of it 05/08 12:16 ah 05/08 12:16 one thing I was wondering about in that pdf soupdragon pointed me at yesterday 05/08 14:17 (http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf) 05/08 14:17 oh, nevermind 05/08 14:18 "i.e. enumeration doesn’t work for context-free types because they contain types with an infinite number of elements" 05/08 14:18 was what I was wondering about, but the issue there is that you'd need codata, not that context-free types aren't enumerable? 05/08 14:19 What page? 05/08 14:19 26 05/08 14:20 under the little table of universes with representative operations 05/08 14:20 "Another possibility is to also allow coinductive context-free types like streams by including codes for terminal coalgebras, e.g. StreamX = νX.A×X. However, this doesn’t fit very well with our way to define El inductively." 05/08 14:21 I guess that sort of covers it, although it doesn't mention it explicitly for CF types 05/08 14:21 Well, certainly you can't fit an infinite number of values in a finite binary tree, which is what their enumeration does. 05/08 14:24 yeah 05/08 14:26 The stuff about coalgebras is an extension of context free types, though, if I understand correctly. 05/08 14:26 but with a context-free language, you can enumerate all strings in it, but of course there may be infinite such strings 05/08 14:26 I just wasn't sure if the issue was the finiteness or the un-enumerability 05/08 14:27 Yes, I imagine infinite binary trees would work. 05/08 14:27 ah, cool 05/08 14:27 Although I just skimmed the paper. 05/08 14:27 I found it pretty interesting, but you probably already know most of that stuff :) 05/08 14:28 Enumerating may be non-trivial, looking. 05/08 14:31 For instance, enumerating List Nat. 05/08 14:32 hrm 05/08 14:33 seems like you'd run into the same issue with the grammar form of the same question though 05/08 14:34 RoseTree nat would be even worse. 05/08 14:34 It may be possible. Just not easy. 05/08 14:34 yeah, you'd need something like your zigzag to do it right I think 05/08 14:35 Well, if you're committed to a stream, yes. 05/08 14:35 which is in fact why I started trying to port control.monad.omega in the first place 05/08 14:35 yeah 05/08 14:35 I guess with a tree it might be harder 05/08 14:35 Going with some type of tree would be more doable. 05/08 14:35 hmm 05/08 14:36 But you might need infinitely branching trees. 05/08 14:36 For a naive solution, at least. 05/08 14:36 And I suppose one could question whether that constitutes an enumeration. 05/08 14:36 isn't the point of omega to traverse infinitely-branching trees? 05/08 14:37 Yeah. But doing it is extra work. 05/08 14:37 fair enough 05/08 14:37 okay, morris' thesis has a nice definition of inductive families too 05/08 21:00 it's fun to examine all these universes and what extra power they give you 05/08 21:00 another way to look at it is, since these work in coq and agda and whatever - that justifies implementing just these data types /directly/ i.e. as axioms in your type theory 05/08 21:02 but also they have practical use for generic programming/proofs 05/08 21:02 what would be the benefit of defining them directly? 05/08 21:02 say you started with a dependent lambda calculus - how will you add inductive data types to it? 05/08 21:03 I think there is two ways - (A) add a schema that accepts/rejects data type definitions or (B) add a grammar of data types built in and just allow people to name them 05/08 21:04 this stuff is fairly complicated 05/08 22:35 a telescope (at least in these presentations) just looks like a list 05/08 22:39 or a heterogeneous list, I guess 05/08 22:40 heterogeneous by a function, if that makes sense 05/08 22:40 so i have a proof "x : a ≡ b" where a and b are two different constructors for a datatype. what's the shortest path from here to ⊥? 05/08 22:41 must i go prove a bunch of lemmas stating that each pair of constructors are unequal? 05/08 22:42 Match on x. 05/08 22:42 did 05/08 22:42 It should be absurd. 05/08 22:42 won't it take an abusrd pattern? 05/08 22:42 if they're constructors it should see it 05/08 22:42 ah, excellent! 05/08 22:43 i was just forgetting how to use absurd patterns 05/08 22:43 i was expecting it to let me omit the cases entirely, and i got stuck when it insisted that i include them 05/08 22:43 copumpkin: The telescopes in that paper have increasing indices. 05/08 22:43 Which allows later elements to refer to earlier ones. 05/08 22:44 codolio: hmm, ignoring the typo in here, http://snapplr.com/afdq 05/08 22:45 here's the full page, http://snapplr.com/c7x3 05/08 22:46 Oh, these aren't the telescopes from the context free types.\ 05/08 22:47 oh, nope, 05/08 22:47 i 05/08 22:47 I've moved on to fancier stuff 05/08 22:47 but in general, telescopes appear to be listlike, but maintain some additional information in the index 05/08 22:47 Well, in this case, each type appears to get a vector of its preceding types. 05/08 22:48 oh I see. I was looking for T-> to appear in the SPF, but the I-> is enough to give it all the preceding stuff 05/08 22:49 Looks that way. 05/08 22:49 interesting 05/08 22:50 hm 05/08 22:50 I haven't quite absorbed this universe yet :P 05/08 22:50 the earlier ones are pretty straightforward 05/08 22:50 danbrown: what are you proving? 05/08 22:53 I'm not sure what O and O' are. 05/08 22:54 danbrown: to go from a ≡ b to F using 'first principles' you could define a function f a = T and f b = F, and then coerce a proof of true into a proof of false 05/08 22:54 danbrown (this is what justifies whatever pattern matching does ) 05/08 22:54 soupdragon: ok, yeah 05/08 22:59 it's interesting to see this because f : C -> * 05/08 22:59 it's a large elimination 05/08 22:59 the pattern matching conceals that 05/08 22:59 * = Set? 05/08 23:00 yes 05/08 23:00 infact without large elimination you cannot do this 05/08 23:00 large meaning it jumps up a level? 05/08 23:00 copumpkin: encoding a small-step semantics for a calculus i'm working on 05/08 23:01 turns out that reduction semantics aren't exactly easy in PHOAS... 05/08 23:01 the denotational semantics should be much, much easier 05/08 23:01 * copumpkin has got to reread this section 05/08 23:06 Reduction in PHOAS is a pain. 05/08 23:09 I have an example of it, though. 05/08 23:09 Oh right, it fails the positivity checker. 05/08 23:10 Never mind. 05/08 23:10 yeah I never figured out how to make PHOAS work for something like system F 05/08 23:11 (other than the way in the paper, which I don't like) 05/08 23:11 You need impredicativity to encode impredicative terms, I think. 05/08 23:11 The thing about reduction in PHOAS, especially if you're doing dependently typed stuff, is that you need to combine a lot of different functions together. 05/08 23:15 Which, one nice thing about PHOAS is that you can write lots of things simply (free variables, alpha equality ...), but they all use different bound variable types. 05/08 23:16 So you need a bound variable type that combines everything to do type checking and normalization of dependent types. 05/08 23:17 Which starts to lose some of the "this implementation is obviously correct" properties. 05/08 23:18 dolio: i used your PHOASNorm module to figure out my reduction function :) 05/08 23:18 in Adam Chlipala's papers and book i could only find a relational encoding of reductions, but i wanted a function 05/08 23:19 your PHOASNorm.norm had the right insight: map a Term (Term v) t to a Term v t 05/08 23:20 dolio: and if you do a small-step function instead of a big-step evaluator then you can get it past the termination checker. from there you can iterate the step function into a Colist 05/08 23:21 iterating the step function is slightly tricky, though ;) 05/08 23:22 anything that looks like haskell Num typeclass for agda? (i.e. I write * and get the appropriate multiplication for my parameters?) 05/08 23:27 benc___: the appropriate structure in Algebra 05/08 23:28 benc___: but it won't behave like a typeclass 05/08 23:28 danbrown: nice 05/08 23:29 --- Day changed Fri Aug 06 2010 (Unsolved metas? In *my* Agda buffer?!?!) 06/08 00:50 omg hax 06/08 00:50 I'm really enjoying this thesis 06/08 00:51 (http://www.cs.nott.ac.uk/~pwm/thesis.pdf) 06/08 00:51 Yeah, that's a good one. 06/08 00:54 is there a discussion of parametricity in light of all this "alternate universe" generic programing work? 06/08 02:28 no 06/08 02:28 You should be able to apply the techniques to prove parameticity but I wasn't able to do it myself 06/08 02:29 oh actually that's because the theory doesn't (didn't) have eta of proof irr. 06/08 02:29 There's work on parametricity for dependent type theories. 06/08 02:55 You wouldn't get very interesting theorems for inductively defined universes in a normal language, though. 06/08 02:56 If you had some way of limiting the operations you could perform on certain arguments, though (like an erasure type system), you'd probably get something more interesting. 06/08 02:58 btw, i wonder how much cayenne is able to erase 06/08 03:22 Types, probably. 06/08 03:27 Not sure beyond that. 06/08 03:27 I suppose it may be smarter than just that, though. 06/08 03:30 wait do you mean how much it can erase in theory? 06/08 03:31 or how much it actually does erase 06/08 03:31 I seem to recall some of jhc's equivalent of dictionary elimination and stuff is based on a general sort unused variable/code detection. 06/08 03:31 I mean theres a lot less it's permitted to erase by General Recursion 06/08 03:31 Sure. 06/08 03:32 i guess a value that appears only in types can be erased too? i guess i should read about the stratification mentioned here http://byorgey.wordpress.com/2010/08/05/typed-type-level-programming-in-haskell-part-iv-collapsing-types-and-kinds/#comment-6452 06/08 03:59 also, what's an easy way to make the typechecker loop with --type-in-type?:) 06/08 04:00 That's the idea behind erasure pure type systems. 06/08 04:00 At first you can erase types and type application, but then that leaves behind additional things that are just constant parameters. 06/08 04:01 Or, whatever you want to call them. Parameters that aren't used at all in the computation. 06/08 04:01 So you can erase those, too. 06/08 04:02 And then I guess the idea is that you can keep track of what all you can erase that way by having two different pi types, lambda abstractions, and applications. 06/08 04:06 Such that programs are only well-typed if it's okay to erase all the things you've marked erasable. 06/08 04:06 And then you can do analysis to turn a normal language into such an annotated language, if you want. 06/08 04:07 i don't see why that conflicts with Set : Set though 06/08 04:07 It doesn't. 06/08 04:08 That doesn't cover all types of erasure, though. 06/08 04:08 yeah, but cayenne can't exploit those given by strong normalization anyway 06/08 04:09 Erasure of proofs, due to irrelevance, despite their making meaningful contributions to the algorithm for instance. 06/08 04:09 But yeah, you can't erase those unless you have strong normalization. 06/08 04:10 anyone has a translation of this in agda or a good reference for the notation used? http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.1953 06/08 11:02 fulfilled my own request: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28629#a28629 06/08 13:26 oh very nice 06/08 13:26 that should be on the wiki somewhere :) 06/08 13:26 except I don't think it has enough unicode in it 06/08 13:28 ;) 06/08 13:28 heh, the paper is not very unicodey either 06/08 13:30 just kidding :P 06/08 13:30 it doesn't seem like we'd be able to conjure a similar construction in haskell's type system even after (* :: *) 06/08 13:32 Saizan: What was the aim? Prove false given Set : Set? 06/08 15:05 what do you guys think of containers? 06/08 17:27 too hardcore for me I have NFI what is going on there 06/08 17:29 the simple ones seem fairly straightforward 06/08 17:44 (with one type) 06/08 17:44 okay, they do get kind of hairy 06/08 17:52 :P 06/08 17:52 okay, I get how to encode families without using them 06/08 18:44 weird, agsy will fill in more than one hole at a time if one hole depends on another 06/08 19:41 if it didn't do that it would probably produce terms that don't typecheck 06/08 19:42 it does that sometimes anyway :P 06/08 19:43 * copumpkin just devised the most useless datastructure ever 06/08 20:21 * copumpkin deletes it 06/08 20:24 Most useless ever? 06/08 20:27 it was an arbitrary-length sigma 06/08 20:27 I called it SigmaVec 06/08 20:27 Well, I don't think that's useless, except it'd probably be a pain to use. 06/08 20:28 yeah, it was 06/08 20:28 lots of yellow unless you provided lots of implicits 06/08 20:28 Nested sigmas having a nice notation is good, though. 06/08 20:28 Like { x : A, y : P x, z : Q x y | R x y z } 06/08 20:29 that would be nice 06/08 20:29 even having a binary version of that would be nice 06/08 20:30 * copumpkin moves to coq 06/08 20:30 Or even \Sig (x : A) (y : P x) (z : Q x y). R x y z 06/08 20:30 Or \ex for a logic flavor. 06/08 20:31 Multiple notations depending on how you want to think about it. 06/08 20:32 ther was a nice trick with containers proving something about vectors 06/08 21:33 http://cs.nott.ac.uk/~rcp/flops08.pdf 06/08 21:34 amusing that they represent the naturals as IN with very little space between them :) 06/08 21:36 Good ol' tex glyph drawing. 06/08 21:39 well \bb{n} doesn't do that 06/08 21:40 or \mathbb{N} I guess 06/08 21:40 They actually use \mathbb{N} elsewhere in the paper, it looks like. 06/08 21:40 hah, yeah 06/08 21:40 That's kind of important if you want to have a type of naturals and a (semantic) set of naturals, I guess. 06/08 21:41 Or something of that sort. 06/08 21:41 *frustrated* 06/08 21:59 how come? 06/08 21:59 i have "x : π₁ p ≡ ⊥" in my environment, but i get a type error "π₁ p != ⊥" 06/08 22:00 what gives? 06/08 22:00 did you math on the proof? 06/08 22:00 match 06/08 22:00 or rewrite by it 06/08 22:00 (which is the same thing) 06/08 22:00 yes—oh crap, should i have matched against the 'refl' constructor? 06/08 22:01 i only named it 'x' 06/08 22:01 yeah 06/08 22:01 :/ 06/08 22:01 of course 06/08 22:01 hrm 06/08 22:01 or just rewrite (whatever gave you pi1 p = _|_) = refl 06/08 22:01 cause if you match on it manually you may need to refine some other parameters 06/08 22:02 when i try to match against refl, the match itself fails with the type error 06/08 22:02 hmm 06/08 22:02 i'll try the rewrite 06/08 22:02 nope, same error 06/08 22:03 with the rewrite 06/08 22:04 maybe i need more pattern matching... 06/08 22:04 yeah, i bet that will do it 06/08 22:04 you could also use subst manually if necessary 06/08 22:05 dolio: in particular the aim was to construct a non-normalizing type term in a way that could be redone in haskell, given Set : Set 06/08 22:06 Ah. 06/08 22:07 ok, more patterns did the trick 06/08 22:09 *frazzled* 06/08 22:10 dolio: since in that case we'd show that typechecking haskell + (* :: *) would be undecidable 06/08 22:10 Oh, right. 06/08 22:11 It rather depends how much evaluation you can get to go on during type checking. 06/08 22:15 actually, proper patterns eliminated some other cruft too. i need to learn to rely on them more 06/08 22:15 They're lifting up all the value-level stuff, as I recall. 06/08 22:15 only the constructors, but yes 06/08 22:16 copumpkin: http://www.e-pig.org/darcs/Pig09/models/Records.agda <- wrt n-ary sigmas 06/08 22:16 If it's only constructors then I'm not sure. 06/08 22:16 You'd need some sort of computation. 06/08 22:17 But that may be restricted to the point that you can't write the terms required to prove false. 06/08 22:18 yeah, type families are pretty weak, but i'd like to try :) 06/08 22:18 Saizan: ah, that's not as ugly as mine :) 06/08 22:28 woah, absurd patterns ftw! 06/08 22:28 :) 06/08 22:28 yeah! 06/08 22:28 http://snapplr.com/068k do they mean "insist that the domain of 'arr'" instead of codomain? 06/08 23:46 i'd think so 06/08 23:51 so that would mean the domain would be Usp 0 and codomain would be Usp n? 06/08 23:51 seems like you could simulate it with Usp n -> Usp (suc n) -> Usp (suc n), but the interpretation would be weird 06/08 23:52 i haven't read the paper, the argument to Usp is the number of free variables? 06/08 23:53 yeah 06/08 23:53 so 'arr' : Usp 0 -> Usp n -> Usp n would fit, i don't think Usp n -> Usp (suc n) -> Usp (suc n) is restrictive enough 06/08 23:55 oh, it isn't 06/08 23:55 I'm thinking that vars defined on the domain would have to be treated specially 06/08 23:56 so that the max of the fin is excluded and everything else is mapped 06/08 23:57 not sure if I'm making any sense :P 06/08 23:57 * Saizan doesn't follow, but feels like he's lacking quite a bit of background 06/08 23:58 nah, I'm probably just being dumb 06/08 23:58 I guess I'm also assuming that the type only has one free variable, which isn't always true 06/08 23:58 okay, I'll go for Usp 0 :P 06/08 23:58 --- Day changed Sat Aug 07 2010 (I'm trying to avoid using the host language's types) 07/08 00:00 as the last comment says, with Usp 0 you'll probably have to struggle with the termination checker 07/08 00:02 (or the positivity checker?) 07/08 00:03 positivity 07/08 00:04 but I'm not really planning on writing an element type 07/08 00:04 not in agda, anyway 07/08 00:04 (you only get negative occurrences in the element type) 07/08 00:04 oh, ok 07/08 00:06 writing a compiler? 07/08 00:06 well, I wouldn't say that 07/08 00:06 playing with various interpreters :) 07/08 00:07 :) 07/08 00:07 I guess for the dependent version of that, I can do Usp 0 -> Usp (suc n) -> Usp n 07/08 00:11 actually, hm 07/08 00:12 yeah, that's what i'd guess too 07/08 00:13 though maybe it's more complicated than that 07/08 00:13 since the variable introduced there is not necessarily a type 07/08 00:14 (assuming the Usp contains all the "value-level" stuf too) 07/08 00:14 since it would just be "Term", containing all the usual value-level stuff and type-level stuff 07/08 00:14 I'd probably want to parametrize it by the universe, too 07/08 00:14 does that work? 07/08 00:15 * copumpkin throws the datatype together to see if it looks right :P 07/08 00:16 mh, maybe you've to keep the vars for mu distinct from the ones for pi.. 07/08 00:16 yeah, I was planning to 07/08 00:17 or how did you mean? 07/08 00:17 if i were doing a shallow embedding i'd probably write "pi : (s : Usp 0) -> (Elem s -> Usp n) -> Usp n" 07/08 00:18 but then it's shallow :P 07/08 00:19 yeah, you'd have to represent "Elem s -> Usp n" with a lambda term of your object language instead, i guess 07/08 00:20 s/with a/with the type of a/ 07/08 00:20 hm, I have something, but it leads me to a problem 07/08 00:23 hmm! 07/08 00:23 this would obviously need a separate typechecking phase, http://snapplr.com/vq4s 07/08 00:25 sorry if it's completely ridiculous :P 07/08 00:25 mh, you can't write the type of id there :) 07/08 00:28 ugh, now I can't stick universes in :P 07/08 00:29 I guess I sort of could 07/08 00:30 oh, I see what you mean 07/08 00:32 hmm 07/08 00:32 Saizan: http://snapplr.com/r081 :P 07/08 00:34 then I also run into the issue of not being able to define heterogeneous-universe sums (or products, going through 2#) 07/08 00:35 so many problems with my term type :P 07/08 00:35 heh :) 07/08 00:36 * copumpkin sighs 07/08 00:36 I need to think about this harder :P 07/08 00:41 any good papers out there on implementing dependent types elegantly? :P 07/08 00:41 (ideally in another DT language) 07/08 00:41 There was something not too long ago about writing compilers in a logical framework or something. 07/08 00:58 all paradoxes seem to live in papers with painful notations 07/08 01:39 which one are you after now? 07/08 01:40 haha ttrue 07/08 01:40 girard's one 07/08 01:41 tried a paper by coquand and one by hurkens (which might not be the exact same paradox though) 07/08 01:41 Does the Coquand paper work for you? 07/08 01:47 Most of the math is all mashed together for me. 07/08 01:47 If it's the one I'm thinking of. 07/08 01:47 tried looking at the coq scripts? 07/08 01:48 "An Analisys of Girard's Paradox" and yeah it has some problems with spacing, still somewhat readable though 07/08 01:49 uh, no, do you have a link for them? 07/08 01:50 http://www.lix.polytechnique.fr/coq/stdlib/Coq.Logic.Hurkens.html <- found 07/08 01:51 There's a Hurkens.agda, too. 07/08 01:54 http://www.cse.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Hurkens.agda <- nice 07/08 01:56 should be easier to see what's going on in the paper now :) 07/08 01:57 It's easier to read than the stuff in Hurkens' paper, too, because Agda isn't anal about whether or not certain abbreviations are first-class in the language. 07/08 01:57 something i don't grasp is how they say girard's paradox shows the logic is inconsistent without showing a non-normalizing proof term 07/08 02:01 Not sure about that. That term definitely isn't normalizing. 07/08 02:02 Maybe the point is that you have normalizing proofs of both D and Not D. 07/08 02:08 Which, when combined, gives a non-normalizing proof of bottom, but you can see that it is inconsistent before that. 07/08 02:08 For instance, if you use something like U A = U A -> A, it's easiest to just construct a looping term directly, and use it to prove bottom. 07/08 02:13 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28687#a28687 agda build error on windows 07/08 20:27 builds fine on ubuntu linux :~( 07/08 20:34 --- Day changed Sun Aug 08 2010 what is the K axiom in type theory? is it related to the K combinator? 08/08 00:10 it's almost impossible to search for 08/08 00:10 I would like to say no but I couldn't be certain.. 08/08 00:12 oh, an eliminator 08/08 00:12 I think J means the normal equality eliminator and K is the one that implies UIT 08/08 00:12 UIP 08/08 00:12 seems to be introduced here: http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf 08/08 00:13 gotta love scanned pages 08/08 00:13 http://www.cs.nott.ac.uk/~ctm/goguen.pdf is interesting 08/08 00:27 K : (A : Set) (x : A) (P : x == x -> Set) (eq : x == x) -> P refl -> P eq 08/08 00:54 sort of substitutive proof irrelevance? 08/08 00:56 Well, that's essentially an induction axiom for equality proofs. 08/08 00:56 Induction on naturals is "all naturals are either 0 or suc n". K is "all proofs of x == x are refl". 08/08 00:57 oh, fair enough 08/08 00:57 That's not the induction you usually get for equality, though. 08/08 00:58 And it's called K because the usual eliminator is J for some reason. 08/08 01:00 ah :) 08/08 01:00 I guess because identity types are I in Martin-Loef type theory. 08/08 01:00 I J K 08/08 01:00 = -1 08/08 01:01 lol 08/08 01:01 type-level quaternion 08/08 01:01 anyone done that yet? 08/08 01:01 --- Day changed Mon Aug 09 2010 dolio: as you mentioned several days ago... .Arrays.absurd x != .Arrays.absurd x of type ⊥ :( 09/08 15:14 looks like the 5 second termination check in agsy doesn't always work :P it's been running for a couple of minutes and allocated a gig of memory so far 09/08 15:59 that'll teach me to be lazy and have it fill in obvious terms for me 09/08 16:00 man, I'm having a lot of trouble on the most trivial of proofs 09/08 17:20 http://snapplr.com/33nc, now trying to prove that toNat on the result of that is always 0 :P 09/08 17:21 kind of sad 09/08 17:22 argument order can be a real pain in agda 09/08 19:36 copumpkin: Yep. Apparently \() isn't first-class. So it's better to make a single false-elim and use it. 09/08 19:57 Although, that requires one for each empty type, then. 09/08 19:57 yeah :/ 09/08 19:57 seems like something that could be fixed in agda itself 09/08 19:57 unless that leads to other issues? 09/08 19:57 No idea. 09/08 19:58 I worked around it by passing around the one I was using 09/08 19:58 Where-defined functions are kind of a tough situation in general, and \() is essentially one of those. 09/08 19:58 For instance, if you want to prove something about foo, which defines bar in a where clause, you might think that you can define bar in a where clause for your proof, and use it, since it will have the same definition as the other bar. 09/08 20:01 But that doesn't work. 09/08 20:01 annoying :/ 09/08 20:14 Extensionality might come in handy for the \() case. With it, you can prove (f g : _|_ -> A) -> f = g. 09/08 20:16 --- Day changed Tue Aug 10 2010 hi all, do you reckon this is a bug or not: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28794#a28796  ? thanks.  i think the goals should be as clean as in the second example for the first and third example as well. 10/08 16:06 * Saizan agrees 10/08 16:09 heh, C-c C-c' generated invalid code for me :) 10/08 21:45 (it saw fit to remove an argument {foo}' when matching on foo', rather than replace it with {()}'. then it immediately flagged an error) 10/08 21:46 yeah, it does that a lot :P 10/08 21:48 I think there's an open bug for it 10/08 21:48 hm, when i have bar : Blah -> ?; bar ... = ?', and refine the body ?' to an expression of type \bn', it doesn't seem to automatically refine the signature ?' to \bn' for me .. 10/08 21:50 is this intended behaviour ? 10/08 21:50 i know Agda1 (using Alfa) would refine the type for me, when i refined things that determined (parts of) the type 10/08 21:51 (in some cases, there can be several possible type expressions which in the local context are equal, but which outside the context behaves differently .. that might be related to a rationale for the current behaviour) 10/08 21:52 different types can have the same constructor names, so i guess that's why the signature goal can't be determined. 10/08 21:54 yeah, but that would only apply when the body type was ambiguous, no ? 10/08 21:55 yeah, i guess 10/08 21:57 .. hm, would naming a variable n_\==_Succ_m' be horrible abuse of mixfix notation ? 10/08 22:04 There are other situations outside of signature vs. definition that it could do such refinement, but it doesn't. 10/08 22:08 Like foo : (A : Set) (x : A) ... 10/08 22:08 yeah, that reminds me .. if i have 10/08 22:09 If you write 'foo ? ? ...' and fill in the second hole with an expression of unambiguous type, it won't automatically fill in the first hole. 10/08 22:09 You'll have to do it manually, even if just with _ 10/08 22:09 foo {A : Set} {n : \bn} {v : Vector A n} -> ... 10/08 22:09 then if i write foo {v}' i want that to mean foo {_} {_} {v}', not foo {v} {_} {_}' 10/08 22:10 foo {v = v} 10/08 22:10 i.e. it would be much nicer if it filled in implicit arguments from the "right", since that would have a much higher chance of determining any previous arguments 10/08 22:11 * ski is not sure whether he likes that .. 10/08 22:12 Would foo {x} {y} be foo {_} {x} {y}? 10/08 22:15 yeah .. 10/08 22:20 though there might be problems with stuff like foo : {A : Set} {n : \bn} {v : Vector A n} -> Foo A n v' .. Foo A n v' might expand to more implicit function arrows 10/08 22:21 (like how e.g. foldr' in Haskell sometimes can take more than three arguments) 10/08 22:21 Yeah, that's an issue. 10/08 22:23 --- Day changed Wed Aug 11 2010 hm .. would it be sensible if C-c C-c' introduced a with' if you've given an expression larger than a variable ? 11/08 02:55 I'd love that, but is it possible in general? 11/08 02:55 .. that's why i'm asking :) 11/08 02:57 Some sort of command for with-introduction would interest me. 11/08 02:57 I'm not even sure it doesn't exist, though. :) 11/08 02:58 hm, strange .. 11/08 08:40 ? 11/08 08:41 i have basically (simplifying) 11/08 08:42 data Foo (n : \bn) : Set 11/08 08:42 where 11/08 08:42 Foo0 : Foo n 11/08 08:42 ... 11/08 08:42 now, i expect that 11/08 08:42 Foo0 : {n : \bn} -> Foo n 11/08 08:43 and if i write Foo0' in an expression, sure, i can write Foo0 {n}' instead 11/08 08:43 ah, yeah, parameters don't appear in patterns 11/08 08:43 however, when i try to write Foo0 {n}' in a pattern, i get a complaint that the Foo0' constructor expects 0 arguments 11/08 08:43 it just seems a bit inconsistent to me 11/08 08:44 (maybe there's some real reason, but i don't know it) 11/08 08:44 it helps keeping them cleaner though, if you have other implicits 11/08 08:44 i was just expecting them to behave the same way in patterns as in expressions 11/08 08:45 .. for a short while i was thinking that rather than Foo0 : {n : \bn} -> Foo n' i got something more like (n : \bn) -> (Foo0 : Foo n)' (i.e. somehow i can't provide an implicit argument explicitly at all, i.e n' really is not an actual argument to Foo0', it instead being polymorphic) 11/08 08:47 i wonder if it's just a matter of convenience, or it's something more fundamental about pattern matching 11/08 08:49 Panic: Right hand side must be a single hole when making case. 11/08 09:51 Panic: unbound variable n 11/08 09:56 when checking that the expression n has type \bn 11/08 09:56 ski: I reported the single hole one recently, but haven't seen the other one 11/08 13:10 (copumpkin : you saw ?) 11/08 13:33 yep, although I'm still half asleep so haven't really looked that closely :) 11/08 13:33 in the unbound variable case i goofed by renaming the variable in one place, but not the other .. but i was still surprised to get a panic 11/08 13:33 (possibly it was something like foo .(Succ y) (Bar y) = ...' and i renamed the latter, but not the former y' to n') 11/08 13:34 ah 11/08 13:35 ski: copumpkin , regarding that quantifier elimination stuff: http://web.student.chalmers.se/~stevan/csallp/html/README.html 11/08 15:34 ooh 11/08 15:35 nice 11/08 15:40 i got stuck trying to prove that the quantifier elimination preserves the semantics tho (failed attempt in the CoqVersion module)... :-/. I tried to explain the problem and draw some conclusions in the CoqVersion module, but I'm not very confident about them being correct. If somebody has any comments on that I'd be happy to hear them. 11/08 15:44 * ski doesn't know that much about quantification elimination (yet, anyway) .. 11/08 16:11 .. bah, i want to write 11/08 16:11 Succ .mn \frob Succ .mn | \iotal (\==Refl {\bn} {mn}) = ? 11/08 16:12 but since i apparently can't name the type parameter arguments for the constructor in patterns, i must break the symmetry and either write 11/08 16:13 Succ .mn \frob Succ mn | \iotal \==Refl = ? 11/08 16:13 or 11/08 16:13 Succ mn \frob Succ .mn | \iotal \==Refl = ? 11/08 16:13 :( 11/08 16:13 * ski wonders why passing \ \==Refl -> ?' to \iotar : (Succ m \== Succ n) -> \bot' doesn't bring the equality of m' and n' into scope inside ?' .. 11/08 16:28 no patterns in lambdas 11/08 16:29 hm .. it didn't complain .. but i suppose it happily shadowed the identifier, then 11/08 16:31 i think so 11/08 16:31 * ski works around by passing irrefl m n m\==nn' (defined in a where') to \iotar' instead 11/08 16:32 (since i don't think i could use with' in this situation) 11/08 16:32 "no patterns" was too strong btw, you can have absurd ones 11/08 16:34 ah, ty 11/08 16:35 hm, so \ ()' ? 11/08 16:44 yep 11/08 16:45 (with no arrow) 11/08 16:45 hm .. parse error 11/08 16:46 Panic: no such interaction point: ?4 11/08 18:29 you filled in a hole but didn't reload? or something like that 11/08 18:31 I've had that when tinkering with holes behind its back 11/08 18:31 what is "Cannot split on the constructor foo"? 11/08 18:43 i'm trying to define a function by pattern matching that specializes the type indexes of its input 11/08 18:44 and the constructor 'foo' computes one of its indexes, unlike the rest of the constructors which just specify constants 11/08 18:45 here's a boiled-down example: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833 11/08 19:11 oops. updated: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a28834 11/08 19:13 copumpkin : yeah, i think so 11/08 20:05 (just sharing the assorted panics i encounter ;) 11/08 20:05 check the bugtracker, too 11/08 20:05 btw, it's irritating when you want to comment out holes, or delete them, or copy them 11/08 20:06 i usually end up having to C-c C-x C-d', fiddle some, C-c C-x C-l' 11/08 20:07 danbrown : well, it appears to me it doesn't like creating a cyclic unification a = o a' .. i'm not sure what to do about it, though 11/08 20:15 ski: cyclic unification isn't the problem... http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a28849 11/08 22:54 it appears i'm confusing the type checker by asking it to reason about the image of a function 11/08 22:55 Yes. The problem with 'X a a' is that 'a' is essentially fixed, and not a variable open to refinement. 11/08 22:59 Pattern matching is not allowed to refine some particular value 'v' into 'f u', where 'v' is the image of 'u' under 'f'. 11/08 23:00 dolio: so are you saying that pattern matching basically doesn't work on datatypes with computed indices? 11/08 23:45 assuming i stick with computed indices, do i need to use eliminators instead of patterns, or is there another technique? 11/08 23:46 I thought it did, if you brought those computed indices into scope with a with block 11/08 23:47 and used the appropriate dotting 11/08 23:47 --- Day changed Thu Aug 12 2010 hrm, or maybe i would still need pattern matching to define the eliminator... 12/08 00:08 can I see? 12/08 00:09 oh, it's that example you gave earlier? 12/08 00:10 copumpkin: ya 12/08 00:15 danbrown: what did you intend to write in that function? 12/08 00:23 just out of curiosity :) 12/08 00:24 that function in particular?—nothing :P 12/08 00:24 this was a contorted example distilled out of something else i'm working on 12/08 00:24 which is a bit too large for an irc hpaste ;) 12/08 00:25 i'm trying to model Filinski's reify and reflect semantics for monads, and i want a way to "match" a type against the image of a type constructor 12/08 00:25 for example, i want a constructor like "reflect : ∀ {t : Type} {e : Effect} → Fun (T e t ⟶  t / e)", where T : Effect → Type → Type 12/08 00:28 but when i add that and try to define a function on "Fun (s ⟶ t)" by pattern matching, it gives me the problem above if i specialize 's', e.g. "Fun (⊤ ⟶ t)" 12/08 00:29 ah :/ 12/08 00:31 It works on datatypes with computed indices, just not the way that you're doing it. 12/08 00:39 If all you know is that 'x : Foo y', where y is eligible for refinement, you can match on x, and refine y to 'f z' or something. 12/08 00:41 But if you know that 'x : Foo true', you cannot match on x and refine true to 'not false'. 12/08 00:41 And, you cannot refine some ys and not others, I think. And when you match on 'x : X a a', you're trying to get 'op a o : X a (o . a)', which is refining the right 'a' and not the left 'a'. It doesn't work that way. 12/08 00:45 Or, inserting another variable, it's trying to refine a to both 'b' and 'o . b', and that doesn't work. 12/08 00:46 Attempting to make that work would appear to require solving for o in 'b = o . b', which does not strike me as a reasonable demand for an arbitrary function _._. 12/08 00:48 ok 12/08 00:51 Note that your f function works fine, because it refines 'b' into 'o . a'. 12/08 00:51 so it sounds like i should redesign my "Fun (⊤ ⟶ t) → X" function to a "Fun (s ⟶ t) → X" function that projects away the unwanted inputs 12/08 00:52 right 12/08 00:52 and then i'll have room to refine 's' 12/08 00:52 for reference, here's a workaround using what i think is the proper eliminator: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a28858 12/08 01:00 data X : Bool → Bool → Set where 12/08 01:01 eh : ∀ a b → X a b 12/08 01:01 eq : ∀ a   → X a a 12/08 01:01 op : ∀ a o → X a (o ∙ a) 12/08 01:01 this type is necessary ? 12/08 01:02 soupdragon: no :P 12/08 01:02 contrived example 12/08 01:03 what's the real case? 12/08 01:03 rather larger. i'm working on a model of effects with Filinski's reify and reflect operators that move between an explicit monadic computation Tτ and its implicit representation as an effectful term τ / e 12/08 01:07 so i want term constructors like "reflect : Fun (Tτ → τ / e)" and "reify : (τ / e → Tτ)" (where the monad T and the effect e are related) 12/08 01:11 the functor action "Tτ" i represent as a function like "_•_ : Mon → Type → Type" 12/08 01:12 the trouble arises when i try to define a function by pattern matching that specializes one of the types in Fun, like "Val? : Fun (⊤ → τ)" 12/08 01:14 solved my problem (earlier) by abstracting over equality 12/08 02:59 sprinkles some refls about, but it at least lets me get on with things 12/08 03:00 using the stdlib, if I want to use \top in Set1, am I forced to write a variant of \top in Set1 instead of Set, or I missed something? In particular, is there a reason for it not to be --set-poly? 12/08 15:01 I think you are forced to write one yourself, unless you want to use Lift from Level 12/08 15:03 is there any reason for not defining "record ⊤ {a} : Set a where ..."? 12/08 15:08 I might see one, namely that this definition is not as first-order as the previous or the manually lifted one. This might lead to complications in practice, in particular wrt. to unification and co.(?) 12/08 15:13 making it polymorphic would probably just give you more yellow in places it wasn't yellow before 12/08 15:16 but I don't think it'll actually break anything? 12/08 15:16 * copumpkin is no expert though 12/08 15:16 I think we mean the same thing: this definition would be less unification-friendly, hence causing a yellow terror. I'm not an expert either, that's why I naively asked :-) 12/08 15:19 all right, now I need Nat in Set1. It is time for --set-in-set. :-) 12/08 15:22 maybe you could be more universe polymorphic in your code? 12/08 15:23 but Nat and \top are not defined as universe polymorphic in the stdlib, isn't it? I just pulled the latest version, it's "data Nat : Set where ..." for instance 12/08 15:28 i meant that maybe the place where you're passing top or Nat might be made more permissive in the universe levels it accepts 12/08 15:32 though that probably leads to a lot of Level paramaters 12/08 15:32 ha, I see your point. That won't work in this particular case: I'm waiting for a Set1 or above, I cannot afford a Set there in any case. But thanks for the hint. 12/08 15:37 ah, fair enough :) 12/08 15:39 --- Day changed Fri Aug 13 2010 pedagand: Your email client mangled the unicode in ILabel.agda ))): 13/08 11:08 I think I found a bug in Agda. The test case is really short. Can anyone confirm that this should type check http://pastebin.com/KL3yfBV3 13/08 15:04 what is E' ? 13/08 15:15 A copy of E 13/08 15:17 sorry I minimized the example afterwards 13/08 15:17 weird, here (A : E true) → A is the only one that won't typecheck 13/08 15:21 i'm using the darcs version though 13/08 15:21 same here 13/08 15:21 anyhow, that seems to support the idea that the commented ones should in fact work 13/08 15:22 Yep but in a more complex example it does make a difference 13/08 15:22 And if it is a bug it ought to be fixed 13/08 15:22 ah, so your problem is that "(A : E true) → A" doesn't typecheck? the comment in the paste seems to say the opposite to me 13/08 15:24 ... sorry 13/08 15:26 http://pastebin.com/pPaAnLpc <= updated version 13/08 15:28 anyhow, i feel like it should work, but expanding the same definition you're typechecking feels dangerous in general so i don't know.. 13/08 15:29 Saizan: this seems to be related to whether or not the term can be reduced 13/08 15:30 yeah, it won't reduce "E true" while typechecking E 13/08 15:30 which kind of makes sense, since it hasn't yet decided if it'd terminate, i presume 13/08 15:32 Yep but using only the type of it should work no? 13/08 15:34 E true is of type Set₁ and so A is of type Set 13/08 15:35 no, consider data B : Set1 where ... 13/08 15:43 and "E true = B" 13/08 15:43 Saizan: yes while saying it I understood the issue 13/08 16:10 --- Day changed Sun Aug 15 2010 shouldn't we introduce sigfpe to Agda? his posts should get clearer, to those who know it at least :) 15/08 09:28 given that he seems to always work with the semiring of types maybe epigram would be more appropriate, actually 15/08 09:29 Saizan, don't act as if epigram existed, that just makes reality unnecessarily painful :-) 15/08 10:34 pedagand: heh, "if it existed" was implicit :) 15/08 11:02 :-) 15/08 11:06 http://blog.sigfpe.com/2010/08/constraining-types-with-regular.html <- Hom is quite similar to desc :) 15/08 11:09 it's a grammar for functors on Set, isn't it? (hopefully, I'll read the post more carefully later) 15/08 11:13 yeah 15/08 11:13 though they are interpreted as matrices :) 15/08 11:15 *baffled* 15/08 19:48 anyone have any idea what might be going on here? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a29085 15/08 19:48 in particular, in the "Have" it appears to be flipping the order of the two arguments to _﹔_ 15/08 19:48 I've had a similar error 15/08 19:49 as a result of unifying b with itself 15/08 19:49 I submitted a report and nobody has a clue, it seems 15/08 19:49 :/ 15/08 19:49 it's just printing the context/goal wrong, I think 15/08 19:49 not sure how something like that could happen 15/08 19:49 but it's not just printing—it won't typecheck 15/08 19:50 oh 15/08 19:50 maybe it's the same in my exampel too... the goal type in mine was so convoluted and wrong I gave up and thought I'd wait for them to fix it 15/08 19:50 ah 15/08 19:50 very frustrating 15/08 19:51 and i can't figure out which knob to twiddle to set it straight 15/08 19:52 definitely submit a bug report if you can trim it down to something manageable 15/08 19:52 I'm sure having another example from my ugly one will help them 15/08 19:52 yeah... 15/08 19:52 ugh 15/08 19:53 the more i code the harder it is to trim down these bug examples 15/08 19:53 yeah, mine was pretty large too 15/08 19:53 copumpkin: which issue #? 15/08 19:55 http://code.google.com/p/agda/issues/detail?id=290 15/08 19:55 isolated: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a29091 15/08 20:36 it seems only a prettyprinting bug, since it behaves as i'd expect 15/08 20:51 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a29093 15/08 20:52 but why do f and g fail to typecheck? 15/08 20:57 err, ok, f _should_ fail 15/08 20:57 but g should pass 15/08 20:58 f is bogus 15/08 20:58 your g you mean? 15/08 21:09 yeah 15/08 21:09 btw, thanks for the workaround 15/08 21:09 i don't understand why matching on "with b ≟ b | F ∙ G" is necessary 15/08 21:10 (would have never thought to try it) 15/08 21:10 because the definition of ﹔ does the same pattern matching 15/08 21:12 so it's not clear what it reduces to until you do the same 15/08 21:12 another way is to perform case analisys on b, so that b ≟ b itself can reduce 15/08 21:13 this is what the "| .b ≟ .b" in the goal says 15/08 21:14 that it's unresolved? 15/08 21:14 "x | y" in a goal in general means that you've to make y rewrite to a normal form before x can reduce further 15/08 21:16 ok, that makes sense 15/08 21:17 err, not normal form, but it has to have a constructor at least, it depends on how strict x is in the end 15/08 21:17 ok 15/08 21:17 but why is matching on "F ∙ G" necessary? 15/08 21:17 because the  b ≟ b appears in the type of "F ∙ G", and it wouldn't get rewritten if we didn't do that 15/08 21:18 you mean the type of "F ∙ G" only gets rewritten because we match on "F ∙ G" along with "b ≟ b"? 15/08 21:20 yeah 15/08 21:20 ok, this is helpful. thanks 15/08 21:21 now i'm unstuck again :) 15/08 21:21 np :) 15/08 21:21 (reported: http://code.google.com/p/agda/issues/detail?id=295) 15/08 21:25 --- Day changed Mon Aug 16 2010 seems like flip in agda (or any dependently typed language) can't be as generic as we might like it to be 16/08 02:53 flip : (a -> b -> c) -> (b -> a -> c) 16/08 02:54 ? 16/08 02:54 well, the full dependent function version 16/08 02:54 ((x : A) -> (y : B) -> C x y) -> (y : B) -> (x : A) -> C x y 16/08 02:54 dolio: yeah, but what if (y : B x)? 16/08 02:54 then yyou can't flip it 16/08 02:55 seems restrictive :P not that I have an application 16/08 02:55 why is that restrictive 16/08 02:55 what about ((x:A)(y:B x)C x y) -> ((y:(x:A), B x)(x:A)C x y) 16/08 02:55 it'd need a proof that they're equal, too, wouldn't it? 16/08 02:57 anyway, utterly pointless 16/08 03:03 just seemed like a curious asymmetry with non-dependent functions 16/08 03:03 It seems straight-forward to me that if you're considering flipping the arguments, the second cannot depend on the first. 16/08 03:03 In a sense, the second determines the first. 16/08 03:04 sure, but normally you consider (a -> b -> c) <=> ((a, b) -> c), and (a, b) <=> (b, a) 16/08 03:04 (in non-dependent land) 16/08 03:04 but yeah, I definitely see why it can't work here 16/08 03:04 * copumpkin shrugs 16/08 03:06 You can't swap pairs, either. 16/08 03:06 yeah, I know 16/08 03:06 Of course. 16/08 03:06 flip = 16/08 03:07 fun (A : Type) (B : A -> Type) (C : forall x : A, B x -> Type) 16/08 03:07 (X : forall (x : A) (y : B x), C x y) (y' : forall x : A, B x) 16/08 03:07 (x : A) => X x (y' x) 16/08 03:07 : forall (A : Type) (B : A -> Type) (C : forall x : A, B x -> Type), 16/08 03:07 (forall (x : A) (y : B x), C x y) -> 16/08 03:07 forall (y' : forall x : A, B x) (x : A), C x (y' x) 16/08 03:07 --- Day changed Wed Aug 18 2010 I guess there's no way to simulate substructural types with dependent types 18/08 00:30 Not that I know of. 18/08 01:00 Nor modal types, really. 18/08 01:01 Barring writing a DSL. 18/08 01:01 Or, EL, maybe. I'm not sure those qualify as "domain specific". 18/08 01:04 http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html yow! 18/08 08:12 cool 18/08 08:49 does ++ mean cons or append? 18/08 19:05 append, usually 18/08 19:07 depends where though :) 18/08 19:07 ok. i was searching the agda wiki for this information but I couldnt find it, do you know where these things are documented? 18/08 19:08 well, nothing is built in, but there's the agda standard library, where documentation means reading the source code at http://www.cs.nott.ac.uk/~nad/listings/lib/Everything.html#254 :P 18/08 19:09 ok cool, Data.List has it 18/08 19:10 yeah, Data.Vec does too 18/08 19:15 is there a nice way to find which standard library file somethign is defined in? 18/08 21:59 eg if I have a source file open and its showing | x |  is there somethign i can press when I'm sitting on a | to tell me thats defined in Data.Integer 18/08 22:00 IIRC assuming the code typechecks and loads middle clicking should take you to the definition. There's probably a keyboard equivalent but I can't remember it. 18/08 22:09 if only i had more than one mouse button 18/08 22:09 http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.EmacsModeKeyCombinations <- M-.Go to the definition of the identifier under point 18/08 22:10 meta dot 18/08 22:12 ok 18/08 22:12 cool 18/08 22:12 --- Day changed Thu Aug 19 2010 Boy, induction for sum types using free theorems is proving much harder than other stuff. 19/08 01:42 what does that look like? 19/08 01:44 Which? 19/08 01:49 induction for sum types using free theorems? what do you mean by that 19/08 01:50 http://code.haskell.org/~dolio/agda-share/ParamInduction.agda 19/08 01:50 http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html 19/08 01:51 The latter only has it for empty, unit and product. 19/08 01:51 I've been looking at bool, sum and sigma, but I can't figure them out. 19/08 01:51 Of course, I don't actually know that the free theorem is enough. 19/08 01:56 Maybe you need the general parametricity result. 19/08 01:56 Or maybe it's just impossible. 19/08 01:56 yikes indeed 19/08 02:06 Bwahahaha! I've done it! 19/08 03:53 Full parametricity for the win. 19/08 03:54 :O 19/08 03:54 Induction for booleans proved. 19/08 04:09 dolio: is the Nat induction particularly hard? 19/08 05:17 I haven't seriously tried it yet. 19/08 05:20 I thought about a while back, but then decided it'd be better to figure out booleans before naturals. 19/08 05:20 ah ok 19/08 05:21 Now I'm trying binary sums. 19/08 05:21 Which I think requires using existentials, like booleans require sums. 19/08 05:22 this is kind of interesting 19/08 05:22 I'm not sure I'll be able to make the existentials into strong sums, though. 19/08 05:22 what got you started on it? 19/08 05:22 I saw Neel Krishnaswami mention that it was possible a while back, so it's been on my to-do list. 19/08 05:23 cool 19/08 05:27 The idea goes something like... 19/08 05:30 System F is cool, because you can encode inductive types in it. 19/08 05:31 But, CoC is less cool, because the inductive types you can encode don't have strong induction principles. 19/08 05:32 is CIC cool? :) 19/08 05:33 However, if you add parametricity axioms to CoC, you can prove the strong induction principles. 19/08 05:33 CIC isn't a pure lambda calculus. 19/08 05:34 The aim is to get everything that CIC provides out of an impredicative lambda calculus. 19/08 05:35 More or less. 19/08 05:35 Of course, that's arguably because CIC is cool, since it has strong induction principles, which are nice. 19/08 05:37 Sums proved. 19/08 06:33 is there a way get the (in Tex notation) "\not\ni" symbol with the unicode input? 19/08 15:36 ha, got it! it's "\nin" 19/08 15:37 ah, I was going to ask what \ni was 19/08 15:37 * copumpkin never used that one before :) 19/08 15:39 it's the mirror image of "\in" 19/08 15:39 yeah 19/08 15:39 anyone know how one might approach proving something is undecidable? 19/08 23:30 I guess it would depend on the something :) 19/08 23:31 i think you either have to do it in the meta-logic or by reducing it to something else that's known to be undecidable 19/08 23:43 but i'm mostly guessing 19/08 23:43 --- Day changed Fri Aug 20 2010 anyone get an error compiling the latest agda? 20/08 02:44 "The last statement in a 'do' construct must be an expression" in src/full/Agda/Auto/Convert.hs 20/08 02:45 hmm, I guess it was just me 20/08 03:04 seems to be working now :o 20/08 03:04 I'm generally impressed that pulling at random gets you something that compiles and works. 20/08 03:04 yeah, same 20/08 03:04 not sure how this file got messed up 20/08 03:04 (on my side) 20/08 03:05 maybe my hard drive is dying 20/08 03:05 Incidentally, I now have sigma with both projections. I figured out what my problem was. 20/08 03:05 ooh, same url? 20/08 03:05 Yes. 20/08 03:05 When I was defining pi0 with curry, I forgot that the postulates would prevent pi0 (x, w) from computing to x. 20/08 03:06 So when you go to define pi1, you have a proof obligation. 20/08 03:06 So I switched to the easy pi0. 20/08 03:06 That means that pi1 doesn't compute properly, either, but proving that pi1 (x, w) = w is a huge pain. 20/08 03:07 oh, I see now 20/08 03:12 hmm, no, I still get the same issue, weird 20/08 03:14 http://snapplr.com/3k90 20/08 03:14 oh that must be when generating documentation 20/08 03:17 I wonder how I managed to break my agda without doing anything 20/08 19:22 It broke without even a darcs pull? 20/08 19:23 oh, that error is just a haddock one cause they have a comment that accidentally looks like haddock 20/08 19:23 but more seriously, agda just doesn't work anymore, and it's a haskell error 20/08 19:23 something about package dependencies no longer being satisfied, let me look 20/08 19:24 http://snapplr.com/hbrx , any ideas? 20/08 19:25 maybe I should just ask in #haskell actually 20/08 19:25 copumpkin: what if you start ghci with -package-id Agda-2.2.7- ? 20/08 19:36 same error 20/08 19:36 ghc-pkg check? 20/08 19:37 no output, I assume that's good? 20/08 19:37 yeah 20/08 19:38 seems like it has something to do with random? 20/08 19:38 all of them eventually boil down to package random-1.0.0.2-f4208c3677aeaaaf41e4d36309c0b4ff is shadowed by package random-1.0.0.2-3f4f79037f4383d8a3872916cdac8d3f 20/08 19:39 I have random-1.0.0.2 in both user and system folders 20/08 19:40 starting ghci with "-package-id Agda-2.2.7-378254d26ce5307092318870fe9b05db" should direct the shadowing to pick the other random 20/08 19:40 maybe that's it? I've never explicitly installed random though 20/08 19:40 but i guess you could also try -package-id random-1.0.0.2-3f4f79037f4383d8a3872916cdac8d3f 20/08 19:41 (if you only have one random-1.0.0.2 shadowing won't be needed, of course) 20/08 19:41 oh I think I see what's wrong 20/08 19:42 f4208c3677aeaaaf41e4d36309c0b4ff is the version of random that haskell98 wants 20/08 19:42 but pandoc wants the other hash for random 20/08 19:42 not sure why pandoc is even relevant for agda though 20/08 19:43 it complains about hakyll, strangely enough 20/08 19:43 http://pastie.org/private/xbkegoyoph4ncfvmyi0p9q 20/08 19:43 I'll just kill my user random and hakyll 20/08 19:43 no, wait 20/08 19:44 whoops :) 20/08 19:44 anyway, it still doesn't work 20/08 19:44 you used -package instead of -package-id 20/08 19:44 for Agda. 20/08 19:45 ugh 20/08 19:45 works now :P 20/08 19:45 but agda-mode is using -package 20/08 19:45 you could put -package-id ... in the .ghci file i guess, or remove the unwanted random.. 20/08 19:47 the unwanted random is gone, but now it just says agda is unusable, and -v gives no information 20/08 19:48 are you sure you removed the right one?:) 20/08 19:49 anyhow, if ghc-pkg check is silent there should be a way to make it work. 20/08 19:50 oh, maybe I should recompile agda now that I only have one random again 20/08 19:51 maybe it got messed up since I tried to build it with the other random there 20/08 19:51 I did delete the right one :P 20/08 19:51 what the hell :P rebuilding agda reinstalls another user random 20/08 19:52 gah 20/08 19:53 it's rebuilding haskell98 and all sorts of stuff I already have installed with the platform at the system level 20/08 19:53 did you upgrade "time"? 20/08 19:54 or "old-locale"? 20/08 19:54 those are the non-base transitive deps of random. 20/08 19:54 I've never explicitly upgraded anything 20/08 19:54 maybe some package you installed required a newer version. 20/08 19:55 but I do seem to have new time in the user  folder 20/08 19:55 ok, so that's why you also get an user random :) 20/08 19:55 with the difference that there's no new version of random, so you get the same version but built against the new time 20/08 19:56 ah 20/08 19:56 looks like it might be doing the right thing now 20/08 19:57 btw, in later ghcs shadowing prefers user packages, which would have make -package Agda-2.2.7 just work in this case 20/08 19:58 yay, it works 20/08 20:04 thanks for all the help :) 20/08 20:07 np 20/08 20:12 I vaguely remember a NBE module by pigworker in agda 20/08 23:12 anyone know where that is? 20/08 23:12 oh, nice: http://web.student.chalmers.se/~stevan/ctfp/html/README.html 20/08 23:17 one thing I never really understood about the agda standard library and the category theory modules in there is that sometimes people seem to make Raw which contains the operations but no laws 20/08 23:24 what's the point of that? 20/08 23:24 well sort of the same point of the Monad class in haskell i guess.. also some laws might require extensionality for some monads 20/08 23:29 why not just postulate extensionality where needed and avoid duplicating definitions? 20/08 23:31 well what do you mean the same point as the Monad class? 20/08 23:31 that you can write e.g. mapM that's polymorphic over the RawMonad, it doesn't use the laws 20/08 23:32 maybe there are other design problems on how to add the laws too? e.g. setoids or not 20/08 23:41 we should ask the authors :) 20/08 23:41 --- Day changed Sat Aug 21 2010 copumpkin: Also, I think there are parallel hierarchies. 21/08 00:47 ? 21/08 00:48 RawFoo contains the minimal operations for a Foo. 21/08 00:48 IsFoo is a proof that those minimal operations follow the right laws to be a Foo. 21/08 00:48 ah yeah 21/08 00:48 And IsFoo contains IsBar, for all the relevant substructures. 21/08 00:48 Then, a Foo is a pair of the minimal operations, and the proof that the operations satisfy the laws. 21/08 00:49 Or, perhaps the record itself doesn't contain it, but the module for IsFoo does. 21/08 00:49 If I remember correctly. 21/08 00:49 Conceivably, you could use the IsFoo records independently. 21/08 00:51 Have a function that accepts a bunch of arguments, and an IsFoo argument for those arguments combined into a structure. 21/08 00:52 Although, I don't know why you'd do that. 21/08 00:52 what issues would I encounter if I postulated extensional equality? 21/08 20:13 any proofs that need to compute on a proof which uses it wont reduce .. 21/08 20:23 sometimes that doesn't even matter, but it can be a problem 21/08 20:23 it seems like for refl it would be less of a problem 21/08 20:23 but maybe I'm oversimplifying thing 21/08 20:24 s 21/08 20:24 oh I guess computing _on_ proofs 21/08 20:26 that's what you said, I just misunderstood 21/08 20:26 how about "passing it in" to functions that use it? seems like you could push the need for extensionality out each time 21/08 20:27 it's the same as a hypothetical proof 21/08 20:51 copumpkin: you'll still run into that problem - when you try to run the functions, they'll do a conversion that depends on the equality proof.  That conversion will get stuck because the equality proof doesn't reduce to refl. 21/08 21:37 but if you're just writing proofs and don't need to compute with them, it's no big deal 21/08 21:37 yeah but the thing is, 21/08 21:39 you write 30 pages of proofs and it all works fine 21/08 21:39 but then you want to use your theory to justify the termination of a function..... 21/08 21:39 basically you get lucky, or don't. at that stadge 21/08 21:40 copumpkin: Same problem as I ran into with pi0 and pi1 for the sigmas defined with Church encoding and parametricity. 21/08 22:07 Instead of pi0 (x, w) computing to x, I would have had to prove that it was equal to x, and use substitution. 21/08 22:09 ****ing universe polymorphism 21/08 23:14 homomorphism : ∀ {X Y Z : Set o} → (f : X → Y) → (g : Y → Z) → (x : Maybe X) → _ ≡ _ 21/08 23:17 feels kind of dirty, somehow 21/08 23:17 --- Day changed Sun Aug 22 2010 copumpkin: That signature isn't yellow? 22/08 01:00 nope :D 22/08 01:03 I don't believe you. 22/08 01:04 :( 22/08 01:05 (it's in a where block) 22/08 01:05 http://snapplr.com/2g4q 22/08 01:06 Is _==_ not the usual _==_? 22/08 01:06 it is the usual one :) 22/08 01:07 Oh. I guess it must figure out what the _s are from the type from the record. 22/08 01:07 That's fairly impressive. 22/08 01:07 I figured it was doing it because of how I was using it 22/08 01:08 isn't that related to the miller unification pigworker was talking about? 22/08 01:08 * copumpkin knows nothing 22/08 01:08 but then again, he was talking about it being unimplemented in agda 22/08 01:08 I don't really know anything about Miller unification. 22/08 01:08 And I recall not being able to find any obvious, short papers on it. I think it has to do with Lambda Prolog. 22/08 01:09 but yeah, as far as I can tell, my usage of homomorphism there is the only thing specifying the _ == _ and preventing it from being yellow 22/08 01:09 if I remove the call to it, it turns yellow 22/08 01:10 Oh, maybe there are short papers on it. 22/08 01:10 Unification of Simply Typed Lambda-Terms as Logic Programming is probably related. 22/08 01:14 Of course, Agda isn't simply typed. 22/08 01:16 I'm kind of enjoying this category theory package 22/08 01:24 pity there's no adjunction stuff in it 22/08 01:45 is there a good way to pull out refl' from http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.html#4538 ? 22/08 02:59 You should be able to use IsPreorder.reflexive, I think. 22/08 03:03 Which is probably exported from IsDecTotalOrder, too. 22/08 03:03 ah yes 22/08 03:10 copumpkin: :-), we ran out of time. you are most welcome to add adjunctions (or anything else for that matter). just let me know if you'd like to be added to the patch-tag project. 22/08 21:17 stevan: still getting a feeling for the library, but I'll definitely let you know if I add anything I consider worthy of eyes that aren't mine :P thanks! 22/08 21:18 (but it's unlikely :)) 22/08 21:18 --- Day changed Mon Aug 23 2010 Is Agda 'better' at the Expression Problem than Haskell ? 23/08 17:17 hm, I sort of doubt it 23/08 17:20 you can sort of simulate typeclasses and tackle it that way 23/08 17:20 it seems like the types à la carte approach might be more elegant on the type side but less elegant on the value side 23/08 17:21 (since you don't have typeclasses and would have to pass the dictionaries around by hand) 23/08 17:21 does Agda provide any simple way to do something like the Show class from Haskell ? 23/08 17:22 not really, unless you make a "typeclass-tagged value type" or something 23/08 17:24 then you'd have to wrap everything in a boring constructor 23/08 17:24 yeah.. 23/08 17:24 sometimes I like type classes, but other times I don't.. 23/08 17:24 like, in happstack we have a, ToMessage a, class which can turn types into HTTP responses. Which is pretty useful. But then you get into situation where the same type might have multiple valid conversions to an HTTP response, and you are forced to only pick one 23/08 17:25 they are a very nice fit for the sort of problems they were meant to solve, to be like that they traded away quite a bit of flexibility though 23/08 17:25 Saizan: yeah, like the issue I just described I expect.. 23/08 17:26 right 23/08 17:26 stepcut: in haskell you'd use newtypes 23/08 17:26 but it's ugly 23/08 17:26 or a two parameter typeclass 23/08 17:26 you can simulate some of the features of type classes in agda via parameterized(?) modules though  ? 23/08 17:27 copumpkin, Saizan: right, I have considered both those options for Happstack 23/08 17:27 I saw something about Agda now having support for IO a few months ago, is that right ? 23/08 17:28 parameterized modules help in dealing with the dictionaries manually, since they let you abstract in a larger scope and also open them 23/08 17:28 It's got an FFI to Haskell, so it can in theory support anything Haskell supports. 23/08 17:28 is there a ready-to-use network socket library ? 23/08 17:31 maybe the web framework linked on the mailing list has something 23/08 17:31 Saizan: that just seemed to provide a few http types 23/08 17:32 this is the IO library I was thinking of, btw, http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/ 23/08 17:35 http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOConsoleLib.html 23/08 17:35 http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleConsole.html 23/08 17:37 I am wondering if it was really required to define new types like ConsoleCommands? Or is he trying to do something special? 23/08 17:37 Haven't seen that. 23/08 17:37 I imagine one of the goals is to be more specific about exactly what effects are used in a particular computation. 23/08 17:38 i suspect he's defining the primitives as constructors which then get interpreted because he wants to inspect the IO action 23/08 17:38 ok 23/08 17:39 I have yet to actually run an agda program.. so far, once it type checks, I'm done :) 23/08 17:39 i've run an hello world once :) 23/08 17:40 it actually took me a while to realize that I had run an agda program, and didn't even know how :) 23/08 17:40 does agda have an concurrency support ? 23/08 18:41 can I just import forkIO ? 23/08 18:42 it can FFI out to haskell 23/08 18:42 cool 23/08 18:42 I will have to give this a shot 23/08 18:42 it's definitely worth playing with :) not sure whether I'd want to write many "real programs" in it, though 23/08 18:43 I'm working on my new book, "Real World Agda" 23/08 18:43 copumpkin: you mentioned a CT lib lately, do you have a link? 23/08 18:59 http://web.student.chalmers.se/~stevan/ctfp/html/README.html :) 23/08 19:00 thanks :) 23/08 19:02 * Saizan darcs gets 23/08 19:03 "Unfortunately, Agda takes too much memory for me to 23/08 19:05 continue working on this." 23/08 19:05 (from a comment in the monoidal categories module :P) 23/08 19:06 sounds fairly common 23/08 19:06 that's why i've ordered a stick of memristors 23/08 19:07 more people in here than in #coq.  Never seen that before 23/08 20:43 but how does it compare to #epigram ? 23/08 20:56 that's only at 12 :) 23/08 21:05 people are scared of epigram because of the +v power structure in there! 23/08 21:05 heh 23/08 21:06 show more respect! 23/08 21:06 i am scared of epigram because I believe that they are drastically overhauling the language and I don't want to invest myself in the learning the old way... 23/08 21:06 but maybe I am wrong :p 23/08 21:07 (we should ask shapr, or anyone with enough power, to remove the autovoice) 23/08 21:07 it's been quite incremental up to now, but i have that kind of feeling, about the internals too :) 23/08 21:08 though perhaps I was thinking of the jump (?) between epigram 1 and epigram 2 23/08 21:10 ah, i've never looked at epigram 1 23/08 21:10 --- Day changed Tue Aug 24 2010 copumpkin: how do you manage huge records in error messages when using ctfp?:) 24/08 08:08 Saizan: ah, i remember that problem. it happened in some goals too. we didn't have the time to try it, but perhaps making some things abstract would help? that could also help speed up typechecking. if one needs the record to normalise for some proof or so, one could perhaps have a concrete version of the abstract record and a function between the two?  apa = record [...]   abstract apa' = apa    bepa : apa <-> apa'  ?  ... 24/08 09:31 ... i dunno if that works tho. 24/08 09:31 stevan: in this case we'd need to make functor composition abstract, it seems like that'd break a lot of things though 24/08 09:33 * Saizan is trying to make the laws for adjuctions work 24/08 09:34 i'm tempted to go the NaturalIsomorphism route, but i'd have to build the product and Set categories for that and i'm feeling lazy 24/08 09:35 oh, found them! 24/08 09:36 pushed a patch where i made the proofs inside functor composition abstract, they are never used so it didn't break anything, i'm not sure if it helps tho. 24/08 10:15 (i don't remember exactly where those huge records occured) 24/08 10:19 the problem with the adjunction laws seem to be that functor composition is not obviously a monoidal operation. 24/08 10:54 the sad part is that only the proofs prevent this. 24/08 10:57 is it non-obviously a monoidal operation? 24/08 11:42 morally yes, i think even intesionally, but i've not written the explicit proof yet 24/08 11:48 extensionality seems to be required 24/08 13:24 care to paste some code? :-)   also, did the huge record problem go away with the abstract proofs? 24/08 13:41 it's less huge :) 24/08 14:02 anyhow, take one of the commented laws "comm₁ : (ε ∙ʳ F) ∘ (F ∙ˡ η) ≅ id {F = F}" 24/08 14:03 the problem is that (F ∙ˡ η : F ∘F idF {C = C} ⇒ F ∘F (U ∘F F)) and (ε ∙ʳ F : (F ∘F U) ∘F F ⇒ idF {C = D} ∘F F) so the types don't match. 24/08 14:04 postulating (or abstracting over) FunctorExtensionality we can cast them to the right types though. 24/08 14:05 using the code in Category.Functors.FunctorProperties 24/08 14:06 i thought that hetro eq would get around the problem that the types don't match, how come it doesn't? 24/08 14:12 you can't compose those two natural transformations 24/08 14:13 hmm 24/08 14:14 F ∘F (U ∘F F) /= (F ∘F U) ∘F F 24/08 14:14 i can't see how to use FunctorExt to solve this... 24/08 14:50 i haven't tried, but i assumed that with FunctorProperties.\o-assoc you could cast one of the two NT to a type compatible with the other, since you can prove F ∘F (U ∘F F) == (F ∘F U) ∘F F by instatiating it 24/08 14:52 we had some casts like that in our implementation 24/08 14:59 http://gitorious.org/cats/setoidcats/blobs/master/Monad.agda 24/08 15:00 cool, thanks 24/08 15:18 did some benchmarks with and without abstract proofs in functor, nattrans composition and identity;  without abstract: ~ 4m 15s    and with: ~ 3m 25s 24/08 15:58 that is the total time to typecheck the whole thing. 24/08 16:00 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29421#a29421 <- scary 24/08 16:50 Saizan: have you seen how other modules in that package deal with needing extensionality? you could just do the same 24/08 16:52 copumpkin: for example? 24/08 16:54 they just have an Extensionality u type 24/08 16:54 it's in one of the modules 24/08 16:54 http://web.student.chalmers.se/~stevan/ctfp/html/Category.Categories.Sets.html#232 for example in here 24/08 16:55 http://snapplr.com/yx8j 24/08 16:55 almost all their properties abstract over it 24/08 16:55 I guess it isn't even from this package, it's just in the standard library 24/08 16:56 it feels a bit cleaner because it's more honest about the assumptions, but it'll never get instantiated so it'll behave as a postulate wrt reduction anyhow 24/08 17:00 yeah, sure 24/08 17:00 lol, gotta love universe polymorphism: -> Set (suc (o₁ ⊔ o₂ ⊔ o₃ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) 24/08 17:03 heh :) 24/08 17:04 perhaps categories.product could be rewritten such that all those implicit arguments need not be passed explicitly... hmm... 24/08 17:10 maybe by defining first and second separately, rather than composing (_,_)C and Cp\_n on the spot 24/08 17:29 parametrising the module on the two product categories might help 24/08 17:31 _⊣_ : ∀ {o₁ ℓ₁}{C D : Category {o₁}{ℓ₁}} (F : Functor C D) (G : Functor D C) -> Set (suc (o₁ ⊔ suc ℓ₁)) 24/08 17:39 _⊣_ {C = C} {D = D} F G = NaturalIsomorphism (hom D ∘F first {C = D} (op F)) (hom C ∘F second {C = opposite C} G) 24/08 17:39 much better already :) 24/08 17:39 nice :-) 24/08 17:48 first \o op and second are the F\_1 of some functors btw 24/08 17:55 i added you to the patch tag project, feel free to push those and other changes 24/08 17:56 same goes for you, copumpkin 24/08 17:59 is there an explicit policy on when something should be an argument vs. a field ? 24/08 18:00 not that i know of, whatever works best i guess 24/08 18:02 oh, thanks :) 24/08 18:17 --- Day changed Wed Aug 25 2010 -!- Irssi: #agda: Total of 31 nicks [0 ops, 0 halfops, 0 voices, 31 normal] 25/08 14:25 anone have a pointer to a good intro to induction-recursion? pigworker just tweeted about it, and a name like that seems impossible to google without getting loads of results about the two not as a single term (even with quotes) 25/08 15:54 I don't know of good intros 25/08 16:01 peter dybjer wrote most of the literature about it, you can see his papers 25/08 16:02 copumpkin, http://www.citeulike.org/user/pedagand/tag/induction-recursion 25/08 16:02 but lots of them are pretty heavy on the set theory 25/08 16:02 whenever you write down a mutual block of agda definitions and you use one in the type of the other, you are using induction recursion 25/08 16:02 *(I think) 25/08 16:02 ah, I've done that before 25/08 16:02 pedagand: any of those more accessible than the others? :) 25/08 16:03 a bit of advice: Dybjer is known for being an excellent writer. 25/08 16:03 but he's first (or only) author on all of them!! 25/08 16:03 :P 25/08 16:03 all right, then I'm risking my life for you by saying: Setzer is not such an excellent writer *hint* *hint* 25/08 16:04 lol 25/08 16:05 I promise not to tell anyone 25/08 16:05 (but be aware there are 32 people in here who are neither you nor me) 25/08 16:05 (thanks!) 25/08 16:05 copumpkin: I use induction-recursion a lot when I am thinking about universes.  I want to define some recursive function [[_]] which interprets the elements of some set of codes 25/08 16:05 ccasin: ah yeah, I played with it in a similar way then, without knowing what it was 25/08 16:06 but it also needs to take an environment as an argument, and that environment contains the interpretations of other codes, so it must refer to [[_]] 25/08 16:06 do things like telescopes fall under it? 25/08 16:06 so I define them mutually - the environment is an inductive definition.  It mentions [[_]] and it is an argument in the type of [[_]] 25/08 16:06 Induction-recursion is when you have 'U : Set' and 'T : U -> Set' and you use T in the constructors of U. 25/08 16:08 Agda's mutual blocks allow other things. 25/08 16:08 aha 25/08 16:08 You can actually get more general than those signatures, too. 25/08 16:09 'U : -> Set' 'T : ( : ) ( : ) -> U -> S ' 25/08 16:10 Or something like that. 25/08 16:10 There are also some restrictions on how you can use T in U and vice versa that Agda doesn't really enforce. 25/08 16:11 restrictions why? 25/08 16:11 For instance 'c2 : T c1 -> ... -> U' isn't allowed, for c1 some other constructor of U. 25/08 16:11 just because IR is defined that way? 25/08 16:11 Rather, you should only use T over parameters to the constructor. 25/08 16:12 dolio: interesting.  In fact, I have used that "feature" and wondered about it.  Is it known to lead to problems? 25/08 16:12 And "T ... = U" is also wrong. 25/08 16:12 ccasin: Last I checked, it doesn't work very well. I'm not sure if it's disallowed for a theoretical reason other than that the formal definition of induction-recursion given by Dybjer (and Setzer) doesn't cover it. 25/08 16:13 (on an unrelated note, I asked here the other day, but does anyone remember where to find pigworker's (I think it was his) NBE code that was posted a couple of months ago?) 25/08 16:14 "T ... = U" is wrong from the perspective of what the definition is supposed to mean. 25/08 16:14 it "worked" for me.  though of course I never actually ran the program 25/08 16:14 In that you're defining U simultaneously with T, where T is at each point well-defined for the elements of U you've constructed so far. 25/08 16:14 However, U as a whole is not. 25/08 16:15 So referencing U in the definition of T doesn't make sense from that perspective. 25/08 16:15 And, of course, in the categorical semantics, you're trying to find functors whose initial algebras are inductive-recursive types, but a functor for "T ... = U" would be one that refers to its own initial algebra, which doesn't make much sense. 25/08 16:17 I think 'c2 : T c1 ...' is similar. 25/08 16:17 ccasin: As for it not working, I think I tried making a universe with something like "set : T level -> U" and then "T level = Nat ; T (set n) = ..." and got errors about T level not being Nat or something. 25/08 16:21 interesting 25/08 16:23 dependent types are fun! 25/08 16:24 Lots of universes with "T ... = U" are disallowed due to the positivity checker. But that's kind of an ad-hoc rejection instead of one motivated by the theoretical basis. 25/08 16:24 copumpkin: http://personal.cis.strath.ac.uk/~conor/fooling/Nobby.agda <- ? 25/08 16:24 Kind of how the productivity checker doesn't correspond to coinduction. 25/08 16:24 nobby! thanks 25/08 16:25 well, the theoretical basis is "we only have proofs for the positives ones", right? 25/08 16:25 (found by grepping foo out of desperation :) 25/08 16:25 been trying to remember what quirky name he'd chosen for it :) 25/08 16:25 *positive 25/08 16:25 Aside from all this, definitions like 'data U : Set ... ; data T : U -> Set ...' are not induction-recursion, either. 25/08 16:26 no, but how about f : (a : A) -> g a -> ... ; g : A -> Set; g a = ... f ...? 25/08 16:28 that is, where neither is actually an inductive definition 25/08 16:28 just two mutually recursive functions 25/08 16:28 ccasin: If you allow types that fail the positivity checker, you can prove false. I guess you can call that theoretically motivated. :) 25/08 16:28 :) 25/08 16:28 I think you can desugar mutual recursion to a single recursive definition with an extra parameter. 25/08 16:29 dolio: but here g is used in f's type 25/08 16:30 Similarly, mutually inductive types that aren't indexed by each other can be turned into an inductive family. 25/08 16:30 Not sure about that. 25/08 16:30 Anyhow, if that were novel, it'd be recursion-recursion, not induction-recursion. :) 25/08 16:31 yes 25/08 16:32 still, my advisor called it induction recursion 25/08 16:32 also coq rejects it and agda doesn't 25/08 16:32 on this thin evidence, I am calling it induction-recursion :) 25/08 16:32 What error does Coq give? 25/08 16:32 a boring one: "undefined variable g" or similar 25/08 16:32 see, I was hoping to sneak induction recursion into coq by encoding the datatype as a large elimination 25/08 16:33 but the coq typechecker is smarter than me 25/08 16:33 Saizan: now for another question :) I vaguely remember someone "translating" (Dep)Nobby.agda to use the standard libraries and stuff 25/08 16:35 they used a datatype to encode IDesc in coq 25/08 16:35 but I have no recollection of who it was, and can't find any reference to it in the logs 25/08 16:35 it was stevan, iirc 25/08 16:35 Saizan: yes, I suppose I could encode it all as a relation, but I wanted to compute with my functions 25/08 16:36 copumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25776#a25776 25/08 16:36 Saizan: <3 25/08 16:36 :P 25/08 16:36 Just checking... does Agda from darcs need ghc >= 6.12 these days? 25/08 16:48 pigworker: I think 6.10.3 is sufficient... the .cabal file claims it needs base-4.1.* 25/08 16:48 weird... my buddy got "cabal: cannot configure Agda-2.2.7. It requires base ==4.2.*" 25/08 16:51 oh 25/08 16:52 http://snapplr.com/kmk0 25/08 16:52 There's a flag use-locale that decides between 4.2 and 4.1 25/08 16:52 Sadly, I'm not in a position to prod things directly. 25/08 16:54 seems that use-locale doesn't have a default though 25/08 16:55 We're trying to figure out how to set up lab machines for course in Edinburgh next year. 25/08 16:55 but I guess it defaults to true if your friend had trouble with base 4.2 requirements 25/08 16:55 pigworker: and it would be a pain to roll out 6.12 or the latest platform to all the lab machines? 25/08 16:55 copumpkin: it would require higher authority, but it could probably be made to happen, given time 25/08 16:56 ah 25/08 16:57 There should be a way to specify the flag when installing. 25/08 16:57 cabal install -flags="-use-locale" 25/08 17:00 --flags, that is. 25/08 17:00 dolio: worth a shot, thanks 25/08 17:02 * stepcut has similar problems, but due to having base 4.3 :-/ 25/08 17:14 I'll just still with agda 2.5 for now maybe 25/08 17:15 ah, the problem is that agda-pkg unconditionally depends on base-4.2.* so with use-locale to false you get inconsistent constraints base-4.1.* && base-4.2.* 25/08 17:16 i guess one'd expect dependencies of agda-pkg to not be taken in consideration when it has buildable: false, but Cabal is not so smart atm 25/08 17:18 These things seem so brittle and confusing. People who aren't active Haskellers often have a bad time trying Agda. 25/08 17:24 next up, the agda platform! 25/08 17:32 a one-click installer for hours of fun 25/08 17:32 i wonder how Agda ends up depending on ghc 25/08 17:42 har har, Agda should be part of HP... 25/08 17:43 anyhow, it seems that because of this you need ghc-6.12.x 25/08 17:43 I'll wait until the dust settles after AIM, then I'll try to negotiate relevant upgrades. 25/08 17:45 (tbc, you need ghc-6.12 even if you delete agda-pkg from the .cabal file) 25/08 17:46 pigworker: is there a long-term goal for agda? like, will it be migrating in the direction of epigram and OTT or will it be exploring other lands? 25/08 17:54 copumpkin: I can speculate, but it's not my call. I think observational equality is likely to arrive in Agda soon after we stabilise it in Epigram. 25/08 17:58 ah, I see 25/08 17:58 exciting times :D 25/08 17:58 The price is that inductive families have to be treated differently, behind the scenes, but everything which currently works should still work. 25/08 18:00 Data.Bool should contain bool : forall {a} (P : Bool -> Set a) -> P true -> P false -> (b : Bool) -> P b 25/08 22:25 or does that live elsewhere? 25/08 22:26 I'm not sure where else boolean induction would live. 25/08 22:27 who knows :) 25/08 22:27 copumpkin: yes, and P should be implicit, for higher-order use 25/08 23:28 yeah 25/08 23:29 * edwinb wonders if it'd be a good idea to get organised about the AIM 25/08 23:39 man, I wish I knew enough to be an AI :P 25/08 23:40 I have never Ied any As ;) 25/08 23:42 But I look forward to finding out stuff about it 25/08 23:42 this is probably something I should do in advance really 25/08 23:42 --- Day changed Thu Aug 26 2010 Maybe they'll finally pin down a lifting operation to go with universe polymorphism. 26/08 00:41 * copumpkin is trying to understand all the different bits of depnobby :) 26/08 00:50 I wonder what parts of agda take up so much memory 26/08 02:42 Saizan: did you push your adjunction in terms of natural isomorphism to the darcs repo? 26/08 02:49 I'm having trouble stating the pullback properties in agda 26/08 05:05 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29450#a29450 does that make any sense? 26/08 05:11 copumpkin: universal-unique is missing things. 26/08 05:25 The two projections from Q should factor into the universal morphism followed by the corresponding projection from P. 26/08 05:26 oh I see 26/08 05:27 And u should only equal the universal morphism if the q-projections factor in the same way. 26/08 05:27 Factor through u in the same way, that is. 26/08 05:27 so stuff like u . p2 == q2 26/08 05:27 p2 . u, I think. 26/08 05:28 yeah, sorry 26/08 05:29 I'm not sure I understand how your second point differs from your first 26/08 05:33 I've changed it to http://snapplr.com/01be now 26/08 05:36 but it's still missing something? 26/08 05:36 You need  p1 . universal q1 q2 commutes = q1 26/08 06:10 And the same for q2. 26/08 06:10 oh 26/08 06:11 Oops, just touched my eye after handling a habanero. 26/08 06:12 damn 26/08 06:12 This is not pleasant. 26/08 06:12 :( 26/08 06:12 lots of water? 26/08 06:12 dunno, I hear water doesn't help actually 26/08 06:12 Keeping my eye closed seems to be working. 26/08 06:12 ah 26/08 06:12 wow, is my code that bad that you'd prefer to blind yourself in painful ways rather than read it? :P 26/08 06:13 No. I was making nacho cheese and then it slipped my mind that I'd handled the peppers. 26/08 06:14 how's it going? 26/08 06:24 Fine. It wasn't that bad. 26/08 06:32 cool 26/08 06:33 Not that I'd recommend it. 26/08 06:34 Didn't think so 26/08 06:36 I just made pullbacks in agda's set category 26/08 06:41 yay 26/08 06:41 (I think :P) 26/08 06:42 Check to see if pullbacks over the terminal object are products. 26/08 06:54 ugh, someone I know from IRC tried to commit suicide and is now a vegetable (probably permanently) :/ 26/08 06:55 That's terrible. 26/08 06:56 that sucks. 26/08 06:58 dolio: use milk. 26/08 06:58 I'll try that next time I rub peppers in my face. 26/08 07:01 dolio: chiliheads learn that one quick. 26/08 07:07 I wasn't really eager to pour milk all over my head. 26/08 07:08 it could be worse, you could have used the bathroom 26/08 07:08 true 26/08 07:08 kinda hard to just get it in your eye when you're in pain. 26/08 07:08 copumpkin: i didn't push it because i'm not sure where i should put it, Category.Adjunction.Alt maybe.. with Hom and Binfunctor under .Functors 26/08 08:19 Saizan: ah, I see 26/08 17:04 hmm 26/08 17:06 pullback : ∀ {o} → Extensionality _ → ∀ {X Y Z : Set o} → ∀ (f : X → Z) (g : Y → Z) → (f∘proj₁≡g∘proj₂ : ∀ x → f (proj₁ x) ≡ g (proj₂ x)) → Pullback Sets f g 26/08 17:06 does that even make sense? 26/08 17:06 is it no longer possible to install agda from source into an alternative prefix (like /opt/agda2) ? 26/08 19:07 * Saizan is torn between avoiding extensionality and avoiding code duplication 26/08 20:37 Saizan: how so? 26/08 22:27 I'm trying to write a hello, agda program, but the type checking fails. This is what I have, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29488 26/08 22:49 I am using Agda and lib from head 26/08 22:50 I remember there being two IOs in agda 26/08 22:53 but I can't remember the difference 26/08 22:53 I don't think you'll find many people in here who actually run programs :P 26/08 22:53 copumpkin: yeah, I think I figured it out.. 26/08 22:57 sure has to compile a lot of files though to build that 26/08 22:57 ok, I pasted the working version 26/08 22:59 next step is to implement a simple loop which reads from stdin and writes to stdout until you enter 'quit' 26/08 23:01 wow 26/08 23:01 that is new and unexplored territory in this channel 26/08 23:01 !! 26/08 23:02 :) 26/08 23:02 (I'm kind of serious, though) 26/08 23:02 :) 26/08 23:02 I think larrytheliquid is the only person I know of who has actually written software that _runs_ 26/08 23:02 hehe 26/08 23:02 copumpkin: ProductCategory is a Product in Cat, which would let me reuse _*_ from Product, but Cat requires extensionality, while defining _*_ directly for ProductCategory doesn't 26/08 23:18 ah :/ 26/08 23:19 damn lack of extensionality :P 26/08 23:19 workin' on it... 26/08 23:19 do you think it's worthwhile for me to put my pullback into the repo? 26/08 23:19 pigworker: can't wait :) 26/08 23:19 pigworker: i wonder what'd happen if i rewrote all of this in cochon :) 26/08 23:20 maybe i'd get insane at some point.. 26/08 23:20 * copumpkin snorts 26/08 23:21 copumpkin: i still have to learn what a pullback is, an Agda version might help :) 26/08 23:21 well, I made it on my way to making a subobject classifier, but then it turned out I was missing half the laws of something I thought I understood, so I'm feeling a lot less confident about my code :P 26/08 23:22 I'll clean it up a bit and see what people think 26/08 23:23 there's a disclaimer to that effect in the README anyhow 26/08 23:23 "some definitions are probably wrong, we'll find out when someone uses them." 26/08 23:24 lol 26/08 23:24 A pullback is like the product of the inverse-image of some object in two other objects. 26/08 23:24 I think that's right. 26/08 23:24 Actually, it's a little more complicated than that, I guess. 26/08 23:24 that's less illuminating than "a monad is a monoid object in the category of endofunctors" 26/08 23:25 ;) 26/08 23:25 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29491#a29491, assuming I haven't missed even more stuff 26/08 23:25 I'm open to suggestions :) 26/08 23:26 You're still missing the fact that the projections from Q factor into the universal morphism and the projections from P. 26/08 23:27 * dolio has to go. 26/08 23:27 p₂ ∘ u ≡ q₂, I thought that was it? 26/08 23:29 (and the _1 counterpart) 26/08 23:29 * copumpkin stares at the diagram some more 26/08 23:29 Why not implement a universe of diagrams? 26/08 23:31 and a "diagram -> equations" compiler? 26/08 23:32 that sounds pretty neat :) 26/08 23:32 If you know what proposition a diagram means, you know you've done the proof you intended. 26/08 23:33 Saizan: that's why I said "universe" not "set" 26/08 23:34 with enough ascii art we'll have 2D type signatures too :) 26/08 23:37 Saizan: zippers in motion... 26/08 23:38 zippers? 26/08 23:38 The Epigram 1 pre-parser is based on zippers. Each time you get a ( or ! or ) or \n, you refocus which part of the tree the rest of the text contributes to. 26/08 23:40 Saizan: McLarty's book "Elementary Categories, Elementary Toposes" has the clearest presentation of pullbacks that I've seen 26/08 23:47 he tells a story using "generalized elements" (which are just arrows) that explains the formal definition of a pullback as, intuitively, the largest subobject of pairs that satisfy the equality given by the pullback corner X -f-> Z <-g- Y 26/08 23:50 it's worth a look 26/08 23:50 OT: grr @ "Record types are not allowed in mutual blocks" 26/08 23:51 --- Day changed Fri Aug 27 2010 do record types in mutual blocks make sense? 27/08 00:03 oh dear; did I do that? 27/08 00:05 if a datatype with a single constructor is a allowed why a record shouldn't? assuming they get checked for positivity too, which isn't currently the case 27/08 00:12 records aren't recursive... unless you make them so by tenuous recursive definition 27/08 00:13 datatypes live in mutual blocks to support induction-recursion; there's no obvious analogue for records 27/08 00:15 ah, makes sense, except that Agda allows recursive records 27/08 00:16 Moreover, the mutual block approach to I-R is taking a long time to get right. 27/08 00:16 Recursive records? Military intelligence! 27/08 00:17 "record Rec : Set where field rec : Rec" :) 27/08 00:18 with eta-expansion, to boot 27/08 00:18 even "record U : Set where field u : U -> U" works :) 27/08 00:18 Gordon Bennett! 27/08 00:19 (colloquial expression of horror) 27/08 00:20 (ah, google only found surprise :) 27/08 00:20 we reported this on the tracker a few months ago 27/08 00:21 surprise-with-disapproval is probably more accurate than horror 27/08 00:21 Whatever its other alleged roots (rakish son of newspaper proprietor, etc) "Gordon Bennett" is certainly an avoidance of blasphemy. 27/08 00:24 wouldn't that be "Gordon Dashiell" 27/08 00:26 now I'm googling 27/08 00:28 http://code.google.com/p/agda/issues/detail?id=138 <- interesting 27/08 00:29 scary, you mean 27/08 00:33 pigworker: "GD" 27/08 00:34 as in gd'ed something-or-other 27/08 00:34 pigworker: lol, nice tweet 27/08 00:36 copumpkin: they'd take my comedy card away if I didn't &c 27/08 00:36 Adamant: as in Jewish blasphemy avoidance? 27/08 00:37 pigworker: yeah, as in general Judeo-Christian blasphemy avoidance 27/08 00:37 The tradition I grew up observing made a distinction between reference to the deity as a deity (permitted by name) and the expletive usage (forbidden). 27/08 00:40 ah 27/08 00:41 general expletive, not specifically in conjunction with foul language 27/08 00:41 I presume 27/08 00:41 Yes. One may use "God" as a proper noun referring to God, but in no other way. 27/08 00:42 right. 27/08 00:43 People from Godalming don't like watching Flash Gordon. 27/08 00:43 Ming The Merciless! 27/08 00:44 or rather, Mentok The Mind-Taker: 27/08 00:46 http://en.wikipedia.org/wiki/Mentok_the_Mind-Taker 27/08 00:46 ok, enough OT. 27/08 00:46 * edwinb was wondering if he'd just wandered into the wrong channel ;) 27/08 00:51 Saizan: have you been able to figure out the logic behind pluralizing module names in the ctfp library? 27/08 01:02 Category.Adjunction vs. Category.Monads or Category.Functors 27/08 01:03 oh is it just to avoid a conflict with the standard library? 27/08 01:03 copumpkin: Oh. You put them in the wrong place. 27/08 01:14 There should be two additional proofs in Pullback. 27/08 01:15 One should say that p1 . universal ... = q1, and the same for 2. 27/08 01:15 oh 27/08 01:15 but q1 aren't set in stone 27/08 01:15 q1 and q2 27/08 01:16 Yes, it'd be parameterized by that. 27/08 01:16 ah, fair enough 27/08 01:16 man, there's a lot of repetition here 27/08 01:16 For any q1 and q2, that commute with f and g, they factor into pk . univ, and said univ is unique. 27/08 01:17 I guess I could just have the proof be a triple to save repetition 27/08 01:18 avoid it 27/08 01:18 but that seems ugly 27/08 01:18 Well, that it's repetitious is probably why categorists don't write it all out this way. 27/08 01:21 yeah 27/08 01:21 You can abstract it all by talking about diagrams, which are functors from some appropriately shaped category. 27/08 01:22 Then you have cones given a diagram, and (co)limits are (initial) final cones. 27/08 01:22 hm yeah, I've been putting off learning about that :P 27/08 01:23 Cones being natural transformations (to) from an object (I think I got the order right). 27/08 01:23 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29491#a29495 27/08 01:24 I don't know how usable something like that would be in Agda, though. 27/08 01:24 yeah, we need a new categorical programming language! 27/08 01:24 :P 27/08 01:24 Yes, this looks pretty right. 27/08 01:25 wow, and it only took me 15 tries :) 27/08 01:25 Of course, I can't rule out that I'm forgetting something. 27/08 01:25 A diagram is given by some V : Set, and some E : V -> V -> Set. Now what does it mean? 27/08 01:25 time for some marmite 27/08 01:26 In my case, time to fall over. G'night! 27/08 01:27 If you're a categorist, you take the free category over that graph, and use that for the stuff I wrote out above. 27/08 01:27 pigworker: Also: did they actually disallow recursive records yet? 27/08 01:30 Last I checked, they were allowed, and not positivity checked, to boot. 27/08 01:30 Bug still seems open. 27/08 01:33 this is odd 27/08 19:49 anyone ever encountered C-c C-r in a hole leading to a parse error 27/08 19:49 ? 27/08 19:49 okay, wrote pushouts too 27/08 20:08 can I reopen a parametrized module from within it, with a different parameter? 27/08 20:12 What's C-c C-r again? 27/08 20:17 I think it's "refine", and I'm not sure what it does in general, but if you give it an empty hole that can be filled with only one constructor, it'll put that in for you 27/08 20:17 so if I put it into a record hole, it'll write the record structure out for me with a bunch more holes in it 27/08 20:17 Ah. 27/08 20:18 or if it's a function, it'll give me a lambda 27/08 20:18 with the right parameters 27/08 20:18 That sounds handy. I should start using that. 27/08 20:18 yeah, I love it, but this is the first time it's failed me 27/08 20:18 * copumpkin is trying to figure out how to write the pushout for Sets 27/08 20:18 seems tougher 27/08 20:19 It's conceivable that Agda's Set doesn't have pushouts. 27/08 20:19 It may require quotients. 27/08 20:19 that's what I thought might be the issue 27/08 20:19 Unless you're using setoids. 27/08 20:19 damn :P 27/08 20:19 hm, I'm not 27/08 20:20 time for a subobject classifier! 27/08 20:27 Anyhow, as I recall, and from thinking for a minute or so, a pushout B C in set is the sum B + C quotiented by the equivalence relation induced by {(left (f x), right (g x))} 27/08 20:31 And the quotient part isn't really available in Agda. 27/08 20:34 yeah 27/08 20:37 I guess I can't write a subobject classifier for Set either, in agda? 27/08 20:38 for the same reason 27/08 20:38 My knowledge of topos theory is limited, but it wouldn't surprise me if Agda weren't a topos. 27/08 20:40 Off the top of my head, toposes correspond to impredicative and extensional type theories. 27/08 20:40 aren't Σ types similar to subobjects? 27/08 20:51 hmm, but would that be in a different category? 27/08 20:52 e.g. Σx:X.φ ~ { x ∈ X : φ } 27/08 20:52 The subobject classifier is an object O such that morphisms A -> O correspond to the subobjects of A, or something like that. 27/08 20:52 In Agda, you'd use O = Set, but you don't have Set : Set, so it's not an object. 27/08 20:52 so maybe we have subobjects without the classifying object? 27/08 20:53 ah, hm 27/08 20:53 It could be Bool, but that only works for decidable subobjects. 27/08 20:53 Anyhow, having a subobject classifier, together with exponentials, is similar to having powersets, I think. 27/08 20:55 O^A being the power-object, the object of all subobjects of A. 27/08 20:56 And powersets seem fairly tied to impredicativity. 27/08 20:57 hmm, are there cases in which eta expanding is necessary? 27/08 21:00 So maybe (some subset of) Coq would have one, but I'm uncertain how it would work out exactly. 27/08 21:00 Prop being the subobject classifier for the topos of Types would seem reasonable, I guess. 27/08 21:01 But that doesn't directly make use of impredicativity. 27/08 21:01 At least, as far as I can see. 27/08 21:01 So perhaps Agda could add some O : Set with no general eliminator, but top, bot : O, and Lift : O -> Set, Lift top = \top, Lift bot = \bot, or something. 27/08 21:05 And have a subobject classifier. 27/08 21:05 But I don't really know what all that would entail. 27/08 21:05 hmm 27/08 21:07 I'm not convinced the pushout is impossible, but I haven't succeeded in making one yet :P 27/08 21:08 Oh no? I bet I can convince you. 27/08 21:08 oh okay 27/08 21:09 now we need a proof of \neg Pushout :P 27/08 21:09 Well, it won't be anything like that. 27/08 21:09 yeah, just being silly :) 27/08 21:09 I'll start with a pushout and get a quotient type. 27/08 21:09 At least, that's the idea. 27/08 21:09 okay 27/08 21:10 Hmm, I may have been over zealous. 27/08 21:25 I'm no longer sure how to do this. 27/08 21:25 I'm getting closer and closer in the proof, which is making me worry about my pushout definition more than my proof :P 27/08 21:27 Hmm, maybe my initial idea was okay... 27/08 21:31 hmm 27/08 21:34 well agda just accepted this, but I think I proved something else 27/08 21:34 oh duh 27/08 21:35 yeah, my proof is pretty meaningless :P 27/08 21:35 man, I can't believe I worked on this for the past half hour without realizing that I was starting from something so obviously untrue 27/08 21:36 if you want to laugh at me, my proof took in a proof of inj1 (f x) == inj2 (g x) 27/08 21:47 so yes, I have pushouts in agda :P 27/08 21:47 That would help. 27/08 21:47 seems like I sort of want polymorphic variants here 27/08 21:59 Bah, the eliminator is going to require extensionality of functions. 27/08 22:00 ok, I realize I am in uncharted territory here, but it seems like sequencing IO operations leaves something to be desired. For example, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29536 27/08 22:29 what's wrong with that? :P 27/08 22:29 I'm sure I've seen people write it more linearly 27/08 22:29 do you need the parentheses? I thought the associativity worked nicely 27/08 22:30 it's not the parens so much that are the issue 27/08 22:30 when you have only two IO operations it looks ok 27/08 22:30 foo4 : IO ⊤ 27/08 22:30 foo4 = 27/08 22:30 ♯ putStrLn "foo 1" >> 27/08 22:30 ♯ putStrLn "foo 2" 27/08 22:30 but, if you want to extend it to three, then you need an extra, ♯ 27/08 22:31 _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B 27/08 22:31 because the return type of (a >> b) is IO B, not ∞ (IO B) .. or something 27/08 22:32 yeah 27/08 22:33 copumpkin: http://code.haskell.org/~dolio/agda-share/html/PushoutQuotients.html 27/08 22:33 stepcut: I see what you mean 27/08 22:33 if you do, (♯ a >> ♯ b) >> ♯ c, that does not work, because (♯ a >> ♯ b) has the type IO b, not ∞ (IO B) 27/08 22:34 so you have to do, ♯ (♯ a >> ♯ b) >> ♯ c 27/08 22:34 dolio: oh thanks, interesting 27/08 22:34 which is pretty ugly pretty fast 27/08 22:34 maybe I am just the first person to try to sequence *3* IO operations in a row ? 27/08 22:34 lol 27/08 22:34 works great for 2 :) 27/08 22:34 stepcut: maybe make some sort of list thing that gets sequenced? :P 27/08 22:35 That's an odd type. Is that a constructor? 27/08 22:35 dolio: yeah 27/08 22:35 Ah, okay. 27/08 22:35 data IO : Set → Set₁ where 27/08 22:35 lift   : ∀ {A} (m : Prim.IO A) → IO A 27/08 22:35 return : ∀ {A} (x : A) → IO A 27/08 22:35 _>>=_  : ∀ {A B} (m : ∞ (IO A)) (f : (x : A) → ∞ (IO B)) → IO B 27/08 22:35 _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B 27/08 22:35 we should have dependent IO! 27/08 22:36 where bind takes (x : A) -> inf (IO (B x)) :P 27/08 22:36 if it had the type, _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → ∞ IO B, then it would be fine? But I don't know if you can even do that.. 27/08 22:36 I'm not surprised, then. Programming directly with the coinductive type as a DSL is unlikely to be nice. 27/08 22:37 I'm not sure a nice DSL (passing all the relevant checkers) has yet been discovered, though. 27/08 22:38 :) 27/08 22:38 is there some what it could be changed so that sequencing 3 in a row was a little less painful? 27/08 22:38 >> and >>= should probably be definitions, for instance, but then you can't write down directly recursive things. 27/08 22:39 And have type IO A -> IO B -> IO B and so on. 27/08 22:39 maybe I should post on the mailing list and ask whoever wrote IO.agda in the first place? 27/08 22:40 And conceivably you could introduce recursion via a combinator, but the question is what that combinator is. 27/08 22:40 stepcut: and you thought you were just going to write hello world! now it's time for you to publish a few papers and write a dissertation 27/08 22:41 copumpkin: :) 27/08 22:41 copumpkin: IO A -> ((x : A) -> IO (B x)) -> IO (B ?) 27/08 22:41 copumpkin: the tricky part is when I want to make it a loop ;) 27/08 22:41 dolio: yeah, beats me :P more research! 27/08 22:42 ? = unsafePerformIO m 27/08 22:42 aka, 10 print "hello, agda!"  ; 20 goto 10 27/08 22:42 I'm still annoyed that those proofs required extensionality. 27/08 22:42 Actually, I could probably get around it if the Pushout proofs weren't formulated as composition. 27/08 22:43 I'll just leave it, I guess. 27/08 22:44 yeah 27/08 22:45 let's just wait for agda 2.2.8 with extensionality and quotient types (and let's throw some substructural types in for stepcut too, while we're at it) 27/08 22:45 how long do we have to wait ? 27/08 22:46 Agda 2.2.8: the type theorist's wet dream 27/08 22:46 stepcut: it's waiting on perl 6 27/08 22:47 k 27/08 22:48 I just want to make a little app that has a 'loop' which does getLine, processes the string, and does a putStrLn 27/08 22:53 it's pretty crazy, I know.. 27/08 22:53 ok, email sent! 27/08 22:54 it's a good thing you can prove you app is correct before you actually compile it .. because compilation takes forever :p 27/08 22:55 check the proof can take even longer! 27/08 22:56 there's a module in the category theory package that has a comment saying "I can't keep working on this because I don't have enough memory" 27/08 22:57 should we buy a server and share a single session? 27/08 22:58 if only I hadn't quit grad school, or I'd still have access to a 32GB machine 27/08 22:59 actually a couple of them 27/08 22:59 so we could prove things in parallel! 27/08 22:59 wow! 27/08 22:59 -or there 27/08 22:59 With 32 GB of memory, I could prove three additional category theory theorems! 27/08 23:01 My desktop has 10GB.. that's enough to run safari, firefox, and chrome at the same time! (Not really sure why I am doing that though..) 27/08 23:02 Wow, 10 is a lot. 27/08 23:02 Mine has 2. 27/08 23:02 It's pretty old, though, I guess. 27/08 23:02 I had 2GB, wasn't enough, so I added 8 more.. wasn't that much though 27/08 23:03 I'm with Saizan! we should pool our money and buy a monster server, for epic proofs 27/08 23:03 ram is pretty cheap these days, but many laptops can't take it :( 27/08 23:03 yeah, my laptop is maxed out a 4GB (though, right now I can only access 3GB) 27/08 23:04 http://gizmodo.com/5365029/sgis-personal-supercomputer-handles-80-cores-1tb-of-ram 27/08 23:05 we might also use the same money to pay someone to optimize Agdas.. 27/08 23:05 yeah, 1TB of ram is still around \$90,000 I think ? 27/08 23:06 Saizan: pff, where's the fun in that 27/08 23:07 I'd be curious to see where most of the ram usage is though 27/08 23:08 products in that category are interesting 27/08 23:16 I think Tyan also had a more PC-based one 27/08 23:16 with all the hyperthreading multi-core stuff, it's much more realistic 27/08 23:17 copumpkin: All right, non-extensionality version: http://code.haskell.org/~dolio/agda-share/html/PushoutQuotients.html 27/08 23:17 I wonder how well GHCs garbage collection would hold up with hundreds of GB of data.. 27/08 23:17 dolio: that makes sense :) 27/08 23:18 should I push the pushout and pullback to the ctfp repo? 27/08 23:38 * Saizan votes yes 27/08 23:41 pushed! omg 27/08 23:51 --- Day changed Sat Aug 28 2010 dolio: do you remember what part of your Category.Product caused agda's memory usage to blow up so much? 28/08 00:55 like, is there something that can be easily commented out to make it a little less ridiculous? 28/08 00:56 The two isomorphisms. 28/08 00:56 A x B ~ B x A and A x (B x C) ~ (A x B) x C 28/08 00:56 ah 28/08 00:57 The proofs themselves are enormous, so it may not be surprising that they're memory heavy. 28/08 00:58 Actually, the first one isn't so bad, but the second is very long. 28/08 00:59 yeah 28/08 01:01 I wonder how much agda uses laziness behind the scenes 28/08 01:17 Evaluation is in fact lazy in agda. 28/08 01:18 You can tell by writing stuff that fails the termination checker. 28/08 01:18 well I mean in the type/termination checker itself 28/08 01:18 http://snapplr.com/fqjm 28/08 01:18 that's a lot of lists 28/08 01:19 I was wondering how much strictness annotations on datatypes + -funbox-strict-fields could help its memory gobblage 28/08 01:19 (yeah, I really want to play with monoidal categories without having to fix my computer and put the other stick of memory back into it :P) 28/08 01:21 is there a way to know the type of the lists? 28/08 01:23 I was trying to figure it out, but couldn't find anything 28/08 01:23 h 28/08 01:23 oh 28/08 01:23 -hy 28/08 01:23 will test again :P 28/08 01:24 lol 28/08 01:25 it gives the type as [] :P 28/08 01:25 I guess it doesn't maintain enough information 28/08 01:25 heh 28/08 01:25 maybe the elements are the stg_ap_2_upd_info thing, or they don't use as much memory.. 28/08 01:26 gah, profiling this thing is terrifying 28/08 02:03 I picked at some of the low-hanging fruit but it didn't help 28/08 02:03 bah, I give up :P this thing is a monster! 28/08 02:29 man, trying to encode a simple linear lambda calculus such that the invariants are encoded in the indices is a real pain 28/08 03:42 http://code.haskell.org/~dolio/agda-share/html/SetoidPushout.html 28/08 04:55 The category of setoids has pushouts. 28/08 04:55 That file somehow manages to load faster than the one showing that pushouts in Set allow quotient types. 28/08 04:57 wow :) 28/08 04:57 neat 28/08 04:57 By a significant margin. 28/08 04:57 copumpkin: So, I'm looking at what a subset classifier set would look like in Agda, and one limitation is that you can't quantify over sets in defining values in the classifier (presumably). 28/08 05:48 Which renders it unable to represent impredicativity. 28/08 05:48 I'm not sure if that would keep it from being a topos or not, though. 28/08 05:48 I hope not! I really want me a topos 28/08 05:52 It probably does, because you can't necessarily define an A -> Ω for every subobject of A. 28/08 05:52 yeah :/ 28/08 05:52 Only, again, decidable subobjects of A, because you need to use a decision procedure to select what Ω to return. 28/08 05:52 would it make sense to make a decidable category? 28/08 05:53 What do you mean by that? 28/08 05:53 trying to think what I mean by it :) 28/08 05:54 category of decidable relations over agda types? 28/08 05:54 That might be pretty limiting. 28/08 05:55 Anyhow, I suspect that whatever you mean by that, it's not going to work out well. 28/08 05:56 :) 28/08 05:56 damn 28/08 05:56 If you want all the objects to have decidable equality, for instance, there are no exponentials. 28/08 05:57 that makes sense 28/08 05:57 dammit 28/08 05:57 category of enumerable types and relations between them? 28/08 05:58 sounds like a nightmare though 28/08 05:58 but that should restore your exponentials and give you subobjects too, I'd think 28/08 05:59 if A is a datatype constructor, how do I derive ⊥ from a proof ~ : A x ≡ x ? 28/08 21:07 absurd patterns appear to not work here 28/08 21:08 "A x ≡ x should be empty, but it isn't obvious that it is." 28/08 21:08 but it doesn't suggest any valid constructors 28/08 21:09 (there aren't any) 28/08 21:18 danbrown, lookup "a few constructions on constructors", you're looking for an acyclicity property here 28/08 21:25 pedagand: great, thanks 28/08 21:25 for nat, this boils down to that: http://pastebin.com/jz4Ek47Y 28/08 21:32 but maybe there is some clever, generic stuff in the stdlib doing that already, I don't know 28/08 21:33 yeah... 28/08 21:34 looks a little more complicated when you have multiple constructors 28/08 21:34 yeah, that's also what they say :-) 28/08 21:49 if I understand correctly, you want to peal off when both sides have same constructor and get back to the point where you've two distinct constructors at the head (at which point '()' dissolves the problem) 28/08 21:51 i see, that makes sense 28/08 21:59 --- Day changed Sun Aug 29 2010 how'd you fomalize the Yoneda Lemma? i'm not sure in which category the bijection should live 29/08 22:58 C x Set^C -> Set 29/08 23:00 (A, F) |-> FA is isomorphic to (A, F) |-> Nat(Hom(A, -), F) 29/08 23:02 I think that's right. 29/08 23:03 what is |-> ? 29/08 23:03 Maps to. 29/08 23:04 i see 29/08 23:06 The first one being the evaluation morphism for functor categories as exponentials. 29/08 23:07 i'm prejudiced against using Set for some reason, it feels like stepping out of the theory 29/08 23:14 Yes, I know. I feel the same way. 29/08 23:14 There's probably a Yoneda lemma in enriched category theory that switches Set with something else. 29/08 23:16 Including other categories if you want. 29/08 23:16 Actually, I guess it'd always be another category. 29/08 23:17 i've realized that my F is going to be an hom functor, and those are already C^op x C -> Set, so it's fine 29/08 23:18 dolio: Set^C is the category of covariant functors from C to Set, right? since i read things like "the category Set^C of presheaves" but a presheave should be C^op -> Value so i'm a bit confused 29/08 23:43 Yes, covariant functors. 29/08 23:44 There's a yoneda lemma for contravariant functors too, though, I think. 29/08 23:45 i think one just takes C = D^op for that? 29/08 23:45 Though maybe you get it by substituting C = D^op. 29/08 23:45 Yeah. 29/08 23:45 You could state it directly, though. 29/08 23:45 C^op x Set^C^op -> Set 29/08 23:46 (A, F) |-> FA is isomorphic to (A, F) |-> Nat(Hom_C(-, A), F) 29/08 23:46 But Hom_C(-, A) is Hom_C^op(A, -) 29/08 23:47 * dolio has to jet. 29/08 23:48 i'm going to need both sides anyway :) 29/08 23:48 thanks! btw 29/08 23:48 No problem. 29/08 23:49 --- Day changed Mon Aug 30 2010 * Saizan pushed some bifunctors 30/08 16:48 Saizan: ooh! 30/08 16:54 I'll do trifunctors and you can do quadrifunctors 30/08 16:54 heh :D 30/08 17:07 (maybe defining Bifunctor explicitly wasn't such a great move, but i think i'll need some convenience operators specialized for those in the future) 30/08 17:08 btw, is it possible to have a Cat where the categories can be at different levels? 30/08 17:09 make a SigmaCat? :P 30/08 17:09 dunno 30/08 17:09 it doesn't seem to like "∃ \ o -> ∃ \ ℓ -> Category {o}{ℓ}" 30/08 17:13 well, I'd wonder what the kind of the resulting Sigma would be 30/08 17:16 I mean the level 30/08 17:16 \inf ?:) 30/08 17:16 :P 30/08 17:17 dolio did mention an omega level that you can't write or something 30/08 17:17 Yes. (l : Level) -> Set l has type Set\omega, for instance. 30/08 17:42 But you can't make analogous sigmas in Agda. 30/08 17:42 so no fundamental reason for not being able to do so beyond not having a way of describing the universe of the resulting Sigma? 30/08 17:48 I think that's right. 30/08 17:49 upts on my code.haskell.org site has sigmas like that. 30/08 17:49 So you can make, for instance, { l : Level, A : Set l | A }. 30/08 17:50 The type of all non-omega types. 30/08 17:50 ah 30/08 17:51 is there a suc omega for the type of all types including those in set omega? 30/08 17:51 No. Omega is the top. 30/08 17:52 copumpkin, Saizan: thanks for the patches :-) 30/08 18:58 stevan: btw, do you know why is-product in Category.Categories.Product was commented out? 30/08 19:15 lack of time probably -- we had a deadline. :-) 30/08 19:17 --- Day changed Tue Aug 31 2010 so say I'd like to do a proof to show that a bounded monotone real sequence converges. I need to show that a sequence enters every neighborhood of its least upper bound, and show that a monotone sequence remains in every neighborhood of an upper bound once it has entered it. 31/08 02:46 it's simple to show this using the definitions of the least upper bound and monotonicity, respectively 31/08 02:47 but what would this look like expressed in agda? 31/08 02:47 would this be a good first task to try formalizing? 31/08 02:48 if it involves the reals, probably not 31/08 02:48 it should work with any lattice that has the least upper bound property and the completeness property, I'm guessing 31/08 02:50 you could probably do that abstractly, but I'd still recommend proving some trivial things first, to get a feel for it 31/08 02:51 doing it abstractly would involve specifying the minimal facts about the real numbers and such that would let me express what I've written out? 31/08 02:54 rather than worrying about computing reals? 31/08 02:54 would supercompilation be automatic in a strongly normalizing language? 31/08 20:09 assuming someone actually bothered to compile it 31/08 20:09 Automatic? 31/08 20:11 well 31/08 20:13 in the sense that you already have the compile-time evaluation mechanism built into the language and you don't need to worry about the non-termination hoops supero had to jump through 31/08 20:14 You don't have to worry about some of them. 31/08 20:14 I think tail recursive functions might still be subject to infinite amounts of unfolding. 31/08 20:15 If my recollection that that is a problem is correct. 31/08 20:16 hmm 31/08 20:16 But you don't have to worry about the partial evaluation part failing to terminate, presumably. 31/08 20:16 As long as your supercompiler never asks for ill-typed or otherwise termination-check-failing terms to be evaluated. 31/08 20:17 Actually, I guess it's functions with an accumulating parameter. 31/08 20:25 "foo acc v" unfolds to something involving "foo acc' v'", where acc' is probably an expression that doesn't match anything above it. 31/08 20:27 For instance, 'length l = foldl (+) 0 l' unfolds to 'case l of [] -> 0 ; x:xs -> foldl (+) 1 xs' wich unfolds to something involving 'foldl (+) 2 ys' and so on. 31/08 20:29 You need to cut that off at some point. 31/08 20:29 yeah 31/08 20:30 makes sense 31/08 20:30 so fewer heuristics would be needed, but you'd still need a few 31/08 20:30 Did you read Max Bolingbroke's paper on supercompilation? 31/08 20:30 yep 31/08 20:30 Well, he mentions that you need the termination heuristic in two places. 31/08 20:31 One is for making sure that your evaluator doesn't run forever, and the other is so that supercompilation doesn't go on forever, more or less. 31/08 20:31 If your language is strongly normalizing, you shouldn't need it for the first. 31/08 20:31 And I think he mentions that the two uses are kind of unrelated, aside from the fact that he uses the same heuristic in both cases. 31/08 20:32 the second case is a "should optimizie this more?" rather than a "does this term terminate?" heuristic? 31/08 20:41 Something like that. 31/08 20:42 Well, the intention of the first is, "should I keep running my evaluator." 31/08 20:42 So they're similar in idea if not all programs terminate. 31/08 20:43 His supercompiler essentially works on STG machine states. 31/08 20:43 So you can check if you should stop evaluating after each machine step. 31/08 20:43 Although, I think he recommends not doing that, because single machine steps might produce states that are similar enough to make the heuristic say stop when it'd be productive to keep going. 31/08 20:44