stevan Berengal_ stevan --- Log opened Mon Mar 01 00:00:17 2010 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 Is it possible to use agda's unicode input in other modes? 01/03 21:22 i'd really like to use it combined with haskell-mode; if you get it working, please let me know :-) 01/03 21:24 I think agda's unicode input isn't its own 01/03 21:24 it has a name 01/03 21:24 * Berengal_ goes source diving 01/03 21:25 i miss proper modules, holes, unicode and mixfix when ever i code in haskell :-/ 01/03 22:05 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 wrt holes in haskell there's a little tool built over the ghc-api 01/03 22:13 it won't give you the context though 01/03 22:14 i recall reading about it; does it work well? do people use it? 01/03 22:14 it worked when i tried it, though i don't think it got much attention 01/03 22:15 does C-c C-c work? 01/03 22:15 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 Also: 01/03 22:15 (require 'agda-input) 01/03 22:15 (set-input-method "Agda") 01/03 22:15 it just gives you the type of the hole, nothing of the rest 01/03 22:15 Put that in your .emacs and you've got agda input everywhere 01/03 22:16 great, thanks. 01/03 22:16 mh, now you're forcing me to use erc 01/03 22:16 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 does using \Gl instead of \ work in haskell? i recall \r \=> \l1 etc all work? 01/03 22:22 \Gl doesn't work 01/03 22:27 :-/, i recall having seen a ticket about it, haskell' proposal perhaps? 01/03 22:30 there's one on ghc's trac 01/03 22:30 http://hackage.haskell.org/trac/ghc/ticket/1102 01/03 22:32 --- Day changed Tue Mar 02 2010 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 I haven't, I'll take a look, thanks 02/03 00:18 stevan: my Value type is indexed by a term, is that unnecessarily descriptive? 02/03 00:32 I was having trouble formulating a few things I wanted to, like the fact that (t \ v) always produces a value (I proved it later) 02/03 00:33 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 you mean you've Value : Term -> Set ? 02/03 00:40 yeah 02/03 00:41 in that case you could "data _⇓_ : Term → {t : Term} -> Value t → Set where" 02/03 00:41 ah, I guess that makes sense, I'll give it a shot, thanks again 02/03 00:42 what's the idea behind parametrizing the value on the term? 02/03 00:45 I was thinking I needed it to get nat values 02/03 00:46 but I guess I could just have nv-zero nv-suc 02/03 00:47 and get the same information 02/03 00:47 Just out of curiosity, who maintains Agda these days? 02/03 12:15 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 I'm not really up on how indexed functors/monads fit into formal category theory. 02/03 13:44 As for what applications it has... 02/03 13:46 Free algebras are (I think) essentially how you give semantics for datatypes, only they're typically called initial algebras. 02/03 13:47 And cofree coalgebras (terminal coalgebras). 02/03 13:47 it would be really nice to get a gentle intro to how those things work. 02/03 13:49 (Co)free (co)monads are similar. 02/03 13:50 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 I think that's an all right description, at least. I'm by no means an expert in this. 02/03 13:55 Obviously in Haskell monads are used to describe various types of computation. 02/03 13:55 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 Instead of represented directly, with a 'runFoo' that just unwraps a newtype. 02/03 13:56 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 I could point you to decent stuff on initial algebras and such. 02/03 13:58 Free monads and the like seems to be something some category theory books build toward. 02/03 13:59 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 the categorical/ algebraic concepts i'm sure i can find info about, but the connections/ applications in CS is harder? 02/03 14:01 In category theory, monads and algebras thereof are how (or, the more popular way) you do (and generalize) abstract algebra. 02/03 14:02 So, I suppose part of the connection is that programming and reasoning about programs involves algebraic structures. 02/03 14:03 And 'free' stuff is the purely syntactic. 02/03 14:04 hmm 02/03 14:10 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 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 not sure, could you give more context? 02/03 14:31 yeah, i thought i may have to resort to universes and that i couldn't pattern match on sets 02/03 14:33 well, for context, i just wanted a little syntactic sugar, like _* : Set -> Set would be basically (FiniteSet A)* = List A 02/03 14:34 but that's not syntactically valid :) 02/03 14:34 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 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 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 hmm, well i'll try playing a bit with universes/levels 02/03 14:44 actually, maybe i'll just make it work for this specific case for now and move on :) 02/03 14:45 :-) 02/03 14:49 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 huh, that was dumb 02/03 14:57 could have just done this all along: 02/03 14:57 _* : Set → Set 02/03 14:57 (A)* = List A 02/03 14:57 :P 02/03 14:57 :-) 02/03 14:58 You don't need the parentheses. 02/03 15:19 A * = List A 02/03 15:19 Saves 1 character! 02/03 15:20 dolio: w00t thanks ;) 02/03 15:45 cool, my hpaste from above now type-checks. we'll see if this will work out in the end though :) 02/03 16:49 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 setoid code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23178#a23178 02/03 19:20 finiteset code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23179#a23179 02/03 19:20 how would i extract the equiv predicate to actually use it? 02/03 19:21 is that even possible with this setup? 02/03 19:21 it seems like i would need the implicit argument of _∈?_ to be explicit in it's second pattern matching clause... 02/03 19:25 (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 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 ok thanks for the implicit vs. explicit part, i'll try that in a second 02/03 19:52 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 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 i may go back to that later though 02/03 19:53 stevan: great, that worked perfectly 02/03 19:57 _∈?_ {S} a (b ∈ B) = a == b where _==_ = eq-pred S 02/03 19:57 :) 02/03 19:57 thanks a lot 02/03 19:57 odd that you couldn't use the {S} in the infix form.. 02/03 20:00 pbly a practical reason for that, i'd imagine 02/03 20:00 (setoid are defined in Relation.Binary btw) 02/03 20:05 i know :) i'm trying something a little different - using predicates for relations.. 02/03 20:06 i find the Rel* code a bit difficult to follow as well 02/03 20:06 may re-do the whole thing with that as i get better with agda 02/03 20:07 normalizing the types: C-n might help 02/03 20:07 hmm.. not using emacs unfotunately 02/03 20:08 what would that do? 02/03 20:08 agda isn't really agda without emacs 02/03 20:09 hmm, didn't realize it would be such a different experience 02/03 20:09 i'm so used to vim.. hard to switch 02/03 20:09 it is like day and night, man :-) 02/03 20:09 use viper-mode 02/03 20:10 emulate vi keys inside emacs 02/03 20:10 ok, well, maybe i'll have to do a tutorial on emacs this weekend 02/03 20:10 (would prefer to use emacs as LISP >>> retarded VIM/ed language) 02/03 20:10 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 that's great 02/03 20:57 thanks a lot 02/03 20:57 (didn't get your 'use viper-mode' comment earlier, but i see now) 02/03 20:57 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 ok, cool 02/03 21:01 sounds like a plan 02/03 21:01 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 voluneering ? ;) 02/03 21:03 i came up with the idea, that's half of the work! :-) 02/03 21:05 some software which displays the keys pressed in a subtitle like fashion would be nice to have for the task 02/03 21:06 hmm, yeah, i haven't seen that before 02/03 21:06 ought to exist 02/03 21:07 --- Day changed Wed Mar 03 2010 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 ski: I think so 03/03 12:46 (i.e., do case analysis on dependent arguments in the constructors) 03/03 12:46 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 and the types of the stdlib for Nat is ℕ with zero and suc as constructors 03/03 12:47 hm, i might be able to do something like that 03/03 12:49 (i thought i had to have the eliminator "around" the return type, but maybe i don't actually) 03/03 12:49 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 so i was trying to eliminate the equality proof in the constructor type .. 03/03 12:51 is this related to John Major equality? 03/03 12:53 yes .. i'm trying out variants of it 03/03 12:53 aka Relation.Binary.HeterogeneousEquality 03/03 12:53 hrm. seems importing Level causes unsolved constraints 03/03 13:19 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23205#a23205 03/03 13:22 also, hiding zero and suc makes the yellow go away 03/03 13:24 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 That's odd. 03/03 13:36 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 copumpkin: hawt 04/03 06:21 Wow, are many people here going to the implementor's meeting this month? 04/03 15:03 It sounds like fun 04/03 15:03 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 What about it? 04/03 19:01 Upon reading the symmetry proof, I wasn't sure anymore if I even got the definition of _≡_, type-wise 04/03 19:02 How to understand that a proof is of type Set1, and what does (\z -> P z -> P x) mean? 04/03 19:03 Maybe the latter is the better question 04/03 19:03 Set1 is the level above Set. 04/03 19:03 That's (more or less) clear to me. 04/03 19:03 Set-1 04/03 19:03 It's necessary because that definition of == quantifies over Set, essentially, because P : A -> Set. 04/03 19:04 (that's values) 04/03 19:04 It's what non-logicians call Class. 04/03 19:04 (\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 So (P z -> P x) : Set ? 04/03 19:05 Yes. 04/03 19:05 Since P : A -> Set 04/03 19:06 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 Which is what you need to reverse the equality. 04/03 19:07 y == x = (P : A -> Set) -> P y -> P x 04/03 19:07 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 I'm getting closer, let me ponder a little 04/03 19:08 is there a name for replacing "structures" with properties of those structures? 04/03 19:11 this seems similar to representing a list by a fold 04/03 19:11 here you're representing equality by subst 04/03 19:11 So xy (\z -> P z -> P x) : (P x -> P x) -> (P y -> P x). 04/03 19:16 Ok so it works out. I'm wondering why I find this to be so hard 04/03 19:18 it's not trivial :) 04/03 19:18 dolio, when you said "Yes. Since P : A -> Set" is that just a general typing rule? 04/03 19:20 Yes. The type of (x : A) -> B[x] is computed as... 04/03 19:21 I mean, that (A -> A) : Set if A : Set 04/03 19:21 If A : SetM, and B[x] : SetN, then (x : A) -> B[x] : Set(max M N) 04/03 19:22 And A -> B is a special case, where B doesn't depend on x. 04/03 19:22 Is B[x] meta-notation for a type that mentions x? 04/03 19:22 Or is it Agda syntax? 04/03 19:23 Meta-notation. 04/03 19:23 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 Ok, so your notation explicitly conveys that this is allowed to be a dependently typed function 04/03 19:25 That was my intention. 04/03 19:25 B is some expression, in which x is in scope, that must have a type SetN for some N. 04/03 19:25 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 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 even more detail in http://en.wikipedia.org/wiki/Leibniz%27s_law 04/03 20:47 guerrilla, heh, yeah notions of equality are interesting on their own 04/03 20:47 especially in TT 04/03 20:48 TT? 04/03 20:48 type theory 04/03 20:48 of course :) 04/03 20:48 guerrilla, technically, yes. 04/03 21:06 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 I would have expected A -> A -> Bool or somesuch. 04/03 21:11 Set is a type-level Bool :) 04/03 21:12 maltem: if it were A -> A -> Bool, the relation would have to be decidable 04/03 21:12 the empty set is false 04/03 21:12 the set with one item is true (as are any other sets, but one item carries no other information) 04/03 21:12 why don't we use a specific type that can only be inhabited by \top (or True if you like)? 04/03 21:13 (say.. Prop) 04/03 21:13 seems like that would be clearer. but i assume that has other issues.. right? 04/03 21:13 guerrilla: we do? 04/03 21:13 ccasin, why needn't it be decidable with this Set encoding? 04/03 21:14 Data.Unit and Data.Empty contain our true and our false 04/03 21:14 I presume there's a way to check if a set is empty? 04/03 21:15 not really, nope 04/03 21:15 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 "The relation associates" rather 04/03 21:15 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 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 not decidable 04/03 21:16 maltem: that's why Bool would show it's decidable 04/03 21:16 Ah, I "forgot" that Set is not in any way a computable model of sets 04/03 21:16 if you can provide a true/false, that's a proof 04/03 21:17 That makes sense now. 04/03 21:17 I meant it's a proof of Bool, which carries more information than a proof of \top 04/03 21:18 But now I must ask myself guerrilla's question, too. 04/03 21:19 so a universe of true/false types? 04/03 21:19 * copumpkin tries to think how that would work 04/03 21:19 Prop in Coq is like that, sort of. 04/03 21:20 dolio: yeah i thought so... 04/03 21:20 Or any theory with proof irrelevance. 04/03 21:21 just like Prop : Set1 and then \top : Prop (and allow nothing else in it).. 04/03 21:21 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 I think agda used to even have a Prop 04/03 21:21 maybe agda 1? 04/03 21:21 copumpkin: yeah, i did see that in old code, i think 04/03 21:22 so.. why is it gone? 04/03 21:22 :) 04/03 21:22 Agda 2 has Prop, too, but it isn't proof irrelevant. It's just like an extra Set. 04/03 21:22 ah 04/03 21:22 ok 04/03 21:22 hmmf 04/03 21:22 :) 04/03 21:22 Let's see, if I define Rel : Set -> ?; Rel A = A -> A -> Prop   then what would ? be? 04/03 21:22 Set1? 04/03 21:23 Rel A = A -> Set 04/03 21:23 oh 04/03 21:23 sorry :) 04/03 21:23 I mean, due to the "-> Prop" I suppose I would have to learn another typing rule 04/03 21:24 maltem: not really necc. since we have universes 04/03 21:26 i think 04/03 21:26 ah I missed that Prop : Set1 04/03 21:27 yeah 04/03 21:27 so indeed ? = Set1 04/03 21:27 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 Set : Set1 04/03 21:28 and btw Set = Set0 04/03 21:28 Set1 : Set2 04/03 21:28 and so on 04/03 21:28 so that we don't have the paradox of having a set that contains all sets (Russel) 04/03 21:29 (among other issues?) 04/03 21:29 Ah a very valuable tip, I wasn't even aware that there's a seperate lib 04/03 21:31 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 Ah ok, so the notations gets a little heavier 04/03 21:33 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 maltem: yeah, just more stuff to keep track of 04/03 21:33 Wow how do you people read the unicodified sources? Do you keep adjusting your terminal font size? ;) 04/03 21:33 monospace? 04/03 21:39 gnome-terminal and monospace for me anyway 04/03 21:39 yeah for me that means that either fancy symbols are too small, or ordinary letters are too large 04/03 21:41 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 is there a difference between symbol \forall and the keyword "forall" in Agda? 05/03 13:54 guerrilla: AFAIK no 05/03 13:55 hmm ok 05/03 13:55 \forall used to not be a keyword. 05/03 14:53 Same with \lambda. 05/03 14:53 Has there been any news about the AIM meeting in Japan? 05/03 15:06 epigra mtime 05/03 21:10 epigram time 05/03 21:10 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 on http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes it says at the bottom: 05/03 22:35 codata ∞ (T : Set) : Set where 05/03 22:35 ♯_ : T → ∞ T 05/03 22:35 but this isn't even a recursively defined type. 05/03 22:35 ∞ appears to me to be just the identity type constructor 05/03 22:35 this can't be right 05/03 22:35 What were you trying to do? 05/03 22:36 understand that wiki page 05/03 22:36 You define your coinductive data types as normal data types with the co-inductive fields using ∞ 05/03 22:37 so that you can have data-types that are inductive in some components and co-inductive in others.. 05/03 22:37 I don't understand it all that well, myself, but I think I get the idea 05/03 22:37 inf : Coℕ 05/03 22:38 inf = suc (♯ inf) 05/03 22:38 what makes this well defined? 05/03 22:38 You can't case on the ♯, for one 05/03 22:38 so you can't do structural recursion on that 05/03 22:38 oh 05/03 22:38 this is so bizarre (coming from the coq world) 05/03 22:39 ♭ : ∀ {T} → ∞ T → T 05/03 22:39 ♭ (♯ x) = x 05/03 22:39 that looks like case analysis to me 05/03 22:39 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 whoa 05/03 22:42 what the heck is ~ ? 05/03 22:42 It doesn't exist anymore. 05/03 22:42 633 says "This type comes with a destructor, which is the only function which is 05/03 22:42 allowed to pattern match on ♯_:" 05/03 22:42 It used to denote corecursive definitions. 05/03 22:42 ok 05/03 22:43 Now 'inf = suc (# inf)' is internally translated to something similar to an auxiliary corecursive definition, or something like that. 05/03 22:43 but I'm left wondering why inf is well defined 05/03 22:43 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 Because it involves a fixed point involving codata, I guess. 05/03 22:45 I guess 05/03 22:45 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 ya 05/03 22:46 codata 'infects' data in an unusual way. 05/03 22:46 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 so I guess codata means something ... strange 05/03 22:47 Which leads to NAD's stuff about (co)data being unable to represent mu-nu fixed points. 05/03 22:48 but nu-mu is okay? 05/03 22:48 If you try to represent a mu-nu, it will end up as a nu-mu instead. 05/03 22:49 wow 05/03 22:50 what a mess 05/03 22:50 but that's okay 05/03 22:50 this is an open problem :D 05/03 22:50 At least we don't lose subject reduction. :) 05/03 22:50 ya 05/03 22:50 I'm no fan of coq's "solution" 05/03 22:50 roconnor, ok, you can case on sharp, but it doesn't count as structural recursion to the termination checker 05/03 22:50 I'm pretty sure that's just avoided by flatly disallowing dependent case analysis on coinductives. 05/03 22:51 dolio: what is avoided? 05/03 22:51 Loss of subject reduction. 05/03 22:51 sure 05/03 22:51 but why then go on with this strange # ∞ stuff? 05/03 22:52 Coinductive types are then defined using /data/, but with ∞ annotating 05/03 22:52 coinductive arguments (this was suggested by Thorsten Altenkirch): 05/03 22:52 It allows for mixing coinduction and induction in a single data definition. 05/03 22:52 ugh 05/03 22:52 Throsten, what did you say? 05/03 22:53 Which is actually being used currently. 05/03 22:53 dolio: it doesn't allow for mixing with my understanding of the definition of ∞. 05/03 22:53 For NAD's parser combinators, for instance. 05/03 22:53 when I see ∞, I just see the identity functor. 05/03 22:53 Well, it isn't. 05/03 22:53 how do I properly read this definition? 05/03 22:54 it is a "delayed" constructor? 05/03 22:54 Thorsten is there ?? 05/03 22:54 Yes, it's like that. 05/03 22:54 that's why inf is allowed 05/03 22:56 'data T : ... where con : ... -> ∞ T ... -> ...' allows you to use 'con' in a corecursive definition. 05/03 22:56 Basically, I think any definition guarded by codata constructors is allowed to be corecursive. 05/03 22:57 By the productivity checker. 05/03 22:57 what are the denotational semantics of Agda's codata? 05/03 22:57 it boggles my mind how to define this delay thing 05/03 22:57 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 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 I think that's right. 05/03 22:59 If you try to represent a mu-nu, it will end up as a nu-mu instead. 05/03 23:00 Right, Coℕ is defined like it is mu-nu but it really is nu-mu 05/03 23:00 nu on the nat, and mu on the identy functor ∞ 05/03 23:01 wow 05/03 23:01 this feels really wrong. 05/03 23:01 "The corresponding domain-theoretic expressions are μO. μZ. Z_⊥ + O and μZ. μO. Z_⊥ + O, and these are equivalent." 05/03 23:02 I'd like to see those semantics worked out 05/03 23:02 When discussing trying to do μO.νZ.Z + O using agda's codata. 05/03 23:02 what about simple νZ.Z+1 ? 05/03 23:04 so you are saying Nat is defined as μZ. Z_⊥ + 1 ? 05/03 23:04 er 05/03 23:04 CoNAt 05/03 23:04 Yes. 05/03 23:05 what is + in domain theory 05/03 23:06 He's saying that adding ∞ is the same as adding _⊥. 05/03 23:06 the domains A and B with a new bottom glued on, or with the two bottoms merged? 05/03 23:06 I don't really know. 05/03 23:07 where is your quote from? 05/03 23:09 'Some observations about μν' on the mailing list. 05/03 23:10 link? 05/03 23:10 Is the list archive still not public? It's asking me to log in. 05/03 23:11 found it 05/03 23:12 http://thread.gmane.org/gmane.comp.lang.agda/952 05/03 23:12 It's from last July. 05/03 23:12 I have to jet, but I'll leave with a query... 05/03 23:14 what query? 05/03 23:15 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 Is there a similar example for parametric, universal types vs. pi types? 05/03 23:16 existential means non-dependent elimination? 05/03 23:16 Yes. I think weak elimination is the key to the abstraction property. 05/03 23:17 I suppose there's no 'strong' pi eliminator. 05/03 23:17 BTW you lose all the information hiding guarentees of existential types if your language also has sigma types 05/03 23:17 basically you can tuck in info way in a sigma type and return it. 05/03 23:17 Right. Luo mentions that, I think. 05/03 23:18 --- Day changed Sat Mar 06 2010 in agda you can make recursion step only by single argument? 06/03 11:09 no, if i understand correctly 06/03 11:10 in the sense that you don't need to recurse on a single argument at a time 06/03 11:10 i have some nat theory here 06/03 11:13 and i want to specify associativity of + here 06/03 11:14 hm, nvm 06/03 11:14 it looks like complete abuse of types 06/03 11:16 you'd have associativity as a separate property 06/03 11:20 \all x y z -> (x + y) + z \== x + (y + z) 06/03 11:20 it's fairly simple to prove by induction over x, iirc 06/03 11:21 hm, i need induction over other variables too? 06/03 11:22 since i do not have yet 0+y = y? 06/03 11:22 ah, well, i'd prove that as a lemma 06/03 11:22 however you could recurse over y too, if that was needed 06/03 11:23 yeah, i currently recurse over all of them 06/03 11:23 i'm now working on commutativity 06/03 11:24 why would this give the error: http://pastebin.com/acTffsTi 06/03 11:39 well because the types don't match.. 06/03 12:32 comm+ y y' : y + y' = y' + y 06/03 12:33 but you've to provide something of type s y + y' ≡ y' + s y 06/03 12:33 hm, i have nothing of that type 06/03 12:38 or do i have to provide something that chops s off from both sides? 06/03 12:39 well, from  y + y' = y' + y you can derive s (y + y') = s (y' + y) easily 06/03 12:40 then you've to prove that s (y' + y) = y' + s y 06/03 12:40 hm 06/03 12:44 i have no idea how to do that 06/03 12:45 or how to express it in agda 06/03 12:45 well, you can just have an helper function \all x y -> s (x + y) \== x + s y 06/03 12:46 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 that's usually called cong 06/03 12:48 well, i have something called cong here, i'm writing def to it at the moment 06/03 12:49 i RLa! 06/03 12:57 hi 06/03 12:57 hey 06/03 12:57 no, it's not going to work 06/03 13:04 i'm even unable to write definition for \all x y -> s (x + y) \== x + s y 06/03 13:07 you must prove x + 0 = 0 + x by induction on x 06/03 13:11 doing this sort of stuff in agda is very long and difficult 06/03 13:11 yes, i already know that 06/03 13:12 anyway, i think i got helper function: http://pastebin.com/7MuVGvpz 06/03 13:13 but i see no way how it would help me 06/03 13:14 are you trying to prove x + y = y + x? 06/03 13:15 on natural numbers 06/03 13:15 yes 06/03 13:21 i have problem with case comm+ (s y) (s y') 06/03 13:24 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 (*if A reduces to B then a proof of A is a proof of B) 06/03 13:27 you've redundant cases in your commHelp btw 06/03 13:27 hm 06/03 13:29 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 (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 i do not get which cases are reduntant in my commHelp 06/03 13:34 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 S x + y = y + S x 06/03 13:36 reduces to 06/03 13:36 S (x + y) = y + S x 06/03 13:36 because of the definition of + 06/03 13:36 hm, i see 06/03 13:36 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 another example of this is, 1 + 1 reduces to 2 .. obviously! 06/03 13:37 so you can prove 1 + 1 = 2 by proving 2 = 2 06/03 13:37 so it's just reflexivity 06/03 13:37 that might seem like a boring example, but you can take this technique and turn it into something really powerful 06/03 13:37 can i use numbers instead of (s y) stuff? 06/03 13:38 well you could write  1+  instead of  S 06/03 13:38 it's all the same though 06/03 13:38 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 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 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 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 i'm missing something important here 06/03 13:48 well, you have to recurse 06/03 13:48 do you have transitivity? 06/03 13:49 comm+ : forall x y, x + y = y + x ? I assume 06/03 13:49 yes 06/03 13:49 then  comm+ (s y) y' : (s x) + y' = y' + (s x) 06/03 13:49 and   comm+ (s y) y' : s (x + y') = y' + (s x) 06/03 13:49 Saizan, no, transitivity went wrong and i do not have code for that 06/03 13:49 the induction hypothesis gives you x + y' = y' + x thought, 06/03 13:49 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 induction gives you x + y' = y' + x 06/03 13:51 RLa: transitivity should just be a matter of pattern matching on the arguments and using triv 06/03 13:52 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 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 oops 06/03 13:54 trans : {A : Set} {x y z : A} -> x \== y -> y \== z -> x \== z 06/03 13:54 Saizan, \== meaning not equal? 06/03 13:55 oh.... 06/03 13:55 this is quail notation for the unicode equals sign 06/03 13:55 im usedto \== for not equal form porolog 06/03 13:55 yeah, i'm not sure why i use the latex notation here on irc :) 06/03 13:55 s/latex/what the agda-mode accepts/ 06/03 13:56 then  comm+ (s y) y' : (s x) + y' = y' + (s x) <- is that actual syntax? 06/03 13:58 shouldn't i use helper function here somehow? 06/03 13:59 also, what is difference between function signatures trans : {A : Set} (x y z : A ) -> ... and \forall x y z -> ...? 06/03 14:02 comm+ (s y) y' = trans (cong s (comm+ y y')) (commHelp y' y) -- should be 06/03 14:02 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 unless your \== is defined only on naturals 06/03 14:03 i have all functions using \forall 06/03 14:04 yes, it's only on nat 06/03 14:04 how is it defined? 06/03 14:04 however, \forall a b c -> .. is the same as (a b c : _) -> ... 06/03 14:05 i.e. you're asking the typechecker to infer the type 06/03 14:05 http://pastebin.com/zDdGS56g 06/03 14:05 hm, i did not know that 06/03 14:05 ooh 06/03 14:05 those definitions look ok? 06/03 14:06 well, that \== is not what i expected 06/03 14:06 hm, i see, i already looked at many agda examples and they all do things differently 06/03 14:07 now i see why your commHelp definition works 06/03 14:07 (i was puzzled before :) 06/03 14:07 i guess you've to define transitivity by pattern matching on the x y z then 06/03 14:08 yes, that's where trouble came in 06/03 14:08 it seems to want some extra data 06/03 14:08 well, trans would have 5 arguments 06/03 14:09 but where those extra 2 come from? 06/03 14:09 or what gives value for them 06/03 14:10 "x \== y" and "y \== z" count as arguments 06/03 14:10 but what evaluates them? 06/03 14:12 or should i completely ignore them? 06/03 14:12 and use results of pattern matching? 06/03 14:12 ah, btw, \forall a b c -> ... is actually (a : _) (b : _) (c : _) -> .., i.e. they can be of different types 06/03 14:12 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 when the equality reduces to False instead you should use an absurd pattern for them 06/03 14:14 so that you can avoid writing a body for that that branch 06/03 14:14 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 hm, it does not let me use those extra arguments in pattern matching at all 06/03 14:16 e.g requires me to return a function 06/03 14:17 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 that's odd. 06/03 14:17 can you paste? 06/03 14:17 oh, duh, we can't use z as a variable name. 06/03 14:19 ok, for example: trans≡ z z z = λ triv triv → triv 06/03 14:20 this seems fine case 06/03 14:20 yeah 06/03 14:22 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 http://pastebin.com/7XL3SC5X <- eg 06/03 14:23 Have there been any applications written in Agda? 06/03 14:24 duh, i tried to write triv as pattern 06/03 14:26 therefore it did not work 06/03 14:26 did you get +comm done yet? 06/03 14:27 no, i'm working on trans 06/03 14:28 () as a pattern means that such case should be never possible? 06/03 14:29 yeah 06/03 14:29 what's trans got to do with this? 06/03 14:32 here is this proof in coq http://pastie.org/857132 06/03 14:32 well, don't you need trans to chain the inductive hypothesis and s (y' + x) = y' + (s x) ? 06/03 14:33 it's how i'd write it, anyway 06/03 14:33 Saizan, it's actally S (S (y' + x)) = S (y' + (S x)) isn't it? So you have to rewrite 06/03 14:34 no you are right, transitivity works too 06/03 14:34 i'm defining cong now 06/03 14:41 trying to do same way as trans 06/03 14:41 cong is actually not needed here 06/03 14:42 since "s x \== s y" reduces to "x \== y" with your definition 06/03 14:43 "reduces to" <- how is reduction defined here? 06/03 14:44 well, as the normal evaluation rules, given the definition of \== 06/03 14:46 since you've defined "s m ≡ s n  = m ≡ n" 06/03 14:47 here is my cong: http://pastebin.com/5qB98ceF 06/03 14:57 i now go back to comm 06/03 14:58 nice :) 06/03 14:58 you won't need that cong here 06/03 14:58 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 i'm on ghc-6.12 06/03 15:19 I think I'll upgrade 06/03 15:21 i'm still working on commutativity 06/03 16:26 what does conc stand for? 06/03 16:26 conc? 06/03 16:28 cong* 06/03 16:34 not sure actually 06/03 16:35 i think that my definition of cong is not usable 06/03 16:36 you don't need it for commutativity, anyhow 06/03 16:36 http://pastebin.com/pXs2S2sS 06/03 16:36 hm, move-s is same as my commHelper 06/03 16:39 yeah 06/03 16:40 hm, if program compiles, it must be correct? 06/03 16:42 it compiles, but i still do not understand that trick with using trans 06/03 16:42 well, it's not like you can run comm+ to get something computationally interesting :) 06/03 16:42 ah, well 06/03 16:43 hehe :D 06/03 16:43 so primitive proofs in simple arithmetics should be not so complex 06/03 16:44 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 then you use move-s to tell that s (y + x) == y + s x 06/03 16:45 combining with transitivity you get s x + y = y + s x, which is what you wanted to prove 06/03 16:46 you can automate proof strategies by reflection, like in the RingSolver module 06/03 16:46 i will look into that 06/03 16:47 i think i have problem that i do not understand how agda prove procedure works 06/03 16:48 anyway, big thanks for help 06/03 16:50 np 06/03 16:51 the first thing is that equality over terms is basically defined by evaluation 06/03 16:52 "if program compiles, it must be correct?" -- no :P 06/03 16:53 you just know that it satisfies its type 06/03 16:53 but you can sometimes express correctness in the type, or prove it afterwards 06/03 16:53 is evaluation in agda like beta-reduction in lambda calculus? 06/03 16:54 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 yeah 06/03 16:54 are there normal forms etc. too? 06/03 16:56 yeah 06/03 16:56 the difference with a pure lambda calculus is the addition of constructors 06/03 16:57 it's beta-reduction + eta-exapansion + unfolding definitions (+ more stuff?) 06/03 17:00 oh yeah pattern matching 06/03 17:01 what about recursion? does it restrict construction of fixpoint combinators somehow? 06/03 17:02 yes, there's a termination checker 06/03 17:03 I hujst cannot figure out how to use pig from the test files : 06/03 17:06 pig? 06/03 17:07 --- Day changed Sun Mar 07 2010 so I have a datatype with only a single constructor and I can't seem to match on it 07/03 01:17 Paste? 07/03 01:22 Offer closing in 2 minutes. :p 07/03 01:23 ooh, sorry, must run 07/03 01:23 thanks though 07/03 01:23 Likewise. :3 07/03 01:23 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 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 some of us here use scala for writing wicket apps? 07/03 11:33 wrong channel 07/03 11:33 is there a part of agda manual that explains the use of () in pattern matching? 07/03 12:38 mh, maybe in some of the tutorials 07/03 12:42 otherwise you've to look at the papers :) 07/03 12:43 or ask here what's unclear 07/03 12:43 I find it fun how you can abuse the agda module system in order not to repeat variable names :) 07/03 16:33 maltem: still to much to repeat according my taste but... 07/03 16:34 *too 07/03 16:36 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 well, you can get open ... public to export a flat namespace if you want 07/03 16:41 what does "public" do? 07/03 16:45 it makes the current module re-export the symbols of the opened moduel 07/03 16:57 it's used a lot in the Algebra records, to give you a "subtyping" feel 07/03 16:58 mmh ok so I when then using the module I could drop the module qualifiers, and just have long types 07/03 16:59 right, which is probably not that nice 07/03 17:07 but you could also make a module that takes all the parameters at once and exports everything 07/03 17:08 right 07/03 17:09 There is no way to instanciate an element of type "data False : Set where" is there? 07/03 18:34 jotik^^: what do you mean by instanciate here? 07/03 18:35 but yes there is no value of type False 07/03 18:35 otherwise we have a problem 07/03 18:35 So I can't make any function return anything of type False, correct? 07/03 18:36 A problem? 07/03 18:36 nevermind last line. 07/03 18:36 jotik^^: you can return a value of type false if you get one as argument 07/03 18:36 or if you get some arguments that forms a contradiction and so have all types 07/03 18:37 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 jotik^^: Set is not just true or false 07/03 18:44 And I just don't know what to do with the case trans≡ (suc a) zero (suc c) 07/03 18:44 trans≡ _ _ _ refl refl = refl 07/03 18:44 hmm... 07/03 18:45 What is that supposed to mean (/me agda noob) 07/03 18:46 if you want to write it the long way as an exercise you will need the () pattern 07/03 18:46 equality is complicated beast 07/03 18:47 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 And I don't understand what you meant by trans≡ _ _ _ refl refl = refl 07/03 18:49 but basically pattern matching on refl forces the substitution of n for m and of o for n 07/03 18:50 but I can't pattern match like that, can I? 07/03 18:55 yes you can 07/03 19:02 jotik^^: however I've not seen the definiton of _≡_ you use 07/03 19:02 npouillard: Well here's what I've got: http://agda.pastebin.com/7s3d7qkL 07/03 19:04 jotik^^: ok so you have a different version of _≡_ than the propositional one 07/03 19:06 What would a propositional one look like? 07/03 19:07 like a type? 07/03 19:07 data _≡_ (A : Set) : Set → Set where refl : A ≡ A 07/03 19:07 yes 07/03 19:08 but you to continue in your direction you will need a function to eliminate False values 07/03 19:08 Wow I think I already managed with one, by declaring an absurd pattern and using () () 07/03 19:10 elim-False : ∀ {A} → False → A 07/03 19:11 elim-False () 07/03 19:11 hmm 07/03 19:12 jotik^^: Was the definition of _≡_ fixed in the assignment 07/03 19:14 If I declare such a function, I get "Sort _55  [ at filename..." What does that mean? 07/03 19:14 npouillard: yes 07/03 19:15 hum ∀ {A : Set} ... 07/03 19:15 thanks 07/03 19:22 btw, what do those _somenumber messages mean? 07/03 20:55 e.g. _59, _60, _61 etc 07/03 20:55 jotik^^: they are meta variables introduced by the typechecker for unknowns which couldn't be resolved to something else 07/03 22:07 jotik^^: a lot like prolog, if you're familiar with it 07/03 22:08 not much 07/03 22:08 bed time for me. Thanks everybody! Good night! 07/03 22:09 --- Day changed Mon Mar 08 2010 so they proved tt = ff in epigram?? 08/03 00:13 Is the Agda "standard library" include in an install from Hackage (via cabal-install)? 08/03 05:06 nope 08/03 06:47 not as far as I know 08/03 06:47 we need an agda platform :P 08/03 06:47 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 for Agda it always worked at the first attempt for me 08/03 07:44 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 Finally I had to beg gentoo devs for ebuilds which were a work-in-progress. 08/03 07:57 ah, i avoid distro packages like the plague, for haskell 08/03 08:05 Since haskell developers avoid them as well, distro packages are bad. 08/03 08:50 Haskell packagers are doing a lousy job, the latest stable ghc in gentoo is 6.8.2 08/03 08:51 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 so you call judgemental equality the one that appears in your typing rules? 08/03 20:09 Yes. Because it's used in typing judgments. 08/03 20:24 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 it'd make some proofs impossible? 08/03 20:27 I'm not really sure. 08/03 20:27 It makes more work, at least. 08/03 20:28 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 Or use a non-canonical empty vector. 08/03 20:29 I'm not sure if there's more to it than that. 08/03 20:30 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 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 i thought that was dispensed earlier by saying that epic(?) erases coercions 08/03 20:48 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 yeah 08/03 20:49 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 I guess. 08/03 21:00 --- Day changed Wed Mar 10 2010 is the RingSolver actually being constructive and finding "solutions" or is it just manipulating the equation to show equality? 10/03 07:52 it kind of looks like the latter but it may be more subtle 10/03 07:53 the Reflection module gives me both a prove and a solve based on it 10/03 07:55 but I can't figure out how the solve function is working 10/03 07:55 i think the variables are meant as universally quantified 10/03 08:13 so, this is pretty intense: http://arxiv.org/abs/1002.4433 10/03 12:30 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 copumpkin: reversing the steps of the manipulation starting from refl yields a constructive solution, if you will. 10/03 12:42 copumpkin: where by manipulation I mean transformation to some normal form. 10/03 12:43 liyang: thanks :) 10/03 20:26 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 hmm, trying to convince it to use a proof of mine during pattern matching :/ 11/03 08:28 I guess I'd really need a subst during pattern matching 11/03 08:29 which seems rather hard to convince it to do 11/03 08:29 yay, I just wrote deinterleave : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n 11/03 08:51 way harder than it should be 11/03 08:51 How does 2 * n compute? 2 * n ==> n + n? 11/03 08:57 n + (n + 0) 11/03 08:58 (sadly) 11/03 08:58 Well, there's your problem. 11/03 08:58 yep 11/03 08:58 that was kind of my point though 11/03 08:58 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 You're trying to do ring solver in GHC? 11/03 09:00 Good luck with that. 11/03 09:00 well, not as part of GHC, just as a separate mini language with its own parser, etc. 11/03 09:00 that emits haskell 11/03 09:00 Oh, okay. 11/03 09:00 That's slightly more sane. 11/03 09:01 :P 11/03 09:01 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 (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 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 Joe 6-monads. 11/03 09:07 lol 11/03 09:07 gotta love things like suc (n + (n + 0)) != n + suc (n + 0) of type ℕ 11/03 09:13 That's the price you pay for decidable typing. 11/03 09:15 yep 11/03 09:15 I wonder how much better stuff like NuPRL actually does at that. 11/03 09:16 Can it figure out that those two things are equal? 11/03 09:16 haven't tried it 11/03 09:16 can't seem to fetch it either 11/03 09:18 ahem: "Build proof assistants that are as indispensible to programmers and mathematicians as word processors are now." 11/03 09:20 Was that supposed to be serious? 11/03 09:21 looks like it: http://www.cs.cornell.edu/Info/Projects/NuPRL/Intro/intro.html 11/03 09:21 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 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 if I can get a few more people interested in agda I'll feel satisfied 11/03 09:35 I just wrote another deinterleave₂ : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n 11/03 09:35 implemented in a different (less efficient) manner 11/03 09:35 pretty exciting stuff 11/03 09:36 all using RingSolver? 11/03 09:37 yep 11/03 09:37 how does it look? 11/03 09:37 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23891#a23891 11/03 09:37 the ringsolver for the second one was pretty trivial 11/03 09:38 but as long as it can do it, I'm happy :) 11/03 09:38 nice 11/03 09:44 well, it could be nicer.. 11/03 09:44 yeah :P 11/03 09:44 my proofs are always butt-ugly 11/03 09:44 but those are the two "obvious" ways of writing deinterleave 11/03 09:45 that I could think of anyway 11/03 09:45 oh, i meant because of the obvious limitations of agda, no idea if you can write it better 11/03 09:46 I'd like my tool to support writing both of those with as little code noise as possible 11/03 09:46 pairs (x:y:zs) = (x,y) : pairs zs :P 11/03 09:46 like in mmorrow's original version 11/03 09:46 I was particularly frustrated with writing that function in agda 11/03 09:47 I could've probably used the solver to rewrite it immediately to a suc (suc ...) form 11/03 09:47 I'm pretty impressed with how general solve is 11/03 09:53 but the type in the source file is effectively useful 11/03 09:53 useless, even 11/03 09:53 n-ary functions seem to have that property.. 11/03 09:55 yeah 11/03 09:55 Isn't the obvious solution to cast to a Vec a (n * 2), and then deinterleave that? 11/03 09:57 let me try that :) 11/03 09:59 it typechecks but doesn't termination check 11/03 10:02 the most obvious thing, anyway 11/03 10:02 oh 11/03 10:02 I'm doing it wrong 11/03 10:02 there, it worked :) 11/03 10:02 http://snapplr.com/mf6q 11/03 10:03 obvious in retrospect :P 11/03 10:03 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 and obviously I'm still pretty close to him if I didn't think of that simple solution :) 11/03 10:06 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 oh, i thought you wanted to use 2 * n to intentionally complicate things 11/03 10:08 no, I'm just stupid :) 11/03 10:08 but yes, I'll claim it was for that reason too 11/03 10:08 rewrite is just a shorthand for the usual with dance 11/03 10:09 I see :) 11/03 10:09 Rewrite isn't quite as general as the usual with p … | refl = ? dance… 11/03 21:37 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 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 :) 12/03 03:49 seems pretty quiet compared to #haskell 12/03 03:49 yeah :P 12/03 03:49 * Mathnerd314 runs away to take his first shower in weeks 12/03 03:50 so, how do I write functions in agda? 12/03 04:05 same way as haskell :) 12/03 04:06 but you don't have type inference in most cases 12/03 04:06 open import Data.Nat; f : \bn \r \bn; f x = x + 1 12/03 04:07 tada 12/03 04:07 you'll need a module X where at the top 12/03 04:07 then do C-c C-l (as in liposuction) 12/03 04:07 and it should turn colorful 12/03 04:07 that \bn types a blackboard N for naturals by the way 12/03 04:10 \r is a pretty -> 12/03 04:10 but -> works too 12/03 04:10 do I need semicolons? 12/03 04:11 O 12/03 04:11 I'm getting a "missing body" error :-/ 12/03 04:11 nope, I just wanted to separate lines 12/03 04:12 is there an agda pastebin? 12/03 04:13 not really, we just use hpaste 12/03 04:13 maybe you should paste what you mean then. 12/03 04:14 agda needs better error messages ;-) 12/03 04:14 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23916#a23916 12/03 04:16 it seems to eat up all my CPU when I try to compile :-( 12/03 04:18 it's typechecking the standard library dependencies 12/03 04:18 from Data.Nat 12/03 04:18 it will be a lot quicker once it's done that 12/03 04:18 where does it store those typechecks? 12/03 04:19 in .agdai files of the same name 12/03 04:19 like .hi files in haskell 12/03 04:19 so if I delete .agdai files... my CPU burns up next compile? 12/03 04:20 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 then it'll have to recheck them 12/03 04:20 your own modules are unlikely to be as complex as the standard library's ones 12/03 04:21 so deleting your own .agdai files won't be too painful 12/03 04:21 * Mathnerd314 sees 12/03 04:21 seems you don't want to install agda as root, then. 12/03 04:22 anyway... I want Control.Monad and Data.List for my program, right? 12/03 04:24 well 12/03 04:24 you might want to define them yourself and talk about the monad actions on their own 12/03 04:25 agda doesn't have typeclasses :) 12/03 04:25 and you'd need a Data.Colist 12/03 04:25 it might not be a good place to start though 12/03 04:25 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 aw 12/03 04:28 http://snapplr.com/tacb 12/03 04:29 there is a Category.Monad and a Data.List 12/03 04:29 but Data.List is only finite lists 12/03 04:30 that IRC client looks cool 12/03 04:31 ok, Agda is definitely rebooting my system every 10 seconds or so 12/03 04:36 :-/ 12/03 04:36 wow 12/03 04:36 this is why I want to switch to linux or some other *sane* OS 12/03 04:37 it's probably not me, but that all-in-one installer 12/03 04:37 so, how do I install the standard library from inside Haskell? 12/03 04:38 you just need to put it in a directory and configure your agda to go looking for it there 12/03 04:39 I'd find it quite disconcerting that a userland program could consistently crash my entire OS 12/03 04:39 even if it's the all-in-one installer's "fault" 12/03 04:39 I use --include-dir? 12/03 04:42 *--include-path=DIR 12/03 04:42 you typically don't want to be calling agda from a command-line 12/03 04:42 but yes, I think so 12/03 04:42 why is it bad to call from a command line? 12/03 04:43 well, for most proofs, you'll want all the help you can get 12/03 04:43 from an interactive UI like emacs 12/03 04:43 you can put holes in your proofs and it can tell you want it needs there 12/03 04:43 and what you have in scope and so on 12/03 04:43 huh. 12/03 04:47 so why doesn't Data.List handle infinite lists? 12/03 04:48 it needs the equivalent of laziness in haskell to handle them 12/03 04:49 so something like a thunk. 12/03 04:50 yeah, sort of 12/03 04:50 that kind of thing is handled formally by talking about data vs. codata 12/03 04:50 data is inductively defined 12/03 04:50 and codata is coinductively defined :) 12/03 04:51 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 that makes even less sense... :-) 12/03 04:51 well 12/03 04:51 hmm 12/03 04:52 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 ok. 12/03 04:53 with codata, you just have "observers" on some value that exists 12/03 04:53 so you have properties of that value? 12/03 04:54 like "this value acts like 0 on this set" 12/03 04:54 sort of 12/03 04:54 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 specifically, it won't try to figure out whether your coinductive type is finite 12/03 04:56 whereas it needs a "base case" for an inductive type 12/03 04:56 but I have a base case - an empty list... right? 12/03 04:57 yes, and you have an observer that tells you whether you have it or not 12/03 04:57 ok then. 12/03 04:57 but agda won't try to ensure that there's one of those at some depth in the colist 12/03 04:58 in haskell, all "data" is actually codata 12/03 04:58 so why does agda have data? 12/03 04:58 but in agda you need to be more explicit about getting that kind of lazy behavior 12/03 04:58 because data is a lot cleaner to work with in general, and many times it's what you want 12/03 04:58 peano naturals as data are the naturals, but peano naturals as codata have an "infinity", for example 12/03 04:59 this isn't helping me with my proof. 12/03 04:59 I know :) 12/03 04:59 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 (but don't give up on agda, it's awesome!) 12/03 05:00 where would I start with a proof? 12/03 05:00 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 so pure : a -> Colist a 12/03 05:01 more specifically 12/03 05:01 pure : {a : Set} -> a -> Colist a 12/03 05:01 (agda doesn't really have polymorphism) 12/03 05:01 you could then define repeat fairly simply on your Colist 12/03 05:02 map too 12/03 05:02 then your proofs would be the laws... here, let me throw together a template for you 12/03 05:02 btw... what encoding are .agda files? 12/03 05:07 utf-8 usually 12/03 05:07 in fact, always I thnk 12/03 05:07 I need a better font then. 12/03 05:07 almost done with my template :) 12/03 05:10 why does it take so long to make a simple template 12/03 05:13 ? 12/03 05:13 I'm explaining stuff in it :) 12/03 05:13 somehow, firefox finds characters for everything, but none of my other programs do. 12/03 05:15 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 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23917#a23917 12/03 05:18 others in here might know more about it :) 12/03 05:18 but basically, coinduction is scary 12/03 05:18 how long have you been using haskell, anyway? 12/03 05:19 * Mathnerd314 checks install date 12/03 05:21 Monday March 8 2010 12/03 05:23 this might be a bit precocious then :) 12/03 05:23 so... 4 days? 12/03 05:23 but it's fascinating stuff, if you're interested in going deeper than haskell 12/03 05:23 deeper in some directions, at least 12/03 05:23 well, I've been thinking about type theory (or some fascimile of it) for a while longer 12/03 05:24 cool 12/03 05:24 anyway, there's a fairly accessible tutorial on the agda wiki 12/03 05:25 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 12/03 05:25 so peano naturals have an infinity in codata... that means you can induct to aleph-null? 12/03 05:30 because my proof is one by induction 12/03 05:40 so you need to do that for infinite lists 12/03 05:40 well, did you actually prove anything for infinite lists? 12/03 05:41 in your earlier proof 12/03 05:41 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 wouldn't it be induction to ω rather? 12/03 05:42 Is that powerful enough? 12/03 05:42 yeah, that's what I want to happen. 12/03 05:42 the definition takes elements one at a time, so the proof should be able to as well... 12/03 05:45 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 Mathnerd314: well, I started writing the laws and then remembered it's hard to prove equality on codata :P 12/03 05:50 but you'd probably want to start by proving the functor laws, and build up to the monad ones 12/03 05:50 how do you prove equivalence? 12/03 05:51 magic? 12/03 05:51 on regular data? 12/03 05:51 on colists 12/03 05:51 well, you could prove that any finite prefix of the colists is equal 12/03 05:52 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 well, the proofs are typically functions 12/03 05:53 "if you give me a colist, I'll hand you back a proof of some property of that colist" 12/03 05:54 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 but it's not too bad 12/03 05:54 you can copy that into your file and try using \~~ instead of \== 12/03 05:55 or you can just import Data.Colist if you'd prefer :) 12/03 05:56 import Data.Colist sounds good... what's the point of libraries if you don't use them? 12/03 05:56 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 I'm not certain I understand what the second part is doing 12/03 05:59 the _::_ constructor? 12/03 06:00 yeah 12/03 06:00 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 that's what I was trying to say above 12/03 06:01 I see :) 12/03 06:01 so you should be able to prove the functor laws fairly simply with those 12/03 06:02 I think the fmap id == id is actually unnecessary given the other law 12/03 06:03 (not in all categories, but in the ones we care about) 12/03 06:03 "all monads are functors and applicatives" 12/03 06:03 yep 12/03 06:03 according to wikipedia 12/03 06:03 ;-) 12/03 06:03 the reason I started with functor is that it's simpler 12/03 06:03 using the return/bind in monad is a lot messier 12/03 06:04 so fmap + return + join tends to be cleaner 12/03 06:04 but you're free to approach that proof as you wish 12/03 06:04 you can probably convert between the proofs if you have one 12/03 06:04 by the way, typing a question mark and typechecking will create a hole for you 12/03 06:06 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 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 so why does xs appear 3 times in the argument list and ys only twice? 12/03 06:06 there's something asymmetric about the definition... 12/03 06:07 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 you have a delayed proof that they are 12/03 06:08 there's xs= : inf (b xs = b ys) 12/03 06:08 I don't see why there's an xs= at the beginning 12/03 06:09 that xs~~ is just a name of the proof 12/03 06:09 it's to make error messages prettier 12/03 06:09 you could omit it 12/03 06:09 (it'll also make a couple of features of the agda interactive environment more useful) 12/03 06:09 oh. so a : b means argument of name a and type b? 12/03 06:10 yeah 12/03 06:10 you typically use it when you need to refer to its actual value later in the type 12/03 06:10 what about a :: b? 12/03 06:10 :: is the colist constructor 12/03 06:10 ok. so the reverse of Haskell ;-) 12/03 06:10 yep :) 12/03 06:11 and the _ on either side of it is a neat feature called mixfix 12/03 06:11 factorial would be _! for example 12/03 06:11 doesn't scala have something like that? 12/03 06:11 you can even have if_then_else_ : Bool -> a -> a -> a 12/03 06:11 :) 12/03 06:11 I don't think so 12/03 06:11 I think you can put underscores in things to make implicit functions, but not sure 12/03 06:12 I remember seeing some language having (_ > _) 12/03 06:12 and using it as an argument to functions 12/03 06:12 I think it does, but that's a form of partial application 12/03 06:12 so you could write 5 + _ * 10 or something and get a function that takes a number to a number 12/03 06:13 I've definitely heard of a language with that feature, but this is different 12/03 06:13 this is giving you pretty deep control of the parser 12/03 06:13 you can write _==_mod_ : Nat -> Nat -> Nat -> Bool, for example 12/03 06:14 ok. 12/03 06:14 and if it sees 7 == 13 mod 6 12/03 06:14 it'll call that function 12/03 06:14 so like pattern matching but better 12/03 06:14 _==_[mod_] : Nat -> Nat -> Nat -> Bool maybe 12/03 06:15 sort of 12/03 06:15 * Mathnerd314 finishes compiling the standard library 12/03 06:16 :) 12/03 06:16 one fairly amusing feature of agda is that most of its users never actually run their programs 12/03 06:16 why run it if you've already proven it to be correct? :P 12/03 06:17 can you actually run them? 12/03 06:17 sure, you can compile down to haskell in two different ways 12/03 06:17 you can also ask the agda-mode to "normalize" terms for you 12/03 06:17 which is a bit like running 12/03 06:17 compile to haskell o_O 12/03 06:17 yep 12/03 06:17 I thought C was high-level... 12/03 06:17 lol 12/03 06:17 haskell is semantically quite similar to agda 12/03 06:17 a lot closer than C, at least :) 12/03 06:18 so, in the standard library, map-cong is the same as fmap? 12/03 06:18 map is fmap 12/03 06:18 (or just map) 12/03 06:18 map-cong is a proof 12/03 06:18 in fact, it's more or less what you need to prove for fmap id == id 12/03 06:19 but its type is pretty obscure :P 12/03 06:19 it's basically saying that map preserves equality 12/03 06:20 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 a function a->b, and it gives a proof a=b -> map a=b? 12/03 06:20 map a = map b 12/03 06:20 * 12/03 06:20 with implicit "type" parameters a and b 12/03 06:21 sort of 12/03 06:21 you can actually ask agda to expand that type for you 12/03 06:21 C-c C-d map-cong 12/03 06:21 I'm using command-line, remember? since emacs+agda crashes? 12/03 06:22 oh, yeah :/ 12/03 06:22 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 you have a function, two colists, a proof that they are equal 12/03 06:23 it gives you a proof that after applying that function to both colists, the results are still equal 12/03 06:23 ok. 12/03 06:24 but it's also a definition of a map function, right? 12/03 06:24 well, sort of 12/03 06:24 its definition is almost identical to that of map 12/03 06:24 but it's constructing a value of _≈_, not a Colist 12/03 06:25 agda automatically disambiguates constructors 12/03 06:25 so there the [] on the right hand side is a constructor of _≈_ 12/03 06:25 and the :: is too 12/03 06:25 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 so how many overloads are there of []? 12/03 06:26 two in this module, as far as I can see 12/03 06:26 but you can write as many as you want 12/03 06:26 ok. 12/03 06:26 overloading only works with constructors 12/03 06:26 so I can just ignore all that and pretend they're constructors 12/03 06:27 of CoLists 12/03 06:27 until I have to prove stuff 12/03 06:27 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 curry-howard isomorphism! 12/03 06:29 yep :) 12/03 06:29 _≈_ =[ map f ]⇒ _≈_ is another example of mixfix by the way 12/03 06:29 the function is _=[_]⇒_ 12/03 06:29 IRC client keeps putting in emoticons in odd places ;-) 12/03 06:32 anyway, how do you get emacs to find plugins? 12/03 06:33 can't remember :P I'm not an expert by any means 12/03 06:33 anyway, I need to go get some work done, lest I get my ass kicked tomorrow :P 12/03 06:34 I'll probably be back tomorrow evening if you have any more questions 12/03 06:34 when do you sleep? I can't figure it out... 12/03 06:34 not often enough :/ but I'm US eastern time, and will probably go to sleep in a few hours :P 12/03 06:35 so 3 am or something? 12/03 06:35 1:35 right now 12/03 06:35 not sure when I'll go to sleep, I hope as soon as possible 12/03 06:35 but I still have to finish a paper 12/03 06:36 on type theory? :p 12/03 06:36 actually, it's a bit of a high-level introduction to that, for a class 12/03 06:36 it's just a writing class, so it's not terribly in-depth 12/03 06:36 fortunately, I have not yet advanced that far. I just have homework to do. 12/03 06:38 :) 12/03 06:38 back to work, then. 12/03 06:38 yep :) good luck with this stuff! 12/03 06:39 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 mh, maybe on the wiki, though only the built-in syntax has ascii equivalents 12/03 21:14 alternately, I just installed some good fonts ;-) 12/03 21:39 saner route :) 12/03 21:40 any recommendations for a good unicode monospace font? 12/03 21:42 (not that DejaVu is that bad) 12/03 21:42 my main font is Bitstream Vera Sans Mono 12/03 21:42 DejaVu is the successor to that, so ok. 12/03 21:43 I wonder how fonts have "snapshots" and "release candidates"... 12/03 21:45 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 But, you have to have those other fonts, of course. 12/03 21:48 I have billions of fonts, but none of my editors are smart enough to use those others :-( 12/03 21:48 Are you not using emacs? 12/03 21:48 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 Ah. 12/03 21:50 Well, then, you are entering a world of pain, probably. 12/03 21:50 Writing Agda is far, far easier with the emacs mode. 12/03 21:51 I'm also trying to install it manually... 12/03 21:52 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 yay 12/03 23:06 but I have to downgrade to Emacs 22.3, since 23.1 doesn't support BDF fonts on windows :-( 12/03 23:30 after further testing, it appears that something in the BDF code is causing my system to reboot. 12/03 23:46 so, like I said before, anybody know a good set of fonts with all the glyphs Agda uses? 12/03 23:47 This is probably not helpful, but how about running some instance of leenucks in a virtual machine? 12/03 23:53 User apps causing the OS to reboot is… er… embarrassing to say the least. 12/03 23:53 I'm doing all this on windows right now 12/03 23:57 --- Day changed Sat Mar 13 2010 If you have the spare memory, VirtualBox is free and Free. 13/03 00:15 yeah, I have virtualbox. it's not running anything though. 13/03 00:15 What is the biggest uni course Agda has been used in so far? 13/03 01:51 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 in emacs you can customize the include dirs 13/03 02:01 otherwise you pass -i flags to the CLI 13/03 02:01 by "working installation", I meant emacs... how do I customize the include dirs? 13/03 02:03 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 customize Agda2 Include Dirs to include the path to the library 13/03 02:09 however you also need the agda-mode setup step 13/03 02:09 TacticalGrace: undergrad? Nottingham has a few fourth-years taking it. 13/03 02:09 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 ok. 13/03 02:26 agda seems to hate byte order marks? 13/03 02:40 Perhaps. Haven't encountered BOMs for a while. File a bug? http://code.google.com/p/agda/ 13/03 02:42 UTF-8 doesn't need BOMs, but under Windows, text editor seem to add them anyway… 13/03 02:44 right. 13/03 02:44 and emacs seems to hide them, so they're hard to remove 13/03 02:45 how active is agda? bug tracker seems rather full... 13/03 02:46 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 it seems to mostly be "call for papers" 13/03 02:50 liyang: yeah, undergrad 13/03 02:52 liyang: I'm currently teaching (parts of) it to a class of 70 something 13/03 02:53 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 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 (At Swansea) 13/03 02:57 (Also, aren't they a bit old to be undergrads?) 13/03 02:58 liyang: ;) 13/03 03:00 hadn't seen Setzer's course, but seen txa's notes 13/03 03:01 agda is *slow* 13/03 03:56 is \to the same as -> ? 13/03 04:00 Mathnerd314: yes 13/03 04:03 how do I do the equivalent of Haskell's case? 13/03 04:06 do I need a helper function? 13/03 04:07 depends, you may want to use a with 13/03 04:07 I want to write this, basically: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23913 13/03 04:08 just the >>= part though 13/03 04:08 so 'with' sounds like the right thing 13/03 04:09 copying from http://www.cs.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Filter.agda 13/03 04:09 you can use with for that 13/03 04:09 see, eg, Appendix A.5 in http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf 13/03 04:09 and function composition is... 13/03 04:16 ^ TacticalGrace 13/03 04:24 I'm not sure whether it is pre-defined 13/03 04:25 Have you downloaded the standard library? 13/03 04:25 yes 13/03 04:25 + added it to the path and compiled everything in it 13/03 04:26 ok 13/03 04:26 I'm not sure whether it is defined in there, but might be worth to have a look 13/03 04:26 There should be a Haddock for Agda.... 13/03 04:26 or if Hoogle could be adapted 13/03 04:28 that would be very useful, gioven types in Agda are even more expressive than in Haskell 13/03 04:28 gioven = given 13/03 04:28 I think it might be better if Haskell just adds enough language extensions that it turns into Agda 13/03 04:28 but anyway, I'm hearing no? 13/03 04:29 there is always that business about termination, but I agree that it is a tantalising goal 13/03 04:29 (as far as composition operator) 13/03 04:30 I'm not aware that is pre-defined, but I'm far from an Agda expert 13/03 04:30 and we are working with an intuitionistic logic, so I'll settle for the third option ;) 13/03 04:31 It doesn't seem that hard to me to just "borrow" the entire Haskell prelude... 13/03 04:32 but this function signature seems wrong: _._ : ∀ {A B C} → (B → C) → (A → B) → A → C 13/03 04:40 ^ TacticalGrace 13/03 04:43 it's no dependent function composition 13/03 04:43 that is more complicated 13/03 04:43 I think it is somewhere in Ulf Norell's AFP'08 lecture notes 13/03 04:43 wow, a very long type ;-) 13/03 04:46 so function composition must be somewhere in the standard library... 13/03 04:51 yep, open import Function 13/03 04:51 I think 13/03 04:51 it's \o with agda's input method 13/03 04:51 not sure if you managed to fix your emacs 13/03 04:51 it was some font problems 13/03 04:52 its type is terrifying, so I recommend you don't look at it :) 13/03 04:52 oh, right 13/03 04:53 it's in Data.Function 13/03 04:53 oh, I think that got renamed to just Function 13/03 04:53 didn't look under Data for function composition 13/03 04:53 but maybe not in any released version of the std lib 13/03 04:53 in lib-0.3 13/03 04:53 supposedly lib-0.3 is the version to go with the latest Agda release 13/03 04:53 yay, that finished my porting of my monad's definition from Haskell to Agda 13/03 04:54 http://www.cs.nott.ac.uk/~nad/listings/lib/Function.html#255 13/03 04:54 yeah, NAD renamed it 13/03 04:54 now it's top-level 13/03 04:54 there's now a Function.(Bi/In/Sur)jection and Function.Equality 13/03 04:54 .Inverse too, all sorts of goodies! 13/03 04:55 it's all line noise to me... 13/03 04:56 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 Mathnerd314: I agree, big chunks of agda are practically illegible, sadly 13/03 04:56 Agda = Perl and Haskell = Python ;-) 13/03 04:57 so, proofs are functions over the variables that return equality? 13/03 04:59 TacticalGrace: are you already teaching the course using agda? 13/03 04:59 Mathnerd314: ? 13/03 04:59 I'm translating my proof into Agda... so I need the type signatures 13/03 04:59 proofs don't have to be functions 13/03 05:00 what else are they? 13/03 05:00 just plain old values 13/03 05:00 test1: 1 :: 2 :: 3 :: [] == 1 :: 2 :: 3 :: [] 13/03 05:01 test1 = refl 13/03 05:01 :P 13/03 05:01 * Mathnerd314 is confused again 13/03 05:01 that is basically forcing agda to run a unit test at compile time for you 13/03 05:01 types are logical statements, values are proofs of the associated types 13/03 05:02 but here, I have to prove that (return x) >>= f == f x 13/03 05:02 copumpkin: yep, two weeks into that course 13/03 05:02 oh cool, how's it going? 13/03 05:02 last week was the first week with Agda 13/03 05:02 You should ask the student's that question 13/03 05:02 :) 13/03 05:03 we are starting very slowly 13/03 05:03 most of them don't know Haskell (or any other FP language) and the math bakcground is very varied 13/03 05:03 Mathnerd314: yeah, you'd state that as forall f x -> return (x >>= f) == f x 13/03 05:03 we basically did Curry-Howard for propositional logic last week 13/03 05:03 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 next week, we'll look at quantifiers and dependent types 13/03 05:04 TacticalGrace: sounds like they'll be learning a lot of awesome stuff pretty quickly :) 13/03 05:04 not quite as quickly as Mathnerd314, maybe 13/03 05:04 I'm not learning, just doing ;-) 13/03 05:05 without at least an intuitive understanding of Curry-Howard, I don't think Agda makes a lot of sense 13/03 05:05 yeah, I agree 13/03 05:05 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 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 besides, I think Curry-Howard is one of these very fundamental results of computing 13/03 05:07 yes, all CS, but from different CS programs 13/03 05:07 some have already done some formal methods using Event-B 13/03 05:07 but not all of them have done that 13/03 05:08 ah 13/03 05:08 (we have computer science, software engineering, computer engineering, and bioinformatics) 13/03 05:08 for the CS and SE students this course is compulsory 13/03 05:08 that's quite nice and granular 13/03 05:08 for the others its an elective 13/03 05:09 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 a functional DSL for array computations? 13/03 05:11 why not E? 13/03 05:11 I mean, why not embedded? 13/03 05:11 well, my main inspiration was my difficulty writing vector-static 13/03 05:11 I tried and failed to make a usable interface for statically sized vectors 13/03 05:11 (built on top of vector) 13/03 05:12 oh, ic 13/03 05:12 so, the idea is to track sizes? 13/03 05:12 statically 13/03 05:12 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 yeah 13/03 05:12 why not just use the monad I'm writing? ;-) 13/03 05:12 ok, that sound interesting 13/03 05:12 but actually writing any useful functions with vector-static proved to be a real pain 13/03 05:13 do you know http://www.cse.chalmers.se/~wouter/Publications/MoreDependentTypesForDistributedArrays.pdf 13/03 05:13 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 copumpkin: yeah, I can imagine that it is a pain in Haskell to help the type checker along 13/03 05:14 oh no, hadn't come across that, I'll check it out 13/03 05:14 even in agda, doing that kind of stuff is fairly painful 13/03 05:14 Algebra.RingSolver is good but the output is noisy 13/03 05:14 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 yep, a specialised solver would be useful 13/03 05:14 it's somewhat like DML, too, I guess 13/03 05:14 (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 cool 13/03 05:15 anyway, it's still vaporware but I've started writing my ring solver 13/03 05:15 sounds like a good plan :) 13/03 05:15 I'm excited! I just finished all my coursework for this term so am more free 13/03 05:15 yeah, it's good to be able to concentrate on something for a longer preriod of time 13/03 05:16 without context switching 13/03 05:16 yep :) 13/03 05:16 wouter's paper looks pretty interesting 13/03 05:17 so, can agda partially evaluate? 13/03 05:23 partially evaluate? 13/03 05:26 I have to use the definitions of bind and return to prove stuff, right? 13/03 05:27 yep 13/03 05:28 so how do I apply those? 13/03 05:28 *use 13/03 05:29 you refer to them in your type 13/03 05:30 but they're already defined... 13/03 05:31 hmm, I don't understand your question :) 13/03 05:34 the type I have is ∀ {A B} → (x : A) → (f : (A → Colist B)) → (bind (repeat x) f) ≈ f x 13/03 05:34 okay 13/03 05:34 so then I have to implement it... 13/03 05:35 yep 13/03 05:35 you'd probably use a with construct 13/03 05:36 have you tried proving simpler properties first? :) 13/03 05:36 I don't see how this is complicated... :-_ 13/03 05:36 * _-: 13/03 05:37 as I said last time, proving things formally can be a lot harder than you'd expect :P 13/03 05:37 but the functor laws are fairly trivial 13/03 05:37 and might be a good start 13/03 05:37 (I just proved them) 13/03 05:37 proved in agda? 13/03 05:38 yep 13/03 05:38 * Mathnerd314 wants to see 13/03 05:38 just a sec 13/03 05:38 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23952#a23952 13/03 05:41 really trivial for functor, we'll see about applicative now :) 13/03 05:41 * Mathnerd314 forgot about [] and _::_ overloading 13/03 05:43 law3 is trivial too 13/03 05:45 law4 might be a little more work (but probably not) 13/03 05:45 huh, I tried filling in the rest of monad law 1 and got "Not implemented: type checking of with application" :- 13/03 05:46 I guess I need a helper function... 13/03 05:48 :o 13/03 05:49 never seen that before :) 13/03 05:49 how would I express that a function a -> Colist b is the same as a Colist of functions (a -> b)? 13/03 05:49 hm, it isn't really, unless you want to "sequence" it 13/03 05:50 over another monad 13/03 05:50 oh, wait, that's just the first law expressed differently 13/03 05:51 first law of what? 13/03 05:56 monads 13/03 05:56 almost done with applicative :P 13/03 06:02 fmap id == id is what you're talking about? 13/03 06:02 no, (bind (repeat x) f) == f x 13/03 06:03 so, if f x == l :: ls, then does ls = next (f x) ? 13/03 06:06 next? 13/03 06:07 a total tail function (next [] = []) 13/03 06:07 meh, hpaste is down now 13/03 06:07 hmm 13/03 06:08 that's the type error I'm getting now ;-) 13/03 06:10 can I see your code? moonpatio.com is still up 13/03 06:10 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8534#a8534 13/03 06:12 I think I might have defined helper wrong, maybe. 13/03 06:12 comments? 13/03 06:14 it looks reasonable so far 13/03 06:15 trying to see how I'd do it 13/03 06:15 definitely more painful than the earlier ones :) 13/03 06:21 well, you need bind or join 13/03 06:22 and bind is simpler IMO 13/03 06:22 yeah 13/03 06:22 I hate coinduction :P 13/03 06:23 anyways, by now I'm pretty certain that it's a monad, despite whether I can prove it or not 13/03 06:25 :P 13/03 06:25 say, if I define [] :: [] = [], then I can turn everything into infinite streams... 13/03 06:26 I'm actually confused at this 13/03 06:31 at what? 13/03 06:32 well 13/03 06:32 for your prop 13/03 06:32 1 13/03 06:32 the place where you call helper, I'd like to avoid calling helper 13/03 06:32 so I stick a hole there, and ask for the goal at that point 13/03 06:32 ((bind (x ∷ .ZipList.♯-2 x) (λ x' → next (f x'))  | next (f x))  ≈ ♭ ys) is what it gives me 13/03 06:33 meaning that further evaluation of the LHS of ~~ is delayed until next (f x) is evaluated 13/03 06:33 so I add another with next (f x) 13/03 06:33 decompose that 13/03 06:33 and it still refuses to evaluate the LHS any further 13/03 06:33 here, try changing, in bind, \b as to next (a \:: as) 13/03 06:39 the type simplifies a bit 13/03 06:40 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 ok, you're right. 13/03 06:42 good to know next is defined correctly though... 13/03 06:42 yep :) 13/03 06:43 gah, can't figure out why this isn't working 13/03 06:44 because it's secretly not a monad? :p 13/03 06:49 nah, I mean it's an agda issue (and I'm clueless) 13/03 06:51 not a thing about the proof 13/03 06:51 well, I'm reading this: http://www.mail-archive.com/haskell-cafe@haskell.org/msg57217.html 13/03 06:51 can't figure out how it's related to my implementation 13/03 06:53 other than that mine works and his doesn't ;-) 13/03 06:57 so yours works on his examples? 13/03 06:58 that's dolio by the way and he's often around here 13/03 06:58 I'm starting to think it isn't true, by trying to prove the associativity law 13/03 07:00 I think that message might give a counterexample... 13/03 07:00 it's pretty painful to type in colist literals :) 13/03 07:01 as I'm sure you're finding out 13/03 07:01 Mathnerd314: Your diagonal was different. 13/03 07:03 does it work on that example? 13/03 07:03 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 Yours quits as soon as it finds a missing diagonal element, which probably works. 13/03 07:05 Not sure why that never occurred to me. 13/03 07:07 it seems to work I think 13/03 07:07 unfortunately I can't get agda to prove it for me 13/03 07:07 oh yes I can 13/03 07:07 success? 13/03 07:08 oh wait 13/03 07:08 nope 13/03 07:08 oh well. 13/03 07:08 it has an extra element 13/03 07:08 .Data.BoundedVec.Inefficient._∷_ 8 .Data.BoundedVec.Inefficient.[] 13/03 07:09 != .Data.BoundedVec.Inefficient.[] 13/03 07:09 I could've done it in half the time in haskell :P 13/03 07:09 so where is this? 13/03 07:10 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8535#a8535 13/03 07:10 at least we have proofs that it's a functor an applicative, in case anyone doubted it 13/03 07:11 now, we should prove that no monad exists for ziplists ;) 13/03 07:11 does it satisfy law7? 13/03 07:12 I wasn't able to get it to reduce the expression further 13/03 07:13 not sure what's wrong 13/03 07:13 I'm probably doing something stupi 13/03 07:13 that hole in law9 looks pretty bad though 13/03 07:14 because there's only one colist in scope whose type will fit in the hole, and it doesn't "fit" 13/03 07:14 trying to prepend x onto it doesn't help eihter :P 13/03 07:14 proof! 13/03 07:15 (also, there's no way to get another colist of that type) 13/03 07:15 so, diag = join, right? 13/03 07:18 yeah 13/03 07:18 well, I get [1,8] and [1] here. 13/03 07:20 so I'm probably missing something. 13/03 07:20 Mathnerd314: the only answer is to prove once and for all that there can be no monad 13/03 07:27 and how do you do that? 13/03 07:27 well, I can state it :P 13/03 07:27 probably can't prove it 13/03 07:27 maybe one could use the laws to reach a contradiction? 13/03 07:27 yeah, that's how you prove negation 13/03 07:27 so one would assume... that the monad obeyed the laws of ZipList? 13/03 07:28 (functor / applicative) 13/03 07:28 yeah 13/03 07:28 basically showing that the applicative laws don't fit with the monad ones 13/03 07:29 not even sure it's true, but it'd be neat :) 13/03 07:29 well, first, it should act correctly on infinite lists, right? 13/03 07:31 and use map and repeat 13/03 07:37 so join should be the diagonal, for infinite lists 13/03 07:39 yeah, it should work correctly on those 13/03 07:40 and for join . (fmap return) to be id, it's the diagonal up to the size of the list 13/03 07:45 so, do bad things happen if I say []:[] = []? 13/03 07:51 * Mathnerd314 is too tired to think 13/03 07:54 where would you say that? 13/03 07:54 in a constructor it's probably fine 13/03 07:55 how can I prove _|_ from f [] ≈ f (something that very clearly is not []) 13/03 09:06 ah I guess it isn't trivial 13/03 09:11 yeah, you need injectivity of f 13/03 09:27 what if I have that f [] ~~ [] 13/03 09:30 and ~~ only has [] ~~ [] and then other constructors 13/03 09:31 hmm 13/03 09:31 I guess it still isn't trivial 13/03 09:31 hmm, it seems like it should be though 13/03 09:32 http://snapplr.com/t3be 13/03 09:32 if I have x ~~ [], it seems like x must be [] 13/03 09:33 hmm, I guess the closest equality I can define on x is what I already have 13/03 09:38 this might actually be provable 13/03 09:45 probably not though 13/03 09:48 what is f here? 13/03 09:56 if you have x ~~ [] you should get x = [] by pattern matching 13/03 09:57 nope :/ 13/03 09:59 oh maybe 13/03 09:59 nah 13/03 10:00 f is join :P 13/03 10:00 a hypothetical join :o 13/03 10:00 I'm trying to prove that there are no monads for ziplist :P 13/03 10:01 on colists, that is 13/03 10:01 where is ~~ defined? 13/03 10:02 in Data.Colist 13/03 10:02 oh, found 13/03 10:02 seems like == really isn't very useful around coinduction 13/03 10:03 http://pastebin.com/bZWru9ui <- i'm sure i miss the bigger picture, but this part works :) 13/03 10:05 hmm, let me try that :) 13/03 10:06 that doesn't even typecheck for me 13/03 10:08 that p 13/03 10:08 _301 ≈ _301 !=< [] ≡ [] of type Set 13/03 10:08 when checking that the expression refl has type [] ≡ [] 13/03 10:08 funny, maybe you've another refl in scope? 13/03 10:09 oh good point 13/03 10:09 I had a setoid open 13/03 10:09 aha, nice 13/03 10:10 now I need to figure out how to get a bottom out of this :) 13/03 10:11 it's kind of a ridiculous exercise 13/03 10:11 i like to prove bottoms :) 13/03 10:12 I feel like I've forgotten something 13/03 10:14 but that I'm on the right track 13/03 10:14 maybe I'll go to sleep 13/03 10:15 http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/ <- UCF' here is supposed to be data or codata? 13/03 15:32 ok, just made *yet another data structure* 13/03 15:51 that acts like ZipList most of the time 13/03 15:52 and the other?:) 13/03 15:52 the other is the ordinary Data.Colist (Haskell's list type) 13/03 15:53 the problem is that ZL (as I call it) is an infinite data structure 100% of the time 13/03 15:58 so I don't see how to display it 13/03 15:58 or test for equality 13/03 15:59 write something like take :: Nat -> ZL a -> List a, to get prefixes 13/03 15:59 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 ok, that works. 13/03 16:41 and ZL works on examples! 13/03 16:44 because the intermediate results aren't proper lists 13/03 16:45 but they are ZL's 13/03 16:45 * Mathnerd314 celebrates 13/03 16:53 nice :) 13/03 16:54 do you have the code somewhere? 13/03 16:54 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8541#a8541 13/03 16:56 (haskell, since I still am fuzzy on Agda) 13/03 16:57 so, normal lists [a,b,c] look like a ZL of {a,b,c,E,E,E,E,...} 13/03 16:59 and infinite lists look like {x,x,x,x,x,...} 13/03 16:59 but you get all these weird ones like {E,x,E,x,...} 13/03 17:00 which need to exist for the monad to preserve associativity 13/03 17:00 (and that disappear in normal cases of lift/zipWith) 13/03 17:01 that ZL type reminds me of dataflow programming, where the Events have different clocks 13/03 17:02 s/clocks/periods/ or whatever they are called 13/03 17:02 yeah, that's where I got the idea (particularly lucid) 13/03 17:02 it calls them streams 13/03 17:02 come to think of it, I can probably say a ZList is an infinite list of Maybe a... 13/03 17:03 yeah 13/03 17:04 then the Applicative is just the composition of ZipList and Maybe applicatives 13/03 17:04 and all the functions are a bit shorter 13/03 17:05 yup 13/03 17:05 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 really? 13/03 17:56 not f (Cons a b) = Cons (g a) (f b) ? 13/03 17:56 i.e. folds? 13/03 17:56 well, the two instances of f have different type arguments 13/03 17:57 ah, sure 13/03 17:57 sounds like you could do f x = fmap f x 13/03 17:58 actually, that pattern is only used in my definition of fmap ;-) 13/03 18:03 it's only the second, g a = Cons (g a) (g b) 13/03 18:03 in fact... that's pretty much my entire code 13/03 18:05 I don't even need all the specifics. 13/03 18:10 it's probably a monad combinator or something... 13/03 18:13 so, for example, I have fmap f (Cons a b) = Cons (fmap f a) (fmap f b) 13/03 18:40 how do I make Cons an instance of Functor? 13/03 18:41 afaik there's no way to avoid that pattern, OTOH you could use DeriveFunctor in ghc-6.12 13/03 18:46 I'm just trying to figure out what I would write for the instance declaration. 13/03 18:52 I think I need... 3 type variables? 13/03 18:54 you can't do that 13/03 18:55 why? :-( 13/03 18:56 well what are the types of Cons? maybe you can 13/03 18:56 data Cons a b = Cons a b 13/03 18:56 fmap f (Cons a b) = Cons a (fmap f b) is the only thing you can do there 13/03 18:57 the Functor is actually (Cons a), so you can't change the a 13/03 18:58 fmap :: (a -> b) -> (Cons c) a -> (Cons c) b 13/03 18:58 fmap :: (Functor c) => (a -> b) -> (Cons c) a -> (Cons c) b, you mean? 13/03 19:01 the thing about functor is that you don't have control over what types it ranges over 13/03 19:12 so not that 13/03 19:12 Mathnerd314: you'd need BiFunctor from category-extras 13/03 19:13 Mathnerd314: that doesn't make sense, Functor only applies to things of kind  * -> * 13/03 19:17 for example it doesn't make sense to say  Functor Int,  only something like  Functor Maybe, or Functor List, or ... 13/03 19:17 well, Cons is of kind * -> * -> * 13/03 19:18 indeed. 13/03 19:18 so it can't be an instance of Functor.  but  (Cons a) can, for any a. 13/03 19:18 hmm, why are we talking about this in #agda? =) 13/03 19:19 if you squint enough it's valid agda too :) 13/03 19:20 hehe 13/03 19:20 * looks just like Set to me 13/03 19:22 :) 13/03 19:22 how do you even write algebraic data types in Agda? 13/03 19:31 Mathnerd314: the syntax is very close to the syntax for writing GADTs in Haskell. 13/03 19:37 oh, data x : x where x 13/03 19:38 yep 13/03 19:39 a line for each constructor with its type, etc. 13/03 19:39 so data Cons : Set1 where cons : ∀ { A B } → A → B → Cons ? 13/03 19:42 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 * not given 13/03 19:47 data Const (A : Set) (B : Set) : Set where cons : A → B → Cons A B 13/03 20:12 or data Cons : Set -> Set -> Set1 where cons : ∀ { A B } → A → B → Cons A B 13/03 20:12 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 no 13/03 20:29 --- Day changed Sun Mar 14 2010 so how do I specify the monad laws, so I can use them to prove properties of things containing monads? 14/03 03:14 magic? 14/03 03:22 --- Day changed Wed Mar 17 2010 hi. Why does it sometimes complain inside { }0 that the text is read-only? 17/03 11:33 emacs i mean. 17/03 11:33 jotik: only on the last space right? 17/03 11:48 jotik: or your are trying to use a command whose scope is beyond the end of the hole. 17/03 11:49 in pattern matching when value is wrapped into {}, what does it mean? 17/03 11:56 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 of course, there is no mention of this is manual 17/03 11:59 in* 17/03 11:59 so can someone confirm it 17/03 11:59 RLLa: {...} denotes implicit arguments both in the types (f : ∀ {A : Set} ...), the expressions (f {ℕ}) and the patterns (f {A} ... = ...) 17/03 12:24 uh oh 17/03 12:24 RLLa: was it clear enough ? 17/03 12:24 certanly not 17/03 12:25 let's take an example 17/03 12:25 well, i'm trying to implement well-known tabulate function here 17/03 12:25 sure 17/03 12:25 id : ∀ {A : Set} → A → A 17/03 12:25 id {A} x = x 17/03 12:26 then a test 17/03 12:26 id {ℕ} zero 17/03 12:26 it just restricts type? 17/03 12:26 nop 17/03 12:26 compare this with: 17/03 12:26 id' : ∀ (A : Set) → A → A 17/03 12:27 id' A x = x 17/03 12:27 test 17/03 12:27 id' ℕ zero 17/03 12:27 in id' the type argument is explicit 17/03 12:27 in id it is implicit, this means that in most cases I can write (id zero) without giving the type 17/03 12:27 but if I want it, I can by using the {} 17/03 12:28 clearer ? 17/03 12:28 implicit arg thing is clear 17/03 12:28 but not in pattern matching 17/03 12:28 ok 17/03 12:29 I could have written the "id" body like this 17/03 12:29 id x = x 17/03 12:29 yes 17/03 12:29 but if I do need the implicit argument I can caputre it with {A} 17/03 12:29 example 17/03 12:29 len : ∀ {A : Set} {n : ℕ} (xs : Vec A n) → ℕ 17/03 12:30 len {_} {n} _ = n 17/03 12:30 don't you have to use {n} on rhs too? 17/03 12:30 len (1 ∷ 2 ∷ 3 ∷ []) ≡ 3 17/03 12:30 nop 17/03 12:30 in expression {...} are used to pass implicit arguments to functions 17/03 12:31 f {x} {y} z t 17/03 12:31 very good 17/03 12:31 i understand this now 17/03 12:31 but {x} means nothing by itself in expression 17/03 12:31 RLLa: cool 17/03 12:32 but is it possible to define tabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n without using {...}? 17/03 12:33 yes but using it will be ackward 17/03 12:33 imagine: 17/03 12:33 len' : ∀ (A : Set) (n : ℕ) (xs : Vec A n) → ℕ 17/03 12:34 len' _ n _ = n 17/03 12:34 test 17/03 12:34 len' ℕ 3 (1 ∷ 2 ∷ 3 ∷ []) ≡ 3 17/03 12:34 you kind of have to give the answer as argument yourself. 17/03 12:34 ah, you have to give N and 3 as explicit actual arguments 17/03 12:35 yes 17/03 12:35 actually you can give _ and let the type-checker try to guess it 17/03 12:35 but i meant definition of tabulate not type signature 17/03 12:35 RLLa: all three should follow the same scheme: type, patterns, expressions 17/03 12:36 hm 17/03 12:36 however you can first define a function with explicit arguments and expose a short definition with implicit argus 17/03 12:36 anyway, here is my definition: tabulate {s n} f = (f (fz {n})) :: (tabulate {n} (λ x → f (fs x))) 17/03 12:36 my question was can you define it without matching on Nat 17/03 12:37 what is your type for tabulate 17/03 12:37 tabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n 17/03 12:38 ? 17/03 12:38 yes 17/03 12:38 and you have a second equation about 0 ? 17/03 12:38 yes 17/03 12:38 but that's trivial case 17/03 12:38 RLLa: so, if you have 2 equations something in the pattern must distinguish them 17/03 12:39 have you tried to write the second line as: 17/03 12:39 tabulate f = f fz :: tabulate (λ x → f (fs x)) 17/03 12:40 ? 17/03 12:40 hm, let me see 17/03 12:40 maybe the type-checker can infer them 17/03 12:40 hm, yes 17/03 12:41 but is it good idea to let type-checker infer things? 17/03 12:41 RLLa: yes 17/03 12:43 Agda inference system only fills a hole when the answer is unique and directed by the typechecking of the rest 17/03 12:43 hm, it looks more like complete magic 17/03 12:44 which is a limitation but on the plus side we can be sure of the safety of it 17/03 12:44 :) 17/03 12:44 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 something you can do is to put a ? instead of _ and then in emacs "C-x =" get the infered value 17/03 12:48 oh, i didn't know that 17/03 12:49 Saizan: what ? 17/03 12:50 the "C-x =" command 17/03 12:51 though it doesn't seem to work in my code 17/03 12:51 maybe it's C-c = 17/03 12:52 * npouillard use viper and so have other bindings 17/03 12:53 found it in the menu 17/03 12:54 though if the term contains applications of record fields you get something very ugly 17/03 12:57 npouillard: Sry for my absence. Duty called. 17/03 14:28 npouillard: I was just trying to type into the hole 17/03 14:28 jotik: no problem, got it to work ? 17/03 14:45 npouillard: well yes somehow. I haven't yet figured out what causes this to happen. 17/03 14:57 bbl 17/03 14:59 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 is there a good representation for a monad in agda? 18/03 20:23 there is one in the "standard" library 18/03 20:26 I want to prove the monad laws, which are missing from that 18/03 20:27 yeah, you have to extend it if you want this 18/03 20:27 agda does not seem like a friendly language... 18/03 20:29 no it's not :> 18/03 20:30 mh, why not? 18/03 20:30 coming from haskell i felt quite at home after a while :) 18/03 20:30 knowing haskell does help 18/03 20:31 but still, brain explosion can't be considered friendly 18/03 20:31 that's just it... there's no brain explosion yet. 18/03 20:33 i actually have some monad code around here 18/03 20:34 with proofs of laws for maybe monad :\ 18/03 20:35 oh, that's the first monad I would implement. 18/03 20:37 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24115#a24115 <- state is quite easy :) 18/03 20:47 list is working out quite well too 18/03 20:47 yeah, it's pretty nice exercise 18/03 20:59 Saizan: wow, that was a lot of work, eh :P 18/03 21:07 you could've saved 3/4 of the proof characters you typed, by the way 18/03 21:08 defining r = refl ? 18/03 21:08 _ 18/03 21:08 oh 18/03 21:08 it saves so much work 18/03 21:09 I love it 18/03 21:09 i thought that only worked for \top 18/03 21:09 anything it can infer unambiguously, as far as I can tell 18/03 21:10 I use it for tedious types I can't be bothered to type out 18/03 21:10 not really much work saved. i think most of it it result of "refine" command 18/03 21:10 ah 18/03 21:10 (I was just being silly about saving work, but I do like using it) 18/03 21:10 yeah, i've used it in types and expressions in EquationalReasoning 18/03 21:11 though i thought that it wouldn't work for data constructors for some reason 18/03 21:11 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 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 hmm, im not having much luck proving comonad laws for stream comonad 19/03 02:38 i think i dont understand agda coinduction stuff yet 19/03 02:38 i gather that i need different equality than the propositional equality? 19/03 02:57 Can I set the fixity of an operator that is a parameter to a type? 19/03 03:19 record R (_+_ : ...) where ... infix 5 _+_ 19/03 03:20 Jaak: yes. See stdlib/{Data/{Conat,Covec},Coinduction}.agda for examples and details. 19/03 03:50 liyang: thanks 19/03 14:35 the module system is confusing me a lot. is there some up to date read on it? 19/03 14:54 Jaak: not that much, better I got was in some talks about it in the agda repo 19/03 14:54 i've learned what i know by the reference manual and seeing it used in the standard library 19/03 14:54 first result on google is a talk from 2006, im don't know if it's current 19/03 14:54 i* 19/03 14:55 there is a module system for agda? 19/03 14:55 what are you confused about, specifically? 19/03 14:55 RLa: yes 19/03 14:55 it's similar to ML functors 19/03 14:56 Saizan: not that much, you cannot take modules as arguments 19/03 14:57 only values 19/03 14:57 and so records which in turns are equipped with a module 19/03 14:57 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 Saizan: i'm not too sure. might be confusion over the standard library 19/03 15:01 i have defined a setoid but i dont really know how to use it for equational reasoning 19/03 15:03 import Relation.Binary.EqReasoning as EqR; open EqR yoursetoid 19/03 15:05 "open EqR yoursetoid" is a shorthand for "module M = EqR yoursetoid; open M" i think 19/03 15:06 awesome, seems to work now 19/03 15:09 can Agda prove termination of loops? 19/03 20:08 ??? yes 19/03 20:11 that question can be interpreted in many ways :) 19/03 20:11 Mathnerd314: Agda is a logic which is strong enough for analysis 19/03 20:11 at least 19/03 20:11 so if you define a language which has loops and its semantics you can prove that 19/03 20:16 or were you referring to recursive definitions in agda itself? 19/03 20:16 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 my problem is that I can't think of any complicated examples of infinite loops... 19/03 20:25 and 19/03 20:38 if (UNPROVED CONJECTURE) then LOOP else HALT 19/03 20:38 oh, that 3x+1 conjecture sounds good. 19/03 20:44 what are you doing this for 19/03 20:46 some small amusement... 19/03 20:47 no 19/03 20:48 I mean like 19/03 20:48 what is it you are doing 19/03 20:48 i don't think you are going to prove 3x+1 terminates 19/03 20:48 for example 19/03 20:48 I was coming up with an example where proving termination is difficult 19/03 20:50 I have one, so now I'm good. 19/03 20:51 im just curious why 19/03 20:51 ... I couldn't see anything in-between "while(true) {}" and the Halting Problem 19/03 21:10 there's a very interesting one 19/03 21:12 hydra 19/03 21:12 fax: what's that one? 19/03 21:40 you cut of its head and it grows infinity more 19/03 21:41 so the question is does hercules win (and the answer is yes he always wins) 19/03 21:41 but you must use ordinal analysis to prove termination 19/03 21:41 this is a non-trivial termination argument 19/03 21:41 http://coq.inria.fr/distrib/V8.2rc1/contribs/Cantor.epsilon0.Hydra.html 19/03 21:41 fax, looks fun, is there a more commented / coqdoc'd version? 19/03 21:48 Idon tkno 19/03 21:48 Mathnerd314 depth first algorithm to four color a planar map 19/03 21:49 coqbloq? 19/03 21:49 :[ 19/03 21:49 :) 19/03 21:50 * Mathnerd314 is confused 19/03 21:51 Mathnerd314, you don't know about four colors suffice? 19/03 21:52 well, I know that. 19/03 21:52 I am just telling you examples that came to me 19/03 21:53 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 use four colors to color an arbitrary tiling of the surface of a torus! 19/03 21:54 7 ? 19/03 21:54 4 is so much more badass 19/03 21:54 I bet chuck norris could do it 19/03 21:55 impossible! 19/03 21:55 p=\left\lfloor\frac{7 + \sqrt{1 + 48g }}{2}\right\rfloor  (Weisstein). 19/03 21:55 lol 19/03 21:55 how many colors you need for a thing with genus g 19/03 21:55 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 (sphere of course corresponds to planar) 19/03 21:56 simple! 19/03 21:56 --- Day changed Sat Mar 20 2010 Does this approach to defining categories and functors make sense? http://www.galois.com/~emertens/category/category.html 20/03 02:44 I tried to follow the spirit of things like IsPreorder and Preorder 20/03 02:44 --- Day changed Sun Mar 21 2010 "In order for the memory footprint of the typechecker to ﬁt within the 21/03 13:02 physical memory of the machine, we were forced to factor the proof – sometimes 21/03 13:02 unnaturally – into several submodules." 21/03 13:02 heh 21/03 13:02 fax: what would need such a large proof? 21/03 14:05 Mathnerd314, I think it's more agda than the proof being big 21/03 14:05 this is from the dependently typed grammars paper 21/03 14:06 --- Day changed Mon Mar 22 2010 Hi all. I'm trying to compile an agda "Hello world" example  (main : IO Unit  [[newline]] main = putStrLn "Hello world!") 22/03 03:42 I get the following error 22/03 03:43 Basics.agda:1,1-1 22/03 03:43 Basics.agda:1,1: Parse error 22/03 03:43 main : IO Unit main = putStrLn "He... 22/03 03:43 what's wrong with it? 22/03 03:44 Is that all that's in the file? 22/03 03:49 Those two lines, that is. 22/03 03:49 I don't think Agda lets you omit the "module Foo where" line. 22/03 03:50 Foo being the name of the file. 22/03 03:50 Thanks. Done. Now I get "Not in scope ... when scope checking IO Unit " 22/03 03:58 You also have to import the modules that define IO and such. 22/03 04:02 I've never really used IO in agda, though. I can't help you beyond that. 22/03 04:03 Now I did an "open import IO.Primitive" and it works for IO. 22/03 04:23 "open import Data.Unit" did not work for "Unit" 22/03 04:23 Unit doesn't exist. It's named \top 22/03 04:24 Which looks like a T. 22/03 04:24 \top being how you type it in in the agda emacs mode. 22/03 04:24 ⊤ 22/03 04:25 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 and get used to that 22/03 04:29 It's quite helpful. 22/03 04:30 I think so. I still have to get used to it. 22/03 04:31 Thanks for your help. 22/03 04:32 No problem. 22/03 04:33 Can i define [_for_in_] python-like list comprehension operator in agda? 22/03 16:20 perhaps. what's the type? 22/03 16:25 Well... 22/03 16:36 [ x for x in list ] is equal to just   list 22/03 16:37 [ even x for x in list ] is equal to    map even list 22/03 16:38 so i'm not sure what is type of first subexpression 22/03 16:39 just a   or  a → b  defaulting to id 22/03 16:40 what?? 22/03 16:47 ah.. forget it 22/03 16:48 Should I be able to make a program parse by removing a line break after a semicolon? 22/03 21:18 pigworker: I'm no agda implementor but does sound fishy to me 22/03 21:23 i think it makes sense. 22/03 21:24 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 you don't need semicolons to do that? 22/03 21:26 I would get something to do with indentation, but I've never observed this kind of thing.. 22/03 21:27 let has sort of layout like in Haskell. 22/03 21:27 So it probably doesn't expect you to put a semicolon at the end of one let line. 22/03 21:27 Only in beteween definitions on the same line. 22/03 21:27 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 You can mix. I just tried it. 22/03 21:28 let i = 0 ; j = 1 k = 2 in k 22/03 21:28 As long as you align k with i. 22/03 21:28 The first k, that is. 22/03 21:29 Yep, that works. I thought I tried that a while ago, but I must have screwed up the alignment. 22/03 21:29 That's easy to do with unicode characters, at least for me. 22/03 21:30 Some of them aren't really monospace, but they count as one character. 22/03 21:30 Not a problem which afflicts me, as I haven't the energy for unicode. 22/03 21:31 I'm about to try it *interactively*. 22/03 21:31 Ah. I can't align stuff interactively. I just have to tidy it up once it's done. 22/03 21:33 Btw does anyone know of a terminal emulator & font combination that will print characters like → at a readable size? 22/03 21:33 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 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 Sometimes I wish Ulf's implementation of pattern unification understood records (not that mine ever did). 22/03 22:01 pigworker: you on irc? nice ... 22/03 22:04 kosmikus: I saw a link to a free mac client on the Agda wiki, and decided to check it out 22/03 22:05 good work :) 22/03 22:06 pigworker: will you be here more often? 22/03 22:09 kosmikus: too early to tell; I'm experimenting with a new form of displacement... 22/03 22:11 we've had Pierre-Evariste, Edwin b, Peter Morris.. now CONor 22/03 22:12 :D 22/03 22:12 this is the unofficial epigram2 channel after all. 22/03 22:12 yeah well there's been an epigram channel but on average 1 person at a time there 22/03 22:13 I didn't know there is one 22/03 22:13 most of the serious work on epigram2 gets prototyped in agda anyway 22/03 22:13 I'd join ;) 22/03 22:13 it roughly doesn't exist 22/03 22:13 to say, 5 decimal places 22/03 22:13 pigworker: as long as you're not claiming that epigram is going to be implemented in agda 22/03 22:14 She is sort of half way between haskell and agda? :) 22/03 22:15 kosmikus: no, but bits of it get weakly approximated, and that way we figure out what to implement 22/03 22:16 fax: true. 22/03 22:16 pigworker: yes, that's absolutely understandable. I'm also using Agda for that purpose more and more. 22/03 22:16 fax: in the tradition of Zeno 22/03 22:16 So, here's something I've been wondering... 22/03 22:20 When you eventually introduce a hierarchy of universes, if that's what you in fact do... 22/03 22:21 What happens with regard to set equality vs value equality? 22/03 22:21 I suppose that makes sense even now with Set : Set, as ! Set > Set == Set > Set ! 22/03 22:22 dolio: sets-as-values equality gets farmed out -- ! Set > S == Set > T ! = S <-> T 22/03 22:24 dolio: that stratifies, too... 22/03 22:25 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 So, for S : SetN, T : SetM, there's a S <-> T. 22/03 22:26 Even if N /= M. 22/03 22:26 pigworker: yes, hpaste will work 22/03 22:26 pigworker: just go to hpaste.org, click new 22/03 22:26 TODO: Agda paste side 22/03 22:26 Someone needs to write an agda hilighter for whatever coloring library hpaste uses. 22/03 22:27 I wonder what the complexity of agda syntax coloring is? 22/03 22:27 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 dolio: good luck. :) 22/03 22:27 :) 22/03 22:27 why not just a file uploader which typechecks the file and gives a link to the html output? 22/03 22:27 stevan: should be a machine with lots of RAM ;) 22/03 22:28 pigworker: I guess that just works out of universes are cumulative? 22/03 22:28 If, even. 22/03 22:28 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 good night 22/03 22:31 dolio: something like http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24263 22/03 22:32 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 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 fax: Thorsten hired a student a while back; it's no longer available 22/03 22:38 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 I probably just have to be patient.. 22/03 22:39 the only ones I know of are martin lofs one and fresh lists and the examples from Peter Dybjer 22/03 22:40 fax: it's more a question of figuring out which IR definitions make sense, and how 22/03 22:40 oh that's quite different than I had imagined then 22/03 22:40 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 Agda seems to get along fine with it. 22/03 22:42 As far as we know. 22/03 22:42 No one's proved false lately. 22/03 22:43 dolio: I constructed an impredicative universe at one stage, because they forgot a check 22/03 22:44 Heh. 22/03 22:44 Although that is something I've wondered off and on... 22/03 22:44 Are families indexed by Set "inductive" families? 22/03 22:45 hehe 22/03 22:45 Set is not defined by induction. 22/03 22:45 At least in Agda. 22/03 22:45 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 dolio: and Gil Hur gets quite close to the bone, thanks to that... 22/03 22:46 In that sense, the line that "GADTs are a special case of inductive families" isn't necessarily true. 22/03 22:48 But, since GHC doesn't have inductively defined static things, there's no other choice. 22/03 22:50 Not that people care about proofs of false in that environment anyhow. 22/03 22:50 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 Even though there are 6 other ways to do the same thing. 22/03 22:51 what does it mean if you can prove false? 22/03 22:53 It means you have a non-terminating 'value'. 22/03 22:53 what blows my mind is that people still go to the trouble of endcoding inductive proofs in haskell.. 22/03 22:53 so it's an infinite loop or something in the type checker? 22/03 23:05 Well, the definition of false would be 'data False : Set where', so there are no proofs (constructors) for it. 22/03 23:06 Mathnerd314: needn't be 22/03 23:06 Mathnerd314: Think of it as the type-theory equivalent of I JUST DIVIDED BY ZERO. OH SHI- 22/03 23:06 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 forall P, P   could be another definition 22/03 23:06 oh, so all it means is that your type checker is too lenient. 22/03 23:16 Well, it could mean lots of things. 22/03 23:17 Haskell, for instance, essentially adds fix as a primitive. And fix id has the right type. 22/03 23:18 That's not a failure of the type system, per se. 22/03 23:18 Crucially, false hypotheses are relatively benign; it's closed proofs of false that behave badly. 22/03 23:18 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 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 general recursive types aka negative types ? 22/03 23:24 Consistency also enables a class of optimizations: it's not just soundness for the sake of it. 22/03 23:24 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 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 I can't figure out what that does... can it ever return a value? 22/03 23:40 It reduces to itself forever. 22/03 23:40 right... but can you feed it arguments and get out values? 22/03 23:41 No, it just spins. 22/03 23:42 so it's an infinite loop, suitably disguised? 22/03 23:43 it's not disguised 22/03 23:43 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 fax: it's disguised in lambda calculus, because usually infinite loops are in imperative languages 22/03 23:44 oh 22/03 23:44 yeah i don't think it's a roundabout way to represent a C program 22/03 23:44 it's a special case of the fixpoint combinator, Y = \ f -> (\ x -> f (x x)) (\ y -> f (y y)) 22/03 23:44 liyang: is that why YI is so-called? 22/03 23:48 pigworker: the editor? I have no idea… 22/03 23:50 * fax thinks yes 22/03 23:51 YI = I(YI) 22/03 23:51 http://haskell.org/haskellwiki/Yi#Trivia says yes. 22/03 23:51 I'm wondering if SICK computes to anything interesting. 22/03 23:52 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 SICK = IK(CK) = K(CK) 22/03 23:54 liyang: I was thinking of the editor; I had a spinning editor situation earlier. 22/03 23:56 Ah nice, KISS IS S 22/03 23:57 YUCK = UUUUUUUUU(YUCK) 22/03 23:57 pigworker: related to the spinning Aquamacs on Twitter earlier? 22/03 23:59 --- Day changed Tue Mar 23 2010 liyang: the very same; ironic, given the proof was about productive coprograms 23/03 00:00 good lord, it's pigworker! 23/03 00:06 evening 23/03 00:06 edwinb: not quite sure how that happened 23/03 00:07 pigworker -- did you ever 'To Mock a Mockingbird'? :) 23/03 00:07 (lovely book... embossed cover and rough pages) 23/03 00:08 fax: my Smullyan coverage is thin, and doesn't make it that far 23/03 00:08 pigworker: how is your agda based central heating system? 23/03 00:09 edwinb: cooler, now that I've been distracted 23/03 00:10 *whooooosh* 23/03 00:14 What was that? Sounded like productivity. 23/03 00:14 good luck making pigs fly anyway ! 23/03 00:15 I hear it happens sometimes 23/03 00:15 just doing some of the exercises I set in my blog post 23/03 00:23 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 g'night all; see yiz round 23/03 01:29 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 Won't Function.id do the job? 23/03 04:20 well, I want to apply it only to true values.. 23/03 04:21 a better question might be.. 23/03 04:21 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 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 stepcut: sure. Require a proof that the list starts with 1 as another parameter. 23/03 04:22 liyang: sounds easy :) 23/03 04:22 Once you see it… 23/03 04:23 yes, that has been my problem so far 23/03 04:23 it's easy after I see it, but not before :p 23/03 04:24 I sort of came up with something that works, by creating a new type 23/03 04:24 but I haven't figure out if it is a weird way to do it yet :) 23/03 04:24 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a24272 23/03 04:25 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 but I am not sure how to make rule1 a 'function' instead of a 'constructor' 23/03 04:26 (Sorry, my Aquamacs is taking forever to go through its spin cycle. Hang on…) 23/03 04:28 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24273#a24273 23/03 04:31 Go into that hole, and refine-case on the xs≡1∷ argument. 23/03 04:31 ok 23/03 04:31 (and again on the second part of the product ^^;;) 23/03 04:33 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 Okay, now put y into the hole and do that again. 23/03 04:38 and then x ? 23/03 04:38 now I have, oneHead .(1 ∷ x ∷ xs) (x ∷ xs , ≡.refl) = {!!} 23/03 04:40 So inspecting the proof forces the first argument to begin with a 1. :) 23/03 04:42 (the x in (x , y) is just the rest of the list. 23/03 04:43 right 23/03 04:43 I sort of understand how this works :) 23/03 04:44 time for bed now. thanks! 23/03 04:45 I think I understand what I have done with the System type in the code I was writing too.. 23/03 04:46 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 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a24274 23/03 04:53 sweet! 23/03 04:56 I hope that wasn't homework. :-/ 23/03 04:58 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 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 I didn't know people even had agda homework :p 23/03 05:00 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 stepcut: I'm aware of a few courses that teach it. :) 23/03 05:00 yeah 23/03 05:00 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 OH SHI- Of course. I ought to have remembered. ^^;; 23/03 05:02 :) 23/03 05:02 I supposed it could be somebodies homework, but it's not mine :) 23/03 05:04 but it's already tomorrow now, so I gotta get to sleep, thanks again! 23/03 05:04 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 right 23/03 05:05 (if that made any sense.) 23/03 05:05 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 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 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 Agda mode for TextMate would be great 23/03 10:32 TextMate at least manages to do the unicode font rendering properly 23/03 10:32 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 I switched to that after I got fed up with aquamacs 23/03 15:25 It fixed the things that annoyed me, although I can't remember what those annoyances were... 23/03 15:26 (if it works better, it might be appropriate to add a note about it on the wiki.) 23/03 15:29 I am not confident enough about that ;) 23/03 15:30 it was only minor annoyances for me 23/03 15:30 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 I was trying to think of a non induction+lots of finicky algebra proof of binomial theorem 23/03 21:26 like counting how many paths has k lefts in them in a size n perfect tree or something 23/03 21:27 never found a good way though 23/03 21:27 (when I said induction above I mean the P(n)=>P(n+1) stuff) 23/03 21:27 --- Day changed Thu Mar 25 2010 is there a convenient way of constructing piecewise functions? 25/03 02:37 Elaborate? What would be the inconvenient way? 25/03 02:51 nested ifs 25/03 02:52 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 Have you got a particular example? (hpaste?) 25/03 02:53 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a24345 25/03 02:54 I defined ≟ and ≠ cause I couldn't find simple boolean versions over nat 25/03 02:54 You can at least do this: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a24346 25/03 02:56 ah, that's perfect, thanks 25/03 02:57 You might actually be able to leave the false values as _ 25/03 02:57 I'm just copy/paste mangling that 25/03 02:57 er… I was going to use Data.Nat._≟_ which returns a proof of i == j if they are equal. 25/03 03:03 I just used boolean cause I wasn't particularly interested in why they were or weren't equal 25/03 03:14 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 Hi. 26/03 02:55 quick question 26/03 02:55 What does MAlonzo have anything to do with me? 26/03 02:55 Seriously, I tried to compile simple agda examples with no success 26/03 03:02 "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 so I'm having an issue with agda not being able to show that two things are equal 26/03 03:45 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24380#a24380 26/03 03:46 Oh that's a very frequent problem. 26/03 03:46 what is it resulting from? 26/03 03:47 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 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 It's not immediately obvious. :( I'd look for where the e₀' was coming from. 26/03 03:51 the go function is actually nothing, just trying to pattern match an ok-add 26/03 03:52 (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 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 unfortunately I see no obvious way of "factoring" the e's that are the terms of the add :( 26/03 03:54 is it maybe because it "forgets" since they become a single term?  Namely the argument to the injection. 26/03 03:58 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 that seemed to be the problem.  Sadly each time one thing gets fixed it introduces another issue 26/03 05:05 It's a gift that never stops giving. 26/03 05:20 looks like lots of exciting stuff was discussed at the AIM.. sized types, structual equality, etc. etc. 26/03 12:57 anyone know what "Java Agda" means? 26/03 12:57 or "Agda-A" 26/03 12:57 ah "A new implementation of Agda written in Java " 26/03 12:58 that sounds cool 26/03 12:58 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 andgra: what's the definition of it? 26/03 13:34 the subset operator? 26/03 13:35 yes 26/03 13:35 well, the one from Data.Sets (stdlib 0.3) is just _?_ : ? ? Set 26/03 13:36 s1 ? s2 = ? x ? x ? s1 ? x ? s2 but 26/03 13:36 I cant read it 26/03 13:36 it's just question marsk 26/03 13:36 weird, that type doesn't even typecheck for me 26/03 13:37 _ss_ : -> -> Set 26/03 13:38 what's the agda file 26/03 13:38 but the definitions of I don't really understand 26/03 13:38 Data.Sets in the standard library 26/03 13:38 is it actualyl called 26/03 13:38 yes 26/03 13:38 so that type actually typechecks? 26/03 13:39 it somehow wrapps DecSetoid from Relation.Binary 26/03 13:39 http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda 26/03 13:39 : Set 26/03 13:39 = DecSetoid.Carrier decSetoid 26/03 13:39 _⊆_ : → Set 26/03 13:39 s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂ 26/03 13:39 andgra, can you see this correctly? 26/03 13:39 yeah 26/03 13:39 okay good 26/03 13:39 so you want to pre 26/03 13:39 so you want to prove* 26/03 13:40 prf : ∀ {a b} {A C : Set a}{B : Set b} →  (x : C) (f : A → B) → (C ⊆ A) → (f x) ⊆ B 26/03 13:40 prf = ? 26/03 13:40 which is the same as: 26/03 13:40 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 ? 26/03 13:40 yeah what Jaak says... 26/03 13:40 why have your paste got  Set a  but the thing is    ? 26/03 13:41 yeah, posting whole file that types might help 26/03 13:41 why not  prf : {A B C : } →  (x : C) (f : A → B) → (∀ x → x ∈ C → x ∈ A) → (∀ x → x ∈ (f x) → x ∈ B)  ? 26/03 13:41 well, in the paste I was using Relation.Unary but I'm guessing that will not work 26/03 13:41 I haven't tried that... 26/03 13:41 Relation.Unary???????????? 26/03 13:42 why am I looking at this http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda 26/03 13:42 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 andgra 26/03 13:42 why would you want to use either of them? 26/03 13:43 andgra: yeah, what are you trying to do - at a high level? 26/03 13:44 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 project on sets? 26/03 13:45 ? 26/03 13:45 guerrilla http://people.cs.uu.nl/stefan/downloads/brink10dependently.pdf 26/03 13:47 yeah, i read most of that.. what part? 26/03 13:47 all of it 26/03 13:48 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 from what i saw, his code works directly 26/03 13:48 fax: why should i look at it? 26/03 13:48 hehe 26/03 13:48 have we talked before? 26/03 13:48 andgra; f : A -> B ? 26/03 13:48 andgra oh you mean like a nonsurjective function 26/03 13:49 the set f(A) <= B 26/03 13:49 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 guerrilla I think agda will get quotients soon! 26/03 13:50 yeah 26/03 13:50 andgra, so in type theory we can define this 'inverse image' in a very different way than set theory 26/03 13:51 fax: sorry, what do you mean by quotient? 26/03 13:51 wait it's not inverse image :/ 26/03 13:52 it's just the normal image 26/03 13:52 data Image {A B} (f : A -> B) : Set where witness : forall (a : A), f a -> Image f 26/03 13:52 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 andgra yeah but it's not set theory 26/03 13:52 no clue why they call it Set actualyl, but it's a type 26/03 13:53 I'm not completley sure I understand? 26/03 13:53 also... {A B C : } doesn't typecheck... 26/03 13:55 in what context? 26/03 13:56 http://pastebin.com/raw.php?i=iF9FSJbG 26/03 13:58 even "{A : } -> \top" doesnt typecheck, infact 26/03 14:00 Jaak: that's interesting... 26/03 14:00 i think andgra's code doesn't because he's saying A and B are members of the type then saying he has some function from some member to another.. which doesn't make a lot of sense 26/03 14:01 that would be like f : zero -> zero for Nat afaik 26/03 14:02 {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 same principle applies here 26/03 14:02 maybe someone can explain that more elegantly though :) 26/03 14:02 im not sure what's with Jaak's though.. i would think that would work 26/03 14:03 so something like '\all {a b} {A C : a} {B : Set b}' or am I missing the point completely? 26/03 14:03 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 well you cant do Set b 26/03 14:04 i see 26/03 14:04 oh, I mean ' b' ofc... 26/03 14:05 yup, giving argument helps 26/03 14:05 well, mtg time. bbiab 26/03 14:24 good luck 26/03 14:24 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 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 I wanna wirte my category theory notes in epigram ;D 26/03 17:24 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 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 ah that's it! thanks 26/03 17:38 --- Day changed Sat Mar 27 2010 Hi all 27/03 01:24 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 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24412#a24412 27/03 03:22 can I somehow tell agda to just do one level of expansion and then apply refl? 27/03 03:23 just "refl" doesn't work 27/03 03:23 as imported from Relation.Binary.Core 27/03 03:24 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 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 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 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a24450 27/03 19:44 the refl simply says "f0 m m m = f0 m m m" 27/03 19:44 'with' is evil 27/03 19:44 ah, why's that? 27/03 19:50 should I expand it to helper functions myself then? 27/03 19:52 i don't know 27/03 20:04 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 like 27/03 20:05 I'll give it a shot, thanks, it actually hadn't crossed my mind to try something like that 27/03 20:05 case1 : Rec i j (suc k) 27/03 20:05 m not quite that 27/03 20:05 case2 : Rec (suc k) (suc k) (suc k) 27/03 20:05 sorry.. 27/03 20:05 case1 : Rec (suc k) (suc k) (suc k) 27/03 20:05 case2a : Rec (suc k) j (suc k) 27/03 20:05 case2b : Rec i (suc k) (suc k) 27/03 20:05 and so on 27/03 20:05 ah, another clever idea, thanks 27/03 20:05 so then you can 'prove' a general theorem, that  forall i j k, Rec i j k 27/03 20:06 that should let you do the e 27/03 20:06 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 maybe it'll work out tohugh 27/03 20:06 (oh Rec might be a recursive type too, where f_0 is recursive) 27/03 20:07 yeah, I'm actually trying to give a more general proof that f0 and this other function T are equal 27/03 20:08 can I see T? 27/03 20:10 this is kind of interesting I thought f_0 was just a made up function 27/03 20:10 yeah, it's actually the schedule for a parallel implementation of the algebraic path problem 27/03 20:13 T is an optimized version 27/03 20:13 wow cool 27/03 20:13 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a24451 27/03 20:14 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 which follows from induction on k 27/03 20:15 f0 is actually an example of a very general class of schedules for affine recurrence equations 27/03 20:20 but they obviously present unreasonable time complexity so more efficient schedules are needed, usually requiring human ingenuity to discover 27/03 20:20 I'd never heard of affine recurrence equations before 27/03 20:21 ill probably start seeing them everywhere now :D 27/03 20:21 haha, that always seems to be how it is 27/03 20:22 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 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 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 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 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 stevan -- you know of Peter Morris' thesis? 28/03 12:50 yes 28/03 12:50 but i only glanced thru it. 28/03 12:51 it seems to be an implementation of the second half of that 28/03 12:51 kmc, Ah, thanks a lot for the answer, very much appreciated. 28/03 13:13 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24467 28/03 14:32 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 (in the comments I meant "case-split" not "refine" btw) 28/03 14:36 actually not lemmas, definitions, but you know what I mean 28/03 14:38 try giving the typechecker more info; respects : forall {A B : Set} [...] 28/03 14:44 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 Is there any point in writing respects eq with eq; … | refl = ? rather than just respects refl = ? 28/03 14:49 probably not 28/03 14:50 in fact, that works, apart from ambiguous levels 28/03 14:50 outside of the context that is 28/03 14:51 might be worth trying   with C2 | eq  ; ...  |.C1 | refl  for a laugh 28/03 14:52 in fact, respects : (C1 ≡ C2) → Set; respects with eq | C2; respects refl | .C1 = ? works… 28/03 14:55 Spot the deliberate mistake. 28/03 14:58 compatible {A} {.A} refl _<_ _≤_ = _<_ ⇒ _≤_ 28/03 15:03 much easier to work on relations than records... 28/03 15:03 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 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 looks like I do, because the def of monotonicity is incorrect otherwise 28/03 15:23 hrm. there's no equality defined on Fin 28/03 15:31 There's an Ordering though. 28/03 15:35 ah, it's in Data.Fin.Props 28/03 15:38 if you say "using ()" does that mean "hide everything"? (it's followed by a "renaming" so it's not pointless) 28/03 15:40 yes 28/03 15:44 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 Setoid !=< _12 of type Set1 28/03 16:15 :\ 28/03 16:15 when checking that the expression Nat₌ has type _12 28/03 16:15 any ideas on why? 28/03 16:15 i'm basically trying to use setoids to emulate Haskell's Eq typeclass functionality... 28/03 16:17 have you discovered _≟_ in Data.Nat yet? 28/03 16:34 I find Agda's records are too cumbersome to emulate type classes tbh 28/03 16:36 yeah.. hmm, i'll check out _≟_ 28/03 16:44 who do I send library patches to? 28/03 16:56 hi byorgey 28/03 18:15 hi fax 28/03 18:16 hrm. how to prove x ∉ [ y ] if x ≢ y 28/03 20:15 I suppose that is equivalent to proving   x in [ y ] -> x = y 28/03 20:19 which is probably trivial from the definitions 28/03 20:19 did you solve it HairyDude ? 28/03 20:46 stevan: solve what? 28/03 20:59 I have 11 holes in my source file atm :) 28/03 20:59 your last question. :-) 28/03 21:00 ah... no 28/03 21:03 I can't even see how to prove x ∉ [] :/ 28/03 21:04 what's the definition 28/03 21:04 it's probably just pattern matching with no RHS (via ()) 28/03 21:05 doh, of course 28/03 21:06 thanks :) 28/03 21:06 here's both ways: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24480#a24480 28/03 21:06 i'm bored. 28/03 21:09 stevan write a program that turns a number into the sum of (at most) three triangular numbers 28/03 21:10 sounds like project euler... 28/03 21:12 no 28/03 21:12 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 Igloo - yes 28/03 21:12 Then what is the advantage of agda? It sounds like writin code in assembly rather than a HLL 28/03 21:13 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 one can write semi-automatic tactics in agda in agda 28/03 21:13 stevan, both coq & agda have this poincare principle 28/03 21:14 Does agda's dependent pattern matching do the same thing as coq's "dependent destruction"/"dependent induction"? 28/03 21:19 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 Igloo, there's a couple aspects to it 28/03 21:20 the theoretical part is the axiom _+ computation_,  you can add the axiom in coq but not the computation 28/03 21:20 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 stevan, I wouldn't say 'better programming language' 28/03 21:21 wasn't there a dependent pattern matching extension to coq recently added? 28/03 21:22 most nontrivial coq developments have some approximations of dependent pattern matching in them 28/03 21:23 we're basically redoing the same stuff again and again :| 28/03 21:24 equations is really nice but coq still lacks the theory part I said above 28/03 21:24 I really hate it when case-split gives you invalid clauses 28/03 21:24 Igloo: http://www.reddit.com/r/dependent_types/comments/b0vb7/agda_vs_coq_by_wouter_swierstra_with_some_input/ 28/03 21:28 Thanks! 28/03 21:29 what I am mostly wondering is once we have  eta, K and quotients.. will that be _enough_? 28/03 21:30 enough for what? :) 28/03 21:31 presumably there will be some point where we can just do everything in a sensible way 28/03 21:31 what's K? 28/03 21:32 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 I didn't phrase that last one correctly actually not sure how to put it other than formally 28/03 21:34 stevan, we can get all this stuff just by having proofs convertibly equal.. for some reason coq doesn't though :/ 28/03 21:34 you mean dependent sums? 28/03 21:36 yeah 28/03 21:36 what is it that ssreflect provides to its user? 28/03 21:42 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 though* 28/03 21:47 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 Igloo - I think it's because us lot are just into the new stuff :P 28/03 22:15 although coq is pretty old. 28/03 22:15 but I don't think it says anything bad about Isabelle 28/03 22:15 Oh, "dependent types" rather than "theorem proving". Maybe that's why 28/03 22:16 i don't really like the reddit situation, there are too many subreddits... 28/03 22:17 stevan yeah I don't really get it 28/03 22:18 and most of them are dead... 28/03 22:18 people create further subreddits because higher level subreddits start to suck 28/03 22:32 and in general, the suck rises as you go up the chain 28/03 22:32 it'd be nice to have all the stuff categorized somehow 28/03 22:33 rather than just in a random list 28/03 22:33 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 it would, but who determines the categorization would be a battle in itself 28/03 22:34 I wish jbapple still blogged he wrote some cool stuff 28/03 22:34 Mathnerd314 -- you know we were talking about termination and the hydra thing? 28/03 22:51 sometime long ago, yes 28/03 22:52 it's called Goodstein sequence 28/03 22:52 didn't know that 28/03 22:52 --- Day changed Mon Mar 29 2010 hmm.. I was going to ask a question, but by typing it out I figured it out... :) 29/03 00:00 I should try that more often. 29/03 00:01 bleh. case-split is causing stack overflows now. 29/03 00:38 theorem proving uses a lot of memory :/ 29/03 00:41 well, agda in general uses a lot of memory, ime :) 29/03 00:45 i should remember to switch back to 32bit 29/03 00:45 hey, are there any plans to parallelise agda? 29/03 00:47 Saizan, ooh, that might be an issue, yes 29/03 00:48 sheesh. just giving one goal takes forever now 29/03 00:48 sometimes splitting your code into different modules helps 29/03 00:50 so it doesn't retypecheck what you don't change 29/03 00:50 mmm 29/03 00:51 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 "end of file during parsing" - weird 29/03 00:51 forgot the module header, maybe? 29/03 00:52 this is the module I've been working on all day 29/03 00:52 weird. new module, I'm getting "ambiguous name refl" even though it's only exported from one place 29/03 00:57 s/exported/imported/ 29/03 00:57 ah, no it isn't 29/03 00:58 end of file error is caused by stack overflow, apparently 29/03 01:03 Let's see if I can cheat. Has anyone written a partiton function for Vec? 29/03 01:04 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 Amadiro: no. there are pragmas that let the compiler know that ℕ is natural numbers, so it can optimise 29/03 01:06 HairyDude, Ah, I guessed something like that would be possible, thanks :) 29/03 01:07 actually... yes, that definition will be, but the actual libraries use primitive functions. I think. 29/03 01:07 I don't know much about the internals of Agda so I might be wrong on that. 29/03 01:08 Amadiro?? 29/03 01:09 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 peano numbers are slow yes 29/03 01:09 Amadiro nobody is seriously going to use peano numbers for computing things........ 29/03 01:09 Amadiro: succ is primitive 29/03 01:09 fax, yeah, I was just wondering. 29/03 01:09 Amadiro the reason we have peano numbers is they are fundamental object in inductive proofs 29/03 01:09 HairyDude, hm, ok, thanks. 29/03 01:09 fax, yeah. 29/03 01:10 Amadiro: the natural numbers are constructed from the constructors zero and suc 29/03 01:10 Amadiro -- you can implement binary numbers of whatever they are more efficent 29/03 01:10 Amadiro or you can axiomatize something like gmp integers and use them via haskell ffi 29/03 01:10 Right, I'll need to get a hang on dependent typing first, but thanks a bunch for the info :D 29/03 01:10 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 Amadiro, you can worry too much about 'efficency' in an attempt to be pragmatic 29/03 01:12 HairyDude -- example for what 29/03 01:12 ? 29/03 01:12 fax, yeah, I'm not really worrying about efficiency, I was just wondering. 29/03 01:12 okay 29/03 01:12 Trying to get an idea of what the compiler will do with the input, etc. 29/03 01:12 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 HairyDude, treesort? 29/03 01:13 realisabiility? 29/03 01:14 does agda do that?? 29/03 01:14 no, I'm just using agda to get the program right, and apply realisability by hand 29/03 01:15 I suspect minlog does it, btw 29/03 01:15 oh cool 29/03 01:15 how do you apply this by hand 29/03 01:15 just strip out the first order part, you end up with a Haskell-like program :) 29/03 01:16 okay 29/03 01:16 well, it's more complex than that, but I can't be bothered to explain it right now. 29/03 01:16 uh ok 29/03 01:16 nice having you 29/03 01:17 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 nope, didn't work 29/03 01:21 pigworker: I don't know treesort, and don't really have time to learn it 29/03 01:21 merge sort maybe 29/03 01:22 HairyDude, what makes you think you don't know treesort, when you do know quicksort? 29/03 01:22 pigworker: because I don't know the name? :) 29/03 01:24 Treesort is build-binary-search-tree, then flatten; which is effectively what quicksort does. 29/03 01:24 ah, right 29/03 01:25 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 I don't know any good examples of well-founded recursion. 29/03 01:27 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 oh and I think Saizan will have maybe done the proofs too, in Agda 29/03 01:28 but maybe I misremember 29/03 01:28 (talking of well founded recursion) 29/03 01:31 or lack of 29/03 01:31 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 hehe 29/03 01:33 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 this stuff? http://www.cs.st-andrews.ac.uk/~rd/publications/ 29/03 01:50 HairyDude: yeah, the stuff with Luis Pinto; the implicational fragment is tiny 29/03 01:56 night all 29/03 02:05 fax, thanks again for telling me about peano numbers, I worked through the wikipedia article, and feel slightly more enlightened :) 29/03 02:07 I actually never read about his axioms before. 29/03 02:08 it'sreally cool stuff ;) 29/03 02:10 It is, and simple enough for me to grasp as well :) 29/03 02:11 sigh. termination checker can't see that suc n < suc (suc n) 29/03 02:26 or... no, that y :: xs < x :: y :: xs 29/03 02:27 again.. what are these qoutients that people keep mentioning? 29/03 13:13 guerrilla do you know setoids 29/03 13:13 i'd like to think i do. trying to work with them now actually 29/03 13:14 they are related i take it? 29/03 13:14 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 you could form the quotient type S/~ and then a function S/~ -> S'/~' must satisfy that 'morphism' relation 29/03 13:15 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 this is a better explanation http://www.e-pig.org/epilogue/?p=319 29/03 13:21 i see 29/03 13:27 ok 29/03 13:27 thanks 29/03 13:27 * guerrilla will look into that link 29/03 13:27 cool: http://code.haskell.org/Agda/test/succeed/TestQuote.agda 29/03 17:56 quoteGoal and quote are built in? 29/03 17:58 seems so 29/03 17:59 that's cool that'll be really useful 29/03 17:59 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 ohhhh 29/03 18:08 it gives TEXT instead of syntax that's weird 29/03 18:08 O_O 29/03 18:08 yeah that is a little bit less useful than i thought 29/03 18:09 typed agda terms inside agda would be hard, no? 29/03 18:15 yes 29/03 18:15 would untyped be enough for this purpose tho? 29/03 18:17 yes 29/03 18:17 a lot better than strings 29/03 18:17 the way I'd like to quote stuff is for agda to invert the interpretation function 29/03 18:18 this would be part of type inference, hopefull 29/03 18:18 hopefully 29/03 18:18 this patch was just pushed, perhaps they will improve it soon 29/03 18:18 I think it's once again time to download Agda and prove the Fundamental Theorem of Algebra. 29/03 21:13 umm 29/03 21:14 you're kidding 29/03 21:14 do you know what the fundametal theorem of algebra IS? 29/03 21:14 --- Day changed Tue Mar 30 2010 Are Agda's Haddock docs available online somewhere? 30/03 17:24 fax: seen todays patches? http://code.haskell.org/Agda/test/succeed/Reflection.agda :-) 30/03 17:31 looks promising 30/03 17:34 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