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