sharada sharada copumpkin --- Log opened Tue Sep 01 00:00:24 2009 # Norio Kato - A new implementation of Agda written in Java 01/09 17:14 anyone know where to get details on that? 01/09 17:14 * copumpkin saw something about an agda in java before disconnecting??? 01/09 19:26 that seems like a very strange choice 01/09 19:26 -!- badtruffle is now known as copumpkin 01/09 20:26 I still don't get the codata equality stuff :( 01/09 21:26 -!- byorgey_ is now known as byorgey 01/09 22:14 --- Day changed Wed Sep 02 2009 copumpkin: good point 02/09 07:20 I wish my emacs wouldn't freeze when I try to use agda :( 02/09 07:29 not really sure what it's doing 02/09 07:29 copumpkin: maybe it's looking for a specific ghci prompt 02/09 07:36 this is a problem I had once 02/09 07:37 it's got ghc as a subprocess 02/09 07:37 and isn't pegging my cpu or anything 02/09 07:37 I had to :set the prompt to something specific or else it froze 02/09 07:37 emacs and ghci are just sitting there idle, and unresponsive 02/09 07:37 hmm 02/09 07:37 i get a similar problem with haskell-mode if i don't have at least a module in the prompt 02/09 07:38 hmm 02/09 07:40 how do I do that? I'm not usually an emacs user, and am just using it so I can play with agda ;) 02/09 07:40 :set is a ghci command 02/09 07:41 I have 02/09 07:41 (load-file (let ((coding-system-for-read 'utf-8)) 02/09 07:41 (shell-command-to-string "agda-mode locate"))) 02/09 07:41 in my .emacs 02/09 07:41 oh, I see 02/09 07:41 but agda-mode appears to ask ghci to ignore the .ghci file 02/09 07:41 how would I set the prompt? 02/09 07:42 :/ 02/09 07:49 ah, I can unhang with C-g 02/09 07:52 and then play with ghci 02/09 07:52 oh, it's a linker problem o.O 02/09 07:53 I'll fix it tomorrow 02/09 07:54 beta eta equalty still doesn't equate \n -> n + 0 with \n -> 0 + n in the same way that $equality equality doesn't relate$codata1 with $codata2 02/09 09:18 help me fill in the blanks? :P 02/09 09:18 am I even on the right track 02/09 09:18 * sharada repeats:::: 02/09 10:03 beta eta equalty still doesn't equate \n -> n + 0 with \n -> 0 + n in the same way that$equality equality doesn't relate $codata1 with$codata2 02/09 10:03 is that right? and what is missing 02/09 10:03 For \$equality you could have "intensional", I suppose. 02/09 10:06 Intensional equality lets you demonstrat \n -> n + 0 = \n -> 0 + n because you can demonstrate that n + 0 = 0 + n. 02/09 10:07 oh yeah 02/09 10:08 I should use intensional in both cases 02/09 10:08 is there a canonical example like the n + 0  0 + n thing for codata though? 02/09 10:08 There are plenty of simple examples, I suppose. 02/09 10:09 '1 :: repeat 1' is not intensionally equal to 'repeat 1'. 02/09 10:09 Well, unless you can cheat by evaluation like in Coq. 02/09 10:10 oh wow :| 02/09 10:10 what if I make 02/09 10:10 f (x :: xs) = x :: xs 02/09 10:10 then f (1 :: repeat 1) = f (repeat 1)? 02/09 10:10 Well, it rather depends on what semantics you're using. With the old, broken codata type stuff, 'f xs' might be treated as a reducible expression, in which case you'd get "1 :: repeat 1 = 1 :: repeat 1". 02/09 10:13 But from a strict categorical perspective, f (1 :: repeat 1) is just as irreducible as 1 :: repeat 1 and repeat 1. 02/09 10:14 And f (repeat 1). So none are intensionally equal. 02/09 10:14 ugbhhh 02/09 10:14 I don't get how any of this can work properly 02/09 10:14 Treating them as able to be reduced is what breaks subject reduction in Coq. 02/09 10:14 (That's the right term, right?) 02/09 10:15 yeah 02/09 10:15 Way back someone showed how you could write a proof of intensional equality for those sorts of bisimulations, though. 02/09 10:15 But that seems wrong to me. 02/09 10:15 The paper on the partiality monad uses some "rewrite" tactic that you couldn't simulate easily in the original coinductive Agda for that purpose, I think. 02/09 10:16 bisimulation -> equality is bad? 02/09 10:16 It's not bad, but it's extensional in character. 02/09 10:17 The fact that you can prove it in Coq instead of assuming it as an axiom or something is weird. 02/09 10:17 It'd be like being able to prove "(forall x -> f x = g x) -> f = g". 02/09 10:19 I see 02/09 10:19 It helps me a little to think of existential encodings of coinductive stuff. 02/09 10:22 So, like, repeat 1 might be "(1 , g) where g x = (x, (x, g))" and the observation functions are "head (x, g) = fst (g x) ; tail (x, g) = snd (g x)". 02/09 10:23 the finality  ? 02/09 10:24 And then you might have "h :: t = ((h, t), id)". 02/09 10:25 wouldn't that g' have cyclic type ? 02/09 10:26 So, if you look at what they're made out of, then "repeat 1 = (1, g)" and "1 :: repeat 1 = ((1, (1, g)), id)", so they're not built out of the same thing. But they do produce the same observations. 02/09 10:27 Does it? I hope not. 02/09 10:28 hm, i would take Stream a = exists s. s * (s -> a * s)' (or s/(s -> a * s)/(s -> a) * (s -> s)/ if preferred) 02/09 10:31 Yeah, the former was my intention. 02/09 10:32 but it seemed you wanted Stream a = exists s. mu r. s * (s -> a * r)' (or maybe s/mu/nu/ ?) 02/09 10:32 Oh, yeah, I guess I was a bit muddled. 02/09 10:33 using the former, repeat 1' becomes (1,g) where g x = (x,x)' with head (s,g) = fst (g s)' and tail (s,g) = (snd (g s),g)' 02/09 10:34 (your "can change the behaviour as we go" can still be encoded) 02/09 10:35 So, 'repeat 1 = (1, g) where g x = (x, x)' and 'x :: (s, f) = (inl x, g) where g (inl x) = (x, inr s) ; g (inr s) = let (y, s') = f s in (y, inr s')' or something. 02/09 10:35 hm .. the repeated use of inr' looks irksome 02/09 10:36 Yeah. I'm not sure how stream fusion handles that sort of thing. 02/09 10:37 They might use (Maybe s1, s2). 02/09 10:37 That doesn't look a lot better, though. 02/09 10:37 btw, wouldn't the same problem happen with equality on quotient types, as with stream and function types ? 02/09 10:38 Probably. 02/09 10:38 NuPRL and MetaPRL from that paper on quotient types are both extensional, I think it says. 02/09 10:38 (maybe it would be better anyway to allow changing the state type) 02/09 10:38 Stream a = mu r. exists s. s * (s -> a * r)  -- s/mu/nu/ ? 02/09 10:40 (but then why use an existential at all, instead of just `Stream a = nu r. a * r' ?) 02/09 10:40 stream-fusion uses Bool * s as the state when you cons, apparently. 02/09 10:42 Only it's not Bool, it's some type with values S1 and S2. 02/09 10:43 * ski_ wonders if one could do it with (contra-)recursive types, instead .. 02/09 10:44 Which it uses like: h :: (s, f) = (Nothing, g) where g Nothing = (h, Just s) ; g (Just s) = let (x, s') = f s in (x, Just s') 02/09 10:45 Only instead of nothing it uses (S2, s) and instead of Just s it uses (S1, s). 02/09 10:46 Anyhow, my overall point was that coinductive types can be modeled with existentials, and you might have two values that are built out of things you couldn't prove intensionally equal, but they are nevertheless the same coinductive value, since all you can do with them is observe them, and they behave identically under that operation. 02/09 10:48 Which is a hand-wavey reason why "repeat 1" and "1 :: repeat 1" are not intensionally equal, despite the fact that they're obviously the same value. 02/09 10:49 And the fact that you can prove them equal in Coq is weird, and leads one to suspect that the way it handles coinductive types and the operations thereon is fishy. 02/09 10:51 * ski_ forgets what's the difference between intensional and extensional equality .. 02/09 10:53 I'm not really certain what the formal definitions are. 02/09 10:53 Intensional equality gets you m = n if m and n have the same normal form, or something. 02/09 10:55 (i think "Programming in Martin-Loef Type Theory" mentioned it .. something with how the equality judgement there is related (or not) to the type of equality proofs) 02/09 10:55 (but i don't recall the details) 02/09 10:55 Extensional gets you m = n when all the ways you can use them produce the same results. 02/09 10:56 Rougly. 02/09 10:56 "normal forms" seems not proper to speak of for coinductive data 02/09 10:56 Roughly, even. 02/09 10:56 (including functions) 02/09 10:56 (cf. "terminating" vs. "productive") 02/09 10:57 I'd say the normal form of "repeat 1" is "repeat 1", because values with a coinductive type aren't subject to reduction. 02/09 10:58 You can only reduce "observe (repeat 1)". 02/09 10:58 -!- codolio is now known as dolio 02/09 10:58 imio, functions (and other things that are defined in terms of how to use them) should have extensional equality 02/09 11:00 dolio : yes 02/09 11:01 Yeah. I'm not sure what problems you face when you add extensional equality to your language. Undecidability comes to mind. 02/09 11:02 But then OTT is claimed to get you all the good without the bad. So that'd be nice. 02/09 11:02 So, I'm looking forward to Epigram 2. :) 02/09 11:03 is that related to OTT ? 02/09 11:03 I'm pretty sure Epigram 2 is where Conor McBride and his buddies are implementing all their ideas in that area. 02/09 11:05 Or that's the idea, anyway. 02/09 11:05 is OTT an abstract system, while Epigram being an implementation ? 02/09 11:06 Yeah. Like System Fc and GHC, I guess. 02/09 11:06 There's already some OTT stuff implemented in Agda somewhere as a proof of concept, I think. 02/09 11:07 ok 02/09 11:07 That is, formalized using Agda. Not built into its type system and whatnot. 02/09 11:08 *nod* 02/09 11:09 imio, functions (and other things that are defined in terms of how to use them) should have extensional equality 02/09 12:16 in type theory?? 02/09 12:16 And the fact that you can prove them equal in Coq is weird, and leads one to suspect that the way it handles coinductive types and the operations thereon is fishy. 02/09 12:18 but is Agda better? and what is the right way to do it 02/09 12:18 I thought they changed Agda to make it handle things different, but I'm not completely sure. 02/09 12:22 People have, at the least, figured out how to set things up appropriately to adhere to the way the category theory works. 02/09 12:24 I'm also not sure anyone figured out how to prove the intensional equality of two different bisimilar things in Agda, either, but that might just be because it isn't as easy. 02/09 12:25 Finding the actual proof is proving difficult, though. 02/09 12:32 And I don't know enough Coq to reconstruct it, if it even still works. 02/09 12:33 Oh, found it. Bad thread name. 02/09 12:38 http://logical.saclay.inria.fr/coq-puma/messages/c8acae734082fd1b#msg-b1a0f4aa5ab9ac6f 02/09 12:40 I think if you scroll down a couple messages (to the one below mine) you'll see a proof that bisimilarity implies intensional equality. 02/09 12:41 For streams. 02/09 12:41 "Actually all coinductive types can be encoded as omega-limits once you have functional extensionality"  says Thorsten 02/09 12:55 Can you build every element using finality? 02/09 13:01 for stream finality is: 02/09 13:02 stream_finality (f : B -> 1 + A * B)  : B -> stream A 02/09 13:02 stream_finality b | f b => left () = nil | f b => right (x, y) = x :: stream_finality y 02/09 13:03 so my emacs has stopped hanging now 02/09 14:48 however, now it's complaining that the function 'main' is not in MAlonzo. 02/09 14:49 I could've sworn I used to use the compile command to compile modules with no main function 02/09 14:53 ah well, I guess the load command will typecheck too 02/09 14:55 the agda emacs mode is much nicer than the haskell one 02/09 15:41 yep :) 02/09 16:05 * copumpkin is enjoying it now 02/09 16:05 Are these reasonable implementations of associativity and commutivity of addition on naturals? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8967 02/09 18:38 no 02/09 19:27 sharada: Was that for me? 02/09 21:16 yeah 02/09 21:16 This is my first .agda file 02/09 21:16 I don't think you should call it 'mylemma' 02/09 21:16 what sort of things could be improved 02/09 21:17 very true 02/09 21:17 also you can write x + y == y + x rather than (x + y) == (y + x), just give == a lower fixity than + 02/09 21:17 it's fine other than that - you could try to rewrite it using the equational reasoning module though, that is a really cool library in agda worth at least reading about 02/09 21:18 That is part of lib-0.2? 02/09 21:18 well it's part of agda standard lib 02/09 21:18 you can get that off the wiki using darcs 02/09 21:19 I don't think it comes with agda program 02/09 21:19 In Relation.Beinary.EqReasoning[1] there is an example using begin and \qed. What defines these? 1. http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Relation.Binary.EqReasoning.html 02/09 21:31 or is that just an explanation in English? 02/09 21:31 glguy no that's actual code 02/09 21:31 Ah, I found it 02/09 21:31 in PreorderReasoning, at least 02/09 21:31 glguy I don't know where it's defined but if you click on it inside agda mode that should take you there I think 02/09 21:32 --- Day changed Thu Sep 03 2009 copumpkin: You were using the compiler? 03/09 02:58 how do I use one "statement" to prove another in agda? in haskell I'd do case blah of x -> and it would "bring its knowledge into scope" 03/09 05:16 * copumpkin fails hard :) 03/09 05:16 with, probably. 03/09 05:17 foo x with bar x 03/09 05:17 ah great, thanks :) 03/09 05:17 ... | match-against-bar-x = ... 03/09 05:18 with is sugar for defining auxillary functions, so you could do that, too. 03/09 05:18 seems like agda could benefit from a hoogle-like search function even more than haskell could 03/09 05:21 "find me a proof that P = NP kthx" 03/09 05:21 Incidentally, you were using the compiler? I've never used that. 03/09 05:25 Maybe it's slower than the interpreter, and that's why it was taking so long. 03/09 05:25 nah, it was taking so long because I had a linker error when loading the agda lib 03/09 05:25 so the ghci prompt was > 03/09 05:26 Especially if it was compiling a chain of imported modules. 03/09 05:26 and agda's silly and hangs 03/09 05:26 Ah. 03/09 05:26 is there a particularly elegant way to express induction over the naturals in agda? 03/09 06:10 I was thinking of using the Holds type from http://wiki.portal.chalmers.se/agda/agda.php?n=Main.TypesSummerSchool2007?action=view 03/09 06:11 something like induction : {n : ℕ} (p : ℕ → Bool) → Holds p zero → ({m : ℕ} → Holds p m → Holds p (suc m)) → Holds p n 03/09 06:13 but is that "idiomatic"? 03/09 06:13 it's a rather restricted definition of induction, for one 03/09 06:17 but assuming it's sufficient 03/09 06:17 maybe going through the Bool type is a little indirect 03/09 06:31 I usually use P : Nat -> Set. 03/09 06:40 (P m -> P (suc m)) -> P 0 -> n -> P n 03/09 06:40 ah, simple enough 03/09 06:41 so do you do an implicit P? 03/09 06:42 or does it not really matter? 03/09 06:42 Yes. 03/09 06:42 ah ok 03/09 06:42 Although I don't know if that's necessarily more useful. 03/09 06:42 It might not be, but it isn't a big deal to wrap braces around the predicate when it can't be inferred. 03/09 06:44 yeah :) 03/09 06:44 In general I'm tempted to not use booleans in a language like Agda. 03/09 06:46 what does it mean when I get something highlighted in yellow? 03/09 06:46 yeah, they seem unnecessary, but I saw them in that wiki page and assumed they'd serve some purpose 03/09 06:47 And instead use (a -> Set) predicates, and "Decidable p" in lieu of value-level booleans. 03/09 06:47 Well, they're useful when you really want to do fiddling with plain booleans. 03/09 06:48 But they lose a lot of their uses from something like Haskell. Like, I might not use them in filter. 03/09 06:49 Even though filter doesn't use any of the extra fanciness. 03/09 06:49 -!- ksf_ is now known as ksf 03/09 07:15 is there a standard name for foo? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8988#a8988 03/09 08:43 I'm sure it has a name in the libraries. 03/09 08:56 Test maybe. 03/09 08:56 Oh, it's called T in the libraries. 03/09 08:57 It's named T in the libraries, if that didn't get through. 03/09 09:01 that's the upparcase t rather than \top, right? 03/09 09:03 Yes. \top is the unit type. 03/09 09:04 Like in your code. 03/09 09:04 Except it's probably a record, for eta to work. 03/09 09:05 ah, there's a difference? 03/09 09:08 Yeah. The type system knows that records satisfy eta laws. So, like, if you had pairs, then it'd know that "p = record { fst = fst p ; snd = snd p }". 03/09 09:12 Which for the unit type means that it knows that every inhabitant is equal to "record {}" and it can fill it in automatically. 03/09 09:13 Whereas it won't automatically suply 'tt'. 03/09 09:14 mmh, i don't understand where that applies 03/09 09:22 Well, if you define, say, _<_ on Naturals recursively, where m < n = \top for appropriate situations... 03/09 09:23 Then if you have, like "_-_ : forall m n -> {n < m} -> Nat" 03/09 09:23 Then, you can write "5 - 4" without having to explicitly prove that 4 < 5. 03/09 09:24 With the "data" version, you'd have to write "(5 - 4) {tt}" I think. 03/09 09:25 oh, i see 03/09 09:28 i wasn't thinking about function calls 03/09 09:29 Yeah, you can write _ and have it filled in, too, but that's less exciting. 03/09 09:30 -!- codolio is now known as dolio 03/09 09:30 after i've pattern matched "p x y" against "True", shouldn't (tt : so (p x y)) typecheck? 03/09 11:42 err 03/09 11:42 so = T there 03/09 11:42 Saizan don't think so! 03/09 11:42 why? 03/09 11:43 True is a type ? (not a constructor? .. agda will think it's a variable in a pattern match context) 03/09 11:43 oh.... 03/09 11:43 i guess i need to give more context :) 03/09 11:43 I didn't notice you had 'so' there 03/09 11:43 forget what I said, you are dead right 03/09 11:43 uhm, i wonder why agda doesn't accept it then 03/09 11:44 accept what? 03/09 11:47 (if you use with then no wonder it doesn't work .. they call it 'magic' with for a reason) 03/09 11:47 (ah..) 03/09 11:48 what is your code 03/09 11:49 uhm, it's quite messy but i'll paste it anyway :( 03/09 11:51 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8988#a8994 <- here it is 03/09 11:52 the above revision works though 03/09 11:52 s/foo/so/ 03/09 11:52 elim-pred works ? 03/09 11:54 yeah, it typechecks 03/09 11:56 though i find that i can't rewrite elem-trans using it because the False branch is using the fact that p a x = False 03/09 11:57 i could use _==_ i guess 03/09 11:57 maybe I just don't have enough context but "so (elem P x xs) -> so (subset P xs ys) -> so (elem P x ys)" seems weird 03/09 11:58 just beacuse these things are decidible - having then as booleans might still be awkard 03/09 11:59 you could try to use instead that a proof of 'elem' is actually a path to that elemen in the list, and likewise subset explains how to take a subset 03/09 11:59 yeah, that might have been a better choice 03/09 12:03 (I can see that writing a program to factor a path through a subset proof might not be /that/ hard.. it's def. going to be longer than the two lines of code you have there though..) 03/09 12:03 hm I wonder if 'so' works a bit like Prop 03/09 12:04 actually it doesn't but it would be possible to have a so in prop 03/09 12:04 elim-pred : {A C : Set} -> (P : A -> A -> Bool) -> (x y : A) -> (so (P x y) -> C) -> (so (not (P x y)) -> C) -> C <- this gets it working 03/09 12:09 Is something like this already in the library? (I'm using == from Relation.Binary.Core) eq-exts : ∀ { A B } { a b : A } (f : A -> B) -> a ≡ b -> f a ≡ f b 03/09 17:36 Is this congruence, perhaps? 03/09 17:37 isn't it usually (f : A -> B) -> a ≡ b -> f a -> f b 03/09 17:38 for rewriting 03/09 17:38 and you instantiate f x = a = x,  prove the first with refl that gets you a = b 03/09 17:38 f x = a ≡ x 03/09 17:38 I have no idea what it usually is :) 03/09 17:39 is that something that is already defined? 03/09 17:41 I was at least able to "simplify" it as: eq-exts : Congruential (_≡_) 03/09 17:54 eq-exts f refl = refl 03/09 17:54 -!- byorgey_ is now known as byorgey 03/09 22:57 --- Day changed Fri Sep 04 2009 -!- byorgey_ is now known as byorgey 04/09 01:01 what's the definition of canonical wrt. coinductives? 04/09 12:55 tail (repeat 1) is canoncial? 04/09 12:55 --- Day changed Sat Sep 05 2009 -!- codolio is now known as dolio 05/09 01:18 -!- codolio is now known as dolio 05/09 12:13 -!- byorgey_ is now known as byorgey 05/09 15:00 hello :) 05/09 18:31 hi 05/09 18:35 hi Saizan_ :) 05/09 18:36 * EnglishGent just taking a quick look at Agda 05/09 18:38 I looked at Cayenne a while back & thought that interesting 05/09 18:38 never looked at cayenne myself, but agda is pretty fun and not that hard to grasp after haskell 05/09 18:43 well I ran into Augustuss recently - and mentioned I'd looked at Cayenne - and he suggested I look at Agda 05/09 18:46 and I'm certainly happy to take advice from a name :) 05/09 18:46 * EnglishGent is still learning Haskell - but I thought it couldnt hurt to take a peek 05/09 18:47 I'm interested in type-systems generally :) 05/09 18:47 have you used it long? 05/09 18:48 * EnglishGent does like the idea of a language that can be used both for programming & theorem proving 05/09 18:48 * EnglishGent is trying very hard to teach himself a bunch of comp-sci ... it's hard going though 05/09 18:49 I'm so grateful for irc! at least I'm not _totally_ alone 05/09 18:49 cool 05/09 18:57 I like "language that can be used both for programming & theorem proving" too 05/09 18:57 hi sharada :) 05/09 18:59 hi 05/09 18:59 what's your background sharada? (just curious) :) 05/09 19:00 none 05/09 19:00 * EnglishGent is a programmer with an interest in better languages (amongst other interests!) :) 05/09 19:01 yeah 05/09 19:01 I don't study this stuff formally 05/09 19:01 i've started using agda seriously only last week when i felt insecure about some functions in my code 05/09 19:03 it turns out i could prove their correctness, fortunately :) 05/09 19:04 -!- Saizan_ is now known as Saizan 05/09 19:04 :) 05/09 19:04 if only more programmers thought that way 05/09 19:05 so much code out there is _so_ bad :| 05/09 19:05 * EnglishGent has been accused of wasting time thinking about 'theoretical problems' by management before... becuase I cared about the correctness of the code I was working on 05/09 19:06 :| 05/09 19:06 :\ 05/09 19:06 Is there a trick to getting characters like \forall and \:: in aquamacs? 05/09 19:07 "agda-mode setup" got the latex input working fine for me, but i'm on linux 05/09 19:08 yeah, it worked find on Linux for me, too 05/09 19:08 I get boxes instead of the actual font glyph for those symbols 05/09 19:09 in Aquamacs 05/09 19:09 maybe better luck with Carbon Emacs 05/09 19:09 OK 05/09 19:09 I'll give that a shot then 05/09 19:09 EnglishGent: have you got any particular dreams in that area (correct programs) 05/09 19:34 ooh EnglishGent :o 05/09 19:35 hi copumpkin :) 05/09 19:35 depends what you mean by dreasm - but yes I have a few sharada :) 05/09 19:35 I think we could do _much_ better than the mainstream languages / tools we're using now 05/09 19:35 yeah of course 05/09 19:37 I'd like to be able to talk about time/space complexities _within_ the language 05/09 19:38 that sounds hard 05/09 19:39 I agree - but Augustuss told me that Agda was looking at it :) 05/09 19:39 I think that some people use monadic style and interepter that gives --> semantics (executable) and also --> time complexity 05/09 19:39 so you can project out either way 05/09 19:40 well I know almost nothing about agda at the moment 05/09 19:40 I'm still learning Haskell 05/09 19:40 So, C doesn't have polymorphic functions because its type system is too limited, and Haskell has polymorphic functions because its type system is too limited? 05/09 19:40 but I thought it couldnt hurt to take a look :) 05/09 19:40 hehe what glguy 05/09 19:41 I'm just reading through AgdaIntro.pdf 05/09 19:42 and they mention that Agda doesn't need polymorphic functions as you just pass the types in as parameters 05/09 19:42 oh I get what you mean 05/09 19:42 (even if you've declared those parameters as implicit) 05/09 19:42 has there been any talk of a hoogle for agda? 05/09 19:43 aoogle doesn't have such a nice ring to it 05/09 19:44 aahoo? 05/09 19:44 well, obviously a different name, but functionality wise 05/09 19:44 aing! 05/09 19:44 it'd be great to be able to search for proofs 05/09 19:44 (I don't know the answer to your actual question) 05/09 19:44 Is there a level of types more "expressive" "powerful" (?) than the dependent types offered by agda? 05/09 19:47 once you allow arbitrary functions in your types, have you hit the theoretical limit? 05/09 19:47 glguy: well there is simple types, then polymorphci types, depedente types .. the cube 05/09 19:48 you know this though.. 05/09 19:48 sharada: I'm aware of the lambda cube 05/09 19:48 I don't have it ingrained in my understanding 05/09 19:48 if that's what you are referring to 05/09 19:48 that's as mucha bout the cube that matters 05/09 19:49 next you can add inductive-recursive universes to get more strength 05/09 19:49 I don't know what is beyond that 05/09 19:49 sharada: unless you were being sarcastic, feel free to assume that I don't know much more than I've let on about dependent types and programming in Agda  :) 05/09 19:49 (Agda has induction recursion) 05/09 19:49 no I am not being sarcastic 05/09 19:49 ok :) 05/09 19:50 dont we hit a limit on model-theoretic power? when the type system becomes Turing complete? 05/09 19:51 * EnglishGent doesnt understand how it can be more powerful that that 05/09 19:51 though of course you can add more proof theoretic power - and allow you to say things more compactly 05/09 19:52 I think once it is Turing complete you have useless 05/09 19:52 and it's rubbish like an inconsistent logic 05/09 19:52 * EnglishGent doesnt really understand this either - but is trying hard to understand it all 05/09 19:52 I thought the problem was simply that type-checking might then never terminate 05/09 19:52 yeah that sucks 05/09 19:52 * EnglishGent fairly certain their are languages with Turing complete type systems - Qi's is - and Cayennes is I think 05/09 19:53 it would be fine for something like haskell but not a proof system 05/09 19:53 sure if you just want to hack 05/09 19:53 well like you - I like the idea of a language that can be used for both theorem proving & programming 05/09 19:54 but I'm a) partly trying to contribute what little I know to answering glguy's question 05/09 19:54 and b) trying to understand things better myself 05/09 19:54 * EnglishGent doesnt see why non-termination in _principle_ has to be a problem - as long as _in practice_ checking terminates 05/09 19:55 the existence of pathalogical cases doesnt seem enough to exclude such systems from use (to me) 05/09 19:55 unless in practice such cases crop up often 05/09 19:55 :) 05/09 19:56 EnglishGent: on the converse, what we have now is:  theoretically does terminate but may not (something might take a million million years and as many MB of RAM) 05/09 19:56 right! so it's not as strong a gurantee as it might seem anyway 05/09 19:57 the problem is that you've to check termination anyway before you accept a proof for an inductive property 05/09 20:05 Can someone explain why in in this definition, we have \forall {xs} rather than {xs : List A}? data _∈_ {A : Set}(x : A) : List A → Set where 05/09 20:21 hd : ∀ {xs} → x ∈ (x ∷ xs) 05/09 20:21 the : List A bit just gets inferred 05/09 20:22 Does Agda simply infer the type for xs? 05/09 20:22 OK 05/09 20:22 yes 05/09 20:22 so the \forall tells agda to try to infer i nthis case? 05/09 20:23 no 05/09 20:23 remember, 05/09 20:23 A -> B 05/09 20:23 is like 05/09 20:23 forall (x : A), B 05/09 20:23 So it is just a syntactic difference then 05/09 20:24 (except well in agda you don't write the comma, it's a -> again, confusingly) 05/09 20:24 yeah -> is just a shorthand 05/09 20:24 * glguy wants mixfix ported to Haskell :) 05/09 20:26 * sharada thinks mixfix SUCKS :P 05/09 20:28 Notation in Coq is a lot better 05/09 20:28 it's annoying to me not being able to change the order in agda 05/09 20:28 I guess I haven't played with Coq's notation 05/09 20:28 I just like that things like "if_then_else_" don't need to be built in 05/09 20:28   you can't do things like   x given b   with (b : A)  (x : f b) 05/09 20:31 you must change it around like  b nevig x,  which I don't like that much 05/09 20:31 (it's kind of rare this comes up, to be fair) 05/09 20:31 -!- byorgey_ is now known as byorgey 05/09 20:43 -!- byorgey_ is now known as byorgey 05/09 21:02 -!- EnglishGent is now known as EnglishGent^afk 05/09 22:27 --- Day changed Sun Sep 06 2009 I've got a goal of "Goal: x \in  (filt p (x :: .xs) | p x)" but I don't know how to express that I want to turn: filt p (x :: .xs) | px  into x :: filt p .xs 06/09 01:39 at which point I believe my constructor "hd :   {xs} -> x \in (x :: xs)" 06/09 01:39 would apply 06/09 01:39 What technique do you use here? (do I need to provide more context?) 06/09 01:40 -!- codolio is now known as dolio 06/09 02:14 glguy: Match against px? 06/09 02:21 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a9103 06/09 02:31 Oh, okay. 06/09 02:38 if I try casing on "el" 06/09 02:39 then I get the goal I mentioned before 06/09 02:39 this is out of the AgdaIntro.pdf 06/09 02:39 Have you tried going into the agda menu and selecting the items about viewing the goal? Sometimes the default display doesn't normalize the goal type all the way. 06/09 02:40 it might be displaying it wrong 06/09 02:41 but it isn't lettme me use my "hd" or "tl" constructors 06/09 02:41 does the display not normalizing also mean that that wouldn't work either? 06/09 02:41 No. 06/09 02:41 Might my filter definition be at fault? filt : {A : Set} → (A → Bool) → List A → List A 06/09 02:42 filt p [] = [] 06/09 02:43 filt p (x ∷ xs) with p x 06/09 02:43 ... | true = x ∷ filt p xs 06/09 02:43 ... | false = filt p xs 06/09 02:43 That looks fine to me. 06/09 02:43 Oh, wait, I know what the problem is. 06/09 02:43 | p x   is different than   | p x == true? 06/09 02:44 You're doing stuff with 'p x' where x is the element you're trying to prove is in the output of filter. 06/09 02:44 That's only useful when you know that the element you're looking for is at the head of the list. 06/09 02:45 but after casing on "el", I do know that 06/09 02:45 Hmm... 06/09 02:45 Are you able to handle the case where it's not at the head of the list? 06/09 02:47 well... no 06/09 02:47 Because you're going to have to do a 'with p y' for the head of the list in that case. 06/09 02:47 Where y is the head. 06/09 02:47 And you don't need to know about 'p x' at all in that case. 06/09 02:48 alright 06/09 02:48 sounds like I have some thinking to do then 06/09 02:48 So I'd recommend matching on xs and/or el first, and p x only when you know it's at the head of the list. 06/09 02:48 I'll probably have to start with printing xs into schope 06/09 02:49 scope 06/09 02:49 since it was implicit earlier 06/09 02:49 What you said 06/09 02:49 But I'm not sure why you wouldn't be able to fill that case. 06/09 02:49 You can actually match against implicit arguments by surrounding them with {}. 06/09 02:49 I just meant that I'd have to add them 06/09 02:50 this problem is pushing agda's emacs mode beyond its capabilities with C-c C-c 06/09 02:52 huraay 06/09 02:58 I got it through 06/09 02:58 it typechecks, is it *must* do something interesting :) 06/09 03:02 :) 06/09 03:02 Agda's not bug-free. 06/09 03:03 Not too long ago you could prove that all functions are injective. 06/09 03:03 Which is pretty egregious. 06/09 03:03 or maybe it's just true and all of mathematics is wrong! 06/09 03:06 Everything is equal! 06/09 03:06 All sets have one element. 06/09 03:06 Zero or one, I guess. 06/09 03:07 this is a huge discovery 06/09 03:07 It might make the ultrafinitists happy. :) 06/09 03:07 The largest number is 1. 06/09 03:08 http://www.youtube.com/watch?v=f3ek85X2uOE 06/09 03:08 dolio: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a9104 06/09 03:15 -!- ksf_ is now known as ksf 06/09 03:16 I don't think you should need to use inspect. 06/09 03:16 I proved it here without it. 06/09 03:17 I was thinking that that might be the case 06/09 03:17 when I saw _ 06/09 03:17 in the second element of "it" 06/09 03:17 yeah, I was able to drop the inspects 06/09 03:19 * glguy is still watching "Biggest Number" 06/09 03:19 dolio: did yours look like this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9101#a9105 06/09 03:26 Yeah, that's about what I have. 06/09 03:26 Funnily enough, those withs are both the same, since x = y in the hd case. So there might be a way to do with only one. 06/09 03:28 I don't think you can get away with less than 4 cases, though. 06/09 03:28 * glguy remembers the ... syntax 06/09 03:30 is "with" or "if_then_else_" more common in agda code? 06/09 03:31 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a9106 06/09 03:32 is there any way to simplify that top case? 06/09 03:32 Well, as I remarked here a few days back, I tend to not use booleans. 06/09 03:33 Because Set valued predicates are more generally useful. 06/09 03:33 What would you do instead, in this situation? 06/09 03:33 And then 'Decidable p' gets you back boolean-like predicates. 06/09 03:33 I'm only using them at this point because I'm following the exercises 06/09 03:34 Yeah, that's fine. 06/09 03:34 I don't think if_then_else_ sees a whole lot of use, though. It's kind of like the mixfix version of Haskell's 4-line quicksort. 06/09 03:34 heh 06/09 03:35 That is a *glowing* endorsement 06/09 03:35 That's only because Agda has dependent types, though. 06/09 03:35 sets rule, booleans drool 06/09 03:36 The equational reasoning stuff is probably a better example of why mixfix operators are awesome. 06/09 03:42 Since they make code that would be terrible to write look nice. 06/09 03:42 I like that begin thing 06/09 03:42 and the square 06/09 03:42 :P 06/09 03:42 I did some similar stuff when I was encoding from theorems from a book on mathematical logic recently. 06/09 03:43 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8234 06/09 03:44 It is time for pygments to get Agda highlighting support 06/09 03:45 it just needs to know how to run agda, I suppose 06/09 03:46 -!- pumpkin is now known as copumpkin 06/09 06:05 there's no concept of installing a lib for agda yet, is there? 06/09 15:50 I don't know of any, except that you'll have to tell the emacs mode where you put it 06/09 15:51 as in, to get the stdlib to work, I had to make my .emacs set the "agda2-include-dirs" variable 06/09 15:52 yeah, i've done that with M-x customize 06/09 16:12 it took a while to load Everything.agda :) 06/09 16:12 Yeah, luckily agda caches some information on disk so it's quicker the next time :) 06/09 16:13 ah, i as wondering that 06/09 16:14 *was 06/09 16:14 where? 06/09 16:14 I think in dotfiles in the directories where the .agda files live 06/09 16:17 ah, yeah 06/09 16:18 Does Coq assume that you can compare any two elements of the same set for equality? Does agda have this same property? 06/09 23:50 Is "{A : Set} -> A -> A -> Set" possible? (where the two Sets would be True and False) 06/09 23:53 -!- Irssi: #agda: Total of 15 nicks [0 ops, 0 halfops, 0 voices, 15 normal] 06/09 23:53 --- Day changed Mon Sep 07 2009 Ah, I worked out it 07/09 00:08 what is the coolest thing written in agda? 07/09 05:15 hmm, coolest? 07/09 05:19 most impressive, say 07/09 05:24 also, are there good exercises beyond http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf 07/09 05:25 this is somewhat related to those exercises, but there's a few differences: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.TypesSummerSchool2007 07/09 05:27 so the head of a datatype declaration looks like "data [name] [arguments] : [type] where"... what changes when i move arguments across the colon? 07/09 05:32 i.e., what is the difference between "data Foo A : Set" and "data Foo : A -> Set" 07/09 05:34 I was wondering that too... the pdf you linked to had a minor chunk about it, giving a definition for both 07/09 05:35 but not actually explaining why the distinction mattered 07/09 05:35 yeah, it did seem to imply it matters 07/09 05:35 "There is a distinction between parameters and indices of a datatype. We say that Vec is parameterised by a type A and indexed over natural numbers." 07/09 05:36 on the coolest thing, I'm not sure many people have written any major programs/proofs in agda yet, most people seem to experiment with proving statements to experiment with it (the largest actual body of agda I know is the standard library) 07/09 05:36 yeah 07/09 05:36 i thought the provably-correct lambda-calculus type inference thing from that pdf was nice 07/09 05:37 Even though "NoDup A Respects Permutation" parses correctly, would it be more acceptable to write "(NoDup A) Respects Permutation"? 07/09 09:00 The compiler may not need the brackets, but I do ) 07/09 09:01 -!- rocketman is now known as soupdragon 07/09 09:58 * glguy finishes http://web.cecs.pdx.edu/~apt/cs510coq/midterm.v in Agda :) 07/09 10:02 hey cool lets see? 07/09 10:04 anything to do with Permutation is usually really arduous 07/09 10:05 OK, I'll post it in a second ( need to do syntax highlighting ) 07/09 10:05 but you can only read it if you understand that I haven't go through at all to clean it up 07/09 10:06 That's an easy permutation. 07/09 10:06 It's got transitivity for free. 07/09 10:06 Although it's rather odd that it has you proving transitivity later. 07/09 10:07 http://www.galois.com/~emertens/midterm.agda.html 07/09 10:07 dolio: yeah, I actually skipped that since it was just a renaming 07/09 10:08 Proving transitivity without an axiom is way too hard for an exam, though. 07/09 10:12 In keeping with the exam, I defined \in as follows, but is it more appropriate to define a new Set for this relation? 07/09 10:54 _∈_ : {A : Set} → A → List A → Set 07/09 10:54 e ∈ [] = ⊥ 07/09 10:54 e ∈ (y ∷ y') = (e ≡ y) ∨ (e ∈ y') 07/09 10:54 rather than building it from the more general _∨_ Set? 07/09 10:55 As the exercises in AgdaIntro.pdf did 07/09 10:55 i wonder, i got exposed to the way it's done in Data.List.Any first 07/09 11:09 -!- EnglishGent is now known as EnglishGent^afk 07/09 13:38 I've heard it mentioned before that dealing with inductive families isn't as nice in Coq as it could be, so they tend to prefer recursive definitions of types like that \in. 07/09 14:14 Whereas in Agda, the inductive definition is often nicer to work with. 07/09 14:15 I don't know the details of what's wrong with working with inductive families in Coq, though. 07/09 14:16 the main problem is that it doesn't have dependent pattern matching 07/09 14:23 so if you have a vector and its length, and match on the vector... 07/09 14:23 you don't know anything about its length 07/09 14:23 which makes proving lots of things very hard 07/09 14:23 Ah. 07/09 14:23 and using a recursive def. like \in above instead works better? 07/09 14:25 When you use a recursive definition of vectors, you have to match on the size first. 07/09 14:25 Which isn't as big a deal when you have to do that anyway, I guess. 07/09 14:26 you then have to prove that the other cases are impossible or it'll complain that your definition isn't total 07/09 14:26 which is annoying, at best 07/09 14:27 but then when things start being indexed by vectors, and so on... 07/09 14:27 Is dependent pattern matching what you need axiom K for? 07/09 14:29 as I understand it, it helps implement dependent pattern matching 07/09 14:33 if you want to implement it via elimination rules rather than directly 07/09 14:34 I prefer it when that sort of thing is done by Anybody But Me 07/09 14:34 :) 07/09 14:34 Program makes such things feasible in Coq 07/09 14:39 -!- copumpkin is now known as sunglassedcopump 07/09 17:00 -!- sunglassedcopump is now known as copumpkin 07/09 17:09 -!- EnglishGent^afk is now known as EnglishGent 07/09 20:13 --- Day changed Tue Sep 08 2009 so when can i expect to read Real World Agda 08/09 00:15 and how do i become a master before it takes over the world 08/09 00:16 (haskell already being well on the way, i want to get ahead of the curve) 08/09 00:16 hah 08/09 00:17 You can't wait for Real World Agda if you want to stay ahead of the curve. :) 08/09 00:19 that's true 08/09 00:19 i'll need to learn Alternate Universe Agda first 08/09 00:19 how well does compiled agda perform? I remember looking at a paper on compiling agda to haskell and how painful that was 08/09 00:20 I've never tried it, myself. 08/09 00:20 people run programs? 08/09 00:20 Most langauges like Agda aren't known for being particularly speedy, as far as I know. 08/09 00:21 shouldn't a bunch of stuff get erased in compilation? 08/09 00:21 Although Agda has a lot of hooks you could use to expose efficient Haskell stuff, I suppose. 08/09 00:22 Or, not a lot. But some. 08/09 00:23 However, extracting dependently typed stuff into a language like haskell can produce code with a lot of unsafeCoercing and such. 08/09 00:26 So if GHC gets more conservative in optimization when it sees that kind of thing, that could be problematic. 08/09 00:27 Although I don't think it does. 08/09 00:27 (It's just dangerous.) 08/09 00:27 Code written to be nice to prove things about isn't necessarily the most amenable to optimization, either. 08/09 00:28 Is there a way in an arbitrary type to convince agda that (xs ++ []) == xs? 08/09 06:31 or do I need a new lemma every time 08/09 06:32 in Coq I think you would give a "rewrite" directive 08/09 06:33 hi 08/09 16:22 kmc: here are some more exercises: http://www.cs.chalmers.se/Cs/Education/Courses/types/   http://www.cs.chalmers.se/~peterd/kurser/tt03/ 08/09 16:27 -!- Saizan_ is now known as Saizan 08/09 17:19 Where can I read about the specifics of what "Prop" is? 08/09 17:34 I haven't seen a lot of documentation on it. It's not the best fleshed out area of Agda. 08/09 17:54 I think Prop < Set in the hierarchy. 08/09 17:54 And there's a flag (--proof-irrelevance maybe) that enforces the condition that any t : Prop has at most one inhabitant. 08/09 17:55 why is that condition enforced? 08/09 17:55 But I think Agda overall lacks certain conditions to make proof irrelevance properly hold, even then. 08/09 17:55 Because proof irrelevance depends on all proofs of t being equal. 08/09 17:56 And t having 0 or 1 inhabitants would seem to be a necessary condition for that. 08/09 17:57 ah, is ee 08/09 18:04 so, multiple constructors would mean that you could have more than one way of constructing the proof 08/09 18:04 yeah I don't think agda has fully implemented prop yet 08/09 18:05 the idea is that any p, q : P, with P : prop, then p and q are convertible 08/09 18:05 that gives you K, inj_t2, JMeq and all these lovely things 08/09 18:05 Conor McBride has talked on the Agda list about how proof irrelevance also requires a certain laziness to evaluation that Agda lacks. 08/09 18:06 (Coq doesn't have this either) 08/09 18:06 And I imagine it still lacks it, since I haven't heard otherwise since he mentioned it. 08/09 18:06 Of course, I think the idea in overview is to make sure proofs have no computational content, and thus you can erase them without affecting the results of your computation. 08/09 18:24 If you have two or more constructors, you can do case distinction, which affects the computation, so disallowing that is one way to get where you want to go. 08/09 18:25 You could also, I suppose, allow many constructors, but provide no way to distinguish between them, like a quotient. 08/09 18:25 But in my limited experience with type theories like that, even that is modeled like a primitive type constructor that produces a type with one inhabitant. 08/09 18:26 Like 'Squash T' has one inhabitant if T is inhabited by one or more values. 08/09 18:27 isn't that a quotient? 08/09 18:28 I found a monadic modality, that lets you implement proof irr. 08/09 18:28 Yeah. But the paper I'm thinking of takes Squash as primitive and builds up more interesting quotients using it. 08/09 18:28 Yeah, Prf or whatever? 08/09 18:30 Squash is probably the same thing. 08/09 18:30 yeah 08/09 18:30 At least, I'd expect Squash to be monadic. 08/09 18:31 The paper got a little over my head. 08/09 18:31 Is there some general way to rewrite (xs ++ []) -> xs 08/09 18:31 in types 08/09 18:31 other than defining a new lemma for every specific instance? 08/09 18:32 You should be able to prove forall xs -> (xs ++ []) == xs. 08/09 18:32 glguy, remember that cong lemma? 08/09 18:32 use that with f instantiated to whatever 08/09 18:32 oh! 08/09 18:33 sharada: everything I needed was defined in Relation.Binary.PropositionalEquality 08/09 21:54 subst, cong, sym 08/09 21:54 --- Day changed Wed Sep 09 2009 -!- codolio is now known as dolio 09/09 14:00 say I wanted to generate a list of the Fibonacci sequence up to some upper limit 'n'. I could use "unfoldr" and 'n' as my measure to ensure termination. "Obviously" there are fewer than or equal to n elements (starting at 1,2,3,5...) 09/09 23:03 but is that typically something you wouldn't want to prove directly 09/09 23:03 (that your measure is always sufficient) 09/09 23:03 if you could prove that would you even need the measure? 09/09 23:04 --- Day changed Thu Sep 10 2009 I think one thing you could do is prove that, n - fibs_i < n - fibs_i+1, and then use some sort of well-founded induction to define the list. 10/09 00:10 Wait, I have that backwards. 10/09 00:11 Anyhow, you prove that the difference shrinks on every recursive call, thus it eventually terminates, but don't specify "use up to n iterations" which just happens to be big enough. 10/09 00:13 Using unfold with a large enough n is, of course, easier. :) 10/09 00:13 could the definition of unfold be modified to insist that your measure never run out early 10/09 00:16 rather than handling that case by silently truncating 10/09 00:16 well, I'm sure it could be 10/09 00:16 would that be very useful? 10/09 00:17 I don't know. It'd probably end up being like the above well-founded induction. 10/09 00:18 ok 10/09 00:19 I'm not really sure how to specify "n is big enough" easily. 10/09 00:20 you can write fib : nat -> nat and fibs : (n : nat) -> Vector nat n 10/09 00:20 no Wf or proofs or anything 10/09 00:21 That's "first n fibs", though, not "fibs less than n". 10/09 00:21 oh 10/09 00:21 so you want (n : nat) -> fibs up to n? 10/09 00:22 yes 10/09 00:22 primarily to understand how you would go about doing it well 10/09 00:23 I would use Wf, 10/09 00:23 x "<" y := x > y /\ x < n 10/09 00:24 or perhaps x "<" y := n - x > y 10/09 00:24 (s/>/ (\all z -> z < y -> P z) -> P y) -> Acc _<_ x -> P x. 10/09 00:29 It seems unfortunate that functions have to be reimplemented completely to have them operate on different sorts (assuming Set, Set1, Set2... are sorts) 10/09 03:37 That can be rectified with universe polymorphism, but obviously Agda doesn't have it yet. 10/09 03:53 You can also use the --type-in-type flag if you don't mind being able to write paradoxes. 10/09 03:54 :q 10/09 03:58 Well, anyhow, here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9241#a9241 10/09 04:31 That's the development of a well-founded unfold. 10/09 04:31 Unfortunately, the two well-founded relations I've come up with that'd admit the fibonaccis are kind of tedious to work with in some way. 10/09 04:32 So I'm going to take a break and may or may not come back to it. 10/09 04:33 As you can see, the idea is that the step function takes a seed s_0, and produces a list element, plus a new seed s_1 that is closer to being complete, according to the relation. 10/09 04:35 dolio: thanks for the paste 10/09 05:16 -!- ToRA_ is now known as ToRA 10/09 14:46 -!- EnglishGent_ is now known as EnglishGent^afk 10/09 14:54 next project, a verified haskell compiler written in agda! ;) 10/09 16:56 that's a joke? 10/09 17:01 copumpkin: you've a lot of trust in the agda one :) 10/09 17:06 yep! 10/09 17:15 I'm not sure that's entirely justified. 10/09 17:19 is there an example of proving the monad laws somewhere? 10/09 18:45 -!- Saizan_ is now known as Saizan 10/09 18:45 for which monad? 10/09 18:46 State 10/09 18:46 i'm not sure what's an appropriate equality, in particular 10/09 18:49 just = I think 10/09 18:51 (Agda has eta conversion) 10/09 18:52 Saizan: example for Continuations http://muaddibspace.blogspot.com/2009/02/agda-supports-eta-cont-is-monad.html 10/09 19:00 glguy: thanks 10/09 19:46 though i'm stuck: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9279#a9279 10/09 19:46 i can't access the x mentioned in the error, right? 10/09 19:46 Saizan: I actually tried doing this exact thing with State last night 10/09 19:48 and I got stuck on that same one 10/09 19:48 what happens if you turn Σ into a record instead? 10/09 19:49 ooh, right 10/09 19:49 sharada: What is the difference in a data vs a record in this case? 10/09 19:51 if i remembered the syntax for records i could tell you, but more or less its that the typechecker knows that "r = record { first = first r, second = second r }" 10/09 19:55 -!- codolio is now known as dolio 10/09 19:58 yeah, it works 10/09 20:00 is there actually a difference or is it just that the type-checker likes records better? 10/09 20:07 Records have eta laws, data doesn't. 10/09 20:07 -!- EnglishGent^afk is now known as EnglishGent 10/09 20:08 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9279#a9281 <- not much to do 10/09 20:09 Equality proofs of functions typically turn out to be either trivial or impossible, in my experience. 10/09 20:18 In the absense of extensionality, of course. 10/09 20:18 For instance, as far as I can tell, it's impossible to prove (\i j k -> i + (j + k)) == (\i j k -> (i + j) + k) intensionally, where i, j and k are inductively defined, Peano naturals. 10/09 20:31 On the other hand, for Church numerals, it's trivial (==-refl), as they both normalize to (\i j k f x -> i f (j f (k f x))). 10/09 20:32 -!- EnglishGent is now known as EnglishGent^afk 10/09 21:19 --- Day changed Fri Sep 11 2009 i wonder why we can't use module syntax to instantiate a record, bad heritage from haskell? 11/09 00:04 Modules aren't precisely first-class, as far as I can tell. 11/09 01:05 Despite there being a link between records and modules. 11/09 01:05 even then allowing where and arguments on the LHS of = doesn't look problematic 11/09 01:11 Yeah, constructing records can be a bit inconvenient. 11/09 01:13 I tend to use a where clause on the definition, which just results in stuff like "foo = record { bar = bar' ; baz = baz' ; ... } where bar' = ... ; baz' = ..." 11/09 01:14 what do you think of defining right identity for monoid (a , _+_ , zero) like this: 11/09 01:14 right-id' : (λ (x : a) -> x + zero) ≡ (λ x -> x) 11/09 01:15 so i can use it with cong to prove equality of functions 11/09 01:15 is there a better way? 11/09 01:15 dolio: ah, yeah, that style is doable but tedious 11/09 01:16 I don't know. What about \x y -> x + zero vs \x y -> x? 11/09 01:17 I don't think you get that from the single-parameter variant. 11/09 01:17 So I think that's rather a losing battle. 11/09 01:17 mh, i think you do 11/09 01:18 I don't think you even get \y x -> ... 11/09 01:19 foo : (λ (x y : m) -> x + zero) ≡ (λ x y -> x) 11/09 01:20 foo = cong (λ f x y -> f x) right-id' 11/09 01:20 that typechecks 11/09 01:21 Hmm... 11/09 01:21 i've given y the type m for convenience 11/09 01:21 i need this because i've a weird hybrid between state and writer to prove a monad 11/09 01:23 Oh, of course you can do \y x -> ..., since you have essentially e == e' and need const e = const e'. 11/09 01:49 right 11/09 01:49 And I guess the \x y case is const . e == const . e'. 11/09 01:50 Although I'm finding it hard to wrap my brain around what exactly is happening with cong in that case. 11/09 01:50 not sure, it's like f is both (+ zero) and id at once 11/09 01:51 Oh, I guess it's \e x -> const (e x) is taking \x -> x (+ zero) to \x y -> x (+ zero). 11/09 01:52 Clearly these evil lambda expressions are getting in the way of my understanding simple equational reasoning. We need to move Agda to a concatenative syntax. :) 11/09 01:53 eheh :) 11/09 01:54 it'd be easier to see that we're wrapping a term around a function, i guess :) 11/09 01:54 -!- codolio is now known as dolio 11/09 01:55 I thought for a few minutes there I might have been wrong about being able to prove (\i j k -> i + (j + k)) == (\i j k -> (i + j) + k) from forall i j k -> i + (j + k) == (i + j) + k. 11/09 01:57 But that's a different case. 11/09 01:57 that requires an extensionality axiom i guess 11/09 01:57 Yeah. 11/09 01:57 though that means that defining associativity like the former makes it impossible to prove for some cases where you can prove the latter? 11/09 02:00 Yeah, I don't know how to prove the former in the first place, off hand. 11/09 02:02 Are you able to prove (\x -> x + zero) == (\x -> x) for your monoid? 11/09 02:02 i don't have any particular monoid for now, so i'm fine :) 11/09 02:03 Heh. 11/09 02:03 For instance, I don't know if it's possible to prove that for addition of naturals without proving \all x -> x + zero == x and using extensionality. 11/09 02:03 I guess what you're doing is taking a pre-extensionalized version of identity/associativity as your definition thereof. 11/09 02:05 i guess so, i've just pushed the problem further behind 11/09 02:06 at this point it'd be nicer to just prove the extensional version of my equality and use the standard formulation of the properties 11/09 02:11 You can assume extensionality as a postulate, but I'm not sure if that has negative effects or not. 11/09 02:12 You can, of course, define a datatype that models extensional equality, but it doesn't get you the sort of magic substitutivity that the usual equality gets you. 11/09 02:13 At least, I don't think it does. 11/09 02:14 I haven't played much with such types. 11/09 02:14 -!- codolio is now known as dolio 11/09 03:55 -!- codolio is now known as dolio 11/09 05:02 -!- dolio is now known as codolio 11/09 05:02 -!- codolio is now known as dolio 11/09 05:03 -!- kssreeram_ is now known as kssreeram 11/09 05:52 -!- kssreeram_ is now known as kssreeram 11/09 06:19 -!- ksf_ is now known as ksf 11/09 10:03 you can't pattern match on records, right? 11/09 13:35 -!- byorgey_ is now known as byorgey 11/09 15:12 --- Day changed Sat Sep 12 2009 Hello. Is here a channel concerning Programming-Language Agda? 12/09 12:43 --- Day changed Sun Sep 13 2009 what does it mean when emacs highlights some of my stuff yellow? 13/09 03:02 It has unsolvable metavariables. 13/09 03:05 oh no 13/09 03:05 You need to fill in some implicit parameters. 13/09 03:05 You can figure out which ones by putting in {_}. It'll highlight the unsolvable ones in yellow instead of the overall function. 13/09 03:06 it's been highlighting individual variables in my functions 13/09 03:06 Well then those presumably take implicit parameters that it can't figure out. 13/09 03:07 aha 13/09 03:08 I think that's it 13/09 03:08 Sometimes it can't figure things out that I feel like it should be able to. 13/09 03:09 But I've never gotten through the paper on it, so I don't know how it works. 13/09 03:09 yeah, this feels like it should be able to figure it out 13/09 03:10 lol, still got some yellow with no implicit arguments 13/09 03:19 oh, got rid of it 13/09 03:19 foldr :  ∀ {a} (p : ℕ → Set) {m} → (∀ {n} → a → p n → p (1 + n)) → p 0 → Vec a m → p m 13/09 03:24 for some reason it can't deal with p being implicit 13/09 03:25 can I not use (->) or \r in my functions? 13/09 03:28 oh I can, the error was elsewhere 13/09 03:29 function : (n : ℕ) → (a : Set) → (b : Set) → Set 13/09 03:35 for some reason it's highlighting the whole thing in yellow, and I have no implicit parameters at all 13/09 03:35 Highlighting it where? 13/09 03:37 that line I just pasted, it has the obvious definition 13/09 03:38 http://snapplr.com/wg84 13/09 03:38 Well, that's weird. 13/09 03:39 the funny thing is, I could've sworn it accepted it with no yellow a little while ago 13/09 03:39 then I added some other unrelated stuff and it turned yellow 13/09 03:39 hah yeah 13/09 03:40 I copied it and pasted it 13/09 03:40 and it stopped being yellow :o 13/09 03:40 obviously after reloading 13/09 03:40 It's not yellow here. 13/09 03:41 yeah, it isn't yellow here anymore either 13/09 03:41 must've just been a random fluke 13/09 03:41 I must say, it is pretty awesome to be able to write things like that without jumping through hoops 13/09 03:43 I guess it isn't that hard to write that in haskell either with type families, but this is nicer :P 13/09 03:43 It's more convenient. 13/09 03:43 hrm 13/09 03:51 VecFunction-function : ∀ {n a b} → (Vec a n → b) → function n a b 13/09 03:51 There's a fairly large class of stuff you can't do yet with type families, too, because their termination conditions are more restrictive than structural recursion. 13/09 03:52 it's not letting me "pick off" individual arguments to curry them from that function n a b 13/09 03:52 At least, type families without undecidable instances. 13/09 03:52 ah yeah 13/09 03:52 What's your definition. I've got one here. 13/09 03:57 well I just wrote VecFunction-function f a = ? and it complained that I gave too many arguments to a function type 13/09 03:59 Ah. Yeah. You can't put the a on the left side for some reason. 13/09 03:59 ah, I got it with a where block 13/09 04:06 now all I have is an off-by-one error I think 13/09 04:06 v-curry {suc n} f = λ x → v-curry {n} (λ xs -> f (x :: xs)) 13/09 04:06 oh that's so much nicer :P 13/09 04:06 I forgot about lambda 13/09 04:07 :) 13/09 04:07 * copumpkin renames his shitty names 13/09 04:08 what's the slash code for lambda? 13/09 04:11 \lambda 13/09 04:11 oh, I just got scared away by the left arrow appearing first 13/09 04:12 Might get there with \lam, I'm not exactly sure. 13/09 04:12 I don't know what else that would match. 13/09 04:12 \l 13/09 04:12 gives me a left arrow 13/09 04:12 lam doesn't appear to work 13/09 04:13 hah, http://snapplr.com/aphc again 13/09 04:13 Yeah, needs the whole word. 13/09 04:13 must be some odd transient bug 13/09 04:13 Whatever version of agda you have is crazy. 13/09 04:14 2.2.4 13/09 04:14 I've got 2.2.5. Take that! 13/09 04:14 ooh, that burns 13/09 04:15 Have you used the compiler? 13/09 04:20 MAlonzo? 13/09 04:20 once I think 13/09 04:20 unless there's more than one compiler 13/09 04:21 I still have a hole in my code so it's refusing to compile it right now 13/09 04:21 is there any way to use list literals in agda? would we define a _,_] operator and a [_ one? 13/09 04:26 list literals in the haskell sense 13/09 04:26 oh wait, that wouldn't work 13/09 04:26 You could define _] a = a :: [], _,_ a b = a :: b, [_ l = l 13/09 04:28 With appropriate precedence. 13/09 04:28 yeah 13/09 04:29 seems like that would be quite nice 13/09 04:29 except for the ability to use those separately 13/09 04:29 Conflicts with _,_ as dependent sum, too. 13/09 04:30 boo 13/09 04:31 yay, I can now write x = [ 1 , 2 , 3 , 4 ] 13/09 04:36 * copumpkin emulates matlab syntax for matrices now :P 13/09 04:36 Doesn't matlab use semicolons? 13/09 04:37 not sure that's much nicer than 1 \:: 2 \:: 3 \:: 4 \:: [] 13/09 04:37 yeah, I guess those are off-limits? 13/09 04:38 I think so. 13/09 04:38 :( 13/09 04:38 how does it resolve between [_ and _] and [_] if all three exist? 13/09 04:39 I'm not really sure. 13/09 04:40 Apparently it's too ambiguous. 13/09 04:45 ⊥-elim : {whatever : Set} → ⊥ → whatever 13/09 04:52 oh whoops :) 13/09 04:52 That function is named "naughty". 13/09 04:55 well, it has the ridiculous pattern or whatever it's called :P 13/09 04:57 ⊥-elim () 13/09 04:57 is that still naughty? 13/09 04:57 Absurd. 13/09 04:57 Yes. 13/09 04:57 how come? 13/09 04:57 Because it's a clever name. 13/09 04:57 And Conor McBride is always right. 13/09 04:58 ah, true 13/09 04:58 If you're into latin, you could call it ex-falso-quodlibet. 13/09 04:59 out of false, whatever you choose? 13/09 05:01 I guess the type signature would suggest that :) 13/09 05:02 I don't know Latin, but it's something like that. 13/09 05:02 That's (one of) the term(s) from logic. 13/09 05:03 oh I see why it's bad, I assumed that the absurd pattern was saying it was impossible, but it's actually just dealing with the fact that bottom is uninhabited, right? 13/09 05:03 Yes. 13/09 05:03 why can that function be written at all? doesn't it undermine everything? 13/09 05:04 How? 13/09 05:04 Anyhow, from the empty type to any type, you have the empty function. 13/09 05:04 oh, I guess it just behaves a bit like flip const? 13/09 05:06 oh, not even 13/09 05:06 The empty function. 13/09 05:06 If you think of a function as a set of pairs, under some restrictions, it's the empty set. 13/09 05:07 yeah, ok :) 13/09 05:07 okay yeah, I see, sorry 13/09 05:07 So A^0 = {{}} = 1 13/09 05:08 Including 0^0. 13/09 05:08 makes sense 13/09 05:08 Although for 0^0, it can also look like \x -> x, which is confusing, I guess. 13/09 05:09 Anyhow, what you're saying is impossible when you use the absurd pattern is that any constructors could result in a value of that type. 13/09 05:12 --- Day changed Mon Sep 14 2009 -!- copumpkin is now known as Meow 14/09 01:57 -!- Meow is now known as copumpkin 14/09 02:05 --- Day changed Tue Sep 15 2009 Hello, is there anybody listening here? 15/09 11:46 I need some help regarding font settings for Agda/emacs. 15/09 11:47 Hello? 15/09 11:47 Hmm. 15/09 11:48 as I just tweeted: Discovered nice undocumented feature in agda: put functions in a record declaration - they'll be added to the created module. Bit like OOP! 15/09 14:14 greenrd: This isn’t undocumented. 15/09 14:28 That is, it is documented. :-) 15/09 14:28 15/09 14:29 page 19 15/09 14:29 ah, I meant in the reference manual 15/09 14:29 There is a reference manual? 15/09 14:30 on the wiki 15/09 14:30 On , I cannot find a link to a reference manual. 15/09 14:30 I always used the above tutorial. 15/09 14:31 I already discovered that this doen’t mention everything. 15/09 14:31 For example, I found the keyword “abstract” in the standard libs. 15/09 14:31 Which is not described in this tutorial. 15/09 14:31 And I have no idea what it is about. :-( 15/09 14:31 manuals & howtos, first link on that page 15/09 14:33 btw, some slides from the talks at AIM are online now 15/09 14:34 cool 15/09 14:39 * greenrd takes a look 15/09 14:39 oh, so defining a record type automatically defines a module? 15/09 14:39 Saizan: yeah - didn't you know that? :) 15/09 14:40 so you can say open Foo to bring the field accessor functions for Foo into scope 15/09 14:41 or open Foo bar if Foo requires a parameter 15/09 14:41 the reference manual said something like that, but i thought you had to do it manually 15/09 14:41 no 15/09 14:41 i think the module is always parametrized on an instance of the record 15/09 14:42 whoops yeah, that's right 15/09 14:42 so you need "open Foo someFoo" ? 15/09 14:42 yeah 15/09 14:42 it's a shame setzer hasn't posted his slides, he has done some pretty cool gui apps in agda that termination check :-) 15/09 15:03 --- Day changed Wed Sep 16 2009 -!- eelco_ is now known as eelco 16/09 09:56 --- Day changed Thu Sep 17 2009 is the complete code for the Observational Equality paper available somewhere? 17/09 17:22 --- Day changed Fri Sep 18 2009 -!- codolio is now known as dolio 18/09 00:40 -!- codolio is now known as dolio 18/09 02:58 -!- dolio is now known as opdolio 18/09 02:59 -!- opdolio is now known as dolio 18/09 03:00 -!- E_G is now known as EnglishGent 18/09 06:33 what is the purpose of InitLast here? http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Vec.html#4062 18/09 07:54 I guess it's just to easily do a reverse :: constructor so you can pull init and last out in one fell swoop? 18/09 07:56 It's a view. 18/09 07:57 makes sense :) 18/09 07:57 http://sneezy.cs.nott.ac.uk/~npo/PowerPi.pdf 18/09 07:57 Or, I think it's a view... 18/09 07:59 Man, why do the standard libraries use 0-10 for precedences? 18/09 08:00 it looks like a view 18/09 08:00 Oh, yeah, it is. 18/09 08:01 Because ::r in the type evaluates into a regular vector. 18/09 08:02 yeah 18/09 08:02 oh! 18/09 08:02 I think I just realized the difference between being indexed by something and being parametrized by it 18/09 08:02 I remember the agda intro paper I read claimed there was a difference but just said something along the lines of "if you're on the right of the colon, you're indexed" 18/09 08:03 Indices can be specified as anything of the appropriate type in the 'return type' of the constructor, whereas parameters are always just the variable name, but parameters are scoped over the entirety of the data definition. 18/09 08:09 yeah 18/09 08:09 And only indices can cause type refinement, I think. 18/09 08:09 They're what make Generalized Algebraic Datatypes generalized. 18/09 08:10 yeah, that was what made me realize, when the paper you just linked to it showed and compared it to a GADT 18/09 08:10 Yeah, GADTs are like inductive families, except the indices are limited to thinks of kind *. 18/09 08:11 Or, maybe things with kinds... 18/09 08:11 Yeah, any kind, I guess. 18/09 08:11 am I allowed to make both Fin and Nat into the builtin natural type? it'd be fun to have it prevent me from writing numbers larger than a certain value 18/09 08:12 Which, I suppose, makes them not "inductive" families, strictly speaking, because the kind level is not inductively defined. :) 18/09 08:12 makes sense 18/09 08:12 I suspect the answer is "no". 18/09 08:12 damn :) 18/09 08:16 is there a nicer way to define Fin than mirroring Nat? 18/09 08:17 Not that I've seen. 18/09 08:19 Having a built-in for Fin would probably be a good idea, though. 18/09 08:34 If you take Fin n as being Z/n, and use it for fast modular arithmetic. 18/09 08:35 yeah 18/09 08:35 I was just writing a _mod_ for my nats 18/09 08:36 hmm, the standard library isn't working for me :o 18/09 08:54 if I import Data.Vec, it complains that Monoid isn't in scope in Data.List 18/09 08:55 the standard library is remarkably extensive 18/09 09:03 there's so much indirection in the standard library 18/09 09:26 hmm, my Algebra module in lib-0.2 seems broken 18/09 09:32 _mod_ is tough. 18/09 09:38 Finally got it. 18/09 09:39 Well-founded recursion is my new best friend. 18/09 09:43 hi 18/09 15:45 hi 18/09 15:46 in Data.List.Properties; where does begin and \qed come from? as far as i can see EqReasoning is never opened? 18/09 15:46 hmm, i got it working somehow, so i guess it doesn't matter :-) 18/09 15:51 btw, http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/ 18/09 15:51 the induction module in the std lib admits that its types are hard to follow, but that agda can normalize them for me 18/09 17:49 how can I get that? 18/09 17:49 has anyone here played with lib-0.2? the Algebra module seems broken, on mine at least 18/09 19:23 broken how? 18/09 19:24 it doesn't appear to be exporting what it should be exporting. I try to import Data.Vec, which imports Data.List, and List contains a Monoid "instance", but it complains that Monoid isn't in scope 18/09 19:25 seems OK with the development version 18/09 19:29 what does your code look like? 18/09 19:31 hmm, maybe I'll try that 18/09 19:31 I was just trying the lib-0.2 tarball 18/09 19:31 my code is empty 18/09 19:31 I just tried importing Data.Vec 18/09 19:32 well, Data.Vec doesn't export Monoid, you need to import that from Algebra 18/09 19:32 module Foo where 18/09 19:32 open import Data.List 18/09 19:32 open import Data.Nat 18/09 19:32 open import Algebra 18/09 19:32 open Monoid (monoid ℕ) 18/09 19:32 I don't expect it to export it 18/09 19:32 that works 18/09 19:32 I mean 18/09 19:33 all I type in my code is open import Data.Vec 18/09 19:33 nothing else 18/09 19:33 and emacs opens up Data.List automatically, with a highlighted Monoid 18/09 19:33 saying it's not in scope 18/09 19:33 oh, weird 18/09 19:33 yeah, don't know 18/09 19:33 I also tried Induction and it also complained about another missing algebraic structure 18/09 19:34 so I assumed Algebra was the culprit :) 18/09 19:35 but I'll grab the more recent lib 18/09 19:35 yeah, might be.  I'd be a little surprised if it was broken though... usually the thing is fully compiled as a test before release 18/09 19:35 well 18/09 19:35 if you get the darcs lib, you will also need the darcs agda 18/09 19:35 oh 18/09 19:36 what's new? 18/09 19:36 few small things mostly... biggest one is a way to reduce primitive equality, so you can reason about it, say for strings 18/09 19:36 there's a couple of bigger changes that will be in there soon from the stuff at AIM 18/09 19:37 universe polymorphism :) 18/09 19:37 and cabal support 18/09 19:37 :O 18/09 19:37 nice! 18/09 19:37 yeah, when I import Induction it complains about CommutativeSemiring being missing from Data.Nat.Properties 18/09 19:40 what version of agda do you have? 18/09 19:41 not sure if it matters, but stil 18/09 19:41 2.2.4, with lib-0.2 18/09 19:41 ok... I'll try to test with those versions later and see if I get any problems 18/09 19:42 thanks :) 18/09 19:42 Data.Vec (List) and Induction have been the painful ones so far 18/09 19:42 k 18/09 19:42 who writes the std lib by the way? it's got WAY more stuff than I thought it did 18/09 19:44 just reading the readme made me think it was just a few modules, but Everything has a lot of awesome stuff 18/09 19:44 Nils Anders Danilesson does most of it 18/09 19:45 some of it is adapted from older code from Ulf 18/09 19:45 but yeah, there's some really cool stuff in there 18/09 19:45 what kind of stuff do you do with agda? 18/09 19:48 so far I've just been taking really simple statements I know to be true and tried to prove them :P 18/09 19:49 I'm a real newbie with this stuff :) 18/09 19:49 that's cool :) 18/09 19:49 I only started with haskell a few months ago, so this seemed like the next step from the types perspective 18/09 19:49 yeah 18/09 19:50 did you find it tricky to start learning the std library? 18/09 19:51 (aside from the probs you just mentioned) 18/09 19:52 the basics are quite simple, the ones with obvious analogs in haskell, like Nat, Vec, List, etc. For the more complicated things there's a lot of indirection 18/09 19:52 yeah... maybe a little too much 18/09 19:53 in the sense that figuring out some of the less basic proofs requires me to look at two or three unrelated modules 18/09 19:53 I'm starting to get used to it 18/09 19:53 that's good 18/09 19:54 --- Day changed Sat Sep 19 2009 I tried to compile the darcs agda 19/09 00:40 but I don't think I got agda-executable out of it 19/09 00:40 does that live somewhere else? 19/09 00:40 so 2.2.5 and the most recent lib fixed my issues, yay 19/09 00:49 -!- opdolio is now known as dolio 19/09 01:02 I feel that rec is the induction function I need 19/09 04:36 from Induction.Nat 19/09 04:37 it claims its type is 19/09 04:37 (P : ℕ → Set) → ((x : ℕ) → Rec P x → P x) → (x : ℕ) → P x 19/09 04:37 That looks sensible. 19/09 04:38 This is another reason why learning about the y-combinator is important. 19/09 04:39 I don't quite get how to use that Rec term 19/09 04:39 it seems to contain the base case and recursive case? 19/09 04:40 Some fancy induction principles look like Y. 19/09 04:40 ah, interesting 19/09 04:40 Y : (a -> a) -> a, wf-induction : ((z < y -> P z) -> P y) -> P x 19/09 04:41 So you get to make recursive calls as with a fixed-point combinator, you just have to prove something about the recursive calls you're making. 19/09 04:42 oh, interesting 19/09 04:42 hmm 19/09 04:44 To turn rec's type into well-founded induction, you do "Rec P x = {y : _} -> y < x -> P y". 19/09 04:44 I think that's right. 19/09 04:44 what's the {y : _} mean? 19/09 04:44 It's what \all y means. 19/09 04:45 oh, I didn't realize 19/09 04:45 Since I'm not going to fire up emacs to type this stuff. 19/09 04:45 :) 19/09 04:45 Anyhow, with the way Rec is defined, apparently it's just another way to do ordinary induction on naturals. 19/09 04:49 But I think the point of the induction framework is rather to do stuff like: 19/09 04:49 rec : (Rec : RecStruct Nat) (P : Nat -> Set) -> ((x : Nat) -> Rec P x -> P x) -> (x : Nat) -> P x 19/09 04:50 Which is parameterized by the induction principle. 19/09 04:51 So you can do rec Rec for normal induction, and rec WellFounded for well-founded induction, and whatever else. 19/09 04:51 Rec P zero = \top ; Rec P (suc n) = P n, so in the original type... 19/09 04:52 ah, cool 19/09 04:52 if f is the (x : nat) -> Rec P x -> P x... 19/09 04:53 when x = zero, you get \top -> P zero which is isomorphic to P zero 19/09 04:53 And when x = suc n you get P n -> P (suc n) 19/09 04:53 Which looks like normal induction: ((x : Nat) -> P n -> P (suc n)) -> P zero -> (x : Nat) -> P x 19/09 04:54 Er, I mixed up my variables there. 19/09 04:54 You get the idea, though. 19/09 04:54 It's similar to how you can do foldr : (a -> r -> r) -> r -> [a] -> r or foldr : (Maybe (a,r) -> r) -> [a] -> r 19/09 04:55 yeah 19/09 04:58 * copumpkin is trying to prove the first induction I ever did, from high school, in agda (the sum of odds being perfect squares) 19/09 04:58 Hmm... It's been a while since I thought about that. 19/09 05:02 it's pretty simple induction, I'm mostly just trying to figure out how to express it :) 19/09 05:02 I guess you use Sum_0^(n-1) 2*i+1 = n^2? 19/09 05:02 I actually expressed the odds more subtly, which might make my life harder later though 19/09 05:03 well, more directly 19/09 05:03 first odd = 1, and then next odd is suc suc of it 19/09 05:03 I don't know if that's better or worse. 19/09 05:08 yeah, I guess this is pretty easy if you assume a lot of "high school -level math" 19/09 05:08 but I haven't thought of what properties of naturals I'll be needing 19/09 05:08 Well, you'll need something like (n + 1)^2 = n^2 + 2*n + 1, at least, I think. 19/09 05:09 yeah 19/09 05:09 That's actually exactly what you get in the inductive case with the 2*i+1 formulation. 19/09 05:09 You ever figure out _mod_? 19/09 05:22 nope :( 19/09 05:23 That isn't actually that surprising. 19/09 05:23 I was thinking of repeatedly subtracting the right hand side 19/09 05:23 copumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9531#a9531 19/09 05:40 oh nice, thanks :) 19/09 05:41 dolio: is there a way to state that your mod function only takes >=1 for its second parameter? with (suc n) or something? 19/09 05:54 (to avoid the maybe) 19/09 05:55 Yeah, you could require a proof. 19/09 05:56 but not just in the type somehow? 19/09 05:57 Yes, in the type. 19/09 05:57 _mod_ : ℕ → ((suc k) : ℕ) → Fin k ? 19/09 05:58 _mod_ : Nat -> (k : Nat) -> (0 < k) -> Fin k 19/09 05:58 yeah, I could see that 19/09 05:58 but it seems like it should be possible to write the constructor in the type to prevent 0 19/09 05:58 maybe not :) 19/09 05:58 You could do _mod_ : Nat -> (k : Nat) -> Fin (suc k) 19/09 05:59 h 19/09 05:59 m 19/09 05:59 But then n mod k means n mod (suc k) in actuality. 19/09 05:59 oh, ok 19/09 05:59 has there been any work on dependent types with subtyping? 19/09 06:04 NuPRL has some kind of subtyping. 19/09 06:05 Like you can have B \subset A. 19/09 06:06 ah, cool 19/09 06:06 I'm not sure if that's useful for the usual uses of subtyping or not. 19/09 06:06 that mod thing you gave me is so clear 19/09 06:08 Excellent. :) 19/09 06:08 I'm used to having to jump around between a dozen files when reading the std lib :P 19/09 06:09 oh, names can overlap? your constructors for Fin and Nat have the same name 19/09 06:10 Constructor names can overlap. 19/09 06:10 excellent! 19/09 06:10 Because it's unambiguous. 19/09 06:10 makes sense 19/09 06:11 I guess it'd be easy to make mod into modRem 19/09 06:37 Yeah. 19/09 06:37 or divMod, rather 19/09 06:37 :P 19/09 06:38 It's actually kind of a pain, because you need to modify the well-foundedness criterion. 19/09 06:38 oh 19/09 06:38 But it's not that hard. 19/09 06:38 * copumpkin tries 19/09 06:38 by the way, I can't define fix suc in agda, right? 19/09 06:40 or not without additional machinery 19/09 06:40 You can't define fix. 19/09 06:40 Or, you can, but it won't pass the termination checker. 19/09 06:41 I see 19/09 06:41 Which won't actually prevent you from using it, but it will be colored pink. 19/09 06:41 does that mean I can't import the module or something? 19/09 06:41 No. 19/09 06:41 Also, if you use something like fix suc in a type, it'll go into a loop trying to compute its normal form. 19/09 06:42 oh :) 19/09 06:42 At least, last I checked. 19/09 06:42 Something like "inf = suc inf" is a valid coinductive natural, though. 19/09 06:44 so if I wanted to represent "the unbounded natural" in a typechecker-friendly manner, I'd need a third constructor for Nat? 19/09 06:46 I guess. If you just want Naturals + infinity, the coinductive version might be better, depending on what you want to do with it. 19/09 06:47 hmm, not sure yet :) really just poking around to see 19/09 06:54 any idea why product is defined with the "snd" as a function of fst? http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Product.html#392 19/09 07:02 That's dependent sum. 19/09 07:05 Binary products are a special case of dependent sums just like ordinary functions are a special case of dependent products. 19/09 07:06 :o 19/09 07:06 oh! 19/09 07:07 so the odd ⊎ symbol is (,) in hasell land 19/09 07:07 haskell 19/09 07:07 and \x can't be represented 19/09 07:07 No. That's ordinary sum. 19/09 07:07 oh, hmm 19/09 07:07 oh I see 19/09 07:07 Dependent sums are a generalization of regular sums, in a way. 19/09 07:08 so sum = Either, product = (,), but dependent sum = ~ (,) with more? 19/09 07:08 With regular sums, you have a finite set of tags (2 of them for the binary one), and a type for each tag. 19/09 07:09 And the sum is the union of those types tagged with the tags. 19/09 07:09 yeah 19/09 07:10 I've heard of sum types and product types colloquially 19/09 07:10 So, dependent sum, Sigma, is the generalization of that to where the tags are an arbitrary type. 19/09 07:10 oh, hmm 19/09 07:10 In Sigma a P, for each x in a, there's an injection into the sum \w -> x , w : P x -> Sigma a P 19/09 07:11 And you get back regular sums by taking some finite set of tags as a. 19/09 07:11 So if you had SumTags = Inl | Inr... 19/09 07:11 And T : SumTags -> Set 19/09 07:12 aha, I think I get it 19/09 07:12 so you can think of it as an index 19/09 07:12 Sigma SumTags T has "Inl, (w : T Inl)" and "Inr , (w : T Inr)" as elements. 19/09 07:12 that's neat 19/09 07:12 Which is isomorphic to "T Inl \uplus T Inr". 19/09 07:12 BUT 19/09 07:13 If instead you take T to be a constant function... 19/09 07:13 Then you get Sigma a (\_ -> b) has elements of b tagged by elements of a. 19/09 07:14 Which is a binary product. 19/09 07:14 interesting 19/09 07:14 Similarly, the important part about product A x B is that you have projections from it to A and B... 19/09 07:14 Or finite n-ary products have n such projections. 19/09 07:15 So, to get the dependent version of that, you have an a-indexed family T : a -> Set... 19/09 07:15 And given the product for that family (f : Pi a T), you need a projection corresponding to each a. 19/09 07:17 Which looks like, for x \in a, "f x : T x" 19/09 07:17 You get back finite n-ary products via (fn : Fin n) -> T fn 19/09 07:18 But you also get functions (_ : a) -> b 19/09 07:19 By ignoring the type dependence in the same way. 19/09 07:20 wow 19/09 07:20 Or, however you want to say that. 19/09 07:20 this feels so deep :P 19/09 07:20 I guess it's similar to how you can define addition by repeated incrementing, multiplication by repeated addition, exponentiation by repeated multiplication 19/09 07:20 in some sense, at least 19/09 07:21 Yeah, well... 19/09 07:21 if in 'Sum_0^n a_i' you take a_i = b, you get b*n. 19/09 07:22 Where a_i = b is like the constant function that ignores i. 19/09 07:22 So, yeah. 19/09 07:22 so cool :) 19/09 07:23 Does that make sense as being related? I'm not entirely sure now. 19/09 07:24 I guess it's similar. 19/09 07:24 I think I get it, but I'm still trying to absorb it all 19/09 07:24 If you know the categorical definitions for products and coproducts, it becomes pretty clear if you try to write down what a generalization would look like. 19/09 07:27 I do roughly know what products and coproducts are 19/09 07:28 but haven't actually done anything significant with it (I know what the diagram looks like and why) 19/09 07:28 Like "a finite some of objects A_i is an object Sum A with morphisms in_i : A_i -> Sum A, and Sum A is initial" 19/09 07:29 sum, even. 19/09 07:29 So "a dependent sum of an a-indexed family T is an object Sigma a T with an a-indexed family of injections in : (x : a) -> T x -> Sigma a T, and Sigma a T is initial." 19/09 07:31 Which, _,_ is exactly that type. 19/09 07:31 And then dependent uncurry corresponds to initiality. 19/09 07:32 Because it takes some other family of injections (x : a) -> T x -> S to a morphism Sigma a T -> S. 19/09 07:33 I think I see 19/09 07:43 * copumpkin needs to ruminate :) 19/09 07:43 (is there any way to get scoped type variables in agda?) 19/09 07:43 if foo : {a : Set} -> ..., do 'foo {a} ... = ...' 19/09 07:44 Then a is in scope in a where clause. 19/09 07:44 oh 19/09 07:44 hmm, but I need it in my type annotation 19/09 07:46 It's in scope in the type annotations of the where clause, too. 19/09 07:46 hrm 19/09 07:48 oh I see 19/09 07:49 :O 19/09 07:54 op opdolio 19/09 07:55 damn, my divMod compiles but contains both yellow and pink 19/09 07:55 Paste it. 19/09 07:58 it's too naive, but sure 19/09 07:59 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9534#a9534 (I added this onto the code you pasted) 19/09 08:00 far too simplistic :P 19/09 08:00 Well, yeah. I used well-founded induction for a reason. 19/09 08:00 Agda can't tell that (x - y) is structurally smaller than x. 19/09 08:01 yeah, makes sense 19/09 08:01 You actually might be able to get away with just well-founded induction on the naturals, same as mine. 19/09 08:03 I was thinking of carrying along the div part to keep it tail recursive. 19/09 08:03 But if you match on the result like that, you only need to make recursive calls on naturals. 19/09 08:03 I see 19/09 08:04 gotta go home now, I'll try again in a bit :) thanks for all your help! 19/09 08:04 So it's roughly the same code. 19/09 08:04 No problem. 19/09 08:05 ciao! 19/09 08:05 -!- opdolio is now known as dolio 19/09 08:08 copumpkin: It occurred to me that the non-dependent analogue of what we were talking about yesterday is stuff like A + A ~ 2 x A and A x A ~ 2 -> A, so yes, repeated sum/product. 19/09 18:13 oh yeah 19/09 18:14 A -> A ~ 2 --> A :P 19/09 18:14 Yeah. Tetration types. 19/09 18:15 Write a paper! 19/09 18:15 hah 19/09 18:15 -!- koninkje_away is now known as koninkje 19/09 21:22 --- Day changed Sun Sep 20 2009 -!- jfredett_ is now known as jfredett 20/09 00:41 -!- koninkje is now known as koninkje_away 20/09 01:57 -!- koninkje_away is now known as koninkje 20/09 03:45 -!- koninkje is now known as koninkje_away 20/09 03:56 http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Relation.Binary.PreorderReasoning.html#1084 seems very elegant 20/09 05:44 ooh, difference naturals! 20/09 05:47 so much to explore! 20/09 05:48 I wonder why there's no matrix stuff in the standard library? is it because there aren't any fields or modules in the algebra module yet? 20/09 05:49 oh, we have integers and naturals in the std lib 20/09 05:59 I mean integers and rationals 20/09 05:59 I wonder why there isn't a Field structure yet, or a Vector space 20/09 06:02 wow, constructing a rational takes some serious proof! _÷_ : (numerator : ℤ) (denominator : ℕ) 20/09 06:05 {coprime : True (C.coprime? ∣ numerator ∣ denominator)} 20/09 06:05 {≢0 : False (ℕ._≟_ denominator 0)} → 20/09 06:05 ℚ 20/09 06:05 Those proofs might be automatic... 20/09 06:12 :o 20/09 06:13 True takes a decidable predicate, turns it into a bool, and then asserts that it's true. 20/09 06:13 Similarly for false. 20/09 06:13 False, even. 20/09 06:13 ah 20/09 06:13 Which seems roundabout, but maybe that's so that it can compute it via the algorithm that decides the predicate, rather than requiring proof be supplied. 20/09 06:14 At least, that's all I can come up with. 20/09 06:14 I hadn't seen that before, but if it works, it might be nice... 20/09 06:15 yeah :) 20/09 06:18 there's so much cool stuff hidden away in Everything 20/09 06:18 the front page of the readme really doesn't do it justice 20/09 06:18 is there a good way to see a list of all unicode characters I can type in emacs? 20/09 06:26 If you type \ and then tab, a giant list pops up. 20/09 06:28 nice, thanks! 20/09 06:29 have you noticed any good way of typing ^T (for matrix transpose?) 20/09 06:30 No. There aren't a lot of unicode super/subscripts it seems. 20/09 06:32 ah well, I can live with english for now 20/09 06:32 I must say, these assertions on decidable predicates don't seem convenient. 20/09 06:50 any idea how to use algebraic structures from http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Algebra.Structures.html#268 ? 20/09 06:55 These are just the laws things have to follow. 20/09 06:57 The things you use are named without the Is 20/09 06:58 oh yeah, I just need {a : Monoid} 20/09 06:58 because Monoid is Set\_1 20/09 06:58 And the way you use them is to open them, I think. 20/09 06:58 I see 20/09 06:58 Because you need access to the carrier, and not opening them is a huge pain with the qualified names. 20/09 06:58 I don't get the raw counterparts to things 20/09 06:59 Raw is just the operations, without the laws. 20/09 06:59 for quick and dirty programs? 20/09 06:59 I'm not sure why they're split up like that. 20/09 07:00 open Monoid using (carrier) identity : {n : ℕ} → {m : Monoid} → Mat n n (carrier m) 20/09 07:11 does that seem "idiomatic"? 20/09 07:11 I guess it needs more than a monoid 20/09 07:12 a semiring or something 20/09 07:13 yeah 20/09 07:14 damn, decisions 20/09 07:14 record SemiringWithoutAnnihilatingZero : Set₁ where 20/09 07:14 now I need to decide if I want the module to be parametrized over a field or something, or just to open the structures I need locally for each operation 20/09 07:16 I need RecordWildcards in agda :P 20/09 07:23 * copumpkin goes crazy with Algebra.agda 20/09 08:38 * copumpkin started writing an IntegralDomain record in Algebra 20/09 09:15 having trouble writing the "no zero divisors" property though 20/09 09:39 yay, I have identity matrix and transposition working 20/09 19:36 and multiplication! 20/09 19:45 Nice. 20/09 19:51 haven't proved anything about them yet :P 20/09 19:51 I could've sworn the std lib Data.Vec had a Vec A n -> Fin n -> A 20/09 20:09 It must. 20/09 20:10 aha, lookup 20/09 20:12 * copumpkin holds off on the left- and right-identity proofs for matrix multiplication for now :P 20/09 20:50 any ideas for a good left-multiply-by-vector and right-multiply-by-vector symbol? 20/09 21:04 I still thought lookup used to have a counterpart called _[_] 20/09 21:44 I'm having trouble reusing the Algebra.FunctionProperties for matrices, as it seems hard to get the operation to depend on implicit parameters 20/09 21:55 I want +-assoc : Associative _+_, where _+_ : ∀ {m n} → Op₂ (Mat carrier m n) 20/09 21:56 it colors it in yellow because (I assume) it can't figure out m and n 20/09 21:56 when I open the Algebra.FunctionProperties there's an implicit parameter for the set I'm working over, but I can't seem to fix the m and n there 20/09 21:57 the type of sum in Data.Vec seems too specific... it feels like it should open Monoid and use the operation in there 20/09 22:10 http://snapplr.com/npeb seems odd, that it would not like the simpler type but not mind the more complex one 20/09 22:26 mmm, 12 holes in my code :P 20/09 22:58 this is no good: http://snapplr.com/c3hz 20/09 23:04 --- Day changed Mon Sep 21 2009 ∣_∣ : ∀ {n} → Mat carrier n n → carrier 21/09 00:15 not sure how to grab the implicit parameter there 21/09 00:16 Which? 21/09 00:17 oh I guess I can write ∣_∣ {0} mat = 1# 21/09 00:17 Oh. Right. 21/09 00:17 now, should I require people to provide a proof that a matrix is invertible, or return a Maybe from my inverse function? 21/09 01:26 Is invertability decidable? 21/09 01:27 I guess it's det m /= 0? 21/09 01:27 why wouldn't it be? 21/09 01:27 yeah 21/09 01:27 It's been a while since I did this stuff. 21/09 01:28 Anyhow, you can make two versions, if you want. 21/09 01:28 true 21/09 01:28 Write the one that takes the proof first, and then write one that wraps that in a Maybe. 21/09 01:28 how would I wrap it in a Maybe? I'm not sure how I'd call the one that wants a proof without it 21/09 01:29 You do case analysis on the decision procedure for the proof. 21/09 01:30 inv m with invertable m ; ... | yes pf = just (inv' m pf) ; ... | no _ = nothing 21/09 01:31 Or invertable? or whatever you call it. 21/09 01:31 oh, I see :) 21/09 01:31 know of any even/odd functions in the std lib? 21/09 01:36 Not off hand. But I don't use the standard libraries much. 21/09 01:36 I like defining Sigma over and over. 21/09 01:37 I read the Coq manual on their Notation construct (similar to mixfix), and it has some nice features. 21/09 01:38 Like, you can define new binding constructs. 21/09 01:38 I can use http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Nat.Divisibility.html#180 for even/odd I guess 21/09 01:38 So you could define a Sigma x:a T 21/09 01:38 Sigma? 21/09 01:39 In fact, their notation { x : a | T } is actually defined using the Notation, I think. 21/09 01:39 Dependent sum. 21/09 01:39 oh that :) 21/09 01:39 In Agda you have to write Sigma a (\x -> T) instead. 21/09 01:40 interesting 21/09 01:45 I wonder if Coq's notation could be used to write list comprehensions 21/09 01:46 Oh, that's another thing. I'm not sure if you can write comprehensions, but it has an experimental feature for defining stuff like [ a , b , c , d ]. 21/09 01:46 fun 21/09 01:48 Other than that, it's just noisier than Agda. 21/09 01:49 * copumpkin is still curious about these famous tactics in coq that everyone raves about 21/09 01:50 Those are two pretty big features, though. 21/09 01:50 Tactics let you describe how to prove something instead of doing it manually via doing C-c C-c and C-c C-space and such in Agda mode. 21/09 01:51 Instead you say stuff like "try induction" and it figures out what specifically to do automatically. 21/09 01:52 And you can write new tactics, too. 21/09 01:53 oh wow 21/09 01:53 If a proof is simple enough, you can just say "figure it out yourself". 21/09 01:53 * copumpkin is still trying to write determinant 21/09 01:57 Well, they won't help you with that. 21/09 02:00 yeah :) 21/09 02:00 C-c C-a never seems to work, what is it supposed to do? 21/09 02:01 What's it called? I'm not familiar with that one. 21/09 02:02 if I right click on a goal, it says "auto", with that shortcut 21/09 02:02 Huh. 21/09 02:03 http://snapplr.com/r8dn 21/09 02:04 That must be new, because I don't have it. 21/09 02:05 :o 21/09 02:11 I just pulled and the first two patches were "Adding Auto" and "Auto update". 21/09 02:12 Doesn't say what it does, though. 21/09 02:12 fun 21/09 02:12 I've tried it in a bunch of places 21/09 02:12 but each time it says it failed 21/09 02:12 Also "added propositional equality to the builtin types" which sounds interesting. 21/09 02:13 I guess that's for the "trustMe : {A : Set} {a b : A} -> a == b" 21/09 02:16 why it's qualified with "propositional"? 21/09 02:19 is there some way I can get more helpful variables than _354? 21/09 02:19 (suc m) != (Data.Nat._+_ (toℕ n) (_354 m mat n)) of type ℕ 21/09 02:19 Not that I know of. And I'm not really sure why it's called propositional equality. 21/09 02:20 and, btw, i try to ask again, anyone knows where i can find the code for "Observational Equality Now!"? 21/09 02:20 more helpful? 21/09 02:21 fresh variables like those suggest that it didn't unify that part with anything 21/09 02:21 Oh, maybe it's propositional because x == y is isomorphic to (T x -> T y)*(T y -> T x). 21/09 02:22 Which, 'equality' of propositions is bi-implication. 21/09 02:22 Saizan: I have it, but I don't remember where I got it. 21/09 02:23 http://code.haskell.org/Agda/examples/outdated-and-incorrect/OTT/ 21/09 02:24 "outdated-and-incorrect" sounds promising :) 21/09 02:25 thanks :) 21/09 02:25 :) 21/09 02:25 hmm, it seems rather difficult to call splitAt or take/drop on Data.Vec 21/09 02:28 I guess I need to convince it that my index is within the bounds 21/09 02:28 -!- jfredett_ is now known as jfredett 21/09 02:32 * copumpkin concludes he needs Data.Fin.inject+ 21/09 02:39 actually 21/09 02:39 just _<_ probably 21/09 02:40 ack 21/09 02:54 i wonder if it wouldn't make more sense to define Fin n = \Sigma N (\m -> m < n) 21/09 03:07 for the life of me I can't seem to call Data.Vec.splitAt 21/09 03:07 It is clearly quite wasteful to have both Fin n and m < n when they obviously have the same structure. :) 21/09 03:23 Depending on your definition of _<_. 21/09 03:23 splitAt : ∀ {a} m {n} (xs : Vec a (m + n)) → SplitAt m xs, shouldn't it be able to infer that if m is Fin (suc (m + n)), then calling splitAt (toN m) is good? 21/09 03:25 I guess it isn't trivial 21/09 03:26 Surely m's type doesn't refer to itself. 21/09 03:29 Or, refer to m, rather. 21/09 03:30 I abused notation a bit there 21/09 03:30 I meant, given the length of xs there 21/09 03:30 m is of type Fin (suc ) 21/09 03:30 Anyhow that means toN m < m' + n 21/09 03:31 So you're trying to call splitAt with toN m and a vector with length m' + n. 21/09 03:32 But toN m /= m' 21/09 03:32 However, given toN m < m' + n, you should be able to find n' such that m' + n = toN m + n', which means you can cast your vector to the type Vec a (toN m + n') and call splitAt. 21/09 03:33 so I need to explicitly subtract to get hold of the n? 21/09 03:34 The proof will look something like subtraction, I guess. 21/09 03:36 copumpkin: It's probably easier to write a new splitAt for finite sets. 21/09 03:44 I see 21/09 03:45 I'll play with that 21/09 03:45 Or, maybe it isn't, with that SplitAt type. I'm not really sure. 21/09 03:46 I must be missing something, cause this feels more complicated than it needs to be 21/09 03:47 Oh crap. I have to rebuild Agda now. 21/09 03:52 how come? 21/09 03:52 I did darcs pull on the library, and the new "trustMe" equality thing blows up without runtime support. 21/09 03:53 ah 21/09 03:53 I guess I'll get to try and figure out what auto does. 21/09 03:54 is anders the main author of the std lib? 21/09 04:01 Yeah. 21/09 04:03 Although I'm not really sure what all are contributions. 21/09 04:03 Other than the delimited continuation monad, which I did. 21/09 04:03 ah :) 21/09 04:04 Although I'm not really happy with that version, because that monad wants type indices not value indices like the indexed monads in the library. 21/09 04:06 the Category.* stuff there seems a little neglected compared to the rest of the std lib 21/09 04:07 it'd be nice to actually model categories 21/09 04:07 Indexed state is the same way, really. 21/09 04:07 They only work for a specified family of types. 21/09 04:08 I'm not really convinced faithfully modeling cateogry theory is a good way to get usable stuff for coding. 21/09 04:12 yeah, I wouldn't expect it to be, but it'd be nice to have a set of categorical constructs that are faithful, and then the usual ones we're used to in haskell for practical coding, and a mapping between them where possible 21/09 04:13 It'd be interesting in its own right, yeah. :) 21/09 04:13 The problem with doing category theory is there's a lot of meta-ness to it. 21/09 04:13 like, not having to do all the crazy jumping through hoops that category-extras is full of would be pretty awesome 21/09 04:14 Which means you need universe polymorphism or Set : Set to avoid writing tons of duplicate code. 21/09 04:14 yeah 21/09 04:14 which appears to be coming soon, right? 21/09 04:14 Apparently. Although I'm not totally thrilled about the explicitness of it in the notes. 21/09 04:15 oh, the plan for it has been announced? 21/09 04:17 There are some notes from a discussion at AIMX... 21/09 04:18 http://wiki.portal.chalmers.se/agda/Main.AIMX 21/09 04:19 All the way at the bottom. 21/09 04:19 oh, so Set is indexed by Nat? 21/09 04:20 Yeah. That seems weird, too. 21/09 04:20 But I'm no expert. 21/09 04:20 so I guess that makes Nat some kind of primitive in the language then? 21/09 04:21 "In an Agda review meeting back in 2007 it was decided that the hierarchy of sets should be cumulative (which would mean that Set_i had type Set_(i + k + 1) for any k ∈ ℕ)" 21/09 04:23 why would that make more sense than just having them behave incrementally? 21/09 04:23 Well, I don't know about it being useful for Set_i specifically. 21/09 04:25 It's useful when A : Set_i means that, in addition, A : Set_(i + k). 21/09 04:26 I think, at least. 21/09 04:26 That lets you cut down on universe parameters. 21/09 04:27 Rather than "Foo : forall {m n} -> Set m -> Set n -> Set (max m n)" you can do "Foo : forall {n} -> Set n -> Set n -> Set n" because whichever is less can automatically be lifted. 21/09 04:28 ah I see 21/09 04:28 doesn't the 21/09 04:30 ⇑_ : ∀ {n}{A : Set n} → A → ↑ A 21/09 04:30 mean that we'd sometimes need multiple arrows for that? 21/09 04:30 seems like the ⇑ arrow could automatically lift it as many times as needed 21/09 04:30 it wouldn't be quite as implicit as what you just said (I don't think) 21/09 04:31 but might make it more pleasant 21/09 04:31 Well, if it's directly in the language, those are the only primitives you need to implement the arbitrary lifting versions. 21/09 04:32 true 21/09 04:33 Which might be the thought on why they have those explicit postulates: that you can define explicit universe manipulations in the language. 21/09 04:34 But I don't know if you ever want to do that if it's mostly handled automatically, like in Coq. 21/09 04:34 So, auto... 21/09 04:36 If you're trying to prove m == n -> 1 + m == 1 + n 21/09 04:36 And you do "lemma refl = ?" and choose auto, it will figure out that "refl" should go in for the ?. 21/09 04:37 oh 21/09 04:37 So my guess is that it fills in obvious solutions for types without eta laws. 21/09 04:38 Where you can't just do _. 21/09 04:38 I guess that could be helpful 21/09 04:38 Auto is pretty limited. 21/09 04:52 If I have 'foo a = ... ? ...' and 'a' is the right type to fill the hole, it doesn't use it. 21/09 04:52 ah :/ 21/09 05:05 do people do any time/space complexity of algorithms proofs using agda or coq? 21/09 05:05 I guess mostly coq since agda's quite young 21/09 05:05 I wouldn't be surprised if someone's tried it in Coq. 21/09 05:06 anders^^: you around? 21/09 05:12 probably not awake if he's in sweden, I guess :) 21/09 05:12 I assume the CReal representation of reals isn't really suitable for reasoning about 21/09 07:38 I don't really know. 21/09 07:44 It probably depends on what sort of reasoning you want to do. 21/09 07:44 * copumpkin is tempted to ask roconnor for his initial haskell implementation of reals, that he then translated into coq 21/09 07:46 I think they're a bit more simplified than the definition of the reals for constructive analysis. 21/09 07:46 But not that much. 21/09 07:46 in roconnor's paper, he said that he implemented them in haskell first 21/09 07:47 which might be a relatively painless translation into agda 21/09 07:47 at least for the basic implementation, not sure about properties of the reals 21/09 07:47 Do you have Integers to work with yet? 21/09 07:49 I guess we do. 21/09 07:49 yeah 21/09 07:50 and rationals 21/09 07:50 Oh, and it's positive or negative natural. :) 21/09 07:50 CReal doesn't use rationals. 21/09 07:50 It uses Natural -> Integer. 21/09 07:50 yeah 21/09 07:50 just saying that we have rationals too if necessary for whatever representation :) 21/09 07:50 Where f n / 2^n approximates the real to within 1/2^n, or something along those lines. 21/09 07:51 yeah 21/09 07:53 Full generality uses an additional function to determine the radius of convergence, I think. 21/09 07:54 Rather than just setting it at 1/b^n. 21/09 07:54 I see 21/09 07:54 I guess Integers being Naturals underneath isn't that bad because Naturals are Integers underneath. 21/09 07:59 I found roconnor's implementation, don't fully understand his representation yet 21/09 08:00 And peano numbers are so much more luxurious than binary digits for proving. 21/09 08:00 yeah 21/09 08:01 there is also a binary natural implementation in the std lib 21/09 08:01 not sure how pleasant it is to work with though 21/09 08:01 his basic real number type appears to be Rational -> Rational 21/09 08:02 Huh. I wouldn't have guessed that. 21/09 08:02 I guess that might be "given a radius of convergence, produce an appropriate approximation." 21/09 08:03 yeah, I think that's it 21/09 08:03 it seems to have various topological-sounding words that I don't understand in it :) 21/09 08:04 other than that, it seems relatively simple 21/09 08:04 Heh, lots of the proofs in the binary  numbers module convert to peano numbers and then use the proofs on those. 21/09 08:07 I don't blame them :) I dread to think of proving stuff directly on the binary representation 21/09 08:08 Yeah. 21/09 08:08 Division by 2 is easy, though. 21/09 08:08 and multiplication by any power of two 21/09 08:12 Multiplication by anything shouldn't be that bad. Just more adding. 21/09 08:13 yeah 21/09 08:13 anders^^: I was wondering why sum in Data.Vec was restricted to Nat 21/09 19:34 copumpkin: maybe youre confusing me with someone else? 21/09 19:41 oh, maybe 21/09 19:41 at least i dont know the answer 21/09 19:41 I thought you wrote the agda standard library :) 21/09 19:41 copumpkin: hehe no 21/09 19:41 oh! 21/09 19:41 I'm just reading a bit of agda in a course at chalmers 21/09 19:42 oh, I assumed that you were Nils Anders Danielsson from the mailing list :) 21/09 19:44 :) 21/09 19:45 -!- Saizan_ is now known as Saizan 21/09 19:59 copumpkin: I think the current rational module might be a little sparse for doing roconnor's reals. 21/09 21:54 what's missing? I'd be more than happy to work on expanding it 21/09 21:55 All arithmetic operations. A constructor that generates the proofs rather than requiring them... 21/09 21:55 And proofs of stuff. 21/09 21:56 I don't know what all you'll need as far as proofs about rationals go. 21/09 21:58 q/2 + q/2 = q is one that looked like it'd be used a lot. 21/09 21:58 I just read the paper, though. I didn't look at the implementation. 21/09 22:01 Interestingly enough, his construction of the reals uses a monad, but it's a monad over the category of metric spaces, so it doesn't fit in a Haskell-like monad representation. 21/09 22:05 So a more faithful embedding of category theory would be needed to talk about it. 21/09 22:05 Or fancy stuff using restricted monads or something. 21/09 22:06 :o 21/09 22:32 sounds like lots of fun to be had! 21/09 22:33 if nothing else it'll help me learn :) 21/09 22:33 I can definitely make the rational module suck a little less 21/09 22:33 Yeah. That shouldn't be too hard. 21/09 22:34 now if only I didn't have "real" work, dammit 21/09 22:35 Oh, by the way, I think the purpose of stuff like "True " is so that you can write stuff like "bar " and have it work without proof. 21/09 22:35 However, it's a lot more of a pain when you want to want to work with inductively defined functions that work on the predicate that's being decided. 21/09 22:37 hmm, you mean like in the rational constructor? 21/09 22:37 Because there are additional hoops to jump through to get from "True (P (Con foo))" to "True (P foo)" even if you know that P (Con foo) implies P foo and such. 21/09 22:38 copumpkin: Yeah, I mean you can write '3 5' and it'll just work. 21/09 22:38 Because it can fully compute the proofs for those. 21/09 22:39 ah 21/09 22:39 Wow, loading up Data.Rational for the first time takes a while... 21/09 22:44 yeah, it needs to compile dependencies I assume 21/09 22:45 even compiling the single Algebra.agda module takes a while 21/09 22:46 and lots of RAM 21/09 22:46 2 minutes 30 seconds and 25% ram so far. 21/09 22:46 I've had the background ghci process take up about 300 megs when I've been working on the std lib 21/09 22:46 Proofs tend to take up a lot of time and space, too. And rational probably loads a lot of those with the gcd and coprimality stuff. 21/09 22:47 yeah 21/09 22:47 I'm really looking forward to writing more algebra for Algebra.agda 21/09 22:49 almost feels like the module should be split up though, as it's getting quite large 21/09 22:49 Yeah. 21/09 22:49 http://snapplr.com/vwq7 it's an owl! 21/09 22:55 :D 21/09 23:00 :) 21/09 23:01 http://blog.sigfpe.com/2008/01/type-that-should-not-be.html looks like it could be implemented in agda? 21/09 23:17 I guess it would just get colored pink 21/09 23:20 Which part? 21/09 23:21 You can do Tree but not U. 21/09 23:22 you can't even define U? 21/09 23:22 Nope. 21/09 23:22 U is a negative type. 21/09 23:22 U allows you to construct non-terminating terms that the termination checked wouldn't catch. 21/09 23:24 ah 21/09 23:25 e.g. data U = U (U -> U) is an embedding of the untyped lambda calculus, which let you define fix etc.. 21/09 23:27 copumpkin: That is, I don't think you could come up with a checker that would correctly identify only the sort stuff in those blog posts. There's nothing directly self-referrential abou them. 21/09 23:33 But it's easy to rule out the types that allow them to be well-typed in the first place. 21/09 23:34 how do they rule it out? you can't refer to yourself to the left of a function arrow? 21/09 23:36 Right. 21/09 23:36 You only allow strictly positive types. 21/09 23:36 Of course, that also rules out K r = (K r -> r) -> r, which I don't think admits the same kind of problems. 21/09 23:37 where does this positive and negative terminology come from for types? 21/09 23:37 I don't know where it comes from originally, but in 'a -> b' b is in the positive position, and a is in the negative position. 21/09 23:38 And in '(a -> b) -> c' c is strictly positive, b is negative, and a is positive, but not strictly positive. 21/09 23:39 a is positive because it's twice negative? 21/09 23:39 So, strictly positive types are only allowed to reference themselves in ways that are strictly positive. 21/09 23:39 Right. 21/09 23:39 I've not seen a language that disallows negative types but doesn't disallow non-strictly positive types. 21/09 23:40 is there a paper on how the termination checker and type inference are implemented in agda? 21/09 23:41 Those might not have obvious induction principles, or something, so maybe it's simpler to rule those out, too. 21/09 23:42 For the types, I think there's a paper called "Type Checking in the Presence of Metavariables" or something close. 21/09 23:43 Ulf's thesis on Agda might talk about it, too. 21/09 23:43 The termination checker probably has papers, too, but I don't know them. It's been rewritten once or more, too, and it slated to be rewritten again. :) 21/09 23:44 * dolio should get going to dinner. 21/09 23:44 heh 21/09 23:44 enjoy :) 21/09 23:46 --- Day changed Tue Sep 22 2009 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9687#a9687 22/09 01:37 that constructor can derive the proof from the other argument? 22/09 01:40 It produces a fraction in lowest terms. 22/09 01:41 The proof required by the rational representation comes from the gcd algorithm. 22/09 01:41 It's kind of a pain to get in the right form, though, as you can see. 22/09 01:42 'proof' really threw me, too. If i don't explicitly state either P or Q for truthFromWitness, I get a type error. 22/09 01:44 i'm not sure how those | work, unless it's just an operator i don't know 22/09 01:44 It's absolute value. 22/09 01:44 That tripped me up, too, since it's not actually |, it's a unicode character that looks almost exactly like |. 22/09 01:45 ah. 22/09 01:45 so Coprime ∣ sgn ◃ num' ∣ (suc den') is parsed as Coprime (∣ sgn ◃ num' ∣) (suc den') ? 22/09 01:46 Yes. 22/09 01:48 the type error is quite weird too 22/09 01:56 Yeah. Some implicit value isn't getting specified, but I don't know what it is, or what specifies it when I put in either P or Q. 22/09 01:59 copumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9687#a9687 22/09 02:25 There's a head's start for you. 22/09 02:25 yay, thank you :) 22/09 02:26 interesting module name :) 22/09 02:26 Thanks. 22/09 02:26 I think build should allow you to write most of the arithmetic operations. 22/09 02:28 great! 22/09 02:34 is that an anonymous record you have there? 22/09 03:00 In build? That's how you construct records. 22/09 03:09 oh 22/09 03:10 aha, I see 22/09 03:10 * copumpkin votes to kill the ◃ character in agda :P it's ugly 22/09 04:36 It's not fun to type, either. 22/09 04:42 How to run typechecker without compiler? I need to time it. 22/09 16:30 -!- jfredett is now known as jfredett-away 22/09 18:36 hi, i been reading the logs :-). copumpkin: here is some complexity analysis in agda: http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.html    dolio: here is some info on the new auto feature: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto   also have you concidered to collect the stuff you do in agda somewhere rather than just scattering it over hpaste :-)? 22/09 21:52 I have it all on my hard drive. :) 22/09 21:52 stevan: once I get something I'm reasonably satisfied with, I'd love to submit patches to the stdlib containing the matrix module I added, and several additional records for algebraic structures that aren't already there (as well as additional rational stuff) 22/09 21:53 Ah, I was supposed to give it hints. 22/09 21:55 stevan: http://code.haskell.org/~dolio/ <- there we go. I'll start putting my random experiments there, if you want to look at them. :) 22/09 22:20 ooh, nice 22/09 22:23 awesome :-) 22/09 22:23 stevan: have you looked at the homework yet? should be a breeze for you, right? 22/09 22:25 utf8 seems messed up tho? http://code.haskell.org/~dolio/agda-share/Conat.agda   agda --html output would be nicer and solve the problem i guess 22/09 22:25 stevan: yeah, I had to ask my browser to treat it as utf8 22/09 22:25 Well, I use konqueror, so that shows up in a text editor part and looks fine. 22/09 22:26 I guess code.haskell.org doesn't host its text files as if they're UTF8. 22/09 22:27 Or... That works in firefox here, too. 22/09 22:28 Tobsan: hi :-), yeah i'm done... i had some problems with the first one... i expected the exercises to be harder... the ones we got in the first homework were harder for example... 22/09 22:31 you two are taking a course on agda? 22/09 22:31 stevan: yes, the first ones were...hard :P. It took me 90 minutes to get the Standard Libraries in today heh 22/09 22:31 not really; http://www.cs.chalmers.se/Cs/Education/Courses/types/ 22/09 22:31 :O 22/09 22:33 * copumpkin wants one of those 22/09 22:33 you can follow ours :-) 22/09 22:33 dolio: if it isn't too much work, html output would be nicer; syntax highlightning + clickable definitions... 22/09 22:34 and utf8 wouldn't be a problem :-) 22/09 22:35 stevan: What do I even use to make html? I seem to have missed whatever part of the install gives me an 'agda' executable to pass the --html flag to. 22/09 22:46 cabal install agda-executable normally, but I wasn't able to find it when I grabbed the darcs version 22/09 22:47 not sure where it comes from 22/09 22:47 Huh. 22/09 22:47 if you got the darcs version, cd into src/main and cabal install there aswell 22/09 22:47 Ah, okay. 22/09 22:48 Okay, done. 22/09 22:54 nice :-) 22/09 22:54 ooh, and the .agda family in that folder grew too 22/09 22:56 if I wanted to express a "no zero divisors" property in agda, I'd write forall n. not (zerodivisor n), right? would not (exists n. zerodivisor n) work? 22/09 23:02 plenty of stuff missing still :-p, the soundness proof for propositional logic, the mod operator, the rational stuff :-) 22/09 23:03 oh, I mean assuming that zerodivisor existed 22/09 23:04 and mod is already there 22/09 23:04 where zerodivisor n might be forall m. n * m /= 0 22/09 23:14 hmm, if you want to use the n later in the function for something i think you have to go with forall? 22/09 23:14 I'd need more restrictions on the values of n and m I guess 22/09 23:17 All right. Added propositional logic with soundness theorem, and provable sorting of vectors. 22/09 23:34 Dinner time. 22/09 23:34 :o 22/09 23:35 cool, i just found an other proof for prop logic soundness: http://wiki.portal.chalmers.se/agda/uploads/Libraries.Sequent/Sound.agda 22/09 23:37 hmm, if I know that suc n is a Fin (suc m), is there an easy way to convince it that n is a Fin m ? 22/09 23:54 the various injection functions in Data.Fin don't seem to cover that 22/09 23:54 --- Day changed Wed Sep 23 2009 hmm, I think I may have it 23/09 00:16 Isn't that true by definition of the suc constructor for Fin? 23/09 00:28 yep, I was just being dumb 23/09 00:40 got it working :) 23/09 00:40 What if you do pf : invertible {n} x? 23/09 01:34 perfect :) 23/09 01:34 that makes sense 23/09 01:34 I'm not sure why the n vs. {n} would make a difference with that, though. 23/09 01:34 maybe it bound the name invertible without it? 23/09 01:35 (ignoring the existing function) 23/09 01:35 ah, you should have put an -> before it, maybe 23/09 01:35 You can't normally have strings of "(foo) (bar) (baz)", only "(f : foo) (b : bar) (bz : baz)". 23/09 01:36 So I don't know why "(f : foo) {bar}" was working. 23/09 01:36 But it was, without the nested {}s, apparently. 23/09 01:36 {bar} could have worked because of the forall 23/09 01:37 i'd be surprised about {bar x} though 23/09 01:37 a {bar} meaning {bar : _}, i mean 23/09 01:37 Yes. 23/09 01:38 Oh, maybe that was it. 23/09 01:39 It was taking {invertible n x} to be {invertible n x : _}. 23/09 01:39 But {invertible {n} x : _} it realizes is an error. 23/09 01:39 i didn't realize you could have higher order patterns like that 23/09 01:40 Maybe it's a bug? 23/09 01:42 foo : \all {a : Set} {b c} -> a -> a ; foo x = x 23/09 01:42 works 23/09 01:42 aaah 23/09 01:42 so n and x are new bindings there 23/09 01:42 But foo : \all {a : Set} (b c) -> a -> a is a prse error. 23/09 01:42 but \all {a : Set} b c -> a -> a works? 23/09 01:43 Yes. invertible, n and x are all bindings. 23/09 01:44 Yes that works. 23/09 01:44 I guess it's not a bug. Just weirdness. 23/09 01:44 Or, I wasn't expecting the \all to extend that far or something. 23/09 01:45 i think shadowing a binding in the same signature shouldn't be allowed 23/09 01:45 Yeah, that seems like it'd be something you'd want caught. 23/09 01:46 I'll file a bug, I guess. 23/09 01:47 (b c) vs. {b c} is a bit surprising too 23/09 01:48 though there's no need to use "(b c)" instead of "b c" 23/09 01:49 but (b c : A) would work, right? 23/09 01:49 Yes. 23/09 01:52 Hmm... 23/09 01:56 But what about \all {x} -> (\all x -> x -> x) -> x -> x? 23/09 01:56 That has multiple scopes. Should shadowing still be disallowed? 23/09 01:57 mh, i'd say no 23/09 01:57 well, it's not as confusing as when one scope spans over the rest of the larger one 23/09 01:59 but i wouldn't really cry if that case was disallowed too 23/09 01:59 Issue submitted. 23/09 02:14 damn, I need sortedness 23/09 02:35 I think 23/09 02:36 mmm writing a permutations module could be fun 23/09 02:40 Proving that two lists/vectors are permutations of one another is really hard work. 23/09 02:41 yeah, I'd imagine 23/09 02:42 I guess your sorting module covers some of that 23/09 02:42 I've tried a lot of representations, and the only one I ever succeeded with just took transitivity as an axiom. 23/09 02:42 hrm 23/09 02:44 But I haven't looked at other proofs people have done much. 23/09 02:44 Doubtless you can find some Coq that has a successful proof. 23/09 02:45 Or maybe other people just take the same cop-out. 23/09 02:45 :) 23/09 02:45 write a function that computes the intensional equality for two terms of any type? 23/09 02:46 *can you 23/09 02:46 No. 23/09 02:46 ok, it makes sense :) 23/09 02:46 You can probably do it for any particular type that's built out of sums and products of various sorts. 23/09 02:49 But anything that has a function in it will be a dead end. 23/09 02:49 ah, yeah, i didn't even took the possibility of functions into account 23/09 02:50 * Saizan__ should get some sleep 23/09 02:51 Codata's a problem, too, because any inspection you can do of it won't tell you anything about intensional equality. 23/09 02:51 so when you code permutations you use a Setoid as the element of the lists/vectors, right? 23/09 02:53 Well, I suppose it depends what you want to do with permutations. 23/09 02:54 You can prove that sorting is a permutation with respect to intenstional equality, for instance. 23/09 02:54 Because you can construct proofs of where each particular element of the original ends up in the result, which doesn't involve deciding anything. 23/09 02:55 But (T, intenstional-equality) is a setoid, just not necessarily a decidable setoid. 23/09 02:56 Man, I keep spelling intensional wrongly. 23/09 02:58 heh 23/09 02:58 okay, today is not the day to be writing matrix inversion in agda 23/09 03:18 * copumpkin is trying to come up with good notation for accessing entire rows and columns of matrices 23/09 03:29 are predicates typically uppercase? 23/09 03:45 should I write Invertible? 23/09 03:45 The standard library uses uppercase for Set-valued stuff as a convention. 23/09 03:50 So if : Set, then should be uppercased. 23/09 03:51 yeah 23/09 03:51 okay 23/09 03:51 And if : B would lead to be uppercased, then : A -> B should be uppercased. 23/09 03:52 I see 23/09 03:54 there doesn't seem to be a unary decidable thing 23/09 03:55 only a nullary Dec and a binary Decidable 23/09 03:55 Yeah. 23/09 03:57 I guess decidable relations are more commonly wanted than decidable unary predicates. 23/09 03:59 * copumpkin finds himself tempted to write all sorts of useless helper functions for matrices 23/09 04:58 if I wanted to add a submodule of Data.Vec for typicaly "mathy" vector operations (dot product, vector addition, norm, and so on), what structure should I parametrize it over? a field seems obvious, but it seems like a ring should be sufficient 23/09 05:39 I guess I could just introduce vector space and/or module for it 23/09 05:41 Ring, probably. 23/09 05:41 Rings are good enough for modules. 23/09 05:41 yeah 23/09 05:42 if I call the record Module, is that confusing? should I call it R-Module? (pretty much everything I know about algebra I got from wikipedia, so I don't entirely trust myself :P) 23/09 05:42 It's been a while since I studied modules. 23/09 05:43 or _-Module :O 23/09 05:43 okay, anyway I can rename stuff later if it bothers people more knowledgeable than myself 23/09 05:44 I mean, vector spaces/modules in general don't depend on anything like the vector type/matrices. 23/09 05:45 yeah 23/09 05:45 I just wanted to write an "instance" 23/09 05:45 for the concrete vector type 23/09 05:45 As it happens, R-module is an actual term. 23/09 05:49 At least as far as An Introduction to Rings and Modules With K-theory in View is concerned. 23/09 05:49 sounds good 23/09 05:50 In fact, there are both right and left R-modules. 23/09 05:51 And then R-S-bimodules. 23/09 05:52 I had left and right 23/09 05:52 what's S-? 23/09 05:52 Different ring. 23/09 05:52 oh 23/09 05:52 any ideas on how to represent the fact that a vector space has a field, and two "carriers" for scalars and vectors, both over that field? 23/09 05:53 I was thinking of a function 23/09 05:53 something like http://snapplr.com/fzt4 23/09 05:54 oh, fieldCarrier should probably be : Field 23/09 05:54 Isn't a vector space a group and a field? 23/09 05:55 Also, fieldCarrier -> Set is one Set for each element of fieldCarrier. 23/09 05:56 ah, hmm 23/09 05:56 I was just trying to tie them together as depending on the same underlying field 23/09 05:57 I can do something like record VectorSpace {f : Field} : Set₁ where 23/09 05:58 A vector space is, as I recall, a group of vectors, and a field of scalars, with various operators for interaction between them. 23/09 05:58 And where matrices come in is linear (?) transformations. 23/09 05:59 yeah 23/09 05:59 but only on the F^n kind of vectors, I guess 23/09 06:00 Well, you can tease F^n vectors out of abstract vector spaces. 23/09 06:01 Like you can tease matrices out of abstract linear transformations. 23/09 06:01 Because v : F^n can be taken to mean Sum g_i * v_i where g_i are some suitable basis elements of the group. 23/09 06:02 yeah 23/09 06:03 Assuming finite dimensionality, of course. 23/09 06:04 yeah 23/09 06:04 http://snapplr.com/xe1p this feels overcomplicated :( 23/09 06:15 and ugly with all the duplicated symbols 23/09 06:16 maybe I can do something nicer with the modules 23/09 06:16 Is that how Ring and such work? 23/09 06:17 yeah, but not nearly as packed with stuff 23/09 06:17 Hmm... 23/09 06:17 Shouldn't scalarIsField and vectorIsGroup go in the fields? 23/09 06:19 oh yeah 23/09 06:19 I don't think there's much getting around it. Vector spaces just have a lot of stuff in them. 23/09 06:19 it seems like I should be able to "open" the two constituent structures without duplicating everything 23/09 06:20 Yeah, but not without bumping the universe level or parameterizing by the structures. 23/09 06:21 ah 23/09 06:21 maybe I can just come up with something nicer than all those \^1s for the scalars 23/09 06:22 I think part of the reason why the Algebra modules are arranged the way they are is to keep everything at Set1. 23/09 06:22 probably 23/09 06:24 bah, I hate naming things 23/09 06:32 the VectorSpace record looks a lot less messy if I group the vector-specific operations, the scalar-specific ones, and then the combination one 23/09 06:32 -!- Tobsan_ is now known as Tobsan 23/09 07:27 well, I think this just about covers it: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9726#a9726 23/09 07:28 there needs to be an algebrapedia like byorgey's typeclassopedia :) 23/09 07:29 noZeroDivisors    : ∀ x y → ¬ (x ≈ 0#) → ¬ (y ≈ 0#) → ¬ ((x * y) ≈ 0#) seems reasonable, right? 23/09 07:49 Yeah. 23/09 07:53 You should definitely define an alias for not-equal, though. :) 23/09 07:54 I wanted to, but I wasn't sure where to put it, since my record introduces _~~_ as a parameter 23/09 07:55 http://snapplr.com/1dpk 23/09 07:55 I guess I don't need FunctionProperties there 23/09 07:56 maybe I should expand FunctionProperties to be more flexible 23/09 07:56 You can put it before "field" 23/09 07:57 ah cool 23/09 07:58 is there a good way of resolving circular module dependencies? 23/09 08:00 I wanted to express unique factorization with Data.Vec but it already requires algebra indirectly and forms a circular dependency 23/09 08:01 Probably not. There's something in Data.Vector that says it's only there because it depends on Data.Fin. 23/09 08:02 ah :/ 23/09 08:03 hmm 23/09 08:03 I'd just define a local copy of the vector structure, but then it'd make it even more painful to prove this than it already is 23/09 08:04 :) 23/09 08:04 I was just going to say that forall xs ys x. x !~ 0 -> x !~ 1 -> product xs ~~ product ys ~~ x -> xs ~~ ys 23/09 08:05 I guess I could use n-ary functions 23/09 08:07 oh and I guess I couldn't use Vec anyway 23/09 08:10 because it's ordered 23/09 08:10 and allows multiple elements 23/09 08:11 * copumpkin is basically walking through wikipedia's algebra pages and defining all the structures he can find... rather sad thing to be doing in the middle of the night :P 23/09 08:27 I've got algebras over rings/modules and fields now, as well as lie algebra 23/09 08:28 if I can't get reals working easily, if nothing else, I can work with polynomials :) 23/09 08:32 and have fun with fields 23/09 08:32 :) 23/09 08:33 dammit, I wish I'd taken more math, or were in a program where I could bullshit my way into taking more pure math 23/09 08:34 hey 23/09 09:11 -!- Saizan__ is now known as Saizan 23/09 13:35 anyone seen http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html ? 23/09 17:54 meh, http://snapplr.com/a4ef :( 23/09 19:12 the error is http://snapplr.com/s17k 23/09 19:14 it's odd, cause the type it claims it isn't, is exactly what the proj2 is supposed to show 23/09 19:16 :( 23/09 20:11 I can't figure out why this isn't working, in my context I have n + 0 == n, but it still complains that n != n + 0 23/09 20:12 --- Day changed Thu Sep 24 2009 I don't think that blog post really gives the whole story. 24/09 00:18 is there some way to show the types of bound variables in scope in some hole? 24/09 01:17 if you right click on the hole and ask for the context 24/09 01:18 right click? 24/09 01:18 C-c C-e works too 24/09 01:18 did that work? 24/09 01:20 yup 24/09 01:21 I seem to have a bajillion refls in scope 24/09 01:21 it's annoying 24/09 01:21 I'm not sure what to make of this free theorem stuff. 24/09 01:21 i don't get to see both the type of the hole and the context at the same time, but that's ok i guess 24/09 01:21 the types in that were amazingly long 24/09 01:21 C-c C- it says 24/09 01:22 for both goal and context 24/09 01:22 not sure how you type that :P 24/09 01:22 anyone know what's going on with http://snapplr.com/f537 ? 24/09 01:23 oh 24/09 01:24 it didn't catch the tooltip 24/09 01:24 n + 0 != n of type ℕ when checking that the pattern Core.refl has type n + 0 ≡ n 24/09 01:24 :t n+0=n ? 24/09 01:25 n+0≡n : ∀ x → (x + 0) ≡ x 24/09 01:25 Use subst 24/09 01:25 subst₁ : ∀ {a} (P : a → Set₁) → ∀ {x y} → x ≡ y → P x → P y ? 24/09 01:26 subst₂ : ∀ {A B} (P : A → B → Set) → 24/09 01:26 ∀ {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂ 24/09 01:26 subst1 is if you're predicate is into Set1. 24/09 01:27 There should be a subst for normal Set. 24/09 01:27 aha 24/09 01:27 And subst2 is for binary relations, which ruins the whole naming scheme. 24/09 01:27 x' ≡ y → P x' → P y 24/09 01:27 though i don't completely get why you don't have a similar error when defining subst, or is it just because with is not magic enough? 24/09 01:28 the official type is subst : {a : Set} → Substitutive {a} _≡_, but that isn't very clear 24/09 01:28 I think it's P -> x == y -> P x -> P y, so you'll need to provide P. 24/09 01:29 P x == P y 24/09 01:29 forall P -> ... even 24/09 01:29 hmm 24/09 01:29 No, P x == P y is cong. 24/09 01:29 hmm 24/09 01:30 ah, true 24/09 01:30 so much indirection in this code! 24/09 01:30 http://snapplr.com/p1h9 24/09 01:30 subst (\n -> ...) (n+0=n n) 24/09 01:30 I mean, code reuse :P 24/09 01:30 Yes. P Respects _~_ means x ~ y -> P x ~ P y. 24/09 01:31 f Preserves _~_ --> _~~_ means x ~ y -> f x ~~ f y. 24/09 01:31 makes sense 24/09 01:32 Congruential _~_ means all endomorphisms f preserve _~_ 24/09 01:33 Or, I guess it's not endomorphisms. 24/09 01:33 It's just that _~_ works on all Sets. 24/09 01:34 btw, what do you think about defining Permutation xs ys = length xs == length ys , Subset xs ys , Subset ys xs ? 24/09 01:36 transitivity should be easy for that 24/09 01:36 How is Subset defined? 24/09 01:38 It's not always transitivity where I run into a problem, if I recall correctly. 24/09 01:39 It's just that the one proof structure I managed to prove everything with, I took transitivity as an axiom, because that's what I couldn't prove for it (and I needed it). 24/09 01:40 Subset xs ys = All (λ x → Some (_==_ x) ys) xs 24/09 01:40 Other formulations I may have had trouble proving other useful properties (like symmetry, for instance), which I could also have assumed, but that makes me equally unhappy. 24/09 01:41 Well, that doesn't work, actually, because then [1,1,2] and [1,2,2] are considered permutations. 24/09 01:41 the anonymous variables are annoying 24/09 01:42 Anyhow, my point is that defining a Subset that captures the necessary conditions will probably be no less difficult than Permutation directly. 24/09 01:42 it accepted this http://snapplr.com/3hek 24/09 01:46 but that _ is bad 24/09 01:46 I thought (Vec carrier) would be a good thing to put for the _ 24/09 01:47 but it didn't like it :( 24/09 01:47 Saizan: In fact, I've probably tried something similar to that. 24/09 01:49 Like "step : x \in xs -> x \in ys -> remove x xs ~ remove x ys -> xs ~ ys" 24/09 01:50 I've also tried "y \in xs -> x \in ys -> xs ~ ys -> x :: xs ~ y :: ys". 24/09 01:51 almost got it! 24/09 01:57 it's all really weird though :P 24/09 01:58 merge {n} xs [] = subst (Vec carrier) { }0 [] 24/09 01:59 it says the hole has shape 0 == n + 0 24/09 02:00 but if I put n+0==0 n in that hole 24/09 02:00 it doesn't like it 24/09 02:00 I mean n+0==n 24/09 02:00 oh 24/09 02:00 that's bad 24/09 02:00 meh :) 24/09 02:02 If the hole is n = n + 0, then you probably need symmetry, since n+0=n presumably has type n + 0 = n 24/09 02:02 no, the hole is actually 0 == n + 0 24/09 02:02 Well... 24/09 02:02 oh I see 24/09 02:02 meh, nope, I can't prove that 24/09 02:02 I thought n had to be 0, but it doesn't 24/09 02:03 Something weird is going on, then, unles n = 0. 24/09 02:03 oh silly me 24/09 02:04 merge {n} xs [] = subst (Vec carrier) {!!} xs is what I really meant 24/09 02:06 the hole there is n == n + 0 24/09 02:06 then you need "sym (n+0==n n)" 24/09 02:08 omg 24/09 02:08 I didn't realize it didn't know == wasn't symmetric :) 24/09 02:09 in a sense it does know since it let you write sym 24/09 02:09 I just need to reassure it 24/09 02:10 so much overlap in my symbols :( 24/09 02:19 * copumpkin needs some of the private properties in Data.Nat.Properties :) 24/09 02:25 crap, I got me some pink 24/09 02:32 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9762#a9762 24/09 02:48 it'd be nice if it gave more of an indication of where the pink is coming from 24/09 02:49 copumpkin: I think I've seen this come up before, but I don't remember what the problem is exactly, or how to fix it. 24/09 02:54 yay, merge Data.Nat.decTotalOrder (1 ∷ 2 ∷ 5 ∷ []) (2 ∷ 3 ∷ []) works find 24/09 02:56 fine 24/09 02:56 gives me 1 ∷ 2 ∷ 2 ∷ 3 ∷ 5 ∷ [] 24/09 02:57 -!- byorgey_ is now known as byorgey 24/09 02:59 * Saizan_ realizes he has never evaluated an expression in agda 24/09 02:59 :) 24/09 03:00 If you look hard enough, you can probably find it on the mailing list. 24/09 03:00 But I'm not exactly sure what to look for. 24/09 03:00 copumpkin: I think the problem is in having the 'with' along with only being verifiably structurally recursive when two arguments are considered. 24/09 03:01 with causes a new anonymous function to be declared, so to the termination checker, it looks something like... 24/09 03:02 "merge ... = aux (x :: xs) (y :: ys) ; aux (x :: xs) (y :: ys) = ... merge xs (y :: ys) ... merge (x :: xs) ys 24/09 03:02 So it has trouble telling that you aren't adding one and then subtracting it back off forever or something. 24/09 03:03 ah, hmm 24/09 03:04 should my merge demand a proof of sortedness for its parameters? or should I just claim that the result will only be sorted if the inputs are sorted 24/09 03:10 Depends. There are, roughly speaking, two ways to do any particular proof. 24/09 03:14 Either you can write your functions 'f : (x : T) -> P x -> \Sigma T' Q' or 'f : T -> Q ; prop-f : \all x -> P x -> Q (f x)' 24/09 03:15 yeah 24/09 03:16 I think that's what I'll do here, probably 24/09 03:16 Oops, I messed up the types in the second part. Anyhow. 24/09 03:17 sometimes these holes seem less informative than they could be 24/09 03:25 I have a hole that claims it just needs Nat -> Set 24/09 03:25 but I've given it plenty of Nat -> Set functions and it barfs every time 24/09 03:25 Relation.Unary still feels rather neglected compared to Nullary or Binary 24/09 03:38 Hah! Figured it out! 24/09 04:08 figured which one out? 24/09 04:08 sorting? 24/09 04:08 http://code.haskell.org/~dolio/agda-share/html/Free.html 24/09 04:08 oh that one :) 24/09 04:08 cool 24/09 04:12 is the fact that it can't determine that merge terminates a bug, or an accepted limitation? 24/09 04:38 I'm not sure how accepted it is. 24/09 04:43 There might be a work-around. 24/09 04:44 I rather like how simple the function looks right now 24/09 04:45 I'm scared of writing anything big in case the proof gets ridiculously hard because of it :P 24/09 04:45 -!- Tobsan_ is now known as Tobsan 24/09 07:03 wow, compiling Rational.agda ate up 600 MB of RAM 24/09 18:16 dolio: I think peer may have it in for you by the way... he keeps resetting your connection 24/09 18:16 have you tried compiling Everything.agda all at once? 24/09 18:29 nope :) 24/09 18:30 have you? 24/09 18:30 yeah, i had to wait a while :) 24/09 18:30 @hoogle getLine 24/09 18:31 @type getLine 24/09 18:31 :( 24/09 18:31 * copumpkin can't get dolio's rat code to compile :( 24/09 18:48 oh. sorry, wrong channel for lambdabotting 24/09 18:50 gotta love agda, http://snapplr.com/6c3h 24/09 18:52 :D 24/09 18:53 build sgn num          den with gcd′ num den build sgn .(num' ℕ* d) .0 {} | d , gcd-* {.d} num' 0 cop 24/09 19:37 agda's ghci is up to over a gig of RAM :P 24/09 19:51 * copumpkin can't figure out what's wrong with that :( 24/09 20:16 * copumpkin curses 24/09 20:23 http://article.gmane.org/gmane.comp.lang.agda/1038 awesome!!!!! 24/09 20:25 esp. Peter Hancock 24/09 20:25 :) 24/09 20:26 ? 24/09 20:26 it does look cool 24/09 20:27 stevan that them ? 24/09 20:28 Saizan did you find the OTT code? 24/09 20:28 pretty sure it's on coq-club 24/09 20:28 dolio "It is clearly quite wasteful to have both Fin n and m < n when they obviously have the same structure. :)" 24/09 20:30 if you can make an isomorphism we can share proofs :P 24/09 20:30 I think that will be important in big developments 24/09 20:30 is there a magic order of hiding, using, and renaming? 24/09 20:32 I can't get any of them to work 24/09 20:32 yeah that free theorem in agda stuff doesn't make any sense 24/09 20:32 yay, got dolio's build working :) 24/09 20:38 dumbest reason ever it wasn't working 24/09 20:38 and agda's error message wasn't very helpful 24/09 20:38 what build? 24/09 20:38 a builder function for Data.Rational 24/09 20:40 oh 24/09 20:40 the existing one wants a proof that the numerator and denominator are coprime 24/09 20:41 how is rational defined? 24/09 20:41 whereas his function reduces it 24/09 20:41 guck 24/09 20:41 it's an integer over a natural 24/09 20:41 you know euclid algorithm? 24/09 20:41 for computing GCD 24/09 20:41 he's using it 24/09 20:41 well, there's a GCD algorithm already in the std lib 24/09 20:41 and he's using that 24/09 20:41 but you know the algo inside out yeah? 24/09 20:42 pretty much 24/09 20:42 why? 24/09 20:42 so lets say  GCD(n,d) = 1 24/09 20:42 and invert the algorithm, 24/09 20:42 you get GCD(n+d,d) = GCD(n,n+d) 24/09 20:43 there's always two things you can do: and every pair of numbers with GCD 1 is reached this way (because the algorithm is total) 24/09 20:44 interesting 24/09 20:44 so you can define rational numbers as:   data Q = One | N Q | D Q 24/09 20:44 (positive) 24/09 20:45 that sounds like it would be more elegant than the current representation 24/09 20:45 try to prove that sqrt(2) isn't in  Q 24/09 20:45 record ℚ : Set where   field     numerator     : ℤ     denominator-1 : ℕ     isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1)) 24/09 20:45 Yuck :P 24/09 20:47 why the hell is that called 'True" 24/09 20:47 one thing I reall hate in math (not just type theory) is when people say  "X is true"  rather than just saying  "X" 24/09 20:48 it converts a Dec back to a type statement of truth 24/09 20:48 if that makes sense 24/09 20:48 data Dec (P : Set) : Set where 24/09 20:48 yes : ( p :   P) → Dec P 24/09 20:48 no  : (¬p : ¬ P) → Dec P 24/09 20:48 when you want to go from 2 -> Prop though use spandau ballet 24/09 20:48 I think True is a terrible name but doesn't really matter I guess 24/09 20:49 maybe :) 24/09 20:51 bring it up with the author of the library! 24/09 20:51 nah I don't care about Agda 24/09 20:51 aw 24/09 20:52 what do you care about? 24/09 20:52 It's way too ad-hoc the only worthwhile thing are what people think when they use Agda 24/09 20:52 on the Wish-List nobody mentions De-Bruijn Criteria 24/09 20:52 maybe we should ditch decidible type checking too? 24/09 20:52 -!- mode/#agda [+o vixey] by ChanServ 24/09 20:58 -!- mode/#agda [-o vixey] by vixey 24/09 20:58 ooh 24/09 21:00 -!- byorgey_ is now known as byorgey 24/09 21:00 mahogny it's a quite lively and good channel somehow ! 24/09 21:05 even though it's about some esoteric research lang :P 24/09 21:05 will stay :) 24/09 21:05 hm. seem to be some chalmers people here <3 24/09 21:06 -!- Saizan_ is now known as Saizan 24/09 23:15 --- Day changed Fri Sep 25 2009 -!- jfredett_ is now known as jfredett 25/09 00:42 copumpkin: build wasn't working as it was? 25/09 01:31 dolio: it was me being stupid as usual :) the error wasn't very clear, but I thought I had imported Data.Product and hadn't, so it couldn't parse the comma 25/09 01:56 Ah. 25/09 01:59 I started adding some arithmetic, anyway 25/09 02:02 * copumpkin is trying to prove no zero divisors for integers 25/09 02:12 as I'm pretty sure I need it for rational multiplication 25/09 02:12 actually, just naturals 25/09 02:12 * copumpkin used his first _|_-elim 25/09 02:27 !! 25/09 02:28 damn, so close! 25/09 02:51 hmm, I have something that is obviously false, but I'm not sure how I can produce a bottom to satisfy it 25/09 02:56 yet it isn't obvious enough that an absurd pattern is enough 25/09 02:56 There's only two ways to "produce a bottom." 25/09 03:01 \x -> x where x is a bottom. 25/09 03:01 And \() 25/09 03:01 I suppose it could be '\x -> f x' where f produces a bottom from whatever x is. 25/09 03:02 yay, the lambda () worked :) 25/09 03:02 http://snapplr.com/h6d3 yay 25/09 03:04 it's probably more complicated than it needs to be 25/09 03:04 Looks about right. 25/09 03:05 You could put the x/=0 before the y so you don't need to use {y = y}. 25/09 03:05 oh, neat 25/09 03:06 you making the proofs implicit is silly? 25/09 03:07 I guess it can infer them some of the time 25/09 03:07 hmm, so I have a blah == 0 -> _|_, and need a False (blah == 0) 25/09 03:19 I can't see how to go in that direction 25/09 03:19 Yeah. You might need to write another one of thise "witnessFromTruth" type things I wrote. 25/09 03:19 oh 25/09 03:19 there's already one in Relation.Nullary.Decidable 25/09 03:20 That goes from True (Dec (Foo)) to Foo. 25/09 03:20 oh yeah :) 25/09 03:20 You need Not Foo -> False (Dec Foo) 25/09 03:21 I needed Foo -> True (Dec Foo) 25/09 03:21 That's why those True/False things suck. :) 25/09 03:21 you'd think there'd be one in the library 25/09 03:21 so the Dec stuff is just so you can get some sort of value-level indication of truthiness, right? 25/09 03:28 Dec is for deciding predicates. 25/09 03:28 I mean, strictly, it's just a sum type that hold either a proof of a proposition or a proof of its negation. 25/09 03:29 But that's the sort of thing you get back from a decision procedure for a predicate. 25/09 03:29 yeah 25/09 03:30 i was wondering, when you write code splitting properties from the actual functions, the proof of the property often has to follow the definition of the function to be accepted, isn't this a potentially big problem for modularity? 25/09 03:36 Yeah, dependent types don't really buy you modularity. 25/09 03:40 i guess you can't prove much about code without looking at it 25/09 03:43 http://www.cs.cmu.edu/~rwh/courses/modules/index.htm 25/09 03:44 The lecture on dependent typing goes over how dependent typing doesn't really model abstraction well. 25/09 03:45 that looks like a great course 25/09 03:49 Yeah. 25/09 03:49 they have a real world haskell user! 25/09 03:56 it does sound fun 25/09 03:58 if only I'd know this stuff was so cool when I was applying to grad school :P 25/09 03:58 *known 25/09 03:58 not that I'd have gotten into CMU anyway 25/09 03:59 onoes, my proof be yellow 25/09 04:24 http://snapplr.com/zweg 25/09 04:24 Yeah, in build, didn't I have to apply it to the implicit {True ...} thing? 25/09 04:26 It actually caused an error in my case when I didn't specify one of the implicit arguments. 25/09 04:28 Kind of an undesirable situation. 25/09 04:30 I'm kind of skeptical of the merits of using 'True (coprime? | n | d)' in the first place. 25/09 04:34 And 'False (d ==? 0)' I guess. 25/09 04:35 yeah 25/09 04:35 mehh 25/09 05:17 oh wow, it didn't need the no zero divisors property at all 25/09 05:22 I guess for naturals, it's a pretty obvious property :) 25/09 05:24 wow, I tried multiplying two rationals 25/09 05:28 it's taking forever :P 25/09 05:28 Heh. 25/09 05:30 yay, it got the right answer! 25/09 05:30 Which two rationals? 25/09 05:30 5/4 and 6/8 25/09 05:31 both built 25/09 05:31 using your function 25/09 05:31 it gave me a numerator=15, denominator-1=15 25/09 05:31 Wow, those aren't even big. 25/09 05:33 yeah, I tried computing it again just to make sure it wasn't random 25/09 05:34 but it's taking forever again 25/09 05:34 maybe the evaluator hasn't had much attention 25/09 05:34 rather disconcerting that it takes that long to compute, but I guess all I care about is the proof! :D 25/09 05:56 can I pattern match on records? 25/09 05:57 No. 25/09 05:57 is there a way to search github for all agda code? 25/09 12:35 vixey: FYI, there's a note in passing in the AIMX notes about a desire to define a core theory for Agda. 25/09 12:43 cool 25/09 12:44 De-Bruijn criterion presumably being one of the reasons. 25/09 12:45 I thought that's what Agda-light was about 25/09 12:46 how do i get to interactive mode in agda? 25/09 14:16 like if i want to evaluate an expression 25/09 14:16 Tobsan: C-c C-n in emacs 25/09 14:32 thanks kosmikus! 25/09 14:35 Man, I'm not sure keeping Agda-generated html in darcs is a good idea. 25/09 15:04 keeping generated files under version control is almost never a good idea 25/09 15:22 Yeah. 25/09 15:23 code.haskell.org doesn't have Agda on it, though. :) 25/09 15:24 has anyone tried compiling agda on a gentoo amd64 system? 25/09 15:31 I use an ubuntu amd64 system. Is there a reason that'd be seriously different? 25/09 15:33 Oh, I suppose I haven't 'compiled' anything, either. I just use the emacs mode. 25/09 15:34 my build fails when linking the type-checker 25/09 15:41 or "agdachecker" 25/09 15:41 I might try doing this with cabal 25/09 15:44 alright, so if you're on a amd64 system on gentoo, use cabal instead of portage to install agda 25/09 15:49 dolio: maybe if you include a .htaccess in your repo with a .agda utf-8 content type that would save you from having to generate .html files? 25/09 17:05 at least it would serve up the files as they were intended to be seen 25/09 17:05 yay universe polymorphism! 25/09 17:17 hi copumpkin 25/09 18:43 :) 25/09 18:43 anyone figured out this paramtricity stuff? 25/09 18:47 http://www.nabble.com/An-encoding-of-parametricity-in-Agda-td25577620.html 25/09 18:47 I still don't get t 25/09 18:47 vixey: dolio said he'd figured it out 25/09 18:48 did anyone see the article posted to the dependent types reddit on representations of integers? 25/09 20:01 or I guess just a mailing list post :) 25/09 20:02 no 25/09 20:02 I read it on agda list 25/09 20:02 ah 25/09 20:02 not sure why it's posted to reddit 25/09 20:02 because it wasn't very interesting :/ 25/09 20:02 unless I missed something? 25/09 20:02 ΠΣ: A Core Language for Dependently Typed Programming (pdf) 25/09 20:03 that's not ancient? 25/09 20:03 what's going on this reddit lol 25/09 20:03 I dunno, interesting to you, a seasoned programming language / type theory person, and me, a complete newbie, might be quite different :) 25/09 20:03 gotta run 25/09 20:04 --- Day changed Sat Sep 26 2009 -!- opdolio is now known as dolio 26/09 00:13 vixey: http://code.haskell.org/~dolio/agda-share/html/Free.html 26/09 00:17 ah 26/09 00:18 yeah I don't really knwo what everyone is doing with this stuff 26/09 00:18 nobody defined a term syntax with evaluation function 26/09 00:18 I sent an e-mail to coq-club/haskell-cafe with more explanation in it, too. 26/09 00:18 I did read that 26/09 00:18 I just don't know why people are trying to show parametricity for the WHOLE language (which is obviosly impossible) rather than picking a subset (like Simple Typed Lambda Calculus) 26/09 00:19 Well, I don't think parametricity is very useful for simple types. 26/09 00:20 rather than picking a subset _which it is actually provable for_ 26/09 00:20 oh sorry yes your completely right I should say some polymorphic calc 26/09 00:21 System F is where it gets useful, because there are quantifiers over types. 26/09 00:21 yeah without the forall you get nothing 26/09 00:21 But, you can't prove that quantifying over Set is parametric in Agda from within Agda. 26/09 00:22 Even though there's no type-case or anything. 26/09 00:23 I'm not sure what you mean ?  if you define a language you should be able to prove polymorpism for terms in that language 26/09 00:23 I'd do this in Coq but (1) it's hard (2) no eta 26/09 00:23 without canonical proofs of eta things I can't get reduction so the whole thing wont go through 26/09 00:24 Yeah, if you define your own language and interpreter embedded in Agda, you can probably do it. 26/09 00:24 what strikes me as bizarre is that he didn't do that :P 26/09 00:24 The proofs are so long and complicated I haven't figured out what (if anything) it's actually showing 26/09 00:25 I'm saying you can't prove that agda functions \all A -> A -> A have a parametricity result from within Agda. 26/09 00:25 Even though they are parametric. 26/09 00:25 yes I absolutely agree & that's what I meant earlier about "obviosly impossible" 26/09 00:25 * vixey now wonders just how to show that it's impossible ... 26/09 00:26 As far as I can tell his blog post is just about how to reprent the 'type relations' involved nicely. But maybe I'm actually missing something, because his mail seems to say there's more to it than that. 26/09 00:26 So, what do you think? Should I rebuild agda and rework the category theory stuff I've been doing to use the experimental, limited universe polymorphism? 26/09 02:33 Or stick with --type-in-type for now? 26/09 02:33 the new stuff sounds like it could be coo 26/09 02:34 l 26/09 02:34 is there a repo? 26/09 02:35 yep 26/09 02:35 http://code.haskell.org/~dolio/agda-share/categorica/ 26/09 02:35 thanks 26/09 02:35 http://code.haskell.org/Agda 26/09 02:35 I don't have much yet. 26/09 02:35 oh :) 26/09 02:35 And I need to rework sums/products, because I realized while I was trying to get to sleep last that my definition of products is a specification of a category that has all binary products. 26/09 02:36 this looks nice :) 26/09 02:37 what is Star by the way? I saw it in the standard library too 26/09 02:37 Of course, that leads to other issues, like should the specification for a product be parameterized by the two objects? By the product object? 26/09 02:38 hah, we have Nat, Rat, Mat, and Cat 26/09 02:41 yikes 26/09 02:41 people should try to use the full names 26/09 02:41 I like the postfix (co)product 26/09 02:48 is there any heterogeneous list-like structure in the standard library? 26/09 02:53 I was thinking of reworking the algebra module significantly! 26/09 02:59 to do crazy things 26/09 02:59 haven't quite decided how to go about it yet though 26/09 03:01 http://code.haskell.org/~dolio/agda-share/categorica/Category/Product.agda <-- what about that? 26/09 03:22 -!- copumpkin is now known as pumpkin 26/09 04:56 * pumpkin is trying to make Data.Rational less painful to typecheck 26/09 05:36 it takes 15 or 20 seconds every time I try to typecheck it 26/09 05:37 maybe more 26/09 05:37 is dependent type compilation inherently "whole-program"? 26/09 05:56 it shouldn't need to retypecheck things already typechecked 26/09 05:57 yeah, but the compiler essentially knows the structure of all the code in all the modules it loads 26/09 05:58 in fact it saves data in dot-files 26/09 05:58 there are .agdai files 26/09 05:58 I was trying to cut out the largest ones cause compilation is so slow 26/09 05:58 yeah, that what i was referring to yesterday, it has to know the implementation of each function, in case you want to prove something about it somewhere else 26/09 05:59 yeah 26/09 05:59 seems like it has the potential for amazing optimizations 26/09 06:00 but is also so complicated 26/09 06:00 There may be ways to hide stuff. 26/09 06:08 There's an "abstract" keyword. 26/09 06:08 But I don't really know what it does. 26/09 06:08 ah 26/09 06:09 Ah, abstract does hide the definition. 26/09 06:13 Whereas private prevents it from being directly exported, but it may still show up during reduction. 26/09 06:14 -!- pumpkin is now known as copumpkin 26/09 07:42 PreorderReasoning is pretty sweet. 26/09 08:31 My proofs are too big. 26/09 12:16 They're using all my memory. 26/09 12:16 category theory proofs? 26/09 12:29 Yes. 26/09 12:30 I'm half way through proving A x (B x C) is isomorphic to (A x B) x C 26/09 12:31 Or, almost half way. 26/09 12:32 I can't think of anything that would help reduce the size 26/09 12:35 since reflection probably doesn't apply here- that wouldn't help 26/09 12:35 you can't make stuff opaque either.. 26/09 12:36 Well now I don't know what's going on. I shut down and reloaded emacs, and now it doesn't even finish type checking. 26/09 12:56 Ah, apparently I'm overflowing the GHC stack somehow. 26/09 13:24 Well, the proof definitely types. But apparently the type checker can't verify that with everything filled in (as opposed to in goals) without using 75% of my memory and then overflowing the stack. 26/09 14:29 :/ 26/09 15:25 dolio: in that course on modularity, they seem to consider dependent sums and esistentials quite different, with the first one not providing abstraction 26/09 16:29 dolio: but that's essentially because in their formalism you've typecase over small types i guess? 26/09 16:29 though dependent sum could still have eta laws.. 26/09 16:36 actually, how do i specify that i want the record to be of type \Sigma a p here? 26/09 17:05 {a : Set} {p : a -> Set} {x : a} {v : p x} -> Σ.first (record{ first = x; second = v}) ≡ x 26/09 17:05 ah, solved 26/09 17:07 dolio: I run into the same problem just modifying existing standard library modules 26/09 17:21 I wonder if the proofs just get really large or if it's a space leak 26/09 17:34 omnomnom 26/09 18:00 copumpkin: eating is allowed in here? :o 26/09 18:00 yep 26/09 18:01 * jmcarthur sips coffee 26/09 18:01 FunctorSalad_: omnomnom 26/09 18:04 you can't eat in here, this is the agda room! 26/09 18:05 oh, whoops 26/09 18:05 sorry! 26/09 18:05 so we were wondering whether you can reason about haskell code in agda? 26/09 18:05 can use agda to reason about haskell code? 26/09 18:05 grr 26/09 18:05 maybe by translation from haskell to agda 26/09 18:05 of course nontermination would be a first obstacle 26/09 18:06 FunctorSalad_: there's a paper on it in ACM dunno if you can access that 26/09 18:06 not totally sure if it's the best approach 26/09 18:06 do you remember the name? 26/09 18:07 no 26/09 18:07 It's called Verifying haskell programs using constructive type theory 26/09 18:08 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.70.8486&rep=rep1&type=pdf 26/09 18:08 thanks vixey 26/09 18:09 hmm is that paper out of date about agda not enforcing totality? 26/09 20:03 you can disable the termination checker with a flag 26/09 20:08 Prood: fix id \qed 26/09 20:09 *Proof 26/09 20:09 gotta try that in homework.... 26/09 20:10 is | and \| the exact same glyph? 26/09 22:16 they look identical to me, but one gives a syntax error and the other works 26/09 22:17 no they aren't 26/09 22:17 | is reserved i think 26/09 22:17 yeah, I mean 26/09 22:17 they're not the same character but they have the same glyph 26/09 22:17 \| is some unicode char that looks like it 26/09 22:17 oh, they look differently in my font 26/09 22:18 http://snapplr.com/4d2f that's both of them, side by side :P 26/09 22:18 \| is a little shorter 26/09 22:18 * Saizan doesn't remember how to take a screenshot 26/09 22:19 * copumpkin wants circular imports in agda 26/09 22:19 it's preventing me from defining unique factorization domains in algebra 26/09 22:20 mutual doesn't work for modules, i guess? 26/09 22:21 well, my problem is that I'd like to import a Map/Set/Multiset module to define unique factorization 26/09 22:23 not sure how else to do it 26/09 22:23 not even sure how to do it with a map structure 26/09 22:24 maybe I should build it with a Vec 26/09 22:24 even then, I still can't import Data.Vec because it makes a circular import 26/09 22:25 hm 26/09 22:26 any ideas on how to express unique factorization without depending on something external? 26/09 23:02 (and not duplicating code) 26/09 23:02 copumpkin: hmm there are some properties not involving lists which are equivalent 26/09 23:05 well, you can also say that every nonzero nonunit element is a product of primes 26/09 23:05 but that's also "setty" 26/09 23:06 http://en.wikipedia.org/wiki/Unique_factorization_domain#Equivalent_conditions_for_a_ring_to_be_a_UFD 26/09 23:06 seems like I'd need a lot of support code to express any of thos 26/09 23:08 e 26/09 23:08 "every irreducible is prime" is quite elementary 26/09 23:09 but there's still this ascending chain condition 26/09 23:09 yeah 26/09 23:09 hmm 26/09 23:10 and I suppose you want the /explicit/ unique factorization anyway ;) 26/09 23:10 you could use lists and say "unique up to permutation" 26/09 23:10 or unique ordered list 26/09 23:10 if the ring is orderd, anyway 26/09 23:10 well I was planning to express it as forall xs ys. product xs == x -> x /= 0 -> x /= 1 -> product ys == x -> xs == ys 26/09 23:11 or something like that 26/09 23:11 yes, but the last (==) has to be up to permutation 26/09 23:12 (and you must ban units in the list) 26/09 23:12 hmm and the primes can differ by units too :) 26/09 23:12 well I can't use the standard library lists because of circular imports 26/09 23:13 FunctorSalad_: oh well I was envisioning the product take a MultiSet or something like that 26/09 23:14 but we don't have such a module anyway 26/09 23:14 to avoid the issue of permutations 26/09 23:15 copumpkin: map of (primes) to nat? 26/09 23:15 (with all but finitely many values zero) 26/09 23:15 I guess that would be complicated too, eh 26/09 23:15 hmm 26/09 23:16 is it reasonably easy to work with equivalence relations in agda? 26/09 23:17 nothing much is easy for me at this point, so I can't really comment :) 26/09 23:20 --- Day changed Sun Sep 27 2009 -!- koninkje1away is now known as koninkje_away 27/09 02:19 -!- opdolio is now known as dolio 27/09 03:08 Saizan: I don't fully grok the difference between weak and strong sums (existential and dependent sums). 27/09 03:09 Saizan: But strong sums somehow let you get a hold of the first parameter in a way that weak sums don't. 27/09 03:10 the eliminators are different 27/09 03:10 I guess that may be it. 27/09 03:10 with strong sums the type of the return value can depend on the value of the contents, or something 27/09 03:10 sig_rect 27/09 03:11 : forall (A : Type) (P : A -> Prop) (P0 : sig P -> Type), 27/09 03:11 (forall (x : A) (p : P x), P0 (exist P x p)) -> forall s : sig P, P0 s 27/09 03:11 (that's in coq, sorry I don't have an agda handy) 27/09 03:11 so the P0 (the elimination thingy) can depend on x and p 27/09 03:12 Yeah. 27/09 03:12 I seem to recall you can't encode strong sums in CoC without them. 27/09 03:12 (but I'm not completely sure that that is the difference) 27/09 03:13 But weak sums are easy. 27/09 03:13 ("sig" is sigma type there, and "exist" is its constructor) 27/09 03:13 Oh, I see why. 27/09 03:17 weak sums are just {a b : Set} {p : a -> Set} -> ((x : a) -> p a -> b), which indeed prevents you from mentioning x in b 27/09 03:20 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a9879 27/09 03:20 ops, .. -> b 27/09 03:21 we need an hpaste that does agda html 27/09 03:21 glguy's mused about adding it to hpaste2, but I'm not sure if he's working on it or not. 27/09 03:22 or AGDABOT? 27/09 03:22 mmm 27/09 03:23 It's a bit harder to do something in one line of agda than in one line of haskell. 27/09 03:23 hmm 27/09 03:24 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a9881 <- i've found quite surprising that x typechecks there 27/09 03:24 but now i see how strong sums are really transparent 27/09 03:24 Saizan: Anyhow, that inability of the eliminator result to depend on A in weak sums gets you more 'abstraction' than with strong sums, I think. 27/09 03:24 Even though you can't really inspect the type stored in 'Sigma Set T' in any way. 27/09 03:26 Without type case and whatnot. 27/09 03:26 yup, i think i get it now 27/09 03:26 It's like a parametricity result, rather than a "what programs can I practically write, but the type system doesn't necessarily guarantee" result. 27/09 03:27 btw, can you write a Sigma that can contain both types and values as the first field depending on how you instance it? 27/09 03:27 Sigmas that contain types are kind of a pain in agda, because they live in Set1. 27/09 03:28 Universe polymorphism fixes that, though. Then there can be one sum that's parameterized by the level. 27/09 03:29 yeah, but since we're talking about modules i'd expect that 27/09 03:29 Well, I just mean if you want to do it all with sigmas, you need a Sigma1 and a Sigma0 right now. 27/09 03:30 Of course, records are 'just' sugar for a string of sigmas. :) 27/09 03:30 ah, no data Sigma (U : ?) (A : U) (A -> Setn) : Setn where .., where 'n' is some fixed one, then? 27/09 03:31 Oh, well, that third paramater can't have that type. It needs to be... 27/09 03:32 i mean, there's no valid thing i can put in place of ? so that i can have U = Set and U = Set1 27/09 03:32 Sigma (U : ?) (A : U) ((A : U) -> A -> Setn) ... 27/09 03:33 Oh. Hmm. 27/09 03:33 Well, you can have ? = Set2, but that's pretty non-specific. 27/09 03:34 Or you can use an explicit universe 'data MySets : Set where MySet : MySets ; MySet1 : Mysets ; up : MySets -> Set2 ; up MySet = Set ; up MySet1 = Set1' 27/09 03:36 Then Sigma (U : MySets) (A : up U) ... 27/09 03:36 uhm, doesn't seem to work with Set2 27/09 03:38 Well, it's going to have to be at least Set2 as a result. 27/09 03:38 I think that's true of both encodings. 27/09 03:39 Maybe the second can go down to Set1. 27/09 03:39 dolio: interestingly, records in agda seem (according to documentation) to be subject to eta-convertiblity; i wonder if this is really necessary in practice 27/09 03:40 I don't think it's necessary. It's useful, though. 27/09 03:41 Ordinary data not being subject to eta can be kind of a pain. 27/09 03:41 how would I define a simple heterogeneous list in agda? 27/09 03:42 Define a list of types, and then parameterize by that. 27/09 03:43 Or, index by that, I should say. 27/09 03:43 as in the existing List\_1 ? 27/09 03:43 Yes. 27/09 03:43 aha 27/09 03:43 dolio: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a9882 27/09 03:44 Oh. Yeah, forget that version. 27/09 03:45 It's not going to work because A isn't necessarily a type. 27/09 03:46 it's weird that it complains about it not being (A : Set1), and not (A : Set) though 27/09 03:48 Oh crap, the universe one doesn't work, either, because Set :/ Set2. 27/09 03:49 ah, i thought it did 27/09 03:50 It's still strict containment. Set : Set1, Set1 : Set2 ... 27/09 03:50 ok, no single sigma for me 27/09 03:51 I must say, it's weird that the slides for translucent sums use 9 for the existential quantifier. 27/09 03:53 yeah. i already noticed an 8 in some of the previous ones 27/09 03:56 I'd use 100000 to be safe ;) 27/09 04:03 the space could vanish quickly if you put new things into the middle.. 27/09 04:04 * copumpkin seems to have written a circular data type that is impossible to type (if I make it of type Set, it wants Set1, if I make it of type Set1, it wants Set2, and so on) 27/09 04:05 I wonder if this new universe polymorphism thing can help me here 27/09 04:11 or whether my definition is just flawed 27/09 04:12 what did you do? 27/09 04:12 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9883#a9883 27/09 04:13 I assumed it would have to live in Set1 because the properties are in Set 27/09 04:13 but no Setn seems to work 27/09 04:13 oh duh 27/09 04:15 I'm just stupid, sorry 27/09 04:15 I forgot to pass the parameters to the Property return type 27/09 04:16 some question: i tried to formalize a bit of category theory in agda, but quickly ran into the problem of typechecking taking time (and space!) exponential to the amount of code i had written; i suspect this is the result of me consistently mixing "data" and "properties" in the same record types (i hoped the typechecker would be "lazy enough" to deal with this, but apparently not) 27/09 04:18 ecst: dolio was just complaining about his CT stuff taking forever too 27/09 04:18 yesterday 27/09 04:18 i realize most library examples avoid this by separating "data" and "properties" into different records 27/09 04:18 Yeah. My module for product no longer type checks. 27/09 04:19 but is there a way the aleviate this and continue writing in a "mathematical" style (grouping data and properties together)? 27/09 04:19 Is that why the standard libraries are organized that way? 27/09 04:20 it seems 27/09 04:20 I'll have to try that. 27/09 04:20 i have yet to find out how to do this separation while not introducing significant amounts of code overhead 27/09 04:22 in particular in regards to equivalence relations emulating extensional equality 27/09 04:24 Yeah, well, I decided to scrap using setoids as the basis for categories pretty quickly. 27/09 04:27 I just stuck a postulate for extensionality in my equality module. 27/09 04:27 how dare you?? 27/09 04:27 Because having the arrow construction produce a setoid makes composition pretty heinous. 27/09 04:28 ;) 27/09 04:28 And I'm sure it would only get worse from there. 27/09 04:28 well, i took that path (though i need extensionality only for category morphism), and it definitely got worse 27/09 04:31 but i still think it is the typecheckers fault 27/09 04:31 but you will need quotients one day 27/09 04:31 quotients have been neglected by type theory in general :( 27/09 04:32 i thought setoids subsume quotients 27/09 04:32 yes 27/09 04:33 I meant without setoids 27/09 04:33 ah 27/09 04:33 support on the computational level would be nicer presumably 27/09 04:34 hm, dunno, i am a purist :) 27/09 04:35 i really have no problem manually emulating this stuff low-level if only the typechecker would behave 27/09 04:35 I don't think this splitting is helping much. 27/09 04:58 then i am at a loss as for the reason 27/09 04:58 the point where i was stuck (as to computer resources) was the definition of prefixing a natural transformation with a functor 27/09 05:04 this was the first time that the result of a function depended on something like (compose-functors F G) 27/09 05:05 result -> result type 27/09 05:05 which of course involved a proof that the functor properties hold for the composition, but which is irrelevant for the function being defined 27/09 05:05 hmm maybe you can relax your properties to hold up to isomorphism 27/09 05:06 prefixing a NT with a functor is a special case of horizontal composition of NTs... 27/09 05:06 I doubt that'll make Agda use less memory. 27/09 05:06 ^^ 27/09 05:07 thought the problem was still equality 27/09 05:07 no, it is the typechecker using exponential resources for non-exponential problems 27/09 05:07 fire up the profiler? 27/09 05:08 there is a profiler? where can i find it? 27/09 05:09 I don't know if agda has one of its own, but you could compile agda with profiling 27/09 05:09 then agda +RTS -P 27/09 05:09 ? 27/09 05:09 well, i am no haskell hacker :( 27/09 05:09 maybe post the mailing list about it? 27/09 05:17 I think I will. I'll at least ask if the std-lib is structured the way it is to avoid performance problems. 27/09 05:18 the current algebra module is rather painful to use, unless I'm missing something 27/09 06:04 can I close a module after opening it? 27/09 06:15 You can open it within a scope. 27/09 06:18 Like creating a new (nested) module and opening in there, for instance. 27/09 06:19 ah 27/09 06:19 I was hoping to be able to do that within a data declaration, but it just gave me a parse error 27/09 06:19 I'll try doing it in a module 27/09 06:19 is there the equivalent of newtype in agda? 27/09 07:38 No. 27/09 07:41 Actually... 27/09 07:41 :o 27/09 07:47 http://code.haskell.org/~dolio/agda-share/html/Newtype.html 27/09 07:49 oh that's neat :) 27/09 07:50 Anything that needs to know that they're the same type has to go on that abstract block. 27/09 07:50 yeah 27/09 07:52 _mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor 27/09 07:55 it seems odd for it to require divisor to not be zero 27/09 07:56 since Fin 0 is empty anyway 27/09 07:56 Yeah, but that means it's impossible for you to produce a Fin 0. 27/09 07:56 yeah, but doesn't that effectively say you can't pass a zero divisor in the first place? 27/09 07:57 maybe I'm confusing notness 27/09 07:57 No, you can pass whatever you want. 27/09 07:57 Without the proof, it would have to give you back a Fin 0. 27/09 07:58 I thought a proof of not p was p -> empty type, and fin 0 was an empty type 27/09 07:58 With it, when you write 'n mod 0' it gives back {False (0 == 0)} -> Fin 0. 27/09 07:58 or rather, a statement of not p 27/09 07:58 hmm 27/09 07:58 And when you provide it with that proof that 0 == 0 is false, it will provide you with a Fin 0. 27/09 07:59 But you can never provide it with the proof, of course. 27/09 07:59 so the issue is that it doesn't fundamentally know that Fin 0 is empty 27/09 08:00 No, it does. 27/09 08:00 so say you have (with no proof this time) _mod_ : (dividend divisor : ℕ) → Fin divisor, and write _mod_ 5, which should have type (divisor : ℕ) → Fin divisor 27/09 08:02 Yes. 27/09 08:02 when divisor is 0, that looks very much like divisor == 0 -> _|_ 27/09 08:02 but I guess it isn't explicitly that 27/09 08:04 So, suppose I call it with 0. Where are you going to get the Fin 0 from? 27/09 08:06 You must return one. 27/09 08:06 yeah, I see 27/09 08:06 If you have a bottom already, you can use that. 27/09 08:06 Which is what the (False (n == 0)) gives you. 27/09 08:06 yeah 27/09 08:06 now, if I have a member of Fin n, can I extract trivially that False (n ?= 0)? 27/09 08:07 Well, as trivially as writing a function and doing case analysis, because working with that False stuff is kind of a pain. 27/09 08:08 ah well, it's simple enough I guess :) 27/09 08:10 You need two cases anyway, I suppose. 27/09 08:11 Even if it were just a proof of n /= 0. 27/09 08:11 yeah 27/09 08:11 it was so simple that even I wrote it with no effort at all :P 27/09 08:11 I'm writing modular arithmetic and polynomials 27/09 08:14 The False stuff just expands one of the cases into a with. 27/09 08:14 does http://snapplr.com/7qgp look weird for a type name? 27/09 08:34 I'm not sure why people call it Z/ instead of N/ 27/09 08:34 Prejudice against the natural numbers. 27/09 08:35 Looks fine to me. 27/09 08:36 all over wikipedia they actually say Z/_Z, but that felt really cumbersome to write 27/09 08:36 Z mod Z? 27/09 08:37 Z/nZ 27/09 08:37 Oh right. 27/09 08:37 I couldn't think of a very nice way to define arithmetic on Fin n directly. 27/09 08:39 the stuff in Data.Fin is rather ugly, yeah 27/09 08:39 hmm, I wonder if I can pull the extended euclidean algorithm out of the GCD stuff 27/09 08:45 Of course, it's pretty easy with a Σ m:ℕ m (carrier (B => C)) -> (carrier (A => B)) -> (carrier (A => C))" 27/09 19:43 hmm? in coq you can have it be "forall {A B C}, (B => C) -> (A => B) -> (A => C)" and require each (X => Y) to be an instance of Setoid 27/09 19:59 (forall {A B}, Setoid (A => B)) 27/09 20:00 (the carrier type isn't wrapped inside the setoid) 27/09 20:00 then you also require the composition to be respectful w.r.t. the setoids 27/09 20:01 (again, the function is not wrapped in the respectfulness ("Proper") instance, it's a param) 27/09 20:02 Hmm, after some experiments, --proof-irrelevance may make things somewhat easier. 27/09 20:02 does agda have typeclasses or some other automatic way to find Eq/Ord/Setoid/etc. instances for a given type? 27/09 20:03 No. 27/09 20:03 Hmm, except you can't have equality of equalities if equalities live in Prop (since it takes Sets). 27/09 20:08 Also, --type-in-type appears to turn off --proof-irrelevance. :) 27/09 20:09 -!- FunctorSalad_ is now known as Semilettuce 27/09 22:00 -!- copumpkin is now known as DistributiveLett 27/09 22:03 -!- DistributiveLett is now known as copumpkin 27/09 22:04 --- Day changed Mon Sep 28 2009 -!- opdolio is now known as dolio 28/09 04:35 -!- opdolio is now known as dolio 28/09 08:33 So, now, Agda type checks my code without using 75% memory and overflowing the haskell stack. 28/09 08:35 dolio: you removed 75% of your code? :) 28/09 08:36 I don't think so. :) 28/09 08:37 Oh wait... 28/09 08:39 I did change one thing in the branch that made it work... 28/09 08:39 Nope, that wasn't it... 28/09 08:48 Well now I'm totally at a loss. Apparently turning equality from Set to Prop, turning on proof irrelevance, reloading everything, then turning it back to Set and reloading everything caused it to work. 28/09 08:53 Whereas just loading it as Set from the get-go doesn't. 28/09 08:53 Nope, that doesn't seem to be working, either. 28/09 09:00 Ah hah! 28/09 09:13 -!- EnglishGent is now known as EnglishGent^afk 28/09 09:22 Evidently my problem was that I needed to put a {C} in when opening/using a module in a couple places. 28/09 09:40 Without that {C}, it uses at least 3x the memory and overflows the stack. :) 28/09 09:40 -!- EnglishGent^afk is now known as EnglishGent 28/09 10:24 -!- FunctorSalad_ is now known as FunctorSalad 28/09 16:54 -!- codolio is now known as dolio 28/09 19:12 what is proof irrelevance? 28/09 20:14 I found http://www.cs.cmu.edu/~fp/courses/15317-f08/lectures/08-irrelevance.pdf but the language in it is a bit over my head 28/09 20:14 it means that all the proofs for a certain proposition are considered equal 28/09 20:16 you clearly don't want that if the proposition has computational content 28/09 20:16 s/a certain/any/ 28/09 20:17 computational content? as in, "does something"? the difference between stating that a number is composite and returning its factors? 28/09 20:17 P \/ Q has computational content (typically), because you can inspect the proof and decide to do a different thing depending on whether you receive a proof of P or a proof of Q. 28/09 20:19 oh 28/09 20:19 If proofs have no computational content, then you get the same results no matter what proof is used. 28/09 20:20 yeah, you usually encode \/ with /\ and negation, i guess? 28/09 20:21 That might be one way. 28/09 20:21 If you can take quotients, that might be another. 28/09 20:21 Smash (P \/ Q) would be okay, I guess. 28/09 20:21 --- Day changed Tue Sep 29 2009 * copumpkin shifts his agda to his macbook pro with more RAM and a heftier CPU 29/09 01:05 -!- pumpkin is now known as copumpkin 29/09 04:29 -!- anders^^ is now known as boefst__ 29/09 18:01 -!- byorgey is now known as axnqfdx 29/09 18:27 has anyone looked into dependent types + subtyping? 29/09 19:53 http://www.cs.rhul.ac.uk/~zhaohui/subtyping.html 29/09 20:09 Did that get through/ 29/09 20:12 thanks, yep :) 29/09 20:12 I haven't read any of his stuff yet. 29/09 20:13 He's a big name in type theory, though. 29/09 20:13 cool 29/09 20:13 Lots of people reference his book and UTT type theory, but I don't think there's any way to get it. 29/09 20:13 His thesis and other stuff on ECC is widely referenced, too. 29/09 20:14 Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, 11. Oxford University Press, 1994. (ISBN 0 19 853835 9) 29/09 20:14 that one? 29/09 20:14 I guess the other one is in chinese 29/09 20:14 Yes. 29/09 20:14 ooh, there's a copy in the library 29/09 20:15 I should say, I happen to be looking at a paper he co-authored now trying to get a handle on universe polymorphism (hopefully). 29/09 20:15 wow, it's expensive on amazon 29/09 20:15 Wow, it's still in print, even. 29/09 20:16 Unfortunately, books like that end up being ridonkulously expensive due to the limited interest. 29/09 20:17 yeah :/ 29/09 20:18 you could probably steal it off google books 29/09 20:18 would take some effort though 29/09 20:18 They randomly blank out pages and stuff, don't they? 29/09 20:18 oh, yeah :/ 29/09 20:18 going to implement universe polymorphism? 29/09 20:19 I'm just trying to get a handle on what's been done in that regard. 29/09 20:19 For instance, I suspect most systems aren't subject to the thing on the mailing list about Set_omega, because quantification over universes isn't first-class, exactly. 29/09 20:20 -!- Saizan_ is now known as Saizan 29/09 20:23 hey someone should code parametricity in Agda 29/09 20:35 & write a paper on it :P 29/09 20:35 -!- Saizan_ is now known as Saizan 29/09 22:01 -!- boefst__ is now known as anders^^ 29/09 22:01 --- Day changed Wed Sep 30 2009 -!- Saizan_ is now known as Saizan 30/09 01:33 -!- axnqfdx_ is now known as axnqfdx 30/09 02:32 -!- axnqfdx is now known as byorgey 30/09 11:55 i have problems to get agda working. if i load a file from within the emacs mode, it says parse error all the time (even on an empty file), same problems with the batch compiler (agda -c). im running ghc 6.10.4 and emacs 23.1 on a 64 bit linux 30/09 14:04 is this a known problem (i dont know what to do) ? 30/09 14:04 I've not heard of that 30/09 14:05 Completely empty, or with a module declaration? 30/09 14:05 It might not accept the former. 30/09 14:05 doesnt matter what the content of the file is, it says parse error all the time 30/09 14:06 -!- Saizan_ is now known as Saizan 30/09 15:17 -!- opdolio is now known as dolio 30/09 20:25 -!- copumpkin is now known as macweenie 30/09 21:36 -!- macweenie is now known as copumpkin 30/09 21:38 -!- copumpkin is now known as TheHunter 30/09 22:11 -!- TheHunter is now known as copumpkin 30/09 22:11