--- Log opened Tue Dec 01 00:00:05 2009
quantumEdheh http://namebinding.wordpress.com/01/12 00:44
uoryglcopumpkin: write everything in Agda and translate it to other systems as desired.01/12 01:39
copumpkinuorygl: unfortunately that doesn't work for things that might not terminate01/12 01:39
uoryglIf 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
copumpkindefinitely01/12 01:54
copumpkinbut I want something that I can't prove in agda without jumping through hoops01/12 01:54
uoryglProve that NBG is a conservative extension of ZFC.01/12 02:09
copumpkindone, next?01/12 02:15
uoryglConstructively prove that it is possible to pastebin your proof and post the link to this channel.01/12 02:26
copumpkinlol01/12 02:27
* copumpkin shuffles subtly toward the door01/12 02:27
uoryglI don't suppose you feel like taking up my effort to write NBG.01/12 02:28
uoryglOr anyone else.01/12 02:29
quantumEduorygl: you should read this http://citeseerx.ist.psu.edu/viewdoc/summary?doi= 02:29
uoryglWhat's that about?01/12 02:31
* uorygl ponders what a "bijection" is.01/12 02:45
uoryglA 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
copumpkina function from Fin 2 to A01/12 02:48
quantumEduorygl, or don't ... whatever01/12 02:48
uoryglquantumEd: well, I'm wondering whether it would help me do this or be interesting.01/12 02:49
quantumEdanyone know where I can get some kind of basic command line tool written in agda, like an interpreter or something01/12 02:53
uoryglI 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
uoryglThen a "first element" is an element of every element, and a "second element" is an element of exactly one element.01/12 03:11
ertaiHi all,01/12 10:32
ertaiis there a way in emacs to introduce variables a kind of intro command01/12 10:32
ertai?01/12 10:33
Saizanyou mean those from implicit arguments?01/12 10:33
-!- EnglishGent is now known as EnglishGent^afk01/12 11:46
ertaiSaizan: no even explicit ones01/12 11:54
ertaiI suppose that refine should do the job, but it doesn't, anyone ?01/12 13:57
quantumEdhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=291 blegh01/12 21:29
quantumEdwhy doesn't he just post the code ?01/12 21:29
copumpkinpost a comment asking for it01/12 21:30
quantumEd?01/12 21:30
copumpkinoh, someone already asked01/12 21:31
Saizani don't get Nicolas Pouillard reply, can't you compute the principal type for lambda terms without annotations, in STLC?01/12 21:32
Saizani mean, you can do it for hindley milner01/12 21:32
quantumEdim not sure you can because e.g.  (\x -> x)  could be  T -> T, or (T -> T) -> (T -> T) etc01/12 21:33
Saizanah, i guess i mean type schemas01/12 21:33
FunctorSaladapropos principal types, the article could use some help ;) http://en.wikipedia.org/wiki/Principal_type01/12 21:34
Saizan(funny that less polymorphism makes this kind of problem harder :)01/12 21:35
FunctorSaladdoes "most general" even make sense without variables?01/12 21:36
FunctorSalador do you get metavariables for STLC01/12 21:36
Saizani guess talking about principal types doesn't make much sense for STLC01/12 21:37
Saizani think i've seen "principal type schema" which would be with metavariables01/12 21:37
FunctorSaladhmm are there any interesting programs that can be expressed in STLC actually?01/12 21:38
FunctorSaladit seems very weak01/12 21:38
quantumEdwhat interesting programs :P01/12 21:38
quantumEdyou can use simple types for a real world programming language01/12 21:38
FunctorSaladwhat do you mean?01/12 21:38
FunctorSaladah01/12 21:38
FunctorSalad(that reply was before your second msg)01/12 21:39
FunctorSaladyeah, but those realworld-langs have `fix'01/12 21:39
FunctorSaladI don't see how to express much of anything in STLC alone01/12 21:39
FunctorSalad(but I haven't tried)01/12 21:39
Saizanwell, you have to add first order data and a let construct i think, however STLC is more like the fibonacci for typecheckers01/12 21:42
quantumEdSaizan 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
quantumEdI think so anyway, I'm not sure how the compiler does01/12 21:47
Saizanwhere do you need negative types?01/12 21:48
quantumEdevaluation01/12 21:48
quantumEdreify something into D~D->D and then pull it back into syntax to get the beta normal form01/12 21:49
Saizanah, right01/12 21:49
quantumEd  -c      --compile               compile program (experimental)01/12 21:54
quantumEdguh01/12 21:54
quantumEdthis sucks01/12 21:54
opdolioIf you add in some extra types beyond arrows, STLC gets a little more useful.01/12 21:55
opdolioLike, Nat/Int, sums, products, unit, empty.01/12 21:55
opdolioThose can technically all be 'simple' types.01/12 21:56
quantumEdyes you can use a make a fully featured language with STLC, something like C or ALGOL or whatever01/12 21:56
FunctorSaladadding naturals, if and fix gives you a turing-complete language (PCF)01/12 21:56
FunctorSaladunless I missed one :)01/12 21:56
quantumEdohh yeah true01/12 21:57
quantumEdthat's a better example than mine01/12 21:57
opdolioIt's just that without any polymorphism, you'll be writing a lot of the same functions over and over.01/12 21:57
FunctorSaladyeah01/12 21:57
opdolioPlain 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 dolio01/12 21:58
FunctorSaladopdolio, you have the complementary colour of dolio in my scheme :o01/12 21:58
dolioNice.01/12 21:58
quantumEdwkat the hell :///////01/12 22:03
quantumEd   primTrustMe : {A : Set}{a b : A} → a ≡ b01/12 22:03
quantumEdthis sucks01/12 22:03
quantumEderror: There is no primitive function called primTrustMe01/12 22:03
copumpkinwow01/12 22:03
copumpkinwhere is that?01/12 22:04
dolioHow old is your agda?01/12 22:04
quantumEdRelation/Binary/PropositionalEquality/TrustMe.agda:11,4-4401/12 22:04
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Binary.PropositionalEquality.TrustMe.html#23401/12 22:05
copumpkinlol01/12 22:05
dolioIt's used for String equality.01/12 22:05
dolioPossibly others.01/12 22:05
quantumEdit sucks !01/12 22:06
copumpkinwell, it's interfacing with primitive haskell stuff01/12 22:07
copumpkinnot sure how else you'd pull out an equality proof01/12 22:08
copumpkinI guess it shouldn't even be decidable because the string is potentially infinite?01/12 22:09
quantumEdshould I do cabal install agda --reinstall?01/12 22:09
quantumEdto get up to  date01/12 22:10
dolioI think trustme was added after the last release.01/12 22:10
quantumEdand also darcs pull in /lib01/12 22:10
dolioSo you'd have to install from darcs.01/12 22:10
quantumEd:(01/12 22:11
quantumEdthis sucks01/12 22:11
dolioUnless you're not getting the library from darcs.01/12 22:11
quantumEdI don't know why I even try and write programs anymore :p01/12 22:11
copumpkinI think trustMe is fine, but its usage should propagate an "infected with evil" flag in the .agdai files01/12 22:12
copumpkinso you can get warnings01/12 22:12
dolioI don't think Strings can be infinite.01/12 22:12
quantumEdim not using agda to check proofs01/12 22:12
quantumEdjust want to code a typechecker01/12 22:12
dolioAnything that could result in an infinite list of characters probably returns a Costring.01/12 22:13
quantumEdI upgraded now I get unrecognized option `--universe-polymorphism'01/12 22:13
quantumEdhm01/12 22:13
quantumEdthat might be progress in the forward direction01/12 22:13
copumpkinI 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
dolioSpeed?01/12 22:14
copumpkinoh, for people who actually run their programs01/12 22:14
copumpkinkeep forgetting01/12 22:14
copumpkinpff01/12 22:14
dolioHaskell Strings aren't exactly speed demons either, though.01/12 22:17
dolioEstablishing a correspondence between Haskell Strings and Agda List Chars might be difficult, though.01/12 22:17
edwinbPeople run their programs too these days?01/12 22:17
dolioAssuming you want them to work in extracted code.01/12 22:18
edwinbI suppose you have to, to check whether they work01/12 22:18
Saizanwhat is this intro/refine command they mention in the commits?01/12 22:20
dolioAlso, 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
quantumEdI installed the newest Agda and it still doesn't like the std lib01/12 22:21
dolioWow, it finished compiling already?01/12 22:22
FunctorSaladhaskell strings aren't bad if they get fused :)01/12 22:22
copumpkinquantumEd haz quantum computer01/12 22:22
quantumEdstill unrecognized option `--universe-polymorphism'01/12 22:24
copumpkinoh, did you install it from darcs?01/12 22:24
Saizandid you recompile the agda-executable too?01/12 22:25
copumpkincause the latest one in hackage is olde01/12 22:25
quantumEdhow do I do that Saizan?01/12 22:25
Saizancd src/main/ && cabal install01/12 22:25
quantumEdummm01/12 22:27
quantumEdthat did soemthing01/12 22:28
quantumEdnow I get a different error about the trustme file01/12 22:28
quantumEdNo binding for builtin thing REFL, use {-# BUILTIN REFL name #-} to01/12 22:28
quantumEdbind it to 'name'01/12 22:28
quantumEdwhen checking that the type of the primitive function primTrustMe01/12 22:28
quantumEdis {A : Set} {a, b : A} → a ≡ b01/12 22:28
Saizanthat's defined in Relation/Binary/Core.agda01/12 22:29
* Saizan has no idea how these things work01/12 22:29
* quantumEd thinks it's quite simple: They don't :P01/12 22:29
Saizan*are supposed to work :)01/12 22:30
quantumEd if this system ever worked it must have been a complete coincidence01/12 22:30
Saizanwhat are you trying to compile btw?01/12 22:30
quantumEdnothing yet,01/12 22:30
quantumEdI was trying to typecheck something that does  import IO01/12 22:31
quantumEdoh the solution is quite obvious, don't use the standard library...01/12 22:31
Saizanbah, i get an even different error from the executable (it works fine in emacs though)01/12 22:37
quantumEdwhat do I use for malonzodir?01/12 22:38
quantumEdthe manual says <DIR> which is really really helpful01/12 22:39
* quantumEd supposes src/full/Agda/Compiler/MAlonzo01/12 22:39
Saizanwow, it compiled!01/12 22:44
quantumEdwhat did?01/12 22:44
Saizanmodule Foo where open import IO; main = run (putStrLn "hello world")01/12 22:45
Saizanwith: agda -i../Agda/lib/src/ -i/home/saizan/snippets/ Foo.agda --compile01/12 22:45
Saizaneverything from darcs01/12 22:46
Saizanit runs too01/12 22:46
quantumEdgreat! thank you01/12 22:48
quantumEdnow I have that working too01/12 22:48
Saizannp01/12 22:49
uoryglIs \eq the same thing as =, \iff the same thing as \<=>, and so on?01/12 23:30
dolioType 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
uoryglI guess so.01/12 23:35
--- Day changed Wed Dec 02 2009
copumpkinis 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
copumpkinlike that?02/12 00:56
edwinbI was going to say "readability" but I don't suppose a name like "i" really helps...02/12 01:00
edwinbhabit, probably02/12 01:00
copumpkinfair enough :)02/12 01:00
dolioWhen you do C-c C-c, agda uses the names specified in constructors to fill in names in the patterns.02/12 01:01
dolioOtherwise you get stuff like x, x', y, y'.02/12 01:02
copumpkinah, I see02/12 01:02
dolioWith that definition, it'd fill in "suc {n} i", which is probably nicer.02/12 01:02
dolioAlthough it probably wouldn't fill in the {n} at all.02/12 01:03
* quantumEd starts my own module Prelude.agda02/12 01:42
uoryglWhat does the Agda distribution consist of?02/12 01:49
uoryglSo 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
copumpkinpretty much that, and there's a standard library in a separate repository02/12 01:56
copumpkinI believe it has two compilers, too02/12 01:57
Saizan_yeah, i discovered today that you can compile things!02/12 01:57
* uorygl nods.02/12 02:09
uoryglIt sounds like the typechecker is the guts of the operation.02/12 02:09
quantumEdoh for goodness sake02/12 02:11
dolioType checking agda requires evaluating agda, though.02/12 02:11
quantumEdyou can't call a function 'abstract' in agda02/12 02:11
quantumEdthis is bloody stupid02/12 02:11
dolioabstract is a keyword.02/12 02:11
uoryglWhat's the computational complexity of the typechecker?02/12 02:14
uoryglWell, 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
dolioWell, the type checker may have to execute arbitrary agda terms.02/12 02:15
dolioSo even if you restrict yourself to terms that would pass the termination checker...02/12 02:15
uoryglSounds like there's probably a one-kilobyte file that will never typecheck.02/12 02:16
byorgeyalmost certainly.02/12 02:16
dolioYou could write a program that requires the type checker to compute the Ackermann function at some value.02/12 02:17
dolioValue(s).02/12 02:17
uoryglNote to self: if I run an Agda typechecker online, I should have it give up after a while.02/12 02:18
quantumEdhow do I use with twice?02/12 02:19
dolioTwice as in matching on two things with a single with, or a second with after another?02/12 02:20
quantumEdone after the other02/12 02:21
dolioYou just put another "with ..." after you match on the stuff in the first with.02/12 02:21
copumpkinquantumEd: you can put02/12 02:21
copumpkin| in02/12 02:21
copumpkinwith f x | g y02/12 02:22
copumpkinI think02/12 02:22
dolioThat's how you match on two things with a single with.02/12 02:22
copumpkinoh ok :)02/12 02:22
quantumEdcool02/12 02:23
quantumEdtest = eval (App (Lam (App (Var fz) (Var fz))) (Lam (Var fz)))02/12 02:23
quantumEdtest ~> Lam (Var fz)02/12 02:24
quantumEdnow I need a parser and pretty printer for lambda terms02/12 02:24
quantumEdwho is writing that? :P02/12 02:24
dolioThere are some parser combinators in agda somewhere.02/12 02:24
dolioPeople have been writing papers on them.02/12 02:25
dolioI'm not sure what sorts of grammars they're usable for.02/12 02:25
quantumEdbtw02/12 02:25
quantumEdI can't figure out this with thing02/12 02:25
quantumEdI have got02/12 02:25
quantumEdNat-lem1 refl = refl02/12 02:25
quantumEdso shouldn'g02/12 02:25
quantumEdS n =Nat= S m with n =Nat= m02/12 02:25
quantumEd... | inl q = inl (Nat-lem1 q)02/12 02:25
quantumEdbe able to be written a lot easier?02/12 02:25
quantumEdI mean without the lemma02/12 02:25
dolioYou mean match on q with refl?02/12 02:26
quantumEdyes02/12 02:26
dolioI think you might not be able to use the ... if you want to do that.02/12 02:26
copumpkinwhat does inl refl do?02/12 02:26
dolioYou'd have to write "S n =Nat= S .n | inl refl = inl refl"02/12 02:26
dolioBecause the match on "refl" refines the m to be the same as n (or vice versa).02/12 02:27
quantumEdinl refl : (n ≡ n) ∨ (~ (n ≡ n))02/12 02:27
quantumEddolio ah! I get it, thanks - that actually makes some sense02/12 02:28
quantumEdNat-lem2 : forall {n m : Nat} -> S n ≡ S m -> n ≡ m02/12 02:28
quantumEdNat-lem2 refl = refl02/12 02:28
quantumEdso for this one ..02/12 02:28
quantumEd... | inr f = inr (\x -> f (Nat-lem2 x))02/12 02:28
quantumEdcan it also be removed?02/12 02:28
quantumEdI think not02/12 02:28
dolioI don't think so, no.02/12 02:29
quantumEdI didn't see any proofs that relate prettyprinting to parsing with the structural combinator stuff02/12 02:32
quantumEdit'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 add02/12 02:32
dolioPretty printing isn't as hard a problem as parsing, termination wise, is it?02/12 02:33
quantumEdno02/12 02:33
quantumEdwhat 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
dolioProving that they're somewhat inverse?02/12 02:35
quantumEdyou 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 recursion02/12 02:36
quantumEdpretting printing isn't injective that's the problem02/12 02:37
quantumEdhm02/12 02:37
quantumEdthat's wrong02/12 02:37
quantumEdpretty printing is injective, but two different texts might have the same meaning02/12 02:37
dolioParsing is the non-injective one.02/12 02:37
Saizan_it's parsing that's not injective02/12 02:37
dolioEven whitespace ruins it.02/12 02:38
quantumEdwell I was thinking that you can lex whitespace away02/12 02:38
quantumEdI guess the real problem is:  Pretty printer isn't a specification02/12 02:39
quantumEdit's just one data point02/12 02:39
Saizan_haskell-src-exts keeps the extra text around to get pp . parse = id02/12 02:39
uoryglDarn, I somehow managed to forget to ask whether the Agda typechecker is entirely in Haskell or no.02/12 02:40
copumpkinit is02/12 02:41
copumpkinall of agda is02/12 02:41
dolioIs haskell-src-exts more of a concrete syntax tree, then?02/12 02:41
uoryglIs the Emacs plugin entirely in Haskell?02/12 02:42
dolioThe emacs plugin is presumably in elisp.02/12 02:42
* uorygl nods.02/12 02:43
uoryglI guess I'll be interested in the Haskell source of Agda at some point.02/12 02:43
dolioCommunicating with some sort of agda checker in a spawned process.02/12 02:43
copumpkinit just keeps ghci running the background02/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
quantumEdanyone know some texts which go into detail about proving parsers correct? even if it's not formal computers stuff02/12 02:50
Saizan_quantumEd: how does your AST look like, btw?02/12 02:51
quantumEddata Lambda : Nat -> Set where02/12 02:51
quantumEd Free : forall {n} -> Nat -> Lambda n02/12 02:51
quantumEd Var : forall {n} -> Fin n -> Lambda n02/12 02:51
quantumEd App : forall {n} -> Lambda n -> Lambda n -> Lambda n02/12 02:51
quantumEd Lam : forall {n} -> Lambda (S n) -> Lambda n02/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 mean02/12 02:53
dolioYou know, you could actually parameterize by 'n' instead of indexing.02/12 02:53
dolioSince it's just a nested type.02/12 02:53
dolioAnd save yourself all the "forall {n}"s.02/12 02:54
quantumEdthis is just a test02/12 02:55
quantumEddolio, oh right, since I used Lambda (S n) and that wouldn't be allowed to be a parameter in Coq02/12 02:55
quantumEdwhich is what I am used to02/12 02:55
copumpkinwhy wouldn't it be?02/12 02:56
dolioIs that still true? I thought they added non-regular parameterized types.02/12 02:56
dolioI thought roconnor mentioned something about it, at least.02/12 02:56
quantumEdSaizan but it is the same approach to do the full thing, just a bit more tricky02/12 03:00
quantumEd(which is why I start with this)02/12 03:00
doliocopumpkin: 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
copumpkinstrange :)02/12 03:03
quantumEdthere is a good reason for it02/12 03:03
copumpkinare there any extensional proof systems?02/12 03:04
dolioNuPRL?02/12 03:04
dolioNuPRL is pretty close to Martin-Loef's extensional type theory, I think.02/12 03:06
copumpkinI see02/12 03:06
dolioOf course, I've not investigated either very closely.02/12 03:14
dolioBut 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
uoryglSuppose 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
uoryglSpecifically, 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
uoryglSo 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
uoryglAnd that's something you can't do in Agda, can you.02/12 05:10
opdolioYou 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
opdolioBut 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
uoryglNow, can you use Peirce's law, ((a -> b) -> a) -> a, to express this proof?02/12 05:14
uoryglI 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
opdolioPeirce'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
opdolioI don't know how easy it'd even be to state the theorem in Agda, though.02/12 05:22
opdolioYou'd have to come up with a representation of real numbers, and proofs of rationality and irrationality.02/12 05:23
BerengalCouldn't you just postulate those?02/12 05:27
opdolioWhich parts?02/12 05:31
opdolioI 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
opdolioAnd that 2 is rational.02/12 05:31
BerengalI guess you'd only end up postulating the theorem itself...02/12 05:32
opdolioYeah, other than some of the logical structure.02/12 05:32
uoryglWell, 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
Berengalhttp://en.wikipedia.org/wiki/Construction_of_the_real_numbers02/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
opdoliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=13489#a1348902/12 06:11
-!- opdolio is now known as dolio02/12 06:12
uorygldolio: what is Dec?02/12 06:23
dolioIt'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
dolioThe law of the excluded middle decides all propositions, essentially.02/12 06:24
uoryglWhat's the type of \neg?02/12 06:24
copumpkinSet -> Set102/12 06:25
* uorygl cowers at the mention of Set1.02/12 06:25
dolioDec P = P \/ \neg P, roughly.02/12 06:25
copumpkinoh wait02/12 06:25
copumpkinit isn't Set102/12 06:25
copumpkinit's just Set -> Set02/12 06:25
copumpkinor Set a -> Set a now probably02/12 06:25
dolioYeah. \neg P = P -> \bot02/12 06:25
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#32702/12 06:26
copumpkinboth of them in there02/12 06:26
uoryglSo the constructors of Dec are no and yes?02/12 06:29
-!- kmc__ is now known as kmc02/12 06:29
copumpkinyep02/12 06:29
copumpkinyes carries a proof of yes-ness and no carries a proof of not-yesness02/12 06:30
uoryglIn the definition of lem, what are P and Q?02/12 06:30
dolioP for peirce is Dec P for the P from lem.02/12 06:32
dolioQ is \bot, I think.02/12 06:33
BerengalQ is anything, including \bot02/12 06:35
dolioYeah, but when I'm using peirce to prove lem, it's \bot.02/12 06:35
BerengalSince if you can prove P -> \bot, you can prove P -> Q, for all Q02/12 06:35
copumpkinhm02/12 06:36
uoryglThis is kind of intriguing.02/12 06:37
uoryglOkay. This means that callCC behaves in a really fun manner when it comes to laziness and data constructors.02/12 06:39
uoryglIt can return the value "no, because--er, actually, yes!"02/12 06:39
dolioRight.02/12 06:39
uorygl(Homework problem: Find the value of because--er,.)02/12 06:40
dolioIt 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
uoryglThat sounds like a pain in the mud.02/12 06:41
dolioAnd if it's impossible to prove the proposition, then it made the right choice.02/12 06:42
uoryglWhat a brave function it is.02/12 06:42
dolioYeah, classical logic is crazy. :)02/12 06:44
uoryglSo taken literally, callCC leads to a program that can output the wrong thing.02/12 06:46
uoryglThat's almost a behavior that I want.02/12 06:46
dolioWhat do you mean the wrong thing?02/12 06:46
uorygllem 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
dolioYes, that's true.02/12 06:48
dolioAlthough, not in Agda, since peirce is a postulate, it probably won't be subject to any normalization.02/12 06:48
dolioSo if you ran the program, you'd probably just get stuck at some point.02/12 06:49
uoryglRight, 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
doliocall/cc isn't really 'pure'.02/12 06:50
dolioIt behaves differently under different evaluation orders and such.02/12 06:51
uoryglFor some reason, I wasn't expecting it to be *that* impure.02/12 06:55
uoryglPerhaps 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
dolioWell, if you think of something like "[a, b, callcc f]"...02/12 06:56
dolioWhere does it jump back to?02/12 06:56
dolioDoes 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
dolioWhich could make a difference, I think. I don't have any good concrete examples.02/12 06:57
dolioIt even distinguishes call-by-need (lazy) from call-by-name (lazy - sharing) I think.02/12 06:58
uoryglThe difference is that if it's the latter, you go "Darn!", while if it's the former, you go "Darn."02/12 06:58
dolioI'm sure oleg has examples, but I'm not really sure what to search for.02/12 07:03
uoryglAsk Oleg if he has an implementation of ZFC or some equivalent postulating only Peirce's law.02/12 07:04
dolioPeople have modeled ZFC in Coq, I think.02/12 07:04
uoryglUnfortunately, Coq isn't Agda.02/12 07:05
BerengalIs there a fundamental difference to what's expressible in them?02/12 07:06
uoryglProbably not.02/12 07:06
dolioCoq has some impredicativity, but that's about it.02/12 07:06
dolioOf course, Agda has induction-recursion, which Coq doesn't.02/12 07:07
uoryglBoth of them have modus ponens. Both of them effectively allow axiom schemas. I think that's all you need.02/12 07:11
dolioApparently impredicativity helps with power sets, though.02/12 07:12
dolioI don't really understand how, though.02/12 07:12
uoryglWhat is impredicativity?02/12 07:12
BerengalSet in Set02/12 07:12
dolioIt's not that.02/12 07:12
BerengalNo?02/12 07:12
BerengalI'm afraid I'm not quite sure what it is myself...02/12 07:14
dolioImpredicativity is where you can quantify over universes that include the thing you're defining.02/12 07:14
dolioSo, Set : Set1 may be a rule, but, for instance, if U : Set, then (T : Set) -> U : Set, instead of Set1.02/12 07:15
dolioOr, for T : whatever, really.02/12 07:15
dolioYou could have (T : Set85) -> U be in Set, as long as U : Set in that context.02/12 07:16
dolioCoq has it off by default for Set now, actually, since it causes problems with some classical postulates.02/12 07:17
dolioLike law of the excluded middle, I think.02/12 07:17
dolioBut Prop is still impredicative.02/12 07:19
dolioDid 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 #agda02/12 07:27
ski_<dolio> Did that get through?02/12 07:27
dolioI know my messages got through. I was wondering if Berengal got them since he got knocked off.02/12 07:28
ski_.. oh02/12 07:28
BerengalI got that02/12 07:29
dolioOkay.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
BerengalSo it's a bit like recursion in the propositions?02/12 07:29
dolioIf 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
dolioBut you still have Set i : Set (i + 1).02/12 07:30
dolioAnd 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
dolioYou have to be careful about inductive/sigma types, too.02/12 07:33
BerengalRight02/12 07:33
BerengalI 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 explodes02/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
dolioYes, 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
BerengalSo 'id' is a proof of itself?02/12 07:36
ski_no02/12 07:37
dolioGHC 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
dolioLike, you can't use it with Maybe :: * -> *02/12 07:38
dolioSo 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
dolioUnless you turn on -XImpredicativeInstantiation, in which case it really is *.02/12 07:39
dolioOr whatever the flag is called.02/12 07:39
ski_*nod*, the mono-type / poly-type distinction02/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, itself02/12 07:41
dolioYes, that's what it buys you, ultimately.02/12 07:42
dolioWhich 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
dolioAlthough that kind of encoding isn't very good for doing proofs.02/12 07:42
ski_(s/instroduct/introduce/)02/12 07:43
dolioSome folks in mathematics distrust the sort of circularity that impredicativity introduces, and try to avoid it.02/12 07:45
ski_Weyl02/12 07:45
dolioWhich, 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
dolioI guess once you have a paradox based on circularity named after you, you have good reason to mistrust it.02/12 07:46
dolioLots of definitions have some sort of impredicative circularity that doesn't seem vicious, though.02/12 07:49
dolioI 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 stratification02/12 07:49
ski_.. but it doesn't appear to be predicate, anyway, according to WP02/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
dolioWell, 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
dolioOh, it says the class comprehension schema is predicative.02/12 07:59
dolioSo you can only quantify over sets in the schema.02/12 07:59
uoryglBerengal: what's Turing-completeness cracked up to be?02/12 08:05
uoryglDoes Set : Set really admit paradoxes?02/12 08:06
dolioThe prerequisite for a language being useful?02/12 08:06
dolioYes.02/12 08:06
dolioIt's a more complicated paradox than Russel's, though.02/12 08:07
uoryglWhat's the paradox?02/12 08:07
doliohttp://code.haskell.org/Agda/test/succeed/Hurkens.agda02/12 08:08
ski_Girard's paradox ?02/12 08:08
dolioYes.02/12 08:08
dolioI 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
uoryglMy, this is abstract.02/12 16:06
uoryglI notice that this has lambdas in places that would not be syntactically valid in Haskell.02/12 16:06
-!- RichardO_ is now known as RichardO02/12 16:11
BerengalI'm trying to prove that 100000 + 0 == 0. This is proving hard...02/12 16:43
quantumEdstart with the easier problem of proving 1 = 002/12 16:44
BerengalI meant 100000 + 0 == 100000...02/12 16:45
BerengalSince I've proven that n + 0 == n, I hoped it would just unify, but it seems it wants to reduce...02/12 16:46
BerengalIs there a way to do this?02/12 16:48
quantumEdif have got    zero_right_identity : forall n -> n + 0 == n,  then  zero_right_identity 100000 : 100000 + 0 == 10000002/12 16:49
BerengalRight, but ghci still overflows the stack02/12 16:50
BerengalWhen typechecking02/12 16:51
* uorygl tries to get his hands on a copy of Hurkens' paper about Girard's paradox.02/12 18:02
quantumEdwhat'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
uoryglI feel like it would help if these types were written using "data" instead of as equations.02/12 18:32
uoryglCan I ask the IDE what the type of a variable is?02/12 18:35
copumpkinwith a conveniently placed hole, you can sort of do that02/12 18:36
* uorygl notes: C-u C-x =02/12 18:41
uoryglI'm guessing that "loop" is not a misnomer, and that expression actually loops.02/12 18:47
-!- RichardO_ is now known as RichardO02/12 18:59
BerengalDoes agda normalize all terms before deciding they're equal?02/12 20:23
dolioYes.02/12 20:23
BerengalBut in theory it doesn't have to, right?02/12 20:24
dolioIn theory it could search for some series of beta/eta conversions between the two terms.02/12 20:25
BerengalHow about simple syntactic equality?02/12 20:25
dolioWell, then, "(\x -> x) 5" wouldn't be equal to "5".02/12 20:26
BerengalUntil you used some other tactic that reduced it to "5"02/12 20:26
dolioThe equality in typing rules is equality up to beta-eta conversion.02/12 20:27
dolioAnd the easiest way to decide that is to normalize both sides and check for syntactic equality.02/12 20:28
BerengalIt means we can't prove 100000 equals 100000 though...02/12 20:28
dolioalpha-beta-eta, I guess.02/12 20:28
dolioNaturals?02/12 20:28
BerengalYeah02/12 20:28
dolioHave you declared them built-in?02/12 20:29
BerengalYep02/12 20:29
dolioHuh.02/12 20:29
dolioThis is about 100000 + 0 = 100000, right?02/12 20:30
BerengalRight now, just 100000 == 10000002/12 20:31
dolioIs _+_ built-in?02/12 20:31
BerengalI'm not using _+_02/12 20:31
dolioOh, right.02/12 20:31
dolio:)02/12 20:31
dolioYeah, I'm trying it now, and I don't understand what its problem would be.02/12 20:32
BerengalAnd _==_ is defined as _==_ {A : Set}(x : A) : A -> Set where refl : x == x02/12 20:32
dolioI'd expect normalizing 100000 once it's BUILTIN to be trivial.02/12 20:33
kosmikusit's not using anything more clever than peano representation internally afaik02/12 20:34
Saizan_the BUILTIN maybe affects only compiled programs?02/12 20:34
dolioI thought it got backed with GMP once you used the BUILTIN pragma.02/12 20:34
BerengalAs I've understood it, builtin naturals just provide syntax...02/12 20:34
Saizan_(aside from literals)02/12 20:34
kosmikusyes, I also thought it's purely syntactic02/12 20:34
kosmikusI wasn't aware that Agda uses GMP for anything02/12 20:35
BerengalIt used to02/12 20:35
dolioFor instance, if you tell it to normalize 5000 * 5000, it finishes immediately.02/12 20:35
dolioWith C-c C-n.02/12 20:35
BerengalBut I think they ripped it out in Agda2...02/12 20:35
dolioAnd I just wrote a factorial function and it computed 1000!02/12 20:37
dolioSo it's using GMP somewhere.02/12 20:37
dolioPerhaps just not during type checking.02/12 20:37
BerengalWhat's the builtin for _*_ called?02/12 20:38
dolioNATTIMES, I think.02/12 20:38
dolioOr, probably not GMP directly, but Haskell Integers.02/12 20:38
BerengalMy emacs stalled on 5000 * 500002/12 20:38
BerengalAnd once I declared it builtin, it works02/12 20:39
dolioYes, that's not particularly surprising.02/12 20:40
BerengalNo, not really. I guess the typechecker doesn't know about that though02/12 20:40
dolioMaybe it can't use the efficient backing because it has to handle neutral terms and stuff.02/12 20:42
kosmikusnot a good excuse02/12 20:42
kosmikus:)02/12 20:42
dolioNo, but it might be the reason. :)02/12 20:42
kosmikusyeah02/12 20:42
kosmikusonly reason I can think of02/12 20:42
BerengalStill, 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 them02/12 20:45
BerengalWe can't just build everything into the language...02/12 20:46
kosmikusyou want things that you prove to be equal to be considered equal *automatically*?02/12 20:47
BerengalYes02/12 20:47
dolioThat leads to pitfalls.02/12 20:48
BerengalIf I've already proved that n + 0 == n, I shouldn't have to prove that 100000 + 0 == 10000002/12 20:48
BerengalIt does02/12 20:48
dolioWell, if you've proved that n + 0 = n, then you should be able to use that proof for n = 100000.02/12 20:49
BerengalYes, but I'm not, because ghci blows the stack02/12 20:50
dolioBut you have to use a substitution function, it won't just happen.02/12 20:50
kosmikusBerengal: what you want is, I think, called a type system with extensional equality, and that's known to be undecidable02/12 20:51
BerengalAh. I've got a couple of papers on that I was just about to read02/12 20:52
BerengalIs it possible to regain decideability with some restrictions though?02/12 20:53
kosmikusbut I completely agree with you that I think none of the current languages is at a "sweet spot" with respect to handling of equality02/12 20:53
BerengalBecause even a restricted version of that would be useful02/12 20:53
kosmikusyeah, it would02/12 20:53
kosmikusI think one should be able to "program" the standard tactic being used to check equality02/12 20:54
kosmikusrather than always just getting beta-eta02/12 20:54
BerengalHumans standing in for the undecideable parts?02/12 20:54
dolioObservational Type Theory has extensional equality that is still decidable, but that's because one still applies equalities using coercions.02/12 20:54
kosmikuswell, it's clear that it can't just automatically work in general02/12 20:55
kosmikusbut for many concrete situations, it works02/12 20:55
kosmikusjust as an example, for natural numbers one could build in lots of extra rules without making the type system undecidable02/12 20:55
BerengalYeah. 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 cases02/12 20:56
Berengali.e. n > 102/12 20:56
kosmikusof 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 apply02/12 20:56
kosmikussimilar to Coq's options to extend the auto tactic02/12 20:57
BerengalIndeed, it'd be nice to have02/12 20:57
dolioIt seems as though the normalizer handles expressions with postulated naturals all right.02/12 21:03
doliox + fact 100 gets normalized right away to x + <a very large number>.02/12 21:04
dolioOnly something like "100 + x" takes a really long time, since it normalizes to "suc (suc (... x))".02/12 21:04
dolioSo 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
BerengalHey, it worked02/12 21:09
Berengalhttp://moonpatio.com/fastcgi/hpaste.fcgi/view?id=5240#a524002/12 21:10
BerengalThough I'm not sure if it's because of builtin naturals or not...02/12 21:11
* Berengal turns them off02/12 21:11
BerengalYup, it's the builtin _+_ that makes it work...02/12 21:12
-!- mak__ is now known as comak02/12 22:22
--- Day changed Thu Dec 03 2009
* uorygl ponders a realization of Set : Set in ZFC.03/12 01:26
uoryglNaturally, 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
uoryglHmm! It's possible to embed arbitrary values inside Set, isn't it.03/12 01:28
dolioSet : 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
quantumEdSet : Set in type theory has the same kind of problem as set of all sets in set theory03/12 01:31
quantumEd(or maybe ordinal of all ordinals)03/12 01:31
uoryglBut 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
uoryglAnd 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
dolioRussel's paradox is much simpler than Girard's.03/12 01:32
uoryglAnd, uh...03/12 01:33
quantumEdyeah you can't have judgements like ~(Set : Set)03/12 01:34
ccasinuorygl: How would you make an Arb?03/12 01:34
ccasinthe type, I mean, not its elements03/12 01:34
uoryglSay it's a primitive in this hypothetical language.03/12 01:35
uoryglAnd there's a function turning any value into an Arb.03/12 01:35
uoryglAlternatively, does this work: data Arb : SetOrWhatever where arb : (S : SetOrWhatever) -> S -> Arb03/12 01:35
uoryglFor some SetOrWhatever.03/12 01:35
uoryglHmm, I just realized that I don't think I have a good definition of a function.03/12 01:38
uoryglDefining a function as a set of ordered pairs doesn't work if the function is capable of taking itself.03/12 01:38
quantumEdself applicable functions don't exist in ZFC03/12 01:41
ccasina function is just any program the typing rules give an arrow type03/12 01:41
dolioquantumEd: 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
ccasinbut I'm not sure any of them take themselves03/12 01:41
ccasincertainly they don't in, say, ML03/12 01:41
quantumEddolio yeah that's what I mean, you can't talk about (:) as a relatioh03/12 01:41
quantumEdrelation*03/12 01:42
uoryglHow about (a : Set) -> a -> a?03/12 01:42
uoryglCan that take itself?03/12 01:42
dolioWhereas 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
uoryglOr is (a : Set) -> a -> a itself not a Set?03/12 01:43
ccasinno, it's a Set103/12 01:43
ccasinso it can't, I think03/12 01:44
Saizan_with impredicativity or Set : Set it is03/12 01:44
dolioIt would be a Set if Set were impredicative.03/12 01:44
copumpkin(a : Set l) -> a -> a03/12 01:44
ccasingood point! so impredicativity at that level lets one construct functions which take themselves as arguments, I never noticed that03/12 01:45
ccasinit's interesting, since "show no well typed function can take itself as an argument" is a standard exercise in intro functional programming courses03/12 01:45
uoryglObviously, lambda calculus provides a definition of "function" by which a function can take itself.03/12 01:45
ccasinsure, but not STLC03/12 01:46
quantumEdccasin: I don't understand the exercise03/12 01:46
dolioThat depends a lot on what your definition of "well-typed" is.03/12 01:46
uoryglIndeed.03/12 01:46
quantumEdccasin: oh in STCL ok..03/12 01:46
copumpkincan we write \x -> x x with universe polymorphism?03/12 01:46
ccasinquantumEd: yeah, I should have been clearer.  I'm thinking ML or Haskell here03/12 01:46
quantumEdccasin: in Hakell you can do   id x = x  and  id id  works though ?03/12 01:47
ccasin only with language extensions, I suspect03/12 01:47
quantumEdI don't think you need any extensions for that03/12 01:47
Saizan_well, depends, are you passing it a polymorpic or monomorphic id there?03/12 01:47
quantumEdPrelude> let id x = x03/12 01:47
quantumEdPrelude> :t id id03/12 01:47
quantumEdid id :: t -> t03/12 01:47
Saizan_yeah03/12 01:48
Saizan_that's hiding an explicit instantiation of the id argument to some type03/12 01:48
ccasinthat's interesting.  I mean, what type is it picking for the second id?03/12 01:48
ccasinyes03/12 01:48
quantumEdfor the second id t -> t03/12 01:48
ccasinwhat is "t" there?03/12 01:48
quantumEdfor the first one (t -> t) -> (t -> t)03/12 01:48
quantumEdwhat do you mean03/12 01:48
ccasincan one ever apply (id id)?  I think no03/12 01:48
quantumEdthis is haskell03/12 01:48
dolioYou 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
quantumEdyou should know what t is :P03/12 01:48
quantumEdyes in Ocaml -rectypes too03/12 01:49
uoryglt is a variable bound by an implicit "forall t." around the entire type.03/12 01:49
uoryglid id :: forall t. t -> t03/12 01:49
ccasinwell, that is very strange, if true03/12 01:49
quantumEdI don't know why "forall t." matters03/12 01:49
quantumEdIt's not important03/12 01:49
Saizan_e = id id ~~ e = /\ t -> id (t -> t) (id t)03/12 01:49
ccasinsince, as Saizan_ pointed out, the second id needs to be not polymorphic03/12 01:49
uoryglYou 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) id03/12 01:50
dolioYeah, writing it Church style makes it a bit clearer.03/12 01:50
quantumEdanyway I have shown that the excersice was wrong03/12 01:50
ccasinI 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 exercise03/12 01:51
ccasinyeah, I'm really thinking STLC03/12 01:51
ccasin"intro functional programming" was a mistake03/12 01:51
quantumEdccasin I think so03/12 01:51
uoryglHere, let's extend ZFC with functions.03/12 01:52
quantumEdbtw03/12 01:52
quantumEdid id is polymorphic03/12 01:52
quantumEdPrelude> (id id) 303/12 01:52
quantumEd303/12 01:52
quantumEdPrelude> (id id) "foo"03/12 01:52
quantumEd"foo"03/12 01:52
ccasinquantumEd: yes, I see03/12 01:53
uoryglThere 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 type03/12 01:54
quantumEdwell types dont' really matter03/12 01:54
quantumEdyou can just see that it is polymorphic because I used it on values of different type03/12 01:54
uoryglAlso, there exist the combinator functions S and K and a bunch of other stuff.03/12 01:54
ccasinPrelude> let foo = id id in (foo 3, foo "foo")03/12 01:55
ccasinoops03/12 01:55
ccasinwell, it worked03/12 01:55
Saizan_quantumEd: so you'd call (\x -> x) polymorphic in STLC?03/12 01:55
ccasinthough my copy paste skills need work03/12 01:55
quantumEdno03/12 01:55
Saizan_but that can be used on values of different types too03/12 01:56
ccasinsaizan_, how do you mean?03/12 01:56
quantumEdhaskell is untyped script language, STLC has curry howard and all this stuff -- they are very different03/12 01:56
ccasinwell, I guess I see, but you couldn't wrote the program I just pasted in stlc03/12 01:57
Saizan_ccasin: it was unrelated to that03/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
ccasinSaizan: yes, definitely (at least in the US)03/12 02:07
dolioI'd stick with Church-style with STLC.03/12 02:08
ccasinthough I'll give that I grossly overstated the scope of the exercise :)03/12 02:08
ccasindolio: interesting. do you remember what book you first learned it from?03/12 02:09
dolioI'm not sure I learned from a book.03/12 02:09
dolioBut (\x -> x) is ambiguous in STLC.03/12 02:10
ccasinyes03/12 02:10
dolioAt least if you have a H-M-like system there's a "best" type for it.03/12 02:10
ccasinyes, I was just curious because most of the resources I've used have a preference for church style, there's always an annotation03/12 02:11
quantumEdwhy is it ambiguous?03/12 02:11
quantumEdit's just a lambda term, it's not a STLC term03/12 02:11
ccasinits type is ambiguous03/12 02:11
ccasinit could be any identity function03/12 02:11
quantumEdit doesn't have a type03/12 02:11
ccasinentirely unrelated question: are there any two Sets that agda can prove unequal?03/12 02:12
quantumEdccasin, is  P A and ~P B then A <> B03/12 02:13
quantumEdso can you find such a P, for say,  A = unit  and B = bool?03/12 02:13
quantumEds/is/if/03/12 02:13
ccasinwell, a good P would be "has just one element"03/12 02:14
ccasinI suppose that works03/12 02:14
ccasinlet me try it out03/12 02:16
copumpkinoh no, peer reversed dolio's arrows03/12 02:16
Saizan_uhm, learning from wikipedia gave me a weird notion of STLC :) or maybe it's the early exposure to HM03/12 02:18
* copumpkin gets all his information from wikipedia! you mean it's not 100% accurate???03/12 02:19
opdolioHM kind of makes the schemas of types you can give to Curry-style STLC terms into real types.03/12 02:19
ccasinquantumEd: that worked, thanks!  I guess I was being silly03/12 02:33
ccasinagda types are just to hard to get a handle on03/12 02:33
quantumEddon't think so03/12 02:33
quantumEdin particular say you hae bool and bool' both with two elements,  you can't prove them equal or apart03/12 02:34
ccasinquantumEd: 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 dolio03/12 02:39
Saizanccasin: what did you choose as P?03/12 02:48
ccasinSaizan: (s : Set) -> (A B : s) -> A = B03/12 03:16
byorgeyhey ccasin, are you back in Philly yet?03/12 03:24
ccasinbyorgey: yes, see you tomorrow!03/12 03:43
quantumEdhttp://old.nabble.com/Re%3A-Implicit-newtype-unwrapping-p26620156.html03/12 07:09
quantumEdeh ??03/12 07:09
copumpkinheh, people have a misconception of dependent types03/12 07:11
quantumEdpeople who don't understand dependent types think "If only we had dependent types, everything would be so easy!"03/12 07:13
copumpkinyeah!03/12 07:13
copumpkinI must admit that's what I thought too :P03/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
copumpkinthis seems to be advocating some sort of subtyping03/12 07:14
quantumEdmaybe he was thinking about coercions (like the stuff Luo is doing)03/12 07:15
dolioMaybe he meant Ada.03/12 07:18
-!- ski__ is now known as ski_03/12 12:49
-!- RichardO_ is now known as RichardO03/12 14:52
-!- RichardO_ is now known as RichardO03/12 15:38
-!- RichardO_ is now known as RichardO03/12 18:42
copumpkinis it normal for data and codata to both live in Set?03/12 21:34
dolioAs normal as it is for a language to have codata at all.03/12 21:51
--- Day changed Fri Dec 04 2009
BerengalCan I have a hint as to how to prove that Vec A (n + 0) == Vec A n?04/12 06:04
BerengalPreferably without recursing on the vector, instead employing the proof that n + 0 == n04/12 06:05
Saizanwith a subst04/12 06:05
copumpkinP = Vec A04/12 06:05
Saizanin the right universes04/12 06:05
copumpkinBerengal: so you already have the n + 0 == n proof?04/12 06:06
Berengalcopumpkin: yup04/12 06:06
copumpkinsubst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p04/12 06:07
copumpkindamn, more indirection :P04/12 06:07
copumpkinBerengal: did it work?04/12 06:09
Berengalcopumpkin: I'm not using the standard library, so I'm busy copy-pasting :P04/12 06:10
copumpkinoh ok :)04/12 06:10
copumpkinit's really simple to write04/12 06:10
BerengalYeah, but the definition of subst spans line a bajillion files, each containing one line...04/12 06:11
copumpkinhm?04/12 06:12
copumpkinoh you mean all the crazy indirection in the standard library04/12 06:12
Saizan_skip that :)04/12 06:12
copumpkinyou can have one line for the type and one line for the def04/12 06:12
copumpkinit's basically x == y -> P x -> P y04/12 06:13
copumpkinhttp://snapplr.com/taks04/12 06:15
copumpkinyou'd want it for any level04/12 06:15
copumpkinhttp://snapplr.com/9f2s04/12 06:17
copumpkinsomething like that, anyway04/12 06:17
Saizan_damn, typechecking Data.Rational takes more than 1.8GB of ram, using a 64bit ghc wasn't a good idea afterall04/12 06:21
copumpkinit's painful even with 32bit04/12 06:21
copumpkinI remember when I wrote some basic arithmetic for rationals it took forever to normalize even a simple expression04/12 06:21
Saizan_it wasn't that painful with agda-2.2.4 though04/12 06:22
copumpkinwe lost him!04/12 06:24
copumpkinoh wait, not really04/12 06:24
Saizan_that was my evil twin04/12 06:24
-!- Saizan_ is now known as Saizan04/12 06:24
copumpkinphew!04/12 06:25
copumpkinBerengal: what are you working on? or just playing around?04/12 06:27
BerengalJust playing around04/12 06:28
BerengalTrying to implement revappend04/12 06:28
copumpkinwhat does that do?04/12 06:28
copumpkinappends the reverse?04/12 06:28
Berengalflip (:)04/12 06:28
BerengalSo I can foldl it04/12 06:28
copumpkinoh04/12 06:28
copumpkinlike snoc?04/12 06:28
Berengalsnoc traverses the list though, doesn't it?04/12 06:29
copumpkinwell, it's just a general notion of sticking an element onto the end of something04/12 06:30
BerengalWell, foldl (flip (:)) [] just repeatedly takes an element in front of one list and conses it onto the other, until the list is empty04/12 06:31
copumpkinoh, so you want reverse04/12 06:31
BerengalEventually04/12 06:31
copumpkinI see04/12 06:31
BerengalSeems I got it not, thanks :)04/12 06:34
Berengalnow*04/12 06:34
copumpkinyay!04/12 06:36
copumpkinyou should name your subst moo btw04/12 06:36
copumpkinall the cool kids are doing it04/12 06:36
copumpkinBerengal: have you come across the two other handy functions? cong and sym?04/12 06:37
Saizanadn trans, and the equational reasoning pretty syntax04/12 06:40
copumpkinmmm04/12 06:40
Saizanthe "begin term \==\< proof \> ... \qed" one04/12 06:41
Berengalcopumpkin: Yup04/12 06:43
BerengalSaizan: That too. Stole it from Ulf's thesis04/12 06:43
BerengalExcept I switch to a hand-writing-ish font and use letters instead of symbols...04/12 06:45
Berengalhttp://forums.xkcd.com/download/file.php?id=1968204/12 06:46
copumpkinis 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
Saizanit seems so04/12 06:47
Saizani can check (using agda-executable) the whole stdlib using less than 700mb, there's something weird going on04/12 06:51
Saizanthat number is for Agda-2.2.404/12 06:51
Saizan(while for 2.2.5 i bump into the OOM killer)04/12 06:51
copumpkinthe calls for papers on the agda mailing list are a little annoying04/12 08:21
dolioWhat kind of cutting edge functional programming language mailing list doesn't have calls for papers?04/12 08:25
copumpkinthe most recent one seems to be an everything conference04/12 08:28
-!- whoppix_ is now known as whoppix04/12 17:32
boyscaredam 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
copumpkinthat isn't valid syntax04/12 18:25
copumpkinyou use a single colon for types, and you can't unify the type and the value setting that way04/12 18:26
boyscaredoops. ok, got a working example now. at least, i think its working04/12 18:31
quantumEdboyscared was that Agda 1 notation?04/12 18:40
boyscaredprobably, got it from here: http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda/agdainstallationFromBinaries.html04/12 18:41
quantumEdhm04/12 18:42
quantumEdso I already asked this but.. whats a good ref for de bruijn syntax?04/12 20:43
quantumEdhow do you state correctness of substitution?04/12 20:52
-!- copumpkin is now known as TheHunter04/12 23:13
-!- TheHunter is now known as copumpkin04/12 23:13
--- Day changed Sat Dec 05 2009
--- Day changed Sun Dec 06 2009
quantumEdthat fplunch STLC thing STILL hasn't updated06/12 01:58
dolioUpdated?06/12 02:02
quantumEdhoping for the author to reply to the comments but he doesn't seem to be aware they are there, or just doesn't want to06/12 02:03
dolioHe replied once, it looks like.06/12 02:07
dolioThat blog seems to have a lot of authors. Maybe they don't get notifications.06/12 02:09
dolioI must say, that program gives very nice looking output.06/12 02:43
* Saizan wants an unverse-polymorphic Vec06/12 09:50
copumpkinedit the file!06/12 09:51
copumpkinit's usually pretty mindless editing06/12 09:51
Saizanuhm, i get a weird error in the definition of splitAt06/12 10:00
copumpkinhm06/12 10:00
copumpkin?06/12 10:00
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=13667#a1366706/12 10:03
copumpkindoesn't it need to be universe polymorphic?06/12 10:04
copumpkinI guess it shouldn't have to be06/12 10:04
Saizanthe error stays the same if i add the indexes06/12 10:06
copumpkinweird06/12 10:06
copumpkinanother case of useless metas :P06/12 10:07
Saizanit's not hard to see what they refer to, but i've no idea what to try06/12 10:09
copumpkinregardless, it sounds like a bug?06/12 10:11
Saizanit might be06/12 10:11
Saizanuh, darcs pulling gives me a generalized Vec, apparently :)06/12 10:14
copumpkinhow does NAD deal with splitAt?06/12 10:14
copumpkinoh weird06/12 10:15
copumpkinvery different :)06/12 10:15
copumpkinit reads quite easily now, at least06/12 10:16
Saizanuhm, explicit equality proofs rather than indexes06/12 10:21
* Saizan wants more ram06/12 10:21
copumpkin:)06/12 10:22
dolioYeah, my 2 gigs doesn't cut it. :)06/12 10:23
yakovhello06/12 10:24
dolio8GB sticks are only $500. :)06/12 10:24
Saizanis there a vector type where the type of the elements depends on their position?06/12 11:27
dolioI doubt there's one in the library, but one could imagine such a thing.06/12 11:37
dolioInstead of Fin n -> A, it's (i : Fin n) -> T i.06/12 11:38
dolioThere'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
Saizani don't need telescopes for now06/12 11:42
Saizanmh, i wonder if i want to write a datatype like Vec or just a function like that06/12 11:43
Saizani need this for my MonadSolver attempt06/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
quantumEdexcellent that means I don't have to code it up in agda :P06/12 20:28
quantumEddolio congrats btw :P06/12 20:31
quantumEdyou got props from Oleg06/12 20:31
quantumEdhttp://www.e-pig.org/epilogue/?p=26306/12 21:49
copumpkinyay :)06/12 21:54
edwinbhehe06/12 21:54
edwinbPierre seems rather active. This is splendid news.06/12 21:54
edwinbI hope they have good cake in Tallinn06/12 21:55
pigmalionedwinb: 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
edwinboh, you're here, excellent :)06/12 22:36
pigmalionbut I'm not alone: Adam is doing a wonderful job too06/12 22:36
edwinbI must see if I can pop over to Glasgow at some point06/12 22:37
edwinbit's good that you have strong motivation anyway :)06/12 22:37
quantumEdpigmalion : oh you are Pierre!06/12 22:37
pigmalionedwinb: that would be great: I would like to compile that 2 + 2 with Epic06/12 22:37
quantumEdyou have a awesome part of your name "Evariste" :P06/12 22:37
pigmalionquantumEd: yes, I landed here for the first time a few hours ago, actually.06/12 22:39
edwinbI 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 case06/12 22:39
quantumEdwhat is your work about? if you're doing something to do with containers and OTT it's got to be interesting06/12 22:39
edwinbparticularly if it means I can show you how to wire it up to anything else that might come up06/12 22:39
pigmalionedwinb: please do, I'm extremely interested with Epic and what we could do with it06/12 22:42
quantumEd(and what is Cochon?)06/12 22:42
pigmalionquantumEd: 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 free06/12 22:43
pigmalionPeter Morris PhD thesis is a good intro to the field06/12 22:43
quantumEdbut you are taking it further?06/12 22:44
pigmalionoh, 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
pigmalionquantumEd: hopefully, yes :-D06/12 22:44
quantumEdin 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
pigmalionsome 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
edwinbI'd quite like to never have to write another data type that looks like a list06/12 22:46
pigmalionedwinb: exactly06/12 22:46
edwinband it's amazing how many things are just Nat with bells on06/12 22:47
pigmalionquantumEd: 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
quantumEdpigmalion well I don't want to sound like some kind of depraved thesis reading person but I really look forward to seeing this :P06/12 22:48
edwinbhehe. no pressure then :)06/12 22:49
pigmalionquantumEd: I'm just getting started, so I find myself in quite a lot of depravation, too :-)06/12 22:50
edwinbbecoming depraved is a good first step06/12 22:53
edwinber06/12 22:53
edwinbif you see what I mean :)06/12 22:53
pigmalion:-)06/12 22:54
quantumEdI 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 that06/12 22:57
edwinbpigmalion: are all the Strathclyde gang going to Pigweek in Tallinn?06/12 22:57
pigmalionedwinb: yes: Conor, Adam, and I (small gang but we have SuperNinja Conor)06/12 22:59
edwinbsplendid06/12 22:59
edwinbI should sort out my travel06/12 22:59
pigmalionedwinb: we should, too (Conor is taking care of the organization (read "this is complete chaos"))06/12 23:00
edwinbvery good06/12 23:00
pigmalionquantumEd: OTT is implemented but it's a pain to write the terms by hand: we are working on some "tacticals" and some automation06/12 23:01
pigmalionquantumEd: 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
quantumEdhm it's really awkward just to write small terms like this?06/12 23:03
edwinbwriting proof terms like that is always a pain06/12 23:04
pigmalionquantumEd, edwinb: I confirm06/12 23:04
quantumEdI mean it's just 3 lines or something in the paper06/12 23:04
edwinbyes, but you have to work out what those 3 lines are06/12 23:05
quantumEdisn't it the same with this implementation?06/12 23:05
edwinbwhich is something machines are usually better at06/12 23:05
pigmalionthere is an induction involved. Moreover, our Nat is not provided by the theory: it's encoded in a simplified inductive universe06/12 23:05
edwinbbut this'll all get fixed, in time...06/12 23:05
quantumEdby the way06/12 23:06
quantumEdoh never mind, I was going to ask something about recursion but I just realized the answer06/12 23:07
quantumEdhey is it possible to prove  forall f : A -> A, f = id  in OTT?06/12 23:13
quantumEdIf you defined some syntax of programs I guess you could get   f : "A -> A", [[ f ]] = id  via parametricity,06/12 23:14
pigmalionquantumEd: 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
quantumEdI just mean identity funciton,   id t = t   (but I am using an implicit for the type parameter)06/12 23:19
pigmalionI'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
quantumEdis stuffs a book or a term that just means a bunch of different things?06/12 23:26
edwinbyou never know with CT06/12 23:26
quantumEdoh does that mean there's some kind of universe heirarchy in OTT now?06/12 23:27
pigmalionquantumEd: 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
pigmalionquantumEd: hum. no. "That's on my Todo list", as one say.06/12 23:28
quantumEdthat's one problem I think is very tricky06/12 23:29
pigmalionit's very Tarsky, actually06/12 23:30
quantumEdhehe06/12 23:30
pigmalion;-)06/12 23:30
dolioquantumEd: I did?06/12 23:33
quantumEddolio yeah06/12 23:33
quantumEdhttp://okmij.org/ftp/Computation/differentiating-parsers.html06/12 23:34
quantumEdDan 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-mon06/12 23:34
quantumEdadic].06/12 23:34
quantumEdetc...06/12 23:34
quantumEdyou didn't know??06/12 23:34
dolioAh. No, I didn't.06/12 23:35
quantumEdah well nice work anyway06/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 Berengal07/12 06:36
quantumEdDarin Morrison Says:07/12 14:48
quantumEdI’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 Berengal07/12 16:08
-!- Berengal_ is now known as Berengal07/12 19:59
quantumEdhttp://www.cs.nott.ac.uk/~dwm/nbe/html/NBE.html07/12 20:06
quantumEd  nbe : ∀ {Γ α} → Γ ⊢ α → Γ ⊢ α07/12 20:07
quantumEd  nbe = completeness ∘ soundness07/12 20:07
quantumEdnice07/12 20:13
-!- Berengal_ is now known as Berengal07/12 20:14
Saizanvery nice07/12 20:32
--- Day changed Tue Dec 08 2009
-!- whoppix_ is now known as whoppix08/12 00:46
copumpkinallo allo!08/12 18:52
copumpkinfancy finding you here08/12 18:52
filcab42heh ;-) Hi08/12 18:53
Saizan_hi!08/12 18:53
filcab42Before asking questions I'll take a look at those URLs :-)08/12 18:53
copumpkinokay :)08/12 18:53
copumpkinthere's also a nice big tutorial pdf for agda08/12 18:54
copumpkinhttp://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf08/12 18:54
filcab42thanks :)08/12 19:01
-!- whoppix_ is now known as whoppix08/12 21:00
-!- copumpkin is now known as c0w08/12 23:31
-!- c0w is now known as copumpkin08/12 23:32
--- Day changed Wed Dec 09 2009
copumpkinsay I had a Vec of Nats09/12 01:51
copumpkinv = 1 :: 2 :: 3 :: []09/12 01:52
copumpkinnow I want map Fin v, which should give me a (in Set1) Fin 1 :: Fin 2 :: Fin 3 :: []09/12 01:53
copumpkinis there a nice way to create a heterogeneous vector of values from that vector of sets?09/12 01:53
copumpkinso 0 :: 0 :: 2 :: [] would be one of the six values in that09/12 01:54
copumpkinseems sort of like a "zipped" type09/12 01:57
copumpkinI could do it with a Vec of Sigmas probably09/12 01:57
copumpkinbut that doesn't feel very clean09/12 01:57
copumpkinmaybe it's the only way though09/12 01:58
copumpkinmmm, the latest std lib gives me09/12 02:06
copumpkinFailed to solve the following constraints:09/12 02:06
copumpkin  Set (a ⊔ ℓ) =< Set (a ⊔ ℓ)09/12 02:06
copumpkinthat seems like something it should be capable of solving on its own :)09/12 02:06
* copumpkin recompiles agda09/12 02:07
copumpkinI made a special HeteroVec type that takes a Vec of types09/12 02:20
copumpkinfeels ugly though09/12 02:20
copumpkinanyone have a better name than HeteroVec?09/12 02:44
copumpkinI was hoping to be able to make HeteroVec self-reliant09/12 02:53
copumpkinbut it can't refer to itself09/12 02:53
copumpkinI guess that would lead to an infinite type09/12 02:54
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=13856#a13856 is what I have09/12 03:03
-!- kmc__ is now known as kmc09/12 04:44
doliocopumpkin: HeteroVec would be inductively defined products/tuples.09/12 06:09
SaizanAll Fin v ?09/12 06:23
Saizan_except that Vec has no All09/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 stdlib09/12 08:59
dolioPartial orders and monotone functions form a category.09/12 09:09
dolioI don't recall anything like that in the standard library, though.09/12 09:09
dolioLots 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 predicates09/12 09:34
Saizan_assuming i understand it09/12 09:35
copumpkinit sure would be nice if two different types could get the number literal sugar at once09/12 16:59
copumpkinsince they enforce that the sugar be attached to constructors in the first place09/12 16:59
copumpkinand constructors can be disambiguated09/12 16:59
Saizan_yes, i want typeclasses too09/12 17:07
copumpkintypeclasses would be nice, but if not those, then just a special case for number literals09/12 17:07
copumpkinand maybe a magic unraveler of number literals when types get printed, too09/12 17:07
copumpkinoh I guess it already does that09/12 17:08
copumpkinis that new?09/12 17:08
Saizan_unraveler?09/12 17:13
copumpkinwell, something that takes suc (suc (suc zero)) in a type and replaces it with 309/12 17:13
quantumEdbut 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
copumpkinhm, for some reason it can't solve a constraint09/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 = here09/12 18:23
copumpkinI wrote this a while ago and it worked :o09/12 18:24
copumpkinmaybe the std lib changed subtly09/12 18:25
quantumEdwhat's the type of here? I don't see how that typechecks09/12 18:27
quantumEdoh wait I see it09/12 18:27
copumpkinthat's just one case09/12 18:27
copumpkinI can give the rest of it if you'd like09/12 18:27
quantumEdnah I was just wondering if here knew about ++ but I see that it doesn't need to nw09/12 18:27
copumpkin:)09/12 18:28
copumpkinbut for some reason it doesn't like that anymore09/12 18:28
copumpkinI'm reasonably confident it used to work09/12 18:28
copumpkinhttp://snapplr.com/8jkp09/12 18:29
copumpkinwait, wrong error09/12 18:30
copumpkinhttp://snapplr.com/9mwf09/12 18:30
copumpkinah09/12 18:31
copumpkina : Set09/12 18:31
copumpkinmeh :)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
copumpkinFinite : Set → Set09/12 19:33
copumpkinFinite A = Σ (List A) (λ v → ∀ x → x ∈ v)09/12 19:33
copumpkinInfinite : Set → Set09/12 19:33
copumpkinInfinite A = ¬ Finite A09/12 19:33
copumpkinit's mostly because I can't reverse the mapping09/12 19:34
copumpkinmaybe if I chose another representation for Finite it would be possible?09/12 19:35
quantumEdttt-- what does that mean ??09/12 19:36
ttt--my name doesnt mean anything if that was the question09/12 19:36
quantumEdwhen you said infinite what do you mean by it09/12 19:37
ttt--oh09/12 19:37
quantumEdand something09/12 19:37
copumpkinToposes, Triples and Theories!09/12 19:37
Saizan_copumpkin: maybe you need a left-inverse instead of just injectivity?09/12 19:37
copumpkinSaizan_: intuitively (classically) it seems like injectivity should be enough09/12 19:37
copumpkinbut I guess I do09/12 19:38
Saizan_classically they are equivalent, afaiu09/12 19:38
copumpkinI think Injective/Surjective/Bijective should be in Data.Function09/12 19:38
Saizan_there's some of that somewhere09/12 19:39
copumpkinoh09/12 19:39
copumpkinI was trying to find it and failed09/12 19:39
quantumEdttt--, well ?09/12 19:39
ttt--I was just wondering how copumpkin was doing things. I dont really know anything09/12 19:40
Saizan_in Relation.Nullary09/12 19:40
quantumEdoh I didn't make the link I just thought that was an independent question09/12 19:40
copumpkinSaizan_: http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.html#340 ?09/12 19:40
copumpkinthat gives you a bijection09/12 19:40
quantumEdyeah me too09/12 19:40
quantumEdcopumpkin can you paste it all up to the theorem you haven't prove yet ??09/12 19:41
Saizan_my Relation.Nullary looks quite differently09/12 19:41
copumpkinsure, but it's really ugly09/12 19:41
quantumEdthat's ok09/12 19:41
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=13885#a13885 at the bottom09/12 19:42
Saizan_oh, there's Relation.Nullary.Injection and .LeftInverse now09/12 19:42
copumpkinooh09/12 19:42
copumpkinack, Setoids09/12 19:43
copumpkinhttp://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 scary09/12 19:44
Saizan_those long arrows do :O09/12 19:46
copumpkinso I guess the only way to do this is with a left inverse09/12 19:47
* copumpkin sighs09/12 19:47
quantumEdI told you 'injective' is useless :P09/12 19:48
copumpkinit breaks the symmetry of finite=>surjective=>finite and infinite=>injective=>infinite09/12 19:48
dolioWhy is that a "nullary" relation?09/12 19:48
quantumEdthis is constructive math09/12 19:48
* copumpkin weeps09/12 19:48
copumpkinmaybe if I whine enough constructive math will listen and be nice09/12 19:49
* Saizan_ puts copumpkin inside a double negation09/12 19:49
* copumpkin pops right back out, unchanged09/12 19:49
copumpkinI bet you thought you could trap me09/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_hah09/12 19:50
copumpkinsorry, really bad :P09/12 19:50
* copumpkin goes back to his corner and weeps09/12 19:50
copumpkinbut yeah, I'm not sure why it's a nullary relation either09/12 19:52
copumpkinmaybe unary09/12 19:52
Saizan_{A : Set} -> A -> Set is unary, Set is nullary09/12 19:53
copumpkinit'd be nice to be able to write (f : a -> b) -> Bijective f  -> (b -> a)09/12 19:53
Saizan_according to the comments09/12 19:53
copumpkinoh, I can write Bijective=>Inverse : ∀ {a b} → (f : a → b) → Bijective f → (b -> a)09/12 19:55
copumpkinat least that09/12 19:55
copumpkinhrrmpf09/12 19:55
dolioI guess it's that f LeftInverseOf g is nullary, not _LeftInverseOf_.09/12 19:56
dolioWhereas _==_ is a binary relation on a single type or something.09/12 19:57
Saizan_how is Bijective defined?09/12 19:57
copumpkinBijective f = Injective f × Surjective f09/12 19:57
copumpkinSurjective f = ∀ y → ∃ (λ x → f x ≡ y)09/12 19:58
dolioSurjective lets you write b -> a, doesn't it?09/12 20:00
copumpkinyep09/12 20:00
dolioAnd 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
quantumEdcopumpkin 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 pigeonhole09/12 20:10
copumpkingenerator in what sense?09/12 20:11
quantumEdsomething which gives you as many distinct elements of the type as you want09/12 20:11
copumpkinhow would you phrase that? the only ways I can think of would imply it being countably infinite09/12 20:12
quantumEdthat shouldn't be a problem, if you have an uncountable infinity the generator only needs to generate a countable subset09/12 20:13
copumpkinso just Nat -> a ?09/12 20:14
quantumEdI was thinking  (n : Nat) -> FreshVector A n09/12 20:14
quantumEd(fresh meaning every element you cons on is different from all the ones before)09/12 20:14
copumpkinhm!09/12 20:15
copumpkinI'll try that09/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 secs09/12 20:35
quantumEdI 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 property09/12 20:35
quantumEdthat's what I meant by isomorphism09/12 20:35
copumpkinah09/12 20:36
copumpkinwell, injectivity as I have it doesn't give you a left inverse09/12 20:36
copumpkinInjective f = ∀ {x y} → f x ≡ f y → x ≡ y09/12 20:37
quantumEdso change it :P09/12 20:37
copumpkinlol09/12 20:37
copumpkinbam! Injective : ∀ {a b : Set} → (a → b) → Set09/12 20:38
copumpkinInjective {a} {b} f = (∀ {x y} → f x ≡ f y → x ≡ y) × b → Maybe a09/12 20:38
copumpkin;)09/12 20:38
copumpkinnow I can do it with my negated Finite representation too, though09/12 20:38
quantumEdInjective : forall {A B : Set} (f : A -> B) -> Set09/12 20:40
quantumEdInjective f = ∀ {x y} → f x ≡ f y → x ≡ y09/12 20:40
quantumEdinj : forall {A B : Set} (f : A -> B) -> Injective f -> ∀ x y -> ¬ x ≡ y -> ¬ f x ≡ f y09/12 20:40
quantumEdinj f feq-prf x y ≠xy fx-fy = ≠xy (feq-prf fx-fy)09/12 20:40
quantumEdwhat about that ?09/12 20:40
copumpkinlooks reasonable09/12 20:42
copumpkindoesn't give me a left inverse though09/12 20:42
quantumEdwhat do you want a left inverse for?09/12 20:42
copumpkinmaybe I don't. I thought I still needed one to get the infinite->injective->infinite proof09/12 20:42
--- Day changed Thu Dec 10 2009
copumpkinwe need inductively defined algebraic structures!10/12 00:38
quantumEdlike universal algebra?10/12 00:39
copumpkinyeah, but more general than what universal algebra appears to deal with10/12 00:39
quantumEdhuh??10/12 00:40
copumpkinuniversal algebra appears to avoid structures with conditional laws10/12 00:40
copumpkinthings like "every element except 0 has an inverse"10/12 00:40
copumpkinunless I'm missing something10/12 00:40
copumpkinapparently the notion of conditional laws is linked to the existence of free structures10/12 00:41
copumpkinbut I don't necessarily care10/12 00:41
copumpkinI'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 objects10/12 00:45
quantumEdwhy?10/12 00:53
quantumEdcan't tell if it's model theory of universal algebra10/12 00:54
quantumEdor**10/12 00:54
copumpkinwell, 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 need10/12 00:55
copumpkinyou 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
copumpkinbasically describing only the relationships between those three things10/12 00:57
copumpkinI mostly don't feel that the current approach is very flexible. For example, IEEE Floats fail associativity but have many other useful properties10/12 00:59
copumpkinpretty much every named structure of interest assumes associativity10/12 01:00
copumpkinif I can specify that my function needs commutativity and an identity element for +, but I don't rely on associativity10/12 01:00
copumpkinI can use floats without worrying about error10/12 01:00
* copumpkin shrugs, it might be a silly idea but I like thinking about it10/12 01:02
quantumEdwhy is it a silly idea?10/12 01:03
copumpkinI don't know :)10/12 01:03
copumpkinI would really just like to make Algebra more usable in programming10/12 01:04
quantumEdme too10/12 01:04
quantumEdhaev you seen CoRN10/12 01:05
copumpkinnope10/12 01:05
copumpkinlooks like a coq module?10/12 01:05
copumpkinaha10/12 01:06
copumpkinthe documentation looks enormous10/12 01:06
copumpkinover 10k entries :O10/12 01:06
copumpkinnow that I think about it10/12 01:47
copumpkinSurjective : ∀ {a b : Set} → (a → b) → Set10/12 01:47
copumpkinSurjective f = ∀ y → ∃ (λ x → f x ≡ y)10/12 01:47
copumpkinisn't that isomorphic to b -> a ?10/12 01:47
copumpkinoh wait, it gives me a little more information10/12 01:48
Saizanis there a tutorial to convert yourself from typeclasses to modules?10/12 16:31
* Saizan would really like to overload \p10/12 16:31
Saizanerr, \o10/12 16:31
copumpkinit seems like Data.Graph.Acyclic's graph type is ismorphic to a Vec10/12 20:59
copumpkinI guess not exactly10/12 21:02
copumpkinwow, agda gets ridiculously slow when there are lots of unsolved metas10/12 21:49
copumpkinit's taking literally about 10 minutes every time I try to load a Data.Graph.Acyclic that I'm converting to universe polymorphism10/12 21:50
Saizanis it using a lot of memory too?10/12 21:55
copumpkinonly about 500 megs10/12 21:56
jmcarthur_work"only"10/12 22:02
copumpkin:)10/12 22:03
copumpkindammit, more yak shaving10/12 22:03
copumpkinnow I need to universe-polymorphism-ize Data.List too10/12 22:03
Saizanisn't it already?10/12 22:03
copumpkinoh it appears to be10/12 22:03
copumpkinI wonder why this fails then10/12 22:03
SaizanAny/All aren't yet, though10/12 22:04
copumpkinoh that's why10/12 22:04
copumpkinnot Any/All10/12 22:05
copumpkinjust a helper function stil in Set10/12 22:05
jmcarthur_worki need to try agda again now that it has universe polymorphism. that was one of my bigger complaints about it in the past10/12 22:14
copumpkindammit, I can't get this helper function to work10/12 22:14
copumpkinhttp://snapplr.com/mqy810/12 22:15
copumpkinthere isn't even a w there!10/12 22:15
jmcarthur_workwhat proposal won, anyway? the one i liked the most was the universe index as parameter idea10/12 22:15
jmcarthur_workof the ones i knew about, anyway10/12 22:15
copumpkinthere's a magic Level type that's isomorphic to Nat10/12 22:16
copumpkinand Set can take that as a parameter10/12 22:16
copumpkinstrangely enough, writing Set on its own gives you just a regular Set10/12 22:16
jmcarthur_workany reason it has to be magic? is it so that it's outside of the Set hierarchy?10/12 22:16
copumpkinbut it can also take parameters of levels10/12 22:16
copumpkinI think so10/12 22:16
copumpkinit is defined in agda too10/12 22:16
copumpkinbut it has some BUILTIN magic pragmas attached to it10/12 22:16
jmcarthur_workoh i see10/12 22:16
jmcarthur_workso if it's defined in agda it must be declared as Level : Set then?10/12 22:18
jmcarthur_worki'll just look it up on my own instead of making somebody else do it. sorry10/12 22:19
jmcarthur_workhuh, it is indeed Level : Set10/12 22:20
jmcarthur_workokay, i have no idea why it's not just Nat now10/12 22:20
copumpkinthere was a post on the mailing list about it, can't remember now10/12 22:21
Saizancopumpkin: is that from the stdlib, or?10/12 22:22
* Saizan grepped10/12 22:22
copumpkinSaizan: yep it is10/12 22:32
copumpkinbut I'm editing it to be universe-polymorphic10/12 22:32
copumpkinSaizan: by the way about your earlier question10/12 22:35
copumpkinSaizan: they aren't exactly the same thing10/12 22:35
copumpkintypeclasses, as far as I can see, are like parametrized modules + implicit parameters + automatic instance lookup10/12 22:36
Saizani meant from a pratical point of view10/12 22:39
copumpkinmodule Eq {A : Set} where _==_ : A -> A -> Bool10/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
copumpkinI guess that isn't it10/12 22:40
copumpkinhmm, I wonder10/12 22:40
Saizani think you'd make Eq a record10/12 22:40
copumpkinyeah10/12 22:40
Saizanso you can have instances10/12 22:40
Saizanbut if you need more than one instance in the same chunk of code, how do you do it? especially with infix operators10/12 22:41
copumpkinI don't think there's an elegant way to do it10/12 22:42
Saizananother options is record Eq where field Carrier : Set; _==_ : Carrier -> Carrier -> Bool, actually10/12 22:42
copumpkinif you parametrize Eq by the carrier, it might be able to infer it more10/12 22:43
copumpkinnot sure10/12 22:43
* copumpkin shrugs :)10/12 22:43
Saizanor 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 practical10/12 22:44
copumpkinvalue?10/12 22:44
Saizanyeah, you bundle up the data with the methods10/12 22:45
copumpkinoh10/12 22:45
copumpkinugh :)10/12 22:45
SaizanInjective or LeftInverse look in that style10/12 22:45
copumpkinyeah10/12 22:46
Saizani guess it doesn't make much sense with binary methods, though10/12 22:46
copumpkinanyone have any ideas about that weird error I'm getting in Acyclic?10/12 22:56
quantumEdwhat error?10/12 22:58
copumpkinhttp://snapplr.com/mqy810/12 22:58
copumpkinit's talking about an expression w that I can't even see10/12 22:58
Saizanthat's probably something you're pattern matching over10/12 22:59
copumpkinhm? I didn't even write that function, just added a Level impicit parameter10/12 22:59
Saizanmh10/12 23:00
copumpkinone thing that bothers me about implicit args is their left-to-right-ness10/12 23:31
copumpkinadding universe polymorphism forces us to add levels to all our functions that need to be polymorphic10/12 23:31
copumpkinso now f {X} binds X to the level10/12 23:31
quantumEdI think there's f {a = b} to set a particular (a) implicit field10/12 23:43
copumpkinyeah10/12 23:43
copumpkinthat's what I'm using now10/12 23:43
copumpkinbut 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 pattern10/12 23:43
quantumEdso there needs to be implicit implicit parameters10/12 23:44
copumpkina universe of implicitness!10/12 23:45
copumpkinbah, more yak shaving10/12 23:51
copumpkinnow need to change wellfounded induction to be universe-polymorphic10/12 23:51
--- Day changed Fri Dec 11 2009
Saizan_send patches when you're done :)11/12 00:01
copumpkinyep :)11/12 00:24
copumpkinis there a quick way to jump to a file something is defined in?11/12 00:26
copumpkinit says "click mouse-2 to jump to definition"11/12 00:26
copumpkinbut I'm not sure if I have a mouse 211/12 00:26
copumpkinaha, found it11/12 00:36
copumpkindoes it make sense to universe-polymorphize Pred?11/12 00:43
copumpkinPred : Set -> Set111/12 00:43
copumpkinPred a = a -> Set11/12 00:43
quantumEdpred ??11/12 00:44
copumpkinRelation.Unary11/12 00:45
quantumEdwhat is it11/12 00:45
copumpkinthe Induction stuff relies on it11/12 00:45
copumpkinjust a Predicate about something11/12 00:45
copumpkinPred Nat11/12 00:45
copumpkincould be prime11/12 00:45
quantumEdoh it means predicate on <set>11/12 00:45
copumpkinyeah11/12 00:45
quantumEdthese abbreviations suck..11/12 00:45
copumpkinoh I see, you could see it as the opposite of suc :P11/12 00:46
copumpkinhadn't thought of that11/12 00:46
copumpkinhmm, is there an easy way to inject a Set A into a Set (A \lub B) ?11/12 00:50
copumpkinhmm, stuck trying to fit a Set into a bigger one :(11/12 01:01
copumpkin.ℓA != .ℓB ⊔ .ℓA of type Level11/12 01:01
copumpkinwe need NAD or Ulf in here11/12 01:10
copumpkinnot that they'd be awake anyway11/12 01:10
copumpkindoes it make sense for _|_ to live in an arbitrary Set level?11/12 01:13
copumpkinmeh, putting it in an arbitrary level breaks a bajillion modules11/12 01:25
copumpkinwell, puts unresolved metas in them11/12 01:25
copumpkinthis might be why Relation.Unary is still not polymorphic11/12 01:29
copumpkindammit, so much yak shaving to get that damn graph module polymorphic11/12 01:41
uoryglHum, it shouldn't be hard to implement Dedekind cuts in Agda.11/12 01:44
uoryglThe standard library has natural numbers, right? Does it have integers? Rational numbers?11/12 01:47
copumpkinyeah^311/12 01:47
copumpkinbut rationals have almost no functionality11/12 01:48
copumpkinthere's apparently functionality coming to them11/12 01:48
uoryglWhat would functionality consist of?11/12 01:48
copumpkinbasic arithmetic, proofs about them, and so on11/12 01:49
* uorygl nods.11/12 01:49
copumpkindo you know how to raise a Set a to Set (a \lub b) ?11/12 01:51
copumpkinI guess I can use subst11/12 01:51
uoryglHum. The typechecker evaluates all the types it receives, right?11/12 01:52
copumpkinif they're data11/12 01:53
copumpkinλ ℓ → Set ℓ -- what is the type of this? Set\_\omega ?11/12 01:53
copumpkinx : (x : Level) → Set (suc x)11/12 01:54
copumpkinfair enough11/12 01:54
uoryglSo it might make sense to pass around thunks, if I don't want the typechecker to actually evaluate stuff.11/12 01:56
copumpkinyou'd probably want codata11/12 01:57
uoryglWhat's that?11/12 01:57
copumpkincoinductively defined data11/12 01:58
copumpkincan be infinite, defined just by observations on the data rather than by constructing it11/12 01:58
uoryglYeah, I think I know that.11/12 01:59
uoryglShould I ask whether Agda supports that?11/12 02:00
copumpkinit does!11/12 02:00
copumpkinjust write codata instead of data11/12 02:00
copumpkinfor your data definition11/12 02:00
copumpkinor if you prefer to be more modular11/12 02:00
copumpkinjust import Coinduction from the standard library and use the \inf type11/12 02:00
uoryglNeat.11/12 02:00
copumpkinfor examples check out Data.Colist or Data.Conat11/12 02:01
* uorygl ponders evil things.11/12 02:01
copumpkinbut it's worth mentioning that sometimes it can be quite painful to prove to the termination checker that your functions terminate11/12 02:01
uoryglIndeed.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 t11/12 02:03
uoryglA 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
uoryglThere, 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
copumpkinthat function is really screwing me in Relation.Unary11/12 02:21
copumpkinbah!11/12 02:24
copumpkinI just commented that out for now, but so much trouble making stuff universe-polymorphic!!!11/12 02:27
copumpkinthe problem with sticking _|_ in an arbitrary universe is that it never seems able to infer the universe11/12 02:38
copumpkinso you'll need an explicit parameter on it11/12 02:38
* copumpkin may have to wait for NAD to do this :(11/12 02:41
* copumpkin doesn't know enough about it all11/12 02:41
copumpkinwow, up to 1 gig11/12 03:22
copumpkinData.Graph.Acyclic is murder11/12 03:22
copumpkindoes emacs with agda-mode steal focus for anyone else?11/12 03:36
copumpkinor is it just aquamacs?11/12 03:36
copumpkinthis 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
uoryglMeh. Do we have a speedy built-in arithmetic thing?11/12 03:45
copumpkinnope11/12 03:46
uoryglAww.11/12 03:46
* uorygl ponders making a semi-speedy digital arithmetic thing.11/12 03:47
copumpkinaha, the slowdown in the graph module is the tests11/12 03:47
* uorygl sticks with his Peano.11/12 03:47
uoryglWe don't have equality testing either, do we.11/12 03:50
copumpkinwell11/12 03:52
copumpkinthere's \==11/12 03:52
uoryglDoes \==\ already mean something?11/12 04:05
copumpkindoubt it11/12 04:05
uoryglEr, \==11/12 04:12
solidsnackWhat is meant by \== and \==\ ?11/12 04:12
uorygl\==\ is a typo.11/12 04:12
solidsnackOh.11/12 04:12
uoryglIs \top the same thing as T?11/12 04:15
uoryglIf not, then I have a true fontfail here.11/12 04:15
copumpkinno11/12 04:17
copumpkin⊤ vs T11/12 04:18
* uorygl gives his font a stern look.11/12 04:23
copumpkin:)11/12 04:24
copumpkinalright, that's enough agda for tonight. With any luck NAD will have a beautiful solution to the problems I posted to the mailing list11/12 04:39
* copumpkin has decided to represent algebraic structures as DAGs11/12 07:55
Saizan_:O11/12 08:04
copumpkin:O indeed11/12 08:05
copumpkinI'll probably fail, but I'll have fun trying11/12 08:05
copumpkinonce I get that Data.Graph.Acyclic working with universe polymorphism11/12 08:05
Saizan_i was going to use LeftInverse from the lib, but all the setoid overhead is putting me off11/12 08:17
copumpkinyeah :/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 secs11/12 20:02
-!- mak__ is now known as comak11/12 20:06
-!- Berengal_ is now known as Berengal11/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 -> C12/12 19:13
quantumEdreally??12/12 19:14
quantumEdwhat if you shuffle the ordering about a bit12/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
quantumEdwhat if it's lambda instead of forall, for the levels?12/12 19:15
Saizan_it works12/12 19:16
quantumEdcan'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 secs12/12 20:06
quantumEdI dont know what you mean12/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 idea12/12 20:09
quantumEdbut if lambda-foo typechecks then why doesn't foo?12/12 20:09
quantumEdthat's weird12/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, afaiu12/12 20:11
quantumEdwell I don't understand this12/12 20:12
Saizan_so you'd have to find a level "suc (a ⊔ b ⊔ c)" for any a b c, leading to omega12/12 20:12
Saizan_but it's not fully clear to me either12/12 20:12
doliofoo has type Set omega, and you're not allowed to name things of type Set omega.12/12 20:13
dolioI think it has that type, at least.12/12 20:13
quantumEdwhy does it have that type12/12 20:13
dolioGiven 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
doliofoo = 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
dolioIf 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 bindings12/12 20:25
dolioThen people will just complain that we need transfinite universe polymorphism to make the transfinite set shuffling functions more uniform. :)12/12 20:25
quantumEdSet omega : Set omega haha12/12 20:25
dolioThere's nothing wrong with giving names to things of type Set omega, though. As an alias.12/12 20:27
dolioBut 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 implications12/12 20:28
Saizan_it says Set omega is not a valid type if you try that12/12 20:28
dolioMy 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
quantumEdI don't get it12/12 20:29
dolioBut you can't write, say, "\(x : Set omega) -> ..."12/12 20:29
dolioOr \ whatever -> something-of-type-Set-omega12/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
dolioI'm not sure you could just have ordinal levels, either.12/12 20:32
dolioFor instance, I was thinking about 'finite set' universe polymorphism.12/12 20:34
dolioWhere you might have (x : Level 5) -> Set x live in Set 6.12/12 20:35
dolioBut 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
dolioLike, (i : Fin 5) -> Set (finToFinLevel i), is that in Set 6, too?12/12 20:37
dolioCrap, 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
dolioBut then what about (i : Fin 5) -> Set (finToFinLevel i + 1), that needs to be in Set 7.12/12 20:38
dolioOr 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
quantumEddependent types to the rescue!12/12 20:39
Saizan_what's the type of finToFinLevel, actually?12/12 20:39
dolioFin n -> Level n, I guess.12/12 20:39
Saizan_uhm, right, it just feels weird that levels are regular datatypes12/12 20:41
quantumEdeyah I don't really understand the point12/12 20:41
dolioWell, 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
dolioI don't remember what it was, though.12/12 20:42
dolioIt may have been smaller versions of the universal sums I have going.12/12 20:43
quantumEdhey 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
dolioSo, 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
dolioNo, I got distracted and haven't worked on my new type theory in a while.12/12 20:45
dolioIt'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 exercise13/12 12:26
ttt--http://hpaste.org/fastcgi/hpaste.fcgi/view?id=1408613/12 12:26
ttt--if anyone is interested :)13/12 12:26
Saizaninstead of defining those get* methods i'd use the module system13/12 12:41
Saizanespecially open13/12 12:41
Saizane.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
Saizanand if you have many definitions all parametrized on a single functor you can group them in a module and make that module parametrised instead13/12 12:44
Saizane.g. the laws13/12 12:44
Saizanttt--: like this http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a1408713/12 12:48
ttt--yeah that looks better, thanks :)13/12 12:49
ttt--http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a1408913/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 there13/12 13:09
* ttt-- goes to read how modules work13/12 13:10
Saizanttt--: you can only use records as parameters13/12 13:24
Saizanttt--: while Functor there refers to the outer one13/12 13:24
Saizanyou can use Functor.Functor i guess13/12 13:25
Saizanoh, you already found that :)13/12 13:28
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14086#a14094 <- how i'd write it13/12 13:30
Saizanis there a sane way to write this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14110#a1411013/12 17:36
Saizanfound it http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14110#a1411113/12 17:47
-!- zarvok is now known as ccasin13/12 20:10
--- Day changed Mon Dec 14 2009
Saizanthere'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
quantumEdno I still don't know a good way to state it14/12 23:37
Saizan_it seems like zippers could be relevant, but i'm wondering too14/12 23:41
quantumEdI have to hope its not just something you got to program carefully14/12 23:58
--- Day changed Tue Dec 15 2009
-!- boyscare1 is now known as boyscared15/12 02:59
-!- boyscare1 is now known as boyscared15/12 17:18
EnglishGentwould 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
Saizanit'd be pink15/12 20:39
Saizani.e. it wouldn't pass the termination checker15/12 20:40
dolioYou can define recursion combinators that look a lot like Y.15/12 21:16
dolioLike, 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 x15/12 21:19
dolioMissing the evidence that _<_ is well founded there, of course.15/12 21:20
dolioBut, if you erase the x, y and z, and associated stuff, you get (P -> P) -> P.15/12 21:21
Saizanyou can abstract over the _<_ or you've to write a specific combinator for each _<_?15/12 21:21
dolioYou can define a type Wf : {A : Set} (_<_ : A -> A -> Set) -> Set that encodes the necessary stuff.15/12 21:22
dolioSo a general combinator would have an Wf _<_ as an argument.15/12 21:23
Saizani see15/12 21:24
dolioActually 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
dolioThen WF _<_ would be forall x -> Acc _<_ x15/12 21:26
dolioI'm not sure what a relation with accessible elements that isn't well-founded would look like, exactly, though.15/12 21:29
dolioMaybe 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
dolioOr, that's probably not a good way to put it.15/12 21:31
dolioYou 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
dolioTo 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
dolioBut 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
dolioOh, 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
dolioI 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 copumpkin15/12 21:50
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14275#a14275 <- i thought it'd be more complicated15/12 22:14
dolioNope, that's it.15/12 22:14
dolioProving that an ordering is well founded/an element is accessible is the trickier bit.15/12 22:15
Saizanheh, i imagine15/12 22:17
dolioIt isn't really that hard for, say, the usual ordering on the naturals.15/12 22:17
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14275#a14279 <- nice when you can just fool around until it typechecks :)15/12 22:45
dolioHeh. I like your equational proof.15/12 22:48
Saizanso explicit, eh? :)15/12 22:56
copumpkinP=NP = _15/12 22:56
-!- EnglishGent is now known as EnglishGent^afk15/12 23:18
--- Day changed Wed Dec 16 2009
HaskellLovei 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 CoqBloq16/12 07:04
-!- EnglishGent^afk is now known as EnglishGent16/12 14:52
--- Day changed Thu Dec 17 2009
-!- opdolio is now known as dolio17/12 00:57
soupdragondoes agda 2.2.4 have universe polymorphism?17/12 07:01
dolioI don't think so.17/12 07:02
dolioThat's the one on hackage, right?17/12 07:02
soupdragonyeah17/12 07:02
dolioThere's a bijection between Nat and (Nat -> Bool) -> Bool if we assume some wacky non-classical axioms, right?17/12 07:04
soupdragonwoah17/12 07:05
soupdragoncan'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
dolioLike, all functions are continuous or something.17/12 07:05
dolioYes. I thought so.17/12 07:06
soupdragonoh you said *non*-classical axioms17/12 07:06
dolioIn a constructive/intuitionistic theory.17/12 07:06
dolioAnd yes, it's weird.17/12 07:07
soupdragonI was wondering if all functions were differentiable, but it turns out you can define abs17/12 07:08
dolioEspecially 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
dolioSo that isn't really a general criterion for being 'bigger', although I guess it still works for Nat.17/12 07:12
dolioAt least, not with the "all functions are continuous" axiom, if it implies what I seem to recall.17/12 07:13
Saizanistr that too17/12 07:14
soupdragonI don't know what you mean by the surjection17/12 07:14
Saizannot sure how you'd even state that axiom though17/12 07:15
soupdragonwhich one?17/12 07:15
Saizanthat all functions are continuous17/12 07:15
dolioI 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. too17/12 07:16
dolioVia Cantor's diagonalization argument.17/12 07:17
Saizanf is surjective if (y : B) -> Σ A λ x → f x ≡ y17/12 07:17
soupdragonof course the eps/delta is a consequence of the general topological definition17/12 07:21
soupdragonI think it goes the other way too17/12 07:21
dolioI assume you can only do epsilon/delta in a metric space, though?17/12 07:22
dolioOr, some generalization that still has something like a metric?17/12 07:22
* dolio knows almost no topology.17/12 07:23
soupdragonI onl yknow an epsilon of topology17/12 07:25
soupdragongod dammit17/12 07:32
soupdragonbootstrap forkbombed me what the hell17/12 07:32
soupdragonlast time I did this it was easy17/12 07:44
Saizandid what?17/12 08:22
soupdragoninstalled agda17/12 08:38
-!- jlouis_ is now known as jlouis17/12 17:04
soupdragonBerengal17/12 23:01
soupdragonI dream of writing ZFC in Agda :(17/12 23:01
soupdragonusing polymorphism to make the powerset17/12 23:01
soupdragonhm am I mixing you with someone else17/12 23:37
--- Day changed Fri Dec 18 2009
-!- whoppix_ is now known as whoppix18/12 00:18
soupdragonhttp://www.e-pig.org/epilogue/?p=26618/12 16:49
Saizansoupdragon: Epic should be the implementation of OTT?18/12 19:42
soupdragonI don't think so, I don't know18/12 19:42
soupdragonEpic is a simple functional language which compiles to reasonably efficient C code18/12 19:57
soupdragonit must be OTT is compiling into this language, which Epic turns into C18/12 19:57
soupdragonxwell not OTT but the OTT implementation18/12 19:57
dolioBoy, some people really have a lot of trouble with the diagonal argument.18/12 20:01
soupdragonlike how?18/12 20:01
dolioLike 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
dolioProvably, on a computer.18/12 20:02
soupdragonsounds like the found happyness already18/12 20:02
soupdragonbb..but.. computers can't prove things! :P18/12 20:02
dolio:)18/12 20:03
soupdragon"they can only disprove"18/12 20:03
copumpkin_wow18/12 20:03
-!- copumpkin_ is now known as copumpkin18/12 20:04
dolioYeah, the computer theorem prover angle didn't accomplish a lot.18/12 20:04
soupdragonthis is specific case?18/12 20:04
doliohttp://scienceblogs.com/goodmath/2009/12/another_cantor_crank_represent.php#comments18/12 20:04
soupdragonthat Chu-Carroll keeps writing stuff I abhor18/12 20:05
dolioI jumped in at 97 to show an Agda encoding of Cantor's argument.18/12 20:05
dolioEven though computable subsets of the naturals are countable. :)18/12 20:05
soupdragondid you get any good responses?18/12 20:05
dolioThey're computably uncountable.18/12 20:05
soupdragonis that so??18/12 20:06
soupdragonis something computable only if you can write it down (finitly)?18/12 20:06
dolioNo. 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
dolioComputability is related to Turing machines or lambda calculi, and you can write those down as finite strings.18/12 20:07
soupdragonwhat about the coinductive calculus18/12 20:07
dolioAt least, I think.18/12 20:07
soupdragonMark Chu-Carroll writes factorial in haskell and says "Look at this wonderful example of Curry-Howard isomorphism"18/12 20:08
dolioYeah, his Haskell stuff is pretty muddled.18/12 20:08
soupdragonAnd the next day he is slaggin someone off for talking nonsense :P18/12 20:08
soupdragonb) countable != diagonalizable18/12 20:09
soupdragonI guess he writes C or something18/12 20:09
dolioAnyhow, 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
dolioOr constructive mathematics in general.18/12 20:10
dolioAnd since it's constructively valid, it's classicaly valid.18/12 20:10
soupdragontelling people they don't know is crazy, it's just an expression of frustration18/12 20:11
soupdragonYou 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
dolioWell, the diagonal argument is pretty simple as proofs go, I think.18/12 20:13
soupdragonthere's a more subtle confusing, I wonder if that guy came around to it18/12 20:13
dolioHis problem doesn't even seem to be the diagonal argument itself.18/12 20:13
soupdragonseems 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
dolioIt'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
soupdragondolio: It's simple and not simple -- Once you understand the first infinity, the argument is very clear and concise18/12 20:15
soupdragonbut to actually learn what N is ?18/12 20:15
soupdragondolio, who?18/12 20:15
dolioPaul Homer.18/12 20:16
dolioHis 'counter example' is a 2-dimensional spreadsheet of all real numbers.18/12 20:16
dolioWhich he says you can't apply the argument to, because you have to go down a single row or column.18/12 20:16
dolioBecause that's the only path that's "fast enough".18/12 20:17
soupdragonhe's using the demonic "..."18/12 20:17
dolioHeh, yeah.18/12 20:17
soupdragonI wonder what his take on 0.999... = 1 is18/12 20:18
dolioI don't know. I'd prefer to not deal with reals since them being a quotient makes things more complicated.18/12 20:18
dolioBut everyone likes the real numbers.18/12 20:19
soupdragonroconnor told me something that sounded nice18/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
dolioZ is the initial ring, I think.18/12 20:20
soupdragonanyway I have no idea what it means yet,18/12 20:20
dolioNot sure about N.18/12 20:20
soupdragon"cardinality is 2^|N|" yikes!18/12 20:20
soupdragonI am just sure that starting to talk about exponentiation like that with infinite objects will help everyone understand what's going on18/12 20:21
dolioMaybe N is the initial semi-ring or something.18/12 20:21
dolioOr whatever a ring without negation is.18/12 20:22
SaizanEelis on #coq said something like that18/12 20:22
dolioThat'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." hehe18/12 20:23
Saizan21:46 < Eelis> the natural numbers can be characterized as the initial object in the category of semirings (a variety).18/12 20:23
Saizan21:46 < Eelis> similarly, the integers can be characterized as the initial object in the category of rings (another variety)18/12 20:23
dolioYeah, that depends on your definition of tree, apparently.18/12 20:23
dolioAnd he's talking about performing some construction 'omega-many times' or something.18/12 20:24
soupdragonI don't know what to learn from all this18/12 20:24
dolioWhich sounds very classicaly set theoretic and evil to me.18/12 20:24
soupdragonone guy makes some odd statements that use lots of soft words and ellipses18/12 20:25
Saizanisn't it just a coinductive tree?18/12 20:25
soupdragonpeople use swear words to tell him he is wrong18/12 20:25
soupdragonhe knows he right ... but other people are mixed up about tangential issues18/12 20:25
dolioSaizan: Not really. The infinite tree is the coinductive tree.18/12 20:25
soupdragonso what does it mean?18/12 20:25
dolioHe'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
dolioSo you have infinitely long paths ending at a node, of which there are obviously uncountably many.18/12 20:26
soupdragonChad corrected me a bunch of times on this point. Sets *are* at infinity, that's part of their definition.18/12 20:27
soupdragonthat's some 'correction' :D18/12 20:27
dolioBut 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
soupdragonas sets?18/12 20:27
soupdragoninfinitely brancing trees?  that's what the  Lim : (N -> O) -> O  constructor is18/12 20:27
dolioAs being able to 'do something' a transfinite ordinal 'number of times'.18/12 20:28
soupdragondolio the program interpretation? I thought they always terminate in finite time18/12 20:28
dolioRight, but I think you can have set theoretic constructions that don't have interpretations like that.18/12 20:28
soupdragonare they well founded?18/12 20:29
doliohttp://en.wikipedia.org/wiki/Surreal_number is the example18/12 20:29
dolioThere are iterations of the surreal construction transfinitely many times.18/12 20:30
dolioLike, you do something infinitely many times, and then after that, you do it 5 more times.18/12 20:34
copumpkin:O18/12 20:34
soupdragondolio so what's the conclusion or whatever with this stuff?18/12 20:36
soupdragonPaul W. Homer etc18/12 20:36
dolioStructural 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
dolioI 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
dolioEven though roconnor has a computer verified proof of it. :)18/12 20:37
soupdragonhttp://knol.google.com/k/are-real-numbers-uncountable#18/12 20:37
soupdragonthat reminds me of it18/12 20:37
soupdragonbut that guy is just playing a game18/12 20:38
dolioWell, that's what the blog post was originally about.18/12 20:38
soupdragonMark Chu-Carroll picks an easy target18/12 20:38
soupdragonhm I don't really see the point in any of this18/12 20:39
dolioAny of what?18/12 20:39
soupdragonall the blogs and knols18/12 20:40
dolioKnols are supposed to be like Google's wikipedia, I think.18/12 20:40
soupdragonI 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
dolioOnly each article is written by a single person unless they specifically allow other people to edit them.18/12 20:40
soupdragonthis seems like a terrible disservice to any young child that is trying to learn real mathematics from the internet18/12 20:41
dolioWhich 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
soupdragonyeah I'm interested in the difference between these two things18/12 20:42
soupdragonmaybe we just have to formally prove everything before we write it18/12 20:43
dolioSomeone posted an article about how Knol is a pretty poor setup.18/12 20:44
dolioThere's no community oversight. And apparently people get paid based on article hits.18/12 20:44
dolioWhich encourages people to write controversial articles, rather than correct ones.18/12 20:45
soupdragondolio well that  is the game he is playing right there18/12 20:45
soupdragonnow this is ridiculous18/12 20:45
soupdragon"Like I keep saying: go read some Conway"18/12 20:46
soupdragonMark C. Chu-Carroll -- the guy who is blogging about all this stuff18/12 20:46
soupdragonwhy doesn't he just type up pages from that book if its so good18/12 20:46
dolioWell, Conway is awesome, isn't he?18/12 20:47
soupdragonI don't know18/12 20:47
soupdragonwell yes he is18/12 20:47
soupdragonI haven't read anything by him though18/12 20:47
dolioYeah, me neither, really.18/12 20:47
soupdragonI'm just saying what's the point in re-describing all this stuff (about diagonals)18/12 20:47
soupdragonit's a hypocritical thing for him to post that comment, imo18/12 20:47
soupdragoneven if he knows the game he is playing (practice writing and argumentation) then doesn't it break the metaphor?18/12 20:48
soupdragonthe only reason anyone here is interesting in diagonalization is because lots of people respond to blog posts about it :P18/12 20:49
soupdragonI'm sure they all learned it an understood it just fine when they were 1518/12 20:49
soupdragonThis whole fiasco is a bit grim actually18/12 20:51
soupdragonnobody seems to want to think critically and carefully read proofs18/12 20:52
soupdragonwell a couple people do, but not enough18/12 20:52
soupdragonthe whole point of proving something is that you can communicate it18/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
dolioHeh.18/12 20:56
soupdragonI love when people say "academics" like it's the worst kind of person in the world18/12 20:56
soupdragondolio all this is really baffling to me18/12 20:59
soupdragonI don't know if I should care18/12 20:59
copumpkinit's amazing how controversial this is18/12 21:00
soupdragonmaybe it's just the phenomena where rubbish stuff becomes popular18/12 21:00
soupdragonlike naked girl that plays a video game or whatever gets voted to #1 straight away, even though it's highly unremarkable18/12 21:00
copumpkinyeah, I guess18/12 21:01
dolioSet theory an infinites are very popular targets for mathematical cranks.18/12 21:01
dolioFor instance, if you check out sci.math.18/12 21:01
copumpkinI got frustrated enough at Earle and Shelby, I think I'll pass :)18/12 21:02
dolioProbably even moreso than the incompleteness theorem.18/12 21:02
soupdragonwhat's Earle and Shelby?18/12 21:02
copumpkinsoupdragon: a couple of cranks that showed up recently on haskell-cafe18/12 21:02
copumpkinJohn D. Earle and Shelby Moore iirc18/12 21:03
soupdragonhttp://old.nabble.com/Haskell---Haskell-Cafe-f13132.html on there somewhere?18/12 21:05
dolioI 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
soupdragonit's all meaningless anyway18/12 21:07
soupdragoninfinity? hah18/12 21:07
soupdragonno wonder so many people take refuge in axiomatics18/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
soupdragonheh18/12 21:08
soupdragonI'd not seen that18/12 21:09
dolioThat's from sci.math18/12 21:09
soupdragonI dunno it's all a joke to some people but not to others18/12 21:10
soupdragonwhat about those integalactic telefunctors?18/12 21:11
soupdragondid they find alien life yet18/12 21:11
soupdragonhmf I don't know what to think about hthis18/12 21:13
soupdragonI am trying to extract some meaning from it but it's probably just loads of people playing a game18/12 21:14
soupdragonwhat do you take from it?18/12 21:16
Saizani 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 post18/12 21:17
Saizan(and my grammar is quite poor currently)18/12 21:18
soupdragonyeah that's one tricky thing..18/12 21:20
soupdragonI think that being too formal is really counterproductive and stifling18/12 21:20
soupdragonbut then you can be wrong if you just guess everything18/12 21:20
dolioWas I not explaining the details well?18/12 21:20
Saizani was talking about Chu-Carrol articles in general actually, i didn't follow this one too closely18/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
soupdragonmaybe if I shut my eyes it will go away18/12 21:29
soupdragondolio nobody can read this :P http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14369#a1437818/12 21:30
soupdragonexcept maybe ... the 50 people that know agda18/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
soupdragonLets 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
soupdragonthis is just silly rambling but there is a wonderfully beautiful thing nearby, proof of the cauchy product18/12 21:32
soupdragonThe 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_i18/12 21:34
dolioThe proofs certainly wouldn't make any sense. The types might, if read as mathematical propositions. :)18/12 21:34
soupdragonnow AB = sum the diagonals of the 'spreadsheet'18/12 21:35
soupdragonm it's a different spreadsheet - my one has, cell_i_j = a_i*b_j18/12 21:36
soupdragonanyway you can prove that converges even though there's "380 non enumerated elements"(!)18/12 21:37
soupdragonIjust dont' know18/12 21:50
dolioSlow and steady ties the race.18/12 22:02
Saizanwait, 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
dolioBecause he also says that his magical sequence is "countable".18/12 22:08
Saizanwell, if he doesn't see how these two concepts are contradictory i wouldn't know how to clarify that18/12 22:13
soupdragonit's all too wordy for me18/12 22:14
soupdragonI don't think he knows what he means18/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
HaskellLovecan I ask type theory questions on this channel?19/12 04:33
copumpkinas I said, #haskell works, but this would probably work too. There's just a lot more activity on #haskell19/12 04:34
HaskellLovemeet you at haskell then19/12 04:37
-!- opdolio is now known as dolio19/12 05:59
Saizandolio: 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 pigmalion19/12 16:03
soupdragonhey dolio19/12 16:26
soupdragonWhat about Löwenheim–Skolem19/12 16:27
soupdragonregarding http://scienceblogs.com/goodmath/2009/12/another_cantor_crank_represent.php#comment-215403019/12 16:27
dolioSaizan: 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
dolioThe 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
Saizandolio: yeah, it wasn't important, it was mostly to confirm my understanding of agda, thanks19/12 21:56
dolioI 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
dolioOr can't prove that the function is computable, or something.19/12 21:59
Saizanwell 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 guess19/12 22:04
dolioRight.19/12 22:29
soupdragon"typechecking would have to solve the halting problem"19/12 22:58
soupdragonthe one writing the program needs to prove termination is all19/12 22:58
soupdragonof course you can't express every computable function in agda19/12 22:59
Saizanwell, i meant in Agda as it is now19/12 22:59
* copumpkin returns to Data.Graph.Acyclic19/12 23:19
copumpkingah19/12 23:30
Saizanmh DGA instead of DAG19/12 23:33
copumpkin:)19/12 23:34
copumpkinit's the hardest time I've had converting a module to UP19/12 23:34
copumpkinwhoa, you can use a variable twice in a type signature19/12 23:46
* copumpkin sighs: .e ⊔ .n != .n of type Level19/12 23:46
--- Day changed Sun Dec 20 2009
copumpkinI'm stumped20/12 00:03
copumpkinoh20/12 00:06
copumpkinI think I might know what's wrong, but am not sure how to solve it20/12 00:12
copumpkinso if I have20/12 00:16
copumpkin  p i (e , j)  with i ≟ j20/12 00:16
copumpkini is a Fin n, j is a Fin n20/12 00:16
copumpkinwhat could possibly make it complain that Dec (x ≡ y) !=< Level of type Set ?20/12 00:16
copumpkinwhoops i == j, not x == y20/12 00:16
doliosoupdragon: You mean that downward Loewenheim-Skolem implies that the reals are countable?20/12 00:41
soupdragonno20/12 00:41
soupdragonThe reals are not countable :P20/12 00:41
copumpkinnuh uh, I have an enumeration right here with me20/12 00:42
soupdragonbut it seems like your argument about the computable reals follows a similar path20/12 00:42
soupdragonI don't believe the computable reals are countable -- just the ones you can write down20/12 00:42
dolioHow can something be computable without being able to write down an algorithm/Turing machine/whatever to compute it?20/12 00:43
soupdragonmaybe you can do it with a neural network or something (one that computes with real numbers), I don't know20/12 00:44
dolioWell, 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
soupdragonthese computable reals are countable http://en.wikipedia.org/wiki/Computable_number20/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
soupdragonhm maybe what I am thinking of is the reals20/12 00:51
dolioPeople 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
dolioOr something like that.20/12 00:52
dolioWhere 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
dolioBut I don't think I've ever heard that about computable reals.20/12 00:54
dolioOr, if you want to get more restrictive, a real number datatype in Agda. Those seem obviously countable.20/12 00:55
soupdragonwell I don't know about that20/12 00:55
dolioYou could have a denotational semantics where the real numbers type is mapped to a set with uncountably many elements.20/12 00:56
soupdragonyou could have agda interpret into a model where 2 -> Nat has uncountable elements20/12 00:56
soupdragonyeah :p20/12 00:56
dolioBut syntactic models (or whatever you want to call them) seem more readily believable as "the" model for a programming language.20/12 00:59
soupdragonit's too bad that reflecting the idea that everything 'there is' can be 'written down' causes inconsistency20/12 00:59
dolioThan they do for a set theory.20/12 00:59
soupdragonI don't beleive in One true model20/12 00:59
soupdragonI 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 reals20/12 01:01
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14444#a14444 :(20/12 01:01
soupdragonbut a type like Nat -> 2 (which I seemed to mix up earlier) might not be20/12 01:01
dolioNat -> 2 isn't "functions from Nat to 2", though, it's "(provably) computable functions from Nat to 2".20/12 01:02
soupdragonwell it's not really anything20/12 01:03
soupdragonif the typechecker passes for a judgement  Gamma |- x : Nat -> 2, then  x is a computable function20/12 01:03
doliocopumpkin: I don't really see where the problem is.20/12 01:05
soupdragonyou can pair up,   (f : Nat -> 2, code f)   that gives elements of Nat -> 2 which come from a finite coding20/12 01:05
copumpkindolio: 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 code20/12 01:06
copumpkinmaybe w is what with desugars to?20/12 01:06
doliowith desugars to an auxiliary function, so maybe.20/12 01:06
copumpkinI'll try with'ing manually20/12 01:07
dolioGamma |- x : Nat -> 2 is a judgment about Agda terms x.20/12 01:09
dolioOr something similar.20/12 01:10
soupdragonyeah (and says that gamma and Nat -> 2 are well formed also)20/12 01:10
dolioSo in (f : Nat -> 2, code f), f is code.20/12 01:11
copumpkinmanual with'ing works fine20/12 01:12
soupdragonno20/12 01:12
copumpkinI guess it's a subtle bug?20/12 01:12
soupdragonf is the interpretation of a code20/12 01:12
dolioThen f : Nat -> 2 doesn't make any sense, because f is not an Agda term.20/12 01:12
soupdragonit is an agda term, with type  Nat -> 220/12 01:13
soupdragonI mean this like a Sigma20/12 01:13
soupdragonSigma (Nat -> 2) (\f -> code f)20/12 01:13
soupdragoncode : {T} -> T -> Set20/12 01:13
soupdragon'0' : code 0, 'S' : code S  etc20/12 01:14
dolioWhat does 'code' mean? Goedel code?20/12 01:14
soupdragonjust like a syntax which has the interpretation built in20/12 01:14
soupdragon'$' : code f -> code x -> code (f x)20/12 01:14
dolioOh, 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
soupdragonwell it's all agda terms20/12 01:16
dolioWhere the term represented corresponds to f.20/12 01:16
soupdragonf is what's being represented20/12 01:16
soupdragonby an element of code f20/12 01:16
dolioRight.20/12 01:17
copumpkinbah, my message is awaiting moderator approval!20/12 01:26
copumpkinthis module has another problem in it that makes no sense to me20/12 01:38
copumpkinI have a g   : Graph (Prod.Σ (Fin .n') (λ _ → N)) E .n'20/12 01:42
copumpkinmy goal is20/12 01:42
copumpkinGraph (Prod.Σ (Fin (suc .n')) (λ x → N)) E .n'20/12 01:42
copumpkinso basically just incrementing the proj_1 of the pair20/12 01:42
copumpkinnmap : ∀ {ℓN₁ ℓN₂ ℓE : Level} {N₁ : Set ℓN₁} {N₂ : Set ℓN₂} {E : Set ℓN₂} {n} → (N₁ → N₂) → Graph N₁ E n → Graph N₂ E n20/12 01:42
copumpkin(ignoring the bad names for a moment)20/12 01:43
copumpkinbut doing the obvious and nmap (Prod.map suc id) g fails saying Set ????? != Set20/12 01:47
copumpkinoh my, totally my own fault20/12 01:55
* copumpkin swears a bit20/12 02:27
copumpkin<-rec in Induction.Nat forces stuff into Set :(20/12 02:31
copumpkinmostly just because of20/12 02:32
copumpkindata _≺_ : ℕ → ℕ → Set where20/12 02:32
copumpkin  _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n20/12 02:32
soupdragonwoah20/12 02:32
soupdragonwhat's that about?20/12 02:32
soupdragonweird way to define less I guess there's nothing more to it20/12 02:33
copumpkinit's used for WfRec20/12 02:34
copumpkinopen WF _≺_ public using () renaming (WfRec to ≺-Rec)20/12 02:34
copumpkinthis is just preventing me from using toForest, which isn't the end of the world I guess20/12 02:35
copumpkinit'll do :)20/12 02:37
doliocopumpkin: So, your e-mail was pretty interesting.20/12 10:17
copumpkinoh, 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 moderation20/12 10:17
copumpkindid you figure out what the problem is?20/12 10:17
doliohttp://img85.imageshack.us/img85/8004/wowu.png20/12 10:20
copumpkinoh crap20/12 10:20
copumpkinso much for pasting code into gmail's rich text editor20/12 10:20
* copumpkin sighs20/12 10:21
dolioThe html version looks fine, but that's what the text version looks like.20/12 10:21
copumpkinI guess gmail felt the need to make sure the links from the html code made it through to the text version20/12 10:22
dolioEvidently.20/12 10:22
larrytheliquidis there a shorthand for implicit arguments without labels? e.g. the precondition here in evenSuc http://hpaste.org/fastcgi/hpaste.fcgi/view?id=14495#a1449520/12 19:56
soupdragonevenSuc : ∀ n → {T (even n)} → ℕ20/12 19:57
soupdragonliek ?20/12 19:57
larrytheliquidya20/12 20:41
larrytheliquid{T (even n)} cannot appear by itself. It needs to be the argument20/12 20:41
larrytheliquidto a function expecting an implicit argument.20/12 20:41
larrytheliquidwhen scope checking {T (even n)}20/12 20:41
larrytheliquidi 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
larrytheliquidthough at the level of a type signature i wouldnt think there would be ambiguity20/12 20:45
larrytheliquidim using agda 2.2.4 via cabal20/12 20:48
copumpkinjust give it a name, if it's complaining20/12 20:48
copumpkin{pf : T (even n)}20/12 20:49
copumpkinor something20/12 20:49
larrytheliquidgiven that the {}s are not already inside another funcall, that is20/12 20:52
larrytheliquidyah i did just use underscore, was just wondering if there was an alternative20/12 21:44
copumpkinunderscore?20/12 21:44
larrytheliquid_20/12 21:44
copumpkinlol20/12 21:45
copumpkinI know what an underscore is20/12 21:45
larrytheliquidhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14495#a1449520/12 21:45
copumpkinI just missed the context20/12 21:45
copumpkinah20/12 21:45
copumpkinhow did you highlight the line?20/12 21:46
larrytheliquidenter the line number into the field below and hit the "highlight line" button20/12 21:46
copumpkinoh, smart20/12 21:46
larrytheliquid;)20/12 21:46
--- Day changed Mon Dec 21 2009
dolioSo, 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
soupdragonwhy?21/12 01:53
dolioBecause 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
soupdragonoh yeah I see21/12 01:54
dolioWhat matters is how many elements of the denotational set are picked out by syntactically valid/well typed/whatever terms.21/12 01:54
dolioAnd that will always be countable.21/12 01:54
soupdragonthat is certainly true21/12 01:55
soupdragonwhy can't there be a bijection between them though?21/12 01:55
dolioUnless you have uncountably many syntactically valid terms, but that'd be pretty weird.21/12 01:55
dolioWhat 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
soupdragonyeah but not one between N and N -> 221/12 01:58
soupdragonwhich is odd21/12 01:58
soupdragonhm the existence of a bijection is okay? but an isomorphism between them is contradictory21/12 01:59
dolioYou can have a meta-bijection between N and N -> 2, but not an Agda bijection.21/12 01:59
soupdragonI 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
dolioIf you postulate one it will contradict the Cantor diagonal argument you can construct in Agda.21/12 02:01
soupdragonI mean one without the equality proofs21/12 02:01
dolioWhat would the postulate be?21/12 02:03
soupdragonI 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
soupdragonbut 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 surjective21/12 02:05
dolioAnyhow, if your logic is consistent, I think you can't show that there's an enumeration N -> (N -> 2).21/12 02:07
dolioIf 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
dolioSo your logic would be inconsistent.21/12 02:08
soupdragonso what about the meta proof?21/12 02:08
soupdragonwhy doesn't that cause a problem21/12 02:08
dolioBecause you don't have access to the meta proof within the language.21/12 02:09
soupdragonthis is a paradox21/12 02:09
soupdragonit's false internally but it's true externally!21/12 02:10
dolioThe meta-proof doesn't prove that there's an N -> (N -> 2), though.21/12 02:11
dolioThat's a bijection, that is.21/12 02:12
dolioIt proves that there's a meta-bijection between N and N -> 2.21/12 02:12
soupdragonif both sets are countable there's a bijection by that crazy proof with the zigzags ?21/12 02:12
* soupdragon tries to remember its name21/12 02:13
dolioYou'd use zigzagging to prove that NxN (or something like it) is countable, if that's what you mean.21/12 02:14
soupdragonno thinking of something else but I can't remember the name :(21/12 02:14
soupdragonI'm trying to search it out21/12 02:14
dolioPerhaps it'd be clearer to say that both types are meta-countable.21/12 02:16
dolioBut N -> 2 isn't Agda-countable.21/12 02:16
soupdragonI can live with that but the question is left:   is N -> 2 countable or not?21/12 02:16
soupdragonWas Cantor an idiot and liar? :P21/12 02:16
soupdragonCantor–Bernstein–Schroeder theorem21/12 02:20
soupdragonno wonder I couldn't remember it21/12 02:20
soupdragondoesn't that give a metabijection?21/12 02:20
soupdragonhttp://en.wikipedia.org/wiki/Cantor%E2%80%93Bernstein%E2%80%93Schroeder_theorem#Visualization is what I meant by the zigzag thing21/12 02:20
dolioOh, that zig zagging.21/12 02:21
dolioAnyhow, yes, that's a meta bijection.21/12 02:21
soupdragonthat 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 it21/12 02:22
whoppixsoupdragon, 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
soupdragonwhoppix it was a joke because this guy claimed these things21/12 02:28
dolioI am the only one who has properly understood and refuted Cantor's argument!21/12 02:32
soupdragonthis constructive math/logic makes me doubt everything21/12 02:34
-!- opdolio is now known as dolio21/12 05:37
-!- BlackM is now known as BMeph21/12 18:25
--- Day changed Tue Dec 22 2009
soupdragonanymore 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
soupdragonhehe22/12 03:55
copumpkingah22/12 03:55
soupdragon:p22/12 03:55
copumpkin:)22/12 03:55
soupdragonhe's cute I like him22/12 03:55
soupdragon 29 Comments fffffffffffffff22/12 03:56
copumpkinwait, which instance are you referring to?22/12 03:57
soupdragonhttp://theprogrammersparadox.blogspot.com/2009/12/crank-it-up.html22/12 03:57
copumpkinthanks22/12 03:57
copumpkinoh this is a different guy22/12 03:58
soupdragonI might send him an email22/12 03:58
copumpkinI love his rigorous proof that his spreadsheet contains them all22/12 03:59
copumpkin"It looks like sqrt(2) will be somewhere in the bottom left quadrant."22/12 04:01
soupdragonwell that is intuition22/12 04:01
soupdragonI think his argument is wrong but his philosophy is tending toward something quite acceptable22/12 04:02
copumpkin"1. By definition the spreadsheet ONLY contains irrationals."22/12 04:02
copumpkinoh okay!22/12 04:02
copumpkin:)22/12 04:02
copumpkinI 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 bat22/12 04:04
soupdragonWhat I think is important is not the formal mathematics22/12 04:05
soupdragonwe can check it on a computer, or we could get a thousand people to check it by hand and everyone would accept it22/12 04:05
soupdragonbut what do the proofs mean?22/12 04:06
dolioHow 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
copumpkinthat seems to be a recurring theme of these arguments22/12 04:08
dolioWhich appear to be either multiplying or dividing by 10, and adding 10^m for some m.22/12 04:08
copumpkinat least, the other dude on the knol seemed to make a similar assumption22/12 04:08
dolioActually, it's not even a finite number of steps, it's just doing either of those once.22/12 04:09
dolioFirst you add 10^m (for switching columns) and then you multiply by 10^m (for changing rows).22/12 04:10
dolioEr, 10^n.22/12 04:10
dolioNot necessarily the same number of course.22/12 04:10
dolioWait, I'm wrong again, the additions are cumulative.22/12 04:11
soupdragonI feel that the Knol guy is just a bastard that is making money by posting bullshit22/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
soupdragonparticularly his "nananana I am not listening" attitude22/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 coughs22/12 04:13
copumpkinQED22/12 04:13
dolioThe guy can't be argued with.22/12 04:22
dolioPeople have pointed out specific numbers that aren't in his spreadsheet, and he just ignores them.22/12 04:22
copumpkinpeople also ask him to show that the diagonal argument fails on his spreadsheet-generated sequence22/12 04:23
dolioYes, 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
dolioI explained multiple times and wrote a program that did it, and proved that it did it.22/12 04:24
copumpkinI'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 wikipedia22/12 04:25
dolioNobody's thought of two dimensional sheets of numbers in 100 years.22/12 04:44
copumpkinhey, this one extends to infinity in all four directions!22/12 04:44
copumpkinit's magic22/12 04:44
soupdragonyou guys are mean :p22/12 04:45
copumpkinI 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
copumpkinas 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 countable22/12 04:46
dolioSome of his objections make sense for ordinals but not cardinals.22/12 04:51
dolioLike, omega*omega is bigger than omega.22/12 04:51
copumpkinyeah, but that's not original or particularly relevant, is it?22/12 04:52
copumpkinnot that I should really be speaking as I'm almost as clueless as he is about math :)22/12 04:52
dolioWell, you don't use ordinals to count how many things are in a set, so no.22/12 04:53
dolioIf you use the standard ordinals-are-sets encoding, then omega*omega has as many elements as omega.22/12 04:55
dolioDespite the first being a bigger ordinal.22/12 04:56
copumpkinI guess that means there's not a bijection between the ordinals and the cardinals? :)22/12 04:57
dolioNeither of those are sets, so I don't really know if you can even talk about bijections between them.22/12 04:58
dolioAt least, I doubt there's a set of cardinals. I know there isn't a set of ordinals.22/12 04:58
copumpkinwell, you could make a category of them with functions on them, I guess22/12 04:59
copumpkinnimbers seem to make ordinals22/12 04:59
copumpkinusable22/12 05:00
* soupdragon titters 22/12 05:09
copumpkinyou should sign up for a titter account and teet your random thoughts :)22/12 05:09
soupdragonI'm smirking at this http://www.reddit.com/r/math/comments/ahb9l/the_diagonal_argument_works_perfectly_fine_with_a/22/12 05:10
copumpkinI wonder who posted that O:-)22/12 05:10
dolioThe god of your categorical dual, evidently.22/12 05:10
dolioIs the math reddit worth looking at regularly?22/12 05:11
soupdragondolio if you want new and exciting ways to cut bagels22/12 05:11
copumpkinI only check it every few days22/12 05:11
dolioWell, I mean, is it more like the Haskell one, or the programming one?22/12 05:12
soupdragonhttp://www.reddit.com/r/haskell/comments/afj53/224_epilogue/22/12 05:13
soupdragon"Bertrand Russell would feel vindicated." funny22/12 05:13
copumpkinprobably more like programing with things like "yo, teach me math"22/12 05:13
dolioYes, did epigram achieve that result faster or slower than principia mathematica? :)22/12 05:14
soupdragondifficult to say :P22/12 05:15
soupdragonhttp://www.reddit.com/r/dependent_types/22/12 05:19
soupdragonthat's the best reddit22/12 05:19
copumpkinlol22/12 05:19
copumpkindidn't you already say you thought that one was super boring? :P22/12 05:20
dolioAre you sure it's better than /r/types? :)22/12 05:20
copumpkinwe could start an /r/agda for the ultimate idle subreddit22/12 05:21
copumpkinhttp://www.reddit.com/r/math/comments/ahb9l/the_diagonal_argument_works_perfectly_fine_with_a/c0hken322/12 05:23
soupdragonhmm guys you know what?  I think I just disproved cantors theorem!22/12 05:25
copumpkinnice!22/12 05:25
dolioWhich one?22/12 05:25
soupdragonall of them22/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
soupdragonthat's an interesting comment22/12 05:26
copumpkinI 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
soupdragonlikely to convince the crank?? haha22/12 05:32
copumpkinwell, assuming he's at all rational :)22/12 05:32
copumpkinI'm sure he's now moved into defensive mode though22/12 05:32
copumpkinany argument against him is just conventional mathematicians not being able to step out of their box22/12 05:33
dolioIf he doesn't believe Cantor's diagonal argument, you'll think he'll accept that pi is transcendental?22/12 05:33
dolioI don't even know how to prove that.22/12 05:33
copumpkinI guess not, but it's a lot more intuitive that it might be true22/12 05:33
soupdragonme neither22/12 05:33
copumpkinthan cantor22/12 05:33
soupdragonhey why is pi trancendental??22/12 05:33
copumpkinoh, 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
copumpkinit just seems a lot easier to accept that it's not going to be a zero of a polynomial22/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
soupdragonhey dolio I like where you are going with this!22/12 05:35
copumpkinmaybe I'm just drinking the kool aid though22/12 05:35
soupdragonsince pi is not trancendental we can actually construct it, and square the circle22/12 05:36
dolioHeh.22/12 05:37
soupdragonIn 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
soupdragonthat seems like an argument that could be made rigerous22/12 05:38
soupdragonrigorous22/12 05:38
dolioYeah, but that just reduces to proving e is transcendental. How do you do that?22/12 05:38
copumpkinhttp://en.wikipedia.org/wiki/Transcendental_number#Sketch_of_a_proof_that_e_is_transcendental22/12 05:39
copumpkinhttp://snapplr.com/5t8222/12 05:39
dolioThat's a weird way of describing the operation.22/12 05:41
copumpkinit's a shorthand22/12 05:41
copumpkinI just thought it was amusing when taken out of context22/12 05:41
dolioNow that proof would not be easy to formalize.22/12 05:45
soupdragoni wonder if there's proofs in CoRN22/12 05:45
soupdragonthey might be different22/12 05:45
copumpkinuniverse polymorphism still messes with my mind22/12 08:03
dolioYeah?22/12 08:10
copumpkinthings like the empty type in a higher universe22/12 08:11
copumpkinwhen it's appropriate to make something polymorphic or not22/12 08:11
dolioI wouldn't bother with the empty type in a higher universe.22/12 08:12
dolioIf you need that, you probably want something else in actuality.22/12 08:12
copumpkinyeah, that's what I figured22/12 08:12
copumpkinis there an obvious connection to logic in UP?22/12 08:13
dolioSome operation to take things in universe i and put it in universe i+1.22/12 08:13
soupdragon UP?22/12 08:13
copumpkinuniverse polymorphism22/12 08:13
dolioI'm not aware of a connection.22/12 08:15
soupdragonwhat's the question ?22/12 08:16
soupdragonlooking for a logical interpretation of polymorphism?22/12 08:16
copumpkinyeah22/12 08:16
dolioUniverse polymorphism.22/12 08:17
copumpkinuniverse polymorphism, that is22/12 08:17
soupdragonI just consider it as denoting a whole family of definitions rather than a single one22/12 08:17
copumpkinwell, even ignoring the polymorphism aspect of it, what are higher universes in logic?22/12 08:18
dolioActually, there was something about a set theory with universes on the n-category cafe not too long ago.22/12 08:19
dolioSpecifically 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
dolioBut not precisely analogous to Agda's version of it.22/12 08:20
copumpkinah22/12 08:20
dolioThe axiom is intended to solve similar problems, though.22/12 08:22
dolioThe 'universes' in question are sets that are closed under various operations, such that they behave a lot like 'all sets'.22/12 08:22
dolioAnd 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
dolioBut 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
doliohttp://golem.ph.utexas.edu/category/2009/11/feferman_set_theory.html22/12 08:27
soupdragonI don't know why I even load these pages22/12 08:28
soupdragonI can't understand anything on any of them22/12 08:28
soupdragon:[22/12 08:28
copumpkinI like the ncatlab wiki22/12 08:34
* copumpkin looks forward to understanding more than the first couple of lines on that blog22/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 xs22/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
soupdragonBullseye22/12 08:49
dolioThat's a good article.22/12 08:50
copumpkingah, this is ridiculously complicated, just because of that nasty codata intermediate language22/12 08:59
copumpkinwell, maybe not just because22/12 08:59
copumpkinbut it is a real pain to even figure out what my goals are given the codata output22/12 09:01
soupdragonwhat's the point of proving this..22/12 09:04
copumpkinfor the fun of it, really22/12 09:04
soupdragoncan you show me the diagMap code?22/12 09:04
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14829#a14829 :(22/12 09:05
soupdragonah well you can probably start by proving the equations you would have liked to define the function with then?22/12 09:06
copumpkinhow do you mean?22/12 09:06
soupdragonactually that doesn't really help anything, never mind that22/12 09:07
copumpkinwow, 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
copumpkinI guess it would help if I could figure out what the | notation meant in a type22/12 10:27
Saizani think (foo | bar) just means that to reduce foo further you've to pattern match against bar22/12 10:28
copumpkinwhat if I have three of them?22/12 10:29
copumpkinoh, they're nested22/12 10:29
copumpkinso I have22/12 10:31
copumpkinwhnf (map [_] (fromColist⁺ zs)) | (whnf (fromColist⁺ zs) | ♭ zs)22/12 10:31
Saizani guess map does case analysis on the whnf of its argument?22/12 10:33
copumpkinyeah22/12 10:34
copumpkinmap is actually a constructor :P22/12 10:35
Saizanhah22/12 10:41
copumpkinwhnf is an evaluator for it22/12 10:41
copumpkinhmmm22/12 10:42
copumpkinwhnf (stripeDiagonal [ ♭ zs ]) !=22/12 10:47
copumpkinwhnf (map [_] (fromColist⁺ zs)) | (whnf (fromColist⁺ zs) | ♭ zs) of22/12 10:47
copumpkintype DiagonalW (List⁺ .B)22/12 10:47
copumpkinthat's my type error22/12 10:47
Saizani guess you've to prove stripeDiagonal [ ♭ zs ] \== map [_] (fromColist⁺ zs)22/12 10:49
copumpkinhmm, okay22/12 10:51
copumpkinI really like the splitter22/12 10:53
copumpkinpity it can't know everything :(22/12 10:53
SaizanC-c C-c ?22/12 10:54
copumpkinyeah22/12 10:54
copumpkinthey don't appear to be equal :o22/12 11:02
copumpkinI guess I need to prove the whnf is equal22/12 11:02
copumpkinnot the constructors themselves22/12 11:02
copumpkinlol22/12 11:05
copumpkinhttp://snapplr.com/hxpx22/12 11:05
copumpkinpretty deep proof22/12 11:05
copumpkindoesn't appear to be possible to simplify further though :)_22/12 11:06
copumpkinhttp://snapplr.com/yca6 says the same thing, I guess22/12 11:07
copumpkingah22/12 11:14
copumpkinI always have the hardest time getting the first parameter to subst right22/12 11:17
copumpkinso if I use the original term in the proof, it complains about the error I wrote above22/12 11:20
copumpkinso I proved that they are equal22/12 11:20
copumpkinnow I use a subst that uses the proof I wrote22/12 11:20
copumpkinand I can't figure out my first term22/12 11:21
copumpkinBAH22/12 11:39
dolioHaving fun monologuing?22/12 11:44
copumpkinyeah, it's awesome22/12 11:44
copumpkin_maybe this isn't a subst22/12 11:53
Saizanmh, sometimes i need to subst in different directions different parts of the type with the same equality22/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 tail22/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 copumpkin22/12 12:08
copumpkinyay, finally22/12 12:22
* copumpkin kicks himself a thousand times22/12 12:22
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=14834#a1483422/12 13:45
copumpkinneat22/12 13:46
dolioBUILTIN pragmas are quite a bit more lenient than I might expect.22/12 13:53
copumpkinhm, nested with blocks seem to behave strangely22/12 14:08
Saizan_i was being able to nest them only on the last case matched22/12 14:20
Saizan_*i've been22/12 14:21
copumpkinI'm actually getting somewhere with this monster22/12 14:49
copumpkinslowly and unsurely22/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 nevermind22/12 16:02
-!- copumpkin_ is now known as copumpkin22/12 16:04
copumpkinhow can I convince agda to evaluate my expression a little more deeply?22/12 16:13
copumpkinGoal: [ 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
copumpkinthat whnf (zipCons ... stuff can be simplified further22/12 16:13
Saizanthere's C-c C-n22/12 16:17
copumpkinyeah, but this is in my goal22/12 16:17
copumpkinI need it to evaluate it more because if it does that, it'll see that the expressions are a lot closer than they look22/12 16:17
Saizanwell, you can ask it to normalize what's in your goal, if you C-c C-n from an hole you get its scope22/12 16:20
copumpkinoh22/12 16:20
copumpkinhm, didn't normalize any further22/12 16:20
copumpkinI wonder what's stopping it22/12 16:20
copumpkindon't you love it when one of the lemmas you built your proof on turns out to be wrong22/12 16:42
copumpkinGoal: [ [ x ] ] ≡ [ y ∷ [ x ] ]22/12 16:43
copumpkinnow to find out how far back the mistake goes :/22/12 16:45
copumpkinagda needs quickcheck, to help you get a quick idea of whether the statement you're trying to prove makes sense at all22/12 16:48
Saizannice idea22/12 16:53
copumpkinGAH termination checker I hate youu22/12 17:02
copumpkinoh termination checker I love you22/12 17:02
copumpkinweird how filling in a hole can convince it you terminate :O22/12 17:03
-!- Berengal_ is now known as Berengal22/12 17:22
copumpkingah, it can't figure out that one of my lemmas terminates22/12 17:28
copumpkinluqui: I'm almost done proving that the my monstrous translation of your omega code does in fact have the important property22/12 18:03
luquiwow, nice work22/12 18:03
luquii tried my hand on it for (Nat ->)s22/12 18:04
luquiand it was... hard22/12 18:04
copumpkindid that work?22/12 18:04
luquiwell, i think it would have22/12 18:04
luquibut my proof-fu was not strong enough22/12 18:04
copumpkinah22/12 18:04
copumpkinthis representation is really tedious, due to all the ugly codata and the intermediate language22/12 18:04
luquiare you using colists.  i.e. ones with nil?22/12 18:05
copumpkinyeah22/12 18:05
luquiyeah ouch, i can see that being a bear22/12 18:05
copumpkinit's not quite as general as omega22/12 18:05
copumpkindiagonal : ∀ {a} → Colist⁺ (Colist⁺ a) → Colist⁺ a22/12 18:05
luquihm?  why?22/12 18:05
copumpkinI force the lists to be non-empty22/12 18:05
luquiah22/12 18:05
luquiyeah that's a good point, you get _|_ if you have an infinite list of empty lists22/12 18:06
luquiallowing nil lists would have to take an additional assumption ensuring productivity22/12 18:06
copumpkinyeah :/22/12 18:06
luquiso i think it's a good compromise22/12 18:06
copumpkinyeah, wasn't sure how to represent productivity explicitly22/12 18:07
copumpkinin a convenient manner, anyway22/12 18:07
luquiyeah without referencing the very same stuff diagonal is doing22/12 18:08
copumpkinmaybe if I get this working I'll move back to my language enumerator module22/12 18:09
luquioh that's what you're using it for?22/12 18:09
copumpkinthat's what my original motivation was, but then I figured it'd be handy for other things too22/12 18:10
luquihmm, using this proof you can prove that you do in fact enumerate all strings of the language22/12 18:10
luquineat22/12 18:10
copumpkinyeah22/12 18:10
luquithat is getting into the realm of the nontrivial :-)22/12 18:10
copumpkinI hope I succeed! currently I'm trying to rewrite one of my lemmas because agda thinks it doesn't terminate :(22/12 18:10
luquioh, that has never happened to me22/12 18:11
luqui(sarcasm)22/12 18:11
copumpkin:P22/12 18:11
copumpkinhmm, or maybe I'll leave my nonterminating lemma alone and try to fill in one of the few remaining holes22/12 18:12
copumpkindecisions decisions!22/12 18:13
-!- BlackM is now known as BMeph22/12 18:42
copumpkinomg BMeph in #agda22/12 18:52
copumpkinit sure would be nice to have rebindable list literals22/12 19:01
copumpkintestlist = (1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ [ 4 ]))) ∷ ♯ ((5 ∷ ♯ [ 6 ]) ∷ ♯ [ 7 ∷ ♯ [ 8 ] ])22/12 19:01
copumpkindamn, the lemma I'm trying to prove doesn't appear to be true either :P22/12 19:06
luquithe 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
copumpkinI 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 both22/12 19:23
* copumpkin yawns22/12 19:30
copumpkinI'm getting annoyed at emacs stealing my focus every time I load a file22/12 19:35
nappingspeaking of other languages, does anyone know about trellys?22/12 20:08
nappingI'm finding no information besides the grant22/12 20:08
copumpkingah, I was hoping to finish this proof today but I'm getting sleepy now :(22/12 20:43
nappingwhat is being proved?22/12 20:55
copumpkinI 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 properties22/12 20:57
nappingis there any essential laziness?22/12 21:02
copumpkinwell, it's infinite22/12 21:02
nappinghmm22/12 21:02
copumpkinso I have to use codata which could be seen as laziness22/12 21:03
nappingwhat's your theorem?22/12 21:03
copumpkindiagMap-proof : ∀ {A B} (a : A) → (xs : Colist⁺ A) → a ∈ xs → (y : B) → (f : A → Colist⁺ B) → y ∈ f a → y ∈ diagMap f xs22/12 21:03
nappinghow's that unicode supposed to work?22/12 21:03
ccasinnapping: trellys is still in the early going22/12 21:03
copumpkinnapping: oh, doesn't it show up for you?22/12 21:04
ccasinnapping: but I believe aaron stump has a draft paper out with some of the ideas under consideration22/12 21:04
nappingccasin: I was hoping to find a mailing list or something22/12 21:04
luquicopumpkin, i assume you have tried proving it for join22/12 21:04
ccasinnapping: only internal stuff at this point22/12 21:04
nappingI just see \uXXXX22/12 21:04
copumpkinluqui: I actually just used that, so the proof for diagMap is one line22/12 21:05
copumpkinhttp://snapplr.com/1c5g22/12 21:05
copumpkinthe diagonal proof is fairly large, and I'm still working on one of its lemmas22/12 21:05
luquiokay cool.  that's how i would have gone about it too...22/12 21:05
nappingah, so you can map over diagonal?22/12 21:06
copumpkinI started out with diagMap directly and that proved to be even more of a nightmare :)22/12 21:06
copumpkinyeah, diagMap is like a fair concatMap22/12 21:06
nappingare you having problems with extensionality?22/12 21:07
copumpkinnot really, mostly my problems are related to having to see through the metalanguage and codata22/12 21:08
copumpkinin fact, I've never really needed extensionality22/12 21:13
copumpkinunless I did and just didn't realize it :)22/12 21:13
nappingwell, sometimes it's hard to prove a = b and you have to just go for bisimulation22/12 21:13
copumpkinyeah22/12 21:15
copumpkinbedtime :) more on this tomorrow!22/12 21:16
nappingccasin: is the draft online somewhere?22/12 21:24
ccasinnapping: at aaron's website22/12 21:25
ccasinhttp://www.cs.uiowa.edu/~astump/22/12 21:25
ccasinits the one about equality reflection22/12 21:26
nappingah, so it's like OTT?22/12 21:27
nappingI was wondering what was specialy about the language, figured it was something like that, or stuff about controlling memory more directly22/12 21:28
ccasinnapping: honestly, I haven't read it yet, just read the conversation on the mailing list22/12 21:28
ccasinthe specifics of the language haven't been decided on yet, at this point we have a bunch of ideas and are trying them out22/12 21:29
ccasin(I'm a grad student on the project)22/12 21:30
ccasinbut, yeah, it's trying to solve some of the same problems as OTT22/12 21:30
nappingthe question is, why a new language?22/12 21:32
ccasinthe ones out there don't do everything we want!22/12 21:32
ccasincoq is too hard to program in, agda too hard to reason in, etc22/12 21:32
nappingor, which reasons motivate the language22/12 21:32
nappingCoq has some nice stuff. A tactics language is a pretty handy thing to have22/12 21:36
nappingI'd be really interested if you have a story for systems programming22/12 21:36
ccasinyes, but coq has problems too.  In particular, it's terrible to program in - two reasons come to mind immediately:22/12 21:37
ccasinfirst, dependent pattern matches are a mess, the programmer is expected to write down too much22/12 21:37
nappingor less ambitiously - some way to treat termination as an effect22/12 21:37
ccasinsecond, it's too strict about termination, programmers need to be able to write nonterminating functions and work with functions which may or may not terminate22/12 21:38
ccasinalso it has all the equality reasoning problems that upset the OTT people22/12 21:38
nappingyeah, that sounds about right22/12 21:38
ccasintactics are nice for reasoning though - the trellys idea is to support multiple external languages, one of them could be a tactic language22/12 21:39
--- Day changed Wed Dec 23 2009
* edwinb has heard sadly little about trellys23/12 00:00
edwinbas 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
Saizanedwinb: so that means you're confident that these decision procedures could be smart enough for most cases?23/12 00:08
edwinbNo23/12 00:08
edwinbjust 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 proofs23/12 00:09
edwinbbecause it's usually just a bit of list associativity, or arithmetic mangling, or similar23/12 00:10
Saizanyeah23/12 00:10
edwinba nice thing about Coq is that a lot of that just goes away23/12 00:10
edwinbit's a pity about the dependent pattern matching ;)23/12 00:10
Saizani guess using reflection in agda isn't near as nice23/12 00:12
edwinbI'm sure it could be eventually23/12 00:13
edwinbas soon as someone gets annoyed enough with doing proofs to make it nice... ;)23/12 00:13
Saizanheh, as i see it you'd need some compiler support to reify the goal at least23/12 00:15
edwinbyou'd need a bit of magic to help you, yes23/12 00:16
copumpkinhmm, not sure how to break up this part of my proof to a point where it becomes manageable23/12 05:15
copumpkinGoal: (x ∈ concat (sd ∷ .Diagonal.♯-0 (q ∷ sd) sds))23/12 05:31
copumpkinI realize that the .#-0 means that it's codata living in #, but what's the -0?23/12 05:31
copumpkinthere seems to be no documentation whatsoever on how it shows codata23/12 05:49
copumpkinagda's being mean to me23/12 07:23
dolioWell, 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
copumpkinlike what?23/12 07:50
dolioWell, type-preserving successor requires rebuilding the whole value, for instance.23/12 07:52
dolioLots 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
dolioRebuilding for successor means + is like O(n * (m + n)).23/12 07:54
dolioI really wish Agda could do binders with its mixfix, too.23/12 07:55
dolioI shed a tear each time I write "∃ λ n".23/12 07:55
copumpkinyeah :/23/12 07:57
copumpkinsubmit a feature request maybe?23/12 07:58
copumpkinnot really sure how the syntax would look23/12 07:58
dolioJust "∃ n" or even "∃ n : T".23/12 08:00
dolioCoq can do it, but I'm sure it's not a trivial change to the parser.23/12 08:01
dolioMaybe something could be done with a BUILTIN sigma declaration.23/12 08:06
dolioBecause sigma and exists are the ones that really grate on me.23/12 08:06
dolioI'm not dying to use W, for instance.23/12 08:09
-!- copumpkin_ is now known as copumpkin23/12 10:23
-!- copumpkin_ is now known as copumpkin23/12 11:20
-!- copumpkin_ is now known as copumpkin23/12 12:17
-!- copumpkin is now known as c0w_____________23/12 15:11
-!- c0w_____________ is now known as copumpkin23/12 15:13
-!- copumpkin_ is now known as copumpkin23/12 16:57
soupdragongrrrrr he didn't reply! "cranks don't respond to other cranks" I must be a crank23/12 16:59
copumpkinyou posted a comment?23/12 17:02
soupdragonI sent an email23/12 17:02
copumpkinoh23/12 17:03
-!- Saizan__ is now known as Saizan23/12 21:46
-!- BlackM is now known as BMeph23/12 21:52
copumpkinI guess we scared that crank back into his hole23/12 23:00
soupdragonno :)23/12 23:01
copumpkinor he realized he was wrong and doesn't quite know how to respond to people23/12 23:01
copumpkinoh did he reply to your email?23/12 23:01
soupdragonyeah23/12 23:02
copumpkinare we all just stuck in the box conventional mathematics has built around us?23/12 23:03
soupdragonwho isn't?23/12 23:05
copumpkinhe isn't!23/12 23:05
soupdragoneveryone is23/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:o23/12 23:12
copumpkinyou encouraged him?23/12 23:12
soupdragonI wouldn't say that23/12 23:14
copumpkinI guess it's good to have people questioning what's accepted23/12 23:14
copumpkinbut it's best if you understand what you're calling bullshit before you call it bullshit23/12 23:14
soupdragonI want to reply to him but I think I'd need another brandy to do so :P23/12 23:15
copumpkinhah23/12 23:15
soupdragonhe says that he is a platonist (in other words), which makes me wonder what sort of philosophy most computerologists are23/12 23:21
soupdragonthat intuitionism.org site is excellent but what about the other folks?23/12 23:21
soupdragonmight be the problem actually23/12 23:28
soupdragonif there's a fundamental truth that exist out there, then formal proof is irrelevant23/12 23:28
Saizanmh, it'd be nice to have some theory to talk about transactions (to e.g. reason about STM code)23/12 23:38
soupdragonSaizan IIRC there's a bit on that in Ynot23/12 23:39
* Saizan googles23/12 23:40
--- Day changed Thu Dec 24 2009
-!- copumpkin_ is now known as copumpkin24/12 01:19
soupdragonhttp://speculativeheresy.wordpress.com/2008/11/26/the-semantic-apocalypse/24/12 05:31
soupdragonstill on this 'crank' stuff24/12 05:31
soupdragonthanks to dolio :P24/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 copumpkin24/12 19:53
--- Day changed Fri Dec 25 2009
-!- copumpkin__ is now known as copumpkin25/12 00:10
soupdragonhi dolio25/12 00:11
dolioHi.25/12 00:34
soupdragonI hate the misuse of = :(25/12 00:34
soupdragonhttp://theprogrammersparadox.blogspot.com/2009/12/cantors-lost-surjection.html25/12 00:35
soupdragonit's the worst thing anyone can do25/12 00:35
dolioOh geeze. You're reading his blog now?25/12 00:35
soupdragonOh geeze?? this is your fault :P25/12 00:36
dolioYou gotta know when to hold 'em, know when to fold 'em.25/12 00:37
soupdragonI thought I got somewhere with my email but he's still writing complete bullshit like "countable != countably infinite"25/12 00:37
dolioWell, technically, countable can mean finite, as well.25/12 00:37
soupdragonthe meaning doesn't matter25/12 00:38
soupdragonit's the syntax he used that make me want to strangle him25/12 00:38
dolioHeh.25/12 00:38
soupdragonyou don't just write:   cats = good25/12 00:38
soupdragonalso he seems to have learned 'logic' or .. soemthing, from Hofstaders books -- so no wonder he writes this fucking nonsense25/12 00:39
dolioYeah, he started that over on good math, bad math.25/12 00:40
dolioI thought it was a bad sign.25/12 00:40
dolioAt some point he said something like "magic sequences are like strange loops, and strange loops are very confusing to people."25/12 00:41
soupdragonespecially to Cantor25/12 00:41
soupdragon:D25/12 00:41
dolioAnyhow, I think he's off the mark on the "you're a crank" diagnosis. That isn't a kneejerk reaction.25/12 00:48
soupdragonChu ?25/12 00:49
dolioIt'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
soupdragonoh right25/12 00:50
soupdragonI was never really interested in the technical content of what any of these folk are writing25/12 00:50
dolioThis one makes even less sense to me.25/12 00:50
dolioHe agrees that countable sets can be in bijection with subsets of themselves.25/12 00:50
dolioBut he still doesn't agree that you can have a bijection between NxN and N.25/12 00:51
soupdragonI gave him a really  nice bijection between Q and N25/12 00:51
soupdragonwhich he understands, I'm sure25/12 00:52
dolioHow'd you do it? Trees?25/12 00:52
dolioThe NxN zig-zagging one has problems since the rationals are a quotient.25/12 00:54
soupdragonsince 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 bijection25/12 00:54
soupdragonThen I said how any computer representation of R will be binary too :D25/12 00:55
dolioAh.25/12 00:55
soupdragonso there's this nuance: computables vs the real reals25/12 00:56
dolioYes, that's true.25/12 00:56
soupdragoncan you biject NxN into N via binary?25/12 00:58
soupdragonlike interleaved digits or something hm25/12 00:58
dolioThat actually sounds much easier than zig-zagging.25/12 00:58
dolioOh, but wait, NxN always has an even number of digits.25/12 00:59
dolioEr, bits.25/12 00:59
dolioOr, no, it doesn't.25/12 00:59
dolioAnd that's a problem.25/12 00:59
dolioYou have to encode the size of each natural somehow.25/12 01:00
soupdragonmaybe it's easier to understand countability as generated by grammars25/12 01:00
soupdragonif you pad with zeros I think it screws up the canonicity25/12 01:01
dolioPadding the first (second) element with zeros would get you a leading zero.25/12 01:04
dolioYou could tack a leading 1 on, though.25/12 01:04
dolio(m,n) = 1(interleave (pad m) (pad n))25/12 01:05
dolioThat probably isn't surjective, though.25/12 01:05
dolioBut, it's injective, and you can easily make an injection in the other direction, like m -> (m, 0).25/12 01:07
dolioAnd then use that 3-name theorem.25/12 01:07
soupdragondamn!!25/12 01:08
soupdragonCantor-Bernstein-Schroeder25/12 01:08
* soupdragon wants to whack him over the head with Conceptual Mathematics a few times, then with Sets for Mathematics25/12 01:13
soupdragonmaybe finish him off with Coq'Art (hardback edition)25/12 01:13
dolioThe guy in the comments of this one is giving some pretty thorough set theory notes.25/12 01:13
soupdragonboo down with set theory25/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
soupdragonT1 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
soupdragonoh right he's claimed ZF(C?) inconsistent25/12 01:21
dolioI don't imagine C is necessary.25/12 01:21
dolioIt hasn't come up, at least.25/12 01:21
soupdragondamn I don't know how to reply to this25/12 01:24
soupdragonthe writing style is such a mess and the syntax is fucked25/12 01:24
dolioI wouldn't bother.25/12 01:24
soupdragonwhat'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
soupdragonhttp://www.bitcount.ca/25/12 01:30
soupdragonthat's his company25/12 01:30
soupdragonit's about COMPLEX software development :D25/12 01:30
soupdragonI've been wasting all my time trying to make things simple25/12 01:31
soupdragonhe's published a book ... http://www.lulu.com/content/105456625/12 01:32
dolioHe 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
dolioBut that's just the union of two countable sets.25/12 01:33
dolioBut {1, 3, 5, ...} and {2, 4, 6, ...} are countable, and their union is N.25/12 01:33
dolioAnd he agrees that N can be put into 1-to-1 correspondence with subsets of itself.25/12 01:33
soupdragonwell {a1, a2, a3, ..., b1, b2, b3, ...} isn't anything25/12 01:34
dolioIt's intended to be the union of {a1, a2, a3, ...} and {b1, b2, b3, ...}25/12 01:34
soupdragonmaybe25/12 01:35
soupdragonI don't really bother to try and understand this stuff, it's all nonsense anyway25/12 01:35
dolioI think the guy in the comments is on to something about (N, <) and order isomorphisms.25/12 01:36
dolioIn 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
soupdragonprobably a screwball :P25/12 01:38
dolio{a1, a2, a3, ..., b1, b2, b3 ...} looks like a depiction of omega + omega.25/12 01:39
dolioAnd his magic sequences were omega*omega.25/12 01:42
soupdragonI don't know what to say about "magic sequences"25/12 01:47
soupdragonmisconstrued sequences25/12 01:47
soupdragonhttp://muaddibspace.blogspot.com/2009/12/zfcs-probably-inconsistent.html25/12 01:52
soupdragonI think I give up on this cantor stuff now25/12 01:52
* soupdragon realized.. nothing else to do25/12 02:04
uoryglHmm. 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
soupdragonuorygl, well that's  not a set theory set, but it is a set in some sense25/12 04:04
uoryglRight.25/12 04:04
uoryglAn 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
soupdragonwait25/12 04:05
soupdragonthat definition doesn't make sense to me25/12 04:05
soupdragonsuppose O : Set, is the type of ordinals25/12 04:05
soupdragonmaybe  zero = const false : O -> Bool  is the zero ordinal?25/12 04:06
uoryglYep.25/12 04:06
soupdragonsort of need to solve the domain equation O = O -> Bool,  i.e. O is closed by powerset?25/12 04:06
uoryglWell, it's not O -> Bool. It's the dependent product of that with something.25/12 04:07
uoryglA subset of O -> Bool.25/12 04:07
soupdragonhm25/12 04:07
dolioThat 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
dolioLike, 1 = {0}, but you can't write "one (const false) = true ; one _ = false".25/12 04:09
uoryglAww.25/12 04:10
uoryglWell, you can determine whether an ordinal is zero or not by passing zero to it.25/12 04:11
uoryglone x = not (x zero)25/12 04:11
uoryglI think you can define all the finite ordinals that way. two x = not (x one); three x = not (x two); . . .25/12 04:13
soupdragonthe problem with  X -> Bool  is that you have decidible membership25/12 04:13
uoryglYou can't define omega that way, though; there's no way to tell that omega is not finite.25/12 04:14
uoryglAlso, I feel a paradox coming on.25/12 04:15
soupdragonI'll make you a cup of honey and lemon25/12 04:16
uoryglLet top x = true. This defines a transitive set, and its domain is the ordinals, meaning it's an ordinal itself.25/12 04:16
uoryglAnd, uh, I'm sure the paradox is around here somewhere.25/12 04:16
soupdragonuoaygl,  isomorphic to powerset  is cantor diagonalization25/12 04:17
soupdragonthink of N -> Bool, not as a set of booleans, but a binary sequence25/12 04:18
uoryglHmm. You can't test that omega is not finite, but you can prove that omega is not finite. I think.25/12 04:18
dolioYou've jettisoned positivity, so you can prove anything you want.25/12 04:19
-!- copumpkin_ is now known as copumpkin25/12 04:54
soupdragonI 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??? lol25/12 05:42
copumpkin?25/12 05:42
copumpkinoh, he replied to all the blog comments25/12 06:40
copumpkinwith no real substance, but luckily for us he's preparing a new blog post25/12 06:40
-!- dblhelix_ is now known as dblhelix25/12 07:32
copumpkintwo days later, I succeeded at proving another case of this25/12 12:36
copumpkinI guess the solution is to keep breaking it down until it's trivial25/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
copumpkinhah25/12 13:24
copumpkinI wish25/12 13:24
copumpkinthis is turning into a monstrosity25/12 13:24
copumpkinhttp://snapplr.com/vsxf25/12 13:25
copumpkinseems like it'd be fairly obvious, but I can't figure out what the notation really means25/12 13:26
copumpkinI 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 where25/12 13:27
copumpkinI've got no wheres anywhere :/25/12 13:27
copumpkinI do have withs25/12 13:28
copumpkinthe frustrating thing is that I'm not decomposing my inputs, I'm decomposing the output of a function on my inputs25/12 13:28
copumpkinhttp://snapplr.com/3ec125/12 13:29
Saizan_hah25/12 13:31
copumpkinit seems like there must be an easier way but I can't see it25/12 13:32
Saizan_i generally decompose inputs to cause refinements in the function applied to them25/12 13:32
copumpkinI tried that, but agda couldn't see through it25/12 13:32
copumpkinmaybe I should shelve this current proof and try decomposing inputs more25/12 13:32
copumpkinqs is codata so I can't decompose that though25/12 13:33
Saizan_ah, no, i'm wrong25/12 13:33
copumpkin?25/12 13:34
copumpkinI'm willing to try anything that would make this less painful :P25/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 anyway25/12 13:36
copumpkinyeah25/12 13:40
-!- copumpkin_ is now known as copumpkin25/12 14:19
-!- copumpkin_ is now known as copumpkin25/12 15:24
-!- copumpkin__ is now known as copumpkin25/12 16:01
copumpkinanyone proving anything interesting these days?25/12 16:13
copumpkinI was leafing through a spinoza book the other day25/12 16:14
copumpkinand came across his proof of god25/12 16:14
copumpkinwe should prove that in agda ;)25/12 16:14
copumpkinaGDa25/12 16:14
soupdragonI heard about spinoza hadn't picked up the loose neds yet25/12 16:14
soupdragonends*25/12 16:14
soupdragonon that round table discussion, they all seemed fto dig spinoza25/12 16:15
Saizan_well, spinoza almost redefined god as the universe, so it's not surprising he has a proof25/12 16:18
soupdragondid you see this punpkin25/12 16:43
soupdragonhttp://muaddibspace.blogspot.com/2009/12/zfcs-probably-inconsistent.html25/12 16:43
copumpkin_hah, nope25/12 16:45
Saizan_nice one :)25/12 16:45
* increpare chuckles25/12 16:46
soupdragonI want to learn more about the link with comptational semantics and dependent type theory, kind of a huge topic to take on though25/12 16:47
-!- copumpkin_ is now known as copumpkin25/12 16:50
copumpkinI guess I should prove more general stuff about this function25/12 17:35
copumpkinmight be easier than dealing with this nasty stuff25/12 17:35
-!- copumpkin is now known as monochromboy25/12 19:28
-!- monochromboy is now known as copumpkin25/12 19:29
-!- EnglishGent is now known as EnglishGent^afk25/12 21:23
-!- copumpkin_ is now known as copumpkin25/12 21:35
-!- copumpkin_ is now known as copumpkin25/12 23:21
-!- copumpkin_ is now known as copumpkin25/12 23:41
--- Day changed Sat Dec 26 2009
-!- copumpkin_ is now known as copumpkin26/12 01:10
-!- copumpkin_ is now known as copumpkin26/12 01:18
-!- copumpkin_ is now known as copumpkin26/12 02:52
-!- copumpkin_ is now known as copumpkin26/12 03:43
-!- copumpkin__ is now known as copumpkin26/12 05:27
-!- copumpkin_ is now known as copumpkin26/12 05:40
-!- copumpkin_ is now known as copumpkin26/12 06:07
-!- dblhelix_ is now known as dblhelix26/12 07:32
copumpkinI wish I could pattern match on codata26/12 08:43
copumpkinhmm, I can't even seem to prove the definition of one of my nasty codata sublanguage evaluator functions26/12 13:28
Saizan_prove the definition?26/12 13:29
copumpkinI guess it isn't quite the definition26/12 13:29
copumpkinbut it's almost f = ...26/12 13:29
copumpkinand I can barely prove that f = ... :P26/12 13:29
soupdragonbring on OTT!26/12 13:29
soupdragonI thought chistmas was coming soon?26/12 13:29
copumpkinthe recursive cases on this indirect codata stuff seem particularly hair-raising26/12 13:36
copumpkinis it normal for a hole to change the termination properties of a function?26/12 14:01
soupdragonon meth it is26/12 14:01
copumpkinI always have a heart attack when my function turns pink, then I fill in another hole and the pink goes away26/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 codata26/12 14:06
copumpkinyay, one more yak shaved26/12 14:33
* copumpkin is inching towards his proof in a giant spiral 26/12 14:33
copumpkin_ is my new best friend26/12 14:41
copumpkinsometimes it can infer things that I wouldn't even know how to write26/12 14:41
Saizan_eheh26/12 14:41
Saizan_it'd be nice if it could spit them out26/12 14:42
-!- copumpkin_ is now known as copumpkin26/12 16:37
copumpkinseems to be a pretty big regression in C-c C-c26/12 17:02
copumpkinit fucks up a lot26/12 17:02
* copumpkin coughs26/12 17:31
copumpkinlemma6 : ∀ {A} → (x : A) → (y : A) → (ys : _) → x ∈ fromList⁺ ys → x ∈ y ∷ _26/12 17:31
copumpkinmy abuse of _ continues26/12 17:31
copumpkinsometimes it gets confused though26/12 17:39
* copumpkin fumbles around in the dark, even proving things that he doesn't understand26/12 18:21
copumpkindolio: do you know what the number is when displaying codata?26/12 19:12
dolioNo.26/12 19:12
copumpkinHm, okay, thanks26/12 19:12
copumpkinit feels a little silly to have a lemma (that I proved) whose type I do not know, but that I use anyway26/12 19:14
dolioOh, it may be an implicitly defined function.26/12 19:25
dolioYou used to have to write corecursion like "cofoo ~ cocon cofoo".26/12 19:25
copumpkinmost of them are of the form Module.♯ -N26/12 19:25
dolioBut now I think you can write "cofoo = cocon cofoo".26/12 19:26
copumpkinyou think something like map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)26/12 19:26
copumpkincounts?26/12 19:26
dolioWhich may still desugar into "cofoo = cocon-0 where cocon-0 ~ cocon cofoo".26/12 19:26
copumpkinoh, I see26/12 19:26
copumpkinso it desugars it when I write it, but when displaying it's forgotten about the sugar26/12 19:27
dolioBecause 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
copumpkinand won't reguar it for me26/12 19:27
copumpkinhm26/12 19:27
copumpkinso I guess -0 is probably the first time I corecurse in that module, and so on26/12 19:28
copumpkinmaybe I'll submit an enhancement request26/12 19:28
dolioYes.26/12 19:28
dolioIf 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
dolioSo that's what it is.26/12 19:29
copumpkinaha, thanks a lot26/12 19:30
dolioIf you write a function on inductive data that uses "foo ... = ... where zing = ...", you might see ".Stuff.zing" during some proofs.26/12 19:32
copumpkinI see26/12 19:34
copumpkinnever noticed that26/12 19:34
doliohttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=15031#a1503126/12 19:38
copumpkincool26/12 19:38
copumpkinlearn something new every day!26/12 19:38
dolioI don't know what exactly the codata stuff is desugaring to, though. The old ~ syntax is no longer accepted.26/12 19:39
copumpkinah26/12 19:40
copumpkinI'm guessing codata doesn't get too much love in most proofs26/12 19:40
copumpkinhmm, I think the numbers may be from the bottom of the module o.O26/12 19:41
copumpkinmaybe not26/12 19:41
copumpkindo the recursive calls to whnf here count too? http://snapplr.com/3t2j26/12 19:52
copumpkinor is it only when I stick some sharps in the recursion?26/12 19:52
dolioI expect it only generates code when you use sharp.26/12 19:59
-!- copumpkin_ is now known as copumpkin26/12 20:32
-!- copumpkin_ is now known as copumpkin26/12 21:11
--- Day changed Sun Dec 27 2009
-!- copumpkin_ is now known as copumpkin27/12 02:43
-!- copumpkin_ is now known as copumpkin27/12 03:15
-!- copumpkin_ is now known as copumpkin27/12 19:15
-!- copumpkin_ is now known as copumpkin27/12 19:45
soupdragonmake nat := (Mu @ [`arg { zero, suc } [ (@ [`done]) (@ [`ind1 @ [`done]]) ] ] ) : * ;27/12 20:37
soupdragonmake zero := @ [`zero] : nat ;27/12 20:37
soupdragonmake suc := (\ x -> @ [`suc x]) : nat -> nat ;27/12 20:37
soupdragonmake one := (suc zero) : nat ;27/12 20:37
soupdragonmake two := (suc one) : nat ;27/12 20:37
soupdragonmake plus := @ @ [(\ r r y -> y) (\ r -> @ \ h r y -> suc (h y))] : nat -> nat -> nat ;27/12 20:37
soupdragonmake x := (plus two two) : nat27/12 20:37
Saizan_what's that?27/12 20:42
soupdragonsomething from inside epigram27/12 20:47
-!- copumpkin is now known as HaskellNinja27/12 21:49
-!- HaskellNinja is now known as copumpkin27/12 21:55
--- Day changed Mon Dec 28 2009
-!- copumpkin_ is now known as copumpkin28/12 03:17
-!- copumpkin_ is now known as copumpkin28/12 03:46
--- Day changed Tue Dec 29 2009
-!- Saizan_ is now known as Saizan29/12 11:15
copumpkinhttp://code.google.com/p/agda/issues/detail?id=23629/12 16:50
copumpkin:(29/12 16:50
Saizan:\29/12 16:55
copumpkinit seems like a pretty shitty state of affairs, to have a bunch of autogenerated names that don't actually mean anything to you29/12 16:56
doliocopumpkin: Is that the goal you get with C-c C-,?29/12 16:57
copumpkinyeah29/12 16:57
copumpkinI have those # -N everywhere in this proof29/12 16:57
copumpkinsometimes I can figure out what they mean, but most of the time it's just really tedious29/12 16:58
Saizanwell, the only possible improvement would be to specify from which application of # they come from29/12 16:58
dolioWell, it's a bit odd for flat (sharp ...) to be there.29/12 16:58
copumpkinoh, that's not common29/12 16:58
copumpkinbut in general, my goals are full of those sharps29/12 16:59
copumpkinis there some secret technique to proving things about corecursive functions that I just missed?29/12 17:00
dolioPresumably you need to do introduce a flat, or to provide enough information for flat to compute.29/12 17:01
copumpkinyeah, but they're recursive, so if I flatten one level, I'll just get another sharp for the next29/12 17:01
copumpkin"Two delayed applications of a coinductive constructor are not29/12 17:02
copumpkin  definitionally equal unless they come from the same location in29/12 17:02
copumpkin  the source code." seems a little scary29/12 17:02
dolioCoinductive types don't have constructors.29/12 17:03
dolioSo, 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
copumpkinyeah29/12 17:07
copumpkinso how would one prove something about those?29/12 17:07
dolioi is an infinite unfold, and j is an unfold that adds one cosuc and reunfolds i.29/12 17:07
Saizanbisimulation!29/12 17:07
copumpkinwould i = cosuc (# i) and j = cosuc (# j) be equal?29/12 17:08
dolioThey might if you expressed them in terms of unfolds, since they could be the same unfold expression.29/12 17:09
dolioBut 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
copumpkinlike what?29/12 17:10
dolioLike 'i = unfold inr 0' 'j = unfold inr 1'.29/12 17:10
dolioN X = 1 + X being the functor in question.29/12 17:11
copumpkinyeah29/12 17:11
dolioSo, does unfold inr 0 = unfold inr 1? Not intensionally.29/12 17:11
copumpkin:/ yeah29/12 17:12
copumpkinso 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
dolioAre you trying to prove things involving equality? Because that'd be a bad idea.29/12 17:14
copumpkinnot really, just trying to show \in things29/12 17:15
copumpkinfor Colists29/12 17:15
copumpkinthis is still related to the Diagonal proof29/12 17:19
copumpkinmaybe I should just drop the Colist29/12 17:19
copumpkinbut I really don't like Nat -> a29/12 17:20
copumpkinespecially since my Colists aren't necessarily infinite29/12 17:20
dolioNat -> a isn't a colist anyway.29/12 17:20
dolioI'm not really sure what the encoding of colists is.29/12 17:20
dolioMaybe 'Sig n. || n || -> a', for that family of countable types I mentioned the other day29/12 17:22
dolioBut then n is codata, so you'd have to encode that, too.29/12 17:22
copumpkinyeah29/12 17:22
dolioI should find and read about encoding M-types some time.29/12 17:23
dolioThere'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
copumpkininteresting29/12 17:23
-!- EnglishGent is now known as EnglishGent^afk29/12 20:04
--- Day changed Wed Dec 30 2009
copumpkinooh30/12 12:20
copumpkinhttp://twitter.com/pigworker/status/719425949630/12 12:21
soupdragoncool30/12 12:22
-!- opdolio is now known as dolio30/12 16:44
--- Day changed Thu Dec 31 2009
jmcarthurso... loading the README.agda file in the standard library is making my laptop with 4 GB of RAM cry31/12 07:36
jmcarthurheh, oh look, it's done loading31/12 07:37
jmcarthuryeah, it's taking over 3.6 gigs of ram. nice31/12 07:38
soupdragongo haskell!31/12 07:42
jmcarthurquitting and loading fresh brought it down to "only" about 1.5 gigs31/12 07:47
copumpkinjmcarthur: proving anything interesting?31/12 13:01
copumpkinI guess he's probably asleep31/12 13:01
jmcarthurcopumpkin: 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 library31/12 16:28
copumpkinah :)31/12 16:28
jmcarthuri would like to start getting more into agda31/12 16:28
copumpkinmmm31/12 16:28
copumpkinbeware of the corecursion!31/12 16:28
copumpkin'sdeath ;)31/12 16:28
jmcarthurrunning into problems with it?31/12 16:29
jmcarthuri like corecursion :(31/12 16:29
copumpkinyeah31/12 16:29
copumpkinI have the ugliest proof ever with a few holes that I can't figure out how to fill because the goal isn't clear31/12 16:29
copumpkinjmcarthur: have you done any proofs about corecursive definitions?31/12 16:31
jmcarthurnope31/12 16:32
jmcarthurare you using codata directly or [infinity symbol]?31/12 16:33
copumpkininfinity symbol31/12 16:33

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