--- Log opened Mon Mar 01 00:00:17 2010
stevanlpjhjdh if you read the logs or if someone else catches him next time: http://www.cs.chalmers.se/Cs/Grundutb/Kurser/types/agda-lecture/Bool.html   http://www.cs.chalmers.se/Cs/Grundutb/Kurser/types/agda-lecture/Arith.html    he might find that helpful, i missed him twice now :-/01/03 18:01
Berengal_Is it possible to use agda's unicode input in other modes?01/03 21:22
stevani'd really like to use it combined with haskell-mode; if you get it working, please let me know :-)01/03 21:24
copumpkinI think agda's unicode input isn't its own01/03 21:24
copumpkinit has a name01/03 21:24
* Berengal_ goes source diving01/03 21:25
stevani miss proper modules, holes, unicode and mixfix when ever i code in haskell :-/01/03 22:05
stevancan'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
Saizanwrt holes in haskell there's a little tool built over the ghc-api01/03 22:13
Saizanit won't give you the context though01/03 22:14
stevani recall reading about it; does it work well? do people use it?01/03 22:14
Saizanit worked when i tried it, though i don't think it got much attention01/03 22:15
stevandoes C-c C-c work?01/03 22:15
Berengal_I sometimes ponder hacking hole and context support into haskell-mode somehow, but then I realize I have neither the time nor the skill to do it :(01/03 22:15
Berengal_Also:01/03 22:15
Berengal_(require 'agda-input)01/03 22:15
Berengal_(set-input-method "Agda")01/03 22:15
Saizanit just gives you the type of the hole, nothing of the rest01/03 22:15
Berengal_Put that in your .emacs and you've got agda input everywhere01/03 22:16
stevangreat, thanks.01/03 22:16
Saizanmh, now you're forcing me to use erc01/03 22:16
Berengal_My elisp skills are unfortunately not currently up to the task of adding that to haskell-mode, or make it its own minor mode. Perhaps I should look into that...01/03 22:17
stevandoes using \Gl instead of \ work in haskell? i recall \r \=> \l1 etc all work?01/03 22:22
Saizan\Gl doesn't work01/03 22:27
stevan:-/, i recall having seen a ticket about it, haskell' proposal perhaps?01/03 22:30
Saizanthere's one on ghc's trac01/03 22:30
stevanhttp://hackage.haskell.org/trac/ghc/ticket/110201/03 22:32
--- Day changed Tue Mar 02 2010
stevanlpjhjdh: 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
lpjhjdhI haven't, I'll take a look, thanks02/03 00:18
lpjhjdhstevan: my Value type is indexed by a term, is that unnecessarily descriptive?02/03 00:32
lpjhjdhI was having trouble formulating a few things I wanted to, like the fact that (t \<Down> v) always produces a value (I proved it later)02/03 00:33
lpjhjdhI 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 it02/03 00:34
Saizanyou mean you've Value : Term -> Set ?02/03 00:40
lpjhjdhyeah02/03 00:41
Saizanin that case you could "data _⇓_ : Term → {t : Term} -> Value t → Set where"02/03 00:41
lpjhjdhah, I guess that makes sense, I'll give it a shot, thanks again02/03 00:42
stevanwhat's the idea behind parametrizing the value on the term?02/03 00:45
lpjhjdhI was thinking I needed it to get nat values02/03 00:46
lpjhjdhbut I guess I could just have nv-zero nv-suc02/03 00:47
lpjhjdhand get the same information02/03 00:47
TacticalGraceJust out of curiosity, who maintains Agda these days?02/03 12:15
stevandolio: 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
dolioI'm not really up on how indexed functors/monads fit into formal category theory.02/03 13:44
dolioAs for what applications it has...02/03 13:46
dolioFree algebras are (I think) essentially how you give semantics for datatypes, only they're typically called initial algebras.02/03 13:47
dolioAnd cofree coalgebras (terminal coalgebras).02/03 13:47
stevanit would be really nice to get a gentle intro to how those things work.02/03 13:49
dolio(Co)free (co)monads are similar.02/03 13:50
dolioIf 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
dolioI think that's an all right description, at least. I'm by no means an expert in this.02/03 13:55
dolioObviously in Haskell monads are used to describe various types of computation.02/03 13:55
dolioAnd 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
dolioInstead of represented directly, with a 'runFoo' that just unwraps a newtype.02/03 13:56
stevanyou don't happen to have a reference to some book/paper which presents this without assuming too much prior knowledge?02/03 13:58
dolioI could point you to decent stuff on initial algebras and such.02/03 13:58
dolioFree monads and the like seems to be something some category theory books build toward.02/03 13:59
dolioI 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
stevanthe categorical/ algebraic concepts i'm sure i can find info about, but the connections/ applications in CS is harder?02/03 14:01
dolioIn category theory, monads and algebras thereof are how (or, the more popular way) you do (and generalize) abstract algebra.02/03 14:02
dolioSo, I suppose part of the connection is that programming and reasoning about programs involves algebraic structures.02/03 14:03
dolioAnd 'free' stuff is the purely syntactic.02/03 14:04
stevanhmm02/03 14:10
guerrillaso, 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
stevanso 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
stevannot sure, could you give more context?02/03 14:31
guerrillayeah, i thought i may have to resort to universes and that i couldn't pattern match on sets02/03 14:33
guerrillawell, for context, i just wanted a little syntactic sugar, like _* : Set -> Set would be basically (FiniteSet A)* = List A02/03 14:34
guerrillabut that's not syntactically valid :)02/03 14:34
guerrillaare 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 Set02/03 14:35
guerrillai'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
stevani 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
guerrillahmm, well i'll try playing a bit with universes/levels02/03 14:44
guerrillaactually, maybe i'll just make it work for this specific case for now and move on :)02/03 14:45
stevan:-)02/03 14:49
guerrillabtw, this is what i'm trying to get to work http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23177#a2317702/03 14:55
guerrillahuh, that was dumb02/03 14:57
guerrillacould have just done this all along:02/03 14:57
guerrilla_* : Set → Set02/03 14:57
guerrilla(A)* = List A02/03 14:57
guerrilla:P02/03 14:57
stevan:-)02/03 14:58
dolioYou don't need the parentheses.02/03 15:19
dolioA * = List A02/03 15:19
dolioSaves 1 character!02/03 15:20
guerrilladolio: w00t thanks ;)02/03 15:45
guerrillacool, my hpaste from above now type-checks. we'll see if this will work out in the end though :)02/03 16:49
guerrillaok, 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
guerrillasetoid code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23178#a2317802/03 19:20
guerrillafiniteset code here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=23179#a2317902/03 19:20
guerrillahow would i extract the equiv predicate to actually use it?02/03 19:21
guerrillais that even possible with this setup?02/03 19:21
guerrillait seems like i would need the implicit argument of _∈?_ to be explicit in it's second pattern matching clause...02/03 19:25
guerrilla(or yet again, pattern match on a type, which i'll just rule out now on the basis of what stevan said)02/03 19:25
stevanyou 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
guerrillaok thanks for the implicit vs. explicit part, i'll try that in a second02/03 19:52
guerrillai did start with the record method first, but had some universe issues for some reason, so decided to just do it that way for now02/03 19:52
guerrillaeven 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
guerrillai may go back to that later though02/03 19:53
guerrillastevan: great, that worked perfectly02/03 19:57
guerrilla_∈?_ {S} a (b ∈ B) = a == b where _==_ = eq-pred S02/03 19:57
guerrilla:)02/03 19:57
guerrillathanks a lot02/03 19:57
guerrillaodd that you couldn't use the {S} in the infix form..02/03 20:00
guerrillapbly a practical reason for that, i'd imagine02/03 20:00
stevan(setoid are defined in Relation.Binary btw)02/03 20:05
guerrillai know :) i'm trying something a little different - using predicates for relations..02/03 20:06
guerrillai find the Rel* code a bit difficult to follow as well02/03 20:06
guerrillamay re-do the whole thing with that as i get better with agda02/03 20:07
stevannormalizing the types: C-n <paste-type-code> might help02/03 20:07
guerrillahmm.. not using emacs unfotunately02/03 20:08
guerrillawhat would that do?02/03 20:08
stevanagda isn't really agda without emacs02/03 20:09
guerrillahmm, didn't realize it would be such a different experience02/03 20:09
guerrillai'm so used to vim.. hard to switch02/03 20:09
stevanit is like day and night, man :-)02/03 20:09
stevanuse viper-mode02/03 20:10
stevanemulate vi keys inside emacs02/03 20:10
guerrillaok, well, maybe i'll have to do a tutorial on emacs this weekend02/03 20:10
guerrilla(would prefer to use emacs as LISP >>> retarded VIM/ed language)02/03 20:10
stevanguerrilla: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing   added section on how to emulate vi inside emacs02/03 20:48
guerrillathat's great02/03 20:57
guerrillathanks a lot02/03 20:57
guerrilla(didn't get your 'use viper-mode' comment earlier, but i see now)02/03 20:57
stevani 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 vim02/03 21:00
guerrillaok, cool02/03 21:01
guerrillasounds like a plan02/03 21:01
stevansomeone should really make a screen cast of an interactive agda session, i think that would be very helpful for new people to appriciate holes02/03 21:02
guerrillavoluneering ? ;)02/03 21:03
stevani came up with the idea, that's half of the work! :-)02/03 21:05
stevansome software which displays the keys pressed in a subtitle like fashion would be nice to have for the task02/03 21:06
guerrillahmm, yeah, i haven't seen that before02/03 21:06
stevanought to exist02/03 21:07
--- Day changed Wed Mar 03 2010
skihm, 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
npouillardski: I think so03/03 12:46
ski(i.e., do case analysis on dependent arguments in the constructors)03/03 12:46
npouillardbut 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
npouillardand the types of the stdlib for Nat is ℕ with zero and suc as constructors03/03 12:47
skihm, i might be able to do something like that03/03 12:49
ski(i thought i had to have the eliminator "around" the return type, but maybe i don't actually)03/03 12:49
skii'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 equal03/03 12:50
skiso i was trying to eliminate the equality proof in the constructor type ..03/03 12:51
npouillardis this related to John Major equality?03/03 12:53
skiyes .. i'm trying out variants of it03/03 12:53
npouillardaka Relation.Binary.HeterogeneousEquality03/03 12:53
HairyDudehrm. seems importing Level causes unsolved constraints03/03 13:19
HairyDudehttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23205#a2320503/03 13:22
HairyDudealso, hiding zero and suc makes the yellow go away03/03 13:24
HairyDudeapparently agda allows them to be overloaded, so it can't tell they should be constructors of ℕ, despite the type signature03/03 13:26
dolioThat's odd.03/03 13:36
HairyDudein fact, it has no trouble with zero, only suc03/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.RingSolver04/03 04:10
Saizancopumpkin: hawt04/03 06:21
appamattoWow, are many people here going to the implementor's meeting this month?04/03 15:03
appamattoIt sounds like fun04/03 15:03
maltemAnyone 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 types04/03 19:00
dolioWhat about it?04/03 19:01
maltemUpon reading the symmetry proof, I wasn't sure anymore if I even got the definition of _≡_, type-wise04/03 19:02
maltemHow to understand that a proof is of type Set1, and what does (\z -> P z -> P x) mean?04/03 19:03
maltemMaybe the latter is the better question04/03 19:03
dolioSet1 is the level above Set.04/03 19:03
maltemThat's (more or less) clear to me.04/03 19:03
copumpkinSet-104/03 19:03
dolioIt's necessary because that definition of == quantifies over Set, essentially, because P : A -> Set.04/03 19:04
copumpkin(that's values)04/03 19:04
maltemIt's what non-logicians call Class.04/03 19:04
dolio(\z -> P z -> P x) takes a value of type A, called z, and returns the type P z -> P x04/03 19:04
maltemSo (P z -> P x) : Set ?04/03 19:05
dolioYes.04/03 19:05
dolioSince P : A -> Set04/03 19:06
dolioSo, 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
dolioWhich is what you need to reverse the equality.04/03 19:07
dolioy == x = (P : A -> Set) -> P y -> P x04/03 19:07
dolioIt'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
maltemI'm getting closer, let me ponder a little04/03 19:08
copumpkinis there a name for replacing "structures" with properties of those structures?04/03 19:11
copumpkinthis seems similar to representing a list by a fold04/03 19:11
copumpkinhere you're representing equality by subst04/03 19:11
maltemSo xy (\z -> P z -> P x) : (P x -> P x) -> (P y -> P x).04/03 19:16
maltemOk so it works out. I'm wondering why I find this to be so hard04/03 19:18
copumpkinit's not trivial :)04/03 19:18
maltemdolio, when you said "Yes. Since P : A -> Set" is that just a general typing rule?04/03 19:20
dolioYes. The type of (x : A) -> B[x] is computed as...04/03 19:21
maltemI mean, that (A -> A) : Set if A : Set04/03 19:21
dolioIf A : SetM, and B[x] : SetN, then (x : A) -> B[x] : Set(max M N)04/03 19:22
dolioAnd A -> B is a special case, where B doesn't depend on x.04/03 19:22
maltemIs B[x] meta-notation for a type that mentions x?04/03 19:22
maltemOr is it Agda syntax?04/03 19:23
dolioMeta-notation.04/03 19:23
dolioI 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
maltemOk, so your notation explicitly conveys that this is allowed to be a dependently typed function04/03 19:25
dolioThat was my intention.04/03 19:25
dolioB is some expression, in which x is in scope, that must have a type SetN for some N.04/03 19:25
maltemThanks 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
guerrillamaltem: 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%2904/03 20:45
guerrillaeven more detail in http://en.wikipedia.org/wiki/Leibniz%27s_law04/03 20:47
maltemguerrilla, heh, yeah notions of equality are interesting on their own04/03 20:47
guerrillaespecially in TT04/03 20:48
maltemTT?04/03 20:48
guerrillatype theory04/03 20:48
maltemof course :)04/03 20:48
maltemguerrilla, technically, yes.04/03 21:06
maltemAnother 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
maltemI would have expected A -> A -> Bool or somesuch.04/03 21:11
copumpkinSet is a type-level Bool :)04/03 21:12
ccasinmaltem: if it were A -> A -> Bool, the relation would have to be decidable04/03 21:12
copumpkinthe empty set is false04/03 21:12
copumpkinthe set with one item is true (as are any other sets, but one item carries no other information)04/03 21:12
guerrillawhy don't we use a specific type that can only be inhabited by \top (or True if you like)?04/03 21:13
guerrilla(say.. Prop)04/03 21:13
guerrillaseems like that would be clearer. but i assume that has other issues.. right?04/03 21:13
copumpkinguerrilla: we do?04/03 21:13
maltemccasin, why needn't it be decidable with this Set encoding?04/03 21:14
copumpkinData.Unit and Data.Empty contain our true and our false04/03 21:14
maltemI presume there's a way to check if a set is empty?04/03 21:15
copumpkinnot really, nope04/03 21:15
ccasinmaltem: 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 inhabited04/03 21:15
ccasin"The relation associates" rather04/03 21:15
guerrillacopumpkin: yeah, but i mean.. both \top and Nat inhabit Set (for example). why not have a type that is only inhabited by \top04/03 21:15
ccasinno, there isn't a way to check if a set is empty.  That's like asking if a theorem is provable04/03 21:16
ccasinnot decidable04/03 21:16
copumpkinmaltem: that's why Bool would show it's decidable04/03 21:16
maltemAh, I "forgot" that Set is not in any way a computable model of sets04/03 21:16
copumpkinif you can provide a true/false, that's a proof04/03 21:17
maltemThat makes sense now.04/03 21:17
copumpkinI meant it's a proof of Bool, which carries more information than a proof of \top04/03 21:18
maltemBut now I must ask myself guerrilla's question, too.04/03 21:19
copumpkinso a universe of true/false types?04/03 21:19
* copumpkin tries to think how that would work04/03 21:19
dolioProp in Coq is like that, sort of.04/03 21:20
guerrilladolio: yeah i thought so...04/03 21:20
dolioOr any theory with proof irrelevance.04/03 21:21
guerrillajust like Prop : Set1 and then \top : Prop (and allow nothing else in it)..04/03 21:21
maltemcopumpkin, 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
copumpkinI think agda used to even have a Prop04/03 21:21
copumpkinmaybe agda 1?04/03 21:21
guerrillacopumpkin: yeah, i did see that in old code, i think04/03 21:22
guerrillaso.. why is it gone?04/03 21:22
guerrilla:)04/03 21:22
dolioAgda 2 has Prop, too, but it isn't proof irrelevant. It's just like an extra Set.04/03 21:22
copumpkinah04/03 21:22
guerrillaok04/03 21:22
guerrillahmmf04/03 21:22
copumpkin:)04/03 21:22
maltemLet's see, if I define Rel : Set -> ?; Rel A = A -> A -> Prop   then what would ? be?04/03 21:22
copumpkinSet1?04/03 21:23
copumpkinRel A = A -> Set04/03 21:23
copumpkinoh04/03 21:23
copumpkinsorry :)04/03 21:23
maltemI mean, due to the "-> Prop" I suppose I would have to learn another typing rule04/03 21:24
guerrillamaltem: not really necc. since we have universes04/03 21:26
guerrillai think04/03 21:26
maltemah I missed that Prop : Set104/03 21:27
guerrillayeah04/03 21:27
maltemso indeed ? = Set104/03 21:27
guerrillaand 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
guerrillaSet : Set104/03 21:28
guerrillaand btw Set = Set004/03 21:28
guerrillaSet1 : Set204/03 21:28
guerrillaand so on04/03 21:28
guerrillaso that we don't have the paradox of having a set that contains all sets (Russel)04/03 21:29
guerrilla(among other issues?)04/03 21:29
maltemAh a very valuable tip, I wasn't even aware that there's a seperate lib04/03 21:31
guerrillayeah, 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
maltemAh ok, so the notations gets a little heavier04/03 21:33
guerrillasomeone 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 it04/03 21:33
guerrillamaltem: yeah, just more stuff to keep track of04/03 21:33
maltemWow how do you people read the unicodified sources? Do you keep adjusting your terminal font size? ;)04/03 21:33
guerrillamonospace?04/03 21:39
guerrillagnome-terminal and monospace for me anyway04/03 21:39
maltemyeah for me that means that either fancy symbols are too small, or ordinary letters are too large04/03 21:41
guerrillaodd04/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 secs05/03 12:47
guerrillais there a difference between symbol \forall and the keyword "forall" in Agda?05/03 13:54
npouillardguerrilla: AFAIK no05/03 13:55
guerrillahmm ok05/03 13:55
dolio\forall used to not be a keyword.05/03 14:53
dolioSame with \lambda.05/03 14:53
appamattoHas there been any news about the AIM meeting in Japan?05/03 15:06
MissPiggyepigra mtime05/03 21:10
MissPiggyepigram time05/03 21:10
MissPiggyI 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
roconnoron http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes it says at the bottom:05/03 22:35
roconnor  codata ∞ (T : Set) : Set where05/03 22:35
roconnor    ♯_ : T → ∞ T05/03 22:35
roconnorbut this isn't even a recursively defined type.05/03 22:35
roconnor ∞ appears to me to be just the identity type constructor05/03 22:35
roconnorthis can't be right05/03 22:35
glguyWhat were you trying to do?05/03 22:36
roconnorunderstand that wiki page05/03 22:36
glguyYou define your coinductive data types as normal data types with the co-inductive fields using ∞05/03 22:37
glguyso that you can have data-types that are inductive in some components and co-inductive in others..05/03 22:37
glguyI don't understand it all that well, myself, but I think I get the idea05/03 22:37
roconnor  inf : Coℕ05/03 22:38
roconnor  inf = suc (♯ inf)05/03 22:38
roconnorwhat makes this well defined?05/03 22:38
glguyYou can't case on the ♯, for one05/03 22:38
glguyso you can't do structural recursion on that05/03 22:38
roconnoroh05/03 22:38
roconnorthis is so bizarre (coming from the coq world)05/03 22:39
roconnor  ♭ : ∀ {T} → ∞ T → T05/03 22:39
roconnor  ♭ (♯ x) = x05/03 22:39
roconnorthat looks like case analysis to me05/03 22:39
roconnorit isn't *dependent* case analysis, but it is still case analysis05/03 22:40
* roconnor tries reading http://article.gmane.org/gmane.comp.lang.agda/63305/03 22:41
roconnorwhoa05/03 22:42
roconnorwhat the heck is ~ ?05/03 22:42
codolioIt doesn't exist anymore.05/03 22:42
glguy633 says "This type comes with a destructor, which is the only function which is05/03 22:42
glguyallowed to pattern match on ♯_:"05/03 22:42
codolioIt used to denote corecursive definitions.05/03 22:42
roconnorok05/03 22:43
codolioNow 'inf = suc (# inf)' is internally translated to something similar to an auxiliary corecursive definition, or something like that.05/03 22:43
roconnorbut I'm left wondering why inf is well defined05/03 22:43
roconnorcodolio: why is it translated to anything corecursive since the input and ouput types are data types?05/03 22:44
* roconnor keeps reading05/03 22:45
codolioBecause it involves a fixed point involving codata, I guess.05/03 22:45
roconnorI guess05/03 22:45
codolioI think the current situation is a bit odd with respect to the theory you'd expect to base it on.05/03 22:45
roconnorya05/03 22:46
codoliocodata 'infects' data in an unusual way.05/03 22:46
roconnorin 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
roconnorso I guess codata means something ... strange05/03 22:47
codolioWhich leads to NAD's stuff about (co)data being unable to represent mu-nu fixed points.05/03 22:48
roconnorbut nu-mu is okay?05/03 22:48
codolioIf you try to represent a mu-nu, it will end up as a nu-mu instead.05/03 22:49
roconnorwow05/03 22:50
roconnorwhat a mess05/03 22:50
roconnorbut that's okay05/03 22:50
roconnorthis is an open problem :D05/03 22:50
dolioAt least we don't lose subject reduction. :)05/03 22:50
roconnorya05/03 22:50
roconnorI'm no fan of coq's "solution"05/03 22:50
glguyroconnor, ok, you can case on sharp, but it doesn't count as structural recursion to the termination checker05/03 22:50
dolioI'm pretty sure that's just avoided by flatly disallowing dependent case analysis on coinductives.05/03 22:51
roconnordolio: what is avoided?05/03 22:51
dolioLoss of subject reduction.05/03 22:51
roconnorsure05/03 22:51
roconnorbut why then go on with this strange # ∞ stuff?05/03 22:52
roconnorCoinductive types are then defined using /data/, but with ∞ annotating05/03 22:52
roconnorcoinductive arguments (this was suggested by Thorsten Altenkirch):05/03 22:52
dolioIt allows for mixing coinduction and induction in a single data definition.05/03 22:52
roconnorugh05/03 22:52
roconnorThrosten, what did you say?05/03 22:53
dolioWhich is actually being used currently.05/03 22:53
roconnordolio: it doesn't allow for mixing with my understanding of the definition of ∞.05/03 22:53
dolioFor NAD's parser combinators, for instance.05/03 22:53
roconnorwhen I see ∞, I just see the identity functor.05/03 22:53
dolioWell, it isn't.05/03 22:53
roconnorhow do I properly read this definition?05/03 22:54
roconnorit is a "delayed" constructor?05/03 22:54
MissPiggyThorsten is there ??05/03 22:54
dolioYes, it's like that.05/03 22:54
roconnorthat's why inf is allowed05/03 22:56
dolio'data T : ... where con : ... -> ∞ T ... -> ...' allows you to use 'con' in a corecursive definition.05/03 22:56
dolioBasically, I think any definition guarded by codata constructors is allowed to be corecursive.05/03 22:57
dolioBy the productivity checker.05/03 22:57
roconnorwhat are the denotational semantics of Agda's codata?05/03 22:57
roconnorit boggles my mind how to define this delay thing05/03 22:57
dolioOr, it can be guarded by a combination of codata and data constructors, but the codata has to be in there.05/03 22:57
dolioroconnor: 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
dolioI think that's right.05/03 22:59
roconnor<codolio> If you try to represent a mu-nu, it will end up as a nu-mu instead.05/03 23:00
roconnorRight, Coℕ is defined like it is mu-nu but it really is nu-mu05/03 23:00
roconnornu on the nat, and mu on the identy functor ∞05/03 23:01
roconnorwow05/03 23:01
roconnorthis feels really wrong.05/03 23:01
dolio"The corresponding domain-theoretic expressions are μO. μZ. Z_⊥ + O and μZ. μO. Z_⊥ + O, and these are equivalent."05/03 23:02
roconnorI'd like to see those semantics worked out05/03 23:02
dolioWhen discussing trying to do μO.νZ.Z + O using agda's codata.05/03 23:02
roconnorwhat about simple νZ.Z+1 ?05/03 23:04
roconnorso you are saying Nat is defined as μZ. Z_⊥ + 1 ?05/03 23:04
roconnorer05/03 23:04
roconnorCoNAt05/03 23:04
dolioYes.05/03 23:05
roconnorwhat is + in domain theory05/03 23:06
dolioHe's saying that adding ∞ is the same as adding _⊥.05/03 23:06
roconnorthe domains A and B with a new bottom glued on, or with the two bottoms merged?05/03 23:06
dolioI don't really know.05/03 23:07
roconnorwhere is your quote from?05/03 23:09
dolio'Some observations about μν' on the mailing list.05/03 23:10
roconnorlink?05/03 23:10
dolioIs the list archive still not public? It's asking me to log in.05/03 23:11
roconnorfound it05/03 23:12
roconnorhttp://thread.gmane.org/gmane.comp.lang.agda/95205/03 23:12
dolioIt's from last July.05/03 23:12
dolioI have to jet, but I'll leave with a query...05/03 23:14
roconnorwhat query?05/03 23:15
dolioIt'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
dolioIs there a similar example for parametric, universal types vs. pi types?05/03 23:16
roconnorexistential means non-dependent elimination?05/03 23:16
dolioYes. I think weak elimination is the key to the abstraction property.05/03 23:17
dolioI suppose there's no 'strong' pi eliminator.05/03 23:17
roconnorBTW you lose all the information hiding guarentees of existential types if your language also has sigma types05/03 23:17
roconnorbasically you can tuck in info way in a sigma type and return it.05/03 23:17
dolioRight. Luo mentions that, I think.05/03 23:18
--- Day changed Sat Mar 06 2010
RLain agda you can make recursion step only by single argument?06/03 11:09
Saizanno, if i understand correctly06/03 11:10
Saizanin the sense that you don't need to recurse on a single argument at a time06/03 11:10
RLai have some nat theory here06/03 11:13
RLaand i want to specify associativity of + here06/03 11:14
RLahm, nvm06/03 11:14
RLait looks like complete abuse of types06/03 11:16
Saizanyou'd have associativity as a separate property06/03 11:20
Saizan\all x y z -> (x + y) + z \== x + (y + z)06/03 11:20
Saizanit's fairly simple to prove by induction over x, iirc06/03 11:21
RLahm, i need induction over other variables too?06/03 11:22
RLasince i do not have yet 0+y = y?06/03 11:22
Saizanah, well, i'd prove that as a lemma06/03 11:22
Saizanhowever you could recurse over y too, if that was needed06/03 11:23
RLayeah, i currently recurse over all of them06/03 11:23
RLai'm now working on commutativity06/03 11:24
RLawhy would this give the error: http://pastebin.com/acTffsTi06/03 11:39
Saizanwell because the types don't match..06/03 12:32
Saizancomm+ y y' : y + y' = y' + y06/03 12:33
Saizanbut you've to provide something of type s y + y' ≡ y' + s y06/03 12:33
RLahm, i have nothing of that type06/03 12:38
RLaor do i have to provide something that chops s off from both sides?06/03 12:39
Saizanwell, from  y + y' = y' + y you can derive s (y + y') = s (y' + y) easily06/03 12:40
Saizanthen you've to prove that s (y' + y) = y' + s y06/03 12:40
RLahm06/03 12:44
RLai have no idea how to do that06/03 12:45
RLaor how to express it in agda06/03 12:45
Saizanwell, you can just have an helper function \all x y -> s (x + y) \== x + s y06/03 12:46
Saizanand for the other part you can write another: (A B : Set) -> (f : A -> B) -> {x y : A} -> x \== y -> f x \== f y06/03 12:48
Saizanthat's usually called cong06/03 12:48
RLawell, i have something called cong here, i'm writing def to it at the moment06/03 12:49
MissPiggyi RLa!06/03 12:57
MissPiggyhi06/03 12:57
RLahey06/03 12:57
RLano, it's not going to work06/03 13:04
RLai'm even unable to write definition for \all x y -> s (x + y) \== x + s y06/03 13:07
MissPiggyyou must prove x + 0 = 0 + x by induction on x06/03 13:11
MissPiggydoing this sort of stuff in agda is very long and difficult06/03 13:11
RLayes, i already know that06/03 13:12
RLaanyway, i think i got helper function: http://pastebin.com/7MuVGvpz06/03 13:13
RLabut i see no way how it would help me06/03 13:14
MissPiggyare you trying to prove x + y = y + x?06/03 13:15
MissPiggyon natural numbers06/03 13:15
RLayes06/03 13:21
RLai have problem with case comm+ (s y) (s y')06/03 13:24
MissPiggyI 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 x06/03 13:27
MissPiggy(*if A reduces to B then a proof of A is a proof of B)06/03 13:27
Saizanyou've redundant cases in your commHelp btw06/03 13:27
RLahm06/03 13:29
MissPiggyrewriting 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 y06/03 13:33
MissPiggy(the S case gives you something like S (S (y + x)) = S (y + S x), which you use the induction hypothesis to rewrite the right hand side into S (S (y + x)))06/03 13:34
RLai do not get which cases are reduntant in my commHelp06/03 13:34
RLaS x + y = y + S x but the second one reduces to S (x + y) = y + S x <- what does mean?06/03 13:35
MissPiggyS x + y = y + S x06/03 13:36
MissPiggyreduces to06/03 13:36
MissPiggyS (x + y) = y + S x06/03 13:36
MissPiggybecause of the definition of +06/03 13:36
RLahm, i see06/03 13:36
MissPiggyso 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
MissPiggyanother example of this is, 1 + 1 reduces to 2 .. obviously!06/03 13:37
MissPiggyso you can prove 1 + 1 = 2 by proving 2 = 206/03 13:37
MissPiggyso it's just reflexivity06/03 13:37
MissPiggythat might seem like a boring example, but you can take this technique and turn it into something really powerful06/03 13:37
RLacan i use numbers instead of (s y) stuff?06/03 13:38
MissPiggywell you could write  1+  instead of  S06/03 13:38
MissPiggyit's all the same though06/03 13:38
RLaok, 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
MissPiggylike 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 proved06/03 13:45
RLaok, this is my case for 0 + y = y + 0: comm+ z y = comm+' y, where comm+' is ∀ n → 0 + n ≡ n + 006/03 13:47
RLabut 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
RLai'm missing something important here06/03 13:48
Saizanwell, you have to recurse06/03 13:48
Saizando you have transitivity?06/03 13:49
MissPiggycomm+ : forall x y, x + y = y + x ? I assume06/03 13:49
RLayes06/03 13:49
MissPiggythen  comm+ (s y) y' : (s x) + y' = y' + (s x)06/03 13:49
MissPiggyand   comm+ (s y) y' : s (x + y') = y' + (s x)06/03 13:49
RLaSaizan, no, transitivity went wrong and i do not have code for that06/03 13:49
MissPiggythe induction hypothesis gives you x + y' = y' + x thought,06/03 13:49
MissPiggyso you can whack the lemma (s (y' + x) = y' + (s x)) with the induction hypothesis to conclude the comm+ (s y) y' case06/03 13:50
MissPiggyinduction gives you x + y' = y' + x06/03 13:51
SaizanRLa: transitivity should just be a matter of pattern matching on the arguments and using triv06/03 13:52
RLaSaizan, apparently it's not, agda wants to put some lambdas in my definitions and i have no idea what to do with them06/03 13:53
Saizantrans : {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
Saizanoops06/03 13:54
Saizantrans : {A : Set} {x y z : A} -> x \== y -> y \== z -> x \== z06/03 13:54
MissPiggySaizan, \== meaning not equal?06/03 13:55
MissPiggyoh....06/03 13:55
MissPiggythis is quail notation for the unicode equals sign06/03 13:55
MissPiggyim usedto \== for not equal form porolog06/03 13:55
Saizanyeah, i'm not sure why i use the latex notation here on irc :)06/03 13:55
Saizans/latex/what the agda-mode accepts/06/03 13:56
RLathen  comm+ (s y) y' : (s x) + y' = y' + (s x) <- is that actual syntax?06/03 13:58
RLashouldn't i use helper function here somehow?06/03 13:59
RLaalso, what is difference between function signatures trans : {A : Set} (x y z : A ) -> ... and \forall x y z -> ...?06/03 14:02
Saizancomm+ (s y) y' = trans (cong s (comm+ y y')) (commHelp y' y) -- should be06/03 14:02
SaizanRLa: that the latter is not polymorphic on the type of those x y z, but it's not specifying a type either06/03 14:03
Saizanunless your \== is defined only on naturals06/03 14:03
RLai have all functions using \forall06/03 14:04
RLayes, it's only on nat06/03 14:04
Saizanhow is it defined?06/03 14:04
Saizanhowever, \forall a b c -> .. is the same as (a b c : _) -> ...06/03 14:05
Saizani.e. you're asking the typechecker to infer the type06/03 14:05
RLahttp://pastebin.com/zDdGS56g06/03 14:05
RLahm, i did not know that06/03 14:05
Saizanooh06/03 14:05
RLathose definitions look ok?06/03 14:06
Saizanwell, that \== is not what i expected06/03 14:06
RLahm, i see, i already looked at many agda examples and they all do things differently06/03 14:07
Saizannow i see why your commHelp definition works06/03 14:07
Saizan(i was puzzled before :)06/03 14:07
Saizani guess you've to define transitivity by pattern matching on the x y z then06/03 14:08
RLayes, that's where trouble came in06/03 14:08
RLait seems to want some extra data06/03 14:08
Saizanwell, trans would have 5 arguments06/03 14:09
RLabut where those extra 2 come from?06/03 14:09
RLaor what gives value for them06/03 14:10
Saizan"x \== y" and "y \== z" count as arguments06/03 14:10
RLabut what evaluates them?06/03 14:12
RLaor should i completely ignore them?06/03 14:12
RLaand use results of pattern matching?06/03 14:12
Saizanah, btw, \forall a b c -> ... is actually (a : _) (b : _) (c : _) -> .., i.e. they can be of different types06/03 14:12
Saizanwell, you can ignore them when those equalities will reduce to True, since pattern matching on triv doesn't give any useful information06/03 14:13
Saizanwhen the equality reduces to False instead you should use an absurd pattern for them06/03 14:14
Saizanso that you can avoid writing a body for that that branch06/03 14:14
Saizane.g. "trans z (s _) _ () _" <- this means "if x = z and y = s _; then you can't tell me x \== y", roughly06/03 14:15
RLahm, it does not let me use those extra arguments in pattern matching at all06/03 14:16
RLae.g requires me to return a function06/03 14:17
Saizanyou can't pattern match on them until you pattern match enough of the nat arguments to make their type reduce to either True or False06/03 14:17
Saizanthat's odd.06/03 14:17
Saizancan you paste?06/03 14:17
Saizanoh, duh, we can't use z as a variable name.06/03 14:19
RLaok, for example: trans≡ z z z = λ triv triv → triv06/03 14:20
RLathis seems fine case06/03 14:20
Saizanyeah06/03 14:22
Saizanbut you should also be able to write trans\== z z z triv triv = triv, if you also write all other cases with 5 arguments06/03 14:22
Saizanhttp://pastebin.com/7XL3SC5X <- eg06/03 14:23
appamattoHave there been any applications written in Agda?06/03 14:24
RLaduh, i tried to write triv as pattern06/03 14:26
RLatherefore it did not work06/03 14:26
MissPiggydid you get +comm done yet?06/03 14:27
RLano, i'm working on trans06/03 14:28
RLa() as a pattern means that such case should be never possible?06/03 14:29
Saizanyeah06/03 14:29
MissPiggywhat's trans got to do with this?06/03 14:32
MissPiggyhere is this proof in coq http://pastie.org/85713206/03 14:32
Saizanwell, don't you need trans to chain the inductive hypothesis and s (y' + x) = y' + (s x) ?06/03 14:33
Saizanit's how i'd write it, anyway06/03 14:33
MissPiggySaizan, it's actally S (S (y' + x)) = S (y' + (S x)) isn't it? So you have to rewrite06/03 14:34
MissPiggyno you are right, transitivity works too06/03 14:34
RLai'm defining cong now06/03 14:41
RLatrying to do same way as trans06/03 14:41
Saizancong is actually not needed here06/03 14:42
Saizansince "s x \== s y" reduces to "x \== y" with your definition06/03 14:43
RLa"reduces to" <- how is reduction defined here?06/03 14:44
Saizanwell, as the normal evaluation rules, given the definition of \==06/03 14:46
Saizansince you've defined "s m ≡ s n  = m ≡ n"06/03 14:47
RLahere is my cong: http://pastebin.com/5qB98ceF06/03 14:57
RLai now go back to comm06/03 14:58
Saizannice :)06/03 14:58
Saizanyou won't need that cong here06/03 14:58
appamattoWhat ghc are you guys using?  I am compiling with 6.10.4, and I'm having problems with dependency conflicts06/03 15:19
Saizani'm on ghc-6.1206/03 15:19
appamattoI think I'll upgrade06/03 15:21
RLai'm still working on commutativity06/03 16:26
RLawhat does conc stand for?06/03 16:26
Saizanconc?06/03 16:28
RLacong*06/03 16:34
Saizannot sure actually06/03 16:35
RLai think that my definition of cong is not usable06/03 16:36
Saizanyou don't need it for commutativity, anyhow06/03 16:36
Saizanhttp://pastebin.com/pXs2S2sS06/03 16:36
RLahm, move-s is same as my commHelper06/03 16:39
Saizanyeah06/03 16:40
RLahm, if program compiles, it must be correct?06/03 16:42
RLait compiles, but i still do not understand that trick with using trans06/03 16:42
Saizanwell, it's not like you can run comm+ to get something computationally interesting :)06/03 16:42
Saizanah, well06/03 16:43
RLahehe :D06/03 16:43
RLaso primitive proofs in simple arithmetics should be not so complex06/03 16:44
Saizanyou'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
Saizanthen you use move-s to tell that s (y + x) == y + s x06/03 16:45
Saizancombining with transitivity you get s x + y = y + s x, which is what you wanted to prove06/03 16:46
Saizanyou can automate proof strategies by reflection, like in the RingSolver module06/03 16:46
RLai will look into that06/03 16:47
RLai think i have problem that i do not understand how agda prove procedure works06/03 16:48
RLaanyway, big thanks for help06/03 16:50
Saizannp06/03 16:51
Saizanthe first thing is that equality over terms is basically defined by evaluation06/03 16:52
MissPiggy"if program compiles, it must be correct?" -- no :P06/03 16:53
MissPiggyyou just know that it satisfies its type06/03 16:53
MissPiggybut you can sometimes express correctness in the type, or prove it afterwards06/03 16:53
RLais evaluation in agda like beta-reduction in lambda calculus?06/03 16:54
Saizanthough it's evaluation in an open context, so it gets stuck on free variables, pattern matching makes it go further06/03 16:54
Saizanyeah06/03 16:54
RLaare there normal forms etc. too?06/03 16:56
Saizanyeah06/03 16:56
Saizanthe difference with a pure lambda calculus is the addition of constructors06/03 16:57
MissPiggyit's beta-reduction + eta-exapansion + unfolding definitions (+ more stuff?)06/03 17:00
MissPiggyoh yeah pattern matching06/03 17:01
RLawhat about recursion? does it restrict construction of fixpoint combinators somehow?06/03 17:02
Saizanyes, there's a termination checker06/03 17:03
MissPiggyI hujst cannot figure out how to use pig from the test files :06/03 17:06
RLapig?06/03 17:07
--- Day changed Sun Mar 07 2010
lpjhjdhso I have a datatype with only a single constructor and I can't seem to match on it07/03 01:17
liyangPaste?07/03 01:22
liyangOffer closing in 2 minutes. :p07/03 01:23
lpjhjdhooh, sorry, must run07/03 01:23
lpjhjdhthanks though07/03 01:23
liyangLikewise. :307/03 01:23
Saizani 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 to07/03 07:52
Saizanthe 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 annotations07/03 07:57
RLasome of us here use scala for writing wicket apps?07/03 11:33
RLawrong channel07/03 11:33
RLais there a part of agda manual that explains the use of () in pattern matching?07/03 12:38
Saizanmh, maybe in some of the tutorials07/03 12:42
Saizanotherwise you've to look at the papers :)07/03 12:43
Saizanor ask here what's unclear07/03 12:43
maltemI find it fun how you can abuse the agda module system in order not to repeat variable names :)07/03 16:33
npouillardmaltem: still to much to repeat according my taste but...07/03 16:34
npouillard*too07/03 16:36
maltemnpouillard, 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 scary07/03 16:37
Saizanwell, you can get open ... public to export a flat namespace if you want07/03 16:41
maltemwhat does "public" do?07/03 16:45
Saizanit makes the current module re-export the symbols of the opened moduel07/03 16:57
Saizanit's used a lot in the Algebra records, to give you a "subtyping" feel07/03 16:58
maltemmmh ok so I when then using the module I could drop the module qualifiers, and just have long types07/03 16:59
Saizanright, which is probably not that nice07/03 17:07
Saizanbut you could also make a module that takes all the parameters at once and exports everything07/03 17:08
maltemright07/03 17:09
jotik^^There is no way to instanciate an element of type "data False : Set where" is there?07/03 18:34
npouillardjotik^^: what do you mean by instanciate here?07/03 18:35
npouillardbut yes there is no value of type False07/03 18:35
npouillardotherwise we have a problem07/03 18:35
jotik^^So I can't make any function return anything of type False, correct?07/03 18:36
jotik^^A problem?07/03 18:36
jotik^^nevermind last line.07/03 18:36
npouillardjotik^^: you can return a value of type false if you get one as argument07/03 18:36
npouillardor if you get some arguments that forms a contradiction and so have all types07/03 18:37
jotik^^I'm trying to prove "trans≡ : ∀ m n o → m ≡ n → n ≡ o → m ≡ o" on natural numbers where _≡_ : Nat -> Nat -> Set (either True or False)07/03 18:43
npouillardjotik^^: Set is not just true or false07/03 18:44
jotik^^And I just don't know what to do with the case trans≡ (suc a) zero (suc c)07/03 18:44
npouillardtrans≡ _ _ _ refl refl = refl07/03 18:44
jotik^^hmm...07/03 18:45
jotik^^What is that supposed to mean (/me agda noob)07/03 18:46
npouillardif you want to write it the long way as an exercise you will need the () pattern07/03 18:46
npouillardequality is complicated beast07/03 18:47
jotik^^well the shorter the better, but since this is a course assignment I'm not allowed to change any data types nor _≡_07/03 18:48
jotik^^And I don't understand what you meant by trans≡ _ _ _ refl refl = refl07/03 18:49
npouillardbut basically pattern matching on refl forces the substitution of n for m and of o for n07/03 18:50
jotik^^but I can't pattern match like that, can I?07/03 18:55
npouillardyes you can07/03 19:02
npouillardjotik^^: however I've not seen the definiton of _≡_ you use07/03 19:02
jotik^^npouillard: Well here's what I've got: http://agda.pastebin.com/7s3d7qkL07/03 19:04
npouillardjotik^^: ok so you have a different version of _≡_ than the propositional one07/03 19:06
jotik^^What would a propositional one look like?07/03 19:07
jotik^^like a type?07/03 19:07
npouillarddata _≡_ (A : Set) : Set → Set where refl : A ≡ A07/03 19:07
npouillardyes07/03 19:08
npouillardbut you to continue in your direction you will need a function to eliminate False values07/03 19:08
jotik^^Wow I think I already managed with one, by declaring an absurd pattern and using () ()07/03 19:10
npouillardelim-False : ∀ {A} → False → A07/03 19:11
npouillardelim-False ()07/03 19:11
jotik^^hmm07/03 19:12
npouillardjotik^^: Was the definition of _≡_ fixed in the assignment07/03 19:14
jotik^^If I declare such a function, I get "Sort _55  [ at filename..." What does that mean?07/03 19:14
jotik^^npouillard: yes07/03 19:15
npouillardhum ∀ {A : Set} ...07/03 19:15
jotik^^thanks07/03 19:22
jotik^^btw, what do those _somenumber messages mean?07/03 20:55
jotik^^e.g. _59, _60, _61 etc07/03 20:55
Saizanjotik^^: they are meta variables introduced by the typechecker for unknowns which couldn't be resolved to something else07/03 22:07
Saizanjotik^^: a lot like prolog, if you're familiar with it07/03 22:08
jotik^^not much07/03 22:08
jotik^^bed time for me. Thanks everybody! Good night!07/03 22:09
--- Day changed Mon Mar 08 2010
MissPiggyso they proved tt = ff in epigram??08/03 00:13
TacticalGraceIs the Agda "standard library" include in an install from Hackage (via cabal-install)?08/03 05:06
copumpkinnope08/03 06:47
copumpkinnot as far as I know08/03 06:47
copumpkinwe need an agda platform :P08/03 06:47
jotik^^I've never succeeded installing anything properly with cabal, including Agda, so I'm keeping as far as possible from cabal.08/03 07:42
Saizanfor Agda it always worked at the first attempt for me08/03 07:44
jotik^^Didn't work for me, tried multi. Then I tried many times in an emulator under Ubuntu and even succeeded to run it for some time until updating something broke it.08/03 07:57
jotik^^Finally I had to beg gentoo devs for ebuilds which were a work-in-progress.08/03 07:57
Saizanah, i avoid distro packages like the plague, for haskell08/03 08:05
jotik^^Since haskell developers avoid them as well, distro packages are bad.08/03 08:50
jotik^^Haskell packagers are doing a lousy job, the latest stable ghc in gentoo is 6.8.208/03 08:51
jotik^^And the usual answers to all questions are "Why don't you use the haskell overlay and ~testing" and "Why don't you use cabal?"08/03 08:52
Saizanso you call judgemental equality the one that appears in your typing rules?08/03 20:09
dolioYes. Because it's used in typing judgments.08/03 20:24
Saizani'm not sure i get why you'd need the different formulations of zero to be judgementally equal rather than just propositionally08/03 20:27
Saizanit'd make some proofs impossible?08/03 20:27
dolioI'm not really sure.08/03 20:27
dolioIt makes more work, at least.08/03 20:28
dolioFor 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
dolioOr use a non-canonical empty vector.08/03 20:29
dolioI'm not sure if there's more to it than that.08/03 20:30
Saizanoh, 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
dolioThe "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
Saizani thought that was dispensed earlier by saying that epic(?) erases coercions08/03 20:48
dolioCoercions 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
Saizanyeah08/03 20:49
Saizanso 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 it08/03 20:52
dolioI guess.08/03 21:00
--- Day changed Wed Mar 10 2010
copumpkinis the RingSolver actually being constructive and finding "solutions" or is it just manipulating the equation to show equality?10/03 07:52
copumpkinit kind of looks like the latter but it may be more subtle10/03 07:53
copumpkinthe Reflection module gives me both a prove and a solve based on it10/03 07:55
copumpkinbut I can't figure out how the solve function is working10/03 07:55
Saizani think the variables are meant as universally quantified10/03 08:13
guerrillaso, this is pretty intense: http://arxiv.org/abs/1002.443310/03 12:30
guerrillathe "Good Math, Bad Math" blog attacks it informally here: http://scienceblogs.com/goodmath/2010/03/grandiose_crankery_cantor_gode.php10/03 12:30
liyangcopumpkin: reversing the steps of the manipulation starting from refl yields a constructive solution, if you will.10/03 12:42
liyangcopumpkin: where by manipulation I mean transformation to some normal form.10/03 12:43
copumpkinliyang: thanks :)10/03 20:26
copumpkinas 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
copumpkinhmm, trying to convince it to use a proof of mine during pattern matching :/11/03 08:28
copumpkinI guess I'd really need a subst during pattern matching11/03 08:29
copumpkinwhich seems rather hard to convince it to do11/03 08:29
copumpkinyay, I just wrote deinterleave : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n11/03 08:51
copumpkinway harder than it should be11/03 08:51
dolioHow does 2 * n compute? 2 * n ==> n + n?11/03 08:57
copumpkinn + (n + 0)11/03 08:58
copumpkin(sadly)11/03 08:58
dolioWell, there's your problem.11/03 08:58
copumpkinyep11/03 08:58
copumpkinthat was kind of my point though11/03 08:58
copumpkinnot 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 unification11/03 08:59
dolioYou're trying to do ring solver in GHC?11/03 09:00
dolioGood luck with that.11/03 09:00
copumpkinwell, not as part of GHC, just as a separate mini language with its own parser, etc.11/03 09:00
copumpkinthat emits haskell11/03 09:00
dolioOh, okay.11/03 09:00
dolioThat's slightly more sane.11/03 09:01
copumpkin:P11/03 09:01
copumpkinjust as an experiment to see if I can provide a nice interface to vector that provides static guarantees without making programmers go insane11/03 09:01
copumpkin(and I'd like it to spit out to agda too, just so you don't have to trust me too much)11/03 09:02
copumpkinof 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 haskell11/03 09:03
dolioJoe 6-monads.11/03 09:07
copumpkinlol11/03 09:07
copumpkingotta love things like suc (n + (n + 0)) != n + suc (n + 0) of type ℕ11/03 09:13
dolioThat's the price you pay for decidable typing.11/03 09:15
copumpkinyep11/03 09:15
dolioI wonder how much better stuff like NuPRL actually does at that.11/03 09:16
dolioCan it figure out that those two things are equal?11/03 09:16
copumpkinhaven't tried it11/03 09:16
copumpkincan't seem to fetch it either11/03 09:18
copumpkinahem: "Build proof assistants that are as indispensible to programmers and mathematicians as word processors are now."11/03 09:20
dolioWas that supposed to be serious?11/03 09:21
copumpkinlooks like it: http://www.cs.cornell.edu/Info/Projects/NuPRL/Intro/intro.html11/03 09:21
kmcit's a nice idea, but the lead time on ideas from programming language theory getting into industry seems to be about 50-70 years11/03 09:32
copumpkinwell part of the goal of my project to make (a tiny subset) this stuff more accessible to the masses and to attract more interest :P11/03 09:35
copumpkinif I can get a few more people interested in agda I'll feel satisfied11/03 09:35
copumpkinI just wrote another deinterleave₂ : ∀ {n} {a : Set} → Vec a (2 * n) → Vec a n × Vec a n11/03 09:35
copumpkinimplemented in a different (less efficient) manner11/03 09:35
copumpkinpretty exciting stuff11/03 09:36
Saizanall using RingSolver?11/03 09:37
copumpkinyep11/03 09:37
Saizanhow does it look?11/03 09:37
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23891#a2389111/03 09:37
copumpkinthe ringsolver for the second one was pretty trivial11/03 09:38
copumpkinbut as long as it can do it, I'm happy :)11/03 09:38
Saizannice11/03 09:44
Saizanwell, it could be nicer..11/03 09:44
copumpkinyeah :P11/03 09:44
copumpkinmy proofs are always butt-ugly11/03 09:44
copumpkinbut those are the two "obvious" ways of writing deinterleave11/03 09:45
copumpkinthat I could think of anyway11/03 09:45
Saizanoh, i meant because of the obvious limitations of agda, no idea if you can write it better11/03 09:46
copumpkinI'd like my tool to support writing both of those with as little code noise as possible11/03 09:46
copumpkinpairs (x:y:zs) = (x,y) : pairs zs :P11/03 09:46
copumpkinlike in mmorrow's original version11/03 09:46
copumpkinI was particularly frustrated with writing that function in agda11/03 09:47
copumpkinI could've probably used the solver to rewrite it immediately to a suc (suc ...) form11/03 09:47
copumpkinI'm pretty impressed with how general solve is11/03 09:53
copumpkinbut the type in the source file is effectively useful11/03 09:53
copumpkinuseless, even11/03 09:53
Saizann-ary functions seem to have that property..11/03 09:55
copumpkinyeah11/03 09:55
dolioIsn't the obvious solution to cast to a Vec a (n * 2), and then deinterleave that?11/03 09:57
copumpkinlet me try that :)11/03 09:59
copumpkinit typechecks but doesn't termination check11/03 10:02
copumpkinthe most obvious thing, anyway11/03 10:02
copumpkinoh11/03 10:02
copumpkinI'm doing it wrong11/03 10:02
copumpkinthere, it worked :)11/03 10:02
copumpkinhttp://snapplr.com/mf6q11/03 10:03
copumpkinobvious in retrospect :P11/03 10:03
copumpkinbut anyway, my point is still that Joe 6-Monads doesn't and shouldn't have to care about which parameter _*_ is recursing on11/03 10:05
copumpkinand obviously I'm still pretty close to him if I didn't think of that simple solution :)11/03 10:06
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23898#a23898 <- cute, but pretty CPU intensive to typecheck11/03 10:07
* copumpkin still has never used rewrite11/03 10:07
Saizanoh, i thought you wanted to use 2 * n to intentionally complicate things11/03 10:08
copumpkinno, I'm just stupid :)11/03 10:08
copumpkinbut yes, I'll claim it was for that reason too11/03 10:08
Saizanrewrite is just a shorthand for the usual with dance11/03 10:09
copumpkinI see :)11/03 10:09
liyangRewrite isn't quite as general as the usual with p … | refl = ? dance…11/03 21:37
liyangRewrite is literally that—a rewrite of the LHS of == with the RHS, while matching on refl may reveal more information.11/03 22:15
Saizanyeah, though i've found my use cases were covered quite nicely by rewrite11/03 22:16
--- Day changed Fri Mar 12 2010
* Mathnerd314 sees #agda12/03 03:49
copumpkin:)12/03 03:49
Mathnerd314seems pretty quiet compared to #haskell12/03 03:49
copumpkinyeah :P12/03 03:49
* Mathnerd314 runs away to take his first shower in weeks12/03 03:50
Mathnerd314so, how do I write functions in agda?12/03 04:05
copumpkinsame way as haskell :)12/03 04:06
copumpkinbut you don't have type inference in most cases12/03 04:06
copumpkinopen import Data.Nat; f : \bn \r \bn; f x = x + 112/03 04:07
copumpkintada12/03 04:07
copumpkinyou'll need a module X where at the top12/03 04:07
copumpkinthen do C-c C-l (as in liposuction)12/03 04:07
copumpkinand it should turn colorful12/03 04:07
copumpkinthat \bn types a blackboard N for naturals by the way12/03 04:10
copumpkin\r is a pretty ->12/03 04:10
copumpkinbut -> works too12/03 04:10
Mathnerd314do I need semicolons?12/03 04:11
Mathnerd314O12/03 04:11
Mathnerd314I'm getting a "missing body" error :-/12/03 04:11
copumpkinnope, I just wanted to separate lines12/03 04:12
Mathnerd314is there an agda pastebin?12/03 04:13
copumpkinnot really, we just use hpaste12/03 04:13
Mathnerd314maybe you should paste what you mean then.12/03 04:14
Mathnerd314agda needs better error messages ;-)12/03 04:14
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23916#a2391612/03 04:16
Mathnerd314it seems to eat up all my CPU when I try to compile :-(12/03 04:18
copumpkinit's typechecking the standard library dependencies12/03 04:18
copumpkinfrom Data.Nat12/03 04:18
copumpkinit will be a lot quicker once it's done that12/03 04:18
Mathnerd314where does it store those typechecks?12/03 04:19
copumpkinin .agdai files of the same name12/03 04:19
copumpkinlike .hi files in haskell12/03 04:19
Mathnerd314so if I delete .agdai files... my CPU burns up next compile?12/03 04:20
copumpkinwell, if you delete all the .agdai files in your standard library and then need the modules whose agdai files you deleted12/03 04:20
copumpkinthen it'll have to recheck them12/03 04:20
copumpkinyour own modules are unlikely to be as complex as the standard library's ones12/03 04:21
copumpkinso deleting your own .agdai files won't be too painful12/03 04:21
* Mathnerd314 sees12/03 04:21
Mathnerd314seems you don't want to install agda as root, then.12/03 04:22
Mathnerd314anyway... I want Control.Monad and Data.List for my program, right?12/03 04:24
copumpkinwell12/03 04:24
copumpkinyou might want to define them yourself and talk about the monad actions on their own12/03 04:25
copumpkinagda doesn't have typeclasses :)12/03 04:25
copumpkinand you'd need a Data.Colist12/03 04:25
copumpkinit might not be a good place to start though12/03 04:25
copumpkinI'd start with trying to define some simple functions and proving things about them12/03 04:27
* Mathnerd314_ hates sudden unexpected reboots12/03 04:28
copumpkinaw12/03 04:28
copumpkinhttp://snapplr.com/tacb12/03 04:29
copumpkinthere is a Category.Monad and a Data.List12/03 04:29
copumpkinbut Data.List is only finite lists12/03 04:30
Mathnerd314that IRC client looks cool12/03 04:31
Mathnerd314_ok, Agda is definitely rebooting my system every 10 seconds or so12/03 04:36
Mathnerd314:-/12/03 04:36
copumpkinwow12/03 04:36
Mathnerd314this is why I want to switch to linux or some other *sane* OS12/03 04:37
Mathnerd314it's probably not me, but that all-in-one installer12/03 04:37
Mathnerd314so, how do I install the standard library from inside Haskell?12/03 04:38
copumpkinyou just need to put it in a directory and configure your agda to go looking for it there12/03 04:39
copumpkinI'd find it quite disconcerting that a userland program could consistently crash my entire OS12/03 04:39
copumpkineven if it's the all-in-one installer's "fault"12/03 04:39
Mathnerd314I use --include-dir?12/03 04:42
Mathnerd314*--include-path=DIR12/03 04:42
copumpkinyou typically don't want to be calling agda from a command-line12/03 04:42
copumpkinbut yes, I think so12/03 04:42
Mathnerd314why is it bad to call from a command line?12/03 04:43
copumpkinwell, for most proofs, you'll want all the help you can get12/03 04:43
copumpkinfrom an interactive UI like emacs12/03 04:43
copumpkinyou can put holes in your proofs and it can tell you want it needs there12/03 04:43
copumpkinand what you have in scope and so on12/03 04:43
Mathnerd314huh.12/03 04:47
Mathnerd314so why doesn't Data.List handle infinite lists?12/03 04:48
copumpkinit needs the equivalent of laziness in haskell to handle them12/03 04:49
Mathnerd314so something like a thunk.12/03 04:50
copumpkinyeah, sort of12/03 04:50
copumpkinthat kind of thing is handled formally by talking about data vs. codata12/03 04:50
copumpkindata is inductively defined12/03 04:50
copumpkinand codata is coinductively defined :)12/03 04:51
copumpkinwhich means, roughly, that with data you have constructors and codata you have destructors12/03 04:51
* Mathnerd314 has no idea of what you're saying12/03 04:51
Mathnerd314that makes even less sense... :-)12/03 04:51
copumpkinwell12/03 04:51
copumpkinhmm12/03 04:52
copumpkinwith 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 want12/03 04:53
Mathnerd314ok.12/03 04:53
copumpkinwith codata, you just have "observers" on some value that exists12/03 04:53
Mathnerd314so you have properties of that value?12/03 04:54
Mathnerd314like "this value acts like 0 on this set"12/03 04:54
copumpkinsort of12/03 04:54
copumpkinfrom 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 differently12/03 04:55
copumpkinspecifically, it won't try to figure out whether your coinductive type is finite12/03 04:56
copumpkinwhereas it needs a "base case" for an inductive type12/03 04:56
Mathnerd314but I have a base case - an empty list... right?12/03 04:57
copumpkinyes, and you have an observer that tells you whether you have it or not12/03 04:57
Mathnerd314ok then.12/03 04:57
copumpkinbut agda won't try to ensure that there's one of those at some depth in the colist12/03 04:58
copumpkinin haskell, all "data" is actually codata12/03 04:58
Mathnerd314so why does agda have data?12/03 04:58
copumpkinbut in agda you need to be more explicit about getting that kind of lazy behavior12/03 04:58
copumpkinbecause data is a lot cleaner to work with in general, and many times it's what you want12/03 04:58
copumpkinpeano naturals as data are the naturals, but peano naturals as codata have an "infinity", for example12/03 04:59
Mathnerd314this isn't helping me with my proof.12/03 04:59
copumpkinI know :)12/03 04:59
copumpkinI was mostly kidding around about coming up with a formal proof of that unless you had a fairly strong background in this kind of stuff12/03 04:59
copumpkin(but don't give up on agda, it's awesome!)12/03 05:00
Mathnerd314where would I start with a proof?12/03 05:00
copumpkinI'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
copumpkinso pure : a -> Colist a12/03 05:01
copumpkinmore specifically12/03 05:01
copumpkinpure : {a : Set} -> a -> Colist a12/03 05:01
copumpkin(agda doesn't really have polymorphism)12/03 05:01
copumpkinyou could then define repeat fairly simply on your Colist12/03 05:02
copumpkinmap too12/03 05:02
copumpkinthen your proofs would be the laws... here, let me throw together a template for you12/03 05:02
Mathnerd314btw... what encoding are .agda files?12/03 05:07
copumpkinutf-8 usually12/03 05:07
copumpkinin fact, always I thnk12/03 05:07
Mathnerd314I need a better font then.12/03 05:07
copumpkinalmost done with my template :)12/03 05:10
Mathnerd314why does it take so long to make a simple template12/03 05:13
Mathnerd314?12/03 05:13
copumpkinI'm explaining stuff in it :)12/03 05:13
Mathnerd314somehow, firefox finds characters for everything, but none of my other programs do.12/03 05:15
copumpkinactually, proving stuff about this might be harder than I anticipated, but I'll show you the file as I have it12/03 05:16
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23917#a2391712/03 05:18
copumpkinothers in here might know more about it :)12/03 05:18
copumpkinbut basically, coinduction is scary12/03 05:18
copumpkinhow long have you been using haskell, anyway?12/03 05:19
* Mathnerd314 checks install date12/03 05:21
Mathnerd314Monday March 8 201012/03 05:23
copumpkinthis might be a bit precocious then :)12/03 05:23
Mathnerd314so... 4 days?12/03 05:23
copumpkinbut it's fascinating stuff, if you're interested in going deeper than haskell12/03 05:23
copumpkindeeper in some directions, at least12/03 05:23
Mathnerd314well, I've been thinking about type theory (or some fascimile of it) for a while longer12/03 05:24
copumpkincool12/03 05:24
copumpkinanyway, there's a fairly accessible tutorial on the agda wiki12/03 05:25
copumpkinhttp://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf12/03 05:25
Mathnerd314so peano naturals have an infinity in codata... that means you can induct to aleph-null?12/03 05:30
Mathnerd314because my proof is one by induction12/03 05:40
Mathnerd314so you need to do that for infinite lists12/03 05:40
copumpkinwell, did you actually prove anything for infinite lists?12/03 05:41
copumpkinin your earlier proof12/03 05:41
Mathnerd314I showed that it was true for the first element, and true for the next if it was true for the previous12/03 05:42
kmcwouldn't it be induction to ω rather?12/03 05:42
Mathnerd314Is that powerful enough?12/03 05:42
Mathnerd314yeah, that's what I want to happen.12/03 05:42
Mathnerd314the definition takes elements one at a time, so the proof should be able to as well...12/03 05:45
Mathnerd314copumpkin: your template is for a Functor, not for a Monad?12/03 05:48
* Mathnerd314 wonders if you sleep :p12/03 05:49
copumpkinMathnerd314: well, I started writing the laws and then remembered it's hard to prove equality on codata :P12/03 05:50
copumpkinbut you'd probably want to start by proving the functor laws, and build up to the monad ones12/03 05:50
Mathnerd314how do you prove equivalence?12/03 05:51
Mathnerd314magic?12/03 05:51
copumpkinon regular data?12/03 05:51
Mathnerd314on colists12/03 05:51
copumpkinwell, you could prove that any finite prefix of the colists is equal12/03 05:52
Mathnerd314so prove x=x and a delayed proof for xs?12/03 05:52
* Mathnerd314 has no idea what he's saying12/03 05:53
copumpkinwell, the proofs are typically functions12/03 05:53
copumpkin"if you give me a colist, I'll hand you back a proof of some property of that colist"12/03 05:54
copumpkinhttp://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
copumpkinbut it's not too bad12/03 05:54
copumpkinyou can copy that into your file and try using \~~ instead of \==12/03 05:55
copumpkinor you can just import Data.Colist if you'd prefer :)12/03 05:56
Mathnerd314import Data.Colist sounds good... what's the point of libraries if you don't use them?12/03 05:56
copumpkinoh 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 :P12/03 05:57
Mathnerd314I'm not certain I understand what the second part is doing12/03 05:59
copumpkinthe _::_ constructor?12/03 06:00
Mathnerd314yeah12/03 06:00
copumpkinit 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 equal12/03 06:01
Mathnerd314that's what I was trying to say above12/03 06:01
copumpkinI see :)12/03 06:01
copumpkinso you should be able to prove the functor laws fairly simply with those12/03 06:02
copumpkinI think the fmap id == id is actually unnecessary given the other law12/03 06:03
copumpkin(not in all categories, but in the ones we care about)12/03 06:03
Mathnerd314"all monads are functors and applicatives"12/03 06:03
copumpkinyep12/03 06:03
Mathnerd314according to wikipedia12/03 06:03
Mathnerd314;-)12/03 06:03
copumpkinthe reason I started with functor is that it's simpler12/03 06:03
copumpkinusing the return/bind in monad is a lot messier12/03 06:04
copumpkinso fmap + return + join tends to be cleaner12/03 06:04
copumpkinbut you're free to approach that proof as you wish12/03 06:04
copumpkinyou can probably convert between the proofs if you have one12/03 06:04
copumpkinby the way, typing a question mark and typechecking will create a hole for you12/03 06:06
copumpkinso 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 that12/03 06:06
copumpkinC-c C-, inside the hole will tell you what's in scope there and what the goal type of that hole is12/03 06:06
Mathnerd314so why does xs appear 3 times in the argument list and ys only twice?12/03 06:06
Mathnerd314there's something asymmetric about the definition...12/03 06:07
copumpkinwell, you have an x so you can reuse it multiple times. the xs and ys aren't really known to be equal at that point12/03 06:08
copumpkinyou have a delayed proof that they are12/03 06:08
Mathnerd314there's xs= : inf (b xs = b ys)12/03 06:08
Mathnerd314I don't see why there's an xs= at the beginning12/03 06:09
copumpkinthat xs~~ is just a name of the proof12/03 06:09
copumpkinit's to make error messages prettier12/03 06:09
copumpkinyou could omit it12/03 06:09
copumpkin(it'll also make a couple of features of the agda interactive environment more useful)12/03 06:09
Mathnerd314oh. so a : b means argument of name a and type b?12/03 06:10
copumpkinyeah12/03 06:10
copumpkinyou typically use it when you need to refer to its actual value later in the type12/03 06:10
Mathnerd314what about a :: b?12/03 06:10
copumpkin:: is the colist constructor12/03 06:10
Mathnerd314ok. so the reverse of Haskell ;-)12/03 06:10
copumpkinyep :)12/03 06:11
copumpkinand the _ on either side of it is a neat feature called mixfix12/03 06:11
copumpkinfactorial would be _! for example12/03 06:11
Mathnerd314doesn't scala have something like that?12/03 06:11
copumpkinyou can even have if_then_else_ : Bool -> a -> a -> a12/03 06:11
copumpkin:)12/03 06:11
copumpkinI don't think so12/03 06:11
copumpkinI think you can put underscores in things to make implicit functions, but not sure12/03 06:12
Mathnerd314I remember seeing some language having (_ > _)12/03 06:12
Mathnerd314and using it as an argument to functions12/03 06:12
copumpkinI think it does, but that's a form of partial application12/03 06:12
copumpkinso you could write 5 + _ * 10 or something and get a function that takes a number to a number12/03 06:13
copumpkinI've definitely heard of a language with that feature, but this is different12/03 06:13
copumpkinthis is giving you pretty deep control of the parser12/03 06:13
copumpkinyou can write _==_mod_ : Nat -> Nat -> Nat -> Bool, for example12/03 06:14
Mathnerd314ok.12/03 06:14
copumpkinand if it sees 7 == 13 mod 612/03 06:14
copumpkinit'll call that function12/03 06:14
Mathnerd314so like pattern matching but better12/03 06:14
copumpkin_==_[mod_] : Nat -> Nat -> Nat -> Bool maybe12/03 06:15
copumpkinsort of12/03 06:15
* Mathnerd314 finishes compiling the standard library12/03 06:16
copumpkin:)12/03 06:16
copumpkinone fairly amusing feature of agda is that most of its users never actually run their programs12/03 06:16
copumpkinwhy run it if you've already proven it to be correct? :P12/03 06:17
Mathnerd314can you actually run them?12/03 06:17
copumpkinsure, you can compile down to haskell in two different ways12/03 06:17
copumpkinyou can also ask the agda-mode to "normalize" terms for you12/03 06:17
copumpkinwhich is a bit like running12/03 06:17
Mathnerd314compile to haskell o_O12/03 06:17
copumpkinyep12/03 06:17
Mathnerd314I thought C was high-level...12/03 06:17
copumpkinlol12/03 06:17
copumpkinhaskell is semantically quite similar to agda12/03 06:17
copumpkina lot closer than C, at least :)12/03 06:18
Mathnerd314so, in the standard library, map-cong is the same as fmap?12/03 06:18
copumpkinmap is fmap12/03 06:18
Mathnerd314(or just map)12/03 06:18
copumpkinmap-cong is a proof12/03 06:18
copumpkinin fact, it's more or less what you need to prove for fmap id == id12/03 06:19
copumpkinbut its type is pretty obscure :P12/03 06:19
copumpkinit's basically saying that map preserves equality12/03 06:20
copumpkinif you have two equal colists to start with, and map a function to them, you'll have two equal colists12/03 06:20
Mathnerd314a function a->b, and it gives a proof a=b -> map a=b?12/03 06:20
Mathnerd314map a = map b12/03 06:20
Mathnerd314*12/03 06:20
Mathnerd314with implicit "type" parameters a and b12/03 06:21
copumpkinsort of12/03 06:21
copumpkinyou can actually ask agda to expand that type for you12/03 06:21
copumpkinC-c C-d map-cong12/03 06:21
Mathnerd314I'm using command-line, remember? since emacs+agda crashes?12/03 06:22
copumpkinoh, yeah :/12/03 06:22
copumpkinbut 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
copumpkinyou have a function, two colists, a proof that they are equal12/03 06:23
copumpkinit gives you a proof that after applying that function to both colists, the results are still equal12/03 06:23
Mathnerd314ok.12/03 06:24
Mathnerd314but it's also a definition of a map function, right?12/03 06:24
copumpkinwell, sort of12/03 06:24
copumpkinits definition is almost identical to that of map12/03 06:24
copumpkinbut it's constructing a value of _≈_, not a Colist12/03 06:25
copumpkinagda automatically disambiguates constructors12/03 06:25
copumpkinso there the [] on the right hand side is a constructor of _≈_12/03 06:25
copumpkinand the :: is too12/03 06:25
copumpkinon the left-hand side, it's pattern matching on Colist constructors (which happen to be identical to the ones of _≈_)12/03 06:26
Mathnerd314so how many overloads are there of []?12/03 06:26
copumpkintwo in this module, as far as I can see12/03 06:26
copumpkinbut you can write as many as you want12/03 06:26
Mathnerd314ok.12/03 06:26
copumpkinoverloading only works with constructors12/03 06:26
Mathnerd314so I can just ignore all that and pretend they're constructors12/03 06:27
Mathnerd314of CoLists12/03 06:27
Mathnerd314until I have to prove stuff12/03 06:27
copumpkinyeah, 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
Mathnerd314curry-howard isomorphism!12/03 06:29
copumpkinyep :)12/03 06:29
copumpkin_≈_ =[ map f ]⇒ _≈_ is another example of mixfix by the way12/03 06:29
copumpkinthe function is _=[_]⇒_12/03 06:29
Mathnerd314IRC client keeps putting in emoticons in odd places ;-)12/03 06:32
Mathnerd314anyway, how do you get emacs to find plugins?12/03 06:33
copumpkincan't remember :P I'm not an expert by any means12/03 06:33
copumpkinanyway, I need to go get some work done, lest I get my ass kicked tomorrow :P12/03 06:34
copumpkinI'll probably be back tomorrow evening if you have any more questions12/03 06:34
Mathnerd314when do you sleep? I can't figure it out...12/03 06:34
copumpkinnot often enough :/ but I'm US eastern time, and will probably go to sleep in a few hours :P12/03 06:35
Mathnerd314so 3 am or something?12/03 06:35
copumpkin1:35 right now12/03 06:35
copumpkinnot sure when I'll go to sleep, I hope as soon as possible12/03 06:35
copumpkinbut I still have to finish a paper12/03 06:36
Mathnerd314on type theory? :p12/03 06:36
copumpkinactually, it's a bit of a high-level introduction to that, for a class12/03 06:36
copumpkinit's just a writing class, so it's not terribly in-depth12/03 06:36
Mathnerd314fortunately, I have not yet advanced that far. I just have homework to do.12/03 06:38
copumpkin:)12/03 06:38
Mathnerd314back to work, then.12/03 06:38
copumpkinyep :) good luck with this stuff!12/03 06:39
Mathnerd314so, 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
Saizanmh, maybe on the wiki, though only the built-in syntax has ascii equivalents12/03 21:14
Mathnerd314alternately, I just installed some good fonts ;-)12/03 21:39
Saizansaner route :)12/03 21:40
Mathnerd314any recommendations for a good unicode monospace font?12/03 21:42
Mathnerd314(not that DejaVu is that bad)12/03 21:42
Saizanmy main font is Bitstream Vera Sans Mono12/03 21:42
Mathnerd314DejaVu is the successor to that, so ok.12/03 21:43
Mathnerd314I wonder how fonts have "snapshots" and "release candidates"...12/03 21:45
dolioIn 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
dolioBut, you have to have those other fonts, of course.12/03 21:48
Mathnerd314I have billions of fonts, but none of my editors are smart enough to use those others :-(12/03 21:48
dolioAre you not using emacs?12/03 21:48
Mathnerd314no, the emacs installed by the all-in-one windows installer seems to forcibly reboot my system after a compile or two12/03 21:50
dolioAh.12/03 21:50
dolioWell, then, you are entering a world of pain, probably.12/03 21:50
dolioWriting Agda is far, far easier with the emacs mode.12/03 21:51
Mathnerd314I'm also trying to install it manually...12/03 21:52
Mathnerd314it 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 load12/03 22:58
Saizanyay12/03 23:06
Mathnerd314but I have to downgrade to Emacs 22.3, since 23.1 doesn't support BDF fonts on windows :-(12/03 23:30
Mathnerd314after further testing, it appears that something in the BDF code is causing my system to reboot.12/03 23:46
Mathnerd314so, like I said before, anybody know a good set of fonts with all the glyphs Agda uses?12/03 23:47
liyangThis is probably not helpful, but how about running some instance of leenucks in a virtual machine?12/03 23:53
liyangUser apps causing the OS to reboot is… er… embarrassing to say the least.12/03 23:53
Mathnerd314I'm doing all this on windows right now12/03 23:57
--- Day changed Sat Mar 13 2010
liyangIf you have the spare memory, VirtualBox is free and Free.13/03 00:15
Mathnerd314yeah, I have virtualbox. it's not running anything though.13/03 00:15
TacticalGraceWhat is the biggest uni course Agda has been used in so far?13/03 01:51
Mathnerd314ok, 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
Saizanin emacs you can customize the include dirs13/03 02:01
Saizanotherwise you pass -i flags to the CLI13/03 02:01
Mathnerd314by "working installation", I meant emacs... how do I customize the include dirs?13/03 02:03
liyangCustomise 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
Saizancustomize Agda2 Include Dirs to include the path to the library13/03 02:09
Saizanhowever you also need the agda-mode setup step13/03 02:09
liyangTacticalGrace: undergrad? Nottingham has a few fourth-years taking it.13/03 02:09
SaizanMathnerd314: you M-x customize-apropos RET Agda RET and then look for Include Dirs in the buffer that comes out13/03 02:09
Mathnerd314ok.13/03 02:26
Mathnerd314agda seems to hate byte order marks?13/03 02:40
liyangPerhaps. Haven't encountered BOMs for a while. File a bug? http://code.google.com/p/agda/13/03 02:42
liyangUTF-8 doesn't need BOMs, but under Windows, text editor seem to add them anyway…13/03 02:44
Mathnerd314right.13/03 02:44
Mathnerd314and emacs seems to hide them, so they're hard to remove13/03 02:45
Mathnerd314how active is agda? bug tracker seems rather full...13/03 02:46
liyangMost 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
Mathnerd314it seems to mostly be "call for papers"13/03 02:50
TacticalGraceliyang: yeah, undergrad13/03 02:52
TacticalGraceliyang: I'm currently teaching (parts of) it to a class of 70 something13/03 02:53
liyangTacticalGrace: 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
liyangTacticalGrace: oh, Anton Setzer had some notes for a course he taught—http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials13/03 02:57
liyang(At Swansea)13/03 02:57
liyang(Also, aren't they a bit old to be undergrads?)13/03 02:58
TacticalGraceliyang: ;)13/03 03:00
TacticalGracehadn't seen Setzer's course, but seen txa's notes13/03 03:01
Mathnerd314agda is *slow*13/03 03:56
Mathnerd314is \to the same as -> ?13/03 04:00
TacticalGraceMathnerd314: yes13/03 04:03
Mathnerd314how do I do the equivalent of Haskell's case?13/03 04:06
Mathnerd314do I need a helper function?13/03 04:07
TacticalGracedepends, you may want to use a with13/03 04:07
Mathnerd314I want to write this, basically: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2391313/03 04:08
Mathnerd314just the >>= part though13/03 04:08
Mathnerd314so 'with' sounds like the right thing13/03 04:09
Mathnerd314copying from http://www.cs.chalmers.se/~ulfn/darcs/Agda2/test/succeed/Filter.agda13/03 04:09
TacticalGraceyou can use with for that13/03 04:09
TacticalGracesee, eg, Appendix A.5 in http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf13/03 04:09
Mathnerd314and function composition is...13/03 04:16
Mathnerd314^ TacticalGrace13/03 04:24
TacticalGraceI'm not sure whether it is pre-defined13/03 04:25
TacticalGraceHave you downloaded the standard library?13/03 04:25
Mathnerd314yes13/03 04:25
Mathnerd314+ added it to the path and compiled everything in it13/03 04:26
TacticalGraceok13/03 04:26
TacticalGraceI'm not sure whether it is defined in there, but might be worth to have a look13/03 04:26
TacticalGraceThere should be a Haddock for Agda....13/03 04:26
TacticalGraceor if Hoogle could be adapted13/03 04:28
TacticalGracethat would be very useful, gioven types in Agda are even more expressive than in Haskell13/03 04:28
TacticalGracegioven = given13/03 04:28
Mathnerd314I think it might be better if Haskell just adds enough language extensions that it turns into Agda13/03 04:28
Mathnerd314but anyway, I'm hearing no?13/03 04:29
TacticalGracethere is always that business about termination, but I agree that it is a tantalising goal13/03 04:29
Mathnerd314(as far as composition operator)13/03 04:30
TacticalGraceI'm not aware that is pre-defined, but I'm far from an Agda expert13/03 04:30
TacticalGraceand we are working with an intuitionistic logic, so I'll settle for the third option ;)13/03 04:31
Mathnerd314It doesn't seem that hard to me to just "borrow" the entire Haskell prelude...13/03 04:32
Mathnerd314but this function signature seems wrong: _._ : ∀ {A B C} → (B → C) → (A → B) → A → C13/03 04:40
Mathnerd314^ TacticalGrace13/03 04:43
TacticalGraceit's no dependent function composition13/03 04:43
TacticalGracethat is more complicated13/03 04:43
TacticalGraceI think it is somewhere in Ulf Norell's AFP'08 lecture notes13/03 04:43
Mathnerd314wow, a very long type ;-)13/03 04:46
Mathnerd314so function composition must be somewhere in the standard library...13/03 04:51
copumpkinyep, open import Function13/03 04:51
copumpkinI think13/03 04:51
copumpkinit's \o with agda's input method13/03 04:51
copumpkinnot sure if you managed to fix your emacs13/03 04:51
Mathnerd314it was some font problems13/03 04:52
copumpkinits type is terrifying, so I recommend you don't look at it :)13/03 04:52
TacticalGraceoh, right13/03 04:53
TacticalGraceit's in Data.Function13/03 04:53
copumpkinoh, I think that got renamed to just Function13/03 04:53
TacticalGracedidn't look under Data for function composition13/03 04:53
copumpkinbut maybe not in any released version of the std lib13/03 04:53
TacticalGracein lib-0.313/03 04:53
TacticalGracesupposedly lib-0.3 is the version to go with the latest Agda release13/03 04:53
Mathnerd314yay, that finished my porting of my monad's definition from Haskell to Agda13/03 04:54
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Function.html#25513/03 04:54
copumpkinyeah, NAD renamed it13/03 04:54
copumpkinnow it's top-level13/03 04:54
copumpkinthere's now a Function.(Bi/In/Sur)jection and Function.Equality13/03 04:54
copumpkin.Inverse too, all sorts of goodies!13/03 04:55
Mathnerd314it's all line noise to me...13/03 04:56
copumpkinI wonder how much time NAD spends perusing lists of unicode characters in search of the perfect symbol for his libraries :)13/03 04:56
copumpkinMathnerd314: I agree, big chunks of agda are practically illegible, sadly13/03 04:56
Mathnerd314Agda = Perl and Haskell = Python ;-)13/03 04:57
Mathnerd314so, proofs are functions over the variables that return equality?13/03 04:59
copumpkinTacticalGrace: are you already teaching the course using agda?13/03 04:59
copumpkinMathnerd314: ?13/03 04:59
Mathnerd314I'm translating my proof into Agda... so I need the type signatures13/03 04:59
copumpkinproofs don't have to be functions13/03 05:00
Mathnerd314what else are they?13/03 05:00
copumpkinjust plain old values13/03 05:00
copumpkintest1: 1 :: 2 :: 3 :: [] == 1 :: 2 :: 3 :: []13/03 05:01
copumpkintest1 = refl13/03 05:01
copumpkin:P13/03 05:01
* Mathnerd314 is confused again13/03 05:01
copumpkinthat is basically forcing agda to run a unit test at compile time for you13/03 05:01
copumpkintypes are logical statements, values are proofs of the associated types13/03 05:02
Mathnerd314but here, I have to prove that (return x) >>= f == f x13/03 05:02
TacticalGracecopumpkin: yep, two weeks into that course13/03 05:02
copumpkinoh cool, how's it going?13/03 05:02
TacticalGracelast week was the first week with Agda13/03 05:02
TacticalGraceYou should ask the student's that question13/03 05:02
copumpkin:)13/03 05:03
TacticalGracewe are starting very slowly13/03 05:03
TacticalGracemost of them don't know Haskell (or any other FP language) and the math bakcground is very varied13/03 05:03
copumpkinMathnerd314: yeah, you'd state that as forall f x -> return (x >>= f) == f x13/03 05:03
TacticalGracewe basically did Curry-Howard for propositional logic last week13/03 05:03
copumpkinyou'll most likely need to be more explicit about the types of f and x though, or you'll get lots of yellow13/03 05:03
TacticalGracenext week, we'll look at quantifiers and dependent types13/03 05:04
copumpkinTacticalGrace: sounds like they'll be learning a lot of awesome stuff pretty quickly :)13/03 05:04
copumpkinnot quite as quickly as Mathnerd314, maybe13/03 05:04
Mathnerd314I'm not learning, just doing ;-)13/03 05:05
TacticalGracewithout at least an intuitive understanding of Curry-Howard, I don't think Agda makes a lot of sense13/03 05:05
copumpkinyeah, I agree13/03 05:05
TacticalGraceI already saw these looks last week, kind of, well anybody can write some random functions, but how is that proving anything13/03 05:05
copumpkinare they all CS people, at least? with some kind of background in abstract reasoning? do they know what induction is?13/03 05:07
TacticalGracebesides, I think Curry-Howard is one of these very fundamental results of computing13/03 05:07
TacticalGraceyes, all CS, but from different CS programs13/03 05:07
TacticalGracesome have already done some formal methods using Event-B13/03 05:07
TacticalGracebut not all of them have done that13/03 05:08
copumpkinah13/03 05:08
TacticalGrace(we have computer science, software engineering, computer engineering, and bioinformatics)13/03 05:08
TacticalGracefor the CS and SE students this course is compulsory13/03 05:08
copumpkinthat's quite nice and granular13/03 05:08
TacticalGracefor the others its an elective13/03 05:09
copumpkinTacticalGrace: I've started designing a new (not E)DSL for using vector (and maybe DPH eventually) by the way :P13/03 05:10
TacticalGracea functional DSL for array computations?13/03 05:11
TacticalGracewhy not E?13/03 05:11
TacticalGraceI mean, why not embedded?13/03 05:11
copumpkinwell, my main inspiration was my difficulty writing vector-static13/03 05:11
copumpkinI tried and failed to make a usable interface for statically sized vectors13/03 05:11
copumpkin(built on top of vector)13/03 05:12
TacticalGraceoh, ic13/03 05:12
TacticalGraceso, the idea is to track sizes?13/03 05:12
TacticalGracestatically13/03 05:12
copumpkinso 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 safe13/03 05:12
copumpkinyeah13/03 05:12
Mathnerd314why not just use the monad I'm writing? ;-)13/03 05:12
TacticalGraceok, that sound interesting13/03 05:12
copumpkinbut actually writing any useful functions with vector-static proved to be a real pain13/03 05:13
TacticalGracedo you know http://www.cse.chalmers.se/~wouter/Publications/MoreDependentTypesForDistributedArrays.pdf13/03 05:13
copumpkinyou 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 solver13/03 05:13
TacticalGracecopumpkin: yeah, I can imagine that it is a pain in Haskell to help the type checker along13/03 05:14
copumpkinoh no, hadn't come across that, I'll check it out13/03 05:14
copumpkineven in agda, doing that kind of stuff is fairly painful13/03 05:14
copumpkinAlgebra.RingSolver is good but the output is noisy13/03 05:14
copumpkinI'd like to get as close to un-noisy vector usage as possible, while still coming up with static proofs of size invariants13/03 05:14
TacticalGraceyep, a specialised solver would be useful13/03 05:14
TacticalGraceit's somewhat like DML, too, I guess13/03 05:14
copumpkin(and then provide an extractor to haskell for performance, and one to agda to verify that my thing isn't doing anything stupid)13/03 05:15
TacticalGracecool13/03 05:15
copumpkinanyway, it's still vaporware but I've started writing my ring solver13/03 05:15
TacticalGracesounds like a good plan :)13/03 05:15
copumpkinI'm excited! I just finished all my coursework for this term so am more free13/03 05:15
TacticalGraceyeah, it's good to be able to concentrate on something for a longer preriod of time13/03 05:16
TacticalGracewithout context switching13/03 05:16
copumpkinyep :)13/03 05:16
copumpkinwouter's paper looks pretty interesting13/03 05:17
Mathnerd314so, can agda partially evaluate?13/03 05:23
copumpkinpartially evaluate?13/03 05:26
Mathnerd314I have to use the definitions of bind and return to prove stuff, right?13/03 05:27
copumpkinyep13/03 05:28
Mathnerd314so how do I apply those?13/03 05:28
Mathnerd314*use13/03 05:29
copumpkinyou refer to them in your type13/03 05:30
Mathnerd314but they're already defined...13/03 05:31
copumpkinhmm, I don't understand your question :)13/03 05:34
Mathnerd314the type I have is ∀ {A B} → (x : A) → (f : (A → Colist B)) → (bind (repeat x) f) ≈ f x13/03 05:34
copumpkinokay13/03 05:34
Mathnerd314so then I have to implement it...13/03 05:35
copumpkinyep13/03 05:35
copumpkinyou'd probably use a with construct13/03 05:36
copumpkinhave you tried proving simpler properties first? :)13/03 05:36
Mathnerd314I don't see how this is complicated... :-_13/03 05:36
Mathnerd314* _-:13/03 05:37
copumpkinas I said last time, proving things formally can be a lot harder than you'd expect :P13/03 05:37
copumpkinbut the functor laws are fairly trivial13/03 05:37
copumpkinand might be a good start13/03 05:37
copumpkin(I just proved them)13/03 05:37
Mathnerd314proved in agda?13/03 05:38
copumpkinyep13/03 05:38
* Mathnerd314 wants to see13/03 05:38
copumpkinjust a sec13/03 05:38
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=23952#a2395213/03 05:41
copumpkinreally trivial for functor, we'll see about applicative now :)13/03 05:41
* Mathnerd314 forgot about [] and _::_ overloading13/03 05:43
copumpkinlaw3 is trivial too13/03 05:45
copumpkinlaw4 might be a little more work (but probably not)13/03 05:45
Mathnerd314huh, I tried filling in the rest of monad law 1 and got "Not implemented: type checking of with application" :-13/03 05:46
Mathnerd314I guess I need a helper function...13/03 05:48
copumpkin:o13/03 05:49
copumpkinnever seen that before :)13/03 05:49
Mathnerd314how would I express that a function a -> Colist b is the same as a Colist of functions (a -> b)?13/03 05:49
copumpkinhm, it isn't really, unless you want to "sequence" it13/03 05:50
copumpkinover another monad13/03 05:50
Mathnerd314oh, wait, that's just the first law expressed differently13/03 05:51
copumpkinfirst law of what?13/03 05:56
Mathnerd314monads13/03 05:56
copumpkinalmost done with applicative :P13/03 06:02
copumpkinfmap id == id is what you're talking about?13/03 06:02
Mathnerd314no, (bind (repeat x) f) == f x13/03 06:03
Mathnerd314so, if f x == l :: ls, then does ls = next (f x) ?13/03 06:06
copumpkinnext?13/03 06:07
Mathnerd314a total tail function (next [] = [])13/03 06:07
copumpkinmeh, hpaste is down now13/03 06:07
copumpkinhmm13/03 06:08
Mathnerd314that's the type error I'm getting now ;-)13/03 06:10
copumpkincan I see your code? moonpatio.com is still up13/03 06:10
Mathnerd314http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8534#a853413/03 06:12
Mathnerd314I think I might have defined helper wrong, maybe.13/03 06:12
Mathnerd314comments?13/03 06:14
copumpkinit looks reasonable so far13/03 06:15
copumpkintrying to see how I'd do it13/03 06:15
copumpkindefinitely more painful than the earlier ones :)13/03 06:21
Mathnerd314well, you need bind or join13/03 06:22
Mathnerd314and bind is simpler IMO13/03 06:22
copumpkinyeah13/03 06:22
copumpkinI hate coinduction :P13/03 06:23
Mathnerd314anyways, by now I'm pretty certain that it's a monad, despite whether I can prove it or not13/03 06:25
copumpkin:P13/03 06:25
Mathnerd314say, if I define [] :: [] = [], then I can turn everything into infinite streams...13/03 06:26
copumpkinI'm actually confused at this13/03 06:31
Mathnerd314at what?13/03 06:32
copumpkinwell13/03 06:32
copumpkinfor your prop13/03 06:32
copumpkin113/03 06:32
copumpkinthe place where you call helper, I'd like to avoid calling helper13/03 06:32
copumpkinso I stick a hole there, and ask for the goal at that point13/03 06:32
copumpkin((bind (x ∷ .ZipList.♯-2 x) (λ x' → next (f x'))  | next (f x))  ≈ ♭ ys) is what it gives me13/03 06:33
copumpkinmeaning that further evaluation of the LHS of ~~ is delayed until next (f x) is evaluated13/03 06:33
copumpkinso I add another with next (f x)13/03 06:33
copumpkindecompose that13/03 06:33
copumpkinand it still refuses to evaluate the LHS any further13/03 06:33
Mathnerd314here, try changing, in bind, \b as to next (a \:: as)13/03 06:39
Mathnerd314the type simplifies a bit13/03 06:40
copumpkinhm, why would that be? it looks the same to me (and I don't see why it would be different13/03 06:41
Mathnerd314ok, you're right.13/03 06:42
Mathnerd314good to know next is defined correctly though...13/03 06:42
copumpkinyep :)13/03 06:43
copumpkingah, can't figure out why this isn't working13/03 06:44
Mathnerd314because it's secretly not a monad? :p13/03 06:49
copumpkinnah, I mean it's an agda issue (and I'm clueless)13/03 06:51
copumpkinnot a thing about the proof13/03 06:51
Mathnerd314well, I'm reading this: http://www.mail-archive.com/haskell-cafe@haskell.org/msg57217.html13/03 06:51
Mathnerd314can't figure out how it's related to my implementation13/03 06:53
Mathnerd314other than that mine works and his doesn't ;-)13/03 06:57
copumpkinso yours works on his examples?13/03 06:58
copumpkinthat's dolio by the way and he's often around here13/03 06:58
copumpkinI'm starting to think it isn't true, by trying to prove the associativity law13/03 07:00
Mathnerd314I think that message might give a counterexample...13/03 07:00
copumpkinit's pretty painful to type in colist literals :)13/03 07:01
copumpkinas I'm sure you're finding out13/03 07:01
dolioMathnerd314: Your diagonal was different.13/03 07:03
Mathnerd314does it work on that example?13/03 07:03
dolioIf I remember correctly, the second case in yours would be "diag ([]:xs) = []".13/03 07:04
* Mathnerd314 tries it out13/03 07:04
dolioYours quits as soon as it finds a missing diagonal element, which probably works.13/03 07:05
dolioNot sure why that never occurred to me.13/03 07:07
copumpkinit seems to work I think13/03 07:07
copumpkinunfortunately I can't get agda to prove it for me13/03 07:07
copumpkinoh yes I can13/03 07:07
Mathnerd314success?13/03 07:08
copumpkinoh wait13/03 07:08
copumpkinnope13/03 07:08
Mathnerd314oh well.13/03 07:08
copumpkinit has an extra element13/03 07:08
copumpkin.Data.BoundedVec.Inefficient._∷_ 8 .Data.BoundedVec.Inefficient.[]13/03 07:09
copumpkin!= .Data.BoundedVec.Inefficient.[]13/03 07:09
copumpkinI could've done it in half the time in haskell :P13/03 07:09
Mathnerd314so where is this?13/03 07:10
copumpkinhttp://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8535#a853513/03 07:10
copumpkinat least we have proofs that it's a functor an applicative, in case anyone doubted it13/03 07:11
copumpkinnow, we should prove that no monad exists for ziplists ;)13/03 07:11
Mathnerd314does it satisfy law7?13/03 07:12
copumpkinI wasn't able to get it to reduce the expression further13/03 07:13
copumpkinnot sure what's wrong13/03 07:13
copumpkinI'm probably doing something stupi13/03 07:13
copumpkinthat hole in law9 looks pretty bad though13/03 07:14
copumpkinbecause there's only one colist in scope whose type will fit in the hole, and it doesn't "fit"13/03 07:14
copumpkintrying to prepend x onto it doesn't help eihter :P13/03 07:14
copumpkinproof!13/03 07:15
copumpkin(also, there's no way to get another colist of that type)13/03 07:15
Mathnerd314so, diag = join, right?13/03 07:18
copumpkinyeah13/03 07:18
Mathnerd314well, I get [1,8] and [1] here.13/03 07:20
Mathnerd314so I'm probably missing something.13/03 07:20
copumpkinMathnerd314: the only answer is to prove once and for all that there can be no monad13/03 07:27
Mathnerd314and how do you do that?13/03 07:27
copumpkinwell, I can state it :P13/03 07:27
copumpkinprobably can't prove it13/03 07:27
Mathnerd314maybe one could use the laws to reach a contradiction?13/03 07:27
copumpkinyeah, that's how you prove negation13/03 07:27
Mathnerd314so one would assume... that the monad obeyed the laws of ZipList?13/03 07:28
Mathnerd314(functor / applicative)13/03 07:28
copumpkinyeah13/03 07:28
copumpkinbasically showing that the applicative laws don't fit with the monad ones13/03 07:29
copumpkinnot even sure it's true, but it'd be neat :)13/03 07:29
Mathnerd314well, first, it should act correctly on infinite lists, right?13/03 07:31
Mathnerd314and use map and repeat13/03 07:37
Mathnerd314so join should be the diagonal, for infinite lists13/03 07:39
copumpkinyeah, it should work correctly on those13/03 07:40
Mathnerd314and for join . (fmap return) to be id, it's the diagonal up to the size of the list13/03 07:45
Mathnerd314so, do bad things happen if I say []:[] = []?13/03 07:51
* Mathnerd314 is too tired to think13/03 07:54
copumpkinwhere would you say that?13/03 07:54
copumpkinin a constructor it's probably fine13/03 07:55
copumpkinhow can I prove _|_ from f [] ≈ f (something that very clearly is not [])13/03 09:06
copumpkinah I guess it isn't trivial13/03 09:11
Saizanyeah, you need injectivity of f13/03 09:27
copumpkinwhat if I have that f [] ~~ []13/03 09:30
copumpkinand ~~ only has [] ~~ [] and then other constructors13/03 09:31
copumpkinhmm13/03 09:31
copumpkinI guess it still isn't trivial13/03 09:31
copumpkinhmm, it seems like it should be though13/03 09:32
copumpkinhttp://snapplr.com/t3be13/03 09:32
copumpkinif I have x ~~ [], it seems like x must be []13/03 09:33
copumpkinhmm, I guess the closest equality I can define on x is what I already have13/03 09:38
copumpkinthis might actually be provable13/03 09:45
copumpkinprobably not though13/03 09:48
Saizanwhat is f here?13/03 09:56
Saizanif you have x ~~ [] you should get x = [] by pattern matching13/03 09:57
copumpkinnope :/13/03 09:59
copumpkinoh maybe13/03 09:59
copumpkinnah13/03 10:00
copumpkinf is join :P13/03 10:00
copumpkina hypothetical join :o13/03 10:00
copumpkinI'm trying to prove that there are no monads for ziplist :P13/03 10:01
copumpkinon colists, that is13/03 10:01
Saizanwhere is ~~ defined?13/03 10:02
copumpkinin Data.Colist13/03 10:02
Saizanoh, found13/03 10:02
copumpkinseems like == really isn't very useful around coinduction13/03 10:03
Saizanhttp://pastebin.com/bZWru9ui <- i'm sure i miss the bigger picture, but this part works :)13/03 10:05
copumpkinhmm, let me try that :)13/03 10:06
copumpkinthat doesn't even typecheck for me13/03 10:08
copumpkinthat p13/03 10:08
copumpkin_301 ≈ _301 !=< [] ≡ [] of type Set13/03 10:08
copumpkinwhen checking that the expression refl has type [] ≡ []13/03 10:08
Saizanfunny, maybe you've another refl in scope?13/03 10:09
copumpkinoh good point13/03 10:09
copumpkinI had a setoid open13/03 10:09
copumpkinaha, nice13/03 10:10
copumpkinnow I need to figure out how to get a bottom out of this :)13/03 10:11
copumpkinit's kind of a ridiculous exercise13/03 10:11
Saizani like to prove bottoms :)13/03 10:12
copumpkinI feel like I've forgotten something13/03 10:14
copumpkinbut that I'm on the right track13/03 10:14
copumpkinmaybe I'll go to sleep13/03 10:15
Saizanhttp://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/ <- UCF' here is supposed to be data or codata?13/03 15:32
Mathnerd314ok, just made *yet another data structure*13/03 15:51
Mathnerd314that acts like ZipList most of the time13/03 15:52
Saizanand the other?:)13/03 15:52
Mathnerd314the other is the ordinary Data.Colist (Haskell's list type)13/03 15:53
Mathnerd314the problem is that ZL (as I call it) is an infinite data structure 100% of the time13/03 15:58
Mathnerd314so I don't see how to display it13/03 15:58
Mathnerd314or test for equality13/03 15:59
Saizanwrite something like take :: Nat -> ZL a -> List a, to get prefixes13/03 15:59
Saizansee \~~ in Data.Colist for an useful definition of equality, though it's not decidable if two arbitrary streams are equal13/03 16:02
Mathnerd314ok, that works.13/03 16:41
Mathnerd314and ZL works on examples!13/03 16:44
Mathnerd314because the intermediate results aren't proper lists13/03 16:45
Mathnerd314but they are ZL's13/03 16:45
* Mathnerd314 celebrates13/03 16:53
Saizannice :)13/03 16:54
Saizando you have the code somewhere?13/03 16:54
Mathnerd314http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=8541#a854113/03 16:56
Mathnerd314(haskell, since I still am fuzzy on Agda)13/03 16:57
Mathnerd314so, normal lists [a,b,c] look like a ZL of {a,b,c,E,E,E,E,...}13/03 16:59
Mathnerd314and infinite lists look like {x,x,x,x,x,...}13/03 16:59
Mathnerd314but you get all these weird ones like {E,x,E,x,...}13/03 17:00
Mathnerd314which need to exist for the monad to preserve associativity13/03 17:00
Mathnerd314(and that disappear in normal cases of lift/zipWith)13/03 17:01
Saizanthat ZL type reminds me of dataflow programming, where the Events have different clocks13/03 17:02
Saizans/clocks/periods/ or whatever they are called13/03 17:02
Mathnerd314yeah, that's where I got the idea (particularly lucid)13/03 17:02
Mathnerd314it calls them streams13/03 17:02
Mathnerd314come to think of it, I can probably say a ZList is an infinite list of Maybe a...13/03 17:03
Saizanyeah13/03 17:04
Saizanthen the Applicative is just the composition of ZipList and Maybe applicatives13/03 17:04
Mathnerd314and all the functions are a bit shorter13/03 17:05
Saizanyup13/03 17:05
Mathnerd314hm, 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
Saizanreally?13/03 17:56
Saizannot f (Cons a b) = Cons (g a) (f b) ?13/03 17:56
Saizani.e. folds?13/03 17:56
Mathnerd314well, the two instances of f have different type arguments13/03 17:57
Saizanah, sure13/03 17:57
Saizansounds like you could do f x = fmap f x13/03 17:58
Mathnerd314actually, that pattern is only used in my definition of fmap ;-)13/03 18:03
Mathnerd314it's only the second, g a = Cons (g a) (g b)13/03 18:03
Mathnerd314in fact... that's pretty much my entire code13/03 18:05
Mathnerd314I don't even need all the specifics.13/03 18:10
Mathnerd314it's probably a monad combinator or something...13/03 18:13
Mathnerd314so, for example, I have fmap f (Cons a b) = Cons (fmap f a) (fmap f b)13/03 18:40
Mathnerd314how do I make Cons an instance of Functor?13/03 18:41
Saizanafaik there's no way to avoid that pattern, OTOH you could use DeriveFunctor in ghc-6.1213/03 18:46
Mathnerd314I'm just trying to figure out what I would write for the instance declaration.13/03 18:52
Mathnerd314I think I need... 3 type variables?13/03 18:54
copumpkinyou can't do that13/03 18:55
Mathnerd314why? :-(13/03 18:56
copumpkinwell what are the types of Cons? maybe you can13/03 18:56
Mathnerd314data Cons a b = Cons a b13/03 18:56
copumpkinfmap f (Cons a b) = Cons a (fmap f b) is the only thing you can do there13/03 18:57
copumpkinthe Functor is actually (Cons a), so you can't change the a13/03 18:58
copumpkinfmap :: (a -> b) -> (Cons c) a -> (Cons c) b13/03 18:58
Mathnerd314fmap :: (Functor c) => (a -> b) -> (Cons c) a -> (Cons c) b, you mean?13/03 19:01
copumpkinthe thing about functor is that you don't have control over what types it ranges over13/03 19:12
copumpkinso not that13/03 19:12
SaizanMathnerd314: you'd need BiFunctor from category-extras13/03 19:13
byorgeyMathnerd314: that doesn't make sense, Functor only applies to things of kind  * -> *13/03 19:17
byorgeyfor example it doesn't make sense to say  Functor Int,  only something like  Functor Maybe, or Functor List, or ...13/03 19:17
Mathnerd314well, Cons is of kind * -> * -> *13/03 19:18
byorgeyindeed.13/03 19:18
byorgeyso it can't be an instance of Functor.  but  (Cons a) can, for any a.13/03 19:18
byorgeyhmm, why are we talking about this in #agda? =)13/03 19:19
Saizanif you squint enough it's valid agda too :)13/03 19:20
byorgeyhehe13/03 19:20
copumpkin* looks just like Set to me13/03 19:22
copumpkin:)13/03 19:22
Mathnerd314how do you even write algebraic data types in Agda?13/03 19:31
byorgeyMathnerd314: the syntax is very close to the syntax for writing GADTs in Haskell.13/03 19:37
Mathnerd314oh, data x : x where x13/03 19:38
byorgeyyep13/03 19:39
byorgeya line for each constructor with its type, etc.13/03 19:39
Mathnerd314so data Cons : Set1 where cons : ∀ { A B } → A → B → Cons ?13/03 19:42
Mathnerd314when Cons was still ZL, it was ZL a = Cons (Maybe a) (ZL a) - so Maybe and ZL were functors/monads/etc. given as type variables13/03 19:44
Mathnerd314* not given13/03 19:47
Saizandata Const (A : Set) (B : Set) : Set where cons : A → B → Cons A B13/03 20:12
Saizanor data Cons : Set -> Set -> Set1 where cons : ∀ { A B } → A → B → Cons A B13/03 20:12
Mathnerd314I'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
copumpkinno13/03 20:29
--- Day changed Sun Mar 14 2010
Mathnerd314so how do I specify the monad laws, so I can use them to prove properties of things containing monads?14/03 03:14
Mathnerd314magic?14/03 03:22
--- Day changed Wed Mar 17 2010
jotikhi. Why does it sometimes complain inside { }0 that the text is read-only?17/03 11:33
jotikemacs i mean.17/03 11:33
npouillardjotik: only on the last space right?17/03 11:48
npouillardjotik: or your are trying to use a command whose scope is beyond the end of the hole.17/03 11:49
RLLain pattern matching when value is wrapped into {}, what does it mean?17/03 11:56
RLLait 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 uses17/03 11:58
RLLaof course, there is no mention of this is manual17/03 11:59
RLLain*17/03 11:59
RLLaso can someone confirm it17/03 11:59
npouillardRLLa: {...} denotes implicit arguments both in the types (f : ∀ {A : Set} ...), the expressions (f {ℕ}) and the patterns (f {A} ... = ...)17/03 12:24
RLLauh oh17/03 12:24
npouillardRLLa: was it clear enough ?17/03 12:24
RLLacertanly not17/03 12:25
npouillardlet's take an example17/03 12:25
RLLawell, i'm trying to implement well-known tabulate function here17/03 12:25
npouillardsure17/03 12:25
npouillardid : ∀ {A : Set} → A → A17/03 12:25
npouillardid {A} x = x17/03 12:26
npouillardthen a test17/03 12:26
npouillardid {ℕ} zero17/03 12:26
RLLait just restricts type?17/03 12:26
npouillardnop17/03 12:26
npouillardcompare this with:17/03 12:26
npouillardid' : ∀ (A : Set) → A → A17/03 12:27
npouillardid' A x = x17/03 12:27
npouillardtest17/03 12:27
npouillardid' ℕ zero17/03 12:27
npouillardin id' the type argument is explicit17/03 12:27
npouillardin id it is implicit, this means that in most cases I can write (id zero) without giving the type17/03 12:27
npouillardbut if I want it, I can by using the {}17/03 12:28
npouillardclearer ?17/03 12:28
RLLaimplicit arg thing is clear17/03 12:28
RLLabut not in pattern matching17/03 12:28
npouillardok17/03 12:29
npouillardI could have written the "id" body like this17/03 12:29
npouillardid x = x17/03 12:29
RLLayes17/03 12:29
npouillardbut if I do need the implicit argument I can caputre it with {A}17/03 12:29
npouillardexample17/03 12:29
npouillardlen : ∀ {A : Set} {n : ℕ} (xs : Vec A n) → ℕ17/03 12:30
npouillardlen {_} {n} _ = n17/03 12:30
RLLadon't you have to use {n} on rhs too?17/03 12:30
npouillardlen (1 ∷ 2 ∷ 3 ∷ []) ≡ 317/03 12:30
npouillardnop17/03 12:30
npouillardin expression {...} are used to pass implicit arguments to functions17/03 12:31
npouillardf {x} {y} z t17/03 12:31
RLLavery good17/03 12:31
RLLai understand this now17/03 12:31
npouillardbut {x} means nothing by itself in expression17/03 12:31
npouillardRLLa: cool17/03 12:32
RLLabut is it possible to define tabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n without using {...}?17/03 12:33
npouillardyes but using it will be ackward17/03 12:33
npouillardimagine:17/03 12:33
npouillardlen' : ∀ (A : Set) (n : ℕ) (xs : Vec A n) → ℕ17/03 12:34
npouillardlen' _ n _ = n17/03 12:34
npouillardtest17/03 12:34
npouillardlen' ℕ 3 (1 ∷ 2 ∷ 3 ∷ []) ≡ 317/03 12:34
npouillardyou kind of have to give the answer as argument yourself.17/03 12:34
RLLaah, you have to give N and 3 as explicit actual arguments17/03 12:35
npouillardyes17/03 12:35
npouillardactually you can give _ and let the type-checker try to guess it17/03 12:35
RLLabut i meant definition of tabulate not type signature17/03 12:35
npouillardRLLa: all three should follow the same scheme: type, patterns, expressions17/03 12:36
RLLahm17/03 12:36
npouillardhowever you can first define a function with explicit arguments and expose a short definition with implicit argus17/03 12:36
RLLaanyway, here is my definition: tabulate {s n} f = (f (fz {n})) :: (tabulate {n} (λ x → f (fs x)))17/03 12:36
RLLamy question was can you define it without matching on Nat17/03 12:37
npouillardwhat is your type for tabulate17/03 12:37
npouillardtabulate : {n : Nat} {X : Set} → (Fin n → X) → Vec X n17/03 12:38
npouillard?17/03 12:38
RLLayes17/03 12:38
npouillardand you have a second equation about 0 ?17/03 12:38
RLLayes17/03 12:38
RLLabut that's trivial case17/03 12:38
npouillardRLLa: so, if you have 2 equations something in the pattern must distinguish them17/03 12:39
npouillardhave you tried to write the second line as:17/03 12:39
npouillardtabulate f = f fz :: tabulate (λ x → f (fs x))17/03 12:40
npouillard?17/03 12:40
RLLahm, let me see17/03 12:40
npouillardmaybe the type-checker can infer them17/03 12:40
RLLahm, yes17/03 12:41
RLLabut is it good idea to let type-checker infer things?17/03 12:41
npouillardRLLa: yes17/03 12:43
npouillardAgda inference system only fills a hole when the answer is unique and directed by the typechecking of the rest17/03 12:43
RLLahm, it looks more like complete magic17/03 12:44
npouillardwhich is a limitation but on the plus side we can be sure of the safety of it17/03 12:44
npouillard:)17/03 12:44
RLLahehe, it might be ok if you know what's going on there but it just confuses me time to time17/03 12:45
npouillardsomething you can do is to put a ? instead of _ and then in emacs "C-x =" get the infered value17/03 12:48
Saizanoh, i didn't know that17/03 12:49
npouillardSaizan: what ?17/03 12:50
Saizanthe "C-x =" command17/03 12:51
Saizanthough it doesn't seem to work in my code17/03 12:51
npouillardmaybe it's C-c =17/03 12:52
* npouillard use viper and so have other bindings17/03 12:53
Saizanfound it in the menu17/03 12:54
Saizanthough if the term contains applications of record fields you get something very ugly17/03 12:57
jotiknpouillard: Sry for my absence. Duty called.17/03 14:28
jotiknpouillard: I was just trying to type into the hole17/03 14:28
npouillardjotik: no problem, got it to work ?17/03 14:45
jotiknpouillard: well yes somehow. I haven't yet figured out what causes this to happen.17/03 14:57
jotikbbl17/03 14:59
Saizaninside 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
Mathnerd314is there a good representation for a monad in agda?18/03 20:23
Jaakthere is one in the "standard" library18/03 20:26
Mathnerd314I want to prove the monad laws, which are missing from that18/03 20:27
Jaakyeah, you have to extend it if you want this18/03 20:27
Mathnerd314agda does not seem like a friendly language...18/03 20:29
Jaakno it's not :>18/03 20:30
Saizanmh, why not?18/03 20:30
Saizancoming from haskell i felt quite at home after a while :)18/03 20:30
Jaakknowing haskell does help18/03 20:31
Jaakbut still, brain explosion can't be considered friendly18/03 20:31
Mathnerd314that's just it... there's no brain explosion yet.18/03 20:33
Jaaki actually have some monad code around here18/03 20:34
Jaakwith proofs of laws for maybe monad :\18/03 20:35
Mathnerd314oh, that's the first monad I would implement.18/03 20:37
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24115#a24115 <- state is quite easy :)18/03 20:47
Jaaklist is working out quite well too18/03 20:47
Jaakyeah, it's pretty nice exercise18/03 20:59
copumpkinSaizan: wow, that was a lot of work, eh :P18/03 21:07
copumpkinyou could've saved 3/4 of the proof characters you typed, by the way18/03 21:08
Saizandefining r = refl ?18/03 21:08
copumpkin_18/03 21:08
Saizanoh18/03 21:08
copumpkinit saves so much work18/03 21:09
copumpkinI love it18/03 21:09
Saizani thought that only worked for \top18/03 21:09
copumpkinanything it can infer unambiguously, as far as I can tell18/03 21:10
copumpkinI use it for tedious types I can't be bothered to type out18/03 21:10
Jaaknot really much work saved. i think most of it it result of "refine" command18/03 21:10
Jaakah18/03 21:10
copumpkin(I was just being silly about saving work, but I do like using it)18/03 21:10
Saizanyeah, i've used it in types and expressions in EquationalReasoning18/03 21:11
Saizanthough i thought that it wouldn't work for data constructors for some reason18/03 21:11
Saizani guess that since we can prove "unique : ∀ {A : Set} {a b : A} (x y : a ≡ b) -> x ≡ y" there's no reason it shouldn't18/03 21:14
copumpkinyeah18/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 secs18/03 23:15
--- Day changed Fri Mar 19 2010
Jaakhmm, im not having much luck proving comonad laws for stream comonad19/03 02:38
Jaaki think i dont understand agda coinduction stuff yet19/03 02:38
Jaaki gather that i need different equality than the propositional equality?19/03 02:57
glguyCan I set the fixity of an operator that is a parameter to a type?19/03 03:19
glguyrecord R (_+_ : ...) where ... infix 5 _+_19/03 03:20
liyang_Jaak: yes. See stdlib/{Data/{Conat,Covec},Coinduction}.agda for examples and details.19/03 03:50
Jaakliyang: thanks19/03 14:35
Jaakthe module system is confusing me a lot. is there some up to date read on it?19/03 14:54
npouillardJaak: not that much, better I got was in some talks about it in the agda repo19/03 14:54
Saizani've learned what i know by the reference manual and seeing it used in the standard library19/03 14:54
Jaakfirst result on google is a talk from 2006, im don't know if it's current19/03 14:54
Jaaki*19/03 14:55
RLathere is a module system for agda?19/03 14:55
Saizanwhat are you confused about, specifically?19/03 14:55
npouillardRLa: yes19/03 14:55
Saizanit's similar to ML functors19/03 14:56
npouillardSaizan: not that much, you cannot take modules as arguments19/03 14:57
npouillardonly values19/03 14:57
npouillardand so records which in turns are equipped with a module19/03 14:57
Saizantrue19/03 14:57
* npouillard would really like a nice up to date, paper/presentation of the design choices of the agda module system19/03 14:58
JaakSaizan: i'm not too sure. might be confusion over the standard library19/03 15:01
Jaaki have defined a setoid but i dont really know how to use it for equational reasoning19/03 15:03
Saizanimport Relation.Binary.EqReasoning as EqR; open EqR yoursetoid19/03 15:05
Saizan"open EqR yoursetoid" is a shorthand for "module M = EqR yoursetoid; open M" i think19/03 15:06
Jaakawesome, seems to work now19/03 15:09
Mathnerd314can Agda prove termination of loops?19/03 20:08
fax??? yes19/03 20:11
Saizanthat question can be interpreted in many ways :)19/03 20:11
faxMathnerd314: Agda is a logic which is strong enough for analysis19/03 20:11
faxat least19/03 20:11
Saizanso if you define a language which has loops and its semantics you can prove that19/03 20:16
Saizanor were you referring to recursive definitions in agda itself?19/03 20:16
Saizanin 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 enough19/03 20:17
Mathnerd314my problem is that I can't think of any complicated examples of infinite loops...19/03 20:25
faxand19/03 20:38
faxif (UNPROVED CONJECTURE) then LOOP else HALT19/03 20:38
Mathnerd314oh, that 3x+1 conjecture sounds good.19/03 20:44
faxwhat are you doing this for19/03 20:46
Mathnerd314some small amusement...19/03 20:47
faxno19/03 20:48
faxI mean like19/03 20:48
faxwhat is it you are doing19/03 20:48
faxi don't think you are going to prove 3x+1 terminates19/03 20:48
faxfor example19/03 20:48
Mathnerd314I was coming up with an example where proving termination is difficult19/03 20:50
Mathnerd314I have one, so now I'm good.19/03 20:51
faxim just curious why19/03 20:51
Mathnerd314... I couldn't see anything in-between "while(true) {}" and the Halting Problem19/03 21:10
faxthere's a very interesting one19/03 21:12
faxhydra19/03 21:12
copumpkinfax: what's that one?19/03 21:40
faxyou cut of its head and it grows infinity more19/03 21:41
faxso the question is does hercules win (and the answer is yes he always wins)19/03 21:41
faxbut you must use ordinal analysis to prove termination19/03 21:41
faxthis is a non-trivial termination argument19/03 21:41
faxhttp://coq.inria.fr/distrib/V8.2rc1/contribs/Cantor.epsilon0.Hydra.html19/03 21:41
kmcfax, looks fun, is there a more commented / coqdoc'd version?19/03 21:48
faxIdon tkno19/03 21:48
faxMathnerd314 depth first algorithm to four color a planar map19/03 21:49
copumpkincoqbloq?19/03 21:49
fax:[19/03 21:49
copumpkin:)19/03 21:50
* Mathnerd314 is confused19/03 21:51
faxMathnerd314, you don't know about four colors suffice?19/03 21:52
Mathnerd314well, I know that.19/03 21:52
faxI am just telling you examples that came to me19/03 21:53
faxthis is a really good one, because I bet we all wrote this program too (I mean... without a termination proof)19/03 21:53
copumpkinuse four colors to color an arbitrary tiling of the surface of a torus!19/03 21:54
fax7 ?19/03 21:54
copumpkin4 is so much more badass19/03 21:54
copumpkinI bet chuck norris could do it19/03 21:55
Mathnerd314impossible!19/03 21:55
faxp=\left\lfloor\frac{7 + \sqrt{1 + 48g }}{2}\right\rfloor  (Weisstein).19/03 21:55
faxlol19/03 21:55
faxhow many colors you need for a thing with genus g19/03 21:55
faxno idea how they come up with that.. but the proof on a torus is apparently much easier than a sphere19/03 21:56
fax(sphere of course corresponds to planar)19/03 21:56
copumpkinsimple!19/03 21:56
--- Day changed Sat Mar 20 2010
glguy_Does this approach to defining categories and functors make sense? http://www.galois.com/~emertens/category/category.html20/03 02:44
glguy_I tried to follow the spirit of things like IsPreorder and Preorder20/03 02:44
--- Day changed Sun Mar 21 2010
fax"In order for the memory footprint of the typechecker to fit within the21/03 13:02
faxphysical memory of the machine, we were forced to factor the proof – sometimes21/03 13:02
faxunnaturally – into several submodules."21/03 13:02
faxheh21/03 13:02
Mathnerd314fax: what would need such a large proof?21/03 14:05
faxMathnerd314, I think it's more agda than the proof being big21/03 14:05
faxthis is from the dependently typed grammars paper21/03 14:06
--- Day changed Mon Mar 22 2010
roberto_Hi all. I'm trying to compile an agda "Hello world" example  (main : IO Unit  [[newline]] main = putStrLn "Hello world!")22/03 03:42
roberto_I get the following error22/03 03:43
roberto_Basics.agda:1,1-122/03 03:43
roberto_Basics.agda:1,1: Parse error22/03 03:43
roberto_main<ERROR> : IO Unit main = putStrLn "He...22/03 03:43
roberto_what's wrong with it?22/03 03:44
dolioIs that all that's in the file?22/03 03:49
dolioThose two lines, that is.22/03 03:49
dolioI don't think Agda lets you omit the "module Foo where" line.22/03 03:50
dolioFoo being the name of the file.22/03 03:50
roberto_Thanks. Done. Now I get "Not in scope ... when scope checking IO Unit "22/03 03:58
dolioYou also have to import the modules that define IO and such.22/03 04:02
dolioI've never really used IO in agda, though. I can't help you beyond that.22/03 04:03
roberto_Now I did an "open import IO.Primitive" and it works for IO.22/03 04:23
roberto_"open import Data.Unit" did not work for "Unit"22/03 04:23
dolioUnit doesn't exist. It's named \top22/03 04:24
dolioWhich looks like a T.22/03 04:24
dolio\top being how you type it in in the agda emacs mode.22/03 04:24
dolio22/03 04:25
roberto_I was with command line and an "normal" text editor. Now I see It doesn't work that way. I'll try to compile with adga emacs mode (already set-up) next time.22/03 04:29
roberto_and get used to that22/03 04:29
dolioIt's quite helpful.22/03 04:30
roberto_I think so. I still have to get used to it.22/03 04:31
roberto_Thanks for your help.22/03 04:32
dolioNo problem.22/03 04:33
temotoCan i define [_for_in_] python-like list comprehension operator in agda?22/03 16:20
stevanperhaps. what's the type?22/03 16:25
temotoWell...22/03 16:36
temoto[ x for x in list ] is equal to just   list22/03 16:37
temoto[ even x for x in list ] is equal to    map even list22/03 16:38
temotoso i'm not sure what is type of first subexpression22/03 16:39
temotojust a   or  a → b  defaulting to id22/03 16:40
faxwhat??22/03 16:47
temotoah.. forget it22/03 16:48
pigworkerShould I be able to make a program parse by removing a line break after a semicolon?22/03 21:18
faxpigworker: I'm no agda implementor but does sound fishy to me22/03 21:23
stevani think it makes sense.22/03 21:24
pigworkerI'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
stevanyou don't need semicolons to do that?22/03 21:26
faxI would get something to do with indentation, but I've never observed this kind of thing..22/03 21:27
doliolet has sort of layout like in Haskell.22/03 21:27
dolioSo it probably doesn't expect you to put a semicolon at the end of one let line.22/03 21:27
dolioOnly in beteween definitions on the same line.22/03 21:27
pigworkeryeah, I'm wondering what the rules are; I can put 'em all on one line with semicolons, or one per line without22/03 21:28
dolioYou can mix. I just tried it.22/03 21:28
doliolet i = 0 ; j = 1 <newline> k = 2 in k22/03 21:28
dolioAs long as you align k with i.22/03 21:28
dolioThe first k, that is.22/03 21:29
pigworkerYep, that works. I thought I tried that a while ago, but I must have screwed up the alignment.22/03 21:29
dolioThat's easy to do with unicode characters, at least for me.22/03 21:30
dolioSome of them aren't really monospace, but they count as one character.22/03 21:30
pigworkerNot a problem which afflicts me, as I haven't the energy for unicode.22/03 21:31
pigworkerI'm about to try it *interactively*.22/03 21:31
pigworkerAh. I can't align stuff interactively. I just have to tidy it up once it's done.22/03 21:33
maltemBtw does anyone know of a terminal emulator & font combination that will print characters like → at a readable size?22/03 21:33
maltemIt seems to me that one can have emacs print those at a larger size than what monospace would actually give you22/03 21:34
liyangI'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
pigworkerSometimes I wish Ulf's implementation of pattern unification understood records (not that mine ever did).22/03 22:01
kosmikuspigworker: you on irc? nice ...22/03 22:04
pigworkerkosmikus: I saw a link to a free mac client on the Agda wiki, and decided to check it out22/03 22:05
kosmikusgood work :)22/03 22:06
kosmikuspigworker: will you be here more often?22/03 22:09
pigworkerkosmikus: too early to tell; I'm experimenting with a new form of displacement...22/03 22:11
faxwe've had Pierre-Evariste, Edwin b, Peter Morris.. now CONor22/03 22:12
fax:D22/03 22:12
stevanthis is the unofficial epigram2 channel after all.22/03 22:12
faxyeah well there's been an epigram channel but on average 1 person at a time there22/03 22:13
kosmikusI didn't know there is one22/03 22:13
pigworkermost of the serious work on epigram2 gets prototyped in agda anyway22/03 22:13
kosmikusI'd join ;)22/03 22:13
faxit roughly doesn't exist22/03 22:13
faxto say, 5 decimal places22/03 22:13
kosmikuspigworker: as long as you're not claiming that epigram is going to be implemented in agda22/03 22:14
faxShe is sort of half way between haskell and agda? :)22/03 22:15
pigworkerkosmikus: no, but bits of it get weakly approximated, and that way we figure out what to implement22/03 22:16
kosmikusfax: true.22/03 22:16
kosmikuspigworker: yes, that's absolutely understandable. I'm also using Agda for that purpose more and more.22/03 22:16
pigworkerfax: in the tradition of Zeno22/03 22:16
dolioSo, here's something I've been wondering...22/03 22:20
dolioWhen you eventually introduce a hierarchy of universes, if that's what you in fact do...22/03 22:21
dolioWhat happens with regard to set equality vs value equality?22/03 22:21
dolioI suppose that makes sense even now with Set : Set, as ! Set > Set == Set > Set !22/03 22:22
pigworkerdolio: sets-as-values equality gets farmed out -- ! Set > S == Set > T ! = S <-> T22/03 22:24
pigworkerdolio: that stratifies, too...22/03 22:25
pigworkerI'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
dolioSo, for S : SetN, T : SetM, there's a S <-> T.22/03 22:26
dolioEven if N /= M.22/03 22:26
kosmikuspigworker: yes, hpaste will work22/03 22:26
kosmikuspigworker: just go to hpaste.org, click new22/03 22:26
faxTODO: Agda paste side22/03 22:26
dolioSomeone needs to write an agda hilighter for whatever coloring library hpaste uses.22/03 22:27
faxI wonder what the complexity of agda syntax coloring is?22/03 22:27
pigworkerdolio: every universe has a <->, which gets used as the value equality for that universe-as-a-set in higher universes22/03 22:27
liyangdolio: good luck. :)22/03 22:27
dolio:)22/03 22:27
stevanwhy not just a file uploader which typechecks the file and gives a link to the html output?22/03 22:27
kosmikusstevan: should be a machine with lots of RAM ;)22/03 22:28
doliopigworker: I guess that just works out of universes are cumulative?22/03 22:28
dolioIf, even.22/03 22:28
stevanperhaps 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
kosmikusgood night22/03 22:31
pigworkerdolio: something like http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2426322/03 22:32
pigworkerdolio: that model isn't fully cumulative yet, but its props are; it's a rather fierce piece of work, I admit22/03 22:34
faxpigworker -- 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
pigworkerfax: Thorsten hired a student a while back; it's no longer available22/03 22:38
faxoh 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 :D22/03 22:39
faxI probably just have to be patient..22/03 22:39
faxthe only ones I know of are martin lofs one and fresh lists and the examples from Peter Dybjer22/03 22:40
pigworkerfax: it's more a question of figuring out which IR definitions make sense, and how22/03 22:40
faxoh that's quite different than I had imagined then22/03 22:40
pigworkerbig 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
dolioAgda seems to get along fine with it.22/03 22:42
dolioAs far as we know.22/03 22:42
dolioNo one's proved false lately.22/03 22:43
pigworkerdolio: I constructed an impredicative universe at one stage, because they forgot a check22/03 22:44
dolioHeh.22/03 22:44
dolioAlthough that is something I've wondered off and on...22/03 22:44
dolioAre families indexed by Set "inductive" families?22/03 22:45
faxhehe22/03 22:45
dolioSet is not defined by induction.22/03 22:45
dolioAt least in Agda.22/03 22:45
pigworkerdolio: 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
pigworkerdolio: and Gil Hur gets quite close to the bone, thanks to that...22/03 22:46
dolioIn that sense, the line that "GADTs are a special case of inductive families" isn't necessarily true.22/03 22:48
dolioBut, since GHC doesn't have inductively defined static things, there's no other choice.22/03 22:50
dolioNot that people care about proofs of false in that environment anyhow.22/03 22:50
dolioAt 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
dolioEven though there are 6 other ways to do the same thing.22/03 22:51
Mathnerd314what does it mean if you can prove false?22/03 22:53
dolioIt means you have a non-terminating 'value'.22/03 22:53
faxwhat blows my mind is that people still go to the trouble of endcoding inductive proofs in haskell..22/03 22:53
Mathnerd314so it's an infinite loop or something in the type checker?22/03 23:05
dolioWell, the definition of false would be 'data False : Set where', so there are no proofs (constructors) for it.22/03 23:06
faxMathnerd314: needn't be22/03 23:06
liyangMathnerd314: Think of it as the type-theory equivalent of I JUST DIVIDED BY ZERO. OH SHI-22/03 23:06
dolioSo, 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
faxforall P, P   could be another definition22/03 23:06
Mathnerd314oh, so all it means is that your type checker is too lenient.22/03 23:16
dolioWell, it could mean lots of things.22/03 23:17
dolioHaskell, for instance, essentially adds fix as a primitive. And fix id has the right type.22/03 23:18
dolioThat's not a failure of the type system, per se.22/03 23:18
pigworkerCrucially, false hypotheses are relatively benign; it's closed proofs of false that behave badly.22/03 23:18
dolioHaskell also has general recursive types, which let you type stuff like (\x -> x x) (\x -> x x) with some fiddling.22/03 23:21
dolioSo 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
faxgeneral recursive types aka negative types ?22/03 23:24
pigworkerConsistency also enables a class of optimizations: it's not just soundness for the sake of it.22/03 23:24
dolioAs 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
dolioSo, 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
Mathnerd314I can't figure out what that does... can it ever return a value?22/03 23:40
dolioIt reduces to itself forever.22/03 23:40
Mathnerd314right... but can you feed it arguments and get out values?22/03 23:41
dolioNo, it just spins.22/03 23:42
Mathnerd314so it's an infinite loop, suitably disguised?22/03 23:43
faxit's not disguised22/03 23:43
dolioI 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
Mathnerd314fax: it's disguised in lambda calculus, because usually infinite loops are in imperative languages22/03 23:44
faxoh22/03 23:44
faxyeah i don't think it's a roundabout way to represent a C program22/03 23:44
liyangit's a special case of the fixpoint combinator, Y = \ f -> (\ x -> f (x x)) (\ y -> f (y y))22/03 23:44
pigworkerliyang: is that why YI is so-called?22/03 23:48
liyangpigworker: the editor? I have no idea…22/03 23:50
* fax thinks yes22/03 23:51
faxYI = I(YI)22/03 23:51
liyanghttp://haskell.org/haskellwiki/Yi#Trivia says yes.22/03 23:51
pigworkerI'm wondering if SICK computes to anything interesting.22/03 23:52
liyangI 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
pigworkerSICK = IK(CK) = K(CK)22/03 23:54
pigworkerliyang: I was thinking of the editor; I had a spinning editor situation earlier.22/03 23:56
pigworkerAh nice, KISS IS S22/03 23:57
faxYUCK = UUUUUUUUU(YUCK)22/03 23:57
liyangpigworker: related to the spinning Aquamacs on Twitter earlier?22/03 23:59
--- Day changed Tue Mar 23 2010
pigworkerliyang: the very same; ironic, given the proof was about productive coprograms23/03 00:00
edwinbgood lord, it's pigworker!23/03 00:06
edwinbevening23/03 00:06
pigworkeredwinb: not quite sure how that happened23/03 00:07
faxpigworker -- did you ever 'To Mock a Mockingbird'? :)23/03 00:07
fax(lovely book... embossed cover and rough pages)23/03 00:08
pigworkerfax: my Smullyan coverage is thin, and doesn't make it that far23/03 00:08
edwinbpigworker: how is your agda based central heating system?23/03 00:09
pigworkeredwinb: cooler, now that I've been distracted23/03 00:10
liyang*whooooosh*23/03 00:14
liyangWhat was that? Sounded like productivity.23/03 00:14
faxgood luck making pigs fly anyway !23/03 00:15
edwinbI hear it happens sometimes23/03 00:15
pigworkerjust doing some of the exercises I set in my blog post23/03 00:23
edwinbHmm, I think I'll wait until morning to catch up with that bit of blogland...23/03 00:41
* Mathnerd314 finds pigworker's blog23/03 01:02
pigworkerg'night all; see yiz round23/03 01:29
stepcutif I have: data Bool : Set where true : Bool ; false : Bool, is there a way to make a function, trueId : true -> true23/03 04:18
liyangWon't Function.id do the job?23/03 04:20
stepcutwell, I want to apply it only to true values..23/03 04:21
stepcuta better question might be..23/03 04:21
stepcutif 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
liyangI 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
liyangstepcut: sure. Require a proof that the list starts with 1 as another parameter.23/03 04:22
stepcutliyang: sounds easy :)23/03 04:22
liyangOnce you see it…23/03 04:23
stepcutyes, that has been my problem so far23/03 04:23
stepcutit's easy after I see it, but not before :p23/03 04:24
stepcutI sort of came up with something that works, by creating a new type23/03 04:24
stepcutbut I haven't figure out if it is a weird way to do it yet :)23/03 04:24
stepcuthttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a2427223/03 04:25
stepcutI have a list (or 'string') of symbols. M I U, and a rule1 which can only be applied to a string that starts with M23/03 04:26
stepcutbut I am not sure how to make rule1 a 'function' instead of a 'constructor'23/03 04:26
liyang(Sorry, my Aquamacs is taking forever to go through its spin cycle. Hang on…)23/03 04:28
liyanghttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24273#a2427323/03 04:31
liyangGo into that hole, and refine-case on the xs≡1∷ argument.23/03 04:31
stepcutok23/03 04:31
liyang(and again on the second part of the product ^^;;)23/03 04:33
stepcutI 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
liyangOkay, now put y into the hole and do that again.23/03 04:38
stepcutand then x ?23/03 04:38
stepcutnow I have, oneHead .(1 ∷ x ∷ xs) (x ∷ xs , ≡.refl) = {!!}23/03 04:40
liyangSo inspecting the proof forces the first argument to begin with a 1. :)23/03 04:42
liyang(the x in (x , y) is just the rest of the list.23/03 04:43
stepcutright23/03 04:43
stepcutI sort of understand how this works :)23/03 04:44
stepcuttime for bed now. thanks!23/03 04:45
stepcutI think I understand what I have done with the System type in the code I was writing too..23/03 04:46
liyangStream 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. :323/03 04:52
liyanghttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24272#a2427423/03 04:53
stepcutsweet!23/03 04:56
liyangI hope that wasn't homework. :-/23/03 04:58
stepcutso 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
stepcutWith 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
stepcutI didn't know people even had agda homework :p23/03 05:00
liyangAnd 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
liyangstepcut: I'm aware of a few courses that teach it. :)23/03 05:00
stepcutyeah23/03 05:00
stepcutthe 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
liyangOH SHI- Of course. I ought to have remembered. ^^;;23/03 05:02
stepcut:)23/03 05:02
stepcutI supposed it could be somebodies homework, but it's not mine :)23/03 05:04
stepcutbut it's already tomorrow now, so I gotta get to sleep, thanks again!23/03 05:04
liyangIt'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
stepcutright23/03 05:05
liyang(if that made any sense.)23/03 05:05
liyangstepcut: 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
Svrogdoes 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 work23/03 07:28
Svrogas 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 me23/03 07:33
TacticalGraceAgda mode for TextMate would be great23/03 10:32
TacticalGraceTextMate at least manages to do the unicode font rendering properly23/03 10:32
stevanTacticalGrace 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
edwinbI switched to that after I got fed up with aquamacs23/03 15:25
edwinbIt fixed the things that annoyed me, although I can't remember what those annoyances were...23/03 15:26
stevan(if it works better, it might be appropriate to add a note about it on the wiki.)23/03 15:29
edwinbI am not confident enough about that ;)23/03 15:30
edwinbit was only minor annoyances for me23/03 15:30
liyangIt won't recognise the C-, in C-c C-, so I ended up adding a mapping from C-c , instead.23/03 19:01
faxI was trying to think of a non induction+lots of finicky algebra proof of binomial theorem23/03 21:26
faxlike counting how many paths has k lefts in them in a size n perfect tree or something23/03 21:27
faxnever found a good way though23/03 21:27
fax(when I said induction above I mean the P(n)=>P(n+1) stuff)23/03 21:27
--- Day changed Thu Mar 25 2010
lpjhjdhis there a convenient way of constructing piecewise functions?25/03 02:37
liyangElaborate? What would be the inconvenient way?25/03 02:51
lpjhjdhnested ifs25/03 02:52
lpjhjdhI'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 cases25/03 02:52
liyangHave you got a particular example? (hpaste?)25/03 02:53
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a2434525/03 02:54
lpjhjdhI defined ≟ and ≠ cause I couldn't find simple boolean versions over nat25/03 02:54
glguy_You can at least do this: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24345#a2434625/03 02:56
lpjhjdhah, that's perfect, thanks25/03 02:57
glguy_You might actually be able to leave the false values as _25/03 02:57
glguy_I'm just copy/paste mangling that25/03 02:57
liyanger… I was going to use Data.Nat._≟_ which returns a proof of i == j if they are equal.25/03 03:03
lpjhjdhI just used boolean cause I wasn't particularly interested in why they were or weren't equal25/03 03:14
stepcutdoes agda have 'module functors' ? I know the module system is more advanced that haskell's, and reminds me of ocaml.. but is it technically correct to say it has module functors?25/03 22:34
--- Day changed Fri Mar 26 2010
roberto_Hi.26/03 02:55
roberto_quick question26/03 02:55
roberto_What does MAlonzo have anything to do with me?26/03 02:55
roberto_Seriously, I tried to compile simple agda examples with no success26/03 03:02
roberto_"The function `main' is not defined in module `MAlonzo.Qbasics'"    (my "basics.agda" file is just a single line: "module basics where")26/03 03:12
lpjhjdhso I'm having an issue with agda not being able to show that two things are equal26/03 03:45
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24380#a2438026/03 03:46
liyangOh that's a very frequent problem.26/03 03:46
lpjhjdhwhat is it resulting from?26/03 03:47
lpjhjdhusing much simpler types the following works out: presa (plusl stn) (ok-add wtn wtm) = ok-add (presa stn wtn) wtm26/03 03:47
lpjhjdhI can expand on some of my types if it's not immediately obvious, I'm not familiar with the actual theory behind dependant types26/03 03:50
liyangIt's not immediately obvious. :( I'd look for where the e₀' was coming from.26/03 03:51
lpjhjdhthe go function is actually nothing, just trying to pattern match an ok-add26/03 03:52
liyang(I mean, the general state of not being able to show two things equal in Agda is a frequent problem for me.)26/03 03:53
lpjhjdhah, 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 worked26/03 03:54
lpjhjdhunfortunately I see no obvious way of "factoring" the e's that are the terms of the add :(26/03 03:54
lpjhjdhis it maybe because it "forgets" since they become a single term?  Namely the argument to the injection.26/03 03:58
liyangI'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
lpjhjdhthat seemed to be the problem.  Sadly each time one thing gets fixed it introduces another issue26/03 05:05
liyangIt's a gift that never stops giving.26/03 05:20
guerrill1looks like lots of exciting stuff was discussed at the AIM.. sized types, structual equality, etc. etc.26/03 12:57
guerrill1anyone know what "Java Agda" means?26/03 12:57
guerrill4or "Agda-A"26/03 12:57
guerrill4ah "A new implementation of Agda written in Java "26/03 12:58
guerrill4that sounds cool26/03 12:58
andgraI 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
faxandgra: what's the definition of it?26/03 13:34
andgrathe subset operator?26/03 13:35
faxyes26/03 13:35
andgrawell, the one from Data.Sets (stdlib 0.3) is just _?_ : <Set> ? <Set> ? Set26/03 13:36
andgra  s1 ? s2 = ? x ? x ? s1 ? x ? s2 but26/03 13:36
faxI cant read it26/03 13:36
faxit's just question marsk26/03 13:36
Jaakweird, that type doesn't even typecheck for me26/03 13:37
andgra_ss_ : <Set> -> <Set> -> Set26/03 13:38
faxwhat's the agda file26/03 13:38
andgrabut the definitions of <Set> I don't really understand26/03 13:38
andgraData.Sets in the standard library26/03 13:38
faxis it actualyl called<Set>26/03 13:38
andgrayes26/03 13:38
Jaakso that type actually typechecks?26/03 13:39
andgrait somehow wrapps DecSetoid from Relation.Binary26/03 13:39
faxhttp://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda26/03 13:39
fax  <Set> : Set26/03 13:39
fax  <Set> = DecSetoid.Carrier decSetoid26/03 13:39
fax  _⊆_ : <Set> → <Set> → Set26/03 13:39
fax  s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂26/03 13:39
faxandgra, can you see this correctly?26/03 13:39
andgrayeah26/03 13:39
faxokay good26/03 13:39
faxso you want to pre26/03 13:39
faxso you want to prove*26/03 13:40
faxprf : ∀ {a b} {A C : Set a}{B : Set b} →  (x : C) (f : A → B) → (C ⊆ A) → (f x) ⊆ B26/03 13:40
faxprf = ?26/03 13:40
faxwhich is the same as:26/03 13:40
faxprf : ∀ {a b} {A C : Set a}{B : Set b} →  (x : C) (f : A → B) → (∀ x → x ∈ C → x ∈ A) → (∀ x → x ∈ (f x) → x ∈ B)26/03 13:40
fax?26/03 13:40
faxyeah what Jaak says...26/03 13:40
faxwhy have your paste got  Set a  but the thing is  <Set>  ?26/03 13:41
Jaakyeah, posting whole file that types might help26/03 13:41
faxwhy not  prf : {A B C : <Set>} →  (x : C) (f : A → B) → (∀ x → x ∈ C → x ∈ A) → (∀ x → x ∈ (f x) → x ∈ B)  ?26/03 13:41
andgrawell, in the paste I was using Relation.Unary but I'm guessing that will not work26/03 13:41
andgraI haven't tried that...26/03 13:41
faxRelation.Unary????????????26/03 13:42
faxwhy am I looking at this http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Sets.agda26/03 13:42
andgraI'm sorry - I have tried to use both because I'm not sure I completley understand the difference between them26/03 13:42
faxandgra26/03 13:42
faxwhy would you want to use either of them?26/03 13:43
guerrill4andgra: yeah, what are you trying to do - at a high level?26/03 13:44
andgrahmm, maybe I don't. I was looking to do some work how functions project on sets so I started reading in the stdlib26/03 13:44
faxproject on sets?26/03 13:45
guerrilla?26/03 13:45
faxguerrilla http://people.cs.uu.nl/stefan/downloads/brink10dependently.pdf26/03 13:47
guerrillayeah, i read most of that.. what part?26/03 13:47
faxall of it26/03 13:48
andgrawhat 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
guerrillafrom what i saw, his code works directly26/03 13:48
guerrillafax: why should i look at it?26/03 13:48
guerrillahehe26/03 13:48
guerrillahave we talked before?26/03 13:48
faxandgra; f : A -> B ?26/03 13:48
faxandgra oh you mean like a nonsurjective function26/03 13:49
faxthe set f(A) <= B26/03 13:49
guerrillafax: (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
faxguerrilla I think agda will get quotients soon!26/03 13:50
andgrayeah26/03 13:50
faxandgra, so in type theory we can define this 'inverse image' in a very different way than set theory26/03 13:51
guerrillafax: sorry, what do you mean by quotient?26/03 13:51
faxwait it's not inverse image :/26/03 13:52
faxit's just the normal image26/03 13:52
faxdata Image {A B} (f : A -> B) : Set where witness : forall (a : A), f a -> Image f26/03 13:52
andgrayes, 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
faxandgra yeah but it's not set theory26/03 13:52
faxno clue why they call it Set actualyl, but it's a type26/03 13:53
andgraI'm not completley sure I understand?26/03 13:53
andgraalso... {A B C : <Set>} doesn't typecheck...26/03 13:55
guerrillain what context?26/03 13:56
andgrahttp://pastebin.com/raw.php?i=iF9FSJbG26/03 13:58
Jaakeven "{A : <Set>} -> \top" doesnt typecheck, infact26/03 14:00
guerrillaJaak: that's interesting...26/03 14:00
guerrillai think andgra's code doesn't because he's saying A and B are members of the type <Set> then saying he has some function from some member to another.. which doesn't make a lot of sense26/03 14:01
guerrillathat would be like f : zero -> zero for Nat afaik26/03 14:02
guerrilla{A B : Nat} -> (f : A -> B) ... wouldn't work because A and B would have to be either zero or succ26/03 14:02
guerrillasame principle applies here26/03 14:02
guerrillamaybe someone can explain that more elegantly though :)26/03 14:02
guerrillaim not sure what's with Jaak's though.. i would think that would work26/03 14:03
andgraso something like '\all {a b} {A C : <Set> a} {B : Set b}' or am I missing the point completely?26/03 14:03
guerrillaor maybe Jaak it's just because you left out a use of A so there's nothing to infer the implicit argument from26/03 14:03
guerrillawell you cant do Set b26/03 14:04
Jaaki see26/03 14:04
andgraoh, I mean '<Set> b' ofc...26/03 14:05
Jaakyup, giving argument helps26/03 14:05
guerrillawell, mtg time. bbiab26/03 14:24
guerrillagood luck26/03 14:24
faxpigworker 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 malfunctioning26/03 17:14
pigworkerfax: I think one of my students was wondering the same thing. It's something stupid and fixable. I forget what.26/03 17:21
faxI wanna wirte my category theory notes in epigram ;D26/03 17:24
faxif 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
pigworkerI 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
faxah that's it! thanks26/03 17:38
--- Day changed Sat Mar 27 2010
IglooHi all27/03 01:24
lpjhjdhso I'm trying to make an extremely simple assertion of equality about the following function but am not sure how27/03 03:22
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24412#a2441227/03 03:22
lpjhjdhcan I somehow tell agda to just do one level of expansion and then apply refl?27/03 03:23
lpjhjdhjust "refl" doesn't work27/03 03:23
lpjhjdhas imported from Relation.Binary.Core27/03 03:24
pigworkerlpjhjdh: 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 equation27/03 14:43
lpjhjdhhmm, that thought occured to me so I changed it to the equality test from Data.Nat but it still doesn't seem to reduce27/03 15:43
lpjhjdhso I've been trying to show a simple equality and I'm not sure how to get agda to expand it27/03 19:44
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a2445027/03 19:44
lpjhjdhthe refl simply says "f0 m m m = f0 m m m"27/03 19:44
fax'with' is evil27/03 19:44
lpjhjdhah, why's that?27/03 19:50
lpjhjdhshould I expand it to helper functions myself then?27/03 19:52
faxi don't know27/03 20:04
faxwhat I would do is define a data type that was indexed by 3 N's, with constructors for each case27/03 20:04
faxlike27/03 20:05
lpjhjdhI'll give it a shot, thanks, it actually hadn't crossed my mind to try something like that27/03 20:05
faxcase1 : Rec i j (suc k)27/03 20:05
faxm not quite that27/03 20:05
faxcase2 : Rec (suc k) (suc k) (suc k)27/03 20:05
faxsorry..27/03 20:05
faxcase1 : Rec (suc k) (suc k) (suc k)27/03 20:05
faxcase2a : Rec (suc k) j (suc k)27/03 20:05
faxcase2b : Rec i (suc k) (suc k)27/03 20:05
faxand so on27/03 20:05
lpjhjdhah, another clever idea, thanks27/03 20:05
faxso then you can 'prove' a general theorem, that  forall i j k, Rec i j k27/03 20:06
faxthat should let you do the e27/03 20:06
faxthat should let you do the 'eq' proof, but it's probably awkward enough that it wont let you do much else27/03 20:06
faxmaybe it'll work out tohugh27/03 20:06
fax(oh Rec might be a recursive type too, where f_0 is recursive)27/03 20:07
lpjhjdhyeah, I'm actually trying to give a more general proof that f0 and this other function T are equal27/03 20:08
faxcan I see T?27/03 20:10
faxthis is kind of interesting I thought f_0 was just a made up function27/03 20:10
lpjhjdhyeah, it's actually the schedule for a parallel implementation of the algebraic path problem27/03 20:13
lpjhjdhT is an optimized version27/03 20:13
faxwow cool27/03 20:13
lpjhjdhhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24450#a2445127/03 20:14
lpjhjdhand the proposition I'm trying to show is: T≡f₀ : (i j k : ℕ) → T i j k ≡ f₀ i j k27/03 20:15
lpjhjdhwhich follows from induction on k27/03 20:15
lpjhjdhf0 is actually an example of a very general class of schedules for affine recurrence equations27/03 20:20
lpjhjdhbut they obviously present unreasonable time complexity so more efficient schedules are needed, usually requiring human ingenuity to discover27/03 20:20
faxI'd never heard of affine recurrence equations before27/03 20:21
faxill probably start seeing them everywhere now :D27/03 20:21
lpjhjdhhaha, that always seems to be how it is27/03 20:22
lpjhjdhit's just a more impressive way of saying an affine equation that depends on itself27/03 20:22
--- Day changed Sun Mar 28 2010
AmadiroGood 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
kmcAmadiro, 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 infancy28/03 09:47
pigworkergood 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 itself28/03 11:02
stevanhi, 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
faxstevan -- you know of Peter Morris' thesis?28/03 12:50
stevanyes28/03 12:50
stevanbut i only glanced thru it.28/03 12:51
faxit seems to be an implementation of the second half of that28/03 12:51
Amadirokmc, Ah, thanks a lot for the answer, very much appreciated.28/03 13:13
HairyDudehttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=2446728/03 14:32
HairyDudetwo lemmas, identical except for their contexts. I can case-split 'pr' to 'refl' in the first, but not the second28/03 14:35
HairyDude(in the comments I meant "case-split" not "refine" btw)28/03 14:36
HairyDudeactually not lemmas, definitions, but you know what I mean28/03 14:38
stevantry giving the typechecker more info; respects : forall {A B : Set} [...]28/03 14:44
pigworkerHairyDude: 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
liyangIs there any point in writing respects eq with eq; … | refl = ? rather than just respects refl = ?28/03 14:49
HairyDudeprobably not28/03 14:50
HairyDudein fact, that works, apart from ambiguous levels28/03 14:50
HairyDudeoutside of the context that is28/03 14:51
pigworkermight be worth trying   with C2 | eq  ; ...  |.C1 | refl  for a laugh28/03 14:52
liyangin fact, respects : (C1 ≡ C2) → Set; respects with eq | C2; respects refl | .C1 = ? works…28/03 14:55
liyangSpot the deliberate mistake.28/03 14:58
HairyDudecompatible {A} {.A} refl _<_ _≤_ = _<_ ⇒ _≤_28/03 15:03
HairyDudemuch easier to work on relations than records...28/03 15:03
HairyDudeis 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
HairyDudefor 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 one28/03 15:13
HairyDudelooks like I do, because the def of monotonicity is incorrect otherwise28/03 15:23
HairyDudehrm. there's no equality defined on Fin28/03 15:31
liyangThere's an Ordering though.28/03 15:35
HairyDudeah, it's in Data.Fin.Props28/03 15:38
HairyDudeif you say "using ()" does that mean "hide everything"? (it's followed by a "renaming" so it's not pointless)28/03 15:40
stevanyes28/03 15:44
guerrillaso, 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
guerrillaSetoid !=< _12 of type Set128/03 16:15
guerrilla:\28/03 16:15
guerrillawhen checking that the expression Nat₌ has type _1228/03 16:15
guerrillaany ideas on why?28/03 16:15
guerrillai'm basically trying to use setoids to emulate Haskell's Eq typeclass functionality...28/03 16:17
HairyDudehave you discovered _≟_ in Data.Nat yet?28/03 16:34
HairyDudeI find Agda's records are too cumbersome to emulate type classes tbh28/03 16:36
guerrillayeah.. hmm, i'll check out _≟_28/03 16:44
HairyDudewho do I send library patches to?28/03 16:56
faxhi byorgey28/03 18:15
byorgeyhi fax28/03 18:16
HairyDudehrm. how to prove x ∉ [ y ] if x ≢ y28/03 20:15
faxI suppose that is equivalent to proving   x in [ y ] -> x = y28/03 20:19
faxwhich is probably trivial from the definitions28/03 20:19
stevandid you solve it HairyDude ?28/03 20:46
HairyDudestevan: solve what?28/03 20:59
HairyDudeI have 11 holes in my source file atm :)28/03 20:59
stevanyour last question. :-)28/03 21:00
HairyDudeah... no28/03 21:03
HairyDudeI can't even see how to prove x ∉ [] :/28/03 21:04
faxwhat's the definition28/03 21:04
faxit's probably just pattern matching with no RHS (via ())28/03 21:05
HairyDudedoh, of course28/03 21:06
HairyDudethanks :)28/03 21:06
stevanhere's both ways: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=24480#a2448028/03 21:06
stevani'm bored.28/03 21:09
faxstevan write a program that turns a number into the sum of (at most) three triangular numbers28/03 21:10
stevansounds like project euler...28/03 21:12
faxno28/03 21:12
IglooWould 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
faxIgloo - yes28/03 21:12
IglooThen what is the advantage of agda? It sounds like writin code in assembly rather than a HLL28/03 21:13
faxIgloo - don't tend to think about it in terms of advantages/disadvantages but Agda has dependent pattern matching and eta conversion28/03 21:13
stevanone can write semi-automatic tactics in agda in agda28/03 21:13
faxstevan, both coq & agda have this poincare principle28/03 21:14
IglooDoes agda's dependent pattern matching do the same thing as coq's "dependent destruction"/"dependent induction"?28/03 21:19
stevansure, 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
faxIgloo, there's a couple aspects to it28/03 21:20
faxthe theoretical part is the axiom _+ computation_,  you can add the axiom in coq but not the computation28/03 21:20
faxand 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 it28/03 21:21
faxstevan, I wouldn't say 'better programming language'28/03 21:21
stevanwasn't there a dependent pattern matching extension to coq recently added?28/03 21:22
faxmost nontrivial coq developments have some approximations of dependent pattern matching in them28/03 21:23
faxwe're basically redoing the same stuff again and again :|28/03 21:24
faxequations is really nice but coq still lacks the theory part I said above28/03 21:24
HairyDudeI really hate it when case-split gives you invalid clauses28/03 21:24
stevanIgloo: http://www.reddit.com/r/dependent_types/comments/b0vb7/agda_vs_coq_by_wouter_swierstra_with_some_input/28/03 21:28
IglooThanks!28/03 21:29
faxwhat I am mostly wondering is once we have  eta, K and quotients.. will that be _enough_?28/03 21:30
kosmikusenough for what? :)28/03 21:31
faxpresumably there will be some point where we can just do everything in a sensible way28/03 21:31
stevanwhat's K?28/03 21:32
faxstevan I mean axiom K, which lets you do (full) pattern matching, JM equality, proving identities identical or some other stuff like dependent pair elimination28/03 21:33
faxI didn't phrase that last one correctly actually not sure how to put it other than formally28/03 21:34
faxstevan, we can get all this stuff just by having proofs convertibly equal.. for some reason coq doesn't though :/28/03 21:34
HairyDudeyou mean dependent sums?28/03 21:36
faxyeah28/03 21:36
stevanwhat is it that ssreflect provides to its user?28/03 21:42
faxstevan - I read a few papers on ssreflect and still have no clue -- what's great is what they're using it for tohugh28/03 21:47
faxthough*28/03 21:47
stevanthe 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
faxIgloo - I think it's because us lot are just into the new stuff :P28/03 22:15
faxalthough coq is pretty old.28/03 22:15
faxbut I don't think it says anything bad about Isabelle28/03 22:15
IglooOh, "dependent types" rather than "theorem proving". Maybe that's why28/03 22:16
stevani don't really like the reddit situation, there are too many subreddits...28/03 22:17
faxstevan yeah I don't really get it28/03 22:18
stevanand most of them are dead...28/03 22:18
Adamantpeople create further subreddits because higher level subreddits start to suck28/03 22:32
Adamantand in general, the suck rises as you go up the chain28/03 22:32
faxit'd be nice to have all the stuff categorized somehow28/03 22:33
faxrather than just in a random list28/03 22:33
stevanbut 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
Adamantit would, but who determines the categorization would be a battle in itself28/03 22:34
faxI wish jbapple still blogged he wrote some cool stuff28/03 22:34
faxMathnerd314 -- you know we were talking about termination and the hydra thing?28/03 22:51
Mathnerd314sometime long ago, yes28/03 22:52
faxit's called Goodstein sequence28/03 22:52
faxdidn't know that28/03 22:52
--- Day changed Mon Mar 29 2010
Amadirohmm.. I was going to ask a question, but by typing it out I figured it out... :)29/03 00:00
AmadiroI should try that more often.29/03 00:01
HairyDudebleh. case-split is causing stack overflows now.29/03 00:38
HairyDudetheorem proving uses a lot of memory :/29/03 00:41
Saizanwell, agda in general uses a lot of memory, ime :)29/03 00:45
Saizani should remember to switch back to 32bit29/03 00:45
HairyDudehey, are there any plans to parallelise agda?29/03 00:47
HairyDudeSaizan, ooh, that might be an issue, yes29/03 00:48
HairyDudesheesh. just giving one goal takes forever now29/03 00:48
Saizansometimes splitting your code into different modules helps29/03 00:50
Saizanso it doesn't retypecheck what you don't change29/03 00:50
HairyDudemmm29/03 00:51
HairyDudein fact, what I'm doing now is pretty much independent of the other stuff, so that would be a good idea29/03 00:51
HairyDude"end of file during parsing" - weird29/03 00:51
Saizanforgot the module header, maybe?29/03 00:52
HairyDudethis is the module I've been working on all day29/03 00:52
HairyDudeweird. new module, I'm getting "ambiguous name refl" even though it's only exported from one place29/03 00:57
HairyDudes/exported/imported/29/03 00:57
HairyDudeah, no it isn't29/03 00:58
HairyDudeend of file error is caused by stack overflow, apparently29/03 01:03
HairyDudeLet's see if I can cheat. Has anyone written a partiton function for Vec?29/03 01:04
AmadiroI'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
HairyDudeAmadiro: no. there are pragmas that let the compiler know that ℕ is natural numbers, so it can optimise29/03 01:06
AmadiroHairyDude, Ah, I guessed something like that would be possible, thanks :)29/03 01:07
HairyDudeactually... yes, that definition will be, but the actual libraries use primitive functions. I think.29/03 01:07
HairyDudeI don't know much about the internals of Agda so I might be wrong on that.29/03 01:08
faxAmadiro??29/03 01:09
AmadiroAnother 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
faxpeano numbers are slow yes29/03 01:09
faxAmadiro nobody is seriously going to use peano numbers for computing things........29/03 01:09
HairyDudeAmadiro: succ is primitive29/03 01:09
Amadirofax, yeah, I was just wondering.29/03 01:09
faxAmadiro the reason we have peano numbers is they are fundamental object in inductive proofs29/03 01:09
AmadiroHairyDude, hm, ok, thanks.29/03 01:09
Amadirofax, yeah.29/03 01:10
HairyDudeAmadiro: the natural numbers are constructed from the constructors zero and suc29/03 01:10
faxAmadiro -- you can implement binary numbers of whatever they are more efficent29/03 01:10
faxAmadiro or you can axiomatize something like gmp integers and use them via haskell ffi29/03 01:10
AmadiroRight, I'll need to get a hang on dependent typing first, but thanks a bunch for the info :D29/03 01:10
HairyDudelooks 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
faxAmadiro, you can worry too much about 'efficency' in an attempt to be pragmatic29/03 01:12
faxHairyDude -- example for what29/03 01:12
fax?29/03 01:12
Amadirofax, yeah, I'm not really worrying about efficiency, I was just wondering.29/03 01:12
faxokay29/03 01:12
AmadiroTrying to get an idea of what the compiler will do with the input, etc.29/03 01:12
HairyDudefax: something that has lots of cumbersome proof terms (the first order part) that have no computational content and so can be stripped using realisability29/03 01:13
pigworkerHairyDude, treesort?29/03 01:13
faxrealisabiility?29/03 01:14
faxdoes agda do that??29/03 01:14
HairyDudeno, I'm just using agda to get the program right, and apply realisability by hand29/03 01:15
HairyDudeI suspect minlog does it, btw29/03 01:15
faxoh cool29/03 01:15
faxhow do you apply this by hand29/03 01:15
HairyDudejust strip out the first order part, you end up with a Haskell-like program :)29/03 01:16
faxokay29/03 01:16
HairyDudewell, it's more complex than that, but I can't be bothered to explain it right now.29/03 01:16
faxuh ok29/03 01:16
faxnice having you29/03 01:17
HairyDudeoh... latest mailing list post, apparently termination checking takes a long time. maybe I'll turn it off and see what happens29/03 01:18
HairyDudenope, didn't work29/03 01:21
HairyDudepigworker: I don't know treesort, and don't really have time to learn it29/03 01:21
HairyDudemerge sort maybe29/03 01:22
pigworkerHairyDude, what makes you think you don't know treesort, when you do know quicksort?29/03 01:22
HairyDudepigworker: because I don't know the name? :)29/03 01:24
pigworkerTreesort is build-binary-search-tree, then flatten; which is effectively what quicksort does.29/03 01:24
HairyDudeah, right29/03 01:25
HairyDudeoh, 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 fix29/03 01:26
pigworkerI don't know any good examples of well-founded recursion.29/03 01:27
faxpigworker - I write your unification program into coq one breaktime that was fun -- it is kind of stunning how it works29/03 01:28
faxoh and I think Saizan will have maybe done the proofs too, in Agda29/03 01:28
faxbut maybe I misremember29/03 01:28
fax(talking of well founded recursion)29/03 01:31
faxor lack of29/03 01:31
pigworkerfax, 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
faxhehe29/03 01:33
pigworkerhairydude, 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 explanation29/03 01:41
HairyDudethis stuff? http://www.cs.st-andrews.ac.uk/~rd/publications/29/03 01:50
pigworkerHairyDude: yeah, the stuff with Luis Pinto; the implicational fragment is tiny29/03 01:56
pigworkernight all29/03 02:05
Amadirofax, thanks again for telling me about peano numbers, I worked through the wikipedia article, and feel slightly more enlightened :)29/03 02:07
AmadiroI actually never read about his axioms before.29/03 02:08
faxit'sreally cool stuff ;)29/03 02:10
AmadiroIt is, and simple enough for me to grasp as well :)29/03 02:11
HairyDudesigh. termination checker can't see that suc n < suc (suc n)29/03 02:26
HairyDudeor... no, that y :: xs < x :: y :: xs29/03 02:27
guerrillaagain.. what are these qoutients that people keep mentioning?29/03 13:13
faxguerrilla do you know setoids29/03 13:13
guerrillai'd like to think i do. trying to work with them now actually29/03 13:14
guerrillathey are related i take it?29/03 13:14
faxinstead 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 y29/03 13:15
faxyou could form the quotient type S/~ and then a function S/~ -> S'/~' must satisfy that 'morphism' relation29/03 13:15
faxso 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 equal29/03 13:16
faxthis is a better explanation http://www.e-pig.org/epilogue/?p=31929/03 13:21
guerrillai see29/03 13:27
guerrillaok29/03 13:27
guerrillathanks29/03 13:27
* guerrilla will look into that link29/03 13:27
stevancool: http://code.haskell.org/Agda/test/succeed/TestQuote.agda29/03 17:56
faxquoteGoal and quote are built in?29/03 17:58
stevanseems so29/03 17:59
faxthat's cool that'll be really useful29/03 17:59
stevani 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
faxohhhh29/03 18:08
faxit gives TEXT instead of syntax that's weird29/03 18:08
faxO_O29/03 18:08
faxyeah that is a little bit less useful than i thought29/03 18:09
stevantyped agda terms inside agda would be hard, no?29/03 18:15
faxyes29/03 18:15
stevanwould untyped be enough for this purpose tho?29/03 18:17
faxyes29/03 18:17
faxa lot better than strings29/03 18:17
faxthe way I'd like to quote stuff is for agda to invert the interpretation function29/03 18:18
faxthis would be part of type inference, hopefull29/03 18:18
faxhopefully29/03 18:18
stevanthis patch was just pushed, perhaps they will improve it soon29/03 18:18
uoryglI think it's once again time to download Agda and prove the Fundamental Theorem of Algebra.29/03 21:13
faxumm29/03 21:14
faxyou're kidding29/03 21:14
faxdo you know what the fundametal theorem of algebra IS?29/03 21:14
--- Day changed Tue Mar 30 2010
uoryglAre Agda's Haddock docs available online somewhere?30/03 17:24
stevanfax: seen todays patches? http://code.haskell.org/Agda/test/succeed/Reflection.agda :-)30/03 17:31
kosmikuslooks promising30/03 17:34
uklI 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 secs31/03 16:33

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