/home/laney/.irssi/irclogs/Freenode/2010/#agda/August.log

--- Log opened Sun Aug 01 00:00:38 2010
Saizanno, that's probably the most annoying thing about universe polymorphism01/08 00:01
liyangcopumpkin: http://www.demotivator.org/index.php/customize/create_image/128061929601/08 00:37
copumpkinhmm that link didn't work, it just took me to a generic page01/08 00:38
liyanghttp://liyang.hu/crap/mycode.png01/08 00:40
copumpkinMY EYES01/08 00:40
copumpkinGIVE THEM BACK01/08 00:40
copumpkinwhat is it?01/08 00:40
liyangI'm not quite sure yet… :-/01/08 00:41
copumpkinwhat's the general topic? :P01/08 00:43
liyangtransactional memory. ;_;01/08 00:45
liyangWas inspired by something you said on #haskell.01/08 00:45
copumpkinoh yeah01/08 00:47
liyangThe absurdity of that ↣-READ′ lemma is that the RHS is always ‘r’. >_<;;01/08 00:55
copumpkin:O01/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
copumpkinwow01/08 10:06
copumpkinwhat are you proving?01/08 10:06
darkwhat is dependently-typed?01/08 12:25
copumpkintypes with arbitrary expressions in them ;)01/08 12:26
darkis coq also dependently-typed?01/08 12:26
copumpkinyep01/08 12:26
darksome people that dealed with coq said it's a bit difficult to grasp01/08 12:26
darkis there an agda tutorial somewhere?:P01/08 12:27
copumpkinsort of01/08 12:27
copumpkinoh yeah01/08 12:27
darkaccessing wiki01/08 12:27
copumpkinhttp://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf01/08 12:27
soupdragondark weren't you asking how to do classical logic in coq?01/08 12:29
darkyes, I actually asked en passant, my problem was other (how to derive a natural deduction proof for a theorem)01/08 12:30
soupdragonI hope you realize that the logic of agda is not close to classical logic either01/08 12:30
darkI then learned about those hints and that if I add the law of excluded middle, I get classical logic01/08 12:30
copumpkinlol, http://snapplr.com/503201/08 12:30
copumpkindark: if you want to add LEM, the coq prop/set distinction is probably better for you than agda01/08 12:31
copumpkinbut agda is fun to play with as a haskell-alike with stronger types :P01/08 12:31
darkif_then_else_, o.o01/08 12:34
darkilluminating01/08 12:34
copumpkinit's cool but I don't think I've ever used that function01/08 12:34
dark"the type of non-empty lists" is interesting01/08 12:40
dolioEventually 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
copumpkininteresting01/08 12:41
dolioAnd unrestricted side effects, too.01/08 12:42
dolioWhich is a little less exciting, perhaps.01/08 12:42
copumpkinoh, hm01/08 12:42
copumpkinlots of interesting stuff happening in this field01/08 12:43
copumpkinwe 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, duh01/08 12:44
dolioMaybe you can test that hypothesis, and write a book about it.01/08 12:45
dolioYou could call it...01/08 12:45
dolioThe Mythical Man-Month.01/08 12:45
dolioThat's a pretty good title.01/08 12:45
darksomething that always puzzled me: can you represent the type of elipses by their characteristic equation? and the type of circles as well01/08 12:45
darkwhen I mention this problem, people come with this soluton: class Elipse { .., class Circle { .., and then make one inherit from the other01/08 12:46
copumpkin:P01/08 12:46
copumpkindark: clearly you need dependent subtyping!01/08 12:47
darkit's not about what I need but if it can be done at all01/08 12:47
darkI'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 circle01/08 12:51
darknow I have the type of curves, and a subtype of it, that is the type of circles01/08 12:52
darkand then I can pass a circle as elipse, but not every elipse as circle01/08 12:52
dolioThat's asking quite a bit.01/08 12:53
darkit looks like that type of non-empty list..01/08 12:53
darkif 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 undecidable01/08 12:54
darkfor example, representing curves as lambdas would not work..01/08 12:54
darks/is undecidable/would be undecidable/01/08 12:55
copumpkinyou can use a dependent pair to model circles01/08 12:57
copumpkincircular :: Ellipse -> Set01/08 12:57
copumpkinCircle = Sigma Ellipse circular01/08 12:57
darkSigma Ellipse?01/08 12:58
copumpkinSigma is like a haskell pair (a, b), but the _type_ of b depends on the value of a01/08 12:58
dolioIt's also like a sum.01/08 13:00
copumpkinyeah01/08 13:00
dolioGeneralized to arbitrary index sets.01/08 13:00
copumpkinit's a pretty awesome type, overall01/08 13:00
darkEllipse -> Set is the type of functions that receive an ellipse and returns.. a type?01/08 13:00
copumpkindark: yeah, that type would typically either be the empty type or the unit type01/08 13:01
copumpkinempty type for false and unit type for true01/08 13:01
copumpkinso 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
copumpkinif 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 it01/08 13:02
copumpkindark: make sense?01/08 13:05
darkno.. there are other types at Set01/08 13:09
copumpkinyes, but circular doesn't return them01/08 13:10
copumpkinso a definition of circular might be01/08 13:10
copumpkincircular (Ellipse x) = if isCircle x then Unit else Empty01/08 13:10
copumpkinwhere data Unit : Set where tt : Unit01/08 13:11
copumpkinand data Empty : Set where -- nothing here01/08 13:11
darkI 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
darkyou 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 circle01/08 13:12
darkwithout needing to define circle as a special case of an ellipse01/08 13:12
soupdragonwhat does this have to do with dependent types??01/08 13:12
darksoupdragon, I saw "the type of the non-empty list" on that paper01/08 13:13
darkit looks like "the type of this arbitrary subset of this more general type"01/08 13:13
darkthat looks like "the type of this arbitrary subset of polynomials"01/08 13:13
copumpkinarbitrary subsets are Sigma01/08 13:14
TheOnionKnightdark: 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
TheOnionKnightdark: 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
darkas 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 case01/08 13:20
copumpkinyou need proofs :)01/08 13:20
copumpkinnothing comes for free01/08 13:20
darkthe mere existence of a total (+ invertible?) function Circle t -> Ellipse t is sufficient for asserting that all circles are ellipsis?01/08 13:23
TheOnionKnightwell, forall t. Circle t -> Ellipse t, but pretty much, yes.01/08 13:24
darkI 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
copumpkindark: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28467#a2846701/08 13:25
TheOnionKnightwell 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
darkah01/08 13:27
dark@.@01/08 13:27
darkps: unicode, yay=)01/08 13:27
copumpkin:P01/08 13:27
copumpkindark: does that code make more sense?01/08 13:28
darkyes01/08 13:29
copumpkinyou could use any inhabited type as "true" but ⊤ carries no additional information01/08 13:29
copumpkinso is often what you want01/08 13:30
darkhow do you type such chars?01/08 13:32
copumpkinin agda-mode in emacs, you can type backslash followed by some representation of the character01/08 13:32
copumpkin\top = ⊤01/08 13:32
copumpkin\bot = ⊥01/08 13:32
copumpkin\bn = ℕ and so on01/08 13:32
* copumpkin is going crazy trying to write this arity-generic function01/08 13:38
copumpkinoh nice, someone fixed the agda haddock01/08 15:58
copumpkinnow I can look and it and wonder why there are two semirings in it :)01/08 15:59
copumpkinI guess one is a class and the other is a record01/08 15:59
copumpkinC-c C-r is handy01/08 16:05
Saizancopumpkin: 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
copumpkinoh my01/08 16:16
dolioWhich bug?01/08 16:17
copumpkinA 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
Saizanhttp://code.google.com/p/agda/issues/detail?id=170 <- it's related to this one, but i can't find it01/08 16:30
Saizan(i should probably say "constructor-headed" rather than "injective", since that's apparently what is checked)01/08 16:30
dolioAh.01/08 16:33
Saizanthe "bug" was that recursive calls were considered constructors for the sake of this check01/08 16:37
Saizanwith the effect of making type inference make guesses that were wrong in some cases01/08 16:39
Saizancopumpkin: sounds scary.01/08 16:41
copumpkinjust found that in the agda source01/08 16:41
Saizanmaybe it's not the most scary thing around then :)01/08 16:43
dolio(A : Set) (P : A -> Set) (x y : A) (eq : x == y) (Px : P x) is a telescope.01/08 16:45
dolioOr something like that.01/08 16:45
Saizanbut Thierry-function-telescope ?01/08 16:47
dolioI'm not sure how to read those sentences. That might just be another reference for what they're talking about.01/08 16:48
dolioI'm not sure who coined the name "telescope." It may well have been Thierry Coquand.01/08 16:49
copumpkinwhy are they specifically named?01/08 16:49
copumpkinI guess they're useful? :P01/08 16:49
copumpkinwhere might one use them?01/08 16:49
dolioYou can make a telescope datatype, too.01/08 16:51
doliodata Telescope : Set1 where nil : Telescope ; cons : (S : Set) (S -> Telescope) -> Telescope01/08 16:52
dolioOr something of that sort.01/08 16:52
dolioOf course, that has limitations.01/08 16:54
Saizanthey are used to represent environments/contexts where the types of later elements can depend on the value of the former ones01/08 16:55
copumpkininteresting01/08 16:56
copumpkinthanks agsy for inserting  an f = f proof for me01/08 20:22
Saizan:O01/08 20:23
copumpkinhmm, I need to prove that equality on my permutations is decidable!01/08 21:18
copumpkinthis seems tricky01/08 21:18
Saizan"on my permutations"?01/08 21:18
copumpkinI branched off my original array stuff and decided to work on the permutations side of things for a bit01/08 21:19
copumpkinI think I may be OCD01/08 21:25
liyangYou don't have to be, but it certainly helps.01/08 21:25
copumpkintwo 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|...).Properties01/08 21:26
copumpkin:P01/08 21:26
copumpkinmmm, I want to prove stuff about decidable equality on Fin-domained functions01/08 22:08
soupdragonwell the theory of bijections on Fin n can get pretty deep01/08 22:37
Saizanseen .BagAndSetEquality ?01/08 22:39
Saizanhas a nice treatment of permutations, imho01/08 22:40
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.Any.BagAndSetEquality.html#270 ?01/08 22:40
Saizanyeah, i guess what i was really referring to is http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.Any.html#482801/08 22:45
Saizani never used it though, it only looked nicer than my more inductive treatment :)01/08 22:47
copumpkinhow did you do it?01/08 22:47
soupdragonthere was an fplunch post about that stuff iirc01/08 22:49
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28484#a2848401/08 22:51
--- Day changed Mon Aug 02 2010
copumpkinI wish I could partially apply implicit variables somehow02/08 11:43
dolioWhat does that mean?02/08 11:47
copumpkinI have a lot of λ {x} {y} → ⁻¹-cong {n} {x} {y}02/08 11:48
copumpkinjust writing -1-cong {n} turns yellow02/08 11:49
copumpkinbecause it won't pass the input {x} and {y} to the cong02/08 11:49
dolioOh.02/08 11:49
liyangcopumpkin: make the {n} explicit and move it after {x} and {y}?02/08 12:38
copumpkinI can't move it after x and y, cause x and y depend on it :/02/08 12:39
liyangSometimes it's just not worth using implicit arguments. :-/02/08 12:40
copumpkinI can't really change this though :( I'm building an algebraic structure from Algebra and it expects a proof in that form02/08 12:40
benc___k02/08 15:21
benc___oops sorry02/08 15:21
copumpkinhttp://code.haskell.org/~Saizan/agda-reflection/doc/main.tex02/08 16:37
copumpkinI guess that paper is still unreleased?02/08 16:38
copumpkinquoteGoal is pretty magical02/08 17:00
danbrowncopumpkin: re decidable permutations: would this help? http://acandystore.org/agda/Retract.html02/08 17:05
danbrown(an extension of dolio's http://code.haskell.org/~dolio/agda-share/DecEq.agda)02/08 17:06
danbrownbasically, if you can define an embedding of your permutations into sexps then you get decidable equality for free02/08 17:07
danbrownexample at the bottom02/08 17:08
copumpkinI see! that seems quite nice :)02/08 17:08
copumpkinI'll play with that, thanks!02/08 17:09
danbrownjust express your perms like (1 3 4 2) and you're all set :P (easier said than done?)02/08 17:12
danbrowngl02/08 17:12
copumpkinthanks :)02/08 17:12
copumpkinyeah, it should be that easy02/08 17:13
copumpkinI already have a transformation to a Vec (Fin n) n02/08 17:13
danbrownah! excellent02/08 17:13
copumpkinnot that I really needed decidable equality for anything :P02/08 17:13
copumpkinmaybe I do02/08 17:13
danbrown(that url is darcs-able, btw)02/08 17:14
copumpkincool!02/08 17:16
copumpkinhttp://code.haskell.org/~Saizan/agda-reflection/rls1/prop_logic/MyReflection.agda is amusing02/08 17:25
copumpkinthey set up a datatype with a constructor `course`02/08 17:25
copumpkinand a mixfix one _is_of_02/08 17:25
copumpkinand so all the proofs end in `of course`02/08 17:26
ccasincute02/08 17:26
liyangas in, ‘… as a matter of course’?02/08 17:27
danbrowni have a type error "A !=< if b then A else A". what's the right way to deal with this?02/08 17:47
danbrownshould i just code up my own eta contraction for Bool?02/08 17:47
danbrownor is there something slicker?02/08 17:48
liyangdanbrown: write a lemma : \all b A \-> if b then A else A \== A, then use rewrite lemma.02/08 18:08
copumpkinI think you just need to code up your own02/08 18:08
danbrownwhere can i read about 'rewrite'?02/08 18:09
danbrownhere? http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-602/08 18:10
copumpkinyeah02/08 18:10
copumpkinit mostly gets rid of the need for subst I think02/08 18:10
copumpkinif you have p : x == y and write rewrite p, it'll replace all instances of x with y in your goal and context types02/08 18:11
copumpkindolio said it's equivalent to just pattern matching on refl and filling in the right patterns02/08 18:11
danbrowndo i have to use it at top level?02/08 18:11
danbrownyeah, that makes sense02/08 18:12
copumpkinyou can stick it before any = in a function definition I think02/08 18:12
copumpkinso f x with rewrite p x = ?02/08 18:12
copumpkinwithout the "with"02/08 18:12
copumpkinf x with moo x \n ... | m rewrite p m = ?02/08 18:13
liyangWith rewrite though, there seems to be less scope for leaving out implicit arguments and letting Agda infer them.02/08 18:13
copumpkinyou can also rewrite by a bunch of things with pipes between them02/08 18:13
copumpkinrewrite p  | q | r = ...02/08 18:13
danbrowncool02/08 18:14
copumpkinI love it02/08 18:14
danbrownthat should nicely solve my first problem02/08 18:14
liyang(or you can also write f x rewrite y with g z\n…)02/08 18:18
copumpkinah, hadn't tried that02/08 18:18
liyangIt 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
copumpkinah yeah, I've used that02/08 18:22
danbrownmysterious failure... oh well. i'll stick to manual eta expansion for now :/02/08 18:30
copumpkindanbrown: rewrite does give the same kind of mysterious error messages as with sometimes02/08 18:30
copumpkinmentioning a w variable02/08 18:30
copumpkinsometimes I've found that calling sym on it will fix it02/08 18:30
danbrownthis was just a "failed to solve constraints"02/08 18:31
copumpkinoh :o02/08 18:31
danbrown_1574 w == _1584 w : _1532 w02/08 18:31
danbrownindeed mentioning a w variable ;)02/08 18:31
copumpkinoh, did you put a hole in the rewrite expression?02/08 18:31
danbrownyes02/08 18:31
copumpkinor does it have implicits that can't be inferred02/08 18:31
copumpkinyeah, it won't know what to do if the rewrite expression isn't fully determined I don't think02/08 18:32
danbrownoh02/08 18:32
danbrownwhen i bottom it out i get a different "failed to solve constriants": if b then _1477 w else _1487 w == _1497 w : Set02/08 18:32
danbrowndoesn't look like it made much progress :P02/08 18:33
liyangYeah, 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
danbrownwell, i do have lots of implicit args flying around02/08 18:33
liyangInstantiate them one by one until Agda stops complaining. :302/08 18:34
copumpkinlol, I see our workflows have things in common :P02/08 18:34
danbrownyeah, 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
danbrownway too easy to get lost in details02/08 18:36
danbrowndamn details02/08 18:37
danbrown(this function is quite ugly, though)02/08 18:37
copumpkindoes anyone know of any work on making a solver for ordered (semi)rings that can figure out inequalities?02/08 19:32
danbrownerror message: "Cannot split on the constructor foo when checking the definition of f"02/08 22:57
danbrownwhat does that mean?02/08 22:57
danbrowni'm starting to write a function matching on a large datatype and gave it a catch-all _ pattern at the bottom02/08 22:58
danbrownwell, but the error is actually on another line, so nm that02/08 22:58
dolioIn 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
dolioOh, and possibly when the refined index would involve an arbitrary function.02/08 23:01
dolioFor instance, I have a permutation type where one of the constructors is like: foo : (xs ys) -> (xs ++ ys) ~ (ys ++ xs)02/08 23:02
dolioSo, in a certian proof, you may have (x :: xs) ~ ys.02/08 23:02
doliobar with that type, say.02/08 23:02
stevancopumpkin: presburger can do inequalities, yes?02/08 23:03
dolioIf you try to match on bar, it will give that error.02/08 23:03
copumpkinstevan: not sure, don't know much about it, but it's a lot weaker than a general semiring, right?02/08 23:03
dolioBecause the (x :: xs) and the (xs ++ ys) are incompatible.02/08 23:04
dolioYou can't refine the former to get the form of the latter in any reasonable way, I guess.02/08 23:04
stevancopumpkin: i don't know much about it either :-). you can't have multiplication between variables, so it's weaker i believe02/08 23:05
copumpkinstevan: from what I understood, people liked it because everything was decidable in it02/08 23:05
copumpkinstevan: but I just need inequalities :)02/08 23:06
dolioIsn't it complete or something?02/08 23:06
stevan(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
copumpkinyeah, I saw that in his reflection folder02/08 23:08
copumpkinlooks cool :)02/08 23:08
copumpkinit seems like the same technique used in the semiring equality solver could be used for inequalities, but maybe not02/08 23:09
danbrowndolio: 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 details02/08 23:12
danbrowni'll comment out the bad constructor for now and keep that in mind as i refine my development02/08 23:13
benc___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 on02/08 23:13
dolioAre you sure there's a difference?02/08 23:14
benc___I get different errors in the emacs mode.02/08 23:14
benc___so yes.02/08 23:14
dolioHuh.02/08 23:14
liyangI 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
benc___maybe its type checking errors manifesting at different places02/08 23:15
copumpkinmaybe there are implicits02/08 23:15
copumpkinand putting a dot around the entire thing is the same as dotting the implicits too?02/08 23:15
benc___yeah maybe thats whats ahppening for me02/08 23:16
danbrowni'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
danbrown*no expert02/08 23:16
benc___I have a giant pattern with {.e :: .e' :: .v'} in it somewhere which gives a ucn' != suc n of type N02/08 23:16
benc___but if I change to {.(e :: e' :: v')} that goes away02/08 23:17
liyangYou can write that as .{e :: e' :: v'} , btw.02/08 23:17
benc___ok02/08 23:18
* liyang isn't sure he could explain the suc n' != suc n error without a concrete example.02/08 23:18
danbrown#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
danbrownnot sure that #1 makes sense, though02/08 23:19
danbrownseems like #1 implies #202/08 23:19
dolioThe multiple-dots version might do cons-matching first, technically.02/08 23:20
benc___so I can put .{any expression, not just a constructor pattern}   ?02/08 23:20
copumpkinbenc___: yeah02/08 23:20
benc___ok02/08 23:20
dolioI wouldn't expect that to really make a difference, except for having to write absurd cases.02/08 23:20
copumpkinbenc___: sometimes you'll see crazy stuff in pattern matches :P02/08 23:20
liyangbenc___: yes, .{any expression}02/08 23:21
liyangYou 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
liyangIt helps you to see what's going on though, of course.02/08 23:28
liyangSo 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
liyangI wish I knew how to fold text in Emacs. :(03/08 03:43
* liyang misses Vim.03/08 03:44
* benc___ wakes up again03/08 08:40
* Saizan never sleeps03/08 09:59
* Amadiro hi03/08 17:44
soupdragonhi03/08 17:44
Amadirohi03/08 17:45
copumpkinhi!03/08 17:50
AmadiroHm, I have to remember that. If I feel down next time, I'll just "/amsg hi", and see all the friendly responses :D03/08 17:51
benc___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 program03/08 19:17
copumpkinrationals03/08 19:18
benc___right03/08 19:18
copumpkinbut no operations on them yet03/08 19:18
benc___where?03/08 19:18
benc___ok03/08 19:18
copumpkinData.Rational03/08 19:18
benc___so "no" ;)03/08 19:18
copumpkinhey, the basic type is there :P03/08 19:18
benc___not in my 0.3 that i have here03/08 19:18
copumpkinit should be there03/08 19:18
benc___oh wait03/08 19:18
benc___it is03/08 19:18
* benc___ was only looking at subdirectories not files03/08 19:18
benc___doh03/08 19:18
benc___else i wouldn't even have asked here03/08 19:19
benc___data.rational and data.float was there first place i looked!03/08 19:19
copumpkin:) NAD said that someone had worked on filling in the Rational code but I'm not sure what happened with that03/08 19:19
* benc___ doesn't really mind building stuff up from low levels but its frustrating to find someone already did it03/08 19:20
copumpkindolio wrote a useful function for that a while back03/08 19:20
copumpkinbut I can't remember where it is03/08 19:20
dolioWhat?03/08 19:21
copumpkinto help definition of rational functions03/08 19:21
copumpkinI thought03/08 19:21
dolioOh.03/08 19:21
doliohttp://code.haskell.org/~dolio/agda-share/html/Rat.html03/08 19:21
copumpkinaha, that's the one03/08 19:22
copumpkintruthFromWitness is now a library function03/08 19:22
copumpkintoWitness I think03/08 19:22
dolioIs it? I wrote the thing in there because it was a counterpart to what was in the library.03/08 19:23
copumpkinoh03/08 19:23
copumpkinyeah, silly me03/08 19:23
--- Day changed Wed Aug 04 2010
copumpkinwow, that fp-lunch reflective presburger solver is pretty large04/08 00:06
Saizanyeah.04/08 00:07
copumpkinMY EYES04/08 00:09
copumpkinliyang: I just found something worse than your picture04/08 00:09
copumpkinI've heard of walls of code before, but holy shit: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28526#a2852604/08 00:09
Saizanis that The Matrix?04/08 00:11
copumpkinyep04/08 00:13
copumpkinit looks more terrifying with wrap on04/08 00:13
copumpkinnow I really want to ask it to solve me some presburger arithmetic statements04/08 00:14
liyang‘lol’.04/08 00:47
soupdragon¯\(°_0)/¯04/08 00:48
dolioThere's no way to improve that code?04/08 00:48
liyangWhat's that from?04/08 00:48
dolioI'm not sure how that was even written in the first place.04/08 00:49
liyangThe .(fdsjllvkdfml) patterns can be left out by replacing them with ._04/08 00:49
dolioEven the type signature is pretty heinous.04/08 00:51
Saizandarcs get http://patch-tag.com/r/gallais/agda04/08 00:51
copumpkinwho is gallais?04/08 00:53
liyangINRIA guy.04/08 00:53
copumpkinah04/08 00:54
liyang(I think. Did he visiting Nottingham? I don't know, I haven't been in the office for months…)04/08 00:54
liyangI 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
liyangThat's just a non-dependent product A × B…04/08 00:58
copumpkinyeah, it looks at least partially automated04/08 00:58
copumpkinbut I'm not sure what would've done that for him04/08 00:58
copumpkinagsy can't figure out way simpler stuff than that04/08 00:58
liyangAnd a lot of parentheses could have been left out with judicious assignment of operator fixities.04/08 00:59
liyang(I still have no idea what it does.)04/08 00:59
copumpkincooper's algorithm is apparently one way to decide statements in presburger arithmetic04/08 01:00
Saizani think the type is probably copy-pasted from a hole's type, and the rest is constructed by C-c C-c04/08 01:00
* copumpkin just discovered C-c C-r the other day04/08 01:01
copumpkinmade me quite happy04/08 01:01
copumpkin I only know half of what it does though04/08 01:01
liyangMmm… but C-c C-c generates quite messy code though.04/08 01:01
liyangIt'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
liyangIf 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
Guest825Hi, can anyone point me towards a tutorial on Theorem proving with agda please?04/08 01:34
liyangIntroductions to Agda: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation04/08 01:39
copumpkinI get the impression Berengal was having connection issues04/08 11:05
dolioLooks that way.04/08 11:32
dolioSo, I read yesterday that some people consider W-types to be impredicative.04/08 11:32
copumpkinW-types being the arbitrarily branching trees?04/08 11:33
dolioYes. data W (A : Set) (T : A -> Set) : Set where sup : (x : A) -> (T x -> W A T) -> W A T04/08 11:33
dolioApparently some people have decided that "predicative" means "has proof-theoretic ordinal less than or equal to Gamma_0."04/08 11:35
dolioBut theories with W-types have ordinals bigger than that.04/08 11:35
dolioAt least, W-types + a single universe.04/08 11:39
dolioBy 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
copumpkinis there an overview of the universe level rules?04/08 18:18
dolioWith or without universe polymorphism?04/08 18:28
copumpkineither, really04/08 18:29
dolioWell, if it's without, it's easy.04/08 18:31
copumpkinlet's do without then04/08 18:31
copumpkinI have an intuitive understanding of it, but wanted to get a summary04/08 18:31
soupdragonin AGDA?04/08 18:32
dolioIf |- A : SetM and x : A |- B : SetN, then |- (x : A) -> B : max(SetM, SetN)04/08 18:32
dolioAnd an inductive definition is valid if the types of its constructors have the same size as specified for the datatype.04/08 18:33
copumpkin that's it?04/08 18:34
dolioI think so.04/08 18:34
dolioThere'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
copumpkinmakes sense :)04/08 18:35
dolioWith universe polymorphism, it's almost the same.04/08 18:36
dolioExcept, 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
copumpkinwhich agda doesn't allow, right?04/08 18:38
dolioIt's buggy in that area.04/08 18:38
dolioAt least, I kind of consider it buggy.04/08 18:38
dolioIt's more buggy when you try to do inductive types involving Set\omega.04/08 18:39
dolioIt could, I think, allow things that it doesn't.04/08 18:39
copumpkinoh, Set\omega is a builtin? cause I looked at Level and there was no third constructor04/08 18:39
dolioYes, it is not a constructor.04/08 18:40
dolioI think naming it 'Set\omega' is a mistake, too.04/08 18:40
copumpkinhow come?04/08 18:40
dolioBecause it gives the impression that \omega is a Level, and thus that quantification over level should range over it.04/08 18:40
copumpkinah, as I guess happened with me :P04/08 18:41
dolioIn my personal interpreter, I called that universe \Omega.04/08 18:41
copumpkinthat's your pts?04/08 18:42
dolioupts.04/08 18:42
dolioThe fork.04/08 18:42
dolioWhich 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
copumpkinah04/08 18:43
dolioNot so broken that it won't likely work for whatever small experiments you're doing.04/08 18:44
dolioBut still broken.04/08 18:45
dolioI didn't discover that pts had problems until I was writing Hurkens' paradox.04/08 18:45
danbrowndolio: isn't it different in CoC? If |- A : SetM and x : A |- B : SetN, then |- (x : A) -> B : SetN04/08 20:07
danbrowndumb question: can someone explain to me how to use C-c C-c ?04/08 20:24
danbrownthe documentation isn't particularly helpful04/08 20:24
Saizanyou put the cursor over a hole, C-c C-c <name of variable> RET04/08 20:25
copumpkinit needs to be just a hole on the RHS04/08 20:25
copumpkinsometimes it'll not be able to figure it out04/08 20:25
danbrownso "f x = {! x !}" ? or "f = {! x !}" ? or "f = {! f !}" ?04/08 20:25
copumpkinoh, the x needs to be there04/08 20:25
copumpkinso you can ask C-c C-c to split it04/08 20:26
copumpkinso there you'd type C-c C-c x RET04/08 20:26
copumpkinand it would give you all the valid cases for x04/08 20:26
copumpkinwith one hole each04/08 20:26
Saizani don't put anything inside the hole04/08 20:26
copumpkinI don't think it makes a difference, but yeah, I usually leave it empty too04/08 20:26
danbrownso 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
copumpkinhmm, how would one represent inductive families (GADT-style) in a low-level dependent LC?04/08 20:27
copumpkindanbrown: what if you leave the hole empty?04/08 20:27
danbrownsame04/08 20:28
copumpkinthen you've probably encountered the bug that I submitted a couple of days ago04/08 20:28
danbrownhrm04/08 20:28
copumpkinhttp://code.google.com/p/agda/issues/detail?id=28904/08 20:28
danbrownso is all case splitting currently broken, or are we trying to do funny splits?04/08 20:29
danbrownmine seems particularly simple :P04/08 20:29
danbrownas do NAD's04/08 20:30
danbrown*does04/08 20:30
copumpkinI've had it work for more complex ones04/08 20:31
Saizanit generally works for me04/08 20:31
copumpkinnot sure under what conditions it breaks04/08 20:31
Saizanhow is your T defined?04/08 20:31
danbrownSaizan: from the stdlib: data ⊤ where tt : ⊤04/08 20:31
danbrown(with : Set something)04/08 20:32
Saizanit's actually a record in the stdlib iirc04/08 20:32
Saizanwhich might be the source of the problem04/08 20:32
Saizanit works with a data decls04/08 20:33
danbrownok, 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
danbrownsame error04/08 20:33
copumpkinmy original example was a data decl though04/08 20:34
copumpkinusing Dec P04/08 20:34
Saizanmaybe because 'a' is a pattern?04/08 20:34
danbrownSaizan: err, yes :P04/08 20:35
Saizanit seems error reporting is quite poor :)04/08 20:35
danbrownok, that "data A" example does indeed work04/08 20:35
Saizan"whatever happens, let's blame the RHS" :)04/08 20:36
danbrowncurious. the problem seems to occur when the _codomain_ is a record04/08 20:38
Saizan:O04/08 20:39
danbrowndata → data and record → data both work, but data → record and record → record both fail04/08 20:39
Saizanmh, that might make sense if there's some eta-expansion going on wrt the hole04/08 20:40
copumpkinoh, mine was using records too04/08 20:40
copumpkinjust indirectly04/08 20:40
copumpkinyou should comment on that ticket04/08 20:41
danbrowncopumpkin: my original problem (before g : ⊤ → ⊤) was also using Dec04/08 20:41
danbrowni will04/08 20:41
copumpkinmine is actually using False and True04/08 20:41
copumpkinbut those are functions that evaluate to \bot or \top04/08 20:41
copumpkinwhy is04/08 20:42
copumpkin\top a record, anyway?04/08 20:42
soupdragonbecause then it gets surjectivity04/08 20:43
soupdragonagda implements surjective/eta conversion for all records (since they have a single constructor)04/08 20:44
soupdragonjust means more things typecheck04/08 20:44
copumpkinsurjectivity in what sense?04/08 20:44
soupdragonwhen it comes down to it04/08 20:44
copumpkinah04/08 20:44
soupdragonlike surjective pairing04/08 20:44
soupdragon(fst p,snd p) = p04/08 20:44
soupdragonif you define pairs as a record ^ will be convertible04/08 20:44
soupdragonbut if you define them as a data type it wil not be provable04/08 20:45
soupdragonin the case of T it's   t = x    (forall x)04/08 20:45
soupdragonsince t is the only constructor04/08 20:45
copumpkinah04/08 20:45
soupdragonin the case of LAMBDA it's  f = \x -> f x04/08 20:45
soupdragonwhich Agda does implement04/08 20:45
copumpkinoh 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
copumpkin(where the constructors refine the type)04/08 20:49
Saizanyou need a primitive equality type, at least04/08 20:49
Saizanafaiu04/08 20:49
soupdragonyeah, Leibniz doesn't cut it04/08 20:49
soupdragonthe reasons why are kind of subtle I can't remember them - Coq'Art covers it04/08 20:49
copumpkinhmm04/08 20:57
copumpkinis there no pdf of it?04/08 21:00
copumpkinI guess it's a real dead tree book04/08 21:00
copumpkinso I guess GADT-alikes mean that you can't really decompose ADTs into sums/products etc.?04/08 21:07
soupdragoncopumpkin you should read Peter Morris' Thesis04/08 21:07
soupdragonwell except skip the chapters on containers04/08 21:08
soupdragonunless you can actually understand that stuff.... (I can't)04/08 21:08
soupdragonbut the rest is important04/08 21:08
copumpkinhttp://www.cs.nott.ac.uk/~pwm/thesis.pdf, right?04/08 21:08
soupdragones04/08 21:10
soupdragoneys04/08 21:10
soupdragonyes04/08 21:10
copumpkinthanks :) will read04/08 21:16
copumpkin"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
copumpkinboo04/08 21:22
doliodanbrown: 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
dolioOf course, the basis CoC doesn't have too many universes.04/08 21:46
danbrownso for Set(N+1) universes CoC uses the ITT-style rule?04/08 21:48
dolioIn 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
dolioYes. You must if you care about strong normalization.04/08 21:49
danbrownhmm04/08 21:50
danbrowncan you succinctly explain to me the essential difference between ITT and lambda-cube-style type theory (e.g. CoC)?04/08 21:50
danbrowni'm more familiar with the latter04/08 21:51
danbrownand as far as i can tell they're very similar, so i'm wondering what different purposes each serves04/08 21:52
dolioThey are pretty similar.04/08 21:52
doliohttp://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/04/08 21:53
dolioSome of the stuff there is pretty good.04/08 21:53
danbrownnot succinct :P04/08 21:54
dolioThe Intuitionistic Type Theory article by Martin-Loef himself is really readable.04/08 21:54
danbrownbut thanks for the references ;)04/08 21:54
dolioI have to step out for a while. Maybe I can try to explain later.04/08 21:54
danbrownok04/08 21:55
dolioI was surprised how readable the Intuitionistic Type Theory book is.04/08 21:55
danbrownhave you read the handbook article?04/08 21:56
danbrownNordström, et al.04/08 21:56
danbrownconfusing problem with magic patterns—any insight? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2855804/08 22:05
danbrownit's possible that it's just a bug04/08 22:06
danbrownbut i'm not sure04/08 22:06
copumpkinif it is empty but agda can't see it, just use \bot-elim04/08 22:07
copumpkinwhat's with your accented letters?04/08 22:07
danbrown;)04/08 22:07
danbrownhmm04/08 22:08
copumpkinoh, I see04/08 22:09
copumpkinwait, my agda got confused04/08 22:09
danbrownyeah, ok. i don't see how ⊥-elim helps.04/08 22:09
soupdragonwhat's happening?04/08 22:09
copumpkindanbrown: remove the absurd pattern and you get some yellow, too04/08 22:10
copumpkinyou need to put an accented pi into the implicits04/08 22:10
danbrown? but it's a constructor04/08 22:10
copumpkinoh yeah04/08 22:11
copumpkinwell, you need to provide its implicits then :P04/08 22:11
soupdragondanbrown, that's weird - looks like a bug to me04/08 22:11
danbrownoh, hmm04/08 22:11
danbrownsoupdragon: probably. trying to see if giving the implicits works around it...04/08 22:13
danbrownok, giving the implicit arguments appears to not help: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558#a2856204/08 22:30
danbrowni'll file a bug04/08 22:30
Saizanafaiu, it boils down to not be able to tell that "y ≡ (y + y') × s" should be empty.04/08 22:32
danbrownshouldn't an occurs check be enough?04/08 22:32
Saizanthat's what i'd naively expect04/08 22:33
Saizanhow would you go about proving that type is empty without dependent pattern matching?04/08 22:34
danbrownuhh...04/08 22:34
danbrowni don't know where to start, formally04/08 22:35
soupdragonwait04/08 22:36
soupdragonwh does it come down to y ≡ (y + y') × s04/08 22:36
soupdragon?04/08 22:36
soupdragonI thought it was just  that   π̀ {s} {t} ∙ M  isn't equal to either of  (ὶ ∙ V) or (ί ∙ V)04/08 22:36
Saizanwell, i've tried to convince agda of that by pattern matching on t first04/08 22:37
Saizanhttp://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 problem04/08 22:39
soupdragonSaizan what about pattern matching on Val in ¬Valπ̀? maybe that would let you avoid having a lemma04/08 22:40
soupdragonwell you'd get some equations to discharge, not sure if agda would do them automatically or not (hopefully would)04/08 22:41
Saizanit doesn't let me do that04/08 22:41
danbrownSaizan: i just created an issue, feel free to follow up: http://code.google.com/p/agda/issues/detail?id=29104/08 22:41
soupdragonI wish agda would install I want to have a look at this :/04/08 22:42
* copumpkin doesn't get why it's a bug04/08 22:46
copumpkinthere are many things that agda can't spot are empty at first glance04/08 22:46
Saizani'm not sure it's a bug either04/08 22:47
Saizanthough i've no idea how to prove "y ≡ (y + y') × s -> \bot" indirectly04/08 22:48
copumpkinagsy can spot it's empty :)04/08 22:50
danbrowncopumpkin: can it convince agda? ;)04/08 22:50
copumpkinnope04/08 22:50
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28558#a2856404/08 22:50
copumpkinvery nice04/08 22:51
Saizanhehe, good old eliminators :)04/08 22:51
dolioHow are those accented characters typed, by the way? Emacs wouldn't tell me?04/08 22:52
dolioIs it a separate accent character?04/08 22:52
dolioLike \^ will put a hat on the previous character?04/08 22:52
danbrowndolio: yeah, they're "combining characters" in unicode. when you enter one they decorate the preceding character04/08 22:53
danbrowndolio: i type them by manually entering a bunch into my .vimrc ;) the agda table for quail could be extended to include them04/08 22:53
dolioHeh.04/08 22:53
danbrown(still grokking your solution)04/08 22:55
dolioI used the standard inductive eliminator for Val.04/08 22:56
danbrownon the bottom line, is _ the only thing you can write there?04/08 22:56
dolioThe predicate I was proving was false for pi-left indices, and true for everything else.04/08 22:56
danbrownright04/08 22:56
dolioBut, to prove predicates over Val, you only need to prove them for the iota-cases.04/08 22:56
dolioWhich is trivial.04/08 22:57
dolioAnd dependent pattern matching actually works for writing the eliminator. :)04/08 22:57
danbrownhmm04/08 22:57
dolioI'm not sure it doesn't work directly. I guess we'll see if it's a bug.04/08 22:58
dolioNot sure *why*, that is.04/08 22:58
danbrownyeah, ok04/08 22:58
dolioIt is somewhat different, though.04/08 22:58
danbrownthose _ at the bottom are of type ⊥, right?04/08 22:59
dolioType top.04/08 22:59
danbrownerr, oh04/08 22:59
danbrownyes04/08 22:59
dolioThe predicate is top for the two iota cases.04/08 22:59
copumpkindanbrown: just out of curiosity, why the accents? :P04/08 22:59
dolioAnd since it's a record, agda fills it in.04/08 22:59
danbrowndolio: right04/08 22:59
dolioI guess the manual way would be 'record{}'04/08 23:00
dolioI never think of that, though.04/08 23:00
danbrowncopumpkin: 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
dolioWhere did I leave off?04/08 23:05
copumpkinmanual way was record{}04/08 23:05
dolioAnyhow, 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
danbrowndolio: thanks, btw04/08 23:05
dolioAnd if the algorithm returns a definite "there are no such terms", the absurd pattern works.04/08 23:05
dolioBut 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
dolioOr, not a term of the relevant type, but a constructor that targets the type.04/08 23:05
copumpkinI guess "no such terms" reduces to SAT04/08 23:07
copumpkinor is it worse than that?04/08 23:07
copumpkinI guess it is04/08 23:08
dolioWell, it might be higher-order unification in general, which is undecidable.04/08 23:08
copumpkinyeah, I see04/08 23:08
dolioThis case doesn't look higher-order, though.04/08 23:08
dolioTo me, anyway. I'm certainly no expert, though.04/08 23:09
doliodanbrown: So, did you find something explaining ITT vs. CoC, or should I still try?04/08 23:18
copumpkindolio: I'd appreciate you trying, if you're still around :)04/08 23:26
dolioWell, for one, the lambda cube languages usually have impredicative polymorphism.04/08 23:27
dolioWhich allows them to encode lots of inductive types using lambdas, but not their strong induction principles.04/08 23:28
dolioThat doesn't matter in System F and stuff, but it matters in the dependently typed corners.04/08 23:28
dolioBy contrast, ITT has lots of direct type formers.04/08 23:29
dolioNatural numbers, finite sets, pi, sigma, W, disjoint union and identity types.04/08 23:30
copumpkinas in, they're primitive?04/08 23:30
dolioThey're all introduced like rules in natural deduction.04/08 23:31
copumpkinah04/08 23:31
dolioAnd I think the usual presentation has judgments describing what things are sets.04/08 23:32
dolioSo, 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
copumpkinyeah04/08 23:33
dolioWhich has none of the universe/sort stuff of the lambda cube type languages.04/08 23:33
dolioBut, at the end, you introduce universes, induction-recursion style.04/08 23:34
dolioSo, 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
dolioAnd you have an eliminator T, such that 'if s is an element of U, then T s is a set'.04/08 23:36
dolioAnd 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
dolioAnd 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
dolioWhich is similar to the direct hierarchies of universes that Agda or Coq use.04/08 23:39
dolioJust presented differently.04/08 23:39
copumpkinwait, what are u0 and t0?04/08 23:40
doliou0 is the name of U0 in U1.04/08 23:40
copumpkinoh ok04/08 23:40
dolioSo u0 : U1, T1 u0 = U004/08 23:40
copumpkinI see, yeah04/08 23:40
dolioAnd t0 s is the name of T0 s in U1.04/08 23:40
dolioI guess T may not be considered an eliminator per-se.04/08 23:42
dolioAnyhow, generalizing that style of definition is how you get induction-recursion.04/08 23:43
dolioIt 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
dolioMore, probably.04/08 23:45
copumpkinso Martin-Loef doesn't have higher universes?04/08 23:46
dolioThe stuff in that short Intuitionistic Type Theory thing doesn't. It only has one U.04/08 23:47
copumpkinah, I see04/08 23:48
dolioBut he had multiple tweaks of the theory over the years.04/08 23:48
soupdragonProgramming in Martin Lof Type Theory has an infinite heirarchy of universe04/08 23:48
dolioAnd I've heard there was one with multiple universes.04/08 23:48
soupdragonsorry that's not the correct title04/08 23:48
copumpkinI've been trying to figure out a minimal set of primitives for a simple DT normalizer I'm writing04/08 23:48
soupdragonConstructive mathematics and computer programming. <-- this  one04/08 23:49
copumpkinah, I'll add that to my reading list04/08 23:49
dolioIn 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
copumpkinah yes04/08 23:49
soupdragonfrustrating all these martin lof papers are out there now04/08 23:50
soupdragonwhen I was obsessed with reading everything there is about type theory none of this stuff was available04/08 23:50
copumpkinaw04/08 23:50
copumpkinis pi, sigma, zero, one, and two sufficient for constructing all non-inductive family types?04/08 23:51
copumpkin(I was reluctant to add two, but couldn't figure out how to do it without it)04/08 23:51
soupdragonI think you need 204/08 23:51
copumpkinyeah04/08 23:51
soupdragonmartin lof gives N (which we call Fin)04/08 23:51
soupdragonN_0 N_1 ..04/08 23:51
copumpkinif I want to use sigma as a non-dependent sum I need two04/08 23:51
copumpkinyeah04/08 23:51
copumpkinI was reluctant to add that cause it seemed like more than was strictly necessary04/08 23:52
copumpkinnow I'm trying to figure out that thesis you pointed me at to see how to add the inductive family stuff04/08 23:52
soupdragonThorstin Alterkirch has some lecture note style document re. some of the basics of peter morris' work04/08 23:53
copumpkinoh, I'll poke around on his site to see if I can find that, thanks04/08 23:54
soupdragonThorsten Altenkirch04/08 23:54
doliocopumpkin: You need W-types for all inductive types, I think.04/08 23:54
soupdragonhttp://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf - but there's other good stuff there too which is related04/08 23:54
copumpkindolio: what would that give me over the sums/products?04/08 23:55
copumpkinoh04/08 23:55
copumpkinI guess I can't really get recursion04/08 23:55
dolioOrdinals, for instance.04/08 23:55
dolioI think you'll have trouble doing ordinals without W-types.04/08 23:55
copumpkinhmm, probably04/08 23:56
copumpkinokay, so I should probably add W04/08 23:56
copumpkinsoupdragon: thanks :)04/08 23:56
--- Day changed Thu Aug 05 2010
dolioW-types and a universe gets you some set theory, too.05/08 00:00
dolioYou represent sets by W U T.05/08 00:00
dolioAnd you can get most all the ways of making a set besides powerset, I think.05/08 00:00
dolioAll the ZF-ways, that is.05/08 00:01
* copumpkin can't remember where he read about W types05/08 00:01
copumpkinmaybe type theory and functional programming05/08 00:01
copumpkinthat book felt like a description of agda05/08 00:01
* Saizan first met them in the OOT paper05/08 00:01
Saizan*OTT05/08 00:01
copumpkinso W, 0, 1, 2, pi, and sigma05/08 00:06
copumpkinis that sufficient for all types?05/08 00:06
soupdragonuh05/08 00:06
soupdragonthat's sufficent for all types you can define with that05/08 00:06
copumpkinwell :P05/08 00:06
soupdragonthe question doesn't make sense as is05/08 00:06
soupdragonif you read Peter Morris' work it classifies types a bit more sharply than just ADT/GADT05/08 00:07
copumpkinokay, I'll keep reading :)05/08 00:07
soupdragonand also maybe have a look at some of the terrifying stuff from Peter Dybjer05/08 00:07
copumpkin:o05/08 00:08
Saizanit sort of leaves out coinductive ones, except that you've pi which is a quite flexible one05/08 00:08
copumpkinoh yeah05/08 00:08
copumpkinI guess I could throw in # and b as defined in Coinduction, but I'll ignore it for now05/08 00:09
soupdragonI can never remember about coinductives05/08 00:10
doliocopumpkin: That's what OTT takes as primitive.05/08 00:10
dolioThe old stuff, at least.05/08 00:13
dolioThe 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
dolioLike, you won't be able to prove induction on the naturals encoded as W-types.05/08 00:15
copumpkinoh05/08 00:15
copumpkin"This reflects the well known fact that the category of finite types is bicartesian closed." of course05/08 00:38
soupdragonusually remarks like that are a hint that you should just give up05/08 00:39
copumpkin:)05/08 00:39
copumpkinI think I actually get it, but it seems weird to remark that offhand05/08 00:39
soupdragonmy favorite one is "as everyone knows,  1 + 2 + 3 + 4 + ... = -1/12"05/08 00:39
copumpkinhmm, I didn't know that ;)05/08 00:40
soupdragon"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
copumpkinhah05/08 00:40
dolio-1/2?05/08 00:40
dolioBicartesian closed means that it has binary sums and products, and exponentials, I believe.05/08 00:42
dolioOr maybe it's all finite sums and products.05/08 00:42
copumpkinI think exponentials too05/08 00:43
dolioAnyhow, convincing yourself of that shouldn't be too hard.05/08 00:43
copumpkinyeah05/08 00:43
dolioYes, I said exponentials. :)05/08 00:43
copumpkinoh, I thought your second thing was contradicting your first, so I was contradicting what I thought you were saying :P05/08 00:44
copumpkin"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
copumpkin"A bicartesian category which is also cartesian closed (but not usually cocartesian closed) is a bicartesian closed category."05/08 00:44
copumpkinaccording to ncatlab05/08 00:44
Saizaniirc if it's both cartesian closed and cocartesian closed it collapses into a category where all objects are isomorphic?05/08 00:46
dolioAh. It's all products, then.05/08 00:46
dolioBicartesian closed doesn't imply coexponentials.05/08 00:46
dolioBut I seem to recall that being the case, yes.05/08 00:47
copumpkinagsy really needs to avoid writing f = f as solutions05/08 00:57
copumpkinit can be pretty helpful sometimes for writing simple stuff though05/08 00:57
copumpkincase splitting seems way buggier than it used to be05/08 01:11
copumpkinsometimes it forgets variables or swaps them05/08 01:11
copumpkinsoupdragon: http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf is wonderful, thanks05/08 01:59
danbrownbtw, does anyone else edit agda code in vim?05/08 05:37
danbrowni made a few improvements to what's on the wiki05/08 05:37
danbrowni should post them at some point...05/08 05:37
copumpkinanyone here played with HOL light?05/08 12:15
soupdragonI spent some time reading the source code but I didn't get a lot out of it05/08 12:16
copumpkinah05/08 12:16
copumpkinone thing I was wondering about in that pdf soupdragon pointed me at yesterday05/08 14:17
copumpkin(http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf)05/08 14:17
copumpkinoh, nevermind05/08 14:18
copumpkin"i.e. enumeration doesn’t work for context-free types because they contain types with an infinite number of elements"05/08 14:18
copumpkinwas 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
dolioWhat page?05/08 14:19
copumpkin2605/08 14:20
copumpkinunder the little table of universes with representative operations05/08 14:20
copumpkin"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
copumpkinI guess that sort of covers it, although it doesn't mention it explicitly for CF types05/08 14:21
dolioWell, 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
copumpkinyeah05/08 14:26
dolioThe stuff about coalgebras is an extension of context free types, though, if I understand correctly.05/08 14:26
copumpkinbut with a context-free language, you can enumerate all strings in it, but of course there may be infinite such strings05/08 14:26
copumpkinI just wasn't sure if the issue was the finiteness or the un-enumerability05/08 14:27
dolioYes, I imagine infinite binary trees would work.05/08 14:27
copumpkinah, cool05/08 14:27
dolioAlthough I just skimmed the paper.05/08 14:27
copumpkinI found it pretty interesting, but you probably already know most of that stuff :)05/08 14:28
dolioEnumerating may be non-trivial, looking.05/08 14:31
dolioFor instance, enumerating List Nat.05/08 14:32
copumpkinhrm05/08 14:33
copumpkinseems like you'd run into the same issue with the grammar form of the same question though05/08 14:34
dolioRoseTree nat would be even worse.05/08 14:34
dolioIt may be possible. Just not easy.05/08 14:34
copumpkinyeah, you'd need something like your zigzag to do it right I think05/08 14:35
dolioWell, if you're committed to a stream, yes.05/08 14:35
copumpkinwhich is in fact why I started trying to port control.monad.omega in the first place05/08 14:35
copumpkinyeah05/08 14:35
copumpkinI guess with a tree it might be harder05/08 14:35
dolioGoing with some type of tree would be more doable.05/08 14:35
copumpkinhmm05/08 14:36
dolioBut you might need infinitely branching trees.05/08 14:36
dolioFor a naive solution, at least.05/08 14:36
dolioAnd I suppose one could question whether that constitutes an enumeration.05/08 14:36
copumpkinisn't the point of omega to traverse infinitely-branching trees?05/08 14:37
dolioYeah. But doing it is extra work.05/08 14:37
copumpkinfair enough05/08 14:37
copumpkinokay, morris' thesis has a nice definition of inductive families too05/08 21:00
copumpkinit's fun to examine all these universes and what extra power they give you05/08 21:00
soupdragonanother 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 theory05/08 21:02
soupdragonbut also they have practical use for generic programming/proofs05/08 21:02
copumpkinwhat would be the benefit of defining them directly?05/08 21:02
soupdragonsay you started with a dependent lambda calculus - how will you add inductive data types to it?05/08 21:03
soupdragonI 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 them05/08 21:04
copumpkinthis stuff is fairly complicated05/08 22:35
copumpkina telescope (at least in these presentations) just looks like a list05/08 22:39
copumpkinor a heterogeneous list, I guess05/08 22:40
copumpkinheterogeneous by a function, if that makes sense05/08 22:40
danbrownso 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
danbrownmust i go prove a bunch of lemmas stating that each pair of constructors are unequal?05/08 22:42
codolioMatch on x.05/08 22:42
danbrowndid05/08 22:42
codolioIt should be absurd.05/08 22:42
copumpkinwon't it take an abusrd pattern?05/08 22:42
copumpkinif they're constructors it should see it05/08 22:42
danbrownah, excellent!05/08 22:43
danbrowni was just forgetting how to use absurd patterns05/08 22:43
danbrowni was expecting it to let me omit the cases entirely, and i got stuck when it insisted that i include them05/08 22:43
codoliocopumpkin: The telescopes in that paper have increasing indices.05/08 22:43
codolioWhich allows later elements to refer to earlier ones.05/08 22:44
copumpkincodolio: hmm, ignoring the typo in here, http://snapplr.com/afdq05/08 22:45
copumpkinhere's the full page, http://snapplr.com/c7x305/08 22:46
dolioOh, these aren't the telescopes from the context free types.\05/08 22:47
copumpkinoh, nope,05/08 22:47
copumpkini05/08 22:47
copumpkinI've moved on to fancier stuff05/08 22:47
copumpkinbut in general, telescopes appear to be listlike, but maintain some additional information in the index05/08 22:47
dolioWell, in this case, each type appears to get a vector of its preceding types.05/08 22:48
copumpkinoh I see. I was looking for T-> to appear in the SPF, but the I-> is enough to give it all the preceding stuff05/08 22:49
dolioLooks that way.05/08 22:49
copumpkininteresting05/08 22:50
copumpkinhm05/08 22:50
copumpkinI haven't quite absorbed this universe yet :P05/08 22:50
copumpkinthe earlier ones are pretty straightforward05/08 22:50
copumpkindanbrown: what are you proving?05/08 22:53
dolioI'm not sure what O and O' are.05/08 22:54
soupdragondanbrown: 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 false05/08 22:54
soupdragondanbrown (this is what justifies whatever pattern matching does )05/08 22:54
danbrownsoupdragon: ok, yeah05/08 22:59
soupdragonit's interesting to see this because f : C -> *05/08 22:59
soupdragonit's a large elimination05/08 22:59
soupdragonthe pattern matching conceals that05/08 22:59
danbrown* = Set?05/08 23:00
soupdragonyes05/08 23:00
soupdragoninfact without large elimination you cannot do this05/08 23:00
danbrownlarge meaning it jumps up a level?05/08 23:00
danbrowncopumpkin: encoding a small-step semantics for a calculus i'm working on05/08 23:01
danbrownturns out that reduction semantics aren't exactly easy in PHOAS...05/08 23:01
danbrownthe denotational semantics should be much, much easier05/08 23:01
* copumpkin has got to reread this section05/08 23:06
dolioReduction in PHOAS is a pain.05/08 23:09
dolioI have an example of it, though.05/08 23:09
dolioOh right, it fails the positivity checker.05/08 23:10
dolioNever mind.05/08 23:10
soupdragonyeah I never figured out how to make PHOAS work for something like system F05/08 23:11
soupdragon(other than the way in the paper, which I don't like)05/08 23:11
dolioYou need impredicativity to encode impredicative terms, I think.05/08 23:11
dolioThe 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
dolioWhich, 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
dolioSo you need a bound variable type that combines everything to do type checking and normalization of dependent types.05/08 23:17
dolioWhich starts to lose some of the "this implementation is obviously correct" properties.05/08 23:18
danbrowndolio: i used your PHOASNorm module to figure out my reduction function :)05/08 23:18
danbrownin Adam Chlipala's papers and book i could only find a relational encoding of reductions, but i wanted a function05/08 23:19
danbrownyour PHOASNorm.norm had the right insight: map a Term (Term v) t to a Term v t05/08 23:20
danbrowndolio: 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 Colist05/08 23:21
danbrowniterating the step function is slightly tricky, though ;)05/08 23:22
benc___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
copumpkinbenc___: the appropriate structure in Algebra05/08 23:28
copumpkinbenc___: but it won't behave like a typeclass05/08 23:28
Saizandanbrown: nice05/08 23:29
--- Day changed Fri Aug 06 2010
liyang(Unsolved metas? In *my* Agda buffer?!?!)06/08 00:50
copumpkinomg hax06/08 00:50
copumpkinI'm really enjoying this thesis06/08 00:51
copumpkin(http://www.cs.nott.ac.uk/~pwm/thesis.pdf)06/08 00:51
dolioYeah, that's a good one.06/08 00:54
copumpkinis there a discussion of parametricity in light of all this "alternate universe" generic programing work?06/08 02:28
soupdragonno06/08 02:28
soupdragonYou should be able to apply the techniques to prove parameticity but I wasn't able to do it myself06/08 02:29
soupdragonoh actually that's because the theory doesn't (didn't) have eta of proof irr.06/08 02:29
dolioThere's work on parametricity for dependent type theories.06/08 02:55
dolioYou wouldn't get very interesting theorems for inductively defined universes in a normal language, though.06/08 02:56
dolioIf 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
Saizanbtw, i wonder how much cayenne is able to erase06/08 03:22
dolioTypes, probably.06/08 03:27
dolioNot sure beyond that.06/08 03:27
dolioI suppose it may be smarter than just that, though.06/08 03:30
soupdragonwait do you mean how much it can erase in theory?06/08 03:31
soupdragonor how much it actually does erase06/08 03:31
dolioI 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
soupdragonI mean theres a lot less it's permitted to erase by General Recursion06/08 03:31
dolioSure.06/08 03:32
Saizani 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-645206/08 03:59
Saizanalso, what's an easy way to make the typechecker loop with --type-in-type?:)06/08 04:00
dolioThat's the idea behind erasure pure type systems.06/08 04:00
dolioAt first you can erase types and type application, but then that leaves behind additional things that are just constant parameters.06/08 04:01
dolioOr, whatever you want to call them. Parameters that aren't used at all in the computation.06/08 04:01
dolioSo you can erase those, too.06/08 04:02
dolioAnd 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
dolioSuch that programs are only well-typed if it's okay to erase all the things you've marked erasable.06/08 04:06
dolioAnd then you can do analysis to turn a normal language into such an annotated language, if you want.06/08 04:07
Saizani don't see why that conflicts with Set : Set though06/08 04:07
dolioIt doesn't.06/08 04:08
dolioThat doesn't cover all types of erasure, though.06/08 04:08
Saizanyeah, but cayenne can't exploit those given by strong normalization anyway06/08 04:09
dolioErasure of proofs, due to irrelevance, despite their making meaningful contributions to the algorithm for instance.06/08 04:09
dolioBut yeah, you can't erase those unless you have strong normalization.06/08 04:10
Saizananyone 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.195306/08 11:02
Saizanfulfilled my own request: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28629#a2862906/08 13:26
copumpkinoh very nice06/08 13:26
copumpkinthat should be on the wiki somewhere :)06/08 13:26
copumpkinexcept I don't think it has enough unicode in it06/08 13:28
copumpkin;)06/08 13:28
Saizanheh, the paper is not very unicodey either06/08 13:30
copumpkinjust kidding :P06/08 13:30
Saizanit doesn't seem like we'd be able to conjure a similar construction in haskell's type system even after (* :: *)06/08 13:32
dolioSaizan: What was the aim? Prove false given Set : Set?06/08 15:05
copumpkinwhat do you guys think of containers?06/08 17:27
soupdragontoo hardcore for me I have NFI what is going on there06/08 17:29
copumpkinthe simple ones seem fairly straightforward06/08 17:44
copumpkin(with one type)06/08 17:44
copumpkinokay, they do get kind of hairy06/08 17:52
copumpkin:P06/08 17:52
copumpkinokay, I get how to encode families without using them06/08 18:44
copumpkinweird, agsy will fill in more than one hole at a time if one hole depends on another06/08 19:41
soupdragonif it didn't do that it would probably produce terms that don't typecheck06/08 19:42
copumpkinit does that sometimes anyway :P06/08 19:43
* copumpkin just devised the most useless datastructure ever06/08 20:21
* copumpkin deletes it06/08 20:24
dolioMost useless ever?06/08 20:27
copumpkinit was an arbitrary-length sigma06/08 20:27
copumpkinI called it SigmaVec06/08 20:27
dolioWell, I don't think that's useless, except it'd probably be a pain to use.06/08 20:28
copumpkinyeah, it was06/08 20:28
copumpkinlots of yellow unless you provided lots of implicits06/08 20:28
dolioNested sigmas having a nice notation is good, though.06/08 20:28
dolioLike { x : A, y : P x, z : Q x y | R x y z }06/08 20:29
copumpkinthat would be nice06/08 20:29
copumpkineven having a binary version of that would be nice06/08 20:30
* copumpkin moves to coq06/08 20:30
dolioOr even \Sig (x : A) (y : P x) (z : Q x y). R x y z06/08 20:30
dolioOr \ex for a logic flavor.06/08 20:31
dolioMultiple notations depending on how you want to think about it.06/08 20:32
soupdragonther was a nice trick with containers proving something about vectors06/08 21:33
soupdragonhttp://cs.nott.ac.uk/~rcp/flops08.pdf06/08 21:34
copumpkinamusing that they represent the naturals as IN with very little space between them :)06/08 21:36
dolioGood ol' tex glyph drawing.06/08 21:39
copumpkinwell \bb{n} doesn't do that06/08 21:40
copumpkinor \mathbb{N} I guess06/08 21:40
dolioThey actually use \mathbb{N} elsewhere in the paper, it looks like.06/08 21:40
copumpkinhah, yeah06/08 21:40
dolioThat'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
dolioOr something of that sort.06/08 21:41
danbrown*frustrated*06/08 21:59
copumpkinhow come?06/08 21:59
danbrowni have "x : π₁ p ≡ ⊥" in my environment, but i get a type error "π₁ p != ⊥"06/08 22:00
danbrownwhat gives?06/08 22:00
copumpkindid you math on the proof?06/08 22:00
copumpkinmatch06/08 22:00
copumpkinor rewrite by it06/08 22:00
copumpkin(which is the same thing)06/08 22:00
danbrownyes—oh crap, should i have matched against the 'refl' constructor?06/08 22:01
danbrowni only named it 'x'06/08 22:01
copumpkinyeah06/08 22:01
danbrown:/06/08 22:01
danbrownof course06/08 22:01
danbrownhrm06/08 22:01
copumpkinor just rewrite (whatever gave you pi1 p = _|_) = refl06/08 22:01
copumpkincause if you match on it manually you may need to refine some other parameters06/08 22:02
danbrownwhen i try to match against refl, the match itself fails with the type error06/08 22:02
danbrownhmm06/08 22:02
danbrowni'll try the rewrite06/08 22:02
danbrownnope, same error06/08 22:03
danbrownwith the rewrite06/08 22:04
danbrownmaybe i need more pattern matching...06/08 22:04
danbrownyeah, i bet that will do it06/08 22:04
copumpkinyou could also use subst manually if necessary06/08 22:05
Saizandolio: in particular the aim was to construct a non-normalizing type term in a way that could be redone in haskell, given Set : Set06/08 22:06
dolioAh.06/08 22:07
danbrownok, more patterns did the trick06/08 22:09
danbrown*frazzled*06/08 22:10
Saizandolio: since in that case we'd show that typechecking haskell + (* :: *) would be undecidable06/08 22:10
dolioOh, right.06/08 22:11
dolioIt rather depends how much evaluation you can get to go on during type checking.06/08 22:15
danbrownactually, proper patterns eliminated some other cruft too. i need to learn to rely on them more06/08 22:15
dolioThey're lifting up all the value-level stuff, as I recall.06/08 22:15
Saizanonly the constructors, but yes06/08 22:16
Saizancopumpkin: http://www.e-pig.org/darcs/Pig09/models/Records.agda <- wrt n-ary sigmas06/08 22:16
dolioIf it's only constructors then I'm not sure.06/08 22:16
dolioYou'd need some sort of computation.06/08 22:17
dolioBut that may be restricted to the point that you can't write the terms required to prove false.06/08 22:18
Saizanyeah, type families are pretty weak, but i'd like to try :)06/08 22:18
copumpkinSaizan: ah, that's not as ugly as mine :)06/08 22:28
danbrownwoah, absurd patterns ftw!06/08 22:28
danbrown:)06/08 22:28
copumpkinyeah!06/08 22:28
copumpkinhttp://snapplr.com/068k do they mean "insist that the domain of 'arr'" instead of codomain?06/08 23:46
Saizani'd think so06/08 23:51
copumpkinso that would mean the domain would be Usp 0 and codomain would be Usp n?06/08 23:51
copumpkinseems like you could simulate it with Usp n -> Usp (suc n) -> Usp (suc n), but the interpretation would be weird06/08 23:52
Saizani haven't read the paper, the argument to Usp is the number of free variables?06/08 23:53
copumpkinyeah06/08 23:53
Saizanso 'arr' : Usp 0 -> Usp n -> Usp n would fit, i don't think Usp n -> Usp (suc n) -> Usp (suc n) is restrictive enough06/08 23:55
copumpkinoh, it isn't06/08 23:55
copumpkinI'm thinking that vars defined on the domain would have to be treated specially06/08 23:56
copumpkinso that the max of the fin is excluded and everything else is mapped06/08 23:57
copumpkinnot sure if I'm making any sense :P06/08 23:57
* Saizan doesn't follow, but feels like he's lacking quite a bit of background06/08 23:58
copumpkinnah, I'm probably just being dumb06/08 23:58
copumpkinI guess I'm also assuming that the type only has one free variable, which isn't always true06/08 23:58
copumpkinokay, I'll go for Usp 0 :P06/08 23:58
--- Day changed Sat Aug 07 2010
copumpkin(I'm trying to avoid using the host language's types)07/08 00:00
Saizanas the last comment says, with Usp 0 you'll probably have to struggle with the termination checker07/08 00:02
Saizan(or the positivity checker?)07/08 00:03
copumpkinpositivity07/08 00:04
copumpkinbut I'm not really planning on writing an element type07/08 00:04
copumpkinnot in agda, anyway07/08 00:04
copumpkin(you only get negative occurrences in the element type)07/08 00:04
Saizanoh, ok07/08 00:06
Saizanwriting a compiler?07/08 00:06
copumpkinwell, I wouldn't say that07/08 00:06
copumpkinplaying with various interpreters :)07/08 00:07
Saizan:)07/08 00:07
copumpkinI guess for the dependent version of that, I can do Usp 0 -> Usp (suc n) -> Usp n07/08 00:11
copumpkinactually, hm07/08 00:12
Saizanyeah, that's what i'd guess too07/08 00:13
Saizanthough maybe it's more complicated than that07/08 00:13
Saizansince the variable introduced there is not necessarily a type07/08 00:14
copumpkin(assuming the Usp contains all the "value-level" stuf too)07/08 00:14
copumpkinsince it would just be "Term", containing all the usual value-level stuff and type-level stuff07/08 00:14
copumpkinI'd probably want to parametrize it by the universe, too07/08 00:14
copumpkindoes that work?07/08 00:15
* copumpkin throws the datatype together to see if it looks right :P07/08 00:16
Saizanmh, maybe you've to keep the vars for mu distinct from the ones for pi..07/08 00:16
copumpkinyeah, I was planning to07/08 00:17
copumpkinor how did you mean?07/08 00:17
Saizanif i were doing a shallow embedding i'd probably write "pi : (s : Usp 0) -> (Elem s -> Usp n) -> Usp n"07/08 00:18
copumpkinbut then it's shallow :P07/08 00:19
Saizanyeah, you'd have to represent "Elem s -> Usp n" with a lambda term of your object language instead, i guess07/08 00:20
Saizans/with a/with the type of a/07/08 00:20
copumpkinhm, I have something, but it leads me to a problem07/08 00:23
copumpkinhmm!07/08 00:23
copumpkinthis would obviously need a separate typechecking phase, http://snapplr.com/vq4s07/08 00:25
copumpkinsorry if it's completely ridiculous :P07/08 00:25
Saizanmh, you can't write the type of id there :)07/08 00:28
copumpkinugh, now I can't stick universes in :P07/08 00:29
copumpkinI guess I sort of could07/08 00:30
copumpkinoh, I see what you mean07/08 00:32
copumpkinhmm07/08 00:32
copumpkinSaizan: http://snapplr.com/r081 :P07/08 00:34
copumpkinthen I also run into the issue of not being able to define heterogeneous-universe sums (or products, going through 2#)07/08 00:35
copumpkinso many problems with my term type :P07/08 00:35
Saizanheh :)07/08 00:36
* copumpkin sighs07/08 00:36
copumpkinI need to think about this harder :P07/08 00:41
copumpkinany good papers out there on implementing dependent types elegantly? :P07/08 00:41
copumpkin(ideally in another DT language)07/08 00:41
dolioThere was something not too long ago about writing compilers in a logical framework or something.07/08 00:58
Saizanall paradoxes seem to live in papers with painful notations07/08 01:39
copumpkinwhich one are you after now?07/08 01:40
soupdragonhaha ttrue07/08 01:40
Saizangirard's one07/08 01:41
Saizantried a paper by coquand and one by hurkens (which might not be the exact same paradox though)07/08 01:41
dolioDoes the Coquand paper work for you?07/08 01:47
dolioMost of the math is all mashed together for me.07/08 01:47
dolioIf it's the one I'm thinking of.07/08 01:47
soupdragontried looking at the coq scripts?07/08 01:48
Saizan"An Analisys of Girard's Paradox" and yeah it has some problems with spacing, still somewhat readable though07/08 01:49
Saizanuh, no, do you have a link for them?07/08 01:50
Saizanhttp://www.lix.polytechnique.fr/coq/stdlib/Coq.Logic.Hurkens.html <- found07/08 01:51
dolioThere's a Hurkens.agda, too.07/08 01:54
Saizanhttp://www.cse.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Hurkens.agda <- nice07/08 01:56
Saizanshould be easier to see what's going on in the paper now :)07/08 01:57
dolioIt'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
Saizansomething i don't grasp is how they say girard's paradox shows the logic is inconsistent without showing a non-normalizing proof term07/08 02:01
dolioNot sure about that. That term definitely isn't normalizing.07/08 02:02
dolioMaybe the point is that you have normalizing proofs of both D and Not D.07/08 02:08
dolioWhich, when combined, gives a non-normalizing proof of bottom, but you can see that it is inconsistent before that.07/08 02:08
dolioFor 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
zachk1http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28687#a28687 agda build error on windows07/08 20:27
zachk1builds fine on ubuntu linux :~(07/08 20:34
--- Day changed Sun Aug 08 2010
copumpkinwhat is the K axiom in type theory? is it related to the K combinator?08/08 00:10
copumpkinit's almost impossible to search for08/08 00:10
soupdragonI would like to say no but I couldn't be certain..08/08 00:12
copumpkinoh, an eliminator08/08 00:12
soupdragonI think J means the normal equality eliminator and K is the one that implies UIT08/08 00:12
soupdragonUIP08/08 00:12
copumpkinseems to be introduced here: http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf08/08 00:13
copumpkingotta love scanned pages08/08 00:13
copumpkinhttp://www.cs.nott.ac.uk/~ctm/goguen.pdf is interesting08/08 00:27
dolioK : (A : Set) (x : A) (P : x == x -> Set) (eq : x == x) -> P refl -> P eq08/08 00:54
copumpkinsort of substitutive proof irrelevance?08/08 00:56
dolioWell, that's essentially an induction axiom for equality proofs.08/08 00:56
dolioInduction on naturals is "all naturals are either 0 or suc n". K is "all proofs of x == x are refl".08/08 00:57
copumpkinoh, fair enough08/08 00:57
dolioThat's not the induction you usually get for equality, though.08/08 00:58
dolioAnd it's called K because the usual eliminator is J for some reason.08/08 01:00
copumpkinah :)08/08 01:00
dolioI guess because identity types are I in Martin-Loef type theory.08/08 01:00
dolioI J K08/08 01:00
soupdragon= -108/08 01:01
copumpkinlol08/08 01:01
copumpkintype-level quaternion08/08 01:01
copumpkinanyone done that yet?08/08 01:01
--- Day changed Mon Aug 09 2010
copumpkindolio: as you mentioned several days ago... .Arrays.absurd x != .Arrays.absurd x of type ⊥ :(09/08 15:14
copumpkinlooks 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 far09/08 15:59
copumpkinthat'll teach me to be lazy and have it fill in obvious terms for me09/08 16:00
copumpkinman, I'm having a lot of trouble on the most trivial of proofs09/08 17:20
copumpkinhttp://snapplr.com/33nc, now trying to prove that toNat on the result of that is always 0 :P09/08 17:21
copumpkinkind of sad09/08 17:22
copumpkinargument order can be a real pain in agda09/08 19:36
doliocopumpkin: Yep. Apparently \() isn't first-class. So it's better to make a single false-elim and use it.09/08 19:57
dolioAlthough, that requires one for each empty type, then.09/08 19:57
copumpkinyeah :/09/08 19:57
copumpkinseems like something that could be fixed in agda itself09/08 19:57
copumpkinunless that leads to other issues?09/08 19:57
dolioNo idea.09/08 19:58
copumpkinI worked around it by passing around the one I was using09/08 19:58
dolioWhere-defined functions are kind of a tough situation in general, and \() is essentially one of those.09/08 19:58
dolioFor 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
dolioBut that doesn't work.09/08 20:01
copumpkinannoying :/09/08 20:14
dolioExtensionality 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
stevanhi 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 agrees10/08 16:09
skiheh, `C-c C-c' generated invalid code for me :)10/08 21:45
ski(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
copumpkinyeah, it does that a lot :P10/08 21:48
copumpkinI think there's an open bug for it10/08 21:48
skihm, 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
skiis this intended behaviour ?10/08 21:50
skii know Agda1 (using Alfa) would refine the type for me, when i refined things that determined (parts of) the type10/08 21:51
ski(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
stevandifferent types can have the same constructor names, so i guess that's why the signature goal can't be determined.10/08 21:54
skiyeah, but that would only apply when the body type was ambiguous, no ?10/08 21:55
stevanyeah, i guess10/08 21:57
ski.. hm, would naming a variable `n_\==_Succ_m' be horrible abuse of mixfix notation ?10/08 22:04
dolioThere are other situations outside of signature vs. definition that it could do such refinement, but it doesn't.10/08 22:08
dolioLike foo : (A : Set) (x : A) ...10/08 22:08
skiyeah, that reminds me .. if i have10/08 22:09
dolioIf 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
dolioYou'll have to do it manually, even if just with _10/08 22:09
ski  foo {A : Set} {n : \bn} {v : Vector A n} -> ...10/08 22:09
skithen if i write `foo {v}' i want that to mean `foo {_} {_} {v}', not `foo {v} {_} {_}'10/08 22:10
stevanfoo {v = v}10/08 22:10
skii.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 arguments10/08 22:11
* ski is not sure whether he likes that ..10/08 22:12
dolioWould foo {x} {y} be foo {_} {x} {y}?10/08 22:15
skiyeah ..10/08 22:20
skithough 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 arrows10/08 22:21
ski(like how e.g. `foldr' in Haskell sometimes can take more than three arguments)10/08 22:21
dolioYeah, that's an issue.10/08 22:23
--- Day changed Wed Aug 11 2010
skihm .. 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
copumpkinI'd love that, but is it possible in general?11/08 02:55
ski.. that's why i'm asking :)11/08 02:57
dolioSome sort of command for with-introduction would interest me.11/08 02:57
dolioI'm not even sure it doesn't exist, though. :)11/08 02:58
skihm, strange ..11/08 08:40
Saizan?11/08 08:41
skii have basically (simplifying)11/08 08:42
ski  data Foo (n : \bn) : Set11/08 08:42
ski    where11/08 08:42
ski    Foo0 : Foo n11/08 08:42
ski    ...11/08 08:42
skinow, i expect that11/08 08:42
ski  Foo0 : {n : \bn} -> Foo n11/08 08:43
skiand if i write `Foo0' in an expression, sure, i can write `Foo0 {n}' instead11/08 08:43
Saizanah, yeah, parameters don't appear in patterns11/08 08:43
skihowever, when i try to write `Foo0 {n}' in a pattern, i get a complaint that the `Foo0' constructor expects 0 arguments11/08 08:43
skiit just seems a bit inconsistent to me11/08 08:44
ski(maybe there's some real reason, but i don't know it)11/08 08:44
Saizanit helps keeping them cleaner though, if you have other implicits11/08 08:44
skii was just expecting them to behave the same way in patterns as in expressions11/08 08:45
ski.. 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
Saizani wonder if it's just a matter of convenience, or it's something more fundamental about pattern matching11/08 08:49
ski  Panic: Right hand side must be a single hole when making case.11/08 09:51
ski  Panic: unbound variable n11/08 09:56
ski  when checking that the expression n has type \bn11/08 09:56
copumpkinski: I reported the single hole one recently, but haven't seen the other one11/08 13:10
ski(copumpkin : you saw <http://wiki.portal.chalmers.se/cse/pmwiki.php/CS/QuantifierEliminationAndFunctionalProgramming> ?)11/08 13:33
copumpkinyep, although I'm still half asleep so haven't really looked that closely :)11/08 13:33
skiin 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 panic11/08 13:33
ski(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
copumpkinah11/08 13:35
stevanski: copumpkin , regarding that quantifier elimination stuff: http://web.student.chalmers.se/~stevan/csallp/html/README.html11/08 15:34
copumpkinooh11/08 15:35
skinice11/08 15:40
stevani 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
ski.. bah, i want to write11/08 16:11
ski  Succ .mn \frob Succ .mn | \iotal (\==Refl {\bn} {mn}) = ?11/08 16:12
skibut since i apparently can't name the type parameter arguments for the constructor in patterns, i must break the symmetry and either write11/08 16:13
ski  Succ .mn \frob Succ mn | \iotal \==Refl = ?11/08 16:13
skior11/08 16:13
ski  Succ mn \frob Succ .mn | \iotal \==Refl = ?11/08 16:13
ski:(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
Saizanno patterns in lambdas11/08 16:29
skihm .. it didn't complain .. but i suppose it happily shadowed the identifier, then11/08 16:31
Saizani think so11/08 16:31
* ski works around by passing `irrefl m n m\==nn' (defined in a `where') to `\iotar' instead11/08 16:32
ski(since i don't think i could use `with' in this situation)11/08 16:32
Saizan"no patterns" was too strong btw, you can have absurd ones11/08 16:34
skiah, ty11/08 16:35
skihm, so `\ ()' ?11/08 16:44
Saizanyep11/08 16:45
copumpkin(with no arrow)11/08 16:45
skihm .. parse error11/08 16:46
ski  Panic: no such interaction point: ?411/08 18:29
copumpkinyou filled in a hole but didn't reload? or something like that11/08 18:31
copumpkinI've had that when tinkering with holes behind its back11/08 18:31
danbrownwhat is "Cannot split on the constructor foo"?11/08 18:43
danbrowni'm trying to define a function by pattern matching that specializes the type indexes of its input11/08 18:44
danbrownand the constructor 'foo' computes one of its indexes, unlike the rest of the constructors which just specify constants11/08 18:45
danbrownhere's a boiled-down example: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2883311/08 19:11
danbrownoops. updated: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a2883411/08 19:13
skicopumpkin : yeah, i think so11/08 20:05
ski(just sharing the assorted panics i encounter ;)11/08 20:05
copumpkincheck the bugtracker, too11/08 20:05
skibtw, it's irritating when you want to comment out holes, or delete them, or copy them11/08 20:06
skii usually end up having to `C-c C-x C-d', fiddle some, `C-c C-x C-l'11/08 20:07
skidanbrown : 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, though11/08 20:15
danbrownski: cyclic unification isn't the problem... http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a2884911/08 22:54
danbrownit appears i'm confusing the type checker by asking it to reason about the image of a function11/08 22:55
dolioYes. The problem with 'X a a' is that 'a' is essentially fixed, and not a variable open to refinement.11/08 22:59
dolioPattern 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
danbrowndolio: so are you saying that pattern matching basically doesn't work on datatypes with computed indices?11/08 23:45
danbrownassuming i stick with computed indices, do i need to use eliminators instead of patterns, or is there another technique?11/08 23:46
copumpkinI thought it did, if you brought those computed indices into scope with a `with` block11/08 23:47
copumpkinand used the appropriate dotting11/08 23:47
--- Day changed Thu Aug 12 2010
danbrownhrm, or maybe i would still need pattern matching to define the eliminator...12/08 00:08
copumpkincan I see?12/08 00:09
copumpkinoh, it's that example you gave earlier?12/08 00:10
danbrowncopumpkin: ya12/08 00:15
copumpkindanbrown: what did you intend to write in that function?12/08 00:23
copumpkinjust out of curiosity :)12/08 00:24
danbrownthat function in particular?—nothing :P12/08 00:24
danbrownthis was a contorted example distilled out of something else i'm working on12/08 00:24
danbrownwhich is a bit too large for an irc hpaste ;)12/08 00:25
danbrowni'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 constructor12/08 00:25
danbrownfor example, i want a constructor like "reflect : ∀ {t : Type} {e : Effect} → Fun (T e t ⟶  t / e)", where T : Effect → Type → Type12/08 00:28
danbrownbut 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
copumpkinah :/12/08 00:31
dolioIt works on datatypes with computed indices, just not the way that you're doing it.12/08 00:39
dolioIf 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
dolioBut if you know that 'x : Foo true', you cannot match on x and refine true to 'not false'.12/08 00:41
dolioAnd, 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
dolioOr, inserting another variable, it's trying to refine a to both 'b' and 'o . b', and that doesn't work.12/08 00:46
dolioAttempting 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
danbrownok12/08 00:51
dolioNote that your f function works fine, because it refines 'b' into 'o . a'.12/08 00:51
danbrownso it sounds like i should redesign my "Fun (⊤ ⟶ t) → X" function to a "Fun (s ⟶ t) → X" function that projects away the unwanted inputs12/08 00:52
danbrownright12/08 00:52
danbrownand then i'll have room to refine 's'12/08 00:52
danbrownfor reference, here's a workaround using what i think is the proper eliminator: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28833#a2885812/08 01:00
soupdragondata X : Bool → Bool → Set where12/08 01:01
soupdragon  eh : ∀ a b → X a b12/08 01:01
soupdragon  eq : ∀ a   → X a a12/08 01:01
soupdragon  op : ∀ a o → X a (o ∙ a)12/08 01:01
soupdragonthis type is necessary ?12/08 01:02
danbrownsoupdragon: no :P12/08 01:02
danbrowncontrived example12/08 01:03
soupdragonwhat's the real case?12/08 01:03
danbrownrather 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 τ / e12/08 01:07
danbrownso 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
danbrownthe functor action "Tτ" i represent as a function like "_•_ : Mon → Type → Type"12/08 01:12
danbrownthe 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
danbrownsolved my problem (earlier) by abstracting over equality12/08 02:59
danbrownsprinkles some refls about, but it at least lets me get on with things12/08 03:00
pedagandusing 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
copumpkinI think you are forced to write one yourself, unless you want to use Lift from Level12/08 15:03
pedagandis there any reason for not defining "record ⊤ {a} : Set a where ..."?12/08 15:08
pedagandI 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
copumpkinmaking it polymorphic would probably just give you more yellow in places it wasn't yellow before12/08 15:16
copumpkinbut I don't think it'll actually break anything?12/08 15:16
* copumpkin is no expert though12/08 15:16
pedagandI 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
pedagandall right, now I need Nat in Set1. It is time for --set-in-set. :-)12/08 15:22
Saizanmaybe you could be more universe polymorphic in your code?12/08 15:23
pedagandbut 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 instance12/08 15:28
Saizani meant that maybe the place where you're passing top or Nat might be made more permissive in the universe levels it accepts12/08 15:32
Saizanthough that probably leads to a lot of Level paramaters12/08 15:32
pedagandha, 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
Saizanah, fair enough :)12/08 15:39
--- Day changed Fri Aug 13 2010
molerispedagand: Your email client mangled the unicode in ILabel.agda ))):13/08 11:08
npouillardI think I found a bug in Agda. The test case is really short. Can anyone confirm that this should type check http://pastebin.com/KL3yfBV313/08 15:04
Saizanwhat is E' ?13/08 15:15
npouillardA copy of E13/08 15:17
npouillardsorry I minimized the example afterwards13/08 15:17
Saizanweird, here (A : E true) → A is the only one that won't typecheck13/08 15:21
Saizani'm using the darcs version though13/08 15:21
npouillardsame here13/08 15:21
Saizananyhow, that seems to support the idea that the commented ones should in fact work13/08 15:22
npouillardYep but in a more complex example it does make a difference13/08 15:22
npouillardAnd if it is a bug it ought to be fixed13/08 15:22
Saizanah, so your problem is that "(A : E true) → A" doesn't typecheck? the comment in the paste seems to say the opposite to me13/08 15:24
npouillard... sorry13/08 15:26
npouillardhttp://pastebin.com/pPaAnLpc <= updated version13/08 15:28
Saizananyhow, 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
npouillardSaizan: this seems to be related to whether or not the term can be reduced13/08 15:30
Saizanyeah, it won't reduce "E true" while typechecking E13/08 15:30
Saizanwhich kind of makes sense, since it hasn't yet decided if it'd terminate, i presume13/08 15:32
npouillardYep but using only the type of it should work no?13/08 15:34
npouillardE true is of type Set₁ and so A is of type Set13/08 15:35
Saizanno, consider data B : Set1 where ...13/08 15:43
Saizanand "E true = B"13/08 15:43
npouillardSaizan: yes while saying it I understood the issue13/08 16:10
--- Day changed Sun Aug 15 2010
Saizanshouldn't we introduce sigfpe to Agda? his posts should get clearer, to those who know it at least :)15/08 09:28
Saizangiven that he seems to always work with the semiring of types maybe epigram would be more appropriate, actually15/08 09:29
pedagandSaizan, don't act as if epigram existed, that just makes reality unnecessarily painful :-)15/08 10:34
Saizanpedagand: heh, "if it existed" was implicit :)15/08 11:02
pedagand:-)15/08 11:06
Saizanhttp://blog.sigfpe.com/2010/08/constraining-types-with-regular.html <- Hom is quite similar to desc :)15/08 11:09
pedagandit's a grammar for functors on Set, isn't it? (hopefully, I'll read the post more carefully later)15/08 11:13
Saizanyeah15/08 11:13
Saizanthough they are interpreted as matrices :)15/08 11:15
danbrown*baffled*15/08 19:48
danbrownanyone have any idea what might be going on here? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a2908515/08 19:48
danbrownin particular, in the "Have" it appears to be flipping the order of the two arguments to _﹔_15/08 19:48
copumpkinI've had a similar error15/08 19:49
danbrownas a result of unifying b with itself15/08 19:49
copumpkinI submitted a report and nobody has a clue, it seems15/08 19:49
danbrown:/15/08 19:49
copumpkinit's just printing the context/goal wrong, I think15/08 19:49
copumpkinnot sure how something like that could happen15/08 19:49
danbrownbut it's not just printing—it won't typecheck15/08 19:50
copumpkinoh15/08 19:50
copumpkinmaybe 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 it15/08 19:50
danbrownah15/08 19:50
danbrownvery frustrating15/08 19:51
danbrownand i can't figure out which knob to twiddle to set it straight15/08 19:52
copumpkindefinitely submit a bug report if you can trim it down to something manageable15/08 19:52
copumpkinI'm sure having another example from my ugly one will help them15/08 19:52
danbrownyeah...15/08 19:52
danbrownugh15/08 19:53
danbrownthe more i code the harder it is to trim down these bug examples15/08 19:53
copumpkinyeah, mine was pretty large too15/08 19:53
danbrowncopumpkin: which issue #?15/08 19:55
copumpkinhttp://code.google.com/p/agda/issues/detail?id=29015/08 19:55
danbrownisolated: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a2909115/08 20:36
Saizanit seems only a prettyprinting bug, since it behaves as i'd expect15/08 20:51
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=29085#a2909315/08 20:52
danbrownbut why do f and g fail to typecheck?15/08 20:57
danbrownerr, ok, f _should_ fail15/08 20:57
danbrownbut g should pass15/08 20:58
danbrownf is bogus15/08 20:58
Saizanyour g you mean?15/08 21:09
danbrownyeah15/08 21:09
danbrownbtw, thanks for the workaround15/08 21:09
danbrowni don't understand why matching on "with b ≟ b | F ∙ G" is necessary15/08 21:10
danbrown(would have never thought to try it)15/08 21:10
Saizanbecause the definition of ﹔ does the same pattern matching15/08 21:12
Saizanso it's not clear what it reduces to until you do the same15/08 21:12
Saizananother way is to perform case analisys on b, so that b ≟ b itself can reduce15/08 21:13
Saizanthis is what the "| .b ≟ .b" in the goal says15/08 21:14
danbrownthat it's unresolved?15/08 21:14
Saizan"x | y" in a goal in general means that you've to make y rewrite to a normal form before x can reduce further15/08 21:16
danbrownok, that makes sense15/08 21:17
Saizanerr, not normal form, but it has to have a constructor at least, it depends on how strict x is in the end15/08 21:17
danbrownok15/08 21:17
danbrownbut why is matching on "F ∙ G" necessary?15/08 21:17
Saizanbecause the  b ≟ b appears in the type of "F ∙ G", and it wouldn't get rewritten if we didn't do that15/08 21:18
danbrownyou mean the type of "F ∙ G" only gets rewritten because we match on "F ∙ G" along with "b ≟ b"?15/08 21:20
Saizanyeah15/08 21:20
danbrownok, this is helpful. thanks15/08 21:21
danbrownnow i'm unstuck again :)15/08 21:21
Saizannp :)15/08 21:21
danbrown(reported: http://code.google.com/p/agda/issues/detail?id=295)15/08 21:25
--- Day changed Mon Aug 16 2010
copumpkinseems like flip in agda (or any dependently typed language) can't be as generic as we might like it to be16/08 02:53
soupdragonflip : (a -> b -> c) -> (b -> a -> c)16/08 02:54
soupdragon?16/08 02:54
copumpkinwell, the full dependent function version16/08 02:54
dolio((x : A) -> (y : B) -> C x y) -> (y : B) -> (x : A) -> C x y16/08 02:54
copumpkindolio: yeah, but what if (y : B x)?16/08 02:54
soupdragonthen yyou can't flip it16/08 02:55
copumpkinseems restrictive :P not that I have an application16/08 02:55
soupdragonwhy is that restrictive16/08 02:55
soupdragonwhat about ((x:A)(y:B x)C x y) -> ((y:(x:A), B x)(x:A)C x y)16/08 02:55
copumpkinit'd need a proof that they're equal, too, wouldn't it?16/08 02:57
copumpkinanyway, utterly pointless16/08 03:03
copumpkinjust seemed like a curious asymmetry with non-dependent functions16/08 03:03
dolioIt seems straight-forward to me that if you're considering flipping the arguments, the second cannot depend on the first.16/08 03:03
dolioIn a sense, the second determines the first.16/08 03:04
copumpkinsure, but normally you consider (a -> b -> c) <=> ((a, b) -> c), and (a, b) <=> (b, a)16/08 03:04
copumpkin(in non-dependent land)16/08 03:04
copumpkinbut yeah, I definitely see why it can't work here16/08 03:04
* copumpkin shrugs16/08 03:06
dolioYou can't swap pairs, either.16/08 03:06
copumpkinyeah, I know16/08 03:06
dolioOf course.16/08 03:06
soupdragonflip =16/08 03:07
soupdragonfun (A : Type) (B : A -> Type) (C : forall x : A, B x -> Type)16/08 03:07
soupdragon  (X : forall (x : A) (y : B x), C x y) (y' : forall x : A, B x)16/08 03:07
soupdragon  (x : A) => X x (y' x)16/08 03:07
soupdragon     : forall (A : Type) (B : A -> Type) (C : forall x : A, B x -> Type),16/08 03:07
soupdragon       (forall (x : A) (y : B x), C x y) ->16/08 03:07
soupdragon       forall (y' : forall x : A, B x) (x : A), C x (y' x)16/08 03:07
--- Day changed Wed Aug 18 2010
copumpkinI guess there's no way to simulate substructural types with dependent types18/08 00:30
dolioNot that I know of.18/08 01:00
dolioNor modal types, really.18/08 01:01
dolioBarring writing a DSL.18/08 01:01
dolioOr, EL, maybe. I'm not sure those qualify as "domain specific".18/08 01:04
doliohttp://code.haskell.org/~dolio/agda-share/html/ParamInduction.html yow!18/08 08:12
Saizancool18/08 08:49
jonrafkinddoes ++ mean cons or append?18/08 19:05
copumpkinappend, usually18/08 19:07
copumpkindepends where though :)18/08 19:07
jonrafkindok. 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
copumpkinwell, 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 :P18/08 19:09
jonrafkindok cool, Data.List has it18/08 19:10
copumpkinyeah, Data.Vec does too18/08 19:15
benc___is there a nice way to find which standard library file somethign is defined in?18/08 21:59
benc___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.Integer18/08 22:00
TheOnionKnightIIRC 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
benc___if only i had more than one mouse button18/08 22:09
dantenhttp://wiki.portal.chalmers.se/agda/agda.php?n=Docs.EmacsModeKeyCombinations <- M-.Go to the definition of the identifier under point18/08 22:10
benc___meta dot18/08 22:12
benc___ok18/08 22:12
benc___cool18/08 22:12
--- Day changed Thu Aug 19 2010
dolioBoy, induction for sum types using free theorems is proving much harder than other stuff.19/08 01:42
copumpkinwhat does that look like?19/08 01:44
dolioWhich?19/08 01:49
copumpkininduction for sum types using free theorems? what do you mean by that19/08 01:50
doliohttp://code.haskell.org/~dolio/agda-share/ParamInduction.agda19/08 01:50
doliohttp://code.haskell.org/~dolio/agda-share/html/ParamInduction.html19/08 01:51
dolioThe latter only has it for empty, unit and product.19/08 01:51
dolioI've been looking at bool, sum and sigma, but I can't figure them out.19/08 01:51
dolioOf course, I don't actually know that the free theorem is enough.19/08 01:56
dolioMaybe you need the general parametricity result.19/08 01:56
dolioOr maybe it's just impossible.19/08 01:56
copumpkinyikes indeed19/08 02:06
dolioBwahahaha! I've done it!19/08 03:53
dolioFull parametricity for the win.19/08 03:54
copumpkin:O19/08 03:54
dolioInduction for booleans proved.19/08 04:09
copumpkindolio: is the Nat induction particularly hard?19/08 05:17
dolioI haven't seriously tried it yet.19/08 05:20
dolioI thought about a while back, but then decided it'd be better to figure out booleans before naturals.19/08 05:20
copumpkinah ok19/08 05:21
dolioNow I'm trying binary sums.19/08 05:21
dolioWhich I think requires using existentials, like booleans require sums.19/08 05:22
copumpkinthis is kind of interesting19/08 05:22
dolioI'm not sure I'll be able to make the existentials into strong sums, though.19/08 05:22
copumpkinwhat got you started on it?19/08 05:22
dolioI saw Neel Krishnaswami mention that it was possible a while back, so it's been on my to-do list.19/08 05:23
copumpkincool19/08 05:27
dolioThe idea goes something like...19/08 05:30
dolioSystem F is cool, because you can encode inductive types in it.19/08 05:31
dolioBut, CoC is less cool, because the inductive types you can encode don't have strong induction principles.19/08 05:32
soupdragonis CIC cool? :)19/08 05:33
dolioHowever, if you add parametricity axioms to CoC, you can prove the strong induction principles.19/08 05:33
dolioCIC isn't a pure lambda calculus.19/08 05:34
dolioThe aim is to get everything that CIC provides out of an impredicative lambda calculus.19/08 05:35
dolioMore or less.19/08 05:35
dolioOf course, that's arguably because CIC is cool, since it has strong induction principles, which are nice.19/08 05:37
dolioSums proved.19/08 06:33
pedagandis there a way get the (in Tex notation) "\not\ni" symbol with the unicode input?19/08 15:36
pedagandha, got it! it's "\nin"19/08 15:37
copumpkinah, I was going to ask what \ni was19/08 15:37
* copumpkin never used that one before :)19/08 15:39
pedagandit's the mirror image of "\in"19/08 15:39
copumpkinyeah19/08 15:39
pumpkinanyone know how one might approach proving something is undecidable?19/08 23:30
pumpkinI guess it would depend on the something :)19/08 23:31
Saizani think you either have to do it in the meta-logic or by reducing it to something else that's known to be undecidable19/08 23:43
Saizanbut i'm mostly guessing19/08 23:43
--- Day changed Fri Aug 20 2010
copumpkinanyone get an error compiling the latest agda?20/08 02:44
copumpkin"The last statement in a 'do' construct must be an expression" in src/full/Agda/Auto/Convert.hs20/08 02:45
copumpkinhmm, I guess it was just me20/08 03:04
copumpkinseems to be working now :o20/08 03:04
dolioI'm generally impressed that pulling at random gets you something that compiles and works.20/08 03:04
copumpkinyeah, same20/08 03:04
copumpkinnot sure how this file got messed up20/08 03:04
copumpkin(on my side)20/08 03:05
copumpkinmaybe my hard drive is dying20/08 03:05
dolioIncidentally, I now have sigma with both projections. I figured out what my problem was.20/08 03:05
copumpkinooh, same url?20/08 03:05
dolioYes.20/08 03:05
dolioWhen I was defining pi0 with curry, I forgot that the postulates would prevent pi0 (x, w) from computing to x.20/08 03:06
dolioSo when you go to define pi1, you have a proof obligation.20/08 03:06
dolioSo I switched to the easy pi0.20/08 03:06
dolioThat means that pi1 doesn't compute properly, either, but proving that pi1 (x, w) = w is a huge pain.20/08 03:07
copumpkinoh, I see now20/08 03:12
copumpkinhmm, no, I still get the same issue, weird20/08 03:14
copumpkinhttp://snapplr.com/3k9020/08 03:14
copumpkinoh that must be when generating documentation20/08 03:17
copumpkinI wonder how I managed to break my agda without doing anything20/08 19:22
dolioIt broke without even a darcs pull?20/08 19:23
copumpkinoh, that error is just a haddock one cause they have a comment that accidentally looks like haddock20/08 19:23
copumpkinbut more seriously, agda just doesn't work anymore, and it's a haskell error20/08 19:23
copumpkinsomething about package dependencies no longer being satisfied, let me look20/08 19:24
copumpkinhttp://snapplr.com/hbrx , any ideas?20/08 19:25
copumpkinmaybe I should just ask in #haskell actually20/08 19:25
Saizancopumpkin: what if you start ghci with -package-id Agda-2.2.7-<hashican'tcopyfromtheimage> ?20/08 19:36
copumpkinsame error20/08 19:36
Saizanghc-pkg check?20/08 19:37
copumpkinno output, I assume that's good?20/08 19:37
Saizanyeah20/08 19:38
copumpkinseems like it has something to do with random?20/08 19:38
copumpkinall of them eventually boil down to package random-1.0.0.2-f4208c3677aeaaaf41e4d36309c0b4ff is shadowed by package random-1.0.0.2-3f4f79037f4383d8a3872916cdac8d3f20/08 19:39
copumpkinI have random-1.0.0.2 in both user and system folders20/08 19:40
Saizanstarting ghci with "-package-id Agda-2.2.7-378254d26ce5307092318870fe9b05db" should direct the shadowing to pick the other random20/08 19:40
copumpkinmaybe that's it? I've never explicitly installed random though20/08 19:40
Saizanbut i guess you could also try -package-id random-1.0.0.2-3f4f79037f4383d8a3872916cdac8d3f20/08 19:41
Saizan(if you only have one random-1.0.0.2 shadowing won't be needed, of course)20/08 19:41
copumpkinoh I think I see what's wrong20/08 19:42
copumpkinf4208c3677aeaaaf41e4d36309c0b4ff is the version of random that haskell98 wants20/08 19:42
copumpkinbut pandoc wants the other hash for random20/08 19:42
copumpkinnot sure why pandoc is even relevant for agda though20/08 19:43
copumpkinit complains about hakyll, strangely enough20/08 19:43
copumpkinhttp://pastie.org/private/xbkegoyoph4ncfvmyi0p9q20/08 19:43
copumpkinI'll just kill my user random and hakyll20/08 19:43
Saizanno, wait20/08 19:44
copumpkinwhoops :)20/08 19:44
copumpkinanyway, it still doesn't work20/08 19:44
Saizanyou used -package instead of -package-id20/08 19:44
Saizanfor Agda.20/08 19:45
copumpkinugh20/08 19:45
copumpkinworks now :P20/08 19:45
copumpkinbut agda-mode is using -package20/08 19:45
Saizanyou could put -package-id ... in the .ghci file i guess, or remove the unwanted random..20/08 19:47
copumpkinthe unwanted random is gone, but now it just says agda is unusable, and -v gives no information20/08 19:48
Saizanare you sure you removed the right one?:)20/08 19:49
Saizananyhow, if ghc-pkg check is silent there should be a way to make it work.20/08 19:50
copumpkinoh, maybe I should recompile agda now that I only have one random again20/08 19:51
copumpkinmaybe it got messed up since I tried to build it with the other random there20/08 19:51
copumpkinI did delete the right one :P20/08 19:51
copumpkinwhat the hell :P rebuilding agda reinstalls another user random20/08 19:52
copumpkingah20/08 19:53
copumpkinit's rebuilding haskell98 and all sorts of stuff I already have installed with the platform at the system level20/08 19:53
Saizandid you upgrade "time"?20/08 19:54
Saizanor "old-locale"?20/08 19:54
Saizanthose are the non-base transitive deps of random.20/08 19:54
copumpkinI've never explicitly upgraded anything20/08 19:54
Saizanmaybe some package you installed required a newer version.20/08 19:55
copumpkinbut I do seem to have new time in the user  folder20/08 19:55
Saizanok, so that's why you also get an user random :)20/08 19:55
Saizanwith the difference that there's no new version of random, so you get the same version but built against the new time20/08 19:56
copumpkinah20/08 19:56
copumpkinlooks like it might be doing the right thing now20/08 19:57
Saizanbtw, in later ghcs shadowing prefers user packages, which would have make -package Agda-2.2.7 just work in this case20/08 19:58
copumpkinyay, it works20/08 20:04
copumpkinthanks for all the help :)20/08 20:07
Saizannp20/08 20:12
copumpkinI vaguely remember a NBE module by pigworker in agda20/08 23:12
copumpkinanyone know where that is?20/08 23:12
copumpkinoh, nice: http://web.student.chalmers.se/~stevan/ctfp/html/README.html20/08 23:17
copumpkinone 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<Structure> which contains the operations but no laws20/08 23:24
copumpkinwhat's the point of that?20/08 23:24
Saizanwell sort of the same point of the Monad class in haskell i guess.. also some laws might require extensionality for some monads20/08 23:29
copumpkinwhy not just postulate extensionality where needed and avoid duplicating definitions?20/08 23:31
copumpkinwell what do you mean the same point as the Monad class?20/08 23:31
Saizanthat you can write e.g. mapM that's polymorphic over the RawMonad, it doesn't use the laws20/08 23:32
Saizanmaybe there are other design problems on how to add the laws too? e.g. setoids or not20/08 23:41
Saizanwe should ask the authors :)20/08 23:41
--- Day changed Sat Aug 21 2010
doliocopumpkin: Also, I think there are parallel hierarchies.21/08 00:47
copumpkin?21/08 00:48
dolioRawFoo contains the minimal operations for a Foo.21/08 00:48
dolioIsFoo is a proof that those minimal operations follow the right laws to be a Foo.21/08 00:48
copumpkinah yeah21/08 00:48
dolioAnd IsFoo contains IsBar, for all the relevant substructures.21/08 00:48
dolioThen, a Foo is a pair of the minimal operations, and the proof that the operations satisfy the laws.21/08 00:49
dolioOr, perhaps the record itself doesn't contain it, but the module for IsFoo does.21/08 00:49
dolioIf I remember correctly.21/08 00:49
dolioConceivably, you could use the IsFoo records independently.21/08 00:51
dolioHave a function that accepts a bunch of arguments, and an IsFoo argument for those arguments combined into a structure.21/08 00:52
dolioAlthough, I don't know why you'd do that.21/08 00:52
copumpkinwhat issues would I encounter if I postulated extensional equality?21/08 20:13
soupdragonany proofs that need to compute on a proof which uses it wont reduce ..21/08 20:23
soupdragonsometimes that doesn't even matter, but it can be a problem21/08 20:23
copumpkinit seems like for refl it would be less of a problem21/08 20:23
copumpkinbut maybe I'm oversimplifying thing21/08 20:24
copumpkins21/08 20:24
copumpkinoh I guess computing _on_ proofs21/08 20:26
copumpkinthat's what you said, I just misunderstood21/08 20:26
copumpkinhow about "passing it in" to functions that use it? seems like you could push the need for extensionality out each time21/08 20:27
soupdragonit's the same as a hypothetical proof21/08 20:51
ccasincopumpkin: 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
ccasinbut if you're just writing proofs and don't need to compute with them, it's no big deal21/08 21:37
soupdragonyeah but the thing is,21/08 21:39
soupdragonyou write 30 pages of proofs and it all works fine21/08 21:39
soupdragonbut then you want to use your theory to justify the termination of a function.....21/08 21:39
soupdragonbasically you get lucky, or don't. at that stadge21/08 21:40
doliocopumpkin: Same problem as I ran into with pi0 and pi1 for the sigmas defined with Church encoding and parametricity.21/08 22:07
dolioInstead 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
copumpkin****ing universe polymorphism21/08 23:14
copumpkin  homomorphism : ∀ {X Y Z : Set o} → (f : X → Y) → (g : Y → Z) → (x : Maybe X) → _ ≡ _21/08 23:17
copumpkinfeels kind of dirty, somehow21/08 23:17
--- Day changed Sun Aug 22 2010
doliocopumpkin: That signature isn't yellow?22/08 01:00
copumpkinnope :D22/08 01:03
dolioI don't believe you.22/08 01:04
copumpkin:(22/08 01:05
copumpkin(it's in a where block)22/08 01:05
copumpkinhttp://snapplr.com/2g4q22/08 01:06
dolioIs _==_ not the usual _==_?22/08 01:06
copumpkinit is the usual one :)22/08 01:07
dolioOh. I guess it must figure out what the _s are from the type from the record.22/08 01:07
dolioThat's fairly impressive.22/08 01:07
copumpkinI figured it was doing it because of how I was using it22/08 01:08
copumpkinisn't that related to the miller unification pigworker was talking about?22/08 01:08
* copumpkin knows nothing22/08 01:08
copumpkinbut then again, he was talking about it being unimplemented in agda22/08 01:08
dolioI don't really know anything about Miller unification.22/08 01:08
dolioAnd 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
copumpkinbut yeah, as far as I can tell, my usage of homomorphism there is the only thing specifying the _ == _ and preventing it from being yellow22/08 01:09
copumpkinif I remove the call to it, it turns yellow22/08 01:10
dolioOh, maybe there are short papers on it.22/08 01:10
dolioUnification of Simply Typed Lambda-Terms as Logic Programming is probably related.22/08 01:14
dolioOf course, Agda isn't simply typed.22/08 01:16
copumpkinI'm kind of enjoying this category theory package22/08 01:24
copumpkinpity there's no adjunction stuff in it22/08 01:45
copumpkinis 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
dolioYou should be able to use IsPreorder.reflexive, I think.22/08 03:03
dolioWhich is probably exported from IsDecTotalOrder, too.22/08 03:03
copumpkinah yes22/08 03:10
stevancopumpkin: :-), 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
copumpkinstevan: 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
copumpkin(but it's unlikely :))22/08 21:18
--- Day changed Mon Aug 23 2010
stepcutIs Agda 'better' at the Expression Problem than Haskell ?23/08 17:17
copumpkinhm, I sort of doubt it23/08 17:20
copumpkinyou can sort of simulate typeclasses and tackle it that way23/08 17:20
copumpkinit seems like the types à la carte approach might be more elegant on the type side but less elegant on the value side23/08 17:21
copumpkin(since you don't have typeclasses and would have to pass the dictionaries around by hand)23/08 17:21
stepcutdoes Agda provide any simple way to do something like the Show class from Haskell ?23/08 17:22
copumpkinnot really, unless you make a "typeclass-tagged value type" or something23/08 17:24
copumpkinthen you'd have to wrap everything in a boring constructor23/08 17:24
stepcutyeah..23/08 17:24
stepcutsometimes I like type classes, but other times I don't..23/08 17:24
stepcutlike, 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 one23/08 17:25
Saizanthey 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 though23/08 17:25
stepcutSaizan: yeah, like the issue I just described I expect..23/08 17:26
Saizanright23/08 17:26
copumpkinstepcut: in haskell you'd use newtypes23/08 17:26
copumpkinbut it's ugly23/08 17:26
Saizanor a two parameter typeclass23/08 17:26
stepcutyou can simulate some of the features of type classes in agda via parameterized(?) modules though  ?23/08 17:27
stepcutcopumpkin, Saizan: right, I have considered both those options for Happstack23/08 17:27
stepcutI saw something about Agda now having support for IO a few months ago, is that right ?23/08 17:28
Saizanparameterized modules help in dealing with the dictionaries manually, since they let you abstract in a larger scope and also open them23/08 17:28
dolioIt's got an FFI to Haskell, so it can in theory support anything Haskell supports.23/08 17:28
stepcutis there a ready-to-use network socket library ?23/08 17:31
Saizanmaybe the web framework linked on the mailing list has something23/08 17:31
stepcutSaizan: that just seemed to provide a few http types23/08 17:32
stepcutthis is the IO library I was thinking of, btw, http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/23/08 17:35
stepcuthttp://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOConsoleLib.html23/08 17:35
stepcuthttp://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleConsole.html23/08 17:37
stepcutI 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
dolioHaven't seen that.23/08 17:37
dolioI imagine one of the goals is to be more specific about exactly what effects are used in a particular computation.23/08 17:38
Saizani suspect he's defining the primitives as constructors which then get interpreted because he wants to inspect the IO action23/08 17:38
stepcutok23/08 17:39
stepcutI have yet to actually run an agda program.. so far, once it type checks, I'm done :)23/08 17:39
Saizani've run an hello world once :)23/08 17:40
stepcutit actually took me a while to realize that I had run an agda program, and didn't even know how :)23/08 17:40
stepcutdoes agda have an concurrency support ?23/08 18:41
stepcutcan I just import forkIO ?23/08 18:42
copumpkinit can FFI out to haskell23/08 18:42
stepcutcool23/08 18:42
stepcutI will have to give this a shot23/08 18:42
copumpkinit's definitely worth playing with :) not sure whether I'd want to write many "real programs" in it, though23/08 18:43
stepcutI'm working on my new book, "Real World Agda"23/08 18:43
Saizancopumpkin: you mentioned a CT lib lately, do you have a link?23/08 18:59
copumpkinhttp://web.student.chalmers.se/~stevan/ctfp/html/README.html :)23/08 19:00
Saizanthanks :)23/08 19:02
* Saizan darcs gets23/08 19:03
copumpkin"Unfortunately, Agda takes too much memory for me to23/08 19:05
copumpkin   continue working on this."23/08 19:05
copumpkin(from a comment in the monoidal categories module :P)23/08 19:06
copumpkinsounds fairly common23/08 19:06
Saizanthat's why i've ordered a stick of memristors23/08 19:07
ccasinmore people in here than in #coq.  Never seen that before23/08 20:43
stepcutbut how does it compare to #epigram ?23/08 20:56
Saizanthat's only at 12 :)23/08 21:05
copumpkinpeople are scared of epigram because of the +v power structure in there!23/08 21:05
stepcutheh23/08 21:06
Saizanshow more respect!23/08 21:06
stepcuti 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
stepcutbut maybe I am wrong :p23/08 21:07
Saizan(we should ask shapr, or anyone with enough power, to remove the autovoice)23/08 21:07
Saizanit's been quite incremental up to now, but i have that kind of feeling, about the internals too :)23/08 21:08
stepcutthough perhaps I was thinking of the jump (?) between epigram 1 and epigram 223/08 21:10
Saizanah, i've never looked at epigram 123/08 21:10
--- Day changed Tue Aug 24 2010
Saizancopumpkin: how do you manage huge records in error messages when using ctfp?:)24/08 08:08
stevanSaizan: 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
stevan... i dunno if that works tho.24/08 09:31
Saizanstevan: in this case we'd need to make functor composition abstract, it seems like that'd break a lot of things though24/08 09:33
* Saizan is trying to make the laws for adjuctions work24/08 09:34
Saizani'm tempted to go the NaturalIsomorphism route, but i'd have to build the product and Set categories for that and i'm feeling lazy24/08 09:35
Saizanoh, found them!24/08 09:36
stevanpushed 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
stevan(i don't remember exactly where those huge records occured)24/08 10:19
Saizanthe problem with the adjunction laws seem to be that functor composition is not obviously a monoidal operation.24/08 10:54
Saizanthe sad part is that only the proofs prevent this.24/08 10:57
benmachineis it non-obviously a monoidal operation?24/08 11:42
Saizanmorally yes, i think even intesionally, but i've not written the explicit proof yet24/08 11:48
Saizanextensionality seems to be required24/08 13:24
stevancare to paste some code? :-)   also, did the huge record problem go away with the abstract proofs?24/08 13:41
Saizanit's less huge :)24/08 14:02
Saizananyhow, take one of the commented laws "comm₁ : (ε ∙ʳ F) ∘ (F ∙ˡ η) ≅ id {F = F}"24/08 14:03
Saizanthe 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
Saizanpostulating (or abstracting over) FunctorExtensionality we can cast them to the right types though.24/08 14:05
Saizanusing the code in Category.Functors.FunctorProperties24/08 14:06
stevani thought that hetro eq would get around the problem that the types don't match, how come it doesn't?24/08 14:12
Saizanyou can't compose those two natural transformations24/08 14:13
stevanhmm24/08 14:14
SaizanF ∘F (U ∘F F) /= (F ∘F U) ∘F F24/08 14:14
stevani can't see how to use FunctorExt to solve this...24/08 14:50
Saizani 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 it24/08 14:52
Laneywe had some casts like that in our implementation24/08 14:59
Laneyhttp://gitorious.org/cats/setoidcats/blobs/master/Monad.agda24/08 15:00
stevancool, thanks24/08 15:18
stevandid some benchmarks with and without abstract proofs in functor, nattrans composition and identity;  without abstract: ~ 4m 15s    and with: ~ 3m 25s24/08 15:58
stevanthat is the total time to typecheck the whole thing.24/08 16:00
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=29421#a29421 <- scary24/08 16:50
copumpkinSaizan: have you seen how other modules in that package deal with needing extensionality? you could just do the same24/08 16:52
Saizancopumpkin: for example?24/08 16:54
copumpkinthey just have an Extensionality u type24/08 16:54
copumpkinit's in one of the modules24/08 16:54
copumpkinhttp://web.student.chalmers.se/~stevan/ctfp/html/Category.Categories.Sets.html#232 for example in here24/08 16:55
copumpkinhttp://snapplr.com/yx8j24/08 16:55
copumpkinalmost all their properties abstract over it24/08 16:55
copumpkinI guess it isn't even from this package, it's just in the standard library24/08 16:56
Saizanit 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 anyhow24/08 17:00
copumpkinyeah, sure24/08 17:00
copumpkinlol, gotta love universe polymorphism: -> Set (suc (o₁ ⊔ o₂ ⊔ o₃ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃))24/08 17:03
Saizanheh :)24/08 17:04
stevanperhaps categories.product could be rewritten such that all those implicit arguments need not be passed explicitly... hmm...24/08 17:10
Saizanmaybe by defining first and second separately, rather than composing (_,_)C and Cp\_n on the spot24/08 17:29
stevanparametrising the module on the two product categories might help24/08 17:31
Saizan_⊣_ : ∀ {o₁ ℓ₁}{C D : Category {o₁}{ℓ₁}} (F : Functor C D) (G : Functor D C) -> Set (suc (o₁ ⊔ suc ℓ₁))24/08 17:39
Saizan_⊣_ {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
Saizanmuch better already :)24/08 17:39
stevannice :-)24/08 17:48
Saizanfirst \o op and second are the F\_1 of some functors btw24/08 17:55
stevani added you to the patch tag project, feel free to push those and other changes24/08 17:56
stevansame goes for you, copumpkin24/08 17:59
Saizanis there an explicit policy on when something should be an argument vs. a field ?24/08 18:00
stevannot that i know of, whatever works best i guess24/08 18:02
copumpkinoh, 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
copumpkinanone 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
ccasinI don't know of good intros25/08 16:01
ccasinpeter dybjer wrote most of the literature about it, you can see his papers25/08 16:02
pedagandcopumpkin, http://www.citeulike.org/user/pedagand/tag/induction-recursion25/08 16:02
ccasinbut lots of them are pretty heavy on the set theory25/08 16:02
ccasinwhenever you write down a mutual block of agda definitions and you use one in the type of the other, you are using induction recursion25/08 16:02
ccasin*(I think)25/08 16:02
copumpkinah, I've done that before25/08 16:02
copumpkinpedagand: any of those more accessible than the others? :)25/08 16:03
pedaganda bit of advice: Dybjer is known for being an excellent writer.25/08 16:03
copumpkinbut he's first (or only) author on all of them!!25/08 16:03
copumpkin:P25/08 16:03
pedagandall right, then I'm risking my life for you by saying: Setzer is not such an excellent writer *hint* *hint*25/08 16:04
copumpkinlol25/08 16:05
copumpkinI promise not to tell anyone25/08 16:05
copumpkin(but be aware there are 32 people in here who are neither you nor me)25/08 16:05
copumpkin(thanks!)25/08 16:05
ccasincopumpkin: 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 codes25/08 16:05
copumpkinccasin: ah yeah, I played with it in a similar way then, without knowing what it was25/08 16:06
ccasinbut 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
copumpkindo things like telescopes fall under it?25/08 16:06
ccasinso 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
dolioInduction-recursion is when you have 'U : Set' and 'T : U -> Set' and you use T in the constructors of U.25/08 16:08
dolioAgda's mutual blocks allow other things.25/08 16:08
copumpkinaha25/08 16:08
dolioYou can actually get more general than those signatures, too.25/08 16:09
dolio'U : <ixs> -> Set' 'T : (<v> : <ixs>) (<w> : <ixs'>) -> U <v> -> S <w>'25/08 16:10
dolioOr something like that.25/08 16:10
dolioThere 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
copumpkinrestrictions why?25/08 16:11
dolioFor instance 'c2 : T c1 -> ... -> U' isn't allowed, for c1 some other constructor of U.25/08 16:11
copumpkinjust because IR is defined that way?25/08 16:11
dolioRather, you should only use T over parameters to the constructor.25/08 16:12
ccasindolio: interesting.  In fact, I have used that "feature" and wondered about it.  Is it known to lead to problems?25/08 16:12
dolioAnd "T ... = U" is also wrong.25/08 16:12
dolioccasin: 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
copumpkin(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
dolio"T ... = U" is wrong from the perspective of what the definition is supposed to mean.25/08 16:14
ccasinit "worked" for me.  though of course I never actually ran the program25/08 16:14
dolioIn 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
dolioHowever, U as a whole is not.25/08 16:15
dolioSo referencing U in the definition of T doesn't make sense from that perspective.25/08 16:15
dolioAnd, 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
dolioI think 'c2 : T c1 ...' is similar.25/08 16:17
dolioccasin: 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
ccasininteresting25/08 16:23
ccasindependent types are fun!25/08 16:24
dolioLots 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
Saizancopumpkin: http://personal.cis.strath.ac.uk/~conor/fooling/Nobby.agda <- ?25/08 16:24
dolioKind of how the productivity checker doesn't correspond to coinduction.25/08 16:24
copumpkinnobby! thanks25/08 16:25
ccasinwell, the theoretical basis is "we only have proofs for the positives ones", right?25/08 16:25
Saizan(found by grepping foo out of desperation :)25/08 16:25
copumpkinbeen trying to remember what quirky name he'd chosen for it :)25/08 16:25
ccasin*positive25/08 16:25
dolioAside from all this, definitions like 'data U : Set ... ; data T : U -> Set ...' are not induction-recursion, either.25/08 16:26
ccasinno, but how about f : (a : A) -> g a -> ... ; g : A -> Set; g a = ... f ...?25/08 16:28
ccasinthat is, where neither is actually an inductive definition25/08 16:28
ccasinjust two mutually recursive functions25/08 16:28
dolioccasin: 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
ccasin:)25/08 16:28
dolioI think you can desugar mutual recursion to a single recursive definition with an extra parameter.25/08 16:29
ccasindolio: but here g is used in f's type25/08 16:30
dolioSimilarly, mutually inductive types that aren't indexed by each other can be turned into an inductive family.25/08 16:30
dolioNot sure about that.25/08 16:30
dolioAnyhow, if that were novel, it'd be recursion-recursion, not induction-recursion. :)25/08 16:31
ccasinyes25/08 16:32
ccasinstill, my advisor called it induction recursion25/08 16:32
ccasinalso coq rejects it and agda doesn't25/08 16:32
ccasinon this thin evidence, I am calling it induction-recursion :)25/08 16:32
dolioWhat error does Coq give?25/08 16:32
ccasina boring one: "undefined variable g" or similar25/08 16:32
ccasinsee, I was hoping to sneak induction recursion into coq by encoding the datatype as a large elimination25/08 16:33
ccasinbut the coq typechecker is smarter than me25/08 16:33
copumpkinSaizan: now for another question :) I vaguely remember someone "translating" (Dep)Nobby.agda to use the standard libraries and stuff25/08 16:35
Saizanthey used a datatype to encode IDesc in coq25/08 16:35
copumpkinbut I have no recollection of who it was, and can't find any reference to it in the logs25/08 16:35
Saizanit was stevan, iirc25/08 16:35
ccasinSaizan: yes, I suppose I could encode it all as a relation, but I wanted to compute with my functions25/08 16:36
Saizancopumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25776#a2577625/08 16:36
copumpkinSaizan: <325/08 16:36
copumpkin:P25/08 16:36
pigworkerJust checking... does Agda from darcs need ghc >= 6.12 these days?25/08 16:48
copumpkinpigworker: I think 6.10.3 is sufficient... the .cabal file claims it needs base-4.1.*25/08 16:48
pigworkerweird... my buddy got "cabal: cannot configure Agda-2.2.7. It requires base ==4.2.*"25/08 16:51
copumpkinoh25/08 16:52
copumpkinhttp://snapplr.com/kmk025/08 16:52
dolioThere's a flag use-locale that decides between 4.2 and 4.125/08 16:52
pigworkerSadly, I'm not in a position to prod things directly.25/08 16:54
copumpkinseems that use-locale doesn't have a default though25/08 16:55
pigworkerWe're trying to figure out how to set up lab machines for course in Edinburgh next year.25/08 16:55
copumpkinbut I guess it defaults to true if your friend had trouble with base 4.2 requirements25/08 16:55
copumpkinpigworker: and it would be a pain to roll out 6.12 or the latest platform to all the lab machines?25/08 16:55
pigworkercopumpkin: it would require higher authority, but it could probably be made to happen, given time25/08 16:56
copumpkinah25/08 16:57
dolioThere should be a way to specify the flag when installing.25/08 16:57
doliocabal install -flags="-use-locale"25/08 17:00
dolio--flags, that is.25/08 17:00
pigworkerdolio: worth a shot, thanks25/08 17:02
* stepcut has similar problems, but due to having base 4.3 :-/25/08 17:14
stepcutI'll just still with agda 2.5 for now maybe25/08 17:15
Saizanah, 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
Saizani 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 atm25/08 17:18
pigworkerThese things seem so brittle and confusing. People who aren't active Haskellers often have a bad time trying Agda.25/08 17:24
copumpkinnext up, the agda platform!25/08 17:32
copumpkina one-click installer for hours of fun25/08 17:32
Saizani wonder how Agda ends up depending on ghc25/08 17:42
pigworkerhar har, Agda should be part of HP...25/08 17:43
Saizananyhow, it seems that because of this you need ghc-6.12.x25/08 17:43
pigworkerI'll wait until the dust settles after AIM, then I'll try to negotiate relevant upgrades.25/08 17:45
Saizan(tbc, you need ghc-6.12 even if you delete agda-pkg from the .cabal file)25/08 17:46
copumpkinpigworker: 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
pigworkercopumpkin: 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
copumpkinah, I see25/08 17:58
copumpkinexciting times :D25/08 17:58
pigworkerThe 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
copumpkinData.Bool should contain bool : forall {a} (P : Bool -> Set a) -> P true -> P false -> (b : Bool) -> P b25/08 22:25
copumpkinor does that live elsewhere?25/08 22:26
dolioI'm not sure where else boolean induction would live.25/08 22:27
copumpkinwho knows :)25/08 22:27
pigworkercopumpkin: yes, and P should be implicit, for higher-order use25/08 23:28
copumpkinyeah25/08 23:29
* edwinb wonders if it'd be a good idea to get organised about the AIM25/08 23:39
copumpkinman, I wish I knew enough to be an AI :P25/08 23:40
edwinbI have never Ied any As ;)25/08 23:42
edwinbBut I look forward to finding out stuff about it25/08 23:42
edwinbthis is probably something I should do in advance really25/08 23:42
--- Day changed Thu Aug 26 2010
dolioMaybe 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
copumpkinI wonder what parts of agda take up so much memory26/08 02:42
copumpkinSaizan: did you push your adjunction in terms of natural isomorphism to the darcs repo?26/08 02:49
copumpkinI'm having trouble stating the pullback properties in agda26/08 05:05
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=29450#a29450 does that make any sense?26/08 05:11
doliocopumpkin: universal-unique is missing things.26/08 05:25
dolioThe two projections from Q should factor into the universal morphism followed by the corresponding projection from P.26/08 05:26
copumpkinoh I see26/08 05:27
dolioAnd u should only equal the universal morphism if the q-projections factor in the same way.26/08 05:27
dolioFactor through u in the same way, that is.26/08 05:27
copumpkinso stuff like u . p2 == q226/08 05:27
doliop2 . u, I think.26/08 05:28
copumpkinyeah, sorry26/08 05:29
copumpkinI'm not sure I understand how your second point differs from your first26/08 05:33
copumpkinI've changed it to http://snapplr.com/01be now26/08 05:36
copumpkinbut it's still missing something?26/08 05:36
dolioYou need  p1 . universal q1 q2 commutes = q126/08 06:10
dolioAnd the same for q2.26/08 06:10
copumpkinoh26/08 06:11
dolioOops, just touched my eye after handling a habanero.26/08 06:12
copumpkindamn26/08 06:12
dolioThis is not pleasant.26/08 06:12
copumpkin:(26/08 06:12
copumpkinlots of water?26/08 06:12
copumpkindunno, I hear water doesn't help actually26/08 06:12
dolioKeeping my eye closed seems to be working.26/08 06:12
copumpkinah26/08 06:12
copumpkinwow, is my code that bad that you'd prefer to blind yourself in painful ways rather than read it? :P26/08 06:13
dolioNo. I was making nacho cheese and then it slipped my mind that I'd handled the peppers.26/08 06:14
copumpkinhow's it going?26/08 06:24
dolioFine. It wasn't that bad.26/08 06:32
copumpkincool26/08 06:33
dolioNot that I'd recommend it.26/08 06:34
copumpkinDidn't think so26/08 06:36
copumpkinI just made pullbacks in agda's set category26/08 06:41
copumpkinyay26/08 06:41
copumpkin(I think :P)26/08 06:42
dolioCheck to see if pullbacks over the terminal object are products.26/08 06:54
copumpkinugh, someone I know from IRC tried to commit suicide and is now a vegetable (probably permanently) :/26/08 06:55
dolioThat's terrible.26/08 06:56
Adamantthat sucks.26/08 06:58
Adamantdolio: use milk.26/08 06:58
dolioI'll try that next time I rub peppers in my face.26/08 07:01
Adamantdolio: chiliheads learn that one quick.26/08 07:07
dolioI wasn't really eager to pour milk all over my head.26/08 07:08
Adamantit could be worse, you could have used the bathroom26/08 07:08
Adamanttrue26/08 07:08
Adamantkinda hard to just get it in your eye when you're in pain.26/08 07:08
Saizancopumpkin: i didn't push it because i'm not sure where i should put it, Category.Adjunction.Alt maybe.. with Hom and Binfunctor under .Functors26/08 08:19
copumpkinSaizan: ah, I see26/08 17:04
copumpkinhmm26/08 17:06
copumpkin  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 g26/08 17:06
copumpkindoes that even make sense?26/08 17:06
stepcutis 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 duplication26/08 20:37
copumpkinSaizan: how so?26/08 22:27
stepcutI'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=2948826/08 22:49
stepcutI am using Agda and lib from head26/08 22:50
copumpkinI remember there being two IOs in agda26/08 22:53
copumpkinbut I can't remember the difference26/08 22:53
copumpkinI don't think you'll find many people in here who actually run programs :P26/08 22:53
stepcutcopumpkin: yeah, I think I figured it out..26/08 22:57
stepcutsure has to compile a lot of files though to build that26/08 22:57
stepcutok, I pasted the working version26/08 22:59
stepcutnext step is to implement a simple loop which reads from stdin and writes to stdout until you enter 'quit'26/08 23:01
copumpkinwow26/08 23:01
copumpkinthat is new and unexplored territory in this channel26/08 23:01
copumpkin!!26/08 23:02
stepcut:)26/08 23:02
copumpkin(I'm kind of serious, though)26/08 23:02
stepcut:)26/08 23:02
copumpkinI think larrytheliquid is the only person I know of who has actually written software that _runs_26/08 23:02
stepcuthehe26/08 23:02
Saizancopumpkin: ProductCategory is a Product in Cat, which would let me reuse _*_ from Product, but Cat requires extensionality, while defining _*_ directly for ProductCategory doesn't26/08 23:18
copumpkinah :/26/08 23:19
copumpkindamn lack of extensionality :P26/08 23:19
pigworkerworkin' on it...26/08 23:19
copumpkindo you think it's worthwhile for me to put my pullback into the repo?26/08 23:19
copumpkinpigworker: can't wait :)26/08 23:19
Saizanpigworker: i wonder what'd happen if i rewrote all of this in cochon :)26/08 23:20
Saizanmaybe i'd get insane at some point..26/08 23:20
* copumpkin snorts26/08 23:21
Saizancopumpkin: i still have to learn what a pullback is, an Agda version might help :)26/08 23:21
copumpkinwell, 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 :P26/08 23:22
copumpkinI'll clean it up a bit and see what people think26/08 23:23
Saizanthere's a disclaimer to that effect in the README anyhow26/08 23:23
Saizan"some definitions are probably wrong, we'll find out when someone uses them."26/08 23:24
copumpkinlol26/08 23:24
dolioA pullback is like the product of the inverse-image of some object in two other objects.26/08 23:24
dolioI think that's right.26/08 23:24
dolioActually, it's a little more complicated than that, I guess.26/08 23:24
Saizanthat's less illuminating than "a monad is a monoid object in the category of endofunctors"26/08 23:25
Saizan;)26/08 23:25
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=29491#a29491, assuming I haven't missed even more stuff26/08 23:25
copumpkinI'm open to suggestions :)26/08 23:26
dolioYou'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
copumpkinp₂ ∘ u ≡ q₂, I thought that was it?26/08 23:29
copumpkin(and the _1 counterpart)26/08 23:29
* copumpkin stares at the diagram some more26/08 23:29
pigworkerWhy not implement a universe of diagrams?26/08 23:31
Saizanand a "diagram -> equations" compiler?26/08 23:32
copumpkinthat sounds pretty neat :)26/08 23:32
pigworkerIf you know what proposition a diagram means, you know you've done the proof you intended.26/08 23:33
pigworkerSaizan: that's why I said "universe" not "set"26/08 23:34
Saizanwith enough ascii art we'll have 2D type signatures too :)26/08 23:37
pigworkerSaizan: zippers in motion...26/08 23:38
Saizanzippers?26/08 23:38
pigworkerThe 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
danbrownSaizan: McLarty's book "Elementary Categories, Elementary Toposes" has the clearest presentation of pullbacks that I've seen26/08 23:47
danbrownhe 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- Y26/08 23:50
danbrownit's worth a look26/08 23:50
danbrownOT: grr @ "Record types are not allowed in mutual blocks"26/08 23:51
--- Day changed Fri Aug 27 2010
pigworkerdo record types in mutual blocks make sense?27/08 00:03
pigworkeroh dear; did I do that?27/08 00:05
Saizanif 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 case27/08 00:12
pigworkerrecords aren't recursive... unless you make them so by tenuous recursive definition27/08 00:13
pigworkerdatatypes live in mutual blocks to support induction-recursion; there's no obvious analogue for records27/08 00:15
Saizanah, makes sense, except that Agda allows recursive records27/08 00:16
pigworkerMoreover, the mutual block approach to I-R is taking a long time to get right.27/08 00:16
pigworkerRecursive records? Military intelligence!27/08 00:17
Saizan"record Rec : Set where field rec : Rec" :)27/08 00:18
pigworkerwith eta-expansion, to boot27/08 00:18
Saizaneven "record U : Set where field u : U -> U" works :)27/08 00:18
pigworkerGordon Bennett!27/08 00:19
pigworker(colloquial expression of horror)27/08 00:20
Saizan(ah, google only found surprise :)27/08 00:20
Saizanwe reported this on the tracker a few months ago27/08 00:21
pigworkersurprise-with-disapproval is probably more accurate than horror27/08 00:21
pigworkerWhatever its other alleged roots (rakish son of newspaper proprietor, etc) "Gordon Bennett" is certainly an avoidance of blasphemy.27/08 00:24
Adamantwouldn't that be "Gordon Dashiell"27/08 00:26
pigworkernow I'm googling27/08 00:28
Saizanhttp://code.google.com/p/agda/issues/detail?id=138 <- interesting27/08 00:29
pigworkerscary, you mean27/08 00:33
Adamantpigworker: "GD"27/08 00:34
Adamantas in gd'ed something-or-other27/08 00:34
copumpkinpigworker: lol, nice tweet27/08 00:36
pigworkercopumpkin: they'd take my comedy card away if I didn't &c27/08 00:36
pigworkerAdamant: as in Jewish blasphemy avoidance?27/08 00:37
Adamantpigworker: yeah, as in general Judeo-Christian blasphemy avoidance27/08 00:37
pigworkerThe 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
Adamantah27/08 00:41
Adamantgeneral expletive, not specifically in conjunction with foul language27/08 00:41
AdamantI presume27/08 00:41
pigworkerYes. One may use "God" as a proper noun referring to God, but in no other way.27/08 00:42
Adamantright.27/08 00:43
pigworkerPeople from Godalming don't like watching Flash Gordon.27/08 00:43
AdamantMing The Merciless!27/08 00:44
Adamantor rather, Mentok The Mind-Taker:27/08 00:46
Adamanthttp://en.wikipedia.org/wiki/Mentok_the_Mind-Taker27/08 00:46
Adamantok, enough OT.27/08 00:46
* edwinb was wondering if he'd just wandered into the wrong channel ;)27/08 00:51
copumpkinSaizan: have you been able to figure out the logic behind pluralizing module names in the ctfp library?27/08 01:02
copumpkinCategory.Adjunction vs. Category.Monads or Category.Functors27/08 01:03
copumpkinoh is it just to avoid a conflict with the standard library?27/08 01:03
doliocopumpkin: Oh. You put them in the wrong place.27/08 01:14
dolioThere should be two additional proofs in Pullback.27/08 01:15
dolioOne should say that p1 . universal ... = q1, and the same for 2.27/08 01:15
copumpkinoh27/08 01:15
copumpkinbut q1 aren't set in stone27/08 01:15
copumpkinq1 and q227/08 01:16
dolioYes, it'd be parameterized by that.27/08 01:16
copumpkinah, fair enough27/08 01:16
copumpkinman, there's a lot of repetition here27/08 01:16
dolioFor any q1 and q2, that commute with f and g, they factor into pk . univ, and said univ is unique.27/08 01:17
copumpkinI guess I could just have the proof be a triple to save repetition27/08 01:18
copumpkinavoid it27/08 01:18
copumpkinbut that seems ugly27/08 01:18
dolioWell, that it's repetitious is probably why categorists don't write it all out this way.27/08 01:21
copumpkinyeah27/08 01:21
dolioYou can abstract it all by talking about diagrams, which are functors from some appropriately shaped category.27/08 01:22
dolioThen you have cones given a diagram, and (co)limits are (initial) final cones.27/08 01:22
copumpkinhm yeah, I've been putting off learning about that :P27/08 01:23
dolioCones being natural transformations (to) from an object (I think I got the order right).27/08 01:23
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=29491#a2949527/08 01:24
dolioI don't know how usable something like that would be in Agda, though.27/08 01:24
copumpkinyeah, we need a new categorical programming language!27/08 01:24
copumpkin:P27/08 01:24
dolioYes, this looks pretty right.27/08 01:25
copumpkinwow, and it only took me 15 tries :)27/08 01:25
dolioOf course, I can't rule out that I'm forgetting something.27/08 01:25
pigworkerA diagram is given by some V : Set, and some E : V -> V -> Set. Now what does it mean?27/08 01:25
copumpkintime for some marmite27/08 01:26
pigworkerIn my case, time to fall over. G'night!27/08 01:27
dolioIf 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
doliopigworker: Also: did they actually disallow recursive records yet?27/08 01:30
dolioLast I checked, they were allowed, and not positivity checked, to boot.27/08 01:30
dolioBug still seems open.27/08 01:33
copumpkinthis is odd27/08 19:49
copumpkinanyone ever encountered C-c C-r in a hole leading to a parse error27/08 19:49
copumpkin?27/08 19:49
copumpkinokay, wrote pushouts too27/08 20:08
copumpkincan I reopen a parametrized module from within it, with a different parameter?27/08 20:12
dolioWhat's C-c C-r again?27/08 20:17
copumpkinI 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 you27/08 20:17
copumpkinso if I put it into a record hole, it'll write the record structure out for me with a bunch more holes in it27/08 20:17
dolioAh.27/08 20:18
copumpkinor if it's a function, it'll give me a lambda27/08 20:18
copumpkinwith the right parameters27/08 20:18
dolioThat sounds handy. I should start using that.27/08 20:18
copumpkinyeah, I love it, but this is the first time it's failed me27/08 20:18
* copumpkin is trying to figure out how to write the pushout for Sets27/08 20:18
copumpkinseems tougher27/08 20:19
dolioIt's conceivable that Agda's Set doesn't have pushouts.27/08 20:19
dolioIt may require quotients.27/08 20:19
copumpkinthat's what I thought might be the issue27/08 20:19
dolioUnless you're using setoids.27/08 20:19
copumpkindamn :P27/08 20:19
copumpkinhm, I'm not27/08 20:20
copumpkintime for a subobject classifier!27/08 20:27
dolioAnyhow, as I recall, and from thinking for a minute or so, a pushout B <f- A -g> 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
dolioAnd the quotient part isn't really available in Agda.27/08 20:34
copumpkinyeah27/08 20:37
copumpkinI guess I can't write a subobject classifier for Set either, in agda?27/08 20:38
copumpkinfor the same reason27/08 20:38
dolioMy knowledge of topos theory is limited, but it wouldn't surprise me if Agda weren't a topos.27/08 20:40
dolioOff the top of my head, toposes correspond to impredicative and extensional type theories.27/08 20:40
danbrownaren't Σ types similar to subobjects?27/08 20:51
copumpkinhmm, but would that be in a different category?27/08 20:52
danbrowne.g. Σx:X.φ ~ { x ∈ X : φ }27/08 20:52
dolioThe 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
dolioIn Agda, you'd use O = Set, but you don't have Set : Set, so it's not an object.27/08 20:52
danbrownso maybe we have subobjects without the classifying object?27/08 20:53
danbrownah, hm27/08 20:53
dolioIt could be Bool, but that only works for decidable subobjects.27/08 20:53
dolioAnyhow, having a subobject classifier, together with exponentials, is similar to having powersets, I think.27/08 20:55
dolioO^A being the power-object, the object of all subobjects of A.27/08 20:56
dolioAnd powersets seem fairly tied to impredicativity.27/08 20:57
copumpkinhmm, are there cases in which eta expanding is necessary?27/08 21:00
dolioSo maybe (some subset of) Coq would have one, but I'm uncertain how it would work out exactly.27/08 21:00
dolioProp being the subobject classifier for the topos of Types would seem reasonable, I guess.27/08 21:01
dolioBut that doesn't directly make use of impredicativity.27/08 21:01
dolioAt least, as far as I can see.27/08 21:01
dolioSo 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
dolioAnd have a subobject classifier.27/08 21:05
dolioBut I don't really know what all that would entail.27/08 21:05
copumpkinhmm27/08 21:07
copumpkinI'm not convinced the pushout is impossible, but I haven't succeeded in making one yet :P27/08 21:08
dolioOh no? I bet I can convince you.27/08 21:08
copumpkinoh okay27/08 21:09
copumpkinnow we need a proof of \neg Pushout :P27/08 21:09
dolioWell, it won't be anything like that.27/08 21:09
copumpkinyeah, just being silly :)27/08 21:09
dolioI'll start with a pushout and get a quotient type.27/08 21:09
dolioAt least, that's the idea.27/08 21:09
copumpkinokay27/08 21:10
dolioHmm, I may have been over zealous.27/08 21:25
dolioI'm no longer sure how to do this.27/08 21:25
copumpkinI'm getting closer and closer in the proof, which is making me worry about my pushout definition more than my proof :P27/08 21:27
dolioHmm, maybe my initial idea was okay...27/08 21:31
copumpkinhmm27/08 21:34
copumpkinwell agda just accepted this, but I think I proved something else27/08 21:34
copumpkinoh duh27/08 21:35
copumpkinyeah, my proof is pretty meaningless :P27/08 21:35
copumpkinman, I can't believe I worked on this for the past half hour without realizing that I was starting from something so obviously untrue27/08 21:36
copumpkinif you want to laugh at me, my proof took in a proof of inj1 (f x) == inj2 (g x)27/08 21:47
copumpkinso yes, I have pushouts in agda :P27/08 21:47
dolioThat would help.27/08 21:47
copumpkinseems like I sort of want polymorphic variants here27/08 21:59
dolioBah, the eliminator is going to require extensionality of functions.27/08 22:00
stepcutok, 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=2953627/08 22:29
copumpkinwhat's wrong with that? :P27/08 22:29
copumpkinI'm sure I've seen people write it more linearly27/08 22:29
copumpkindo you need the parentheses? I thought the associativity worked nicely27/08 22:30
stepcutit's not the parens so much that are the issue27/08 22:30
stepcutwhen you have only two IO operations it looks ok27/08 22:30
stepcutfoo4 : IO ⊤27/08 22:30
stepcutfoo4 =27/08 22:30
stepcut   ♯ putStrLn "foo 1" >>27/08 22:30
stepcut   ♯ putStrLn "foo 2"27/08 22:30
stepcutbut, if you want to extend it to three, then you need an extra, ♯27/08 22:31
stepcut  _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B27/08 22:31
stepcutbecause the return type of (a >> b) is IO B, not ∞ (IO B) .. or something27/08 22:32
stepcutyeah27/08 22:33
doliocopumpkin: http://code.haskell.org/~dolio/agda-share/html/PushoutQuotients.html27/08 22:33
copumpkinstepcut: I see what you mean27/08 22:33
stepcutif you do, (♯ a >> ♯ b) >> ♯ c, that does not work, because (♯ a >> ♯ b) has the type IO b, not ∞ (IO B)27/08 22:34
stepcutso you have to do, ♯ (♯ a >> ♯ b) >> ♯ c27/08 22:34
copumpkindolio: oh thanks, interesting27/08 22:34
stepcutwhich is pretty ugly pretty fast27/08 22:34
stepcutmaybe I am just the first person to try to sequence *3* IO operations in a row ?27/08 22:34
copumpkinlol27/08 22:34
stepcutworks great for 2 :)27/08 22:34
copumpkinstepcut: maybe make some sort of list thing that gets sequenced? :P27/08 22:35
dolioThat's an odd type. Is that a constructor?27/08 22:35
stepcutdolio: yeah27/08 22:35
dolioAh, okay.27/08 22:35
stepcutdata IO : Set → Set₁ where27/08 22:35
stepcut  lift   : ∀ {A} (m : Prim.IO A) → IO A27/08 22:35
stepcut  return : ∀ {A} (x : A) → IO A27/08 22:35
stepcut  _>>=_  : ∀ {A B} (m : ∞ (IO A)) (f : (x : A) → ∞ (IO B)) → IO B27/08 22:35
stepcut  _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B27/08 22:35
copumpkinwe should have dependent IO!27/08 22:36
copumpkinwhere bind takes (x : A) -> inf (IO (B x)) :P27/08 22:36
stepcutif 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
dolioI'm not surprised, then. Programming directly with the coinductive type as a DSL is unlikely to be nice.27/08 22:37
dolioI'm not sure a nice DSL (passing all the relevant checkers) has yet been discovered, though.27/08 22:38
stepcut:)27/08 22:38
stepcutis there some what it could be changed so that sequencing 3 in a row was a little less painful?27/08 22:38
dolio>> and >>= should probably be definitions, for instance, but then you can't write down directly recursive things.27/08 22:39
dolioAnd have type IO A -> IO B -> IO B and so on.27/08 22:39
stepcutmaybe I should post on the mailing list and ask whoever wrote IO.agda in the first place?27/08 22:40
dolioAnd conceivably you could introduce recursion via a combinator, but the question is what that combinator is.27/08 22:40
copumpkinstepcut: 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 dissertation27/08 22:41
stepcutcopumpkin: :)27/08 22:41
doliocopumpkin: IO A -> ((x : A) -> IO (B x)) -> IO (B ?)27/08 22:41
stepcutcopumpkin: the tricky part is when I want to make it a loop ;)27/08 22:41
copumpkindolio: yeah, beats me :P more research!27/08 22:42
dolio? = unsafePerformIO m27/08 22:42
stepcutaka, 10 print "hello, agda!"  ; 20 goto 1027/08 22:42
dolioI'm still annoyed that those proofs required extensionality.27/08 22:42
dolioActually, I could probably get around it if the Pushout proofs weren't formulated as composition.27/08 22:43
dolioI'll just leave it, I guess.27/08 22:44
copumpkinyeah27/08 22:45
copumpkinlet'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
stepcuthow long do we have to wait ?27/08 22:46
copumpkinAgda 2.2.8: the type theorist's wet dream27/08 22:46
copumpkinstepcut: it's waiting on perl 627/08 22:47
stepcutk27/08 22:48
stepcutI just want to make a little app that has a 'loop' which does getLine, processes the string, and does a putStrLn27/08 22:53
stepcutit's pretty crazy, I know..27/08 22:53
stepcutok, email sent!27/08 22:54
stepcutit's a good thing you can prove you app is correct before you actually compile it .. because compilation takes forever :p27/08 22:55
copumpkincheck the proof can take even longer!27/08 22:56
copumpkinthere'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
Saizanshould we buy a server and share a single session?27/08 22:58
copumpkinif only I hadn't quit grad school, or I'd still have access to a 32GB machine27/08 22:59
copumpkinactually a couple of them27/08 22:59
copumpkinso we could prove things in parallel!27/08 22:59
Saizanwow!27/08 22:59
copumpkin-or there27/08 22:59
dolioWith 32 GB of memory, I could prove three additional category theory theorems!27/08 23:01
stepcutMy 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
dolioWow, 10 is a lot.27/08 23:02
dolioMine has 2.27/08 23:02
dolioIt's pretty old, though, I guess.27/08 23:02
stepcutI had 2GB, wasn't enough, so I added 8 more.. wasn't that much though27/08 23:03
copumpkinI'm with Saizan! we should pool our money and buy a monster server, for epic proofs27/08 23:03
copumpkinram is pretty cheap these days, but many laptops can't take it :(27/08 23:03
stepcutyeah, my laptop is maxed out a 4GB (though, right now I can only access 3GB)27/08 23:04
stepcuthttp://gizmodo.com/5365029/sgis-personal-supercomputer-handles-80-cores-1tb-of-ram27/08 23:05
Saizanwe might also use the same money to pay someone to optimize Agdas..27/08 23:05
stepcutyeah, 1TB of ram is still around $90,000 I think ?27/08 23:06
copumpkinSaizan: pff, where's the fun in that27/08 23:07
copumpkinI'd be curious to see where most of the ram usage is though27/08 23:08
Adamantproducts in that category are interesting27/08 23:16
AdamantI think Tyan also had a more PC-based one27/08 23:16
Adamantwith all the hyperthreading multi-core stuff, it's much more realistic27/08 23:17
doliocopumpkin: All right, non-extensionality version: http://code.haskell.org/~dolio/agda-share/html/PushoutQuotients.html27/08 23:17
stepcutI wonder how well GHCs garbage collection would hold up with hundreds of GB of data..27/08 23:17
copumpkindolio: that makes sense :)27/08 23:18
copumpkinshould I push the pushout and pullback to the ctfp repo?27/08 23:38
* Saizan votes yes27/08 23:41
copumpkinpushed! omg27/08 23:51
--- Day changed Sat Aug 28 2010
copumpkindolio: do you remember what part of your Category.Product caused agda's memory usage to blow up so much?28/08 00:55
copumpkinlike, is there something that can be easily commented out to make it a little less ridiculous?28/08 00:56
dolioThe two isomorphisms.28/08 00:56
dolioA x B ~ B x A and A x (B x C) ~ (A x B) x C28/08 00:56
copumpkinah28/08 00:57
dolioThe proofs themselves are enormous, so it may not be surprising that they're memory heavy.28/08 00:58
dolioActually, the first one isn't so bad, but the second is very long.28/08 00:59
copumpkinyeah28/08 01:01
copumpkinI wonder how much agda uses laziness behind the scenes28/08 01:17
dolioEvaluation is in fact lazy in agda.28/08 01:18
dolioYou can tell by writing stuff that fails the termination checker.28/08 01:18
copumpkinwell I mean in the type/termination checker itself28/08 01:18
copumpkinhttp://snapplr.com/fqjm28/08 01:18
copumpkinthat's a lot of lists28/08 01:19
copumpkinI was wondering how much strictness annotations on datatypes + -funbox-strict-fields could help its memory gobblage28/08 01:19
copumpkin(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
Saizanis there a way to know the type of the lists?28/08 01:23
copumpkinI was trying to figure it out, but couldn't find anything28/08 01:23
copumpkinh28/08 01:23
copumpkinoh28/08 01:23
copumpkin-hy28/08 01:23
copumpkinwill test again :P28/08 01:24
copumpkinlol28/08 01:25
copumpkinit gives the type as [] :P28/08 01:25
copumpkinI guess it doesn't maintain enough information28/08 01:25
Saizanheh28/08 01:25
Saizanmaybe the elements are the stg_ap_2_upd_info thing, or they don't use as much memory..28/08 01:26
copumpkingah, profiling this thing is terrifying28/08 02:03
copumpkinI picked at some of the low-hanging fruit but it didn't help28/08 02:03
copumpkinbah, I give up :P this thing is a monster!28/08 02:29
copumpkinman, trying to encode a simple linear lambda calculus such that the invariants are encoded in the indices is a real pain28/08 03:42
doliohttp://code.haskell.org/~dolio/agda-share/html/SetoidPushout.html28/08 04:55
dolioThe category of setoids has pushouts.28/08 04:55
dolioThat file somehow manages to load faster than the one showing that pushouts in Set allow quotient types.28/08 04:57
copumpkinwow :)28/08 04:57
copumpkinneat28/08 04:57
dolioBy a significant margin.28/08 04:57
doliocopumpkin: 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
dolioWhich renders it unable to represent impredicativity.28/08 05:48
dolioI'm not sure if that would keep it from being a topos or not, though.28/08 05:48
copumpkinI hope not! I really want me a topos28/08 05:52
dolioIt probably does, because you can't necessarily define an A -> Ω for every subobject of A.28/08 05:52
copumpkinyeah :/28/08 05:52
dolioOnly, again, decidable subobjects of A, because you need to use a decision procedure to select what Ω to return.28/08 05:52
copumpkinwould it make sense to make a decidable category?28/08 05:53
dolioWhat do you mean by that?28/08 05:53
copumpkintrying to think what I mean by it :)28/08 05:54
copumpkincategory of decidable relations over agda types?28/08 05:54
dolioThat might be pretty limiting.28/08 05:55
dolioAnyhow, I suspect that whatever you mean by that, it's not going to work out well.28/08 05:56
copumpkin:)28/08 05:56
copumpkindamn28/08 05:56
dolioIf you want all the objects to have decidable equality, for instance, there are no exponentials.28/08 05:57
copumpkinthat makes sense28/08 05:57
copumpkindammit28/08 05:57
copumpkincategory of enumerable types and relations between them?28/08 05:58
copumpkinsounds like a nightmare though28/08 05:58
copumpkinbut that should restore your exponentials and give you subobjects too, I'd think28/08 05:59
danbrownif A is a datatype constructor, how do I derive ⊥ from a proof ~ : A x ≡ x ?28/08 21:07
danbrownabsurd patterns appear to not work here28/08 21:08
danbrown"A x ≡ x should be empty, but it isn't obvious that it is."28/08 21:08
danbrownbut it doesn't suggest any valid constructors28/08 21:09
danbrown(there aren't any)28/08 21:18
pedaganddanbrown, lookup "a few constructions on constructors", you're looking for an acyclicity property here28/08 21:25
danbrownpedagand: great, thanks28/08 21:25
pedagandfor nat, this boils down to that: http://pastebin.com/jz4Ek47Y28/08 21:32
pedagandbut maybe there is some clever, generic stuff in the stdlib doing that already, I don't know28/08 21:33
danbrownyeah...28/08 21:34
danbrownlooks a little more complicated when you have multiple constructors28/08 21:34
pedagandyeah, that's also what they say :-)28/08 21:49
pedagandif 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
danbrowni see, that makes sense28/08 21:59
--- Day changed Sun Aug 29 2010
Saizanhow'd you fomalize the Yoneda Lemma? i'm not sure in which category the bijection should live29/08 22:58
dolioC x Set^C -> Set29/08 23:00
dolio(A, F) |-> FA is isomorphic to (A, F) |-> Nat(Hom(A, -), F)29/08 23:02
dolioI think that's right.29/08 23:03
Saizanwhat is |-> ?29/08 23:03
dolioMaps to.29/08 23:04
Saizani see29/08 23:06
dolioThe first one being the evaluation morphism for functor categories as exponentials.29/08 23:07
Saizani'm prejudiced against using Set for some reason, it feels like stepping out of the theory29/08 23:14
dolioYes, I know. I feel the same way.29/08 23:14
dolioThere's probably a Yoneda lemma in enriched category theory that switches Set with something else.29/08 23:16
dolioIncluding other categories if you want.29/08 23:16
dolioActually, I guess it'd always be another category.29/08 23:17
Saizani've realized that my F is going to be an hom functor, and those are already C^op x C -> Set, so it's fine29/08 23:18
Saizandolio: 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 confused29/08 23:43
dolioYes, covariant functors.29/08 23:44
dolioThere's a yoneda lemma for contravariant functors too, though, I think.29/08 23:45
Saizani think one just takes C = D^op for that?29/08 23:45
dolioThough maybe you get it by substituting C = D^op.29/08 23:45
dolioYeah.29/08 23:45
dolioYou could state it directly, though.29/08 23:45
dolioC^op x Set^C^op -> Set29/08 23:46
dolio(A, F) |-> FA is isomorphic to (A, F) |-> Nat(Hom_C(-, A), F)29/08 23:46
dolioBut Hom_C(-, A) is Hom_C^op(A, -)29/08 23:47
* dolio has to jet.29/08 23:48
Saizani'm going to need both sides anyway :)29/08 23:48
Saizanthanks! btw29/08 23:48
dolioNo problem.29/08 23:49
--- Day changed Mon Aug 30 2010
* Saizan pushed some bifunctors 30/08 16:48
copumpkinSaizan: ooh!30/08 16:54
copumpkinI'll do trifunctors and you can do quadrifunctors30/08 16:54
Saizanheh :D30/08 17:07
Saizan(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
Saizanbtw, is it possible to have a Cat where the categories can be at different levels?30/08 17:09
copumpkinmake a SigmaCat? :P30/08 17:09
copumpkindunno30/08 17:09
Saizanit doesn't seem to like "∃ \ o -> ∃ \ ℓ -> Category {o}{ℓ}"30/08 17:13
copumpkinwell, I'd wonder what the kind of the resulting Sigma would be30/08 17:16
copumpkinI mean the level30/08 17:16
Saizan\inf ?:)30/08 17:16
copumpkin:P30/08 17:17
copumpkindolio did mention an omega level that you can't write or something30/08 17:17
dolioYes. (l : Level) -> Set l has type Set\omega, for instance.30/08 17:42
dolioBut you can't make analogous sigmas in Agda.30/08 17:42
copumpkinso 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
dolioI think that's right.30/08 17:49
dolioupts on my code.haskell.org site has sigmas like that.30/08 17:49
dolioSo you can make, for instance, { l : Level, A : Set l | A }.30/08 17:50
dolioThe type of all non-omega types.30/08 17:50
copumpkinah30/08 17:51
copumpkinis there a suc omega for the type of all types including those in set omega?30/08 17:51
dolioNo. Omega is the top.30/08 17:52
stevancopumpkin, Saizan: thanks for the patches :-)30/08 18:58
Saizanstevan: btw, do you know why is-product in Category.Categories.Product was commented out?30/08 19:15
stevanlack of time probably -- we had a deadline. :-)30/08 19:17
--- Day changed Tue Aug 31 2010
Cadsso 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
Cadsit's simple to show this using the definitions of the least upper bound and monotonicity, respectively31/08 02:47
Cadsbut what would this look like expressed in agda?31/08 02:47
Cadswould this be a good first task to try formalizing?31/08 02:48
copumpkinif it involves the reals, probably not31/08 02:48
Cadsit should work with any lattice that has the least upper bound property and the completeness property, I'm guessing31/08 02:50
copumpkinyou could probably do that abstractly, but I'd still recommend proving some trivial things first, to get a feel for it31/08 02:51
Cadsdoing 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
Cadsrather than worrying about computing reals?31/08 02:54
copumpkinwould supercompilation be automatic in a strongly normalizing language?31/08 20:09
copumpkinassuming someone actually bothered to compile it31/08 20:09
dolioAutomatic?31/08 20:11
copumpkinwell31/08 20:13
copumpkinin 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 through31/08 20:14
dolioYou don't have to worry about some of them.31/08 20:14
dolioI think tail recursive functions might still be subject to infinite amounts of unfolding.31/08 20:15
dolioIf my recollection that that is a problem is correct.31/08 20:16
copumpkinhmm31/08 20:16
dolioBut you don't have to worry about the partial evaluation part failing to terminate, presumably.31/08 20:16
dolioAs long as your supercompiler never asks for ill-typed or otherwise termination-check-failing terms to be evaluated.31/08 20:17
dolioActually, I guess it's functions with an accumulating parameter.31/08 20:25
dolio"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
dolioFor 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
dolioYou need to cut that off at some point.31/08 20:29
copumpkinyeah31/08 20:30
copumpkinmakes sense31/08 20:30
copumpkinso fewer heuristics would be needed, but you'd still need a few31/08 20:30
dolioDid you read Max Bolingbroke's paper on supercompilation?31/08 20:30
copumpkinyep31/08 20:30
dolioWell, he mentions that you need the termination heuristic in two places.31/08 20:31
dolioOne 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
dolioIf your language is strongly normalizing, you shouldn't need it for the first.31/08 20:31
dolioAnd 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
Saizanthe second case is a "should optimizie this more?" rather than a "does this term terminate?" heuristic?31/08 20:41
dolioSomething like that.31/08 20:42
dolioWell, the intention of the first is, "should I keep running my evaluator."31/08 20:42
dolioSo they're similar in idea if not all programs terminate.31/08 20:43
dolioHis supercompiler essentially works on STG machine states.31/08 20:43
dolioSo you can check if you should stop evaluating after each machine step.31/08 20:43
dolioAlthough, 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

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