--- Log opened Tue Sep 01 00:00:24 2009
sharada# Norio Kato - A new implementation of Agda written in Java01/09 17:14
sharadaanyone know where to get details on that?01/09 17:14
* copumpkin saw something about an agda in java before disconnecting???01/09 19:26
copumpkinthat seems like a very strange choice01/09 19:26
-!- badtruffle is now known as copumpkin01/09 20:26
sharadaI still don't get the codata equality stuff :(01/09 21:26
-!- byorgey_ is now known as byorgey01/09 22:14
--- Day changed Wed Sep 02 2009
glguycopumpkin: good point02/09 07:20
copumpkinI wish my emacs wouldn't freeze when I try to use agda :(02/09 07:29
copumpkinnot really sure what it's doing02/09 07:29
byorgeycopumpkin: maybe it's looking for a specific ghci prompt02/09 07:36
byorgeythis is a problem I had once02/09 07:37
copumpkinit's got ghc as a subprocess02/09 07:37
copumpkinand isn't pegging my cpu or anything02/09 07:37
byorgeyI had to :set the prompt to something specific or else it froze02/09 07:37
copumpkinemacs and ghci are just sitting there idle, and unresponsive02/09 07:37
copumpkinhmm02/09 07:37
Saizani get a similar problem with haskell-mode if i don't have at least a module in the prompt02/09 07:38
copumpkinhmm02/09 07:40
copumpkinhow do I do that? I'm not usually an emacs user, and am just using it so I can play with agda ;)02/09 07:40
Saizan:set is a ghci command02/09 07:41
copumpkinI have02/09 07:41
copumpkin(load-file (let ((coding-system-for-read 'utf-8))02/09 07:41
copumpkin                (shell-command-to-string "agda-mode locate")))02/09 07:41
copumpkinin my .emacs02/09 07:41
copumpkinoh, I see02/09 07:41
copumpkinbut agda-mode appears to ask ghci to ignore the .ghci file02/09 07:41
copumpkinhow would I set the prompt?02/09 07:42
copumpkin:/02/09 07:49
copumpkinah, I can unhang with C-g02/09 07:52
copumpkinand then play with ghci02/09 07:52
copumpkinoh, it's a linker problem o.O02/09 07:53
copumpkinI'll fix it tomorrow02/09 07:54
sharadabeta eta equalty still doesn't equate \n -> n + 0 with \n -> 0 + n in the same way that $equality equality doesn't relate $codata1 with $codata202/09 09:18
sharadahelp me fill in the blanks? :P02/09 09:18
sharadaam I even on the right track02/09 09:18
* sharada repeats::::02/09 10:03
sharadabeta eta equalty still doesn't equate \n -> n + 0 with \n -> 0 + n in the same way that $equality equality doesn't relate $codata1 with $codata202/09 10:03
sharadais that right? and what is missing02/09 10:03
dolioFor $equality you could have "intensional", I suppose.02/09 10:06
dolioIntensional equality lets you demonstrat \n -> n + 0 = \n -> 0 + n because you can demonstrate that n + 0 = 0 + n.02/09 10:07
sharadaoh yeah02/09 10:08
sharadaI should use intensional in both cases02/09 10:08
sharadais there a canonical example like the n + 0  0 + n thing for codata though?02/09 10:08
dolioThere are plenty of simple examples, I suppose.02/09 10:09
dolio'1 :: repeat 1' is not intensionally equal to 'repeat 1'.02/09 10:09
dolioWell, unless you can cheat by evaluation like in Coq.02/09 10:10
sharadaoh wow :|02/09 10:10
sharadawhat if I make02/09 10:10
sharadaf (x :: xs) = x :: xs02/09 10:10
sharadathen f (1 :: repeat 1) = f (repeat 1)?02/09 10:10
dolioWell, it rather depends on what semantics you're using. With the old, broken codata type stuff, 'f xs' might be treated as a reducible expression, in which case you'd get "1 :: repeat 1 = 1 :: repeat 1".02/09 10:13
dolioBut from a strict categorical perspective, f (1 :: repeat 1) is just as irreducible as 1 :: repeat 1 and repeat 1.02/09 10:14
dolioAnd f (repeat 1). So none are intensionally equal.02/09 10:14
sharadaugbhhh02/09 10:14
sharadaI don't get how any of this can work properly02/09 10:14
dolioTreating them as able to be reduced is what breaks subject reduction in Coq.02/09 10:14
dolio(That's the right term, right?)02/09 10:15
sharadayeah02/09 10:15
dolioWay back someone showed how you could write a proof of intensional equality for those sorts of bisimulations, though.02/09 10:15
dolioBut that seems wrong to me.02/09 10:15
dolioThe paper on the partiality monad uses some "rewrite" tactic that you couldn't simulate easily in the original coinductive Agda for that purpose, I think.02/09 10:16
sharadabisimulation -> equality is bad?02/09 10:16
dolioIt's not bad, but it's extensional in character.02/09 10:17
dolioThe fact that you can prove it in Coq instead of assuming it as an axiom or something is weird.02/09 10:17
dolioIt'd be like being able to prove "(forall x -> f x = g x) -> f = g".02/09 10:19
sharadaI see02/09 10:19
dolioIt helps me a little to think of existential encodings of coinductive stuff.02/09 10:22
dolioSo, like, repeat 1 might be "(1 , g) where g x = (x, (x, g))" and the observation functions are "head (x, g) = fst (g x) ; tail (x, g) = snd (g x)".02/09 10:23
sharadathe finality  ?02/09 10:24
dolioAnd then you might have "h :: t = ((h, t), id)".02/09 10:25
ski_wouldn't that `g' have cyclic type ?02/09 10:26
dolioSo, if you look at what they're made out of, then "repeat 1 = (1, g)" and "1 :: repeat 1 = ((1, (1, g)), id)", so they're not built out of the same thing. But they do produce the same observations.02/09 10:27
dolioDoes it? I hope not.02/09 10:28
ski_hm, i would take `Stream a = exists s. s * (s -> a * s)' (or s/(s -> a * s)/(s -> a) * (s -> s)/ if preferred)02/09 10:31
dolioYeah, the former was my intention.02/09 10:32
ski_but it seemed you wanted `Stream a = exists s. mu r. s * (s -> a * r)' (or maybe s/mu/nu/ ?)02/09 10:32
dolioOh, yeah, I guess I was a bit muddled.02/09 10:33
ski_using the former, `repeat 1' becomes `(1,g) where g x = (x,x)' with `head (s,g) = fst (g s)' and `tail (s,g) = (snd (g s),g)'02/09 10:34
ski_(your "can change the behaviour as we go" can still be encoded)02/09 10:35
dolioSo, 'repeat 1 = (1, g) where g x = (x, x)' and 'x :: (s, f) = (inl x, g) where g (inl x) = (x, inr s) ; g (inr s) = let (y, s') = f s in (y, inr s')' or something.02/09 10:35
ski_hm .. the repeated use of `inr' looks irksome02/09 10:36
dolioYeah. I'm not sure how stream fusion handles that sort of thing.02/09 10:37
dolioThey might use (Maybe s1, s2).02/09 10:37
dolioThat doesn't look a lot better, though.02/09 10:37
ski_btw, wouldn't the same problem happen with equality on quotient types, as with stream and function types ?02/09 10:38
dolioProbably.02/09 10:38
dolioNuPRL and MetaPRL from that paper on quotient types are both extensional, I think it says.02/09 10:38
ski_(maybe it would be better anyway to allow changing the state type)02/09 10:38
ski_  Stream a = mu r. exists s. s * (s -> a * r)  -- s/mu/nu/ ?02/09 10:40
ski_(but then why use an existential at all, instead of just `Stream a = nu r. a * r' ?)02/09 10:40
doliostream-fusion uses Bool * s as the state when you cons, apparently.02/09 10:42
dolioOnly it's not Bool, it's some type with values S1 and S2.02/09 10:43
* ski_ wonders if one could do it with (contra-)recursive types, instead ..02/09 10:44
dolioWhich it uses like: h :: (s, f) = (Nothing, g) where g Nothing = (h, Just s) ; g (Just s) = let (x, s') = f s in (x, Just s')02/09 10:45
dolioOnly instead of nothing it uses (S2, s) and instead of Just s it uses (S1, s).02/09 10:46
dolioAnyhow, my overall point was that coinductive types can be modeled with existentials, and you might have two values that are built out of things you couldn't prove intensionally equal, but they are nevertheless the same coinductive value, since all you can do with them is observe them, and they behave identically under that operation.02/09 10:48
dolioWhich is a hand-wavey reason why "repeat 1" and "1 :: repeat 1" are not intensionally equal, despite the fact that they're obviously the same value.02/09 10:49
dolioAnd the fact that you can prove them equal in Coq is weird, and leads one to suspect that the way it handles coinductive types and the operations thereon is fishy.02/09 10:51
* ski_ forgets what's the difference between intensional and extensional equality ..02/09 10:53
dolioI'm not really certain what the formal definitions are.02/09 10:53
dolioIntensional equality gets you m = n if m and n have the same normal form, or something.02/09 10:55
ski_(i think "Programming in Martin-Loef Type Theory" mentioned it .. something with how the equality judgement there is related (or not) to the type of equality proofs)02/09 10:55
ski_(but i don't recall the details)02/09 10:55
dolioExtensional gets you m = n when all the ways you can use them produce the same results.02/09 10:56
dolioRougly.02/09 10:56
ski_"normal forms" seems not proper to speak of for coinductive data02/09 10:56
dolioRoughly, even.02/09 10:56
ski_(including functions)02/09 10:56
ski_(cf. "terminating" vs. "productive")02/09 10:57
codolioI'd say the normal form of "repeat 1" is "repeat 1", because values with a coinductive type aren't subject to reduction.02/09 10:58
codolioYou can only reduce "observe (repeat 1)".02/09 10:58
-!- codolio is now known as dolio02/09 10:58
ski_imio, functions (and other things that are defined in terms of how to use them) should have extensional equality02/09 11:00
ski_dolio : yes02/09 11:01
dolioYeah. I'm not sure what problems you face when you add extensional equality to your language. Undecidability comes to mind.02/09 11:02
dolioBut then OTT is claimed to get you all the good without the bad. So that'd be nice.02/09 11:02
dolioSo, I'm looking forward to Epigram 2. :)02/09 11:03
ski_is that related to OTT ?02/09 11:03
dolioI'm pretty sure Epigram 2 is where Conor McBride and his buddies are implementing all their ideas in that area.02/09 11:05
dolioOr that's the idea, anyway.02/09 11:05
ski_is OTT an abstract system, while Epigram being an implementation ?02/09 11:06
dolioYeah. Like System Fc and GHC, I guess.02/09 11:06
dolioThere's already some OTT stuff implemented in Agda somewhere as a proof of concept, I think.02/09 11:07
ski_ok02/09 11:07
dolioThat is, formalized using Agda. Not built into its type system and whatnot.02/09 11:08
ski_*nod*02/09 11:09
sharada <ski_> imio, functions (and other things that are defined in terms of how to use them) should have extensional equality02/09 12:16
sharadain type theory??02/09 12:16
sharada <dolio> And the fact that you can prove them equal in Coq is weird, and leads one to suspect that the way it handles coinductive types and the operations thereon is fishy.02/09 12:18
sharadabut is Agda better? and what is the right way to do it02/09 12:18
dolioI thought they changed Agda to make it handle things different, but I'm not completely sure.02/09 12:22
dolioPeople have, at the least, figured out how to set things up appropriately to adhere to the way the category theory works.02/09 12:24
dolioI'm also not sure anyone figured out how to prove the intensional equality of two different bisimilar things in Agda, either, but that might just be because it isn't as easy.02/09 12:25
dolioFinding the actual proof is proving difficult, though.02/09 12:32
dolioAnd I don't know enough Coq to reconstruct it, if it even still works.02/09 12:33
dolioOh, found it. Bad thread name.02/09 12:38
doliohttp://logical.saclay.inria.fr/coq-puma/messages/c8acae734082fd1b#msg-b1a0f4aa5ab9ac6f02/09 12:40
dolioI think if you scroll down a couple messages (to the one below mine) you'll see a proof that bisimilarity implies intensional equality.02/09 12:41
dolioFor streams.02/09 12:41
sharada"Actually all coinductive types can be encoded as omega-limits once you have functional extensionality"  says Thorsten02/09 12:55
sharadaCan you build every element using finality?02/09 13:01
sharadafor stream finality is:02/09 13:02
sharadastream_finality (f : B -> 1 + A * B)  : B -> stream A02/09 13:02
sharadastream_finality b | f b => left () = nil | f b => right (x, y) = x :: stream_finality y02/09 13:03
copumpkinso my emacs has stopped hanging now02/09 14:48
copumpkinhowever, now it's complaining that the function 'main' is not in MAlonzo.<MyModule>02/09 14:49
copumpkinI could've sworn I used to use the compile command to compile modules with no main function02/09 14:53
copumpkinah well, I guess the load command will typecheck too02/09 14:55
Saizanthe agda emacs mode is much nicer than the haskell one02/09 15:41
copumpkinyep :)02/09 16:05
* copumpkin is enjoying it now02/09 16:05
glguyAre these reasonable implementations of associativity and commutivity of addition on naturals? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=896702/09 18:38
sharadano02/09 19:27
glguysharada: Was that for me?02/09 21:16
sharadayeah02/09 21:16
glguyThis is my first .agda file02/09 21:16
sharadaI don't think you should call it 'mylemma'02/09 21:16
glguywhat sort of things could be improved02/09 21:17
glguyvery true02/09 21:17
sharadaalso you can write x + y == y + x rather than (x + y) == (y + x), just give == a lower fixity than +02/09 21:17
sharadait's fine other than that - you could try to rewrite it using the equational reasoning module though, that is a really cool library in agda worth at least reading about02/09 21:18
glguyThat is part of lib-0.2?02/09 21:18
sharadawell it's part of agda standard lib02/09 21:18
sharadayou can get that off the wiki using darcs02/09 21:19
sharadaI don't think it comes with agda program02/09 21:19
glguyIn Relation.Beinary.EqReasoning[1] there is an example using begin and \qed. What defines these? 1. http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Relation.Binary.EqReasoning.html02/09 21:31
glguyor is that just an explanation in English?02/09 21:31
sharadaglguy no that's actual code02/09 21:31
glguyAh, I found it02/09 21:31
glguyin PreorderReasoning, at least02/09 21:31
sharadaglguy I don't know where it's defined but if you click on it inside agda mode that should take you there I think02/09 21:32
--- Day changed Thu Sep 03 2009
doliocopumpkin: You were using the compiler?03/09 02:58
copumpkinhow do I use one "statement" to prove another in agda? in haskell I'd do case blah of x -> and it would "bring its knowledge into scope"03/09 05:16
* copumpkin fails hard :)03/09 05:16
doliowith, probably.03/09 05:17
doliofoo x with bar x03/09 05:17
copumpkinah great, thanks :)03/09 05:17
dolio... | match-against-bar-x = ...03/09 05:18
doliowith is sugar for defining auxillary functions, so you could do that, too.03/09 05:18
copumpkinseems like agda could benefit from a hoogle-like search function even more than haskell could03/09 05:21
copumpkin"find me a proof that P = NP kthx"03/09 05:21
dolioIncidentally, you were using the compiler? I've never used that.03/09 05:25
dolioMaybe it's slower than the interpreter, and that's why it was taking so long.03/09 05:25
copumpkinnah, it was taking so long because I had a linker error when loading the agda lib03/09 05:25
copumpkinso the ghci prompt was >03/09 05:26
dolioEspecially if it was compiling a chain of imported modules.03/09 05:26
copumpkinand agda's silly and hangs03/09 05:26
dolioAh.03/09 05:26
copumpkinis there a particularly elegant way to express induction over the naturals in agda?03/09 06:10
copumpkinI was thinking of using the Holds type from http://wiki.portal.chalmers.se/agda/agda.php?n=Main.TypesSummerSchool2007?action=view03/09 06:11
copumpkinsomething like induction : {n : ℕ} (p : ℕ → Bool) → Holds p zero → ({m : ℕ} → Holds p m → Holds p (suc m)) → Holds p n03/09 06:13
copumpkinbut is that "idiomatic"?03/09 06:13
copumpkinit's a rather restricted definition of induction, for one03/09 06:17
copumpkinbut assuming it's sufficient03/09 06:17
copumpkinmaybe going through the Bool type is a little indirect03/09 06:31
dolioI usually use P : Nat -> Set.03/09 06:40
dolio(P m -> P (suc m)) -> P 0 -> n -> P n03/09 06:40
copumpkinah, simple enough03/09 06:41
copumpkinso do you do an implicit P?03/09 06:42
copumpkinor does it not really matter?03/09 06:42
dolioYes.03/09 06:42
copumpkinah ok03/09 06:42
dolioAlthough I don't know if that's necessarily more useful.03/09 06:42
dolioIt might not be, but it isn't a big deal to wrap braces around the predicate when it can't be inferred.03/09 06:44
copumpkinyeah :)03/09 06:44
dolioIn general I'm tempted to not use booleans in a language like Agda.03/09 06:46
copumpkinwhat does it mean when I get something highlighted in yellow?03/09 06:46
copumpkinyeah, they seem unnecessary, but I saw them in that wiki page and assumed they'd serve some purpose03/09 06:47
dolioAnd instead use (a -> Set) predicates, and "Decidable p" in lieu of value-level booleans.03/09 06:47
dolioWell, they're useful when you really want to do fiddling with plain booleans.03/09 06:48
dolioBut they lose a lot of their uses from something like Haskell. Like, I might not use them in filter.03/09 06:49
dolioEven though filter doesn't use any of the extra fanciness.03/09 06:49
-!- ksf_ is now known as ksf03/09 07:15
Saizanis there a standard name for foo? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8988#a898803/09 08:43
dolioI'm sure it has a name in the libraries.03/09 08:56
dolioTest maybe.03/09 08:56
dolioOh, it's called T in the libraries.03/09 08:57
codolioIt's named T in the libraries, if that didn't get through.03/09 09:01
Saizan_that's the upparcase t rather than \top, right?03/09 09:03
codolioYes. \top is the unit type.03/09 09:04
codolioLike in your code.03/09 09:04
codolioExcept it's probably a record, for eta to work.03/09 09:05
Saizan_ah, there's a difference?03/09 09:08
codolioYeah. The type system knows that records satisfy eta laws. So, like, if you had pairs, then it'd know that "p = record { fst = fst p ; snd = snd p }".03/09 09:12
codolioWhich for the unit type means that it knows that every inhabitant is equal to "record {}" and it can fill it in automatically.03/09 09:13
codolioWhereas it won't automatically suply 'tt'.03/09 09:14
Saizan_mmh, i don't understand where that applies03/09 09:22
codolioWell, if you define, say, _<_ on Naturals recursively, where m < n = \top for appropriate situations...03/09 09:23
codolioThen if you have, like "_-_ : forall m n -> {n < m} -> Nat"03/09 09:23
codolioThen, you can write "5 - 4" without having to explicitly prove that 4 < 5.03/09 09:24
codolioWith the "data" version, you'd have to write "(5 - 4) {tt}" I think.03/09 09:25
Saizan_oh, i see03/09 09:28
Saizan_i wasn't thinking about function calls03/09 09:29
codolioYeah, you can write _ and have it filled in, too, but that's less exciting.03/09 09:30
-!- codolio is now known as dolio03/09 09:30
Saizan_after i've pattern matched "p x y" against "True", shouldn't (tt : so (p x y)) typecheck?03/09 11:42
Saizan_err03/09 11:42
Saizan_so = T there03/09 11:42
sharadaSaizan don't think so!03/09 11:42
Saizan_why?03/09 11:43
sharadaTrue is a type ? (not a constructor? .. agda will think it's a variable in a pattern match context)03/09 11:43
sharadaoh....03/09 11:43
Saizan_i guess i need to give more context :)03/09 11:43
sharadaI didn't notice you had 'so' there03/09 11:43
sharadaforget what I said, you are dead right03/09 11:43
Saizan_uhm, i wonder why agda doesn't accept it then03/09 11:44
sharadaaccept what?03/09 11:47
sharada(if you use with then no wonder it doesn't work .. they call it 'magic' with for a reason)03/09 11:47
Saizan_(ah..)03/09 11:48
sharadawhat is your code03/09 11:49
Saizan_uhm, it's quite messy but i'll paste it anyway :(03/09 11:51
Saizan_http://hpaste.org/fastcgi/hpaste.fcgi/view?id=8988#a8994 <- here it is03/09 11:52
Saizan_the above revision works though03/09 11:52
sharadas/foo/so/03/09 11:52
sharadaelim-pred works ?03/09 11:54
Saizan_yeah, it typechecks03/09 11:56
Saizan_though i find that i can't rewrite elem-trans using it because the False branch is using the fact that p a x = False03/09 11:57
Saizan_i could use _==_ i guess03/09 11:57
sharadamaybe I just don't have enough context but "so (elem P x xs) -> so (subset P xs ys) -> so (elem P x ys)" seems weird03/09 11:58
sharadajust beacuse these things are decidible - having then as booleans might still be awkard03/09 11:59
sharadayou could try to use instead that a proof of 'elem' is actually a path to that elemen in the list, and likewise subset explains how to take a subset03/09 11:59
Saizan_yeah, that might have been a better choice03/09 12:03
sharada(I can see that writing a program to factor a path through a subset proof might not be /that/ hard.. it's def. going to be longer than the two lines of code you have there though..)03/09 12:03
sharadahm I wonder if 'so' works a bit like Prop03/09 12:04
sharadaactually it doesn't but it would be possible to have a so in prop03/09 12:04
Saizan_elim-pred : {A C : Set} -> (P : A -> A -> Bool) -> (x y : A) -> (so (P x y) -> C) -> (so (not (P x y)) -> C) -> C <- this gets it working03/09 12:09
glguyIs something like this already in the library? (I'm using == from Relation.Binary.Core) eq-exts : ∀ { A B } { a b : A } (f : A -> B) -> a ≡ b -> f a ≡ f b03/09 17:36
glguyIs this congruence, perhaps?03/09 17:37
sharadaisn't it usually (f : A -> B) -> a ≡ b -> f a -> f b03/09 17:38
sharadafor rewriting03/09 17:38
sharadaand you instantiate f x = a = x,  prove the first with refl that gets you a = b03/09 17:38
sharadaf x = a ≡ x03/09 17:38
glguyI have no idea what it usually is :)03/09 17:39
glguyis that something that is already defined?03/09 17:41
glguyI was at least able to "simplify" it as: eq-exts : Congruential (_≡_)03/09 17:54
glguyeq-exts f refl = refl03/09 17:54
-!- byorgey_ is now known as byorgey03/09 22:57
--- Day changed Fri Sep 04 2009
-!- byorgey_ is now known as byorgey04/09 01:01
sharadawhat's the definition of canonical wrt. coinductives?04/09 12:55
sharadatail (repeat 1) is canoncial?04/09 12:55
--- Day changed Sat Sep 05 2009
-!- codolio is now known as dolio05/09 01:18
-!- codolio is now known as dolio05/09 12:13
-!- byorgey_ is now known as byorgey05/09 15:00
EnglishGenthello :)05/09 18:31
Saizan_hi05/09 18:35
EnglishGenthi Saizan_ :)05/09 18:36
* EnglishGent just taking a quick look at Agda05/09 18:38
EnglishGentI looked at Cayenne a while back & thought that interesting05/09 18:38
Saizan_never looked at cayenne myself, but agda is pretty fun and not that hard to grasp after haskell05/09 18:43
EnglishGentwell I ran into Augustuss recently - and mentioned I'd looked at Cayenne - and he suggested I look at Agda05/09 18:46
EnglishGentand I'm certainly happy to take advice from a name :)05/09 18:46
* EnglishGent is still learning Haskell - but I thought it couldnt hurt to take a peek05/09 18:47
EnglishGentI'm interested in type-systems generally :)05/09 18:47
EnglishGenthave you used it long?05/09 18:48
* EnglishGent does like the idea of a language that can be used both for programming & theorem proving05/09 18:48
* EnglishGent is trying very hard to teach himself a bunch of comp-sci ... it's hard going though05/09 18:49
EnglishGentI'm so grateful for irc! at least I'm not _totally_ alone05/09 18:49
sharadacool05/09 18:57
sharadaI like "language that can be used both for programming & theorem proving" too05/09 18:57
EnglishGenthi sharada :)05/09 18:59
sharadahi05/09 18:59
EnglishGentwhat's your background sharada? (just curious) :)05/09 19:00
sharadanone05/09 19:00
* EnglishGent is a programmer with an interest in better languages (amongst other interests!) :)05/09 19:01
sharadayeah05/09 19:01
sharadaI don't study this stuff formally05/09 19:01
Saizan_i've started using agda seriously only last week when i felt insecure about some functions in my code05/09 19:03
Saizan_it turns out i could prove their correctness, fortunately :)05/09 19:04
-!- Saizan_ is now known as Saizan05/09 19:04
EnglishGent:)05/09 19:04
EnglishGentif only more programmers thought that way05/09 19:05
EnglishGentso much code out there is _so_ bad :|05/09 19:05
* EnglishGent has been accused of wasting time thinking about 'theoretical problems' by management before... becuase I cared about the correctness of the code I was working on05/09 19:06
EnglishGent:|05/09 19:06
Saizan:\05/09 19:06
glguyIs there a trick to getting characters like \forall and \:: in aquamacs?05/09 19:07
Saizan"agda-mode setup" got the latex input working fine for me, but i'm on linux05/09 19:08
glguyyeah, it worked find on Linux for me, too05/09 19:08
glguyI get boxes instead of the actual font glyph for those symbols05/09 19:09
glguyin Aquamacs05/09 19:09
sharadamaybe better luck with Carbon Emacs05/09 19:09
glguyOK05/09 19:09
glguyI'll give that a shot then05/09 19:09
sharadaEnglishGent: have you got any particular dreams in that area (correct programs)05/09 19:34
copumpkinooh EnglishGent :o05/09 19:35
EnglishGenthi copumpkin :)05/09 19:35
EnglishGentdepends what you mean by dreasm - but yes I have a few sharada :)05/09 19:35
EnglishGentI think we could do _much_ better than the mainstream languages / tools we're using now05/09 19:35
sharadayeah of course05/09 19:37
EnglishGentI'd like to be able to talk about time/space complexities _within_ the language05/09 19:38
sharadathat sounds hard05/09 19:39
EnglishGentI agree - but Augustuss told me that Agda was looking at it :)05/09 19:39
sharadaI think that some people use monadic style and interepter that gives --> semantics (executable) and also --> time complexity05/09 19:39
sharadaso you can project out either way05/09 19:40
EnglishGentwell I know almost nothing about agda at the moment05/09 19:40
EnglishGentI'm still learning Haskell05/09 19:40
glguySo, C doesn't have polymorphic functions because its type system is too limited, and Haskell has polymorphic functions because its type system is too limited?05/09 19:40
EnglishGentbut I thought it couldnt hurt to take a look :)05/09 19:40
sharadahehe what glguy05/09 19:41
glguyI'm just reading through AgdaIntro.pdf05/09 19:42
glguyand they mention that Agda doesn't need polymorphic functions as you just pass the types in as parameters05/09 19:42
sharadaoh I get what you mean05/09 19:42
glguy(even if you've declared those parameters as implicit)05/09 19:42
copumpkinhas there been any talk of a hoogle for agda?05/09 19:43
glguyaoogle doesn't have such a nice ring to it05/09 19:44
glguyaahoo?05/09 19:44
copumpkinwell, obviously a different name, but functionality wise05/09 19:44
glguyaing!05/09 19:44
copumpkinit'd be great to be able to search for proofs05/09 19:44
glguy(I don't know the answer to your actual question)05/09 19:44
glguyIs there a level of types more "expressive" "powerful" (?) than the dependent types offered by agda?05/09 19:47
glguyonce you allow arbitrary functions in your types, have you hit the theoretical limit?05/09 19:47
sharadaglguy: well there is simple types, then polymorphci types, depedente types .. the cube05/09 19:48
sharadayou know this though..05/09 19:48
glguysharada: I'm aware of the lambda cube05/09 19:48
glguyI don't have it ingrained in my understanding05/09 19:48
glguyif that's what you are referring to05/09 19:48
sharadathat's as mucha bout the cube that matters05/09 19:49
sharadanext you can add inductive-recursive universes to get more strength05/09 19:49
sharadaI don't know what is beyond that05/09 19:49
glguysharada: unless you were being sarcastic, feel free to assume that I don't know much more than I've let on about dependent types and programming in Agda  :)05/09 19:49
sharada(Agda has induction recursion)05/09 19:49
sharadano I am not being sarcastic05/09 19:49
glguyok :)05/09 19:50
EnglishGentdont we hit a limit on model-theoretic power? when the type system becomes Turing complete?05/09 19:51
* EnglishGent doesnt understand how it can be more powerful that that05/09 19:51
EnglishGentthough of course you can add more proof theoretic power - and allow you to say things more compactly05/09 19:52
sharadaI think once it is Turing complete you have useless05/09 19:52
sharadaand it's rubbish like an inconsistent logic05/09 19:52
* EnglishGent doesnt really understand this either - but is trying hard to understand it all05/09 19:52
EnglishGentI thought the problem was simply that type-checking might then never terminate05/09 19:52
sharadayeah that sucks05/09 19:52
* EnglishGent fairly certain their are languages with Turing complete type systems - Qi's is - and Cayennes is I think05/09 19:53
sharadait would be fine for something like haskell but not a proof system05/09 19:53
sharadasure if you just want to hack05/09 19:53
EnglishGentwell like you - I like the idea of a language that can be used for both theorem proving & programming05/09 19:54
EnglishGentbut I'm a) partly trying to contribute what little I know to answering glguy's question05/09 19:54
EnglishGentand b) trying to understand things better myself05/09 19:54
* EnglishGent doesnt see why non-termination in _principle_ has to be a problem - as long as _in practice_ checking terminates05/09 19:55
EnglishGentthe existence of pathalogical cases doesnt seem enough to exclude such systems from use (to me)05/09 19:55
EnglishGentunless in practice such cases crop up often05/09 19:55
EnglishGent:)05/09 19:56
sharadaEnglishGent: on the converse, what we have now is:  theoretically does terminate but may not (something might take a million million years and as many MB of RAM)05/09 19:56
EnglishGentright! so it's not as strong a gurantee as it might seem anyway05/09 19:57
Saizanthe problem is that you've to check termination anyway before you accept a proof for an inductive property05/09 20:05
glguyCan someone explain why in in this definition, we have \forall {xs} rather than {xs : List A}? data _∈_ {A : Set}(x : A) : List A → Set where05/09 20:21
glguy  hd : ∀ {xs} → x ∈ (x ∷ xs)05/09 20:21
sharadathe : List A bit just gets inferred05/09 20:22
glguyDoes Agda simply infer the type for xs?05/09 20:22
glguyOK05/09 20:22
sharadayes05/09 20:22
glguyso the \forall tells agda to try to infer i nthis case?05/09 20:23
sharadano05/09 20:23
sharadaremember,05/09 20:23
sharadaA -> B05/09 20:23
sharadais like05/09 20:23
sharadaforall (x : A), B05/09 20:23
glguySo it is just a syntactic difference then05/09 20:24
sharada(except well in agda you don't write the comma, it's a -> again, confusingly)05/09 20:24
sharadayeah -> is just a shorthand05/09 20:24
* glguy wants mixfix ported to Haskell :)05/09 20:26
* sharada thinks mixfix SUCKS :P05/09 20:28
sharadaNotation in Coq is a lot better05/09 20:28
sharadait's annoying to me not being able to change the order in agda05/09 20:28
glguyI guess I haven't played with Coq's notation05/09 20:28
glguyI just like that things like "if_then_else_" don't need to be built in05/09 20:28
sharada<ridiculous example incoming>  you can't do things like   x given b   with (b : A)  (x : f b)05/09 20:31
sharadayou must change it around like  b nevig x,  which I don't like that much05/09 20:31
sharada(it's kind of rare this comes up, to be fair)05/09 20:31
-!- byorgey_ is now known as byorgey05/09 20:43
-!- byorgey_ is now known as byorgey05/09 21:02
-!- EnglishGent is now known as EnglishGent^afk05/09 22:27
--- Day changed Sun Sep 06 2009
glguyI've got a goal of "Goal: x \in  (filt p (x :: .xs) | p x)" but I don't know how to express that I want to turn: filt p (x :: .xs) | px  into x :: filt p .xs06/09 01:39
glguyat which point I believe my constructor "hd :   {xs} -> x \in (x :: xs)"06/09 01:39
glguywould apply06/09 01:39
glguyWhat technique do you use here? (do I need to provide more context?)06/09 01:40
-!- codolio is now known as dolio06/09 02:14
dolioglguy: Match against px?06/09 02:21
glguyhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a910306/09 02:31
dolioOh, okay.06/09 02:38
glguyif I try casing on "el"06/09 02:39
glguythen I get the goal I mentioned before06/09 02:39
glguythis is out of the AgdaIntro.pdf06/09 02:39
dolioHave you tried going into the agda menu and selecting the items about viewing the goal? Sometimes the default display doesn't normalize the goal type all the way.06/09 02:40
glguyit might be displaying it wrong06/09 02:41
glguybut it isn't lettme me use my "hd" or "tl" constructors06/09 02:41
glguydoes the display not normalizing also mean that that wouldn't work either?06/09 02:41
dolioNo.06/09 02:41
glguyMight my filter definition be at fault? filt : {A : Set} → (A → Bool) → List A → List A06/09 02:42
glguyfilt p [] = []06/09 02:43
glguyfilt p (x ∷ xs) with p x06/09 02:43
glguy... | true = x ∷ filt p xs06/09 02:43
glguy... | false = filt p xs06/09 02:43
dolioThat looks fine to me.06/09 02:43
dolioOh, wait, I know what the problem is.06/09 02:43
glguy| p x   is different than   | p x == true?06/09 02:44
dolioYou're doing stuff with 'p x' where x is the element you're trying to prove is in the output of filter.06/09 02:44
dolioThat's only useful when you know that the element you're looking for is at the head of the list.06/09 02:45
glguybut after casing on "el", I do know that06/09 02:45
dolioHmm...06/09 02:45
dolioAre you able to handle the case where it's not at the head of the list?06/09 02:47
glguywell... no06/09 02:47
dolioBecause you're going to have to do a 'with p y' for the head of the list in that case.06/09 02:47
dolioWhere y is the head.06/09 02:47
dolioAnd you don't need to know about 'p x' at all in that case.06/09 02:48
glguyalright06/09 02:48
glguysounds like I have some thinking to do then06/09 02:48
dolioSo I'd recommend matching on xs and/or el first, and p x only when you know it's at the head of the list.06/09 02:48
glguyI'll probably have to start with printing xs into schope06/09 02:49
glguyscope06/09 02:49
glguysince it was implicit earlier06/09 02:49
glguyWhat you said06/09 02:49
dolioBut I'm not sure why you wouldn't be able to fill that case.06/09 02:49
dolioYou can actually match against implicit arguments by surrounding them with {}.06/09 02:49
glguyI just meant that I'd have to add them06/09 02:50
glguythis problem is pushing agda's emacs mode beyond its capabilities with C-c C-c06/09 02:52
glguyhuraay06/09 02:58
glguyI got it through06/09 02:58
glguyit typechecks, is it *must* do something interesting :)06/09 03:02
dolio:)06/09 03:02
dolioAgda's not bug-free.06/09 03:03
dolioNot too long ago you could prove that all functions are injective.06/09 03:03
dolioWhich is pretty egregious.06/09 03:03
copumpkinor maybe it's just true and all of mathematics is wrong!06/09 03:06
dolioEverything is equal!06/09 03:06
dolioAll sets have one element.06/09 03:06
dolioZero or one, I guess.06/09 03:07
glguythis is a huge discovery06/09 03:07
dolioIt might make the ultrafinitists happy. :)06/09 03:07
dolioThe largest number is 1.06/09 03:08
doliohttp://www.youtube.com/watch?v=f3ek85X2uOE06/09 03:08
glguydolio: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a910406/09 03:15
-!- ksf_ is now known as ksf06/09 03:16
dolioI don't think you should need to use inspect.06/09 03:16
dolioI proved it here without it.06/09 03:17
glguyI was thinking that that might be the case06/09 03:17
glguywhen I saw _06/09 03:17
glguyin the second element of "it"06/09 03:17
glguyyeah, I was able to drop the inspects06/09 03:19
* glguy is still watching "Biggest Number"06/09 03:19
glguydolio: did yours look like this? http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9101#a910506/09 03:26
dolioYeah, that's about what I have.06/09 03:26
dolioFunnily enough, those withs are both the same, since x = y in the hd case. So there might be a way to do with only one.06/09 03:28
dolioI don't think you can get away with less than 4 cases, though.06/09 03:28
* glguy remembers the ... syntax06/09 03:30
glguyis "with" or "if_then_else_" more common in agda code?06/09 03:31
glguyhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9102#a910606/09 03:32
glguyis there any way to simplify that top case?06/09 03:32
dolioWell, as I remarked here a few days back, I tend to not use booleans.06/09 03:33
dolioBecause Set valued predicates are more generally useful.06/09 03:33
glguyWhat would you do instead, in this situation?06/09 03:33
dolioAnd then 'Decidable p' gets you back boolean-like predicates.06/09 03:33
glguyI'm only using them at this point because I'm following the exercises06/09 03:34
dolioYeah, that's fine.06/09 03:34
dolioI don't think if_then_else_ sees a whole lot of use, though. It's kind of like the mixfix version of Haskell's 4-line quicksort.06/09 03:34
glguyheh06/09 03:35
glguyThat is a *glowing* endorsement06/09 03:35
dolioThat's only because Agda has dependent types, though.06/09 03:35
copumpkinsets rule, booleans drool06/09 03:36
dolioThe equational reasoning stuff is probably a better example of why mixfix operators are awesome.06/09 03:42
dolioSince they make code that would be terrible to write look nice.06/09 03:42
copumpkinI like that begin thing06/09 03:42
copumpkinand the square06/09 03:42
copumpkin:P06/09 03:42
dolioI did some similar stuff when I was encoding from theorems from a book on mathematical logic recently.06/09 03:43
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=823406/09 03:44
glguyIt is time for pygments to get Agda highlighting support06/09 03:45
glguyit just needs to know how to run agda, I suppose06/09 03:46
-!- pumpkin is now known as copumpkin06/09 06:05
Saizanthere's no concept of installing a lib for agda yet, is there?06/09 15:50
ccasinI don't know of any, except that you'll have to tell the emacs mode where you put it06/09 15:51
ccasinas in, to get the stdlib to work, I had to make my .emacs set the "agda2-include-dirs" variable06/09 15:52
Saizanyeah, i've done that with M-x customize06/09 16:12
Saizanit took a while to load Everything.agda :)06/09 16:12
ccasinYeah, luckily agda caches some information on disk so it's quicker the next time :)06/09 16:13
Saizanah, i as wondering that06/09 16:14
Saizan*was06/09 16:14
Saizanwhere?06/09 16:14
ccasinI think in dotfiles in the directories where the .agda files live06/09 16:17
Saizanah, yeah06/09 16:18
glguyDoes Coq assume that you can compare any two elements of the same set for equality? Does agda have this same property?06/09 23:50
glguyIs "{A : Set} -> A -> A -> Set" possible? (where the two Sets would be True and False)06/09 23:53
-!- Irssi: #agda: Total of 15 nicks [0 ops, 0 halfops, 0 voices, 15 normal]06/09 23:53
--- Day changed Mon Sep 07 2009
glguyAh, I worked out it07/09 00:08
kmcwhat is the coolest thing written in agda?07/09 05:15
copumpkinhmm, coolest?07/09 05:19
kmcmost impressive, say07/09 05:24
kmcalso, are there good exercises beyond http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf07/09 05:25
copumpkinthis is somewhat related to those exercises, but there's a few differences: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.TypesSummerSchool200707/09 05:27
kmcso the head of a datatype declaration looks like "data [name] [arguments] : [type] where"... what changes when i move arguments across the colon?07/09 05:32
kmci.e., what is the difference between "data Foo A : Set" and "data Foo : A -> Set"07/09 05:34
copumpkinI was wondering that too... the pdf you linked to had a minor chunk about it, giving a definition for both07/09 05:35
copumpkinbut not actually explaining why the distinction mattered07/09 05:35
kmcyeah, it did seem to imply it matters07/09 05:35
kmc"There is a distinction between parameters and indices of a datatype. We say that Vec is parameterised by a type A and indexed over natural numbers."07/09 05:36
copumpkinon the coolest thing, I'm not sure many people have written any major programs/proofs in agda yet, most people seem to experiment with proving statements to experiment with it (the largest actual body of agda I know is the standard library)07/09 05:36
copumpkinyeah07/09 05:36
kmci thought the provably-correct lambda-calculus type inference thing from that pdf was nice07/09 05:37
glguyEven though "NoDup A Respects Permutation" parses correctly, would it be more acceptable to write "(NoDup A) Respects Permutation"?07/09 09:00
edwinbThe compiler may not need the brackets, but I do )07/09 09:01
-!- rocketman is now known as soupdragon07/09 09:58
* glguy finishes http://web.cecs.pdx.edu/~apt/cs510coq/midterm.v in Agda :)07/09 10:02
soupdragonhey cool lets see?07/09 10:04
soupdragonanything to do with Permutation is usually really arduous07/09 10:05
glguyOK, I'll post it in a second ( need to do syntax highlighting )07/09 10:05
glguybut you can only read it if you understand that I haven't go through at all to clean it up07/09 10:06
dolioThat's an easy permutation.07/09 10:06
dolioIt's got transitivity for free.07/09 10:06
dolioAlthough it's rather odd that it has you proving transitivity later.07/09 10:07
glguyhttp://www.galois.com/~emertens/midterm.agda.html07/09 10:07
glguydolio: yeah, I actually skipped that since it was just a renaming07/09 10:08
dolioProving transitivity without an axiom is way too hard for an exam, though.07/09 10:12
glguyIn keeping with the exam, I defined \in as follows, but is it more appropriate to define a new Set for this relation?07/09 10:54
glguy_∈_ : {A : Set} → A → List A → Set07/09 10:54
glguye ∈ [] = ⊥07/09 10:54
glguye ∈ (y ∷ y') = (e ≡ y) ∨ (e ∈ y')07/09 10:54
glguyrather than building it from the more general _∨_ Set?07/09 10:55
glguyAs the exercises in AgdaIntro.pdf did07/09 10:55
Saizani wonder, i got exposed to the way it's done in Data.List.Any first07/09 11:09
-!- EnglishGent is now known as EnglishGent^afk07/09 13:38
dolioI've heard it mentioned before that dealing with inductive families isn't as nice in Coq as it could be, so they tend to prefer recursive definitions of types like that \in.07/09 14:14
dolioWhereas in Agda, the inductive definition is often nicer to work with.07/09 14:15
dolioI don't know the details of what's wrong with working with inductive families in Coq, though.07/09 14:16
edwinbthe main problem is that it doesn't have dependent pattern matching07/09 14:23
edwinbso if you have a vector and its length, and match on the vector...07/09 14:23
edwinbyou don't know anything about its length07/09 14:23
edwinbwhich makes proving lots of things very hard07/09 14:23
dolioAh.07/09 14:23
Saizanand using a recursive def. like \in above instead works better?07/09 14:25
dolioWhen you use a recursive definition of vectors, you have to match on the size first.07/09 14:25
dolioWhich isn't as big a deal when you have to do that anyway, I guess.07/09 14:26
edwinbyou then have to prove that the other cases are impossible or it'll complain that your definition isn't total07/09 14:26
edwinbwhich is annoying, at best07/09 14:27
edwinbbut then when things start being indexed by vectors, and so on...07/09 14:27
dolioIs dependent pattern matching what you need axiom K for?07/09 14:29
edwinbas I understand it, it helps implement dependent pattern matching07/09 14:33
edwinbif you want to implement it via elimination rules rather than directly07/09 14:34
edwinbI prefer it when that sort of thing is done by Anybody But Me07/09 14:34
dolio:)07/09 14:34
LaneyProgram makes such things feasible in Coq07/09 14:39
-!- copumpkin is now known as sunglassedcopump07/09 17:00
-!- sunglassedcopump is now known as copumpkin07/09 17:09
-!- EnglishGent^afk is now known as EnglishGent07/09 20:13
--- Day changed Tue Sep 08 2009
kmcso when can i expect to read Real World Agda08/09 00:15
kmcand how do i become a master before it takes over the world08/09 00:16
kmc(haskell already being well on the way, i want to get ahead of the curve)08/09 00:16
copumpkinhah08/09 00:17
dolioYou can't wait for Real World Agda if you want to stay ahead of the curve. :)08/09 00:19
kmcthat's true08/09 00:19
kmci'll need to learn Alternate Universe Agda first08/09 00:19
copumpkinhow well does compiled agda perform? I remember looking at a paper on compiling agda to haskell and how painful that was08/09 00:20
dolioI've never tried it, myself.08/09 00:20
Laneypeople run programs?08/09 00:20
dolioMost langauges like Agda aren't known for being particularly speedy, as far as I know.08/09 00:21
kmcshouldn't a bunch of stuff get erased in compilation?08/09 00:21
dolioAlthough Agda has a lot of hooks you could use to expose efficient Haskell stuff, I suppose.08/09 00:22
dolioOr, not a lot. But some.08/09 00:23
dolioHowever, extracting dependently typed stuff into a language like haskell can produce code with a lot of unsafeCoercing and such.08/09 00:26
dolioSo if GHC gets more conservative in optimization when it sees that kind of thing, that could be problematic.08/09 00:27
dolioAlthough I don't think it does.08/09 00:27
dolio(It's just dangerous.)08/09 00:27
dolioCode written to be nice to prove things about isn't necessarily the most amenable to optimization, either.08/09 00:28
glguyIs there a way in an arbitrary type to convince agda that (xs ++ []) == xs?08/09 06:31
glguyor do I need a new lemma every time08/09 06:32
glguyin Coq I think you would give a "rewrite" directive08/09 06:33
stevanhi08/09 16:22
stevankmc: here are some more exercises: http://www.cs.chalmers.se/Cs/Education/Courses/types/   http://www.cs.chalmers.se/~peterd/kurser/tt03/08/09 16:27
-!- Saizan_ is now known as Saizan08/09 17:19
glguyWhere can I read about the specifics of what "Prop" is?08/09 17:34
dolioI haven't seen a lot of documentation on it. It's not the best fleshed out area of Agda.08/09 17:54
dolioI think Prop < Set in the hierarchy.08/09 17:54
dolioAnd there's a flag (--proof-irrelevance maybe) that enforces the condition that any t : Prop has at most one inhabitant.08/09 17:55
elliotttwhy is that condition enforced?08/09 17:55
dolioBut I think Agda overall lacks certain conditions to make proof irrelevance properly hold, even then.08/09 17:55
dolioBecause proof irrelevance depends on all proofs of t being equal.08/09 17:56
dolioAnd t having 0 or 1 inhabitants would seem to be a necessary condition for that.08/09 17:57
elliotttah, is ee08/09 18:04
elliotttso, multiple constructors would mean that you could have more than one way of constructing the proof08/09 18:04
sharadayeah I don't think agda has fully implemented prop yet08/09 18:05
sharadathe idea is that any p, q : P, with P : prop, then p and q are convertible08/09 18:05
sharadathat gives you K, inj_t2, JMeq and all these lovely things08/09 18:05
dolioConor McBride has talked on the Agda list about how proof irrelevance also requires a certain laziness to evaluation that Agda lacks.08/09 18:06
sharada(Coq doesn't have this either)08/09 18:06
dolioAnd I imagine it still lacks it, since I haven't heard otherwise since he mentioned it.08/09 18:06
dolioOf course, I think the idea in overview is to make sure proofs have no computational content, and thus you can erase them without affecting the results of your computation.08/09 18:24
dolioIf you have two or more constructors, you can do case distinction, which affects the computation, so disallowing that is one way to get where you want to go.08/09 18:25
dolioYou could also, I suppose, allow many constructors, but provide no way to distinguish between them, like a quotient.08/09 18:25
dolioBut in my limited experience with type theories like that, even that is modeled like a primitive type constructor that produces a type with one inhabitant.08/09 18:26
dolioLike 'Squash T' has one inhabitant if T is inhabited by one or more values.08/09 18:27
sharadaisn't that a quotient?08/09 18:28
sharadaI found a monadic modality, that lets you implement proof irr.08/09 18:28
dolioYeah. But the paper I'm thinking of takes Squash as primitive and builds up more interesting quotients using it.08/09 18:28
dolioYeah, Prf or whatever?08/09 18:30
dolioSquash is probably the same thing.08/09 18:30
sharadayeah08/09 18:30
dolioAt least, I'd expect Squash to be monadic.08/09 18:31
dolioThe paper got a little over my head.08/09 18:31
glguyIs there some general way to rewrite (xs ++ []) -> xs08/09 18:31
glguyin types08/09 18:31
glguyother than defining a new lemma for every specific instance?08/09 18:32
dolioYou should be able to prove forall xs -> (xs ++ []) == xs.08/09 18:32
sharadaglguy, remember that cong lemma?08/09 18:32
sharadause that with f instantiated to whatever08/09 18:32
glguyoh!08/09 18:33
glguysharada: everything I needed was defined in Relation.Binary.PropositionalEquality08/09 21:54
glguysubst, cong, sym08/09 21:54
--- Day changed Wed Sep 09 2009
-!- codolio is now known as dolio09/09 14:00
glguysay I wanted to generate a list of the Fibonacci sequence up to some upper limit 'n'. I could use "unfoldr" and 'n' as my measure to ensure termination. "Obviously" there are fewer than or equal to n elements (starting at 1,2,3,5...)09/09 23:03
glguybut is that typically something you wouldn't want to prove directly09/09 23:03
glguy(that your measure is always sufficient)09/09 23:03
glguyif you could prove that would you even need the measure?09/09 23:04
--- Day changed Thu Sep 10 2009
dolioI think one thing you could do is prove that, n - fibs_i < n - fibs_i+1, and then use some sort of well-founded induction to define the list.10/09 00:10
dolioWait, I have that backwards.10/09 00:11
dolioAnyhow, you prove that the difference shrinks on every recursive call, thus it eventually terminates, but don't specify "use up to n iterations" which just happens to be big enough.10/09 00:13
dolioUsing unfold with a large enough n is, of course, easier. :)10/09 00:13
glguycould the definition of unfold be modified to insist that your measure never run out early10/09 00:16
glguyrather than handling that case by silently truncating10/09 00:16
glguywell, I'm sure it could be10/09 00:16
glguywould that be very useful?10/09 00:17
dolioI don't know. It'd probably end up being like the above well-founded induction.10/09 00:18
glguyok10/09 00:19
dolioI'm not really sure how to specify "n is big enough" easily.10/09 00:20
sharadayou can write fib : nat -> nat and fibs : (n : nat) -> Vector nat n10/09 00:20
sharadano Wf or proofs or anything10/09 00:21
dolioThat's "first n fibs", though, not "fibs less than n".10/09 00:21
sharadaoh10/09 00:21
sharadaso you want (n : nat) -> fibs up to n?10/09 00:22
glguyyes10/09 00:22
glguyprimarily to understand how you would go about doing it well10/09 00:23
sharadaI would use Wf,10/09 00:23
sharadax "<" y := x > y /\ x < n10/09 00:24
sharadaor perhaps x "<" y := n - x > y10/09 00:24
sharada(s/>/</ ***)10/09 00:24
glguysharada: the sort of stuff in Induction.Nat?10/09 00:24
sharadaI don't use the libs10/09 00:25
dolioWell-founded induction looks something like (\all y -> (\all z -> z < y -> P z) -> P y) -> Acc _<_ x -> P x.10/09 00:29
glguyIt seems unfortunate that functions have to be reimplemented completely to have them operate on different sorts (assuming Set, Set1, Set2... are sorts)10/09 03:37
dolioThat can be rectified with universe polymorphism, but obviously Agda doesn't have it yet.10/09 03:53
dolioYou can also use the --type-in-type flag if you don't mind being able to write paradoxes.10/09 03:54
glguy:q10/09 03:58
dolioWell, anyhow, here: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9241#a924110/09 04:31
dolioThat's the development of a well-founded unfold.10/09 04:31
dolioUnfortunately, the two well-founded relations I've come up with that'd admit the fibonaccis are kind of tedious to work with in some way.10/09 04:32
dolioSo I'm going to take a break and may or may not come back to it.10/09 04:33
dolioAs you can see, the idea is that the step function takes a seed s_0, and produces a list element, plus a new seed s_1 that is closer to being complete, according to the relation.10/09 04:35
glguydolio: thanks for the paste10/09 05:16
-!- ToRA_ is now known as ToRA10/09 14:46
-!- EnglishGent_ is now known as EnglishGent^afk10/09 14:54
copumpkinnext project, a verified haskell compiler written in agda! ;)10/09 16:56
sharadathat's a joke?10/09 17:01
Saizan_copumpkin: you've a lot of trust in the agda one :)10/09 17:06
copumpkinyep!10/09 17:15
dolioI'm not sure that's entirely justified.10/09 17:19
Saizan_is there an example of proving the monad laws somewhere?10/09 18:45
-!- Saizan_ is now known as Saizan10/09 18:45
sharadafor which monad?10/09 18:46
SaizanState10/09 18:46
Saizani'm not sure what's an appropriate equality, in particular10/09 18:49
sharadajust = I think10/09 18:51
sharada(Agda has eta conversion)10/09 18:52
glguySaizan: example for Continuations http://muaddibspace.blogspot.com/2009/02/agda-supports-eta-cont-is-monad.html10/09 19:00
Saizanglguy: thanks10/09 19:46
Saizanthough i'm stuck: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9279#a927910/09 19:46
Saizani can't access the x mentioned in the error, right?10/09 19:46
glguySaizan: I actually tried doing this exact thing with State last night10/09 19:48
glguyand I got stuck on that same one10/09 19:48
sharadawhat happens if you turn Σ into a record instead?10/09 19:49
Saizanooh, right10/09 19:49
glguysharada: What is the difference in a data vs a record in this case?10/09 19:51
Saizanif i remembered the syntax for records i could tell you, but more or less its that the typechecker knows that "r = record { first = first r, second = second r }"10/09 19:55
-!- codolio is now known as dolio10/09 19:58
Saizanyeah, it works10/09 20:00
glguyis there actually a difference or is it just that the type-checker likes records better?10/09 20:07
dolioRecords have eta laws, data doesn't.10/09 20:07
-!- EnglishGent^afk is now known as EnglishGent10/09 20:08
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9279#a9281 <- not much to do10/09 20:09
dolioEquality proofs of functions typically turn out to be either trivial or impossible, in my experience.10/09 20:18
dolioIn the absense of extensionality, of course.10/09 20:18
dolioFor instance, as far as I can tell, it's impossible to prove (\i j k -> i + (j + k)) == (\i j k -> (i + j) + k) intensionally, where i, j and k are inductively defined, Peano naturals.10/09 20:31
dolioOn the other hand, for Church numerals, it's trivial (==-refl), as they both normalize to (\i j k f x -> i f (j f (k f x))).10/09 20:32
-!- EnglishGent is now known as EnglishGent^afk10/09 21:19
--- Day changed Fri Sep 11 2009
Saizani wonder why we can't use module syntax to instantiate a record, bad heritage from haskell?11/09 00:04
dolioModules aren't precisely first-class, as far as I can tell.11/09 01:05
dolioDespite there being a link between records and modules.11/09 01:05
Saizaneven then allowing where and arguments on the LHS of = doesn't look problematic11/09 01:11
dolioYeah, constructing records can be a bit inconvenient.11/09 01:13
dolioI tend to use a where clause on the definition, which just results in stuff like "foo = record { bar = bar' ; baz = baz' ; ... } where bar' = ... ; baz' = ..."11/09 01:14
Saizanwhat do you think of defining right identity for monoid (a , _+_ , zero) like this:11/09 01:14
Saizan right-id' : (λ (x : a) -> x + zero) ≡ (λ x -> x)11/09 01:15
Saizanso i can use it with cong to prove equality of functions11/09 01:15
Saizanis there a better way?11/09 01:15
Saizandolio: ah, yeah, that style is doable but tedious11/09 01:16
dolioI don't know. What about \x y -> x + zero vs \x y -> x?11/09 01:17
dolioI don't think you get that from the single-parameter variant.11/09 01:17
dolioSo I think that's rather a losing battle.11/09 01:17
Saizanmh, i think you do11/09 01:18
dolioI don't think you even get \y x -> ...11/09 01:19
Saizan  foo : (λ (x y : m) -> x + zero) ≡ (λ x y -> x)11/09 01:20
Saizan  foo = cong (λ f x y -> f x) right-id'11/09 01:20
Saizanthat typechecks11/09 01:21
dolioHmm...11/09 01:21
Saizani've given y the type m for convenience11/09 01:21
Saizani need this because i've a weird hybrid between state and writer to prove a monad11/09 01:23
dolioOh, of course you can do \y x -> ..., since you have essentially e == e' and need const e = const e'.11/09 01:49
Saizanright11/09 01:49
dolioAnd I guess the \x y case is const . e == const . e'.11/09 01:50
dolioAlthough I'm finding it hard to wrap my brain around what exactly is happening with cong in that case.11/09 01:50
Saizannot sure, it's like f is both (+ zero) and id at once11/09 01:51
dolioOh, I guess it's \e x -> const (e x) is taking \x -> x (+ zero) to \x y -> x (+ zero).11/09 01:52
dolioClearly these evil lambda expressions are getting in the way of my understanding simple equational reasoning. We need to move Agda to a concatenative syntax. :)11/09 01:53
Saizaneheh :)11/09 01:54
Saizanit'd be easier to see that we're wrapping a term around a function, i guess :)11/09 01:54
-!- codolio is now known as dolio11/09 01:55
dolioI thought for a few minutes there I might have been wrong about being able to prove (\i j k -> i + (j + k)) == (\i j k -> (i + j) + k) from forall i j k -> i + (j + k) == (i + j) + k.11/09 01:57
dolioBut that's a different case.11/09 01:57
Saizanthat requires an extensionality axiom i guess11/09 01:57
dolioYeah.11/09 01:57
Saizanthough that means that defining associativity like the former makes it impossible to prove for some cases where you can prove the latter?11/09 02:00
dolioYeah, I don't know how to prove the former in the first place, off hand.11/09 02:02
dolioAre you able to prove (\x -> x + zero) == (\x -> x) for your monoid?11/09 02:02
Saizani don't have any particular monoid for now, so i'm fine :)11/09 02:03
dolioHeh.11/09 02:03
dolioFor instance, I don't know if it's possible to prove that for addition of naturals without proving \all x -> x + zero == x and using extensionality.11/09 02:03
dolioI guess what you're doing is taking a pre-extensionalized version of identity/associativity as your definition thereof.11/09 02:05
Saizani guess so, i've just pushed the problem further behind11/09 02:06
Saizanat this point it'd be nicer to just prove the extensional version of my equality and use the standard formulation of the properties11/09 02:11
dolioYou can assume extensionality as a postulate, but I'm not sure if that has negative effects or not.11/09 02:12
dolioYou can, of course, define a datatype that models extensional equality, but it doesn't get you the sort of magic substitutivity that the usual equality gets you.11/09 02:13
dolioAt least, I don't think it does.11/09 02:14
dolioI haven't played much with such types.11/09 02:14
-!- codolio is now known as dolio11/09 03:55
-!- codolio is now known as dolio11/09 05:02
-!- dolio is now known as codolio11/09 05:02
-!- codolio is now known as dolio11/09 05:03
-!- kssreeram_ is now known as kssreeram11/09 05:52
-!- kssreeram_ is now known as kssreeram11/09 06:19
-!- ksf_ is now known as ksf11/09 10:03
Saizan_you can't pattern match on records, right?11/09 13:35
-!- byorgey_ is now known as byorgey11/09 15:12
--- Day changed Sat Sep 12 2009
ranhaHello. Is here a channel concerning Programming-Language Agda?12/09 12:43
--- Day changed Sun Sep 13 2009
copumpkinwhat does it mean when emacs highlights some of my stuff yellow?13/09 03:02
dolioIt has unsolvable metavariables.13/09 03:05
copumpkinoh no13/09 03:05
dolioYou need to fill in some implicit parameters.13/09 03:05
dolioYou can figure out which ones by putting in {_}. It'll highlight the unsolvable ones in yellow instead of the overall function.13/09 03:06
copumpkinit's been highlighting individual variables in my functions13/09 03:06
dolioWell then those presumably take implicit parameters that it can't figure out.13/09 03:07
copumpkinaha13/09 03:08
copumpkinI think that's it13/09 03:08
dolioSometimes it can't figure things out that I feel like it should be able to.13/09 03:09
dolioBut I've never gotten through the paper on it, so I don't know how it works.13/09 03:09
copumpkinyeah, this feels like it should be able to figure it out13/09 03:10
copumpkinlol, still got some yellow with no implicit arguments13/09 03:19
copumpkinoh, got rid of it13/09 03:19
copumpkinfoldr :  ∀ {a} (p : ℕ → Set) {m} → (∀ {n} → a → p n → p (1 + n)) → p 0 → Vec a m → p m13/09 03:24
copumpkinfor some reason it can't deal with p being implicit13/09 03:25
copumpkincan I not use (->) or \r in my functions?13/09 03:28
copumpkinoh I can, the error was elsewhere13/09 03:29
copumpkinfunction : (n : ℕ) → (a : Set) → (b : Set) → Set13/09 03:35
copumpkinfor some reason it's highlighting the whole thing in yellow, and I have no implicit parameters at all13/09 03:35
dolioHighlighting it where?13/09 03:37
copumpkinthat line I just pasted, it has the obvious definition13/09 03:38
copumpkinhttp://snapplr.com/wg8413/09 03:38
dolioWell, that's weird.13/09 03:39
copumpkinthe funny thing is, I could've sworn it accepted it with no yellow a little while ago13/09 03:39
copumpkinthen I added some other unrelated stuff and it turned yellow13/09 03:39
copumpkinhah yeah13/09 03:40
copumpkinI copied it and pasted it13/09 03:40
copumpkinand it stopped being yellow :o13/09 03:40
copumpkinobviously after reloading13/09 03:40
dolioIt's not yellow here.13/09 03:41
copumpkinyeah, it isn't yellow here anymore either13/09 03:41
copumpkinmust've just been a random fluke13/09 03:41
copumpkinI must say, it is pretty awesome to be able to write things like that without jumping through hoops13/09 03:43
copumpkinI guess it isn't that hard to write that in haskell either with type families, but this is nicer :P13/09 03:43
dolioIt's more convenient.13/09 03:43
copumpkinhrm13/09 03:51
copumpkinVecFunction-function : ∀ {n a b} → (Vec a n → b) → function n a b13/09 03:51
dolioThere's a fairly large class of stuff you can't do yet with type families, too, because their termination conditions are more restrictive than structural recursion.13/09 03:52
copumpkinit's not letting me "pick off" individual arguments to curry them from that function n a b13/09 03:52
dolioAt least, type families without undecidable instances.13/09 03:52
copumpkinah yeah13/09 03:52
dolioWhat's your definition. I've got one here.13/09 03:57
copumpkinwell I just wrote VecFunction-function f a = ? and it complained that I gave too many arguments to a function type13/09 03:59
dolioAh. Yeah. You can't put the a on the left side for some reason.13/09 03:59
copumpkinah, I got it with a where block13/09 04:06
copumpkinnow all I have is an off-by-one error I think13/09 04:06
doliov-curry {suc n} f = λ x → v-curry {n} (λ xs -> f (x :: xs))13/09 04:06
copumpkinoh that's so much nicer :P13/09 04:06
copumpkinI forgot about lambda13/09 04:07
dolio:)13/09 04:07
* copumpkin renames his shitty names13/09 04:08
copumpkinwhat's the slash code for lambda?13/09 04:11
dolio\lambda13/09 04:11
copumpkinoh, I just got scared away by the left arrow appearing first13/09 04:12
dolioMight get there with \lam, I'm not exactly sure.13/09 04:12
dolioI don't know what else that would match.13/09 04:12
copumpkin\l13/09 04:12
copumpkingives me a left arrow13/09 04:12
copumpkinlam doesn't appear to work13/09 04:13
copumpkinhah, http://snapplr.com/aphc again13/09 04:13
dolioYeah, needs the whole word.13/09 04:13
copumpkinmust be some odd transient bug13/09 04:13
dolioWhatever version of agda you have is crazy.13/09 04:14
copumpkin2.2.413/09 04:14
dolioI've got 2.2.5. Take that!13/09 04:14
copumpkinooh, that burns13/09 04:15
dolioHave you used the compiler?13/09 04:20
dolioMAlonzo?13/09 04:20
copumpkinonce I think13/09 04:20
copumpkinunless there's more than one compiler13/09 04:21
copumpkinI still have a hole in my code so it's refusing to compile it right now13/09 04:21
copumpkinis there any way to use list literals in agda? would we define a _,_] operator and a [_ one?13/09 04:26
copumpkinlist literals in the haskell sense13/09 04:26
copumpkinoh wait, that wouldn't work13/09 04:26
dolioYou could define _] a = a :: [], _,_ a b = a :: b, [_ l = l13/09 04:28
dolioWith appropriate precedence.13/09 04:28
copumpkinyeah13/09 04:29
copumpkinseems like that would be quite nice13/09 04:29
copumpkinexcept for the ability to use those separately13/09 04:29
dolioConflicts with _,_ as dependent sum, too.13/09 04:30
copumpkinboo13/09 04:31
copumpkinyay, I can now write x = [ 1 , 2 , 3 , 4 ]13/09 04:36
* copumpkin emulates matlab syntax for matrices now :P13/09 04:36
dolioDoesn't matlab use semicolons?13/09 04:37
copumpkinnot sure that's much nicer than 1 \:: 2 \:: 3 \:: 4 \:: []13/09 04:37
copumpkinyeah, I guess those are off-limits?13/09 04:38
dolioI think so.13/09 04:38
copumpkin:(13/09 04:38
copumpkinhow does it resolve between [_ and _] and [_] if all three exist?13/09 04:39
dolioI'm not really sure.13/09 04:40
dolioApparently it's too ambiguous.13/09 04:45
copumpkin⊥-elim : {whatever : Set} → ⊥ → whatever13/09 04:52
copumpkinoh whoops :)13/09 04:52
dolioThat function is named "naughty".13/09 04:55
copumpkinwell, it has the ridiculous pattern or whatever it's called :P13/09 04:57
copumpkin⊥-elim ()13/09 04:57
copumpkinis that still naughty?13/09 04:57
dolioAbsurd.13/09 04:57
dolioYes.13/09 04:57
copumpkinhow come?13/09 04:57
dolioBecause it's a clever name.13/09 04:57
dolioAnd Conor McBride is always right.13/09 04:58
copumpkinah, true13/09 04:58
dolioIf you're into latin, you could call it ex-falso-quodlibet.13/09 04:59
copumpkinout of false, whatever you choose?13/09 05:01
copumpkinI guess the type signature would suggest that :)13/09 05:02
dolioI don't know Latin, but it's something like that.13/09 05:02
dolioThat's (one of) the term(s) from logic.13/09 05:03
copumpkinoh I see why it's bad, I assumed that the absurd pattern was saying it was impossible, but it's actually just dealing with the fact that bottom is uninhabited, right?13/09 05:03
dolioYes.13/09 05:03
copumpkinwhy can that function be written at all? doesn't it undermine everything?13/09 05:04
dolioHow?13/09 05:04
dolioAnyhow, from the empty type to any type, you have the empty function.13/09 05:04
copumpkinoh, I guess it just behaves a bit like flip const?13/09 05:06
copumpkinoh, not even13/09 05:06
dolioThe empty function.13/09 05:06
dolioIf you think of a function as a set of pairs, under some restrictions, it's the empty set.13/09 05:07
copumpkinyeah, ok :)13/09 05:07
copumpkinokay yeah, I see, sorry13/09 05:07
dolioSo A^0 = {{}} = 113/09 05:08
dolioIncluding 0^0.13/09 05:08
copumpkinmakes sense13/09 05:08
dolioAlthough for 0^0, it can also look like \x -> x, which is confusing, I guess.13/09 05:09
dolioAnyhow, what you're saying is impossible when you use the absurd pattern is that any constructors could result in a value of that type.13/09 05:12
--- Day changed Mon Sep 14 2009
-!- copumpkin is now known as Meow14/09 01:57
-!- Meow is now known as copumpkin14/09 02:05
--- Day changed Tue Sep 15 2009
jeltschHello, is there anybody listening here?15/09 11:46
jeltschI need some help regarding font settings for Agda/emacs.15/09 11:47
jeltschHello?15/09 11:47
jeltschHmm.15/09 11:48
greenrdas I just tweeted: Discovered nice undocumented feature in agda: put functions in a record declaration - they'll be added to the created module. Bit like OOP!15/09 14:14
jeltschgreenrd: This isn’t undocumented.15/09 14:28
jeltschThat is, it is documented. :-)15/09 14:28
jeltsch<http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf>15/09 14:29
jeltschpage 1915/09 14:29
greenrdah, I meant in the reference manual15/09 14:29
jeltschThere is a reference manual?15/09 14:30
greenrdon the wiki15/09 14:30
jeltschOn <http://wiki.portal.chalmers.se/agda/>, I cannot find a link to a reference manual.15/09 14:30
jeltschI always used the above tutorial.15/09 14:31
jeltschI already discovered that this doen’t mention everything.15/09 14:31
jeltschFor example, I found the keyword “abstract” in the standard libs.15/09 14:31
jeltschWhich is not described in this tutorial.15/09 14:31
jeltschAnd I have no idea what it is about. :-(15/09 14:31
greenrdmanuals & howtos, first link on that page15/09 14:33
stevanbtw, some slides from the talks at AIM are online now15/09 14:34
greenrdcool15/09 14:39
* greenrd takes a look15/09 14:39
Saizanoh, so defining a record type automatically defines a module?15/09 14:39
greenrdSaizan: yeah - didn't you know that? :)15/09 14:40
greenrdso you can say open Foo to bring the field accessor functions for Foo into scope15/09 14:41
greenrdor open Foo bar if Foo requires a parameter15/09 14:41
Saizanthe reference manual said something like that, but i thought you had to do it manually15/09 14:41
greenrdno15/09 14:41
Saizani think the module is always parametrized on an instance of the record15/09 14:42
greenrdwhoops yeah, that's right15/09 14:42
Saizanso you need "open Foo someFoo" ?15/09 14:42
greenrdyeah15/09 14:42
stevanit's a shame setzer hasn't posted his slides, he has done some pretty cool gui apps in agda that termination check :-)15/09 15:03
--- Day changed Wed Sep 16 2009
-!- eelco_ is now known as eelco16/09 09:56
--- Day changed Thu Sep 17 2009
Saizanis the complete code for the Observational Equality paper available somewhere?17/09 17:22
--- Day changed Fri Sep 18 2009
-!- codolio is now known as dolio18/09 00:40
-!- codolio is now known as dolio18/09 02:58
-!- dolio is now known as opdolio18/09 02:59
-!- opdolio is now known as dolio18/09 03:00
-!- E_G is now known as EnglishGent18/09 06:33
copumpkinwhat is the purpose of InitLast here? http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Vec.html#406218/09 07:54
copumpkinI guess it's just to easily do a reverse :: constructor so you can pull init and last out in one fell swoop?18/09 07:56
dolioIt's a view.18/09 07:57
copumpkinmakes sense :)18/09 07:57
doliohttp://sneezy.cs.nott.ac.uk/~npo/PowerPi.pdf18/09 07:57
dolioOr, I think it's a view...18/09 07:59
dolioMan, why do the standard libraries use 0-10 for precedences?18/09 08:00
copumpkinit looks like a view18/09 08:00
dolioOh, yeah, it is.18/09 08:01
dolioBecause ::r in the type evaluates into a regular vector.18/09 08:02
copumpkinyeah18/09 08:02
copumpkinoh!18/09 08:02
copumpkinI think I just realized the difference between being indexed by something and being parametrized by it18/09 08:02
copumpkinI remember the agda intro paper I read claimed there was a difference but just said something along the lines of "if you're on the right of the colon, you're indexed"18/09 08:03
dolioIndices can be specified as anything of the appropriate type in the 'return type' of the constructor, whereas parameters are always just the variable name, but parameters are scoped over the entirety of the data definition.18/09 08:09
copumpkinyeah18/09 08:09
dolioAnd only indices can cause type refinement, I think.18/09 08:09
dolioThey're what make Generalized Algebraic Datatypes generalized.18/09 08:10
copumpkinyeah, that was what made me realize, when the paper you just linked to it showed and compared it to a GADT18/09 08:10
dolioYeah, GADTs are like inductive families, except the indices are limited to thinks of kind *.18/09 08:11
dolioOr, maybe things with kinds...18/09 08:11
dolioYeah, any kind, I guess.18/09 08:11
copumpkinam I allowed to make both Fin and Nat into the builtin natural type? it'd be fun to have it prevent me from writing numbers larger than a certain value18/09 08:12
dolioWhich, I suppose, makes them not "inductive" families, strictly speaking, because the kind level is not inductively defined. :)18/09 08:12
copumpkinmakes sense18/09 08:12
dolioI suspect the answer is "no".18/09 08:12
copumpkindamn :)18/09 08:16
copumpkinis there a nicer way to define Fin than mirroring Nat?18/09 08:17
dolioNot that I've seen.18/09 08:19
dolioHaving a built-in for Fin would probably be a good idea, though.18/09 08:34
dolioIf you take Fin n as being Z/n, and use it for fast modular arithmetic.18/09 08:35
copumpkinyeah18/09 08:35
copumpkinI was just writing a _mod_ for my nats18/09 08:36
copumpkinhmm, the standard library isn't working for me :o18/09 08:54
copumpkinif I import Data.Vec, it complains that Monoid isn't in scope in Data.List18/09 08:55
copumpkinthe standard library is remarkably extensive18/09 09:03
copumpkinthere's so much indirection in the standard library18/09 09:26
copumpkinhmm, my Algebra module in lib-0.2 seems broken18/09 09:32
dolio_mod_ is tough.18/09 09:38
dolioFinally got it.18/09 09:39
dolioWell-founded recursion is my new best friend.18/09 09:43
stevanhi18/09 15:45
Saizanhi18/09 15:46
stevanin Data.List.Properties; where does begin and \qed come from? as far as i can see EqReasoning is never opened?18/09 15:46
stevanhmm, i got it working somehow, so i guess it doesn't matter :-)18/09 15:51
stevanbtw, http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/18/09 15:51
copumpkinthe induction module in the std lib admits that its types are hard to follow, but that agda can normalize them for me18/09 17:49
copumpkinhow can I get that?18/09 17:49
copumpkinhas anyone here played with lib-0.2? the Algebra module seems broken, on mine at least18/09 19:23
darinmbroken how?18/09 19:24
copumpkinit doesn't appear to be exporting what it should be exporting. I try to import Data.Vec, which imports Data.List, and List contains a Monoid "instance", but it complains that Monoid isn't in scope18/09 19:25
darinmseems OK with the development version18/09 19:29
darinmwhat does your code look like?18/09 19:31
copumpkinhmm, maybe I'll try that18/09 19:31
copumpkinI was just trying the lib-0.2 tarball18/09 19:31
copumpkinmy code is empty18/09 19:31
copumpkinI just tried importing Data.Vec18/09 19:32
darinmwell, Data.Vec doesn't export Monoid, you need to import that from Algebra18/09 19:32
darinmmodule Foo where18/09 19:32
darinmopen import Data.List18/09 19:32
darinmopen import Data.Nat18/09 19:32
darinmopen import Algebra18/09 19:32
darinmopen Monoid (monoid ℕ)18/09 19:32
copumpkinI don't expect it to export it18/09 19:32
darinmthat works18/09 19:32
copumpkinI mean18/09 19:33
copumpkinall I type in my code is open import Data.Vec18/09 19:33
copumpkinnothing else18/09 19:33
copumpkinand emacs opens up Data.List automatically, with a highlighted Monoid18/09 19:33
copumpkinsaying it's not in scope18/09 19:33
darinmoh, weird18/09 19:33
darinmyeah, don't know18/09 19:33
copumpkinI also tried Induction and it also complained about another missing algebraic structure18/09 19:34
copumpkinso I assumed Algebra was the culprit :)18/09 19:35
copumpkinbut I'll grab the more recent lib18/09 19:35
darinmyeah, might be.  I'd be a little surprised if it was broken though... usually the thing is fully compiled as a test before release18/09 19:35
darinmwell18/09 19:35
darinmif you get the darcs lib, you will also need the darcs agda18/09 19:35
copumpkinoh18/09 19:36
copumpkinwhat's new?18/09 19:36
darinmfew small things mostly... biggest one is a way to reduce primitive equality, so you can reason about it, say for strings18/09 19:36
darinmthere's a couple of bigger changes that will be in there soon from the stuff at AIM18/09 19:37
darinmuniverse polymorphism :)18/09 19:37
darinmand cabal support18/09 19:37
copumpkin:O18/09 19:37
copumpkinnice!18/09 19:37
copumpkinyeah, when I import Induction it complains about CommutativeSemiring being missing from Data.Nat.Properties18/09 19:40
darinmwhat version of agda do you have?18/09 19:41
darinmnot sure if it matters, but stil18/09 19:41
copumpkin2.2.4, with lib-0.218/09 19:41
darinmok... I'll try to test with those versions later and see if I get any problems18/09 19:42
copumpkinthanks :)18/09 19:42
copumpkinData.Vec (List) and Induction have been the painful ones so far18/09 19:42
darinmk18/09 19:42
copumpkinwho writes the std lib by the way? it's got WAY more stuff than I thought it did18/09 19:44
copumpkinjust reading the readme made me think it was just a few modules, but Everything has a lot of awesome stuff18/09 19:44
darinmNils Anders Danilesson does most of it18/09 19:45
darinmsome of it is adapted from older code from Ulf18/09 19:45
darinmbut yeah, there's some really cool stuff in there18/09 19:45
darinmwhat kind of stuff do you do with agda?18/09 19:48
copumpkinso far I've just been taking really simple statements I know to be true and tried to prove them :P18/09 19:49
copumpkinI'm a real newbie with this stuff :)18/09 19:49
darinmthat's cool :)18/09 19:49
copumpkinI only started with haskell a few months ago, so this seemed like the next step from the types perspective18/09 19:49
darinmyeah18/09 19:50
darinmdid you find it tricky to start learning the std library?18/09 19:51
darinm(aside from the probs you just mentioned)18/09 19:52
copumpkinthe basics are quite simple, the ones with obvious analogs in haskell, like Nat, Vec, List, etc. For the more complicated things there's a lot of indirection18/09 19:52
darinmyeah... maybe a little too much18/09 19:53
copumpkinin the sense that figuring out some of the less basic proofs requires me to look at two or three unrelated modules18/09 19:53
copumpkinI'm starting to get used to it18/09 19:53
darinmthat's good18/09 19:54
--- Day changed Sat Sep 19 2009
copumpkinI tried to compile the darcs agda19/09 00:40
copumpkinbut I don't think I got agda-executable out of it19/09 00:40
copumpkindoes that live somewhere else?19/09 00:40
copumpkinso 2.2.5 and the most recent lib fixed my issues, yay19/09 00:49
-!- opdolio is now known as dolio19/09 01:02
copumpkinI feel that rec is the induction function I need19/09 04:36
copumpkinfrom Induction.Nat19/09 04:37
copumpkinit claims its type is19/09 04:37
copumpkin(P : ℕ → Set) → ((x : ℕ) → Rec P x → P x) → (x : ℕ) → P x19/09 04:37
dolioThat looks sensible.19/09 04:38
dolioThis is another reason why learning about the y-combinator is important.19/09 04:39
copumpkinI don't quite get how to use that Rec term19/09 04:39
copumpkinit seems to contain the base case and recursive case?19/09 04:40
dolioSome fancy induction principles look like Y.19/09 04:40
copumpkinah, interesting19/09 04:40
dolioY : (a -> a) -> a, wf-induction : ((z < y -> P z) -> P y) -> P x19/09 04:41
dolioSo you get to make recursive calls as with a fixed-point combinator, you just have to prove something about the recursive calls you're making.19/09 04:42
copumpkinoh, interesting19/09 04:42
copumpkinhmm19/09 04:44
dolioTo turn rec's type into well-founded induction, you do "Rec P x = {y : _} -> y < x -> P y".19/09 04:44
dolioI think that's right.19/09 04:44
copumpkinwhat's the {y : _} mean?19/09 04:44
dolioIt's what \all y means.19/09 04:45
copumpkinoh, I didn't realize19/09 04:45
dolioSince I'm not going to fire up emacs to type this stuff.19/09 04:45
copumpkin:)19/09 04:45
dolioAnyhow, with the way Rec is defined, apparently it's just another way to do ordinary induction on naturals.19/09 04:49
dolioBut I think the point of the induction framework is rather to do stuff like:19/09 04:49
doliorec : (Rec : RecStruct Nat) (P : Nat -> Set) -> ((x : Nat) -> Rec P x -> P x) -> (x : Nat) -> P x19/09 04:50
dolioWhich is parameterized by the induction principle.19/09 04:51
dolioSo you can do rec Rec for normal induction, and rec WellFounded for well-founded induction, and whatever else.19/09 04:51
dolioRec P zero = \top ; Rec P (suc n) = P n, so in the original type...19/09 04:52
copumpkinah, cool19/09 04:52
dolioif f is the (x : nat) -> Rec P x -> P x...19/09 04:53
doliowhen x = zero, you get \top -> P zero which is isomorphic to P zero19/09 04:53
dolioAnd when x = suc n you get P n -> P (suc n)19/09 04:53
dolioWhich looks like normal induction: ((x : Nat) -> P n -> P (suc n)) -> P zero -> (x : Nat) -> P x19/09 04:54
dolioEr, I mixed up my variables there.19/09 04:54
dolioYou get the idea, though.19/09 04:54
dolioIt's similar to how you can do foldr : (a -> r -> r) -> r -> [a] -> r or foldr : (Maybe (a,r) -> r) -> [a] -> r19/09 04:55
copumpkinyeah19/09 04:58
* copumpkin is trying to prove the first induction I ever did, from high school, in agda (the sum of odds being perfect squares)19/09 04:58
dolioHmm... It's been a while since I thought about that.19/09 05:02
copumpkinit's pretty simple induction, I'm mostly just trying to figure out how to express it :)19/09 05:02
dolioI guess you use Sum_0^(n-1) 2*i+1 = n^2?19/09 05:02
copumpkinI actually expressed the odds more subtly, which might make my life harder later though19/09 05:03
copumpkinwell, more directly19/09 05:03
copumpkinfirst odd = 1, and then next odd is suc suc of it19/09 05:03
dolioI don't know if that's better or worse.19/09 05:08
copumpkinyeah, I guess this is pretty easy if you assume a lot of "high school -level math"19/09 05:08
copumpkinbut I haven't thought of what properties of naturals I'll be needing19/09 05:08
dolioWell, you'll need something like (n + 1)^2 = n^2 + 2*n + 1, at least, I think.19/09 05:09
copumpkinyeah19/09 05:09
dolioThat's actually exactly what you get in the inductive case with the 2*i+1 formulation.19/09 05:09
dolioYou ever figure out _mod_?19/09 05:22
copumpkinnope :(19/09 05:23
dolioThat isn't actually that surprising.19/09 05:23
copumpkinI was thinking of repeatedly subtracting the right hand side19/09 05:23
doliocopumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9531#a953119/09 05:40
copumpkinoh nice, thanks :)19/09 05:41
copumpkindolio: is there a way to state that your mod function only takes >=1 for its second parameter? with (suc n) or something?19/09 05:54
copumpkin(to avoid the maybe)19/09 05:55
dolioYeah, you could require a proof.19/09 05:56
copumpkinbut not just in the type somehow?19/09 05:57
dolioYes, in the type.19/09 05:57
copumpkin_mod_ : ℕ → ((suc k) : ℕ) → Fin k ?19/09 05:58
dolio_mod_ : Nat -> (k : Nat) -> (0 < k) -> Fin k19/09 05:58
copumpkinyeah, I could see that19/09 05:58
copumpkinbut it seems like it should be possible to write the constructor in the type to prevent 019/09 05:58
copumpkinmaybe not :)19/09 05:58
dolioYou could do _mod_ : Nat -> (k : Nat) -> Fin (suc k)19/09 05:59
copumpkinh19/09 05:59
copumpkinm19/09 05:59
dolioBut then n mod k means n mod (suc k) in actuality.19/09 05:59
copumpkinoh, ok19/09 05:59
copumpkinhas there been any work on dependent types with subtyping?19/09 06:04
dolioNuPRL has some kind of subtyping.19/09 06:05
dolioLike you can have B \subset A.19/09 06:06
copumpkinah, cool19/09 06:06
dolioI'm not sure if that's useful for the usual uses of subtyping or not.19/09 06:06
copumpkinthat mod thing you gave me is so clear19/09 06:08
dolioExcellent. :)19/09 06:08
copumpkinI'm used to having to jump around between a dozen files when reading the std lib :P19/09 06:09
copumpkinoh, names can overlap? your constructors for Fin and Nat have the same name19/09 06:10
dolioConstructor names can overlap.19/09 06:10
copumpkinexcellent!19/09 06:10
dolioBecause it's unambiguous.19/09 06:10
copumpkinmakes sense19/09 06:11
copumpkinI guess it'd be easy to make mod into modRem19/09 06:37
dolioYeah.19/09 06:37
copumpkinor divMod, rather19/09 06:37
copumpkin:P19/09 06:38
dolioIt's actually kind of a pain, because you need to modify the well-foundedness criterion.19/09 06:38
copumpkinoh19/09 06:38
dolioBut it's not that hard.19/09 06:38
* copumpkin tries19/09 06:38
copumpkinby the way, I can't define fix suc in agda, right?19/09 06:40
copumpkinor not without additional machinery19/09 06:40
dolioYou can't define fix.19/09 06:40
dolioOr, you can, but it won't pass the termination checker.19/09 06:41
copumpkinI see19/09 06:41
dolioWhich won't actually prevent you from using it, but it will be colored pink.19/09 06:41
copumpkindoes that mean I can't import the module or something?19/09 06:41
dolioNo.19/09 06:41
dolioAlso, if you use something like fix suc in a type, it'll go into a loop trying to compute its normal form.19/09 06:42
copumpkinoh :)19/09 06:42
dolioAt least, last I checked.19/09 06:42
dolioSomething like "inf = suc inf" is a valid coinductive natural, though.19/09 06:44
copumpkinso if I wanted to represent "the unbounded natural" in a typechecker-friendly manner, I'd need a third constructor for Nat?19/09 06:46
dolioI guess. If you just want Naturals + infinity, the coinductive version might be better, depending on what you want to do with it.19/09 06:47
copumpkinhmm, not sure yet :) really just poking around to see19/09 06:54
copumpkinany idea why product is defined with the "snd" as a function of fst? http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Product.html#39219/09 07:02
dolioThat's dependent sum.19/09 07:05
dolioBinary products are a special case of dependent sums just like ordinary functions are a special case of dependent products.19/09 07:06
copumpkin:o19/09 07:06
copumpkinoh!19/09 07:07
copumpkinso the odd ⊎ symbol is (,) in hasell land19/09 07:07
copumpkinhaskell19/09 07:07
copumpkinand \x can't be represented19/09 07:07
dolioNo. That's ordinary sum.19/09 07:07
copumpkinoh, hmm19/09 07:07
copumpkinoh I see19/09 07:07
dolioDependent sums are a generalization of regular sums, in a way.19/09 07:08
copumpkinso sum = Either, product = (,), but dependent sum = ~ (,) with more?19/09 07:08
dolioWith regular sums, you have a finite set of tags (2 of them for the binary one), and a type for each tag.19/09 07:09
dolioAnd the sum is the union of those types tagged with the tags.19/09 07:09
copumpkinyeah19/09 07:10
copumpkinI've heard of sum types and product types colloquially19/09 07:10
dolioSo, dependent sum, Sigma, is the generalization of that to where the tags are an arbitrary type.19/09 07:10
copumpkinoh, hmm19/09 07:10
dolioIn Sigma a P, for each x in a, there's an injection into the sum \w -> x , w : P x -> Sigma a P19/09 07:11
dolioAnd you get back regular sums by taking some finite set of tags as a.19/09 07:11
dolioSo if you had SumTags = Inl | Inr...19/09 07:11
dolioAnd T : SumTags -> Set19/09 07:12
copumpkinaha, I think I get it19/09 07:12
copumpkinso you can think of it as an index19/09 07:12
dolioSigma SumTags T has "Inl, (w : T Inl)" and "Inr , (w : T Inr)" as elements.19/09 07:12
copumpkinthat's neat19/09 07:12
dolioWhich is isomorphic to "T Inl \uplus T Inr".19/09 07:12
dolioBUT19/09 07:13
dolioIf instead you take T to be a constant function...19/09 07:13
dolioThen you get Sigma a (\_ -> b) has elements of b tagged by elements of a.19/09 07:14
dolioWhich is a binary product.19/09 07:14
copumpkininteresting19/09 07:14
dolioSimilarly, the important part about product A x B is that you have projections from it to A and B...19/09 07:14
dolioOr finite n-ary products have n such projections.19/09 07:15
dolioSo, to get the dependent version of that, you have an a-indexed family T : a -> Set...19/09 07:15
dolioAnd given the product for that family (f : Pi a T), you need a projection corresponding to each a.19/09 07:17
dolioWhich looks like, for x \in a, "f x : T x"19/09 07:17
dolioYou get back finite n-ary products via (fn : Fin n) -> T fn19/09 07:18
dolioBut you also get functions (_ : a) -> b19/09 07:19
dolioBy ignoring the type dependence in the same way.19/09 07:20
copumpkinwow19/09 07:20
dolioOr, however you want to say that.19/09 07:20
copumpkinthis feels so deep :P19/09 07:20
copumpkinI guess it's similar to how you can define addition by repeated incrementing, multiplication by repeated addition, exponentiation by repeated multiplication19/09 07:20
copumpkinin some sense, at least19/09 07:21
dolioYeah, well...19/09 07:21
dolioif in 'Sum_0^n a_i' you take a_i = b, you get b*n.19/09 07:22
dolioWhere a_i = b is like the constant function that ignores i.19/09 07:22
dolioSo, yeah.19/09 07:22
copumpkinso cool :)19/09 07:23
dolioDoes that make sense as being related? I'm not entirely sure now.19/09 07:24
dolioI guess it's similar.19/09 07:24
copumpkinI think I get it, but I'm still trying to absorb it all19/09 07:24
dolioIf you know the categorical definitions for products and coproducts, it becomes pretty clear if you try to write down what a generalization would look like.19/09 07:27
copumpkinI do roughly know what products and coproducts are19/09 07:28
copumpkinbut haven't actually done anything significant with it (I know what the diagram looks like and why)19/09 07:28
dolioLike "a finite some of objects A_i is an object Sum A with morphisms in_i : A_i -> Sum A, and Sum A is initial"19/09 07:29
doliosum, even.19/09 07:29
dolioSo "a dependent sum of an a-indexed family T is an object Sigma a T with an a-indexed family of injections in : (x : a) -> T x -> Sigma a T, and Sigma a T is initial."19/09 07:31
dolioWhich, _,_ is exactly that type.19/09 07:31
dolioAnd then dependent uncurry corresponds to initiality.19/09 07:32
dolioBecause it takes some other family of injections (x : a) -> T x -> S to a morphism Sigma a T -> S.19/09 07:33
copumpkinI think I see19/09 07:43
* copumpkin needs to ruminate :)19/09 07:43
copumpkin(is there any way to get scoped type variables in agda?)19/09 07:43
dolioif foo : {a : Set} -> ..., do 'foo {a} ... = ...'19/09 07:44
dolioThen a is in scope in a where clause.19/09 07:44
copumpkinoh19/09 07:44
copumpkinhmm, but I need it in my type annotation19/09 07:46
dolioIt's in scope in the type annotations of the where clause, too.19/09 07:46
copumpkinhrm19/09 07:48
copumpkinoh I see19/09 07:49
copumpkin:O19/09 07:54
copumpkinop opdolio19/09 07:55
copumpkindamn, my divMod compiles but contains both yellow and pink19/09 07:55
opdolioPaste it.19/09 07:58
copumpkinit's too naive, but sure19/09 07:59
copumpkinhttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9534#a9534 (I added this onto the code you pasted)19/09 08:00
copumpkinfar too simplistic :P19/09 08:00
opdolioWell, yeah. I used well-founded induction for a reason.19/09 08:00
opdolioAgda can't tell that (x - y) is structurally smaller than x.19/09 08:01
copumpkinyeah, makes sense19/09 08:01
opdolioYou actually might be able to get away with just well-founded induction on the naturals, same as mine.19/09 08:03
opdolioI was thinking of carrying along the div part to keep it tail recursive.19/09 08:03
opdolioBut if you match on the result like that, you only need to make recursive calls on naturals.19/09 08:03
copumpkinI see19/09 08:04
copumpkingotta go home now, I'll try again in a bit :) thanks for all your help!19/09 08:04
opdolioSo it's roughly the same code.19/09 08:04
opdolioNo problem.19/09 08:05
copumpkinciao!19/09 08:05
-!- opdolio is now known as dolio19/09 08:08
doliocopumpkin: It occurred to me that the non-dependent analogue of what we were talking about yesterday is stuff like A + A ~ 2 x A and A x A ~ 2 -> A, so yes, repeated sum/product.19/09 18:13
copumpkinoh yeah19/09 18:14
copumpkinA -> A ~ 2 --> A :P19/09 18:14
dolioYeah. Tetration types.19/09 18:15
dolioWrite a paper!19/09 18:15
copumpkinhah19/09 18:15
-!- koninkje_away is now known as koninkje19/09 21:22
--- Day changed Sun Sep 20 2009
-!- jfredett_ is now known as jfredett20/09 00:41
-!- koninkje is now known as koninkje_away20/09 01:57
-!- koninkje_away is now known as koninkje20/09 03:45
-!- koninkje is now known as koninkje_away20/09 03:56
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Relation.Binary.PreorderReasoning.html#1084 seems very elegant20/09 05:44
copumpkinooh, difference naturals!20/09 05:47
copumpkinso much to explore!20/09 05:48
copumpkinI wonder why there's no matrix stuff in the standard library? is it because there aren't any fields or modules in the algebra module yet?20/09 05:49
copumpkinoh, we have integers and naturals in the std lib20/09 05:59
copumpkinI mean integers and rationals20/09 05:59
copumpkinI wonder why there isn't a Field structure yet, or a Vector space20/09 06:02
copumpkinwow, constructing a rational takes some serious proof! _÷_ : (numerator : ℤ) (denominator : ℕ)20/09 06:05
copumpkin      {coprime : True (C.coprime? ∣ numerator ∣ denominator)}20/09 06:05
copumpkin      {≢0 : False (ℕ._≟_ denominator 0)} →20/09 06:05
copumpkin      ℚ20/09 06:05
dolioThose proofs might be automatic...20/09 06:12
copumpkin:o20/09 06:13
dolioTrue takes a decidable predicate, turns it into a bool, and then asserts that it's true.20/09 06:13
dolioSimilarly for false.20/09 06:13
dolioFalse, even.20/09 06:13
copumpkinah20/09 06:13
dolioWhich seems roundabout, but maybe that's so that it can compute it via the algorithm that decides the predicate, rather than requiring proof be supplied.20/09 06:14
dolioAt least, that's all I can come up with.20/09 06:14
dolioI hadn't seen that before, but if it works, it might be nice...20/09 06:15
copumpkinyeah :)20/09 06:18
copumpkinthere's so much cool stuff hidden away in Everything20/09 06:18
copumpkinthe front page of the readme really doesn't do it justice20/09 06:18
copumpkinis there a good way to see a list of all unicode characters I can type in emacs?20/09 06:26
dolioIf you type \ and then tab, a giant list pops up.20/09 06:28
copumpkinnice, thanks!20/09 06:29
copumpkinhave you noticed any good way of typing ^T (for matrix transpose?)20/09 06:30
dolioNo. There aren't a lot of unicode super/subscripts it seems.20/09 06:32
copumpkinah well, I can live with english for now20/09 06:32
dolioI must say, these assertions on decidable predicates don't seem convenient.20/09 06:50
copumpkinany idea how to use algebraic structures from http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Algebra.Structures.html#268 ?20/09 06:55
dolioThese are just the laws things have to follow.20/09 06:57
dolioThe things you use are named without the Is20/09 06:58
copumpkinoh yeah, I just need {a : Monoid}20/09 06:58
copumpkinbecause Monoid is Set\_120/09 06:58
dolioAnd the way you use them is to open them, I think.20/09 06:58
copumpkinI see20/09 06:58
dolioBecause you need access to the carrier, and not opening them is a huge pain with the qualified names.20/09 06:58
copumpkinI don't get the raw counterparts to things20/09 06:59
dolioRaw is just the operations, without the laws.20/09 06:59
copumpkinfor quick and dirty programs?20/09 06:59
dolioI'm not sure why they're split up like that.20/09 07:00
copumpkinopen Monoid using (carrier) identity : {n : ℕ} → {m : Monoid} → Mat n n (carrier m)20/09 07:11
copumpkindoes that seem "idiomatic"?20/09 07:11
copumpkinI guess it needs more than a monoid20/09 07:12
copumpkina semiring or something20/09 07:13
copumpkinyeah20/09 07:14
copumpkindamn, decisions20/09 07:14
copumpkinrecord SemiringWithoutAnnihilatingZero : Set₁ where20/09 07:14
copumpkinnow I need to decide if I want the module to be parametrized over a field or something, or just to open the structures I need locally for each operation20/09 07:16
copumpkinI need RecordWildcards in agda :P20/09 07:23
* copumpkin goes crazy with Algebra.agda20/09 08:38
* copumpkin started writing an IntegralDomain record in Algebra20/09 09:15
copumpkinhaving trouble writing the "no zero divisors" property though20/09 09:39
copumpkinyay, I have identity matrix and transposition working20/09 19:36
copumpkinand multiplication!20/09 19:45
dolioNice.20/09 19:51
copumpkinhaven't proved anything about them yet :P20/09 19:51
copumpkinI could've sworn the std lib Data.Vec had a Vec A n -> Fin n -> A20/09 20:09
dolioIt must.20/09 20:10
copumpkinaha, lookup20/09 20:12
* copumpkin holds off on the left- and right-identity proofs for matrix multiplication for now :P20/09 20:50
copumpkinany ideas for a good left-multiply-by-vector and right-multiply-by-vector symbol?20/09 21:04
copumpkinI still thought lookup used to have a counterpart called _[_]20/09 21:44
copumpkinI'm having trouble reusing the Algebra.FunctionProperties for matrices, as it seems hard to get the operation to depend on implicit parameters20/09 21:55
copumpkinI want +-assoc : Associative _+_, where _+_ : ∀ {m n} → Op₂ (Mat carrier m n)20/09 21:56
copumpkinit colors it in yellow because (I assume) it can't figure out m and n20/09 21:56
copumpkinwhen I open the Algebra.FunctionProperties there's an implicit parameter for the set I'm working over, but I can't seem to fix the m and n there20/09 21:57
copumpkinthe type of sum in Data.Vec seems too specific... it feels like it should open Monoid and use the operation in there20/09 22:10
copumpkinhttp://snapplr.com/npeb seems odd, that it would not like the simpler type but not mind the more complex one20/09 22:26
copumpkinmmm, 12 holes in my code :P20/09 22:58
copumpkinthis is no good: http://snapplr.com/c3hz20/09 23:04
--- Day changed Mon Sep 21 2009
copumpkin∣_∣ : ∀ {n} → Mat carrier n n → carrier21/09 00:15
copumpkinnot sure how to grab the implicit parameter there21/09 00:16
dolioWhich?21/09 00:17
copumpkinoh I guess I can write ∣_∣ {0} mat = 1#21/09 00:17
dolioOh. Right.21/09 00:17
copumpkinnow, should I require people to provide a proof that a matrix is invertible, or return a Maybe from my inverse function?21/09 01:26
dolioIs invertability decidable?21/09 01:27
dolioI guess it's det m /= 0?21/09 01:27
copumpkinwhy wouldn't it be?21/09 01:27
copumpkinyeah21/09 01:27
dolioIt's been a while since I did this stuff.21/09 01:28
dolioAnyhow, you can make two versions, if you want.21/09 01:28
copumpkintrue21/09 01:28
dolioWrite the one that takes the proof first, and then write one that wraps that in a Maybe.21/09 01:28
copumpkinhow would I wrap it in a Maybe? I'm not sure how I'd call the one that wants a proof without it21/09 01:29
dolioYou do case analysis on the decision procedure for the proof.21/09 01:30
dolioinv m with invertable m ; ... | yes pf = just (inv' m pf) ; ... | no _ = nothing21/09 01:31
dolioOr invertable? or whatever you call it.21/09 01:31
copumpkinoh, I see :)21/09 01:31
copumpkinknow of any even/odd functions in the std lib?21/09 01:36
dolioNot off hand. But I don't use the standard libraries much.21/09 01:36
dolioI like defining Sigma over and over.21/09 01:37
dolioI read the Coq manual on their Notation construct (similar to mixfix), and it has some nice features.21/09 01:38
dolioLike, you can define new binding constructs.21/09 01:38
copumpkinI can use http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Nat.Divisibility.html#180 for even/odd I guess21/09 01:38
dolioSo you could define a Sigma x:a T21/09 01:38
copumpkinSigma?21/09 01:39
dolioIn fact, their notation { x : a | T } is actually defined using the Notation, I think.21/09 01:39
dolioDependent sum.21/09 01:39
copumpkinoh that :)21/09 01:39
dolioIn Agda you have to write Sigma a (\x -> T) instead.21/09 01:40
copumpkininteresting21/09 01:45
copumpkinI wonder if Coq's notation could be used to write list comprehensions21/09 01:46
dolioOh, that's another thing. I'm not sure if you can write comprehensions, but it has an experimental feature for defining stuff like [ a , b , c , d ].21/09 01:46
copumpkinfun21/09 01:48
dolioOther than that, it's just noisier than Agda.21/09 01:49
* copumpkin is still curious about these famous tactics in coq that everyone raves about21/09 01:50
dolioThose are two pretty big features, though.21/09 01:50
dolioTactics let you describe how to prove something instead of doing it manually via doing C-c C-c and C-c C-space and such in Agda mode.21/09 01:51
dolioInstead you say stuff like "try induction" and it figures out what specifically to do automatically.21/09 01:52
dolioAnd you can write new tactics, too.21/09 01:53
copumpkinoh wow21/09 01:53
dolioIf a proof is simple enough, you can just say "figure it out yourself".21/09 01:53
* copumpkin is still trying to write determinant21/09 01:57
dolioWell, they won't help you with that.21/09 02:00
copumpkinyeah :)21/09 02:00
copumpkinC-c C-a never seems to work, what is it supposed to do?21/09 02:01
dolioWhat's it called? I'm not familiar with that one.21/09 02:02
copumpkinif I right click on a goal, it says "auto", with that shortcut21/09 02:02
dolioHuh.21/09 02:03
copumpkinhttp://snapplr.com/r8dn21/09 02:04
dolioThat must be new, because I don't have it.21/09 02:05
copumpkin:o21/09 02:11
dolioI just pulled and the first two patches were "Adding Auto" and "Auto update".21/09 02:12
dolioDoesn't say what it does, though.21/09 02:12
copumpkinfun21/09 02:12
copumpkinI've tried it in a bunch of places21/09 02:12
copumpkinbut each time it says it failed21/09 02:12
dolioAlso "added propositional equality to the builtin types" which sounds interesting.21/09 02:13
dolioI guess that's for the "trustMe : {A : Set} {a b : A} -> a == b"21/09 02:16
Saizanwhy it's qualified with "propositional"?21/09 02:19
copumpkinis there some way I can get more helpful variables than _354?21/09 02:19
copumpkin(suc m) != (Data.Nat._+_ (toℕ n) (_354 m mat n)) of type ℕ21/09 02:19
dolioNot that I know of. And I'm not really sure why it's called propositional equality.21/09 02:20
Saizanand, btw, i try to ask again, anyone knows where i can find the code for "Observational Equality Now!"?21/09 02:20
Saizanmore helpful?21/09 02:21
Saizanfresh variables like those suggest that it didn't unify that part with anything21/09 02:21
dolioOh, maybe it's propositional because x == y is isomorphic to (T x -> T y)*(T y -> T x).21/09 02:22
dolioWhich, 'equality' of propositions is bi-implication.21/09 02:22
dolioSaizan: I have it, but I don't remember where I got it.21/09 02:23
doliohttp://code.haskell.org/Agda/examples/outdated-and-incorrect/OTT/21/09 02:24
Saizan"outdated-and-incorrect" sounds promising :)21/09 02:25
Saizanthanks :)21/09 02:25
dolio:)21/09 02:25
copumpkinhmm, it seems rather difficult to call splitAt or take/drop on Data.Vec21/09 02:28
copumpkinI guess I need to convince it that my index is within the bounds21/09 02:28
-!- jfredett_ is now known as jfredett21/09 02:32
* copumpkin concludes he needs Data.Fin.inject+21/09 02:39
copumpkinactually21/09 02:39
copumpkinjust _<_ probably21/09 02:40
copumpkinack21/09 02:54
Saizan_i wonder if it wouldn't make more sense to define Fin n = \Sigma N (\m -> m < n)21/09 03:07
copumpkinfor the life of me I can't seem to call Data.Vec.splitAt21/09 03:07
dolioIt is clearly quite wasteful to have both Fin n and m < n when they obviously have the same structure. :)21/09 03:23
dolioDepending on your definition of _<_.21/09 03:23
copumpkinsplitAt : ∀ {a} m {n} (xs : Vec a (m + n)) → SplitAt m xs, shouldn't it be able to infer that if m is Fin (suc (m + n)), then calling splitAt (toN m) is good?21/09 03:25
copumpkinI guess it isn't trivial21/09 03:26
dolioSurely m's type doesn't refer to itself.21/09 03:29
dolioOr, refer to m, rather.21/09 03:30
copumpkinI abused notation a bit there21/09 03:30
copumpkinI meant, given the length of xs there21/09 03:30
copumpkinm is of type Fin (suc <that length>)21/09 03:30
dolioAnyhow that means toN m < m' + n21/09 03:31
dolioSo you're trying to call splitAt with toN m and a vector with length m' + n.21/09 03:32
dolioBut toN m /= m'21/09 03:32
dolioHowever, given toN m < m' + n, you should be able to find n' such that m' + n = toN m + n', which means you can cast your vector to the type Vec a (toN m + n') and call splitAt.21/09 03:33
copumpkinso I need to explicitly subtract to get hold of the n?21/09 03:34
dolioThe proof will look something like subtraction, I guess.21/09 03:36
doliocopumpkin: It's probably easier to write a new splitAt for finite sets.21/09 03:44
copumpkinI see21/09 03:45
copumpkinI'll play with that21/09 03:45
dolioOr, maybe it isn't, with that SplitAt type. I'm not really sure.21/09 03:46
copumpkinI must be missing something, cause this feels more complicated than it needs to be21/09 03:47
dolioOh crap. I have to rebuild Agda now.21/09 03:52
copumpkinhow come?21/09 03:52
dolioI did darcs pull on the library, and the new "trustMe" equality thing blows up without runtime support.21/09 03:53
copumpkinah21/09 03:53
dolioI guess I'll get to try and figure out what auto does.21/09 03:54
copumpkinis anders the main author of the std lib?21/09 04:01
dolioYeah.21/09 04:03
dolioAlthough I'm not really sure what all are contributions.21/09 04:03
dolioOther than the delimited continuation monad, which I did.21/09 04:03
copumpkinah :)21/09 04:04
dolioAlthough I'm not really happy with that version, because that monad wants type indices not value indices like the indexed monads in the library.21/09 04:06
copumpkinthe Category.* stuff there seems a little neglected compared to the rest of the std lib21/09 04:07
copumpkinit'd be nice to actually model categories21/09 04:07
dolioIndexed state is the same way, really.21/09 04:07
dolioThey only work for a specified family of types.21/09 04:08
dolioI'm not really convinced faithfully modeling cateogry theory is a good way to get usable stuff for coding.21/09 04:12
copumpkinyeah, I wouldn't expect it to be, but it'd be nice to have a set of categorical constructs that are faithful, and then the usual ones we're used to in haskell for practical coding, and a mapping between them where possible21/09 04:13
dolioIt'd be interesting in its own right, yeah. :)21/09 04:13
dolioThe problem with doing category theory is there's a lot of meta-ness to it.21/09 04:13
copumpkinlike, not having to do all the crazy jumping through hoops that category-extras is full of would be pretty awesome21/09 04:14
dolioWhich means you need universe polymorphism or Set : Set to avoid writing tons of duplicate code.21/09 04:14
copumpkinyeah21/09 04:14
copumpkinwhich appears to be coming soon, right?21/09 04:14
dolioApparently. Although I'm not totally thrilled about the explicitness of it in the notes.21/09 04:15
copumpkinoh, the plan for it has been announced?21/09 04:17
dolioThere are some notes from a discussion at AIMX...21/09 04:18
doliohttp://wiki.portal.chalmers.se/agda/Main.AIMX21/09 04:19
dolioAll the way at the bottom.21/09 04:19
copumpkinoh, so Set is indexed by Nat?21/09 04:20
dolioYeah. That seems weird, too.21/09 04:20
dolioBut I'm no expert.21/09 04:20
copumpkinso I guess that makes Nat some kind of primitive in the language then?21/09 04:21
copumpkin"In an Agda review meeting back in 2007 it was decided that the hierarchy of sets should be cumulative (which would mean that Set_i had type Set_(i + k + 1) for any k ∈ ℕ)"21/09 04:23
copumpkinwhy would that make more sense than just having them behave incrementally?21/09 04:23
dolioWell, I don't know about it being useful for Set_i specifically.21/09 04:25
dolioIt's useful when A : Set_i means that, in addition, A : Set_(i + k).21/09 04:26
dolioI think, at least.21/09 04:26
dolioThat lets you cut down on universe parameters.21/09 04:27
dolioRather than "Foo : forall {m n} -> Set m -> Set n -> Set (max m n)" you can do "Foo : forall {n} -> Set n -> Set n -> Set n" because whichever is less can automatically be lifted.21/09 04:28
copumpkinah I see21/09 04:28
copumpkindoesn't the21/09 04:30
copumpkin       ⇑_ : ∀ {n}{A : Set n} → A → ↑ A21/09 04:30
copumpkinmean that we'd sometimes need multiple arrows for that?21/09 04:30
copumpkinseems like the ⇑ arrow could automatically lift it as many times as needed21/09 04:30
copumpkinit wouldn't be quite as implicit as what you just said (I don't think)21/09 04:31
copumpkinbut might make it more pleasant21/09 04:31
dolioWell, if it's directly in the language, those are the only primitives you need to implement the arbitrary lifting versions.21/09 04:32
copumpkintrue21/09 04:33
dolioWhich might be the thought on why they have those explicit postulates: that you can define explicit universe manipulations in the language.21/09 04:34
dolioBut I don't know if you ever want to do that if it's mostly handled automatically, like in Coq.21/09 04:34
dolioSo, auto...21/09 04:36
dolioIf you're trying to prove m == n -> 1 + m == 1 + n21/09 04:36
dolioAnd you do "lemma refl = ?" and choose auto, it will figure out that "refl" should go in for the ?.21/09 04:37
copumpkinoh21/09 04:37
dolioSo my guess is that it fills in obvious solutions for types without eta laws.21/09 04:38
dolioWhere you can't just do _.21/09 04:38
copumpkinI guess that could be helpful21/09 04:38
dolioAuto is pretty limited.21/09 04:52
dolioIf I have 'foo a = ... ? ...' and 'a' is the right type to fill the hole, it doesn't use it.21/09 04:52
copumpkinah :/21/09 05:05
copumpkindo people do any time/space complexity of algorithms proofs using agda or coq?21/09 05:05
copumpkinI guess mostly coq since agda's quite young21/09 05:05
dolioI wouldn't be surprised if someone's tried it in Coq.21/09 05:06
copumpkinanders^^: you around?21/09 05:12
copumpkinprobably not awake if he's in sweden, I guess :)21/09 05:12
copumpkinI assume the CReal representation of reals isn't really suitable for reasoning about21/09 07:38
dolioI don't really know.21/09 07:44
dolioIt probably depends on what sort of reasoning you want to do.21/09 07:44
* copumpkin is tempted to ask roconnor for his initial haskell implementation of reals, that he then translated into coq21/09 07:46
dolioI think they're a bit more simplified than the definition of the reals for constructive analysis.21/09 07:46
dolioBut not that much.21/09 07:46
copumpkinin roconnor's paper, he said that he implemented them in haskell first21/09 07:47
copumpkinwhich might be a relatively painless translation into agda21/09 07:47
copumpkinat least for the basic implementation, not sure about properties of the reals21/09 07:47
dolioDo you have Integers to work with yet?21/09 07:49
dolioI guess we do.21/09 07:49
copumpkinyeah21/09 07:50
copumpkinand rationals21/09 07:50
dolioOh, and it's positive or negative natural. :)21/09 07:50
dolioCReal doesn't use rationals.21/09 07:50
dolioIt uses Natural -> Integer.21/09 07:50
copumpkinyeah21/09 07:50
copumpkinjust saying that we have rationals too if necessary for whatever representation :)21/09 07:50
dolioWhere f n / 2^n approximates the real to within 1/2^n, or something along those lines.21/09 07:51
copumpkinyeah21/09 07:53
dolioFull generality uses an additional function to determine the radius of convergence, I think.21/09 07:54
dolioRather than just setting it at 1/b^n.21/09 07:54
copumpkinI see21/09 07:54
dolioI guess Integers being Naturals underneath isn't that bad because Naturals are Integers underneath.21/09 07:59
copumpkinI found roconnor's implementation, don't fully understand his representation yet21/09 08:00
dolioAnd peano numbers are so much more luxurious than binary digits for proving.21/09 08:00
copumpkinyeah21/09 08:01
copumpkinthere is also a binary natural implementation in the std lib21/09 08:01
copumpkinnot sure how pleasant it is to work with though21/09 08:01
copumpkinhis basic real number type appears to be Rational -> Rational21/09 08:02
dolioHuh. I wouldn't have guessed that.21/09 08:02
dolioI guess that might be "given a radius of convergence, produce an appropriate approximation."21/09 08:03
copumpkinyeah, I think that's it21/09 08:03
copumpkinit seems to have various topological-sounding words that I don't understand in it :)21/09 08:04
copumpkinother than that, it seems relatively simple21/09 08:04
dolioHeh, lots of the proofs in the binary  numbers module convert to peano numbers and then use the proofs on those.21/09 08:07
copumpkinI don't blame them :) I dread to think of proving stuff directly on the binary representation21/09 08:08
dolioYeah.21/09 08:08
dolioDivision by 2 is easy, though.21/09 08:08
copumpkinand multiplication by any power of two21/09 08:12
dolioMultiplication by anything shouldn't be that bad. Just more adding.21/09 08:13
copumpkinyeah21/09 08:13
copumpkinanders^^: I was wondering why sum in Data.Vec was restricted to Nat21/09 19:34
anders^^copumpkin: maybe youre confusing me with someone else?21/09 19:41
copumpkinoh, maybe21/09 19:41
anders^^at least i dont know the answer21/09 19:41
copumpkinI thought you wrote the agda standard library :)21/09 19:41
anders^^copumpkin: hehe no21/09 19:41
copumpkinoh!21/09 19:41
anders^^I'm just reading a bit of agda in a course at chalmers21/09 19:42
copumpkinoh, I assumed that you were Nils Anders Danielsson from the mailing list :)21/09 19:44
anders^^:)21/09 19:45
-!- Saizan_ is now known as Saizan21/09 19:59
doliocopumpkin: I think the current rational module might be a little sparse for doing roconnor's reals.21/09 21:54
copumpkinwhat's missing? I'd be more than happy to work on expanding it21/09 21:55
dolioAll arithmetic operations. A constructor that generates the proofs rather than requiring them...21/09 21:55
dolioAnd proofs of stuff.21/09 21:56
dolioI don't know what all you'll need as far as proofs about rationals go.21/09 21:58
dolioq/2 + q/2 = q is one that looked like it'd be used a lot.21/09 21:58
dolioI just read the paper, though. I didn't look at the implementation.21/09 22:01
dolioInterestingly enough, his construction of the reals uses a monad, but it's a monad over the category of metric spaces, so it doesn't fit in a Haskell-like monad representation.21/09 22:05
dolioSo a more faithful embedding of category theory would be needed to talk about it.21/09 22:05
dolioOr fancy stuff using restricted monads or something.21/09 22:06
copumpkin:o21/09 22:32
copumpkinsounds like lots of fun to be had!21/09 22:33
copumpkinif nothing else it'll help me learn :)21/09 22:33
copumpkinI can definitely make the rational module suck a little less21/09 22:33
dolioYeah. That shouldn't be too hard.21/09 22:34
copumpkinnow if only I didn't have "real" work, dammit21/09 22:35
dolioOh, by the way, I think the purpose of stuff like "True <decidable predicate>" is so that you can write stuff like "bar <literal>" and have it work without proof.21/09 22:35
dolioHowever, it's a lot more of a pain when you want to want to work with inductively defined functions that work on the predicate that's being decided.21/09 22:37
copumpkinhmm, you mean like in the rational constructor?21/09 22:37
dolioBecause there are additional hoops to jump through to get from "True (P (Con foo))" to "True (P foo)" even if you know that P (Con foo) implies P foo and such.21/09 22:38
doliocopumpkin: Yeah, I mean you can write '3 <dividedby> 5' and it'll just work.21/09 22:38
dolioBecause it can fully compute the proofs for those.21/09 22:39
copumpkinah21/09 22:39
dolioWow, loading up Data.Rational for the first time takes a while...21/09 22:44
copumpkinyeah, it needs to compile dependencies I assume21/09 22:45
copumpkineven compiling the single Algebra.agda module takes a while21/09 22:46
copumpkinand lots of RAM21/09 22:46
dolio2 minutes 30 seconds and 25% ram so far.21/09 22:46
copumpkinI've had the background ghci process take up about 300 megs when I've been working on the std lib21/09 22:46
dolioProofs tend to take up a lot of time and space, too. And rational probably loads a lot of those with the gcd and coprimality stuff.21/09 22:47
copumpkinyeah21/09 22:47
copumpkinI'm really looking forward to writing more algebra for Algebra.agda21/09 22:49
copumpkinalmost feels like the module should be split up though, as it's getting quite large21/09 22:49
dolioYeah.21/09 22:49
copumpkinhttp://snapplr.com/vwq7 it's an owl!21/09 22:55
Saizan:D21/09 23:00
copumpkin:)21/09 23:01
copumpkinhttp://blog.sigfpe.com/2008/01/type-that-should-not-be.html looks like it could be implemented in agda?21/09 23:17
copumpkinI guess it would just get colored pink21/09 23:20
dolioWhich part?21/09 23:21
dolioYou can do Tree but not U.21/09 23:22
copumpkinyou can't even define U?21/09 23:22
dolioNope.21/09 23:22
dolioU is a negative type.21/09 23:22
dolioU allows you to construct non-terminating terms that the termination checked wouldn't catch.21/09 23:24
copumpkinah21/09 23:25
Saizane.g. data U = U (U -> U) is an embedding of the untyped lambda calculus, which let you define fix etc..21/09 23:27
doliocopumpkin: That is, I don't think you could come up with a checker that would correctly identify only the sort stuff in those blog posts. There's nothing directly self-referrential abou them.21/09 23:33
dolioBut it's easy to rule out the types that allow them to be well-typed in the first place.21/09 23:34
copumpkinhow do they rule it out? you can't refer to yourself to the left of a function arrow?21/09 23:36
dolioRight.21/09 23:36
dolioYou only allow strictly positive types.21/09 23:36
dolioOf course, that also rules out K r = (K r -> r) -> r, which I don't think admits the same kind of problems.21/09 23:37
copumpkinwhere does this positive and negative terminology come from for types?21/09 23:37
dolioI don't know where it comes from originally, but in 'a -> b' b is in the positive position, and a is in the negative position.21/09 23:38
dolioAnd in '(a -> b) -> c' c is strictly positive, b is negative, and a is positive, but not strictly positive.21/09 23:39
copumpkina is positive because it's twice negative?21/09 23:39
dolioSo, strictly positive types are only allowed to reference themselves in ways that are strictly positive.21/09 23:39
dolioRight.21/09 23:39
dolioI've not seen a language that disallows negative types but doesn't disallow non-strictly positive types.21/09 23:40
Saizanis there a paper on how the termination checker and type inference are implemented in agda?21/09 23:41
dolioThose might not have obvious induction principles, or something, so maybe it's simpler to rule those out, too.21/09 23:42
dolioFor the types, I think there's a paper called "Type Checking in the Presence of Metavariables" or something close.21/09 23:43
dolioUlf's thesis on Agda might talk about it, too.21/09 23:43
dolioThe termination checker probably has papers, too, but I don't know them. It's been rewritten once or more, too, and it slated to be rewritten again. :)21/09 23:44
* dolio should get going to dinner.21/09 23:44
Saizanheh21/09 23:44
copumpkinenjoy :)21/09 23:46
--- Day changed Tue Sep 22 2009
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9687#a968722/09 01:37
Saizanthat constructor can derive the proof from the other argument?22/09 01:40
dolioIt produces a fraction in lowest terms.22/09 01:41
dolioThe proof required by the rational representation comes from the gcd algorithm.22/09 01:41
dolioIt's kind of a pain to get in the right form, though, as you can see.22/09 01:42
dolio'proof' really threw me, too. If i don't explicitly state either P or Q for truthFromWitness, I get a type error.22/09 01:44
Saizani'm not sure how those | work, unless it's just an operator i don't know22/09 01:44
dolioIt's absolute value.22/09 01:44
dolioThat tripped me up, too, since it's not actually |, it's a unicode character that looks almost exactly like |.22/09 01:45
Saizanah.22/09 01:45
Saizanso Coprime ∣ sgn ◃ num' ∣ (suc den') is parsed as Coprime (∣ sgn ◃ num' ∣) (suc den') ?22/09 01:46
dolioYes.22/09 01:48
Saizanthe type error is quite weird too22/09 01:56
dolioYeah. Some implicit value isn't getting specified, but I don't know what it is, or what specifies it when I put in either P or Q.22/09 01:59
doliocopumpkin: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9687#a968722/09 02:25
dolioThere's a head's start for you.22/09 02:25
copumpkinyay, thank you :)22/09 02:26
copumpkininteresting module name :)22/09 02:26
dolioThanks.22/09 02:26
dolioI think build should allow you to write most of the arithmetic operations.22/09 02:28
copumpkingreat!22/09 02:34
copumpkinis that an anonymous record you have there?22/09 03:00
dolioIn build? That's how you construct records.22/09 03:09
copumpkinoh22/09 03:10
copumpkinaha, I see22/09 03:10
* copumpkin votes to kill the ◃ character in agda :P it's ugly22/09 04:36
dolioIt's not fun to type, either.22/09 04:42
vagHow to run typechecker without compiler? I need to time it.22/09 16:30
-!- jfredett is now known as jfredett-away22/09 18:36
stevanhi, i been reading the logs :-). copumpkin: here is some complexity analysis in agda: http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.html    dolio: here is some info on the new auto feature: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto   also have you concidered to collect the stuff you do in agda somewhere rather than just scattering it over hpaste :-)?22/09 21:52
dolioI have it all on my hard drive. :)22/09 21:52
copumpkinstevan: once I get something I'm reasonably satisfied with, I'd love to submit patches to the stdlib containing the matrix module I added, and several additional records for algebraic structures that aren't already there (as well as additional rational stuff)22/09 21:53
dolioAh, I was supposed to give it hints.22/09 21:55
doliostevan: http://code.haskell.org/~dolio/ <- there we go. I'll start putting my random experiments there, if you want to look at them. :)22/09 22:20
copumpkinooh, nice22/09 22:23
stevanawesome :-)22/09 22:23
Tobsanstevan: have you looked at the homework yet? should be a breeze for you, right?22/09 22:25
stevanutf8 seems messed up tho? http://code.haskell.org/~dolio/agda-share/Conat.agda   agda --html output would be nicer and solve the problem i guess22/09 22:25
copumpkinstevan: yeah, I had to ask my browser to treat it as utf822/09 22:25
dolioWell, I use konqueror, so that shows up in a text editor part and looks fine.22/09 22:26
dolioI guess code.haskell.org doesn't host its text files as if they're UTF8.22/09 22:27
dolioOr... That works in firefox here, too.22/09 22:28
stevanTobsan: hi :-), yeah i'm done... i had some problems with the first one... i expected the exercises to be harder... the ones we got in the first homework were harder for example...22/09 22:31
copumpkinyou two are taking a course on agda?22/09 22:31
Tobsanstevan: yes, the first ones were...hard :P. It took me 90 minutes to get the Standard Libraries in today heh22/09 22:31
stevannot really; http://www.cs.chalmers.se/Cs/Education/Courses/types/22/09 22:31
copumpkin:O22/09 22:33
* copumpkin wants one of those22/09 22:33
stevanyou can follow ours :-)22/09 22:33
stevandolio: if it isn't too much work, html output would be nicer; syntax highlightning + clickable definitions...22/09 22:34
stevanand utf8 wouldn't be a problem :-)22/09 22:35
doliostevan: What do I even use to make html? I seem to have missed whatever part of the install gives me an 'agda' executable to pass the --html flag to.22/09 22:46
copumpkincabal install agda-executable normally, but I wasn't able to find it when I grabbed the darcs version22/09 22:47
copumpkinnot sure where it comes from22/09 22:47
dolioHuh.22/09 22:47
stevanif you got the darcs version, cd into src/main and cabal install there aswell22/09 22:47
dolioAh, okay.22/09 22:48
dolioOkay, done.22/09 22:54
stevannice :-)22/09 22:54
copumpkinooh, and the .agda family in that folder grew too22/09 22:56
copumpkinif I wanted to express a "no zero divisors" property in agda, I'd write forall n. not (zerodivisor n), right? would not (exists n. zerodivisor n) work?22/09 23:02
stevanplenty of stuff missing still :-p, the soundness proof for propositional logic, the mod operator, the rational stuff :-)22/09 23:03
copumpkinoh, I mean assuming that zerodivisor existed22/09 23:04
copumpkinand mod is already there22/09 23:04
copumpkinwhere zerodivisor n might be forall m. n * m /= 022/09 23:14
stevanhmm, if you want to use the n later in the function for something i think you have to go with forall?22/09 23:14
copumpkinI'd need more restrictions on the values of n and m I guess22/09 23:17
dolioAll right. Added propositional logic with soundness theorem, and provable sorting of vectors.22/09 23:34
dolioDinner time.22/09 23:34
copumpkin:o22/09 23:35
stevancool, i just found an other proof for prop logic soundness: http://wiki.portal.chalmers.se/agda/uploads/Libraries.Sequent/Sound.agda22/09 23:37
copumpkinhmm, if I know that suc n is a Fin (suc m), is there an easy way to convince it that n is a Fin m ?22/09 23:54
copumpkinthe various injection functions in Data.Fin don't seem to cover that22/09 23:54
--- Day changed Wed Sep 23 2009
copumpkinhmm, I think I may have it23/09 00:16
dolioIsn't that true by definition of the suc constructor for Fin?23/09 00:28
copumpkinyep, I was just being dumb23/09 00:40
copumpkingot it working :)23/09 00:40
dolioWhat if you do pf : invertible {n} x?23/09 01:34
copumpkinperfect :)23/09 01:34
copumpkinthat makes sense23/09 01:34
dolioI'm not sure why the n vs. {n} would make a difference with that, though.23/09 01:34
copumpkinmaybe it bound the name invertible without it?23/09 01:35
copumpkin(ignoring the existing function)23/09 01:35
Saizan__ah, you should have put an -> before it, maybe23/09 01:35
dolioYou can't normally have strings of "(foo) (bar) (baz)", only "(f : foo) (b : bar) (bz : baz)".23/09 01:36
dolioSo I don't know why "(f : foo) {bar}" was working.23/09 01:36
dolioBut it was, without the nested {}s, apparently.23/09 01:36
Saizan__{bar} could have worked because of the forall23/09 01:37
Saizan__i'd be surprised about {bar x} though23/09 01:37
Saizan__a {bar} meaning {bar : _}, i mean23/09 01:37
dolioYes.23/09 01:38
dolioOh, maybe that was it.23/09 01:39
dolioIt was taking {invertible n x} to be {invertible n x : _}.23/09 01:39
dolioBut {invertible {n} x : _} it realizes is an error.23/09 01:39
Saizan__i didn't realize you could have higher order patterns like that23/09 01:40
dolioMaybe it's a bug?23/09 01:42
doliofoo : \all {a : Set} {b c} -> a -> a ; foo x = x23/09 01:42
dolioworks23/09 01:42
Saizan__aaah23/09 01:42
Saizan__so n and x are new bindings there23/09 01:42
dolioBut foo : \all {a : Set} (b c) -> a -> a is a prse error.23/09 01:42
Saizan__but \all {a : Set} b c -> a -> a works?23/09 01:43
dolioYes. invertible, n and x are all bindings.23/09 01:44
dolioYes that works.23/09 01:44
dolioI guess it's not a bug. Just weirdness.23/09 01:44
dolioOr, I wasn't expecting the \all to extend that far or something.23/09 01:45
Saizan__i think shadowing a binding in the same signature shouldn't be allowed23/09 01:45
dolioYeah, that seems like it'd be something you'd want caught.23/09 01:46
dolioI'll file a bug, I guess.23/09 01:47
Saizan__(b c) vs. {b c} is a bit surprising too23/09 01:48
Saizan__though there's no need to use "(b c)" instead of "b c"23/09 01:49
Saizan__but (b c : A) would work, right?23/09 01:49
dolioYes.23/09 01:52
dolioHmm...23/09 01:56
dolioBut what about \all {x} -> (\all x -> x -> x) -> x -> x?23/09 01:56
dolioThat has multiple scopes. Should shadowing still be disallowed?23/09 01:57
Saizan__mh, i'd say no23/09 01:57
Saizan__well, it's not as confusing as when one scope spans over the rest of the larger one23/09 01:59
Saizan__but i wouldn't really cry if that case was disallowed too23/09 01:59
dolioIssue submitted.23/09 02:14
copumpkindamn, I need sortedness23/09 02:35
copumpkinI think23/09 02:36
copumpkinmmm writing a permutations module could be fun23/09 02:40
dolioProving that two lists/vectors are permutations of one another is really hard work.23/09 02:41
copumpkinyeah, I'd imagine23/09 02:42
copumpkinI guess your sorting module covers some of that23/09 02:42
dolioI've tried a lot of representations, and the only one I ever succeeded with just took transitivity as an axiom.23/09 02:42
copumpkinhrm23/09 02:44
dolioBut I haven't looked at other proofs people have done much.23/09 02:44
dolioDoubtless you can find some Coq that has a successful proof.23/09 02:45
dolioOr maybe other people just take the same cop-out.23/09 02:45
dolio:)23/09 02:45
Saizan__write a function that computes the intensional equality for two terms of any type?23/09 02:46
Saizan__*can you23/09 02:46
dolioNo.23/09 02:46
Saizan__ok, it makes sense :)23/09 02:46
dolioYou can probably do it for any particular type that's built out of sums and products of various sorts.23/09 02:49
dolioBut anything that has a function in it will be a dead end.23/09 02:49
Saizan__ah, yeah, i didn't even took the possibility of functions into account23/09 02:50
* Saizan__ should get some sleep23/09 02:51
dolioCodata's a problem, too, because any inspection you can do of it won't tell you anything about intensional equality.23/09 02:51
Saizan__so when you code permutations you use a Setoid as the element of the lists/vectors, right?23/09 02:53
dolioWell, I suppose it depends what you want to do with permutations.23/09 02:54
dolioYou can prove that sorting is a permutation with respect to intenstional equality, for instance.23/09 02:54
dolioBecause you can construct proofs of where each particular element of the original ends up in the result, which doesn't involve deciding anything.23/09 02:55
dolioBut (T, intenstional-equality) is a setoid, just not necessarily a decidable setoid.23/09 02:56
dolioMan, I keep spelling intensional wrongly.23/09 02:58
Saizan__heh23/09 02:58
copumpkinokay, today is not the day to be writing matrix inversion in agda23/09 03:18
* copumpkin is trying to come up with good notation for accessing entire rows and columns of matrices23/09 03:29
copumpkinare predicates typically uppercase?23/09 03:45
copumpkinshould I write Invertible?23/09 03:45
dolioThe standard library uses uppercase for Set-valued stuff as a convention.23/09 03:50
dolioSo if <name> : Set, then <name> should be uppercased.23/09 03:51
copumpkinyeah23/09 03:51
copumpkinokay23/09 03:51
dolioAnd if <name> : B would lead <name> to be uppercased, then <name> : A -> B should be uppercased.23/09 03:52
copumpkinI see23/09 03:54
copumpkinthere doesn't seem to be a unary decidable thing23/09 03:55
copumpkinonly a nullary Dec and a binary Decidable23/09 03:55
dolioYeah.23/09 03:57
dolioI guess decidable relations are more commonly wanted than decidable unary predicates.23/09 03:59
* copumpkin finds himself tempted to write all sorts of useless helper functions for matrices23/09 04:58
copumpkinif I wanted to add a submodule of Data.Vec for typicaly "mathy" vector operations (dot product, vector addition, norm, and so on), what structure should I parametrize it over? a field seems obvious, but it seems like a ring should be sufficient23/09 05:39
copumpkinI guess I could just introduce vector space and/or module for it23/09 05:41
dolioRing, probably.23/09 05:41
dolioRings are good enough for modules.23/09 05:41
copumpkinyeah23/09 05:42
copumpkinif I call the record Module, is that confusing? should I call it R-Module? (pretty much everything I know about algebra I got from wikipedia, so I don't entirely trust myself :P)23/09 05:42
dolioIt's been a while since I studied modules.23/09 05:43
copumpkinor _-Module :O23/09 05:43
copumpkinokay, anyway I can rename stuff later if it bothers people more knowledgeable than myself23/09 05:44
dolioI mean, vector spaces/modules in general don't depend on anything like the vector type/matrices.23/09 05:45
copumpkinyeah23/09 05:45
copumpkinI just wanted to write an "instance"23/09 05:45
copumpkinfor the concrete vector type23/09 05:45
dolioAs it happens, R-module is an actual term.23/09 05:49
dolioAt least as far as An Introduction to Rings and Modules With K-theory in View is concerned.23/09 05:49
copumpkinsounds good23/09 05:50
dolioIn fact, there are both right and left R-modules.23/09 05:51
dolioAnd then R-S-bimodules.23/09 05:52
copumpkinI had left and right23/09 05:52
copumpkinwhat's S-?23/09 05:52
dolioDifferent ring.23/09 05:52
copumpkinoh23/09 05:52
copumpkinany ideas on how to represent the fact that a vector space has a field, and two "carriers" for scalars and vectors, both over that field?23/09 05:53
copumpkinI was thinking of a function23/09 05:53
copumpkinsomething like http://snapplr.com/fzt423/09 05:54
copumpkinoh, fieldCarrier should probably be : Field23/09 05:54
dolioIsn't a vector space a group and a field?23/09 05:55
dolioAlso, fieldCarrier -> Set is one Set for each element of fieldCarrier.23/09 05:56
copumpkinah, hmm23/09 05:56
copumpkinI was just trying to tie them together as depending on the same underlying field23/09 05:57
copumpkinI can do something like record VectorSpace {f : Field} : Set₁ where23/09 05:58
dolioA vector space is, as I recall, a group of vectors, and a field of scalars, with various operators for interaction between them.23/09 05:58
dolioAnd where matrices come in is linear (?) transformations.23/09 05:59
copumpkinyeah23/09 05:59
copumpkinbut only on the F^n kind of vectors, I guess23/09 06:00
dolioWell, you can tease F^n vectors out of abstract vector spaces.23/09 06:01
dolioLike you can tease matrices out of abstract linear transformations.23/09 06:01
dolioBecause v : F^n can be taken to mean Sum g_i * v_i where g_i are some suitable basis elements of the group.23/09 06:02
copumpkinyeah23/09 06:03
dolioAssuming finite dimensionality, of course.23/09 06:04
copumpkinyeah23/09 06:04
copumpkinhttp://snapplr.com/xe1p this feels overcomplicated :(23/09 06:15
copumpkinand ugly with all the duplicated symbols23/09 06:16
copumpkinmaybe I can do something nicer with the modules23/09 06:16
dolioIs that how Ring and such work?23/09 06:17
copumpkinyeah, but not nearly as packed with stuff23/09 06:17
dolioHmm...23/09 06:17
dolioShouldn't scalarIsField and vectorIsGroup go in the fields?23/09 06:19
copumpkinoh yeah23/09 06:19
dolioI don't think there's much getting around it. Vector spaces just have a lot of stuff in them.23/09 06:19
copumpkinit seems like I should be able to "open" the two constituent structures without duplicating everything23/09 06:20
dolioYeah, but not without bumping the universe level or parameterizing by the structures.23/09 06:21
copumpkinah23/09 06:21
copumpkinmaybe I can just come up with something nicer than all those \^1s for the scalars23/09 06:22
dolioI think part of the reason why the Algebra modules are arranged the way they are is to keep everything at Set1.23/09 06:22
copumpkinprobably23/09 06:24
copumpkinbah, I hate naming things23/09 06:32
copumpkinthe VectorSpace record looks a lot less messy if I group the vector-specific operations, the scalar-specific ones, and then the combination one23/09 06:32
-!- Tobsan_ is now known as Tobsan23/09 07:27
copumpkinwell, I think this just about covers it: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9726#a972623/09 07:28
copumpkinthere needs to be an algebrapedia like byorgey's typeclassopedia :)23/09 07:29
copumpkin    noZeroDivisors    : ∀ x y → ¬ (x ≈ 0#) → ¬ (y ≈ 0#) → ¬ ((x * y) ≈ 0#) seems reasonable, right?23/09 07:49
dolioYeah.23/09 07:53
dolioYou should definitely define an alias for not-equal, though. :)23/09 07:54
copumpkinI wanted to, but I wasn't sure where to put it, since my record introduces _~~_ as a parameter23/09 07:55
copumpkinhttp://snapplr.com/1dpk23/09 07:55
copumpkinI guess I don't need FunctionProperties there23/09 07:56
copumpkinmaybe I should expand FunctionProperties to be more flexible23/09 07:56
dolioYou can put it before "field"23/09 07:57
copumpkinah cool23/09 07:58
copumpkinis there a good way of resolving circular module dependencies?23/09 08:00
copumpkinI wanted to express unique factorization with Data.Vec but it already requires algebra indirectly and forms a circular dependency23/09 08:01
dolioProbably not. There's something in Data.Vector that says it's only there because it depends on Data.Fin.23/09 08:02
copumpkinah :/23/09 08:03
copumpkinhmm23/09 08:03
copumpkinI'd just define a local copy of the vector structure, but then it'd make it even more painful to prove this than it already is23/09 08:04
dolio:)23/09 08:04
copumpkinI was just going to say that forall xs ys x. x !~ 0 -> x !~ 1 -> product xs ~~ product ys ~~ x -> xs ~~ ys23/09 08:05
copumpkinI guess I could use n-ary functions23/09 08:07
copumpkinoh and I guess I couldn't use Vec anyway23/09 08:10
copumpkinbecause it's ordered23/09 08:10
copumpkinand allows multiple elements23/09 08:11
* copumpkin is basically walking through wikipedia's algebra pages and defining all the structures he can find... rather sad thing to be doing in the middle of the night :P23/09 08:27
copumpkinI've got algebras over rings/modules and fields now, as well as lie algebra23/09 08:28
copumpkinif I can't get reals working easily, if nothing else, I can work with polynomials :)23/09 08:32
copumpkinand have fun with fields23/09 08:32
dolio:)23/09 08:33
copumpkindammit, I wish I'd taken more math, or were in a program where I could bullshit my way into taking more pure math23/09 08:34
yakovhey23/09 09:11
-!- Saizan__ is now known as Saizan23/09 13:35
copumpkinanyone seen http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html ?23/09 17:54
copumpkinmeh, http://snapplr.com/a4ef :(23/09 19:12
copumpkinthe error is http://snapplr.com/s17k23/09 19:14
copumpkinit's odd, cause the type it claims it isn't, is exactly what the proj2 is supposed to show23/09 19:16
copumpkin:(23/09 20:11
copumpkinI can't figure out why this isn't working, in my context I have n + 0 == n, but it still complains that n != n + 023/09 20:12
--- Day changed Thu Sep 24 2009
dolioI don't think that blog post really gives the whole story.24/09 00:18
Saizanis there some way to show the types of bound variables in scope in some hole?24/09 01:17
copumpkinif you right click on the hole and ask for the context24/09 01:18
Saizanright click?24/09 01:18
copumpkinC-c C-e works too24/09 01:18
copumpkindid that work?24/09 01:20
Saizanyup24/09 01:21
copumpkinI seem to have a bajillion refls in scope24/09 01:21
copumpkinit's annoying24/09 01:21
dolioI'm not sure what to make of this free theorem stuff.24/09 01:21
Saizani don't get to see both the type of the hole and the context at the same time, but that's ok i guess24/09 01:21
copumpkinthe types in that were amazingly long24/09 01:21
copumpkinC-c C- it says24/09 01:22
copumpkinfor both goal and context24/09 01:22
copumpkinnot sure how you type that :P24/09 01:22
copumpkinanyone know what's going on with http://snapplr.com/f537 ?24/09 01:23
copumpkinoh24/09 01:24
copumpkinit didn't catch the tooltip24/09 01:24
copumpkinn + 0 != n of type ℕ when checking that the pattern Core.refl has type n + 0 ≡ n24/09 01:24
Saizan:t n+0=n ?24/09 01:25
copumpkinn+0≡n : ∀ x → (x + 0) ≡ x24/09 01:25
dolioUse subst24/09 01:25
copumpkinsubst₁ : ∀ {a} (P : a → Set₁) → ∀ {x y} → x ≡ y → P x → P y ?24/09 01:26
copumpkinsubst₂ : ∀ {A B} (P : A → B → Set) →24/09 01:26
copumpkin         ∀ {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂24/09 01:26
doliosubst1 is if you're predicate is into Set1.24/09 01:27
dolioThere should be a subst for normal Set.24/09 01:27
copumpkinaha24/09 01:27
dolioAnd subst2 is for binary relations, which ruins the whole naming scheme.24/09 01:27
copumpkinx' ≡ y → P x' → P y24/09 01:27
Saizanthough i don't completely get why you don't have a similar error when defining subst, or is it just because with is not magic enough?24/09 01:28
copumpkinthe official type is subst : {a : Set} → Substitutive {a} _≡_, but that isn't very clear24/09 01:28
dolioI think it's P -> x == y -> P x -> P y, so you'll need to provide P.24/09 01:29
SaizanP x == P y24/09 01:29
dolioforall P -> ... even24/09 01:29
copumpkinhmm24/09 01:29
dolioNo, P x == P y is cong.24/09 01:29
copumpkinhmm24/09 01:30
Saizanah, true24/09 01:30
copumpkinso much indirection in this code!24/09 01:30
copumpkinhttp://snapplr.com/p1h924/09 01:30
Saizansubst (\n -> ...) (n+0=n n)24/09 01:30
copumpkinI mean, code reuse :P24/09 01:30
dolioYes. P Respects _~_ means x ~ y -> P x ~ P y.24/09 01:31
doliof Preserves _~_ --> _~~_ means x ~ y -> f x ~~ f y.24/09 01:31
copumpkinmakes sense24/09 01:32
dolioCongruential _~_ means all endomorphisms f preserve _~_24/09 01:33
dolioOr, I guess it's not endomorphisms.24/09 01:33
dolioIt's just that _~_ works on all Sets.24/09 01:34
Saizanbtw, what do you think about defining Permutation xs ys = length xs == length ys , Subset xs ys , Subset ys xs ?24/09 01:36
Saizantransitivity should be easy for that24/09 01:36
dolioHow is Subset defined?24/09 01:38
dolioIt's not always transitivity where I run into a problem, if I recall correctly.24/09 01:39
dolioIt's just that the one proof structure I managed to prove everything with, I took transitivity as an axiom, because that's what I couldn't prove for it (and I needed it).24/09 01:40
SaizanSubset xs ys = All (λ x → Some (_==_ x) ys) xs24/09 01:40
dolioOther formulations I may have had trouble proving other useful properties (like symmetry, for instance), which I could also have assumed, but that makes me equally unhappy.24/09 01:41
dolioWell, that doesn't work, actually, because then [1,1,2] and [1,2,2] are considered permutations.24/09 01:41
copumpkinthe anonymous variables are annoying24/09 01:42
dolioAnyhow, my point is that defining a Subset that captures the necessary conditions will probably be no less difficult than Permutation directly.24/09 01:42
copumpkinit accepted this http://snapplr.com/3hek24/09 01:46
copumpkinbut that _ is bad24/09 01:46
copumpkinI thought (Vec carrier) would be a good thing to put for the _24/09 01:47
copumpkinbut it didn't like it :(24/09 01:47
dolioSaizan: In fact, I've probably tried something similar to that.24/09 01:49
dolioLike "step : x \in xs -> x \in ys -> remove x xs ~ remove x ys -> xs ~ ys"24/09 01:50
dolioI've also tried "y \in xs -> x \in ys -> xs ~ ys -> x :: xs ~ y :: ys".24/09 01:51
copumpkinalmost got it!24/09 01:57
copumpkinit's all really weird though :P24/09 01:58
copumpkinmerge {n} xs [] = subst (Vec carrier) { }0 []24/09 01:59
copumpkinit says the hole has shape 0 == n + 024/09 02:00
copumpkinbut if I put n+0==0 n in that hole24/09 02:00
copumpkinit doesn't like it24/09 02:00
copumpkinI mean n+0==n24/09 02:00
copumpkinoh24/09 02:00
copumpkinthat's bad24/09 02:00
copumpkinmeh :)24/09 02:02
dolioIf the hole is n = n + 0, then you probably need symmetry, since n+0=n presumably has type n + 0 = n24/09 02:02
copumpkinno, the hole is actually 0 == n + 024/09 02:02
dolioWell...24/09 02:02
copumpkinoh I see24/09 02:02
copumpkinmeh, nope, I can't prove that24/09 02:02
copumpkinI thought n had to be 0, but it doesn't24/09 02:03
dolioSomething weird is going on, then, unles n = 0.24/09 02:03
copumpkinoh silly me24/09 02:04
copumpkinmerge {n} xs [] = subst (Vec carrier) {!!} xs is what I really meant24/09 02:06
copumpkinthe hole there is n == n + 024/09 02:06
Saizanthen you need "sym (n+0==n n)"24/09 02:08
copumpkinomg24/09 02:08
copumpkinI didn't realize it didn't know == wasn't symmetric :)24/09 02:09
Saizanin a sense it does know since it let you write sym24/09 02:09
copumpkinI just need to reassure it24/09 02:10
copumpkinso much overlap in my symbols :(24/09 02:19
* copumpkin needs some of the private properties in Data.Nat.Properties :)24/09 02:25
copumpkincrap, I got me some pink24/09 02:32
copumpkinhttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9762#a976224/09 02:48
copumpkinit'd be nice if it gave more of an indication of where the pink is coming from24/09 02:49
doliocopumpkin: I think I've seen this come up before, but I don't remember what the problem is exactly, or how to fix it.24/09 02:54
copumpkinyay, merge Data.Nat.decTotalOrder (1 ∷ 2 ∷ 5 ∷ []) (2 ∷ 3 ∷ []) works find24/09 02:56
copumpkinfine24/09 02:56
copumpkingives me 1 ∷ 2 ∷ 2 ∷ 3 ∷ 5 ∷ []24/09 02:57
-!- byorgey_ is now known as byorgey24/09 02:59
* Saizan_ realizes he has never evaluated an expression in agda24/09 02:59
copumpkin:)24/09 03:00
dolioIf you look hard enough, you can probably find it on the mailing list.24/09 03:00
dolioBut I'm not exactly sure what to look for.24/09 03:00
doliocopumpkin: I think the problem is in having the 'with' along with only being verifiably structurally recursive when two arguments are considered.24/09 03:01
doliowith causes a new anonymous function to be declared, so to the termination checker, it looks something like...24/09 03:02
dolio"merge ... = aux (x :: xs) (y :: ys) ; aux (x :: xs) (y :: ys) = ... merge xs (y :: ys) ... merge (x :: xs) ys24/09 03:02
dolioSo it has trouble telling that you aren't adding one and then subtracting it back off forever or something.24/09 03:03
copumpkinah, hmm24/09 03:04
copumpkinshould my merge demand a proof of sortedness for its parameters? or should I just claim that the result will only be sorted if the inputs are sorted24/09 03:10
dolioDepends. There are, roughly speaking, two ways to do any particular proof.24/09 03:14
dolioEither you can write your functions 'f : (x : T) -> P x -> \Sigma T' Q' or 'f : T -> Q ; prop-f : \all x -> P x -> Q (f x)'24/09 03:15
copumpkinyeah24/09 03:16
copumpkinI think that's what I'll do here, probably24/09 03:16
dolioOops, I messed up the types in the second part. Anyhow.24/09 03:17
copumpkinsometimes these holes seem less informative than they could be24/09 03:25
copumpkinI have a hole that claims it just needs Nat -> Set24/09 03:25
copumpkinbut I've given it plenty of Nat -> Set functions and it barfs every time24/09 03:25
copumpkinRelation.Unary still feels rather neglected compared to Nullary or Binary24/09 03:38
dolioHah! Figured it out!24/09 04:08
copumpkinfigured which one out?24/09 04:08
copumpkinsorting?24/09 04:08
doliohttp://code.haskell.org/~dolio/agda-share/html/Free.html24/09 04:08
copumpkinoh that one :)24/09 04:08
copumpkincool24/09 04:12
copumpkinis the fact that it can't determine that merge terminates a bug, or an accepted limitation?24/09 04:38
dolioI'm not sure how accepted it is.24/09 04:43
dolioThere might be a work-around.24/09 04:44
copumpkinI rather like how simple the function looks right now24/09 04:45
copumpkinI'm scared of writing anything big in case the proof gets ridiculously hard because of it :P24/09 04:45
-!- Tobsan_ is now known as Tobsan24/09 07:03
copumpkinwow, compiling Rational.agda ate up 600 MB of RAM24/09 18:16
copumpkindolio: I think peer may have it in for you by the way... he keeps resetting your connection24/09 18:16
Saizanhave you tried compiling Everything.agda all at once?24/09 18:29
copumpkinnope :)24/09 18:30
copumpkinhave you?24/09 18:30
Saizanyeah, i had to wait a while :)24/09 18:30
danr@hoogle getLine24/09 18:31
danr@type getLine24/09 18:31
danr:(24/09 18:31
* copumpkin can't get dolio's rat code to compile :(24/09 18:48
danroh. sorry, wrong channel for lambdabotting24/09 18:50
copumpkingotta love agda, http://snapplr.com/6c3h24/09 18:52
danr:D24/09 18:53
copumpkinbuild sgn num          den with gcd′ num den build sgn .(num' ℕ* d) .0 {} | d , gcd-* {.d} num' 0 cop24/09 19:37
copumpkinagda's ghci is up to over a gig of RAM :P24/09 19:51
* copumpkin can't figure out what's wrong with that :(24/09 20:16
* copumpkin curses24/09 20:23
vixeyhttp://article.gmane.org/gmane.comp.lang.agda/1038 awesome!!!!!24/09 20:25
vixeyesp. Peter Hancock24/09 20:25
copumpkin:)24/09 20:26
vixey?24/09 20:26
copumpkinit does look cool24/09 20:27
vixeystevan that them ?24/09 20:28
vixeySaizan did you find the OTT code?24/09 20:28
vixeypretty sure it's on coq-club24/09 20:28
vixeydolio "It is clearly quite wasteful to have both Fin n and m < n when they obviously have the same structure. :)"24/09 20:30
vixeyif you can make an isomorphism we can share proofs :P24/09 20:30
vixeyI think that will be important in big developments24/09 20:30
copumpkinis there a magic order of hiding, using, and renaming?24/09 20:32
copumpkinI can't get any of them to work24/09 20:32
vixeyyeah that free theorem in agda stuff doesn't make any sense24/09 20:32
copumpkinyay, got dolio's build working :)24/09 20:38
copumpkindumbest reason ever it wasn't working24/09 20:38
copumpkinand agda's error message wasn't very helpful24/09 20:38
vixeywhat build?24/09 20:38
copumpkina builder function for Data.Rational24/09 20:40
vixeyoh24/09 20:40
copumpkinthe existing one wants a proof that the numerator and denominator are coprime24/09 20:41
vixeyhow is rational defined?24/09 20:41
copumpkinwhereas his function reduces it24/09 20:41
vixeyguck24/09 20:41
copumpkinit's an integer over a natural24/09 20:41
vixeyyou know euclid algorithm?24/09 20:41
vixeyfor computing GCD24/09 20:41
copumpkinhe's using it24/09 20:41
copumpkinwell, there's a GCD algorithm already in the std lib24/09 20:41
copumpkinand he's using that24/09 20:41
vixeybut you know the algo inside out yeah?24/09 20:42
copumpkinpretty much24/09 20:42
copumpkinwhy?24/09 20:42
vixeyso lets say  GCD(n,d) = 124/09 20:42
vixeyand invert the algorithm,24/09 20:42
vixeyyou get GCD(n+d,d) = GCD(n,n+d)24/09 20:43
vixeythere's always two things you can do: and every pair of numbers with GCD 1 is reached this way (because the algorithm is total)24/09 20:44
copumpkininteresting24/09 20:44
vixeyso you can define rational numbers as:   data Q = One | N Q | D Q24/09 20:44
vixey(positive)24/09 20:45
copumpkinthat sounds like it would be more elegant than the current representation24/09 20:45
vixeytry to prove that sqrt(2) isn't in  Q24/09 20:45
copumpkinrecord ℚ : Set where   field     numerator     : ℤ     denominator-1 : ℕ     isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1))24/09 20:45
vixeyYuck :P24/09 20:47
vixeywhy the hell is that called 'True"24/09 20:47
vixeyone thing I reall hate in math (not just type theory) is when people say  "X is true"  rather than just saying  "X"24/09 20:48
copumpkinit converts a Dec back to a type statement of truth24/09 20:48
copumpkinif that makes sense24/09 20:48
copumpkindata Dec (P : Set) : Set where24/09 20:48
copumpkin  yes : ( p :   P) → Dec P24/09 20:48
copumpkin  no  : (¬p : ¬ P) → Dec P24/09 20:48
vixeywhen you want to go from 2 -> Prop though use spandau ballet24/09 20:48
vixeyI think True is a terrible name but doesn't really matter I guess24/09 20:49
copumpkinmaybe :)24/09 20:51
copumpkinbring it up with the author of the library!24/09 20:51
vixeynah I don't care about Agda24/09 20:51
copumpkinaw24/09 20:52
copumpkinwhat do you care about?24/09 20:52
vixeyIt's way too ad-hoc the only worthwhile thing are what people think when they use Agda24/09 20:52
vixeyon the Wish-List nobody mentions De-Bruijn Criteria24/09 20:52
vixeymaybe we should ditch decidible type checking too?24/09 20:52
-!- mode/#agda [+o vixey] by ChanServ24/09 20:58
-!- mode/#agda [-o vixey] by vixey24/09 20:58
mahognyooh24/09 21:00
-!- byorgey_ is now known as byorgey24/09 21:00
vixeymahogny it's a quite lively and good channel somehow !24/09 21:05
vixeyeven though it's about some esoteric research lang :P24/09 21:05
mahognywill stay :)24/09 21:05
mahognyhm. seem to be some chalmers people here <324/09 21:06
-!- Saizan_ is now known as Saizan24/09 23:15
--- Day changed Fri Sep 25 2009
-!- jfredett_ is now known as jfredett25/09 00:42
doliocopumpkin: build wasn't working as it was?25/09 01:31
copumpkindolio: it was me being stupid as usual :) the error wasn't very clear, but I thought I had imported Data.Product and hadn't, so it couldn't parse the comma25/09 01:56
dolioAh.25/09 01:59
copumpkinI started adding some arithmetic, anyway25/09 02:02
* copumpkin is trying to prove no zero divisors for integers25/09 02:12
copumpkinas I'm pretty sure I need it for rational multiplication25/09 02:12
copumpkinactually, just naturals25/09 02:12
* copumpkin used his first _|_-elim25/09 02:27
copumpkin!!25/09 02:28
copumpkindamn, so close!25/09 02:51
copumpkinhmm, I have something that is obviously false, but I'm not sure how I can produce a bottom to satisfy it25/09 02:56
copumpkinyet it isn't obvious enough that an absurd pattern is enough25/09 02:56
dolioThere's only two ways to "produce a bottom."25/09 03:01
dolio\x -> x where x is a bottom.25/09 03:01
dolioAnd \()25/09 03:01
dolioI suppose it could be '\x -> f x' where f produces a bottom from whatever x is.25/09 03:02
copumpkinyay, the lambda () worked :)25/09 03:02
copumpkinhttp://snapplr.com/h6d3 yay25/09 03:04
copumpkinit's probably more complicated than it needs to be25/09 03:04
dolioLooks about right.25/09 03:05
dolioYou could put the x/=0 before the y so you don't need to use {y = y}.25/09 03:05
copumpkinoh, neat25/09 03:06
copumpkinyou making the proofs implicit is silly?25/09 03:07
copumpkinI guess it can infer them some of the time25/09 03:07
copumpkinhmm, so I have a blah == 0 -> _|_, and need a False (blah == 0)25/09 03:19
copumpkinI can't see how to go in that direction25/09 03:19
dolioYeah. You might need to write another one of thise "witnessFromTruth" type things I wrote.25/09 03:19
copumpkinoh25/09 03:19
copumpkinthere's already one in Relation.Nullary.Decidable25/09 03:20
dolioThat goes from True (Dec (Foo)) to Foo.25/09 03:20
copumpkinoh yeah :)25/09 03:20
dolioYou need Not Foo -> False (Dec Foo)25/09 03:21
dolioI needed Foo -> True (Dec Foo)25/09 03:21
dolioThat's why those True/False things suck. :)25/09 03:21
copumpkinyou'd think there'd be one in the library25/09 03:21
copumpkinso the Dec stuff is just so you can get some sort of value-level indication of truthiness, right?25/09 03:28
dolioDec is for deciding predicates.25/09 03:28
dolioI mean, strictly, it's just a sum type that hold either a proof of a proposition or a proof of its negation.25/09 03:29
dolioBut that's the sort of thing you get back from a decision procedure for a predicate.25/09 03:29
copumpkinyeah25/09 03:30
Saizani was wondering, when you write code splitting properties from the actual functions, the proof of the property often has to follow the definition of the function to be accepted, isn't this a potentially big problem for modularity?25/09 03:36
dolioYeah, dependent types don't really buy you modularity.25/09 03:40
Saizani guess you can't prove much about code without looking at it25/09 03:43
doliohttp://www.cs.cmu.edu/~rwh/courses/modules/index.htm25/09 03:44
dolioThe lecture on dependent typing goes over how dependent typing doesn't really model abstraction well.25/09 03:45
Saizanthat looks like a great course25/09 03:49
dolioYeah.25/09 03:49
copumpkinthey have a real world haskell user!25/09 03:56
copumpkinit does sound fun25/09 03:58
copumpkinif only I'd know this stuff was so cool when I was applying to grad school :P25/09 03:58
copumpkin*known25/09 03:58
copumpkinnot that I'd have gotten into CMU anyway25/09 03:59
copumpkinonoes, my proof be yellow25/09 04:24
copumpkinhttp://snapplr.com/zweg25/09 04:24
dolioYeah, in build, didn't I have to apply it to the implicit {True ...} thing?25/09 04:26
dolioIt actually caused an error in my case when I didn't specify one of the implicit arguments.25/09 04:28
dolioKind of an undesirable situation.25/09 04:30
dolioI'm kind of skeptical of the merits of using 'True (coprime? | n | d)' in the first place.25/09 04:34
dolioAnd 'False (d ==? 0)' I guess.25/09 04:35
copumpkinyeah25/09 04:35
copumpkinmehh25/09 05:17
copumpkinoh wow, it didn't need the no zero divisors property at all25/09 05:22
copumpkinI guess for naturals, it's a pretty obvious property :)25/09 05:24
copumpkinwow, I tried multiplying two rationals25/09 05:28
copumpkinit's taking forever :P25/09 05:28
dolioHeh.25/09 05:30
copumpkinyay, it got the right answer!25/09 05:30
dolioWhich two rationals?25/09 05:30
copumpkin5/4 and 6/825/09 05:31
copumpkinboth built25/09 05:31
copumpkinusing your function25/09 05:31
copumpkinit gave me a numerator=15, denominator-1=1525/09 05:31
dolioWow, those aren't even big.25/09 05:33
copumpkinyeah, I tried computing it again just to make sure it wasn't random25/09 05:34
copumpkinbut it's taking forever again25/09 05:34
copumpkinmaybe the evaluator hasn't had much attention25/09 05:34
copumpkinrather disconcerting that it takes that long to compute, but I guess all I care about is the proof! :D25/09 05:56
copumpkincan I pattern match on records?25/09 05:57
dolioNo.25/09 05:57
vixeyis there a way to search github for all agda code?25/09 12:35
doliovixey: FYI, there's a note in passing in the AIMX notes about a desire to define a core theory for Agda.25/09 12:43
vixeycool25/09 12:44
dolioDe-Bruijn criterion presumably being one of the reasons.25/09 12:45
vixeyI thought that's what Agda-light was about25/09 12:46
Tobsanhow do i get to interactive mode in agda?25/09 14:16
Tobsanlike if i want to evaluate an expression25/09 14:16
kosmikusTobsan: C-c C-n in emacs25/09 14:32
Tobsanthanks kosmikus!25/09 14:35
dolioMan, I'm not sure keeping Agda-generated html in darcs is a good idea.25/09 15:04
kosmikuskeeping generated files under version control is almost never a good idea25/09 15:22
dolioYeah.25/09 15:23
doliocode.haskell.org doesn't have Agda on it, though. :)25/09 15:24
Tobsanhas anyone tried compiling agda on a gentoo amd64 system?25/09 15:31
dolioI use an ubuntu amd64 system. Is there a reason that'd be seriously different?25/09 15:33
dolioOh, I suppose I haven't 'compiled' anything, either. I just use the emacs mode.25/09 15:34
Tobsanmy build fails when linking the type-checker25/09 15:41
Tobsanor "agdachecker"25/09 15:41
TobsanI might try doing this with cabal25/09 15:44
Tobsanalright, so if you're on a amd64 system on gentoo, use cabal instead of portage to install agda25/09 15:49
copumpkindolio: maybe if you include a .htaccess in your repo with a .agda utf-8 content type that would save you from having to generate .html files?25/09 17:05
copumpkinat least it would serve up the files as they were intended to be seen25/09 17:05
copumpkinyay universe polymorphism!25/09 17:17
EnglishGenthi copumpkin25/09 18:43
EnglishGent:)25/09 18:43
vixeyanyone figured out this paramtricity stuff?25/09 18:47
vixeyhttp://www.nabble.com/An-encoding-of-parametricity-in-Agda-td25577620.html25/09 18:47
vixeyI still don't get t25/09 18:47
copumpkinvixey: dolio said he'd figured it out25/09 18:48
copumpkindid anyone see the article posted to the dependent types reddit on representations of integers?25/09 20:01
copumpkinor I guess just a mailing list post :)25/09 20:02
vixeyno25/09 20:02
vixeyI read it on agda list25/09 20:02
copumpkinah25/09 20:02
vixeynot sure why it's posted to reddit25/09 20:02
vixeybecause it wasn't very interesting :/25/09 20:02
vixeyunless I missed something?25/09 20:02
vixeyΠΣ: A Core Language for Dependently Typed Programming (pdf)25/09 20:03
vixeythat's not ancient?25/09 20:03
vixeywhat's going on this reddit lol25/09 20:03
copumpkinI dunno, interesting to you, a seasoned programming language / type theory person, and me, a complete newbie, might be quite different :)25/09 20:03
copumpkingotta run25/09 20:04
--- Day changed Sat Sep 26 2009
-!- opdolio is now known as dolio26/09 00:13
doliovixey: http://code.haskell.org/~dolio/agda-share/html/Free.html26/09 00:17
vixeyah26/09 00:18
vixeyyeah I don't really knwo what everyone is doing with this stuff26/09 00:18
vixeynobody defined a term syntax with evaluation function26/09 00:18
dolioI sent an e-mail to coq-club/haskell-cafe with more explanation in it, too.26/09 00:18
vixeyI did read that26/09 00:18
vixeyI just don't know why people are trying to show parametricity for the WHOLE language (which is obviosly impossible) rather than picking a subset (like Simple Typed Lambda Calculus)26/09 00:19
dolioWell, I don't think parametricity is very useful for simple types.26/09 00:20
vixeyrather than picking a subset _which it is actually provable for_26/09 00:20
vixeyoh sorry yes your completely right I should say some polymorphic calc26/09 00:21
dolioSystem F is where it gets useful, because there are quantifiers over types.26/09 00:21
vixeyyeah without the forall you get nothing26/09 00:21
dolioBut, you can't prove that quantifying over Set is parametric in Agda from within Agda.26/09 00:22
dolioEven though there's no type-case or anything.26/09 00:23
vixeyI'm not sure what you mean ?  if you define a language you should be able to prove polymorpism for terms in that language26/09 00:23
vixeyI'd do this in Coq but (1) it's hard (2) no eta26/09 00:23
vixeywithout canonical proofs of eta things I can't get reduction so the whole thing wont go through26/09 00:24
dolioYeah, if you define your own language and interpreter embedded in Agda, you can probably do it.26/09 00:24
vixeywhat strikes me as bizarre is that he didn't do that :P26/09 00:24
vixeyThe proofs are so long and complicated I haven't figured out what (if anything) it's actually showing26/09 00:25
dolioI'm saying you can't prove that agda functions \all A -> A -> A have a parametricity result from within Agda.26/09 00:25
dolioEven though they are parametric.26/09 00:25
vixeyyes I absolutely agree & that's what I meant earlier about "obviosly impossible"26/09 00:25
* vixey now wonders just how to show that it's impossible ...26/09 00:26
dolioAs far as I can tell his blog post is just about how to reprent the 'type relations' involved nicely. But maybe I'm actually missing something, because his mail seems to say there's more to it than that.26/09 00:26
dolioSo, what do you think? Should I rebuild agda and rework the category theory stuff I've been doing to use the experimental, limited universe polymorphism?26/09 02:33
dolioOr stick with --type-in-type for now?26/09 02:33
copumpkinthe new stuff sounds like it could be coo26/09 02:34
copumpkinl26/09 02:34
vixeyis there a repo?26/09 02:35
copumpkinyep26/09 02:35
doliohttp://code.haskell.org/~dolio/agda-share/categorica/26/09 02:35
vixeythanks26/09 02:35
copumpkinhttp://code.haskell.org/Agda26/09 02:35
dolioI don't have much yet.26/09 02:35
copumpkinoh :)26/09 02:35
dolioAnd I need to rework sums/products, because I realized while I was trying to get to sleep last that my definition of products is a specification of a category that has all binary products.26/09 02:36
copumpkinthis looks nice :)26/09 02:37
copumpkinwhat is Star by the way? I saw it in the standard library too26/09 02:37
dolioOf course, that leads to other issues, like should the specification for a product be parameterized by the two objects? By the product object?26/09 02:38
copumpkinhah, we have Nat, Rat, Mat, and Cat26/09 02:41
vixeyyikes26/09 02:41
vixeypeople should try to use the full names26/09 02:41
copumpkinI like the postfix (co)product26/09 02:48
copumpkinis there any heterogeneous list-like structure in the standard library?26/09 02:53
copumpkinI was thinking of reworking the algebra module significantly!26/09 02:59
copumpkinto do crazy things26/09 02:59
copumpkinhaven't quite decided how to go about it yet though26/09 03:01
doliohttp://code.haskell.org/~dolio/agda-share/categorica/Category/Product.agda <-- what about that?26/09 03:22
-!- copumpkin is now known as pumpkin26/09 04:56
* pumpkin is trying to make Data.Rational less painful to typecheck26/09 05:36
pumpkinit takes 15 or 20 seconds every time I try to typecheck it26/09 05:37
pumpkinmaybe more26/09 05:37
pumpkinis dependent type compilation inherently "whole-program"?26/09 05:56
Saizan_it shouldn't need to retypecheck things already typechecked26/09 05:57
pumpkinyeah, but the compiler essentially knows the structure of all the code in all the modules it loads26/09 05:58
Saizan_in fact it saves data in dot-files26/09 05:58
pumpkinthere are .agdai files26/09 05:58
pumpkinI was trying to cut out the largest ones cause compilation is so slow26/09 05:58
Saizan_yeah, that what i was referring to yesterday, it has to know the implementation of each function, in case you want to prove something about it somewhere else26/09 05:59
pumpkinyeah26/09 05:59
pumpkinseems like it has the potential for amazing optimizations26/09 06:00
pumpkinbut is also so complicated26/09 06:00
dolioThere may be ways to hide stuff.26/09 06:08
dolioThere's an "abstract" keyword.26/09 06:08
dolioBut I don't really know what it does.26/09 06:08
pumpkinah26/09 06:09
dolioAh, abstract does hide the definition.26/09 06:13
dolioWhereas private prevents it from being directly exported, but it may still show up during reduction.26/09 06:14
-!- pumpkin is now known as copumpkin26/09 07:42
dolioPreorderReasoning is pretty sweet.26/09 08:31
dolioMy proofs are too big.26/09 12:16
dolioThey're using all my memory.26/09 12:16
vixeycategory theory proofs?26/09 12:29
dolioYes.26/09 12:30
dolioI'm half way through proving A x (B x C) is isomorphic to (A x B) x C26/09 12:31
dolioOr, almost half way.26/09 12:32
vixeyI can't think of anything that would help reduce the size26/09 12:35
vixeysince reflection probably doesn't apply here- that wouldn't help26/09 12:35
vixeyyou can't make stuff opaque either..26/09 12:36
dolioWell now I don't know what's going on. I shut down and reloaded emacs, and now it doesn't even finish type checking.26/09 12:56
dolioAh, apparently I'm overflowing the GHC stack somehow.26/09 13:24
dolioWell, the proof definitely types. But apparently the type checker can't verify that with everything filled in (as opposed to in goals) without using 75% of my memory and then overflowing the stack.26/09 14:29
vixey:/26/09 15:25
Saizandolio: in that course on modularity, they seem to consider dependent sums and esistentials quite different, with the first one not providing abstraction26/09 16:29
Saizandolio: but that's essentially because in their formalism you've typecase over small types i guess?26/09 16:29
Saizanthough dependent sum could still have eta laws..26/09 16:36
Saizanactually, how do i specify that i want the record to be of type \Sigma a p here?26/09 17:05
Saizan {a : Set} {p : a -> Set} {x : a} {v : p x} -> Σ.first (record{ first = x; second = v}) ≡ x26/09 17:05
Saizanah, solved26/09 17:07
copumpkindolio: I run into the same problem just modifying existing standard library modules26/09 17:21
copumpkinI wonder if the proofs just get really large or if it's a space leak26/09 17:34
copumpkinomnomnom26/09 18:00
FunctorSalad_copumpkin: eating is allowed in here? :o26/09 18:00
copumpkinyep26/09 18:01
* jmcarthur sips coffee26/09 18:01
copumpkinFunctorSalad_: omnomnom26/09 18:04
vixeyyou can't eat in here, this is the agda room!26/09 18:05
copumpkinoh, whoops26/09 18:05
copumpkinsorry!26/09 18:05
FunctorSalad_so we were wondering whether you can reason about haskell code in agda?26/09 18:05
jmcarthurcan use agda to reason about haskell code?26/09 18:05
jmcarthurgrr26/09 18:05
FunctorSalad_maybe by translation from haskell to agda26/09 18:05
FunctorSalad_of course nontermination would be a first obstacle26/09 18:06
vixeyFunctorSalad_: there's a paper on it in ACM dunno if you can access that26/09 18:06
vixeynot totally sure if it's the best approach26/09 18:06
Saizando you remember the name?26/09 18:07
vixeyno26/09 18:07
vixeyIt's called Verifying haskell programs using constructive type theory26/09 18:08
FunctorSalad_http://citeseerx.ist.psu.edu/viewdoc/download?doi= 18:08
FunctorSalad_thanks vixey26/09 18:09
FunctorSalad_hmm is that paper out of date about agda not enforcing totality?26/09 20:03
Saizanyou can disable the termination checker with a flag26/09 20:08
FunctorSalad_Prood: fix id \qed26/09 20:09
FunctorSalad_*Proof26/09 20:09
FunctorSalad_gotta try that in homework....26/09 20:10
copumpkinis | and \| the exact same glyph?26/09 22:16
copumpkinthey look identical to me, but one gives a syntax error and the other works26/09 22:17
Saizanno they aren't26/09 22:17
Saizan| is reserved i think26/09 22:17
copumpkinyeah, I mean26/09 22:17
copumpkinthey're not the same character but they have the same glyph26/09 22:17
Saizan\| is some unicode char that looks like it26/09 22:17
Saizanoh, they look differently in my font26/09 22:18
copumpkinhttp://snapplr.com/4d2f that's both of them, side by side :P26/09 22:18
Saizan\| is a little shorter26/09 22:18
* Saizan doesn't remember how to take a screenshot26/09 22:19
* copumpkin wants circular imports in agda26/09 22:19
copumpkinit's preventing me from defining unique factorization domains in algebra26/09 22:20
Saizanmutual doesn't work for modules, i guess?26/09 22:21
copumpkinwell, my problem is that I'd like to import a Map/Set/Multiset module to define unique factorization26/09 22:23
copumpkinnot sure how else to do it26/09 22:23
copumpkinnot even sure how to do it with a map structure26/09 22:24
copumpkinmaybe I should build it with a Vec26/09 22:24
copumpkineven then, I still can't import Data.Vec because it makes a circular import26/09 22:25
copumpkinhm26/09 22:26
copumpkinany ideas on how to express unique factorization without depending on something external?26/09 23:02
copumpkin(and not duplicating code)26/09 23:02
FunctorSalad_copumpkin: hmm there are some properties not involving lists which are equivalent26/09 23:05
copumpkinwell, you can also say that every nonzero nonunit element is a product of primes26/09 23:05
copumpkinbut that's also "setty"26/09 23:06
FunctorSalad_http://en.wikipedia.org/wiki/Unique_factorization_domain#Equivalent_conditions_for_a_ring_to_be_a_UFD26/09 23:06
copumpkinseems like I'd need a lot of support code to express any of thos26/09 23:08
copumpkine26/09 23:08
FunctorSalad_"every irreducible is prime" is quite elementary26/09 23:09
FunctorSalad_but there's still this ascending chain condition26/09 23:09
copumpkinyeah26/09 23:09
copumpkinhmm26/09 23:10
FunctorSalad_and I suppose you want the /explicit/ unique factorization anyway ;)26/09 23:10
FunctorSalad_you could use lists and say "unique up to permutation"26/09 23:10
FunctorSalad_or unique ordered list26/09 23:10
FunctorSalad_if the ring is orderd, anyway26/09 23:10
copumpkinwell I was planning to express it as forall xs ys. product xs == x -> x /= 0 -> x /= 1 -> product ys == x -> xs == ys26/09 23:11
copumpkinor something like that26/09 23:11
FunctorSalad_yes, but the last (==) has to be up to permutation26/09 23:12
FunctorSalad_(and you must ban units in the list)26/09 23:12
FunctorSalad_hmm and the primes can differ by units too :)26/09 23:12
copumpkinwell I can't use the standard library lists because of circular imports26/09 23:13
copumpkinFunctorSalad_: oh well I was envisioning the product take a MultiSet or something like that26/09 23:14
copumpkinbut we don't have such a module anyway26/09 23:14
copumpkinto avoid the issue of permutations26/09 23:15
FunctorSalad_copumpkin: map of (primes) to nat?26/09 23:15
FunctorSalad_(with all but finitely many values zero)26/09 23:15
copumpkinI guess that would be complicated too, eh26/09 23:15
copumpkinhmm26/09 23:16
FunctorSalad_is it reasonably easy to work with equivalence relations in agda?26/09 23:17
copumpkinnothing much is easy for me at this point, so I can't really comment :)26/09 23:20
--- Day changed Sun Sep 27 2009
-!- koninkje1away is now known as koninkje_away27/09 02:19
-!- opdolio is now known as dolio27/09 03:08
dolioSaizan: I don't fully grok the difference between weak and strong sums (existential and dependent sums).27/09 03:09
dolioSaizan: But strong sums somehow let you get a hold of the first parameter in a way that weak sums don't.27/09 03:10
FunctorSalad_the eliminators are different27/09 03:10
dolioI guess that may be it.27/09 03:10
FunctorSalad_with strong sums the type of the return value can depend on the value of the contents, or something27/09 03:10
FunctorSalad_sig_rect27/09 03:11
FunctorSalad_     : forall (A : Type) (P : A -> Prop) (P0 : sig P -> Type),27/09 03:11
FunctorSalad_       (forall (x : A) (p : P x), P0 (exist P x p)) -> forall s : sig P, P0 s27/09 03:11
FunctorSalad_(that's in coq, sorry I don't have an agda handy)27/09 03:11
FunctorSalad_so the P0 (the elimination thingy) can depend on x and p27/09 03:12
dolioYeah.27/09 03:12
dolioI seem to recall you can't encode strong sums in CoC without them.27/09 03:12
FunctorSalad_(but I'm not completely sure that that is the difference)27/09 03:13
dolioBut weak sums are easy.27/09 03:13
FunctorSalad_("sig" is sigma type there, and "exist" is its constructor)27/09 03:13
dolioOh, I see why.27/09 03:17
Saizanweak sums are just {a b : Set} {p : a -> Set} -> ((x : a) -> p a -> b), which indeed prevents you from mentioning x in b27/09 03:20
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a987927/09 03:20
Saizanops, .. -> b27/09 03:21
copumpkinwe need an hpaste that does agda html27/09 03:21
dolioglguy's mused about adding it to hpaste2, but I'm not sure if he's working on it or not.27/09 03:22
FunctorSalad_or AGDABOT?27/09 03:22
copumpkinmmm27/09 03:23
dolioIt's a bit harder to do something in one line of agda than in one line of haskell.27/09 03:23
FunctorSalad_hmm27/09 03:24
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a9881 <- i've found quite surprising that x typechecks there27/09 03:24
Saizanbut now i see how strong sums are really transparent27/09 03:24
dolioSaizan: Anyhow, that inability of the eliminator result to depend on A in weak sums gets you more 'abstraction' than with strong sums, I think.27/09 03:24
dolioEven though you can't really inspect the type stored in 'Sigma Set T' in any way.27/09 03:26
dolioWithout type case and whatnot.27/09 03:26
Saizanyup, i think i get it now27/09 03:26
dolioIt's like a parametricity result, rather than a "what programs can I practically write, but the type system doesn't necessarily guarantee" result.27/09 03:27
Saizanbtw, can you write a Sigma that can contain both types and values as the first field depending on how you instance it?27/09 03:27
dolioSigmas that contain types are kind of a pain in agda, because they live in Set1.27/09 03:28
dolioUniverse polymorphism fixes that, though. Then there can be one sum that's parameterized by the level.27/09 03:29
Saizanyeah, but since we're talking about modules i'd expect that27/09 03:29
dolioWell, I just mean if you want to do it all with sigmas, you need a Sigma1 and a Sigma0 right now.27/09 03:30
dolioOf course, records are 'just' sugar for a string of sigmas. :)27/09 03:30
Saizanah, no data Sigma (U : ?) (A : U) (A -> Setn) : Setn where .., where 'n' is some fixed one, then?27/09 03:31
dolioOh, well, that third paramater can't have that type. It needs to be...27/09 03:32
Saizani mean, there's no valid thing i can put in place of ? so that i can have U = Set and U = Set127/09 03:32
dolioSigma (U : ?) (A : U) ((A : U) -> A -> Setn) ...27/09 03:33
dolioOh. Hmm.27/09 03:33
dolioWell, you can have ? = Set2, but that's pretty non-specific.27/09 03:34
dolioOr you can use an explicit universe 'data MySets : Set where MySet : MySets ; MySet1 : Mysets ; up : MySets -> Set2 ; up MySet = Set ; up MySet1 = Set1'27/09 03:36
dolioThen Sigma (U : MySets) (A : up U) ...27/09 03:36
Saizanuhm, doesn't seem to work with Set227/09 03:38
dolioWell, it's going to have to be at least Set2 as a result.27/09 03:38
dolioI think that's true of both encodings.27/09 03:39
dolioMaybe the second can go down to Set1.27/09 03:39
ecstdolio: interestingly, records in agda seem (according to documentation) to be subject to eta-convertiblity; i wonder if this is really necessary in practice27/09 03:40
dolioI don't think it's necessary. It's useful, though.27/09 03:41
dolioOrdinary data not being subject to eta can be kind of a pain.27/09 03:41
copumpkinhow would I define a simple heterogeneous list in agda?27/09 03:42
dolioDefine a list of types, and then parameterize by that.27/09 03:43
dolioOr, index by that, I should say.27/09 03:43
copumpkinas in the existing List\_1 ?27/09 03:43
dolioYes.27/09 03:43
copumpkinaha27/09 03:43
Saizandolio: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=9879#a988227/09 03:44
dolioOh. Yeah, forget that version.27/09 03:45
dolioIt's not going to work because A isn't necessarily a type.27/09 03:46
Saizanit's weird that it complains about it not being (A : Set1), and not (A : Set) though27/09 03:48
dolioOh crap, the universe one doesn't work, either, because Set :/ Set2.27/09 03:49
Saizanah, i thought it did27/09 03:50
dolioIt's still strict containment. Set : Set1, Set1 : Set2 ...27/09 03:50
Saizanok, no single sigma for me27/09 03:51
dolioI must say, it's weird that the slides for translucent sums use 9 for the existential quantifier.27/09 03:53
Saizanyeah. i already noticed an 8 in some of the previous ones27/09 03:56
FunctorSalad_I'd use 100000 to be safe ;)27/09 04:03
FunctorSalad_the space could vanish quickly if you put new things into the middle..27/09 04:04
* copumpkin seems to have written a circular data type that is impossible to type (if I make it of type Set, it wants Set1, if I make it of type Set1, it wants Set2, and so on)27/09 04:05
copumpkinI wonder if this new universe polymorphism thing can help me here27/09 04:11
copumpkinor whether my definition is just flawed27/09 04:12
ecstwhat did you do?27/09 04:12
copumpkinhttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=9883#a988327/09 04:13
copumpkinI assumed it would have to live in Set1 because the properties are in Set27/09 04:13
copumpkinbut no Setn seems to work27/09 04:13
copumpkinoh duh27/09 04:15
copumpkinI'm just stupid, sorry27/09 04:15
copumpkinI forgot to pass the parameters to the Property return type27/09 04:16
ecstsome question: i tried to formalize a bit of category theory in agda, but quickly ran into the problem of typechecking taking time (and space!) exponential to the amount of code i had written; i suspect this is the result of me consistently mixing "data" and "properties" in the same record types (i hoped the typechecker would be "lazy enough" to deal with this, but apparently not)27/09 04:18
copumpkinecst: dolio was just complaining about his CT stuff taking forever too27/09 04:18
copumpkinyesterday27/09 04:18
ecsti realize most library examples avoid this by separating "data" and "properties" into different records27/09 04:18
dolioYeah. My module for product no longer type checks.27/09 04:19
ecstbut is there a way the aleviate this and continue writing in a "mathematical" style (grouping data and properties together)?27/09 04:19
dolioIs that why the standard libraries are organized that way?27/09 04:20
ecstit seems27/09 04:20
dolioI'll have to try that.27/09 04:20
ecsti have yet to find out how to do this separation while not introducing significant amounts of code overhead27/09 04:22
ecstin particular in regards to equivalence relations emulating extensional equality27/09 04:24
dolioYeah, well, I decided to scrap using setoids as the basis for categories pretty quickly.27/09 04:27
dolioI just stuck a postulate for extensionality in my equality module.27/09 04:27
ecsthow dare you??27/09 04:27
dolioBecause having the arrow construction produce a setoid makes composition pretty heinous.27/09 04:28
ecst;)27/09 04:28
dolioAnd I'm sure it would only get worse from there.27/09 04:28
ecstwell, i took that path (though i need extensionality only for category morphism), and it definitely got worse27/09 04:31
ecstbut i still think it is the typecheckers fault27/09 04:31
FunctorSalad_but you will need quotients one day27/09 04:31
FunctorSalad_quotients have been neglected by type theory in general :(27/09 04:32
ecsti thought setoids subsume quotients27/09 04:32
FunctorSalad_yes27/09 04:33
FunctorSalad_I meant without setoids27/09 04:33
ecstah27/09 04:33
FunctorSalad_support on the computational level would be nicer presumably27/09 04:34
ecsthm, dunno, i am a purist :)27/09 04:35
ecsti really have no problem manually emulating this stuff low-level if only the typechecker would behave27/09 04:35
dolioI don't think this splitting is helping much.27/09 04:58
ecstthen i am at a loss as for the reason27/09 04:58
ecstthe point where i was stuck (as to computer resources) was the definition of prefixing a natural transformation with a functor27/09 05:04
ecstthis was the first time that the result of a function depended on something like (compose-functors F G)27/09 05:05
ecstresult -> result type27/09 05:05
ecstwhich of course involved a proof that the functor properties hold for the composition, but which is irrelevant for the function being defined27/09 05:05
FunctorSalad_hmm maybe you can relax your properties to hold up to isomorphism27/09 05:06
FunctorSalad_prefixing a NT with a functor is a special case of horizontal composition of NTs...27/09 05:06
dolioI doubt that'll make Agda use less memory.27/09 05:06
FunctorSalad_^^27/09 05:07
FunctorSalad_thought the problem was still equality27/09 05:07
ecstno, it is the typechecker using exponential resources for non-exponential problems27/09 05:07
FunctorSalad_fire up the profiler?27/09 05:08
ecstthere is a profiler? where can i find it?27/09 05:09
FunctorSalad_I don't know if agda has one of its own, but you could compile agda with profiling27/09 05:09
FunctorSalad_then agda +RTS -P27/09 05:09
FunctorSalad_?27/09 05:09
ecstwell, i am no haskell hacker :(27/09 05:09
copumpkinmaybe post the mailing list about it?27/09 05:17
dolioI think I will. I'll at least ask if the std-lib is structured the way it is to avoid performance problems.27/09 05:18
copumpkinthe current algebra module is rather painful to use, unless I'm missing something27/09 06:04
copumpkincan I close a module after opening it?27/09 06:15
dolioYou can open it within a scope.27/09 06:18
dolioLike creating a new (nested) module and opening in there, for instance.27/09 06:19
copumpkinah27/09 06:19
copumpkinI was hoping to be able to do that within a data declaration, but it just gave me a parse error27/09 06:19
copumpkinI'll try doing it in a module27/09 06:19
copumpkinis there the equivalent of newtype in agda?27/09 07:38
dolioNo.27/09 07:41
dolioActually...27/09 07:41
copumpkin:o27/09 07:47
doliohttp://code.haskell.org/~dolio/agda-share/html/Newtype.html27/09 07:49
copumpkinoh that's neat :)27/09 07:50
dolioAnything that needs to know that they're the same type has to go on that abstract block.27/09 07:50
copumpkinyeah27/09 07:52
copumpkin_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor27/09 07:55
copumpkinit seems odd for it to require divisor to not be zero27/09 07:56
copumpkinsince Fin 0 is empty anyway27/09 07:56
dolioYeah, but that means it's impossible for you to produce a Fin 0.27/09 07:56
copumpkinyeah, but doesn't that effectively say you can't pass a zero divisor in the first place?27/09 07:57
copumpkinmaybe I'm confusing notness27/09 07:57
dolioNo, you can pass whatever you want.27/09 07:57
dolioWithout the proof, it would have to give you back a Fin 0.27/09 07:58
copumpkinI thought a proof of not p was p -> empty type, and fin 0 was an empty type27/09 07:58
dolioWith it, when you write 'n mod 0' it gives back {False (0 == 0)} -> Fin 0.27/09 07:58
copumpkinor rather, a statement of not p27/09 07:58
copumpkinhmm27/09 07:58
dolioAnd when you provide it with that proof that 0 == 0 is false, it will provide you with a Fin 0.27/09 07:59
dolioBut you can never provide it with the proof, of course.27/09 07:59
copumpkinso the issue is that it doesn't fundamentally know that Fin 0 is empty27/09 08:00
dolioNo, it does.27/09 08:00
copumpkinso say you have (with no proof this time) _mod_ : (dividend divisor : ℕ) → Fin divisor, and write _mod_ 5, which should have type (divisor : ℕ) → Fin divisor27/09 08:02
dolioYes.27/09 08:02
copumpkinwhen divisor is 0, that looks very much like divisor == 0 -> _|_27/09 08:02
copumpkinbut I guess it isn't explicitly that27/09 08:04
dolioSo, suppose I call it with 0. Where are you going to get the Fin 0 from?27/09 08:06
dolioYou must return one.27/09 08:06
copumpkinyeah, I see27/09 08:06
dolioIf you have a bottom already, you can use that.27/09 08:06
dolioWhich is what the (False (n == 0)) gives you.27/09 08:06
copumpkinyeah27/09 08:06
copumpkinnow, if I have a member of Fin n, can I extract trivially that False (n ?= 0)?27/09 08:07
dolioWell, as trivially as writing a function and doing case analysis, because working with that False stuff is kind of a pain.27/09 08:08
copumpkinah well, it's simple enough I guess :)27/09 08:10
dolioYou need two cases anyway, I suppose.27/09 08:11
dolioEven if it were just a proof of n /= 0.27/09 08:11
copumpkinyeah27/09 08:11
copumpkinit was so simple that even I wrote it with no effort at all :P27/09 08:11
copumpkinI'm writing modular arithmetic and polynomials27/09 08:14
dolioThe False stuff just expands one of the cases into a with.27/09 08:14
copumpkindoes http://snapplr.com/7qgp look weird for a type name?27/09 08:34
copumpkinI'm not sure why people call it Z/ instead of N/27/09 08:34
dolioPrejudice against the natural numbers.27/09 08:35
dolioLooks fine to me.27/09 08:36
copumpkinall over wikipedia they actually say Z/_Z, but that felt really cumbersome to write27/09 08:36
dolioZ mod Z?27/09 08:37
copumpkinZ/nZ27/09 08:37
dolioOh right.27/09 08:37
dolioI couldn't think of a very nice way to define arithmetic on Fin n directly.27/09 08:39
copumpkinthe stuff in Data.Fin is rather ugly, yeah27/09 08:39
copumpkinhmm, I wonder if I can pull the extended euclidean algorithm out of the GCD stuff27/09 08:45
dolioOf course, it's pretty easy with a Σ m:ℕ m<n implementation.27/09 08:48
copumpkinnow to decide if I want to perpetuate this True (decidablething) tradition27/09 08:56
copumpkinDecidable ShouldUseTrueAndDecidableOnMyPredicates27/09 09:09
doliohttp://code.haskell.org/~dolio/agda-share/html/FinLT.html27/09 09:16
copumpkinthat's quite nice :)27/09 09:17
copumpkinyou should propose that as a replacement for the existing Fin!27/09 09:18
dolio:)27/09 09:18
copumpkinnow we can move on to our plan for world domination, by proving the correctness of several crypto algorithms, with epic unary aritmetic on large numbers27/09 09:20
copumpkin(muahahahahahaha)27/09 09:20
dolioNow that I think about it, since the two types are pretty much isomorphic, there's probably an analogue to <-dec for Fin.27/09 09:23
dolioWhich will let you write modular arithmetic on it.27/09 09:24
copumpkinI've been doing it the hard way with mod so far27/09 09:24
copumpkinbut it's really ugly :)27/09 09:24
dolio+ and * anyway.27/09 09:24
dolio- is easy with fromNat.27/09 09:25
dolioAnd, of course, / is some complicated problem in number theory that I don't remember, I'm sure.27/09 09:25
copumpkinI have all the basic ones except for _^-127/09 09:25
copumpkinwhich I need the extended euclidean algorithm for27/09 09:26
copumpkinand the GCD module doesn't seem to export anthing useful along those lines27/09 09:26
copumpkineven though it seems to use some form of it internally27/09 09:26
dolioReally?27/09 09:27
dolioWhat results do you need (d, m', n') such that m = d * m' and n = d * n'?27/09 09:27
copumpkinnot necessarily the same d, if I understand what you mean27/09 09:29
copumpkinoh, I guess I didn't27/09 09:30
copumpkinyou mean d is the common divisor27/09 09:30
dolioYes.27/09 09:30
copumpkinyeah, except here the common divisor is just 127/09 09:31
copumpkinhere, http://en.wikipedia.org/wiki/Modular_multiplicative_inverse#Extended_Euclidean_Algorithm27/09 09:32
copumpkinso what I have is _⁻¹ : ∀ {n} → (x : ℤ/ n) {coprime : True (coprime? n (toℕ x))} → ℤ/ n27/09 09:33
dolioHave you looked in the coprimality module?27/09 09:34
dolioOne of those two have some kind of Bezout type.27/09 09:34
copumpkinoh, it's in the GCD module27/09 09:35
copumpkinthat looks promising27/09 09:35
copumpkinanyway, bedtime, ciao :)27/09 09:36
dolioNight.27/09 09:36
-!- opdolio is now known as dolio27/09 10:06
doliohttp://code.haskell.org/~dolio/agda-share/html/MFin.html success.27/09 10:06
-!- opdolio is now known as dolio27/09 10:52
copumpkindolio: that's neat27/09 19:27
dolioMan, a lot of categories seem to have pretty arduous encodings in type theory.27/09 19:36
FunctorSalad_hmm my last attempt in coq wasn't that bad27/09 19:37
FunctorSalad_which ones, dolio ?27/09 19:37
dolioWell, I tried to do the category of categories.27/09 19:37
FunctorSalad_should be a 2-cat :)27/09 19:37
dolioThat involves proving 'composition' of records that contain proofs equal.27/09 19:37
dolioAnd I was just doing slice. That also involves proving that proofs are equal.27/09 19:38
FunctorSalad_you need proof_irrelevance27/09 19:38
vixeyeverything is arduous in type theory27/09 19:38
FunctorSalad_vixey, as compared to what?27/09 19:38
FunctorSalad_have you become disillusioned?:(27/09 19:38
vixeycompared to writing python scripts or whatever27/09 19:38
FunctorSalad_:)27/09 19:39
vixeyor drawing pictures of cats27/09 19:39
dolioSo I expect anything involving "morphisms in Foo are morphisms in Bar with some property" to be a pain.27/09 19:40
FunctorSalad_dolio: isn't there some analogue of proof_irrelevance in agda?27/09 19:40
dolioNot really.27/09 19:40
FunctorSalad_that sounds like a problem27/09 19:40
dolioThere's a flag --proof-irrelevance, but I don't think it's very well developed.27/09 19:40
FunctorSalad_OTOH you might want to use setoids anyway27/09 19:40
dolioYeah, I started with setoids.27/09 19:41
dolioThen I realized that composition was going to look like "{A B C} -> (carrier (B => C)) -> (carrier (A => B)) -> (carrier (A => C))"27/09 19:43
FunctorSalad_hmm? in coq you can have it be "forall {A B C}, (B => C) -> (A => B) -> (A => C)" and require each (X => Y) to be an instance of Setoid27/09 19:59
FunctorSalad_(forall {A B}, Setoid (A => B))27/09 20:00
FunctorSalad_(the carrier type isn't wrapped inside the setoid)27/09 20:00
FunctorSalad_then you also require the composition to be respectful w.r.t. the setoids27/09 20:01
FunctorSalad_(again, the function is not wrapped in the respectfulness ("Proper") instance, it's a param)27/09 20:02
dolioHmm, after some experiments, --proof-irrelevance may make things somewhat easier.27/09 20:02
FunctorSalad_does agda have typeclasses or some other automatic way to find Eq/Ord/Setoid/etc. instances for a given type?27/09 20:03
dolioNo.27/09 20:03
dolioHmm, except you can't have equality of equalities if equalities live in Prop (since it takes Sets).27/09 20:08
dolioAlso, --type-in-type appears to turn off --proof-irrelevance. :)27/09 20:09
-!- FunctorSalad_ is now known as Semilettuce27/09 22:00
-!- copumpkin is now known as DistributiveLett27/09 22:03
-!- DistributiveLett is now known as copumpkin27/09 22:04
--- Day changed Mon Sep 28 2009
-!- opdolio is now known as dolio28/09 04:35
-!- opdolio is now known as dolio28/09 08:33
dolioSo, now, Agda type checks my code without using 75% memory and overflowing the haskell stack.28/09 08:35
kosmikusdolio: you removed 75% of your code? :)28/09 08:36
dolioI don't think so. :)28/09 08:37
dolioOh wait...28/09 08:39
dolioI did change one thing in the branch that made it work...28/09 08:39
dolioNope, that wasn't it...28/09 08:48
dolioWell now I'm totally at a loss. Apparently turning equality from Set to Prop, turning on proof irrelevance, reloading everything, then turning it back to Set and reloading everything caused it to work.28/09 08:53
dolioWhereas just loading it as Set from the get-go doesn't.28/09 08:53
dolioNope, that doesn't seem to be working, either.28/09 09:00
dolioAh hah!28/09 09:13
-!- EnglishGent is now known as EnglishGent^afk28/09 09:22
dolioEvidently my problem was that I needed to put a {C} in when opening/using a module in a couple places.28/09 09:40
dolioWithout that {C}, it uses at least 3x the memory and overflows the stack. :)28/09 09:40
-!- EnglishGent^afk is now known as EnglishGent28/09 10:24
-!- FunctorSalad_ is now known as FunctorSalad28/09 16:54
-!- codolio is now known as dolio28/09 19:12
copumpkinwhat is proof irrelevance?28/09 20:14
copumpkinI found http://www.cs.cmu.edu/~fp/courses/15317-f08/lectures/08-irrelevance.pdf but the language in it is a bit over my head28/09 20:14
Saizan_it means that all the proofs for a certain proposition are considered equal28/09 20:16
Saizan_you clearly don't want that if the proposition has computational content28/09 20:16
Saizan_s/a certain/any/28/09 20:17
copumpkincomputational content? as in, "does something"? the difference between stating that a number is composite and returning its factors?28/09 20:17
dolioP \/ Q has computational content (typically), because you can inspect the proof and decide to do a different thing depending on whether you receive a proof of P or a proof of Q.28/09 20:19
copumpkinoh28/09 20:19
dolioIf proofs have no computational content, then you get the same results no matter what proof is used.28/09 20:20
Saizan_yeah, you usually encode \/ with /\ and negation, i guess?28/09 20:21
dolioThat might be one way.28/09 20:21
dolioIf you can take quotients, that might be another.28/09 20:21
dolioSmash (P \/ Q) would be okay, I guess.28/09 20:21
--- Day changed Tue Sep 29 2009
* copumpkin shifts his agda to his macbook pro with more RAM and a heftier CPU29/09 01:05
-!- pumpkin is now known as copumpkin29/09 04:29
-!- anders^^ is now known as boefst__29/09 18:01
-!- byorgey is now known as axnqfdx29/09 18:27
copumpkinhas anyone looked into dependent types + subtyping?29/09 19:53
doliohttp://www.cs.rhul.ac.uk/~zhaohui/subtyping.html29/09 20:09
dolioDid that get through/29/09 20:12
copumpkinthanks, yep :)29/09 20:12
dolioI haven't read any of his stuff yet.29/09 20:13
dolioHe's a big name in type theory, though.29/09 20:13
copumpkincool29/09 20:13
dolioLots of people reference his book and UTT type theory, but I don't think there's any way to get it.29/09 20:13
dolioHis thesis and other stuff on ECC is widely referenced, too.29/09 20:14
copumpkinZ. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, 11. Oxford University Press, 1994. (ISBN 0 19 853835 9)29/09 20:14
copumpkinthat one?29/09 20:14
copumpkinI guess the other one is in chinese29/09 20:14
dolioYes.29/09 20:14
copumpkinooh, there's a copy in the library29/09 20:15
dolioI should say, I happen to be looking at a paper he co-authored now trying to get a handle on universe polymorphism (hopefully).29/09 20:15
copumpkinwow, it's expensive on amazon29/09 20:15
dolioWow, it's still in print, even.29/09 20:16
dolioUnfortunately, books like that end up being ridonkulously expensive due to the limited interest.29/09 20:17
copumpkinyeah :/29/09 20:18
copumpkinyou could probably steal it off google books29/09 20:18
copumpkinwould take some effort though29/09 20:18
dolioThey randomly blank out pages and stuff, don't they?29/09 20:18
copumpkinoh, yeah :/29/09 20:18
FunctorSaladgoing to implement universe polymorphism?29/09 20:19
dolioI'm just trying to get a handle on what's been done in that regard.29/09 20:19
dolioFor instance, I suspect most systems aren't subject to the thing on the mailing list about Set_omega, because quantification over universes isn't first-class, exactly.29/09 20:20
-!- Saizan_ is now known as Saizan29/09 20:23
vixeyhey someone should code parametricity in Agda29/09 20:35
vixey& write a paper on it :P29/09 20:35
-!- Saizan_ is now known as Saizan29/09 22:01
-!- boefst__ is now known as anders^^29/09 22:01
--- Day changed Wed Sep 30 2009
-!- Saizan_ is now known as Saizan30/09 01:33
-!- axnqfdx_ is now known as axnqfdx30/09 02:32
-!- axnqfdx is now known as byorgey30/09 11:55
simplesimon2ki have problems to get agda working. if i load a file from within the emacs mode, it says parse error all the time (even on an empty file), same problems with the batch compiler (agda -c). im running ghc 6.10.4 and emacs 23.1 on a 64 bit linux30/09 14:04
simplesimon2kis this a known problem (i dont know what to do) ?30/09 14:04
vixeyI've not heard of that30/09 14:05
dolioCompletely empty, or with a module declaration?30/09 14:05
dolioIt might not accept the former.30/09 14:05
simplesimon2kdoesnt matter what the content of the file is, it says parse error all the time30/09 14:06
-!- Saizan_ is now known as Saizan30/09 15:17
-!- opdolio is now known as dolio30/09 20:25
-!- copumpkin is now known as macweenie30/09 21:36
-!- macweenie is now known as copumpkin30/09 21:38
-!- copumpkin is now known as TheHunter30/09 22:11
-!- TheHunter is now known as copumpkin30/09 22:11

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