liyang vixey vixey --- Log opened Fri May 01 00:00:04 2009 -!- dolio_ is now known as dolio 01/05 01:46 -!- iago is now known as iago_ 01/05 10:29 --- Day changed Sat May 02 2009 -!- iago is now known as iago_ 02/05 10:27 -!- _dolio is now known as dolio 02/05 17:14 -!- byorgey_ is now known as byorgey 02/05 17:20 --- Day changed Sun May 03 2009 -!- Elly is now known as ThreAple 03/05 09:59 -!- ThreAple is now known as THREAPLE 03/05 09:59 -!- iago is now known as iago_ 03/05 11:05 -!- THREAPLE is now known as Elly 03/05 11:31 -!- _dolio is now known as dolio 03/05 15:33 -!- byorgey__ is now known as byorgey 03/05 15:50 --- Day changed Mon May 04 2009 Mmmm... Futurama projections: http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html 04/05 13:07 -!- _dolio is now known as dolio 04/05 20:38 --- Day changed Tue May 05 2009 -!- byorgey_ is now known as byorgey 05/05 02:14 --- Day changed Wed May 06 2009 -!- badtruffle is now known as copumpkin 06/05 02:33 -!- koninkje_away is now known as koninkje 06/05 04:44 -!- koninkje is now known as koninkje_away 06/05 06:10 -!- _dolio is now known as dolio 06/05 09:12 -!- badtruffle is now known as copumpkin 06/05 17:16 -!- _dolio is now known as dolio 06/05 19:58 -!- badtruffle is now known as copumpkin 06/05 20:39 -!- badtruffle is now known as copumpkin 06/05 22:54 --- Day changed Thu May 07 2009 -!- byorgey_ is now known as byorgey 07/05 01:29 -!- byorgey_ is now known as byorgey 07/05 02:58 -!- badtruffle is now known as copumpkin 07/05 04:21 -!- byorgey_ is now known as byorgey 07/05 12:46 -!- byorgey_ is now known as byorgey 07/05 15:34 -!- badtruffle is now known as copumpkin 07/05 17:57 -!- _dolio is now known as dolio 07/05 18:40 --- Day changed Fri May 08 2009 -!- badtruffl is now known as pumpkin_ 08/05 00:29 -!- e__ is now known as vixey 08/05 01:29 -!- badtruffle is now known as pumpkin_ 08/05 05:16 -!- byorgey__ is now known as byorgey 08/05 20:25 --- Day changed Sat May 09 2009 -!- byorgey_ is now known as byorgey 09/05 12:52 --- Day changed Sun May 10 2009 -!- codolio is now known as dolio 10/05 01:03 http://www.iis.sinica.edu.tw/~scm/2009/proof-irrelevance-extensional-equality-and-the-excluded-middle/ 10/05 02:55 you might have already seen this 10/05 02:55 anyone read it? 10/05 04:23 got a question actually 10/05 04:23 nvm 10/05 04:23 how do you install happy? 10/05 04:57 I just got loads of errors.. 10/05 04:57 -!- badtruffle is now known as copumpkin 10/05 17:45 --- Day changed Mon May 11 2009 -!- badtruffle is now known as copumpkin 11/05 00:47 -!- jfredett_ is now known as jfredett 11/05 02:31 -!- badtruffle is now known as copumpkin 11/05 03:21 -!- byorgey_ is now known as byorgey 11/05 20:47 --- Day changed Tue May 12 2009 -!- badtruffle is now known as pumpkin_ 12/05 00:21 -!- badtruffle is now known as copumpkin 12/05 01:56 -!- codolio is now known as dolio 12/05 03:12 -!- badtruffle is now known as copumpkin 12/05 07:11 -!- badtruffle is now known as copumpkin 12/05 17:33 -!- Jerry_ is now known as XOO 12/05 18:42 is there an agda matrix library? 12/05 20:08 yes. but no one can be told about it. 12/05 20:15 you have to see for yourself. 12/05 20:15 ! 12/05 20:16 so it's a profound realization one comes to after playing with agda for a while? then you suddenly have a matrix library? 12/05 20:16 (It was a bad reference to the matrix movie). 12/05 20:17 But there's some stuff in Data.Vec that should be useful. 12/05 20:17 oh :) 12/05 20:22 maybe I'll play around with making a simple one myself to get a feel for the language 12/05 20:22 are there any plans to revive the --interactive mode? 12/05 20:35 I  think it may still work. 12/05 20:35 It's just that it's no longer actively maintained. 12/05 20:36 The emacs mode is quite nice once you get used to it. 12/05 20:36 I'm just not a big fan of emacs in general 12/05 20:37 lets hope somebody makes an agda mode for yi soon :-) 12/05 20:40 -!- iago is now known as iago_ 12/05 21:08 is there a specific way to "install" the standard library 12/05 23:10 ? 12/05 23:10 add to agda2-include-dirs the path to the lib (in emacs  do M-x customize-mode and add to that) 12/05 23:12 agda2-include-dirs where? I'm not using emacs right now... (the only docs I can see mention agda2-include-dirs in .emacs) 12/05 23:20 what os 12/05 23:21 mac os 12/05 23:21 you should get Carbon Emacs 12/05 23:21 not a big fan of emacs :/ 12/05 23:24 I guess I could give in, but I'd prefer not to 12/05 23:24 your being really silly 12/05 23:24 You want emacs. 12/05 23:25 Proving non-trivial things without tool support is a pain. 12/05 23:28 Proving non-trivial things in Agda is a pain :p 12/05 23:29 -!- byorgey_ is now known as byorgey 12/05 23:30 I just want to fool around with it, not do any substantial proving 12/05 23:48 --- Day changed Wed May 13 2009 -!- koninkje1away is now known as koninkje 13/05 04:04 -!- copumpkin is now known as pumpkin 13/05 04:35 how does Monoid in http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Algebra.html#277 enforce associativity? 13/05 04:51 oh, I see 13/05 04:52 http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Algebra.FunctionProperties.html#785 13/05 04:52 whoa, why is C-c C-l running GHC? 13/05 05:21 oh, it's running ghci 13/05 05:22 and it's pegging my CPU 13/05 05:22 wow, it took about a minute at 100% cpu for it to tell me my program was invalid 13/05 05:23 okay, I'm stuck on the most basic of problems 13/05 05:47 anyone around? 13/05 06:11 -!- koninkje is now known as koninkje_away 13/05 06:24 is there something like a "Show instance" in agda? 13/05 06:33 pumpkin: well, all the values can be printed on screen 13/05 06:38 ooh, how? it's not like I don't trust all the dependent magic, but I wanna "see" it! :P 13/05 06:39 pumpkin: just evaluate something 13/05 06:39 also, I couldn't get my main function working without adding some pragmas into haskell 13/05 06:39 into Haskell? 13/05 06:39 oh, you're compiling 13/05 06:39 well, then I don't know if you can print 13/05 06:40 I had main : \forall {A} \r A; main = putStrLn "hello!" 13/05 06:40 I meant IO A 13/05 06:40 where IO came from the IO in the standard library 13/05 06:40 but it complained that putStrLn had type IO \top 13/05 06:40 yes, that's true 13/05 06:40 so if I made main : IO \top, it complained that main had to be IO A 13/05 06:41 it does? 13/05 06:41 let me check 13/05 06:41 for compilation only 13/05 06:41 C-c C-l works fine 13/05 06:41 hmmm 13/05 06:44 user error? :P 13/05 06:44 seems like there are two IO types 13/05 06:45 a "primitive" IO type next to the one that "putStrLn" returns 13/05 06:47 and there seems to be a function "run" converting one into the other 13/05 06:47 ah 13/05 06:50 is there something like "type" for type aliases in agda? I've made a custom matrix type, but it might be easier to work with as a Vec of Vecs 13/05 06:50 Just write a function. 13/05 06:50 oh, good point 13/05 06:51 hmm, actually I thought I knew how to do that :P 13/05 06:55 so I can write a function that takes a type and returns one 13/05 06:56 Yes. 13/05 06:56 Mat : ∀ {n m} → (a : Set) → Vec (Vec a n) m 13/05 06:56 'type Foo f = f Int' would be 'Foo : (Set -> Set) -> Set ; Foo f = f Int'. 13/05 06:57 would that have to be Set1? 13/05 06:57 Which? 13/05 06:58 the last one 13/05 06:58 (Set -> Set) -> Set1 ? 13/05 06:58 or is that different? 13/05 06:58 No. 13/05 06:58 Set : Set1 13/05 06:59 Set1 : Set2, etc. 13/05 06:59 (Set -> Set) -> Set : Set1 as well. 13/05 06:59 how is that : binding there? to the whole expression on the left, or only to the rightmost Set? 13/05 07:00 ((Set -> Set) -> Set) : Set1 13/05 07:01 aha 13/05 07:01 T -> T' : lub K K', where T : K and T' : K', as I recall. 13/05 07:04 looks good 13/05 07:04 If you think of Set3 being an upper bound of Set2 and Set3, for instance. 13/05 07:04 so, sorry for the stupid question, but what would the actual body of such a Mat function be? 13/05 07:05 quantifying over sets increases the universe level, though 13/05 07:05 with the type I wrote above (assuming it makes sense) 13/05 07:05 What do you want your Mat to look like? Mat a m n? 13/05 07:06 Mat n m = Vec (Vec a n) m 13/05 07:06 or something like that? 13/05 07:06 oh, well, Mat A n m = Vec (Vec A n) m 13/05 07:06 Mat : Set -> \bn -> \bn -> Set 13/05 07:07 Yeah, and the type is: Mat : Set -> Nat -> Nat -> Set 13/05 07:07 why does the Set come before the two Nats? 13/05 07:07 Well, whatever order you want. 13/05 07:07 ah ok 13/05 07:07 but it's compatible with Vec then 13/05 07:08 also, Agda encourages parameters to come before indices 13/05 07:08 makes sense 13/05 07:08 Opposite of GHC. :) 13/05 07:09 for Mat a n m = Vec (Vec a n) m I'm getting "left hand side gives too many parameters to a function of type " 13/05 07:09 are you sure you got the right type? 13/05 07:09 Mat : ∀ {n m} → (a : Set) → Vec (Vec a n) m Mat a n m = Vec (Vec a n) m 13/05 07:10 whoops, it stuck them on same line 13/05 07:10 but it doesn't like the Mat definition, given that type 13/05 07:10 not implicit for n, m 13/05 07:10 also, now you got different orders in the type and the def 13/05 07:11 and the type shouldn't mention Vec 13/05 07:11 we gave the type above 13/05 07:11 oh, sorry 13/05 07:11 sometimes I see \forall {...} followed by \r and sometimes it isn't... is there a difference? 13/05 07:13 \r is ->? 13/05 07:13 I guess \r is -> 13/05 07:14 well, there isn't really a difference 13/05 07:14 yeah, sorry 13/05 07:14 When you're listing several named pis in a row, you don't have to put ->. 13/05 07:14 if you have multiple function arguments that have names 13/05 07:14 well, I'm too slow typing compared to dolio :) 13/05 07:14 :) 13/05 07:14 thank you so much! this is fun 13/05 07:14 is there a way to overload operators? Nat already took _+_ but I'd like to use it for Mat too 13/05 07:15 sorry if I sound totally clueless... it's probably because I am :/ 13/05 07:15 pumpkin: only via modules/records 13/05 07:15 Oddly enough, constructors can be overloaded. 13/05 07:15 pumpkin: but since you can locally open modules, it's actually quite ok 13/05 07:15 hmm, so my matrix addition is valid, but uses _+++_ which feels ugly :P 13/05 07:17 you can rename the addition on natural numbers instead if you like 13/05 07:18 oh, I guess that's one option 13/05 07:19 hmm 13/05 07:19 so when you talk about records for overloading, is that a bit like explicitly dealing with haskell's typeclass dictionaries? 13/05 07:19 but basically implementing them in the language itself? 13/05 07:19 yes 13/05 07:20 ooh, fancy :) 13/05 07:20 Kind of the opposite of fancy. :) 13/05 07:22 Aside from the nicer modules and records-as-modules, which is fancy. 13/05 07:22 well, it's fancy that we can do that, but not fancy in that we have to do it ourselves 13/05 07:22 unless there's some kind of fancy first-class typeclass abstraction defined somewhere? 13/05 07:22 what is agda's goal? is there an interest in making it a general-purpose programming language, or is it intended mainly as a theorem prover? 13/05 07:26 like, would putting "practical" Num/Show records in there be useful, or just a distraction 13/05 07:27 well, maybe not Num 13/05 07:27 I see there's lots of nice algebraic structures already 13/05 07:27 The really fancy stuff is in EqReasoning or some such module. 13/05 07:29 how would agda get around the Sum/Product newtypes for Monoid in haskell issue? 13/05 07:30 Relation.Binary.EqReasoning 13/05 07:30 At least, I think that looks cool. 13/05 07:30 yes, it is quite cool 13/05 07:31 http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Relation.Binary.EqReasoning.html#453 can't see much i it? 13/05 07:31 I think the goal of Agda is to be more a programming language than a theorem prover 13/05 07:31 is the PreorderReasoning doing the work? 13/05 07:31 I have to leave now 13/05 07:31 Yeah. 13/05 07:31 cool :) 13/05 07:31 EqReasoning has an example of how to use it, though. 13/05 07:31 thanks for the help :) 13/05 07:32 yeah 13/05 07:32 dammit, I need to go to sleep, but I want to keep playing with this 13/05 07:33 this is making me want to contribute to the standard lib 13/05 07:35 http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Data.Vec.html#740 how does one write a Vec literal using that? 13/05 07:43 1 ∷ 2 ∷ 3 ∷ [] 13/05 07:44 oh 13/05 07:44 what's that _[_]=_ thing? 13/05 07:44 v [ i ]= x is a proof that the ith element of v is x. 13/05 07:45 oh 13/05 07:46 I need to redefine my alias for ℕ. \mathbb{N} is too much work. 13/05 07:47 \bn doesn't work? 13/05 07:47 Does it? 13/05 07:47 does for me, on a vanilla install 13/05 07:47 Ah, nice. 13/05 07:48 whee, I just added a matrix to itself! 13/05 07:48 * pumpkin beams 13/05 07:48 tomorrow, cholesky! 13/05 07:48 :P 13/05 07:48 Make sure you prove it correct. 13/05 07:49 I'm assuming it won't be as simple as saying that chol(A) chol(A)* = A 13/05 07:51 That doesn't look like a proof. :) 13/05 07:51 I was hoping it would do all the work for me :P boo 13/05 07:51 Try Coq, maybe it will. :) 13/05 07:52 I guess it's just a proof assistant after all, not a proof master 13/05 07:52 so coq can do even more than agda? 13/05 07:53 Coq has automatic proving 'tactics' that you use. 13/05 07:53 I must say that compared to haskell, I feel all-powerful now :P but I've only been playing with agda for a little while 13/05 07:53 So, in Agda, when you want to prove something, you give the type of the thing you want to prove, and write down a bunch of equations, like a haskell function. 13/05 07:54 You can write stuff like 'proof input1 input2 = ?' and then say, "split input1 for me" and so on, but you're still figuring out the proof by hand. 13/05 07:54 I see 13/05 07:54 Coq lets you do stuff more like writing down the type of the proof and then saying, "try induction. Okay, we're done." 13/05 07:55 wow 13/05 07:55 And you can write new tactics and stuff. 13/05 07:55 sound awesome 13/05 07:55 * pumpkin sings "a whole new world" from disney's aladdin 13/05 07:56 Yeah, although the Agda way has its charms. 13/05 07:56 I've not really used Coq at all, though. Perhaps I'd feel differently if I had. 13/05 07:56 I wonder if a math prof would accept an agda program as a proof 13/05 07:57 I guess it depends on the math prof 13/05 07:57 I wonder at what point it would make sense to introduce a general _+_ 13/05 08:01 as part of a semiring? 13/05 08:01 oh, I guess they already have that in Algebra 13/05 08:02 ah well, thanks again for all your help :) bedtime now 13/05 08:03 (Oh wow. Activity!) 13/05 08:03 liyang: just me being a noob, nothing to get excited about :P 13/05 08:04 * dolio hits the hay. 13/05 08:06 pumpkin: no, it was good. 13/05 08:08 There needs to be an introduction to the standard library doc somewhere. 13/05 08:08 Anyone want to collaborate? 13/05 08:09 I don't think Nisse wants to write one (nor is he suited to writing an introduction from the perspective of someone who doesn't already know the stdlib) 13/05 08:10 (Oh, also, use the head libs if you can, rather than lib-0.1) 13/05 08:11 liyang: I would love to write some Agda documentation, but time is as always the problem 13/05 12:02 edwinb: ping 13/05 12:02 hello 13/05 12:02 hi there 13/05 12:02 I tried to install Idris 13/05 12:02 yikes ;) 13/05 12:02 what happened? 13/05 12:02 but strangely enough, the binary segfaults 13/05 12:02 weird 13/05 12:02 so you haven't actually seen this before, I guess 13/05 12:03 which ghc? 13/05 12:03 I tested with 6.10.3 and 6.10.2 13/05 12:03 I could also try 6.8.3 13/05 12:03 I'm using 6.10.1 13/05 12:03 6.8 is unlikely to work since I'm using some recent cabal stuff in the build 13/05 12:04 ok 13/05 12:04 it's not unlikely that the actual problem is caused by me using Nix (www.nixos.org) rather than by Idris itself 13/05 12:04 this is the latest darcs version presumably? 13/05 12:04 but I don't generally have segfaulting Haskell programs 13/05 12:05 no, that's usually a bad sign with haskell programs... 13/05 12:05 yes, it's the latest darcs version 13/05 12:05 I don't think it's doing anything at all strange on startup 13/05 12:05 yes, that's what I expected 13/05 12:06 let me test it with 6.10.1 then 13/05 12:06 just reading command line arguments... 13/05 12:06 I'm not really sure where to start here to be honest... 13/05 12:06 I mainly wanted to verify that this isn't a known problem 13/05 12:06 no, it's new to me 13/05 12:07 ok then 13/05 12:07 let me know if you get any clues... 13/05 12:07 I'll let you know, yes 13/05 12:07 edwinb: what's the status of Prefix.hs 13/05 13:09 edwinb: I seem to have it in my darcs checkout, and it seems to be required(?), but it doesn't seem to actually be in the repo ... 13/05 13:09 that's generated by the Makefile 13/05 13:25 it should shortly be superceded by some cabal magic 13/05 13:25 it is an evil hack to get libraries in the right place... 13/05 13:25 hmm, actually, it's not the only evil hack that needs fixing 13/05 13:26 ah, but the Makefile isn't actually called by the cabal file 13/05 13:46 so you can't just build using cabal 13/05 13:46 alas, not yet 13/05 13:50 I see 13/05 13:55 I think the segfault is solved though 13/05 13:55 problem on my side 13/05 13:55 using incompatible library versions 13/05 13:55 aha 13/05 13:59 -!- byorgey_ is now known as byorgey 13/05 15:59 edwinb: ok, I got much further now 13/05 16:29 edwinb: now when I call idris, I get lots of output, and ultimately and index too large error 13/05 16:29 this is good! 13/05 16:30 or rather, now it's my fault 13/05 16:30 you need to give a source file 13/05 16:30 ah, ok 13/05 16:32 I was trying --help 13/05 16:32 but that didn't work well 13/05 16:32 but I'll play some more tonight 13/05 16:32 darcs ivor seems to have a rather funky .cabal file. 13/05 16:34 how so? I'm using the Hackage ivor, and haven't looked at the file. It seemed to just work. 13/05 16:36 It's got some lines with "v v v v v v v" "^ ^ ^ ^ ^ ^ ^" and "*************" on them them. cabal doesn't like the last one. 13/05 16:37 Hackage ivor works, yeah. 13/05 16:37 ok 13/05 16:37 I'll not try darcs then 13/05 16:37 darcs has two different "Build-depends" lines, too. Maybe this is the result of a merge... 13/05 16:39 v v v v v and ^ ^ ^ ^ ^ ^ etc looks like an unresolved merge conflict. 13/05 16:41 kosmikus: yes, helpful things like usage instructions would be nice 13/05 16:41 I think I might take a but of time to make it more usable soon 13/05 16:41 bit of time, even 13/05 16:41 is there a standard location for the standard lib? I have it in my agda search path, but was wondering where people usually put it 13/05 20:45 cocopumpkin: good question. I don't have it in any "standard" location ... 13/05 20:48 there was talk about piggybacking on cabal for agda packages 13/05 20:53 maybe ~/.agda/* somewhere? 13/05 20:53 I remember the talk, but I don't know if there was a conclusion 13/05 20:59 as a matter of fact, I'm not even using the released version of the stdlib right now, but still the darcs repo 13/05 20:59 The patches to the standard library have some amusing descriptions. 13/05 21:06 "Made Everything boring" 13/05 21:06 I like how half the stdlib is rewritting with Set replaced with Set1 13/05 21:07 and it comes up every few days on the mailing list 13/05 21:07 but still nobody really knows a good way to do polymorphism? 13/05 21:07 The Coq way isn't good? 13/05 21:08 better than the Agda way, in any case 13/05 21:10 Certainly. 13/05 21:10 I tend to use --type-in-type 13/05 21:10 -!- koninkje_away is now known as koninkje 13/05 21:58 -!- cocopumpkin is now known as copumpkin 13/05 23:06 how does the compilation work in agda? 13/05 23:19 does it pass through haskell? 13/05 23:19 why are head and tail private in Data.List? 13/05 23:45 --- Day changed Thu May 14 2009 does Nat in the standard lib not have any algebraic structures defined on it? 14/05 00:12 Algebraic stuff seems to be in Data.Nat.Properties. 14/05 00:24 -!- koninkje is now known as koninkje_away 14/05 04:26 would there be a problem with making syntactic sugar for records that looks like haskell typeclasses? 14/05 04:38 what do you mean exactly? 14/05 04:40 sorry 14/05 04:40 well, as I understand it records (among other things) are exposing the dictionary behind typeclasses in haskell 14/05 04:41 but I guess the syntax isn't a big deal really 14/05 04:42 so for simulating typeclass-like constraints on a type, you just ask for that record type? 14/05 04:43 bah, I don't think I'm being very clear, but I don't know the language yet :/ 14/05 04:43 no, it's not clear what you are saying 14/05 04:43 well, on a high level, I'm wondering how I'd do the various things we do with typeclasses in haskell, in agda 14/05 04:44 Not possible afaict 14/05 04:44 There's no way to define any 'open' object 14/05 04:44 oh 14/05 04:44 but you could have similar behavior if you knew all the instances in advance? 14/05 04:44 yes 14/05 04:45 like, a record type definition would be the class ... bit, creating individual records would be the instance ... bits, and requesting the record type in a type signature would be the => constraints? 14/05 04:45 how do you make a record for monad? 14/05 04:52 record Monad (m : Set -> Set) : Set1 where 14/05 04:54 field 14/05 04:54 return : {A : Set} -> A -> m A 14/05 04:54 they have http://www.cs.nott.ac.uk/~nad/listings/lib-0.1/Category.Functor.html#240 in the stdlib 14/05 04:55 it seems like you could do something similar for Monad 14/05 04:55 :/ 14/05 05:01 how do you project out of a record 14/05 05:01 open Monad 14/05 05:03 * vixey has trouble getting implicit parameters to solve enough here 14/05 05:07 * pumpkin is totally clueless 14/05 05:11 about? 14/05 05:12 agda in general :) I just meant that I'm not much use 14/05 05:13 I tried something out based on your idea but agdas implicit parameter solving isn't clever enough 14/05 05:13 I thought it might do a bit of back-propagation though functions (so I could quote types), but it seems not 14/05 05:14 * vixey has a look at Implicit.hs to see if what I wanted is possible 14/05 05:22 where can I find all the cool tricks with implicit parameters 14/05 06:07 I couldn't do what I wanted with it 14/05 06:08 * liyang wishes vixey could lurk moar so he can actually reply to him. 14/05 10:45 * Laney lurks around liyang 14/05 12:38 -!- codolio is now known as dolio 14/05 15:52 hey Laney :3 14/05 16:27 -!- iago is now known as iago_ 14/05 18:02 -!- iago_ is now known as iago 14/05 18:11 oh? 14/05 20:19 did anyone find some more uses of implicit parameters? 14/05 20:19 more than what uses? 14/05 20:24 mostly I have just used it like:  f : {T : Set} -> T -> ... 14/05 20:25 the type checker can resolv trivial proofs that are passed as implicit arguments. 14/05 20:28 can you show me some exmaples of it? 14/05 20:29 http://pastie.org/478359 14/05 20:34 :(( 14/05 20:35 again with the broken formatting 14/05 20:35 hmm 14/05 20:35 this 'is not zero' is good 14/05 20:36 do you know why it fills in ⊥? is it because it has only on constructor, or that it's a record ? or both 14/05 20:36 seems to have to be a record 14/05 20:38 :/// this sucks 14/05 20:45 http://pastie.org/478369 14/05 20:45 that typechecks 14/05 20:45 but if you uncomment it, adding a field to the record ... it doesn't typecheck 14/05 20:45 can't do what I wanted 14/05 20:48 I wonder why my code doesn't typecheck when the record has a field, should it really not? 14/05 20:56 It checks, but it doesn't know what to fill in. 14/05 21:04 For "record Q (T : Set) : Set where", all values are eta equal to each other, so it's trivial what it has to fill in, "record {}". 14/05 21:05 For "record Q (T : Set) : Set where field name : Name", it could either fill in "record { name = Bool-name }" or "record { name = ℕ-name }". 14/05 21:06 Both of which have type Q T, for any T. 14/05 21:06 That you've named two records, Bool and ℕ isn't relevant. 14/05 21:06 oh 14/05 21:11 I was totally confused about how records work 14/05 21:11 I thought it had to choose one of my instances 14/05 21:11 --- Day changed Fri May 15 2009 --- Day changed Sat May 16 2009 -!- koninkje_away is now known as koninkje 16/05 02:07 -!- koninkje is now known as koninkje_away 16/05 06:31 hi! 16/05 06:46 I was playing with something but agda doesn't like it, and I can't figure out why 16/05 06:47 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=4923#a4923 16/05 06:49 it was just a toy function to get a feel for things 16/05 06:52 obviously it's of no real use :) 16/05 06:52 I'll be back in a few :) 16/05 06:54 So, if you think about it in terms of just the naturals... 16/05 07:07 It's the difference between 'double n = n + n' and 'double z = z ; double (s n) = s (s (double n))'. 16/05 07:07 You need to prove that those two functions are equal. It's non-obvious. 16/05 07:07 oh, I see! that makes sense 16/05 07:08 what would such a proof look like in agda? it seems like I could use induction, but I have no idea how to write real proofs in agda :P I've just been using it as a supercool typed haskell so far 16/05 07:08 You'll need to look into equality. Generally people use something like 'data _==_ {a : Set} (x : a) : a -> Set where refl : x == x'. 16/05 07:10 Then you write something: 'double-proof : forall {n} -> double1 n == double2 n', which you'll do by induction. 16/05 07:11 the propositional equality thing should help me here, right? 16/05 07:12 And to use it in map2, you'll probably need a function like: 'resp : forall {f x y} -> x == y -> f x == f y', which you'll use with f = \n -> Vec a n. 16/05 07:12 resp? 16/05 07:13 Respects. 16/05 07:15 oh 16/05 07:15 And, yes, propositional equality is the type you want to use. 16/05 07:16 Took me a while to find the definition. 16/05 07:16 cool 16/05 07:18 so it seems like the fundamental thing it doesn't understand is that (suc n) + n === n + (suc n) ? 16/05 07:55 Well, (s n) + (s n) = s (n + (s n)), which it can tell from evaluation. 16/05 07:57 Then you're trying to give it 's (s (n + n))'. 16/05 07:57 So it sees that the outermost constructor matches, but then it doesn't like 'n + (s n) = s (n + n)'. 16/05 07:58 I see 16/05 07:59 damn you agda for not being omniscient! 16/05 07:59 :) 16/05 07:59 In general I'd try proving that (m * s n) = m + m * n. 16/05 08:01 That probably gets you where you need to be. 16/05 08:02 I'm not sure how hard that is. 16/05 08:02 hmm 16/05 08:03 seems like that's most of what's missing to make a Semiring out of Nat 16/05 08:05 I'm surprised that isn't already in the std lib 16/05 08:05 It's in Data.Nat.Properties. 16/05 08:16 Maybe not exported, though. 16/05 08:16 ah, hmm 16/05 08:18 I think there's even a ring solver in the libs, but it's not very efficient (to typecheck) 16/05 08:21 -!- codolio is now known as dolio 16/05 17:03 -!- byorgey_ is now known as byorgey 16/05 21:35 --- Day changed Sun May 17 2009 -!- codolio is now known as dolio 17/05 01:45 Nat.Properties looks helpful, but it's all private 17/05 06:12 -!- copumpki is now known as copumpkin 17/05 06:18 You should prove some simple stuff yourself at first anyhow, to get the hang of it. :) 17/05 06:21 yeah, I should :) I've moved back to playing with my matrices, but I was wondering if there was such a notion as "class" constraints 17/05 06:22 I'd like to say that I want my matrices to contain anything that is a field 17/05 06:23 that's what the module system is about 17/05 06:23 Yeah, there's a couple ways to do similar things. 17/05 06:28 oh, I see, parametrized modules? 17/05 06:28 You can either pass dictionaries to all your functions giving the field structure for the given type, or parameterize the module by the field. 17/05 06:29 If you pass the dictionaries to a function, represented by records, you can open the record locally. 17/05 06:29 Which is kind of like a type class you have to pass explicitly, with a little boilerplate. 17/05 06:30 so that requires the creation of a named dictionary for each instance of a type? 17/05 06:30 / record 17/05 06:30 Parameterizing a whole module by it is probably nicer, though. 17/05 06:31 Right. 17/05 06:31 I haven't seen the std lib using the parameterized module thing, I guess they only took the record approach? 17/05 06:31 They use it in setoid reasoning or something like that. 17/05 06:32 I think the monads use it 17/05 06:33 'module Relation.Binary.PreorderReasoning (p : Preorder) where open Preorder p ...'. 17/05 06:33 Then all the stuff is defined in terms of 'carrier' which is in the Preorder record. 17/05 06:34 Data.List.Equality uses it in a local module, too. 17/05 06:35 ah, cool 17/05 06:39 is there any work for providing additional numeric types? reals, rationals, and so on? 17/05 06:44 I wonder if we could prove interesting things about continuous functions 17/05 06:45 There's integers at least, right? 17/05 06:45 yeah, I think I saw them 17/05 06:45 I guess it'd be easy to make really slow reals 17/05 06:46 well, not easy, but possible 17/05 06:46 You could probably port whatever CReal does. 17/05 06:47 yeah 17/05 06:47 But, yeah, it'd probably be slow. 17/05 06:47 proving stuff about that representation might be a little painful though 17/05 06:47 Well, technically, I don't even know if a straight port is possible, assuming you want to pass the termination checker. 17/05 06:48 true 17/05 06:48 wow, even the : isn't primitive 17/05 06:53 or maybe it is 17/05 06:53 could Set be represented as a type dependent on a nat, to represent its cardinality? 17/05 06:56 to avoid Set1 etc. 17/05 06:56 I don't think so. But you can add something like that primitively to the type theory to get a similar effect. 17/05 06:58 That's called universe polymorphism. 17/05 06:58 ah 17/05 06:59 If you think about doing it with Nat, you have to ask what type \i -> Set i is. 17/05 07:02 yeah, I guess you need a primitive somewhere 17/05 07:02 Which I guess you can do, but then you have, like, an infinite tower Set i, and then something above all of them. 17/05 07:02 Nat has to be built in, too. 17/05 07:03 yeah 17/05 07:04 Maybe similar questions come up with universe polymorphism, though. I'm not really familiar with its theoretical basis, or implementation. 17/05 07:04 Coq has it, though. 17/05 07:05 ah 17/05 07:06 It also hides the universe parameters most of the time, so it'll tell you things like "Type : Type", but it really means "Type[i] : Type[j] where j>i", but the former leads to cleaner looking stuff. 17/05 07:06 I see 17/05 07:06 it seems like coq has everything! :P 17/05 07:06 Well, it's been around somewhat longer, and has more people using/working on it. 17/05 07:07 I think, at least. 17/05 07:08 yeah, it seems more famous at least 17/05 07:08 Isabelle's another more established one, but it gets less press than Coq these days for some reason. 17/05 07:08 that one has some haskell converter too, doesn't it? 17/05 07:09 I can't remember. 17/05 07:09 epigram and pi sigma are also roughly equivalent? 17/05 07:45 I guess there are no built-in matrix libs because we have no fields to use them on at this point 17/05 07:48 oh, and no fields type in the algebra module either 17/05 07:49 is there some way I can write the equivalent of ^{-1} in agda-mode? I need to define a multiplicative inverse for fields 17/05 08:01 \^-\^1 17/05 08:06 oh, that's simple enough 17/05 08:06 pi sigma is an intermediate language, isn't it? 17/05 08:06 oh, maybe 17/05 08:07 -!- byorgey_ is now known as byorgey 17/05 16:25 -!- codolio is now known as dolio 17/05 18:26 -!- codolio is now known as dolio 17/05 18:53 why can't the law of excluded middle be represented in agda? 17/05 23:41 copumpkin: it can be represented; it can't be proved 17/05 23:44 ah 17/05 23:46 do you understand what all the logical connectives mean? 17/05 23:50 like 'or' and so on? 17/05 23:50 me? yup, although I'm not sure how "formal" my knowledge of them is 17/05 23:51 LEM proves  forall p : Program, halts p or not (halts p) 17/05 23:54 LEM? 17/05 23:58 --- Day changed Mon May 18 2009 law of the excluded middle 18/05 00:05 oh, duh :) 18/05 00:07 sorry, I'm not too fast today 18/05 00:07 What's halts look like? :) 18/05 00:17 probably like  eval p /= bot 18/05 00:17 can I clear up some confusion I have that's not strictly related to agda, in here? 18/05 00:19 it has to do with halts 18/05 00:19 (that  eval _ /= _  would be one relation, not an 'eval' function btw) 18/05 00:20 Ah. 18/05 00:20 what is it ? 18/05 00:21 about halts? 18/05 00:21 so I think the way I've been looking at it is wrong... I tend to see it as an inherently paradoxical function, a bit like how the premise of russell's paradox is the source of the paradox... but I'm not sure if that's correct, because people talk about the halting problem and not the halting paradox 18/05 00:23 'I tend to see it as an inherently paradoxical function' you're talkng about   halts : program -> bool  ? 18/05 00:24 yup 18/05 00:24 "Halting problem" gets its name because it's a decision problem about halting. 18/05 00:24 halts : program -> bool is fine you can write that in Haskell 18/05 00:24 the problem is that  halts halts  isn't True 18/05 00:25 well my problem with it is that if you assume the existence of the function, you can write a function that neither halts nor doesn't 18/05 00:25 the really important issue I'm pointing out earlier is actually the meaning of 'o'r 18/05 00:25 'or'* 18/05 00:25 you can write halts in a strongly normalizing calculus too,  halts _ = True 18/05 00:26 and we have  halts halts = True 18/05 00:26 Heh. 18/05 00:26 Anyhow, it's only if you assume that a Turing machine can decide halts for Turing machines that you get a problem. 18/05 00:28 yeah, that was the context I was thinking of 18/05 00:28 oh sure, not arguing with that - Just Turing machines are kinda overdone 18/05 00:28 You can have an oracle that decides halts for Turing machines, but you can't construct a Turing machine to defeat the oracle, because Turing machines don't have oracles. 18/05 00:28 Or, perhaps I should have worded that "you get a paradox". 18/05 00:30 Or contradiction. 18/05 00:30 yeah 18/05 00:31 I suppose it's a contradiction, because then you go on to conclude that Turing machines can't decide halts for Turing machines. 18/05 00:31 Whereas in Russel's paradox, your 'assumptions' are the axioms of naive set theory, so you have to amend those, which is a bit wider in scope. 18/05 00:32 yeah, I'm not saying it's analogous, but the kind of contradiction you get is similar 18/05 00:33 the fun thing about halting is you can phrase any mathematical theorem as a question of whether a program halts or not 18/05 00:34 if that's what 'turing complete' means - well you can do that in these logical frameworks/type theories too 18/05 00:34 (except instead of being about halting, it's about inhabitance) 18/05 00:35 I don't see any relation of halting and russel 18/05 00:35 they're both like the "barber" paradox, if you've come across that 18/05 00:37 neither of them seem like that if ask m 18/05 00:38 me 18/05 00:38 if I have halts :: Program -> Input -> Bool, I can write f x = if halts f x then fix id else x 18/05 00:38 I can't really make a sophisticated argument showing them to be similar, but I can definitely see a similarity 18/05 00:39 not sure how else to show it though :) 18/05 00:39 I guess to be more correct, I should write halts :: (a -> a) -> a -> Bool, and f :: a -> a 18/05 00:41 the usual formulation is  Nat -> Nat  actually 18/05 00:42 and you work on the source of the program not the function itsself 18/05 00:42 well yeah 18/05 00:42 but I couldn't write that succinctly 18/05 00:42 of course programs are encoded as natural numbers so it's   halts :: Nat -> Bool 18/05 00:42 anyway, that wasn't my point :P 18/05 00:42 so what is? 18/05 00:47 that just like you don't know whether the barber who shaves people who don't shave themselves, shaves himself, you don't know whether the program that uses halts in the above way itself halts, and you don't know whether russell's set of sets that don't contain themselves contains itself 18/05 00:49 * vixey thought the barber turned out to be a woman 18/05 00:50 I guess it could be made more clear in the halts case by making another intermediate function 18/05 00:50 You probably like that GEB book I hear it's all about this bullshit :p 18/05 00:50 hah, my friends have recommended it to me but I haven't read it yet :) 18/05 00:51 -!- copumpki is now known as pumpkin_ 18/05 01:42 -!- copumpki is now known as pumpkin 18/05 18:50 -!- copumpki is now known as pumpkin 18/05 20:19 --- Day changed Tue May 19 2009 what are the "next steps" for agda? what are developers working on currently? 19/05 07:04 is there some reason agate compiles to ghc instead of yhc core (which is already untyped)?  or even scheme? 19/05 07:19 -!- copumpki is now known as pumpkin 19/05 09:29 --- Day changed Wed May 20 2009 -!- copumpki is now known as hoggle 20/05 20:31 -!- hoggle is now known as pumpkin_ 20/05 20:38 -!- codolio is now known as dolio 20/05 20:57 Hi, I have some questions regarding parsing mixfix operators. Is agda's parser using the technique explained here: http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf ? 20/05 23:36 --- Day changed Thu May 21 2009 British0zzy: I just skimmed the paper, but I think the answer is "no". The paper is proposing a new way of defining mixfix operators. 21/05 00:24 British0zzy: Currently it uses Haskell-style "infix[lr]? N op" definitions. 21/05 00:25 N being an integer between 0 and 100, or something like that (rather than 0 to 9 like Haskell). 21/05 00:27 is the agda compiler using agate? 21/05 00:27 ok, thanks. 21/05 00:28 Do you know of any examples of programming languages with precedence graphs? 21/05 00:29 No. I've seen them proposed for Haskell as "what we should be doing," but I've not seen anyone do it. Maybe Agda will get it all nailed down, finally, if they're publishing papers on their progress. 21/05 00:31 Of course, there may be languages that do it that I don't know of. 21/05 00:31 surely not! 21/05 00:32 I just want to get a feeling whether or not precedence graphs are nicer than a precedence table 21/05 00:33 in agda, can one define _! and have it bind greater than a prefix expression?? 21/05 00:34 I think function application is always highest. 21/05 00:35 But you can have _! bind tighter than some other operator ^_ 21/05 00:35 what if I define !_, _!, and !_! 21/05 00:36 ambiguity 21/05 00:36 does it detect that one of them is impossible? 21/05 00:36 If it can't figure it out, it will complain. 21/05 00:36 you could get a warning when you define them, and a parsing error when it finds the ambiguity 21/05 00:36 But I don't think it does any fancy type directed stuff or anything. 21/05 00:36 i think type directed stuff is the wrong way to go 21/05 00:37 It would certainly allow for quite a bit of confusion. :) 21/05 00:37 I think I have a fancy natural number type around here somewhere, where I made 1+_ the successor. 21/05 00:38 So you get to prove things like "m + 1+ n == 1+ m + n". 21/05 00:38 hah 21/05 00:38 i'm trying to develop a language where the compiler can recognize an expression like "1 + m" and convert it to "succ m" making for a much nicer proof assistant. 21/05 00:41 rewrite rules? 21/05 00:41 yea, but more powerful 21/05 00:41 uses the Rete matching algorithms 21/05 00:42 and it's dynamically typed, lol 21/05 00:43 :o 21/05 00:43 well, kinda 21/05 00:44 i guess it is "gradually typed" 21/05 00:44 i think that is the buzz word for it 21/05 00:44 ah yeah 21/05 00:44 i've gotten it to do some cool type inference using the rete alg on ASTs 21/05 00:45 but whether or not it can verify a type is not guaranteed 21/05 00:45 but the cool thing is, if you have enough memory, and you let it sit there calculating long enough, it can do some pretty powerful inference 21/05 00:47 i still need to get it to where I can emit code. 21/05 00:47 I've thought about that for other optimizations 21/05 00:48 I think dons has mentioned it too 21/05 00:48 the more compiler time you give it the more optimization it gets, it'd be pretty cool 21/05 00:48 the hardest part is writing a heuristic engine to determine the best code. 21/05 00:50 because the rete alg will give the codegen numerous AST's representing the same program. 21/05 00:50 and i am trying to define a general language for defining rules. 21/05 00:51 such as 1 + m => succ m 21/05 00:51 but m has to be a natural number 21/05 00:52 (or integer) 21/05 00:52 if you're interested, read this: http://cs.ucsd.edu/~ztatlock/publications/eqsat_tate_popl09.pdf 21/05 00:53 1 + (m : Nat) => succ m ? 21/05 00:53 ooh thanks 21/05 00:53 yea, or: m : Nat, 1 + m => succ m 21/05 00:53 where ',' represents that both must be true 21/05 00:54 why not just m : Nat => 1 + m = succ m 21/05 00:54 to use the => for constraints a bit like haskell does 21/05 00:54 i'm trying to develop a language based completely on equality saturation 21/05 00:54 ah 21/05 00:54 I haven't determined a syntax for the rules yet, but as i get more accustomed to the rete alg and how rules are translated to it, hopefully I can create a general language for it 21/05 00:56 i want compiler optimizations to be written by the programmer 21/05 00:56 x : int, (2 ^ n) * x => x << n, could be a potential optimization. it's up to the heuristic engine to decide whether or not to apply it. You'd also need a rule like: k : int, (log k) : int => ∃ (n : int) s.t. k = 2 ^ n 21/05 01:02 is it proven that a dependently typed programming language is not turing complete? 21/05 01:58 statically typed 21/05 01:59 dependent dynamic types seems like an odd concept :P 21/05 02:00 lol, i guess, technically, when you mix values and types then a branch in a program represents a typecheck 21/05 02:02 which is why completely general type checking is undecidable. 21/05 02:04 can one creat existential types in Agda? 21/05 02:17 British0zzy: yes. module Data.Product 21/05 12:08 e.g. boring = \lambda x -> x & \equiv-refl : forall (x : X) -> \Sigma X (\lambda x -> x \equiv x) 21/05 12:25 (Where X can be inferred, you'd just write \exists \lambda x -> x \equiv x instead of \Sigma ... 21/05 12:27 -!- copumpkin is now known as pumpkin 21/05 19:09 -!- pumpkin is now known as copumpkin 21/05 19:09 * liyang has conquered complete induction over ℕ! Really ought to stop naming things ‘cow’ though. 21/05 21:01 That is all. 21/05 21:01 When I have the time, I'll write a gentle introduction to the Agda stdlib. 21/05 21:02 Maybe. 21/05 21:02 good god please do 21/05 21:05 how would you go about doing it? thru examples? theory? 21/05 21:06 from haskell as a starting point? 21/05 21:08 you'd have to explain too much then 21/05 21:11 "How to avoid reinventing the wheel using the standard library" 21/05 21:12 ^by using 21/05 21:12 -!- copumpki is now known as pumpkin 21/05 23:47 --- Day changed Fri May 22 2009 -!- copumpki is now known as pumpkin 22/05 02:04 Dunno lol. Haven't thought about it in much detail yet. 22/05 08:55 Following the style of learn you a haskell? 22/05 08:55 -!- copumpki is now known as pumpkin 22/05 16:09 -!- pumpkin is now known as Rianstradh 22/05 23:32 -!- Rianstradh is now known as pumpkin 22/05 23:32 -!- koninkje_away is now known as koninkje 22/05 23:46 --- Day changed Sat May 23 2009 -!- codolio is now known as dolio 23/05 01:56 -!- koninkje is now known as koninkje_away 23/05 05:33 dear agda hackers, could you tell me what is wrong with the following code...? 23/05 12:45 mymatch : ℕ → ℕ → ℕ 23/05 12:46 mymatch k i with (compare k i) 23/05 12:46 ... | equal _ = 1 23/05 12:46 ... | _       = 0 23/05 12:46 AFAICT, nothing is wrong, but agda complains: 23/05 12:46 m != k of type ℕ 23/05 12:46 when checking that the pattern equal _ has type Ordering k i 23/05 12:46 version: agda 2.2.2, lib-0.1 23/05 12:49 _shift: first of all, shouldn't mymatch have a function type? where do the two arguments come from? 23/05 13:02 _shift: but I just see that perhaps my screen is messed up, because I can't correctly display unicode in my irc client 23/05 13:03 ah, ok, the signature is: mymatch : Nat -> Nat -> Nat 23/05 13:05 right 23/05 13:05 you should try to replace the equal case with something like "mymatch k .k | equal _ = 1" 23/05 13:06 i don't get it 23/05 13:08 you probably need "mymatch k .k | equal .k = 1", even 23/05 13:12 I can explain it later, but I first have to have lunch :) 23/05 13:12 ok, thanks:) i'll try 23/05 13:14 the compare function in Data.Nat.Properties.strictTotalOrder is perhaps more suitable to do the thing you want, _shift. 23/05 13:14 thanks, the 'cmp' from strictTotalOrder is a good example. i wonder what the dot is 23/05 13:18 btw, is there anywhere some documentation on the symtax of agda? 23/05 13:19 there is the reference manual draft, but the "dot" feature is not there 23/05 13:34 _shift: the dot is for marking inaccessible patterns 23/05 13:39 arguments where you know what value the argument must have 23/05 13:40 in this case, Agda can just check for you that the second argument is also k (which is determined by the type of equal), instead of generating a fresh name for it 23/05 13:41 or something like that 23/05 13:41 thanks. i'm a bit surprised that the first version without the dot didn't work, though... 23/05 13:41 I am too, actually, I don't really understand it well enough to know why the dotted version is required. 23/05 13:42 hmm, is it possible to have vararg functions in agda without wrapping the args up in a Vec or something similar? 23/05 20:55 copumpkin: I don't think so. 23/05 21:05 not unless you use tricks akin to the Haskell Printf stuff. 23/05 21:06 I'm not even sure how/if that would work in Agda without type classes. 23/05 21:06 yeah :/ 23/05 21:07 alright ,thanks :) 23/05 21:07 I wasn't actually trying to do something in agda with varargs, was just curious if the dependent types allowed for something like that in an elegant manner 23/05 21:07 you could just compute the type of the funtion... 23/05 21:14 with printf, say, the format argument gives you the type of the rest of the function 23/05 21:14 copumpkin: something like this? http://pastie.org/487559 23/05 21:19 interesting 23/05 21:20 there is a printf implementation in the cayenne paper also 23/05 21:20 that's pretty neat :) 23/05 21:21 oh, I see, the typeclasses in Haskell's printf are just so that you can do computation at the type level 23/05 21:30 so of course you can do that directly in Agda =) 23/05 21:31 still, I think you have to be able to compute the type that you want from previous arguments, right? 23/05 21:31 you couldn't just have a function that takes any number of Nats and returns their sum. 23/05 21:31 byorgey: yes 23/05 21:54 * kosmikus is just reading the log on #haskell to pick up on the hac phi discussion 23/05 21:54 hacking on agda at the hac phi could be neat! 23/05 21:55 copumpkin: are you going to be at hac phi? 23/05 21:55 I'll do my best to be 23/05 21:56 I've put my name down 23/05 21:56 hmm, it's so soon :) 23/05 21:56 not sure I'd be much help for agda hacking, but I'd definitely be willing to try 23/05 21:56 I'm not sure if any of the Agda developers will be there 23/05 21:57 that would certainly help 23/05 21:57 there are AIMs though; next is in September in Gothenburg 23/05 21:58 Agda hacking at Hac phi is definitely welcome =) 23/05 23:18 byorgey: how would accommodation and other boring things work? I've never been to something like this 23/05 23:19 we'll publish info on nearby hotels and such 23/05 23:21 unfortunately unless we get some really wealthy sponsor you'll have to pay for your own accomodation 23/05 23:21 although there may be a few local people willing to let others crash on their couch etc. 23/05 23:22 I can probably manage to pay for my own hotel room if I really try :P 23/05 23:22 ok =) 23/05 23:22 --- Day changed Sun May 24 2009 -!- pumpkin is now known as Gruppetto 24/05 02:18 -!- Gruppetto is now known as pumpkin 24/05 02:20 copumpkin: there's test/succeed/Printf.agda under the Agda source tree. 24/05 17:23 In other news, I've registered http://learnyouanagda.org/ :3 24/05 17:23 :-) 24/05 17:34 but currently faffing with http://liyang.hu/ so I can use the same build system / UI for the pages. Nearly there... 24/05 17:38 paramorphisms are generalizations of catamorphisms. 24/05 19:02 er, sorry, wrong channel =) 24/05 19:03 --- Day changed Mon May 25 2009 -!- byorgey_ is now known as byorgey 25/05 12:41 hi there 25/05 17:16 .n₁ + 0 != .n₁ of type ℕ 25/05 17:16 what can I do to resolve this, again? 25/05 17:16 nobody awake? 25/05 21:25 endojelly: oh hai. 25/05 21:45 endojelly: open import Data.Nat.Properties 25/05 21:49 endojelly: open CommutativeSemiring commutativeSemiring 25/05 21:49 endojelly: +-assoc : n + 0 \equiv n or something like that. 25/05 21:50 assoc? What am I on about? 25/05 21:59 Sorry, rather full of dinner and watching Legally Blonde. I think it's infected me. 25/05 21:59 endojelly: here's something I prepared earl^Wjust a second ago -- http://liyang.hu/crap/AddZero.agda.html 25/05 22:05 liyang, ah, thanks a lot! I just did it by hand by proving everything I needed myself, but I suspected it would already be in the standard library :P 25/05 23:44 If you're just beginning Agda, the stdlib seems a bit overwhelming, so a lot of people get put off investigating further. D: 25/05 23:47 I do intend to do a tutorial of some sort on that. Time is always the problem though. 25/05 23:48 --- Day changed Tue May 26 2009 liyang, thanks a lot again! 26/05 08:35 _91 order !=< StrictTotalOrder 26/05 10:23 when checking that the expression i has type StrictTotalOrder 26/05 10:23 okay, I have no idea why it wants a StrictTotalOrder at this place 26/05 10:23 aah. 26/05 10:27 that's why. I forgot to parameterize a parameterized module 26/05 10:27 using products makes everything really complicated :( 26/05 12:58 I need to pattern match inside of a function type declaration 26/05 15:44 if that makes sense 26/05 15:44 is it possible? 26/05 15:44 or am I thinking wrong? 8) 26/05 15:44 I think somehow with-≡ is the answer 26/05 16:24 now I just need to find the right substitution 26/05 16:24 the product datatype makes life hard. 26/05 16:24 --- Day changed Wed May 27 2009 -!- pumpkin is now known as Thwog 27/05 00:48 -!- Thwog is now known as pumpkin 27/05 00:52 endojelly: could you show us the code? I'm not really sure exactly what you're trying to achieve... 27/05 09:59 liyang, thanks, but the code is way different now 27/05 12:15 endojelly: hope you got your issue sorted out in any case. :3 27/05 18:21 liyang, I did, thanks! 8) 27/05 18:22 PS: content sought for http://learnyouanagda.org/ -- send me text; I'll make it suitable snarky and upload the finished work. Content under CC by-nc-sa. 27/05 18:53 awesome! 27/05 18:53 you should get BONUS to contribute some art :P 27/05 18:54 I may steal some. :3 27/05 18:54 Or take photos instead. 27/05 18:54 Because I like my camera. 27/05 18:54 hah :) I'm sure he'd draw you some if you asked 27/05 18:54 And I have kittehz. 27/05 18:54 maybe even a flaming unicorn with a rainbow 27/05 18:54 speaking of art; it would be nice if agda had a logo 27/05 18:55 a flaming unicorn! 27/05 18:55 stevan: take it up with the Agda mailing list. :3 27/05 18:56 I tried thinking of a good domain name for the Agda Wiki which wasn't already taken, and failed. But then the idea of doing an informal (hah!) introduction to the language + stdlibs hit me... 27/05 18:57 agdawiki.org? 27/05 18:57 wikipagdia.org? :P 27/05 18:58 Again, take it up with the mailing list. :) 27/05 18:59 I got slides to do before 15:00 tomorrow. :-/ 27/05 18:59 just throwing out random suggestions, am not being too serious :) 27/05 18:59 I do support wikipagdia.org though. 27/05 19:00 --- Day changed Thu May 28 2009 -!- eelco_ is now known as eelco 28/05 08:24 -!- Hennet_port is now known as Hennet_Port_Away 28/05 11:24 -!- Hennet_Port_Away is now known as Hennet_port 28/05 11:42 -!- Hennet_port is now known as Hennet_Port_Away 28/05 16:43 -!- Hennet_Port_Away is now known as Hennet_port 28/05 17:31 -!- Hennet_port is now known as Hennet_Port_Away 28/05 18:01 -!- Hennet_Port_Away is now known as Hennet_port 28/05 18:25 --- Day changed Fri May 29 2009 -!- jfredett_ is now known as jfredett 29/05 06:07 -!- endojelly is now known as endo 29/05 17:01 -!- endo is now known as endojelly 29/05 17:01 --- Day changed Sat May 30 2009 -!- byorgey__ is now known as byorgey 30/05 04:28 -!- byorgey_ is now known as byorgey 30/05 17:55 -!- byorgey_ is now known as byorgey 30/05 20:25 --- Day changed Sun May 31 2009