xplat xplat augur --- Log opened Thu Sep 01 00:00:54 2011 there are lots of intuitionistic toposes that justify 2^2^S ~ S, i think 01/09 01:53 but if you want to work over conventional math foundations, you can't use the obvious semantics 01/09 01:55 xplat: who are you talking to :| 01/09 02:06 [02:42:37 PM] Having a set S that is isomorphic to 2^2^S is problematic. 01/09 02:08 gosh that was a while ago 01/09 02:11 #agda doesn't exactly scroll like #haskell 01/09 02:12 @tell dolio if we take S = A * S', then an element looks like (a_0,(a_1,(a_2,...)))', and given the usual Kuratowski-pairs, this would contradict foundation (infinitely deeply nested sets) 01/09 10:37 Consider it noted. 01/09 10:37 @tell Eduard_Munteanu data Santa (A : Set) : Set where WithSanta : (Santa A -> A) -> Santa A', using this you can prove {A : Set} -> (A -> A) -> A' and {A : Set} -> A' 01/09 10:43 Consider it noted. 01/09 10:43 ski: So, you've found one erroneous interpretation of type theory into set theory, therefore there can be no such interpretation? 01/09 16:23 hi 01/09 17:22 i'm thinking about reasoning about values 'in' monads 01/09 17:22 say i have something like m ℕ 01/09 17:22 what is the best way to say that n  > k ? 01/09 17:23 have "m (Sigma ℕ \ n -> n > k)" instead 01/09 17:24 the obvious way is to redefine > in terms of m ℕ and to use monadic laws. Are there better approaches? 01/09 17:24 Saizan: what will be the sort of  (Sigma ℕ \ n -> n > k)? 01/09 17:25 (Sigma ℕ \ n -> n > k) : Set 01/09 17:25 hm.... 01/09 17:26 hm….it's Set! 01/09 17:26 %))))) 01/09 17:26 ok, i'm probably too tired at the end of the workday to overlook this :))) 01/09 17:27 thanks :) 01/09 17:27 ops… not exactly…. have to think more about this... 01/09 17:29 at the risk of being stupid…. suppose i already have something like 01/09 17:37 prog : m ℕ 01/09 17:37 should i rewrite it for every possible predicate on ℕ i want to prove holds for prog? 01/09 17:37 if you want to prove stuff about prog : m ℕ after the fact then how you do it will depend on what m is 01/09 17:41 from the monad interface you can't do much, unless prog = return n 01/09 17:42 ppavelV6_: think about common monads 01/09 17:42 ppavelV6_: they don't necessarily "contain" values at all 01/09 17:43 copumpkin: i know %) 01/09 17:43 but something like prog >>= (\k -> k < 5)  would be nice :) 01/09 17:44 prog >>= (\k -> return ( k < 5)) 01/09 17:44 fmap (< 5) 01/09 17:44 copumpkin: not gonna work i believe. or will it? 01/09 17:44 well, you want to be universe-polymorphic 01/09 17:45 but what does that mean? 01/09 17:45 you could lift a decision procedure into the monad 01/09 17:46 i want to have argument-universe-polymorphic monads :) 01/09 17:47 but it seem like Setω or something. I can lift a decision procedure but can't specify the decision 01/09 17:47 seems like to reason about values in M, you need prodicates in the comonad dual to M, and then you 'zap' them together... or something 01/09 17:48 are prodicates fancier than predicates? 01/09 17:48 i have nothing other than intuition behind that idea though, so take it with a few thousand grains of salt 01/09 17:48 probably 01/09 17:48 but i meant predicates of course ;) 01/09 17:49 well, if profunctors are like fancier relations 01/09 17:50 and predicates are unary relations 01/09 17:50 the a prodicate would be like a fancier predicate 01/09 17:50 then 01/09 17:50 ok the use case: I'd like to postulate the existence of a monad (think IO) and a function in it that does something with a number (N -> IO N). I also want to specify some properties about the function's input and output 01/09 17:51 although a prodicate would probably be a presheaf or something like that 01/09 17:51 a prodicate is what you get when 'e' is next to 'o' on your keyboard ;) 01/09 17:51 not a fancier dicate? 01/09 17:52 probably i can postulate that function returns something like irrelevantSigma N (\n -> pred n) 01/09 17:52 ppavelV6_: seems like simple equational reasoning with the monad laws and your assumptions should be sufficient 01/09 17:54 do you have an example of where that breaks down? 01/09 17:55 ok, let see… 01/09 17:58 prog : (Monad m) -> (Monad.M m Bool) -> Monad.M m N 01/09 17:58 prog m mb = mb >>= \b -> if b then (return 5) else (return 7) 01/09 17:58 * copumpkin screams at Bool 01/09 17:58 i should to prove things about prog' b = if b then 5 else 7 and then re-construct prog from prog' using monadic laws and equational reasoning? 01/09 17:58 copumpkin: what wrong with Bool? :) 01/09 17:59 ppavelV6_: it's close to useless if you ever want to prove things about your programs 01/09 17:59 copumpkin: oh :))) 01/09 18:00 It's hard to read proves from the network :) 01/09 18:00 the question is: how to reason about the programs that are initially written in monadic style 01/09 18:01 not really that hard 01/09 18:01 ppavelV6_: one approach would be to express your 'prog' as a composition of morphisms and manipulate them using known equivalences in the category 01/09 18:01 you use decision procedures instead of boolean predicates 01/09 18:01 they're harder to write 01/09 18:01 but definitely not impossible 01/09 18:01 then your bool says something 01/09 18:01 copumpkin: i'm ok with this if the decision procedures return irrelevant proves 01/09 18:02 think that i want to specify the external library (C-library!) behavior. 01/09 18:02 sure, they could :P 01/09 18:02 translating comments into postulates :) 01/09 18:02 although you don't always want that 01/09 18:02 except for maybe the negation 01/09 18:03 that could be irrelevant probably 01/09 18:03 the question 01/09 18:03 ok. I want a "user" to write "programs". She wants to write them in monadic style. I want to prove things about programs :) or at least specify the requirements to them. 01/09 18:04 forget bools :) the program reads integers from a file, stores them in an IO array and sorts the array. I want to specify that array is sorted. 01/09 18:06 proving things about a program specified at runtime sounds impossible to me, unless you have some pretty strong restrictions on the language the program is defined in 01/09 18:07 so it sounds like specifying the requirements would be the bigger part 01/09 18:08 mokus: what do you mean "at runtime"? 01/09 18:09 well, you're talking about "user" defining a "program", so that sounds like the program is arbitrary data 01/09 18:10 and user work time is runtime :) ok :) 01/09 18:10 yea 01/09 18:10 so maybe you want your program to be specified as having the type 'IO (SortedArray x)', where SortedArray is a type of arrays which contain proofs that they are sorted 01/09 18:11 but it doesn't sound like your user language is agda, so maybe not 01/09 18:11 mokus: you may think of my user language as a stack of monads in agda :) 01/09 18:12 it might be helpful to think of the whole stack as one "abstract monad" along the lines of the MonadPrompt in Haskell, and then prove that 'for all implementations', the program reduces to 'return xs' where xs is sorted 01/09 18:13 or at least make the type of such proofs be your user's proof obligation 01/09 18:13 mokus i think i got it 01/09 18:13 ok, have to think more about what i really want :))) 01/09 18:18 mokus: logically, a monad is a lax modality 01/09 19:19 Saizan: a dicate is already a fancier predicate, probably one with more laws 01/09 19:20 Saizan: so a prodicate is transitively a fancier predicate 01/09 19:21 hm, ppavelV6_ has left 01/09 19:24 xplat: is the AbstractBinaryProducts thing a way of using less RAM when checking the proofs in Categories.Monoidal.Cartesian or does it serve some other purpose? 01/09 19:37 it also makes the goals a lot easier to look at :P 01/09 19:38 for humans 01/09 19:38 since we don't really want them to reduce down to normal form 01/09 19:38 keeping them abstract and having an explicit rewrite to a simpler form is nice 01/09 19:38 how do I actually get the goals to normal form when I want to use it with my chosen products? 01/09 19:38 each of the abstract things comes with a proof that it's equal to its definition, iirc 01/09 19:39 I found a proof relating *** to <>, but <> is abstract too.  I guess I can probably use the abstract eta and beta rules to define my own conversion to the non-abstract <> though 01/09 19:41 or I could just do more of the reasoning in the abstract language 01/09 19:42 I need to stop trying to reshape the tools to my workflow and shape my workflow to the tools a bit more, I think 01/09 19:43 it doesn't matter if the proof is abstract 01/09 19:44 if it's an equality, you can rewrite by it 01/09 19:44 except that if it's an equality in the abstract operations, those symbols don't appear in the things i'm wanting to rewrite 01/09 19:44 hmm 01/09 19:45 actually i think i could just use the isomorphism-of-products to go between them without too much work though 01/09 19:46 well, maybe not - doesn't change the fact that the abstract version of *** isn't an instance of the Categories.Object.BinaryProducts one 01/09 19:46 but it would allow me to convert between expressions involving the projections and <_,_> , at least 01/09 19:47 which is convenient enough, I think 01/09 19:48 hmm 01/09 19:48 not sure :/ can't really look now though 01/09 19:48 copumpkin! 01/09 19:49 hey 01/09 19:49 no problem, I think you gave me enough of a hint to get me moving again - thanks 01/09 19:49 hi augur 01/09 19:49 well, moving again as soon as my laptop finishes recompiling the monoidal stuff for no apparent reason :( 01/09 19:50 copumpkin: do you know of any nice little tutorials for writing and/or using pseudotactics in agda? besides just "read the bit in the standard library that has one"? 01/09 19:50 augur: nope :P it's almost completely undocumented 01/09 19:55 oh! I bet the only real problem I'm having is that i'm trying to claim that the abstract products _are_ my chosen products when they're not; if I just open them as if they were any other normal product i bet I can use all the non-abstract operators with them 01/09 19:55 copumpkin: you should document it! 01/09 19:55 augur: your best bet might be to bug xplat for his tactic code (or poke around on hpaste for it, since it's still there) 01/09 19:55 no u 01/09 19:55 i cant document what i dont know! D: 01/09 19:55 guess how I know ;) 01/09 19:55 copumpkin: youre mister smarty pants 01/09 19:56 lol 01/09 19:56 no, I sat down and figured it out 01/09 19:56 http://code.google.com/p/agda/issues/detail?id=444&start=100 01/09 19:56 proving false isn't critical! 01/09 19:56 augur: anyway, I'll be more helpful later, but got an annoying bug at work with a time limit on it and need to get back to it :P 01/09 19:57 bug in agda, or bug because its not in agda? 01/09 19:57 :x 01/09 19:57 bug at my job ;) 01/09 19:57 like 01/09 19:57 an insect? 01/09 19:58 copumpkin, which city are you in again? boston/nyc? 01/09 20:01 boston 01/09 20:10 lame 01/09 20:11 boston is pretty nice 01/09 20:11 i bet there are lots of cafes within walking distance 01/09 20:12 yep 01/09 20:17 i hate you :( 01/09 20:17 * mokus wishes they'd open some Peet's stores in or around NYC 01/09 20:18 i've driven out to Boston once or twice just to go there 01/09 20:18 they're by far the best coffee/tea chain in the US, in my opinion 01/09 20:19 and there are about 5 of them in Boston 01/09 20:19 does anybody know if there's a paper or other source presenting the version of OTT with quotients? 01/09 20:28 xplat: you mean other than the one blog post pigworker did awhile back? 01/09 21:05 yay, caught the bug 01/09 21:14 mucho subtle 01/09 21:14 the fix should be simple 01/09 21:14 xplat: you see the nice proof of false? 01/09 21:17 I love it when that happens 01/09 21:17 makes my proofs so much easier 01/09 21:17 I'm glad false is true, that makes my proofs a lot easier ;) 01/09 21:17 * copumpkin high-fives mokus 01/09 21:17 lol 01/09 21:17 copumpkin! i had an idea for a multitouch display :o 01/09 21:19 oh? 01/09 21:19 have you seen jeff hans TED talk? 01/09 21:19 nope 01/09 21:19 well, in it he demos a display that uses a projector that projects onto a frosted plexiglass sheet 01/09 21:20 the sheet has only the bottom frosted 01/09 21:20 and it has LEDs in the edge, so that when you touch the glossy front, bright spots show up on the back where your fingers are pressing 01/09 21:20 so you use a camera to track these dots, and shazam, multitouch 01/09 21:21 but it requires a projector, right 01/09 21:21 thats a problem 01/09 21:21 but heres an idea: 01/09 21:21 TOLED screen with a glass front, and behind the toled, you have a grid of photosensitive cells 01/09 21:22 you flicker the TOLED on and off 01/09 21:22 and during the off cycles, your light detecting grid reads where the bright spots on 01/09 21:23 from your fingers touching the screen 01/09 21:23 yay, a legit proof of false: http://code.google.com/p/agda/issues/detail?id=444 01/09 21:44 copumpkin: this is bad, no? 01/09 21:53 this is a curious thing, copumpkin 01/09 21:54 that you can have inconsistent logics 01/09 21:55 and modify them in this way or that, and in doing so, get a consistent logic 01/09 21:55 but the consistentification doesnt require a rewrite of everything written previously 01/09 21:55 just some of it 01/09 21:55 as if certain aspects of the pre-existing logic are consistency-independent 01/09 21:55 i was thinking about that before, myself 01/09 22:20 and i wonder, do some of these inconsistent logics have the property that all proofs of falsum have cuts? 01/09 22:21 so that the cut-free fragment is actually still consistent? 01/09 22:21 that would be the same as saying that none of the terms inhabiting _|_ beta-normalize 01/09 22:25 which seems like it's a common form of inconsistency in type theories 01/09 22:25 copumpkin: your proof can be made even shorter: false = relevant false 01/09 23:06 oh, wonderful 01/09 23:07 you should add to the ticket 01/09 23:07 I'd feel like I was spamming if I added anything else 01/09 23:08 copumpkin: does this bug depend on irrelevance? 01/09 23:08 mokus: or I'll do it if it's a pain for you :P 01/09 23:09 I wonder where things start breaking. 01/09 23:09 it's the termination checker 01/09 23:09 and its bad interaction with irrelevance 01/09 23:09 copumpkin: nah, i already have a google account - just added it 01/09 23:10 sweet :) 01/09 23:10 Ah, so even if I'm not using irrelevance it could still be a problem? 01/09 23:10 Eduard_Munteanu: no 01/09 23:10 or shouldn't be 01/09 23:10 I see. 01/09 23:10 it's just that the irrelevance discards information about who's recursing 01/09 23:10 so the termination checker doesn't notice it's an infinite loop 01/09 23:10 copumpkin: i missed another opportunity to make it shorter - don't need a type signature for false ;) 01/09 23:24 nice 01/09 23:26 I like how you can ask it to normalize that term 01/09 23:26 and it gives you relevant _ 01/09 23:26 yea, i was just playing with that 01/09 23:26 --- Day changed Fri Sep 02 2011 so just relevant : ._|_ -> _|_; relevant (); false = relevant false? 02/09 00:18 yeah 02/09 00:18 pretty clean! 02/09 00:19 termination schmermination 02/09 00:19 try normalizing false! 02/09 00:19 false = relevant _ :) 02/09 00:19 i guess the termination checker is actually being accurate, in a way ... 02/09 00:20 relevant _ is stuck, but it doesn't spin 02/09 00:21 i compiled and ran 'bang : _|_ -> IO unit; bang (); main = bang false' 02/09 00:57 it gave me: {-# OPTIONS --universe-polymorphism #-} 02/09 00:57 oops 02/09 00:57 goodbye: MAlonzo Runtime Error: Impossible Clause Body 02/09 00:57 didn't have what i thought on the pasteboard 02/09 00:57 i was surprised, i expected a segfault 02/09 00:58 copumpkin: i have to ask you a question 02/09 02:55 I don't have to answer, but I probably will 02/09 02:56 a really really big question 02/09 02:56 the biggest question i will ever ask anyone 02/09 02:56 :o 02/09 02:56 should i buy deus ex now or wait for the price to drop 02/09 02:56 I hear it's pretty good 02/09 02:56 if you enjoy games, I say buy it now 02/09 02:56 i wonder if its possible to simulate linear types in agda's type system 02/09 02:58 or would that have to be built in 02/09 02:58 copumpkin! whats the most exotic type system you know of? :o 02/09 02:58 hmm 02/09 03:02 not much :) 02/09 03:02 I'm definitely no expert 02/09 03:02 augur, should be possible to 'simulate' it in the sense of building a type that only allows for linear typing 02/09 03:02 You should buy the original Deus Ex and play that instead. 02/09 03:06 dolio: i have it actually 02/09 03:07 it just runs really slowly for some unknown reason 02/09 03:07 Huh. 02/09 03:07 yeah 02/09 03:09 its annoying 02/09 03:09 does agda have a testsuite similar to Test.HUnit? 02/09 05:23 no 02/09 05:25 copumpkin: any plans to add something like that? 02/09 05:38 joe6: not by anyone I know 02/09 05:38 tests aren't really the first thing people think of when using a proof language 02/09 05:39 copumpkin: yes, that's true. I was looking at agda from a general purpose language too.. 02/09 05:39 copumpkin: yes, that's true. I was looking at agda from a general purpose language perspective.. 02/09 05:39 it still is a general-purpose language :P it just gives you facilities to prove things about your code so tests feel kind of weak by comparison 02/09 05:40 you can write lame tests in agda by just asking it to compute at compile-time 02/09 05:40 testPlus : 5 + 6 == 11 02/09 05:40 testPlus = refl 02/09 05:40 if that doesn't typecheck, you've failed your test 02/09 05:41 copumpkin: i am testing some C code, and I use test.hunit as a wrapper to test that code. (i am not generating that code). haskell is giving me the ambiguous type variable errors and I am thinking of agda (given the implicit variables) 02/09 05:42 maybe, I sholud generate the C code from agda? but, that would be a lot of work though.. 02/09 05:43 if things were ambiguous in haskell, it means you're doing something wrong, not a shortcoming of haskell 02/09 05:43 agda's typeclass-like things would be no better (and probably worse) than haskell's typeclasses 02/09 05:44 ok, thanks. 02/09 05:44 source: http://codepad.org/h6g1sng7 , error: http://codepad.org/iKNKZSAa 02/09 05:47 it is a "Ptr a", and a can be any of the Foreign.C.Types (such as CUInt or CInt) or such that. 02/09 05:47 but, I will not know that until I start writing the instance. 02/09 05:47 or, should I make the typeclass have 2 variables, one for the type? 02/09 05:47 and fill it in while writing the instance? 02/09 05:47 but, maybe I should stick to the #haskell channel. 02/09 05:48 is there a stream of primes somewhere? 02/09 10:35 @oeis [1,3,5,7,11,13,17] 02/09 11:18 Sequence not found. 02/09 11:18 @oeis 1,3,5,7,11,13,17 02/09 11:18 The odd prime numbers together with 1. 02/09 11:18 [1,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,... 02/09 11:18 erm, discard 1 :) 02/09 11:19 @oeis 2,3,5,7,11,13,17 02/09 11:19 The prime numbers. 02/09 11:19 [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,... 02/09 11:19 i meant implemented in agda :) 02/09 11:19 Ah. 02/09 11:19 * Eduard_Munteanu should get some sleep 02/09 11:20 Hi, whenever I try to compile a simple main = putStrLn "foo" I get: String !=< (Colist .Data.Char.Char) of type Set 02/09 16:46 Any ideas what's going wrong? I'm just tinkering. 02/09 16:46 String is not a colist of characters. 02/09 16:49 I'm not sure which of those "foo" is. 02/09 16:50 And which putStrLn takes. 02/09 16:50 However, you'll need a conversion of some sort. 02/09 16:50 dolio: I just followed the instructions in the tutorial. I'm making my first steps in Agda so I have actually no idea what you are talking about ^^ 02/09 16:51 Colist is a potentially infinite list. 02/09 16:52 ok 02/09 16:52 Colist Char is one of those with characters in it. 02/09 16:52 And a costring is potential infinite string? 02/09 16:52 I don't remember what String is defined to be, but it must be something else. 02/09 16:52 Oh, String is just imported from Haskell. 02/09 16:53 Yeah, but putStrLn really expects a costring 02/09 16:54 Ah there is a toCostring 02/09 16:54 How old is your standard library checkout? 02/09 16:55 To me, it looks like putStrLn takes a String, and putStrLn∞ takes a Costring. 02/09 16:56 Costring = Colist Char 02/09 16:56 I downloaded 0.5 from the agda wiki 02/09 16:56 Looks like the same situation there. 02/09 16:57 So you might want putStrLn∞ 02/09 16:57 I'm not sure. 02/09 16:57 dolio: That didn't solve it but at least it's starting to push me into the right direction ^^ 02/09 17:04 raichoo: I recently spent some time looking through that stuff too, you can check out what I came up with if you like 02/09 17:12 https://github.com/mokus0/junkbox/blob/master/Agda/hello.agda 02/09 17:12 it may not be all that enlightening, but you can at least see some of the operators I had to look for, and use them as clues in your search 02/09 17:14 mokus: Yay thanks :3 02/09 17:21 That compiled ^^ 02/09 17:21 cool, wasn't actually sure it would with the latest stdlib, but I was using lib 0.5 when I wrote that so I figured there'd be a good chance it'd work for you 02/09 17:24 mokus: Are you using agda to write real programs or just as a proof assistant? 02/09 18:57 as a proof assistant 02/09 18:58 I don't really think it's suitable for programming at this time 02/09 18:58 though if someone were to put a lot of work into libraries and such, it could be a pretty nice language for general purpose programming I think 02/09 18:59 ^^ 02/09 18:59 that's just my opinion though, others here may not agree 02/09 18:59 I've been tinkering with omega lately but it does not have real dependent types so I decided to take a look at agda. 02/09 19:00 mokus: Do you know of another language with dependent types that is mature enough to write programs in? 02/09 19:06 I took a look at epigram2 and coq already. 02/09 19:06 I know of a lot of others that I haven't looked that closely at 02/09 19:07 I've used coq as well, though I also probably wouldn't use it for general programming 02/09 19:07 idris sounds appealing but I've never actually looked at it 02/09 19:07 Yeah, heard of idris 02/09 19:07 I think the complexity of dependent types has yet to really be tamed to the point that a general programmer could pick it up and spend more time getting  things done than building infrastructure 02/09 19:08 idris seems the most suited to plain old programming 02/09 19:08 there's just too many ways to do any given task 02/09 19:08 and no agreement yet about the best way 02/09 19:08 It's still an exciting topic. 02/09 19:10 definitely 02/09 19:10 and I think in time it'll become more tractable too 02/09 19:11 There's cayenne from back in the day, too. 02/09 19:15 Although I don't know how good the compiler was for building stuff to run. 02/09 19:16 there's also ur/web if you're into web programming, though i don't know much about it other than that I hear it's dependently typed 02/09 19:17 ur/web is dependently typed? 02/09 19:59 dependent javascript! 02/09 19:59 not really 02/09 20:26 copumpkin: lets make a dependent JS 02/09 20:55 :D 02/09 20:55 where the types themselves are JS expressions? 02/09 21:17 that could lead to some pretty spectacular weirdness, I think 02/09 21:17 dependent PHP… the horror the horror O_O 02/09 21:51 --- Day changed Sat Sep 03 2011 dolio : nah, just that the obvious (arguably sensible) interpretation doesn't work 03/09 00:14 I don't know why it's sensible. 03/09 00:14 It's not even defined as an actual equation in most type theories. 03/09 00:14 Merely an isomorphism. 03/09 00:15 how hard would it be to do this in agda. I am getting a type error with ghci/haskell. 03/09 01:28 error: http://codepad.org/Ow4qMfmv, U1IR.hs (template haskell used file): http://codepad.org/dEFIZmhJ, CType.hs (template haskell defined file): http://codepad.org/nMpiA3Ze 03/09 01:28 it appears that reify does not work with associated type synonym definitions. 03/09 01:28 I want Haskell's associated type but to read the type from a function return type 03/09 01:29 any thoughts, please? 03/09 01:29 this is the associated type class: http://codepad.org/o12EL0Nh 03/09 01:30 i am using Template Haskell because there is no way I could read the type of p'U1IR into the type of the associated type 03/09 01:31 is there some mechanism to do this in agda? 03/09 01:31 i guess in agda the value level and the type level can intermix? can I read a function type into a type definition? 03/09 01:32 joe6: read how? Through FFI? Nah. 03/09 02:31 FFI stuff stays opaque during typechecking so even if you can write such a type, you won't be able to depend on the exact value you get. 03/09 02:32 There's some reflection thingy in Agda but it might not work at the moment. Not sure if that helps either. 03/09 02:34 Eduard_Munteanu: ok, thanks. 03/09 02:44 When I read about Intuitionists or "Ultra-finitists" how can I think about that label as it applies to that person? Is it in like calling someone a Haskell Programmer? Protestant? Outfielder? What I'm trying to understand is how much does it describe the person and how much a role at a particular point? 03/09 05:56 I'm a nazi 03/09 05:57 lol 03/09 06:01 intuitionism is not the same as ultrafinitism 03/09 06:01 Of course 03/09 06:02 intuitionism is just not using excluded middle 03/09 06:02 I'm talking about a category of labels 03/09 06:02 ie, some things are true, some are false, and some go into infinite loops 03/09 06:02 thats intuitionism in a nutshell 03/09 06:03 I'm asking about the label for the person, not the logic 03/09 06:03 ultrafinitists, on the other hand, deny the existence of things you havent constructed 03/09 06:03 I understand the distinction 03/09 06:03 well what does that mean then :| 03/09 06:03 The word "intuitionist", not "intuitionistic logic" 03/09 06:04 what about it tho 03/09 06:04 Are there people who *are* intuitionists 03/09 06:05 or is it more of a position you take for a given argument or statement? 03/09 06:06 ofcourse there are intuitionists 03/09 06:06 I'm occasionally an intuitionist 03/09 06:07 im intuitionistically occasional 03/09 06:07 Do you see the distinction I'm looking for? Someone can be a "haskell programmer" at the moment, it doesn't describe their world view 03/09 06:07 I guess I have different standards for proof depending on what the statement is 03/09 06:07 glguy: some people are intuitionists and think that non-intuitionistic logic is bs 03/09 06:08 it does sometimes describe their world view 03/09 06:09 i would say im preferentially intuitionistic in that im not sure i think classical logic is bs, but i'd certainly prefer constructions 03/09 06:09 Funny how intuitionism sometimes defies intuition, I mean look at Not (Not a) -> a. :) 03/09 06:25 Tho' I guess that's a small WTF in comparison with Banach-Tarski. 03/09 06:28 s/with/to/ 03/09 06:28 I think a bigger wtf 03/09 06:29 is A -> A x A 03/09 06:29 how the fuck did you just make two things out of one 03/09 06:29 that shit is fucked 03/09 06:30 I'm a linearist 03/09 06:30 yeah, if you dig too deep into intuitions you'll find everyone has their own ;) 03/09 06:30 or any other substructural logic that prevents you from using shit twice 03/09 06:30 to me rejecting LEM is intuitive, if you understand proofs to be concrete evidence 03/09 06:30 copumpkin: Are Clean's uniqueness types the closest thing to linear logic in programming? 03/09 06:38 ATS supposedly has them too, but then you'd have to use ATS 03/09 06:38 so probably, yeah 03/09 06:38 apparently (before my time) GHC used to have linearish types as an extension, too 03/09 06:38 Oh, kmc is here too. 03/09 06:38 kmc is omnipresent 03/09 06:38 http://www.haskell.org/ghc/docs/6.4/html/users_guide/type-extensions.html 03/09 06:39 linear implicit parameters 03/09 06:39 sadly gone now 03/09 06:39 seem like they'd be fun to play with 03/09 06:39 is (∃ \(x : ₂ℕ) → x ∈ ℕ∞) supposed to be isomorphic to "CoNaturals" ? http://www.cs.bham.ac.uk/~mhe/papers/omniscient/GenericConvergentSequence.html#186 03/09 10:56 yeah, you just have to take the first natural for which x returns 0, or infinity otherwise 03/09 11:08 intuitionist describing a person generally refers to their worldview, except if they are a fulltime logician, then they might just be concentrating on intuitionist logics because they find them interesting 03/09 14:52 but even then nobody would probably say 'intuitionist' if they were trying to be precise 03/09 14:53 and 'ultrafinitist' is pretty much worldview period. 03/09 14:53 i don't think the ultrafinitists have ever come up with an expression of their views that much of anyone finds mathematically, as opposed to philosophically, interesting 03/09 14:54 http://www.scottaaronson.com/blog/?p=103 03/09 15:08 2^100 is way too small a number to not exist. 03/09 16:23 So is 2^1000. 03/09 16:23 where do you draw the line?:) 03/09 16:24 If I were going to draw it, it'd be way higher than two machine words. 03/09 16:25 Er, wait. 03/09 16:25 I guess 1000 is around 16 machine words. 03/09 16:26 Which is still way too small. 03/09 16:26 then you can gain some order of magnitudes by storing programs rather than normal forms 03/09 16:29 *orders of magnitude 03/09 16:30 not even philosophers care about "platonic existence" though 03/09 16:31 Some do. 03/09 16:32 There was a post on the n-category cafe not long ago trying to 'save' Platonism in set theory, or something, by proposing the idea that every model (of every axiom system) of set theory Platonically exists, or something. 03/09 16:33 Er, it was on some guy's paper on the topic or something. 03/09 16:34 Anyhow, that was supposed to be better than trying to commit to one. 03/09 16:35 i guess it depends on where you draw the line on "philosopher" 03/09 16:36 That concern certainly seems to fall into the philosophy camp to me. I can't imagine someone having a mathematical interest in whether there really are sets floating 'out there'. 03/09 16:41 I don't see how it could have an impact on your theorems. 03/09 16:41 i could imagine someone arguing that a number doesn't exist unless there are actually that many of some physical thing, so that things like a base-10 representation of the number are only "schemes" by which one can attempt to identify a number which may or may not actually exist 03/09 16:44 in such a world view, 2^100 might be 'big' enough to question its existence 03/09 16:45 No, even then it isn't big enough. 03/09 16:45 true, but the strong connection between mathematical constructs and general onthology that was there in the past seems to be gone from philosophical discourse, so you've to be much more of a mathematicians to bring them together at this point in time 03/09 16:45 why not? just because someone says there are that many atoms in the universe doesn't mean a person believes it 03/09 16:45 Because there are around that many atoms in your body. 03/09 16:46 well, 2^1000 then 03/09 16:47 but even at 2^100, such a person might say "you've only claimed that the body has that many atoms, not proved it" 03/09 16:49 and by way of proof, they may want you to sit and count them 03/09 16:49 Then that person can go to hell. 03/09 16:49 they have bigger problems than the existence of numbers then 03/09 16:49 I've never counted to 1,000,000. 03/09 16:49 i really don't know if that's what this guy believes, but it seems like it about has to be 03/09 16:50 So it doesn't exist. 03/09 16:50 i tried once... don't remember how far i got ;) 03/09 16:50 i think i quit around 150k 03/09 16:50 Let's see you count all the people in New York city before I believe there are more than a million. 03/09 16:50 3 doesn't exist 03/09 16:51 copumpkin: NO U 03/09 16:51 i'm not saying it's a sane way to think, but if a serious mathematician is claiming that 2^100 doesn't exist they must have _some_ underlying logic to it, no matter how bizarre 03/09 16:51 it's called a brain tumor 03/09 16:52 I mean, um 03/09 16:53 Anyhow, that line of thinking has the same defect as Platonism, to me. 03/09 16:53 They're committed to the idea that everything in mathematics must have some actual realization 'out there.' 03/09 16:53 yea, and ultimately it doesn't diminish the fact that logic works independently of the existence of the things it's manipulating 03/09 16:53 The Platonist just says, "since we have the axioms, the sets must really exist." 03/09 16:54 it really don't matter at all whether pi exists 03/09 16:54 or what you say the word "exist" means, which is really what it's about IMO 03/09 16:54 if you don't like me saying 2^100 "exists" you can just make up a word for what I call "exists" and do a mental translation whenever you'r etalking to me 03/09 16:55 and write off all my proofs as irrelevant because i'm not talking about things that "exist" 03/09 16:55 Yeah. Like, "I used 2^100 in a calculation yesterday and it worked." 03/09 16:55 yup 03/09 16:56 same thing with sqrt(-1) 03/09 16:56 > let exists n = length (replicate n ()) seq True in exists 10 03/09 16:56 True 03/09 16:56 > let exists n = length (replicate n ()) seq` True in exists 1000 03/09 16:56 True 03/09 16:56 who cares if it's a number or not?  calculations using it work 03/09 16:56 If you refuse to use, say, 2^1000, you're probably going to have trouble explaining how RSA cryptography works. 03/09 16:58 At the levels people use it at today. 03/09 16:58 The key space is larger than that. 03/09 16:58 yea, it seems like a pretty useless world view 03/09 16:58 you pretty much have to consider everything a computer does to be magic 03/09 16:58 but then there are probably also serious nihilists and solipsists out there too 03/09 16:59 i think absurdity is mostly unrelated to believability, when it comes to real people's views 03/09 17:01 or i guess i should weaken that and say usefulness... absurdity is more of a relative concept in that context probably 03/09 17:02 nobody would consider their own views absurd, but they might be willing to concede they aren't useful, but still believe them anyway 03/09 17:03 dolio: I wonder whether someone claiming 2^1000 doesn't exist would necessarily decline to use it - they may use it just like you or I would, but think of it as something other than a number.  A logical sentence devoid of numerical meaning, perhaps. 03/09 17:05 at some level you believe by doing things that have a meaning only if that belief holds 03/09 17:05 mokus: That just sounds like wanking about the definition of "number". 03/09 17:13 yes, it does 03/09 17:13 that's what i mean when i was talking about arguing over definitions of "exists" above too 03/09 17:13 i think most philosophical differences come down to namespace collisions 03/09 17:14 Heh. 03/09 17:14 Can't say those thrill me. 03/09 17:14 me either, but keeping that in the back of my mind helps me keep calm more often than I probably would otherwise ;) 03/09 17:14 Anyhow, for instance, I recall hearing a story about this group of people working on a digital circuit.... 03/09 17:14 They were working using some discrete model of how the circuit actually worked. 03/09 17:15 Then Feynmann came in and used some model using calculus and the real numbers, which wasn't really how the circuit worked. 03/09 17:15 And his solution to whatever problem they were working on was better, and actually worked with the circuit. 03/09 17:16 Better than was possible to get with the accurate, discrete model, or something. 03/09 17:16 heh, that story can be used against contructivism, unless we show the model could work with just computable reals 03/09 17:17 yea, it's amazing how often a kludge can get the job done better than a perfect solution, in any domain 03/09 17:17 I think you can do calculus with computable reals. 03/09 17:18 Some, anyway. 03/09 17:18 i suspect a lot more than people think 03/09 17:19 Yes. 03/09 17:20 abstract stone duality seems like a promising foundation to rebuild an awful lot of existing theory on 03/09 17:20 A lot of classical vs. constructive differences seem, to me, to end up being on the wrong side of the 'I can use this' gap, too. 03/09 17:21 Like, "2^100 doesn't exist" "But I just used it and it worked." 03/09 17:21 yea, i think constructive logic is in a really sweet spot in that regard 03/09 17:22 even classical logic is usable as a modality within it 03/09 17:22 so you don't have to "give up" classical logic, really 03/09 17:22 justlike in Haskell you don't "give up" IO to gain purity 03/09 17:22 Whereas with classical you often get, "in classical mathematics, all Foos have this useful property Bar." "But, your proof of that doesn't show how to calculate or determine the Bar for any particular Foo, so how useful is it that they all 'have' that property?" 03/09 17:23 I mean, it's useful if you want a fuzzy feeling that all Foos are nice. 03/09 17:24 or a fuzzy feeling that one sphere is isomorphic to two spheres ;) 03/09 17:24 not sure why anyone actually wants that though 03/09 17:25 in some cases it might work as a bound on a search algorithm 03/09 17:25 maybe 03/09 17:25 thouhg i guess complexity considerations are going to get in the way 03/09 17:25 yea, if you're searching over the classical set of points in a sphere, you're gonna have a hard time making your algorithm practical 03/09 17:26 and if you're searching over neighborhoods then that isomorphism doesn't apply 03/09 17:27 i was talking about "all Foo have this udeful property Bar" in general, not Banach-Tarski :) 03/09 17:28 oh, sorry ;) 03/09 17:28 As I understand it, in constructive mathematics, that situation often leads to one where you can prove a similar theorem that takes a little more structure on the inputs. 03/09 17:29 And then all the things you actually care about have that extra structure. 03/09 17:29 seems like if you're limiting search spaces, you can probably use the same properties, because you're aiming to prove something that's already a negation, and "not not not P x" is as good as "not P x" in most logics 03/09 17:30 All shiny foos are constructively bar, and all the foos we've come up with are shiny. 03/09 17:30 Of course, there's also work on what you can add to constructive systems to leave them still constructive, but prove more nice things. 03/09 17:31 although it would be a bit more useful if you could also prove "all foos are shiny", as that removes the proof obligation of shininess whenever you discover a new foo 03/09 17:32 Search principles. 03/09 17:32 Stuff like that. 03/09 17:32 but i imagine the idea of such a translation is that you're confining all the classical assumptions to shininess, so 'shiny' will generally be a simpler property but still not constructively provable 03/09 17:33 (when quantified over all foos that is) 03/09 17:33 Well, you can't prove that all foos are shiny, of course. 03/09 17:34 i guess Foo = decision procedure; shiny = works on conats too; in escardo's last message to the mailing list 03/09 17:37 I imagine it's usually when you'd use, say, the axiom of choice to go, "give me a function for this purpose by magic," you instead have to provide an appropriate function. 03/09 17:37 But there's a sensible constructive definition of such a function for any particular foo you care about. 03/09 17:38 Saizan: Yeah, I didn't look into that too much. Was he using conat? Or something else? 03/09 17:38 Conat isn't exactly the natural numbers extended with a point at infinity, because you lose induction. 03/09 17:39 But then, I don't know what "extended" means exactly. 03/09 17:40 it's using "convergent sequences" which are isomorphic to conat 03/09 17:40 (i guess they are more closely related to predicates characterizing open sets of conat) 03/09 17:42 Damn, how do I indent nested ... | in with-patterns? 03/09 18:08 It seems it will only take them starting at the first column 03/09 18:08 But it's ugly :) 03/09 18:08 Ah, I have to indent just the '|' 03/09 18:10 Does Peirce's law follow from LEM? I'm trying to prove the former. 03/09 18:34 yes 03/09 18:35 is how I did the classical laws (LEM, Peirce, Double Negation Elim) http://www.galois.com/~emertens/Classical.html 03/09 18:35 (I guess they aren't all "laws") 03/09 18:36 Ah, my approach seems a bit different... http://paste.pocoo.org/show/469603/ 03/09 18:37 I see 03/09 18:37 I remember that there is a hierarchy to those three propositions but I don't remember what it was :) 03/09 18:38 If you can prove double negation elimination from LEM 03/09 18:38 then you can use that to use my Peirce proof 03/09 18:39 Yeah, I have DNE from LEM. 03/09 18:39 So you could copy what I wrote and then say: dne₂ PeircesLaw 03/09 18:39 I see. 03/09 18:41 xplat: you know if I can pattern match in a term I generate through reflection? 03/09 18:41 or glguy ? 03/09 18:41 I suspect you'd rather do it on your own, but this at least shows that you can :) 03/09 18:41 That classical embedding is nice, it also isolates the classical parts from the others, no? 03/09 18:41 Eduard_Menteanu: yeah, I like to think of it like Haskell's IO 03/09 18:41 keep your constructive parts pure and only push what you have to into "Classical" 03/09 18:41 Yeah, this seems nice. 03/09 18:43 and then dne₂ becomes "unsafePerformIO" :) 03/09 18:43 Heh, indeed. 03/09 18:44 Still, I'm a bit puzzled this doesn't need any postulate. 03/09 18:45 You can import Relation.Nullary.Negation to get its RawMonad implementation for Classical 03/09 18:45 Is there a limitation to decidable predicates? 03/09 18:45 Eduard_Munteanu: my file doesn't prove ((P → Q) → P) → P, It proves ¬ ¬ (((P → Q) → P) → P) 03/09 18:45 Eduard_Munteanu: I don't understand your question about limitations 03/09 18:46 ExcludedMiddle : ∀ {A} → Classical (Decidable A) 03/09 18:47 I wonder if this could work for any A : Set \ell instead of a decidable A 03/09 18:48 (A : Set) -> Classical A ? 03/09 18:48 Yeah, for instance. 03/09 18:48 Well, what happens if A were chosen to be ⊥ 03/09 18:50 I handle that with a match like   with lem P ... | inj₂ f with p f ... | () 03/09 18:51 I'm not sure something like that works in that case though. 03/09 18:52 ExcludedMiddle isn't requiring A to be decidable, it's showing that classically every A is decidable 03/09 18:52 Try to write a proof of [Classical ⊥],    [(⊥ → ⊥) → ⊥] 03/09 18:52 Ah, hrm... (⊥ → ⊥) is inhabited so that won't do. 03/09 18:53 I find it a bit non-obvious how proving ¬ ¬ (a ∨ ¬a) is doable without a postulate :) 03/09 18:54 bad : ((A : Set) → Classical A) → ⊥ 03/09 18:54 bad f = f ⊥ (λ ()) 03/09 18:54 since that's just dne1 + lem 03/09 18:55 Eduard_Munteanu: In English it works like this: First you say that there is no "A" because if there was one you'd give it to me and I'd tell you that there was one :) 03/09 18:55 ExcludedMiddle f = f (no (λ a → f (yes a))) 03/09 18:56 Ah, I see. 03/09 18:58 it's more like "i'd go back in time and tell you .." 03/09 18:58 I love the structure of that implementation 03/09 18:59 I wonder if such an approach can be generalized to eliminate other postulates as well. 03/09 18:59 anyone have any idea how I can get the names of existing types in reflection? 03/09 19:00 You can \=?-Name (quote SomethingElse) 03/09 19:00 oh I see 03/09 19:00 thanks 03/09 19:00 no pattern matches though :/ 03/09 19:01 I discovered "quote" though experimentation 03/09 19:01 I'd hate to see the ADT representing pattern matches though 03/09 19:01 "Ugh, I need a way to quote names, like [quote] 03/09 19:01 lol 03/09 19:01 * Eduard_Munteanu guesses the monad is T = Classical, return = dne\_1, join = T dne\_2 03/09 19:05 As for the adjoints, maybe F = U = ¬, F -| U for some functorial interpretation of ¬ ? 03/09 19:08 what's up with the weird coloring on this function? http://snapplr.com/jk7p 03/09 19:20 is getArg a record accessor somewhere? 03/09 19:20 it should be, but Arg is a data type, not a record 03/09 19:21 copumpkin: When did you last compile? 03/09 19:32 They made a bunch of changes about 'projector-like functions.' 03/09 19:33 I just pulled half an hour ago 03/09 19:34 Well, that might explain it. 03/09 19:34 I guess they're recognizing it as a projector-like function 03/09 19:34 interesting 03/09 19:34 You were able to build half an hour ago? 03/09 19:34 yeah 03/09 19:35 I can't get alex 2.3.5 to build. 03/09 19:35 And the latest one that does build it too new for Agda, I guess. 03/09 19:35 hmm 03/09 19:36 not sure, I didn't do anything crazy 03/09 19:36 Was your alex built prior to 7.2? 03/09 19:39 probably 03/09 19:39 Yeah.... 03/09 19:39 It probably doesn't even matter, because I don't think there have been any agda-mode changes. 03/09 19:40 yeah 03/09 19:41 gah, so I guess I still can't write "deriving Eq" for simple types with reflection 03/09 19:41 copumpkin: itd be nice if there was a language that had a conveniently extensible type system 03/09 20:00 not a serious language to do serious stuff in, just one to toy around with various ideas in 03/09 20:00 dolio: is the idea to recognize projector-like functions so that you can see that the result got smaller? 03/09 20:18 and use that in termination checking? 03/09 20:19 oh, he left :) 03/09 20:20 glguy: what timing! 03/09 20:44 the def constructor in Term is kind of a weird way to do application 03/09 23:34 whoops, got agda into a loop by unquoting fix 03/09 23:38 it seems like unquote could have a type 03/09 23:43 if they had a function that interpreted types into agda types 03/09 23:43 --- Day changed Sun Sep 04 2011 if I use agda, would I still need the type constructor F 04/09 01:32 haskell source : http://codepad.org/Sm3glEFq 04/09 01:32 in agda equivalent of type classes, can I inherit characterstics? 04/09 01:32 joe6: do you mean stuff like   class (Foo a) => Bar a? 04/09 01:57 has anyone tried curry? 04/09 04:12 uri: http://www-ps.informatik.uni-kiel.de/currywiki/documentation/tutorial 04/09 04:12 any thoughts/experiences? 04/09 04:12 ive tried it 04/09 04:23 did you like it? it seems interesting. 04/09 04:24 i prefer vindaloo tho 04/09 04:24 are you kidding? 04/09 04:24 you need papadums tho crucially 04/09 04:25 or puri 04/09 04:25 oh god puri 04/09 04:25 kulcha ftw 04/09 04:27 puri > kulcha 04/09 04:28 sorry 04/09 04:28 how about epigram2? any thoughts? 04/09 04:29 oh puris 04/09 04:29 joe6: ask pigworker! 04/09 04:30 i am getting back to agda after a long break. Any good tutorials to get me back into the groove. 04/09 04:37 I'd suggest finding something to prove/code in Agda first. 04/09 04:39 Then you can look around the stdlib. 04/09 04:39 ok, thanks. will do. 04/09 04:39 just found this article: 04/09 04:42 uri: http://people.cs.kuleuven.be/~dominique.devriese/agda-non-canonical-implicits/ 04/09 04:42 joe6: that looks a lot like the release notes I pointed you to 04/09 04:49 joe6: Did you figure out that Agda doesn't have typeclasses? There is a feature called "instance arguments" in the development branch, but it isn't released yet and is a bit different 04/09 04:49 the non-canonical-implicits seem to be a lot powerful than the haskell typeclasses. 04/09 04:49 Eduard_Munteanu: yes, thanks. 04/09 04:49 glguy, it has not been released yet? 04/09 04:49 they're different 04/09 04:49 agda is a lot weaker at finding valid "instances" than haskell is 04/09 04:49 it also allows you to pass custom instances that haskell does not do 04/09 04:50 oh, ok. 04/09 04:50 You can't even write a recursive show AFAIK 04/09 04:50 it's closer to scala in that regard, but at least agda lets you require specific instances 04/09 04:50 since it has value unification 04/09 04:50 You can write one, but it doesn't recursively search for you. 04/09 04:50 copumpkin: what is a custom instance? 04/09 04:50 you need to bring the special instantiation into scope if you want it 04/09 04:50 so if you have Show a => Show [a] 04/09 04:50 you need to apply that to your existing show instance 04/09 04:51 to get the one for lists 04/09 04:51 (explicitly) 04/09 04:51 joe6: say you have two orderings on naturals 04/09 04:51 in haskell you couldn't write two instances 04/09 04:51 showyThing = showLists showChars 04/09 04:51 you'd wrap one or both of them in a newtype to write custom instances 04/09 04:51 will something like this in haskell be better(easier/simpler/smaller) in agda? http://codepad.org/JEdSikMn 04/09 04:52 copumpkin: yes, that is what I find. You need a newtype in haskell. 04/09 04:53 it wouldn't be all that different 04/09 04:53 oh, ok. 04/09 04:53 It probably makes sense in your local context, but that Gettable class looks like a mess at first glance /:-) 04/09 04:54 glguy, I am just playing around with it. 04/09 04:55 i wanted to figure out if I could create a super-type-class that can define an instance for a smaller type-class automatically? 04/09 04:56 You should finish it off and parameterize it on the monad instead of only supporting IO :-P 04/09 04:56 I wish I could do the instance (Flags a) => Gettable (F a) where 04/09 04:56 without the need for the newtype 04/09 04:56 that you can do in agda 04/09 04:57 but agda doesn't have a C FFI, so you'd have to use Haskell's 04/09 04:57 i got the idea from copumpkin. Thanks to you,  i learned associated types. 04/09 04:57 and Haskell's would probably want you to use typeclasses 04/09 04:57 in haskell, I meant. 04/09 04:57 that agda can't FFI to as far as I know 04/09 04:57 :) 04/09 04:57 copumpkin: what about that Agda FFI web browser thingy from months ago? 04/09 04:57 How did it do the FFI that actually did anything? via Haskell? 04/09 04:58 not sure 04/09 04:58 copumpkin: is there any way you can think of (using different mechanisms/gadt/or any such) that "instance (Flags a) => Gettable (F a) where" can be made to work without the need for a newtype? 04/09 04:58 not for now, sometime in the future 04/09 04:58 you can write it, but you shouldn't write it 04/09 04:59 you just need undecidable and overlapping instances, iirc 04/09 04:59 any future stuff, in agda, that can make it possible? 04/09 04:59 oh, really, I can. 04/09 04:59 joe6: What is your actual goal? 04/09 04:59 as I said, an instance like that is already possible in agda, but since agda won't go looking for instances like that automatically, you don't get the benefits 04/09 04:59 I don't understand your question so it is making it hard to contribute 04/09 04:59 glguy, I have a class Gettable and then I have another class Flag. All the types in Flag have a certain implementation of Gettable. 04/09 05:00 I do not have to define a Gettable instance for every type in Flag, as they all have a similar interface. 04/09 05:01 I was wondering if there was a way to define the Gettable instances for all types that are part of the Flag class, without having to list each Gettable instance for each Flag type. 04/09 05:02 glguy, does that make sense? 04/09 05:02 yeah. Like copumpkin said you do it with overlapping and undecidable instances. (That's a bit error prone but it does what you are asking for) 04/09 05:02 There is nothing to stop someone from adding another instance for something that also has a Flags instance 04/09 05:03 and with different imports in different modules you can get funky behavior 04/09 05:03 The safe way to do it is to define functions as the default implementation for the instance 04/09 05:03 http://hackage.haskell.org/packages/archive/base/4.4.0.0/doc/html/Data-Traversable.html#v:fmapDefault 04/09 05:03 is an example of this 04/09 05:04 so you still have to add all the instances but you don't have to reimplement the logic every time 04/09 05:04 makes sense. Thanks 04/09 05:05 copumpkin: you could at least reduce Eq to using eliminators instead, and you could even generate the correct type signature for the eliminator, which is the most complicated part of writing it usually 04/09 05:21 true 04/09 05:21 it'd be nice to autodefine eliminators in general, too 04/09 05:22 then we can have coq 04/09 05:22 copumpkin: reflection has unquote now? 04/09 05:22 yeah 04/09 05:22 it's very finicky though 04/09 05:22 you can't give it anything that contains a hole 04/09 05:22 anywhere in its normalized form 04/09 05:23 it makes a lot of things easier, though, i bet 04/09 05:27 i mean, i can think of things that can't be done without it without kludges 04/09 05:28 well, kludges or a much more extensive set of apis 04/09 05:28 one of the drives in my raid array seems about to fail, guess what i'm doing tomorrow ... 04/09 05:29 :/ 04/09 05:46 copumpkin: btw, does reflection work now? 04/09 05:49 it doesn't have the Nat bug it had before 04/09 05:50 I was under the impression it was totally broken at some point. 04/09 05:50 I don't think so 04/09 06:09 unless you wanted naturals in it 04/09 06:09 Hrm, I remember something about the ring solver not using it. 04/09 06:13 that's because it's a pain to make it use it 04/09 06:14 xplat wrote a wrapper around it so that you could use reflection for it 04/09 06:14 but ran into the nat bug I mentioned 04/09 06:14 Ah, that explains it. 04/09 06:14 so he could only solve expressions that reduced to things that don't involve nats 04/09 06:14 I mentioned knowing how to work around it 04/09 06:28 and my binding worked with them 04/09 06:28 err 04/09 06:28 xplat mentioned* 04/09 06:28 I'm sure it gets better with practice and understanding, but using reflection felt like a big hack to me 04/09 06:31 it does :P 04/09 06:32 In order to limit derivations to intuitionistic ones, the additional constraint that every succedent may have not more one formula is added. -- http://mathworld.wolfram.com/SequentCalculus.html 04/09 06:46 What does this sentence mean? 04/09 06:46 oh "more than one" 04/09 06:47 xs |- x 04/09 06:47 hello 04/09 15:40 i'd like to use a proof assistant in order to write proofs about basic set theory 04/09 15:40 is it possible/easy to do that with agda? 04/09 15:40 by "basic set theory" i mean things such as "inclusion is transitive" or "intersection is commutative" 04/09 15:43 if you are ok with using Agda's (maybe decidable) predicates as sets then those should be simple 04/09 15:45 i wrote a few theorems with coq, but it seems to be too much complex for me 04/09 15:45 i'm used to first order logic and natural deduction 04/09 15:46 I am newbie in type theory, but I think problems can occur when you will encode sets as predicates (sometype -> Set) and try to encode infinite sums. 04/09 15:47 coming from natural deduction you might have a lot to learn 04/09 15:47 wieczyk: it sounds like Data.Product.\Sigma should work for that 04/09 15:48 sorry but i don't understand why natural deduction is wrong 04/09 15:50 i'm not saying it's wrong, just that it's quite different from how stuff looks in agda 04/09 15:50 ok 04/09 15:50 (even if they are sort of isomorphic) 04/09 15:51 my main problem is i can't find a proof checker that is easy to use for me 04/09 15:52 it seems people use them for entirely different goals than me 04/09 15:53 or different backgrounds 04/09 15:53 Saizan: if I understand whole stuff correctly, (\Sigma A B) is in higher universe than A and B. I think it could do some complications. Hm, I will do some tests today. 04/09 15:53 (A : Set) (B : A -> Set) |- Sigma A B : Set 04/09 15:54 Ok. 04/09 15:54 besides coq i also looked at isabelle 04/09 15:55 but its manual is way too complex 04/09 15:55 qasn: i guess you've to be comfortable with how proofs look like in type theory to use Agda or Coq, Coq also adds another layer of "tactics" on top of it though 04/09 15:56 i don't know type theory. i guess this is the problem 04/09 15:57 most agda tutorials will teach you type theory as you go, though 04/09 15:58 do you know any good tutorial? 04/09 16:00 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation <- see "Introductions to Agda" here 04/09 16:02 ok thank you 04/09 16:02 bye 04/09 16:09 i wonder if i should build a darcs agda today or if it will be totally broken 04/09 22:29 What version of ghc? 04/09 22:32 7.0.3 04/09 22:33 Oh. It will probably compile, at least. 04/09 22:33 i'm not completely sure how encouraging that is 04/09 22:34 More encouraging than it not compiling? 04/09 22:34 more encouraging than 'it probably won't compile' 04/09 22:34 but really you were just reaffirming my initial assumption 04/09 22:35 i.e. 'probably compiles, but who knows how many interesting ways there will be to prove false?' 04/09 22:36 I haven't been able to use Agda in months, so I can't tell you how broken or not it is once it compiles. 04/09 22:36 still haven't gotten that fixed?  :( 04/09 22:36 Oh, well, proofs of false are nothing new, really. 04/09 22:36 well, or make the typechecker loop, or the emacs mode rewrite things into gibberish 04/09 22:37 Yeah, I was going to post to the mailing list, but then I decided I should try the latest first, but then I discovered I couldn't compile it on 7.2. 04/09 22:37 p 04/09 22:37 what i'd suggest is rip every mention of agda out of your emacs directories and reinstall agda-mode from scratch, and do the same with haskell too if it doesn't work 04/09 22:38 It's been broken from scratch on this machine. 04/09 22:39 ! 04/09 22:39 Fresh emacs file with agda-mode install run on it. 04/09 22:39 no wonder you haven't fixed it :( 04/09 22:39 what does it actually do? 04/09 22:39 It locks up emacs as soon as I open anything with a .agda extension. 04/09 22:40 Including if I just do something like 'emacs Foo.agda' where the file doesn't exist. 04/09 22:41 darcs Agda built fine here with ghc-7.2.1 04/09 22:43 I went back home recently and noticed that I have an older version of emacs at home. 04/09 22:43 Did you have alex built already from a previous version? 04/09 22:43 probably 04/09 22:43 Okay. 04/09 22:43 Agda complains about alex 3.x, and 2.x doesn't build on 7.2.1 anymore due to misused bang patterns or something. 04/09 22:44 ah, true, had to use --ghc-options=-XBangPatterns 04/09 22:46 Oh, I see. 04/09 22:47 how long has it been since pigworker was here anyway? 04/09 23:06 hm, in OTT heterogenous equality is conditional? 04/09 23:51 so there's no reason to assume you can't prove something like 'true : Bool == zero : Nat' 04/09 23:51 ? 04/09 23:51 --- Day changed Mon Sep 05 2011 xplat: that type reduces to the empty one though 05/09 08:30 xplat: but e.g. (p : (:- P) == q : (:- Q)) reduces to unit, so it's trivially provable, afaiu 05/09 08:33 (forall p P q Q) 05/09 08:33 xplat: where :- is the injection from Prop to Set 05/09 08:58 * bxc-paella wonders what fun stuff to implement in agdabot irc bot 05/09 17:25 there's one already? 05/09 17:37 there is 05/09 17:38 i'm playing with it 05/09 17:38 its on #agdabot but it only knows 'hi' 05/09 17:42 hah, kreisel showed that there is no admissible Pi_1 axiom we can add to PA that will let us show even a single additional function is recursive 05/09 20:10 xplat: what 05/09 20:12 of course, this is Pi_1 where the body being quantified over is already a provably recursive predicate 05/09 20:13 rather than the stronger one where it can be any quantifier-free definable predicate 05/09 20:13 wat 05/09 20:46 --- Day changed Tue Sep 06 2011 hi 06/09 08:48 i'm trying to play with something like "monad of proof-carrying values". The final goal is to get Hoare state. Is it possible at all in this direction? http://hpaste.org/51002 06/09 08:49 ppavelV6: seen this one? http://lambda-the-ultimate.org/node/4273 06/09 09:08 Saizan: no, but i'm trying to do something in this direction - using kleisli arrows instead :) thanks for the reference :) 06/09 09:08 Saizan: talking about original problem - is this indeed a problem? 06/09 09:08 ok, is this something more than a limitation of ppavelV6 or agda's type-checking algorithm? 06/09 09:10 ppavelV6: the type you give to f in the signature of bind is too restrictive 06/09 09:14 and so you've to modify the type of P2 too 06/09 09:15 Saizan: hmm… to me it seems to except any "existential" :) any examples how to weaken it? 06/09 09:16 ... {P2 : r1 -> r2 -> Set} -> ... (f : (x : r1) -> ∃ (P2 r1)) -> .. 06/09 09:16 sorry 06/09 09:16 ... {P2 : r1 -> r2 -> Set} -> ... (f : (x : r1) -> ∃ (P2 x)) -> .. 06/09 09:16 makes sense 06/09 09:18 it somehow exposes the metavar i believe? 06/09 09:22 it allows the result type of f to be dependent on its argument 06/09 09:23 yes 06/09 09:26 the metavar _453 is probably the one agda tries to use to fill the P2 argument of bind 06/09 09:27 i think so. just didn't come out with the solution of how to allow agda to depend on a var 06/09 09:28 hi 06/09 09:32 hi 06/09 09:32 Saizan: thanks very much. It actually solved all of problems :) 06/09 09:32 np 06/09 09:32 my mood goes up :) 06/09 09:32 man, it was so simple :( 06/09 09:33 * ppavelV6 feels stupid 06/09 09:33 I'm learning Agda and there's one thing I don't understand: why does the type Desc in, for example, Conor McBride's ornament draft has to have type Set1 ? 06/09 09:33 i guess because some of its constructors take an argument of type Set 06/09 09:34 hmm ok 06/09 09:36 this stratification is to avoid stuff like russel paradox that would make agda inconsistent 06/09 09:36 actually I thought it has type Set1 for some "semantic" reason, not because Agda obliged it 06/09 09:37 one could say that wanting to avoid impredicativity is more "semantic" 06/09 09:39 if you had T : Set; T = (A : Set) -> Foo; then that A in the definition of T would quantify over a set that contains T too 06/09 09:40 making T definition self-referential, even if indirectly 06/09 09:40 hm ok 06/09 09:41 So are we going to get live updates from AIM? 06/09 12:10 in agda, is there any way to do induction-recursion over Set\omega? 06/09 18:30 i'd like to make a universe that is stratified, but i don't currently see a way to do that 06/09 18:31 xplat: like this? http://code.haskell.org/~Saizan/bisim/ObsEq.agda 06/09 18:42 xplat: though it won't build with an agda that requires Level to be made of postulates 06/09 18:42 (not sure if it's easy to port) 06/09 18:43 Saizan: ah, thanks.  but can you lift things from one universe level to another with that?  that was the main problem i was having with my attempt 06/09 19:43 xplat: i'd have to try, where did you get stuck? 06/09 19:49 Saizan: i'm not really sure whether i actually got stuck or if it was just far harder than i'd imagined 06/09 20:09 i guess the Pi case is going to be the harder one since it's contravariant too 06/09 20:20 Saizan: is your example the same as http://www.e-pig.org/epilogue/?p=418 ? 06/09 21:02 except, of course, with levels added? 06/09 21:03 yeah, and with a Desc version of IMu/INu rather than a Comm/Resp/next one 06/09 21:07 mostly because you couldn't complete the proof with the latter in a decent amount of memory 06/09 21:08 xplat: you may (or may not ;)) be interested to know I've got Categories.Monoidal.Cartesian compiling in <1 min now, using only 2 GB RAM 06/09 21:21 but I dropped AbstractBinaryProducts to get there, I'm not sure whether that's something you needed for other purposes 06/09 21:21 just switching it off AbstractBinaryProducts dropped agda's peak memory usage from 6.5 GB to 4.2GB 06/09 21:22 mokus: hm, that's the opposite effect from when i put it on AbstractBinaryProducts in the first place 06/09 21:26 mokus: what did you end up doing? 06/09 21:26 just made that switch and then spent some time "filing" the other proofs into more general places 06/09 21:27 mokus: ? 06/09 21:27 I just changed the imports of AbstractBinaryProducts to BinaryProducts and fixed all the missing sybols, most of which were 'convert' functions from AbstractBinaryProducts 06/09 21:28 then i took a lot of the simpler proofs from Categories.Monoidal.Cartesian and moved them out of that module, mostly into a new Categories.Object.Products.Properties module 06/09 21:28 mostly related to the top-is-unit isomorphisms 06/09 21:29 https://github.com/mokus0/categories/commit/60bce0e9f5f11e6ab33de38d708506571926cba7 06/09 21:29 mokus: did it get a lot slower when you took out the AbstractBinaryProducts but before you started moving things, or did the new 2.2.12 optimizations help a lot there? 06/09 21:30 i think the new optimizations made it faster to not use AbstractBinaryProducts 06/09 21:30 just removing them sped it up about 70% 06/09 21:30 mostly because it cut it down to where it was hardly using any swap 06/09 21:30 ah.  2.2.10 is a *lot* slower without AbstractBinaryProducts. 06/09 21:31 sounds like the agda optimizations reversed that 06/09 21:31 it went from 14 min to 5 min just by changing that 06/09 21:32 and after moving some proofs out, it got down to about 50 sec 06/09 21:32 what happened to all the outer bracket layers? 06/09 21:39 you mean with the ⟩,⟨'s? 06/09 21:42 yeah 06/09 21:42 i had it like that because the operator being conged is <_,_>, not _,_ 06/09 21:42 i'm not sure why i changed it, it seemed to make sense at the time... probably because i had used _⟩,⟨_ in something else before 06/09 21:42 I can change it back, though I was actually planning on either replacing it with explicit ⟨⟩-cong's 06/09 21:43 or asking where would be a good place to put it for more general use 06/09 21:44 aside from that, what do you think about the Categories-specific version of equational reasoning (with the arrows)? 06/09 21:44 i like it, and i think it would make more sense in other places too 06/09 21:44 ooh categories talk 06/09 21:44 yay 06/09 21:44 xplat: did you see my feature request for local abstraction barriers? 06/09 21:45 copumpkin: yep 06/09 21:45 feel free to chime in on that if you have ideas of how to make it work 06/09 21:45 xplat: gave ⟨_⟩,⟨_⟩ its braces back ;) 06/09 21:49 maybe with such a drastic performance flip between abstracted/unabstracted on the two versions it could be time to drop 2.2.10 06/09 22:01 it was already starting to be painful to keep things building on both 06/09 22:02 I'm amazed you've lasted this long 06/09 22:07 well, i kind of meant for the library, not just me 06/09 22:19 oh :) 06/09 22:21 yeah, compatibility has never been a big concern of mine, if you hadn't noticed 06/09 22:21 gah, how do i undo a git commit?  (i want to keep the change, just forget the actual commit) 06/09 22:50 can't remember, but maybe you just want to amend the last one? 06/09 22:51 there's a git commit --amend 06/09 22:51 unfortunately there were two 06/09 22:57 basically a while ago i had forgot i was in a branch and started committing stuff 06/09 22:59 after 2 commits in i was all 'd'oh i am in the wrong branch' 06/09 22:59 so even amend wouldn't actually work 06/09 23:00 i need to recommit stuff in a branch of the branch, then rebase that to master and merge it 06/09 23:00 but i don't know how to kill those 2 commits from the old branch tip so i can take them with me 06/09 23:02 probably with git reset, but i wouldn't know the right flags 06/09 23:04 when in doubt, rewrite history 06/09 23:10 call the doctor 06/09 23:12 maybe merge to the new branch, rebase out the merge commit, and rebase the merged commits out of the old branch? 06/09 23:26 --- Day changed Wed Sep 07 2011 Yes, you want a mixed git reset 07/09 00:07 Wait, you don't... you could just switch to the other branch and cherry-pick your commit on top 07/09 00:08 git cherry-pick 07/09 00:09 i was thinking i'll probably reset the branch to an earlier commit, then create a new branch with the old tip 07/09 02:29 and then rebase it to the place i want 07/09 02:30 agh, i upgraded debian, and mplayer started segfaulting.  tried to upgrade through it, and i have to bring libc, gtk, and perl up to testing 07/09 02:44 oh, and gcc-4.4 07/09 02:45 and incidentally irssi 07/09 02:46 if i were on nix i could have just reversed the upgrade 07/09 02:46 and now i'm getting internal errors from apt, brilliant! 07/09 02:48 oh, and now perl made me upgrade elinks, which is making me upgrade ruby 07/09 02:55 oh, shit.  can't upgrade perl, because there's no new version of postgresql-plperl-8.3 07/09 02:58 wtf.  carefully matched all the versions of everything to use the stable packages from christian mariallat where available, still segfaulting :( 07/09 03:36 xplat: you might want to get xine or something else in the meanwhile 07/09 03:45 or vlc 07/09 03:45 Maybe it'll just get fixed. 07/09 03:46 in the meantime, i used vlc, but unfortunately it's a piece of crap 07/09 04:23 what kind of video player comes with default keybindings for cycling through aspect ratio and crop, and speeding up and slowing down, but not adjusting volume or advance/rewind? 07/09 04:24 or if it has them i haven't found them yet 07/09 04:25 http://hpaste.org/51051 <- anyone knows if there's already an open issue about this with darcs agda? 07/09 17:13 Saizan: is it specific to coinduction? 07/09 17:48 btw, http://hpaste.org/51053 07/09 17:48 i couldn't trigger it without 07/09 17:48 also a bug from today noon agda, seems related to projections 07/09 17:49 where's the projection there? 07/09 17:51 Saizan: yours seems to be the well-known 'too much generativity' bug 07/09 17:51 the flat should be squashing the generativity 07/09 17:51 i think the problem is that it doesn't get computed all the time 07/09 17:52 i've reported it as new anyhow 07/09 17:53 oic 07/09 17:56 while you're at it could you report mine too?  i haven't a google account 07/09 17:57 the error message is '.n