--- Log opened Mon Mar 01 00:00:17 2010 | ||

stevan | lpjhjdh if you read the logs or if someone else catches him next time: http://www.cs.chalmers.se/Cs/Grundutb/Kurser/types/agda-lecture/Bool.html http://www.cs.chalmers.se/Cs/Grundutb/Kurser/types/agda-lecture/Arith.html he might find that helpful, i missed him twice now :-/ | 01/03 18:01 |
---|---|---|

Berengal_ | Is it possible to use agda's unicode input in other modes? | 01/03 21:22 |

stevan | i'd really like to use it combined with haskell-mode; if you get it working, please let me know :-) | 01/03 21:24 |

copumpkin | I think agda's unicode input isn't its own | 01/03 21:24 |

copumpkin | it has a name | 01/03 21:24 |

* Berengal_ goes source diving | 01/03 21:25 | |

stevan | i miss proper modules, holes, unicode and mixfix when ever i code in haskell :-/ | 01/03 22:05 |

stevan | can't understand those vim guys on the wiki, do they know what they are missing out not having goals? i figure there should be a big warning in red on that "vim editing" wiki page saying it's a completely different thing without goals? :-) | 01/03 22:09 |

Saizan | wrt holes in haskell there's a little tool built over the ghc-api | 01/03 22:13 |

Saizan | it won't give you the context though | 01/03 22:14 |

stevan | i recall reading about it; does it work well? do people use it? | 01/03 22:14 |

Saizan | it worked when i tried it, though i don't think it got much attention | 01/03 22:15 |

stevan | does C-c C-c work? | 01/03 22:15 |

Berengal_ | I sometimes ponder hacking hole and context support into haskell-mode somehow, but then I realize I have neither the time nor the skill to do it :( | 01/03 22:15 |

Berengal_ | Also: | 01/03 22:15 |

Berengal_ | (require 'agda-input) | 01/03 22:15 |

Berengal_ | (set-input-method "Agda") | 01/03 22:15 |

Saizan | it just gives you the type of the hole, nothing of the rest | 01/03 22:15 |

Berengal_ | Put that in your .emacs and you've got agda input everywhere | 01/03 22:16 |

stevan | great, thanks. | 01/03 22:16 |

Saizan | mh, now you're forcing me to use erc | 01/03 22:16 |

Berengal_ | My elisp skills are unfortunately not currently up to the task of adding that to haskell-mode, or make it its own minor mode. Perhaps I should look into that... | 01/03 22:17 |

stevan | does using \Gl instead of \ work in haskell? i recall \r \=> \l1 etc all work? | 01/03 22:22 |

Saizan | \Gl doesn't work | 01/03 22:27 |

stevan | :-/, i recall having seen a ticket about it, haskell' proposal perhaps? | 01/03 22:30 |

Saizan | there's one on ghc's trac | 01/03 22:30 |

stevan | http://hackage.haskell.org/trac/ghc/ticket/1102 | 01/03 22:32 |

--- Day changed Tue Mar 02 2010 | ||

stevan | lpjhjdh: hi, i posted two links to TaPL exercises in agda and coq a couple of hours ago on the dependent_types subreddit, i figured they might interest you, have you seen them? | 02/03 00:17 |

lpjhjdh | I haven't, I'll take a look, thanks | 02/03 00:18 |

lpjhjdh | stevan: my Value type is indexed by a term, is that unnecessarily descriptive? | 02/03 00:32 |

lpjhjdh | I was having trouble formulating a few things I wanted to, like the fact that (t \<Down> v) always produces a value (I proved it later) | 02/03 00:33 |

lpjhjdh | I had "data _⇓_ : Term → Term → Set where" and I wanted "data _⇓_ : Term → Value → Set where" but I have to give Value some term and I wasn't sure what to give it | 02/03 00:34 |

Saizan | you mean you've Value : Term -> Set ? | 02/03 00:40 |

lpjhjdh | yeah | 02/03 00:41 |

Saizan | in that case you could "data _⇓_ : Term → {t : Term} -> Value t → Set where" | 02/03 00:41 |

lpjhjdh | ah, I guess that makes sense, I'll give it a shot, thanks again | 02/03 00:42 |

stevan | what's the idea behind parametrizing the value on the term? | 02/03 00:45 |

lpjhjdh | I was thinking I needed it to get nat values | 02/03 00:46 |

lpjhjdh | but I guess I could just have nv-zero nv-suc | 02/03 00:47 |

lpjhjdh | and get the same information | 02/03 00:47 |

TacticalGrace | Just out of curiosity, who maintains Agda these days? | 02/03 12:15 |

stevan | dolio: nice haskell wiki entry! i was wondering about what applications this has in functional programming? also how does indexed functors and free indexed monads from those fit into this context? from the little i read about ifunctors/imonads in conor's slides it seems you can get subst for free for STLC? would you get subst for free for LC in the unindexed setting? | 02/03 13:43 |

dolio | I'm not really up on how indexed functors/monads fit into formal category theory. | 02/03 13:44 |

dolio | As for what applications it has... | 02/03 13:46 |

dolio | Free algebras are (I think) essentially how you give semantics for datatypes, only they're typically called initial algebras. | 02/03 13:47 |

dolio | And cofree coalgebras (terminal coalgebras). | 02/03 13:47 |

stevan | it would be really nice to get a gentle intro to how those things work. | 02/03 13:49 |

dolio | (Co)free (co)monads are similar. | 02/03 13:50 |

dolio | If free algebras over a functor are the datatypes of that shape, then free monads over the functor are rather like computations/expression trees with operations defined by the functor. | 02/03 13:54 |

dolio | I think that's an all right description, at least. I'm by no means an expert in this. | 02/03 13:55 |

dolio | Obviously in Haskell monads are used to describe various types of computation. | 02/03 13:55 |

dolio | And I think most of them could be given in a fairly straight-forward way as free monads, together with an appropriate 'interpreter' function. | 02/03 13:56 |

dolio | Instead of represented directly, with a 'runFoo' that just unwraps a newtype. | 02/03 13:56 |

stevan | you don't happen to have a reference to some book/paper which presents this without assuming too much prior knowledge? | 02/03 13:58 |

dolio | I could point you to decent stuff on initial algebras and such. | 02/03 13:58 |

dolio | Free monads and the like seems to be something some category theory books build toward. | 02/03 13:59 |

dolio | I recently finished reading Awodey's book, and he gets to that area right at the end, but I didn't come away feeling like I knew much about it. | 02/03 14:00 |

stevan | the categorical/ algebraic concepts i'm sure i can find info about, but the connections/ applications in CS is harder? | 02/03 14:01 |

dolio | In category theory, monads and algebras thereof are how (or, the more popular way) you do (and generalize) abstract algebra. | 02/03 14:02 |

dolio | So, I suppose part of the connection is that programming and reasoning about programs involves algebraic structures. | 02/03 14:03 |

dolio | And 'free' stuff is the purely syntactic. | 02/03 14:04 |

stevan | hmm | 02/03 14:10 |

guerrilla | so, in agda, is it possible to have a function of type Set -> Set that turns an X A into a Y A (e.g. Foo A to List A) - what would the syntax for such a function look like? | 02/03 14:22 |

stevan | so for a specific X and Y it would be a natural transformation, yes? but you want it to work for arbitrary X and Y? you'd have to resort to universes for that i think? since you can't pattern match on Sets. | 02/03 14:28 |

stevan | not sure, could you give more context? | 02/03 14:31 |

guerrilla | yeah, i thought i may have to resort to universes and that i couldn't pattern match on sets | 02/03 14:33 |

guerrilla | well, for context, i just wanted a little syntactic sugar, like _* : Set -> Set would be basically (FiniteSet A)* = List A | 02/03 14:34 |

guerrilla | but that's not syntactically valid :) | 02/03 14:34 |

guerrilla | are elements of Set considered constructors of Set1? if that were the case it seems like you would be able to pattern match on elements of Set | 02/03 14:35 |

guerrilla | i'm thinking that F A and L A aren't actually elements of Set though... maybe they are \forall (A : Set) . A -> Set or something similar.. | 02/03 14:36 |

stevan | i think you have to lift things manually to higher level sets. i recall having read an explaination of why you can't pattern match on sets, but i can't recall the reason or where i read it -- a guess is that something like: f (\bot) = \top might potentially cause problems? don't know. | 02/03 14:43 |

guerrilla | hmm, well i'll try playing a bit with universes/levels | 02/03 14:44 |

guerrilla | actually, maybe i'll just make it work for this specific case for now and move on :) | 02/03 14:45 |

stevan | :-) | 02/03 14:49 |

guerrilla | btw, this is what i'm trying to get to work http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23177#a23177 | 02/03 14:55 |

guerrilla | huh, that was dumb | 02/03 14:57 |

guerrilla | could have just done this all along: | 02/03 14:57 |

guerrilla | _* : Set → Set | 02/03 14:57 |

guerrilla | (A)* = List A | 02/03 14:57 |

guerrilla | :P | 02/03 14:57 |

stevan | :-) | 02/03 14:58 |

dolio | You don't need the parentheses. | 02/03 15:19 |

dolio | A * = List A | 02/03 15:19 |

dolio | Saves 1 character! | 02/03 15:20 |

guerrilla | dolio: w00t thanks ;) | 02/03 15:45 |

guerrilla | cool, my hpaste from above now type-checks. we'll see if this will work out in the end though :) | 02/03 16:49 |

guerrilla | ok, i'm a bit stuck again. i've defined type for a (minamalistic) Setoid and am trying to build a list-like type for finite sets, but I can't seem to figure out how to use the equality predicate of the setoid to do a comparison... | 02/03 19:20 |

guerrilla | setoid code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23178#a23178 | 02/03 19:20 |

guerrilla | finiteset code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23179#a23179 | 02/03 19:20 |

guerrilla | how would i extract the equiv predicate to actually use it? | 02/03 19:21 |

guerrilla | is that even possible with this setup? | 02/03 19:21 |

guerrilla | it seems like i would need the implicit argument of _∈?_ to be explicit in it's second pattern matching clause... | 02/03 19:25 |

guerrilla | (or yet again, pattern match on a type, which i'll just rule out now on the basis of what stevan said) | 02/03 19:25 |

stevan | you can get access to implicit variables; _\in?_ {A} a (b \in A')... a better solution is perhaps to parametrize the whole module with a setoid. module FiniteSet (A : Setoid) where... you might want to make the setoid a record instead of a data type (that way to get the projections for free). | 02/03 19:51 |

guerrilla | ok thanks for the implicit vs. explicit part, i'll try that in a second | 02/03 19:52 |

guerrilla | i did start with the record method first, but had some universe issues for some reason, so decided to just do it that way for now | 02/03 19:52 |

guerrilla | even when i had record Setoid : Set1 where.. and a 'setoid' function/constructor, i couldn't use any of the constructed setoids in any forms of (A : XYZoid) | 02/03 19:53 |

guerrilla | i may go back to that later though | 02/03 19:53 |

guerrilla | stevan: great, that worked perfectly | 02/03 19:57 |

guerrilla | _∈?_ {S} a (b ∈ B) = a == b where _==_ = eq-pred S | 02/03 19:57 |

guerrilla | :) | 02/03 19:57 |

guerrilla | thanks a lot | 02/03 19:57 |

guerrilla | odd that you couldn't use the {S} in the infix form.. | 02/03 20:00 |

guerrilla | pbly a practical reason for that, i'd imagine | 02/03 20:00 |

stevan | (setoid are defined in Relation.Binary btw) | 02/03 20:05 |

guerrilla | i know :) i'm trying something a little different - using predicates for relations.. | 02/03 20:06 |

guerrilla | i find the Rel* code a bit difficult to follow as well | 02/03 20:06 |

guerrilla | may re-do the whole thing with that as i get better with agda | 02/03 20:07 |

stevan | normalizing the types: C-n <paste-type-code> might help | 02/03 20:07 |

guerrilla | hmm.. not using emacs unfotunately | 02/03 20:08 |

guerrilla | what would that do? | 02/03 20:08 |

stevan | agda isn't really agda without emacs | 02/03 20:09 |

guerrilla | hmm, didn't realize it would be such a different experience | 02/03 20:09 |

guerrilla | i'm so used to vim.. hard to switch | 02/03 20:09 |

stevan | it is like day and night, man :-) | 02/03 20:09 |

stevan | use viper-mode | 02/03 20:10 |

stevan | emulate vi keys inside emacs | 02/03 20:10 |

guerrilla | ok, well, maybe i'll have to do a tutorial on emacs this weekend | 02/03 20:10 |

guerrilla | (would prefer to use emacs as LISP >>> retarded VIM/ed language) | 02/03 20:10 |

stevan | guerrilla: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing added section on how to emulate vi inside emacs | 02/03 20:48 |

guerrilla | that's great | 02/03 20:57 |

guerrilla | thanks a lot | 02/03 20:57 |

guerrilla | (didn't get your 'use viper-mode' comment earlier, but i see now) | 02/03 20:57 |

stevan | i reckon all you need is to work thru the built in emacs tutorial (it says how to enter it when you fire up emacs) so you learn how to switch between buffers and some other basic stuff (ignore the text movement etc parts) and then you will feel as home in emacs as in vim | 02/03 21:00 |

guerrilla | ok, cool | 02/03 21:01 |

guerrilla | sounds like a plan | 02/03 21:01 |

stevan | someone should really make a screen cast of an interactive agda session, i think that would be very helpful for new people to appriciate holes | 02/03 21:02 |

guerrilla | voluneering ? ;) | 02/03 21:03 |

stevan | i came up with the idea, that's half of the work! :-) | 02/03 21:05 |

stevan | some software which displays the keys pressed in a subtitle like fashion would be nice to have for the task | 02/03 21:06 |

guerrilla | hmm, yeah, i haven't seen that before | 02/03 21:06 |

stevan | ought to exist | 02/03 21:07 |

--- Day changed Wed Mar 03 2010 | ||

ski | hm, is it possible in Agda2 to define something like `data Foo : Nat -> Set where MkFoo : (b : Bool) -> if b then Foo Zero else Foo (Succ Zero)' ? | 03/03 12:45 |

npouillard | ski: I think so | 03/03 12:46 |

ski | (i.e., do case analysis on dependent arguments in the constructors) | 03/03 12:46 |

npouillard | but maybe write it that way: `data Foo : Nat -> Set where MkFoo : (b : Bool) -> Foo (if b then Zero else Succ Zero)' | 03/03 12:47 |

npouillard | and the types of the stdlib for Nat is ℕ with zero and suc as constructors | 03/03 12:47 |

ski | hm, i might be able to do something like that | 03/03 12:49 |

ski | (i thought i had to have the eliminator "around" the return type, but maybe i don't actually) | 03/03 12:49 |

ski | i'm trying to define a variant of equality, where you can state the equality of two terms of possibly different types in `Set', but where the constructor takes a proof that the two types are actually equal | 03/03 12:50 |

ski | so i was trying to eliminate the equality proof in the constructor type .. | 03/03 12:51 |

npouillard | is this related to John Major equality? | 03/03 12:53 |

ski | yes .. i'm trying out variants of it | 03/03 12:53 |

npouillard | aka Relation.Binary.HeterogeneousEquality | 03/03 12:53 |

HairyDude | hrm. seems importing Level causes unsolved constraints | 03/03 13:19 |

HairyDude | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23205#a23205 | 03/03 13:22 |

HairyDude | also, hiding zero and suc makes the yellow go away | 03/03 13:24 |

HairyDude | apparently agda allows them to be overloaded, so it can't tell they should be constructors of ℕ, despite the type signature | 03/03 13:26 |

dolio | That's odd. | 03/03 13:36 |

HairyDude | in fact, it has no trouble with zero, only suc | 03/03 14:45 |

* ski plays the game "push the level one step upwards, running around in a circle" | 03/03 17:09 | |

--- Day changed Thu Mar 04 2010 | ||

* copumpkin is getting intimate with Algebra.RingSolver | 04/03 04:10 | |

Saizan | copumpkin: hawt | 04/03 06:21 |

appamatto | Wow, are many people here going to the implementor's meeting this month? | 04/03 15:03 |

appamatto | It sounds like fun | 04/03 15:03 |

maltem | Anyone willing to explain about, say, http://code.haskell.org/Agda/examples/lib/Logic/Leibniz.agda to me? I'm trying to make a little more sense of dependent types | 04/03 19:00 |

dolio | What about it? | 04/03 19:01 |

maltem | Upon reading the symmetry proof, I wasn't sure anymore if I even got the definition of _≡_, type-wise | 04/03 19:02 |

maltem | How to understand that a proof is of type Set1, and what does (\z -> P z -> P x) mean? | 04/03 19:03 |

maltem | Maybe the latter is the better question | 04/03 19:03 |

dolio | Set1 is the level above Set. | 04/03 19:03 |

maltem | That's (more or less) clear to me. | 04/03 19:03 |

copumpkin | Set-1 | 04/03 19:03 |

dolio | It's necessary because that definition of == quantifies over Set, essentially, because P : A -> Set. | 04/03 19:04 |

copumpkin | (that's values) | 04/03 19:04 |

maltem | It's what non-logicians call Class. | 04/03 19:04 |

dolio | (\z -> P z -> P x) takes a value of type A, called z, and returns the type P z -> P x | 04/03 19:04 |

maltem | So (P z -> P x) : Set ? | 04/03 19:05 |

dolio | Yes. | 04/03 19:05 |

dolio | Since P : A -> Set | 04/03 19:06 |

dolio | So, what ==-sym does is substitutes the first x in a P x -> P x for a y, giving a P y -> P x. | 04/03 19:06 |

dolio | Which is what you need to reverse the equality. | 04/03 19:07 |

dolio | y == x = (P : A -> Set) -> P y -> P x | 04/03 19:07 |

dolio | It's kind of clever. It's not initially obvious (to me) that you can get away with just having (x == y) just be P x -> P y. | 04/03 19:08 |

maltem | I'm getting closer, let me ponder a little | 04/03 19:08 |

copumpkin | is there a name for replacing "structures" with properties of those structures? | 04/03 19:11 |

copumpkin | this seems similar to representing a list by a fold | 04/03 19:11 |

copumpkin | here you're representing equality by subst | 04/03 19:11 |

maltem | So xy (\z -> P z -> P x) : (P x -> P x) -> (P y -> P x). | 04/03 19:16 |

maltem | Ok so it works out. I'm wondering why I find this to be so hard | 04/03 19:18 |

copumpkin | it's not trivial :) | 04/03 19:18 |

maltem | dolio, when you said "Yes. Since P : A -> Set" is that just a general typing rule? | 04/03 19:20 |

dolio | Yes. The type of (x : A) -> B[x] is computed as... | 04/03 19:21 |

maltem | I mean, that (A -> A) : Set if A : Set | 04/03 19:21 |

dolio | If A : SetM, and B[x] : SetN, then (x : A) -> B[x] : Set(max M N) | 04/03 19:22 |

dolio | And A -> B is a special case, where B doesn't depend on x. | 04/03 19:22 |

maltem | Is B[x] meta-notation for a type that mentions x? | 04/03 19:22 |

maltem | Or is it Agda syntax? | 04/03 19:23 |

dolio | Meta-notation. | 04/03 19:23 |

dolio | I used to write (x : A) -> B, but someone complained at me that it isn't clear that x may be used in B. | 04/03 19:23 |

maltem | Ok, so your notation explicitly conveys that this is allowed to be a dependently typed function | 04/03 19:25 |

dolio | That was my intention. | 04/03 19:25 |

dolio | B is some expression, in which x is in scope, that must have a type SetN for some N. | 04/03 19:25 |

maltem | Thanks for your explanations, I start to get the hang of this - and am determined to take the Mathematical Logics II course ;) | 04/03 19:27 |

guerrilla | maltem: thanks for brining the above up btw :) apparently wikipedia has a pretty good expalanation of this stuff as well. check it out: http://en.wikipedia.org/wiki/Equality_%28mathematics%29 | 04/03 20:45 |

guerrilla | even more detail in http://en.wikipedia.org/wiki/Leibniz%27s_law | 04/03 20:47 |

maltem | guerrilla, heh, yeah notions of equality are interesting on their own | 04/03 20:47 |

guerrilla | especially in TT | 04/03 20:48 |

maltem | TT? | 04/03 20:48 |

guerrilla | type theory | 04/03 20:48 |

maltem | of course :) | 04/03 20:48 |

maltem | guerrilla, technically, yes. | 04/03 21:06 |

maltem | Another question: in lib/Logic/Relations.agda, a relation on a set A is defined to be a function A -> A -> Set. What does "Set" do here? | 04/03 21:11 |

maltem | I would have expected A -> A -> Bool or somesuch. | 04/03 21:11 |

copumpkin | Set is a type-level Bool :) | 04/03 21:12 |

ccasin | maltem: if it were A -> A -> Bool, the relation would have to be decidable | 04/03 21:12 |

copumpkin | the empty set is false | 04/03 21:12 |

copumpkin | the set with one item is true (as are any other sets, but one item carries no other information) | 04/03 21:12 |

guerrilla | why don't we use a specific type that can only be inhabited by \top (or True if you like)? | 04/03 21:13 |

guerrilla | (say.. Prop) | 04/03 21:13 |

guerrilla | seems like that would be clearer. but i assume that has other issues.. right? | 04/03 21:13 |

copumpkin | guerrilla: we do? | 04/03 21:13 |

maltem | ccasin, why needn't it be decidable with this Set encoding? | 04/03 21:14 |

copumpkin | Data.Unit and Data.Empty contain our true and our false | 04/03 21:14 |

maltem | I presume there's a way to check if a set is empty? | 04/03 21:15 |

copumpkin | not really, nope | 04/03 21:15 |

ccasin | maltem: think of it this way. The relation is associates a type with each pair of As. Then, you give a proof that a particular pair is in the relation by showing that type is inhabited | 04/03 21:15 |

ccasin | "The relation associates" rather | 04/03 21:15 |

guerrilla | copumpkin: yeah, but i mean.. both \top and Nat inhabit Set (for example). why not have a type that is only inhabited by \top | 04/03 21:15 |

ccasin | no, there isn't a way to check if a set is empty. That's like asking if a theorem is provable | 04/03 21:16 |

ccasin | not decidable | 04/03 21:16 |

copumpkin | maltem: that's why Bool would show it's decidable | 04/03 21:16 |

maltem | Ah, I "forgot" that Set is not in any way a computable model of sets | 04/03 21:16 |

copumpkin | if you can provide a true/false, that's a proof | 04/03 21:17 |

maltem | That makes sense now. | 04/03 21:17 |

copumpkin | I meant it's a proof of Bool, which carries more information than a proof of \top | 04/03 21:18 |

maltem | But now I must ask myself guerrilla's question, too. | 04/03 21:19 |

copumpkin | so a universe of true/false types? | 04/03 21:19 |

* copumpkin tries to think how that would work | 04/03 21:19 | |

dolio | Prop in Coq is like that, sort of. | 04/03 21:20 |

guerrilla | dolio: yeah i thought so... | 04/03 21:20 |

dolio | Or any theory with proof irrelevance. | 04/03 21:21 |

guerrilla | just like Prop : Set1 and then \top : Prop (and allow nothing else in it).. | 04/03 21:21 |

maltem | copumpkin, yeah and that in turn would raise the question what makes this universe so special that we should have it, but not certain others :) | 04/03 21:21 |

copumpkin | I think agda used to even have a Prop | 04/03 21:21 |

copumpkin | maybe agda 1? | 04/03 21:21 |

guerrilla | copumpkin: yeah, i did see that in old code, i think | 04/03 21:22 |

guerrilla | so.. why is it gone? | 04/03 21:22 |

guerrilla | :) | 04/03 21:22 |

dolio | Agda 2 has Prop, too, but it isn't proof irrelevant. It's just like an extra Set. | 04/03 21:22 |

copumpkin | ah | 04/03 21:22 |

guerrilla | ok | 04/03 21:22 |

guerrilla | hmmf | 04/03 21:22 |

copumpkin | :) | 04/03 21:22 |

maltem | Let's see, if I define Rel : Set -> ?; Rel A = A -> A -> Prop then what would ? be? | 04/03 21:22 |

copumpkin | Set1? | 04/03 21:23 |

copumpkin | Rel A = A -> Set | 04/03 21:23 |

copumpkin | oh | 04/03 21:23 |

copumpkin | sorry :) | 04/03 21:23 |

maltem | I mean, due to the "-> Prop" I suppose I would have to learn another typing rule | 04/03 21:24 |

guerrilla | maltem: not really necc. since we have universes | 04/03 21:26 |

guerrilla | i think | 04/03 21:26 |

maltem | ah I missed that Prop : Set1 | 04/03 21:27 |

guerrilla | yeah | 04/03 21:27 |

maltem | so indeed ? = Set1 | 04/03 21:27 |

guerrilla | and btw, since we seem to be in the same boat. i should off you a couple of tips i've found useful in the last couple of days.. use lib-0.2 for reading (even though universes are pretty straght forward to me, i think the code is cleaner) and also.. old Agda and even Alfa code has way more comments :) | 04/03 21:28 |

guerrilla | Set : Set1 | 04/03 21:28 |

guerrilla | and btw Set = Set0 | 04/03 21:28 |

guerrilla | Set1 : Set2 | 04/03 21:28 |

guerrilla | and so on | 04/03 21:28 |

guerrilla | so that we don't have the paradox of having a set that contains all sets (Russel) | 04/03 21:29 |

guerrilla | (among other issues?) | 04/03 21:29 |

maltem | Ah a very valuable tip, I wasn't even aware that there's a seperate lib | 04/03 21:31 |

guerrilla | yeah, lib-0.3 makes heavy use of universe quantification.. e.g instead of Set0 or Set1, it uses Set a and Set (succ a) | 04/03 21:32 |

maltem | Ah ok, so the notations gets a little heavier | 04/03 21:33 |

guerrilla | someone should write a book about the lib :) seems like a lot of cool stuff has been figured out, but not much explaining as to why things are they way that they are in it | 04/03 21:33 |

guerrilla | maltem: yeah, just more stuff to keep track of | 04/03 21:33 |

maltem | Wow how do you people read the unicodified sources? Do you keep adjusting your terminal font size? ;) | 04/03 21:33 |

guerrilla | monospace? | 04/03 21:39 |

guerrilla | gnome-terminal and monospace for me anyway | 04/03 21:39 |

maltem | yeah for me that means that either fancy symbols are too small, or ordinary letters are too large | 04/03 21:41 |

guerrilla | odd | 04/03 21:43 |

--- Log closed Fri Mar 05 12:46:07 2010 | ||

--- Log opened Fri Mar 05 12:46:14 2010 | ||

-!- Irssi: #agda: Total of 26 nicks [0 ops, 0 halfops, 0 voices, 26 normal] | 05/03 12:46 | |

-!- Irssi: Join to #agda was synced in 74 secs | 05/03 12:47 | |

guerrilla | is there a difference between symbol \forall and the keyword "forall" in Agda? | 05/03 13:54 |

npouillard | guerrilla: AFAIK no | 05/03 13:55 |

guerrilla | hmm ok | 05/03 13:55 |

dolio | \forall used to not be a keyword. | 05/03 14:53 |

dolio | Same with \lambda. | 05/03 14:53 |

appamatto | Has there been any news about the AIM meeting in Japan? | 05/03 15:06 |

MissPiggy | epigra mtime | 05/03 21:10 |

MissPiggy | epigram time | 05/03 21:10 |

MissPiggy | I wish there was more stuff in /test because that's all I really have to figure out how to use this thing :/ | 05/03 22:26 |

roconnor | on http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes it says at the bottom: | 05/03 22:35 |

roconnor | codata ∞ (T : Set) : Set where | 05/03 22:35 |

roconnor | ♯_ : T → ∞ T | 05/03 22:35 |

roconnor | but this isn't even a recursively defined type. | 05/03 22:35 |

roconnor | ∞ appears to me to be just the identity type constructor | 05/03 22:35 |

roconnor | this can't be right | 05/03 22:35 |

glguy | What were you trying to do? | 05/03 22:36 |

roconnor | understand that wiki page | 05/03 22:36 |

glguy | You define your coinductive data types as normal data types with the co-inductive fields using ∞ | 05/03 22:37 |

glguy | so that you can have data-types that are inductive in some components and co-inductive in others.. | 05/03 22:37 |

glguy | I don't understand it all that well, myself, but I think I get the idea | 05/03 22:37 |

roconnor | inf : Coℕ | 05/03 22:38 |

roconnor | inf = suc (♯ inf) | 05/03 22:38 |

roconnor | what makes this well defined? | 05/03 22:38 |

glguy | You can't case on the ♯, for one | 05/03 22:38 |

glguy | so you can't do structural recursion on that | 05/03 22:38 |

roconnor | oh | 05/03 22:38 |

roconnor | this is so bizarre (coming from the coq world) | 05/03 22:39 |

roconnor | ♭ : ∀ {T} → ∞ T → T | 05/03 22:39 |

roconnor | ♭ (♯ x) = x | 05/03 22:39 |

roconnor | that looks like case analysis to me | 05/03 22:39 |

roconnor | it isn't *dependent* case analysis, but it is still case analysis | 05/03 22:40 |

* roconnor tries reading http://article.gmane.org/gmane.comp.lang.agda/633 | 05/03 22:41 | |

roconnor | whoa | 05/03 22:42 |

roconnor | what the heck is ~ ? | 05/03 22:42 |

codolio | It doesn't exist anymore. | 05/03 22:42 |

glguy | 633 says "This type comes with a destructor, which is the only function which is | 05/03 22:42 |

glguy | allowed to pattern match on ♯_:" | 05/03 22:42 |

codolio | It used to denote corecursive definitions. | 05/03 22:42 |

roconnor | ok | 05/03 22:43 |

codolio | Now 'inf = suc (# inf)' is internally translated to something similar to an auxiliary corecursive definition, or something like that. | 05/03 22:43 |

roconnor | but I'm left wondering why inf is well defined | 05/03 22:43 |

roconnor | codolio: why is it translated to anything corecursive since the input and ouput types are data types? | 05/03 22:44 |

* roconnor keeps reading | 05/03 22:45 | |

codolio | Because it involves a fixed point involving codata, I guess. | 05/03 22:45 |

roconnor | I guess | 05/03 22:45 |

codolio | I think the current situation is a bit odd with respect to the theory you'd expect to base it on. | 05/03 22:45 |

roconnor | ya | 05/03 22:46 |

codolio | codata 'infects' data in an unusual way. | 05/03 22:46 |

roconnor | in coq a consiductive definition of ∞ would be isomorphic to the inductive definiton of ∞ which would be isomorphic to (fun X:Type -> X) | 05/03 22:46 |

roconnor | so I guess codata means something ... strange | 05/03 22:47 |

codolio | Which leads to NAD's stuff about (co)data being unable to represent mu-nu fixed points. | 05/03 22:48 |

roconnor | but nu-mu is okay? | 05/03 22:48 |

codolio | If you try to represent a mu-nu, it will end up as a nu-mu instead. | 05/03 22:49 |

roconnor | wow | 05/03 22:50 |

roconnor | what a mess | 05/03 22:50 |

roconnor | but that's okay | 05/03 22:50 |

roconnor | this is an open problem :D | 05/03 22:50 |

dolio | At least we don't lose subject reduction. :) | 05/03 22:50 |

roconnor | ya | 05/03 22:50 |

roconnor | I'm no fan of coq's "solution" | 05/03 22:50 |

glguy | roconnor, ok, you can case on sharp, but it doesn't count as structural recursion to the termination checker | 05/03 22:50 |

dolio | I'm pretty sure that's just avoided by flatly disallowing dependent case analysis on coinductives. | 05/03 22:51 |

roconnor | dolio: what is avoided? | 05/03 22:51 |

dolio | Loss of subject reduction. | 05/03 22:51 |

roconnor | sure | 05/03 22:51 |

roconnor | but why then go on with this strange # ∞ stuff? | 05/03 22:52 |

roconnor | Coinductive types are then defined using /data/, but with ∞ annotating | 05/03 22:52 |

roconnor | coinductive arguments (this was suggested by Thorsten Altenkirch): | 05/03 22:52 |

dolio | It allows for mixing coinduction and induction in a single data definition. | 05/03 22:52 |

roconnor | ugh | 05/03 22:52 |

roconnor | Throsten, what did you say? | 05/03 22:53 |

dolio | Which is actually being used currently. | 05/03 22:53 |

roconnor | dolio: it doesn't allow for mixing with my understanding of the definition of ∞. | 05/03 22:53 |

dolio | For NAD's parser combinators, for instance. | 05/03 22:53 |

roconnor | when I see ∞, I just see the identity functor. | 05/03 22:53 |

dolio | Well, it isn't. | 05/03 22:53 |

roconnor | how do I properly read this definition? | 05/03 22:54 |

roconnor | it is a "delayed" constructor? | 05/03 22:54 |

MissPiggy | Thorsten is there ?? | 05/03 22:54 |

dolio | Yes, it's like that. | 05/03 22:54 |

roconnor | that's why inf is allowed | 05/03 22:56 |

dolio | 'data T : ... where con : ... -> ∞ T ... -> ...' allows you to use 'con' in a corecursive definition. | 05/03 22:56 |

dolio | Basically, I think any definition guarded by codata constructors is allowed to be corecursive. | 05/03 22:57 |

dolio | By the productivity checker. | 05/03 22:57 |

roconnor | what are the denotational semantics of Agda's codata? | 05/03 22:57 |

roconnor | it boggles my mind how to define this delay thing | 05/03 22:57 |

dolio | Or, it can be guarded by a combination of codata and data constructors, but the codata has to be in there. | 05/03 22:57 |

dolio | roconnor: In the stuff on mu-nu, they talked about ∞ T being some sort of lifted T in a domain or something. | 05/03 22:59 |

dolio | I think that's right. | 05/03 22:59 |

roconnor | <codolio> If you try to represent a mu-nu, it will end up as a nu-mu instead. | 05/03 23:00 |

roconnor | Right, Coℕ is defined like it is mu-nu but it really is nu-mu | 05/03 23:00 |

roconnor | nu on the nat, and mu on the identy functor ∞ | 05/03 23:01 |

roconnor | wow | 05/03 23:01 |

roconnor | this feels really wrong. | 05/03 23:01 |

dolio | "The corresponding domain-theoretic expressions are μO. μZ. Z_⊥ + O and μZ. μO. Z_⊥ + O, and these are equivalent." | 05/03 23:02 |

roconnor | I'd like to see those semantics worked out | 05/03 23:02 |

dolio | When discussing trying to do μO.νZ.Z + O using agda's codata. | 05/03 23:02 |

roconnor | what about simple νZ.Z+1 ? | 05/03 23:04 |

roconnor | so you are saying Nat is defined as μZ. Z_⊥ + 1 ? | 05/03 23:04 |

roconnor | er | 05/03 23:04 |

roconnor | CoNAt | 05/03 23:04 |

dolio | Yes. | 05/03 23:05 |

roconnor | what is + in domain theory | 05/03 23:06 |

dolio | He's saying that adding ∞ is the same as adding _⊥. | 05/03 23:06 |

roconnor | the domains A and B with a new bottom glued on, or with the two bottoms merged? | 05/03 23:06 |

dolio | I don't really know. | 05/03 23:07 |

roconnor | where is your quote from? | 05/03 23:09 |

dolio | 'Some observations about μν' on the mailing list. | 05/03 23:10 |

roconnor | link? | 05/03 23:10 |

dolio | Is the list archive still not public? It's asking me to log in. | 05/03 23:11 |

roconnor | found it | 05/03 23:12 |

roconnor | http://thread.gmane.org/gmane.comp.lang.agda/952 | 05/03 23:12 |

dolio | It's from last July. | 05/03 23:12 |

dolio | I have to jet, but I'll leave with a query... | 05/03 23:14 |

roconnor | what query? | 05/03 23:15 |

dolio | It's (fairly) easy to show the difference between existentials and sigma types as far as transparency goes by trying to implement signaturs/abstract datatypes. Sigmas let you use certain details of the implementation---if you know which implementation you're using---that existentials would make opaque. | 05/03 23:15 |

dolio | Is there a similar example for parametric, universal types vs. pi types? | 05/03 23:16 |

roconnor | existential means non-dependent elimination? | 05/03 23:16 |

dolio | Yes. I think weak elimination is the key to the abstraction property. | 05/03 23:17 |

dolio | I suppose there's no 'strong' pi eliminator. | 05/03 23:17 |

roconnor | BTW you lose all the information hiding guarentees of existential types if your language also has sigma types | 05/03 23:17 |

roconnor | basically you can tuck in info way in a sigma type and return it. | 05/03 23:17 |

dolio | Right. Luo mentions that, I think. | 05/03 23:18 |

--- Day changed Sat Mar 06 2010 | ||

RLa | in agda you can make recursion step only by single argument? | 06/03 11:09 |

Saizan | no, if i understand correctly | 06/03 11:10 |

Saizan | in the sense that you don't need to recurse on a single argument at a time | 06/03 11:10 |

RLa | i have some nat theory here | 06/03 11:13 |

RLa | and i want to specify associativity of + here | 06/03 11:14 |

RLa | hm, nvm | 06/03 11:14 |

RLa | it looks like complete abuse of types | 06/03 11:16 |

Saizan | you'd have associativity as a separate property | 06/03 11:20 |

Saizan | \all x y z -> (x + y) + z \== x + (y + z) | 06/03 11:20 |

Saizan | it's fairly simple to prove by induction over x, iirc | 06/03 11:21 |

RLa | hm, i need induction over other variables too? | 06/03 11:22 |

RLa | since i do not have yet 0+y = y? | 06/03 11:22 |

Saizan | ah, well, i'd prove that as a lemma | 06/03 11:22 |

Saizan | however you could recurse over y too, if that was needed | 06/03 11:23 |

RLa | yeah, i currently recurse over all of them | 06/03 11:23 |

RLa | i'm now working on commutativity | 06/03 11:24 |

RLa | why would this give the error: http://pastebin.com/acTffsTi | 06/03 11:39 |

Saizan | well because the types don't match.. | 06/03 12:32 |

Saizan | comm+ y y' : y + y' = y' + y | 06/03 12:33 |

Saizan | but you've to provide something of type s y + y' ≡ y' + s y | 06/03 12:33 |

RLa | hm, i have nothing of that type | 06/03 12:38 |

RLa | or do i have to provide something that chops s off from both sides? | 06/03 12:39 |

Saizan | well, from y + y' = y' + y you can derive s (y + y') = s (y' + y) easily | 06/03 12:40 |

Saizan | then you've to prove that s (y' + y) = y' + s y | 06/03 12:40 |

RLa | hm | 06/03 12:44 |

RLa | i have no idea how to do that | 06/03 12:45 |

RLa | or how to express it in agda | 06/03 12:45 |

Saizan | well, you can just have an helper function \all x y -> s (x + y) \== x + s y | 06/03 12:46 |

Saizan | and for the other part you can write another: (A B : Set) -> (f : A -> B) -> {x y : A} -> x \== y -> f x \== f y | 06/03 12:48 |

Saizan | that's usually called cong | 06/03 12:48 |

RLa | well, i have something called cong here, i'm writing def to it at the moment | 06/03 12:49 |

MissPiggy | i RLa! | 06/03 12:57 |

MissPiggy | hi | 06/03 12:57 |

RLa | hey | 06/03 12:57 |

RLa | no, it's not going to work | 06/03 13:04 |

RLa | i'm even unable to write definition for \all x y -> s (x + y) \== x + s y | 06/03 13:07 |

MissPiggy | you must prove x + 0 = 0 + x by induction on x | 06/03 13:11 |

MissPiggy | doing this sort of stuff in agda is very long and difficult | 06/03 13:11 |

RLa | yes, i already know that | 06/03 13:12 |

RLa | anyway, i think i got helper function: http://pastebin.com/7MuVGvpz | 06/03 13:13 |

RLa | but i see no way how it would help me | 06/03 13:14 |

MissPiggy | are you trying to prove x + y = y + x? | 06/03 13:15 |

MissPiggy | on natural numbers | 06/03 13:15 |

RLa | yes | 06/03 13:21 |

RLa | i have problem with case comm+ (s y) (s y') | 06/03 13:24 |

MissPiggy | I would say that if you defined 0 + y = 0 & S x + y = S (x + y) then to show x + y = y + x you can split it into two cases 0 + y = y + 0 & S x + y = y + S x but the second one reduces to* S (x + y) = y + S x | 06/03 13:27 |

MissPiggy | (*if A reduces to B then a proof of A is a proof of B) | 06/03 13:27 |

Saizan | you've redundant cases in your commHelp btw | 06/03 13:27 |

RLa | hm | 06/03 13:29 |

MissPiggy | rewriting the induction hypothesis onto that gives S (y + x) = y + S x, so you need a lemma that proves you can rip S through a + like this: S (y + x) = y + S x, which will come by induction on y | 06/03 13:33 |

MissPiggy | (the S case gives you something like S (S (y + x)) = S (y + S x), which you use the induction hypothesis to rewrite the right hand side into S (S (y + x))) | 06/03 13:34 |

RLa | i do not get which cases are reduntant in my commHelp | 06/03 13:34 |

RLa | S x + y = y + S x but the second one reduces to S (x + y) = y + S x <- what does mean? | 06/03 13:35 |

MissPiggy | S x + y = y + S x | 06/03 13:36 |

MissPiggy | reduces to | 06/03 13:36 |

MissPiggy | S (x + y) = y + S x | 06/03 13:36 |

MissPiggy | because of the definition of + | 06/03 13:36 |

RLa | hm, i see | 06/03 13:36 |

MissPiggy | so what that means is, to prove "S x + y = y + S x" you need to prove "S (x + y) = y + S x" | 06/03 13:36 |

MissPiggy | another example of this is, 1 + 1 reduces to 2 .. obviously! | 06/03 13:37 |

MissPiggy | so you can prove 1 + 1 = 2 by proving 2 = 2 | 06/03 13:37 |

MissPiggy | so it's just reflexivity | 06/03 13:37 |

MissPiggy | that might seem like a boring example, but you can take this technique and turn it into something really powerful | 06/03 13:37 |

RLa | can i use numbers instead of (s y) stuff? | 06/03 13:38 |

MissPiggy | well you could write 1+ instead of S | 06/03 13:38 |

MissPiggy | it's all the same though | 06/03 13:38 |

RLa | ok, i have both S (y + x) = y + S x and 0 + y = y + 0, how do i combine them into comm+? | 06/03 13:41 |

MissPiggy | like I said before to show x + y = y + x it makes sense to split it into cases (by induction), so you have 0 + y = y + 0 (that's already been proved) and the other case reduces to S (x + y) = y + S x -- so just rewrite the induction hypothesis to get S (y + x) = y + S x which has already been proved | 06/03 13:45 |

RLa | ok, this is my case for 0 + y = y + 0: comm+ z y = comm+' y, where comm+' is ∀ n → 0 + n ≡ n + 0 | 06/03 13:47 |

RLa | but for comm+ (s y) y' i have no idea how to make it use comm+'' : ∀ x y → s (x + y) ≡ x + (s y) | 06/03 13:48 |

RLa | i'm missing something important here | 06/03 13:48 |

Saizan | well, you have to recurse | 06/03 13:48 |

Saizan | do you have transitivity? | 06/03 13:49 |

MissPiggy | comm+ : forall x y, x + y = y + x ? I assume | 06/03 13:49 |

RLa | yes | 06/03 13:49 |

MissPiggy | then comm+ (s y) y' : (s x) + y' = y' + (s x) | 06/03 13:49 |

MissPiggy | and comm+ (s y) y' : s (x + y') = y' + (s x) | 06/03 13:49 |

RLa | Saizan, no, transitivity went wrong and i do not have code for that | 06/03 13:49 |

MissPiggy | the induction hypothesis gives you x + y' = y' + x thought, | 06/03 13:49 |

MissPiggy | so you can whack the lemma (s (y' + x) = y' + (s x)) with the induction hypothesis to conclude the comm+ (s y) y' case | 06/03 13:50 |

MissPiggy | induction gives you x + y' = y' + x | 06/03 13:51 |

Saizan | RLa: transitivity should just be a matter of pattern matching on the arguments and using triv | 06/03 13:52 |

RLa | Saizan, apparently it's not, agda wants to put some lambdas in my definitions and i have no idea what to do with them | 06/03 13:53 |

Saizan | trans : {A : Set} (x y z : A ) -> x \== y -> y \== z -> x \== z; trans triv triv = triv -- assuming triv is the constructor for your \== | 06/03 13:54 |

Saizan | oops | 06/03 13:54 |

Saizan | trans : {A : Set} {x y z : A} -> x \== y -> y \== z -> x \== z | 06/03 13:54 |

MissPiggy | Saizan, \== meaning not equal? | 06/03 13:55 |

MissPiggy | oh.... | 06/03 13:55 |

MissPiggy | this is quail notation for the unicode equals sign | 06/03 13:55 |

MissPiggy | im usedto \== for not equal form porolog | 06/03 13:55 |

Saizan | yeah, i'm not sure why i use the latex notation here on irc :) | 06/03 13:55 |

Saizan | s/latex/what the agda-mode accepts/ | 06/03 13:56 |

RLa | then comm+ (s y) y' : (s x) + y' = y' + (s x) <- is that actual syntax? | 06/03 13:58 |

RLa | shouldn't i use helper function here somehow? | 06/03 13:59 |

RLa | also, what is difference between function signatures trans : {A : Set} (x y z : A ) -> ... and \forall x y z -> ...? | 06/03 14:02 |

Saizan | comm+ (s y) y' = trans (cong s (comm+ y y')) (commHelp y' y) -- should be | 06/03 14:02 |

Saizan | RLa: that the latter is not polymorphic on the type of those x y z, but it's not specifying a type either | 06/03 14:03 |

Saizan | unless your \== is defined only on naturals | 06/03 14:03 |

RLa | i have all functions using \forall | 06/03 14:04 |

RLa | yes, it's only on nat | 06/03 14:04 |

Saizan | how is it defined? | 06/03 14:04 |

Saizan | however, \forall a b c -> .. is the same as (a b c : _) -> ... | 06/03 14:05 |

Saizan | i.e. you're asking the typechecker to infer the type | 06/03 14:05 |

RLa | http://pastebin.com/zDdGS56g | 06/03 14:05 |

RLa | hm, i did not know that | 06/03 14:05 |

Saizan | ooh | 06/03 14:05 |

RLa | those definitions look ok? | 06/03 14:06 |

Saizan | well, that \== is not what i expected | 06/03 14:06 |

RLa | hm, i see, i already looked at many agda examples and they all do things differently | 06/03 14:07 |

Saizan | now i see why your commHelp definition works | 06/03 14:07 |

Saizan | (i was puzzled before :) | 06/03 14:07 |

Saizan | i guess you've to define transitivity by pattern matching on the x y z then | 06/03 14:08 |

RLa | yes, that's where trouble came in | 06/03 14:08 |

RLa | it seems to want some extra data | 06/03 14:08 |

Saizan | well, trans would have 5 arguments | 06/03 14:09 |

RLa | but where those extra 2 come from? | 06/03 14:09 |

RLa | or what gives value for them | 06/03 14:10 |

Saizan | "x \== y" and "y \== z" count as arguments | 06/03 14:10 |

RLa | but what evaluates them? | 06/03 14:12 |

RLa | or should i completely ignore them? | 06/03 14:12 |

RLa | and use results of pattern matching? | 06/03 14:12 |

Saizan | ah, btw, \forall a b c -> ... is actually (a : _) (b : _) (c : _) -> .., i.e. they can be of different types | 06/03 14:12 |

Saizan | well, you can ignore them when those equalities will reduce to True, since pattern matching on triv doesn't give any useful information | 06/03 14:13 |

Saizan | when the equality reduces to False instead you should use an absurd pattern for them | 06/03 14:14 |

Saizan | so that you can avoid writing a body for that that branch | 06/03 14:14 |

Saizan | e.g. "trans z (s _) _ () _" <- this means "if x = z and y = s _; then you can't tell me x \== y", roughly | 06/03 14:15 |

RLa | hm, it does not let me use those extra arguments in pattern matching at all | 06/03 14:16 |

RLa | e.g requires me to return a function | 06/03 14:17 |

Saizan | you can't pattern match on them until you pattern match enough of the nat arguments to make their type reduce to either True or False | 06/03 14:17 |

Saizan | that's odd. | 06/03 14:17 |

Saizan | can you paste? | 06/03 14:17 |

Saizan | oh, duh, we can't use z as a variable name. | 06/03 14:19 |

RLa | ok, for example: trans≡ z z z = λ triv triv → triv | 06/03 14:20 |

RLa | this seems fine case | 06/03 14:20 |

Saizan | yeah | 06/03 14:22 |

Saizan | but you should also be able to write trans\== z z z triv triv = triv, if you also write all other cases with 5 arguments | 06/03 14:22 |

Saizan | http://pastebin.com/7XL3SC5X <- eg | 06/03 14:23 |

appamatto | Have there been any applications written in Agda? | 06/03 14:24 |

RLa | duh, i tried to write triv as pattern | 06/03 14:26 |

RLa | therefore it did not work | 06/03 14:26 |

MissPiggy | did you get +comm done yet? | 06/03 14:27 |

RLa | no, i'm working on trans | 06/03 14:28 |

RLa | () as a pattern means that such case should be never possible? | 06/03 14:29 |

Saizan | yeah | 06/03 14:29 |

MissPiggy | what's trans got to do with this? | 06/03 14:32 |

MissPiggy | here is this proof in coq http://pastie.org/857132 | 06/03 14:32 |

Saizan | well, don't you need trans to chain the inductive hypothesis and s (y' + x) = y' + (s x) ? | 06/03 14:33 |

Saizan | it's how i'd write it, anyway | 06/03 14:33 |

MissPiggy | Saizan, it's actally S (S (y' + x)) = S (y' + (S x)) isn't it? So you have to rewrite | 06/03 14:34 |

MissPiggy | no you are right, transitivity works too | 06/03 14:34 |

RLa | i'm defining cong now | 06/03 14:41 |

RLa | trying to do same way as trans | 06/03 14:41 |

Saizan | cong is actually not needed here | 06/03 14:42 |

Saizan | since "s x \== s y" reduces to "x \== y" with your definition | 06/03 14:43 |

RLa | "reduces to" <- how is reduction defined here? | 06/03 14:44 |

Saizan | well, as the normal evaluation rules, given the definition of \== | 06/03 14:46 |

Saizan | since you've defined "s m ≡ s n = m ≡ n" | 06/03 14:47 |

RLa | here is my cong: http://pastebin.com/5qB98ceF | 06/03 14:57 |

RLa | i now go back to comm | 06/03 14:58 |

Saizan | nice :) | 06/03 14:58 |

Saizan | you won't need that cong here | 06/03 14:58 |

appamatto | What ghc are you guys using? I am compiling with 6.10.4, and I'm having problems with dependency conflicts | 06/03 15:19 |

Saizan | i'm on ghc-6.12 | 06/03 15:19 |

appamatto | I think I'll upgrade | 06/03 15:21 |

RLa | i'm still working on commutativity | 06/03 16:26 |

RLa | what does conc stand for? | 06/03 16:26 |

Saizan | conc? | 06/03 16:28 |

RLa | cong* | 06/03 16:34 |

Saizan | not sure actually | 06/03 16:35 |

RLa | i think that my definition of cong is not usable | 06/03 16:36 |

Saizan | you don't need it for commutativity, anyhow | 06/03 16:36 |

Saizan | http://pastebin.com/pXs2S2sS | 06/03 16:36 |

RLa | hm, move-s is same as my commHelper | 06/03 16:39 |

Saizan | yeah | 06/03 16:40 |

RLa | hm, if program compiles, it must be correct? | 06/03 16:42 |

RLa | it compiles, but i still do not understand that trick with using trans | 06/03 16:42 |

Saizan | well, it's not like you can run comm+ to get something computationally interesting :) | 06/03 16:42 |

Saizan | ah, well | 06/03 16:43 |

RLa | hehe :D | 06/03 16:43 |

RLa | so primitive proofs in simple arithmetics should be not so complex | 06/03 16:44 |

Saizan | you've comm+ x y which is of type x + y == y + x, which is the same as s (x + y) == s (y + x), which is the same as s x + y == s (y + x) | 06/03 16:45 |

Saizan | then you use move-s to tell that s (y + x) == y + s x | 06/03 16:45 |

Saizan | combining with transitivity you get s x + y = y + s x, which is what you wanted to prove | 06/03 16:46 |

Saizan | you can automate proof strategies by reflection, like in the RingSolver module | 06/03 16:46 |

RLa | i will look into that | 06/03 16:47 |

RLa | i think i have problem that i do not understand how agda prove procedure works | 06/03 16:48 |

RLa | anyway, big thanks for help | 06/03 16:50 |

Saizan | np | 06/03 16:51 |

Saizan | the first thing is that equality over terms is basically defined by evaluation | 06/03 16:52 |

MissPiggy | "if program compiles, it must be correct?" -- no :P | 06/03 16:53 |

MissPiggy | you just know that it satisfies its type | 06/03 16:53 |

MissPiggy | but you can sometimes express correctness in the type, or prove it afterwards | 06/03 16:53 |

RLa | is evaluation in agda like beta-reduction in lambda calculus? | 06/03 16:54 |

Saizan | though it's evaluation in an open context, so it gets stuck on free variables, pattern matching makes it go further | 06/03 16:54 |

Saizan | yeah | 06/03 16:54 |

RLa | are there normal forms etc. too? | 06/03 16:56 |

Saizan | yeah | 06/03 16:56 |

Saizan | the difference with a pure lambda calculus is the addition of constructors | 06/03 16:57 |

MissPiggy | it's beta-reduction + eta-exapansion + unfolding definitions (+ more stuff?) | 06/03 17:00 |

MissPiggy | oh yeah pattern matching | 06/03 17:01 |

RLa | what about recursion? does it restrict construction of fixpoint combinators somehow? | 06/03 17:02 |

Saizan | yes, there's a termination checker | 06/03 17:03 |

MissPiggy | I hujst cannot figure out how to use pig from the test files : | 06/03 17:06 |

RLa | pig? | 06/03 17:07 |

--- Day changed Sun Mar 07 2010 | ||

lpjhjdh | so I have a datatype with only a single constructor and I can't seem to match on it | 07/03 01:17 |

liyang | Paste? | 07/03 01:22 |

liyang | Offer closing in 2 minutes. :p | 07/03 01:23 |

lpjhjdh | ooh, sorry, must run | 07/03 01:23 |

lpjhjdh | thanks though | 07/03 01:23 |

liyang | Likewise. :3 | 07/03 01:23 |

Saizan | i think we should move type inference into the editor, together with folding code capabilities so you don't see the annotated terms unless you want to | 07/03 07:52 |

Saizan | the point is that at that point it could even use partial and/or not so predictable heuristics, because if you want to know what's going on you can always look at the annotations | 07/03 07:57 |

RLa | some of us here use scala for writing wicket apps? | 07/03 11:33 |

RLa | wrong channel | 07/03 11:33 |

RLa | is there a part of agda manual that explains the use of () in pattern matching? | 07/03 12:38 |

Saizan | mh, maybe in some of the tutorials | 07/03 12:42 |

Saizan | otherwise you've to look at the papers :) | 07/03 12:43 |

Saizan | or ask here what's unclear | 07/03 12:43 |

maltem | I find it fun how you can abuse the agda module system in order not to repeat variable names :) | 07/03 16:33 |

npouillard | maltem: still to much to repeat according my taste but... | 07/03 16:34 |

npouillard | *too | 07/03 16:36 |

maltem | npouillard, I suppose http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23308 is an extreme example then. No repitition at all! Of course, using this as a library would probably be just scary | 07/03 16:37 |

Saizan | well, you can get open ... public to export a flat namespace if you want | 07/03 16:41 |

maltem | what does "public" do? | 07/03 16:45 |

Saizan | it makes the current module re-export the symbols of the opened moduel | 07/03 16:57 |

Saizan | it's used a lot in the Algebra records, to give you a "subtyping" feel | 07/03 16:58 |

maltem | mmh ok so I when then using the module I could drop the module qualifiers, and just have long types | 07/03 16:59 |

Saizan | right, which is probably not that nice | 07/03 17:07 |

Saizan | but you could also make a module that takes all the parameters at once and exports everything | 07/03 17:08 |

maltem | right | 07/03 17:09 |

jotik^^ | There is no way to instanciate an element of type "data False : Set where" is there? | 07/03 18:34 |

npouillard | jotik^^: what do you mean by instanciate here? | 07/03 18:35 |

npouillard | but yes there is no value of type False | 07/03 18:35 |

npouillard | otherwise we have a problem | 07/03 18:35 |

jotik^^ | So I can't make any function return anything of type False, correct? | 07/03 18:36 |

jotik^^ | A problem? | 07/03 18:36 |

jotik^^ | nevermind last line. | 07/03 18:36 |

npouillard | jotik^^: you can return a value of type false if you get one as argument | 07/03 18:36 |

npouillard | or if you get some arguments that forms a contradiction and so have all types | 07/03 18:37 |

jotik^^ | I'm trying to prove "trans≡ : ∀ m n o → m ≡ n → n ≡ o → m ≡ o" on natural numbers where _≡_ : Nat -> Nat -> Set (either True or False) | 07/03 18:43 |

npouillard | jotik^^: Set is not just true or false | 07/03 18:44 |

jotik^^ | And I just don't know what to do with the case trans≡ (suc a) zero (suc c) | 07/03 18:44 |

npouillard | trans≡ _ _ _ refl refl = refl | 07/03 18:44 |

jotik^^ | hmm... | 07/03 18:45 |

jotik^^ | What is that supposed to mean (/me agda noob) | 07/03 18:46 |

npouillard | if you want to write it the long way as an exercise you will need the () pattern | 07/03 18:46 |

npouillard | equality is complicated beast | 07/03 18:47 |

jotik^^ | well the shorter the better, but since this is a course assignment I'm not allowed to change any data types nor _≡_ | 07/03 18:48 |

jotik^^ | And I don't understand what you meant by trans≡ _ _ _ refl refl = refl | 07/03 18:49 |

npouillard | but basically pattern matching on refl forces the substitution of n for m and of o for n | 07/03 18:50 |

jotik^^ | but I can't pattern match like that, can I? | 07/03 18:55 |

npouillard | yes you can | 07/03 19:02 |

npouillard | jotik^^: however I've not seen the definiton of _≡_ you use | 07/03 19:02 |

jotik^^ | npouillard: Well here's what I've got: http://agda.pastebin.com/7s3d7qkL | 07/03 19:04 |

npouillard | jotik^^: ok so you have a different version of _≡_ than the propositional one | 07/03 19:06 |

jotik^^ | What would a propositional one look like? | 07/03 19:07 |

jotik^^ | like a type? | 07/03 19:07 |

npouillard | data _≡_ (A : Set) : Set → Set where refl : A ≡ A | 07/03 19:07 |

npouillard | yes | 07/03 19:08 |

npouillard | but you to continue in your direction you will need a function to eliminate False values | 07/03 19:08 |

jotik^^ | Wow I think I already managed with one, by declaring an absurd pattern and using () () | 07/03 19:10 |

npouillard | elim-False : ∀ {A} → False → A | 07/03 19:11 |

npouillard | elim-False () | 07/03 19:11 |

jotik^^ | hmm | 07/03 19:12 |

npouillard | jotik^^: Was the definition of _≡_ fixed in the assignment | 07/03 19:14 |

jotik^^ | If I declare such a function, I get "Sort _55 [ at filename..." What does that mean? | 07/03 19:14 |

jotik^^ | npouillard: yes | 07/03 19:15 |

npouillard | hum ∀ {A : Set} ... | 07/03 19:15 |

jotik^^ | thanks | 07/03 19:22 |

jotik^^ | btw, what do those _somenumber messages mean? | 07/03 20:55 |

jotik^^ | e.g. _59, _60, _61 etc | 07/03 20:55 |

Saizan | jotik^^: they are meta variables introduced by the typechecker for unknowns which couldn't be resolved to something else | 07/03 22:07 |

Saizan | jotik^^: a lot like prolog, if you're familiar with it | 07/03 22:08 |

jotik^^ | not much | 07/03 22:08 |

jotik^^ | bed time for me. Thanks everybody! Good night! | 07/03 22:09 |

--- Day changed Mon Mar 08 2010 | ||

MissPiggy | so they proved tt = ff in epigram?? | 08/03 00:13 |

TacticalGrace | Is the Agda "standard library" include in an install from Hackage (via cabal-install)? | 08/03 05:06 |

copumpkin | nope | 08/03 06:47 |

copumpkin | not as far as I know | 08/03 06:47 |

copumpkin | we need an agda platform :P | 08/03 06:47 |

jotik^^ | I've never succeeded installing anything properly with cabal, including Agda, so I'm keeping as far as possible from cabal. | 08/03 07:42 |

Saizan | for Agda it always worked at the first attempt for me | 08/03 07:44 |

jotik^^ | Didn't work for me, tried multi. Then I tried many times in an emulator under Ubuntu and even succeeded to run it for some time until updating something broke it. | 08/03 07:57 |

jotik^^ | Finally I had to beg gentoo devs for ebuilds which were a work-in-progress. | 08/03 07:57 |

Saizan | ah, i avoid distro packages like the plague, for haskell | 08/03 08:05 |

jotik^^ | Since haskell developers avoid them as well, distro packages are bad. | 08/03 08:50 |

jotik^^ | Haskell packagers are doing a lousy job, the latest stable ghc in gentoo is 6.8.2 | 08/03 08:51 |

jotik^^ | And the usual answers to all questions are "Why don't you use the haskell overlay and ~testing" and "Why don't you use cabal?" | 08/03 08:52 |

Saizan | so you call judgemental equality the one that appears in your typing rules? | 08/03 20:09 |

dolio | Yes. Because it's used in typing judgments. | 08/03 20:24 |

Saizan | i'm not sure i get why you'd need the different formulations of zero to be judgementally equal rather than just propositionally | 08/03 20:27 |

Saizan | it'd make some proofs impossible? | 08/03 20:27 |

dolio | I'm not really sure. | 08/03 20:27 |

dolio | It makes more work, at least. | 08/03 20:28 |

dolio | For instance, if you need a Vec A 0, but that 0 is non-canonical, you have to cast the empty vector to that non-canonical zero via an explicit proof. | 08/03 20:29 |

dolio | Or use a non-canonical empty vector. | 08/03 20:29 |

dolio | I'm not sure if there's more to it than that. | 08/03 20:30 |

Saizan | oh, i think "natInd C zc sc zero = coerce (C zero) (C zero) (resp {f → C (ff ⊲ f)} Ψ) zc" should really be "natInd C zc sc zero = coerce (C zero) (C (ff ⊲ f)) (resp {f → C (ff ⊲ f)} Ψ) zc", so since "coerce X X Q x = x" you need (C zero) = (C (ff ⊲ f)) judgementally to make it progress? | 08/03 20:42 |

dolio | The "coerce X X Q x = x" rule isn't for making progress, if I understand correctly. It's for eliminating work at runtime. | 08/03 20:46 |

Saizan | i thought that was dispensed earlier by saying that epic(?) erases coercions | 08/03 20:48 |

dolio | Coercions between two judgmentally different but provably equal things require you to actually do work 'transporting' the types between the two judgmentally different types. | 08/03 20:48 |

Saizan | yeah | 08/03 20:49 |

Saizan | so in the above case you'd have to expand the coerce if you need to check if the result is equal to something else, rather than just ignoring it | 08/03 20:52 |

dolio | I guess. | 08/03 21:00 |

--- Day changed Wed Mar 10 2010 | ||

copumpkin | is the RingSolver actually being constructive and finding "solutions" or is it just manipulating the equation to show equality? | 10/03 07:52 |

copumpkin | it kind of looks like the latter but it may be more subtle | 10/03 07:53 |

copumpkin | the Reflection module gives me both a prove and a solve based on it | 10/03 07:55 |

copumpkin | but I can't figure out how the solve function is working | 10/03 07:55 |

Saizan | i think the variables are meant as universally quantified | 10/03 08:13 |

guerrilla | so, this is pretty intense: http://arxiv.org/abs/1002.4433 | 10/03 12:30 |

guerrilla | the "Good Math, Bad Math" blog attacks it informally here: http://scienceblogs.com/goodmath/2010/03/grandiose_crankery_cantor_gode.php | 10/03 12:30 |

liyang | copumpkin: reversing the steps of the manipulation starting from refl yields a constructive solution, if you will. | 10/03 12:42 |

liyang | copumpkin: where by manipulation I mean transformation to some normal form. | 10/03 12:43 |

copumpkin | liyang: thanks :) | 10/03 20:26 |

copumpkin | as far as I can understand, the normal form encodes variable identities in the number of up-arrows (and the type) | 10/03 21:11 |

--- Day changed Thu Mar 11 2010 | ||

copumpkin | hmm, trying to convince it to use a proof of mine during pattern matching :/ | 11/03 08:28 |

copumpkin | I guess I'd really need a subst during pattern matching | 11/03 08:29 |

copumpkin | which seems rather hard to convince it to do | 11/03 08:29 |

copumpkin | yay, I just wrote deinterleave : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n | 11/03 08:51 |

copumpkin | way harder than it should be | 11/03 08:51 |

dolio | How does 2 * n compute? 2 * n ==> n + n? | 11/03 08:57 |

copumpkin | n + (n + 0) | 11/03 08:58 |

copumpkin | (sadly) | 11/03 08:58 |

dolio | Well, there's your problem. | 11/03 08:58 |

copumpkin | yep | 11/03 08:58 |

copumpkin | that was kind of my point though | 11/03 08:58 |

copumpkin | not sure if you caught what I was talking about with Saizan in #haskell, but I'm trying to make a "simple" vector DSL that proves silly things like that for you by having a built-in (semi)ring solver (like Algebra.RingSolver) for unification | 11/03 08:59 |

dolio | You're trying to do ring solver in GHC? | 11/03 09:00 |

dolio | Good luck with that. | 11/03 09:00 |

copumpkin | well, not as part of GHC, just as a separate mini language with its own parser, etc. | 11/03 09:00 |

copumpkin | that emits haskell | 11/03 09:00 |

dolio | Oh, okay. | 11/03 09:00 |

dolio | That's slightly more sane. | 11/03 09:01 |

copumpkin | :P | 11/03 09:01 |

copumpkin | just as an experiment to see if I can provide a nice interface to vector that provides static guarantees without making programmers go insane | 11/03 09:01 |

copumpkin | (and I'd like it to spit out to agda too, just so you don't have to trust me too much) | 11/03 09:02 |

copumpkin | of course, I won't have a proof that the agda output is equivalent to the haskell output, but whatever, I'm just trying to make this stuff more attractive to joe haskell | 11/03 09:03 |

dolio | Joe 6-monads. | 11/03 09:07 |

copumpkin | lol | 11/03 09:07 |

copumpkin | gotta love things like suc (n + (n + 0)) != n + suc (n + 0) of type ℕ | 11/03 09:13 |

dolio | That's the price you pay for decidable typing. | 11/03 09:15 |

copumpkin | yep | 11/03 09:15 |

dolio | I wonder how much better stuff like NuPRL actually does at that. | 11/03 09:16 |

dolio | Can it figure out that those two things are equal? | 11/03 09:16 |

copumpkin | haven't tried it | 11/03 09:16 |

copumpkin | can't seem to fetch it either | 11/03 09:18 |

copumpkin | ahem: "Build proof assistants that are as indispensible to programmers and mathematicians as word processors are now." | 11/03 09:20 |

dolio | Was that supposed to be serious? | 11/03 09:21 |

copumpkin | looks like it: http://www.cs.cornell.edu/Info/Projects/NuPRL/Intro/intro.html | 11/03 09:21 |

kmc | it's a nice idea, but the lead time on ideas from programming language theory getting into industry seems to be about 50-70 years | 11/03 09:32 |

copumpkin | well part of the goal of my project to make (a tiny subset) this stuff more accessible to the masses and to attract more interest :P | 11/03 09:35 |

copumpkin | if I can get a few more people interested in agda I'll feel satisfied | 11/03 09:35 |

copumpkin | I just wrote another deinterleave₂ : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n | 11/03 09:35 |

copumpkin | implemented in a different (less efficient) manner | 11/03 09:35 |

copumpkin | pretty exciting stuff | 11/03 09:36 |

Saizan | all using RingSolver? | 11/03 09:37 |

copumpkin | yep | 11/03 09:37 |

Saizan | how does it look? | 11/03 09:37 |

copumpkin | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23891#a23891 | 11/03 09:37 |

copumpkin | the ringsolver for the second one was pretty trivial | 11/03 09:38 |

copumpkin | but as long as it can do it, I'm happy :) | 11/03 09:38 |

Saizan | nice | 11/03 09:44 |

Saizan | well, it could be nicer.. | 11/03 09:44 |

copumpkin | yeah :P | 11/03 09:44 |

copumpkin | my proofs are always butt-ugly | 11/03 09:44 |

copumpkin | but those are the two "obvious" ways of writing deinterleave | 11/03 09:45 |

copumpkin | that I could think of anyway | 11/03 09:45 |

Saizan | oh, i meant because of the obvious limitations of agda, no idea if you can write it better | 11/03 09:46 |

copumpkin | I'd like my tool to support writing both of those with as little code noise as possible | 11/03 09:46 |

copumpkin | pairs (x:y:zs) = (x,y) : pairs zs :P | 11/03 09:46 |

copumpkin | like in mmorrow's original version | 11/03 09:46 |

copumpkin | I was particularly frustrated with writing that function in agda | 11/03 09:47 |

copumpkin | I could've probably used the solver to rewrite it immediately to a suc (suc ...) form | 11/03 09:47 |

copumpkin | I'm pretty impressed with how general solve is | 11/03 09:53 |

copumpkin | but the type in the source file is effectively useful | 11/03 09:53 |

copumpkin | useless, even | 11/03 09:53 |

Saizan | n-ary functions seem to have that property.. | 11/03 09:55 |

copumpkin | yeah | 11/03 09:55 |

dolio | Isn't the obvious solution to cast to a Vec a (n * 2), and then deinterleave that? | 11/03 09:57 |

copumpkin | let me try that :) | 11/03 09:59 |

copumpkin | it typechecks but doesn't termination check | 11/03 10:02 |

copumpkin | the most obvious thing, anyway | 11/03 10:02 |

copumpkin | oh | 11/03 10:02 |

copumpkin | I'm doing it wrong | 11/03 10:02 |

copumpkin | there, it worked :) | 11/03 10:02 |

copumpkin | http://snapplr.com/mf6q | 11/03 10:03 |

copumpkin | obvious in retrospect :P | 11/03 10:03 |

copumpkin | but anyway, my point is still that Joe 6-Monads doesn't and shouldn't have to care about which parameter _*_ is recursing on | 11/03 10:05 |

copumpkin | and obviously I'm still pretty close to him if I didn't think of that simple solution :) | 11/03 10:06 |

Saizan | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23898#a23898 <- cute, but pretty CPU intensive to typecheck | 11/03 10:07 |

* copumpkin still has never used rewrite | 11/03 10:07 | |

Saizan | oh, i thought you wanted to use 2 * n to intentionally complicate things | 11/03 10:08 |

copumpkin | no, I'm just stupid :) | 11/03 10:08 |

copumpkin | but yes, I'll claim it was for that reason too | 11/03 10:08 |

Saizan | rewrite is just a shorthand for the usual with dance | 11/03 10:09 |

copumpkin | I see :) | 11/03 10:09 |

liyang | Rewrite isn't quite as general as the usual with p … | refl = ? dance… | 11/03 21:37 |

liyang | Rewrite is literally that—a rewrite of the LHS of == with the RHS, while matching on refl may reveal more information. | 11/03 22:15 |

Saizan | yeah, though i've found my use cases were covered quite nicely by rewrite | 11/03 22:16 |

--- Day changed Fri Mar 12 2010 | ||

* Mathnerd314 sees #agda | 12/03 03:49 | |

copumpkin | :) | 12/03 03:49 |

Mathnerd314 | seems pretty quiet compared to #haskell | 12/03 03:49 |

copumpkin | yeah :P | 12/03 03:49 |

* Mathnerd314 runs away to take his first shower in weeks | 12/03 03:50 | |

Mathnerd314 | so, how do I write functions in agda? | 12/03 04:05 |

copumpkin | same way as haskell :) | 12/03 04:06 |

copumpkin | but you don't have type inference in most cases | 12/03 04:06 |

copumpkin | open import Data.Nat; f : \bn \r \bn; f x = x + 1 | 12/03 04:07 |

copumpkin | tada | 12/03 04:07 |

copumpkin | you'll need a module X where at the top | 12/03 04:07 |

copumpkin | then do C-c C-l (as in liposuction) | 12/03 04:07 |

copumpkin | and it should turn colorful | 12/03 04:07 |

copumpkin | that \bn types a blackboard N for naturals by the way | 12/03 04:10 |

copumpkin | \r is a pretty -> | 12/03 04:10 |

copumpkin | but -> works too | 12/03 04:10 |

Mathnerd314 | do I need semicolons? | 12/03 04:11 |

Mathnerd314 | O | 12/03 04:11 |

Mathnerd314 | I'm getting a "missing body" error :-/ | 12/03 04:11 |

copumpkin | nope, I just wanted to separate lines | 12/03 04:12 |

Mathnerd314 | is there an agda pastebin? | 12/03 04:13 |

copumpkin | not really, we just use hpaste | 12/03 04:13 |

Mathnerd314 | maybe you should paste what you mean then. | 12/03 04:14 |

Mathnerd314 | agda needs better error messages ;-) | 12/03 04:14 |

copumpkin | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23916#a23916 | 12/03 04:16 |

Mathnerd314 | it seems to eat up all my CPU when I try to compile :-( | 12/03 04:18 |

copumpkin | it's typechecking the standard library dependencies | 12/03 04:18 |

copumpkin | from Data.Nat | 12/03 04:18 |

copumpkin | it will be a lot quicker once it's done that | 12/03 04:18 |

Mathnerd314 | where does it store those typechecks? | 12/03 04:19 |

copumpkin | in .agdai files of the same name | 12/03 04:19 |

copumpkin | like .hi files in haskell | 12/03 04:19 |

Mathnerd314 | so if I delete .agdai files... my CPU burns up next compile? | 12/03 04:20 |

copumpkin | well, if you delete all the .agdai files in your standard library and then need the modules whose agdai files you deleted | 12/03 04:20 |

copumpkin | then it'll have to recheck them | 12/03 04:20 |

copumpkin | your own modules are unlikely to be as complex as the standard library's ones | 12/03 04:21 |

copumpkin | so deleting your own .agdai files won't be too painful | 12/03 04:21 |

* Mathnerd314 sees | 12/03 04:21 | |

Mathnerd314 | seems you don't want to install agda as root, then. | 12/03 04:22 |

Mathnerd314 | anyway... I want Control.Monad and Data.List for my program, right? | 12/03 04:24 |

copumpkin | well | 12/03 04:24 |

copumpkin | you might want to define them yourself and talk about the monad actions on their own | 12/03 04:25 |

copumpkin | agda doesn't have typeclasses :) | 12/03 04:25 |

copumpkin | and you'd need a Data.Colist | 12/03 04:25 |

copumpkin | it might not be a good place to start though | 12/03 04:25 |

copumpkin | I'd start with trying to define some simple functions and proving things about them | 12/03 04:27 |

* Mathnerd314_ hates sudden unexpected reboots | 12/03 04:28 | |

copumpkin | aw | 12/03 04:28 |

copumpkin | http://snapplr.com/tacb | 12/03 04:29 |

copumpkin | there is a Category.Monad and a Data.List | 12/03 04:29 |

copumpkin | but Data.List is only finite lists | 12/03 04:30 |

Mathnerd314 | that IRC client looks cool | 12/03 04:31 |

Mathnerd314_ | ok, Agda is definitely rebooting my system every 10 seconds or so | 12/03 04:36 |

Mathnerd314 | :-/ | 12/03 04:36 |

copumpkin | wow | 12/03 04:36 |

Mathnerd314 | this is why I want to switch to linux or some other *sane* OS | 12/03 04:37 |

Mathnerd314 | it's probably not me, but that all-in-one installer | 12/03 04:37 |

Mathnerd314 | so, how do I install the standard library from inside Haskell? | 12/03 04:38 |

copumpkin | you just need to put it in a directory and configure your agda to go looking for it there | 12/03 04:39 |

copumpkin | I'd find it quite disconcerting that a userland program could consistently crash my entire OS | 12/03 04:39 |

copumpkin | even if it's the all-in-one installer's "fault" | 12/03 04:39 |

Mathnerd314 | I use --include-dir? | 12/03 04:42 |

Mathnerd314 | *--include-path=DIR | 12/03 04:42 |

copumpkin | you typically don't want to be calling agda from a command-line | 12/03 04:42 |

copumpkin | but yes, I think so | 12/03 04:42 |

Mathnerd314 | why is it bad to call from a command line? | 12/03 04:43 |

copumpkin | well, for most proofs, you'll want all the help you can get | 12/03 04:43 |

copumpkin | from an interactive UI like emacs | 12/03 04:43 |

copumpkin | you can put holes in your proofs and it can tell you want it needs there | 12/03 04:43 |

copumpkin | and what you have in scope and so on | 12/03 04:43 |

Mathnerd314 | huh. | 12/03 04:47 |

Mathnerd314 | so why doesn't Data.List handle infinite lists? | 12/03 04:48 |

copumpkin | it needs the equivalent of laziness in haskell to handle them | 12/03 04:49 |

Mathnerd314 | so something like a thunk. | 12/03 04:50 |

copumpkin | yeah, sort of | 12/03 04:50 |

copumpkin | that kind of thing is handled formally by talking about data vs. codata | 12/03 04:50 |

copumpkin | data is inductively defined | 12/03 04:50 |

copumpkin | and codata is coinductively defined :) | 12/03 04:51 |

copumpkin | which means, roughly, that with data you have constructors and codata you have destructors | 12/03 04:51 |

* Mathnerd314 has no idea of what you're saying | 12/03 04:51 | |

Mathnerd314 | that makes even less sense... :-) | 12/03 04:51 |

copumpkin | well | 12/03 04:51 |

copumpkin | hmm | 12/03 04:52 |

copumpkin | with data you build values by taking constructors and sticking them together. You take them apart by pattern matching on those constructors and finding what you want | 12/03 04:53 |

Mathnerd314 | ok. | 12/03 04:53 |

copumpkin | with codata, you just have "observers" on some value that exists | 12/03 04:53 |

Mathnerd314 | so you have properties of that value? | 12/03 04:54 |

Mathnerd314 | like "this value acts like 0 on this set" | 12/03 04:54 |

copumpkin | sort of | 12/03 04:54 |

copumpkin | from your point of view, you can treat both of them roughly in the same way. A type can have multiple "constructors", but agda will treat them differently | 12/03 04:55 |

copumpkin | specifically, it won't try to figure out whether your coinductive type is finite | 12/03 04:56 |

copumpkin | whereas it needs a "base case" for an inductive type | 12/03 04:56 |

Mathnerd314 | but I have a base case - an empty list... right? | 12/03 04:57 |

copumpkin | yes, and you have an observer that tells you whether you have it or not | 12/03 04:57 |

Mathnerd314 | ok then. | 12/03 04:57 |

copumpkin | but agda won't try to ensure that there's one of those at some depth in the colist | 12/03 04:58 |

copumpkin | in haskell, all "data" is actually codata | 12/03 04:58 |

Mathnerd314 | so why does agda have data? | 12/03 04:58 |

copumpkin | but in agda you need to be more explicit about getting that kind of lazy behavior | 12/03 04:58 |

copumpkin | because data is a lot cleaner to work with in general, and many times it's what you want | 12/03 04:58 |

copumpkin | peano naturals as data are the naturals, but peano naturals as codata have an "infinity", for example | 12/03 04:59 |

Mathnerd314 | this isn't helping me with my proof. | 12/03 04:59 |

copumpkin | I know :) | 12/03 04:59 |

copumpkin | I was mostly kidding around about coming up with a formal proof of that unless you had a fairly strong background in this kind of stuff | 12/03 04:59 |

copumpkin | (but don't give up on agda, it's awesome!) | 12/03 05:00 |

Mathnerd314 | where would I start with a proof? | 12/03 05:00 |

copumpkin | I'd start by defining a colist (I'd mostly avoid the standard library until you know the basics) structure, write some basic functions on it, and then eventually write your pure/fmap/bind for your instance (as separate functions) | 12/03 05:01 |

copumpkin | so pure : a -> Colist a | 12/03 05:01 |

copumpkin | more specifically | 12/03 05:01 |

copumpkin | pure : {a : Set} -> a -> Colist a | 12/03 05:01 |

copumpkin | (agda doesn't really have polymorphism) | 12/03 05:01 |

copumpkin | you could then define repeat fairly simply on your Colist | 12/03 05:02 |

copumpkin | map too | 12/03 05:02 |

copumpkin | then your proofs would be the laws... here, let me throw together a template for you | 12/03 05:02 |

Mathnerd314 | btw... what encoding are .agda files? | 12/03 05:07 |

copumpkin | utf-8 usually | 12/03 05:07 |

copumpkin | in fact, always I thnk | 12/03 05:07 |

Mathnerd314 | I need a better font then. | 12/03 05:07 |

copumpkin | almost done with my template :) | 12/03 05:10 |

Mathnerd314 | why does it take so long to make a simple template | 12/03 05:13 |

Mathnerd314 | ? | 12/03 05:13 |

copumpkin | I'm explaining stuff in it :) | 12/03 05:13 |

Mathnerd314 | somehow, firefox finds characters for everything, but none of my other programs do. | 12/03 05:15 |

copumpkin | actually, proving stuff about this might be harder than I anticipated, but I'll show you the file as I have it | 12/03 05:16 |

copumpkin | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23917#a23917 | 12/03 05:18 |

copumpkin | others in here might know more about it :) | 12/03 05:18 |

copumpkin | but basically, coinduction is scary | 12/03 05:18 |

copumpkin | how long have you been using haskell, anyway? | 12/03 05:19 |

* Mathnerd314 checks install date | 12/03 05:21 | |

Mathnerd314 | Monday March 8 2010 | 12/03 05:23 |

copumpkin | this might be a bit precocious then :) | 12/03 05:23 |

Mathnerd314 | so... 4 days? | 12/03 05:23 |

copumpkin | but it's fascinating stuff, if you're interested in going deeper than haskell | 12/03 05:23 |

copumpkin | deeper in some directions, at least | 12/03 05:23 |

Mathnerd314 | well, I've been thinking about type theory (or some fascimile of it) for a while longer | 12/03 05:24 |

copumpkin | cool | 12/03 05:24 |

copumpkin | anyway, there's a fairly accessible tutorial on the agda wiki | 12/03 05:25 |

copumpkin | http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf | 12/03 05:25 |

Mathnerd314 | so peano naturals have an infinity in codata... that means you can induct to aleph-null? | 12/03 05:30 |

Mathnerd314 | because my proof is one by induction | 12/03 05:40 |

Mathnerd314 | so you need to do that for infinite lists | 12/03 05:40 |

copumpkin | well, did you actually prove anything for infinite lists? | 12/03 05:41 |

copumpkin | in your earlier proof | 12/03 05:41 |

Mathnerd314 | I showed that it was true for the first element, and true for the next if it was true for the previous | 12/03 05:42 |

kmc | wouldn't it be induction to ω rather? | 12/03 05:42 |

Mathnerd314 | Is that powerful enough? | 12/03 05:42 |

Mathnerd314 | yeah, that's what I want to happen. | 12/03 05:42 |

Mathnerd314 | the definition takes elements one at a time, so the proof should be able to as well... | 12/03 05:45 |

Mathnerd314 | copumpkin: your template is for a Functor, not for a Monad? | 12/03 05:48 |

* Mathnerd314 wonders if you sleep :p | 12/03 05:49 | |

copumpkin | Mathnerd314: well, I started writing the laws and then remembered it's hard to prove equality on codata :P | 12/03 05:50 |

copumpkin | but you'd probably want to start by proving the functor laws, and build up to the monad ones | 12/03 05:50 |

Mathnerd314 | how do you prove equivalence? | 12/03 05:51 |

Mathnerd314 | magic? | 12/03 05:51 |

copumpkin | on regular data? | 12/03 05:51 |

Mathnerd314 | on colists | 12/03 05:51 |

copumpkin | well, you could prove that any finite prefix of the colists is equal | 12/03 05:52 |

Mathnerd314 | so prove x=x and a delayed proof for xs? | 12/03 05:52 |

* Mathnerd314 has no idea what he's saying | 12/03 05:53 | |

copumpkin | well, the proofs are typically functions | 12/03 05:53 |

copumpkin | "if you give me a colist, I'll hand you back a proof of some property of that colist" | 12/03 05:54 |

copumpkin | http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Colist.html#2938 is how the standard library deals with colist "equality", and it isn't pretty :) | 12/03 05:54 |

copumpkin | but it's not too bad | 12/03 05:54 |

copumpkin | you can copy that into your file and try using \~~ instead of \== | 12/03 05:55 |

copumpkin | or you can just import Data.Colist if you'd prefer :) | 12/03 05:56 |

Mathnerd314 | import Data.Colist sounds good... what's the point of libraries if you don't use them? | 12/03 05:56 |

copumpkin | oh I do use them, but I figured it'd be best in a completely new language to see how you'd define the basics yourself :P | 12/03 05:57 |

Mathnerd314 | I'm not certain I understand what the second part is doing | 12/03 05:59 |

copumpkin | the _::_ constructor? | 12/03 06:00 |

Mathnerd314 | yeah | 12/03 06:00 |

copumpkin | it says that if you have an x, two colists, and a (deferred) proof that those two colists are equal, then the x consed onto both those colists is equal | 12/03 06:01 |

Mathnerd314 | that's what I was trying to say above | 12/03 06:01 |

copumpkin | I see :) | 12/03 06:01 |

copumpkin | so you should be able to prove the functor laws fairly simply with those | 12/03 06:02 |

copumpkin | I think the fmap id == id is actually unnecessary given the other law | 12/03 06:03 |

copumpkin | (not in all categories, but in the ones we care about) | 12/03 06:03 |

Mathnerd314 | "all monads are functors and applicatives" | 12/03 06:03 |

copumpkin | yep | 12/03 06:03 |

Mathnerd314 | according to wikipedia | 12/03 06:03 |

Mathnerd314 | ;-) | 12/03 06:03 |

copumpkin | the reason I started with functor is that it's simpler | 12/03 06:03 |

copumpkin | using the return/bind in monad is a lot messier | 12/03 06:04 |

copumpkin | so fmap + return + join tends to be cleaner | 12/03 06:04 |

copumpkin | but you're free to approach that proof as you wish | 12/03 06:04 |

copumpkin | you can probably convert between the proofs if you have one | 12/03 06:04 |

copumpkin | by the way, typing a question mark and typechecking will create a hole for you | 12/03 06:06 |

copumpkin | so if you want to write out the type of a proof and leave a bit out because you haven't figured it out yet, just do that | 12/03 06:06 |

copumpkin | C-c C-, inside the hole will tell you what's in scope there and what the goal type of that hole is | 12/03 06:06 |

Mathnerd314 | so why does xs appear 3 times in the argument list and ys only twice? | 12/03 06:06 |

Mathnerd314 | there's something asymmetric about the definition... | 12/03 06:07 |

copumpkin | well, you have an x so you can reuse it multiple times. the xs and ys aren't really known to be equal at that point | 12/03 06:08 |

copumpkin | you have a delayed proof that they are | 12/03 06:08 |

Mathnerd314 | there's xs= : inf (b xs = b ys) | 12/03 06:08 |

Mathnerd314 | I don't see why there's an xs= at the beginning | 12/03 06:09 |

copumpkin | that xs~~ is just a name of the proof | 12/03 06:09 |

copumpkin | it's to make error messages prettier | 12/03 06:09 |

copumpkin | you could omit it | 12/03 06:09 |

copumpkin | (it'll also make a couple of features of the agda interactive environment more useful) | 12/03 06:09 |

Mathnerd314 | oh. so a : b means argument of name a and type b? | 12/03 06:10 |

copumpkin | yeah | 12/03 06:10 |

copumpkin | you typically use it when you need to refer to its actual value later in the type | 12/03 06:10 |

Mathnerd314 | what about a :: b? | 12/03 06:10 |

copumpkin | :: is the colist constructor | 12/03 06:10 |

Mathnerd314 | ok. so the reverse of Haskell ;-) | 12/03 06:10 |

copumpkin | yep :) | 12/03 06:11 |

copumpkin | and the _ on either side of it is a neat feature called mixfix | 12/03 06:11 |

copumpkin | factorial would be _! for example | 12/03 06:11 |

Mathnerd314 | doesn't scala have something like that? | 12/03 06:11 |

copumpkin | you can even have if_then_else_ : Bool -> a -> a -> a | 12/03 06:11 |

copumpkin | :) | 12/03 06:11 |

copumpkin | I don't think so | 12/03 06:11 |

copumpkin | I think you can put underscores in things to make implicit functions, but not sure | 12/03 06:12 |

Mathnerd314 | I remember seeing some language having (_ > _) | 12/03 06:12 |

Mathnerd314 | and using it as an argument to functions | 12/03 06:12 |

copumpkin | I think it does, but that's a form of partial application | 12/03 06:12 |

copumpkin | so you could write 5 + _ * 10 or something and get a function that takes a number to a number | 12/03 06:13 |

copumpkin | I've definitely heard of a language with that feature, but this is different | 12/03 06:13 |

copumpkin | this is giving you pretty deep control of the parser | 12/03 06:13 |

copumpkin | you can write _==_mod_ : Nat -> Nat -> Nat -> Bool, for example | 12/03 06:14 |

Mathnerd314 | ok. | 12/03 06:14 |

copumpkin | and if it sees 7 == 13 mod 6 | 12/03 06:14 |

copumpkin | it'll call that function | 12/03 06:14 |

Mathnerd314 | so like pattern matching but better | 12/03 06:14 |

copumpkin | _==_[mod_] : Nat -> Nat -> Nat -> Bool maybe | 12/03 06:15 |

copumpkin | sort of | 12/03 06:15 |

* Mathnerd314 finishes compiling the standard library | 12/03 06:16 | |

copumpkin | :) | 12/03 06:16 |

copumpkin | one fairly amusing feature of agda is that most of its users never actually run their programs | 12/03 06:16 |

copumpkin | why run it if you've already proven it to be correct? :P | 12/03 06:17 |

Mathnerd314 | can you actually run them? | 12/03 06:17 |

copumpkin | sure, you can compile down to haskell in two different ways | 12/03 06:17 |

copumpkin | you can also ask the agda-mode to "normalize" terms for you | 12/03 06:17 |

copumpkin | which is a bit like running | 12/03 06:17 |

Mathnerd314 | compile to haskell o_O | 12/03 06:17 |

copumpkin | yep | 12/03 06:17 |

Mathnerd314 | I thought C was high-level... | 12/03 06:17 |

copumpkin | lol | 12/03 06:17 |

copumpkin | haskell is semantically quite similar to agda | 12/03 06:17 |

copumpkin | a lot closer than C, at least :) | 12/03 06:18 |

Mathnerd314 | so, in the standard library, map-cong is the same as fmap? | 12/03 06:18 |

copumpkin | map is fmap | 12/03 06:18 |

Mathnerd314 | (or just map) | 12/03 06:18 |

copumpkin | map-cong is a proof | 12/03 06:18 |

copumpkin | in fact, it's more or less what you need to prove for fmap id == id | 12/03 06:19 |

copumpkin | but its type is pretty obscure :P | 12/03 06:19 |

copumpkin | it's basically saying that map preserves equality | 12/03 06:20 |

copumpkin | if you have two equal colists to start with, and map a function to them, you'll have two equal colists | 12/03 06:20 |

Mathnerd314 | a function a->b, and it gives a proof a=b -> map a=b? | 12/03 06:20 |

Mathnerd314 | map a = map b | 12/03 06:20 |

Mathnerd314 | * | 12/03 06:20 |

Mathnerd314 | with implicit "type" parameters a and b | 12/03 06:21 |

copumpkin | sort of | 12/03 06:21 |

copumpkin | you can actually ask agda to expand that type for you | 12/03 06:21 |

copumpkin | C-c C-d map-cong | 12/03 06:21 |

Mathnerd314 | I'm using command-line, remember? since emacs+agda crashes? | 12/03 06:22 |

copumpkin | oh, yeah :/ | 12/03 06:22 |

copumpkin | but it's basically (minus the noise), map-cong : (f : A -> B) -> (xs : Colist A) -> (ys : Colist A) -> (xs ≈ ys) -> (map f xs ≈ map f ys) | 12/03 06:23 |

copumpkin | you have a function, two colists, a proof that they are equal | 12/03 06:23 |

copumpkin | it gives you a proof that after applying that function to both colists, the results are still equal | 12/03 06:23 |

Mathnerd314 | ok. | 12/03 06:24 |

Mathnerd314 | but it's also a definition of a map function, right? | 12/03 06:24 |

copumpkin | well, sort of | 12/03 06:24 |

copumpkin | its definition is almost identical to that of map | 12/03 06:24 |

copumpkin | but it's constructing a value of _≈_, not a Colist | 12/03 06:25 |

copumpkin | agda automatically disambiguates constructors | 12/03 06:25 |

copumpkin | so there the [] on the right hand side is a constructor of _≈_ | 12/03 06:25 |

copumpkin | and the :: is too | 12/03 06:25 |

copumpkin | on the left-hand side, it's pattern matching on Colist constructors (which happen to be identical to the ones of _≈_) | 12/03 06:26 |

Mathnerd314 | so how many overloads are there of []? | 12/03 06:26 |

copumpkin | two in this module, as far as I can see | 12/03 06:26 |

copumpkin | but you can write as many as you want | 12/03 06:26 |

Mathnerd314 | ok. | 12/03 06:26 |

copumpkin | overloading only works with constructors | 12/03 06:26 |

Mathnerd314 | so I can just ignore all that and pretend they're constructors | 12/03 06:27 |

Mathnerd314 | of CoLists | 12/03 06:27 |

Mathnerd314 | until I have to prove stuff | 12/03 06:27 |

copumpkin | yeah, pretty much. Just keep it in mind (and be intrigued that the structure of a proof like that is almost identical to the structure of a "regular computation" like map) | 12/03 06:28 |

Mathnerd314 | curry-howard isomorphism! | 12/03 06:29 |

copumpkin | yep :) | 12/03 06:29 |

copumpkin | _≈_ =[ map f ]⇒ _≈_ is another example of mixfix by the way | 12/03 06:29 |

copumpkin | the function is _=[_]⇒_ | 12/03 06:29 |

Mathnerd314 | IRC client keeps putting in emoticons in odd places ;-) | 12/03 06:32 |

Mathnerd314 | anyway, how do you get emacs to find plugins? | 12/03 06:33 |

copumpkin | can't remember :P I'm not an expert by any means | 12/03 06:33 |

copumpkin | anyway, I need to go get some work done, lest I get my ass kicked tomorrow :P | 12/03 06:34 |

copumpkin | I'll probably be back tomorrow evening if you have any more questions | 12/03 06:34 |

Mathnerd314 | when do you sleep? I can't figure it out... | 12/03 06:34 |

copumpkin | not often enough :/ but I'm US eastern time, and will probably go to sleep in a few hours :P | 12/03 06:35 |

Mathnerd314 | so 3 am or something? | 12/03 06:35 |

copumpkin | 1:35 right now | 12/03 06:35 |

copumpkin | not sure when I'll go to sleep, I hope as soon as possible | 12/03 06:35 |

copumpkin | but I still have to finish a paper | 12/03 06:36 |

Mathnerd314 | on type theory? :p | 12/03 06:36 |

copumpkin | actually, it's a bit of a high-level introduction to that, for a class | 12/03 06:36 |

copumpkin | it's just a writing class, so it's not terribly in-depth | 12/03 06:36 |

Mathnerd314 | fortunately, I have not yet advanced that far. I just have homework to do. | 12/03 06:38 |

copumpkin | :) | 12/03 06:38 |

Mathnerd314 | back to work, then. | 12/03 06:38 |

copumpkin | yep :) good luck with this stuff! | 12/03 06:39 |

Mathnerd314 | so, is there a page somewhere mapping all those unicode chars (that I'm missing proper fonts for) that agda uses to their ascii equivalents? | 12/03 21:13 |

Saizan | mh, maybe on the wiki, though only the built-in syntax has ascii equivalents | 12/03 21:14 |

Mathnerd314 | alternately, I just installed some good fonts ;-) | 12/03 21:39 |

Saizan | saner route :) | 12/03 21:40 |

Mathnerd314 | any recommendations for a good unicode monospace font? | 12/03 21:42 |

Mathnerd314 | (not that DejaVu is that bad) | 12/03 21:42 |

Saizan | my main font is Bitstream Vera Sans Mono | 12/03 21:42 |

Mathnerd314 | DejaVu is the successor to that, so ok. | 12/03 21:43 |

Mathnerd314 | I wonder how fonts have "snapshots" and "release candidates"... | 12/03 21:45 |

dolio | In my experience, a fair number of glyphs aren't provided by DejaVu, but emacs is able to pull them in from other fonts somehow. | 12/03 21:47 |

dolio | But, you have to have those other fonts, of course. | 12/03 21:48 |

Mathnerd314 | I have billions of fonts, but none of my editors are smart enough to use those others :-( | 12/03 21:48 |

dolio | Are you not using emacs? | 12/03 21:48 |

Mathnerd314 | no, the emacs installed by the all-in-one windows installer seems to forcibly reboot my system after a compile or two | 12/03 21:50 |

dolio | Ah. | 12/03 21:50 |

dolio | Well, then, you are entering a world of pain, probably. | 12/03 21:50 |

dolio | Writing Agda is far, far easier with the emacs mode. | 12/03 21:51 |

Mathnerd314 | I'm also trying to install it manually... | 12/03 21:52 |

Mathnerd314 | it looks like http://wiki.portal.chalmers.se/agda/agda.php?n=Main.README-2-2-6 is the most accurate page? | 12/03 22:02 |

* Mathnerd314 succeeds in getting Agda to load | 12/03 22:58 | |

Saizan | yay | 12/03 23:06 |

Mathnerd314 | but I have to downgrade to Emacs 22.3, since 23.1 doesn't support BDF fonts on windows :-( | 12/03 23:30 |

Mathnerd314 | after further testing, it appears that something in the BDF code is causing my system to reboot. | 12/03 23:46 |

Mathnerd314 | so, like I said before, anybody know a good set of fonts with all the glyphs Agda uses? | 12/03 23:47 |

liyang | This is probably not helpful, but how about running some instance of leenucks in a virtual machine? | 12/03 23:53 |

liyang | User apps causing the OS to reboot is… er… embarrassing to say the least. | 12/03 23:53 |

Mathnerd314 | I'm doing all this on windows right now | 12/03 23:57 |

--- Day changed Sat Mar 13 2010 | ||

liyang | If you have the spare memory, VirtualBox is free and Free. | 13/03 00:15 |

Mathnerd314 | yeah, I have virtualbox. it's not running anything though. | 13/03 00:15 |

TacticalGrace | What is the biggest uni course Agda has been used in so far? | 13/03 01:51 |

Mathnerd314 | ok, finally have a working Agda installation... how do I add the standard library to the path so that I can compile things based on it from anywhere? | 13/03 01:59 |

Saizan | in emacs you can customize the include dirs | 13/03 02:01 |

Saizan | otherwise you pass -i flags to the CLI | 13/03 02:01 |

Mathnerd314 | by "working installation", I meant emacs... how do I customize the include dirs? | 13/03 02:03 |

liyang | Customise Emacs's include dirs to include agda-mode? Compiling Agda gives you an agda-mode binary which makes the necessary modifications to your .emacs (or whatever the Windows equivalent is. Maybe.) | 13/03 02:08 |

Saizan | customize Agda2 Include Dirs to include the path to the library | 13/03 02:09 |

Saizan | however you also need the agda-mode setup step | 13/03 02:09 |

liyang | TacticalGrace: undergrad? Nottingham has a few fourth-years taking it. | 13/03 02:09 |

Saizan | Mathnerd314: you M-x customize-apropos RET Agda RET and then look for Include Dirs in the buffer that comes out | 13/03 02:09 |

Mathnerd314 | ok. | 13/03 02:26 |

Mathnerd314 | agda seems to hate byte order marks? | 13/03 02:40 |

liyang | Perhaps. Haven't encountered BOMs for a while. File a bug? http://code.google.com/p/agda/ | 13/03 02:42 |

liyang | UTF-8 doesn't need BOMs, but under Windows, text editor seem to add them anyway… | 13/03 02:44 |

Mathnerd314 | right. | 13/03 02:44 |

Mathnerd314 | and emacs seems to hide them, so they're hard to remove | 13/03 02:45 |

Mathnerd314 | how active is agda? bug tracker seems rather full... | 13/03 02:46 |

liyang | Most of those listed bugs aren't anything major. I'm not sure how to quantify activeness, but see the mailing list for an idea… | 13/03 02:48 |

Mathnerd314 | it seems to mostly be "call for papers" | 13/03 02:50 |

TacticalGrace | liyang: yeah, undergrad | 13/03 02:52 |

TacticalGrace | liyang: I'm currently teaching (parts of) it to a class of 70 something | 13/03 02:53 |

liyang | TacticalGrace: our second years here are still using Coq for maths, that's all I know. Have been burying my head in sand for some time; that's all I know of. | 13/03 02:56 |

liyang | TacticalGrace: oh, Anton Setzer had some notes for a course he taught—http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials | 13/03 02:57 |

liyang | (At Swansea) | 13/03 02:57 |

liyang | (Also, aren't they a bit old to be undergrads?) | 13/03 02:58 |

TacticalGrace | liyang: ;) | 13/03 03:00 |

TacticalGrace | hadn't seen Setzer's course, but seen txa's notes | 13/03 03:01 |

Mathnerd314 | agda is *slow* | 13/03 03:56 |

Mathnerd314 | is \to the same as -> ? | 13/03 04:00 |

TacticalGrace | Mathnerd314: yes | 13/03 04:03 |

Mathnerd314 | how do I do the equivalent of Haskell's case? | 13/03 04:06 |

Mathnerd314 | do I need a helper function? | 13/03 04:07 |

TacticalGrace | depends, you may want to use a with | 13/03 04:07 |

Mathnerd314 | I want to write this, basically: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23913 | 13/03 04:08 |

Mathnerd314 | just the >>= part though | 13/03 04:08 |

Mathnerd314 | so 'with' sounds like the right thing | 13/03 04:09 |

Mathnerd314 | copying from http://www.cs.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Filter.agda | 13/03 04:09 |

TacticalGrace | you can use with for that | 13/03 04:09 |

TacticalGrace | see, eg, Appendix A.5 in http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf | 13/03 04:09 |

Mathnerd314 | and function composition is... | 13/03 04:16 |

Mathnerd314 | ^ TacticalGrace | 13/03 04:24 |

TacticalGrace | I'm not sure whether it is pre-defined | 13/03 04:25 |

TacticalGrace | Have you downloaded the standard library? | 13/03 04:25 |

Mathnerd314 | yes | 13/03 04:25 |

Mathnerd314 | + added it to the path and compiled everything in it | 13/03 04:26 |

TacticalGrace | ok | 13/03 04:26 |

TacticalGrace | I'm not sure whether it is defined in there, but might be worth to have a look | 13/03 04:26 |

TacticalGrace | There should be a Haddock for Agda.... | 13/03 04:26 |

TacticalGrace | or if Hoogle could be adapted | 13/03 04:28 |

TacticalGrace | that would be very useful, gioven types in Agda are even more expressive than in Haskell | 13/03 04:28 |

TacticalGrace | gioven = given | 13/03 04:28 |

Mathnerd314 | I think it might be better if Haskell just adds enough language extensions that it turns into Agda | 13/03 04:28 |

Mathnerd314 | but anyway, I'm hearing no? | 13/03 04:29 |

TacticalGrace | there is always that business about termination, but I agree that it is a tantalising goal | 13/03 04:29 |

Mathnerd314 | (as far as composition operator) | 13/03 04:30 |

TacticalGrace | I'm not aware that is pre-defined, but I'm far from an Agda expert | 13/03 04:30 |

TacticalGrace | and we are working with an intuitionistic logic, so I'll settle for the third option ;) | 13/03 04:31 |

Mathnerd314 | It doesn't seem that hard to me to just "borrow" the entire Haskell prelude... | 13/03 04:32 |

Mathnerd314 | but this function signature seems wrong: _._ : ∀ {A B C} → (B → C) → (A → B) → A → C | 13/03 04:40 |

Mathnerd314 | ^ TacticalGrace | 13/03 04:43 |

TacticalGrace | it's no dependent function composition | 13/03 04:43 |

TacticalGrace | that is more complicated | 13/03 04:43 |

TacticalGrace | I think it is somewhere in Ulf Norell's AFP'08 lecture notes | 13/03 04:43 |

Mathnerd314 | wow, a very long type ;-) | 13/03 04:46 |

Mathnerd314 | so function composition must be somewhere in the standard library... | 13/03 04:51 |

copumpkin | yep, open import Function | 13/03 04:51 |

copumpkin | I think | 13/03 04:51 |

copumpkin | it's \o with agda's input method | 13/03 04:51 |

copumpkin | not sure if you managed to fix your emacs | 13/03 04:51 |

Mathnerd314 | it was some font problems | 13/03 04:52 |

copumpkin | its type is terrifying, so I recommend you don't look at it :) | 13/03 04:52 |

TacticalGrace | oh, right | 13/03 04:53 |

TacticalGrace | it's in Data.Function | 13/03 04:53 |

copumpkin | oh, I think that got renamed to just Function | 13/03 04:53 |

TacticalGrace | didn't look under Data for function composition | 13/03 04:53 |

copumpkin | but maybe not in any released version of the std lib | 13/03 04:53 |

TacticalGrace | in lib-0.3 | 13/03 04:53 |

TacticalGrace | supposedly lib-0.3 is the version to go with the latest Agda release | 13/03 04:53 |

Mathnerd314 | yay, that finished my porting of my monad's definition from Haskell to Agda | 13/03 04:54 |

copumpkin | http://www.cs.nott.ac.uk/~nad/listings/lib/Function.html#255 | 13/03 04:54 |

copumpkin | yeah, NAD renamed it | 13/03 04:54 |

copumpkin | now it's top-level | 13/03 04:54 |

copumpkin | there's now a Function.(Bi/In/Sur)jection and Function.Equality | 13/03 04:54 |

copumpkin | .Inverse too, all sorts of goodies! | 13/03 04:55 |

Mathnerd314 | it's all line noise to me... | 13/03 04:56 |

copumpkin | I wonder how much time NAD spends perusing lists of unicode characters in search of the perfect symbol for his libraries :) | 13/03 04:56 |

copumpkin | Mathnerd314: I agree, big chunks of agda are practically illegible, sadly | 13/03 04:56 |

Mathnerd314 | Agda = Perl and Haskell = Python ;-) | 13/03 04:57 |

Mathnerd314 | so, proofs are functions over the variables that return equality? | 13/03 04:59 |

copumpkin | TacticalGrace: are you already teaching the course using agda? | 13/03 04:59 |

copumpkin | Mathnerd314: ? | 13/03 04:59 |

Mathnerd314 | I'm translating my proof into Agda... so I need the type signatures | 13/03 04:59 |

copumpkin | proofs don't have to be functions | 13/03 05:00 |

Mathnerd314 | what else are they? | 13/03 05:00 |

copumpkin | just plain old values | 13/03 05:00 |

copumpkin | test1: 1 :: 2 :: 3 :: [] == 1 :: 2 :: 3 :: [] | 13/03 05:01 |

copumpkin | test1 = refl | 13/03 05:01 |

copumpkin | :P | 13/03 05:01 |

* Mathnerd314 is confused again | 13/03 05:01 | |

copumpkin | that is basically forcing agda to run a unit test at compile time for you | 13/03 05:01 |

copumpkin | types are logical statements, values are proofs of the associated types | 13/03 05:02 |

Mathnerd314 | but here, I have to prove that (return x) >>= f == f x | 13/03 05:02 |

TacticalGrace | copumpkin: yep, two weeks into that course | 13/03 05:02 |

copumpkin | oh cool, how's it going? | 13/03 05:02 |

TacticalGrace | last week was the first week with Agda | 13/03 05:02 |

TacticalGrace | You should ask the student's that question | 13/03 05:02 |

copumpkin | :) | 13/03 05:03 |

TacticalGrace | we are starting very slowly | 13/03 05:03 |

TacticalGrace | most of them don't know Haskell (or any other FP language) and the math bakcground is very varied | 13/03 05:03 |

copumpkin | Mathnerd314: yeah, you'd state that as forall f x -> return (x >>= f) == f x | 13/03 05:03 |

TacticalGrace | we basically did Curry-Howard for propositional logic last week | 13/03 05:03 |

copumpkin | you'll most likely need to be more explicit about the types of f and x though, or you'll get lots of yellow | 13/03 05:03 |

TacticalGrace | next week, we'll look at quantifiers and dependent types | 13/03 05:04 |

copumpkin | TacticalGrace: sounds like they'll be learning a lot of awesome stuff pretty quickly :) | 13/03 05:04 |

copumpkin | not quite as quickly as Mathnerd314, maybe | 13/03 05:04 |

Mathnerd314 | I'm not learning, just doing ;-) | 13/03 05:05 |

TacticalGrace | without at least an intuitive understanding of Curry-Howard, I don't think Agda makes a lot of sense | 13/03 05:05 |

copumpkin | yeah, I agree | 13/03 05:05 |

TacticalGrace | I already saw these looks last week, kind of, well anybody can write some random functions, but how is that proving anything | 13/03 05:05 |

copumpkin | are they all CS people, at least? with some kind of background in abstract reasoning? do they know what induction is? | 13/03 05:07 |

TacticalGrace | besides, I think Curry-Howard is one of these very fundamental results of computing | 13/03 05:07 |

TacticalGrace | yes, all CS, but from different CS programs | 13/03 05:07 |

TacticalGrace | some have already done some formal methods using Event-B | 13/03 05:07 |

TacticalGrace | but not all of them have done that | 13/03 05:08 |

copumpkin | ah | 13/03 05:08 |

TacticalGrace | (we have computer science, software engineering, computer engineering, and bioinformatics) | 13/03 05:08 |

TacticalGrace | for the CS and SE students this course is compulsory | 13/03 05:08 |

copumpkin | that's quite nice and granular | 13/03 05:08 |

TacticalGrace | for the others its an elective | 13/03 05:09 |

copumpkin | TacticalGrace: I've started designing a new (not E)DSL for using vector (and maybe DPH eventually) by the way :P | 13/03 05:10 |

TacticalGrace | a functional DSL for array computations? | 13/03 05:11 |

TacticalGrace | why not E? | 13/03 05:11 |

TacticalGrace | I mean, why not embedded? | 13/03 05:11 |

copumpkin | well, my main inspiration was my difficulty writing vector-static | 13/03 05:11 |

copumpkin | I tried and failed to make a usable interface for statically sized vectors | 13/03 05:11 |

copumpkin | (built on top of vector) | 13/03 05:12 |

TacticalGrace | oh, ic | 13/03 05:12 |

TacticalGrace | so, the idea is to track sizes? | 13/03 05:12 |

TacticalGrace | statically | 13/03 05:12 |

copumpkin | so the vector types are parametrized by type-level numbers, and then it hooks into all the unsafe* functions in vector because they're known to be safe | 13/03 05:12 |

copumpkin | yeah | 13/03 05:12 |

Mathnerd314 | why not just use the monad I'm writing? ;-) | 13/03 05:12 |

TacticalGrace | ok, that sound interesting | 13/03 05:12 |

copumpkin | but actually writing any useful functions with vector-static proved to be a real pain | 13/03 05:13 |

TacticalGrace | do you know http://www.cse.chalmers.se/~wouter/Publications/MoreDependentTypesForDistributedArrays.pdf | 13/03 05:13 |

copumpkin | you need to "prove" (as close as haskell gets) basic things like commutativity and so on. So my goal is to have a DSL with primitive nats and fins and a built-in (semi)ring solver | 13/03 05:13 |

TacticalGrace | copumpkin: yeah, I can imagine that it is a pain in Haskell to help the type checker along | 13/03 05:14 |

copumpkin | oh no, hadn't come across that, I'll check it out | 13/03 05:14 |

copumpkin | even in agda, doing that kind of stuff is fairly painful | 13/03 05:14 |

copumpkin | Algebra.RingSolver is good but the output is noisy | 13/03 05:14 |

copumpkin | I'd like to get as close to un-noisy vector usage as possible, while still coming up with static proofs of size invariants | 13/03 05:14 |

TacticalGrace | yep, a specialised solver would be useful | 13/03 05:14 |

TacticalGrace | it's somewhat like DML, too, I guess | 13/03 05:14 |

copumpkin | (and then provide an extractor to haskell for performance, and one to agda to verify that my thing isn't doing anything stupid) | 13/03 05:15 |

TacticalGrace | cool | 13/03 05:15 |

copumpkin | anyway, it's still vaporware but I've started writing my ring solver | 13/03 05:15 |

TacticalGrace | sounds like a good plan :) | 13/03 05:15 |

copumpkin | I'm excited! I just finished all my coursework for this term so am more free | 13/03 05:15 |

TacticalGrace | yeah, it's good to be able to concentrate on something for a longer preriod of time | 13/03 05:16 |

TacticalGrace | without context switching | 13/03 05:16 |

copumpkin | yep :) | 13/03 05:16 |

copumpkin | wouter's paper looks pretty interesting | 13/03 05:17 |

Mathnerd314 | so, can agda partially evaluate? | 13/03 05:23 |

copumpkin | partially evaluate? | 13/03 05:26 |

Mathnerd314 | I have to use the definitions of bind and return to prove stuff, right? | 13/03 05:27 |

copumpkin | yep | 13/03 05:28 |

Mathnerd314 | so how do I apply those? | 13/03 05:28 |

Mathnerd314 | *use | 13/03 05:29 |

copumpkin | you refer to them in your type | 13/03 05:30 |

Mathnerd314 | but they're already defined... | 13/03 05:31 |

copumpkin | hmm, I don't understand your question :) | 13/03 05:34 |

Mathnerd314 | the type I have is ∀ {A B} → (x : A) → (f : (A → Colist B)) → (bind (repeat x) f) ≈ f x | 13/03 05:34 |

copumpkin | okay | 13/03 05:34 |

Mathnerd314 | so then I have to implement it... | 13/03 05:35 |

copumpkin | yep | 13/03 05:35 |

copumpkin | you'd probably use a with construct | 13/03 05:36 |

copumpkin | have you tried proving simpler properties first? :) | 13/03 05:36 |

Mathnerd314 | I don't see how this is complicated... :-_ | 13/03 05:36 |

Mathnerd314 | * _-: | 13/03 05:37 |

copumpkin | as I said last time, proving things formally can be a lot harder than you'd expect :P | 13/03 05:37 |

copumpkin | but the functor laws are fairly trivial | 13/03 05:37 |

copumpkin | and might be a good start | 13/03 05:37 |

copumpkin | (I just proved them) | 13/03 05:37 |

Mathnerd314 | proved in agda? | 13/03 05:38 |

copumpkin | yep | 13/03 05:38 |

* Mathnerd314 wants to see | 13/03 05:38 | |

copumpkin | just a sec | 13/03 05:38 |

copumpkin | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23952#a23952 | 13/03 05:41 |

copumpkin | really trivial for functor, we'll see about applicative now :) | 13/03 05:41 |

* Mathnerd314 forgot about [] and _::_ overloading | 13/03 05:43 | |

copumpkin | law3 is trivial too | 13/03 05:45 |

copumpkin | law4 might be a little more work (but probably not) | 13/03 05:45 |

Mathnerd314 | huh, I tried filling in the rest of monad law 1 and got "Not implemented: type checking of with application" :- | 13/03 05:46 |

Mathnerd314 | I guess I need a helper function... | 13/03 05:48 |

copumpkin | :o | 13/03 05:49 |

copumpkin | never seen that before :) | 13/03 05:49 |

Mathnerd314 | how would I express that a function a -> Colist b is the same as a Colist of functions (a -> b)? | 13/03 05:49 |

copumpkin | hm, it isn't really, unless you want to "sequence" it | 13/03 05:50 |

copumpkin | over another monad | 13/03 05:50 |

Mathnerd314 | oh, wait, that's just the first law expressed differently | 13/03 05:51 |

copumpkin | first law of what? | 13/03 05:56 |

Mathnerd314 | monads | 13/03 05:56 |

copumpkin | almost done with applicative :P | 13/03 06:02 |

copumpkin | fmap id == id is what you're talking about? | 13/03 06:02 |

Mathnerd314 | no, (bind (repeat x) f) == f x | 13/03 06:03 |

Mathnerd314 | so, if f x == l :: ls, then does ls = next (f x) ? | 13/03 06:06 |

copumpkin | next? | 13/03 06:07 |

Mathnerd314 | a total tail function (next [] = []) | 13/03 06:07 |

copumpkin | meh, hpaste is down now | 13/03 06:07 |

copumpkin | hmm | 13/03 06:08 |

Mathnerd314 | that's the type error I'm getting now ;-) | 13/03 06:10 |

copumpkin | can I see your code? moonpatio.com is still up | 13/03 06:10 |

Mathnerd314 | http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8534#a8534 | 13/03 06:12 |

Mathnerd314 | I think I might have defined helper wrong, maybe. | 13/03 06:12 |

Mathnerd314 | comments? | 13/03 06:14 |

copumpkin | it looks reasonable so far | 13/03 06:15 |

copumpkin | trying to see how I'd do it | 13/03 06:15 |

copumpkin | definitely more painful than the earlier ones :) | 13/03 06:21 |

Mathnerd314 | well, you need bind or join | 13/03 06:22 |

Mathnerd314 | and bind is simpler IMO | 13/03 06:22 |

copumpkin | yeah | 13/03 06:22 |

copumpkin | I hate coinduction :P | 13/03 06:23 |

Mathnerd314 | anyways, by now I'm pretty certain that it's a monad, despite whether I can prove it or not | 13/03 06:25 |

copumpkin | :P | 13/03 06:25 |

Mathnerd314 | say, if I define [] :: [] = [], then I can turn everything into infinite streams... | 13/03 06:26 |

copumpkin | I'm actually confused at this | 13/03 06:31 |

Mathnerd314 | at what? | 13/03 06:32 |

copumpkin | well | 13/03 06:32 |

copumpkin | for your prop | 13/03 06:32 |

copumpkin | 1 | 13/03 06:32 |

copumpkin | the place where you call helper, I'd like to avoid calling helper | 13/03 06:32 |

copumpkin | so I stick a hole there, and ask for the goal at that point | 13/03 06:32 |

copumpkin | ((bind (x ∷ .ZipList.♯-2 x) (λ x' → next (f x')) | next (f x)) ≈ ♭ ys) is what it gives me | 13/03 06:33 |

copumpkin | meaning that further evaluation of the LHS of ~~ is delayed until next (f x) is evaluated | 13/03 06:33 |

copumpkin | so I add another with next (f x) | 13/03 06:33 |

copumpkin | decompose that | 13/03 06:33 |

copumpkin | and it still refuses to evaluate the LHS any further | 13/03 06:33 |

Mathnerd314 | here, try changing, in bind, \b as to next (a \:: as) | 13/03 06:39 |

Mathnerd314 | the type simplifies a bit | 13/03 06:40 |

copumpkin | hm, why would that be? it looks the same to me (and I don't see why it would be different | 13/03 06:41 |

Mathnerd314 | ok, you're right. | 13/03 06:42 |

Mathnerd314 | good to know next is defined correctly though... | 13/03 06:42 |

copumpkin | yep :) | 13/03 06:43 |

copumpkin | gah, can't figure out why this isn't working | 13/03 06:44 |

Mathnerd314 | because it's secretly not a monad? :p | 13/03 06:49 |

copumpkin | nah, I mean it's an agda issue (and I'm clueless) | 13/03 06:51 |

copumpkin | not a thing about the proof | 13/03 06:51 |

Mathnerd314 | well, I'm reading this: http://www.mail-archive.com/haskell-cafe@haskell.org/msg57217.html | 13/03 06:51 |

Mathnerd314 | can't figure out how it's related to my implementation | 13/03 06:53 |

Mathnerd314 | other than that mine works and his doesn't ;-) | 13/03 06:57 |

copumpkin | so yours works on his examples? | 13/03 06:58 |

copumpkin | that's dolio by the way and he's often around here | 13/03 06:58 |

copumpkin | I'm starting to think it isn't true, by trying to prove the associativity law | 13/03 07:00 |

Mathnerd314 | I think that message might give a counterexample... | 13/03 07:00 |

copumpkin | it's pretty painful to type in colist literals :) | 13/03 07:01 |

copumpkin | as I'm sure you're finding out | 13/03 07:01 |

dolio | Mathnerd314: Your diagonal was different. | 13/03 07:03 |

Mathnerd314 | does it work on that example? | 13/03 07:03 |

dolio | If I remember correctly, the second case in yours would be "diag ([]:xs) = []". | 13/03 07:04 |

* Mathnerd314 tries it out | 13/03 07:04 | |

dolio | Yours quits as soon as it finds a missing diagonal element, which probably works. | 13/03 07:05 |

dolio | Not sure why that never occurred to me. | 13/03 07:07 |

copumpkin | it seems to work I think | 13/03 07:07 |

copumpkin | unfortunately I can't get agda to prove it for me | 13/03 07:07 |

copumpkin | oh yes I can | 13/03 07:07 |

Mathnerd314 | success? | 13/03 07:08 |

copumpkin | oh wait | 13/03 07:08 |

copumpkin | nope | 13/03 07:08 |

Mathnerd314 | oh well. | 13/03 07:08 |

copumpkin | it has an extra element | 13/03 07:08 |

copumpkin | .Data.BoundedVec.Inefficient._∷_ 8 .Data.BoundedVec.Inefficient.[] | 13/03 07:09 |

copumpkin | != .Data.BoundedVec.Inefficient.[] | 13/03 07:09 |

copumpkin | I could've done it in half the time in haskell :P | 13/03 07:09 |

Mathnerd314 | so where is this? | 13/03 07:10 |

copumpkin | http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8535#a8535 | 13/03 07:10 |

copumpkin | at least we have proofs that it's a functor an applicative, in case anyone doubted it | 13/03 07:11 |

copumpkin | now, we should prove that no monad exists for ziplists ;) | 13/03 07:11 |

Mathnerd314 | does it satisfy law7? | 13/03 07:12 |

copumpkin | I wasn't able to get it to reduce the expression further | 13/03 07:13 |

copumpkin | not sure what's wrong | 13/03 07:13 |

copumpkin | I'm probably doing something stupi | 13/03 07:13 |

copumpkin | that hole in law9 looks pretty bad though | 13/03 07:14 |

copumpkin | because there's only one colist in scope whose type will fit in the hole, and it doesn't "fit" | 13/03 07:14 |

copumpkin | trying to prepend x onto it doesn't help eihter :P | 13/03 07:14 |

copumpkin | proof! | 13/03 07:15 |

copumpkin | (also, there's no way to get another colist of that type) | 13/03 07:15 |

Mathnerd314 | so, diag = join, right? | 13/03 07:18 |

copumpkin | yeah | 13/03 07:18 |

Mathnerd314 | well, I get [1,8] and [1] here. | 13/03 07:20 |

Mathnerd314 | so I'm probably missing something. | 13/03 07:20 |

copumpkin | Mathnerd314: the only answer is to prove once and for all that there can be no monad | 13/03 07:27 |

Mathnerd314 | and how do you do that? | 13/03 07:27 |

copumpkin | well, I can state it :P | 13/03 07:27 |

copumpkin | probably can't prove it | 13/03 07:27 |

Mathnerd314 | maybe one could use the laws to reach a contradiction? | 13/03 07:27 |

copumpkin | yeah, that's how you prove negation | 13/03 07:27 |

Mathnerd314 | so one would assume... that the monad obeyed the laws of ZipList? | 13/03 07:28 |

Mathnerd314 | (functor / applicative) | 13/03 07:28 |

copumpkin | yeah | 13/03 07:28 |

copumpkin | basically showing that the applicative laws don't fit with the monad ones | 13/03 07:29 |

copumpkin | not even sure it's true, but it'd be neat :) | 13/03 07:29 |

Mathnerd314 | well, first, it should act correctly on infinite lists, right? | 13/03 07:31 |

Mathnerd314 | and use map and repeat | 13/03 07:37 |

Mathnerd314 | so join should be the diagonal, for infinite lists | 13/03 07:39 |

copumpkin | yeah, it should work correctly on those | 13/03 07:40 |

Mathnerd314 | and for join . (fmap return) to be id, it's the diagonal up to the size of the list | 13/03 07:45 |

Mathnerd314 | so, do bad things happen if I say []:[] = []? | 13/03 07:51 |

* Mathnerd314 is too tired to think | 13/03 07:54 | |

copumpkin | where would you say that? | 13/03 07:54 |

copumpkin | in a constructor it's probably fine | 13/03 07:55 |

copumpkin | how can I prove _|_ from f [] ≈ f (something that very clearly is not []) | 13/03 09:06 |

copumpkin | ah I guess it isn't trivial | 13/03 09:11 |

Saizan | yeah, you need injectivity of f | 13/03 09:27 |

copumpkin | what if I have that f [] ~~ [] | 13/03 09:30 |

copumpkin | and ~~ only has [] ~~ [] and then other constructors | 13/03 09:31 |

copumpkin | hmm | 13/03 09:31 |

copumpkin | I guess it still isn't trivial | 13/03 09:31 |

copumpkin | hmm, it seems like it should be though | 13/03 09:32 |

copumpkin | http://snapplr.com/t3be | 13/03 09:32 |

copumpkin | if I have x ~~ [], it seems like x must be [] | 13/03 09:33 |

copumpkin | hmm, I guess the closest equality I can define on x is what I already have | 13/03 09:38 |

copumpkin | this might actually be provable | 13/03 09:45 |

copumpkin | probably not though | 13/03 09:48 |

Saizan | what is f here? | 13/03 09:56 |

Saizan | if you have x ~~ [] you should get x = [] by pattern matching | 13/03 09:57 |

copumpkin | nope :/ | 13/03 09:59 |

copumpkin | oh maybe | 13/03 09:59 |

copumpkin | nah | 13/03 10:00 |

copumpkin | f is join :P | 13/03 10:00 |

copumpkin | a hypothetical join :o | 13/03 10:00 |

copumpkin | I'm trying to prove that there are no monads for ziplist :P | 13/03 10:01 |

copumpkin | on colists, that is | 13/03 10:01 |

Saizan | where is ~~ defined? | 13/03 10:02 |

copumpkin | in Data.Colist | 13/03 10:02 |

Saizan | oh, found | 13/03 10:02 |

copumpkin | seems like == really isn't very useful around coinduction | 13/03 10:03 |

Saizan | http://pastebin.com/bZWru9ui <- i'm sure i miss the bigger picture, but this part works :) | 13/03 10:05 |

copumpkin | hmm, let me try that :) | 13/03 10:06 |

copumpkin | that doesn't even typecheck for me | 13/03 10:08 |

copumpkin | that p | 13/03 10:08 |

copumpkin | _301 ≈ _301 !=< [] ≡ [] of type Set | 13/03 10:08 |

copumpkin | when checking that the expression refl has type [] ≡ [] | 13/03 10:08 |

Saizan | funny, maybe you've another refl in scope? | 13/03 10:09 |

copumpkin | oh good point | 13/03 10:09 |

copumpkin | I had a setoid open | 13/03 10:09 |

copumpkin | aha, nice | 13/03 10:10 |

copumpkin | now I need to figure out how to get a bottom out of this :) | 13/03 10:11 |

copumpkin | it's kind of a ridiculous exercise | 13/03 10:11 |

Saizan | i like to prove bottoms :) | 13/03 10:12 |

copumpkin | I feel like I've forgotten something | 13/03 10:14 |

copumpkin | but that I'm on the right track | 13/03 10:14 |

copumpkin | maybe I'll go to sleep | 13/03 10:15 |

Saizan | http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/ <- UCF' here is supposed to be data or codata? | 13/03 15:32 |

Mathnerd314 | ok, just made *yet another data structure* | 13/03 15:51 |

Mathnerd314 | that acts like ZipList most of the time | 13/03 15:52 |

Saizan | and the other?:) | 13/03 15:52 |

Mathnerd314 | the other is the ordinary Data.Colist (Haskell's list type) | 13/03 15:53 |

Mathnerd314 | the problem is that ZL (as I call it) is an infinite data structure 100% of the time | 13/03 15:58 |

Mathnerd314 | so I don't see how to display it | 13/03 15:58 |

Mathnerd314 | or test for equality | 13/03 15:59 |

Saizan | write something like take :: Nat -> ZL a -> List a, to get prefixes | 13/03 15:59 |

Saizan | see \~~ in Data.Colist for an useful definition of equality, though it's not decidable if two arbitrary streams are equal | 13/03 16:02 |

Mathnerd314 | ok, that works. | 13/03 16:41 |

Mathnerd314 | and ZL works on examples! | 13/03 16:44 |

Mathnerd314 | because the intermediate results aren't proper lists | 13/03 16:45 |

Mathnerd314 | but they are ZL's | 13/03 16:45 |

* Mathnerd314 celebrates | 13/03 16:53 | |

Saizan | nice :) | 13/03 16:54 |

Saizan | do you have the code somewhere? | 13/03 16:54 |

Mathnerd314 | http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8541#a8541 | 13/03 16:56 |

Mathnerd314 | (haskell, since I still am fuzzy on Agda) | 13/03 16:57 |

Mathnerd314 | so, normal lists [a,b,c] look like a ZL of {a,b,c,E,E,E,E,...} | 13/03 16:59 |

Mathnerd314 | and infinite lists look like {x,x,x,x,x,...} | 13/03 16:59 |

Mathnerd314 | but you get all these weird ones like {E,x,E,x,...} | 13/03 17:00 |

Mathnerd314 | which need to exist for the monad to preserve associativity | 13/03 17:00 |

Mathnerd314 | (and that disappear in normal cases of lift/zipWith) | 13/03 17:01 |

Saizan | that ZL type reminds me of dataflow programming, where the Events have different clocks | 13/03 17:02 |

Saizan | s/clocks/periods/ or whatever they are called | 13/03 17:02 |

Mathnerd314 | yeah, that's where I got the idea (particularly lucid) | 13/03 17:02 |

Mathnerd314 | it calls them streams | 13/03 17:02 |

Mathnerd314 | come to think of it, I can probably say a ZList is an infinite list of Maybe a... | 13/03 17:03 |

Saizan | yeah | 13/03 17:04 |

Saizan | then the Applicative is just the composition of ZipList and Maybe applicatives | 13/03 17:04 |

Mathnerd314 | and all the functions are a bit shorter | 13/03 17:05 |

Saizan | yup | 13/03 17:05 |

Mathnerd314 | hm, now my code has a lot of "f (Cons a b) = Cons (f a) (f b)" and "g a = Cons (g a) (g b)" | 13/03 17:54 |

Saizan | really? | 13/03 17:56 |

Saizan | not f (Cons a b) = Cons (g a) (f b) ? | 13/03 17:56 |

Saizan | i.e. folds? | 13/03 17:56 |

Mathnerd314 | well, the two instances of f have different type arguments | 13/03 17:57 |

Saizan | ah, sure | 13/03 17:57 |

Saizan | sounds like you could do f x = fmap f x | 13/03 17:58 |

Mathnerd314 | actually, that pattern is only used in my definition of fmap ;-) | 13/03 18:03 |

Mathnerd314 | it's only the second, g a = Cons (g a) (g b) | 13/03 18:03 |

Mathnerd314 | in fact... that's pretty much my entire code | 13/03 18:05 |

Mathnerd314 | I don't even need all the specifics. | 13/03 18:10 |

Mathnerd314 | it's probably a monad combinator or something... | 13/03 18:13 |

Mathnerd314 | so, for example, I have fmap f (Cons a b) = Cons (fmap f a) (fmap f b) | 13/03 18:40 |

Mathnerd314 | how do I make Cons an instance of Functor? | 13/03 18:41 |

Saizan | afaik there's no way to avoid that pattern, OTOH you could use DeriveFunctor in ghc-6.12 | 13/03 18:46 |

Mathnerd314 | I'm just trying to figure out what I would write for the instance declaration. | 13/03 18:52 |

Mathnerd314 | I think I need... 3 type variables? | 13/03 18:54 |

copumpkin | you can't do that | 13/03 18:55 |

Mathnerd314 | why? :-( | 13/03 18:56 |

copumpkin | well what are the types of Cons? maybe you can | 13/03 18:56 |

Mathnerd314 | data Cons a b = Cons a b | 13/03 18:56 |

copumpkin | fmap f (Cons a b) = Cons a (fmap f b) is the only thing you can do there | 13/03 18:57 |

copumpkin | the Functor is actually (Cons a), so you can't change the a | 13/03 18:58 |

copumpkin | fmap :: (a -> b) -> (Cons c) a -> (Cons c) b | 13/03 18:58 |

Mathnerd314 | fmap :: (Functor c) => (a -> b) -> (Cons c) a -> (Cons c) b, you mean? | 13/03 19:01 |

copumpkin | the thing about functor is that you don't have control over what types it ranges over | 13/03 19:12 |

copumpkin | so not that | 13/03 19:12 |

Saizan | Mathnerd314: you'd need BiFunctor from category-extras | 13/03 19:13 |

byorgey | Mathnerd314: that doesn't make sense, Functor only applies to things of kind * -> * | 13/03 19:17 |

byorgey | for example it doesn't make sense to say Functor Int, only something like Functor Maybe, or Functor List, or ... | 13/03 19:17 |

Mathnerd314 | well, Cons is of kind * -> * -> * | 13/03 19:18 |

byorgey | indeed. | 13/03 19:18 |

byorgey | so it can't be an instance of Functor. but (Cons a) can, for any a. | 13/03 19:18 |

byorgey | hmm, why are we talking about this in #agda? =) | 13/03 19:19 |

Saizan | if you squint enough it's valid agda too :) | 13/03 19:20 |

byorgey | hehe | 13/03 19:20 |

copumpkin | * looks just like Set to me | 13/03 19:22 |

copumpkin | :) | 13/03 19:22 |

Mathnerd314 | how do you even write algebraic data types in Agda? | 13/03 19:31 |

byorgey | Mathnerd314: the syntax is very close to the syntax for writing GADTs in Haskell. | 13/03 19:37 |

Mathnerd314 | oh, data x : x where x | 13/03 19:38 |

byorgey | yep | 13/03 19:39 |

byorgey | a line for each constructor with its type, etc. | 13/03 19:39 |

Mathnerd314 | so data Cons : Set1 where cons : ∀ { A B } → A → B → Cons ? | 13/03 19:42 |

Mathnerd314 | when Cons was still ZL, it was ZL a = Cons (Maybe a) (ZL a) - so Maybe and ZL were functors/monads/etc. given as type variables | 13/03 19:44 |

Mathnerd314 | * not given | 13/03 19:47 |

Saizan | data Const (A : Set) (B : Set) : Set where cons : A → B → Cons A B | 13/03 20:12 |

Saizan | or data Cons : Set -> Set -> Set1 where cons : ∀ { A B } → A → B → Cons A B | 13/03 20:12 |

Mathnerd314 | I'm still thinking in Haskell... suppose I want fmap f (Cons a b) = Cons (fmap f a) (fmap f b) - is that a functor? | 13/03 20:28 |

copumpkin | no | 13/03 20:29 |

--- Day changed Sun Mar 14 2010 | ||

Mathnerd314 | so how do I specify the monad laws, so I can use them to prove properties of things containing monads? | 14/03 03:14 |

Mathnerd314 | magic? | 14/03 03:22 |

--- Day changed Wed Mar 17 2010 | ||

jotik | hi. Why does it sometimes complain inside { }0 that the text is read-only? | 17/03 11:33 |

jotik | emacs i mean. | 17/03 11:33 |

npouillard | jotik: only on the last space right? | 17/03 11:48 |

npouillard | jotik: or your are trying to use a command whose scope is beyond the end of the hole. | 17/03 11:49 |

RLLa | in pattern matching when value is wrapped into {}, what does it mean? | 17/03 11:56 |

RLLa | it looks like pattern matching on some argument that does not appear to be argument of my function but is an argument of some type that my function uses | 17/03 11:58 |

RLLa | of course, there is no mention of this is manual | 17/03 11:59 |

RLLa | in* | 17/03 11:59 |

RLLa | so can someone confirm it | 17/03 11:59 |

npouillard | RLLa: {...} denotes implicit arguments both in the types (f : ∀ {A : Set} ...), the expressions (f {ℕ}) and the patterns (f {A} ... = ...) | 17/03 12:24 |

RLLa | uh oh | 17/03 12:24 |

npouillard | RLLa: was it clear enough ? | 17/03 12:24 |

RLLa | certanly not | 17/03 12:25 |

npouillard | let's take an example | 17/03 12:25 |

RLLa | well, i'm trying to implement well-known tabulate function here | 17/03 12:25 |

npouillard | sure | 17/03 12:25 |

npouillard | id : ∀ {A : Set} → A → A | 17/03 12:25 |

npouillard | id {A} x = x | 17/03 12:26 |

npouillard | then a test | 17/03 12:26 |

npouillard | id {ℕ} zero | 17/03 12:26 |

RLLa | it just restricts type? | 17/03 12:26 |

npouillard | nop | 17/03 12:26 |

npouillard | compare this with: | 17/03 12:26 |

npouillard | id' : ∀ (A : Set) → A → A | 17/03 12:27 |

npouillard | id' A x = x | 17/03 12:27 |

npouillard | test | 17/03 12:27 |

npouillard | id' ℕ zero | 17/03 12:27 |

npouillard | in id' the type argument is explicit | 17/03 12:27 |

npouillard | in id it is implicit, this means that in most cases I can write (id zero) without giving the type | 17/03 12:27 |

npouillard | but if I want it, I can by using the {} | 17/03 12:28 |

npouillard | clearer ? | 17/03 12:28 |

RLLa | implicit arg thing is clear | 17/03 12:28 |

RLLa | but not in pattern matching | 17/03 12:28 |

npouillard | ok | 17/03 12:29 |

npouillard | I could have written the "id" body like this | 17/03 12:29 |

npouillard | id x = x | 17/03 12:29 |

RLLa | yes | 17/03 12:29 |

npouillard | but if I do need the implicit argument I can caputre it with {A} | 17/03 12:29 |

npouillard | example | 17/03 12:29 |

npouillard | len : ∀ {A : Set} {n : ℕ} (xs : Vec A n) → ℕ | 17/03 12:30 |

npouillard | len {_} {n} _ = n | 17/03 12:30 |

RLLa | don't you have to use {n} on rhs too? | 17/03 12:30 |

npouillard | len (1 ∷ 2 ∷ 3 ∷ []) ≡ 3 | 17/03 12:30 |

npouillard | nop | 17/03 12:30 |

npouillard | in expression {...} are used to pass implicit arguments to functions | 17/03 12:31 |

npouillard | f {x} {y} z t | 17/03 12:31 |

RLLa | very good | 17/03 12:31 |

RLLa | i understand this now | 17/03 12:31 |

npouillard | but {x} means nothing by itself in expression | 17/03 12:31 |

npouillard | RLLa: cool | 17/03 12:32 |

RLLa | but is it possible to define tabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n without using {...}? | 17/03 12:33 |

npouillard | yes but using it will be ackward | 17/03 12:33 |

npouillard | imagine: | 17/03 12:33 |

npouillard | len' : ∀ (A : Set) (n : ℕ) (xs : Vec A n) → ℕ | 17/03 12:34 |

npouillard | len' _ n _ = n | 17/03 12:34 |

npouillard | test | 17/03 12:34 |

npouillard | len' ℕ 3 (1 ∷ 2 ∷ 3 ∷ []) ≡ 3 | 17/03 12:34 |

npouillard | you kind of have to give the answer as argument yourself. | 17/03 12:34 |

RLLa | ah, you have to give N and 3 as explicit actual arguments | 17/03 12:35 |

npouillard | yes | 17/03 12:35 |

npouillard | actually you can give _ and let the type-checker try to guess it | 17/03 12:35 |

RLLa | but i meant definition of tabulate not type signature | 17/03 12:35 |

npouillard | RLLa: all three should follow the same scheme: type, patterns, expressions | 17/03 12:36 |

RLLa | hm | 17/03 12:36 |

npouillard | however you can first define a function with explicit arguments and expose a short definition with implicit argus | 17/03 12:36 |

RLLa | anyway, here is my definition: tabulate {s n} f = (f (fz {n})) :: (tabulate {n} (λ x → f (fs x))) | 17/03 12:36 |

RLLa | my question was can you define it without matching on Nat | 17/03 12:37 |

npouillard | what is your type for tabulate | 17/03 12:37 |

npouillard | tabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n | 17/03 12:38 |

npouillard | ? | 17/03 12:38 |

RLLa | yes | 17/03 12:38 |

npouillard | and you have a second equation about 0 ? | 17/03 12:38 |

RLLa | yes | 17/03 12:38 |

RLLa | but that's trivial case | 17/03 12:38 |

npouillard | RLLa: so, if you have 2 equations something in the pattern must distinguish them | 17/03 12:39 |

npouillard | have you tried to write the second line as: | 17/03 12:39 |

npouillard | tabulate f = f fz :: tabulate (λ x → f (fs x)) | 17/03 12:40 |

npouillard | ? | 17/03 12:40 |

RLLa | hm, let me see | 17/03 12:40 |

npouillard | maybe the type-checker can infer them | 17/03 12:40 |

RLLa | hm, yes | 17/03 12:41 |

RLLa | but is it good idea to let type-checker infer things? | 17/03 12:41 |

npouillard | RLLa: yes | 17/03 12:43 |

npouillard | Agda inference system only fills a hole when the answer is unique and directed by the typechecking of the rest | 17/03 12:43 |

RLLa | hm, it looks more like complete magic | 17/03 12:44 |

npouillard | which is a limitation but on the plus side we can be sure of the safety of it | 17/03 12:44 |

npouillard | :) | 17/03 12:44 |

RLLa | hehe, it might be ok if you know what's going on there but it just confuses me time to time | 17/03 12:45 |

npouillard | something you can do is to put a ? instead of _ and then in emacs "C-x =" get the infered value | 17/03 12:48 |

Saizan | oh, i didn't know that | 17/03 12:49 |

npouillard | Saizan: what ? | 17/03 12:50 |

Saizan | the "C-x =" command | 17/03 12:51 |

Saizan | though it doesn't seem to work in my code | 17/03 12:51 |

npouillard | maybe it's C-c = | 17/03 12:52 |

* npouillard use viper and so have other bindings | 17/03 12:53 | |

Saizan | found it in the menu | 17/03 12:54 |

Saizan | though if the term contains applications of record fields you get something very ugly | 17/03 12:57 |

jotik | npouillard: Sry for my absence. Duty called. | 17/03 14:28 |

jotik | npouillard: I was just trying to type into the hole | 17/03 14:28 |

npouillard | jotik: no problem, got it to work ? | 17/03 14:45 |

jotik | npouillard: well yes somehow. I haven't yet figured out what causes this to happen. | 17/03 14:57 |

jotik | bbl | 17/03 14:59 |

Saizan | inside Pig, is there a command like whatis but that gives you only the pretty-printed term? | 17/03 16:41 |

--- Day changed Thu Mar 18 2010 | ||

Mathnerd314 | is there a good representation for a monad in agda? | 18/03 20:23 |

Jaak | there is one in the "standard" library | 18/03 20:26 |

Mathnerd314 | I want to prove the monad laws, which are missing from that | 18/03 20:27 |

Jaak | yeah, you have to extend it if you want this | 18/03 20:27 |

Mathnerd314 | agda does not seem like a friendly language... | 18/03 20:29 |

Jaak | no it's not :> | 18/03 20:30 |

Saizan | mh, why not? | 18/03 20:30 |

Saizan | coming from haskell i felt quite at home after a while :) | 18/03 20:30 |

Jaak | knowing haskell does help | 18/03 20:31 |

Jaak | but still, brain explosion can't be considered friendly | 18/03 20:31 |

Mathnerd314 | that's just it... there's no brain explosion yet. | 18/03 20:33 |

Jaak | i actually have some monad code around here | 18/03 20:34 |

Jaak | with proofs of laws for maybe monad :\ | 18/03 20:35 |

Mathnerd314 | oh, that's the first monad I would implement. | 18/03 20:37 |

Saizan | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24115#a24115 <- state is quite easy :) | 18/03 20:47 |

Jaak | list is working out quite well too | 18/03 20:47 |

Jaak | yeah, it's pretty nice exercise | 18/03 20:59 |

copumpkin | Saizan: wow, that was a lot of work, eh :P | 18/03 21:07 |

copumpkin | you could've saved 3/4 of the proof characters you typed, by the way | 18/03 21:08 |

Saizan | defining r = refl ? | 18/03 21:08 |

copumpkin | _ | 18/03 21:08 |

Saizan | oh | 18/03 21:08 |

copumpkin | it saves so much work | 18/03 21:09 |

copumpkin | I love it | 18/03 21:09 |

Saizan | i thought that only worked for \top | 18/03 21:09 |

copumpkin | anything it can infer unambiguously, as far as I can tell | 18/03 21:10 |

copumpkin | I use it for tedious types I can't be bothered to type out | 18/03 21:10 |

Jaak | not really much work saved. i think most of it it result of "refine" command | 18/03 21:10 |

Jaak | ah | 18/03 21:10 |

copumpkin | (I was just being silly about saving work, but I do like using it) | 18/03 21:10 |

Saizan | yeah, i've used it in types and expressions in EquationalReasoning | 18/03 21:11 |

Saizan | though i thought that it wouldn't work for data constructors for some reason | 18/03 21:11 |

Saizan | i guess that since we can prove "unique : ∀ {A : Set} {a b : A} (x y : a ≡ b) -> x ≡ y" there's no reason it shouldn't | 18/03 21:14 |

copumpkin | yeah | 18/03 21:21 |

--- Log closed Thu Mar 18 23:13:56 2010 | ||

--- Log opened Thu Mar 18 23:14:02 2010 | ||

-!- Irssi: #agda: Total of 30 nicks [0 ops, 0 halfops, 0 voices, 30 normal] | 18/03 23:14 | |

-!- Irssi: Join to #agda was synced in 73 secs | 18/03 23:15 | |

--- Day changed Fri Mar 19 2010 | ||

Jaak | hmm, im not having much luck proving comonad laws for stream comonad | 19/03 02:38 |

Jaak | i think i dont understand agda coinduction stuff yet | 19/03 02:38 |

Jaak | i gather that i need different equality than the propositional equality? | 19/03 02:57 |

glguy | Can I set the fixity of an operator that is a parameter to a type? | 19/03 03:19 |

glguy | record R (_+_ : ...) where ... infix 5 _+_ | 19/03 03:20 |

liyang_ | Jaak: yes. See stdlib/{Data/{Conat,Covec},Coinduction}.agda for examples and details. | 19/03 03:50 |

Jaak | liyang: thanks | 19/03 14:35 |

Jaak | the module system is confusing me a lot. is there some up to date read on it? | 19/03 14:54 |

npouillard | Jaak: not that much, better I got was in some talks about it in the agda repo | 19/03 14:54 |

Saizan | i've learned what i know by the reference manual and seeing it used in the standard library | 19/03 14:54 |

Jaak | first result on google is a talk from 2006, im don't know if it's current | 19/03 14:54 |

Jaak | i* | 19/03 14:55 |

RLa | there is a module system for agda? | 19/03 14:55 |

Saizan | what are you confused about, specifically? | 19/03 14:55 |

npouillard | RLa: yes | 19/03 14:55 |

Saizan | it's similar to ML functors | 19/03 14:56 |

npouillard | Saizan: not that much, you cannot take modules as arguments | 19/03 14:57 |

npouillard | only values | 19/03 14:57 |

npouillard | and so records which in turns are equipped with a module | 19/03 14:57 |

Saizan | true | 19/03 14:57 |

* npouillard would really like a nice up to date, paper/presentation of the design choices of the agda module system | 19/03 14:58 | |

Jaak | Saizan: i'm not too sure. might be confusion over the standard library | 19/03 15:01 |

Jaak | i have defined a setoid but i dont really know how to use it for equational reasoning | 19/03 15:03 |

Saizan | import Relation.Binary.EqReasoning as EqR; open EqR yoursetoid | 19/03 15:05 |

Saizan | "open EqR yoursetoid" is a shorthand for "module M = EqR yoursetoid; open M" i think | 19/03 15:06 |

Jaak | awesome, seems to work now | 19/03 15:09 |

Mathnerd314 | can Agda prove termination of loops? | 19/03 20:08 |

fax | ??? yes | 19/03 20:11 |

Saizan | that question can be interpreted in many ways :) | 19/03 20:11 |

fax | Mathnerd314: Agda is a logic which is strong enough for analysis | 19/03 20:11 |

fax | at least | 19/03 20:11 |

Saizan | so if you define a language which has loops and its semantics you can prove that | 19/03 20:16 |

Saizan | or were you referring to recursive definitions in agda itself? | 19/03 20:16 |

Saizan | in that case there's a termination checker that checks that the definition is structurally recursive on some argument, and you can use the "well-founded recursion" technique if that's not enough | 19/03 20:17 |

Mathnerd314 | my problem is that I can't think of any complicated examples of infinite loops... | 19/03 20:25 |

fax | and | 19/03 20:38 |

fax | if (UNPROVED CONJECTURE) then LOOP else HALT | 19/03 20:38 |

Mathnerd314 | oh, that 3x+1 conjecture sounds good. | 19/03 20:44 |

fax | what are you doing this for | 19/03 20:46 |

Mathnerd314 | some small amusement... | 19/03 20:47 |

fax | no | 19/03 20:48 |

fax | I mean like | 19/03 20:48 |

fax | what is it you are doing | 19/03 20:48 |

fax | i don't think you are going to prove 3x+1 terminates | 19/03 20:48 |

fax | for example | 19/03 20:48 |

Mathnerd314 | I was coming up with an example where proving termination is difficult | 19/03 20:50 |

Mathnerd314 | I have one, so now I'm good. | 19/03 20:51 |

fax | im just curious why | 19/03 20:51 |

Mathnerd314 | ... I couldn't see anything in-between "while(true) {}" and the Halting Problem | 19/03 21:10 |

fax | there's a very interesting one | 19/03 21:12 |

fax | hydra | 19/03 21:12 |

copumpkin | fax: what's that one? | 19/03 21:40 |

fax | you cut of its head and it grows infinity more | 19/03 21:41 |

fax | so the question is does hercules win (and the answer is yes he always wins) | 19/03 21:41 |

fax | but you must use ordinal analysis to prove termination | 19/03 21:41 |

fax | this is a non-trivial termination argument | 19/03 21:41 |

fax | http://coq.inria.fr/distrib/V8.2rc1/contribs/Cantor.epsilon0.Hydra.html | 19/03 21:41 |

kmc | fax, looks fun, is there a more commented / coqdoc'd version? | 19/03 21:48 |

fax | Idon tkno | 19/03 21:48 |

fax | Mathnerd314 depth first algorithm to four color a planar map | 19/03 21:49 |

copumpkin | coqbloq? | 19/03 21:49 |

fax | :[ | 19/03 21:49 |

copumpkin | :) | 19/03 21:50 |

* Mathnerd314 is confused | 19/03 21:51 | |

fax | Mathnerd314, you don't know about four colors suffice? | 19/03 21:52 |

Mathnerd314 | well, I know that. | 19/03 21:52 |

fax | I am just telling you examples that came to me | 19/03 21:53 |

fax | this is a really good one, because I bet we all wrote this program too (I mean... without a termination proof) | 19/03 21:53 |

copumpkin | use four colors to color an arbitrary tiling of the surface of a torus! | 19/03 21:54 |

fax | 7 ? | 19/03 21:54 |

copumpkin | 4 is so much more badass | 19/03 21:54 |

copumpkin | I bet chuck norris could do it | 19/03 21:55 |

Mathnerd314 | impossible! | 19/03 21:55 |

fax | p=\left\lfloor\frac{7 + \sqrt{1 + 48g }}{2}\right\rfloor (Weisstein). | 19/03 21:55 |

fax | lol | 19/03 21:55 |

fax | how many colors you need for a thing with genus g | 19/03 21:55 |

fax | no idea how they come up with that.. but the proof on a torus is apparently much easier than a sphere | 19/03 21:56 |

fax | (sphere of course corresponds to planar) | 19/03 21:56 |

copumpkin | simple! | 19/03 21:56 |

--- Day changed Sat Mar 20 2010 | ||

glguy_ | Does this approach to defining categories and functors make sense? http://www.galois.com/~emertens/category/category.html | 20/03 02:44 |

glguy_ | I tried to follow the spirit of things like IsPreorder and Preorder | 20/03 02:44 |

--- Day changed Sun Mar 21 2010 | ||

fax | "In order for the memory footprint of the typechecker to ﬁt within the | 21/03 13:02 |

fax | physical memory of the machine, we were forced to factor the proof – sometimes | 21/03 13:02 |

fax | unnaturally – into several submodules." | 21/03 13:02 |

fax | heh | 21/03 13:02 |

Mathnerd314 | fax: what would need such a large proof? | 21/03 14:05 |

fax | Mathnerd314, I think it's more agda than the proof being big | 21/03 14:05 |

fax | this is from the dependently typed grammars paper | 21/03 14:06 |

--- Day changed Mon Mar 22 2010 | ||

roberto_ | Hi all. I'm trying to compile an agda "Hello world" example (main : IO Unit [[newline]] main = putStrLn "Hello world!") | 22/03 03:42 |

roberto_ | I get the following error | 22/03 03:43 |

roberto_ | Basics.agda:1,1-1 | 22/03 03:43 |

roberto_ | Basics.agda:1,1: Parse error | 22/03 03:43 |

roberto_ | main<ERROR> : IO Unit main = putStrLn "He... | 22/03 03:43 |

roberto_ | what's wrong with it? | 22/03 03:44 |

dolio | Is that all that's in the file? | 22/03 03:49 |

dolio | Those two lines, that is. | 22/03 03:49 |

dolio | I don't think Agda lets you omit the "module Foo where" line. | 22/03 03:50 |

dolio | Foo being the name of the file. | 22/03 03:50 |

roberto_ | Thanks. Done. Now I get "Not in scope ... when scope checking IO Unit " | 22/03 03:58 |

dolio | You also have to import the modules that define IO and such. | 22/03 04:02 |

dolio | I've never really used IO in agda, though. I can't help you beyond that. | 22/03 04:03 |

roberto_ | Now I did an "open import IO.Primitive" and it works for IO. | 22/03 04:23 |

roberto_ | "open import Data.Unit" did not work for "Unit" | 22/03 04:23 |

dolio | Unit doesn't exist. It's named \top | 22/03 04:24 |

dolio | Which looks like a T. | 22/03 04:24 |

dolio | \top being how you type it in in the agda emacs mode. | 22/03 04:24 |

dolio | ⊤ | 22/03 04:25 |

roberto_ | I was with command line and an "normal" text editor. Now I see It doesn't work that way. I'll try to compile with adga emacs mode (already set-up) next time. | 22/03 04:29 |

roberto_ | and get used to that | 22/03 04:29 |

dolio | It's quite helpful. | 22/03 04:30 |

roberto_ | I think so. I still have to get used to it. | 22/03 04:31 |

roberto_ | Thanks for your help. | 22/03 04:32 |

dolio | No problem. | 22/03 04:33 |

temoto | Can i define [_for_in_] python-like list comprehension operator in agda? | 22/03 16:20 |

stevan | perhaps. what's the type? | 22/03 16:25 |

temoto | Well... | 22/03 16:36 |

temoto | [ x for x in list ] is equal to just list | 22/03 16:37 |

temoto | [ even x for x in list ] is equal to map even list | 22/03 16:38 |

temoto | so i'm not sure what is type of first subexpression | 22/03 16:39 |

temoto | just a or a → b defaulting to id | 22/03 16:40 |

fax | what?? | 22/03 16:47 |

temoto | ah.. forget it | 22/03 16:48 |

pigworker | Should I be able to make a program parse by removing a line break after a semicolon? | 22/03 21:18 |

fax | pigworker: I'm no agda implementor but does sound fishy to me | 22/03 21:23 |

stevan | i think it makes sense. | 22/03 21:24 |

pigworker | I've got a bunch of short definitions to put in a let..in, and I'm hoping to write them 2 or 3 to a line. | 22/03 21:25 |

stevan | you don't need semicolons to do that? | 22/03 21:26 |

fax | I would get something to do with indentation, but I've never observed this kind of thing.. | 22/03 21:27 |

dolio | let has sort of layout like in Haskell. | 22/03 21:27 |

dolio | So it probably doesn't expect you to put a semicolon at the end of one let line. | 22/03 21:27 |

dolio | Only in beteween definitions on the same line. | 22/03 21:27 |

pigworker | yeah, I'm wondering what the rules are; I can put 'em all on one line with semicolons, or one per line without | 22/03 21:28 |

dolio | You can mix. I just tried it. | 22/03 21:28 |

dolio | let i = 0 ; j = 1 <newline> k = 2 in k | 22/03 21:28 |

dolio | As long as you align k with i. | 22/03 21:28 |

dolio | The first k, that is. | 22/03 21:29 |

pigworker | Yep, that works. I thought I tried that a while ago, but I must have screwed up the alignment. | 22/03 21:29 |

dolio | That's easy to do with unicode characters, at least for me. | 22/03 21:30 |

dolio | Some of them aren't really monospace, but they count as one character. | 22/03 21:30 |

pigworker | Not a problem which afflicts me, as I haven't the energy for unicode. | 22/03 21:31 |

pigworker | I'm about to try it *interactively*. | 22/03 21:31 |

pigworker | Ah. I can't align stuff interactively. I just have to tidy it up once it's done. | 22/03 21:33 |

maltem | Btw does anyone know of a terminal emulator & font combination that will print characters like → at a readable size? | 22/03 21:33 |

maltem | It seems to me that one can have emacs print those at a larger size than what monospace would actually give you | 22/03 21:34 |

liyang | I've given up on trying to find a monospace font that works. I align at the start of lines in Emacs, and if I need to do any intra-line spacing for lhs2TeX, I do that in Vim instead. | 22/03 21:58 |

pigworker | Sometimes I wish Ulf's implementation of pattern unification understood records (not that mine ever did). | 22/03 22:01 |

kosmikus | pigworker: you on irc? nice ... | 22/03 22:04 |

pigworker | kosmikus: I saw a link to a free mac client on the Agda wiki, and decided to check it out | 22/03 22:05 |

kosmikus | good work :) | 22/03 22:06 |

kosmikus | pigworker: will you be here more often? | 22/03 22:09 |

pigworker | kosmikus: too early to tell; I'm experimenting with a new form of displacement... | 22/03 22:11 |

fax | we've had Pierre-Evariste, Edwin b, Peter Morris.. now CONor | 22/03 22:12 |

fax | :D | 22/03 22:12 |

stevan | this is the unofficial epigram2 channel after all. | 22/03 22:12 |

fax | yeah well there's been an epigram channel but on average 1 person at a time there | 22/03 22:13 |

kosmikus | I didn't know there is one | 22/03 22:13 |

pigworker | most of the serious work on epigram2 gets prototyped in agda anyway | 22/03 22:13 |

kosmikus | I'd join ;) | 22/03 22:13 |

fax | it roughly doesn't exist | 22/03 22:13 |

fax | to say, 5 decimal places | 22/03 22:13 |

kosmikus | pigworker: as long as you're not claiming that epigram is going to be implemented in agda | 22/03 22:14 |

fax | She is sort of half way between haskell and agda? :) | 22/03 22:15 |

pigworker | kosmikus: no, but bits of it get weakly approximated, and that way we figure out what to implement | 22/03 22:16 |

kosmikus | fax: true. | 22/03 22:16 |

kosmikus | pigworker: yes, that's absolutely understandable. I'm also using Agda for that purpose more and more. | 22/03 22:16 |

pigworker | fax: in the tradition of Zeno | 22/03 22:16 |

dolio | So, here's something I've been wondering... | 22/03 22:20 |

dolio | When you eventually introduce a hierarchy of universes, if that's what you in fact do... | 22/03 22:21 |

dolio | What happens with regard to set equality vs value equality? | 22/03 22:21 |

dolio | I suppose that makes sense even now with Set : Set, as ! Set > Set == Set > Set ! | 22/03 22:22 |

pigworker | dolio: sets-as-values equality gets farmed out -- ! Set > S == Set > T ! = S <-> T | 22/03 22:24 |

pigworker | dolio: that stratifies, too... | 22/03 22:25 |

pigworker | I'm new here -- can someone tell me how to chuck a lump of code somewhere visible (is that what hpaste does? how do I use it?) | 22/03 22:26 |

dolio | So, for S : SetN, T : SetM, there's a S <-> T. | 22/03 22:26 |

dolio | Even if N /= M. | 22/03 22:26 |

kosmikus | pigworker: yes, hpaste will work | 22/03 22:26 |

kosmikus | pigworker: just go to hpaste.org, click new | 22/03 22:26 |

fax | TODO: Agda paste side | 22/03 22:26 |

dolio | Someone needs to write an agda hilighter for whatever coloring library hpaste uses. | 22/03 22:27 |

fax | I wonder what the complexity of agda syntax coloring is? | 22/03 22:27 |

pigworker | dolio: every universe has a <->, which gets used as the value equality for that universe-as-a-set in higher universes | 22/03 22:27 |

liyang | dolio: good luck. :) | 22/03 22:27 |

dolio | :) | 22/03 22:27 |

stevan | why not just a file uploader which typechecks the file and gives a link to the html output? | 22/03 22:27 |

kosmikus | stevan: should be a machine with lots of RAM ;) | 22/03 22:28 |

dolio | pigworker: I guess that just works out of universes are cumulative? | 22/03 22:28 |

dolio | If, even. | 22/03 22:28 |

stevan | perhaps the html generation thing could be tweaked so that it doesn't actually type check the file first, not sure how complicated that would be tho... | 22/03 22:29 |

kosmikus | good night | 22/03 22:31 |

pigworker | dolio: something like http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24263 | 22/03 22:32 |

pigworker | dolio: that model isn't fully cumulative yet, but its props are; it's a rather fierce piece of work, I admit | 22/03 22:34 |

fax | pigworker -- what I wanted to ask you (or thorsten, but I don't have the courage to email).. is what's going on with this induction-recursion PhD (if anything?) | 22/03 22:36 |

pigworker | fax: Thorsten hired a student a while back; it's no longer available | 22/03 22:38 |

fax | oh yeah I am in no position to write a PhD I'm just super curious if he's found some new data structures or anything :D | 22/03 22:39 |

fax | I probably just have to be patient.. | 22/03 22:39 |

fax | the only ones I know of are martin lofs one and fresh lists and the examples from Peter Dybjer | 22/03 22:40 |

pigworker | fax: it's more a question of figuring out which IR definitions make sense, and how | 22/03 22:40 |

fax | oh that's quite different than I had imagined then | 22/03 22:40 |

pigworker | big question just now -- if we can have IR definitions with large decoders, why can't we have inductive families with large indices? | 22/03 22:41 |

dolio | Agda seems to get along fine with it. | 22/03 22:42 |

dolio | As far as we know. | 22/03 22:42 |

dolio | No one's proved false lately. | 22/03 22:43 |

pigworker | dolio: I constructed an impredicative universe at one stage, because they forgot a check | 22/03 22:44 |

dolio | Heh. | 22/03 22:44 |

dolio | Although that is something I've wondered off and on... | 22/03 22:44 |

dolio | Are families indexed by Set "inductive" families? | 22/03 22:45 |

fax | hehe | 22/03 22:45 |

dolio | Set is not defined by induction. | 22/03 22:45 |

dolio | At least in Agda. | 22/03 22:45 |

pigworker | dolio: Agda allows large indices, but nobody knows if that's ok. | 22/03 22:46 |

* fax has yet to understand how anyone can actually follow normalization proofs for anything beyond systemf... | 22/03 22:46 | |

pigworker | dolio: and Gil Hur gets quite close to the bone, thanks to that... | 22/03 22:46 |

dolio | In that sense, the line that "GADTs are a special case of inductive families" isn't necessarily true. | 22/03 22:48 |

dolio | But, since GHC doesn't have inductively defined static things, there's no other choice. | 22/03 22:50 |

dolio | Not that people care about proofs of false in that environment anyhow. | 22/03 22:50 |

dolio | At least, I'm inclined not to. Some people were bothered by the fact that you could use impredicativity + injective type constructors to prove false in GHC. | 22/03 22:51 |

dolio | Even though there are 6 other ways to do the same thing. | 22/03 22:51 |

Mathnerd314 | what does it mean if you can prove false? | 22/03 22:53 |

dolio | It means you have a non-terminating 'value'. | 22/03 22:53 |

fax | what blows my mind is that people still go to the trouble of endcoding inductive proofs in haskell.. | 22/03 22:53 |

Mathnerd314 | so it's an infinite loop or something in the type checker? | 22/03 23:05 |

dolio | Well, the definition of false would be 'data False : Set where', so there are no proofs (constructors) for it. | 22/03 23:06 |

fax | Mathnerd314: needn't be | 22/03 23:06 |

liyang | Mathnerd314: Think of it as the type-theory equivalent of I JUST DIVIDED BY ZERO. OH SHI- | 22/03 23:06 |

dolio | So, the only way you could proof it is if you had some sort of infinite loop, or bottom-like value from Haskell. | 22/03 23:06 |

fax | forall P, P could be another definition | 22/03 23:06 |

Mathnerd314 | oh, so all it means is that your type checker is too lenient. | 22/03 23:16 |

dolio | Well, it could mean lots of things. | 22/03 23:17 |

dolio | Haskell, for instance, essentially adds fix as a primitive. And fix id has the right type. | 22/03 23:18 |

dolio | That's not a failure of the type system, per se. | 22/03 23:18 |

pigworker | Crucially, false hypotheses are relatively benign; it's closed proofs of false that behave badly. | 22/03 23:18 |

dolio | Haskell also has general recursive types, which let you type stuff like (\x -> x x) (\x -> x x) with some fiddling. | 22/03 23:21 |

dolio | So that's the kind of thing you'd want to rule out of your type system if you cared about it being a sound logic. | 22/03 23:22 |

fax | general recursive types aka negative types ? | 22/03 23:24 |

pigworker | Consistency also enables a class of optimizations: it's not just soundness for the sake of it. | 22/03 23:24 |

dolio | As I recall, GHC's inliner relies on the fact that you can't write (\x -> x x) (\x -> x x), which would inline forever. | 22/03 23:38 |

dolio | So, if you use negative types to trick it, it can go into infinite loops if you don't mark it noinline. | 22/03 23:38 |

Mathnerd314 | I can't figure out what that does... can it ever return a value? | 22/03 23:40 |

dolio | It reduces to itself forever. | 22/03 23:40 |

Mathnerd314 | right... but can you feed it arguments and get out values? | 22/03 23:41 |

dolio | No, it just spins. | 22/03 23:42 |

Mathnerd314 | so it's an infinite loop, suitably disguised? | 22/03 23:43 |

fax | it's not disguised | 22/03 23:43 |

dolio | I mean, denotationally, if you decide it's a function, then you can give it a value, and it will give you back the bottom value. | 22/03 23:43 |

Mathnerd314 | fax: it's disguised in lambda calculus, because usually infinite loops are in imperative languages | 22/03 23:44 |

fax | oh | 22/03 23:44 |

fax | yeah i don't think it's a roundabout way to represent a C program | 22/03 23:44 |

liyang | it's a special case of the fixpoint combinator, Y = \ f -> (\ x -> f (x x)) (\ y -> f (y y)) | 22/03 23:44 |

pigworker | liyang: is that why YI is so-called? | 22/03 23:48 |

liyang | pigworker: the editor? I have no idea… | 22/03 23:50 |

* fax thinks yes | 22/03 23:51 | |

fax | YI = I(YI) | 22/03 23:51 |

liyang | http://haskell.org/haskellwiki/Yi#Trivia says yes. | 22/03 23:51 |

pigworker | I'm wondering if SICK computes to anything interesting. | 22/03 23:52 |

liyang | I don't think naming a project after a non-terminating computation is a good idea. (Plus my dad's first name is Yi and it always weirds me out a bit when I hear people talking about the editor.) | 22/03 23:53 |

pigworker | SICK = IK(CK) = K(CK) | 22/03 23:54 |

pigworker | liyang: I was thinking of the editor; I had a spinning editor situation earlier. | 22/03 23:56 |

pigworker | Ah nice, KISS IS S | 22/03 23:57 |

fax | YUCK = UUUUUUUUU(YUCK) | 22/03 23:57 |

liyang | pigworker: related to the spinning Aquamacs on Twitter earlier? | 22/03 23:59 |

--- Day changed Tue Mar 23 2010 | ||

pigworker | liyang: the very same; ironic, given the proof was about productive coprograms | 23/03 00:00 |

edwinb | good lord, it's pigworker! | 23/03 00:06 |

edwinb | evening | 23/03 00:06 |

pigworker | edwinb: not quite sure how that happened | 23/03 00:07 |

fax | pigworker -- did you ever 'To Mock a Mockingbird'? :) | 23/03 00:07 |

fax | (lovely book... embossed cover and rough pages) | 23/03 00:08 |

pigworker | fax: my Smullyan coverage is thin, and doesn't make it that far | 23/03 00:08 |

edwinb | pigworker: how is your agda based central heating system? | 23/03 00:09 |

pigworker | edwinb: cooler, now that I've been distracted | 23/03 00:10 |

liyang | *whooooosh* | 23/03 00:14 |

liyang | What was that? Sounded like productivity. | 23/03 00:14 |

fax | good luck making pigs fly anyway ! | 23/03 00:15 |

edwinb | I hear it happens sometimes | 23/03 00:15 |

pigworker | just doing some of the exercises I set in my blog post | 23/03 00:23 |

edwinb | Hmm, I think I'll wait until morning to catch up with that bit of blogland... | 23/03 00:41 |

* Mathnerd314 finds pigworker's blog | 23/03 01:02 | |

pigworker | g'night all; see yiz round | 23/03 01:29 |

stepcut | if I have: data Bool : Set where true : Bool ; false : Bool, is there a way to make a function, trueId : true -> true | 23/03 04:18 |

liyang | Won't Function.id do the job? | 23/03 04:20 |

stepcut | well, I want to apply it only to true values.. | 23/03 04:21 |

stepcut | a better question might be.. | 23/03 04:21 |

stepcut | if I have a List Int, can I write a function that can only be applied to a list that starts with the number 1.. | 23/03 04:21 |

liyang | I don't quite get your type signature though. true is a value of Bool, and you can write functions of type Bool -> Bool. | 23/03 04:21 |

liyang | stepcut: sure. Require a proof that the list starts with 1 as another parameter. | 23/03 04:22 |

stepcut | liyang: sounds easy :) | 23/03 04:22 |

liyang | Once you see it… | 23/03 04:23 |

stepcut | yes, that has been my problem so far | 23/03 04:23 |

stepcut | it's easy after I see it, but not before :p | 23/03 04:24 |

stepcut | I sort of came up with something that works, by creating a new type | 23/03 04:24 |

stepcut | but I haven't figure out if it is a weird way to do it yet :) | 23/03 04:24 |

stepcut | http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a24272 | 23/03 04:25 |

stepcut | I have a list (or 'string') of symbols. M I U, and a rule1 which can only be applied to a string that starts with M | 23/03 04:26 |

stepcut | but I am not sure how to make rule1 a 'function' instead of a 'constructor' | 23/03 04:26 |

liyang | (Sorry, my Aquamacs is taking forever to go through its spin cycle. Hang on…) | 23/03 04:28 |

liyang | http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24273#a24273 | 23/03 04:31 |

liyang | Go into that hole, and refine-case on the xs≡1∷ argument. | 23/03 04:31 |

stepcut | ok | 23/03 04:31 |

liyang | (and again on the second part of the product ^^;;) | 23/03 04:33 |

stepcut | I don't think I did it right. I loaded the buffer. Then I went to the beginning of {!xs≡1∷!} and hit C-c C-c, and it changed the line to, oneHead xs (x , y) = {!!} | 23/03 04:35 |

liyang | Okay, now put y into the hole and do that again. | 23/03 04:38 |

stepcut | and then x ? | 23/03 04:38 |

stepcut | now I have, oneHead .(1 ∷ x ∷ xs) (x ∷ xs , ≡.refl) = {!!} | 23/03 04:40 |

liyang | So inspecting the proof forces the first argument to begin with a 1. :) | 23/03 04:42 |

liyang | (the x in (x , y) is just the rest of the list. | 23/03 04:43 |

stepcut | right | 23/03 04:43 |

stepcut | I sort of understand how this works :) | 23/03 04:44 |

stepcut | time for bed now. thanks! | 23/03 04:45 |

stepcut | I think I understand what I have done with the System type in the code I was writing too.. | 23/03 04:46 |

liyang | Stream is a predicate on Strings generated by rule1 and initial. Or Stream is a type indexed by valid Strings generated by the aforementioned. A value of Stream xs is a a proof that you can be inspect, to reveal exactly what rules were applied to obtain xs. :3 | 23/03 04:52 |

liyang | http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a24274 | 23/03 04:53 |

stepcut | sweet! | 23/03 04:56 |

liyang | I hope that wasn't homework. :-/ | 23/03 04:58 |

stepcut | so with the rule1 function, I have an actual String of MU, and test function manipulates that String by applying rule1 and returns the modified results. | 23/03 04:58 |

stepcut | With the version I had the MU list only existed in the type system, and the constructors where building up a 'description' of the rules I had applied.. so the test function returned 'how' I got from one MU list to another.. | 23/03 05:00 |

stepcut | I didn't know people even had agda homework :p | 23/03 05:00 |

liyang | And in order to apply rule1, you need to supply a second argument—namely a proof that the first argument begins with M. | 23/03 05:00 |

liyang | stepcut: I'm aware of a few courses that teach it. :) | 23/03 05:00 |

stepcut | yeah | 23/03 05:00 |

stepcut | the MIU stuff is from 'Gödel, Escher, and Bach'. I am reading it for fun and it seemed like a small enough problem that I might be able to tackle it with my limited agda skills ;) | 23/03 05:01 |

liyang | OH SHI- Of course. I ought to have remembered. ^^;; | 23/03 05:02 |

stepcut | :) | 23/03 05:02 |

stepcut | I supposed it could be somebodies homework, but it's not mine :) | 23/03 05:04 |

stepcut | but it's already tomorrow now, so I gotta get to sleep, thanks again! | 23/03 05:04 |

liyang | It's useful to keep both notions handy: sometimes you *do* want an indexed data structure that provides evidence of how the result is obtained, rather than carrying around an explicit proof. | 23/03 05:05 |

stepcut | right | 23/03 05:05 |

liyang | (if that made any sense.) | 23/03 05:05 |

liyang | stepcut: for example, Data.List.Any.any not only returns a yes/no answer of whether some element of the list satisfies some property, it also tells you where it is. | 23/03 05:22 |

Svrog | does anyone here have any experience with twelf? i'm confused - trying to build a nat type out of integers by putting a constraint on the values that get passed in but can't seem to get it to work | 23/03 07:28 |

Svrog | as in i can't seem to get the constraint in the constructor - it works if i put a constraint somewhere else but i can't figure out what the difference is, more so since the same syntax seems to be used for defining types and constructors and functions so why it works in one definition but not in another one is bugging me | 23/03 07:33 |

TacticalGrace | Agda mode for TextMate would be great | 23/03 10:32 |

TacticalGrace | TextMate at least manages to do the unicode font rendering properly | 23/03 10:32 |

stevan | TacticalGrace and others complaining about aquamacs, have you tried http://emacsformacosx.com/ ? (I don't have a mac myself, just recalled seeing this a while ago and thought it might help). | 23/03 15:23 |

edwinb | I switched to that after I got fed up with aquamacs | 23/03 15:25 |

edwinb | It fixed the things that annoyed me, although I can't remember what those annoyances were... | 23/03 15:26 |

stevan | (if it works better, it might be appropriate to add a note about it on the wiki.) | 23/03 15:29 |

edwinb | I am not confident enough about that ;) | 23/03 15:30 |

edwinb | it was only minor annoyances for me | 23/03 15:30 |

liyang | It won't recognise the C-, in C-c C-, so I ended up adding a mapping from C-c , instead. | 23/03 19:01 |

fax | I was trying to think of a non induction+lots of finicky algebra proof of binomial theorem | 23/03 21:26 |

fax | like counting how many paths has k lefts in them in a size n perfect tree or something | 23/03 21:27 |

fax | never found a good way though | 23/03 21:27 |

fax | (when I said induction above I mean the P(n)=>P(n+1) stuff) | 23/03 21:27 |

--- Day changed Thu Mar 25 2010 | ||

lpjhjdh | is there a convenient way of constructing piecewise functions? | 25/03 02:37 |

liyang | Elaborate? What would be the inconvenient way? | 25/03 02:51 |

lpjhjdh | nested ifs | 25/03 02:52 |

lpjhjdh | I'm thinking something like with's that don't make me match everything, but then I see how it could be difficult to prove I handled all cases | 25/03 02:52 |

liyang | Have you got a particular example? (hpaste?) | 25/03 02:53 |

lpjhjdh | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a24345 | 25/03 02:54 |

lpjhjdh | I defined ≟ and ≠ cause I couldn't find simple boolean versions over nat | 25/03 02:54 |

glguy_ | You can at least do this: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a24346 | 25/03 02:56 |

lpjhjdh | ah, that's perfect, thanks | 25/03 02:57 |

glguy_ | You might actually be able to leave the false values as _ | 25/03 02:57 |

glguy_ | I'm just copy/paste mangling that | 25/03 02:57 |

liyang | er… I was going to use Data.Nat._≟_ which returns a proof of i == j if they are equal. | 25/03 03:03 |

lpjhjdh | I just used boolean cause I wasn't particularly interested in why they were or weren't equal | 25/03 03:14 |

stepcut | does agda have 'module functors' ? I know the module system is more advanced that haskell's, and reminds me of ocaml.. but is it technically correct to say it has module functors? | 25/03 22:34 |

--- Day changed Fri Mar 26 2010 | ||

roberto_ | Hi. | 26/03 02:55 |

roberto_ | quick question | 26/03 02:55 |

roberto_ | What does MAlonzo have anything to do with me? | 26/03 02:55 |

roberto_ | Seriously, I tried to compile simple agda examples with no success | 26/03 03:02 |

roberto_ | "The function `main' is not defined in module `MAlonzo.Qbasics'" (my "basics.agda" file is just a single line: "module basics where") | 26/03 03:12 |

lpjhjdh | so I'm having an issue with agda not being able to show that two things are equal | 26/03 03:45 |

lpjhjdh | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24380#a24380 | 26/03 03:46 |

liyang | Oh that's a very frequent problem. | 26/03 03:46 |

lpjhjdh | what is it resulting from? | 26/03 03:47 |

lpjhjdh | using much simpler types the following works out: presa (plusl stn) (ok-add wtn wtm) = ok-add (presa stn wtn) wtm | 26/03 03:47 |

lpjhjdh | I can expand on some of my types if it's not immediately obvious, I'm not familiar with the actual theory behind dependant types | 26/03 03:50 |

liyang | It's not immediately obvious. :( I'd look for where the e₀' was coming from. | 26/03 03:51 |

lpjhjdh | the go function is actually nothing, just trying to pattern match an ok-add | 26/03 03:52 |

liyang | (I mean, the general state of not being able to show two things equal in Agda is a frequent problem for me.) | 26/03 03:53 |

lpjhjdh | ah, yeah, before I was having issues with the "inj" stuff, but then I factored it out into an Injection type with the fromInj to turn it into a function which worked | 26/03 03:54 |

lpjhjdh | unfortunately I see no obvious way of "factoring" the e's that are the terms of the add :( | 26/03 03:54 |

lpjhjdh | is it maybe because it "forgets" since they become a single term? Namely the argument to the injection. | 26/03 03:58 |

liyang | I'm not really understanding what the code is doing, but I'd suggest inspecting / doing something with the injf argument. (Probably what you already said.) | 26/03 04:05 |

lpjhjdh | that seemed to be the problem. Sadly each time one thing gets fixed it introduces another issue | 26/03 05:05 |

liyang | It's a gift that never stops giving. | 26/03 05:20 |

guerrill1 | looks like lots of exciting stuff was discussed at the AIM.. sized types, structual equality, etc. etc. | 26/03 12:57 |

guerrill1 | anyone know what "Java Agda" means? | 26/03 12:57 |

guerrill4 | or "Agda-A" | 26/03 12:57 |

guerrill4 | ah "A new implementation of Agda written in Java " | 26/03 12:58 |

guerrill4 | that sounds cool | 26/03 12:58 |

andgra | I would like to prove http://pastebin.com/raw.php?i=NTQf6pqf but I do not understand how to use the 'subset' operator, I have looked at both Relation.Unary and Data.Sets and they're both confusing me... | 26/03 13:30 |

fax | andgra: what's the definition of it? | 26/03 13:34 |

andgra | the subset operator? | 26/03 13:35 |

fax | yes | 26/03 13:35 |

andgra | well, the one from Data.Sets (stdlib 0.3) is just _?_ : <Set> ? <Set> ? Set | 26/03 13:36 |

andgra | s1 ? s2 = ? x ? x ? s1 ? x ? s2 but | 26/03 13:36 |

fax | I cant read it | 26/03 13:36 |

fax | it's just question marsk | 26/03 13:36 |

Jaak | weird, that type doesn't even typecheck for me | 26/03 13:37 |

andgra | _ss_ : <Set> -> <Set> -> Set | 26/03 13:38 |

fax | what's the agda file | 26/03 13:38 |

andgra | but the definitions of <Set> I don't really understand | 26/03 13:38 |

andgra | Data.Sets in the standard library | 26/03 13:38 |

fax | is it actualyl called<Set> | 26/03 13:38 |

andgra | yes | 26/03 13:38 |

Jaak | so that type actually typechecks? | 26/03 13:39 |

andgra | it somehow wrapps DecSetoid from Relation.Binary | 26/03 13:39 |

fax | http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda | 26/03 13:39 |

fax | <Set> : Set | 26/03 13:39 |

fax | <Set> = DecSetoid.Carrier decSetoid | 26/03 13:39 |

fax | _⊆_ : <Set> → <Set> → Set | 26/03 13:39 |

fax | s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂ | 26/03 13:39 |

fax | andgra, can you see this correctly? | 26/03 13:39 |

andgra | yeah | 26/03 13:39 |

fax | okay good | 26/03 13:39 |

fax | so you want to pre | 26/03 13:39 |

fax | so you want to prove* | 26/03 13:40 |

fax | prf : ∀ {a b} {A C : Set a}{B : Set b} → (x : C) (f : A → B) → (C ⊆ A) → (f x) ⊆ B | 26/03 13:40 |

fax | prf = ? | 26/03 13:40 |

fax | which is the same as: | 26/03 13:40 |

fax | prf : ∀ {a b} {A C : Set a}{B : Set b} → (x : C) (f : A → B) → (∀ x → x ∈ C → x ∈ A) → (∀ x → x ∈ (f x) → x ∈ B) | 26/03 13:40 |

fax | ? | 26/03 13:40 |

fax | yeah what Jaak says... | 26/03 13:40 |

fax | why have your paste got Set a but the thing is <Set> ? | 26/03 13:41 |

Jaak | yeah, posting whole file that types might help | 26/03 13:41 |

fax | why not prf : {A B C : <Set>} → (x : C) (f : A → B) → (∀ x → x ∈ C → x ∈ A) → (∀ x → x ∈ (f x) → x ∈ B) ? | 26/03 13:41 |

andgra | well, in the paste I was using Relation.Unary but I'm guessing that will not work | 26/03 13:41 |

andgra | I haven't tried that... | 26/03 13:41 |

fax | Relation.Unary???????????? | 26/03 13:42 |

fax | why am I looking at this http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda | 26/03 13:42 |

andgra | I'm sorry - I have tried to use both because I'm not sure I completley understand the difference between them | 26/03 13:42 |

fax | andgra | 26/03 13:42 |

fax | why would you want to use either of them? | 26/03 13:43 |

guerrill4 | andgra: yeah, what are you trying to do - at a high level? | 26/03 13:44 |

andgra | hmm, maybe I don't. I was looking to do some work how functions project on sets so I started reading in the stdlib | 26/03 13:44 |

fax | project on sets? | 26/03 13:45 |

guerrilla | ? | 26/03 13:45 |

fax | guerrilla http://people.cs.uu.nl/stefan/downloads/brink10dependently.pdf | 26/03 13:47 |

guerrilla | yeah, i read most of that.. what part? | 26/03 13:47 |

fax | all of it | 26/03 13:48 |

andgra | what I meant was how a function takes element from it's domain and produces an element in it's 'image' and thus how a subdomain will produces a subimage... | 26/03 13:48 |

guerrilla | from what i saw, his code works directly | 26/03 13:48 |

guerrilla | fax: why should i look at it? | 26/03 13:48 |

guerrilla | hehe | 26/03 13:48 |

guerrilla | have we talked before? | 26/03 13:48 |

fax | andgra; f : A -> B ? | 26/03 13:48 |

fax | andgra oh you mean like a nonsurjective function | 26/03 13:49 |

fax | the set f(A) <= B | 26/03 13:49 |

guerrilla | fax: (i am doing formal grammar stuff, but i'll be using setoids instead of doing it his way.. which by the way, i thought was for the most part fairly elegant :) | 26/03 13:49 |

fax | guerrilla I think agda will get quotients soon! | 26/03 13:50 |

andgra | yeah | 26/03 13:50 |

fax | andgra, so in type theory we can define this 'inverse image' in a very different way than set theory | 26/03 13:51 |

guerrilla | fax: sorry, what do you mean by quotient? | 26/03 13:51 |

fax | wait it's not inverse image :/ | 26/03 13:52 |

fax | it's just the normal image | 26/03 13:52 |

fax | data Image {A B} (f : A -> B) : Set where witness : forall (a : A), f a -> Image f | 26/03 13:52 |

andgra | yes, at the time all I'm trying to prove that a subset of a functions domain will only produce a subimage.. | 26/03 13:52 |

fax | andgra yeah but it's not set theory | 26/03 13:52 |

fax | no clue why they call it Set actualyl, but it's a type | 26/03 13:53 |

andgra | I'm not completley sure I understand? | 26/03 13:53 |

andgra | also... {A B C : <Set>} doesn't typecheck... | 26/03 13:55 |

guerrilla | in what context? | 26/03 13:56 |

andgra | http://pastebin.com/raw.php?i=iF9FSJbG | 26/03 13:58 |

Jaak | even "{A : <Set>} -> \top" doesnt typecheck, infact | 26/03 14:00 |

guerrilla | Jaak: that's interesting... | 26/03 14:00 |

guerrilla | i think andgra's code doesn't because he's saying A and B are members of the type <Set> then saying he has some function from some member to another.. which doesn't make a lot of sense | 26/03 14:01 |

guerrilla | that would be like f : zero -> zero for Nat afaik | 26/03 14:02 |

guerrilla | {A B : Nat} -> (f : A -> B) ... wouldn't work because A and B would have to be either zero or succ | 26/03 14:02 |

guerrilla | same principle applies here | 26/03 14:02 |

guerrilla | maybe someone can explain that more elegantly though :) | 26/03 14:02 |

guerrilla | im not sure what's with Jaak's though.. i would think that would work | 26/03 14:03 |

andgra | so something like '\all {a b} {A C : <Set> a} {B : Set b}' or am I missing the point completely? | 26/03 14:03 |

guerrilla | or maybe Jaak it's just because you left out a use of A so there's nothing to infer the implicit argument from | 26/03 14:03 |

guerrilla | well you cant do Set b | 26/03 14:04 |

Jaak | i see | 26/03 14:04 |

andgra | oh, I mean '<Set> b' ofc... | 26/03 14:05 |

Jaak | yup, giving argument helps | 26/03 14:05 |

guerrilla | well, mtg time. bbiab | 26/03 14:24 |

guerrilla | good luck | 26/03 14:24 |

fax | pigworker why does she take all my CPU :((( | 26/03 17:09 |

* fax needs a way to compile Pig without it sounding like the harddisk is malfunctioning | 26/03 17:14 | |

pigworker | fax: I think one of my students was wondering the same thing. It's something stupid and fixable. I forget what. | 26/03 17:21 |

fax | I wanna wirte my category theory notes in epigram ;D | 26/03 17:24 |

fax | if coq had quotients it would be so easy (probably not just don't know the problems that would come up yet) | 26/03 17:25 |

pigworker | I just found a she patch Pierre-Evariste sent me. I think I've applied it and pushed to the main she repo. | 26/03 17:33 |

fax | ah that's it! thanks | 26/03 17:38 |

--- Day changed Sat Mar 27 2010 | ||

Igloo | Hi all | 27/03 01:24 |

lpjhjdh | so I'm trying to make an extremely simple assertion of equality about the following function but am not sure how | 27/03 03:22 |

lpjhjdh | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24412#a24412 | 27/03 03:22 |

lpjhjdh | can I somehow tell agda to just do one level of expansion and then apply refl? | 27/03 03:23 |

lpjhjdh | just "refl" doesn't work | 27/03 03:23 |

lpjhjdh | as imported from Relation.Binary.Core | 27/03 03:24 |

pigworker | lpjhjdh: looks to me like m =N m won't compute to true, because m is a variable, so you'll have to reason about the result of that test to prove your equation | 27/03 14:43 |

lpjhjdh | hmm, that thought occured to me so I changed it to the equality test from Data.Nat but it still doesn't seem to reduce | 27/03 15:43 |

lpjhjdh | so I've been trying to show a simple equality and I'm not sure how to get agda to expand it | 27/03 19:44 |

lpjhjdh | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a24450 | 27/03 19:44 |

lpjhjdh | the refl simply says "f0 m m m = f0 m m m" | 27/03 19:44 |

fax | 'with' is evil | 27/03 19:44 |

lpjhjdh | ah, why's that? | 27/03 19:50 |

lpjhjdh | should I expand it to helper functions myself then? | 27/03 19:52 |

fax | i don't know | 27/03 20:04 |

fax | what I would do is define a data type that was indexed by 3 N's, with constructors for each case | 27/03 20:04 |

fax | like | 27/03 20:05 |

lpjhjdh | I'll give it a shot, thanks, it actually hadn't crossed my mind to try something like that | 27/03 20:05 |

fax | case1 : Rec i j (suc k) | 27/03 20:05 |

fax | m not quite that | 27/03 20:05 |

fax | case2 : Rec (suc k) (suc k) (suc k) | 27/03 20:05 |

fax | sorry.. | 27/03 20:05 |

fax | case1 : Rec (suc k) (suc k) (suc k) | 27/03 20:05 |

fax | case2a : Rec (suc k) j (suc k) | 27/03 20:05 |

fax | case2b : Rec i (suc k) (suc k) | 27/03 20:05 |

fax | and so on | 27/03 20:05 |

lpjhjdh | ah, another clever idea, thanks | 27/03 20:05 |

fax | so then you can 'prove' a general theorem, that forall i j k, Rec i j k | 27/03 20:06 |

fax | that should let you do the e | 27/03 20:06 |

fax | that should let you do the 'eq' proof, but it's probably awkward enough that it wont let you do much else | 27/03 20:06 |

fax | maybe it'll work out tohugh | 27/03 20:06 |

fax | (oh Rec might be a recursive type too, where f_0 is recursive) | 27/03 20:07 |

lpjhjdh | yeah, I'm actually trying to give a more general proof that f0 and this other function T are equal | 27/03 20:08 |

fax | can I see T? | 27/03 20:10 |

fax | this is kind of interesting I thought f_0 was just a made up function | 27/03 20:10 |

lpjhjdh | yeah, it's actually the schedule for a parallel implementation of the algebraic path problem | 27/03 20:13 |

lpjhjdh | T is an optimized version | 27/03 20:13 |

fax | wow cool | 27/03 20:13 |

lpjhjdh | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a24451 | 27/03 20:14 |

lpjhjdh | and the proposition I'm trying to show is: T≡f₀ : (i j k : ℕ) → T i j k ≡ f₀ i j k | 27/03 20:15 |

lpjhjdh | which follows from induction on k | 27/03 20:15 |

lpjhjdh | f0 is actually an example of a very general class of schedules for affine recurrence equations | 27/03 20:20 |

lpjhjdh | but they obviously present unreasonable time complexity so more efficient schedules are needed, usually requiring human ingenuity to discover | 27/03 20:20 |

fax | I'd never heard of affine recurrence equations before | 27/03 20:21 |

fax | ill probably start seeing them everywhere now :D | 27/03 20:21 |

lpjhjdh | haha, that always seems to be how it is | 27/03 20:22 |

lpjhjdh | it's just a more impressive way of saying an affine equation that depends on itself | 27/03 20:22 |

--- Day changed Sun Mar 28 2010 | ||

Amadiro | Good evening. I'm just starting to get a hang on dependent typing, and I'm wondering, is agda mainly used for it's quality as theorem prover, or can/is it used to write actual programs, that are proven to be correct in this way? I guess this is somewhat a question about the implementation, but also about whether the language would be practical enough to solve practical programming problems with it. | 28/03 02:02 |

kmc | Amadiro, both. Agda is supposed to be better for actual programming than, say, Coq, but the practice of writing real programs in dependently typed languages is still in its infancy | 28/03 09:47 |

pigworker | good plan (A Bove, V Capretta) to define the domain of the function as an inductive relation, then use recursion on the domain to (a) define and (b) prove stuff about the function itself | 28/03 11:02 |

stevan | hi, i just noticed that Data.Container was recently added to the standard library. is there a single paper summing up all you need to know about containers (i.e. a good starting point) or does one have to work thru the whole series of papers? thanks. | 28/03 12:49 |

fax | stevan -- you know of Peter Morris' thesis? | 28/03 12:50 |

stevan | yes | 28/03 12:50 |

stevan | but i only glanced thru it. | 28/03 12:51 |

fax | it seems to be an implementation of the second half of that | 28/03 12:51 |

Amadiro | kmc, Ah, thanks a lot for the answer, very much appreciated. | 28/03 13:13 |

HairyDude | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24467 | 28/03 14:32 |

HairyDude | two lemmas, identical except for their contexts. I can case-split 'pr' to 'refl' in the first, but not the second | 28/03 14:35 |

HairyDude | (in the comments I meant "case-split" not "refine" btw) | 28/03 14:36 |

HairyDude | actually not lemmas, definitions, but you know what I mean | 28/03 14:38 |

stevan | try giving the typechecker more info; respects : forall {A B : Set} [...] | 28/03 14:44 |

pigworker | HairyDude: context is important; in the troubled case, C1 and C2 are not pattern vars and thus *fixed* so you can't learn that C2 is really C1; in the good case, C2 is a pattern var, and can become C1 when eq becomes refl. | 28/03 14:45 |

liyang | Is there any point in writing respects eq with eq; … | refl = ? rather than just respects refl = ? | 28/03 14:49 |

HairyDude | probably not | 28/03 14:50 |

HairyDude | in fact, that works, apart from ambiguous levels | 28/03 14:50 |

HairyDude | outside of the context that is | 28/03 14:51 |

pigworker | might be worth trying with C2 | eq ; ... |.C1 | refl for a laugh | 28/03 14:52 |

liyang | in fact, respects : (C1 ≡ C2) → Set; respects with eq | C2; respects refl | .C1 = ? works… | 28/03 14:55 |

liyang | Spot the deliberate mistake. | 28/03 14:58 |

HairyDude | compatible {A} {.A} refl _<_ _≤_ = _<_ ⇒ _≤_ | 28/03 15:03 |

HairyDude | much easier to work on relations than records... | 28/03 15:03 |

HairyDude | is there a more sensible way of parametrising a module over a total order and its strict version other than importing both along with a proof that they're compatible? | 28/03 15:10 |

HairyDude | for example, is there something in the libarary that just constructs an STO from a DTO (which after all comes with an equivalence relation)? | 28/03 15:12 |

* HairyDude wonders if he even needs the non-strict one | 28/03 15:13 | |

HairyDude | looks like I do, because the def of monotonicity is incorrect otherwise | 28/03 15:23 |

HairyDude | hrm. there's no equality defined on Fin | 28/03 15:31 |

liyang | There's an Ordering though. | 28/03 15:35 |

HairyDude | ah, it's in Data.Fin.Props | 28/03 15:38 |

HairyDude | if you say "using ()" does that mean "hide everything"? (it's followed by a "renaming" so it's not pointless) | 28/03 15:40 |

stevan | yes | 28/03 15:44 |

guerrilla | so, i'm trying to figure out how to use setoids here to get equality working (http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24470#a24470 and http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24471#a24471).. but i keep getting the followin error when trying to define that x in the second linke.... | 28/03 16:15 |

guerrilla | Setoid !=< _12 of type Set1 | 28/03 16:15 |

guerrilla | :\ | 28/03 16:15 |

guerrilla | when checking that the expression Nat₌ has type _12 | 28/03 16:15 |

guerrilla | any ideas on why? | 28/03 16:15 |

guerrilla | i'm basically trying to use setoids to emulate Haskell's Eq typeclass functionality... | 28/03 16:17 |

HairyDude | have you discovered _≟_ in Data.Nat yet? | 28/03 16:34 |

HairyDude | I find Agda's records are too cumbersome to emulate type classes tbh | 28/03 16:36 |

guerrilla | yeah.. hmm, i'll check out _≟_ | 28/03 16:44 |

HairyDude | who do I send library patches to? | 28/03 16:56 |

fax | hi byorgey | 28/03 18:15 |

byorgey | hi fax | 28/03 18:16 |

HairyDude | hrm. how to prove x ∉ [ y ] if x ≢ y | 28/03 20:15 |

fax | I suppose that is equivalent to proving x in [ y ] -> x = y | 28/03 20:19 |

fax | which is probably trivial from the definitions | 28/03 20:19 |

stevan | did you solve it HairyDude ? | 28/03 20:46 |

HairyDude | stevan: solve what? | 28/03 20:59 |

HairyDude | I have 11 holes in my source file atm :) | 28/03 20:59 |

stevan | your last question. :-) | 28/03 21:00 |

HairyDude | ah... no | 28/03 21:03 |

HairyDude | I can't even see how to prove x ∉ [] :/ | 28/03 21:04 |

fax | what's the definition | 28/03 21:04 |

fax | it's probably just pattern matching with no RHS (via ()) | 28/03 21:05 |

HairyDude | doh, of course | 28/03 21:06 |

HairyDude | thanks :) | 28/03 21:06 |

stevan | here's both ways: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24480#a24480 | 28/03 21:06 |

stevan | i'm bored. | 28/03 21:09 |

fax | stevan write a program that turns a number into the sum of (at most) three triangular numbers | 28/03 21:10 |

stevan | sounds like project euler... | 28/03 21:12 |

fax | no | 28/03 21:12 |

Igloo | Would it be correct to say that in agda one writes proof terms directly, unlike coq, where higher level tactics construct the proof terms? | 28/03 21:12 |

fax | Igloo - yes | 28/03 21:12 |

Igloo | Then what is the advantage of agda? It sounds like writin code in assembly rather than a HLL | 28/03 21:13 |

fax | Igloo - don't tend to think about it in terms of advantages/disadvantages but Agda has dependent pattern matching and eta conversion | 28/03 21:13 |

stevan | one can write semi-automatic tactics in agda in agda | 28/03 21:13 |

fax | stevan, both coq & agda have this poincare principle | 28/03 21:14 |

Igloo | Does agda's dependent pattern matching do the same thing as coq's "dependent destruction"/"dependent induction"? | 28/03 21:19 |

stevan | sure, but given that agda is a better programming language (given dep pattern matching etc) these type of tactics become clearer in agda? | 28/03 21:19 |

fax | Igloo, there's a couple aspects to it | 28/03 21:20 |

fax | the theoretical part is the axiom _+ computation_, you can add the axiom in coq but not the computation | 28/03 21:20 |

fax | and the practical part is having the actual pattern match stuff implemented -- you can pretty much do that in Ltac with coq, but with the possibility of computation getting blocked it's not worth it | 28/03 21:21 |

fax | stevan, I wouldn't say 'better programming language' | 28/03 21:21 |

stevan | wasn't there a dependent pattern matching extension to coq recently added? | 28/03 21:22 |

fax | most nontrivial coq developments have some approximations of dependent pattern matching in them | 28/03 21:23 |

fax | we're basically redoing the same stuff again and again :| | 28/03 21:24 |

fax | equations is really nice but coq still lacks the theory part I said above | 28/03 21:24 |

HairyDude | I really hate it when case-split gives you invalid clauses | 28/03 21:24 |

stevan | Igloo: http://www.reddit.com/r/dependent_types/comments/b0vb7/agda_vs_coq_by_wouter_swierstra_with_some_input/ | 28/03 21:28 |

Igloo | Thanks! | 28/03 21:29 |

fax | what I am mostly wondering is once we have eta, K and quotients.. will that be _enough_? | 28/03 21:30 |

kosmikus | enough for what? :) | 28/03 21:31 |

fax | presumably there will be some point where we can just do everything in a sensible way | 28/03 21:31 |

stevan | what's K? | 28/03 21:32 |

fax | stevan I mean axiom K, which lets you do (full) pattern matching, JM equality, proving identities identical or some other stuff like dependent pair elimination | 28/03 21:33 |

fax | I didn't phrase that last one correctly actually not sure how to put it other than formally | 28/03 21:34 |

fax | stevan, we can get all this stuff just by having proofs convertibly equal.. for some reason coq doesn't though :/ | 28/03 21:34 |

HairyDude | you mean dependent sums? | 28/03 21:36 |

fax | yeah | 28/03 21:36 |

stevan | what is it that ssreflect provides to its user? | 28/03 21:42 |

fax | stevan - I read a few papers on ssreflect and still have no clue -- what's great is what they're using it for tohugh | 28/03 21:47 |

fax | though* | 28/03 21:47 |

stevan | the manual is so long... :-/ | 28/03 21:50 |

* Igloo searches the dependent_types reddit for "isabelle" and gets nothing. Not encouraging. | 28/03 22:14 | |

fax | Igloo - I think it's because us lot are just into the new stuff :P | 28/03 22:15 |

fax | although coq is pretty old. | 28/03 22:15 |

fax | but I don't think it says anything bad about Isabelle | 28/03 22:15 |

Igloo | Oh, "dependent types" rather than "theorem proving". Maybe that's why | 28/03 22:16 |

stevan | i don't really like the reddit situation, there are too many subreddits... | 28/03 22:17 |

fax | stevan yeah I don't really get it | 28/03 22:18 |

stevan | and most of them are dead... | 28/03 22:18 |

Adamant | people create further subreddits because higher level subreddits start to suck | 28/03 22:32 |

Adamant | and in general, the suck rises as you go up the chain | 28/03 22:32 |

fax | it'd be nice to have all the stuff categorized somehow | 28/03 22:33 |

fax | rather than just in a random list | 28/03 22:33 |

stevan | but the reason types sucked was because noone used it, creating dependent_types and coq didn't really help in this regard imo. | 28/03 22:33 |

Adamant | it would, but who determines the categorization would be a battle in itself | 28/03 22:34 |

fax | I wish jbapple still blogged he wrote some cool stuff | 28/03 22:34 |

fax | Mathnerd314 -- you know we were talking about termination and the hydra thing? | 28/03 22:51 |

Mathnerd314 | sometime long ago, yes | 28/03 22:52 |

fax | it's called Goodstein sequence | 28/03 22:52 |

fax | didn't know that | 28/03 22:52 |

--- Day changed Mon Mar 29 2010 | ||

Amadiro | hmm.. I was going to ask a question, but by typing it out I figured it out... :) | 29/03 00:00 |

Amadiro | I should try that more often. | 29/03 00:01 |

HairyDude | bleh. case-split is causing stack overflows now. | 29/03 00:38 |

HairyDude | theorem proving uses a lot of memory :/ | 29/03 00:41 |

Saizan | well, agda in general uses a lot of memory, ime :) | 29/03 00:45 |

Saizan | i should remember to switch back to 32bit | 29/03 00:45 |

HairyDude | hey, are there any plans to parallelise agda? | 29/03 00:47 |

HairyDude | Saizan, ooh, that might be an issue, yes | 29/03 00:48 |

HairyDude | sheesh. just giving one goal takes forever now | 29/03 00:48 |

Saizan | sometimes splitting your code into different modules helps | 29/03 00:50 |

Saizan | so it doesn't retypecheck what you don't change | 29/03 00:50 |

HairyDude | mmm | 29/03 00:51 |

HairyDude | in fact, what I'm doing now is pretty much independent of the other stuff, so that would be a good idea | 29/03 00:51 |

HairyDude | "end of file during parsing" - weird | 29/03 00:51 |

Saizan | forgot the module header, maybe? | 29/03 00:52 |

HairyDude | this is the module I've been working on all day | 29/03 00:52 |

HairyDude | weird. new module, I'm getting "ambiguous name refl" even though it's only exported from one place | 29/03 00:57 |

HairyDude | s/exported/imported/ | 29/03 00:57 |

HairyDude | ah, no it isn't | 29/03 00:58 |

HairyDude | end of file error is caused by stack overflow, apparently | 29/03 01:03 |

HairyDude | Let's see if I can cheat. Has anyone written a partiton function for Vec? | 29/03 01:04 |

Amadiro | I'm idly wondering, will something like "succ n + m = succ (n + m)" (primitive recursion) actually get translated to a recursive function by the compiler? Sounds like it would be insanely slow. | 29/03 01:04 |

HairyDude | Amadiro: no. there are pragmas that let the compiler know that ℕ is natural numbers, so it can optimise | 29/03 01:06 |

Amadiro | HairyDude, Ah, I guessed something like that would be possible, thanks :) | 29/03 01:07 |

HairyDude | actually... yes, that definition will be, but the actual libraries use primitive functions. I think. | 29/03 01:07 |

HairyDude | I don't know much about the internals of Agda so I might be wrong on that. | 29/03 01:08 |

fax | Amadiro?? | 29/03 01:09 |

Amadiro | Another question, I'm currently reading "Dependent Types at Work", and it explains how to implement * in terms of +, + and pred in terms of succ, but it doesn't show how succ is implemented. Can I see a definition for that somewhere? | 29/03 01:09 |

fax | peano numbers are slow yes | 29/03 01:09 |

fax | Amadiro nobody is seriously going to use peano numbers for computing things........ | 29/03 01:09 |

HairyDude | Amadiro: succ is primitive | 29/03 01:09 |

Amadiro | fax, yeah, I was just wondering. | 29/03 01:09 |

fax | Amadiro the reason we have peano numbers is they are fundamental object in inductive proofs | 29/03 01:09 |

Amadiro | HairyDude, hm, ok, thanks. | 29/03 01:09 |

Amadiro | fax, yeah. | 29/03 01:10 |

HairyDude | Amadiro: the natural numbers are constructed from the constructors zero and suc | 29/03 01:10 |

fax | Amadiro -- you can implement binary numbers of whatever they are more efficent | 29/03 01:10 |

fax | Amadiro or you can axiomatize something like gmp integers and use them via haskell ffi | 29/03 01:10 |

Amadiro | Right, I'll need to get a hang on dependent typing first, but thanks a bunch for the info :D | 29/03 01:10 |

HairyDude | looks like I'll have to abandon my plan of using quicksort as an example dependently-typed program. Can anyone suggest something simpler but still interesting? | 29/03 01:11 |

fax | Amadiro, you can worry too much about 'efficency' in an attempt to be pragmatic | 29/03 01:12 |

fax | HairyDude -- example for what | 29/03 01:12 |

fax | ? | 29/03 01:12 |

Amadiro | fax, yeah, I'm not really worrying about efficiency, I was just wondering. | 29/03 01:12 |

fax | okay | 29/03 01:12 |

Amadiro | Trying to get an idea of what the compiler will do with the input, etc. | 29/03 01:12 |

HairyDude | fax: something that has lots of cumbersome proof terms (the first order part) that have no computational content and so can be stripped using realisability | 29/03 01:13 |

pigworker | HairyDude, treesort? | 29/03 01:13 |

fax | realisabiility? | 29/03 01:14 |

fax | does agda do that?? | 29/03 01:14 |

HairyDude | no, I'm just using agda to get the program right, and apply realisability by hand | 29/03 01:15 |

HairyDude | I suspect minlog does it, btw | 29/03 01:15 |

fax | oh cool | 29/03 01:15 |

fax | how do you apply this by hand | 29/03 01:15 |

HairyDude | just strip out the first order part, you end up with a Haskell-like program :) | 29/03 01:16 |

fax | okay | 29/03 01:16 |

HairyDude | well, it's more complex than that, but I can't be bothered to explain it right now. | 29/03 01:16 |

fax | uh ok | 29/03 01:16 |

fax | nice having you | 29/03 01:17 |

HairyDude | oh... latest mailing list post, apparently termination checking takes a long time. maybe I'll turn it off and see what happens | 29/03 01:18 |

HairyDude | nope, didn't work | 29/03 01:21 |

HairyDude | pigworker: I don't know treesort, and don't really have time to learn it | 29/03 01:21 |

HairyDude | merge sort maybe | 29/03 01:22 |

pigworker | HairyDude, what makes you think you don't know treesort, when you do know quicksort? | 29/03 01:22 |

HairyDude | pigworker: because I don't know the name? :) | 29/03 01:24 |

pigworker | Treesort is build-binary-search-tree, then flatten; which is effectively what quicksort does. | 29/03 01:24 |

HairyDude | ah, right | 29/03 01:25 |

HairyDude | oh, also I would like something that uses well-founded recursion, since the real code uses it and I want to show how the guard is thrown away and it becomes just fix | 29/03 01:26 |

pigworker | I don't know any good examples of well-founded recursion. | 29/03 01:27 |

fax | pigworker - I write your unification program into coq one breaktime that was fun -- it is kind of stunning how it works | 29/03 01:28 |

fax | oh and I think Saizan will have maybe done the proofs too, in Agda | 29/03 01:28 |

fax | but maybe I misremember | 29/03 01:28 |

fax | (talking of well founded recursion) | 29/03 01:31 |

fax | or lack of | 29/03 01:31 |

pigworker | fax, crikey that was last century; I remember waiting for the proofs to typecheck (in Lego); I did some painting; I watched it dry. | 29/03 01:33 |

fax | hehe | 29/03 01:33 |

pigworker | hairydude, you could try Dyckhoff-style proof search in implicational logic (a kind of mini-djinn); to prove an implication, introduce its hyp; to prove an atom, try backchaining on each hyp (and throw it away when proving its subgoals); that's a small program with a complex termination explanation | 29/03 01:41 |

HairyDude | this stuff? http://www.cs.st-andrews.ac.uk/~rd/publications/ | 29/03 01:50 |

pigworker | HairyDude: yeah, the stuff with Luis Pinto; the implicational fragment is tiny | 29/03 01:56 |

pigworker | night all | 29/03 02:05 |

Amadiro | fax, thanks again for telling me about peano numbers, I worked through the wikipedia article, and feel slightly more enlightened :) | 29/03 02:07 |

Amadiro | I actually never read about his axioms before. | 29/03 02:08 |

fax | it'sreally cool stuff ;) | 29/03 02:10 |

Amadiro | It is, and simple enough for me to grasp as well :) | 29/03 02:11 |

HairyDude | sigh. termination checker can't see that suc n < suc (suc n) | 29/03 02:26 |

HairyDude | or... no, that y :: xs < x :: y :: xs | 29/03 02:27 |

guerrilla | again.. what are these qoutients that people keep mentioning? | 29/03 13:13 |

fax | guerrilla do you know setoids | 29/03 13:13 |

guerrilla | i'd like to think i do. trying to work with them now actually | 29/03 13:14 |

guerrilla | they are related i take it? | 29/03 13:14 |

fax | instead of having a type and equivalence (S,~) and making sure every function f : S -> S' has the property that forall x y, x ~ y -> f x ~' f y | 29/03 13:15 |

fax | you could form the quotient type S/~ and then a function S/~ -> S'/~' must satisfy that 'morphism' relation | 29/03 13:15 |

fax | so there is an introduction rule for a quotient, S -> S/~ and I think there is also elimination which takes S/~ -> (S -> X) -> X with the property that X is identical if S is equal | 29/03 13:16 |

fax | this is a better explanation http://www.e-pig.org/epilogue/?p=319 | 29/03 13:21 |

guerrilla | i see | 29/03 13:27 |

guerrilla | ok | 29/03 13:27 |

guerrilla | thanks | 29/03 13:27 |

* guerrilla will look into that link | 29/03 13:27 | |

stevan | cool: http://code.haskell.org/Agda/test/succeed/TestQuote.agda | 29/03 17:56 |

fax | quoteGoal and quote are built in? | 29/03 17:58 |

stevan | seems so | 29/03 17:59 |

fax | that's cool that'll be really useful | 29/03 17:59 |

stevan | i wonder how tricky it would be to make the ringsolver fully automatic now, still need to parse the quoted goal string and build the expression inside agda i guess. never used the total parser combinators... | 29/03 18:07 |

fax | ohhhh | 29/03 18:08 |

fax | it gives TEXT instead of syntax that's weird | 29/03 18:08 |

fax | O_O | 29/03 18:08 |

fax | yeah that is a little bit less useful than i thought | 29/03 18:09 |

stevan | typed agda terms inside agda would be hard, no? | 29/03 18:15 |

fax | yes | 29/03 18:15 |

stevan | would untyped be enough for this purpose tho? | 29/03 18:17 |

fax | yes | 29/03 18:17 |

fax | a lot better than strings | 29/03 18:17 |

fax | the way I'd like to quote stuff is for agda to invert the interpretation function | 29/03 18:18 |

fax | this would be part of type inference, hopefull | 29/03 18:18 |

fax | hopefully | 29/03 18:18 |

stevan | this patch was just pushed, perhaps they will improve it soon | 29/03 18:18 |

uorygl | I think it's once again time to download Agda and prove the Fundamental Theorem of Algebra. | 29/03 21:13 |

fax | umm | 29/03 21:14 |

fax | you're kidding | 29/03 21:14 |

fax | do you know what the fundametal theorem of algebra IS? | 29/03 21:14 |

--- Day changed Tue Mar 30 2010 | ||

uorygl | Are Agda's Haddock docs available online somewhere? | 30/03 17:24 |

stevan | fax: seen todays patches? http://code.haskell.org/Agda/test/succeed/Reflection.agda :-) | 30/03 17:31 |

kosmikus | looks promising | 30/03 17:34 |

ukl | I recently skimmed a paper on using Coq for modal logic -- Has anybody tried something similar in Agda or does anyone know further resources on non-classical logic in Agda? | 30/03 18:18 |

--- Log closed Wed Mar 31 16:31:03 2010 | ||

--- Log opened Wed Mar 31 16:31:56 2010 | ||

-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal] | 31/03 16:31 | |

-!- Irssi: Join to #agda was synced in 73 secs | 31/03 16:33 |

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