--- Log opened Mon Dec 01 00:00:54 2008
--- Day changed Tue Dec 02 2008
* Smerdyakov has a hard time coming up with good examples distinguishing Agda from Coq.02/12 21:05
SmerdyakovI have examples of pattern matching on terms in inductive types with indices that have structure; I have a simple K example; and I have an inductive-recursive definition.02/12 21:05
vixeyI did a comparison02/12 21:06
vixey if you like02/12 21:07
vixeyit's a universe of types then a view defined on them02/12 21:07
vixeyit's orders of magnitude easier in Agda ..02/12 21:07
vixey(basically typed out from Peter Morris Universes papers)02/12 21:09
Smerdyakovvixey, what does this development "do"?02/12 21:12
vixeyit typechecks :)02/12 21:12
SmerdyakovBut why should I care?02/12 21:12
* vixey thinks it's a good example that distinguished Agda and Coq, the idea in the paper is that you can do generic programming over inductives or inductive families in this way02/12 21:14
vixeySmerdyakov, (I posted it because you seemed to be looking for examples like that .. maybe I mixed up what you meant?)02/12 21:18
SmerdyakovI'm still trying to understand what is going on in it.02/12 21:18
SmerdyakovSo you build up this machinery and only put it to use in converting between representations of naturals?02/12 21:20
vixeyyes02/12 21:20
vixeywell it doesn't really convert between representations02/12 21:21
vixeyit's just that the names like “succ” get unfolded02/12 21:21
vixeyI think it's possible to make an intepretation into 'real' agda types and write generic programs over them though02/12 21:23
--- Day changed Wed Dec 03 2008
-!- jfredett_ is now known as jfredett03/12 05:03
* Smerdyakov is failing again to get Agda built on a different machine, after spending a few hours on it. :(03/12 15:44
SmerdyakovI think Agda needs a lot more documentation on building, to the point where it seems fair to consider that there hasn't yet been a "real" public release.03/12 15:46
stevanthey updated the documentation on building yesterday03/12 15:56
stevan 15:57
SmerdyakovThose instructions are, to me, obviously insufficient.03/12 15:59
SmerdyakovConfiguration fails because of missing packages.03/12 15:59
SmerdyakovIn general, I refuse to use packages that need more than one command line to install.03/12 16:00
SmerdyakovUnfortunately, I already committed to doing an Agda demo in class today. :P03/12 16:00
SmerdyakovWhat the heck.... somehow I ended up with an old Cabal version.  I followed the download link from the first Google hit.03/12 16:09
vixeyI did that too03/12 16:09
vixeythat's why I had the wrong zlib version03/12 16:10
vixeyso I patched it and gave the author a patch and he was like: " I fixed this last year"03/12 16:10
SmerdyakovHaskell is such a mess.03/12 16:10
vixeyso is Agda ...03/12 16:18
vixeyhave you read tried to the source code? :p03/12 16:19
SmerdyakovNo.03/12 16:19
LaneyI swear I just did "cabal install" to install agda03/12 17:45
Laneythen added the load path to my .emacs file03/12 17:45
Laney(obviously this requires the right cabal)03/12 17:45
kosmikussame here03/12 18:35
--- Day changed Thu Dec 04 2008
--- Day changed Fri Dec 05 2008
--- Day changed Sat Dec 06 2008
--- Day changed Sun Dec 07 2008
--- Day changed Mon Dec 08 2008
--- Day changed Tue Dec 09 2008
--- Day changed Wed Dec 10 2008
--- Day changed Thu Dec 11 2008
--- Day changed Fri Dec 12 2008
ksf Warning: -fallow-undecidable-instances is deprecated: use -XUndecidableInstances or pragma {-# LANGUAGE UndecidableInstances#-} instead12/12 14:43
ksfFailing due to -Werror.12/12 14:43
ksfoh, come on.12/12 14:43
* ksf gives up installing agda via portage12/12 14:44
vixeyyeah get the darcs repo and compile it12/12 14:50
vixeyall the automatic installer stuff is broken12/12 14:50
kosmikusksf: does portage have an up-to-date version anyway?12/12 14:58
kosmikusthe last release of agda was ages ago12/12 14:58
ksfthere's a darcs package, but it seems to pull a tagged version.12/12 14:59
--- Day changed Sat Dec 13 2008
-!- jfredett_ is now known as jfredett13/12 04:26
--- Day changed Sun Dec 14 2008
kosmikusok, let's continue here then ;)14/12 18:59
mmorrowheh14/12 18:59
SamBwhat do you know, there is one14/12 19:00
mmorrowso i'm trying to get started and want to eval something (anything) in the interpreter (agda -I)14/12 19:00
kosmikusyou need to import a module for natural number literals to be available14/12 19:00
mmorrow(w/ loading any files at first)14/12 19:00
mmorrowkosmikus: ah, ok.14/12 19:00
mmorrowso there's not something like a Prelude or equiv then i take it14/12 19:01
SamBum ... why are you using that thing ?14/12 19:01
kosmikusbasically the only thing that's predefined is Set14/12 19:01
kosmikusand of course you can type in closed terms14/12 19:01
kosmikus\ x -> x14/12 19:01
kosmikus(\ x -> x) Set14/12 19:02
SamBare you going to be using a library ?14/12 19:02
mmorrowperfect! that's what i wanted. to successfuly eval at least one thing. :)14/12 19:02
SamBand ... what about Emacs ?14/12 19:03
mmorrowSamB: that's the next step. i want to eventually get to where i can ffi import haskell function and write (say) an echo server in Agda14/12 19:03
mmorrow;)14/12 19:03
SamBhuh14/12 19:03
mmorrowoh yes14/12 19:03
SamBhow do you prove things with Haskell functions in the picture14/12 19:03
SamB?14/12 19:04
mmorrowSamB: well, if i have to sacrifice some things to write an echo server, then so be it14/12 19:04
kosmikuswell, you can assume some behaviour14/12 19:04
kosmikusthere's no problem in proving things14/12 19:04
mmorrowi could still have isolated parts of the code which aren't "infected"?14/12 19:04
kosmikusthe question is whether they're actually ture14/12 19:04
kosmikuss/ture/true/14/12 19:04
mmorrowheh, yeah.14/12 19:05
SamBkosmikus: oh ?14/12 19:05
kosmikusSamB: you can postulate functions in Agda, for example14/12 19:05
SamBI wish haddock comments COULD be given for instances ...14/12 19:05
kosmikushm? is this related?14/12 19:05
SamBI often wish to READ such14/12 19:05
* mmorrow looks over the example code and reads a few tutorial14/12 19:06
* SamB is pulling and was talking about this patch:14/12 19:10
SamBFri Jul 18 11:01:53 EDT 2008  Liyang HU14/12 19:10
SamB  * fixed documentation for Haddock 0.814/12 19:10
mmorrowwhat's the type of Set? like as in # in Cayenne.14/12 19:28
mmorrow(\(x : ?) -> x) Set14/12 19:28
SamBMain> :typeOf Set14/12 19:30
SamBSet114/12 19:30
mmorrowoh nice. thx14/12 19:31
SamBI tried :t but there were 3 commands that matched ;-P14/12 19:31
mmorrowheh14/12 19:32
mmorrowcool, so    #_i === Set_(i-1) , i `elem` [1..]14/12 19:35
mmorrow(where #_i is the equivalent Cayenne concept)14/12 19:35
* SamB wonders if agda has stopped inappropriately using the *ghci* buffer yet14/12 19:49
kosmikuswhat's inappropriate?14/12 19:58
mmorrowis an expression of type (x' : x) -> x possible to write with a let expression alone? (i haven't figured out how to get where-expressions working at the prompt yet)14/12 20:04
vixeyhey what's going on in here?14/12 20:04
mmorrowvixey: hey vixey14/12 20:04
mmorrowi just built agda14/12 20:04
vixeymmorrow you should try the emacs mode14/12 20:04
mmorrowvixey: i would if i didn't use vim (well, yi now sorta)14/12 20:05
SamBwell, it's more of an Agda UI than an Emacs mode IMO14/12 20:05
SamBor rather, the Agda UI14/12 20:05
vixeyit's the agda UI ...14/12 20:05
vixeyyeah14/12 20:05
vixeynobody is writing a different one14/12 20:05
mmorrowhmm, ok. i should try that.14/12 20:05
vixeyexcept I think you can get vim syntax coloring from the agda binary..14/12 20:06
vixeynot sure how but iirc that is at least possible14/12 20:06
mmorrowcool14/12 20:06
SamBwhy isn't the UI written in Agda ;-P14/12 20:06
mmorrowdo either of you know how to write a one-liner expression of type (x' : x) -> x (assuming only basic syntax and Set{0..})?14/12 20:06
vixeyyeah just \(x' : x) -> x'14/12 20:07
mmorrow\(x':x) -> x14/12 20:08
vixeyno14/12 20:08
mmorrowlet f : (t : Set1)(x : t) -> t; f (x:t) = t in f Set14/12 20:08
mmorrowthat doesn't work though14/12 20:08
vixeyyou must put lots of spaces in14/12 20:08
mmorrowhmm14/12 20:08
mmorrowit says that `t' isn't in scope though14/12 20:08
mmorrowi think i can't pattern match on the type in "f (x:t)"14/12 20:09
* mmorrow reads more14/12 20:09
vixeyf : (t : Set1)(x : t) -> t14/12 20:10
vixeyf t x = x14/12 20:10
mmorrowohhh14/12 20:10
vixeyf : {t : Set1} (x : t) -> t14/12 20:10
vixeyf x = x14/12 20:10
mmorrowah, nice14/12 20:10
vixeyf : (t : Set1)(x : t) -> t14/12 20:11
vixeyf = \(t : Set1)(x : t) -> x14/12 20:11
mmorrownice14/12 20:11
mmorrowMain> let f : {t : Set2}(x : t) -> t; f x = x in f Set14/12 20:11
mmorrowSet14/12 20:11
mmorrowexactly what i wanted to do :)14/12 20:12
vixeyI realy hate this Set1 Set2 crap..14/12 20:12
mmorrowi guess it has to be so for soundness14/12 20:12
mmorrow(or so i've read, but i don't know the precise argument)14/12 20:13
vixeythe alternative is to write Set everywhere and have the computer place numbers on them14/12 20:13
mmorrowah, yeah14/12 20:13
mmorrowi believe cayenne does that14/12 20:13
vixeyanyway that's not in Agda so..14/12 20:13
mmorrowCayenne uses # for Set14/12 20:13
mmorrowooh, i think i messed that up before14/12 20:14
mmorrowno, # := #_114/12 20:14
mmorrow#_i === Set_(i-1) , i `elem` [1..]14/12 20:14
vixeyI had a brief look at Cayennes implementation14/12 20:15
mmorrowbut i think you just always type # (i haven't used Cayenne enough to know if you ever have to be explicit about which # you're using)14/12 20:15
mmorrowvixey: what'd you think of it?14/12 20:15
mmorrowi've looked over the code a bunch. neat.14/12 20:15
vixeyyou can tell they were having fun hacking when they wrote it :)14/12 20:16
mmorrowheh14/12 20:16
mmorrowi bet14/12 20:16
SamBokay, library-test is failing14/12 20:20
vixeyis that like make test?14/12 20:21
SamBvixey: maybe!14/12 20:21
vixeyhey SamB14/12 20:24
vixeyyou were doing something with explicit substitutions in Agda right?14/12 20:24
SamBwas I?14/12 20:25
vixeyI guess I made it up then14/12 20:25
SamBeither that or I didn't know what I was doing14/12 20:25
mmorrowthere needs to be an agda evalbot for sure14/12 20:25
vixey 20:25
vixey 20:27
SamBoh, maybe I was then ;-)14/12 20:30
vixey;p14/12 20:30
vixeymmorrow but it's a bit awkward with the multiline definitions14/12 20:31
SamBbut just saying "explicit substitutions" somehow made me think of the rewrite tactics in Coq ;-)14/12 20:31
vixeylike I think most code is a few lines long with pattern matches?14/12 20:31
vixeyCoq is giving me a sore arm :/14/12 20:32
vixeyholding left control for so long14/12 20:32
vixeywell proof-general not Coq14/12 20:32
mmorrowvixey14/12 20:32
vixeyyes?14/12 20:33
mmorrow: it should be doable though as long as you can put semis in between stuff14/12 20:33
mmorrowto stick it on one line14/12 20:33
mmorrowor else i guess you'd have to use some illegal/appropriate char to denote a linebreak for the purpose of the bot14/12 20:34
mmorrowthen preproc the incoming string14/12 20:34
SamB¶?14/12 20:39
vixeymmorrow, hey14/12 20:41
vixeythat timber thing is in haskell right14/12 20:41
vixeyyou could hook it up with agda14/12 20:41
vixeyfor doing the server14/12 20:42
vixeybut proving things in Agda ... ? how do you do it14/12 20:42
vixeyI mean just writing out huge proof terms is not really a good way14/12 20:42
mmorrowyeah, timber's in haskell14/12 20:43
vixeyother methods than reflective proofs?14/12 20:43
mmorrowthat's an interesting thought. what do you ave in mind when you say "hook it up" to agda?14/12 20:44
mmorrowlike as in, what part do you see as being the part that agda would be the best use for?14/12 20:46
mmorrow*to use for14/12 20:47
vixeyI don't really know it just occured to me14/12 20:47
vixeyI don't really program anything in Agda actually14/12 20:47
mmorrowvixey: me neither yet ;)14/12 20:47
mmorrowvixey: i want to as an experiment write something along the lines of an echo server (the important part being communicating over the network) in agda to see if i'd want to use agda for such things. (and along the way learn agda)14/12 20:50
mmorrow(and to see the extent to which writing such a thing in agda defeats the purpose of using the languge in the first place)14/12 20:52
mmorrowor if at all14/12 20:52
mmorrow*or if it defeats the purpose at all14/12 20:53
mmorrowhow would one get across that this is well-typed?14/12 22:15
mmorrowmap typeOf (2 :: 4 :: [])14/12 22:15
mmorrowi tried annotations in various places (in agda -I), but came up with syntax errors14/12 22:16
mmorrow(ignoring the fact that that would better be done another way)14/12 22:17
mmorrown/m14/12 22:17
vixeytypeOf ??!14/12 22:19
vixeyis that a function14/12 22:19
mmorrowvixey: yeah, it's in examples/lib/Prelude.agda14/12 22:26
mmorrowi'm currently assembling my stdlib14/12 22:26
mmorrowMain> 41 + 114/12 22:29
mmorrow4214/12 22:29
vixeyyou got the actual stdlib?14/12 22:29
vixeyof Agda14/12 22:29
mmorrowMain> pi14/12 22:29
mmorrow3.14159265358979314/12 22:29
mmorrowi had to define pi14/12 22:29
mmorrowvixey: kinda. i took everything under examples/lib/ and am picking out what i want and making a "personal" stdlib14/12 22:30
mmorrow:)14/12 22:30
mmorrowplus adding stuff that i want that isn't there14/12 22:30
mmorrowvixey: 22:32
mmorrowtypeOf is in there14/12 22:32
mmorrowlooks like i'll have to figure out how to add Agda syntax highlighting to hpaste2 now14/12 22:32
mmorrow 22:33
mmorrowvixey: oh, and re: Set_i, looks like there's a flag to14/12 22:35
mmorrow--type-in-type          ignore universe levels (this makes Agda inconsistent)14/12 22:35
mmorrowbut..14/12 22:35
vixeyomg that was frustrating I couldn't find this thing14/12 22:35
vixey 22:35
vixeyThis is the one I meant though14/12 22:35
mmorrowwhoa14/12 22:35
mmorrownice14/12 22:35
* mmorrow looks14/12 22:35
vixeyIT's got some very interesting dependently typed things14/12 22:35
mmorrowvery cool. that's gonna save me a ton of work :)14/12 22:36
vixeyI want it to act like type-in-type but also topological sort the types (or give a universe inconsistency error)14/12 22:36
mmorrowinteresting. do you know yet if it's possible to infer the levels of types or under what conditions it is?14/12 22:37
mmorrowbecause it'd be great if it was14/12 22:38
vixeyso if you have this term14/12 22:39
vixeyfoo x = f x Set (g Set) h x14/12 22:39
vixeyyou can just put a fresh name to each one14/12 22:39
vixeyfoo x = f x Set[#g0] (g Set[#g1]) h x14/12 22:39
vixeythen as you typecheck you build up a bunch of constraints like,  { #g0 < #g7, #g3 < #g1, ... }14/12 22:39
mmorrowah i see14/12 22:40
mmorrowthen topo sort and voila14/12 22:40
vixeyso it's always decidable if there is a mapping from there to the nats that make the (<)'s true14/12 22:40
mmorrowcool14/12 22:40
mmorrowthat'd be interesting too if you allowed a /partial/ ordering on the #g_i (i'm not sure what this would mean off the top of my head)14/12 22:42
SamBisn't that what vixey just said though ?14/12 22:43
mmorrowSamB: i'm trying to figure that out14/12 22:43
mmorrow(i'm not sure)14/12 22:44
SamBthose constraints form a partial order relation, do they not ?14/12 22:44
SamBI mean, when the code is right ;-)14/12 22:45
mmorrowto clarify (to make sure we're using the same defs), i'm using totally ordered as in Z (or N), and partially ordered as in C (complex nums)14/12 22:45
SamBhuh, and I was thinking partially ordered like modules that aren't allowed to recursively import eachother ...14/12 22:46
mmorrowheh14/12 22:46
mmorrowyeah, so a partial odering would be a dag14/12 22:46
mmorrowso i guess the fact that she's topologically sorting things means that she's talking about a partial ordering14/12 22:47
SamBmmorrow: what did you define pi to be ?14/12 22:48
mmorrowbut since Set_i is indexed by N, which is not a dag (well, a trivial on), but has a total ordering14/12 22:48
mmorrowi'm confused14/12 22:48
mmorrowSamB: i just used ghci> pi::Double14/12 22:48
mmorrowand copy/pasted14/12 22:48
SamBthat doesn't sound too good somehow14/12 22:48
mmorrowapparently agda's using ghc's Double, so that's the best you can do14/12 22:49
mmorrow{-# BUILTIN FLOAT   Float  #-}14/12 22:49
SamBam I the only one who doesn't see how that's useful ?14/12 22:49
mmorrowtype Float = Prelude.Double14/12 22:50
mmorrowSamB: yes :)14/12 22:50
mmorrowwhat if i wanted to code up a FFT in agda?14/12 22:50
vixeydo you know Fin?14/12 22:50
mmorrowvixey: i saw that module, but didn't look at it yet14/12 22:50
SamBmmorrow: you can't say yes, you could say no if you didn't either though14/12 22:50
mmorrowheh14/12 22:51
vixeymmorrow, with total correctness proof?14/12 22:51
SamByou can't code correct FFT with floating point can you ?14/12 22:51
vixeyif not .. just like you would in haskell I gues...14/12 22:51
mmorrowvixey: that'd be cool14/12 22:51
vixeySamB: well somebody did it 22:51
mmorrowSamB: the correctness isn't at the level of rounding14/12 22:51
SamBmmorrow: um, I beg to differ!14/12 22:52
mmorrowSamB: and anyone using floating point for numerical analysis (which is everyone) always bounds their error14/12 22:52
SamBokay, I suppose that's good enough, but how are you going to prove stuff like that using native floats ???14/12 22:52
vixeyFin 0 has no elements, Fin 1 ~ (), Fin 2 ~ Bool, Fin 3 ~ Either () (Either () ()) ...14/12 22:53
mmorrowSamB: i don't know14/12 22:53
vixeyFin n ~ { i : nat | i < n }14/12 22:53
mmorrowSamB: also, i'm assuming that i'd actually use agda to /execute/ the fft as well14/12 22:53
mmorrowwhich would suck if it was realllllly slow14/12 22:54
mmorrowanyhow, i just threw that out there. i haven't really thought about it14/12 22:54
* mmorrow looks at Fin14/12 22:56
SamBhmm, perhaps holds the answer14/12 23:05
SamB(total coincidence that I bumped into it -- I was just correcting stuff in vicinity of C-CoRN ...)14/12 23:05
mmorrowinteresting14/12 23:07
vixeySamB, do you work in C-CoRN by the way?14/12 23:09
SamBnot really14/12 23:09
SamBthe thing I tried to use it for seems to be really hard ...14/12 23:09
vixey"Our high-level formalization of floats: pairs" lol14/12 23:10
vixeywhat was that?14/12 23:10
SamBperhaps impossible ?14/12 23:10
SamBI was trying to lift a ring structure pointwise14/12 23:11
vixeyI don't know what that means :(14/12 23:11
SamBinstance Num n => Num (a -> n)14/12 23:12
SamBonly, you know, with the ring axioms carrying over too ;-)14/12 23:12
vixeyoh14/12 23:13
vixeyit's const?14/12 23:13
SamBwhat the ?14/12 23:13
vixey9 gets lifted to const 9 ?14/12 23:13
SamBoh, sure14/12 23:13
vixeywith x + y = \o -> x o + y o14/12 23:13
SamBbut I was trying to lift the structure, not the elements14/12 23:13
* vixey I guess I really don't understand14/12 23:13
SamBactually you seem to have it14/12 23:14
SamBbut I was having trouble with some stuff trying to do it with equivalence as the primitive, so I decided to try the apartness-as-primitive approach14/12 23:15
vixey(=) is a tricky thing14/12 23:16
SamBbut then I couldn't find a way to represent apartness that satisfied the ... er ... cotransitive property without requiring something of the argument type14/12 23:17
SamB 23:18
vixeyI haven't read about how setoids work yet14/12 23:20
SamBwhere ?14/12 23:20
vixeyanywhere14/12 23:20
SamBbasically, it's a first-class equivalence relation14/12 23:21
SamBhmm, make test fails too :-(14/12 23:22
* mmorrow just figured out how to import arbitrary haskell functions. <sys/socket.h>-via-haskell-ffi-via-agda-ffi here i come14/12 23:50
* mmorrow meant here he comes14/12 23:51
vixeyhehe14/12 23:51
vixeyyou know the IO definition as a GADT and as a Cont IOTree?14/12 23:51
vixeydo you think you will do it like that?14/12 23:51
vixeyI guess there are already some monads in the stdlib but14/12 23:52
mmorrowi do. the first time i saw the IOTree def was the other day, but it makes sense i guess.14/12 23:52
mmorrowvixey: yeah, i'm not sure how i'm gonna do it yet.14/12 23:52
mmorrowIO.agda is pretty minimal14/12 23:52
mmorrowand IO could always be split up into Net, Disk, ... (whatever)14/12 23:54
mmorrowvixey: have you seen IOSpec? it's pretty cool.14/12 23:54
vixeyhave seen the papers about it14/12 23:54
mmorrowoleg's ZFS is cool as well14/12 23:55
vixeyI wish I could stay on a bit but I have to go14/12 23:55
vixeylater14/12 23:55
mmorrowvixey: oh, check out the code on hackage.14/12 23:55
mmorrowlater14/12 23:55
--- Day changed Mon Dec 15 2008
mmorrowByteString.agda 04:32
-!- kosmikus_ is now known as kosmikus15/12 13:55
--- Day changed Tue Dec 16 2008
--- Day changed Wed Dec 17 2008
--- Day changed Thu Dec 18 2008
--- Day changed Fri Dec 19 2008
--- Day changed Sat Dec 20 2008
--- Day changed Sun Dec 21 2008
--- Day changed Mon Dec 22 2008
--- Day changed Tue Dec 23 2008
--- Day changed Wed Dec 24 2008
--- Day changed Thu Dec 25 2008
--- Day changed Fri Dec 26 2008
--- Day changed Sat Dec 27 2008
--- Day changed Sun Dec 28 2008
--- Day changed Mon Dec 29 2008
--- Day changed Tue Dec 30 2008
--- Day changed Wed Dec 31 2008
--- Log closed Thu Jan 01 00:00:36 2009

Generated by 2.7 by Marius Gedminas - find it at!