# /home/laney/.irssi/irclogs/Freenode/2009/#agda/December.log

quantumEd uorygl copumpkin --- Log opened Tue Dec 01 00:00:05 2009 heh http://namebinding.wordpress.com/ 01/12 00:44 copumpkin: write everything in Agda and translate it to other systems as desired. 01/12 01:39 uorygl: unfortunately that doesn't work for things that might not terminate 01/12 01:39 If you can prove it in Agda, and Agda is correct, you can prove it in any universal proof system. If you can compute it in Agda, you can compute it in any universal computation system. 01/12 01:53 definitely 01/12 01:54 but I want something that I can't prove in agda without jumping through hoops 01/12 01:54 Prove that NBG is a conservative extension of ZFC. 01/12 02:09 done, next? 01/12 02:15 Constructively prove that it is possible to pastebin your proof and post the link to this channel. 01/12 02:26 lol 01/12 02:27 * copumpkin shuffles subtly toward the door 01/12 02:27 I don't suppose you feel like taking up my effort to write NBG. 01/12 02:28 Or anyone else. 01/12 02:29 uorygl: you should read this http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709 01/12 02:29 What's that about? 01/12 02:31 * uorygl ponders what a "bijection" is. 01/12 02:45 A bijection is a set of ordered pairs such that for any two pairs, their first elements are equal if and only if their second elements are equal. 01/12 02:46 (Yeah, I'm using this channel as a notepad.) 01/12 02:47 * uorygl ponders what an "ordered pair" is. 01/12 02:47 a function from Fin 2 to A 01/12 02:48 uorygl, or don't ... whatever 01/12 02:48 quantumEd: well, I'm wondering whether it would help me do this or be interesting. 01/12 02:49 anyone know where I can get some kind of basic command line tool written in agda, like an interpreter or something 01/12 02:53 I can't think of a nice and simple way to say that a set is of the form {{a},{a,b}}. I guess I'll just brute force it and say "there exist a and b such that S = {{a},{a,b}}". 01/12 02:55 Then a "first element" is an element of every element, and a "second element" is an element of exactly one element. 01/12 03:11 Hi all, 01/12 10:32 is there a way in emacs to introduce variables a kind of intro command 01/12 10:32 ? 01/12 10:33 you mean those from implicit arguments? 01/12 10:33 -!- EnglishGent is now known as EnglishGent^afk 01/12 11:46 Saizan: no even explicit ones 01/12 11:54 I suppose that refine should do the job, but it doesn't, anyone ? 01/12 13:57 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=291 blegh 01/12 21:29 why doesn't he just post the code ? 01/12 21:29 post a comment asking for it 01/12 21:30 ? 01/12 21:30 oh, someone already asked 01/12 21:31 i don't get Nicolas Pouillard reply, can't you compute the principal type for lambda terms without annotations, in STLC? 01/12 21:32 i mean, you can do it for hindley milner 01/12 21:32 im not sure you can because e.g.  (\x -> x)  could be  T -> T, or (T -> T) -> (T -> T) etc 01/12 21:33 ah, i guess i mean type schemas 01/12 21:33 apropos principal types, the article could use some help ;) http://en.wikipedia.org/wiki/Principal_type 01/12 21:34 (funny that less polymorphism makes this kind of problem harder :) 01/12 21:35 does "most general" even make sense without variables? 01/12 21:36 or do you get metavariables for STLC 01/12 21:36 i guess talking about principal types doesn't make much sense for STLC 01/12 21:37 i think i've seen "principal type schema" which would be with metavariables 01/12 21:37 hmm are there any interesting programs that can be expressed in STLC actually? 01/12 21:38 it seems very weak 01/12 21:38 what interesting programs :P 01/12 21:38 you can use simple types for a real world programming language 01/12 21:38 what do you mean? 01/12 21:38 ah 01/12 21:38 (that reply was before your second msg) 01/12 21:39 yeah, but those realworld-langs have fix' 01/12 21:39 I don't see how to express much of anything in STLC alone 01/12 21:39 (but I haven't tried) 01/12 21:39 well, you have to add first order data and a let construct i think, however STLC is more like the fibonacci for typecheckers 01/12 21:42 Saizan it occured to me that I could use agda instead of haskell (just turn on the no termination checking and non positive types and so on) 01/12 21:46 I think so anyway, I'm not sure how the compiler does 01/12 21:47 where do you need negative types? 01/12 21:48 evaluation 01/12 21:48 reify something into D~D->D and then pull it back into syntax to get the beta normal form 01/12 21:49 ah, right 01/12 21:49 -c      --compile               compile program (experimental) 01/12 21:54 guh 01/12 21:54 this sucks 01/12 21:54 If you add in some extra types beyond arrows, STLC gets a little more useful. 01/12 21:55 Like, Nat/Int, sums, products, unit, empty. 01/12 21:55 Those can technically all be 'simple' types. 01/12 21:56 yes you can use a make a fully featured language with STLC, something like C or ALGOL or whatever 01/12 21:56 adding naturals, if and fix gives you a turing-complete language (PCF) 01/12 21:56 unless I missed one :) 01/12 21:56 ohh yeah true 01/12 21:57 that's a better example than mine 01/12 21:57 It's just that without any polymorphism, you'll be writing a lot of the same functions over and over. 01/12 21:57 yeah 01/12 21:57 Plain STLC is bad, though, because you can't encode the types using lambda terms like you can in System F. 01/12 21:58 -!- opdolio is now known as dolio 01/12 21:58 opdolio, you have the complementary colour of dolio in my scheme :o 01/12 21:58 Nice. 01/12 21:58 wkat the hell ://///// 01/12 22:03 primTrustMe : {A : Set}{a b : A} → a ≡ b 01/12 22:03 this sucks 01/12 22:03 error: There is no primitive function called primTrustMe 01/12 22:03 wow 01/12 22:03 where is that? 01/12 22:04 How old is your agda? 01/12 22:04 Relation/Binary/PropositionalEquality/TrustMe.agda:11,4-44 01/12 22:04 http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Binary.PropositionalEquality.TrustMe.html#234 01/12 22:05 lol 01/12 22:05 It's used for String equality. 01/12 22:05 Possibly others. 01/12 22:05 it sucks ! 01/12 22:06 well, it's interfacing with primitive haskell stuff 01/12 22:07 not sure how else you'd pull out an equality proof 01/12 22:08 I guess it shouldn't even be decidable because the string is potentially infinite? 01/12 22:09 should I do cabal install agda --reinstall? 01/12 22:09 to get up to  date 01/12 22:10 I think trustme was added after the last release. 01/12 22:10 and also darcs pull in /lib 01/12 22:10 So you'd have to install from darcs. 01/12 22:10 :( 01/12 22:11 this sucks 01/12 22:11 Unless you're not getting the library from darcs. 01/12 22:11 I don't know why I even try and write programs anymore :p 01/12 22:11 I think trustMe is fine, but its usage should propagate an "infected with evil" flag in the .agdai files 01/12 22:12 so you can get warnings 01/12 22:12 I don't think Strings can be infinite. 01/12 22:12 im not using agda to check proofs 01/12 22:12 just want to code a typechecker 01/12 22:12 Anything that could result in an infinite list of characters probably returns a Costring. 01/12 22:13 I upgraded now I get unrecognized option --universe-polymorphism' 01/12 22:13 hm 01/12 22:13 that might be progress in the forward direction 01/12 22:13 I don't actually see why it's using primitive strings at all there. If we have Costring = Colist Char, why not have String = List Char ? 01/12 22:14 Speed? 01/12 22:14 oh, for people who actually run their programs 01/12 22:14 keep forgetting 01/12 22:14 pff 01/12 22:14 Haskell Strings aren't exactly speed demons either, though. 01/12 22:17 Establishing a correspondence between Haskell Strings and Agda List Chars might be difficult, though. 01/12 22:17 People run their programs too these days? 01/12 22:17 Assuming you want them to work in extracted code. 01/12 22:18 I suppose you have to, to check whether they work 01/12 22:18 what is this intro/refine command they mention in the commits? 01/12 22:20 Also, having String built-in probably displays nicer, and I'm not sure that their system would work if you tried to declare {-# BUILTIN STRING List Char #-}. 01/12 22:21 I installed the newest Agda and it still doesn't like the std lib 01/12 22:21 Wow, it finished compiling already? 01/12 22:22 haskell strings aren't bad if they get fused :) 01/12 22:22 quantumEd haz quantum computer 01/12 22:22 still unrecognized option --universe-polymorphism' 01/12 22:24 oh, did you install it from darcs? 01/12 22:24 did you recompile the agda-executable too? 01/12 22:25 cause the latest one in hackage is olde 01/12 22:25 how do I do that Saizan? 01/12 22:25 cd src/main/ && cabal install 01/12 22:25 ummm 01/12 22:27 that did soemthing 01/12 22:28 now I get a different error about the trustme file 01/12 22:28 No binding for builtin thing REFL, use {-# BUILTIN REFL name #-} to 01/12 22:28 bind it to 'name' 01/12 22:28 when checking that the type of the primitive function primTrustMe 01/12 22:28 is {A : Set} {a, b : A} → a ≡ b 01/12 22:28 that's defined in Relation/Binary/Core.agda 01/12 22:29 * Saizan has no idea how these things work 01/12 22:29 * quantumEd thinks it's quite simple: They don't :P 01/12 22:29 *are supposed to work :) 01/12 22:30 if this system ever worked it must have been a complete coincidence 01/12 22:30 what are you trying to compile btw? 01/12 22:30 nothing yet, 01/12 22:30 I was trying to typecheck something that does  import IO 01/12 22:31 oh the solution is quite obvious, don't use the standard library... 01/12 22:31 bah, i get an even different error from the executable (it works fine in emacs though) 01/12 22:37 what do I use for malonzodir? 01/12 22:38 the manual says which is really really helpful 01/12 22:39 * quantumEd supposes src/full/Agda/Compiler/MAlonzo 01/12 22:39 wow, it compiled! 01/12 22:44 what did? 01/12 22:44 module Foo where open import IO; main = run (putStrLn "hello world") 01/12 22:45 with: agda -i../Agda/lib/src/ -i/home/saizan/snippets/ Foo.agda --compile 01/12 22:45 everything from darcs 01/12 22:46 it runs too 01/12 22:46 great! thank you 01/12 22:48 now I have that working too 01/12 22:48 np 01/12 22:49 Is \eq the same thing as =, \iff the same thing as \<=>, and so on? 01/12 23:30 Type them in and type 'C-u C-x =' with the cursor over them to see if the characters are the same. 01/12 23:32 I guess so. 01/12 23:35 --- Day changed Wed Dec 02 2009 is there any reason so many constructors in the standard library name parameters and don't use the names? 02/12 00:56 suc  : {n : ℕ} (i : Fin n) → Fin (suc n) 02/12 00:56 like that? 02/12 00:56 I was going to say "readability" but I don't suppose a name like "i" really helps... 02/12 01:00 habit, probably 02/12 01:00 fair enough :) 02/12 01:00 When you do C-c C-c, agda uses the names specified in constructors to fill in names in the patterns. 02/12 01:01 Otherwise you get stuff like x, x', y, y'. 02/12 01:02 ah, I see 02/12 01:02 With that definition, it'd fill in "suc {n} i", which is probably nicer. 02/12 01:02 Although it probably wouldn't fill in the {n} at all. 02/12 01:03 * quantumEd starts my own module Prelude.agda 02/12 01:42 What does the Agda distribution consist of? 02/12 01:49 So far, I've seen Emacs, some Emacs plugin thing, and a typechecker. I'm guessing it's also possible to run an Agda program, but I've never tried to. 02/12 01:53 pretty much that, and there's a standard library in a separate repository 02/12 01:56 I believe it has two compilers, too 02/12 01:57 yeah, i discovered today that you can compile things! 02/12 01:57 * uorygl nods. 02/12 02:09 It sounds like the typechecker is the guts of the operation. 02/12 02:09 oh for goodness sake 02/12 02:11 Type checking agda requires evaluating agda, though. 02/12 02:11 you can't call a function 'abstract' in agda 02/12 02:11 this is bloody stupid 02/12 02:11 abstract is a keyword. 02/12 02:11 What's the computational complexity of the typechecker? 02/12 02:14 Well, let me say that differently. Is it possible to make a relatively short file that takes a really long time to typecheck? 02/12 02:15 Well, the type checker may have to execute arbitrary agda terms. 02/12 02:15 So even if you restrict yourself to terms that would pass the termination checker... 02/12 02:15 Sounds like there's probably a one-kilobyte file that will never typecheck. 02/12 02:16 almost certainly. 02/12 02:16 You could write a program that requires the type checker to compute the Ackermann function at some value. 02/12 02:17 Value(s). 02/12 02:17 Note to self: if I run an Agda typechecker online, I should have it give up after a while. 02/12 02:18 how do I use with twice? 02/12 02:19 Twice as in matching on two things with a single with, or a second with after another? 02/12 02:20 one after the other 02/12 02:21 You just put another "with ..." after you match on the stuff in the first with. 02/12 02:21 quantumEd: you can put 02/12 02:21 | in 02/12 02:21 with f x | g y 02/12 02:22 I think 02/12 02:22 That's how you match on two things with a single with. 02/12 02:22 oh ok :) 02/12 02:22 cool 02/12 02:23 test = eval (App (Lam (App (Var fz) (Var fz))) (Lam (Var fz))) 02/12 02:23 test ~> Lam (Var fz) 02/12 02:24 now I need a parser and pretty printer for lambda terms 02/12 02:24 who is writing that? :P 02/12 02:24 There are some parser combinators in agda somewhere. 02/12 02:24 People have been writing papers on them. 02/12 02:25 I'm not sure what sorts of grammars they're usable for. 02/12 02:25 btw 02/12 02:25 I can't figure out this with thing 02/12 02:25 I have got 02/12 02:25 Nat-lem1 refl = refl 02/12 02:25 so shouldn'g 02/12 02:25 S n =Nat= S m with n =Nat= m 02/12 02:25 ... | inl q = inl (Nat-lem1 q) 02/12 02:25 be able to be written a lot easier? 02/12 02:25 I mean without the lemma 02/12 02:25 You mean match on q with refl? 02/12 02:26 yes 02/12 02:26 I think you might not be able to use the ... if you want to do that. 02/12 02:26 what does inl refl do? 02/12 02:26 You'd have to write "S n =Nat= S .n | inl refl = inl refl" 02/12 02:26 Because the match on "refl" refines the m to be the same as n (or vice versa). 02/12 02:27 inl refl : (n ≡ n) ∨ (~ (n ≡ n)) 02/12 02:27 dolio ah! I get it, thanks - that actually makes some sense 02/12 02:28 Nat-lem2 : forall {n m : Nat} -> S n ≡ S m -> n ≡ m 02/12 02:28 Nat-lem2 refl = refl 02/12 02:28 so for this one .. 02/12 02:28 ... | inr f = inr (\x -> f (Nat-lem2 x)) 02/12 02:28 can it also be removed? 02/12 02:28 I think not 02/12 02:28 I don't think so, no. 02/12 02:29 I didn't see any proofs that relate prettyprinting to parsing with the structural combinator stuff 02/12 02:32 it's actually kind of hard to get all the machinary up and running for that though so maybe it's just a matter of how much tedium it would be to add 02/12 02:32 Pretty printing isn't as hard a problem as parsing, termination wise, is it? 02/12 02:33 no 02/12 02:33 what I mean is putting a condition into the type of a parser, that says what well.... it's kind of difficult to even state this :/ 02/12 02:34 Proving that they're somewhat inverse? 02/12 02:35 you can't just say  pretty printing it gives you the text you were looking at back - if parsing (f x y) gives the same as ((f x) y), but you can't say parsing the pretty printed version of what we parsed would giv you back what we parsend in the type of parser because that's some kind of insane recursion 02/12 02:36 pretting printing isn't injective that's the problem 02/12 02:37 hm 02/12 02:37 that's wrong 02/12 02:37 pretty printing is injective, but two different texts might have the same meaning 02/12 02:37 Parsing is the non-injective one. 02/12 02:37 it's parsing that's not injective 02/12 02:37 Even whitespace ruins it. 02/12 02:38 well I was thinking that you can lex whitespace away 02/12 02:38 I guess the real problem is:  Pretty printer isn't a specification 02/12 02:39 it's just one data point 02/12 02:39 haskell-src-exts keeps the extra text around to get pp . parse = id 02/12 02:39 Darn, I somehow managed to forget to ask whether the Agda typechecker is entirely in Haskell or no. 02/12 02:40 it is 02/12 02:41 all of agda is 02/12 02:41 Is haskell-src-exts more of a concrete syntax tree, then? 02/12 02:41 Is the Emacs plugin entirely in Haskell? 02/12 02:42 The emacs plugin is presumably in elisp. 02/12 02:42 * uorygl nods. 02/12 02:43 I guess I'll be interested in the Haskell source of Agda at some point. 02/12 02:43 Communicating with some sort of agda checker in a spawned process. 02/12 02:43 it just keeps ghci running the background 02/12 02:47 mh, it seems most of the over 1.4gig of memory used by the typechecker are made of : 02/12 02:49 anyone know some texts which go into detail about proving parsers correct? even if it's not formal computers stuff 02/12 02:50 quantumEd: how does your AST look like, btw? 02/12 02:51 data Lambda : Nat -> Set where 02/12 02:51 Free : forall {n} -> Nat -> Lambda n 02/12 02:51 Var : forall {n} -> Fin n -> Lambda n 02/12 02:51 App : forall {n} -> Lambda n -> Lambda n -> Lambda n 02/12 02:51 Lam : forall {n} -> Lambda (S n) -> Lambda n 02/12 02:51 (Var is 'Bound' like in I am not a number I am a free variable) 02/12 02:51 i see, so you're going to extend that with the other constructs later, or you're going to translate them to that? for OTT i mean 02/12 02:53 You know, you could actually parameterize by 'n' instead of indexing. 02/12 02:53 Since it's just a nested type. 02/12 02:53 And save yourself all the "forall {n}"s. 02/12 02:54 this is just a test 02/12 02:55 dolio, oh right, since I used Lambda (S n) and that wouldn't be allowed to be a parameter in Coq 02/12 02:55 which is what I am used to 02/12 02:55 why wouldn't it be? 02/12 02:56 Is that still true? I thought they added non-regular parameterized types. 02/12 02:56 I thought roconnor mentioned something about it, at least. 02/12 02:56 Saizan but it is the same approach to do the full thing, just a bit more tricky 02/12 03:00 (which is why I start with this) 02/12 03:00 copumpkin: It's just a restriction on datatypes in Coq. I'm not sure if there was ever a good reason for it. 02/12 03:02 strange :) 02/12 03:03 there is a good reason for it 02/12 03:03 are there any extensional proof systems? 02/12 03:04 NuPRL? 02/12 03:04 NuPRL is pretty close to Martin-Loef's extensional type theory, I think. 02/12 03:06 I see 02/12 03:06 Of course, I've not investigated either very closely. 02/12 03:14 But I think the former was modeled on the latter. 02/12 03:14 * uorygl ponders Wikipedia's non-constructive proof that there are two irrational numbers a and b such that a^b is rational. 02/12 05:06 Suppose there are no such numbers. Then sqrt(2)^sqrt(2) must be irrational. Then (sqrt(2)^sqrt(2))^sqrt(2) = 2 must be irrational. This is a contradiction. 02/12 05:06 Specifically, either sqrt(2)^sqrt(2) is irrational and therefore the a we want, or it's rational and therefore the a^b we want. 02/12 05:07 So it's going from "whether [sqrt(2)^sqrt(2) is rational] is true or false, we have an answer" to the answer. 02/12 05:09 And that's something you can't do in Agda, can you. 02/12 05:10 You might be able to use that to prove that Not (Not (there are irrational a and b such that a^b is rational)). 02/12 05:12 But no, that proof is obviously not constructive, because a constructive proof of the original statement would contain the a and b. 02/12 05:13 Now, can you use Peirce's law, ((a -> b) -> a) -> a, to express this proof? 02/12 05:14 I hope so; it would alleviate my slight confusion. 02/12 05:14 (Where "slight confusion" is defined as the type of confusion that you do not attempt to alleviate unless you're the person suffering it.) 02/12 05:15 Peirce's law lets you eliminate double negation, so if you can prove the double-negated theorem, you can prove the theorem with Peirce's law. 02/12 05:22 I don't know how easy it'd even be to state the theorem in Agda, though. 02/12 05:22 You'd have to come up with a representation of real numbers, and proofs of rationality and irrationality. 02/12 05:23 Couldn't you just postulate those? 02/12 05:27 Which parts? 02/12 05:31 I mean, you also need that sqrt 2 * sqrt 2 = 2, and (sqrt 2)^2 = 2, and (a^b)^c = a^(b*c). 02/12 05:31 And that 2 is rational. 02/12 05:31 I guess you'd only end up postulating the theorem itself... 02/12 05:32 Yeah, other than some of the logical structure. 02/12 05:32 Well, suppose we have all the number stuff down. How do you represent the proof, even in English, using Peirce's law? 02/12 05:34 http://en.wikipedia.org/wiki/Construction_of_the_real_numbers 02/12 05:34 * uorygl ponders how to do that. 02/12 06:02 * uorygl ponders how to prove "X is either true or false" using Peirce's law. 02/12 06:02 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=13489#a13489 02/12 06:11 -!- opdolio is now known as dolio 02/12 06:12 dolio: what is Dec? 02/12 06:23 It's basically a sum. But Dec P is intended to be the result of a decision procedure for some proposition P. 02/12 06:24 The law of the excluded middle decides all propositions, essentially. 02/12 06:24 What's the type of \neg? 02/12 06:24 Set -> Set1 02/12 06:25 * uorygl cowers at the mention of Set1. 02/12 06:25 Dec P = P \/ \neg P, roughly. 02/12 06:25 oh wait 02/12 06:25 it isn't Set1 02/12 06:25 it's just Set -> Set 02/12 06:25 or Set a -> Set a now probably 02/12 06:25 Yeah. \neg P = P -> \bot 02/12 06:25 http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#327 02/12 06:26 both of them in there 02/12 06:26 So the constructors of Dec are no and yes? 02/12 06:29 -!- kmc__ is now known as kmc 02/12 06:29 yep 02/12 06:29 yes carries a proof of yes-ness and no carries a proof of not-yesness 02/12 06:30 In the definition of lem, what are P and Q? 02/12 06:30 P for peirce is Dec P for the P from lem. 02/12 06:32 Q is \bot, I think. 02/12 06:33 Q is anything, including \bot 02/12 06:35 Yeah, but when I'm using peirce to prove lem, it's \bot. 02/12 06:35 Since if you can prove P -> \bot, you can prove P -> Q, for all Q 02/12 06:35 hm 02/12 06:36 This is kind of intriguing. 02/12 06:37 Okay. This means that callCC behaves in a really fun manner when it comes to laziness and data constructors. 02/12 06:39 It can return the value "no, because--er, actually, yes!" 02/12 06:39 Right. 02/12 06:39 (Homework problem: Find the value of because--er,.) 02/12 06:40 It returns no at first, but if you prove the proposition in question, and hand it to the 'no', it jumps back to when it gave you the answer and gives you the proof you constructed instead. 02/12 06:40 That sounds like a pain in the mud. 02/12 06:41 And if it's impossible to prove the proposition, then it made the right choice. 02/12 06:42 What a brave function it is. 02/12 06:42 Yeah, classical logic is crazy. :) 02/12 06:44 So taken literally, callCC leads to a program that can output the wrong thing. 02/12 06:46 That's almost a behavior that I want. 02/12 06:46 What do you mean the wrong thing? 02/12 06:46 lem is going to return "no" at some point no matter what. If all I do is look at that and print "It's false!", I'll end up with the wrong behavior. 02/12 06:47 Yes, that's true. 02/12 06:48 Although, not in Agda, since peirce is a postulate, it probably won't be subject to any normalization. 02/12 06:48 So if you ran the program, you'd probably just get stuck at some point. 02/12 06:49 Right, Agda won't actually do that. 02/12 06:49 * uorygl ponders whether he actually wants a version of Agda that will do that. 02/12 06:49 call/cc isn't really 'pure'. 02/12 06:50 It behaves differently under different evaluation orders and such. 02/12 06:51 For some reason, I wasn't expecting it to be *that* impure. 02/12 06:55 Perhaps I wasn't thinking about escaping continuations; it never "returns the wrong thing" if the continuation never escapes and the interior is evaluated strictly enough. 02/12 06:55 Well, if you think of something like "[a, b, callcc f]"... 02/12 06:56 Where does it jump back to? 02/12 06:56 Does it jump back to when you eventually do case analysis on the "callcc f" stored in the list, or does it jump back to when the list was built? 02/12 06:56 Which could make a difference, I think. I don't have any good concrete examples. 02/12 06:57 It even distinguishes call-by-need (lazy) from call-by-name (lazy - sharing) I think. 02/12 06:58 The difference is that if it's the latter, you go "Darn!", while if it's the former, you go "Darn." 02/12 06:58 I'm sure oleg has examples, but I'm not really sure what to search for. 02/12 07:03 Ask Oleg if he has an implementation of ZFC or some equivalent postulating only Peirce's law. 02/12 07:04 People have modeled ZFC in Coq, I think. 02/12 07:04 Unfortunately, Coq isn't Agda. 02/12 07:05 Is there a fundamental difference to what's expressible in them? 02/12 07:06 Probably not. 02/12 07:06 Coq has some impredicativity, but that's about it. 02/12 07:06 Of course, Agda has induction-recursion, which Coq doesn't. 02/12 07:07 Both of them have modus ponens. Both of them effectively allow axiom schemas. I think that's all you need. 02/12 07:11 Apparently impredicativity helps with power sets, though. 02/12 07:12 I don't really understand how, though. 02/12 07:12 What is impredicativity? 02/12 07:12 Set in Set 02/12 07:12 It's not that. 02/12 07:12 No? 02/12 07:12 I'm afraid I'm not quite sure what it is myself... 02/12 07:14 Impredicativity is where you can quantify over universes that include the thing you're defining. 02/12 07:14 So, Set : Set1 may be a rule, but, for instance, if U : Set, then (T : Set) -> U : Set, instead of Set1. 02/12 07:15 Or, for T : whatever, really. 02/12 07:15 You could have (T : Set85) -> U be in Set, as long as U : Set in that context. 02/12 07:16 Coq has it off by default for Set now, actually, since it causes problems with some classical postulates. 02/12 07:17 Like law of the excluded middle, I think. 02/12 07:17 But Prop is still impredicative. 02/12 07:19 Did that get through? 02/12 07:20 which ? 02/12 07:27 But Prop is still impredicative. 02/12 07:27 -!- Berengal [n=berengal@98.85-200-142.bkkb.no] has quit [Remote closed the connection] 02/12 07:27 -!- Berengal [n=berengal@98.85-200-142.bkkb.no] has joined #agda 02/12 07:27 Did that get through? 02/12 07:27 I know my messages got through. I was wondering if Berengal got them since he got knocked off. 02/12 07:28 .. oh 02/12 07:28 I got that 02/12 07:29 Okay. 02/12 07:29 uorygl : in (classical) linear logic, you have to use every proof, so there you can't avoid using the "no" returned by lem' 02/12 07:29 So it's a bit like recursion in the propositions? 02/12 07:29 If you know pure type systems, then impredicativity is having rules like (s,t,t) instead of (s,t,max s t). 02/12 07:29 But you still have Set i : Set (i + 1). 02/12 07:30 And impredicativity at the lowest universe level can still be proved strongly normalizing for theories like Coq, whereas Set : Set admits paradoxes (as does impredicativity at higher levels). 02/12 07:31 You have to be careful about inductive/sigma types, too. 02/12 07:33 Right 02/12 07:33 I basically just discovered turing-completeness isn't all it's cracked up to be. Still wondering how far down the rabit-hole of totality and strongly normalizing languages I can go before my head explodes 02/12 07:34 i thought impredicativity was like if you have P : Set -> Set' and F : (A : Set) -> P A', then ((A : Set) -> P A) : Set', so you can form F ((A : Set) -> P A) : P ((A : Set) -> P A)' 02/12 07:35 (in Haskell terms, if we have id :: forall a. a -> a', then we can instantiate the a' to e.g. forall a. a -> a' so we get id :: (forall a. a -> a) -> (forall a. a -> a)') 02/12 07:36 Yes, that will work in a pure type system with impredicative rules. 02/12 07:36 (but i may not have the full picture ..) 02/12 07:36 So 'id' is a proof of itself? 02/12 07:36 no 02/12 07:37 GHC lies about being impredicative, though. It'll tell you that forall a. a -> a has kind *, but you can't use it like a * in all situations. 02/12 07:37 Like, you can't use it with Maybe :: * -> * 02/12 07:38 So it's not really a *. 02/12 07:38 ** 02/12 07:38 (i should probably have said : if we have P :: * -> *' and f : forall (a :: *). P a', (and then (forall (a :: *). P a) :: *'), then we can instantiate the a' to e.g. forall (a :: *). P a' so we get f :: P (forall (a :: *). P a)') 02/12 07:39 (the second one is an asterisk with small print at the bottom of the page, saying "not really") 02/12 07:39 Unless you turn on -XImpredicativeInstantiation, in which case it really is *. 02/12 07:39 Or whatever the flag is called. 02/12 07:39 *nod*, the mono-type / poly-type distinction 02/12 07:39 the point being that we can instantiate the variable bound by a universal with universally quantified types, including the original universally quantified type, itself 02/12 07:41 Yes, that's what it buys you, ultimately. 02/12 07:42 Which is handy, because then you can define Nat = forall (r :: *). (r -> r) -> r -> r, and do recursion with Nat as a result. 02/12 07:42 (while a predicate system would probably either : disallow instantiate universally quantified variables with universally quantified types ; or instroduct some kind of stratification so that you can't instantiate the variable with the origianl universally quantified type, at least) 02/12 07:42 Although that kind of encoding isn't very good for doing proofs. 02/12 07:42 (s/instroduct/introduce/) 02/12 07:43 Some folks in mathematics distrust the sort of circularity that impredicativity introduces, and try to avoid it. 02/12 07:45 Weyl 02/12 07:45 Which, I think Russel was one, with his hierarchy of types. 02/12 07:45 (and folks in predicative arithmetic, who don't believe in induction :) 02/12 07:45 I guess once you have a paradox based on circularity named after you, you have good reason to mistrust it. 02/12 07:46 Lots of definitions have some sort of impredicative circularity that doesn't seem vicious, though. 02/12 07:49 I think "the tallest person in the room" is an example on Stanford's online philosophy encyclopedia's article. 02/12 07:49 hm, NF uses stratification 02/12 07:49 .. but it doesn't appear to be predicate, anyway, according to WP 02/12 07:51 s/predicate/predicative/ 02/12 07:51 (though NBG is claimed to be predicative .. i suppose it's set' and class' are the only two stratification levels there) 02/12 07:53 Well, the other issue is that I don't think there's any firm definition of "predicative", so it may be used in different ways in different places. 02/12 07:54 Oh, it says the class comprehension schema is predicative. 02/12 07:59 So you can only quantify over sets in the schema. 02/12 07:59 Berengal: what's Turing-completeness cracked up to be? 02/12 08:05 Does Set : Set really admit paradoxes? 02/12 08:06 The prerequisite for a language being useful? 02/12 08:06 Yes. 02/12 08:06 It's a more complicated paradox than Russel's, though. 02/12 08:07 What's the paradox? 02/12 08:07 http://code.haskell.org/Agda/test/succeed/Hurkens.agda 02/12 08:08 Girard's paradox ? 02/12 08:08 Yes. 02/12 08:08 I think Girard's paradox was initially developed for impredicativity on the non-lowest level, but Set : Set lets you write the same terms. 02/12 08:10 * uorygl ponders Hurkens.agda. 02/12 15:59 My, this is abstract. 02/12 16:06 I notice that this has lambdas in places that would not be syntactically valid in Haskell. 02/12 16:06 -!- RichardO_ is now known as RichardO 02/12 16:11 I'm trying to prove that 100000 + 0 == 0. This is proving hard... 02/12 16:43 start with the easier problem of proving 1 = 0 02/12 16:44 I meant 100000 + 0 == 100000... 02/12 16:45 Since I've proven that n + 0 == n, I hoped it would just unify, but it seems it wants to reduce... 02/12 16:46 Is there a way to do this? 02/12 16:48 if have got    zero_right_identity : forall n -> n + 0 == n,  then  zero_right_identity 100000 : 100000 + 0 == 100000 02/12 16:49 Right, but ghci still overflows the stack 02/12 16:50 When typechecking 02/12 16:51 * uorygl tries to get his hands on a copy of Hurkens' paper about Girard's paradox. 02/12 18:02 what's a good paper with lots of theory regarding de bruijn variables? 02/12 18:22 * uorygl continues pondering Hurkens.agda. 02/12 18:28 I feel like it would help if these types were written using "data" instead of as equations. 02/12 18:32 Can I ask the IDE what the type of a variable is? 02/12 18:35 with a conveniently placed hole, you can sort of do that 02/12 18:36 * uorygl notes: C-u C-x = 02/12 18:41 I'm guessing that "loop" is not a misnomer, and that expression actually loops. 02/12 18:47 -!- RichardO_ is now known as RichardO 02/12 18:59 Does agda normalize all terms before deciding they're equal? 02/12 20:23 Yes. 02/12 20:23 But in theory it doesn't have to, right? 02/12 20:24 In theory it could search for some series of beta/eta conversions between the two terms. 02/12 20:25 How about simple syntactic equality? 02/12 20:25 Well, then, "(\x -> x) 5" wouldn't be equal to "5". 02/12 20:26 Until you used some other tactic that reduced it to "5" 02/12 20:26 The equality in typing rules is equality up to beta-eta conversion. 02/12 20:27 And the easiest way to decide that is to normalize both sides and check for syntactic equality. 02/12 20:28 It means we can't prove 100000 equals 100000 though... 02/12 20:28 alpha-beta-eta, I guess. 02/12 20:28 Naturals? 02/12 20:28 Yeah 02/12 20:28 Have you declared them built-in? 02/12 20:29 Yep 02/12 20:29 Huh. 02/12 20:29 This is about 100000 + 0 = 100000, right? 02/12 20:30 Right now, just 100000 == 100000 02/12 20:31 Is _+_ built-in? 02/12 20:31 I'm not using _+_ 02/12 20:31 Oh, right. 02/12 20:31 :) 02/12 20:31 Yeah, I'm trying it now, and I don't understand what its problem would be. 02/12 20:32 And _==_ is defined as _==_ {A : Set}(x : A) : A -> Set where refl : x == x 02/12 20:32 I'd expect normalizing 100000 once it's BUILTIN to be trivial. 02/12 20:33 it's not using anything more clever than peano representation internally afaik 02/12 20:34 the BUILTIN maybe affects only compiled programs? 02/12 20:34 I thought it got backed with GMP once you used the BUILTIN pragma. 02/12 20:34 As I've understood it, builtin naturals just provide syntax... 02/12 20:34 (aside from literals) 02/12 20:34 yes, I also thought it's purely syntactic 02/12 20:34 I wasn't aware that Agda uses GMP for anything 02/12 20:35 It used to 02/12 20:35 For instance, if you tell it to normalize 5000 * 5000, it finishes immediately. 02/12 20:35 With C-c C-n. 02/12 20:35 But I think they ripped it out in Agda2... 02/12 20:35 And I just wrote a factorial function and it computed 1000! 02/12 20:37 So it's using GMP somewhere. 02/12 20:37 Perhaps just not during type checking. 02/12 20:37 What's the builtin for _*_ called? 02/12 20:38 NATTIMES, I think. 02/12 20:38 Or, probably not GMP directly, but Haskell Integers. 02/12 20:38 My emacs stalled on 5000 * 5000 02/12 20:38 And once I declared it builtin, it works 02/12 20:39 Yes, that's not particularly surprising. 02/12 20:40 No, not really. I guess the typechecker doesn't know about that though 02/12 20:40 Maybe it can't use the efficient backing because it has to handle neutral terms and stuff. 02/12 20:42 not a good excuse 02/12 20:42 :) 02/12 20:42 No, but it might be the reason. :) 02/12 20:42 yeah 02/12 20:42 only reason I can think of 02/12 20:42 Still, I'd be nice if when there's a proof that two terms are equal, it should be able to use whichever of them interchangably, even if they're not identical, without having to normalize them 02/12 20:45 We can't just build everything into the language... 02/12 20:46 you want things that you prove to be equal to be considered equal *automatically*? 02/12 20:47 Yes 02/12 20:47 That leads to pitfalls. 02/12 20:48 If I've already proved that n + 0 == n, I shouldn't have to prove that 100000 + 0 == 100000 02/12 20:48 It does 02/12 20:48 Well, if you've proved that n + 0 = n, then you should be able to use that proof for n = 100000. 02/12 20:49 Yes, but I'm not, because ghci blows the stack 02/12 20:50 But you have to use a substitution function, it won't just happen. 02/12 20:50 Berengal: what you want is, I think, called a type system with extensional equality, and that's known to be undecidable 02/12 20:51 Ah. I've got a couple of papers on that I was just about to read 02/12 20:52 Is it possible to regain decideability with some restrictions though? 02/12 20:53 but I completely agree with you that I think none of the current languages is at a "sweet spot" with respect to handling of equality 02/12 20:53 Because even a restricted version of that would be useful 02/12 20:53 yeah, it would 02/12 20:53 I think one should be able to "program" the standard tactic being used to check equality 02/12 20:54 rather than always just getting beta-eta 02/12 20:54 Humans standing in for the undecideable parts? 02/12 20:54 Observational Type Theory has extensional equality that is still decidable, but that's because one still applies equalities using coercions. 02/12 20:54 well, it's clear that it can't just automatically work in general 02/12 20:55 but for many concrete situations, it works 02/12 20:55 just as an example, for natural numbers one could build in lots of extra rules without making the type system undecidable 02/12 20:55 Yeah. I'm thinking about Haskell's rank-n-types, which make type inference undecideable, but still works in haskell because it requires human intervention in the uncommon cases 02/12 20:56 i.e. n > 1 02/12 20:56 of course, one does not want to hack these things directly into the compiler (although, for natural numbers, one even might argue that it'd be useful), but if you'd just allow the user to specify extra tactics to apply 02/12 20:56 similar to Coq's options to extend the auto tactic 02/12 20:57 Indeed, it'd be nice to have 02/12 20:57 It seems as though the normalizer handles expressions with postulated naturals all right. 02/12 21:03 x + fact 100 gets normalized right away to x + . 02/12 21:04 Only something like "100 + x" takes a really long time, since it normalizes to "suc (suc (... x))". 02/12 21:04 So I'm not sure why the normalization during type checking couldn't do similarly. 02/12 21:05 it surely can typecheck "foo | 100000 + 0 | n+0==0 100000; ... | .100000 | refl = " ? 02/12 21:07 Hey, it worked 02/12 21:09 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=5240#a5240 02/12 21:10 Though I'm not sure if it's because of builtin naturals or not... 02/12 21:11 * Berengal turns them off 02/12 21:11 Yup, it's the builtin _+_ that makes it work... 02/12 21:12 -!- mak__ is now known as comak 02/12 22:22 --- Day changed Thu Dec 03 2009 * uorygl ponders a realization of Set : Set in ZFC. 03/12 01:26 Naturally, if you want Set : Set in ZFC, you can't represent each Set simply as the set of all values of that type. 03/12 01:27 Hmm! It's possible to embed arbitrary values inside Set, isn't it. 03/12 01:28 Set : Set would be like having a set of all sets in ZFC, which leads to Russel's paradox. 03/12 01:30 : doesn't necessarily follow all the axioms that \in follows. 03/12 01:31 Set : Set in type theory has the same kind of problem as set of all sets in set theory 03/12 01:31 (or maybe ordinal of all ordinals) 03/12 01:31 But suppose we have a type Arb which is a proper class, containing so many values that no set can contain all of them. 03/12 01:32 : is less relaxed than \in, yes. Which makes the associated paradox more complicated, I guess. 03/12 01:32 And we come out with some constructor of type Arb -> Set, embedding Arb in Set; this shows that Set is also a proper class. 03/12 01:32 Russel's paradox is much simpler than Girard's. 03/12 01:32 And, uh... 03/12 01:33 yeah you can't have judgements like ~(Set : Set) 03/12 01:34 uorygl: How would you make an Arb? 03/12 01:34 the type, I mean, not its elements 03/12 01:34 Say it's a primitive in this hypothetical language. 03/12 01:35 And there's a function turning any value into an Arb. 03/12 01:35 Alternatively, does this work: data Arb : SetOrWhatever where arb : (S : SetOrWhatever) -> S -> Arb 03/12 01:35 For some SetOrWhatever. 03/12 01:35 Hmm, I just realized that I don't think I have a good definition of a function. 03/12 01:38 Defining a function as a set of ordered pairs doesn't work if the function is capable of taking itself. 03/12 01:38 self applicable functions don't exist in ZFC 03/12 01:41 a function is just any program the typing rules give an arrow type 03/12 01:41 quantumEd: Well, not just that, but a straight forward translation of Russel's paradox to type theory would lead one to attempt to construct a type T such that t : T implies that it is not the case that t : t. But that last part isn't well-defined. 03/12 01:41 but I'm not sure any of them take themselves 03/12 01:41 certainly they don't in, say, ML 03/12 01:41 dolio yeah that's what I mean, you can't talk about (:) as a relatioh 03/12 01:41 relation* 03/12 01:42 How about (a : Set) -> a -> a? 03/12 01:42 Can that take itself? 03/12 01:42 Whereas in a set theory like ZFC, everything is a single 'type' V, and \in is a relation from V to V. 03/12 01:42 Or is (a : Set) -> a -> a itself not a Set? 03/12 01:43 no, it's a Set1 03/12 01:43 so it can't, I think 03/12 01:44 with impredicativity or Set : Set it is 03/12 01:44 It would be a Set if Set were impredicative. 03/12 01:44 (a : Set l) -> a -> a 03/12 01:44 good point! so impredicativity at that level lets one construct functions which take themselves as arguments, I never noticed that 03/12 01:45 it's interesting, since "show no well typed function can take itself as an argument" is a standard exercise in intro functional programming courses 03/12 01:45 Obviously, lambda calculus provides a definition of "function" by which a function can take itself. 03/12 01:45 sure, but not STLC 03/12 01:46 ccasin: I don't understand the exercise 03/12 01:46 That depends a lot on what your definition of "well-typed" is. 03/12 01:46 Indeed. 03/12 01:46 ccasin: oh in STCL ok.. 03/12 01:46 can we write \x -> x x with universe polymorphism? 03/12 01:46 quantumEd: yeah, I should have been clearer.  I'm thinking ML or Haskell here 03/12 01:46 ccasin: in Hakell you can do   id x = x  and  id id  works though ? 03/12 01:47 only with language extensions, I suspect 03/12 01:47 I don't think you need any extensions for that 03/12 01:47 well, depends, are you passing it a polymorpic or monomorphic id there? 03/12 01:47 Prelude> let id x = x 03/12 01:47 Prelude> :t id id 03/12 01:47 id id :: t -> t 03/12 01:47 yeah 03/12 01:48 that's hiding an explicit instantiation of the id argument to some type 03/12 01:48 that's interesting.  I mean, what type is it picking for the second id? 03/12 01:48 yes 03/12 01:48 for the second id t -> t 03/12 01:48 what is "t" there? 03/12 01:48 for the first one (t -> t) -> (t -> t) 03/12 01:48 what do you mean 03/12 01:48 can one ever apply (id id)?  I think no 03/12 01:48 this is haskell 03/12 01:48 You could even have a type system with equirecursive types, and type \x -> x x as something like (t ~ t -> t) => t -> t. 03/12 01:48 you should know what t is :P 03/12 01:48 yes in Ocaml -rectypes too 03/12 01:49 t is a variable bound by an implicit "forall t." around the entire type. 03/12 01:49 id id :: forall t. t -> t 03/12 01:49 well, that is very strange, if true 03/12 01:49 I don't know why "forall t." matters 03/12 01:49 It's not important 03/12 01:49 e = id id ~~ e = /\ t -> id (t -> t) (id t) 03/12 01:49 since, as Saizan_ pointed out, the second id needs to be not polymorphic 03/12 01:49 You know, I never knew the mundane aspects of Haskell were so weird. 03/12 01:50 which is not e = id (forall t. t -> t) id 03/12 01:50 Yeah, writing it Church style makes it a bit clearer. 03/12 01:50 anyway I have shown that the excersice was wrong 03/12 01:50 I see.  In SML, this should hit the value restriction, right? 03/12 01:51 from the pov of haskell it's quite ambiguous as an exercise 03/12 01:51 yeah, I'm really thinking STLC 03/12 01:51 "intro functional programming" was a mistake 03/12 01:51 ccasin I think so 03/12 01:51 Here, let's extend ZFC with functions. 03/12 01:52 btw 03/12 01:52 id id is polymorphic 03/12 01:52 Prelude> (id id) 3 03/12 01:52 3 03/12 01:52 Prelude> (id id) "foo" 03/12 01:52 "foo" 03/12 01:52 quantumEd: yes, I see 03/12 01:53 There is now a ternary relation _$_#_, and for all a, b, c and d, if a$ b # c and a $b # d, then c = d. 03/12 01:53 strictly speaking that doesn't tell us that it's polymorphic, however if you use let then the implicit generalization gives you a polymorphic type 03/12 01:54 well types dont' really matter 03/12 01:54 you can just see that it is polymorphic because I used it on values of different type 03/12 01:54 Also, there exist the combinator functions S and K and a bunch of other stuff. 03/12 01:54 Prelude> let foo = id id in (foo 3, foo "foo") 03/12 01:55 oops 03/12 01:55 well, it worked 03/12 01:55 quantumEd: so you'd call (\x -> x) polymorphic in STLC? 03/12 01:55 though my copy paste skills need work 03/12 01:55 no 03/12 01:55 but that can be used on values of different types too 03/12 01:56 saizan_, how do you mean? 03/12 01:56 haskell is untyped script language, STLC has curry howard and all this stuff -- they are very different 03/12 01:56 well, I guess I see, but you couldn't wrote the program I just pasted in stlc 03/12 01:57 ccasin: it was unrelated to that 03/12 01:57 quantumEd: untyped because of let x = x in x ? 03/12 01:59 btw, even in STLC the exercise would be weird, unless you specify the use of church-style terms (maybe that's the norm though?) 03/12 02:04 Saizan: yes, definitely (at least in the US) 03/12 02:07 I'd stick with Church-style with STLC. 03/12 02:08 though I'll give that I grossly overstated the scope of the exercise :) 03/12 02:08 dolio: interesting. do you remember what book you first learned it from? 03/12 02:09 I'm not sure I learned from a book. 03/12 02:09 But (\x -> x) is ambiguous in STLC. 03/12 02:10 yes 03/12 02:10 At least if you have a H-M-like system there's a "best" type for it. 03/12 02:10 yes, I was just curious because most of the resources I've used have a preference for church style, there's always an annotation 03/12 02:11 why is it ambiguous? 03/12 02:11 it's just a lambda term, it's not a STLC term 03/12 02:11 its type is ambiguous 03/12 02:11 it could be any identity function 03/12 02:11 it doesn't have a type 03/12 02:11 entirely unrelated question: are there any two Sets that agda can prove unequal? 03/12 02:12 ccasin, is P A and ~P B then A <> B 03/12 02:13 so can you find such a P, for say, A = unit and B = bool? 03/12 02:13 s/is/if/ 03/12 02:13 well, a good P would be "has just one element" 03/12 02:14 I suppose that works 03/12 02:14 let me try it out 03/12 02:16 oh no, peer reversed dolio's arrows 03/12 02:16 uhm, learning from wikipedia gave me a weird notion of STLC :) or maybe it's the early exposure to HM 03/12 02:18 * copumpkin gets all his information from wikipedia! you mean it's not 100% accurate??? 03/12 02:19 HM kind of makes the schemas of types you can give to Curry-style STLC terms into real types. 03/12 02:19 quantumEd: that worked, thanks! I guess I was being silly 03/12 02:33 agda types are just to hard to get a handle on 03/12 02:33 don't think so 03/12 02:33 in particular say you hae bool and bool' both with two elements, you can't prove them equal or apart 03/12 02:34 quantumEd: true, but it's very nice to know we can prove some distinctions, and I should have seen how! 03/12 02:34 -!- opdolio is now known as dolio 03/12 02:39 ccasin: what did you choose as P? 03/12 02:48 Saizan: (s : Set) -> (A B : s) -> A = B 03/12 03:16 hey ccasin, are you back in Philly yet? 03/12 03:24 byorgey: yes, see you tomorrow! 03/12 03:43 http://old.nabble.com/Re%3A-Implicit-newtype-unwrapping-p26620156.html 03/12 07:09 eh ?? 03/12 07:09 heh, people have a misconception of dependent types 03/12 07:11 people who don't understand dependent types think "If only we had dependent types, everything would be so easy!" 03/12 07:13 yeah! 03/12 07:13 I must admit that's what I thought too :P 03/12 07:13 "zomg dependent types can save us from array out of bounds errors!" 03/12 07:14 "oh, we need to prove our index fits in the array? boo" 03/12 07:14 this seems to be advocating some sort of subtyping 03/12 07:14 maybe he was thinking about coercions (like the stuff Luo is doing) 03/12 07:15 Maybe he meant Ada. 03/12 07:18 -!- ski__ is now known as ski_ 03/12 12:49 -!- RichardO_ is now known as RichardO 03/12 14:52 -!- RichardO_ is now known as RichardO 03/12 15:38 -!- RichardO_ is now known as RichardO 03/12 18:42 is it normal for data and codata to both live in Set? 03/12 21:34 As normal as it is for a language to have codata at all. 03/12 21:51 --- Day changed Fri Dec 04 2009 Can I have a hint as to how to prove that Vec A (n + 0) == Vec A n? 04/12 06:04 Preferably without recursing on the vector, instead employing the proof that n + 0 == n 04/12 06:05 with a subst 04/12 06:05 P = Vec A 04/12 06:05 in the right universes 04/12 06:05 Berengal: so you already have the n + 0 == n proof? 04/12 06:06 copumpkin: yup 04/12 06:06 subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p 04/12 06:07 damn, more indirection :P 04/12 06:07 Berengal: did it work? 04/12 06:09 copumpkin: I'm not using the standard library, so I'm busy copy-pasting :P 04/12 06:10 oh ok :) 04/12 06:10 it's really simple to write 04/12 06:10 Yeah, but the definition of subst spans line a bajillion files, each containing one line... 04/12 06:11 hm? 04/12 06:12 oh you mean all the crazy indirection in the standard library 04/12 06:12 skip that :) 04/12 06:12 you can have one line for the type and one line for the def 04/12 06:12 it's basically x == y -> P x -> P y 04/12 06:13 http://snapplr.com/taks 04/12 06:15 you'd want it for any level 04/12 06:15 http://snapplr.com/9f2s 04/12 06:17 something like that, anyway 04/12 06:17 damn, typechecking Data.Rational takes more than 1.8GB of ram, using a 64bit ghc wasn't a good idea afterall 04/12 06:21 it's painful even with 32bit 04/12 06:21 I remember when I wrote some basic arithmetic for rationals it took forever to normalize even a simple expression 04/12 06:21 it wasn't that painful with agda-2.2.4 though 04/12 06:22 we lost him! 04/12 06:24 oh wait, not really 04/12 06:24 that was my evil twin 04/12 06:24 -!- Saizan_ is now known as Saizan 04/12 06:24 phew! 04/12 06:25 Berengal: what are you working on? or just playing around? 04/12 06:27 Just playing around 04/12 06:28 Trying to implement revappend 04/12 06:28 what does that do? 04/12 06:28 appends the reverse? 04/12 06:28 flip (:) 04/12 06:28 So I can foldl it 04/12 06:28 oh 04/12 06:28 like snoc? 04/12 06:28 snoc traverses the list though, doesn't it? 04/12 06:29 well, it's just a general notion of sticking an element onto the end of something 04/12 06:30 Well, foldl (flip (:)) [] just repeatedly takes an element in front of one list and conses it onto the other, until the list is empty 04/12 06:31 oh, so you want reverse 04/12 06:31 Eventually 04/12 06:31 I see 04/12 06:31 Seems I got it not, thanks :) 04/12 06:34 now* 04/12 06:34 yay! 04/12 06:36 you should name your subst moo btw 04/12 06:36 all the cool kids are doing it 04/12 06:36 Berengal: have you come across the two other handy functions? cong and sym? 04/12 06:37 adn trans, and the equational reasoning pretty syntax 04/12 06:40 mmm 04/12 06:40 the "begin term \==\< proof \> ... \qed" one 04/12 06:41 copumpkin: Yup 04/12 06:43 Saizan: That too. Stole it from Ulf's thesis 04/12 06:43 Except I switch to a hand-writing-ish font and use letters instead of symbols... 04/12 06:45 http://forums.xkcd.com/download/file.php?id=19682 04/12 06:46 is the only difference between writing f and f_ for a function name that you can set the precedence of the second one? 04/12 06:46 it seems so 04/12 06:47 i can check (using agda-executable) the whole stdlib using less than 700mb, there's something weird going on 04/12 06:51 that number is for Agda-2.2.4 04/12 06:51 (while for 2.2.5 i bump into the OOM killer) 04/12 06:51 the calls for papers on the agda mailing list are a little annoying 04/12 08:21 What kind of cutting edge functional programming language mailing list doesn't have calls for papers? 04/12 08:25 the most recent one seems to be an everything conference 04/12 08:28 -!- whoppix_ is now known as whoppix 04/12 17:32 am i missing something here on this agda setup? i did a cabal install Agda-executable -p', then agda-mode setup. then i load a test.agda file and type A :: Type = Set' which does drop me into "Adga" mode, but not "Agda:run". hitting C-c C-l then results in a parse error. 04/12 18:22 that isn't valid syntax 04/12 18:25 you use a single colon for types, and you can't unify the type and the value setting that way 04/12 18:26 oops. ok, got a working example now. at least, i think its working 04/12 18:31 boyscared was that Agda 1 notation? 04/12 18:40 probably, got it from here: http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda/agdainstallationFromBinaries.html 04/12 18:41 hm 04/12 18:42 so I already asked this but.. whats a good ref for de bruijn syntax? 04/12 20:43 how do you state correctness of substitution? 04/12 20:52 -!- copumpkin is now known as TheHunter 04/12 23:13 -!- TheHunter is now known as copumpkin 04/12 23:13 --- Day changed Sat Dec 05 2009 --- Day changed Sun Dec 06 2009 that fplunch STLC thing STILL hasn't updated 06/12 01:58 Updated? 06/12 02:02 hoping for the author to reply to the comments but he doesn't seem to be aware they are there, or just doesn't want to 06/12 02:03 He replied once, it looks like. 06/12 02:07 That blog seems to have a lot of authors. Maybe they don't get notifications. 06/12 02:09 I must say, that program gives very nice looking output. 06/12 02:43 * Saizan wants an unverse-polymorphic Vec 06/12 09:50 edit the file! 06/12 09:51 it's usually pretty mindless editing 06/12 09:51 uhm, i get a weird error in the definition of splitAt 06/12 10:00 hm 06/12 10:00 ? 06/12 10:00 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=13667#a13667 06/12 10:03 doesn't it need to be universe polymorphic? 06/12 10:04 I guess it shouldn't have to be 06/12 10:04 the error stays the same if i add the indexes 06/12 10:06 weird 06/12 10:06 another case of useless metas :P 06/12 10:07 it's not hard to see what they refer to, but i've no idea what to try 06/12 10:09 regardless, it sounds like a bug? 06/12 10:11 it might be 06/12 10:11 uh, darcs pulling gives me a generalized Vec, apparently :) 06/12 10:14 how does NAD deal with splitAt? 06/12 10:14 oh weird 06/12 10:15 very different :) 06/12 10:15 it reads quite easily now, at least 06/12 10:16 uhm, explicit equality proofs rather than indexes 06/12 10:21 * Saizan wants more ram 06/12 10:21 :) 06/12 10:22 Yeah, my 2 gigs doesn't cut it. :) 06/12 10:23 hello 06/12 10:24 8GB sticks are only$500. :) 06/12 10:24 is there a vector type where the type of the elements depends on their position? 06/12 11:27 I doubt there's one in the library, but one could imagine such a thing. 06/12 11:37 Instead of Fin n -> A, it's (i : Fin n) -> T i. 06/12 11:38 There's also telescopes, where elements can refer to the elements that follow it in the list (although in that case, it might be better to flip it around and think of it as a snoc list. 06/12 11:40 i don't need telescopes for now 06/12 11:42 mh, i wonder if i want to write a datatype like Vec or just a function like that 06/12 11:43 i need this for my MonadSolver attempt 06/12 11:43 "We’ve decided that the best way to get our new type theory out there for you to play with, sooner rather than later, is not to wrap it up in a new version of the Epigram language, but rather to present it as is, in a low-budget command-driven interactive proof assistant. This is beginning to materialise." 06/12 20:28 excellent that means I don't have to code it up in agda :P 06/12 20:28 dolio congrats btw :P 06/12 20:31 you got props from Oleg 06/12 20:31 http://www.e-pig.org/epilogue/?p=263 06/12 21:49 yay :) 06/12 21:54 hehe 06/12 21:54 Pierre seems rather active. This is splendid news. 06/12 21:54 I hope they have good cake in Tallinn 06/12 21:55 edwinb: yep, I'm active, and the reason is simple: I want to graduate before the end of the century. And for that, I will need Cochon/Epigram with a working OTT + Containers ;-) 06/12 22:36 oh, you're here, excellent :) 06/12 22:36 but I'm not alone: Adam is doing a wonderful job too 06/12 22:36 I must see if I can pop over to Glasgow at some point 06/12 22:37 it's good that you have strong motivation anyway :) 06/12 22:37 pigmalion : oh you are Pierre! 06/12 22:37 edwinb: that would be great: I would like to compile that 2 + 2 with Epic 06/12 22:37 you have a awesome part of your name "Evariste" :P 06/12 22:37 quantumEd: yes, I landed here for the first time a few hours ago, actually. 06/12 22:39 I suspect wiring up the compiler to print something that resembles "four" would be reasonably easy, and a good excuse for me to visit in any case 06/12 22:39 what is your work about? if you're doing something to do with containers and OTT it's got to be interesting 06/12 22:39 particularly if it means I can show you how to wire it up to anything else that might come up 06/12 22:39 edwinb: please do, I'm extremely interested with Epic and what we could do with it 06/12 22:42 (and what is Cochon?) 06/12 22:42 quantumEd: my PhD is supposed to be about "Reusability for Dependent Types", in which we plan to abuse containers to get a lot of stuffs for free 06/12 22:43 Peter Morris PhD thesis is a good intro to the field 06/12 22:43 but you are taking it further? 06/12 22:44 oh, sorry: Cochon is the name of the proof assistant. I hope I've spoiled an industrial secret :-) 06/12 22:44 (I've read his work it's really quite something) 06/12 22:44 quantumEd: hopefully, yes :-D 06/12 22:44 in what respects? the only thing I know about in that area is ornaments (and I guess the induction-recursion stuff but I don't like to think about that too much so my head stays in one piece) 06/12 22:45 some interesting question arised in Peter's PhD. A simple one (in its formulation) is "how to declare these data-types?": it looks like we need a language for defining data-types (and their respective properties) 06/12 22:46 I'd quite like to never have to write another data type that looks like a list 06/12 22:46 edwinb: exactly 06/12 22:46 and it's amazing how many things are just Nat with bells on 06/12 22:47 quantumEd: if you know about ornanements, then I guess that you get the point: you would like to be able to say "I have NAT here, I want to ornament it with some data. I get my list and it's fold, etc." 06/12 22:48 pigmalion well I don't want to sound like some kind of depraved thesis reading person but I really look forward to seeing this :P 06/12 22:48 hehe. no pressure then :) 06/12 22:49 quantumEd: I'm just getting started, so I find myself in quite a lot of depravation, too :-) 06/12 22:50 becoming depraved is a good first step 06/12 22:53 er 06/12 22:53 if you see what I mean :) 06/12 22:53 :-) 06/12 22:54 I really want to play with an OTT checker thoughhh its frustrating so I started to implement one -- but now I read this post on e-pig I can happily not complete that 06/12 22:57 pigmalion: are all the Strathclyde gang going to Pigweek in Tallinn? 06/12 22:57 edwinb: yes: Conor, Adam, and I (small gang but we have SuperNinja Conor) 06/12 22:59 splendid 06/12 22:59 I should sort out my travel 06/12 22:59 edwinb: we should, too (Conor is taking care of the organization (read "this is complete chaos")) 06/12 23:00 very good 06/12 23:00 quantumEd: OTT is implemented but it's a pain to write the terms by hand: we are working on some "tacticals" and some automation 06/12 23:01 quantumEd: for example, we know how to write the proof of \x. x + 0 == \x. 0 + x, but writing the actual proof term by hand is... hem... 06/12 23:03 hm it's really awkward just to write small terms like this? 06/12 23:03 writing proof terms like that is always a pain 06/12 23:04 quantumEd, edwinb: I confirm 06/12 23:04 I mean it's just 3 lines or something in the paper 06/12 23:04 yes, but you have to work out what those 3 lines are 06/12 23:05 isn't it the same with this implementation? 06/12 23:05 which is something machines are usually better at 06/12 23:05 there is an induction involved. Moreover, our Nat is not provided by the theory: it's encoded in a simplified inductive universe 06/12 23:05 but this'll all get fixed, in time... 06/12 23:05 by the way 06/12 23:06 oh never mind, I was going to ask something about recursion but I just realized the answer 06/12 23:07 hey is it possible to prove  forall f : A -> A, f = id  in OTT? 06/12 23:13 If you defined some syntax of programs I guess you could get   f : "A -> A", [[ f ]] = id  via parametricity, 06/12 23:14 quantumEd: interesting question... (which is a way to admit that I don't have the answer). How is/would be 'id' defined? 06/12 23:18 I just mean identity funciton,   id t = t   (but I am using an implicit for the type parameter) 06/12 23:19 I'll think about that, that's interesting. With a colleague, we plan to translate "stuffs" from Category Theory, to exercise the limit of OTT. Your question is interesting in that respect. 06/12 23:26 is stuffs a book or a term that just means a bunch of different things? 06/12 23:26 you never know with CT 06/12 23:26 oh does that mean there's some kind of universe heirarchy in OTT now? 06/12 23:27 quantumEd: well, "stuff" would be the definition of a category and populating this thing with some trivial examples and, maybe, some less trivial ones :-) 06/12 23:28 quantumEd: hum. no. "That's on my Todo list", as one say. 06/12 23:28 that's one problem I think is very tricky 06/12 23:29 it's very Tarsky, actually 06/12 23:30 hehe 06/12 23:30 ;-) 06/12 23:30 quantumEd: I did? 06/12 23:33 dolio yeah 06/12 23:33 http://okmij.org/ftp/Computation/differentiating-parsers.html 06/12 23:34 Dan Doel has applied the above differentiation technique to Haskell parsers, built with parser combinators. He started with a pure parser over an ordinary string; he then turned to a parser written in monadic style and consuming a monadic list. He used the CC-delcont library of delimited control, which he packaged for Hackage. Dan Doel described his results in two messages posted on the Haskell-Cafe mailing list, [inv-parser-pure] and [inv-parser-mon 06/12 23:34 adic]. 06/12 23:34 etc... 06/12 23:34 you didn't know?? 06/12 23:34 Ah. No, I didn't. 06/12 23:35 ah well nice work anyway 06/12 23:35 (if I just understood wtf it was :P) 06/12 23:35 --- Day changed Mon Dec 07 2009 -!- Berengal_ is now known as Berengal 07/12 06:36 Darin Morrison Says: 07/12 14:48 I’d rather not quite post the code online yet because some bits of it are not as polished as I like. If you (or anyone else) would like a copy though, feel free to email me and I’ll send it to you. 07/12 14:48 -!- Berengal_ is now known as Berengal 07/12 16:08 -!- Berengal_ is now known as Berengal 07/12 19:59 http://www.cs.nott.ac.uk/~dwm/nbe/html/NBE.html 07/12 20:06 nbe : ∀ {Γ α} → Γ ⊢ α → Γ ⊢ α 07/12 20:07 nbe = completeness ∘ soundness 07/12 20:07 nice 07/12 20:13 -!- Berengal_ is now known as Berengal 07/12 20:14 very nice 07/12 20:32 --- Day changed Tue Dec 08 2009 -!- whoppix_ is now known as whoppix 08/12 00:46 allo allo! 08/12 18:52 fancy finding you here 08/12 18:52 heh ;-) Hi 08/12 18:53 hi! 08/12 18:53 Before asking questions I'll take a look at those URLs :-) 08/12 18:53 okay :) 08/12 18:53 there's also a nice big tutorial pdf for agda 08/12 18:54 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 08/12 18:54 thanks :) 08/12 19:01 -!- whoppix_ is now known as whoppix 08/12 21:00 -!- copumpkin is now known as c0w 08/12 23:31 -!- c0w is now known as copumpkin 08/12 23:32 --- Day changed Wed Dec 09 2009 say I had a Vec of Nats 09/12 01:51 v = 1 :: 2 :: 3 :: [] 09/12 01:52 now I want map Fin v, which should give me a (in Set1) Fin 1 :: Fin 2 :: Fin 3 :: [] 09/12 01:53 is there a nice way to create a heterogeneous vector of values from that vector of sets? 09/12 01:53 so 0 :: 0 :: 2 :: [] would be one of the six values in that 09/12 01:54 seems sort of like a "zipped" type 09/12 01:57 I could do it with a Vec of Sigmas probably 09/12 01:57 but that doesn't feel very clean 09/12 01:57 maybe it's the only way though 09/12 01:58 mmm, the latest std lib gives me 09/12 02:06 Failed to solve the following constraints: 09/12 02:06 Set (a ⊔ ℓ) =< Set (a ⊔ ℓ) 09/12 02:06 that seems like something it should be capable of solving on its own :) 09/12 02:06 * copumpkin recompiles agda 09/12 02:07 I made a special HeteroVec type that takes a Vec of types 09/12 02:20 feels ugly though 09/12 02:20 anyone have a better name than HeteroVec? 09/12 02:44 I was hoping to be able to make HeteroVec self-reliant 09/12 02:53 but it can't refer to itself 09/12 02:53 I guess that would lead to an infinite type 09/12 02:54 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=13856#a13856 is what I have 09/12 03:03 -!- kmc__ is now known as kmc 09/12 04:44 copumpkin: HeteroVec would be inductively defined products/tuples. 09/12 06:09 All Fin v ? 09/12 06:23 except that Vec has no All 09/12 06:31 the composition of monotone functions is a monotone function, right? i wonder if there's something to this effect in the stdlib 09/12 08:59 Partial orders and monotone functions form a category. 09/12 09:09 I don't recall anything like that in the standard library, though. 09/12 09:09 Lots of algebraic structures are defined, but not much is built around structure respecting functions. 09/12 09:10 yeah, there's _Respects_ but it's for predicates 09/12 09:34 assuming i understand it 09/12 09:35 it sure would be nice if two different types could get the number literal sugar at once 09/12 16:59 since they enforce that the sugar be attached to constructors in the first place 09/12 16:59 and constructors can be disambiguated 09/12 16:59 yes, i want typeclasses too 09/12 17:07 typeclasses would be nice, but if not those, then just a special case for number literals 09/12 17:07 and maybe a magic unraveler of number literals when types get printed, too 09/12 17:07 oh I guess it already does that 09/12 17:08 is that new? 09/12 17:08 unraveler? 09/12 17:13 well, something that takes suc (suc (suc zero)) in a type and replaces it with 3 09/12 17:13 but then what values do you pick for a b and c in the case where  cons a (cons b (cons c nil))  replaced from  3? 09/12 17:14 hm, for some reason it can't solve a constraint 09/12 18:22 ∈++ : ∀ {m n a} (x : a) (xs : Vec a n) (ys : Vec a m) → x ∈ xs → x ∈ (xs ++ ys) 09/12 18:23 ∈++ a (.a ∷ xs) ys here = here 09/12 18:23 I wrote this a while ago and it worked :o 09/12 18:24 maybe the std lib changed subtly 09/12 18:25 what's the type of here? I don't see how that typechecks 09/12 18:27 oh wait I see it 09/12 18:27 that's just one case 09/12 18:27 I can give the rest of it if you'd like 09/12 18:27 nah I was just wondering if here knew about ++ but I see that it doesn't need to nw 09/12 18:27 :) 09/12 18:28 but for some reason it doesn't like that anymore 09/12 18:28 I'm reasonably confident it used to work 09/12 18:28 http://snapplr.com/8jkp 09/12 18:29 wait, wrong error 09/12 18:30 http://snapplr.com/9mwf 09/12 18:30 ah 09/12 18:31 a : Set 09/12 18:31 meh :) 09/12 18:31 * copumpkin is still bothered by not being able to prove an infinite domain + an injective function = an infinite codomain :( 09/12 19:29 how do you express something is infinite in agda? 09/12 19:33 Finite : Set → Set 09/12 19:33 Finite A = Σ (List A) (λ v → ∀ x → x ∈ v) 09/12 19:33 Infinite : Set → Set 09/12 19:33 Infinite A = ¬ Finite A 09/12 19:33 it's mostly because I can't reverse the mapping 09/12 19:34 maybe if I chose another representation for Finite it would be possible? 09/12 19:35 ttt-- what does that mean ?? 09/12 19:36 my name doesnt mean anything if that was the question 09/12 19:36 when you said infinite what do you mean by it 09/12 19:37 oh 09/12 19:37 and something 09/12 19:37 Toposes, Triples and Theories! 09/12 19:37 copumpkin: maybe you need a left-inverse instead of just injectivity? 09/12 19:37 Saizan_: intuitively (classically) it seems like injectivity should be enough 09/12 19:37 but I guess I do 09/12 19:38 classically they are equivalent, afaiu 09/12 19:38 I think Injective/Surjective/Bijective should be in Data.Function 09/12 19:38 there's some of that somewhere 09/12 19:39 oh 09/12 19:39 I was trying to find it and failed 09/12 19:39 ttt--, well ? 09/12 19:39 I was just wondering how copumpkin was doing things. I dont really know anything 09/12 19:40 in Relation.Nullary 09/12 19:40 oh I didn't make the link I just thought that was an independent question 09/12 19:40 Saizan_: http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.html#340 ? 09/12 19:40 that gives you a bijection 09/12 19:40 yeah me too 09/12 19:40 copumpkin can you paste it all up to the theorem you haven't prove yet ?? 09/12 19:41 my Relation.Nullary looks quite differently 09/12 19:41 sure, but it's really ugly 09/12 19:41 that's ok 09/12 19:41 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=13885#a13885 at the bottom 09/12 19:42 oh, there's Relation.Nullary.Injection and .LeftInverse now 09/12 19:42 ooh 09/12 19:42 ack, Setoids 09/12 19:43 http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.LeftInverse.html#230 and http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Injection.html#227 looks scary 09/12 19:44 those long arrows do :O 09/12 19:46 so I guess the only way to do this is with a left inverse 09/12 19:47 * copumpkin sighs 09/12 19:47 I told you 'injective' is useless :P 09/12 19:48 it breaks the symmetry of finite=>surjective=>finite and infinite=>injective=>infinite 09/12 19:48 Why is that a "nullary" relation? 09/12 19:48 this is constructive math 09/12 19:48 * copumpkin weeps 09/12 19:48 maybe if I whine enough constructive math will listen and be nice 09/12 19:49 * Saizan_ puts copumpkin inside a double negation 09/12 19:49 * copumpkin pops right back out, unchanged 09/12 19:49 I bet you thought you could trap me 09/12 19:49 i actually did. 09/12 19:49 * copumpkin is from rome! being classical is what we do! 09/12 19:50 hah 09/12 19:50 sorry, really bad :P 09/12 19:50 * copumpkin goes back to his corner and weeps 09/12 19:50 but yeah, I'm not sure why it's a nullary relation either 09/12 19:52 maybe unary 09/12 19:52 {A : Set} -> A -> Set is unary, Set is nullary 09/12 19:53 it'd be nice to be able to write (f : a -> b) -> Bijective f  -> (b -> a) 09/12 19:53 according to the comments 09/12 19:53 oh, I can write Bijective=>Inverse : ∀ {a b} → (f : a → b) → Bijective f → (b -> a) 09/12 19:55 at least that 09/12 19:55 hrrmpf 09/12 19:55 I guess it's that f LeftInverseOf g is nullary, not _LeftInverseOf_. 09/12 19:56 Whereas _==_ is a binary relation on a single type or something. 09/12 19:57 how is Bijective defined? 09/12 19:57 Bijective f = Injective f × Surjective f 09/12 19:57 Surjective f = ∀ y → ∃ (λ x → f x ≡ y) 09/12 19:58 Surjective lets you write b -> a, doesn't it? 09/12 20:00 yep 09/12 20:00 And injective probably lets you prove that it's an inverse. 09/12 20:01 is there a name for a monotone function f such that \all x -> x <= f x ? 09/12 20:05 copumpkin if you change Infinite to be a genereator (rather than the negative statement which it currently is) then I think you can prove Infinite⇒Injective⇒Infinite using pigeonhole 09/12 20:10 generator in what sense? 09/12 20:11 something which gives you as many distinct elements of the type as you want 09/12 20:11 how would you phrase that? the only ways I can think of would imply it being countably infinite 09/12 20:12 that shouldn't be a problem, if you have an uncountable infinity the generator only needs to generate a countable subset 09/12 20:13 so just Nat -> a ? 09/12 20:14 I was thinking  (n : Nat) -> FreshVector A n 09/12 20:14 (fresh meaning every element you cons on is different from all the ones before) 09/12 20:14 hm! 09/12 20:15 I'll try that 09/12 20:20 --- Log closed Wed Dec 09 20:33:00 2009 --- Log opened Wed Dec 09 20:34:05 2009 -!- Irssi: #agda: Total of 22 nicks [0 ops, 0 halfops, 0 voices, 22 normal] 09/12 20:34 -!- Irssi: Join to #agda was synced in 85 secs 09/12 20:35 I think:   injection (N -> A)   <->   forall n, freshvec A n,   (<-) is easy, just take the last element of the nth freshvector,   (->) is tricky because you need to know that  i <> j -> f i <> f j  (i j : Nat) (f : Nat -> A) -- but since if injectivity is defined as having a left inverse then we have that property 09/12 20:35 that's what I meant by isomorphism 09/12 20:35 ah 09/12 20:36 well, injectivity as I have it doesn't give you a left inverse 09/12 20:36 Injective f = ∀ {x y} → f x ≡ f y → x ≡ y 09/12 20:37 so change it :P 09/12 20:37 lol 09/12 20:37 bam! Injective : ∀ {a b : Set} → (a → b) → Set 09/12 20:38 Injective {a} {b} f = (∀ {x y} → f x ≡ f y → x ≡ y) × b → Maybe a 09/12 20:38 ;) 09/12 20:38 now I can do it with my negated Finite representation too, though 09/12 20:38 Injective : forall {A B : Set} (f : A -> B) -> Set 09/12 20:40 Injective f = ∀ {x y} → f x ≡ f y → x ≡ y 09/12 20:40 inj : forall {A B : Set} (f : A -> B) -> Injective f -> ∀ x y -> ¬ x ≡ y -> ¬ f x ≡ f y 09/12 20:40 inj f feq-prf x y ≠xy fx-fy = ≠xy (feq-prf fx-fy) 09/12 20:40 what about that ? 09/12 20:40 looks reasonable 09/12 20:42 doesn't give me a left inverse though 09/12 20:42 what do you want a left inverse for? 09/12 20:42 maybe I don't. I thought I still needed one to get the infinite->injective->infinite proof 09/12 20:42 --- Day changed Thu Dec 10 2009 we need inductively defined algebraic structures! 10/12 00:38 like universal algebra? 10/12 00:39 yeah, but more general than what universal algebra appears to deal with 10/12 00:39 huh?? 10/12 00:40 universal algebra appears to avoid structures with conditional laws 10/12 00:40 things like "every element except 0 has an inverse" 10/12 00:40 unless I'm missing something 10/12 00:40 apparently the notion of conditional laws is linked to the existence of free structures 10/12 00:41 but I don't necessarily care 10/12 00:41 I'm trying to think of a nice way to come up with a universe of structures over sets (types, possibly more than one) with operations, laws, and distinguished objects 10/12 00:45 why? 10/12 00:53 can't tell if it's model theory of universal algebra 10/12 00:54 or** 10/12 00:54 well, I'm not a big fan of the current approach of naming all the algebraic structures one can think of and their associated properties, each with accessors to get at the properties you need 10/12 00:55 you save some effort by nesting the structures, but it still feels unnecessary. Being able to specify the structures in a generic manner so you can say "A group is a structure that has one set, one operation, and one distinguished element such that the operation is associative and its identity is the element" 10/12 00:56 basically describing only the relationships between those three things 10/12 00:57 I mostly don't feel that the current approach is very flexible. For example, IEEE Floats fail associativity but have many other useful properties 10/12 00:59 pretty much every named structure of interest assumes associativity 10/12 01:00 if I can specify that my function needs commutativity and an identity element for +, but I don't rely on associativity 10/12 01:00 I can use floats without worrying about error 10/12 01:00 * copumpkin shrugs, it might be a silly idea but I like thinking about it 10/12 01:02 why is it a silly idea? 10/12 01:03 I don't know :) 10/12 01:03 I would really just like to make Algebra more usable in programming 10/12 01:04 me too 10/12 01:04 haev you seen CoRN 10/12 01:05 nope 10/12 01:05 looks like a coq module? 10/12 01:05 aha 10/12 01:06 the documentation looks enormous 10/12 01:06 over 10k entries :O 10/12 01:06 now that I think about it 10/12 01:47 Surjective : ∀ {a b : Set} → (a → b) → Set 10/12 01:47 Surjective f = ∀ y → ∃ (λ x → f x ≡ y) 10/12 01:47 isn't that isomorphic to b -> a ? 10/12 01:47 oh wait, it gives me a little more information 10/12 01:48 is there a tutorial to convert yourself from typeclasses to modules? 10/12 16:31 * Saizan would really like to overload \p 10/12 16:31 err, \o 10/12 16:31 it seems like Data.Graph.Acyclic's graph type is ismorphic to a Vec 10/12 20:59 I guess not exactly 10/12 21:02 wow, agda gets ridiculously slow when there are lots of unsolved metas 10/12 21:49 it's taking literally about 10 minutes every time I try to load a Data.Graph.Acyclic that I'm converting to universe polymorphism 10/12 21:50 is it using a lot of memory too? 10/12 21:55 only about 500 megs 10/12 21:56 "only" 10/12 22:02 :) 10/12 22:03 dammit, more yak shaving 10/12 22:03 now I need to universe-polymorphism-ize Data.List too 10/12 22:03 isn't it already? 10/12 22:03 oh it appears to be 10/12 22:03 I wonder why this fails then 10/12 22:03 Any/All aren't yet, though 10/12 22:04 oh that's why 10/12 22:04 not Any/All 10/12 22:05 just a helper function stil in Set 10/12 22:05 i need to try agda again now that it has universe polymorphism. that was one of my bigger complaints about it in the past 10/12 22:14 dammit, I can't get this helper function to work 10/12 22:14 http://snapplr.com/mqy8 10/12 22:15 there isn't even a w there! 10/12 22:15 what proposal won, anyway? the one i liked the most was the universe index as parameter idea 10/12 22:15 of the ones i knew about, anyway 10/12 22:15 there's a magic Level type that's isomorphic to Nat 10/12 22:16 and Set can take that as a parameter 10/12 22:16 strangely enough, writing Set on its own gives you just a regular Set 10/12 22:16 any reason it has to be magic? is it so that it's outside of the Set hierarchy? 10/12 22:16 but it can also take parameters of levels 10/12 22:16 I think so 10/12 22:16 it is defined in agda too 10/12 22:16 but it has some BUILTIN magic pragmas attached to it 10/12 22:16 oh i see 10/12 22:16 so if it's defined in agda it must be declared as Level : Set then? 10/12 22:18 i'll just look it up on my own instead of making somebody else do it. sorry 10/12 22:19 huh, it is indeed Level : Set 10/12 22:20 okay, i have no idea why it's not just Nat now 10/12 22:20 there was a post on the mailing list about it, can't remember now 10/12 22:21 copumpkin: is that from the stdlib, or? 10/12 22:22 * Saizan grepped 10/12 22:22 Saizan: yep it is 10/12 22:32 but I'm editing it to be universe-polymorphic 10/12 22:32 Saizan: by the way about your earlier question 10/12 22:35 Saizan: they aren't exactly the same thing 10/12 22:35 typeclasses, as far as I can see, are like parametrized modules + implicit parameters + automatic instance lookup 10/12 22:36 i meant from a pratical point of view 10/12 22:39 module Eq {A : Set} where _==_ : A -> A -> Bool 10/12 22:40 ? 10/12 22:40 "what's the less painful way to write code that i'd write with typeclasses, using modules?" 10/12 22:40 I guess that isn't it 10/12 22:40 hmm, I wonder 10/12 22:40 i think you'd make Eq a record 10/12 22:40 yeah 10/12 22:40 so you can have instances 10/12 22:40 but if you need more than one instance in the same chunk of code, how do you do it? especially with infix operators 10/12 22:41 I don't think there's an elegant way to do it 10/12 22:42 another options is record Eq where field Carrier : Set; _==_ : Carrier -> Carrier -> Bool, actually 10/12 22:42 if you parametrize Eq by the carrier, it might be able to infer it more 10/12 22:43 not sure 10/12 22:43 * copumpkin shrugs :) 10/12 22:43 or even record Eq {A} where field value : A; _==_ : A -> A -> Bool, which is more OO-style i guess, but i think it's the less practical 10/12 22:44 value? 10/12 22:44 yeah, you bundle up the data with the methods 10/12 22:45 oh 10/12 22:45 ugh :) 10/12 22:45 Injective or LeftInverse look in that style 10/12 22:45 yeah 10/12 22:46 i guess it doesn't make much sense with binary methods, though 10/12 22:46 anyone have any ideas about that weird error I'm getting in Acyclic? 10/12 22:56 what error? 10/12 22:58 http://snapplr.com/mqy8 10/12 22:58 it's talking about an expression w that I can't even see 10/12 22:58 that's probably something you're pattern matching over 10/12 22:59 hm? I didn't even write that function, just added a Level impicit parameter 10/12 22:59 mh 10/12 23:00 one thing that bothers me about implicit args is their left-to-right-ness 10/12 23:31 adding universe polymorphism forces us to add levels to all our functions that need to be polymorphic 10/12 23:31 so now f {X} binds X to the level 10/12 23:31 I think there's f {a = b} to set a particular (a) implicit field 10/12 23:43 yeah 10/12 23:43 that's what I'm using now 10/12 23:43 but it adds clutter, and you're going to have to do it on all universe-polymorphic functions unless you want some dummy {_} at the beginning of each pattern 10/12 23:43 so there needs to be implicit implicit parameters 10/12 23:44 a universe of implicitness! 10/12 23:45 bah, more yak shaving 10/12 23:51 now need to change wellfounded induction to be universe-polymorphic 10/12 23:51 --- Day changed Fri Dec 11 2009 send patches when you're done :) 11/12 00:01 yep :) 11/12 00:24 is there a quick way to jump to a file something is defined in? 11/12 00:26 it says "click mouse-2 to jump to definition" 11/12 00:26 but I'm not sure if I have a mouse 2 11/12 00:26 aha, found it 11/12 00:36 does it make sense to universe-polymorphize Pred? 11/12 00:43 Pred : Set -> Set1 11/12 00:43 Pred a = a -> Set 11/12 00:43 pred ?? 11/12 00:44 Relation.Unary 11/12 00:45 what is it 11/12 00:45 the Induction stuff relies on it 11/12 00:45 just a Predicate about something 11/12 00:45 Pred Nat 11/12 00:45 could be prime 11/12 00:45 oh it means predicate on 11/12 00:45 yeah 11/12 00:45 these abbreviations suck.. 11/12 00:45 oh I see, you could see it as the opposite of suc :P 11/12 00:46 hadn't thought of that 11/12 00:46 hmm, is there an easy way to inject a Set A into a Set (A \lub B) ? 11/12 00:50 hmm, stuck trying to fit a Set into a bigger one :( 11/12 01:01 .ℓA != .ℓB ⊔ .ℓA of type Level 11/12 01:01 we need NAD or Ulf in here 11/12 01:10 not that they'd be awake anyway 11/12 01:10 does it make sense for _|_ to live in an arbitrary Set level? 11/12 01:13 meh, putting it in an arbitrary level breaks a bajillion modules 11/12 01:25 well, puts unresolved metas in them 11/12 01:25 this might be why Relation.Unary is still not polymorphic 11/12 01:29 dammit, so much yak shaving to get that damn graph module polymorphic 11/12 01:41 Hum, it shouldn't be hard to implement Dedekind cuts in Agda. 11/12 01:44 The standard library has natural numbers, right? Does it have integers? Rational numbers? 11/12 01:47 yeah^3 11/12 01:47 but rationals have almost no functionality 11/12 01:48 there's apparently functionality coming to them 11/12 01:48 What would functionality consist of? 11/12 01:48 basic arithmetic, proofs about them, and so on 11/12 01:49 * uorygl nods. 11/12 01:49 do you know how to raise a Set a to Set (a \lub b) ? 11/12 01:51 I guess I can use subst 11/12 01:51 Hum. The typechecker evaluates all the types it receives, right? 11/12 01:52 if they're data 11/12 01:53 λ ℓ → Set ℓ -- what is the type of this? Set\_\omega ? 11/12 01:53 x : (x : Level) → Set (suc x) 11/12 01:54 fair enough 11/12 01:54 So it might make sense to pass around thunks, if I don't want the typechecker to actually evaluate stuff. 11/12 01:56 you'd probably want codata 11/12 01:57 What's that? 11/12 01:57 coinductively defined data 11/12 01:58 can be infinite, defined just by observations on the data rather than by constructing it 11/12 01:58 Yeah, I think I know that. 11/12 01:59 Should I ask whether Agda supports that? 11/12 02:00 it does! 11/12 02:00 just write codata instead of data 11/12 02:00 for your data definition 11/12 02:00 or if you prefer to be more modular 11/12 02:00 just import Coinduction from the standard library and use the \inf type 11/12 02:00 Neat. 11/12 02:00 for examples check out Data.Colist or Data.Conat 11/12 02:01 * uorygl ponders evil things. 11/12 02:01 but it's worth mentioning that sometimes it can be quite painful to prove to the termination checker that your functions terminate 11/12 02:01 Indeed. 11/12 02:01 * uorygl ponders ordinal numbers in a countable model of ZFC, to be specific. 11/12 02:02 * copumpkin is pretty mathematically clueless :) 11/12 02:03 * copumpkin knows the broad idea of ZFC, and knows what ordinals are, but that's about t 11/12 02:03 A model of ZFC is a set of things, and a relation called "is an element of" over it, that together follow the axioms of ZFC. 11/12 02:05 There, now you know what a model of ZFC is. 11/12 02:05 :) 11/12 02:05 _⟨⊎⟩_ : ∀ {ℓA ℓB : Level} {A : Set ℓA} {B : Set ℓB} → Pred A → Pred B → Pred (A ⊎ B) 11/12 02:21 that function is really screwing me in Relation.Unary 11/12 02:21 bah! 11/12 02:24 I just commented that out for now, but so much trouble making stuff universe-polymorphic!!! 11/12 02:27 the problem with sticking _|_ in an arbitrary universe is that it never seems able to infer the universe 11/12 02:38 so you'll need an explicit parameter on it 11/12 02:38 * copumpkin may have to wait for NAD to do this :( 11/12 02:41 * copumpkin doesn't know enough about it all 11/12 02:41 wow, up to 1 gig 11/12 03:22 Data.Graph.Acyclic is murder 11/12 03:22 does emacs with agda-mode steal focus for anyone else? 11/12 03:36 or is it just aquamacs? 11/12 03:36 this module is basically unusable, every time I make a change it takes another 10 minutes to compile :( 11/12 03:41 * uorygl ponders whether he wants to make his Peano arithmetic efficient or not. 11/12 03:44 Meh. Do we have a speedy built-in arithmetic thing? 11/12 03:45 nope 11/12 03:46 Aww. 11/12 03:46 * uorygl ponders making a semi-speedy digital arithmetic thing. 11/12 03:47 aha, the slowdown in the graph module is the tests 11/12 03:47 * uorygl sticks with his Peano. 11/12 03:47 We don't have equality testing either, do we. 11/12 03:50 well 11/12 03:52 there's \== 11/12 03:52 Does \==\ already mean something? 11/12 04:05 doubt it 11/12 04:05 Er, \== 11/12 04:12 What is meant by \== and \==\ ? 11/12 04:12 \==\ is a typo. 11/12 04:12 Oh. 11/12 04:12 Is \top the same thing as T? 11/12 04:15 If not, then I have a true fontfail here. 11/12 04:15 no 11/12 04:17 ⊤ vs T 11/12 04:18 * uorygl gives his font a stern look. 11/12 04:23 :) 11/12 04:24 alright, that's enough agda for tonight. With any luck NAD will have a beautiful solution to the problems I posted to the mailing list 11/12 04:39 * copumpkin has decided to represent algebraic structures as DAGs 11/12 07:55 :O 11/12 08:04 :O indeed 11/12 08:05 I'll probably fail, but I'll have fun trying 11/12 08:05 once I get that Data.Graph.Acyclic working with universe polymorphism 11/12 08:05 i was going to use LeftInverse from the lib, but all the setoid overhead is putting me off 11/12 08:17 yeah :/ 11/12 08:18 --- Log closed Fri Dec 11 19:58:44 2009 --- Log opened Fri Dec 11 20:01:25 2009 -!- Irssi: #agda: Total of 18 nicks [0 ops, 0 halfops, 0 voices, 18 normal] 11/12 20:01 -!- Irssi: Join to #agda was synced in 84 secs 11/12 20:02 -!- mak__ is now known as comak 11/12 20:06 -!- Berengal_ is now known as Berengal 11/12 20:39 --- Day changed Sat Dec 12 2009 damn, there's no type for ∀ {a b c} ->  {A : Set a} {B : Set b} {C : Set c} -> (B -> C) -> (A -> B) -> A -> C 12/12 19:13 really?? 12/12 19:14 what if you shuffle the ordering about a bit 12/12 19:15 if you try to write "foo = ∀ {a b c} ->  {A : Set a} {B : Set b} {C : Set c} -> (B -> C) -> (A -> B) -> A -> C" you get an error saying "Setω is not a valid type." 12/12 19:15 what if it's lambda instead of forall, for the levels? 12/12 19:15 it works 12/12 19:16 can't you use the lambda one to make foo? 12/12 20:03 --- Log closed Sat Dec 12 20:05:11 2009 --- Log opened Sat Dec 12 20:05:19 2009 -!- Irssi: #agda: Total of 22 nicks [0 ops, 0 halfops, 0 voices, 22 normal] 12/12 20:05 wouldn't i need to quantify over levels anyway? 12/12 20:05 -!- Irssi: Join to #agda was synced in 85 secs 12/12 20:06 I dont know what you mean 12/12 20:07 well, if i have the lambda one, let's call it lambda-foo, how do i build foo with it? if i just write foo = forall {a b c} -> lambda-foo a b c i get the same problem, but i have no other idea 12/12 20:09 but if lambda-foo typechecks then why doesn't foo? 12/12 20:09 that's weird 12/12 20:10 lambda-foo : (a b c : Level) -> Set (suc (a ⊔ b ⊔ c)) 12/12 20:10 but the type of foo can't involve a, b and c, since they are quantified in its body, afaiu 12/12 20:11 well I don't understand this 12/12 20:12 so you'd have to find a level "suc (a ⊔ b ⊔ c)" for any a b c, leading to omega 12/12 20:12 but it's not fully clear to me either 12/12 20:12 foo has type Set omega, and you're not allowed to name things of type Set omega. 12/12 20:13 I think it has that type, at least. 12/12 20:13 why does it have that type 12/12 20:13 Given S : k1, and for x : S, T[x] : k2, and if x is free in k2, then (x : S) -> T[x] has type Set omega. 12/12 20:15 foo = forall {a b c} -> Set (suc (max a b c)), and Set (suc ...) : Set (suc (suc (max a b c))), which mentions a b and c. 12/12 20:17 and if you allow abstraction over things of type Set omega bad things happen? 12/12 20:23 If you want to abstract over things of type Set omega, you need a Set (omega + 1) 12/12 20:23 where's the problem?:) 12/12 20:24 btw, i said abstraction assuming it was the same for let bindings 12/12 20:25 Then people will just complain that we need transfinite universe polymorphism to make the transfinite set shuffling functions more uniform. :) 12/12 20:25 Set omega : Set omega haha 12/12 20:25 There's nothing wrong with giving names to things of type Set omega, though. As an alias. 12/12 20:27 But Agda doesn't like it, I think. 12/12 20:28 levels should clearly be ordinals from the start! /me has no idea of the implications 12/12 20:28 it says Set omega is not a valid type if you try that 12/12 20:28 My homebrew checker would let you define foo as that type, and it'd say "foo : Set omega" (or, it'd use a capital omega, but close enough). 12/12 20:29 I don't get it 12/12 20:29 But you can't write, say, "\(x : Set omega) -> ..." 12/12 20:29 Or \ whatever -> something-of-type-Set-omega 12/12 20:30 mh, i guess you meant one would like to port code for omega to omega^2 etc.. 12/12 20:30 I'm not sure you could just have ordinal levels, either. 12/12 20:32 For instance, I was thinking about 'finite set' universe polymorphism. 12/12 20:34 Where you might have (x : Level 5) -> Set x live in Set 6. 12/12 20:35 But if you can eliminate regulard datatypes into levels, it's not obvious how to set up typing rules that would make that workable. 12/12 20:36 Like, (i : Fin 5) -> Set (finToFinLevel i), is that in Set 6, too? 12/12 20:37 Crap, where did I leave off? 12/12 20:37 "dolio: Like, (i : Fin 5) -> Set (finToFinLevel i), is that in Set 6, too?" 12/12 20:38 But then what about (i : Fin 5) -> Set (finToFinLevel i + 1), that needs to be in Set 7. 12/12 20:38 Or maybe (n : Nat) -> Set (finToFinLevel (n mod 6)). Can that live in Set 6, since it only uses Sets up to 5? But how do you figure that out? 12/12 20:39 dependent types to the rescue! 12/12 20:39 what's the type of finToFinLevel, actually? 12/12 20:39 Fin n -> Level n, I guess. 12/12 20:39 uhm, right, it just feels weird that levels are regular datatypes 12/12 20:41 eyah I don't really understand the point 12/12 20:41 Well, at the time I had some idea for a datatype where I thought it would be cool for it to live in something other than Set omega, despite being universe polymorphic. 12/12 20:42 I don't remember what it was, though. 12/12 20:42 It may have been smaller versions of the universal sums I have going. 12/12 20:43 hey did you make your think OTT? 12/12 20:43 { i : Level, A : Set i | A } is like a sum of all (non-omega) sets. 12/12 20:43 So, what if you could do { i : Level n, A : Set i | A }, and have a sum of all Set m, for m < n, living in Set n. 12/12 20:44 No, I got distracted and haven't worked on my new type theory in a while. 12/12 20:45 It's stuck with some half-assed extension of erasure typing that I don't believe will really work well. 12/12 20:45 --- Day changed Sun Dec 13 2009 hi, i wrote the functor and applicative and monad laws here as an exercise 13/12 12:26 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086 13/12 12:26 if anyone is interested :) 13/12 12:26 instead of defining those get* methods i'd use the module system 13/12 12:41 especially open 13/12 12:41 e.g. you can translate the definition into "getMapF functorRecord = mapF where open Functor functorRecord" so it might be clearer to just inline that "where open Functor F" 13/12 12:43 and if you have many definitions all parametrized on a single functor you can group them in a module and make that module parametrised instead 13/12 12:44 e.g. the laws 13/12 12:44 ttt--: like this http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a14087 13/12 12:48 yeah that looks better, thanks :) 13/12 12:49 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a14089 13/12 13:07 it doesnt let me use Functor M as a parameter (probably because it hasnt been opened yet?) 13/12 13:08 ok it seems to work if i put Functor.Functor M there 13/12 13:09 * ttt-- goes to read how modules work 13/12 13:10 ttt--: you can only use records as parameters 13/12 13:24 ttt--: while Functor there refers to the outer one 13/12 13:24 you can use Functor.Functor i guess 13/12 13:25 oh, you already found that :) 13/12 13:28 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a14094 <- how i'd write it 13/12 13:30 is there a sane way to write this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14110#a14110 13/12 17:36 found it http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14110#a14111 13/12 17:47 -!- zarvok is now known as ccasin 13/12 20:10 --- Day changed Mon Dec 14 2009 there's no way to get shadowing at the module level? 14/12 16:33 quantumEd: did you get to formulate the correctness of substitution in the end? 14/12 23:37 no I still don't know a good way to state it 14/12 23:37 it seems like zippers could be relevant, but i'm wondering too 14/12 23:41 I have to hope its not just something you got to program carefully 14/12 23:58 --- Day changed Tue Dec 15 2009 -!- boyscare1 is now known as boyscared 15/12 02:59 -!- boyscare1 is now known as boyscared 15/12 17:18 would it be possible to define a Y combinator in agda? (I think no becuase it allows general recursion - but I really dont know agda nearly well enough to say) 15/12 20:36 it'd be pink 15/12 20:39 i.e. it wouldn't pass the termination checker 15/12 20:40 You can define recursion combinators that look a lot like Y. 15/12 21:16 Like, if you have a well-founded relation R, you can define a recursion combinator where the recursive call requires a proof obligation that the argument you're using it with is 'less than' the case you're on, according to the relation. 15/12 21:17 {A : Set} {P : A -> Set} {_<_ : A -> A -> Set} -> ({y : A} -> ({z : A} -> z < y -> P z) -> P y) -> (x : A) -> P x 15/12 21:19 Missing the evidence that _<_ is well founded there, of course. 15/12 21:20 But, if you erase the x, y and z, and associated stuff, you get (P -> P) -> P. 15/12 21:21 you can abstract over the _<_ or you've to write a specific combinator for each _<_? 15/12 21:21 You can define a type Wf : {A : Set} (_<_ : A -> A -> Set) -> Set that encodes the necessary stuff. 15/12 21:22 So a general combinator would have an Wf _<_ as an argument. 15/12 21:23 i see 15/12 21:24 Actually I think you might define Acc _<_ x, where the _<_ might not even be well-founded as a whole, but x is an 'accessible' element, which is defined as "x is accessible if forall y < x, y is accessible". 15/12 21:26 Then WF _<_ would be forall x -> Acc _<_ x 15/12 21:26 I'm not sure what a relation with accessible elements that isn't well-founded would look like, exactly, though. 15/12 21:29 Maybe something like 0 < 1 < 2 < 3 < 4 < n forall n \notin {0,1,2,3,4}, but forall n n <= 5. 15/12 21:31 Or, that's probably not a good way to put it. 15/12 21:31 You get the idea, though. Make it the normal natural less-than up to some number, and then turn it backwards after that. 15/12 21:32 To prove that 5 is accessible, you have to prove that 6 is accessible, so you have to prove that 7 is accessible, and so on. 15/12 21:33 But to prove that 4 is accessible, you only have to prove that 0 through 3 are accessible, and 0 is trivially accessible. 15/12 21:33 Oh, and of course, Acc is an inductive fixedpoint, so you can't prove the infinite regress for the ... < 7 < 6 < 5 situation. :) 15/12 21:41 I guess I should have come up with 0 < 1 < 2 < 3 < 4 < ... < 7 < 6 < 5 in the first place. :) 15/12 21:42 -!- copumpkin_ is now known as copumpkin 15/12 21:50 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14275#a14275 <- i thought it'd be more complicated 15/12 22:14 Nope, that's it. 15/12 22:14 Proving that an ordering is well founded/an element is accessible is the trickier bit. 15/12 22:15 heh, i imagine 15/12 22:17 It isn't really that hard for, say, the usual ordering on the naturals. 15/12 22:17 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14275#a14279 <- nice when you can just fool around until it typechecks :) 15/12 22:45 Heh. I like your equational proof. 15/12 22:48 so explicit, eh? :) 15/12 22:56 P=NP = _ 15/12 22:56 -!- EnglishGent is now known as EnglishGent^afk 15/12 23:18 --- Day changed Wed Dec 16 2009 i will read a tutorial on agda and in hour i wanna talk agda vs haskell, or agda in general. anyone in the mood ? 16/12 01:37 -!- copumpkin is now known as CoqBloq 16/12 07:04 -!- EnglishGent^afk is now known as EnglishGent 16/12 14:52 --- Day changed Thu Dec 17 2009 -!- opdolio is now known as dolio 17/12 00:57 does agda 2.2.4 have universe polymorphism? 17/12 07:01 I don't think so. 17/12 07:02 That's the one on hackage, right? 17/12 07:02 yeah 17/12 07:02 There's a bijection between Nat and (Nat -> Bool) -> Bool if we assume some wacky non-classical axioms, right? 17/12 07:04 woah 17/12 07:05 can't y ou think of Nat -> Bool like real numbers written in binary, and you're saying there's only omega many predicates on them? 17/12 07:05 Like, all functions are continuous or something. 17/12 07:05 Yes. I thought so. 17/12 07:06 oh you said *non*-classical axioms 17/12 07:06 In a constructive/intuitionistic theory. 17/12 07:06 And yes, it's weird. 17/12 07:07 I was wondering if all functions were differentiable, but it turns out you can define abs 17/12 07:08 Especially since Nat -> Bool is computably uncountable, so it looks bigger than Nat. But then 'forming the power set' again gets you back to the original size. 17/12 07:09 *And*, the argument for showing that there's no surjection Nat -> (Nat -> Bool) works for any A instead of Nat, so it also means that there's no surjection (Nat -> Bool) -> ((Nat -> Bool) -> Bool). 17/12 07:10 So that isn't really a general criterion for being 'bigger', although I guess it still works for Nat. 17/12 07:12 At least, not with the "all functions are continuous" axiom, if it implies what I seem to recall. 17/12 07:13 istr that too 17/12 07:14 I don't know what you mean by the surjection 17/12 07:14 not sure how you'd even state that axiom though 17/12 07:15 which one? 17/12 07:15 that all functions are continuous 17/12 07:15 I mean that given any function b : A -> (A -> Bool), there exists an f : A -> Bool such that forall x : A. f /= b x. 17/12 07:15 I think it's some topological thing but functions R -> R are actually eps/delta cont. too 17/12 07:16 Via Cantor's diagonalization argument. 17/12 07:17 f is surjective if (y : B) -> Σ A λ x → f x ≡ y 17/12 07:17 of course the eps/delta is a consequence of the general topological definition 17/12 07:21 I think it goes the other way too 17/12 07:21 I assume you can only do epsilon/delta in a metric space, though? 17/12 07:22 Or, some generalization that still has something like a metric? 17/12 07:22 * dolio knows almost no topology. 17/12 07:23 I onl yknow an epsilon of topology 17/12 07:25 god dammit 17/12 07:32 bootstrap forkbombed me what the hell 17/12 07:32 last time I did this it was easy 17/12 07:44 did what? 17/12 08:22 installed agda 17/12 08:38 -!- jlouis_ is now known as jlouis 17/12 17:04 Berengal 17/12 23:01 I dream of writing ZFC in Agda :( 17/12 23:01 using polymorphism to make the powerset 17/12 23:01 hm am I mixing you with someone else 17/12 23:37 --- Day changed Fri Dec 18 2009 -!- whoppix_ is now known as whoppix 18/12 00:18 http://www.e-pig.org/epilogue/?p=266 18/12 16:49 soupdragon: Epic should be the implementation of OTT? 18/12 19:42 I don't think so, I don't know 18/12 19:42 Epic is a simple functional language which compiles to reasonably efficient C code 18/12 19:57 it must be OTT is compiling into this language, which Epic turns into C 18/12 19:57 xwell not OTT but the OTT implementation 18/12 19:57 Boy, some people really have a lot of trouble with the diagonal argument. 18/12 20:01 like how? 18/12 20:01 Like they go on at length about how they've found non-diagonalizable 'magic sequences' even when you show them how to diagonalize the magic sequences. 18/12 20:02 Provably, on a computer. 18/12 20:02 sounds like the found happyness already 18/12 20:02 bb..but.. computers can't prove things! :P 18/12 20:02 :) 18/12 20:03 "they can only disprove" 18/12 20:03 wow 18/12 20:03 -!- copumpkin_ is now known as copumpkin 18/12 20:04 Yeah, the computer theorem prover angle didn't accomplish a lot. 18/12 20:04 this is specific case? 18/12 20:04 http://scienceblogs.com/goodmath/2009/12/another_cantor_crank_represent.php#comments 18/12 20:04 that Chu-Carroll keeps writing stuff I abhor 18/12 20:05 I jumped in at 97 to show an Agda encoding of Cantor's argument. 18/12 20:05 Even though computable subsets of the naturals are countable. :) 18/12 20:05 did you get any good responses? 18/12 20:05 They're computably uncountable. 18/12 20:05 is that so?? 18/12 20:06 is something computable only if you can write it down (finitly)? 18/12 20:06 No. I just got to post a bunch of stuff telling a guy that he hadn't found a counter example, and I could (and have since) prove it. 18/12 20:06 Computability is related to Turing machines or lambda calculi, and you can write those down as finite strings. 18/12 20:07 what about the coinductive calculus 18/12 20:07 At least, I think. 18/12 20:07 Mark Chu-Carroll writes factorial in haskell and says "Look at this wonderful example of Curry-Howard isomorphism" 18/12 20:08 Yeah, his Haskell stuff is pretty muddled. 18/12 20:08 And the next day he is slaggin someone off for talking nonsense :P 18/12 20:08 b) countable != diagonalizable 18/12 20:09 I guess he writes C or something 18/12 20:09 Anyhow, even if the computable reals are countable, you can't write a computable function that enumerates them all, so the diagonal argument still works in Agda. 18/12 20:10 "Paul: Neil's comments are right on. Let me be more clear: you don't know what the fuck you're talking about." 18/12 20:10 Or constructive mathematics in general. 18/12 20:10 And since it's constructively valid, it's classicaly valid. 18/12 20:10 telling people they don't know is crazy, it's just an expression of frustration 18/12 20:11 You don't understand ! 18/12 20:12 "I don't think any mathematicians would call Cantor's diagonal a "constructive" proof. It only constructs something if there were already the list of real numbers to work with, and the whole point is to prove that that list doesn't exist." 18/12 20:13 Well, the diagonal argument is pretty simple as proofs go, I think. 18/12 20:13 there's a more subtle confusing, I wonder if that guy came around to it 18/12 20:13 His problem doesn't even seem to be the diagonal argument itself. 18/12 20:13 seems like he didn't but nobody is telling him "You don't have a clue what the fuck you are talking about" 18/12 20:14 It's that he thinks ℕ x ℕ is bigger than ℕ. And that if you try to zig-zag to cover all elements, it doesn't "happen fast enough" for the diagonal argument to work or something. 18/12 20:14 dolio: It's simple and not simple -- Once you understand the first infinity, the argument is very clear and concise 18/12 20:15 but to actually learn what N is ? 18/12 20:15 dolio, who? 18/12 20:15 Paul Homer. 18/12 20:16 His 'counter example' is a 2-dimensional spreadsheet of all real numbers. 18/12 20:16 Which he says you can't apply the argument to, because you have to go down a single row or column. 18/12 20:16 Because that's the only path that's "fast enough". 18/12 20:17 he's using the demonic "..." 18/12 20:17 Heh, yeah. 18/12 20:17 I wonder what his take on 0.999... = 1 is 18/12 20:18 I don't know. I'd prefer to not deal with reals since them being a quotient makes things more complicated. 18/12 20:18 But everyone likes the real numbers. 18/12 20:19 roconnor told me something that sounded nice 18/12 20:19 "Fred Richman says the real numbers are a terminal object in the category of archemedian Heyting fields" 18/12 20:19 (whereas things like N and Z are initial objects of some category) 18/12 20:19 Z is the initial ring, I think. 18/12 20:20 anyway I have no idea what it means yet, 18/12 20:20 Not sure about N. 18/12 20:20 "cardinality is 2^|N|" yikes! 18/12 20:20 I am just sure that starting to talk about exponentiation like that with infinite objects will help everyone understand what's going on 18/12 20:21 Maybe N is the initial semi-ring or something. 18/12 20:21 Or whatever a ring without negation is. 18/12 20:22 Eelis on #coq said something like that 18/12 20:22 That'd fit the situation with Z. 18/12 20:22 "As usual, Mark CC clams up once proven wrong. The tree obviously has countably many vertices, and equally obviously has uncountably many paths." hehe 18/12 20:23 21:46 < Eelis> the natural numbers can be characterized as the initial object in the category of semirings (a variety). 18/12 20:23 21:46 < Eelis> similarly, the integers can be characterized as the initial object in the category of rings (another variety) 18/12 20:23 Yeah, that depends on your definition of tree, apparently. 18/12 20:23 And he's talking about performing some construction 'omega-many times' or something. 18/12 20:24 I don't know what to learn from all this 18/12 20:24 Which sounds very classicaly set theoretic and evil to me. 18/12 20:24 one guy makes some odd statements that use lots of soft words and ellipses 18/12 20:25 isn't it just a coinductive tree? 18/12 20:25 people use swear words to tell him he is wrong 18/12 20:25 he knows he right ... but other people are mixed up about tangential issues 18/12 20:25 Saizan: Not really. The infinite tree is the coinductive tree. 18/12 20:25 so what does it mean? 18/12 20:25 He's talking about computing some kind of limit, where you have leaves at the end of each path, at level omega of the tree. 18/12 20:26 So you have infinitely long paths ending at a node, of which there are obviously uncountably many. 18/12 20:26 Chad corrected me a bunch of times on this point. Sets *are* at infinity, that's part of their definition. 18/12 20:27 that's some 'correction' :D 18/12 20:27 But I don't really grok using ordinals like that. They don't work that way when you represent them in Coq or Agda. 18/12 20:27 as sets? 18/12 20:27 infinitely brancing trees?  that's what the  Lim : (N -> O) -> O  constructor is 18/12 20:27 As being able to 'do something' a transfinite ordinal 'number of times'. 18/12 20:28 dolio the program interpretation? I thought they always terminate in finite time 18/12 20:28 Right, but I think you can have set theoretic constructions that don't have interpretations like that. 18/12 20:28 are they well founded? 18/12 20:29 http://en.wikipedia.org/wiki/Surreal_number is the example 18/12 20:29 There are iterations of the surreal construction transfinitely many times. 18/12 20:30 Like, you do something infinitely many times, and then after that, you do it 5 more times. 18/12 20:34 :O 18/12 20:34 dolio so what's the conclusion or whatever with this stuff? 18/12 20:36 Paul W. Homer etc 18/12 20:36 Structural induction on the Brouwer ordinal omega + 5 just lets you do something 5 times, and then choose an arbitrary (finite) number of times to do something, I think would be an accurate characterization. 18/12 20:36 I don't know. It reminded me of roconnor's blog post about arguing with some guy who thought he'd refuted the incompleteness theorem. 18/12 20:37 Even though roconnor has a computer verified proof of it. :) 18/12 20:37 http://knol.google.com/k/are-real-numbers-uncountable# 18/12 20:37 that reminds me of it 18/12 20:37 but that guy is just playing a game 18/12 20:38 Well, that's what the blog post was originally about. 18/12 20:38 Mark Chu-Carroll picks an easy target 18/12 20:38 hm I don't really see the point in any of this 18/12 20:39 Any of what? 18/12 20:39 all the blogs and knols 18/12 20:40 Knols are supposed to be like Google's wikipedia, I think. 18/12 20:40 I think it's pretty much just people with some basic knowledge (or more than basic) of sets or logic or something, and they practice writing and arguing (and they're really awful at arguing as witness by the "You don't know what you are talking about" comment) 18/12 20:40 Only each article is written by a single person unless they specifically allow other people to edit them. 18/12 20:40 this seems like a terrible disservice to any young child that is trying to learn real mathematics from the internet 18/12 20:41 Which is fine when edwardk writes a knol about categorical recursion combinators. But probably not fine when some guy incorrectly thinks he's refuted basic set theory. 18/12 20:42 yeah I'm interested in the difference between these two things 18/12 20:42 maybe we just have to formally prove everything before we write it 18/12 20:43 Someone posted an article about how Knol is a pretty poor setup. 18/12 20:44 There's no community oversight. And apparently people get paid based on article hits. 18/12 20:44 Which encourages people to write controversial articles, rather than correct ones. 18/12 20:45 dolio well that  is the game he is playing right there 18/12 20:45 now this is ridiculous 18/12 20:45 "Like I keep saying: go read some Conway" 18/12 20:46 Mark C. Chu-Carroll -- the guy who is blogging about all this stuff 18/12 20:46 why doesn't he just type up pages from that book if its so good 18/12 20:46 Well, Conway is awesome, isn't he? 18/12 20:47 I don't know 18/12 20:47 well yes he is 18/12 20:47 I haven't read anything by him though 18/12 20:47 Yeah, me neither, really. 18/12 20:47 I'm just saying what's the point in re-describing all this stuff (about diagonals) 18/12 20:47 it's a hypocritical thing for him to post that comment, imo 18/12 20:47 even if he knows the game he is playing (practice writing and argumentation) then doesn't it break the metaphor? 18/12 20:48 the only reason anyone here is interesting in diagonalization is because lots of people respond to blog posts about it :P 18/12 20:49 I'm sure they all learned it an understood it just fine when they were 15 18/12 20:49 This whole fiasco is a bit grim actually 18/12 20:51 nobody seems to want to think critically and carefully read proofs 18/12 20:52 well a couple people do, but not enough 18/12 20:52 the whole point of proving something is that you can communicate it 18/12 20:53 "I use the term   limit   because this is the ethereal idea most academics associate with real numbers." 18/12 20:56 Heh. 18/12 20:56 I love when people say "academics" like it's the worst kind of person in the world 18/12 20:56 dolio all this is really baffling to me 18/12 20:59 I don't know if I should care 18/12 20:59 it's amazing how controversial this is 18/12 21:00 maybe it's just the phenomena where rubbish stuff becomes popular 18/12 21:00 like naked girl that plays a video game or whatever gets voted to #1 straight away, even though it's highly unremarkable 18/12 21:00 yeah, I guess 18/12 21:01 Set theory an infinites are very popular targets for mathematical cranks. 18/12 21:01 For instance, if you check out sci.math. 18/12 21:01 I got frustrated enough at Earle and Shelby, I think I'll pass :) 18/12 21:02 Probably even moreso than the incompleteness theorem. 18/12 21:02 what's Earle and Shelby? 18/12 21:02 soupdragon: a couple of cranks that showed up recently on haskell-cafe 18/12 21:02 John D. Earle and Shelby Moore iirc 18/12 21:03 http://old.nabble.com/Haskell---Haskell-Cafe-f13132.html on there somewhere? 18/12 21:05 I think they're also popular among people without much mathematical training, because they're things people expect to intuitively understand, but their intuition doesn't match the matematics. 18/12 21:05 'Some infinities are bigger than others, but multiplying two infinities gives the same infinity? That's bogus.' 18/12 21:06 it's all meaningless anyway 18/12 21:07 infinity? hah 18/12 21:07 no wonder so many people take refuge in axiomatics 18/12 21:07 "it's not a proof if you can't turn it into a formal deduction" 18/12 21:08 "Because of time constraints we were not able to focus on this, and confirm by hand, BUT these Equations, spell the doom for your Mathematics." 18/12 21:08 heh 18/12 21:08 I'd not seen that 18/12 21:09 That's from sci.math 18/12 21:09 I dunno it's all a joke to some people but not to others 18/12 21:10 what about those integalactic telefunctors? 18/12 21:11 did they find alien life yet 18/12 21:11 hmf I don't know what to think about hthis 18/12 21:13 I am trying to extract some meaning from it but it's probably just loads of people playing a game 18/12 21:14 what do you take from it? 18/12 21:16 i don't take much from it, some people think an intuitive understanding suffices, some other people don't but aren't good at explain the details, or they don't think they could in a blog post 18/12 21:17 (and my grammar is quite poor currently) 18/12 21:18 yeah that's one tricky thing.. 18/12 21:20 I think that being too formal is really counterproductive and stifling 18/12 21:20 but then you can be wrong if you just guess everything 18/12 21:20 Was I not explaining the details well? 18/12 21:20 i was talking about Chu-Carrol articles in general actually, i didn't follow this one too closely 18/12 21:21 "Wow! This particular Cantor crackpot not only fails to understand the nature of proof and of the real numbers" 18/12 21:28 maybe if I shut my eyes it will go away 18/12 21:29 dolio nobody can read this :P http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14369#a14378 18/12 21:30 except maybe ... the 50 people that know agda 18/12 21:30 "Lets start with a 10x10 square. This cube contains 100 elements. If we enumerate the first 10 elements, then there are 90 elements we have NOT yet enumerated. 18/12 21:31 Lets double our x and y axis to a 20x20 square. We enumerate the next 20 elements, and we now how 380 non-enumerated elements. Lets call this a tick (like the tick of a clock)." 18/12 21:31 this is just silly rambling but there is a wonderfully beautiful thing nearby, proof of the cauchy product 18/12 21:32 The cauchy product is say you got some absolutely convergent sequences, (a_i), (b_i) then let A = sum[i=1..] a_i, B = sum[i=1..] b_i 18/12 21:34 The proofs certainly wouldn't make any sense. The types might, if read as mathematical propositions. :) 18/12 21:34 now AB = sum the diagonals of the 'spreadsheet' 18/12 21:35 m it's a different spreadsheet - my one has, cell_i_j = a_i*b_j 18/12 21:36 anyway you can prove that converges even though there's "380 non enumerated elements"(!) 18/12 21:37 Ijust dont' know 18/12 21:50 Slow and steady ties the race. 18/12 22:02 wait, but if he says that his magical sequence can't be made a sequence, what should this have to do with Cantor's argument? 18/12 22:07 Because he also says that his magical sequence is "countable". 18/12 22:08 well, if he doesn't see how these two concepts are contradictory i wouldn't know how to clarify that 18/12 22:13 it's all too wordy for me 18/12 22:14 I don't think he knows what he means 18/12 22:14 (but that might just be because I can't be bothered parsing all his prose) 18/12 22:14 --- Day changed Sat Dec 19 2009 can I ask type theory questions on this channel? 19/12 04:33 as I said, #haskell works, but this would probably work too. There's just a lot more activity on #haskell 19/12 04:34 meet you at haskell then 19/12 04:37 -!- opdolio is now known as dolio 19/12 05:59 dolio: in your last post on the Cantor thread, you say (Nat -> Bool) represents the computable reals, aren't they the provably-computable reals actually?or do they concide from this point of view? 19/12 12:46 -!- pigmalion_ is now known as pigmalion 19/12 16:03 hey dolio 19/12 16:26 What about Löwenheim–Skolem 19/12 16:27 regarding http://scienceblogs.com/goodmath/2009/12/another_cantor_crank_represent.php#comment-2154030 19/12 16:27 Saizan: I guess it's probably the provably computable reals. But I'm not sure it makes much difference for the point I was making. 19/12 21:49 The provably computable reals are provably computably uncountable, the computable reals are computably uncountable, and the reals are uncountable. Whether that makes them bigger than the naturals is somewhat open to interpretation. 19/12 21:54 dolio: yeah, it wasn't important, it was mostly to confirm my understanding of agda, thanks 19/12 21:56 I hadn't really thought about reals generated by some computable function, but you can't prove that they are. But I guess that situation might come up. 19/12 21:58 Or can't prove that the function is computable, or something. 19/12 21:59 well if computable is still "there's an halting turing machine that does it" and (Nat -> Bool) members included all the computable functions then typechecking would have to solve the halting problem, i guess 19/12 22:04 Right. 19/12 22:29 "typechecking would have to solve the halting problem" 19/12 22:58 the one writing the program needs to prove termination is all 19/12 22:58 of course you can't express every computable function in agda 19/12 22:59 well, i meant in Agda as it is now 19/12 22:59 * copumpkin returns to Data.Graph.Acyclic 19/12 23:19 gah 19/12 23:30 mh DGA instead of DAG 19/12 23:33 :) 19/12 23:34 it's the hardest time I've had converting a module to UP 19/12 23:34 whoa, you can use a variable twice in a type signature 19/12 23:46 * copumpkin sighs: .e ⊔ .n != .n of type Level 19/12 23:46 --- Day changed Sun Dec 20 2009 I'm stumped 20/12 00:03 oh 20/12 00:06 I think I might know what's wrong, but am not sure how to solve it 20/12 00:12 so if I have 20/12 00:16 p i (e , j)  with i ≟ j 20/12 00:16 i is a Fin n, j is a Fin n 20/12 00:16 what could possibly make it complain that Dec (x ≡ y) !=< Level of type Set ? 20/12 00:16 whoops i == j, not x == y 20/12 00:16 soupdragon: You mean that downward Loewenheim-Skolem implies that the reals are countable? 20/12 00:41 no 20/12 00:41 The reals are not countable :P 20/12 00:41 nuh uh, I have an enumeration right here with me 20/12 00:42 but it seems like your argument about the computable reals follows a similar path 20/12 00:42 I don't believe the computable reals are countable -- just the ones you can write down 20/12 00:42 How can something be computable without being able to write down an algorithm/Turing machine/whatever to compute it? 20/12 00:43 maybe you can do it with a neural network or something (one that computes with real numbers), I don't know 20/12 00:44 Well, then you've just postulated the existence of reals that can be computed with, but not simulated by Turing machines to prove that there exist reals that cannot be simulated by Turing machines. 20/12 00:47 these computable reals are countable http://en.wikipedia.org/wiki/Computable_number 20/12 00:50 "The computable numbers can be counted by assigning a Gödel number to each Turing machine definition" 20/12 00:51 hm maybe what I am thinking of is the reals 20/12 00:51 People generally argue that there are reals (whose existence is implied by ZF, I guess) that don't correspond to any formula you could write down describing them. 20/12 00:52 Or something like that. 20/12 00:52 Where the ones you can describe are 'definable reals', I believe, and that's what Loewenheim-Skolem uses for their countable model. 20/12 00:53 But I don't think I've ever heard that about computable reals. 20/12 00:54 Or, if you want to get more restrictive, a real number datatype in Agda. Those seem obviously countable. 20/12 00:55 well I don't know about that 20/12 00:55 You could have a denotational semantics where the real numbers type is mapped to a set with uncountably many elements. 20/12 00:56 you could have agda interpret into a model where 2 -> Nat has uncountable elements 20/12 00:56 yeah :p 20/12 00:56 But syntactic models (or whatever you want to call them) seem more readily believable as "the" model for a programming language. 20/12 00:59 it's too bad that reflecting the idea that everything 'there is' can be 'written down' causes inconsistency 20/12 00:59 Than they do for a set theory. 20/12 00:59 I don't beleive in One true model 20/12 00:59 I have to agree with you that the computable numbers are countable because any definition like I was thinking about wrt. infinitary lambda calculus actually defines the real reals 20/12 01:01 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14444#a14444 :( 20/12 01:01 but a type like Nat -> 2 (which I seemed to mix up earlier) might not be 20/12 01:01 Nat -> 2 isn't "functions from Nat to 2", though, it's "(provably) computable functions from Nat to 2". 20/12 01:02 well it's not really anything 20/12 01:03 if the typechecker passes for a judgement  Gamma |- x : Nat -> 2, then  x is a computable function 20/12 01:03 copumpkin: I don't really see where the problem is. 20/12 01:05 you can pair up,   (f : Nat -> 2, code f)   that gives elements of Nat -> 2 which come from a finite coding 20/12 01:05 dolio: me neither, it makes no sense to me. All I did was add an implicit parameter for the level and parametrize the set by it. The error seems related to the decision of two Fin elements but as a context it says "in the expression w", which doesn't exist anywhere in the code 20/12 01:06 maybe w is what with desugars to? 20/12 01:06 with desugars to an auxiliary function, so maybe. 20/12 01:06 I'll try with'ing manually 20/12 01:07 Gamma |- x : Nat -> 2 is a judgment about Agda terms x. 20/12 01:09 Or something similar. 20/12 01:10 yeah (and says that gamma and Nat -> 2 are well formed also) 20/12 01:10 So in (f : Nat -> 2, code f), f is code. 20/12 01:11 manual with'ing works fine 20/12 01:12 no 20/12 01:12 I guess it's a subtle bug? 20/12 01:12 f is the interpretation of a code 20/12 01:12 Then f : Nat -> 2 doesn't make any sense, because f is not an Agda term. 20/12 01:12 it is an agda term, with type  Nat -> 2 20/12 01:13 I mean this like a Sigma 20/12 01:13 Sigma (Nat -> 2) (\f -> code f) 20/12 01:13 code : {T} -> T -> Set 20/12 01:13 '0' : code 0, 'S' : code S  etc 20/12 01:14 What does 'code' mean? Goedel code? 20/12 01:14 just like a syntax which has the interpretation built in 20/12 01:14 '\$' : code f -> code x -> code (f x) 20/12 01:14 Oh, okay, f is an Agda term, and code f is a value of an agda term representation in agda, or something. 20/12 01:16 well it's all agda terms 20/12 01:16 Where the term represented corresponds to f. 20/12 01:16 f is what's being represented 20/12 01:16 by an element of code f 20/12 01:16 Right. 20/12 01:17 bah, my message is awaiting moderator approval! 20/12 01:26 this module has another problem in it that makes no sense to me 20/12 01:38 I have a g   : Graph (Prod.Σ (Fin .n') (λ _ → N)) E .n' 20/12 01:42 my goal is 20/12 01:42 Graph (Prod.Σ (Fin (suc .n')) (λ x → N)) E .n' 20/12 01:42 so basically just incrementing the proj_1 of the pair 20/12 01:42 nmap : ∀ {ℓN₁ ℓN₂ ℓE : Level} {N₁ : Set ℓN₁} {N₂ : Set ℓN₂} {E : Set ℓN₂} {n} → (N₁ → N₂) → Graph N₁ E n → Graph N₂ E n 20/12 01:42 (ignoring the bad names for a moment) 20/12 01:43 but doing the obvious and nmap (Prod.map suc id) g fails saying Set ????? != Set 20/12 01:47 oh my, totally my own fault 20/12 01:55 * copumpkin swears a bit 20/12 02:27 <-rec in Induction.Nat forces stuff into Set :( 20/12 02:31 mostly just because of 20/12 02:32 data _≺_ : ℕ → ℕ → Set where 20/12 02:32 _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n 20/12 02:32 woah 20/12 02:32 what's that about? 20/12 02:32 weird way to define less I guess there's nothing more to it 20/12 02:33 it's used for WfRec 20/12 02:34 open WF _≺_ public using () renaming (WfRec to ≺-Rec) 20/12 02:34 this is just preventing me from using toForest, which isn't the end of the world I guess 20/12 02:35 it'll do :) 20/12 02:37 copumpkin: So, your e-mail was pretty interesting. 20/12 10:17 oh, I didn't even realize it got through. The mailing list replied to me and told me it was too big and that it was awaiting moderation 20/12 10:17 did you figure out what the problem is? 20/12 10:17 http://img85.imageshack.us/img85/8004/wowu.png 20/12 10:20 oh crap 20/12 10:20 so much for pasting code into gmail's rich text editor 20/12 10:20 * copumpkin sighs 20/12 10:21 The html version looks fine, but that's what the text version looks like. 20/12 10:21 I guess gmail felt the need to make sure the links from the html code made it through to the text version 20/12 10:22 Evidently. 20/12 10:22 is there a shorthand for implicit arguments without labels? e.g. the precondition here in evenSuc http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14495#a14495 20/12 19:56 evenSuc : ∀ n → {T (even n)} → ℕ 20/12 19:57 liek ? 20/12 19:57 ya 20/12 20:41 {T (even n)} cannot appear by itself. It needs to be the argument 20/12 20:41 to a function expecting an implicit argument. 20/12 20:41 when scope checking {T (even n)} 20/12 20:41 i guess {} with a funcall inside is ambiguous in the grammar bc it could be designated calling a function with an implicit arg explicitly? 20/12 20:44 though at the level of a type signature i wouldnt think there would be ambiguity 20/12 20:45 im using agda 2.2.4 via cabal 20/12 20:48 just give it a name, if it's complaining 20/12 20:48 {pf : T (even n)} 20/12 20:49 or something 20/12 20:49 given that the {}s are not already inside another funcall, that is 20/12 20:52 yah i did just use underscore, was just wondering if there was an alternative 20/12 21:44 underscore? 20/12 21:44 _ 20/12 21:44 lol 20/12 21:45 I know what an underscore is 20/12 21:45 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14495#a14495 20/12 21:45 I just missed the context 20/12 21:45 ah 20/12 21:45 how did you highlight the line? 20/12 21:46 enter the line number into the field below and hit the "highlight line" button 20/12 21:46 oh, smart 20/12 21:46 ;) 20/12 21:46 --- Day changed Mon Dec 21 2009 So, I was thinking about it, and I'm pretty sure denotational semantics are irrelevant to whether "Agda reals" (or whatever) are countable. 21/12 01:53 why? 21/12 01:53 Because I could use the real numbers as the denotation of the natural datatype, and everything would work, but that doesn't mean the natural datatype has uncountably many members. 21/12 01:53 oh yeah I see 21/12 01:54 What matters is how many elements of the denotational set are picked out by syntactically valid/well typed/whatever terms. 21/12 01:54 And that will always be countable. 21/12 01:54 that is certainly true 21/12 01:55 why can't there be a bijection between them though? 21/12 01:55 Unless you have uncountably many syntactically valid terms, but that'd be pretty weird. 21/12 01:55 What kind of a bijection? You can have a meta/set-theoretic bijection between the naturals and the syntax (and thus between different datatypes). 21/12 01:58 yeah but not one between N and N -> 2 21/12 01:58 which is odd 21/12 01:58 hm the existence of a bijection is okay? but an isomorphism between them is contradictory 21/12 01:59 You can have a meta-bijection between N and N -> 2, but not an Agda bijection. 21/12 01:59 I know you can't construct a bijection between them (well I think I know this) but if you postulate one, it wouldn't lead to a contradiction would it? 21/12 02:00 If you postulate one it will contradict the Cantor diagonal argument you can construct in Agda. 21/12 02:01 I mean one without the equality proofs 21/12 02:01 What would the postulate be? 21/12 02:03 I was thinking about the difference between having f and g, with f . g = id and g . f = id vs having f and g, and then saying they are both surjective (or injective) 21/12 02:04 but I guess that in the case of injectivity and surjectivity that's not really telling you about the types (N and N -> 2) but more about the definitions of injective and surjective 21/12 02:05 Anyhow, if your logic is consistent, I think you can't show that there's an enumeration N -> (N -> 2). 21/12 02:07 If you're in a language where you could enumerate and eval all programs in your language, then you'd be able to try to diagonalize it, as well, and you'd get non-termination somewhere. 21/12 02:08 So your logic would be inconsistent. 21/12 02:08 so what about the meta proof? 21/12 02:08 why doesn't that cause a problem 21/12 02:08 Because you don't have access to the meta proof within the language. 21/12 02:09 this is a paradox 21/12 02:09 it's false internally but it's true externally! 21/12 02:10 The meta-proof doesn't prove that there's an N -> (N -> 2), though. 21/12 02:11 That's a bijection, that is. 21/12 02:12 It proves that there's a meta-bijection between N and N -> 2. 21/12 02:12 if both sets are countable there's a bijection by that crazy proof with the zigzags ? 21/12 02:12 * soupdragon tries to remember its name 21/12 02:13 You'd use zigzagging to prove that NxN (or something like it) is countable, if that's what you mean. 21/12 02:14 no thinking of something else but I can't remember the name :( 21/12 02:14 I'm trying to search it out 21/12 02:14 Perhaps it'd be clearer to say that both types are meta-countable. 21/12 02:16 But N -> 2 isn't Agda-countable. 21/12 02:16 I can live with that but the question is left:   is N -> 2 countable or not? 21/12 02:16 Was Cantor an idiot and liar? :P 21/12 02:16 Cantor–Bernstein–Schroeder theorem 21/12 02:20 no wonder I couldn't remember it 21/12 02:20 doesn't that give a metabijection? 21/12 02:20 http://en.wikipedia.org/wiki/Cantor%E2%80%93Bernstein%E2%80%93Schroeder_theorem#Visualization is what I meant by the zigzag thing 21/12 02:20 Oh, that zig zagging. 21/12 02:21 Anyhow, yes, that's a meta bijection. 21/12 02:21 that wasn't some deep statement I wanted to make I didn't mean to hype it up so much it was just frustrating me that I couldn't remember the name of it 21/12 02:22 soupdragon, usually, from a second persons perspective you are either an idiot or a liar. Not that you can't actually be both at the same time, but if you are, that's not really remarkable enough to be mentioned :) 21/12 02:27 whoppix it was a joke because this guy claimed these things 21/12 02:28 I am the only one who has properly understood and refuted Cantor's argument! 21/12 02:32 this constructive math/logic makes me doubt everything 21/12 02:34 -!- opdolio is now known as dolio 21/12 05:37 -!- BlackM is now known as BMeph 21/12 18:25 --- Day changed Tue Dec 22 2009 anymore thoughts about this cantor stuff? 22/12 03:52 "Since we can circle around the spreadsheet starting it the middle and making gradually larger and larger loops, we can map each and every cell onto N. This means that our spreadsheet is countable, and thus the irrationals themselves are countable." 22/12 03:55 hehe 22/12 03:55 gah 22/12 03:55 :p 22/12 03:55 :) 22/12 03:55 he's cute I like him 22/12 03:55 29 Comments fffffffffffffff 22/12 03:56 wait, which instance are you referring to? 22/12 03:57 http://theprogrammersparadox.blogspot.com/2009/12/crank-it-up.html 22/12 03:57 thanks 22/12 03:57 oh this is a different guy 22/12 03:58 I might send him an email 22/12 03:58 I love his rigorous proof that his spreadsheet contains them all 22/12 03:59 "It looks like sqrt(2) will be somewhere in the bottom left quadrant." 22/12 04:01 well that is intuition 22/12 04:01 I think his argument is wrong but his philosophy is tending toward something quite acceptable 22/12 04:02 "1. By definition the spreadsheet ONLY contains irrationals." 22/12 04:02 oh okay! 22/12 04:02 :) 22/12 04:02 I just wish he'd address where diagonalization goes wrong, since regardless of how he constructs his crazy spreadsheet and spirals, he's eventually going to get an enumeration of the reals, which cantor just can't wait to smack down with a baseball bat 22/12 04:04 What I think is important is not the formal mathematics 22/12 04:05 we can check it on a computer, or we could get a thousand people to check it by hand and everyone would accept it 22/12 04:05 but what do the proofs mean? 22/12 04:06 How does that contain all the irrationals? It only generates the irrationals derivable in a finite number of various operations on pi. 22/12 04:07 that seems to be a recurring theme of these arguments 22/12 04:08 Which appear to be either multiplying or dividing by 10, and adding 10^m for some m. 22/12 04:08 at least, the other dude on the knol seemed to make a similar assumption 22/12 04:08 Actually, it's not even a finite number of steps, it's just doing either of those once. 22/12 04:09 First you add 10^m (for switching columns) and then you multiply by 10^m (for changing rows). 22/12 04:10 Er, 10^n. 22/12 04:10 Not necessarily the same number of course. 22/12 04:10 Wait, I'm wrong again, the additions are cumulative. 22/12 04:11 I feel that the Knol guy is just a bastard that is making money by posting bullshit 22/12 04:12 "Yep. I'm claiming that N to N is a bijection, but N to NxN is only injective. Well, if you don't care that NxN is growing faster than N, then you might assume it's a bijection (but I still imagine it to be wrong)." 22/12 04:12 particularly his "nananana I am not listening" attitude 22/12 04:12 "I did. The diagonal argument works perfectly fine with a sequence. It is invalid, however, when used on a magic sequence. " 22/12 04:13 * copumpkin coughs 22/12 04:13 QED 22/12 04:13 The guy can't be argued with. 22/12 04:22 People have pointed out specific numbers that aren't in his spreadsheet, and he just ignores them. 22/12 04:22 people also ask him to show that the diagonal argument fails on his spreadsheet-generated sequence 22/12 04:23 Yes, I know, and he doesn't appear to understand how to apply the argument to them, despite multiple descriptions, so I don't think there's much hope of reaching him that way. 22/12 04:24 I explained multiple times and wrote a program that did it, and proved that it did it. 22/12 04:24 I'm just amazed at these people who appear to think that they can disprove a century of mathematicians with knowledge they've picked up from a couple of math books and wikipedia 22/12 04:25 Nobody's thought of two dimensional sheets of numbers in 100 years. 22/12 04:44 hey, this one extends to infinity in all four directions! 22/12 04:44 it's magic 22/12 04:44 you guys are mean :p 22/12 04:45 I just love "Yep. I'm claiming that N to N is a bijection, but N to NxN is only injective. Well, if you don't care that NxN is growing faster than N, then you might assume it's a bijection (but I still imagine it to be wrong)." 22/12 04:45 as I said, he seems to be implying that the reals are actually uncountable, but not because rationals are countable and irrationals are uncountable, but because rationals are uncountable and irrationals are countable 22/12 04:46 Some of his objections make sense for ordinals but not cardinals. 22/12 04:51 Like, omega*omega is bigger than omega. 22/12 04:51 yeah, but that's not original or particularly relevant, is it? 22/12 04:52 not that I should really be speaking as I'm almost as clueless as he is about math :) 22/12 04:52 Well, you don't use ordinals to count how many things are in a set, so no. 22/12 04:53 If you use the standard ordinals-are-sets encoding, then omega*omega has as many elements as omega. 22/12 04:55 Despite the first being a bigger ordinal. 22/12 04:56 I guess that means there's not a bijection between the ordinals and the cardinals? :) 22/12 04:57 Neither of those are sets, so I don't really know if you can even talk about bijections between them. 22/12 04:58 At least, I doubt there's a set of cardinals. I know there isn't a set of ordinals. 22/12 04:58 well, you could make a category of them with functions on them, I guess 22/12 04:59 nimbers seem to make ordinals 22/12 04:59 usable 22/12 05:00 * soupdragon titters 22/12 05:09 you should sign up for a titter account and teet your random thoughts :) 22/12 05:09 I'm smirking at this http://www.reddit.com/r/math/comments/ahb9l/the_diagonal_argument_works_perfectly_fine_with_a/ 22/12 05:10 I wonder who posted that O:-) 22/12 05:10 The god of your categorical dual, evidently. 22/12 05:10 Is the math reddit worth looking at regularly? 22/12 05:11 dolio if you want new and exciting ways to cut bagels 22/12 05:11 I only check it every few days 22/12 05:11 Well, I mean, is it more like the Haskell one, or the programming one? 22/12 05:12 http://www.reddit.com/r/haskell/comments/afj53/224_epilogue/ 22/12 05:13 "Bertrand Russell would feel vindicated." funny 22/12 05:13 probably more like programing with things like "yo, teach me math" 22/12 05:13 Yes, did epigram achieve that result faster or slower than principia mathematica? :) 22/12 05:14 difficult to say :P 22/12 05:15 http://www.reddit.com/r/dependent_types/ 22/12 05:19 that's the best reddit 22/12 05:19 lol 22/12 05:19 didn't you already say you thought that one was super boring? :P 22/12 05:20 Are you sure it's better than /r/types? :) 22/12 05:20 we could start an /r/agda for the ultimate idle subreddit 22/12 05:21 http://www.reddit.com/r/math/comments/ahb9l/the_diagonal_argument_works_perfectly_fine_with_a/c0hken3 22/12 05:23 hmm guys you know what?  I think I just disproved cantors theorem! 22/12 05:25 nice! 22/12 05:25 Which one? 22/12 05:25 all of them 22/12 05:25 "Ok. The existence of cranks is a fact that weights heavily upon me-- I guess I just don't have the constitution to accept that there are people smart enough to be that dumb. That man apparently writes code for a living-- surely he would be capable of wading through the relevant wikipedia article before humiliating himself before millions. The real math isn't even any harder than the fake math!" 22/12 05:26 that's an interesting comment 22/12 05:26 I like the comment I linked to. I think an argument like that (showing that all his irrationals are of a restricted form) is most likely to convince the crank. 22/12 05:32 likely to convince the crank?? haha 22/12 05:32 well, assuming he's at all rational :) 22/12 05:32 I'm sure he's now moved into defensive mode though 22/12 05:32 any argument against him is just conventional mathematicians not being able to step out of their box 22/12 05:33 If he doesn't believe Cantor's diagonal argument, you'll think he'll accept that pi is transcendental? 22/12 05:33 I don't even know how to prove that. 22/12 05:33 I guess not, but it's a lot more intuitive that it might be true 22/12 05:33 me neither 22/12 05:33 than cantor 22/12 05:33 hey why is pi trancendental?? 22/12 05:33 oh, I don't know how to prove it :) 22/12 05:34 'This was proved by Ferdinand von Lindemann in 1882' 22/12 05:34 it just seems a lot easier to accept that it's not going to be a zero of a polynomial 22/12 05:34 'An important consequence of the transcendence of π is the fact that it is not constructible. Because the coordinates of all points that can be constructed with compass and straightedge are constructible numbers, it is impossible to square the circle' 22/12 05:35 hey dolio I like where you are going with this! 22/12 05:35 maybe I'm just drinking the kool aid though 22/12 05:35 since pi is not trancendental we can actually construct it, and square the circle 22/12 05:36 Heh. 22/12 05:37 In 1873, Hermite proved that the constant e was transcendental. Combining this with Euler's famous equation e^(i*π)+1=0, Lindemann proved that since e^x+1=0, x is required to be transcendental. Since it was accepted that i was algebraic, π had to be transcendental in order to make i*π transcendental. 22/12 05:38 that seems like an argument that could be made rigerous 22/12 05:38 rigorous 22/12 05:38 Yeah, but that just reduces to proving e is transcendental. How do you do that? 22/12 05:38 http://en.wikipedia.org/wiki/Transcendental_number#Sketch_of_a_proof_that_e_is_transcendental 22/12 05:39 http://snapplr.com/5t82 22/12 05:39 That's a weird way of describing the operation. 22/12 05:41 it's a shorthand 22/12 05:41 I just thought it was amusing when taken out of context 22/12 05:41 Now that proof would not be easy to formalize. 22/12 05:45 i wonder if there's proofs in CoRN 22/12 05:45 they might be different 22/12 05:45 universe polymorphism still messes with my mind 22/12 08:03 Yeah? 22/12 08:10 things like the empty type in a higher universe 22/12 08:11 when it's appropriate to make something polymorphic or not 22/12 08:11 I wouldn't bother with the empty type in a higher universe. 22/12 08:12 If you need that, you probably want something else in actuality. 22/12 08:12 yeah, that's what I figured 22/12 08:12 is there an obvious connection to logic in UP? 22/12 08:13 Some operation to take things in universe i and put it in universe i+1. 22/12 08:13 UP? 22/12 08:13 universe polymorphism 22/12 08:13 I'm not aware of a connection. 22/12 08:15 what's the question ? 22/12 08:16 looking for a logical interpretation of polymorphism? 22/12 08:16 yeah 22/12 08:16 Universe polymorphism. 22/12 08:17 universe polymorphism, that is 22/12 08:17 I just consider it as denoting a whole family of definitions rather than a single one 22/12 08:17 well, even ignoring the polymorphism aspect of it, what are higher universes in logic? 22/12 08:18 Actually, there was something about a set theory with universes on the n-category cafe not too long ago. 22/12 08:19 Specifically about an axiom where 'if you prove P in some universe, P' which is derived from P by substituting some stuff holds in all universes', which is rather like universe polymorphism. 22/12 08:20 But not precisely analogous to Agda's version of it. 22/12 08:20 ah 22/12 08:20 The axiom is intended to solve similar problems, though. 22/12 08:22 The 'universes' in question are sets that are closed under various operations, such that they behave a lot like 'all sets'. 22/12 08:22 And then you can have 'every set belongs to some universe' as an axiom in your set theory, which is kind of nice. 22/12 08:23 But then anything you prove about a universe applies only to that universe, even if it might be identical to theorems about some other universe. 22/12 08:24 http://golem.ph.utexas.edu/category/2009/11/feferman_set_theory.html 22/12 08:27 I don't know why I even load these pages 22/12 08:28 I can't understand anything on any of them 22/12 08:28 :[ 22/12 08:28 I like the ncatlab wiki 22/12 08:34 * copumpkin looks forward to understanding more than the first couple of lines on that blog 22/12 08:36 * copumpkin gets back to attempting proof : ∀ {A B} (a : A) → (xs : Colist⁺ A) → a ∈ xs → (y : B) → (f : A → Colist⁺ B) → y ∈ f a → y ∈ diagMap f xs 22/12 08:38 "the really interesting crackpots are the ones trying to really, seriously do science, because their productions and their failures tells us important things about science itself" Yes! 22/12 08:49 Bullseye 22/12 08:49 That's a good article. 22/12 08:50 gah, this is ridiculously complicated, just because of that nasty codata intermediate language 22/12 08:59 well, maybe not just because 22/12 08:59 but it is a real pain to even figure out what my goals are given the codata output 22/12 09:01 what's the point of proving this.. 22/12 09:04 for the fun of it, really 22/12 09:04 can you show me the diagMap code? 22/12 09:04 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14829#a14829 :( 22/12 09:05 ah well you can probably start by proving the equations you would have liked to define the function with then? 22/12 09:06 how do you mean? 22/12 09:06 actually that doesn't really help anything, never mind that 22/12 09:07 wow, I can't even prove diagonal-singleton : ∀ {A B : Set} → (x : A) → (y : B) → (ys : Colist⁺ B) → y ∈ ys → y ∈ diagonal [ ys ] :( 22/12 10:27 I guess it would help if I could figure out what the | notation meant in a type 22/12 10:27 i think (foo | bar) just means that to reduce foo further you've to pattern match against bar 22/12 10:28 what if I have three of them? 22/12 10:29 oh, they're nested 22/12 10:29 so I have 22/12 10:31 whnf (map [_] (fromColist⁺ zs)) | (whnf (fromColist⁺ zs) | ♭ zs) 22/12 10:31 i guess map does case analysis on the whnf of its argument? 22/12 10:33 yeah 22/12 10:34 map is actually a constructor :P 22/12 10:35 hah 22/12 10:41 whnf is an evaluator for it 22/12 10:41 hmmm 22/12 10:42 whnf (stripeDiagonal [ ♭ zs ]) != 22/12 10:47 whnf (map [_] (fromColist⁺ zs)) | (whnf (fromColist⁺ zs) | ♭ zs) of 22/12 10:47 type DiagonalW (List⁺ .B) 22/12 10:47 that's my type error 22/12 10:47 i guess you've to prove stripeDiagonal [ ♭ zs ] \== map [_] (fromColist⁺ zs) 22/12 10:49 hmm, okay 22/12 10:51 I really like the splitter 22/12 10:53 pity it can't know everything :( 22/12 10:53 C-c C-c ? 22/12 10:54 yeah 22/12 10:54 they don't appear to be equal :o 22/12 11:02 I guess I need to prove the whnf is equal 22/12 11:02 not the constructors themselves 22/12 11:02 lol 22/12 11:05 http://snapplr.com/hxpx 22/12 11:05 pretty deep proof 22/12 11:05 doesn't appear to be possible to simplify further though :)_ 22/12 11:06 http://snapplr.com/yca6 says the same thing, I guess 22/12 11:07 gah 22/12 11:14 I always have the hardest time getting the first parameter to subst right 22/12 11:17 so if I use the original term in the proof, it complains about the error I wrote above 22/12 11:20 so I proved that they are equal 22/12 11:20 now I use a subst that uses the proof I wrote 22/12 11:20 and I can't figure out my first term 22/12 11:21 BAH 22/12 11:39 Having fun monologuing? 22/12 11:44 yeah, it's awesome 22/12 11:44 maybe this isn't a subst 22/12 11:53 mh, sometimes i need to subst in different directions different parts of the type with the same equality 22/12 11:55 well I'm sort of moving along the list and need to show that if it isn't in the head, it's in the tail 22/12 11:57 but proving that it's in the tail means recursing and proving it's in the tail (which doesn't match the original type sig) 22/12 11:57 -!- copumpkin_ is now known as copumpkin 22/12 12:08 yay, finally 22/12 12:22 * copumpkin kicks himself a thousand times 22/12 12:22 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14834#a14834 22/12 13:45 neat 22/12 13:46 BUILTIN pragmas are quite a bit more lenient than I might expect. 22/12 13:53 hm, nested with blocks seem to behave strangely 22/12 14:08 i was being able to nest them only on the last case matched 22/12 14:20 *i've been 22/12 14:21 I'm actually getting somewhere with this monster 22/12 14:49 slowly and unsurely 22/12 14:49 Saizan: how do you mean? 22/12 16:00 it's telling me I have repeated variables where I see none :( 22/12 16:00 oh nevermind 22/12 16:02 -!- copumpkin_ is now known as copumpkin 22/12 16:04 how can I convince agda to evaluate my expression a little more deeply? 22/12 16:13 Goal: [ y ] ∷ stripeDiagonal (♭ zs') ≡ 22/12 16:13 (whnf (zipCons (fromColist⁺ ys') (stripeDiagonal (♭ zs'))) | [ y ] 22/12 16:13 | q) 22/12 16:13 that whnf (zipCons ... stuff can be simplified further 22/12 16:13 there's C-c C-n 22/12 16:17 yeah, but this is in my goal 22/12 16:17 I need it to evaluate it more because if it does that, it'll see that the expressions are a lot closer than they look 22/12 16:17 well, you can ask it to normalize what's in your goal, if you C-c C-n from an hole you get its scope 22/12 16:20 oh 22/12 16:20 hm, didn't normalize any further 22/12 16:20 I wonder what's stopping it 22/12 16:20 don't you love it when one of the lemmas you built your proof on turns out to be wrong 22/12 16:42 Goal: [ [ x ] ] ≡ [ y ∷ [ x ] ] 22/12 16:43 now to find out how far back the mistake goes :/ 22/12 16:45 agda needs quickcheck, to help you get a quick idea of whether the statement you're trying to prove makes sense at all 22/12 16:48 nice idea 22/12 16:53 GAH termination checker I hate youu 22/12 17:02 oh termination checker I love you 22/12 17:02 weird how filling in a hole can convince it you terminate :O 22/12 17:03 -!- Berengal_ is now known as Berengal 22/12 17:22 gah, it can't figure out that one of my lemmas terminates 22/12 17:28 luqui: I'm almost done proving that the my monstrous translation of your omega code does in fact have the important property 22/12 18:03 wow, nice work 22/12 18:03 i tried my hand on it for (Nat ->)s 22/12 18:04 and it was... hard 22/12 18:04 did that work? 22/12 18:04 well, i think it would have 22/12 18:04 but my proof-fu was not strong enough 22/12 18:04 ah 22/12 18:04 this representation is really tedious, due to all the ugly codata and the intermediate language 22/12 18:04 are you using colists.  i.e. ones with nil? 22/12 18:05 yeah 22/12 18:05 yeah ouch, i can see that being a bear 22/12 18:05 it's not quite as general as omega 22/12 18:05 diagonal : ∀ {a} → Colist⁺ (Colist⁺ a) → Colist⁺ a 22/12 18:05 hm?  why? 22/12 18:05 I force the lists to be non-empty 22/12 18:05 ah 22/12 18:05 yeah that's a good point, you get _|_ if you have an infinite list of empty lists 22/12 18:06 allowing nil lists would have to take an additional assumption ensuring productivity 22/12 18:06 yeah :/ 22/12 18:06 so i think it's a good compromise 22/12 18:06 yeah, wasn't sure how to represent productivity explicitly 22/12 18:07 in a convenient manner, anyway 22/12 18:07 yeah without referencing the very same stuff diagonal is doing 22/12 18:08 maybe if I get this working I'll move back to my language enumerator module 22/12 18:09 oh that's what you're using it for? 22/12 18:09 that's what my original motivation was, but then I figured it'd be handy for other things too 22/12 18:10 hmm, using this proof you can prove that you do in fact enumerate all strings of the language 22/12 18:10 neat 22/12 18:10 yeah 22/12 18:10 that is getting into the realm of the nontrivial :-) 22/12 18:10 I hope I succeed! currently I'm trying to rewrite one of my lemmas because agda thinks it doesn't terminate :( 22/12 18:10 oh, that has never happened to me 22/12 18:11 (sarcasm) 22/12 18:11 :P 22/12 18:11 hmm, or maybe I'll leave my nonterminating lemma alone and try to fill in one of the few remaining holes 22/12 18:12 decisions decisions! 22/12 18:13 -!- BlackM is now known as BMeph 22/12 18:42 omg BMeph in #agda 22/12 18:52 it sure would be nice to have rebindable list literals 22/12 19:01 testlist = (1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ [ 4 ]))) ∷ ♯ ((5 ∷ ♯ [ 6 ]) ∷ ♯ [ 7 ∷ ♯ [ 8 ] ]) 22/12 19:01 damn, the lemma I'm trying to prove doesn't appear to be true either :P 22/12 19:06 the thing i like about proof checkers is that a lot of times my frustrations with its refusal to typecheck my code are cured by finding out that what i'm trying to prove is false :-) 22/12 19:15 I was doing it wrong, I was trying to show unequal things were equal when in fact what they have in common is that something is an element of both 22/12 19:23 * copumpkin yawns 22/12 19:30 I'm getting annoyed at emacs stealing my focus every time I load a file 22/12 19:35 speaking of other languages, does anyone know about trellys? 22/12 20:08 I'm finding no information besides the grant 22/12 20:08 gah, I was hoping to finish this proof today but I'm getting sleepy now :( 22/12 20:43 what is being proved? 22/12 20:55 I translated http://hackage.haskell.org/packages/archive/control-monad-omega/0.2/doc/html/Control-Monad-Omega.html to agda and am proving that the traversal has the desired properties 22/12 20:57 is there any essential laziness? 22/12 21:02 well, it's infinite 22/12 21:02 hmm 22/12 21:02 so I have to use codata which could be seen as laziness 22/12 21:03 what's your theorem? 22/12 21:03 diagMap-proof : ∀ {A B} (a : A) → (xs : Colist⁺ A) → a ∈ xs → (y : B) → (f : A → Colist⁺ B) → y ∈ f a → y ∈ diagMap f xs 22/12 21:03 how's that unicode supposed to work? 22/12 21:03 napping: trellys is still in the early going 22/12 21:03 napping: oh, doesn't it show up for you? 22/12 21:04 napping: but I believe aaron stump has a draft paper out with some of the ideas under consideration 22/12 21:04 ccasin: I was hoping to find a mailing list or something 22/12 21:04 copumpkin, i assume you have tried proving it for join 22/12 21:04 napping: only internal stuff at this point 22/12 21:04 I just see \uXXXX 22/12 21:04 luqui: I actually just used that, so the proof for diagMap is one line 22/12 21:05 http://snapplr.com/1c5g 22/12 21:05 the diagonal proof is fairly large, and I'm still working on one of its lemmas 22/12 21:05 okay cool.  that's how i would have gone about it too... 22/12 21:05 ah, so you can map over diagonal? 22/12 21:06 I started out with diagMap directly and that proved to be even more of a nightmare :) 22/12 21:06 yeah, diagMap is like a fair concatMap 22/12 21:06 are you having problems with extensionality? 22/12 21:07 not really, mostly my problems are related to having to see through the metalanguage and codata 22/12 21:08 in fact, I've never really needed extensionality 22/12 21:13 unless I did and just didn't realize it :) 22/12 21:13 well, sometimes it's hard to prove a = b and you have to just go for bisimulation 22/12 21:13 yeah 22/12 21:15 bedtime :) more on this tomorrow! 22/12 21:16 ccasin: is the draft online somewhere? 22/12 21:24 napping: at aaron's website 22/12 21:25 http://www.cs.uiowa.edu/~astump/ 22/12 21:25 its the one about equality reflection 22/12 21:26 ah, so it's like OTT? 22/12 21:27 I was wondering what was specialy about the language, figured it was something like that, or stuff about controlling memory more directly 22/12 21:28 napping: honestly, I haven't read it yet, just read the conversation on the mailing list 22/12 21:28 the specifics of the language haven't been decided on yet, at this point we have a bunch of ideas and are trying them out 22/12 21:29 (I'm a grad student on the project) 22/12 21:30 but, yeah, it's trying to solve some of the same problems as OTT 22/12 21:30 the question is, why a new language? 22/12 21:32 the ones out there don't do everything we want! 22/12 21:32 coq is too hard to program in, agda too hard to reason in, etc 22/12 21:32 or, which reasons motivate the language 22/12 21:32 Coq has some nice stuff. A tactics language is a pretty handy thing to have 22/12 21:36 I'd be really interested if you have a story for systems programming 22/12 21:36 yes, but coq has problems too.  In particular, it's terrible to program in - two reasons come to mind immediately: 22/12 21:37 first, dependent pattern matches are a mess, the programmer is expected to write down too much 22/12 21:37 or less ambitiously - some way to treat termination as an effect 22/12 21:37 second, it's too strict about termination, programmers need to be able to write nonterminating functions and work with functions which may or may not terminate 22/12 21:38 also it has all the equality reasoning problems that upset the OTT people 22/12 21:38 yeah, that sounds about right 22/12 21:38 tactics are nice for reasoning though - the trellys idea is to support multiple external languages, one of them could be a tactic language 22/12 21:39 --- Day changed Wed Dec 23 2009 * edwinb has heard sadly little about trellys 23/12 00:00 as far as reasoning goes, what I'd really like is to never have to do any... so I'd quite like a way of plugging in decision procedures. 23/12 00:04 * edwinb realises he's joining in 2 hours late ;) 23/12 00:04 edwinb: so that means you're confident that these decision procedures could be smart enough for most cases? 23/12 00:08 No 23/12 00:08 just that most of the time I find myself having to do a proof, I keep thinking it'd be easier to write a program to make the proofs 23/12 00:09 because it's usually just a bit of list associativity, or arithmetic mangling, or similar 23/12 00:10 yeah 23/12 00:10 a nice thing about Coq is that a lot of that just goes away 23/12 00:10 it's a pity about the dependent pattern matching ;) 23/12 00:10 i guess using reflection in agda isn't near as nice 23/12 00:12 I'm sure it could be eventually 23/12 00:13 as soon as someone gets annoyed enough with doing proofs to make it nice... ;) 23/12 00:13 heh, as i see it you'd need some compiler support to reify the goal at least 23/12 00:15 you'd need a bit of magic to help you, yes 23/12 00:16 hmm, not sure how to break up this part of my proof to a point where it becomes manageable 23/12 05:15 Goal: (x ∈ concat (sd ∷ .Diagonal.♯-0 (q ∷ sd) sds)) 23/12 05:31 I realize that the .#-0 means that it's codata living in #, but what's the -0? 23/12 05:31 there seems to be no documentation whatsoever on how it shows codata 23/12 05:49 agda's being mean to me 23/12 07:23 Well, lovely as that conat-indexed family of countable types is, I don't think it works so great for a lot of operations. 23/12 07:50 like what? 23/12 07:50 Well, type-preserving successor requires rebuilding the whole value, for instance. 23/12 07:52 Lots of stuff might be okay if you just work with || omega ||, but making it work on arbitrary stuff does a lot of extra work. 23/12 07:52 Rebuilding for successor means + is like O(n * (m + n)). 23/12 07:54 I really wish Agda could do binders with its mixfix, too. 23/12 07:55 I shed a tear each time I write "∃ λ n". 23/12 07:55 yeah :/ 23/12 07:57 submit a feature request maybe? 23/12 07:58 not really sure how the syntax would look 23/12 07:58 Just "∃ n" or even "∃ n : T". 23/12 08:00 Coq can do it, but I'm sure it's not a trivial change to the parser. 23/12 08:01 Maybe something could be done with a BUILTIN sigma declaration. 23/12 08:06 Because sigma and exists are the ones that really grate on me. 23/12 08:06 I'm not dying to use W, for instance. 23/12 08:09 -!- copumpkin_ is now known as copumpkin 23/12 10:23 -!- copumpkin_ is now known as copumpkin 23/12 11:20 -!- copumpkin_ is now known as copumpkin 23/12 12:17 -!- copumpkin is now known as c0w_____________ 23/12 15:11 -!- c0w_____________ is now known as copumpkin 23/12 15:13 -!- copumpkin_ is now known as copumpkin 23/12 16:57 grrrrr he didn't reply! "cranks don't respond to other cranks" I must be a crank 23/12 16:59 you posted a comment? 23/12 17:02 I sent an email 23/12 17:02 oh 23/12 17:03 -!- Saizan__ is now known as Saizan 23/12 21:46 -!- BlackM is now known as BMeph 23/12 21:52 I guess we scared that crank back into his hole 23/12 23:00 no :) 23/12 23:01 or he realized he was wrong and doesn't quite know how to respond to people 23/12 23:01 oh did he reply to your email? 23/12 23:01 yeah 23/12 23:02 are we all just stuck in the box conventional mathematics has built around us? 23/12 23:03 who isn't? 23/12 23:05 he isn't! 23/12 23:05 everyone is 23/12 23:06 "Thank you for the email. It arrived just in time to keep me from giving up." 23/12 23:11 :o 23/12 23:12 you encouraged him? 23/12 23:12 I wouldn't say that 23/12 23:14 I guess it's good to have people questioning what's accepted 23/12 23:14 but it's best if you understand what you're calling bullshit before you call it bullshit 23/12 23:14 I want to reply to him but I think I'd need another brandy to do so :P 23/12 23:15 hah 23/12 23:15 he says that he is a platonist (in other words), which makes me wonder what sort of philosophy most computerologists are 23/12 23:21 that intuitionism.org site is excellent but what about the other folks? 23/12 23:21 might be the problem actually 23/12 23:28 if there's a fundamental truth that exist out there, then formal proof is irrelevant 23/12 23:28 mh, it'd be nice to have some theory to talk about transactions (to e.g. reason about STM code) 23/12 23:38 Saizan IIRC there's a bit on that in Ynot 23/12 23:39 * Saizan googles 23/12 23:40 --- Day changed Thu Dec 24 2009 -!- copumpkin_ is now known as copumpkin 24/12 01:19 http://speculativeheresy.wordpress.com/2008/11/26/the-semantic-apocalypse/ 24/12 05:31 still on this 'crank' stuff 24/12 05:31 thanks to dolio :P 24/12 05:31 "arguing that the results of neuroscience have far more radical implications for philosophy, the subject, and meaning than any poststructuralist critique." Heh, there's a shocker. 24/12 06:54 -!- copumpkin_ is now known as copumpkin 24/12 19:53 --- Day changed Fri Dec 25 2009 -!- copumpkin__ is now known as copumpkin 25/12 00:10 hi dolio 25/12 00:11 Hi. 25/12 00:34 I hate the misuse of = :( 25/12 00:34 http://theprogrammersparadox.blogspot.com/2009/12/cantors-lost-surjection.html 25/12 00:35 it's the worst thing anyone can do 25/12 00:35 Oh geeze. You're reading his blog now? 25/12 00:35 Oh geeze?? this is your fault :P 25/12 00:36 You gotta know when to hold 'em, know when to fold 'em. 25/12 00:37 I thought I got somewhere with my email but he's still writing complete bullshit like "countable != countably infinite" 25/12 00:37 Well, technically, countable can mean finite, as well. 25/12 00:37 the meaning doesn't matter 25/12 00:38 it's the syntax he used that make me want to strangle him 25/12 00:38 Heh. 25/12 00:38 you don't just write:   cats = good 25/12 00:38 also he seems to have learned 'logic' or .. soemthing, from Hofstaders books -- so no wonder he writes this fucking nonsense 25/12 00:39 Yeah, he started that over on good math, bad math. 25/12 00:40 I thought it was a bad sign. 25/12 00:40 At some point he said something like "magic sequences are like strange loops, and strange loops are very confusing to people." 25/12 00:41 especially to Cantor 25/12 00:41 :D 25/12 00:41 Anyhow, I think he's off the mark on the "you're a crank" diagnosis. That isn't a kneejerk reaction. 25/12 00:48 Chu ? 25/12 00:49 It's the conclusion from people telling him he's wrong, telling him why he's wrong, and him continuing to insist on being wrong. 25/12 00:49 oh right 25/12 00:50 I was never really interested in the technical content of what any of these folk are writing 25/12 00:50 This one makes even less sense to me. 25/12 00:50 He agrees that countable sets can be in bijection with subsets of themselves. 25/12 00:50 But he still doesn't agree that you can have a bijection between NxN and N. 25/12 00:51 I gave him a really  nice bijection between Q and N 25/12 00:51 which he understands, I'm sure 25/12 00:52 How'd you do it? Trees? 25/12 00:52 The NxN zig-zagging one has problems since the rationals are a quotient. 25/12 00:54 since he hacks code I wrote about how the elements of N have a binary representation (obvious), and how Q does too (record traces of inverting the euclidean algorithm, to get pairs of numbers with gcd 1) -- since they all have binary representations they're in bijection 25/12 00:54 Then I said how any computer representation of R will be binary too :D 25/12 00:55 Ah. 25/12 00:55 so there's this nuance: computables vs the real reals 25/12 00:56 Yes, that's true. 25/12 00:56 can you biject NxN into N via binary? 25/12 00:58 like interleaved digits or something hm 25/12 00:58 That actually sounds much easier than zig-zagging. 25/12 00:58 Oh, but wait, NxN always has an even number of digits. 25/12 00:59 Er, bits. 25/12 00:59 Or, no, it doesn't. 25/12 00:59 And that's a problem. 25/12 00:59 You have to encode the size of each natural somehow. 25/12 01:00 maybe it's easier to understand countability as generated by grammars 25/12 01:00 if you pad with zeros I think it screws up the canonicity 25/12 01:01 Padding the first (second) element with zeros would get you a leading zero. 25/12 01:04 You could tack a leading 1 on, though. 25/12 01:04 (m,n) = 1(interleave (pad m) (pad n)) 25/12 01:05 That probably isn't surjective, though. 25/12 01:05 But, it's injective, and you can easily make an injection in the other direction, like m -> (m, 0). 25/12 01:07 And then use that 3-name theorem. 25/12 01:07 damn!! 25/12 01:08 Cantor-Bernstein-Schroeder 25/12 01:08 * soupdragon wants to whack him over the head with Conceptual Mathematics a few times, then with Sets for Mathematics 25/12 01:13 maybe finish him off with Coq'Art (hardback edition) 25/12 01:13 The guy in the comments of this one is giving some pretty thorough set theory notes. 25/12 01:13 boo down with set theory 25/12 01:13 "You'll notice that at no point does the diagonal argument "claim" to be correct. It simply is correct" 25/12 01:16 T1 starts a landslide in set theory. And given that it is a theory that contradicts it's own axioms, it is not a reasonable theory in mathematical terms. 25/12 01:20 oh right he's claimed ZF(C?) inconsistent 25/12 01:21 I don't imagine C is necessary. 25/12 01:21 It hasn't come up, at least. 25/12 01:21 damn I don't know how to reply to this 25/12 01:24 the writing style is such a mess and the syntax is fucked 25/12 01:24 I wouldn't bother. 25/12 01:24 what's a polite way to say 'don't use = when you mean is or I will rip you to bits with my claws' 25/12 01:27 http://www.bitcount.ca/ 25/12 01:30 that's his company 25/12 01:30 it's about COMPLEX software development :D 25/12 01:30 I've been wasting all my time trying to make things simple 25/12 01:31 he's published a book ... http://www.lulu.com/content/1054566 25/12 01:32 He doesn't seem to think that {a1, a2, a3, ..., b1, b2, b3, ...} can be put into correspondence with the naturals, either. 25/12 01:32 But that's just the union of two countable sets. 25/12 01:33 But {1, 3, 5, ...} and {2, 4, 6, ...} are countable, and their union is N. 25/12 01:33 And he agrees that N can be put into 1-to-1 correspondence with subsets of itself. 25/12 01:33 well {a1, a2, a3, ..., b1, b2, b3, ...} isn't anything 25/12 01:34 It's intended to be the union of {a1, a2, a3, ...} and {b1, b2, b3, ...} 25/12 01:34 maybe 25/12 01:35 I don't really bother to try and understand this stuff, it's all nonsense anyway 25/12 01:35 I think the guy in the comments is on to something about (N, <) and order isomorphisms. 25/12 01:36 In that, the guy seems to switch between thinking about ordinals and about cardinals as it suits whatever point he's making. 25/12 01:37 probably a screwball :P 25/12 01:38 {a1, a2, a3, ..., b1, b2, b3 ...} looks like a depiction of omega + omega. 25/12 01:39 And his magic sequences were omega*omega. 25/12 01:42 I don't know what to say about "magic sequences" 25/12 01:47 misconstrued sequences 25/12 01:47 http://muaddibspace.blogspot.com/2009/12/zfcs-probably-inconsistent.html 25/12 01:52 I think I give up on this cantor stuff now 25/12 01:52 * soupdragon realized.. nothing else to do 25/12 02:04 Hmm. It's easy enough to define a set in Agda: it's a function from whatever you're interested to Bool. 25/12 04:04 uorygl, well that's  not a set theory set, but it is a set in some sense 25/12 04:04 Right. 25/12 04:04 An ordinal number can be defined as a set of ordinal numbers satisfying a certain property. 25/12 04:04 (Bye bye, positivity!) 25/12 04:04 wait 25/12 04:05 that definition doesn't make sense to me 25/12 04:05 suppose O : Set, is the type of ordinals 25/12 04:05 maybe  zero = const false : O -> Bool  is the zero ordinal? 25/12 04:06 Yep. 25/12 04:06 sort of need to solve the domain equation O = O -> Bool,  i.e. O is closed by powerset? 25/12 04:06 Well, it's not O -> Bool. It's the dependent product of that with something. 25/12 04:07 A subset of O -> Bool. 25/12 04:07 hm 25/12 04:07 That isn't a very useful definition, though, because you need operations on sets that you don't get for O -> Bool. 25/12 04:08 Like, 1 = {0}, but you can't write "one (const false) = true ; one _ = false". 25/12 04:09 Aww. 25/12 04:10 Well, you can determine whether an ordinal is zero or not by passing zero to it. 25/12 04:11 one x = not (x zero) 25/12 04:11 I think you can define all the finite ordinals that way. two x = not (x one); three x = not (x two); . . . 25/12 04:13 the problem with  X -> Bool  is that you have decidible membership 25/12 04:13 You can't define omega that way, though; there's no way to tell that omega is not finite. 25/12 04:14 Also, I feel a paradox coming on. 25/12 04:15 I'll make you a cup of honey and lemon 25/12 04:16 Let top x = true. This defines a transitive set, and its domain is the ordinals, meaning it's an ordinal itself. 25/12 04:16 And, uh, I'm sure the paradox is around here somewhere. 25/12 04:16 uoaygl,  isomorphic to powerset  is cantor diagonalization 25/12 04:17 think of N -> Bool, not as a set of booleans, but a binary sequence 25/12 04:18 Hmm. You can't test that omega is not finite, but you can prove that omega is not finite. I think. 25/12 04:18 You've jettisoned positivity, so you can prove anything you want. 25/12 04:19 -!- copumpkin_ is now known as copumpkin 25/12 04:54 I am confused and scared. Is this how people who believe in [ZFC/God] feel when they read [your post/that sign]? 25/12 05:42 ??? lol 25/12 05:42 ? 25/12 05:42 oh, he replied to all the blog comments 25/12 06:40 with no real substance, but luckily for us he's preparing a new blog post 25/12 06:40 -!- dblhelix_ is now known as dblhelix 25/12 07:32 two days later, I succeeded at proving another case of this 25/12 12:36 I guess the solution is to keep breaking it down until it's trivial 25/12 12:50 copumpkin: if we were in #haskell someone would golf your proof down to 2 lines full of HOFs and in pointfree style :) 25/12 13:24 hah 25/12 13:24 I wish 25/12 13:24 this is turning into a monstrosity 25/12 13:24 http://snapplr.com/vsxf 25/12 13:25 seems like it'd be fairly obvious, but I can't figure out what the notation really means 25/12 13:26 I got around it in an earlier one by forcing it to infer the value that would involve those nasty # 25/12 13:26 .Diagonal.#-0 looks somewhat like something defined in a where 25/12 13:27 I've got no wheres anywhere :/ 25/12 13:27 I do have withs 25/12 13:28 the frustrating thing is that I'm not decomposing my inputs, I'm decomposing the output of a function on my inputs 25/12 13:28 http://snapplr.com/3ec1 25/12 13:29 hah 25/12 13:31 it seems like there must be an easier way but I can't see it 25/12 13:32 i generally decompose inputs to cause refinements in the function applied to them 25/12 13:32 I tried that, but agda couldn't see through it 25/12 13:32 maybe I should shelve this current proof and try decomposing inputs more 25/12 13:32 qs is codata so I can't decompose that though 25/12 13:33 ah, no, i'm wrong 25/12 13:33 ? 25/12 13:34 I'm willing to try anything that would make this less painful :P 25/12 13:34 well, i'm not in the position to suggest you anything :) 25/12 13:35 a thing that's annoying is that if you've defined some function with overlapping patterns, to get its application reduced you have to do full case analysis on the inputs anyway 25/12 13:36 yeah 25/12 13:40 -!- copumpkin_ is now known as copumpkin 25/12 14:19 -!- copumpkin_ is now known as copumpkin 25/12 15:24 -!- copumpkin__ is now known as copumpkin 25/12 16:01 anyone proving anything interesting these days? 25/12 16:13 I was leafing through a spinoza book the other day 25/12 16:14 and came across his proof of god 25/12 16:14 we should prove that in agda ;) 25/12 16:14 aGDa 25/12 16:14 I heard about spinoza hadn't picked up the loose neds yet 25/12 16:14 ends* 25/12 16:14 on that round table discussion, they all seemed fto dig spinoza 25/12 16:15 well, spinoza almost redefined god as the universe, so it's not surprising he has a proof 25/12 16:18 did you see this punpkin 25/12 16:43 http://muaddibspace.blogspot.com/2009/12/zfcs-probably-inconsistent.html 25/12 16:43 hah, nope 25/12 16:45 nice one :) 25/12 16:45 * increpare chuckles 25/12 16:46 I want to learn more about the link with comptational semantics and dependent type theory, kind of a huge topic to take on though 25/12 16:47 -!- copumpkin_ is now known as copumpkin 25/12 16:50 I guess I should prove more general stuff about this function 25/12 17:35 might be easier than dealing with this nasty stuff 25/12 17:35 -!- copumpkin is now known as monochromboy 25/12 19:28 -!- monochromboy is now known as copumpkin 25/12 19:29 -!- EnglishGent is now known as EnglishGent^afk 25/12 21:23 -!- copumpkin_ is now known as copumpkin 25/12 21:35 -!- copumpkin_ is now known as copumpkin 25/12 23:21 -!- copumpkin_ is now known as copumpkin 25/12 23:41 --- Day changed Sat Dec 26 2009 -!- copumpkin_ is now known as copumpkin 26/12 01:10 -!- copumpkin_ is now known as copumpkin 26/12 01:18 -!- copumpkin_ is now known as copumpkin 26/12 02:52 -!- copumpkin_ is now known as copumpkin 26/12 03:43 -!- copumpkin__ is now known as copumpkin 26/12 05:27 -!- copumpkin_ is now known as copumpkin 26/12 05:40 -!- copumpkin_ is now known as copumpkin 26/12 06:07 -!- dblhelix_ is now known as dblhelix 26/12 07:32 I wish I could pattern match on codata 26/12 08:43 hmm, I can't even seem to prove the definition of one of my nasty codata sublanguage evaluator functions 26/12 13:28 prove the definition? 26/12 13:29 I guess it isn't quite the definition 26/12 13:29 but it's almost f = ... 26/12 13:29 and I can barely prove that f = ... :P 26/12 13:29 bring on OTT! 26/12 13:29 I thought chistmas was coming soon? 26/12 13:29 the recursive cases on this indirect codata stuff seem particularly hair-raising 26/12 13:36 is it normal for a hole to change the termination properties of a function? 26/12 14:01 on meth it is 26/12 14:01 I always have a heart attack when my function turns pink, then I fill in another hole and the pink goes away 26/12 14:01 well, over data i can see why having an hole inside the argument of a recursive call can upset the termination checker, i guess there's a dual for codata 26/12 14:06 yay, one more yak shaved 26/12 14:33 * copumpkin is inching towards his proof in a giant spiral 26/12 14:33 _ is my new best friend 26/12 14:41 sometimes it can infer things that I wouldn't even know how to write 26/12 14:41 eheh 26/12 14:41 it'd be nice if it could spit them out 26/12 14:42 -!- copumpkin_ is now known as copumpkin 26/12 16:37 seems to be a pretty big regression in C-c C-c 26/12 17:02 it fucks up a lot 26/12 17:02 * copumpkin coughs 26/12 17:31 lemma6 : ∀ {A} → (x : A) → (y : A) → (ys : _) → x ∈ fromList⁺ ys → x ∈ y ∷ _ 26/12 17:31 my abuse of _ continues 26/12 17:31 sometimes it gets confused though 26/12 17:39 * copumpkin fumbles around in the dark, even proving things that he doesn't understand 26/12 18:21 dolio: do you know what the number is when displaying codata? 26/12 19:12 No. 26/12 19:12 Hm, okay, thanks 26/12 19:12 it feels a little silly to have a lemma (that I proved) whose type I do not know, but that I use anyway 26/12 19:14 Oh, it may be an implicitly defined function. 26/12 19:25 You used to have to write corecursion like "cofoo ~ cocon cofoo". 26/12 19:25 most of them are of the form Module.♯ -N 26/12 19:25 But now I think you can write "cofoo = cocon cofoo". 26/12 19:26 you think something like map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) 26/12 19:26 counts? 26/12 19:26 Which may still desugar into "cofoo = cocon-0 where cocon-0 ~ cocon cofoo". 26/12 19:26 oh, I see 26/12 19:26 so it desugars it when I write it, but when displaying it's forgotten about the sugar 26/12 19:27 Because the stuff that appears in the lower display looks like what you get when you have a locally defined function in a where clause. 26/12 19:27 and won't reguar it for me 26/12 19:27 hm 26/12 19:27 so I guess -0 is probably the first time I corecurse in that module, and so on 26/12 19:28 maybe I'll submit an enhancement request 26/12 19:28 Yes. 26/12 19:28 If I write two "omega = suc (sharp omega)" definitions in a module, the second one will have a sharp-1 in it. 26/12 19:29 So that's what it is. 26/12 19:29 aha, thanks a lot 26/12 19:30 If you write a function on inductive data that uses "foo ... = ... where zing = ...", you might see ".Stuff.zing" during some proofs. 26/12 19:32 I see 26/12 19:34 never noticed that 26/12 19:34 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=15031#a15031 26/12 19:38 cool 26/12 19:38 learn something new every day! 26/12 19:38 I don't know what exactly the codata stuff is desugaring to, though. The old ~ syntax is no longer accepted. 26/12 19:39 ah 26/12 19:40 I'm guessing codata doesn't get too much love in most proofs 26/12 19:40 hmm, I think the numbers may be from the bottom of the module o.O 26/12 19:41 maybe not 26/12 19:41 do the recursive calls to whnf here count too? http://snapplr.com/3t2j 26/12 19:52 or is it only when I stick some sharps in the recursion? 26/12 19:52 I expect it only generates code when you use sharp. 26/12 19:59 -!- copumpkin_ is now known as copumpkin 26/12 20:32 -!- copumpkin_ is now known as copumpkin 26/12 21:11 --- Day changed Sun Dec 27 2009 -!- copumpkin_ is now known as copumpkin 27/12 02:43 -!- copumpkin_ is now known as copumpkin 27/12 03:15 -!- copumpkin_ is now known as copumpkin 27/12 19:15 -!- copumpkin_ is now known as copumpkin 27/12 19:45 make nat := (Mu @ [arg { zero, suc } [ (@ [done]) (@ [ind1 @ [done]]) ] ] ) : * ; 27/12 20:37 make zero := @ [zero] : nat ; 27/12 20:37 make suc := (\ x -> @ [suc x]) : nat -> nat ; 27/12 20:37 make one := (suc zero) : nat ; 27/12 20:37 make two := (suc one) : nat ; 27/12 20:37 make plus := @ @ [(\ r r y -> y) (\ r -> @ \ h r y -> suc (h y))] : nat -> nat -> nat ; 27/12 20:37 make x := (plus two two) : nat 27/12 20:37 what's that? 27/12 20:42 something from inside epigram 27/12 20:47 -!- copumpkin is now known as HaskellNinja 27/12 21:49 -!- HaskellNinja is now known as copumpkin 27/12 21:55 --- Day changed Mon Dec 28 2009 -!- copumpkin_ is now known as copumpkin 28/12 03:17 -!- copumpkin_ is now known as copumpkin 28/12 03:46 --- Day changed Tue Dec 29 2009 -!- Saizan_ is now known as Saizan 29/12 11:15 http://code.google.com/p/agda/issues/detail?id=236 29/12 16:50 :( 29/12 16:50 :\ 29/12 16:55 it seems like a pretty shitty state of affairs, to have a bunch of autogenerated names that don't actually mean anything to you 29/12 16:56 copumpkin: Is that the goal you get with C-c C-,? 29/12 16:57 yeah 29/12 16:57 I have those # -N everywhere in this proof 29/12 16:57 sometimes I can figure out what they mean, but most of the time it's just really tedious 29/12 16:58 well, the only possible improvement would be to specify from which application of # they come from 29/12 16:58 Well, it's a bit odd for flat (sharp ...) to be there. 29/12 16:58 oh, that's not common 29/12 16:58 but in general, my goals are full of those sharps 29/12 16:59 is there some secret technique to proving things about corecursive functions that I just missed? 29/12 17:00 Presumably you need to do introduce a flat, or to provide enough information for flat to compute. 29/12 17:01 yeah, but they're recursive, so if I flatten one level, I'll just get another sharp for the next 29/12 17:01 "Two delayed applications of a coinductive constructor are not 29/12 17:02 definitionally equal unless they come from the same location in 29/12 17:02 the source code." seems a little scary 29/12 17:02 Coinductive types don't have constructors. 29/12 17:03 So, if you consider definitions like "i = cosuc (# i)" and "j = cosuc (# i)", i and j aren't necessarily the same thing. 29/12 17:06 yeah 29/12 17:07 so how would one prove something about those? 29/12 17:07 i is an infinite unfold, and j is an unfold that adds one cosuc and reunfolds i. 29/12 17:07 bisimulation! 29/12 17:07 would i = cosuc (# i) and j = cosuc (# j) be equal? 29/12 17:08 They might if you expressed them in terms of unfolds, since they could be the same unfold expression. 29/12 17:09 But then again, there are lots of arbitrary choices you could make about that unfold, which wouldn't have any effect on what results you'd observe, but would make them prima facie unequal. 29/12 17:10 like what? 29/12 17:10 Like 'i = unfold inr 0' 'j = unfold inr 1'. 29/12 17:10 N X = 1 + X being the functor in question. 29/12 17:11 yeah 29/12 17:11 So, does unfold inr 0 = unfold inr 1? Not intensionally. 29/12 17:11 :/ yeah 29/12 17:12 so is there a single strategy when dealing with codata? some particular representation one should stick to? or is it just inherently painful? 29/12 17:13 Are you trying to prove things involving equality? Because that'd be a bad idea. 29/12 17:14 not really, just trying to show \in things 29/12 17:15 for Colists 29/12 17:15 this is still related to the Diagonal proof 29/12 17:19 maybe I should just drop the Colist 29/12 17:19 but I really don't like Nat -> a 29/12 17:20 especially since my Colists aren't necessarily infinite 29/12 17:20 Nat -> a isn't a colist anyway. 29/12 17:20 I'm not really sure what the encoding of colists is. 29/12 17:20 Maybe 'Sig n. || n || -> a', for that family of countable types I mentioned the other day 29/12 17:22 But then n is codata, so you'd have to encode that, too. 29/12 17:22 yeah 29/12 17:22 I should find and read about encoding M-types some time. 29/12 17:23 There's some systematic way you can do it where Nat -> A is what you get for Stream A, as I understand. 29/12 17:23 interesting 29/12 17:23 -!- EnglishGent is now known as EnglishGent^afk 29/12 20:04 --- Day changed Wed Dec 30 2009 ooh 30/12 12:20 http://twitter.com/pigworker/status/7194259496 30/12 12:21 cool 30/12 12:22 -!- opdolio is now known as dolio 30/12 16:44 --- Day changed Thu Dec 31 2009 so... loading the README.agda file in the standard library is making my laptop with 4 GB of RAM cry 31/12 07:36 heh, oh look, it's done loading 31/12 07:37 yeah, it's taking over 3.6 gigs of ram. nice 31/12 07:38 go haskell! 31/12 07:42 quitting and loading fresh brought it down to "only" about 1.5 gigs 31/12 07:47 jmcarthur: proving anything interesting? 31/12 13:01 I guess he's probably asleep 31/12 13:01 copumpkin: no, nothing interesting. at home i'm setting up a fresh installation of arch on my laptop and just reinstalled agda and went ahead and built the standard library 31/12 16:28 ah :) 31/12 16:28 i would like to start getting more into agda 31/12 16:28 mmm 31/12 16:28 beware of the corecursion! 31/12 16:28 'sdeath ;) 31/12 16:28 running into problems with it? 31/12 16:29 i like corecursion :( 31/12 16:29 yeah 31/12 16:29 I have the ugliest proof ever with a few holes that I can't figure out how to fill because the goal isn't clear 31/12 16:29 jmcarthur: have you done any proofs about corecursive definitions? 31/12 16:31 nope 31/12 16:32 are you using codata directly or [infinity symbol]? 31/12 16:33 infinity symbol 31/12 16:33

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