augur augur augur --- Log opened Wed Jun 01 00:00:16 2011 dolio: x3 01/06 00:01 i feel as tho induction-recursion is induction where some of the params/indices are calculated by recursion 01/06 00:02 but im probably wrong 01/06 00:02 It's a simultaneous definition. 01/06 00:02 hmm 01/06 00:02 example? 01/06 00:02 Where you define constructors of a family F by induction. 01/06 00:03 hmm 01/06 00:03 And they're allowed to make reference to a function defined by recursion over F . 01/06 00:03 example? :P 01/06 00:03 A simple example is lists of unique values. 01/06 00:04 Suppose we have an equality test for T. 01/06 00:04 data Uniq : Set where nil : Uniq ; cons : (x : T) -> (xs : Uniq) -> x notElem xs -> Uniq 01/06 00:05 supposing 01/06 00:05 ok 01/06 00:05 _notElem_ : (x : T) -> (xs : Uniq) -> Set 01/06 00:05 ok 01/06 00:06 Actually, scratch that, you don't even need a test. 01/06 00:06 Yup... emb (Fin.zero {n}) = Fin.zero {ℕ.suc n}    emb (Fin.suc {k} n) = Fin.suc {ℕ.suc k} (emb n) 01/06 00:06 Eduard_Munteanu: do you even need to explicitly look at those implicits? 01/06 00:06 x notElem (cons y ys _) = (x /= y) * (x notElem ys) 01/06 00:06 Eduard_Munteanu: I'm pretty sure it can infer them for you 01/06 00:06 Ah, I think so. 01/06 00:07 * Eduard_Munteanu tries 'max' 01/06 00:07 So, you're simultaneously defining Uniq and _notElem_. 01/06 00:08 Wait, I can't write 'max' for Fin 0... 01/06 00:08 Erm, well I could set it to zero, but anyway. 01/06 00:08 Eduard_Munteanu: no you couldn't 01/06 00:08 yes you can.  max () () 01/06 00:08 Ah, right. 01/06 00:09 nope 01/06 00:09 (can write it, not can set it) 01/06 00:09 max : forall {n} -> Fin n 01/06 00:09 * Eduard_Munteanu actually tries writing it now... 01/06 00:09 that's me being dumb 01/06 00:09 max : forall {n} -> Fin (suc n) 01/06 00:09 :) 01/06 00:09 Ah. :) 01/06 00:09 you couldn't write it otherwise 01/06 00:09 dolio: are you really simultaneously defining it tho?? 01/06 00:10 well i guess you are 01/06 00:10 Yes. 01/06 00:10 both depend on one another 01/06 00:10 oh, the ONE-argument max 01/06 00:10 It requires the mutual keyword in Agda. 01/06 00:10 ok 01/06 00:10 dolio: do you know anything about ornamentation? 01/06 00:10 yeah, you can't write that to work on Fin 0 01/06 00:10 max {n} = fromℕ n :) 01/06 00:10 Of course, regular definitions are sort of a special case of inductive-recursive definitions. 01/06 00:11 Well, I suppose I could pattern-match further so I don't use fromN 01/06 00:11 Where you don't even bother to specify the recursive function, and don't make use of it in the type. 01/06 00:11 No, I've never read about ornaments. 01/06 00:11 Wait why mutual? 01/06 00:12 You need to use the mutual keyword for mutually recursive definitions. 01/06 00:12 Otherwise Agda assumes definitions can be processed one at a time. 01/06 00:12 Why is it set up that way anyways? 01/06 00:13 i worked out that syntax example from earlier a bit further, but now it's too big to display as a screenshot :I 01/06 00:13 max {zero} = zero     max {suc n} = suc (max {n}) 01/06 00:13 Or the point was to avoid implicits? 01/06 00:13 It makes it easier on the compiler if you manually annotate your strongly connected components, I think. 01/06 00:13 Eduard_Munteanu: you could hardly write that while avoiding the implicits 01/06 00:14 Ah, I thought dolio was telling me max needed mutual 01/06 00:14 Although augustss isn't happy about it. 01/06 00:14 Now for the view... 01/06 00:15 hmm 01/06 00:15 I'm not sure there's any stronger reason than it makes things easier to implement. 01/06 00:15 anyone know of any really good papers about getting indices to really do a lot of work? 01/06 00:15 < copumpkin> the view will give you the embedding or the max   -- so view : forall {n k} -> Fin n -> Fin k ? 01/06 00:16 Or did you mean the embedding _and_ max? 01/06 00:17 *sigh* 01/06 00:29 view : (n k : ℕ) → Fin n → Fin k    view n k a with Data.Nat._≤?_ (ℕ.suc n) k 01/06 00:29 no ey 01/06 00:30 ... | yes a = ?    ... | no a = ?      but Agda doesn't like the 'yes a' there. Any ideas? 01/06 00:30 Eduard_Munteanu: my suggestion is this: 01/06 00:30 dont fill in the cases 01/06 00:31 just do ... | answer = ? 01/06 00:31 load it up 01/06 00:31 and then C-c C-c on answer 01/06 00:31 and let agda figure out what the cases should be 01/06 00:31 itll put in all and only the cases it DOES like 01/06 00:31 Ah, yeah, I don't even need to spell out "yes" or "no" 01/06 00:32 Ah, right, I didn't import Relation.Nullary.Core.Dec 01/06 00:32 blah 01/06 00:33 my body feels like im hungover :\ 01/06 00:33 Thanks , 'with' works now 01/06 00:34 Eduard_Munteanu: the view is an indexed datatype 01/06 00:40 Eduard_Munteanu: then you'd have a function that views any Fin 01/06 00:41 forall {n} -> (f : Fin n) -> EmbMax f 01/06 00:41 if you finish that and want more to do, there's also the invert function 01/06 00:43 Fin n -> Fin n 01/06 00:43 copumpkin: can you think of any relatively simple functions that are uniquely determined by some property they have? 01/06 00:44 that embMax view I just mentioned is uniquely determined 01/06 00:46 by its type 01/06 00:46 but that's not painfully simple 01/06 00:47 hm 01/06 00:47 im just looking for something that isnt obnoxiously complicated 01/06 00:47 that i can use as a simple example of doing definition by property satisfaction 01/06 00:48 work with functions on booleans 01/06 00:51 it seems like there should only be one group on the booleans? 01/06 00:52 maybe not 01/06 00:52 hmm 01/06 00:53 i think maybe i'll try to do the Theorems-for-Free stuff backwards 01/06 00:53 or at least one of them 01/06 00:53 or maybe something like map 01/06 00:53 not sure you can even prove something like : (f : forall a. a -> a) -> (A : Set) -> (x : A) -> x == f x 01/06 00:55 in fact, I'm pretty sure you can't 01/06 00:55 ey? 01/06 00:56 copumpkin: wat? 01/06 01:12 wat? 01/06 01:12 so, hypothesis: there is exactly one group on the booleans 01/06 01:12 too lazy to exhaustively check 01/06 01:13 false: && and || are both groups 01/06 01:13 er, not groups, monoids 01/06 01:13 yeah, I knew that 01/06 01:13 but neither of those is a group 01/06 01:13 okay, groups.  xor is a group.  equiv has ... \all x -> x equiv true == x.  is false its own inverse?  yes, false equiv false == true 01/06 01:14 but is it associative? 01/06 01:15 I'd hope so 01/06 01:16 isn't that just transitivity of == ? 01/06 01:16 okay, not transitivity 01/06 01:17 quickcheck? :P 01/06 01:17 Smallcheck. 01/06 01:18 @check \x y z -> ((x == y) == z) == (x == (y == z)) 01/06 01:18 "OK, passed 500 tests." 01/06 01:18 @check \x y z -> ((x == y) == z) == (x == (y == (z :: Bool))) 01/06 01:18 "OK, passed 500 tests." 01/06 01:18 @scheck \x y z -> ((x == y) == z) == (z == (y == (z :: Bool))) 01/06 01:18 "Falsifiable, after 1 tests:\nTrue\nFalse\nFalse\n" 01/06 01:18 @scheck \x y z -> ((x == y) == z) == (x == (y == (z :: Bool))) 01/06 01:18 "OK, passed 500 tests." 01/06 01:18 agrees with my result.  so, equiv is a group. 01/06 01:20 i think they're isomorphic through 'not' 01/06 01:20 (which is why i suggested it in the first place) 01/06 01:22 yes! 01/06 01:23 you could also use http://math.andrej.com/2011/01/22/alg/ 01/06 01:24 well, I'm now wondering if there's some definition of property such that forall properties P, structures on Bool appear twice (so there's a multiple of two of them) 01/06 01:25 but that thing looks cool 01/06 01:25 So, what you get with homotopy type theory... 01/06 01:26 Is that if P : Set -> Prop... 01/06 01:26 And P T, and T is isomorphic to U, then P U. 01/06 01:26 Why doesn't this pass the strict positivity test: http://hpaste.org/47320/not_working when this does: http://code.haskell.org/~Saizan/UCodes.agda ? 01/06 01:50 hm! 01/06 02:00 i can derive a definition for map! 01/06 02:00 relational map, anyway 01/06 02:00 eee\la 01/06 02:06 copumpkin: chekidout 01/06 02:08 https://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda 01/06 02:08 Now it's down to μ₁ working when μ₂ doesn't :-( http://hpaste.org/47321/not_working_annotation 01/06 02:08 Saizan: you checkit too :D 01/06 02:13 Hmm. I forget who in here actually mentioned that Oregon summer school... 01/06 02:17 Ah, ccasin? 01/06 02:17 what summer school :o 01/06 02:18 Haven't I mentioned this to you before augur? :p http://www.cs.uoregon.edu/Activities/summerschool/summer11/ 01/06 02:25 oh that one 01/06 02:25 some people have discussed it, me being one, yeah 01/06 02:25 i wonder if i can plausibly take the propositional definition of map and just drop it down into the value domain 01/06 02:31 once i know map f nil nil = \Top ; map f (x :: xs) (y :: ys) = f x y * map f xs ys 01/06 02:32 can i just drop that into 01/06 02:32 map f nil nil = true ; map f (x :: xs) (y :: ys) = f x y && map f xs ys 01/06 02:32 i mean, its certainly true that it works in this case but is it general, i wonder 01/06 02:32 probably 01/06 02:34 sets are just values and whats one value vs another, i suppose 01/06 02:34 you can generally only turn real predicates into boolean predicates if they are decidable 01/06 02:51 xplat: hm! 01/06 02:52 well thats ok 01/06 02:52 i only care about decidable things 01/06 02:52 :) 01/06 02:52 Silly question - so in Observational Equality, Now! it references their development in Agda as being available as a standard example. ...where? I swear I didn't see it in the standard lib or anything. 01/06 03:19 caylee: what sort of stuff are you looking for? 01/06 03:26 Do they actually say it's in the stdlib? 01/06 03:26 No, they just say that it's available as an example with the distribution of Agda - of course this was 3 years ago I believe 01/06 03:29 and I was wondering if the OTT development was still anywhere to be found 01/06 03:29 caylee: hm, maybe it's in the Agda latest darcs / package 01/06 04:09 ? 01/06 04:09 There is an examples/ dir there. 01/06 04:09 Eduard_Munteanu: did you succeed!? 01/06 04:10 copumpkin: did you look? :o 01/06 04:15 not yet 01/06 04:16 :( 01/06 04:16 gimme a few to finish this video 01/06 04:16 copumpkin: ah no, I took a break, had to work on some C code :) 01/06 04:19 http://vimeo.com/16534403 is nice 01/06 04:30 copumpkin: :| 01/06 04:37 I'm on the phone! 01/06 04:37 :| 01/06 04:37 so mean 01/06 04:37 lol 01/06 04:37 What HTML5 codecs is Vimeo using? I'm using Firefox 4, but it's complaining. 01/06 04:49 augur: looking now 01/06 05:06 :D 01/06 05:06 augur: I'm confused 01/06 05:06 ok 01/06 05:06 map-theorem : ∃ (∀ {X Y n} 01/06 05:07 → (X → Y → Set) → Vec X n → Vec Y n 01/06 05:07 → Set) 01/06 05:07 (λ map → (X Y : Set) (n : ℕ) (f : X → Y → Set) (xs : Vec X n) (ys : Vec Y n) 01/06 05:07 → map f xs ys ↔ ((i : Fin n) → f (proj xs i) (proj ys i))) 01/06 05:07 that type 01/06 05:07 yes 01/06 05:07 it feels like it should have more parentheses 01/06 05:08 why 01/06 05:08 (∀ {X Y n} → (X → Y → Set) → Vec X n → Vec Y n) 01/06 05:08 that alone is the type of a map for vectors 01/06 05:08 sort of, anyway 01/06 05:08 oh I see 01/06 05:08 no no 01/06 05:08 yeah 01/06 05:08 yeah, I'm dumb 01/06 05:08 its relational map 01/06 05:09 not functional map 01/06 05:09 yeah 01/06 05:09 okay, ignoe me 01/06 05:09 i shouldve put the Vec's on the line after that 01/06 05:09 to make it more symmetric 01/06 05:09 looks cool 01/06 05:10 however 01/06 05:10 map f nil nil = ⊤ 01/06 05:10 map f (x :: xs) (y :: ys) = f x y ∧ map f xs ys 01/06 05:10 that kind of thing is where I'd probably start making my own types 01/06 05:10 ? 01/06 05:10 that's basically defining a type, right? 01/06 05:11 yes 01/06 05:11 well 01/06 05:11 not quite 01/06 05:11 but i mean, sure 01/06 05:11 data MapRel (X Y : Set) : {n} -> Vec X n -> Vec Y n -> Set where 01/06 05:11 nil : MapRel nil nil 01/06 05:11 cons :  blahblah 01/06 05:11 well 01/06 05:12 im not sure how that would integrate with the definition discovery component 01/06 05:12 see, the point is 01/06 05:12 the value for map f nil nil wasnt decided on, it was discovered 01/06 05:12 the first case for the proof p determined that the value of map f nil nil should be something that's provable in some general fashion 01/06 05:13 you discovered it, but you haven't proved that it's the only definition 01/06 05:13 and it isn't the only definition 01/06 05:13 oh im not saying it is 01/06 05:14 i said it's _a_ definition 01/06 05:14 thats all im interested in right now 01/06 05:14 ah 01/06 05:14 given some property that the function must have, can we find a definition 01/06 05:14 and how 01/06 05:14 well, creating an inductive family to define your relation can be a process of discovery too, just as much as that function :) 01/06 05:14 just saying it'll be more fun to work with later if you do it that way, but I see that isn't the point 01/06 05:15 im not sure how to do that with this 01/06 05:15 yeah, you can't use holes in the same way 01/06 05:17 well 01/06 05:18 i could leave some of it missing and add it when i need more cases 01/06 05:18 but im not sure what that would do for me 01/06 05:18 well, in general, it lets you pattern match on the proof and get more information by doing so 01/06 05:22 rather than pattern matching on something that then gives you more information about something else which you also match on 01/06 05:23 oh sure, but the point isnt really to define map in a way thats usable and informative 01/06 05:23 rather, to discover the stucture of such a definition 01/06 05:23 yeah 01/06 05:23 so what do you think of the general structure of the method, copumpkin 01/06 05:25 i suppose its something of a proof pattern 01/06 05:25 or something 01/06 05:26 it looks rather indirect 01/06 05:26 it lets you do what you want to do with it 01/06 05:26 but it feels like there should be a more straightforward way? 01/06 05:26 i know 01/06 05:26 i'd like to find a more straightforward way too! 01/06 05:27 copumpkin: im not really sure how to clarify it any further tho 01/06 05:32 this will make it all clear: http://www.youtube.com/watch?v=lBC6z6xcnFM 01/06 05:32 i feel like what you'd want to do is put the proofs for each case along side the definition cases 01/06 05:33 or indeed, derive the definition cases from the proofs somehow 01/06 05:33 but im not sure how to achieve that 01/06 05:34 copumpkin: any ideas? 01/06 06:05 How can I see what a meta refers to without correcting errors? 01/06 11:14 Hi, is it possible to specify an implicit argument while using a function in a mixfix way? 01/06 13:32 no 01/06 13:55 Saizan: Is there a particular reason ou defined _==_ as _\==_?  The tutorial uses the former name. 01/06 14:05 sshc: the stdlib uses the latter 01/06 14:10 * sshc nods 01/06 14:10 i came up with a new way to avoid the 'all yellow' problem with my <_>,<_> operator, but it doesn't work because no modules are allowed in mutual blocks 01/06 15:28 argh 01/06 15:34 once again i tried defining it outside the abstract block, once again every occurrence fails to solve for two objects 01/06 15:35 djahandarie: yeah, it was probably me - are you coming? 01/06 15:48 it's going to be fun! 01/06 15:48 it seems like it can't figure out the destination of arrows f and g from \< f , g \> 01/06 15:51 ccasin, yep! 01/06 15:51 or from the type of same 01/06 15:51 How many people usually show up at these things anyways? 01/06 15:51 djahandarie: I think it's pretty big, say 100 people.  They might have a list on the website already, let me see 01/06 15:52 Oh wow, that's pretty big 01/06 15:53 Was expecting like ~35-40 01/06 15:54 looks like last year there were 95 or so.  I'd guess it will be a similar size this year 01/06 15:54 sorry, make that 86 last year 01/06 15:55 so this year there should be 99 01/06 15:56 I'll have to do my best to absorb all information possible 01/06 15:57 I hope some of the lectures go into hardcore category theory 01/06 15:57 sure, but don't stress out about it too much - the best part is hanging around with 100 other type theory nerds for two weeks 01/06 15:57 lectures or not 01/06 15:58 you're bound to learn loads 01/06 15:58 Hardly stressing out about it, more interested in efficent absorbtion. :p 01/06 15:58 :) 01/06 15:58 they'll all be like "wtf is this young dude doing here??" 01/06 15:59 i don't get this at all, the abstract type of <_,_> should be plenty to recover the targets of its arguments 01/06 15:59 * djahandarie prepares his assimilation beam 01/06 15:59 copumpkin, I'm not /that/ young looking :p 01/06 15:59 you should go around telling everyone you're in middle school, just to fuck with them 01/06 15:59 Haha 01/06 15:59 make them feel really bad about themselves 01/06 15:59 * copumpkin just received an RSA securid! 01/06 15:59 zomg 01/06 15:59 now I can get hacked just like the big guys did 01/06 16:00 copumpkin: help!  i want to get this over with so i can start porting to stdlib :( 01/06 16:01 Hmm, only lecture that mentions categories is "Programming languages in string diagrams" 01/06 16:01 xplat: what's wrong? sorry, haven't really been following :) 01/06 16:01 what code is this? 01/06 16:01 copumpkin: Category.Object.BinaryProducts.Abstract.HomReasoningP defines <_>,<_> as 'the same thing as <>-cong₂ plsthx' 01/06 16:03 oh, that thing! 01/06 16:03 copumpkin: but unlike the former it fails (100% of the time) to solve A and B, which are the targets of the arrows being <_,_>·d 01/06 16:04 copumpkin: this problem goes away if it's defined in the abstract block, but i don't know why it goes away, nor why it exists in the first place 01/06 16:05 I remember looking at this last time you mentioned it and maybe it's a bug? could be worth posting to the mailing list 01/06 16:05 also, i can't figure out any way to have it appear in the right scope if it's defined in the abstract block 01/06 16:05 I keep on ending up at linear logic and linear type theory in my internet traversals. Maybe I should do something with it. 01/06 16:07 have you read the ATTaPL chapter on it? 01/06 16:08 I haven't, maybe I'll do that 01/06 16:08 djahandarie: I highly recommend Frank Pfenning's lecture notes too, for a good introduction.  They are somewhere on his website 01/06 16:08 linear logic is well-known as the only field of knowledge that allows you to use an upside-down ampersand as a legitimate piece of math notation 01/06 16:08 Heh 01/06 16:09 copumpkin, do you have symmetric monoidal categories in your lib? 01/06 16:09 not symmetric yet 01/06 16:09 Only braided? 01/06 16:09 not even braided 01/06 16:10 no, just monoidal 01/06 16:10 :( 01/06 16:10 we have cartesian and monoidal 01/06 16:10 :) 01/06 16:10 How about closed? 01/06 16:10 feel free to add braided or symmetric 01/06 16:10 nope 01/06 16:10 or add closed :P 01/06 16:10 I don't think I could actually do any of the proofs for these 01/06 16:11 closed might take some work if I want to start with closed non-monoidal and then move up 01/06 16:11 I need extranatural transformations I think before I can even write that 01/06 16:11 i'm a little fuzzy on what closed actually means without a monoidal product you want to be able to curry 01/06 16:11 Same 01/06 16:12 http://ncatlab.org/nlab/show/closed+category 01/06 16:12 copumpkin: lmncltfy? 01/06 16:13 lol 01/06 16:13 yeah! 01/06 16:13 Haha 01/06 16:13 * djahandarie already got off that page and started reading about Cat_g 01/06 16:14 Stop linking me to ncatlab when I'm at work! ;) 01/06 16:14 I really need brush up on adjoints and pullbacks and such 01/06 16:15 * copumpkin screams: http://www.reddit.com/r/programming/comments/ho20s/imperative_vs_functional_programming/c1x6n1z 01/06 16:17 This looks like a good link 01/06 16:18 * copumpkin wants to strangle someone 01/06 16:18 why am i following this link?  surely nothing good can come of this 01/06 16:18 haha, if you don't like objects you are a climate change denier 01/06 16:18 priceless 01/06 16:18 well, my previous point was that I found it hard to believe that people had actually done research claiming that it's "more natural" to believe in OO 01/06 16:19 since it's impossible to control all variables that would be required to make such a strong claim 01/06 16:19 i would definitely believe that it is more natural for rhesus monkeys to program in OO 01/06 16:20 generalizing this result to humans seems premature 01/06 16:21 yes, this style of argument is silly.  We'll never all agree on what style of programming is the "most natural to humans".  But we can agree on which style of programming humans have had the best success reasoning _about_ 01/06 16:22 I, for one, like writing correct programs :) 01/06 16:22 I suppose there aren't many imperative programmers left to convince in #agda... 01/06 16:25 the cited paper is interesting but only slightly on-point 01/06 16:26 Oh, great comments on the article itself too 01/06 16:31 heyo 01/06 16:51 i hope i can get this working somehow, because it is far nicer to write something like 01/06 18:12 ↑⟨ ⟨ assoc ⟩,⟨ ⟨ assoc ⟩,⟨ refl ⟩ ⟩ ⟩ 01/06 18:12 rather than ↑⟨ ⟨⟩-cong₂ assoc (⟨⟩-cong₂ assoc refl) ⟩ 01/06 18:14 yeah 01/06 18:44 I'd honestly send an email to the mailing list 01/06 18:44 copumpkin! 01/06 18:45 :D 01/06 18:45 yo dawg 01/06 18:45 lets figure out how to make this proof more elegant! 01/06 18:45 how about let's work 01/06 18:46 thats what i said! 01/06 18:46 I have a day job :P 01/06 18:46 day jobs are for chumps 01/06 18:46 your job is to do this stuff, mine is not :P 01/06 18:46 :) 01/06 18:47 im not really sure how to avoid the use of internal definitions and with 01/06 18:48 and i think that forces a certain structure onto things 01/06 18:49 copumpkin: i'm trying to create a small example 01/06 18:55 xplat: have you seen my little deduction of relational map? :D 01/06 18:59 argh 01/06 19:00 my small example works correctly!  damn it. 01/06 19:00 is it talk like a pirate day already? 01/06 19:00 ARR matey 01/06 19:01 @arr 01/06 19:01 I'll crush ye barnacles! 01/06 19:01 > (arr (+1) >>> arr (*2)) 5 01/06 19:02 mueval-core: Time limit exceeded 01/06 19:02 o.O 01/06 19:02 hmm 01/06 19:02 nae, that'd be 'arr, my small example ain't half near as yellow as a lily-livered spaniard!  scupper me wi' a cutlass, arr.' 01/06 19:02 maybe i can define some sort of eliminator-like thing that breaks down existential proofs into their cases 01/06 19:03 or something like that 01/06 19:03 im not sure how that'd really work tho 01/06 19:03 no it probably couldnt actually 01/06 19:03 does the stdlib define product of setoids anywhere? 01/06 19:39 I suspect not. 01/06 19:42 Setoids don't get much love 01/06 19:43 well, they are kind of a pain to use :( 01/06 19:50 i am totally failing at reducing this to a smaller test case 01/06 19:50 okay, here's an example of how setoids are a pain to use: there's a way to define a functionspace setoid from one setoid to another setoid or family of setoids 01/06 19:52 but for a functionoid you have to write f : (Q ⟶ A) 01/06 19:53 but the setoid of functionoids is Q ⇨ A 01/06 19:54 and there's no nice inline way to get from one to the other (either direction) without importing either Setoid.Carrier (with frozen level arguments if you open, ugh) or else reconstructing Q ⇨ A from Q and A yourself 01/06 19:56 basically this comes down to the fact that the translation from setoid to Set forgets all the setoid structure so you have to pass it separately 01/06 19:58 of course i can't figure out a better way to do this because if you wrap it in a sigma/record of which setoid it is you'll need to prove things are in the same setoid before you compare them 01/06 19:59 which is even more awkward 01/06 20:00 (and is an example of how the type system treats sigmas as second-class compared to pis even with all agda's special record support) 01/06 20:02 What was the type on f? Windows is not advanced enough to display it. 01/06 20:04 Anyhow, I agree they're a pain to use. 01/06 20:05 Same, can't see the type of f. Unless that is actually suppose to be a box. 01/06 20:09 type of f is Q \r-- A 01/06 20:10 setoid of functionoids is Q \r7 A 01/06 20:10 anyway, you end up with types like  ∀ {A B C : Setoid ℓ e} {f f′ : C ⟶ A} {g g′ : C ⟶ B} → Setoid._≈_ (C ⇨ A) f f′ → Setoid._≈_ (C ⇨ B) g g′ → Setoid._≈_ (C ⇨ A ×̃ B) ⟨ f , g ⟩ ⟨ f′ , g′ ⟩ 01/06 20:11 dolio! 01/06 20:41 Berengal!! 01/06 20:54 say, why won't blah : 0 \== 0 ; blah = _ resolve? 01/06 21:00 it can only infer _ if it's a record 01/06 21:00 I'd assume it could be made a little bit more clever 01/06 21:00 so only for records will it refine a _ to a constructor without unifying wiht a constructor that already exists 01/06 21:26 even if the type of the _ is a data with only one constructor 01/06 21:27 yeah, it doesn't know that the indices allow the constructor to be introduced 01/06 21:33 Eta expansion will turn the _ into record {}. 01/06 21:45 But there's no eta expansion for data. 01/06 21:45 copumpkin: how do i eval something in aquamacs? 01/06 22:53 Saizan: thanks (for your reply in the morning) 01/06 22:57 Favonia: heh, np 01/06 22:59 Hello everybody, is there any difference between ∀ {x : A} → ... and {x : A} → ? I only noticed the difference when it is ∀ {A} → ... and {A} → .... Also, is ∀ {A} equivalent to ∀ {A : Set} ? 01/06 22:59 Saizan! :o 01/06 23:00 ∀ {x : A} → ... and {x : A} → are the same 01/06 23:00 {A} -> ... is illegal 01/06 23:00 and ∀ {A} -> .. is the same as {A : _} -> .. 01/06 23:01 so copumpkin: i think i've found a bit of a general pattern going on here 01/06 23:01 { A : _} ? cool! 01/06 23:01 I've never thought that the underline can be used in the signature :P 01/06 23:02 it can be used anywhere :) 01/06 23:02 for the map case, anyway 01/06 23:02 Saizan: so I guess forall is actually a syntax sugar, right? 01/06 23:03 crap!  i've created an example with setoids, and it doesn't have the problem either 01/06 23:03 for map it looks like you have this thing,   H R = ∀ X Y n (f : X → Y → Set) (xs : Vec X n) (ys : Vec Y n) → R X Y n f xs ys 01/06 23:03 and the type of the witness is H (λ _ _ _ _ _ _ → Set) 01/06 23:04 Favonia: yep, it's so you can avoid giving type signatures to parameters 01/06 23:04 and the type of the proof is H (λ X Y n f xs ys → map f xs ys ↔ ((i : Fin n) → f (proj xs i) (proj ys i))) 01/06 23:04 Favonia: you do see a difference with ∀ A -> B and A -> B 01/06 23:05 copumpkin: im not sure what such a beast as H is, but 01/06 23:05 in the former, A is the parameter name and the type is _, in the latter A is the type and there is no name 01/06 23:05 nor what the operation is that turns  H ...  into H ...' 01/06 23:05 Saizan: cool. if ∀ {A} is translated into {A : _}, what will "∃ blah" be translated to? 01/06 23:05 xplat: I see 01/06 23:05 i guess if you wanted to be obscure as possible you could write _ -> B :) 01/06 23:06 xplat: haha 01/06 23:06 there's no ∃ syntactic sugar, but Data.Product defines a ∃ 01/06 23:06 Saizan: thanks. I'll take a look on it 01/06 23:06 \exists and sigmas in general have no magic, except for the occasional syntax declaration someone might have done 01/06 23:07 Also a general question: are there any general libraries for basic number theory? or example, what would you suggest if I want to prove that the number of primes is countably infinite :P 01/06 23:08 so you have to write things like \Sigma[ x \: A ] B where \: isn't an actual : but kind of looks like one 01/06 23:08 I see there are Coprime and GCD 01/06 23:08 xplat: hmmm 01/06 23:09 there is syntax magic to define records, but nothing for one-off sigmas 01/06 23:10 xplat: I am sorry but what is "one-off" sigmas? 01/06 23:11 xplat: I see the line "syntax Σ A (λ x → B) = Σ[ x ∶ A ] B" in the std lib 01/06 23:14 --- Day changed Thu Jun 02 2011 'one-off' means a specific type you use only in one place 02/06 00:06 pi types get special treatment for that situation, sigma types do not 02/06 00:07 that syntax line kind of fakes up what it might look like if they did 02/06 00:07 but if it were built-in it would be more consistent with the syntax of functions and other binders 02/06 00:08 xplat: i think its important that you can build sigmas from prods 02/06 00:17 i mean, important in the underlying sense 02/06 00:18 that sigmas aren't necessarily primitive, so long as you have dependent functions 02/06 00:18 hmm 02/06 01:32 the new OAAO paper is like twice the original length 02/06 01:32 interesting 02/06 01:32 hmm interesting 02/06 14:15 is there a way to show some sort of natural correspondence between \ () and \top ? 02/06 14:16 or well.. i suppose a natural correspondence between something like 02/06 14:17 \bot -> X and \top 02/06 14:17 where \() ~ tt 02/06 14:17 maybe.. \bot -> Set ~ \top perhaps 02/06 14:19 no i think its really \ () : \bot -> Set ~ \top : Set 02/06 14:23 thats the relation thats important 02/06 14:23 i suppose it could go by way of \bot -> Set ~ \top tho 02/06 14:24 \ () ==type==> Zero -> Set ==iso==> One   but is there a general thing iso that will do that more generically? hm. 02/06 14:26 hmm 02/06 16:37 why wont this syntax definition work: syntax caseP z (λ x y → f x y) xs = case xs []→ z [ x ∷ y ]→ f x y 02/06 16:37 augur: I don't think you're supposed to have that 'f x y' part on the rhs there 02/06 16:38 Have you seen the one for bind? 02/06 16:39 oh maybe thats it 02/06 16:40 'f' should be enough I think 02/06 16:40 The lambda on the lhs should bring x and y into f's scope, granted f must take two parameters. 02/06 16:40 mm nope, not working either 02/06 16:40 I'm also worried about that 'case'. 02/06 16:41 Does it say you don't have alternating holes and non-holes? 02/06 16:41 its just giving me a parse error 02/06 16:42 Could you repaste what you have? 02/06 16:42 syntax caseP z (λ x y → F) xs = case xs []→ z [ x ∷ y ]→ F 02/06 16:42 Syntax/algebraic-syntax/Map.agda:25,21: Parse error y → F) xs = case xs []→ z [ x ∷... 02/06 16:43 Hrm, I didn't try using two things in a lambda. 02/06 16:44 ahh thats the problem 02/06 16:44 how obnoxious 02/06 16:44 thats stupid 02/06 16:45 augur: try defining _∷_ as _,_, and replace x ∷ y by some 't'. Then you can use projections I guess. 02/06 16:45 meh. its not that important 02/06 16:46 Are you trying to define case-of expressions for lists? 02/06 16:48 Eduard_Munteanu: yeah, for convenience 02/06 16:52 i looked and didnt see a predefined one 02/06 16:52 I'm not sure you can make it pattern-match, though. 02/06 16:53 The _∷_ in your syntax won't do anything wrt the list _∷_ 02/06 16:54 ofcourse not 02/06 16:54 but im not asking it to! 02/06 16:55 caseP does the pattern match 02/06 16:55 In which case it's more like an if-empty-then_else_ :) 02/06 16:55 case_[]->_[_::_]->_ is just sugar! 02/06 16:55 Damn, case expressions would be really nice to have. 02/06 16:56 i dont actually need them for definitions 02/06 16:56 its for types 02/06 16:56 im trying to define a proposition thats provable differentially 02/06 16:57 P [] = \top ; P (x :: xs) = ... 02/06 16:57 ehh no i can get away with using something else actually 02/06 16:59 whats a good code font :| 02/06 17:53 ahh courier 13 is what im seeing for the library 02/06 17:55 i shall continue using monaco 13 02/06 17:57 monaco 12 even! 02/06 18:39 I use DejaVu Sans Mono. 02/06 18:48 11, I think 02/06 18:49 Proportional fonts might look nicer depending on what sort of unicode magic you might be writing, I guess. 02/06 18:50 i use unicode /everywhere/ 02/06 18:51 * djahandarie thinks augur is very much the opposite of himself 02/06 18:51 I wonder what sort of category I am 02/06 18:53 or at least what kind you're in 02/06 18:53 the category Hum 02/06 18:53 for hummus 02/06 18:55 i want to write code in the font that is used for lagda documents :| 02/06 19:36 "    z =/= b : {n : Nat}   ->            zero   =/= succ n 02/06 20:29 " Why can't "z" and "b" be replaced with "_"? 02/06 20:29 AgdaBasics.agda:674,5: Parse error _ =/= _ : 02/06 20:30 {n : Nat} -> ... 02/06 20:30 huh 02/06 20:30 you want it part of the operator 02/06 20:30 _=/=_ 02/06 20:30 you dont put spaces there, sshc 02/06 20:30 \==n is a nicer symbol, too 02/06 20:30 and you dont put the arguments in the lhs of the type 02/06 20:30 Oh.  I see 02/06 20:31 so you couldnt do z =/= b even if you wanted to, afaik 02/06 20:31 unless that's supposed to be a constructor z=/=b? 02/06 20:31 napping: It was.  I read the tutorial wrongly 02/06 20:32 have you done much with the inequality? 02/06 22:17 sshc, you might also try 02/06 22:17 data _≢_ {A : Set} : A → A → Set where 02/06 22:17 different : {a b : A} → .(a ≡ b → ⊥) → a ≢ b 02/06 22:18 it's kind of interesting, with the irrelevant argument you can prove 02/06 22:18 neq-eq : {A : Set} {a b : A} (p q : a ≢ b) → p ≡ q 02/06 22:18 you can even extract a refutation 02/06 22:18 neq-not-eq : {A : Set} {a b : A} → a ≢ b → a ≡ b → ⊥ 02/06 22:19 i feel like this isnt terribly surprising 02/06 22:26 well, the refutation extraction anyway 02/06 22:27 neg-not-eq (different ref) = ref 02/06 22:27 how is that allowed? 02/06 22:28 how isnt it? 02/06 22:28 well, that component is marked irrelevant 02/06 22:29 well then unmark it irrelevant! 02/06 22:29 i dont really get the whole irrelevant thing 02/06 22:29 at least in constructors like that 02/06 22:29 The point is to mark it irrelevant so different equality proofs are equivalent 02/06 22:29 i get it when pattern matching -- duplication of information, etc. 02/06 22:30 but i dont know how it would work for constructors 02/06 22:30 You definition is accepted anyway 02/06 22:30 well then! 02/06 22:30 something seems broken 02/06 22:33 data irrtest : Set where Irr : .ℕ → irrtest 02/06 22:34 shouldn't allow extract : irrtest → ℕ; extract (Irr n) = n 02/06 22:34 how do you write neq-not-eq? 02/06 22:38 hmm, maybe I ended up with an irrelevant version 02/06 22:39 but, you are allowed to match irrelevent things with absurd patterns 02/06 22:39 hm 02/06 22:40 I see 02/06 22:40 this is frustrating, I don't see how to tell if a definition is relevant or not 02/06 22:40 http://hpaste.org/47371/irrelevance 02/06 22:41 It fails at the very last step 02/06 22:41 wait, 7 doesn't fail? 02/06 22:42 no 02/06 22:43 only 16/17 fails 02/06 22:43 it does fail on 7 02/06 22:44 in my agda 02/06 22:44 hmm, maybe mine is old 02/06 22:45 2.2.10 02/06 22:46 yeah, I built mine a few days ago 02/06 22:47 that line 7 should definitely not typecheck 02/06 22:47 I'll rebuild 02/06 22:50 hmm, seems to be up to date with respect to hackage 02/06 22:50 that one may just be broken 02/06 22:52 I'm sure you can derive a contradiction if 7 typechecks 02/06 22:52 well, that's what I tried to do at 16, but it didn't 02/06 22:52 It turns out that extract gives you a "_ : bool" 02/06 22:53 an ignored bool, which is condiered equivalent to any other ignored bool 02/06 22:53 so copumpkin 02/06 22:53 explain to me these irrelevant thingies 02/06 22:53 basically says they can't be computationally relevant 02/06 22:58 you can use them in other irrelevant contexts 02/06 22:58 but otherwise it'll prevent you from doing that 02/06 22:59 im not sure i follow but ok! 02/06 22:59 The irrelevance in Agda allows the type system to check that your don't actually look at certain arguments when producing results. 02/06 23:24 Or certain parts of their arguments. 02/06 23:24 And since your functions don't look at them, they can be erased. 02/06 23:25 During type checking, even. 02/06 23:25 --- Day changed Fri Jun 03 2011 so tired x.x 03/06 00:16 dolio! :D 03/06 00:17 also, copumpkin 03/06 00:17 i have a modified version of the mapR file 03/06 00:17 https://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda 03/06 00:18 i added a really dumb, simple induction as a starting point, and also clarified some of the mapR reasoning 03/06 00:19 also theres a bunch of notes that might be useful in coming up with the right combinators 03/06 00:19 Can you prove {A : Set} (f g : A → ⊥) → f ≡ g? 03/06 19:46 no 03/06 19:48 ok. It's easy enough to show pointwise 03/06 19:49 i wonder what could go wrong if all bottoms were definitionally equal 03/06 19:50 you mean all empty types? 03/06 19:51 s/bottoms/elements of \bot/ 03/06 19:51 bot-eq : (x y : ⊥) → x ≡ y; bot-eq () () 03/06 19:51 they already are. 03/06 19:51 that's propositionally 03/06 19:51 bot-eq _ _ = refl won't typecheck 03/06 19:51 while it would for s/\bot/\top/ 03/06 19:51 \bot isn't the only empty type though 03/06 19:52 trying to identify different empty types is hard 03/06 19:52 i'd be happy if it worked for datatypes with no constructors :) 03/06 19:52 what do you mean it works for top? 03/06 19:53 I don't see that either 03/06 19:53 Well you ask that for stuff that's isomorphic to \bot 03/06 19:53 top is defined as a record, so it eta expands into the same thing in both cases. 03/06 19:53 Ah 03/06 19:53 For little things like this, I usually just redefine \== and so on, rather than picking up the reloading cost of importing from the standard library 03/06 19:54 a single-constructor data type does not work like that 03/06 19:54 yeap 03/06 19:55 What about stuff like    isBot : (A : Set) -> (A -> \bot) \x (\bot -> A)      bot-eq : (x y : Set) -> {_ : isBot x \x isBot y} -> x \== y 03/06 19:55 that bot-eq doesn't have much to do with the one above, btw 03/06 19:56 Ah, oops, it has more to do with napping's stuff 03/06 19:57 Did you see my question yesterday about irrelevance? 03/06 19:57 http://hpaste.org/47371/irrelevance 03/06 19:57 anyhow that can't be proved, i think 03/06 19:57 It's a case of functional extensionality, I was wondering if the empty result type made it easier somehow 03/06 19:57 The "oops" in the paste fails to typecheck, but surprisingly the rest are fine 03/06 19:58 the fact that extract doesn't need to be marked somehow is what's surprising for me 03/06 19:59 Saizan: have i shown you my derivation of mapR? 03/06 19:59 Yes, pretty much 03/06 20:00 If it was .extract : irrtest -> Bool, or extract : irrtest -> .Bool I wouldn't be suprised 03/06 20:00 but as it is, there seems to be no way to require or even to check whether a function has become (partially?) irrelevant 03/06 20:00 extract doesn't typecheck with darcs agda, btw 03/06 20:01 So it's changed from 2.2.10 03/06 20:01 Saizan: https://github.com/psygnisfive/algebraic-syntax/blob/master/Map.agda 03/06 20:01 i'd like your opinion 03/06 20:01 some of it is leftovers from previous versions 03/06 20:03 the important bits are the derivation of empty-theorem and mapR-theorem 03/06 20:03 napping: extract doesn't generate complaints? 03/06 20:06 If it doesn't, then you need to report a bug. 03/06 20:08 augur: what kind of opinion? 03/06 20:12 Saizan: any! 03/06 20:12 especially if its the sort that might point in the direction of a cleaner way to do such derivation of definitions :p 03/06 20:12 well, when you know that the type you're looking for has to be equivalent to a function type the are fairly mechanical rules to deduce the equivalent "table" 03/06 20:19 oh? 03/06 20:19 which is the stuff MemoTrie is based on 03/06 20:19 what should i read 03/06 20:19 e.g. "Type Fusion" by Hinze 03/06 20:24 (which talks about isomorphic types anyhow) 03/06 20:24 dolio: Saizan says it does in the darcs version 03/06 20:24 I could mention it on the list, if you think it would help 03/06 20:25 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.3272 <- or this 03/06 20:25 Saizan: im not sure i understand 03/06 20:27 napping: Not if it's already fixed, probably. 03/06 20:35 napping: didn't I say it did in the darcs version too, yesterday? :P 03/06 20:36 I remember you saying you expected it to fail on "extract" 03/06 20:44 but not saying that it was actually fixed 03/06 20:44 http://snapplr.com/0h8t 03/06 20:44 I guess I didn't actually say it was fixed 03/06 20:44 just that it didn't typecheck on mine :) 03/06 20:44 I guess I didn't think very carefully what version you would have built a few days ago 03/06 20:46 Reading that right after I recompiled the broken 2.2.10 didn't help :) 03/06 20:47 by the way, http://hpaste.org/47411/not :P 03/06 20:47 I'm not sure what eelis is on in #coq 03/06 20:47 Yeah, it's of course an instance of extensionality 03/06 20:48 and pointwise equivalence is proven how he suggests, at least in Coq 03/06 20:48 yeah 03/06 20:48 Is code.haskell.org down? 03/06 20:49 not for me 03/06 20:49 it seems to be from here 03/06 20:49 community.haskell.org (178.63.91.44) ? 03/06 20:58 yep 03/06 21:00 Saizan: can you explain the connection? i dont really see it 03/06 22:17 i skimmed the papers you pointed me to and dont see any explanations there of how to use properties to derive definitions.. 03/06 22:18 augur: see Example 6.1 03/06 22:23 of Type Fusion 03/06 22:23 well, actually, the whole section 6 03/06 22:24 it starts by noting that (Nat -> A) ~~ Stream A, and then proceeds to generalize that for a fairly wide family of types 03/06 22:25 i see a bunch of stuff on tabulation, but i dont see how that connects up 03/06 22:25 so, as i said, when you want a type that's isomorphic to some function space, you can use that 03/06 22:26 augur: well, look further 03/06 22:26 or deeper 03/06 22:26 what 03/06 22:27 this does not make any sense 03/06 22:27 augur: sorry, i seem to always fail to communicate with you, and i don't want to try harder atm 03/06 22:27 i have no idea how functions-from-naturals-as-streams has anything to do with deriving the definition of a function from a property it must have.. 03/06 22:29 what if that property it must have happens to be "isomorphic to Nat -> A"? 03/06 22:30 as your Map-theorem example is "isormorphic to Fin i -> .."? 03/06 22:31 for those special cases you can use what i linked. 03/06 22:32 This stuff doesn't seem to be useful for "deriving the definition of a function from a property it must have" 03/06 22:32 What it does do, is let you show that the space of functions is isomorphic to a table form 03/06 22:32 It sounds like that might actually be what you are trying to prove 03/06 22:32 Saizan: its actually not about isomorphisms 03/06 22:33 <-> isnt an isomorphism, its merely simultaneous-inhabitance 03/06 22:33 yeah, you can derive that from an isomorphism 03/06 22:33 more generally, it can help to prove things about functions on finite domains, if it's easy to check concrete examples 03/06 22:34 sure, but isomorphism is stricter 03/06 22:34 even infinite domains 03/06 22:34 1 <-> N is easily satisfied 03/06 22:34 but theres no isomorphism 03/06 22:34 i know 03/06 22:34 i just really dont see how this is relevant. ill read the paper tho 03/06 22:35 You can't check properties on infinite domains by truth tables 03/06 22:35 but dont for a second thing ill feel like im getting anything out of it! 03/06 22:35 think** 03/06 22:35 napping: he wants some technique to derive a type T by knowing it is logically equivalent to some other one 03/06 22:37 napping: so, if that other one happens to be a function space the table is a candidate at least 03/06 22:38 Saizan: well thats not what _i_ want but maybe its what hinze wants? 03/06 22:40 augur: then sorry, i completely failed to get the point of your agda code 03/06 22:41 well 03/06 22:41 the .. point was that we're asserting the existence of a function of some type, and that it satisfies a certain property 03/06 22:41 the question is to use that property to discover a possible definition 03/06 22:41 in the mapR case, we're saying that a function with the properties of a map exists 03/06 22:42 ok, both your examples matched my description though 03/06 22:42 and then we're using that property to whittle away at what the proof to see what the definition of map is. 03/06 22:42 we know its type already, thats not at issue 03/06 22:42 what is at issue is its /value/ 03/06 22:43 it's value is a type though. 03/06 22:43 *its 03/06 22:43 only because its easier to prove stuff using types 03/06 22:43 its nicer to use propositions than truth values 03/06 22:44 mapR f xs ys == true <-> ... would work just as well 03/06 22:44 but would probably be nastier to give an inhabitant for 03/06 22:44 and mapR would ofcourse fail to be usable as a type-level predicate, too 03/06 22:45 anyhow, i don't mind if you don't read the paper :) 03/06 22:46 im going to read it 03/06 22:47 its just im not sure how the paper really relates properties to definitions 03/06 22:48 at least, it doesnt _seem_ to be about that sort of thing, and doesnt _seem_ to discuss such an issue 03/06 22:48 not in any way that i can see 03/06 22:48 but its not a long paper so 03/06 22:48 --- Day changed Sat Jun 04 2011 bweeeeeoo 04/06 03:23 what is the topology of \bn ? 04/06 18:06 copumpkin: give me ideas 04/06 20:10 nope 04/06 20:10 at my gf's house, doing stuff :P just wanted to check something on the computer 04/06 20:10 and now you're here to give me ideas! :| 04/06 20:11 nope 04/06 20:12 lame :| 04/06 20:12 oh man, only like 04/06 20:12 what 04/06 20:12 two months until hacphi 04/06 20:12 --- Day changed Sun Jun 05 2011 byorgey! 05/06 04:17 Why can't Agda infer that "[]" can be List A here? 05/06 21:11 data _⊆_ {A : Set} (a : List A) (b : List A) : Set where empty : [] ⊆ b 05/06 21:11 AgdaBasics.agda:697,3-17 05/06 21:11 [] != a of type List A 05/06 21:11 when checking the constructor empty in the declaration of _⊆_ 05/06 21:11 the problem is that "a" and "[]" aren't the same list 05/06 21:13 data _⊆_ {A : Set} : List A -> List A -> Set where empty : {b : _} -> [] ⊆ b -- this would work 05/06 21:15 Saizan: Same error 05/06 21:27 "  empty : {b : _} -> [] ⊆ b 05/06 21:27 have you changed the " : List A -> List A -> Set" part too? 05/06 21:27 Oh.  "Unsolved metas" 05/06 21:29 sshc: what is [] 05/06 21:30 data List (A : Set) : Set where []   : List A _::_ : A -> List A -> List A 05/06 21:31 aha ok 05/06 21:34 sorry i wasnt really paying attention :p 05/06 21:34 I think I'm going to give up and see how it is defined in the tutorial 05/06 21:45 sshc: what are you trying to define now 05/06 21:45 augur: ≤ 05/06 21:46 Er 05/06 21:46 Subset type 05/06 21:46 ah 05/06 21:46 mm 05/06 21:46 _⊆ 05/06 21:46 subset for .. sets? 05/06 21:46 Lists 05/06 21:46 so sublist 05/06 21:46 sublist is going to be tricky no doubt 05/06 21:46 because there are multiple ways for one list to be a sublist of another 05/06 21:46 but if what is intended is a contiguous sublist, thats easier 05/06 21:47 It's not what is intended, but that's probably good practice before I do the real one 05/06 21:47 * sshc tries 05/06 21:47 I'm not sure how to define "empty" even for that, though 05/06 21:50 data _scl_ {A : Set} (a : List A) (b : List A) : Set where empty : [] scl b 05/06 21:51 AgdaBasics.agda:705,5-21 05/06 21:51 [] != a of type List A 05/06 21:51 when checking the constructor empty in the declaration of _scl_ 05/06 21:51 What exactly does that error message mean? 05/06 21:54 you shouldnt put a and b as parameters to the datatype 05/06 21:56 data _scl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] scl b 05/06 21:57 --- Day changed Mon Jun 06 2011 is there a notion of equality that makes it possible to test the equality of objects by reference as well as structure 06/06 02:35 so that two infinite objects can be compared? 06/06 02:35 i mean, its hard to evaluate (haskell)  let ones = 1 : ones in ones == ones   without something like that 06/06 02:36 does anyone have good references for K rule? I am wondering what it is and why it leads to inconsistency with homotopy types. (btw, the Agda option seems not to guarantee that K rule is disabled :( ) 06/06 16:45 Oh, you have an example? 06/06 16:47 It's not a great reference, but there's file:///usr/local/share/doc/coq/html/stdlib/Coq.Logic.EqdepFacts.html 06/06 16:48 also http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/ 06/06 16:48 napping, I think you just linked to a file on your box :p 06/06 16:48 Ah, so I did 06/06 16:49 djahandarie: I can find it anyway :p thanks, google! 06/06 16:49 http://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html 06/06 16:49 The second link I posted seems more likely to be informative 06/06 16:50 Yeah, that's a good article 06/06 16:50 napping: thanks :) 06/06 16:52 I think K holds on any simply connected types 06/06 16:53 about my last question, is it guaranteed that the K rule is disabled in Agda by adding "--without-K" ? it says "disable the K rule (maybe)". hmm... "maybe"? 06/06 16:54 Ah, I thought you were claiming you had a proof of K. 06/06 16:54 No, nobody is entirely sure whether that makes it impossible to prove K 06/06 16:54 But probably. I think Conor McBride's thesis on eliminating dependent pattern matching would be the place to start 06/06 16:54 napping: so you're saying that, they adopt some other mechanism in hope to "prevent" K rules, right? 06/06 16:55 Just see if you can redo all the proofs for the subset of pattern matching allowed by --without-k, while only assuming J 06/06 16:55 ;) 06/06 16:55 napping: so the "maybe" means that K might be still provable. did I understand your saying correctly? 06/06 16:56 More like they ban the kinds of pattern matching which definitely require axiom K to translate into eliminators 06/06 16:56 So the rest should be justifiable only in terms of J, but nobody has proven it 06/06 16:56 "Might still be provable", yes 06/06 16:57 napping: I see. Thanks. :) 06/06 16:58 To be more specific, I don't think anyone has reason to believe that it is still provable, but no solid proof either way 06/06 16:58 Also, if I read that article right, K is actually valid on any of the types you can define in Agda today 06/06 16:58 augur: equality by reference is meaningless in agda, and propositional equality is the minimal/most refined equivalence relation that can be reified as a type/proposition 06/06 18:13 augur: (proof: you can write subst and use it to inject proofs of propositional equality into any equivalence relation) 06/06 18:15 or actually into any reflexive relation period 06/06 18:15 O_O 06/06 18:20 i didnt mean in agda 06/06 18:22 oh 06/06 18:23 what did you mean, then? 06/06 18:23 just more generallt 06/06 18:23 in order to have equality of reference, you need to have a domain where equality of reference makes sense 06/06 18:24 you don't need equality of reference to prove things about equality of codata, though 06/06 18:24 that's what bisimulation is for 06/06 18:25 hmm 06/06 18:25 xplat: have you see my mapR derivation code 06/06 18:26 augur: i have seen, but not looked.  or is it the other way around? 06/06 18:27 :p 06/06 18:27 Usually the other way around 06/06 18:45 well xplat, i want as many opinions as possible! 06/06 18:49 copumpkin: BTW: I got Agda installed here. 06/06 20:31 The font situation is still pretty abysmal, though. 06/06 20:31 The fill-in-the-gap fonts listed on the wiki are pretty hideous. 06/06 20:33 the fonts i have are ugly as sin, too 06/06 20:33 and i don't mean the fun kind of sin 06/06 20:34 Ubuntu managed to cobble together a pretty decent collection of glyphs. 06/06 20:34 I can't say the same for windows. 06/06 20:34 hm, i'm on ubuntu 06/06 20:34 but i seem to get a bunch of symbols and things in handwriting fonts 06/06 20:35 \==, greek letters ... 06/06 20:35 Well, technically, I'm talking about kubuntu, but that probably doesn't matter much. 06/06 20:35 i have no idea why, the console font doesn't get this fugly 06/06 20:35 the glyph substitutions i see in a terminal are pretty sane 06/06 20:35 dolio: oh, on your work computer? 06/06 20:36 ah, looks like it :) 06/06 20:36 Yeah. 06/06 20:36 It wasn't actually as bad as I was expecting. 06/06 20:36 do you have the same emacs server issue on windows? 06/06 20:36 No. 06/06 20:37 I couldn't figure out how to make cabal-install or darcs work, though. 06/06 20:37 ah 06/06 20:37 So I had to check it out on your laptop and e-mail myself a copy. 06/06 20:37 i'm disappointed that no carrier pigeons feature in this story 06/06 20:38 Gmail may use pigeons. You never know. 06/06 20:38 dolio: I'm going to send you some stuff on a usb key via carrier pigeon 06/06 20:38 it might take a while to get there 06/06 20:38 not sure how fast carrier pigeons are 06/06 20:39 If they use pigeons for ranking pages.... 06/06 20:39 oh yeah 06/06 20:39 dolio: it would explain a lot, wouldn't it? 06/06 20:39 (i'm a little bitter at google over a search i did this morning, although they usually still rank decently) 06/06 20:40 Oh, also, was the place you went Pho Basil? 06/06 20:41 (it really gets old fast when you're clicking through shopping results trying to find maintenance information on your dead power brick while your laptop is running off a mostly-depleted battery ... 06/06 20:42 ... and most of the results that aren't shopping are keyword-faking wannabe guru sites) 06/06 20:43 btw the most common conclusion was that the brick isn't user-servicable and they cold-weld it shut, so i ended up buying a new one :( 06/06 20:44 dolio: yep! 06/06 20:47 that sounds delicious 06/06 20:48 copumpkin: All right. I tracked down the right one, then. 06/06 20:49 There are a surprising number of places that serve pho in the area. 06/06 20:50 Compared to Cincinnati, at least. 06/06 20:50 indeed i was in boston myself last time i had pho 06/06 20:50 although that place has closed 06/06 20:51 oh no! 06/06 20:52 it was that 'pan-asian noodle' place right smack in the middle of everything, so probably not the most authentic pho in boston, but it was a cool restaurant concept 06/06 20:53 if it was asian and it was noodly and it wasn't an obscure specialty in its own homeland, they would try to approximate it for you :-7 06/06 20:55 I want biang noodles 06/06 20:56 they have the distinction of requiring the most strokes in the usual character for them 06/06 20:56 http://en.wikipedia.org/wiki/File:Bi%C3%A1ng_(regular_script).svg 06/06 20:56 Wow. That's like a character that contains 6 other characters. 06/06 20:58 oh yes 06/06 20:58 if you want truly crazy 06/06 20:58 japan invented a rather sketchy 84-stroke one 06/06 20:59 it's rather uninteresting though 06/06 20:59 http://en.wikipedia.org/wiki/File:Taito_2_l.png 06/06 20:59 See, now that just looks lazy. 06/06 21:00 yeah 06/06 21:00 technically i think that countains at least 10 other characters 06/06 21:01 biang, that is 06/06 21:01 yeah, it's quite a few 06/06 21:01 I'm sure it'd be pretty easy to come up with a mnemonic for all of them 06/06 21:01 all the constituents are pretty common and easy 06/06 21:01 horse, moon, sword, heart, word, at least 06/06 21:02 road, heart, bird, moon, say, and 3 more uniques, if the meanings haven't drifted too much since kanji split off 06/06 21:02 oh, was it horse?  i always mix up horse and bird, they look similar to me 06/06 21:03 馬 06/06 21:03 that's horse 06/06 21:03 but yeah 06/06 21:03 it also has a ~six stuck on the top, I guess 06/06 21:04 although it isn't quite six 06/06 21:04 yeah, what is that anyway? 06/06 21:04 which one is sword? 06/06 21:04 (taito certainly seems a lot more compressible) 06/06 21:06 鳥馬－ｂｉｒｄ＆ｈｏｒｓｅ 06/06 21:07 well, it isn't so much sword 06/06 21:08 as a very "swordy" component that shows up in many choppy characters 06/06 21:08 the two vertical bars 06/06 21:08 剣 06/06 21:09 the thing on the right there 06/06 21:09 ah 06/06 21:14 so two leaders next to a horse, below a word with two threads, flanked on the left by the moon and the right by a choppy bladey thing, all of which is standing on a heart with a hole above it, and the whole thing happens in the road 06/06 21:17 i think my mnemonic generator overheated 06/06 21:18 That description definitely makes me think of noodles. 06/06 21:19 This noodle was a poor-man's meal in the countryside, but has recently become popular in trendy restaurants due to its weird character name.^[citation needed] 06/06 21:20 copumpkin 06/06 21:36 your intro to agda video was marred by errors, from what i could tell. i really wanted to watch it, really really, but i couldnt 06/06 21:36 :( 06/06 21:36 but on the bright side, you're totally adorable 06/06 21:37 augur: errors? 06/06 21:43 yeah 06/06 21:43 thanks :P 06/06 21:43 but what kind of errors? 06/06 21:43 i'd have to go back and watch, but they were sloppy mistakes 06/06 21:43 :o 06/06 21:44 like your definition of the evenness function 06/06 21:44 what about it? 06/06 21:44 the slides are up 06/06 21:44 you had one case defined as even (suc (suc n)) = even (suc (suc n)) and said it should terminate but agda cant tell this is true 06/06 21:44 link to slides! 06/06 21:44 or no sorry 06/06 21:45 it was halve not even 06/06 21:45 I didn't say it should terminate 06/06 21:45 you certainly did sir 06/06 21:45 I'm not sure why I would've said that 06/06 21:45 neither am i! 06/06 21:45 the whole point of that slide was that the termination checker can help you catch bugs 06/06 21:45 ill find you the video with a timestamp tho 06/06 21:45 I'll survive 06/06 21:45 http://dl.dropbox.com/u/361503/Agda%20and%20dependent%20types.pdf 06/06 21:46 you mean you won't terminate? 06/06 21:46 not for a while, I hope :) 06/06 21:46 page 5 of your slides in evince is the slowest thing in the entire universe 06/06 21:49 not counting web browsers and typechecking my agda modules 06/06 21:49 page 6 too, i bet it's those red circles 06/06 21:49 oh, no, copumpkin, i totally maligned you 06/06 21:50 im sorry 06/06 21:50 i misheard your doesnt as does. 06/06 21:50 I mean, I was pretty nervous, so I probably did make other mistakes :P 06/06 21:50 thank god. copumpking [ sexiness ]+= 1 06/06 21:50 lol 06/06 21:51 i'm glad someone finally recognizes that an individual's knowledge of computer programs is determined by eir sexiness 06/06 21:54 xplat: I wonder why they're so slow 06/06 21:54 they're find 06/06 21:54 they're fine here, is what I meant 06/06 21:54 hm, this page doesn't have circles and it's still slow 06/06 21:54 :o 06/06 21:55 xplat: other way around 06/06 21:55 also, spivak pronouns 06/06 21:55 please tell me you're an orion's arm fan 06/06 21:55 your "-- no sections" comment doesn't have a :( .  i am disappoint 06/06 21:55 augur: we've had this discussion before 06/06 21:56 spivak pronouns? 06/06 21:56 xplat: have we 06/06 21:56 lets have it again, it mustve been good 06/06 21:56 xplat: oh yeah, I am disappoint too, but I guess I forgot to put it on 06/06 21:56 copumpkin: http://en.wikipedia.org/wiki/Spivak_pronoun 06/06 21:56 'e, em, eir, eirs, eirself' 06/06 21:56 oh okay 06/06 21:56 i like old school spival 06/06 21:57 I thought it was some reference to the speaker who came after me :) 06/06 21:57 tho really all spivaks are nifty 06/06 21:57 'eir' is a cool looking possessive pronoun :D 06/06 21:57 Spivak wrote calculus on manifolds! :o 06/06 21:58 the very same spivak! 06/06 21:58 i am more of an old-schooler myself 06/06 21:59 xplat: be an orions armer 06/06 21:59 :D 06/06 21:59 i have enough arms already 06/06 22:01 well, not true really, i lack a gripping hand 06/06 22:01 (or maybe i have two) 06/06 22:02 orionsarm.com 06/06 22:02 what, there's an rpg?! 06/06 22:03 post-singularity roleplaying sounds kind of hard 06/06 22:03 well, i imagine someones got an RPG going 06/06 22:05 but mostly its worldbuilding 06/06 22:05 is it just or me or does agda-mode have no syntax highlighting? 06/06 22:42 load the file 06/06 22:42 ah, i'll try that once agda has finished recompiling... 06/06 22:44 The highlighting is more intelligent, but it calls out to the Agda implementation, so you don't get any color until you've type checked things, generally. 06/06 22:53 And once you've checked, the color will bleed into what you type until you next check. 06/06 22:53 That's a bit annoying. 06/06 23:12 The bleeding, or the general situation? 06/06 23:13 The need to typecheck. 06/06 23:13 It's conceivable you could do better. 06/06 23:15 I also wonder if the scoping restrictions could be relaxed, so you could have some f defined after it's used like in Haskell. 06/06 23:15 That I don't know. 06/06 23:16 It can probably be made more lax. 06/06 23:16 'mutual' seems to do something like that. 06/06 23:16 But even in mutual blocks, types are checked in order of occurrence. 06/06 23:17 So later definitions are not available in the types of earlier ones. 06/06 23:17 Oh. 06/06 23:17 As I recall. 06/06 23:18 I suppose it's got something to do with parsing rather than typechecking, no? 06/06 23:18 I don't think it has to do with parsing. 06/06 23:18 Of course, in induction-recursion, you use later definitions in the types of constructors earlier. 06/06 23:19 But that's a slightly different case. 06/06 23:19 foo : ... bar ... ; foo = ... ; bar : ... ; bar = ...  won't work, as I recall. 06/06 23:19 Even in a mutual block. 06/06 23:19 --- Day changed Tue Jun 07 2011 what is the response to Quine's critique of higher order logic as being not a logic due to the lack of a proof theory, in light of CoC etc.? 07/06 05:06 and what refinements of the notion of impredicativity exist that admit of the good cases (ones = 1 : ones) but not the bad ones? 07/06 05:23 ones = 1 : ones doesn't have anything to do with impredicativity. 07/06 05:33 dolio: sure it does: ones is defined in terms of itself. thats an impredicative definition 07/06 05:54 Then recursive definitions are also "impredicative." 07/06 06:07 this is i think true! 07/06 06:07 well, with the exception of the fact that that sort of self reference can be factored out by the relevant combinators 07/06 06:08 The combinators are all that exist. 07/06 06:08 whereas ones recursion afaik cant 07/06 06:08 No. 07/06 06:08 ones is defined by corecursion. 07/06 06:08 right 07/06 06:08 So what's the problem? 07/06 06:09 ones is still impredicative! 07/06 06:09 Nope. 07/06 06:10 no? 07/06 06:10 but it IS self referential 07/06 06:13 The self-referential definition is sugar for a primitive corecursion combinator. 07/06 06:15 ahh 07/06 06:16 whats a corecursion combinator :o 07/06 06:16 It's like a recursion combinator, only for corecursion. 07/06 06:17 :P 07/06 06:19 whats an example of one, i should say 07/06 06:19 unfoldr 07/06 06:20 hmmmm 07/06 06:31 unfoldr is basically a paradigm example like foldr is for recursion 07/06 06:32 not the most powerful scheme available, but the most basic and structural 07/06 06:34 hmm 07/06 06:36 ok 07/06 06:36 ill be off. see you 07/06 06:36 cofix :P 07/06 06:58 unfoldr : forall {X Y} -> (Y -> Maybe (X x Y)) -> Y -> List X, where (X x Y) is the functor for List .. 07/06 07:09 hmm 07/06 07:09 well, Maybe (X x Y) rather 07/06 07:10 hmm.. F X Y = 1 + X x Y; unfoldr : forall {X Y} -> (Y -> F X Y) -> Y -> List X 07/06 07:10 but List X = mu (F X) 07/06 07:11 so unfoldr : forall {X Y} -> (Y -> F X Y) -> Y -> mu (F X) 07/06 07:11 more generally, i suppose, unfoldr : forall {Y} -> (Y -> F Y) -> Y -> mu F ?? 07/06 07:12 or less generally, i guess, but 07/06 07:12 ah right, this is looking familiar actually 07/06 07:13 Y -> F Y, thats a coalgebra 07/06 07:13 i suppose it should be comu not mu 07/06 07:14 can i have the case split put arguments in the positions indicated by the underscores instead of prefix style? 07/06 12:15 augur: comu is called nu 07/06 12:32 mixis: do you mean the automatic case split? 07/06 12:35 xplat: C-c C-c 07/06 12:41 also, a way to generate the first line of the body with a goal on the rhs after having typed the signature would be neat 07/06 12:49 if you start with mixfix i think it will at least sometimes stay that way, but if it feels it has to insert an implicit argument it definitely won't 07/06 12:49 i had a 3 argument function with 2 underscores in the name and that got changed 07/06 12:51 it definitely isn't as smart as it could be 07/06 12:52 well, then i'll be looking at Agda.Interactoin for a while 07/06 12:54 i already actually have a whole wishlist for agda-mode (and agda in general) that i haven't got around to working on any of yet 07/06 12:55 https://gist.github.com/979524 07/06 12:58 they're really more like 'it seems like this should be doable' than having an actual plan :-7 07/06 12:59 undo with reload: does that mean undo with automatic reload? 07/06 13:13 eh, undo withOUT reload in your list 07/06 13:15 mixis: undo that undoes the state changes (highlighting, filled goals, etc).  effectively the same as automatic reload, but hopefully it could be done faster if you don't go too far into the undo stack 07/06 14:32 just wanted to check on your experiences, I have an spi eeprom device that I am trying to program from my pic. I notice that the bytes written are being read back as 0xff, all the time. Anything simple that I could be missing? 07/06 15:45 oh, sorry. should not have posted this here 07/06 15:56 I meant to post it somewhere else.. 07/06 15:56 This is where I go for all my eeprom advice. 07/06 15:56 really?  i just ask my bartender 07/06 16:00 Your garbage man might be better for that. 07/06 16:01 roly poli dolio 07/06 16:38 hmm 07/06 18:55 i wonder if i could phrase these propositional types as relations... 07/06 18:56 and then use AoP style manipulations 07/06 18:56 data Diag (X : Set) : X -> X -> Set : Set n where diag : (x : X) -> IsA X x x 07/06 19:00 or something like that 07/06 19:00 er, that should be Diag X x x obvviously x3 07/06 19:00 how is that different from refl and _\==_ ? 07/06 19:01 with less implicitness 07/06 19:02 copumpkin: well, you're probably right! 07/06 19:05 except that its supposed to be the relational type X 07/06 19:05 the content is the same but the intention is different 07/06 19:06 anyway, thats just me dicking around trying to figure out the shape of things, nothing important 07/06 19:06 brb! 07/06 19:06 hmm 07/06 19:37 can AoP relations be represented as actual relations 07/06 19:41 eg X <- Y = X -> Y -> Set 07/06 19:41 ? 07/06 19:41 pr X x Y -> Set, whichever is preferable 07/06 19:42 Nice, JS backend is UP! 07/06 20:27 Time to use Agda for my day job 07/06 20:27 copumpkin: i've got a working example of the yellow menace that is one file, but it's 190 lines (wc -l) 07/06 20:28 oh wow 07/06 20:29 may I see? 07/06 20:29 http://hpaste.org/47565/inference_fail_v1 07/06 20:33 it should be possible to cut it down further 07/06 20:35 I see 07/06 20:40 it's still pretty non-minimal 07/06 20:44 yeah 07/06 20:44 i basically found the least annoying-looking yellow line from the pentagon proof and pulled all its dependencies into the file 07/06 20:45 they've been simplified some, but not much 07/06 20:45 I'm guessing it must be something about being hidden in that module 07/06 20:46 yeah 07/06 20:46 i got rid of the Category type and record by just breaking out the fields that are used as postulates 07/06 20:46 a lot of stuff is brought in just for Product.⟨⟩∘ so if i postulate that i can probably kill like a third of the file 07/06 20:50 well maybe a quarter 07/06 20:50 new version has a 'good' version of badproof for comparison and the end of the old file is now at line 124 07/06 21:12 cool 07/06 21:14 ! 07/06 21:26 i've found a paper thats /even closer/ to what im looking for :O 07/06 21:26 copumpkin: Pointwise Relational Programming - de Moor and Gibbons 07/06 21:31 :X 07/06 21:31 hmm no it doesnt look like itll do what im looking for after all :( 07/06 21:33 oh well 07/06 21:34 okay, now down to 59 lines 07/06 21:34 copumpkin: http://hpaste.org/47571/inference_fail_v2 07/06 21:41 it turned out to still fail without using actual equational reasoning 07/06 21:42 oh cool 07/06 21:42 so i could get rid of SetoidReasoning and Setoid and even IsEquivalence and the example got *much* smaller 07/06 21:42 copumpkin: any suggestions before i post it to the mailing list? 07/06 21:46 hem 07/06 21:50 if i take the (useless) implicit parameters off HomReasoningP then it works 07/06 21:50 but they weren't useless originally! 07/06 21:50 FFFFFFFFFFUUUUUUUUUUU--!! 07/06 21:52 I'm wondering how I could match with a finite list on the type-level (in a data constructor, in this case) 07/06 21:52 data _scl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] scl b notLarger : … scl [] 07/06 21:53 why would there be any constructors (other than empty) for ... scl []? 07/06 21:54 also, it's easier to do subsequence than sub(consecutive)list 07/06 21:57 for subsequence you could call your constructors 'skip', 'advance', and 'done' 07/06 21:58 those names should help you figure out the types 07/06 21:58 if you want to make a constructor for the case where the first argument of scl is a cons you do it like constr : (x : A) (xs : List A) -> ... -> (x :: xs) scl ..., if that was the question 07/06 21:59 (but don't feel slow if you need more hints too) 07/06 22:00 < xplat> also, it's easier to do subsequence than sub(consecutive)list — What's the difference betwen the two? 07/06 22:01 sshc: 1,3,5 is a subsequence of 1,2,3,4,5 but not a sublist of it 07/06 22:02 man, i wish i committed more versions of this file so i could bisect and figure out where i went wrong condensing this 07/06 22:07 is unification required for type inference even when the types of all terms can be inferred directly (e.g. using Church-style function abstraction and/or inj0 and inj1 annoated with the disjunction type)? 07/06 22:13 hm, maybe the original problem is that the thing was being autogeneralized since the module took implicit parameters (instead of taking a record that took implicit parameters) 07/06 22:15 guerrill1: if your language provides enough type information or a simple enough type system that you don't have to do unification or constraint solving when inferring types, you are supposed to call it 'type propagation' instead 07/06 22:18 in "bidirectional type checking" they still call it inference though 07/06 22:19 (the part where you extract the type from the term) 07/06 22:19 fstElem   : {a : A} -> {as : List A} -> {b : A} -> {b : List A} -> {a \== b} -> {as scl bs} -> (a :: as) scl (b :: bs) 07/06 22:23 {a \== b} cannot appear by itself. It needs to be the argument to a 07/06 22:23 function expecting an implicit argument. 07/06 22:23 when scope checking {a \== b} 07/06 22:23 (These are subsequences, actually) 07/06 22:23 sshc: implicit arguments must have names 07/06 22:24 anyway, congrats, you now have an _isPrefixOf_ type named _scl_ :) 07/06 22:25 btw, you could do without a \== b by using just one variable 07/06 22:28 oops, sorry.. "< guerrill1> Saizan: i think that is what i'm doing. given a term and a type, i infer the type of the term and compare it to the given type."  "< guerrill1> by compare, i mean using an equivalence relation that i'm still not done writing..." 07/06 22:28 fstElem   : {a : A} -> {as : List A} -> {bs : List A} -> {_ : as scl bs} -> (a :: as) scl (a :: bs) 07/06 22:28 Oh.  Interesting :) 07/06 22:29 which one of those is easier kind of depends on what you're going to do with it 07/06 22:30 your original version generalizes better to different equivalence relations 07/06 22:30 bidirectional typechecking is specifically about splitting your terms' syntax into a part where you can deduce the type from and one where you've to push the type into to make sense of what you have, these two parts usually end up being mutually recursive 07/06 22:31 Saizan: ok thanks, reading up on it now... 07/06 22:33 Saizan: so, given ctx, M, τ, you can't just do (τ ≡ inferType ctx M) to verify that M : τ, thus moving most of the work into the theory and implentation of ≡? 07/06 22:34 guerrill1: you can if your language is simple and/or annotated enough, otherwise it's pretty useful to make use of that τ during "inferType" (which wouldn't be named so), instead 07/06 22:36 it would seem that my method destroy sthe locality and clarity of where a type error occurs, but that could be moved into ≡ ,i think... 07/06 22:37 ok, i think my language is annotated enough. i designed it this way, since i wanted type checking to be as simple and clear as possible; plus, the core code is a translation from a higher-level language anyway... 07/06 22:39 i just keep seeing tons of references to unification and its making me feel like i was missing something 07/06 22:39 ≡ doesn't seem like it'd have any hope to give a sensible type error, since it doesn't look at the term at all 07/06 22:42 and making τ available to inferType doesn't mean you'd use unification 07/06 22:42 indeed, that is true 07/06 22:43 at least you could say what doesnt match up to what when retuning on error from ≡ 07/06 22:43 anyhow the most common use of unification is to fill in information that the user left implicit, but if your input is machine generated this is not relevant 07/06 22:43 ok cool 07/06 22:43 though e.g. typecheking even a fully annotated Agda program requires unification to handle pattern matching 07/06 22:44 ok, i don't have that issue, i went a different route regarding pattern matching 07/06 22:45 so unification is for a) filling in implicit/missing type information b) better error reporting and c) dependently type pattern matching (ML-TT or COC) 07/06 22:46 (regarding type checking only of course, obviously useful for resolution and other areas) 07/06 22:46 the b) was unrelated to unification 07/06 22:47 ok 07/06 22:47 Saizan: thanks. i have a bit more confidence that what i'm doing makes sense now. 07/06 23:05 xplat: you too 07/06 23:05 hmm.. 07/06 23:10 interesting 07/06 23:11 (x : X) -> (g x) . r . (h x)   isnt a relation but theres a way to make it one 07/06 23:13 \x -> (g x) . r . (h x)    rather 07/06 23:13 \x y -> (g x) . r . (h y)   plus some identity constraint on x and y 07/06 23:14 well, i suppose what i intend is not g x but x g 07/06 23:15 \x y -> (x g) . r . (h y)  == \x y -> x (g . y . h) y 07/06 23:16 so, to get the identity constraint 07/06 23:16 \x y -> x < id , g . r . h > y 07/06 23:16 ~ \x y -> x id y & x (g . r . h) y 07/06 23:18 thats interesting 07/06 23:18 xplat: sorry, kind of busy. Don't wait for me but I'll take a look at it later 07/06 23:26 hmm hmm 07/06 23:44 ok im off 07/06 23:44 --- Day changed Wed Jun 08 2011 is there a reverse agdamode?? 08/06 01:01 er well 08/06 01:01 a reverse completions 08/06 01:01 is there a way to simultaneously have a variable and know its value so that you retain the type, when the type is polymorphic? 08/06 03:06 sort of like @'s in haskell? 08/06 03:08 f xs@(x : xs') = ... xs ...  ? 08/06 03:08 i mean, obviously you can use x : xs' in this case 08/06 03:08 but say .. f xs@[] = ... [] ... 08/06 03:08 there you cant just use [] right 08/06 03:08 because it lacks the type info, but you could use xs right 08/06 03:09 hmm no nevermind, its not necessary 08/06 03:11 Hm, it's probably not possible to represent a higher coinductive type in Agda right? Probably could with something OTT-based like Epigram 2 08/06 03:11 * djahandarie summons dolio for commentary 08/06 03:16 higher dimensional? 08/06 03:22 What's a higher coinductive type? 08/06 03:24 Like a higher inductive type.     data circle : Set where base : circle, loop : paths base base    or whatever. I'm not sure of an actual example of a higher coinductive type though. I don't see why they wouldn't conceptually exist in the HoTT framework though. 08/06 03:27 [2,2,2] isn't considered a sublist of [2], right? 08/06 03:28 Agda doesn't even really have coinductive types. 08/06 03:28 As the equality is too intensional. 08/06 03:29 Right, weak coinducutive types or something like that? I forget the name 08/06 03:29 I don't think it's so obvious what the dual of the higher inductive types would be, either. 08/06 03:36 Higher inductive types are about adding identities between constructors and identities on the relevant type.... 08/06 03:37 But there are no constructors for coinductive types. 08/06 03:37 djahandarie: where'd you get that example? what is "paths" in it? 08/06 03:37 Hmm 08/06 03:38 paths is the identity type. 08/06 03:38 So, higher coinductive types are defined by deconstructors plus... additional elements of the identity type? 08/06 03:39 guerrill4,   data paths {A : Set} (x : A) : A -> Set where refl : paths x x    -- or something liek that 08/06 03:39 I've only see the coq definition of this stuff, kind of just hoping these are the correct Agda definitions :p 08/06 03:39 Yeah, those are correct. 08/06 03:40 I seem to recall that the homotopy blog suggested that you can actually encode higher inductive types by their eliminator, as usual. 08/06 03:43 If you don't care about the strong elimination principle, probably. 08/06 03:43 Which would suggest it might be good to think about hat a higher coinductive introduction would be. 08/06 03:44 What, even. Not hat. 08/06 03:44 data _sl_ {A : Set} : List A -> List A -> Set where empty : {b : List A} -> [] sl b _is-a-sublist-of_ : {a : A} -> {as : List A} -> {b : A} -> {bs : List A} -> (f : (A -> A -> Bool)) -> {_ : elemBy f a (b :: bs) \== true} -> {_ : as sl bs} -> (a :: as) sl (b :: bs) 08/06 03:45 What's wrong with the type of "example" here? 08/06 03:45 example : (List Nat) sl (List Nat) 08/06 03:45 example = (zero :: []) is-a-sublist-of (zero :: zero :: []) 08/06 03:45 Set !=< List _948 of type Set₁ 08/06 03:46 when checking that the expression List Nat has type List _948 08/06 03:46 djahandarie: ok. 08/06 03:55 sshc: I guess you can say "[] sl []", not "(List Nat) sl (List Nat)" 08/06 04:12 Favonia: Huh? 08/06 04:12 "example : [] sl []" 08/06 04:12 the constructor _::_ does not construct an element of Bool 08/06 04:13 when checking that the expression zero :: [] has type 08/06 04:13 They're not empty lists, also 08/06 04:14 hmm what is f? 08/06 04:15 i am confused because you have only one explicit argument in the signature of _is-a-sublist-of_ 08/06 04:16 for set1, the problem is that "List Nat" is of type "Set", and a particular nat list is of type "List Nat" 08/06 04:18 Oh 08/06 04:21 elemBy : {A : Set} -> (A -> A -> Bool) -> A -> List A -> Bool 08/06 04:21 elemBy _    _ [] = false 08/06 04:21 elemBy _==_ a (x :: xs) with a == x 08/06 04:21 ... | true  = true 08/06 04:21 ... | false = elemBy _==_ a xs 08/06 04:21 Agda is predicative by default and Set1 is the next universe with higher level. If sl is really well-typed in "(List Nat) sl (List Nat)" then sl has type "Set -> Set -> X", where X is at least Set1. 08/06 04:23 sshc: the problem is that, f is an explicit argument in _is-a-sublist-of_, but in the proof of "example" "f" is not offered. 08/06 04:24 I think the signature/type of _is-a-sublist-of_ is probabily not what you want. also I guess Agda is not smart enough to automatically do the induction (like {_ : as sl bs}) for you. 08/06 04:32 Oh! 08/06 04:33 Yes, the definition of "example" clearly doesn't match with the type of is-a-sublist-of (which only has one explicit argument) 08/06 04:34 example : (zero :: []) sl (zero :: zero :: []) 08/06 04:35 example = sublist _nat==_ 08/06 04:35 Unsolved metas at the following locations: AgdaBasics.agda:738,11-26 08/06 04:35 seems that Agda is unable to do the whole induction for you :O 08/06 04:36 sshc: sorry that I can't run agda now. personally I would suggest something like _≤_ in the stdlib: data _≤_ : Rel ℕ zero where z≤n : ∀ {n} → zero  ≤ n  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n 08/06 04:40 example : (zero :: []) sl (zero :: zero :: []) 08/06 04:41 example = sublist {a = zero} {as = []} {b = zero} {bs = zero :: []} _nat==_ 08/06 04:41 sshc: you can see that the whole data structure is actually induction steps. also all the important arguments are explicit 08/06 04:41 ^ That's still not explicit enough, apparently 08/06 04:42 yay, now a fresh agda rechecks the pentagon law for cartesian products in 681m peak 08/06 15:01 :o 08/06 15:01 removing unnecessary imports turned out helpful 08/06 15:02 So hexagon laws and such for braided categories are probably possible? 08/06 15:04 Maybe I should try it out 08/06 15:05 yeah, they probably are possible 08/06 15:05 with a little work 08/06 15:05 copumpkin: i fixed the problems with equational flair, it turned out the functions were being automatically generalized with extra unused implicits and that was the source of the problems 08/06 15:12 ended up having nothing to do with abstraction or scope at all 08/06 15:13 oh good 08/06 15:14 is it a bug then? 08/06 15:15 also it turns out you could probably replace Category.Category.Equiv with ‘module Equiv {A B : Obj} where { open IsEquivalence (equiv {A} {B}) public } 08/06 15:16 it was my bug, assuming modules with their own trailing implicit arguments would freeze like modules whose explicit arguments have implicit arguments do 08/06 15:17 Do the standard libraries contain the proof that ℤ forms a ring? 08/06 16:26 I don't see it. Integers look under-developed. 08/06 16:33 no number theorists using agda? :\ 08/06 16:36 There's a bunch of stuff about the naturals. 08/06 16:36 Who cares about those negative numbers. They're pretty much imaginary. :) 08/06 16:36 copumpkin: Everything.agda won't build for me because it refers to a nonexistent Category.Presheaves 08/06 16:43 whoops 08/06 16:43 must've forgotten to add that 08/06 16:43 There is a Category.Presheaf 08/06 16:44 Everything refers to both 08/06 16:44 so unification is also what makes agda's implicit arguments work? 08/06 16:46 xplat: just remove the import... I never finished that module anyway 08/06 16:47 i just pushed anyhow, it built most of the modules fine and i was pretty sure i rebuilt everything i touched 08/06 16:49 and the number of modules that did rebuild makes me pretty sure i didn't break any dependent modules with any of the changes 08/06 16:50 once everything is merged i should be able to start porting to the stdlib 08/06 16:51 Your porting it to the stdlib? 08/06 16:51 You're* 08/06 16:51 yes, that is the plan. 08/06 16:52 i'm thinking everything should just go under a single root directory, my favorite at the moment is CTL, followed by CT and Category.Theory 08/06 16:52 er, CT, Categories, and Category.Theory 08/06 16:53 the stdlib's Category should really be renamed to something like Control or Notion or Idiom, but there's no use waiting on that 08/06 16:54 yeah 08/06 16:54 I wouldn't mind any of those, but Categories seems nicest 08/06 16:54 it'd also stop us from having to open Category.Category all the time 08/06 16:54 which was annoying as hell 08/06 16:54 dpiponi: there are binary naturals mod (2^n) (i.e., machine words) in a module I made with someone 08/06 16:55 they have lots of algebraic structures on them :P 08/06 16:55 as in all the proofs 08/06 16:55 i guess Categories does have that advantage, since Category.agda could become Categories.agda instead of /Category.agda like in the other proposals 08/06 16:56 copumpkin: The standard libraries define Z and rings so I thought they'd already have an IsRing record for Z. 08/06 16:59 probably different people added those 08/06 16:59 although you would think whoever added rings would pay attention to Z anyway since it's the initial ring 08/06 17:00 I thought I'd reproduce the first induction proof I learnt at school: http://en.wikipedia.org/wiki/Mathematical_induction#Example 08/06 17:00 oh I remember doing that 08/06 17:01 it was a lot harder to do in agda than it was in high school :P 08/06 17:01 No doubt about that! 08/06 17:01 oh wait, it wasn't that one 08/06 17:01 it was the sum of odds is a square 08/06 17:01 seems pretty similar though 08/06 17:01 Should be about the same level of difficulty anyway. 08/06 17:02 Can't you do that with the natural numbers? 08/06 17:02 xplat: nah, I think it's all NAD 08/06 17:02 In fact, that's what that proof is for. 08/06 17:02 dolio: Maybe, but there is a substraction. 08/06 17:02 yeah, I did mine over the naturals 08/06 17:02 the subtraction is trivial there, it can just be rephrased as addition 08/06 17:03 xplat: Yes, but I don't want to do that, especially because I might generalise. 08/06 17:04 also, induction doesn't work on Z 08/06 17:04 at least not plain induction 08/06 17:04 can't you have two inductive cases? 08/06 17:04 xplat: I was playing with summing functions N → Z so induction is fine 08/06 17:04 And I was hoping to eventually get into the RingSolver thingy to make things easier for more complex cases. 08/06 17:05 you can do bidirectional induction with a single base case, or bounded induction 08/06 17:05 but in agda you must first prove those work :) 08/06 17:06 * copumpkin pulls out the postulate block 08/06 17:06 :Þ 08/06 17:07 xplat: Now that's a character I don't use enough in my Agda. I should use ð too. 08/06 17:08 ðe hell you say!  :) 08/06 17:09 use Ϝ 08/06 17:15 or ϝ 08/06 17:16 ϟ or ϡ 08/06 17:17 I thought it'd be fun to use "invisible times" but no application seems to handle it correctly: http://www.fileformat.info/info/unicode/char/2062/index.htm 08/06 17:18 oh nice 08/06 17:20 Is bidirectional induction not what you get from the particular encoding of Z? 08/06 17:25 I guess it's probably not quite. 08/06 17:25 dolio: you need two base cases (0 and -1) and on the other hand the two proofs can make use of the sign of the number 08/06 17:34 i'm still looking for a good excuse to use the snowman operator 08/06 17:36 Is there any way to prove equality is decidable with less than a quadratic number of cases in the constructors? 08/06 18:48 I think I recall something about converting to nat codes? 08/06 18:48 napping: converting to Fin codes works better 08/06 18:55 yeah, it seems to work reasonably well for nullary constructors 08/06 18:55 is there a nice way to prove something holds for every value in a fixed Fin k? 08/06 18:56 You could construct a universe of finite types, and write a generic procedure for provably deciding equality of finite types. 08/06 18:56 if you have constructors with arity your best bet is encoding with Eithers 08/06 18:56 I was thinking of a dependent sum of a fin tag and payload 08/06 18:56 but a more basic question is just how to prove (f : Fin 8) -> f ≡ test-to-fin (fin-to-test f) 08/06 18:57 without writing cases like iso2 (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl 08/06 18:57 hmm, I guess I can't really compute anything much nicer than that 08/06 18:57 hm, does iso2 (# 7) = refl work? 08/06 18:58 no, and I would be surprised if it did 08/06 18:58 with nullary constructors i'd have suggested proving it in the other direction, though 08/06 18:58 napping: i would have been slightly surprised, but not extremely 08/06 18:59 well, the cases for the other side (t : Test) → t ≡ fin-to-test (test-to-fin t) are at least flst 08/06 18:59 flat - like iso1 F = refl 08/06 18:59 I guess I might only need the one direction to get the proof to go through 08/06 18:59 hm, come to think of it i'm not sure if you need just one direction or both 08/06 19:00 t ≡ fin-to-test (test-to-fin t) should be enough, if I could rewrite it in Dec (a ≡ b) 08/06 19:01 if you need both, it might be easier to express one of the functions as a Vec 08/06 19:01 yeah, that's what I did for the conversion from fin 08/06 19:01 http://code.haskell.org/~Saizan/Eq.agda <- one direction is enough 08/06 19:26 Can you prove y ≡ y' from (i' , y) ≡ (i' , y') ? 08/06 19:45 cong snd 08/06 19:46 the pairs are dependent 08/06 19:46 and cong proj₂ does not work 08/06 19:46 first pattern match on cong fst 08/06 19:46 so, what you can prove is  y ≡ subst .. .. y' 08/06 19:48 what do you mean, pattern match on cong fst? 08/06 19:50 on i'? 08/06 19:51 with block of cong fst and match on refl? 08/06 19:51 oh, to make the type of the second part reduce 08/06 19:51 cong fst of the equality, to make the first projections equal in the context 08/06 20:03 I don't see how to do that 08/06 20:17 cong proj\_2 of the equality isn't well typed, so you can't state it ahead of time 08/06 20:17 use cong on heterogeneous equality? 08/06 20:19 and then bring that back to homogeneous 08/06 20:20 that should work 08/06 20:20 Is there a nice way to prove {k : ℕ} → Decidable (_≡_{A = Fin k})? 08/06 20:23 foo : ∀ {A : Set}{B : A -> Set} -> (a b : Σ A B) -> a ≡ b -> A 08/06 20:25 foo (i , y) (i' , y') eq with cong proj₁ eq 08/06 20:25 foo (i , y) (.i , .y) refl | refl = { }1 08/06 20:25 also works 08/06 20:26 napping: there's one in the stdlib 08/06 20:26 copumpkin: that worked nicely 08/06 20:26 Data.Fin.Props._≟_ 08/06 20:27 the .Props vs. .Properties has bothered me for a while :P 08/06 20:28 heyo 08/06 20:29 how it that foo supposed to be used? 08/06 20:29 Actually, that will work fine. 08/06 20:29 I think he was just illustrating the idea of matching on cong proj1 08/06 20:30 That won't do to prove the projections equal in a visible way, but I just need to feed the equality to a ≢ proof 08/06 20:30 well, ≅ is working great 08/06 20:30 Is there a nice way to define records containing functions that need to do pattern matching 08/06 20:34 something like a module? 08/06 20:34 or even record puns 08/06 20:35 napping: the best right now is record { foo = foo ; bar = bar } where { foo x = blah; bar y = woof } 08/06 20:35 (sadly) 08/06 20:36 a proper record block is on my agda wishlist 08/06 20:36 a where clause doesn't introduce the local definitions of your record either 08/06 20:39 They're discussing ways to have pattern matching lambdas on the mailing list. 08/06 20:39 that would help too. 08/06 20:39 Seeing the = and ;, I hoped you could write patterns directly in a record block 08/06 20:39 There, finished: http://hpaste.org/47596/deciding_equality 08/06 20:47 cool 08/06 20:48 Now I should get back to the Coq proof where it wants eq_dec on a type with 14 constructors. 196 cases the naive way, before you even start comparing arguments 08/06 20:50 maybe best to leave it an Axiom 08/06 20:50 I guess that suggests the question of whether the proof can go through without K 08/06 20:51 I'm guessing no, for this version with arguments. 08/06 20:51 you don't need K in general, but you probably need some cases of K 08/06 20:52 (which ones depending on your type) 08/06 20:52 not sure if they would be directly provable cases or not though 08/06 20:53 i'm still a little uncertain on how much J buys you 08/06 20:53 Where is K being used there? 08/06 20:54 converting heterogeneous to homogenous equality, maybe some of the pattern matching 08/06 20:55 Oh. 08/06 20:55 being able to project like that from a dependent equality is one of the things listed in EqdepFacts 08/06 20:56 This is for equality on finite sets? 08/06 20:56 For types with arguments 08/06 20:57 I might be able to make it go through by using more custom types rather than trying to reuse Vec and Fin and Σ 08/06 20:57 technically you could make info-dec a Vec too, couldn't you? 08/06 20:59 it would need to be a more dependent kind of Vec 08/06 21:00 oh, Vec isn't dependent enough?  :( 08/06 21:00 "A" doesn't vary by index 08/06 21:00 you need HVec!  :) 08/06 21:00 I've wondered how to write HVec without writing a non-heterogeneous one before 08/06 21:01 you can index it by a list of Set 08/06 21:01 but that feels ugly 08/06 21:02 or maybe you could make info : \Sigma Set (\ T -> Decidable (_\==_ { A = T })) 08/06 21:02 xplat: how would you use that? 08/06 21:02 well, "info" is the one describing the arguments to the constructor with a given code, but I don't see how that would work for info-dec 08/06 21:03 Perhaps you mean (T : Set) -> Decidable (_\==_{A = T})? 08/06 21:04 that would certainly be strong enough :) 08/06 21:04 lol 08/06 21:04 you make code = \Sigma (Fin 2) (\ i -> proj\_1 (lookup i info)) and then you use them together 08/06 21:04 you can derive LEM from that can't you? 08/06 21:04 something like that. 08/06 21:04 Well, yes you can. 08/06 21:04 in fact, it's almost exactly LEM 08/06 21:04 er, info should be a Vec of the type i gave before 08/06 21:04 but there have been things before that made Agda anti-classical 08/06 21:05 well, i folded info-dec into info and the same technique would work on unrep, but napping already left 08/06 21:29 is there some kind of way to have implicit fields in a record? 08/06 21:32 specifically, one with constructor 08/06 21:32 try putting the field name in {..} 08/06 21:33 Saizan: thanks 08/06 21:51 what causes errors like this? 08/06 21:51 Cannot instantiate the metavariable _115 to A since it contains the 08/06 21:51 variable A which _115 cannot depend on 08/06 21:51 when checking that the expression info has type Vec Coder k 08/06 21:51 xplat: sounds like circularity 08/06 21:53 never mind, found it 08/06 21:53 augur: no, i left off a type parameter from a function when another type implicitly depended on that parameter 08/06 21:53 ahh! 08/06 21:56 @tell napping annotated your paste with http://hpaste.org/47598/same_great_decidability_less which illustrates what i was talking about ... 08/06 22:02 Consider it noted. 08/06 22:02 data _bsl_ {A : Set} : List A -> List A -> Set where stop : [] bsl [] drop : forall {xs y ys} -> xs bsl ys -> xs        bsl (y :: ys) keep : forall {x xs ys} -> xs bsl ys -> (x :: xs) bsl (x :: ys) 08/06 22:04 ^ Isn't this really subsequence? 08/06 22:04 yes 08/06 22:05 Okay.  Thanks. 08/06 22:13 i guess the ultimate form of HVec would be a snoc-vector where the type of each last was dependent on its corresponding init 08/06 22:16 well, it could be a cons vector too, but that wouldn't be very intuitive 08/06 22:18 usually called a "telescope" 08/06 22:18 yeah, can you write a real telescope type in agda? 08/06 22:18 hm, maybe a cons with l-r dependencies would be doable, but you would definitely have to resolve them before you entered the tail 08/06 22:19 i find myself honestly unsure which direction would be less annoying :) 08/06 22:20 i just started thinking about this because if you don't want to hand-uncurry constructors in the semi-automatic equality code you need telescop-y stuff 08/06 22:22 (even with that i'm not sure it's possible to write something easier to use than hand-uncurrying when you have a highly dependent constructor) 08/06 22:23 http://hpaste.org/47599/telescope <- from the outrageous coincidences paper, using Agda's Set as the base universe though 08/06 22:25 hah, forgot to make Cx : Set1 08/06 22:26 which paper is that? 08/06 22:26 http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf 08/06 22:26 thanks! 08/06 22:28 --- Day changed Thu Jun 09 2011 are there any data types that represent graphs inherently, as opposed to just by way of, say, an edge list or adjacency matrix? 09/06 01:06 i mean, like, a data type where the constructors are node constructors, for instance 09/06 01:07 what do you mean by 'inherently?' 09/06 01:07 well, a tree could in principle be represented as a pair list or adjacency matrix or some nonsense like that, right 09/06 01:07 or 'node constructors'? 09/06 01:07 but the algebraic tree types are not that 09/06 01:07 they just directly represent tree structure 09/06 01:07 is there an analogy for graphs? of any sort? 09/06 01:08 well in principle you could have a datatype of rational trees 09/06 01:08 rational trees huh 09/06 01:09 a rational tree is basically a pointed finite digraph where there's a path from the basepoint to anywhere 09/06 01:09 hmm 09/06 01:09 how about trees where some nodes can be "sewn together"? 09/06 01:11 that's basically what a rational tree is 09/06 01:11 aha! ok 09/06 01:11 any pointers? google seems to have a high noise ratio for this term 09/06 01:12 YAML is able to serialize rational trees 09/06 01:12 it's not a common term, but i don't think there's a commoner alternative 09/06 01:13 hm 09/06 01:13 i first heard of them in connection with logic programming 09/06 01:13 and whats the data structure for them, do you know? 09/06 01:13 if i google 'rational tree' (no quotes in the search term) i find several relevant papers on the first page 09/06 01:14 hm 09/06 01:15 ok 09/06 01:15 in memory a rational tree is usually represented exactly the same way as a regular tree except there are no restrictions on which nodes can point to which 09/06 01:16 they are a little different from true graphs though since nodes don't have identity 09/06 01:17 xplat: sure, except in an algebraic data type thats harder to explain 09/06 01:18 since theres no way to really say "this node and that node are actually the same" 09/06 01:18 they might be equal but distinct 09/06 01:18 Branch 2 (Leaf 1) (Leaf 1) 09/06 01:18 so any two rational trees that have the same set of valid paths and the same sequence of labels on each path are equal 09/06 01:19 is there one leaf or two? 09/06 01:19 hm 09/06 01:19 that cant be all there is to it tho 09/06 01:19 is it? 09/06 01:19 hm 09/06 01:19 well, you can create a form with identity too, but the basic form has that property 09/06 01:19 right, but _all_ trees are rational trees then 09/06 01:19 and all rational trees are normal trees 09/06 01:19 at least in an ADT 09/06 01:20 no, because if you unfold a rational tree with a cycle you would get an infinite tree 09/06 01:20 ahh ok i see 09/06 01:20 i was thinking more where you can sew nodes together as long as you dont create cycles 09/06 01:20 i didnt think of the cyclic case 09/06 01:20 hm 09/06 01:20 and if you add node identity to rational trees even the acyclic case gives you something different from normal trees 09/06 01:22 you would normally do this in, e.g., the case of mutable rational trees 09/06 01:23 hmm 09/06 01:23 sure ok 09/06 01:23 im just looking for a data structure that represents this sort of thing in a natural way 09/06 01:23 besides a pointer structure, you can also represent a rational tree as a bag of equations 09/06 01:24 er, set of equations 09/06 01:24 a simple example: {a = true :: b ; b = true :: a} 09/06 01:25 er, b was supposed to be false :: a 09/06 01:25 right, so basically the pair list thing 09/06 01:25 otherwise it may as well be {a = true :: a} 09/06 01:26 hmm 09/06 01:26 aha, hows this for a representation of (acyclic?) rational trees 09/06 01:26 (t : Tree) x List ((i : Index t) x (j : Index t) x (i == j)) 09/06 01:27 er sorry 09/06 01:28 (t : Tree) x List ((i : Index t) x (j : Index t) x (lookup i t  == lookup j t)) 09/06 01:28 a tree and a list of triples -- two paths and a proof that the two paths point to the same thing in the tree 09/06 01:28 is this inductive tho .. hmm 09/06 01:29 well, that seems like a workable (if sometimes potentially exponentially oversized) inductive-ish definition of rooted DAGs 09/06 01:32 hmm 09/06 01:32 exponentially oversized? 09/06 01:32 (otoh although it can sometimes be exponentially oversized, it can also sometimes be exponentially undersized compared to, say, an adjacency list) 09/06 01:32 hm. 09/06 01:33 well, ill just stick with implementation neutral algebraic approaches for now 09/06 01:34 using structured Set's 09/06 01:34 augur: if the graph has a lot more paths than nodes (say it's a 'snake' made of diamonds, or a 'ladder' made from 2 lists) then depending how it's computed it can have exponentially more real nodes than an adjacency list representation 09/06 01:34 oh, but theres no reason why the list has to have ALL the paths to the objects in question 09/06 01:35 ah well i guess it would tho wouldnt it 09/06 01:35 to ensure that things arent mistakenly disidentified 09/06 01:35 hmm 09/06 01:35 augur: it wouldn't necessarily, but it could, and it could also have exponentially many copies of nodes far from the root 09/06 01:35 hmm hmm 09/06 01:36 otoh, if you have a big graph with lots of nodes and lots of isomorphic subgraphs, you can represent it with logarithmically many in-memory nodes if you compute it carefully 09/06 01:36 so it's not always huge compared to standard reps, it just has very different, and somewhat fussy, performance characteristics 09/06 01:37 you can help it perform better by judicious use of memoizing and never recording equations between paths that already have a nontrivial equation between prefixes 09/06 01:41 like, never equate {abcd} and {efgh} if you already equated {ab} and {ef} 09/06 01:42 you actually should probably be even more particular like that about managing the equations, but that's a start and it expresses the general idea 09/06 01:43 ok. 09/06 01:50 its not that big a deal 09/06 01:50 its not really something i need, just something i was curious about 09/06 01:51 P 09/06 01:51 :P 09/06 01:51 so why cant i have multiple lambdas in a syntax definition? 09/06 12:47 also, why does   syntax Σ A (λ x → B) = x ∶ A ∣ B   give me the error   syntax Σ A (λ x → B) = x ∶ A ∣ B 09/06 12:59 er.. 09/06 12:59 damnit aquamacs :| 09/06 12:59 Names out of scope in fixity declarations: Σ 09/06 12:59 'syntax' is considered a fixity declaration for the purpose of that message.  try putting the syntax declaration closer to the definition of \Sigma.  or outside the record definition, if \Sigma is declared as a record constructor. 09/06 15:46 augur: ^ 09/06 15:52 I want to use Relation.Binary.EqReasoning to reason about equalities in ℕ. What's the correct way to open it? I can't see what the appropriate setoid should be called. 09/06 16:24 Ah, got it. open Relation.Binary.EqReasoning (setoid ℕ) 09/06 16:26 I think the Nat module already has a module you can open for that in it 09/06 16:26 maybe I'm misremembering though 09/06 16:26 somewhere there's a \==-Reasoning that works for \== in general 09/06 16:27 yeah, I guess I'm wrong 09/06 16:27 I found an example on the web using Data.Nat.setoid but it didn't seem to exist. setoid ℕ is fine though. 09/06 16:28 oh, the module I was thinking of was the order-based reasonining on Nat 09/06 16:28 reasoning 09/06 16:28 ah, in Relation.Binary.PropositionalEquality 09/06 16:28 module ≤-Reasoning where 09/06 16:28 setoid \bn?  how is that supposed to even work? 09/06 16:34 you can't pattern-match on Set·s ... 09/06 16:35 you don't need to 09/06 16:36 oh, maybe it's Relation.Binary.PropositionalEquality's \bn? 09/06 16:36 setoid : ∀ {a} → Set a → Setoid _ _ 09/06 16:36 er, setoid? 09/06 16:36 yep 09/06 16:36 but \==-Reasoning seems better if you already know you're using \== 09/06 16:37 yeah 09/06 16:37 copumpkin: Do you have slides from your Agda talk? 09/06 20:30 yep 09/06 20:32 http://dl.dropbox.com/u/361503/Agda%20and%20dependent%20types.pdf 09/06 20:32 there's also the underlying keynote file if you prefer 09/06 20:32 Nah, I just wanted to look at what you talked about. 09/06 20:42 I still don't know what to talk about tomorrow. 09/06 20:42 What are you doing tomorrow that involves you talking? 09/06 20:44 We have a weekly FP/category theory/math stuff meeting at work. 09/06 20:45 So I've been covering type theory stuff. 09/06 20:45 Starting with propositional calculus and natural deduction, then simple types, then dependent types. 09/06 20:45 So tomorrow the plan was to show some Agda, for a real language with dependent types. 09/06 20:45 Why can't I work at a good job? :( 09/06 20:46 You could. 09/06 20:46 I tried to get you set up with an internship, but no, you were like "I'm too good for this" 09/06 20:47 They just sent out a PDF with intern pictures today. 09/06 20:47 Yes, I need to hone my skills at this PHP chopshop instead. 09/06 20:47 You could have been in there. 09/06 20:47 I'm sure he still could be if we tried hard enough 09/06 20:48 He can't be in the PDF they sent out today. 09/06 20:48 it's a harry potter PDF 09/06 20:48 Unless we use your time machine. 09/06 20:48 with interactive content 09/06 20:49 I'm sure the PDF spec allows fully executable programs on pages these days 09/06 20:49 Probably. 09/06 20:49 I don't think that works when you print it 09/06 20:49 no, it does 09/06 20:49 new special printers 09/06 20:49 What does it do, print out an iPad? 09/06 20:50 something like that 09/06 20:50 So I guess I can go through defining all the basic types... 09/06 20:51 Explain the operator syntax. 09/06 20:51 And the holes. 09/06 20:51 and inductive families! yay 09/06 20:51 Equality, at least. 09/06 20:52 Maybe I could try to explain why sigmas are like sums, and pis like products. 09/06 20:52 Instead of the obvious products and functions respectively. 09/06 20:52 yeah, that'd be good 09/06 20:52 That was part of my notes I didn't get to last week. 09/06 20:53 And after that I was going to talk about the adjunctions between them. 09/06 20:53 Which I started doing in Agda, but I'm not sure how bad that'd get. 09/06 20:53 I don't really want to talk about universe polymorphism, but it requires equality at the type level. 09/06 20:54 Universe polymorphism is like the coolest part of Agda 09/06 20:54 meh 09/06 20:54 Also one of the parts that I still feel like I don't formally understand 09/06 20:54 It's also one of the least well grounded in literature. 09/06 20:55 Maybe you should skip dependent type implementations like Agda and go directly to HoTT (or OTT first). :p 09/06 20:56 Go towards OTT. I missed that joke. 09/06 20:58 :O 09/06 20:58 djahandarie: look at Type Checking with Universes for an intuition. it's technically not the same thing, but related 09/06 21:02 Wow, I need to be careful not to press C-c C-a tomorrow. 09/06 21:05 It's writing this stuff itself. 09/06 21:05 map∏ : ∀{I J} {F G : Fam (I × J)} → (F ⇉ G) → ∏ F ⇉ ∏ G 09/06 21:05 map∏ f = λ i x j → f (i , j) (x j) 09/06 21:05 Oh, it can't do sums, though. 09/06 21:09 xplat: thank you 09/06 21:19 has anyone read Denney's refinement paper? 09/06 21:20 well, his dissertation 09/06 21:20 Are there any examples with sized types? 09/06 23:00 napping: You have 1 new message. '/msg lambdabot @messages' to read it. 09/06 23:00 napping: I vaguely remember coming across some a while back in the agda repo 09/06 23:01 which repo? 09/06 23:02 agda-lib defines Size, but nothing uses it 09/06 23:02 http://code.haskell.org/Agda/examples/Termination/Sized/DeBruijn.agda 09/06 23:05 not sure if that stuff still works 09/06 23:05 http://code.haskell.org/Agda/examples/Termination/Sized/SizedNat.agda 09/06 23:05 that? 09/06 23:05 for some reason, code.haskell.org is not visible from here 09/06 23:07 I found slides from AIM 2008, I'll see if that code works 09/06 23:08 seems to be accepted, with the --sized-types flag 09/06 23:13 I wonder if the interaction with the new coinductive definitions has ever been checked 09/06 23:18 It seems ^ is supposed to be something different from ↑ 09/06 23:25 --- Day changed Fri Jun 10 2011 copumpkin! 10/06 00:04 yo 10/06 00:05 hows life, copumpkin 10/06 00:14 pretty good 10/06 00:16 you? 10/06 00:16 copumpkin: same same. trying to finish a revision of a paper that i really should have done by now 10/06 00:28 oh man, contravariant subtyping in agda! 10/06 15:04 napping sure doesn't tend to stay on long 10/06 15:22 still have no idea if that hpaste annotation i did was ever read :-/ 10/06 15:22 it's kind of annoying on github having ssh keys and a password and they pretty much have non-overlapping functionality 10/06 15:33 i don't suppose there's some sort of secret github api via ssh 10/06 15:33 the regular API only supports password auth too 10/06 15:34 not sure 10/06 15:36 @tell napping xplat wanted you to read something 10/06 15:37 Consider it noted. 10/06 15:37 copumpkin: i already tried that :) 10/06 15:48 @tell napping xplat also used @tell to tell you something, so you should read that after you read this, in case you didn't notice it in your @messages output. So yeah, it's a couple of lines above this one. Look up^^ 10/06 15:49 Consider it noted. 10/06 15:49 lol 10/06 15:49 you can never be too sure 10/06 15:49 * xplat takes off and @tells napping from orbit. It's the only way to be sure. 10/06 15:50 oh yeah, I hadn't thought of that 10/06 15:52 copumpkin: btw are you going to have time to merge my categories changes into master so i have a good base to start the porting from?  or do you want to just push the new files you missed so i can merge from my end?  (assuming you can even get at them from there ...) 10/06 15:52 oh yeah, sorry, didn't realize you were waiting on me 10/06 15:53 should be up to date now :) 10/06 15:54 I think I'll try to fix Agda and tinker with that library today 10/06 15:54 there's lots of stuff still todo! 10/06 15:54 yay 10/06 15:54 (co)equalizers 10/06 15:54 yoneda! 10/06 15:54 all the monoidal junk 10/06 15:54 kan extensions so we can finally finish them there profunctors in a cute category 10/06 15:55 Enriched categories! 10/06 15:55 Category.Agda still bothers me 10/06 15:55 we should probably just accept that one will be setoids and the other will be sets 10/06 15:55 or something 10/06 15:55 or that one will be category theory and the other will be category-extras 10/06 15:56 well, I did kind of want a distinction like that 10/06 15:56 so you're saying Setoids is more pure, and Sets is more for hardcore categorical programming in agda? 10/06 15:56 I also kind of wanted to play with that non-endo-monad 10/06 15:58 How do you plan on handling things when it gets bicategories and such? Won't that allow like half of the definitions to be rewritten? 10/06 15:58 I dunno, I can't say I have much of a vision for this :) 10/06 16:00 I think it wouldn't be terrible to keep the simple versions of structures around unless we can make the specific generalized instances as easy to use 10/06 16:00 Wait, Agda has subtyping? 10/06 16:01 I think the sized types thing behaves a bit like subtyping 10/06 16:01 How do I eliminate lemma₁ from this: http://hpaste.org/47645 10/06 17:07 Thought I could just use refl but it doesn't like that. 10/06 17:09 i don't know why refl won't work there, what does it say? 10/06 17:14 it works for me, but is yellow 10/06 17:15 The preceding expression headed by cong ends up yellow. Yellow isn't good, right? 10/06 17:15 2 * suc n + n * (1 + n)    ≡⟨ cong (λ p → 2 * p + n * (1 + n)) (refl {_} {_} {suc n}) ⟩ 10/06 17:16 that works 10/06 17:16 Not 100% sure what yellow means. I guessed it was something like: "I can't rule this out but I don't have enough info to prove it correct." 10/06 17:16 as does 10/06 17:16 2 * suc n + n * (1 + n)    ≡⟨ cong (λ p → 2 * p + n * (1 + n)) (refl {x = suc n}) ⟩ 10/06 17:16 dpiponi: it means that there are unsolved metavariables 10/06 17:16 underconstrained 10/06 17:16 often could be implicits that it can't figure out from context 10/06 17:16 i loaded it as is and there was no yellow 10/06 17:16 xplat: well, with the explicit lemma it's fine 10/06 17:17 xplat, he means get rid of lemma_1 and replace it with refl 10/06 17:17 Oh! That works! But I could swear I tried exactly that. 10/06 17:17 dpiponi: well, you might have passed the wrong implicit? constructors get all the parameters to the data type 10/06 17:17 so the first implicit is the universe level 10/06 17:17 the next is the type, then comes the value 10/06 17:17 * copumpkin shrugs 10/06 17:18 Yes. But I did look up to exactly what those implicits were. Must have been a typo. Anyway, I'm excited I've reproduced by first high school induction, even if not over ℤ. 10/06 17:18 oh 10/06 17:18 but actually 10/06 17:18 cong on refl is pointless 10/06 17:18 Implicits have always seemed a little ugly to me 10/06 17:18 that whole line turns into 10/06 17:18 2 * suc n + n * (1 + n)    ≡⟨ refl ⟩ 10/06 17:18 or you can just rewrite it directly 10/06 17:19 Oh yeah! And it doesn't need help with the implicits either. 10/06 17:19 yeah 10/06 17:19 this theorem is not tail recursive!! 10/06 17:21 Is that bad? 10/06 17:21 no, just being silly :) 10/06 17:21 i just replaced the whole cong with refl 10/06 17:22 It doesn't even matter if actual functions in Agda are tail recursive. 10/06 17:22 No one will be running them, after all. 10/06 17:22 exactly! 10/06 17:22 oh, already done :) 10/06 17:22 Took me ages to figure out how to unpack all of the properties of semirings. But now I've done it once, it should be easier in future. 10/06 17:22 at some point I started an ambitious project to do extensible dependent records for universal algebra-like structures 10/06 17:24 but then I started ripping my hair out 10/06 17:24 I wonder if I'd be more clueful now 10/06 17:24 I wonder how hard it would be to prove the infinitude of the primes. 10/06 17:24 Extensible dependent records for universal algebra-like structures? 10/06 17:24 dpiponi: it's in the stdlib readme btw: http://www.cse.chalmers.se/~nad//listings/lib/README.Nat.html 10/06 17:25 you could do something like module * = IsCommutativeMonoid *-isCommutativeMonoid and then do *.comm and such 10/06 17:25 djahandarie: talking about structures as combinations of sets, n-ary functions on those sets (where 0-ary is a "distinguished element"), and properties relating those functions to each other 10/06 17:26 it was fun, but I didn't like the way I was approaching it so put it off to another day 10/06 17:26 What was complicated about it? 10/06 17:27 my main issue was with "naming" (in some abstract manner) the sets, operations, and properties 10/06 17:27 stevan: thanks. I should keep my eyes more open for things called README! 10/06 17:27 so that you can share them between structures and talk about x being a subset of y 10/06 17:27 Ah. 10/06 17:27 does agda allow any kind of module qualification on infix operators? 10/06 17:28 don't think so 10/06 17:28 Lame, even Haskell can do that! ;) 10/06 17:28 I can see where module qualification on mixfix operators would get a little confusing though. 10/06 17:28 Haskell can do a *lot* more with binary operators than agda, the only thing it lacks is some flexibility in naming 10/06 17:29 otoh, agda can do lots of stuff with non-binary operators that Haskell can't 10/06 17:29 What else can Haskell do, besides sections? 10/06 17:29 well, sections and qualification are basically it, but that's already a lot more 10/06 17:30 xplat: I'd argue that qualification isn't all that relevant given Agda's renaming feature 10/06 17:33 xplat: plus the possibility to open modules locally 10/06 17:33 kosmikus: that's like arguing that renaming modules isn't relevant since you can always make a new local module 10/06 17:33 xplat: feel free to disagree :) but I certainly miss sections more than qualified infix operators 10/06 17:34 well, try writing open Category C renaming (_\o_ to _\oC_; _\==_ to _\==C_) and the same for D and E a few dozen times and you'll already start getting sick of it 10/06 17:35 but yeah, i also miss sections even more 10/06 17:36 I thought there were some plans at some point to have mixfix sections 10/06 17:41 it sounds horrifying to parse, but maybe not if I read the mixfix parsing stuff 10/06 17:41 if the module system was less of a language of its own you could abstract the repetitive renaming into a function 10/06 17:45 copumpkin: i figure it wouldn't be so horrifying to parse if instead of the null string you indicated sections by _ glued in 10/06 17:48 so _+ 1 or 1 +_ 10/06 17:48 and it's a nice generalization of 1 + 1 vs _+_ 10/06 17:49 so it makes more sense that way anyhow 10/06 17:49 except that currently you can have a distinct _+ identifier 10/06 17:52 but i don't think anyone would mind losing that 10/06 17:53 currently you can already cause issues like that 10/06 18:12 with <_+_> and _+_ 10/06 18:12 do the fixity annotations allow one to take precedence over another? 10/06 18:12 that seems kind of scary 10/06 18:12 argh 10/06 18:16 i could totally write module Equiv {A B : Obj} = IsEquivalence (equiv {A} {B}) except it complains because equiv is irrelevant 10/06 18:17 same thing happens if i open public :( 10/06 18:19 if i open privately then it lets me, and marks all the functions as irrelevant 10/06 18:19 why won't it do that for a public open? 10/06 18:20 grumble grumble pointless rewriting of type signatures 10/06 18:20 yeah, that's what I wanted irrelevant modules for 10/06 18:24 there's a ticket in the tracker for that 10/06 18:24 i can also write something like refl = IsEquivalence.refl (equiv {A} {B}) without a type signature 10/06 18:26 only if equiv is irrelevant it complains again 10/06 18:26 and i can't just write .refl, i have to write a whole type signature 10/06 18:26 argh 10/06 18:26 standard library setoids do not have irrelevant equivalence either 10/06 18:38 and probably something would go wrong if i made hom-setoid irrelevant as a whole :( 10/06 18:39 I'm not sure, is irrelevance supposed to change semantics? I first had the impression it was meant to provably discard arguments at runtime. 10/06 18:40 well, i'm going to try just making the whole thing irrelevant and see what problems come up 10/06 18:41 * Eduard_Munteanu should play with those too 10/06 18:41 well, the first problem is i can't take a setoid as an irrelevant parameter in a module (?!) 10/06 18:43 or if i can i can't figure out where to put the dot 10/06 18:43 the more i use irrelevance the less it seems like it is ready for prime time 10/06 18:45 but throwing it out is definitely not an option either 10/06 18:45 What does irrelevance give you anyway? 10/06 18:46 Surely it doesn't make typechecking use less memory or finish sooner. 10/06 18:46 i'm not going to accomplish much by porting this if i end up having to make the irrelevance-annotated version of everything in the standard library anyway though 10/06 18:47 Eduard_Munteanu: actually it does; once a closed value is supplied for an irrelevant parameter it can be erased even during typechecking 10/06 18:47 Oh. I guess it makes sense then. 10/06 18:48 Eduard_Munteanu: if you have data Moo : Set where x : .Nat -> Moo, you could prove x 5 == x 7 10/06 19:22 this for example: http://snapplr.com/3z5s 10/06 19:25 gah, can't even use Data.Unit in Categories.Terminal 10/06 19:36 why not? 10/06 19:36 ⊤ is only in Set 10/06 19:36 I've wondered about how important that is 10/06 19:36 My client can't even display that character. :( 10/06 19:36 Who needs cumulativity? 10/06 19:36 people who want to have a category of categories that is cumulative and doesn't have a sigma for a bounded level 10/06 19:37 Defining a universe polymorphic top doesn't work very well, either. 10/06 19:38 Unless you like writing '\top i' everywhere. 10/06 19:38 apparently that's what we've been doing up to now 10/06 19:38 yeah, we have 10/06 19:38 but it's implicit and silly 10/06 19:38 see, I don't really know how important it is to have things like that be able to live at arbitrary levels 10/06 19:38 same issue with discrete categories 10/06 19:39 and the parameter seems to infer just fine the few places it's used 10/06 19:39 using == for morphisms 10/06 19:39 copumpkin: well, without a level-polymorphic Categories.Terminal only the categories-of-categories where objects are at level 0 have finite products 10/06 19:39 fair enough 10/06 19:40 that'd be annoying 10/06 19:40 we could just use Lift everywhere though 10/06 19:40 that'd probably be even more annoying though 10/06 19:40 time to port this all to mini-agda 10/06 19:40 :) 10/06 19:40 How would mini agda help? 10/06 19:41 I should really go read more about that thing 10/06 19:41 i just made a private unit type since no operations on it are needed 10/06 19:43 I wonder how many interesting operations there are on it :) 10/06 19:44 djahandarie: cumulativity 10/06 19:44 djahandarie: Because miniAgda has cumulativity? I think it does. 10/06 19:47 It has variance tracking, too. 10/06 19:48 for sizes? 10/06 19:48 or what? 10/06 19:48 You can write Mu in it. 10/06 19:48 :o 10/06 19:48 data Mu (F : Set++ -> Set) where roll : F (Mu F) -> Mu F 10/06 19:49 Something like that. 10/06 19:49 can it be a record? 10/06 19:49 Meaning that F is strictly positive in its first argument. 10/06 19:49 that seems like fun 10/06 19:49 And there's + and -, too. 10/06 19:50 Whether it could be a record depends on whether recursive records are allowed. And I don't know that. 10/06 19:51 Just a week until my laptop allegedly ships. I wonder if they'll charge me. 10/06 19:52 oh man 10/06 19:52 that's exciting 10/06 19:53 are you itching to write some hardcore agda again? 10/06 19:53 Yeah. 10/06 19:53 Assuming the order is actually valid. 10/06 19:53 Hardcore Agda, 18+ only 10/06 19:54 I don't think we have any under-18s in here 10/06 19:54 cause dylukes left :( 10/06 19:55 :( 10/06 19:55 woo 10/06 19:55 I can pretend to be <18 10/06 19:55 activity 10/06 19:55 :D 10/06 19:55 hi guyz im in middle school, tryin to understand how agda works, u know, dependent types n stuff 10/06 19:56 I wonder how far I could get teaching middle schoolers Agda 10/06 19:58 djahandarie: omg go away, only hardcore agda in here 10/06 19:58 djahandarie: I don't think it's that fundamentally difficult 10/06 19:59 Ageist! 10/06 19:59 it's more types than most programmers are used to 10/06 19:59 but people with no expectations might not have as much trouble with it 10/06 19:59 it's a fairly simple and consistent set of rules, at least if you stay away from coinduction :) 10/06 19:59 and maybe irrelevance 10/06 19:59 The irrelevance stuff isn't really very hard, either, until you muck it up with all the ways Agda is different from the simpler theories in papers on it. 10/06 20:02 yeah 10/06 20:03 the irrelevant pi thing seems kind odd and not quite fleshed out yet 10/06 20:03 Real coinduction isn't harder than induction, either. 10/06 20:03 yeah, but the whole story about # x /= # x seems odd 10/06 20:04 What might be harder is the Agda, "no one knows the underlying theory of this stuff," version. :) 10/06 20:04 maybe I'm just thinking about it wrong 10/06 20:04 also, equality of where clauses and absurd lambdas! :P 10/06 20:05 Yeah, the implicit generativity is weird. 10/06 20:06 Combined with the lack of sufficiently extensional equality. 10/06 20:06 random idea: take the BitVector work glguy and I did, and build floats on top of it 10/06 21:36 then model floating point algorithms 10/06 21:36 it'd be nice to have rationals though 10/06 21:37 to "ground" the floats in 10/06 21:37 I'm certainly dying to prove things about the IEEE spec. 10/06 21:37 I thought you might 10/06 21:37 --- Day changed Sat Jun 11 2011 copumpkin: so far i'm up to Categories.Grothendieck, but i'm running out of steam 11/06 03:33 yet again there's an irrelevant version of something in the stdlib 11/06 03:33 and now i'm on Globe and there is no proof in the stdlib that <-trans is associative 11/06 04:01 uniqueness for < would work too 11/06 04:02 xplat: ack :/ 11/06 04:21 yeah, I wish irrelevance would infect the stdlib 11/06 04:21 * augur infects copumpkin's stdlib 11/06 04:23 lol 11/06 04:23 so, i get that this would fail termination checking, but aside from embedding Nat in a data strcuture that includes negativie/positive infinity, how might one implement the following: http://www.randomhacks.net/articles/2007/02/02/divide-infinity-by-2 11/06 05:11 infinity = Succ infinity 11/06 05:11 is what i'm referring to 11/06 05:11 i'm guessing it would use coinduction somehow, but i'm not really up to speed on that 11/06 05:12 Yes. The naturals he's using are coinductive. 11/06 05:15 Technically they're also inductive, because inductive and coinductive types coincide for Haskell. 11/06 05:16 dolio: which is to say its all coinductive in haskell, no? 11/06 05:16 Yes, everything is inductive and coinductive. 11/06 05:17 well but nothing in haskell can be truly inductive due to laziness, no? 11/06 05:17 No, they're all inductive. 11/06 05:17 They're just not inductive sets. 11/06 05:17 hmm 11/06 05:17 They're inductive domains. 11/06 05:17 hmm 11/06 05:17 right 11/06 05:18 but could you do something that would acheive the same results without making Nat codata? 11/06 05:19 (and without wrapping Nat) 11/06 05:19 not opposed to the latter, just curious 11/06 05:19 You could turn off the termination checker. 11/06 05:19 haha yeah 11/06 05:19 i like to keep it on and pretend agda is CIC^ :P 11/06 05:20 Agda actually does non-strict evaluation, so it'd work out. 11/06 05:21 Except, perhaps, if you used the BUILTIN pragma, which makes Nat backed by Haskell's Integer, which can't encode inf = succ inf. 11/06 05:22 yeah 11/06 05:23 However, if you used the infinite value in a type such that it had to be normalized, there'd be a problem. 11/06 05:23 this is an interesting solution, going the packing route: http://blog.jbapple.com/2007/02/countable-ordinals-in-haskell.html 11/06 05:23 indeed 11/06 05:23 in the case i'm considering using for, it wouldn't need to be normalized 11/06 05:23 Ordinals are rather different. 11/06 05:23 yeh, the size of the set of nats, instead of the value 11/06 05:24 (or size of any set) 11/06 05:24 "Now, according to Fokkinga and Meijer, there’s actually some pretty deep math lurking here. Apparently, Haskell’s lazy evaluation moves us from category Set to category CPO, where our initial F-algebras and our final F-coalgebras turn out to be the same!" 11/06 05:26 is that what you were refering to abov? 11/06 05:26 Yes. 11/06 05:26 ok 11/06 05:27 All CPOs have a bottom element and limits of monotone sequences of elements. 11/06 05:28 In addition to the elements produced by the constructors along with those. 11/06 05:28 interesting 11/06 05:29 yeah, i remember this from my domain theory reading 11/06 05:30 So that gives your inductive types elements that match coinductive elements. 11/06 05:30 not sure what that means. "match"? 11/06 05:31 It gives you the 'inf = suc inf' element, for instance, which in Set would require coinduction. 11/06 05:31 Because it's the limit of _|_, suc _|_, suc (suc _|_), ... 11/06 05:32 right 11/06 05:32 ok 11/06 05:32 dolio: thanks for the insight 11/06 05:48 hi 11/06 05:50 what does 'unresolved meta' mean? 11/06 05:50 oh 11/06 05:51 I think I see 11/06 05:51 ok 11/06 05:53 so now my question becomes: 11/06 05:55 if I have four implicit arguments for a function, 11/06 05:55 and I need to give, at a certain invocation, the third one only (the others are inferrable) 11/06 05:56 then what's the syntax for it, apart from {_} {_} {foo} {_} ? 11/06 05:56 copumpkin: i finished porting 11/06 05:59 oh wow 11/06 05:59 massive effort! 11/06 05:59 what'd you do about duplication of none-irrelevant things? 11/06 05:59 massive effort = massive win 11/06 05:59 still duplicated, but made closer in interface to the stdlib versions 11/06 06:00 cool :) 11/06 06:00 amazing 11/06 06:00 _Cactus_: if you know the name of the third argument, you can write blah { name = foo } 11/06 06:01 and what happens if 'name' is also bound in the scope? 11/06 06:01 or is there no problem with htat? 11/06 06:01 copumpkin: should i push it? 11/06 06:02 e.g. can I do {foo = foo} if foo is also the name of the implicit argument? 11/06 06:02 _Cactus_: that's fine 11/06 06:02 great 11/06 06:02 thanks 11/06 06:02 xplat: sure! 11/06 06:03 what's the new module? 11/06 06:03 Categories.* 11/06 06:04 sounds good :) 11/06 06:04 is there a way to pass these implicit arguments without resorting to prefix notation? so that instead of having to write _op_ {foo = foo} x y is there something like (x op y){foo = foo}? 11/06 06:04 all the old support modules are now unused, but there are new ones under Categories.Support 11/06 06:04 (is there an #agda-newbies?:)) 11/06 06:04 _Cactus_: sadly nope, to both questions ;) 11/06 06:05 :) 11/06 06:05 the old ones are also under Categories.Support but only for reference 11/06 06:06 currently It Works For Me with the stdlib v0.5 11/06 06:07 hopefully nothing much breaks with darcs stdlib 11/06 06:07 cool :) 11/06 06:07 * copumpkin goes to sleep 11/06 06:11 will check i out tomorrow 11/06 06:11 :) 11/06 06:11 so, im curious, what are people doing for the lack of type classes in agda? 11/06 06:56 i saw the implicits post on the mailing list but afaik, that's not implemented yet 11/06 06:56 It's not like they're really needed for the majority of things. You get ad-hoc polymorphism by pattern matching on types in Agda. 11/06 06:58 You can't pattern match on types. 11/06 07:01 Erm. Yeah, bit of the wrong terminology there I guess. 11/06 07:02 is there a way to tell agda that my function is injective, and give its inverse, and then if I have something like forall {x} -> f x -> y then not have to pass {x}? 11/06 07:04 djahandarie: depends on what you're doing. i use typeclasses a lot in haskell. for example, Eq a 11/06 07:04 guerrilla: you can always just pass around records witnessing the instance 11/06 07:04 _Cactus_: yeah, i do that now. just curious if theres work for that to be able to be implicit 11/06 07:05 Okay, scratch that, not wrong terminology, just wrong. I swear I saw this somewhere but I guess it wasn't Agda. 11/06 07:14 whats the example you tried? 11/06 07:21 just curious 11/06 07:21 _Cactus_: cool syntax btw regarding the implicit arguments 11/06 07:22 maybe someday :) 11/06 07:22 guerrilla, I didn't try any code, I just tried looking it up and I couldn't find it. It was some formulation of type classes where you could group together types and write instances by just pattern matching on the type constructors in the function. 11/06 07:26 hmmm, actually, i see what you mean 11/06 07:27 lemi play with that for a sec and get back to you 11/06 07:28 I'm sure it doesn't work in Agda. 11/06 07:28 hmm 11/06 07:29 http://www.extremetech.com/article2/0,2845,2386710,00.asp 11/06 07:29 100 to 300GHz processors 11/06 07:29 sounds good for agda type checking! 11/06 07:30 uh wow 11/06 07:30 yeah, first thing came to mind, stdlib will compile fast 11/06 07:30 lol 11/06 07:30 :) 11/06 07:30 i wonder what the physical size is 11/06 07:31 guerrilla: did you know that the soviet microelectronics industry failed only because the end products couldn't fit through the factory gate? 11/06 07:35 i am skeptical, but i could see that 11/06 07:37 (this was my lame attempt at a joke) 11/06 07:37 *wooosh* 11/06 07:37 djahandarie: yeh, i give up. :P did you find the reference you were looking for? 11/06 07:49 guerrilla: maybe djahandarie was referring to universes, like in The Power of Pi, iirc 11/06 13:29 guerrilla: and i thought the new implicits were implemented in the darcs version of agda 11/06 13:30 xplat: I was thinking if you renamed ⟨_⟩,⟨_⟩ to _⟩,⟨_ it would look like it fits in better with the equational reasoning stuff 11/06 14:29 Saizan: ah, i havet checked out darcs lately, thanks for letting me know 11/06 15:11 Saizan: and thanks for the ref on the other, looking at it now 11/06 15:11 --- Day changed Sun Jun 12 2011 asking this question here given the caliber of the people hanging out here: is there a hash algorithm without collisions?, without a complicated algorithm, something that can be done in assembly? 12/06 00:15 i have 1500 bytes available to index data in 100K bytes and I am doing this in assembly. 12/06 00:17 You can't have a hash algorithm without collisions unless you know something about the space you're hashing from. 12/06 00:18 just curious, if there might be some smart way of doing that, without having to reload the pages? 12/06 00:18 Specifically, that it's smaller than the hash space. 12/06 00:18 dolio, I know everything about the space available. 12/06 00:18 dolio: oh, ok. 12/06 00:18 is hash the best way to do this? 12/06 00:19 i currently have a linked list that I match against. 12/06 00:19 but, that is not scalable and provides very limited indexing capabilities. 12/06 00:20 i thought of huffman encoding, but it is not that simple in asm. 12/06 00:20 what about the SHA-1 algorithm that git uses? is it a complicated algorithm? 12/06 00:20 not to go into extreme specifics, but there is no hash function that will hash a fixed number of keys with no collisions regardless of what the keys are 12/06 00:21 No idea. I've not looked much at hash algorithms. 12/06 00:21 i have a list of patterns that I search with, and the pattern that matches, I lookup the value that it contains and send that value over. 12/06 00:21 if you want zero collisions, you have to adapt the hash function to the data set, because any fixed hash function has data sets it doesn't get along with 12/06 00:22 i have the patterns currently as a linked list, but, it just seems inefficent 12/06 00:22 I just know that it's mathematically impossible to hash a set of N values into a set of M values where N > M without collisions. 12/06 00:22 and, there is a limitation of how many patterns I can store in 1500 bytes.. 12/06 00:22 if the hash space is really large (like sha-1's) then you can make it statistically pretty likely that you will have zero collisions with the fixed function, but then you can't use the hash value as an index directly anyway and when you fold it down to the size of your table you get collisions again 12/06 00:24 dolio, not with my infinite compression algorithm!!! 12/06 00:24 i have 1500 bytes of ram space and 100K bytes of eeprom space, that I do not want to hit (unless required). Any suggestions that you can think of? 12/06 00:25 i want to keep the patterns in the ram space and take the number of the pattern that matched as an array index to the lookup-value. 12/06 00:26 is that a good idea? 12/06 00:27 1500 bytes is not much ram for search patterns, but i guess if there's nothing else you're doing with it ... 12/06 00:28 1500 bytes is exclusively reserved for the search patterns, I mean. 12/06 00:28 what kind of search are you doing? 12/06 00:29 because a lot of data structures REALLY won't work for some kinds of searches 12/06 00:30 just a simple list of 8(or 10) possible alternatives strung together one after the other. 12/06 00:30 that tells me nothing 12/06 00:30 and I have the length of each such pattern list 12/06 00:30 i don't know what kind of pattern, what they're being matched against, or anything 12/06 00:31 i could have a sample pattern of : a,b,c,a,b 12/06 00:32 xplat: i am talking about simple stuff 12/06 00:32 maybe, but i would still have to be psychic to know what it is 12/06 00:33 and I match it against a search space that could contain, a,b,c,d ; a,a,c: a,d,c,e : 12/06 00:33 and when I find the pattern that is a,b,c,a,b, then bingo, I have my match. 12/06 00:34 nothing serious, it is a very simple search on an 8-bit mcu 12/06 00:34 xplat: does that make sense? 12/06 00:34 and, distinct elements can be 8 or 10 (I know exactly how many, beforehand) 12/06 00:35 what are the ; and :?  is the 'search space' what you are keeping in the linked list, or is the 'sample pattern'? 12/06 00:36 and I will be writing out the patterns that it will be matching against, so, order of the patterns is in my control. 12/06 00:36 i used the : to denote the next pattern 12/06 00:36 sorry, the ; = : 12/06 00:36 typo 12/06 00:36 is it an exact string match, prefix match or substring match? 12/06 00:36 exact string match 12/06 00:36 do you expect most inputs to be matches or non-matches? 12/06 00:37 most matches 12/06 00:37 very rarely, non-matches. 12/06 00:37 very very rarely. I should say. 12/06 00:37 how many inputs come in per second? 12/06 00:38 < 1, dozens, thousands, or millions and up? 12/06 00:38 xplat, maybe one pattern or < 3-4 such pattern sets 12/06 00:39 when I say a pattern set, I mean around 10'ish patterns 12/06 00:39 so, yes, dozens such patterns would be too much. 12/06 00:39 and how many inputs do you usually match before the pattern set changes? 12/06 00:39 xplat, all? 12/06 00:39 i wait for the pattern set to form, and then start the match 12/06 00:40 to form?! 12/06 00:40 i am not matching while processing is going on (ie., the pattern set is forming). I wait until the pattern set is complete, and then I start working on it. 12/06 00:40 i mean, an example pattern set is : a,b,c,d,a. 12/06 00:41 and then followed by a delimiter. 12/06 00:41 I wait to get the delimiter and then start the match. 12/06 00:41 i do not know if that is a good idea, but, it is(seemed) simpler than the alternative 12/06 00:42 i feel like we don't share enough vocabulary to have this conversation 12/06 00:42 should I query you? do you have a few minutes? 12/06 00:42 okay, wait, let's establish words to use 12/06 00:43 an 'input' is a string, followed by a delimeter 12/06 00:44 yes, 12/06 00:44 and, also has a length 12/06 00:44 delimiter and length are redundant, but I have both. 12/06 00:44 a 'key' is a string that you want to notice if it occurs as an input 12/06 00:45 a 'key space' is a list of keys 12/06 00:45 to be treated as alternatives 12/06 00:46 hold on, input = 3,a,b,c . My search patterns are as: 3.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f 12/06 00:46 an so on. 12/06 00:46 okay, so how often do new inputs come in? 12/06 00:47 an input such as 3,a.b,c comes in a few times per second. 12/06 00:47 and how many inputs do you match against a key space before the key space changes? 12/06 00:48 what is the key space? 12/06 00:48 the 3.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f 12/06 00:48 ? 12/06 00:48 3,a,b,c,4,a,b,c,d,6,a,b,c,d,e,f 12/06 00:49 it does not change, it is a static space 12/06 00:49 there is only one, and it never changes, and is used to match every input? 12/06 00:49 over the lifetime of the device? 12/06 00:50 yes 12/06 00:50 and contains only 8-10 alternatives 12/06 00:50 ? 12/06 00:51 3.a,b,c,4,a,b,c,d,6,a,b,c,d,e,f,10,a,a,b,c,d,e,f,g,a,b 12/06 00:51 the a b or c alternatives can be 8-10 12/06 00:51 which is known in advance. 12/06 00:51 so, the number of alternatives does not change 12/06 00:51 neither, does the space that I search in. 12/06 00:52 does that make sense? 12/06 00:52 when you say 'alternatives', you mean 'a' or 'b' or 'c'? 12/06 00:52 yes 12/06 00:52 instead of 'number of alternatives', one would say 'size of the alphabet' 12/06 00:52 and the 3.a,b,c or 4,a,b,c,d, is what I call Pattern 12/06 00:52 yes, the size of the alphabet is perfect 12/06 00:52 that is 8-10 12/06 00:53 okay, but how many patterns/keys are in the key space? 12/06 00:53 do not know, yet. i need to figure out how much is possible, given the algorithm. 12/06 00:54 well, how many would you expect to be useful?  dozens? hundreds? 12/06 00:54 hundreds 12/06 00:54 atleat 12/06 00:54 atleast 12/06 00:55 well, obviously you will want to store them in eeprom 12/06 00:55 could be around thousands too. 12/06 00:55 but, not more than a few thousands. 12/06 00:55 since they never change you can prepare them offline on a larger computer 12/06 00:55 yes, I have to store in eeprom, but they do not take more than a few bytes each. 12/06 00:56 yes, I can prepare them as I want it in an offline computer 12/06 00:56 regarding the format or the content 12/06 00:56 or the ordering 12/06 00:56 and how much of the mcu's time can you devote to looking them up? 12/06 00:56 100%?  10%?  1%? 12/06 00:57 quicker the better? I am trying to minimise the eeprom lookups for searching 12/06 00:57 if that is possible. 12/06 00:57 preload the ram, lookup the eeprom only when a match is found 12/06 00:57 is ideal. 12/06 00:57 but, that gives me 1500 bytes to store my patterns into, which is not much. 12/06 00:58 hence, wondering if there are better ideas? 12/06 00:58 i think there is quite some idle cpu cycles available, so, some processing for hash might be possibel. 12/06 00:59 s/el/le/ 12/06 00:59 if you absolutely want to minimize eeprom queries, and you almost always match, you should use a perfect hashing tool 12/06 00:59 yes, that seems to be the best idea. 12/06 01:00 i would not be wasting the bytes storing the patterns.. 12/06 01:00 and the ram usage would be the utmost. 12/06 01:01 yes, you can store the patterns only in eeprom, and still only query at most one from eeprom to match 12/06 01:01 on collisions? 12/06 01:01 or, to doublecheck the match? 12/06 01:01 doublecheck 12/06 01:01 the perfect hash tool will choose a hash function that does not collide for your fixed set of keys 12/06 01:02 smart thinking.. thanks. 12/06 01:02 instead of assigning sequential numbers to the alphabet, I was thinking if there is a smarter way of doing it. 12/06 01:03 if that helps the hasking function 12/06 01:04 i am generating the inputs too, so, I could assign the alphabet any byte value (could be 1,2,3,4.. or 1,2,4..) 12/06 01:05 i think some hash function families will do that themselves.  it depends what tool you use to generate the perfect hash. 12/06 01:06 i have to code the hashing function in assembly 12/06 01:06 for that mcu. 12/06 01:07 any suggestions on the hash function, please? or where i can find something that can help me out. 12/06 01:07 yes, you probably want a perfect hashing tool with source code so you can see what kind of hash functions it generates and write assembly to do those sorts of hashes 12/06 01:07 on the other hand, if you go with commercial tools you might be able to find one that already generates assembly for your mcu 12/06 01:08 that would be the most convenient, it depends on your budget 12/06 01:09 anything opensource? 12/06 01:09 that you can think of? 12/06 01:09 gphash is opensource and the hash functions it generates are simple 12/06 01:10 not sure if the license is okay for your project though 12/06 01:10 ok, thanks a lot. I will check it out. 12/06 01:10 xplat:  what about bloom filters? would they help, in this scenario? 12/06 01:18 found this: uri: http://www.partow.net/programming/hashfunctions/ 12/06 01:19 joe6: bloom filters would not help.  they only tell whether you match, and you expect to almost always match. 12/06 01:21 so you would always do extra work, and hardly ever save any 12/06 01:21 the size of the alphabet is 8-10 12/06 01:22 xplat: what do you think of a trie  instead of a hashing function? 12/06 01:44 joe6: it would be easier, but probably take more (eeprom) memory and make more eeprom queries 12/06 01:47 ok, thanks. 12/06 01:47 the best way to limit eeprom queries for a trie is probably to put the 'top' of the trie in ram, or even a selection of nodes weighted by how often you expect them to be visited 12/06 01:48 i am not able to find much from google about gpHash other than that it is used by EPOS. do you have a link or something that you can share with me? 12/06 01:48 hm, sorry, i got the name wrong :( 12/06 01:49 xplat, so, would you recommend a trie over a hash? 12/06 01:49 http://www.gnu.org/software/gperf/ 12/06 01:49 xplat, that is perfect. Thanks. 12/06 01:49 well, a trie is easier to create, but it's harder to keep small or to adapt to a nonuniform memory speed like you need 12/06 01:51 so it depends on your relative tolerance for different kinds of risks 12/06 01:52 with a trie it's more likely that you'll get it working but not scaling as well as you want, with a hash it's more likely that you won't get it working at all but if it works at all it will scale well 12/06 01:53 let me try the hashing function, I have used hashing functions before, whereas a trie is new territory for me. 12/06 01:54 since you already have a working-but-slow implementation that reduces the advantage of a trie anyway 12/06 01:54 but, a bitwise trie is supposedly very helpful with caching (from wikipedia). 12/06 01:54 an 8-bit mcu won't do that kind of caching, and it's hard to tune your own trie implementation to cache well anyway 12/06 01:55 oh, ok. 12/06 01:56 thanks a lot. 12/06 01:56 xplat, just from reading the introduction of gperf, I gather that the C code changes based on the given list of strings. I need to translate the C to Asm. Just curious, is the C code generated vastly different each time or is it approximately the same? 12/06 02:02 it would just be too much work to translate the C code to Asm, every time the list of string tables change. 12/06 02:02 if it does not change that much, then I could just use a simple to C -> Asm template that can be reused.. 12/06 02:03 joe6: the C code is generated from a template, it doesn't do anything vastly different 12/06 02:04 well, i think there can be big changes depending on a few of the command line switches, but not for most switches or depending on the keys 12/06 02:05 xplat, ok, thanks a lot. looks like it is the way to go. the more I read about it, the more it seems to fit. 12/06 02:05 yes, I will probably stick with the same switches. but, am more worried about the differences due to change in inputlist.. 12/06 02:06 xplat, thanks for your excellent suggestion and guidance. 12/06 02:06 joe6: I'd suggest trying to do stuff in C first. 12/06 02:43 At least compare the size of what you get from C and from hand-written asm. 12/06 02:43 The compiler could be able optimize for code size, so with proper options the machine might just be able to beat you at that :) 12/06 02:45 Eduard_Munteanu, ok, thanks. 12/06 12:24 What is the syntax of "{! !}" in vec : {n : Nat}{A : Set} -> A -> Vec A n 12/06 17:38 vec {n} x = {! !} 12/06 17:38 It looks like it's listed as a solution to the first exercise, but agda can't even parse that: "Unsolved metas at the following locations:" 12/06 17:40 this is a guess but agda --allow-unsolved-metas 12/06 17:50 not sure if that's what it's for though 12/06 17:51 is {! !} suppose to work like Haskell's "undefined :: a"? 12/06 17:57 or it's more? 12/06 17:58 Ah.  That would make sense in this context (so that I can write a definition myself for the exercises in the tutoria). 12/06 18:03 But how is it like Haskell's undefined?  Is that special-case syntax? 12/06 18:03 i just use undefined a lot for a stub to see that the rest of my code compiles 12/06 18:06 {! ! 12/06 18:27 {! !} is what agda-mode inserts in place of a ? when you load the file, btw 12/06 18:27 it's called a "hole" or a "shed", agda-mode has a few nice commands to interactively fill it 12/06 18:28 ok 12/06 18:37 i don't use agda-mode since i don't use emacs.. so yeah 12/06 18:39 Saizan: So it is special-case syntax? 12/06 19:07 yep 12/06 19:07 well, i'm not even sure if i'd consider it part of the language itself 12/06 19:07 sshc: you've never used "?" before? 12/06 19:08 I'm following the tutorial, and I don't think it's ever been mentioned 12/06 19:09 Many of Agda's interactive features are pretty much inaccessible to me, since I use vim 12/06 19:09 shachaf: ditto 12/06 19:11 oops i meant sshc 12/06 19:11 i strongly recommend using emacs for agda, it really helps to be able to inspect the types and context of these holes while you develop 12/06 19:11 Saizan: ah, you know me, do everything the hard way ;) 12/06 19:12 but, in reality, i just can't use emacs.. 15 years of vi... hard habit to break, would really have to fight to use emacs 12/06 19:13 What about viper? 12/06 19:14 dolio: ohhhh yes, thank you for reminding me. i remember reading about it a long time ago, i forgot to try it out 12/06 19:16 bookmarking and installing now so i dont forget again 12/06 19:16 I'm sure it's not perfect, but it's probably worth it for what agda mode gets you. 12/06 19:20 "I used to think that emacs was a great OS but lacked a decent editor, but then I found out that it could run vim." 12/06 19:23 hahaha 12/06 19:24 guerrilla: Agreed. 12/06 22:33 Oops, I meant goomba. 12/06 22:33 both gorillas and goombas have been marios enemy 12/06 22:38 What's the difference between "∀ {x xs}" and "∀ x {xs}"? 12/06 23:33 What does the latter expand to? 12/06 23:33 In the first one, both arguments are implicit. 12/06 23:35 In the second, only the second is. 12/06 23:35 Thanks 12/06 23:36 --- Day changed Mon Jun 13 2011 hello everybody 13/06 01:41 shachaf: guerrillas and gorillas are not related.. well I guess, at times, both operate in jungles :P 13/06 02:49 damnit, i meant augur. how did i screw that one up :) 13/06 02:50 ymasory: I believe you may be correct. 13/06 02:53 sshc: moi? 13/06 02:54 ymasory: i think its part of the runnin joke here of addressing the worng person 13/06 02:59 guerrilla: bye bye #agda 13/06 02:59 whoa hey hello 13/06 03:12 guerrilla: thats not the point! 13/06 03:12 ok :) 13/06 03:34 hmm 13/06 11:41 im going to be teaching a friend how to program 13/06 11:41 should i teach him in haskell or agda? 13/06 11:41 or scheme? 13/06 11:42 im most comfortable with scheme, but haskell has a good mix of theoretical import and practical value 13/06 11:42 agda is pretty theory oriented, which is a real plus, but if he ever wants to actually write a program.. 13/06 11:42 augur: i'd say haskell or scheme, depending on exactly how much more comfortable you are with the latter than the former 13/06 12:29 im fine with both, i just havent taught with haskell before 13/06 12:30 I'd go for Haskell. But I'm biased and believe that programming without (static) types is a dead end. 13/06 12:30 and a lot of the SICP type stuff will be pointless to translate over, since a lot of SICP revolves around roll-your-own ADTs 13/06 12:30 i suppose this allows me the opportunity to talk about some more mathematical stuff tho 13/06 12:31 someone actually started a haskell translation of SICP 13/06 12:40 i don't know how far along it is 13/06 12:41 oh? 13/06 12:47 xglat, how are you doing? 13/06 18:06 xplat, just wanted to let you know that your suggestion to use gperf has proven to be a godsend. 13/06 18:20 joe6: cool, i'm glad it worked out 13/06 18:21 xplat, thanks again for taking the time to understand my problem and for helping me out. 13/06 18:24 We haven't seen xglat for days. I suspect he's been killed by xplat. 13/06 18:30 djahandarie: yes, typo.. sorry about that. 13/06 18:33 the agda mailing list has been pretty busy these few days.. 13/06 18:33 xplat: wanna put categories on the agda org on github? 13/06 20:28 I sent something to the mailing list to that effect, too 13/06 20:35 copumpkin: I'm still learning Agda, and I have a few questions about your library if you don't mind taking the time to answer them: in "record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where", does "(o ℓ e : Level)" expand to "(o : Level) (ℓ : Level) (e : Level)"? 13/06 20:45 sshc: yep 13/06 20:46 "    Obj : Set o 13/06 20:46 ^ Why is "Set" being applied with a parameter? 13/06 20:46 Shouldn't that be of the form "Cons : Set"? 13/06 20:49 wargle 13/06 20:49 moin copumpkin 13/06 20:49 yo 13/06 20:49 sshc: that's universe polymorphism at work 13/06 20:49 Set o is "set at universe level o" 13/06 20:49 sshc: Set0, Set1, etc are the same as Set zero, Set (suc zero), etc. 13/06 20:54 just don't ask what the type of Set (as a function) is 13/06 20:54 Interesting.  This only applies specially to "Set", right? 13/06 20:55 he made it so this function works at various levels... 13/06 20:55 sshc: yeah 13/06 20:55 Set on its own is just Set0 13/06 20:55 it's kind of wonky 13/06 20:55 copumpkin: ⊔ is max, right? and doing it this is gives you the same results as cumulativity, right? 13/06 20:56 Mm.  Thanks. 13/06 20:56 Ah, good, there's this: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.UniversePolymorphism 13/06 20:56 guerrilla: it's typically called lub 13/06 20:56 but yeah, basically 13/06 20:56 least upper bound, ok, cool 13/06 20:56 not same results as cumulativity 13/06 20:56 oh ok 13/06 20:56 it just lets me get into the right universe 13/06 20:57 yeah 13/06 20:57 or, 13/06 20:57 Was this mentioned in the tutorial? 13/06 20:57 nope 13/06 20:58 I don't recall seeing it 13/06 20:58 it was added after the tutorial was written 13/06 20:58 'k. 13/06 20:58 without cumulativity, every type is in a specific universe 13/06 21:03 lub helps you figure out which is the right universe for a composite, universe-polymorphic type 13/06 21:03 one thing I had trouble with, for example 13/06 21:03 even with cumulativity, though, you would still need something like lub so you could find the smallest universe your type exists in 13/06 21:04 maybe I was just dumb back when I tried this 13/06 21:04 write a function that generates N-ary functions of (A : Set a) inputs and (B : Set b) output 13/06 21:04 N-ary : {a b : Level} -> Nat -> Set a -> Set b -> Set (suc (a \lub b)) 13/06 21:05 of course, now there's example code for n-ary stuff in the library 13/06 21:05 oh, I see what I was doing wrong 13/06 21:06 he has a helper function 13/06 21:06 for determining the level of the output 13/06 21:06 so clever 13/06 21:06 copumpkin-- 13/06 21:06 isn't the type of Set as a function Set : (l : Level) -> Set (suc l) ? 13/06 21:08 this is a valid type, although it's not about to pass the termination checker, or maybe even the scope checker 13/06 21:08 "_»_ : {n : Nat} -> Vec Set n -> Set -> Set 13/06 21:10 []        » tt = tt 13/06 21:10 (t :: ts) » tt = t -> (ts » tt) 13/06 21:10 xplat: yeah, you're right 13/06 21:10 " What's wrong with the type here? 13/06 21:10 xplat: now, what's the type of that? 13/06 21:10 "Set₁ != Set" 13/06 21:11 sshc: your types don't fit 13/06 21:12 make the return type Set1 13/06 21:12 or Set\_1 13/06 21:12 ^ This is my attempt at translating the pseudo-Haskell code on page 3 of "Faking dependently-typed programming" to Agda 13/06 21:12 s/programming"/programming in Haskell"/ 13/06 21:12 it's almost correct, it just doesn't quite fit :) 13/06 21:13 copumpkin: I don't understand.  "_»_ : {n : Nat} -> Vec Set n -> Set -> Set1" reults in the same error 13/06 21:13 sshc: maybe the problem is that tt is the constructor for the unit type 13/06 21:14 copumpkin: X Y : Set gives you X -> Y : Set 13/06 21:14 so the return type should be a set 13/06 21:14 Set should be fine as the result type 13/06 21:14 yeah, you're right 13/06 21:16 Saizan: Thta doesn't seem to be the problem 13/06 21:16 it typechecks fine here 13/06 21:16 oh, I know what the problem is 13/06 21:16 your Vec isn't universe-polymorphic 13/06 21:16 so it can't contain Set 13/06 21:16 back in the bad old days, we'd use Data.Vec1 13/06 21:17 or something like that iirc 13/06 21:17 228 data Vec (a : Set) : Nat -> Set where 13/06 21:17 229     []   : Vec a zero 13/06 21:17 230     _::_ : {n : Nat} -> a -> Vec a n -> Vec a (succ n) 13/06 21:17 yeah 13/06 21:17 passing Set to Vec doesn't work, cause Set : Set1 13/06 21:17 How can I define "Vec" universally polymorphically? 13/06 21:18 data Vec {woof} (a : Set woof) : Nat -> Set where 13/06 21:19 make sure you have {-# OPTIONS --universe-polymorphism #-} at the top 13/06 21:19 and have imported Level 13/06 21:19 {-# WAVEOFFERINGS --rubber-chicken #-} 13/06 21:21 That pragma seems.. non-standard-y unportable-ish, like {-# OPTIONS_GHC broda #-3 13/06 21:21 there's only one agda implementation anyway :) 13/06 21:21 sshc: Agda isn't standardized, so no problem :) 13/06 21:22 agda2019 13/06 21:23 "{woof}" looks odd.  Are you sure that shouldn't be "{woof : Nat}"? 13/06 21:23 {woof : Level} if anything 13/06 21:23 Import level?  I can't use my own definition of "Nat"? 13/06 21:23 (Level is Nat, right?) 13/06 21:23 it's not the same thing 13/06 21:23 it looks just like Nat :) 13/06 21:23 but I don't think you're allowed to use Nat there 13/06 21:24 but the Level is not needed because the only possible argument to Set is a Level 13/06 21:24 % grep -nri "data.*level" . -A9 13/06 21:24 ./Support.agda:7:data Level : Set where 13/06 21:24 ./Support.agda-8-  zero : Level 13/06 21:24 ./Support.agda-9-  suc  : (i : Level) → Level 13/06 21:24 The htree BUILTIN pragmas below seem relevant 13/06 21:25 they are 13/06 21:25 that's what allows you to feed Level arguments to Set 13/06 21:25 If I use "{woof}" (is that ever allowed?), can the Level type be implied with implying it? 13/06 21:26 and they also allow the typechecker to treat Level constraints specially 13/06 21:26 * sshc doesn't like "suc", because "succ" is consistent in its length and is named just like Haskell's "succ" 13/06 21:26 you can call zero and suc for levels whatever you want as long as you use the right pragmas 13/06 21:27 s/with implying it/without defining it/, I mean. 13/06 21:27 xplat: thanks for that explanation, sorry I was afk for a momenet. 13/06 21:27 zero and suc, zero and succ, level-zero and level-succ, ground and upstairs 13/06 21:27 sshc: yeah, you can leave out the type and ask it to infer them 13/06 21:27 usually you need a forall in front of it 13/06 21:28 but not on data declarations 13/06 21:28 or module declarations 13/06 21:28 xplat: yeah, in cumulativity usually there is a relation defined axiomatically usually represented by \preceq 13/06 21:28 copumpkin: Okay.  Now can I do that without actually defining Level? 13/06 21:28 no 13/06 21:28 when it sees something get passed to Set 13/06 21:28 it goes and looks for what's attached to the builtin level 13/06 21:28 copumpkin: actually, yes, you can do that without defining Level 13/06 21:28 really? 13/06 21:29 weird :o 13/06 21:29 but then you can't really refer to it much 13/06 21:29 what's the type of the data type then? 13/06 21:29 copumpkin: it seems to work on Don't Ask, Don't Tell 13/06 21:29 lol 13/06 21:29 sound principles! 13/06 21:29 sshc/copumpkin.. cool trick for n-ary functions, very clever 13/06 21:30 i think what happens actually is that the builtin Level type already exists 13/06 21:31 it just doesn't have a name for itself or its constructors and such 13/06 21:32 It's defined in the standard library 13/06 21:32 In Data.Level or something 13/06 21:32 just Level 13/06 21:32 Yeah, just Level 13/06 21:32 djahandarie: see my /msg btw? 13/06 21:32 the pragmas tell the compiler to instantiate the type and associated constructors and functions from an isomorphic type to the preexisting Level stuff 13/06 21:33 explains our confusion the other day 13/06 21:33 so without it, Level basically acts like a type that's been defined out of scope 13/06 21:33 interesting 13/06 21:33 guerrilla, didn't get it for some reason 13/06 21:34 copumpkin: categories takes hours to build for me, by the way 13/06 21:34 djahandarie: ok, just a moment 13/06 21:34 sshc: you typechecking the Everything.agda? 13/06 21:34 copumpkin: Yes 13/06 21:34 it's pretty heavy to typecheck some of the modules :) 13/06 21:34 especially the Monoidal stuff, but it's a lot better than it used to be 13/06 21:34 have you pulled recently? xplat fixed it to use way less memory 13/06 21:35 it helps in that case to interrupt it after the first hour, reload agda (C-c C-x C-r) and start it checking again 13/06 21:35 I think the modules in which Power sets (I think; might be something similar) are defined take a long time 13/06 21:35 I also started moving away from nested sigmas for some things like slice and arrow categories 13/06 21:35 there are still a couple of places I use them though 13/06 21:35 xplat: do you know why? 13/06 21:36 guerrilla: not really, a long build uses more memory than a series of smaller builds but i have no idea why that is the case 13/06 21:38 xplat: maybe we could add in a re-start on a timer.. just as a temporary hack 13/06 21:39 sshc: Category.Power.NaturalTransformations takes a long time 13/06 21:39 xplat: That was one, yes 13/06 21:39 although not as long as a few other things 13/06 21:39 I wonder why this is wrong 13/06 21:40 240 data Vec {universe : Nat} (a : Set universe) : Nat -> Set where 13/06 21:40 241     []   : Vec a zero 13/06 21:40 242     _::_ : {n : Nat} -> a -> Vec a n -> Vec a (succ n) 13/06 21:40 if Category.Power takes a long time then either your agda is slowing down or you really don't have enough memory for this 13/06 21:40 the simplest explanation is that it doesn't "garbage collect" unneeded modules 13/06 21:40 AgdaBasics.agda:242,5-55 13/06 21:40 The type of the constructor does not fit in the sort of the 13/06 21:40 datatype, since Set universe is not less or equal than Set 13/06 21:40 when checking the constructor _::_ in the declaration of Vec 13/06 21:40 xplat: That one was slow too 13/06 21:40 sshc: it needs to be  data Vec {universe : Nat} (a : Set universe) : Nat -> Set universe where 13/06 21:41 copumpkin: btw, for \<_\>,\<_\> , i don't think it would be improved by losing the outer brackets 13/06 21:41 Ah, thaks 13/06 21:41 sshc: you want universe : Level 13/06 21:42 guerrilla: I defined my own Level type 13/06 21:42 you can't do that 13/06 21:42 guerrilla: yes you can 13/06 21:42 xplat: what? 13/06 21:42 serious? 13/06 21:42 as long as you have the right pragmas 13/06 21:42 230 {-# BUILTIN LEVEL     Nat  #-} 13/06 21:42 231 {-# BUILTIN LEVELZERO zero #-} 13/06 21:42 232 {-# BUILTIN LEVELSUC  succ #-} 13/06 21:42 oh oh ok 13/06 21:42 sorry, i didnt catch that part 13/06 21:43 i thought you meant just a Nat data. 13/06 21:43 the reason they are usually separate from Nat, though, is that Nat usually is given its own pragmas that let it be represented efficiently as an Integer in the underlying runtime 13/06 21:43 I see 13/06 21:44 But Levels don't need to be efficient because there's no way someone would use like 15 of them right? 13/06 21:44 if you try to use the same type as Nat and Level your arithmetic will be hurtin' 13/06 21:44 Saizan: Polymorphisizationizing Vec seems to make some definition that use it with forall not work ("unsolved metas") 13/06 21:44 djahandarie: well, it's more like Levels are optimized to be efficient at different things 13/06 21:44 xplat: next question.. how are Levels not metatheoretic? 13/06 21:45 sshc, conjugation fail? 13/06 21:45 special constraint solver for constraints built with suc and \lub 13/06 21:45 sshc: that's probably because the universe level can't be deduced from the context 13/06 21:45 guerrilla: ? 13/06 21:46 xplat: wel, how can a Set depend on something of type Set? 13/06 21:46 djahandarie: I'd says so. 13/06 21:46 guerrilla: a Level is basically just a name for a universe.  unary Set turns the name into a real universe. 13/06 21:47 or rather, it finds the actual universe that you asked for by name 13/06 21:48 hmm ok, im used to seeing Level defined as a natural number in the axioms of the underlying type theory 13/06 21:48 yes, the latter makes sense 13/06 21:48 maybe i'll have to look at the source code. was there a paper on how this was done? 13/06 21:49 pushing metatheoretic notions down into the object language is quite trendy in type theory, anyway 13/06 21:49 * augur levitates 13/06 21:51 Saizan: i've seen quite a bit of that internalising lately too 13/06 21:51 i havent finished the reading about that, but im not 100% convinced it doesnt lead to inconsistency at some point 13/06 21:51 what, noone got that reference? 13/06 21:51 augur: ah, thats the paper, eh? 13/06 21:52 in which a full algebraic type system is implemented by pushing it down into just core types in the underlying language 13/06 21:53 i dont know if they have a way of distinguishing isomorphic types tho 13/06 21:54 er.. super-isomorphic types! 13/06 21:54 not only are the sets isomorphic, but there are isomorphisms for the elements too 13/06 21:54 F X = 1 + A*X   vs   G X = 1 + A*X 13/06 21:55 this is ofcourse possible in haskell, agda, etc. 13/06 21:55 where F != G 13/06 21:55 but if you levitate, F = G trivially 13/06 21:55 hmm augur , its "The Gentle Art of Levitation", right? abstract seems to fit 13/06 22:00 but brb, must eat or will die 13/06 22:00 yes 13/06 22:00 augur: looks promising, but no mention of the word "consistent" 13/06 22:38 (didn't start reading, just searched) 13/06 22:38 guerrilla: its as consistent as the underlying logic i think 13/06 22:43 augur: ok, interesting. i'm still skeptical though, which won't change until i muster the energry to tackle this :) 13/06 22:45 these internalisations are not easy for me to wrap my head around 13/06 22:46 i do beleive in internalisation, it has to be the future. i just want a proof that it works. 13/06 22:46 --- Day changed Tue Jun 14 2011 xplat: I wrote a couple of diagonal functors 14/06 06:24 and also started writing functors for "partially applied" products, both ways 14/06 06:29 wasn't sure what to call those though 14/06 06:29 what's this 14/06 08:32 This is AGDAAA! 14/06 08:34 ok good 14/06 08:34 what's agdaaa? 14/06 08:34 Johndk: see the topic, /topic 14/06 08:35 lol so you understand this shit? 14/06 08:36 Put shortly, it's a dependently-typed language / theorem prover with syntax partly inspired by Haskell. 14/06 08:36 ah 14/06 08:37 science 14/06 08:37 Johndk: I'm curious, how did you get here? 14/06 08:38 picked a room randomly 14/06 08:38 :) 14/06 08:38 ahaha 14/06 09:34 johndk has a nice way of exploring irc 14/06 09:34 weird.  i thought i had already pushed my stdlib port of categories, but i don't see evidence of it on github ... 14/06 12:08 huh. ccshan follows copumpking on twitter 14/06 12:25 crazy 14/06 12:25 wow 14/06 12:27 he also follows travis 14/06 12:27 wtf 14/06 12:27 and jimmy lin 14/06 12:27 maybe hes a strong reciprocalist 14/06 12:28 copumpkin: okay, NOW my port stuff is pushed.  it was a branch but i mistakenly only pushed master before 14/06 14:24 cool :) 14/06 14:24 was wondering actually 14/06 14:24 have any ideas where to put those product functors? 14/06 14:24 you should have said something!  :7 14/06 14:25 maybe Categor{y,ies}.Functor.Product? 14/06 14:25 hmm, that's better than Categories.Object.BinaryProducts.Functors 14/06 14:26 :P 14/06 14:26 also 14/06 14:27 I think we should start bundling up categories with properties they have in a consistent manner, at some point 14/06 14:27 not sure if you've looked at the stdlib 14/06 14:28 but the distinction between Monoid and IsMonoid 14/06 14:28 i haven't looked much at that *part* of the stdlib 14/06 14:29 :) 14/06 14:29 well, I found myself wanting "a category with all binary products" 14/06 14:29 and had to pass the binary products bit separately from the category 14/06 14:29 the article i read on representing categories with type classes in coq was really down on that kind of bundling 14/06 14:31 oh yeah? 14/06 14:31 hmm 14/06 14:31 maybe not then 14/06 14:31 because bundles like that are hard to combine with proper sharing 14/06 14:31 but then the functors take a crapload o' arguments 14/06 14:31 then I need to pass them a category, the binary products proofs, and an object 14/06 14:32 ah I see 14/06 14:32 hmm 14/06 14:33 it's the same reason you normally pass a Level, a Set, and a value in that set instead of combining some of them with a sigma 14/06 14:34 (or rather, the reason you have Sets parameterized by a level instead of a level predicate on sets) 14/06 14:35 hmm, okay 14/06 14:35 oh, the <_>,<_> 14/06 14:36 the idea i had in my head is 'justifications are inside angle brackets, congruences are represented by the same operator as their underlying function, but partly stuck to the outsides of angle brackets' 14/06 14:37 cool, that sounds reasonable 14/06 14:38 I was wondering if it was worth doing two halves of that one too 14/06 14:38 like I have the \o-resp-\==\^l and \^r 14/06 14:38 that would just pass refl to the other one 14/06 14:38 this can't possibly work for every mixfix operator because of how the nesting works, but it can work for infix and it can work for infix surrounded by angle brackets 14/06 14:38 for <_>,<_> both of the angle brackets 'belong' to the justifications, while the extra angle brackets from the surroundings become the ones from <_,_> 14/06 14:40 whereas for _>o<_ , the angle brackets on the >o< match with the surrounding ones 14/06 14:41 (of course as soon as you need parentheses to decide operator precedence the whole thing explodes, unfortunately) 14/06 14:41 oh also 14/06 14:42 what should we call the programming-y CT library that will be built on top of all this? 14/06 14:42 if you mean what i think you mean, maybe we should use Notion or Idiom or get all traditional and use Control 14/06 14:43 control kind of bothers me, but the other two sound nice 14/06 14:44 (Notion seems to be the academically correct word, per papers like Parameterized Notions of Computation) 14/06 14:44 I was wondering how we might represent CPO\_\bot 14/06 14:45 or some usable category where initial algebras and terminal coalgebras coincide 14/06 14:45 hm, yes 14/06 14:46 otherwise a huge wealth of esoteric *morphisms will be lost to us 14/06 14:46 i was thinking about that too, because i want to do proofs about Haskell, but i haven't got very far yet 14/06 14:46 I mean, we could perpetuate the Hask myth 14/06 14:47 but then people will wonder why we're missing all the combined fold/unfold thingies 14/06 14:47 i was actually thinking of doing a small family of Hask categories, where the most basic one doesn't allow recursion at all and the fullest one has general recursion and at least some model of 'execution' 14/06 14:48 that'd be neat 14/06 14:49 there is that partiality monad 14/06 14:49 we could look into adapting the ideas there 14/06 14:49 so that 'morally correct' reasoning could be used and would carry its domain of applicability along with it 14/06 14:49 do you have a reference for the partiality monad? 14/06 14:52 http://www.cse.chalmers.se/~nad/listings/lib/Category.Monad.Partiality.html#1 14/06 14:58 it's basically a coinductive iteratee with no input 14/06 14:58 heh, i didn't think there was one in the stdlib 14/06 15:01 amazing what you can find in there if you look 14/06 15:01 there's all sorts of goodies buried in Everything.agda 14/06 15:01 I've spent ages looking all over it 14/06 15:01 fix is not as simple as fix f = f (fix f) with that, though 14/06 15:02 i don't think it matters for what we're talking about right now--as long as fix can be written, we could use it to model general recursion in an object language 14/06 15:03 so anyway, I was reading adjoint folds last night on the plane 14/06 15:35 and it actually talks about kan extensions in the context of programming languages! 14/06 15:35 it's also fairly easy to follow 14/06 15:35 are you using it somewhere? 14/06 15:40 nope 14/06 15:41 just felt like reading something on the plane 14/06 15:41 also wrote some boring CT functors while I was on the plane 14/06 15:41 In the last line of http://hpaste.org/47793 the [_,_] expressions gets marked yellow. I can't see why. Seems like a trivial ⊎-elimination to me. Anyone able to help? 14/06 16:02 t might be because it can't infer the "motive" 14/06 16:03 *it 14/06 16:03 i.e. the (P : A ⊎ B -> Set l) argument 14/06 16:04 the goals buffer should tell you more about the types of unsolved metas 14/06 16:06 xplat: is the other branch ready for switching? it looks like there's some stuff missing, unless you moved it around 14/06 16:11 copumpkin: i probably moved it around, but just for safety's sake, you can ask me about the specific items 14/06 16:12 things like Terminal objects, iirc 14/06 16:12 basically, a lot of the red items in here: https://github.com/xplat/categories/compare/port 14/06 16:12 Categories/Object/Terminal? 14/06 16:12 many of them were empty anyway 14/06 16:12 which are fine to remove 14/06 16:12 basically all the things with largeish numbers of lines here: http://snapplr.com/xavh 14/06 16:13 oh 14/06 16:14 it just didn't recognize the rename 14/06 16:14 a lot of the smaller files had too many changes relative to their size to be recognized as moved versions of their prior versions 14/06 16:14 I see 14/06 16:14 which weirded me out since i used git mv for everything, but whatever 14/06 16:14 i wonder if it would have done better if i'd committed before i moved.  i might have believed too much of git's own hype about history-insensitivity... 14/06 16:16 er, not before i moved, after i moved but before i edited 14/06 16:16 I think git mv is just a move followed by a git add 14/06 16:16 it still uses heuristics to detect renames 14/06 16:16 particularly, all the files with one line had that line changed to match their paths 14/06 16:17 yeah 14/06 16:17 those are kind of silly to keep around anyway, but one day I'll get around to filling them in 14/06 16:17 even files like Categories/Enriched had so many imports and opens changed that they don't register as the same file 14/06 16:19 (all imports were changed in every file, in fact) 14/06 16:19 (and every ‘open Category.Category foo’ 14/06 16:20 yeah 14/06 16:23 we need an agda refactoring tool! 14/06 16:23 maybe something to work on during hac phi :) 14/06 16:23 maybe 14/06 16:24 Categories.Product probably needs a cleanup 14/06 16:24 ah 14/06 16:25 just killing all the stuff that's commented out 14/06 16:25 I looked at your Power stuff for the first time in a while yesterday 14/06 16:25 it's impressive :) 14/06 16:25 heh, thanks.  it wasn't that impressive the first 3 times :) 14/06 16:25 lol 14/06 16:25 it seems like we should have some way of transforming it to and from a functor from a discrete category 14/06 16:26 yeah, maybe i'll add that 14/06 16:27 it doesn't sound too hard 14/06 16:29 copumpkin: should i push the new version of Categories/Product.agda (sans commented-out stuff)? 14/06 17:07 sure 14/06 17:09 there are various places I commented out stuff 14/06 17:09 feel free to get rid of it any time you see it 14/06 17:09 well, i don't want to do anything on this branch that's less related to porting than any of what i've already done, but i'll keep it in mind for later 14/06 17:11 pushed 14/06 17:13 the new version has no lambdas and no functions defined in wheres 14/06 17:13 a rare example of where i was able to abstract agda code to the level i'm used to with haskell 14/06 17:14 very nice 14/06 17:16 hello everybody 14/06 18:01 I just trying to compile a program using agda -c Database_con.agda but it throws an error "MAlonzo/Data/Maybe/Core.hs:9:17: 14/06 18:04 Could not find module Database.HDBC.PostgreSQL.Connection': 14/06 18:04 it is a hidden module in the package HDBC-postgresql-2.2.3.3' 14/06 18:04 Use -v to see a list of the files searched for." 14/06 18:04 any ideas? 14/06 18:04 anyone ever seen an example of equirecursive types where inferring of the type (\mu x . B) would infer to the type of B instead of just a sort? 14/06 18:25 s/infer to/result in 14/06 18:25 like (\mu x . B) : typeOf(B) instead of (\mu x . B) : Type 14/06 18:26 or have a reason why that is a bad idea? 14/06 18:40 for example, http://hpaste.org/47803 14/06 18:43 so, i retract my hpaste in favor of the this rule: http://hpaste.org/47806 14/06 19:56 and Saizan says, this introduces the ability to define non-regular types 14/06 19:57 i wrote this function: 14/06 20:13 map⁎ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v)) 14/06 20:13 map⁎ f g (x , y) = (f x , g y) 14/06 20:13 but it seems like Q can hardly ever (never?) be inferred, probably because of the nonlinear use of x 14/06 20:14 is there some way around that? 14/06 20:15 it seems like it could only be inferred if the return type is fixed 14/06 20:24 nothing else seems to really determine Q 14/06 20:25 right? 14/06 20:25 it seems like the second argument (after f) could determine Q 14/06 20:34 (∀ {x} → (y : P x) → Q y (f x)) 14/06 20:34 i guess it would be hard to factor the builtin f out of that though 14/06 20:36 is there a better way to write the bimap of dependent functions over a sigma? 14/06 20:37 xplat: how would it determine it? 14/06 20:42 maybe you're right, hmm 14/06 20:43 ugh 14/06 20:43 when i actually used it i ended up punting and writing a version that sacrifices dependency in the sigma for dependency in the pis 14/06 20:44 ah 14/06 21:04 man, I can't wait for some hardcore agda hax at hac phi 14/06 21:07 Wait, is xplat coming? 14/06 21:11 I hope so 14/06 21:11 xplat: I've forked categories to the agda organization on github, so it feels more "official" now :P 14/06 22:12 I'll still be doing most of my development on my own fork though 14/06 22:12 well, i've got functors exp->functor and functor->exp 14/06 22:32 oh nice 14/06 22:32 did you see my lame diagonal addition? 14/06 22:32 i have yet to prove these sufficiently inverse-y 14/06 22:33 oh, is that checked in now? 14/06 22:33 I was thinking of making the usual sequence of adjunctions 14/06 22:33 yeah 14/06 22:34 but I'm not sure where to put those adjunctions 14/06 22:34 I hate organizing code :( 14/06 22:34 hey, cool, you have the Power version of the diagonal too 14/06 22:37 it almost  feels like we should just make plain old binary products be instances of Power :P 14/06 22:37 but that might get annoying 14/06 22:38 i think it might, yeah 14/06 22:38 adjunctions in Categories.Functor.{Product,Coproduct}.Properties maybe? 14/06 22:39 oh, fair enough 14/06 22:39 man, them there module hierarchies are getting deep 14/06 22:39 I heard you like modules so I put a module in your module so you can modularize while you modularize 14/06 22:41 I'd like to play with abstract definitions of structures with "view" records of them 14/06 22:41 if that makes any sense 14/06 22:42 it probably does, with enough context 14/06 22:42 maybe I'll play with that idea on the Adjunction module 14/06 22:42 well let's say 14/06 22:42 Like ViewL and ViewR in Seq? 14/06 22:42 an Adjunction is an abstract entity 14/06 22:42 you can't look inside it, and we implement it as we please 14/06 22:42 then the adjunction module exports two (or more?) modules inside it 14/06 22:43 each of which has record in it 14/06 22:43 and that record is either the unit/counit set of fields 14/06 22:43 or the hom-set correspondence thing 14/06 22:44 now, you can provide either of those two records, and get an (abstract) adjunction 14/06 22:44 and the abstract adjunction can be converted to either of those, if you want one particular view of it 14/06 22:44 the abstract adjunction also lets you pull monads or comonads out of it 14/06 22:44 and do other representation-agnostic stuff 14/06 22:44 then we could do something similar with monads 14/06 22:45 with the various ways of getting a monad 14/06 22:45 hm, that does have some appeal 14/06 22:45 and other structures that have multiple "definitions" 14/06 22:45 it'd make this feel more like a "programming" library 14/06 22:45 with abstract definitions and such 14/06 22:45 and it'd let us choose the easiest representation for our own proofs 14/06 22:46 and let other modules rely only on an external interface 14/06 22:46 which could be either of the views of adjunctions 14/06 22:46 in practice the adjunction would probably be implemented as one of those views 14/06 22:46 so the translation would  be id for one of them 14/06 22:46 I dunno 14/06 22:48 it might get unwieldy 14/06 22:48 but it feels more principled somehow 14/06 22:48 * copumpkin crazytalk 14/06 22:48 i should actually know this, since i touched EVERY SINGLE FILE four days ago, but is there anything that represents an isomorphism of categories? 14/06 22:51 an Iso in Cat? 14/06 22:52 but nothing explicit, no 14/06 22:52 ah, that's what i thought it might be 14/06 22:52 subcategories and the like would also be nice to have 14/06 22:53 or subobject-like things in generla 14/06 22:53 general 14/06 22:53 is http://en.wikipedia.org/wiki/Subobject a common definition? 14/06 22:57 copumpkin: actually, i don't think an Iso in Cat will work.  i think because of a lack of commutativity the two representations might not be in a common instantiation of Cat 14/06 23:01 *lack of cumulativity 14/06 23:01 oh 14/06 23:01 true 14/06 23:01 we could make lots of noise on the mailing list and bug them to implement cumulativity :P 14/06 23:02 then again, maybe i screwed something up 14/06 23:02 copumpkin: hrm, I saw Awodey define a subobject as a mono going into that object. 14/06 23:02 well, I think one of the issues with a functor from discrete was the fact that the universes weren't very polymorphic 14/06 23:02 right? 14/06 23:03 Which kinda makes sense if you think of equalizers as defining particular subsets. 14/06 23:03 The Wikipedia stuff seems a bit contrived though. 14/06 23:04 copumpkin: yes 14/06 23:05 we could always just make Discrete more polymorphic 14/06 23:05 and use lifted equalities or something 14/06 23:05 the definition of subobject i'm familiar with is an equivalence class of monos 14/06 23:05 copumpkin: the problem, if there is one, is coming from Functors 14/06 23:05 oh 14/06 23:06 Or that, yeah. 14/06 23:06 copumpkin: it looks like the object level for Functors (Discrete I) C might be e \lub (\ell \lub o) for some reason 14/06 23:07 it's hard to tell because they're specified as _ in Functors.agda 14/06 23:07 oh :P 14/06 23:08 you might be right 14/06 23:08 oh, right, it's e \lub (\ell \lub o) because actual functors have to deal with all the pieces so they will live at that level 14/06 23:09 copumpkin: i looked at the wikipedia definition, and yes, i think that's the common concept 14/06 23:15 in practice you indicate a subobject with a mono since the equivalence classes may not be small, so in agda one would create a setoid of them i guess 14/06 23:17 yeah 14/06 23:22 it doesn't seem like you could even make a cumulative universe manually, come to think of it 14/06 23:24 at least, i can't think how to make a type 'sets of level up to n' 14/06 23:25 well, maybe as an indexed data family 14/06 23:25 actually i think that could work 14/06 23:26 maybe i'll try it later and see if i can come up with an enhanced Cat 14/06 23:27 ooh 14/06 23:27 xplat: wanna join the agda organization on github? 14/06 23:38 also, is it worth merging the port branch in now? 14/06 23:41 so we don't do more work on the obsolete structure 14/06 23:42 --- Day changed Wed Jun 15 2011 anyone could help me to make a connection to a database? 15/06 00:14 isn't that basically a haskell question? 15/06 00:20 I don't think anyone in here has ever used databases in agda :P 15/06 00:20 but you can try and wait and see if anyone responds :) 15/06 00:20 You're basically asking how to write a binding, no? 15/06 00:22 yes, a binding to a database 15/06 00:25 starclouded: did you pick a Haskell binding to use? 15/06 00:29 You'll have to go through Haskell (or through C if you're using the Epic backend) 15/06 00:30 not sure what you're asking 15/06 00:33 starclouded: suppose you were using Haskell, and wanted to connect to a database. How would you do it? 15/06 00:37 You'd use some package that supplied a binding, right? 15/06 00:38 yes 15/06 00:39 I am using HDBC 15/06 00:39 Ok. Now you have to write a binding to HDBC from Agda. 15/06 00:39 the thing is how can I use a type like connection? in the power of pi wouter and nicolas "The constructors of the Connection type are not visible to the library’s users" 15/06 00:42 Well besides HDBC itself you also need the HDBC drivers (i.e. package) for the particular kind of database you want to access. 15/06 00:45 e.g.  http://hackage.haskell.org/package/HDBC-mysql 15/06 00:46 yes, I am using DHBC-PostgreSQL 15/06 00:46 Ok, so you have for example    connectPostgreSQL :: String -> IO Connection 15/06 00:48 You'll have to access that function from Agda. 15/06 00:48 but for using that connectPostgreSQL Do I need something of type IO Connection? 15/06 00:52 no? 15/06 00:52 do you understand how to write this code in haskell? 15/06 00:53 No, look at the type. It *gives* you a IO Connection 15/06 00:53 I am watching the IO.Primitive and in there I need to define something of type Unit, for example for using the putStrLn function, putStrLn    : Costring → IO Unit 15/06 00:57 starclouded: Unit is something isomorphic to () 15/06 01:00 ok then what is something isomorphic to Connection? 15/06 01:01 you can "postulate Connection : Set" on the Agda side 15/06 01:01 Well, you'll use a COMPILED_TYPE pragma to relate Agda's Connection to the Haskell one 15/06 01:01 And a postulate, yeah. 15/06 01:02 Have you seen examples on how to write FFI bindings in Agda? 15/06 01:03 yes, I think this is the page http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI , but I try to do the example of list and it throws me an error 15/06 01:06 Agda libs might prove useful too, for example see: http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGraphicsLib.html 15/06 01:06 What error? Maybe you can pastebin. 15/06 01:07 in the page I mentioned the list example is {-# COMPILED_DATA http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#632 [] (:) #-} but the correct is {-# COMPILED_DATA http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#632 [] [] (:) #-} according with the code of the interxtivePrograms 15/06 01:10 I think {-# COMPILED_DATA List [] [] (:) #-} is wrong 15/06 01:14 look http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/Data.List.html#169 15/06 01:15 Well that doesn't mean it isn't wrong :) 15/06 01:18 Why would '[]' occur twice anyway? 15/06 01:18 List has only two constructors. 15/06 01:19 one is the type-level 15/06 01:23 Wouldn't that go into a COMPILED_TYPE pragma? 15/06 01:25 That, or the syntax  {-# COMPILED_DATA D HsC1 .. HsCn #-} 15/06 01:25 is wrong. 15/06 01:25 Eduard_Munteanu: but when I wirte postulate 15/06 01:33 connect : String → IO Connection 15/06 01:33 {-# COMPILED connect connectPostgreSQL #-} and I compile it says that Not in scope: type constructor or class Connection' and Not in scope: connectPostgreSQL' 15/06 01:33 starclouded: you need a IMPORT pragma, do you have one? 15/06 01:34 yes 15/06 01:36 {-# IMPORT Database.HDBC #-} 15/06 01:36 {-# IMPORT Database.HDBC.PostgreSQL #-} 15/06 01:36 I think you need to refer to connectPostgreSQL using the fully-qualified name. 15/06 01:38 i.e. {-# COMPILED connect Database.HDBC.PostgreSQL.connectPostgreSQL #-} 15/06 01:38 THAT 15/06 01:41 thanks 15/06 01:41 funny, Google's results in .pt have been poisoned when searching for "weak head reduction" i keep getting this paper "Games and Weak-Head Reduction for Classical PCF" repeated hundreds of times 15/06 04:44 .gr and .us don't seem to be affected 15/06 04:44 xplat: ohai 15/06 05:02 | The sort of CumulativeCategory cannot depend on its indices in the type (top : Level) → Set top when checking the definition of CumulativeCategory 15/06 15:23 well, so much for that plan :( 15/06 15:23 hello everybody 15/06 15:39 anyone could tell why when I include inside COMPILED pragma a postulate that has a Maybe I get this error The type Maybe cannot be translated to a Haskell type. when checking the pragma 15/06 15:41 COMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL 15/06 15:41 starclouded: you need a COMPILED_TYPE (or _DATA?) for Maybe first 15/06 15:44 postulate 15/06 15:46 Connection : Set 15/06 15:46 dbConnect  : String → IO (Maybe Connection) 15/06 15:46 {-# COMPILED_TYPE Connection Database.HDBC.PostgreSQL.Connection #-} 15/06 15:46 {-# COMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL #-} 15/06 15:46 you need a COMPILED_TYPE or COMPILED_DATA for every type mentioned in dbConnect's type 15/06 15:48 xplat: yo! 15/06 15:49 copumpkin: did you see the error i pasted?  :( 15/06 15:49 xplat: nope 15/06 15:49 where? 15/06 15:51 i'm pretty sure you can make a function (top : Level) → Set top though 15/06 15:51 Saizan: yeah, you can 15/06 15:51 but if you ask for the type of its type, then it'll complain that it isn't a type 15/06 15:51 Set\omega 15/06 15:51 | The sort of CumulativeCategory cannot depend on its indices in the type (top : Level) → Set top when checking the definition of CumulativeCategory 15/06 15:54 oh 15/06 15:55 yeah, I've run into that before 15/06 15:55 how were you trying to define it? 15/06 15:55 data CumulativeCategory : (top : Level) → Set top where lift : ∀ {d o ℓ e} → Category o ℓ e → CumulativeCategory (d ⊔ o ⊔ ℓ ⊔ e) 15/06 15:58 I wonder why it's more strict about not making a Set\omega there than it is for functions 15/06 16:00 maybe worth a mailing list post? 15/06 16:00 in Data/Maybe/Core.agda after the definition of Maybe I add {-# COMPILED_DATA Maybe Maybe Just Nothing #-} 15/06 16:02 and this error is shown Maybe' is applied to too many type arguments In the type signature for check9': check9 :: xA -> (Maybe xa xA) 15/06 16:02 i wonder if the level argument is somehow not being erased there 15/06 16:08 in fact, that's exactly what it looks like 15/06 16:09 When I type check this is shown The type .Level.Level.zero cannot be translated to a Haskell type. when checking the pragma COMPILED dbConnect Database.HDBC.PostgreSQL.connectPostgreSQL 15/06 16:10 i seem to recall a thread on that on the mailing list 15/06 16:10 if you do your own HMaybe type (data HMaybe (A : Set) : Set where { just (x : A) -> HMaybe a ; nothing : HMaybe a } 15/06 16:11 then it should work, although that does not seem ideal 15/06 16:11 I guess that stuff hasn't been tested since universe polymorphism was added? 15/06 16:12 xplat: have any objections to me merging in the port branch this evening? 15/06 17:15 tawny 15/06 17:16 the same thing that happens with maybe happens with list, so I redefine List in my program but this error is shown The type Σ cannot be translated to a Haskell type. when checking the pragma 15/06 17:45 COMPILED describeTable Database.HDBC.PostgreSQL.describeTable 15/06 17:45 well, it's right... 15/06 17:46 Sigma can't be made into a haskell type 15/06 17:46 so how can I refer from agda list to a list in haskell 15/06 17:48 =+ 15/06 17:48 starclouded: um are you sure you're doing it right? Some of the code I linked you earlier used lists. 15/06 17:56 I just did this describeTable : Connection → TableName → IO (dbList Attribute) 15/06 17:57 and dbList is the same as List but defined in my program 15/06 17:58 That should do if you supply correct COMPILED_TYPE and COMPILED_DATA pragmas. 15/06 17:59 I'm not sure how you end up with a sigma in there. 15/06 17:59 {-# COMPILED_TYPE Connection Database.HDBC.PostgreSQL.Connection #-} 15/06 18:00 {-# COMPILED describeTable Database.HDBC.PostgreSQL.describeTable #-} 15/06 18:00 how is TableName defined? 15/06 18:01 TablaName = String 15/06 18:01 are you sure the error you pasted above is thrown by those lines? 15/06 18:01 oh, also, Attribute? 15/06 18:02 The type Σ cannot be translated to a Haskell type. when checking the pragma COMPILED describeTable Database.HDBC.PostgreSQL.describeTable 15/06 18:03 Attribute  = String × U, with el, U  like the universes defined in the power of pi 15/06 18:04 so don't use x 15/06 18:04 write your own product that isn't dependent 15/06 18:04 data Pair (A B : Set) -> Set where ... 15/06 18:05 (since x is indeed a sigma) 15/06 18:06 Actually that should be a record. 15/06 18:06 ok now that I define the attribute like a record I need to bind it to something in haskell? the thing I need in haskell is something like [(String, SqlColDesc)]? 15/06 18:47 You need four bindings, for lists, pairs, String and SqlColDesc. 15/06 18:56 but can I do a binding of a record type? 15/06 19:03 Hrm. I'm unsure how that works. 15/06 19:05 You might want to try the COMPILED_DATA pragma using the fields instead of constructors (since record only have one constructor). 15/06 19:07 If that doesn't work you can translate the record to a data. 15/06 19:07 data Pair (A B : Set) -> Set where pair : A -> B -> Pair A B 15/06 19:08 And you can define the projections manually   fst : \forall {A B} -> Pair A B -> A   and similarly for snd 15/06 19:09 (e.g.   fst (pair a _) = a  ) 15/06 19:10 Eduard_Munteanu: this is what I did first {-# COMPILED_DATA Pair fst snd #-} 15/06 19:41 the I postulate SqlColDesc : Set 15/06 19:41 {-# COMPILED_TYPE SqlColDesc SqlColDesc #-} 15/06 19:41 The I define the Attribute Attribute = Pair String SqlColDesc 15/06 19:42 postulate TableType : dbList Attribute 15/06 19:42 {-# COMPILED_TYPE TableType [(String , SqlColDesc)] #-} 15/06 19:42 but when I compile it shows me an error []' is applied to too many type arguments 15/06 19:43 * copumpkin barfs: _[_][_×-] : ∀ {o ℓ e} → (C : Category o ℓ e) → BinaryProducts.BinaryProducts C → Category.Obj C → Functor C C 15/06 19:51 any idea? 15/06 19:58 starclouded: did you relate your Pair type to the Haskell (,) ? 15/06 20:09 I think you need a COMPILED_TYPE pragma for that. 15/06 20:10 Also, I don't think TableType should be a a COMPILED_TYPE 15/06 20:11 TableType : Set     TableType = dbList Attribute 15/06 20:12 (without making that a postulate) 15/06 20:12 And shouldn't that be    dbList (Pair String Attribute)   ? 15/06 20:13 I use that because for using the COMPILED_TYPE pragma I need the postulate 15/06 20:13 But TableType is merely a synonym for [(String , SqlColDesc)]. 15/06 20:13 You should define it in Agda. 15/06 20:14 Scratch the "dbList (Pair String Attribute)" part, "dbList Attribute" is fine. 15/06 20:15 copumpkin: _[_][_×-] : ∀ {o ℓ e} → let open ... in ... 15/06 20:19 * Eduard_Munteanu ducks :P 15/06 20:19 I suppose you could use modules for that, say WithCategory. 15/06 20:19 it's not so much that 15/06 20:22 it's just having to have the BinaryProducts parameter 15/06 20:22 instead of a CategoryWithBinaryProducts 15/06 20:22 but that has its own issues 15/06 20:23 maybe I should make it one of those new fancy implicit thingies 15/06 20:23 Mm, you mean letting it pick up a proof the category has all binary products using implicits? 15/06 20:24 erm, non-canonical implicits 15/06 20:26 yeah, except they aren't called that anymore 15/06 20:26 but I can't remember what they are called now 15/06 20:26 Fancy implicits? :P 15/06 20:26 yeah! 15/06 20:26 fancy implicit thingies 15/06 20:26 Heh. 15/06 20:26 * Eduard_Munteanu wishes the stdlib used them 15/06 20:27 I wish the stdlib even used irrelevance :P 15/06 20:28 Yeah, and that's been there for a while. 15/06 20:28 I am getting this []' is applied to too many type arguments no matter what my program is 15/06 20:28 starclouded: where are you using [] ? 15/06 20:28 I don't think you should be using it at all. 15/06 20:29 (erm, except the dbList COMPILED_TYPE/DATA) 15/06 20:29 I relate my type Pair with haskell using {-# COMPILED_DATA Pair fst snd irc://irc.freenode.net:6667/#-} 15/06 20:39 Which one, the record or the data variant? 15/06 20:40 data 15/06 20:40 I'm not sure if it works with records. 15/06 20:40 data Pair (A B : Set) : Set where 15/06 20:40 _,_ : A -> B -> Pair A B 15/06 20:40 Well, then it's wrong. 15/06 20:40 why? 15/06 20:41 You can only use constructors there, not your projection functions. 15/06 20:42 I mean in the pragma. 15/06 20:42 but I define fst : {A B : Set} -> Pair A B -> A 15/06 20:42 fst  (a , _)  = a 15/06 20:42 snd : {A B : Set} -> Pair A B -> B 15/06 20:42 [03:42:03 PM] You can only use constructors there, not your projection functions. 15/06 20:42 {-# COMPILED_DATA D HsD HsC1 .. HsCn #-} 15/06 20:43 Now now, who updated the wiki? That HsD wasn't there earlier. 15/06 20:43 Ah, NAD. 15/06 20:44 record Pair (A B : Set) : Set where 15/06 20:44 constructor _,_ 15/06 20:44 field 15/06 20:44 Eduard_Munteanu: he reads the logs in here 15/06 20:45 Neat. 15/06 20:45 COMPILED_DATA on non datatype when checking the pragma COMPILED_DATA Pair fst snd 15/06 20:46 starclouded: I'd try something like {-# COMPILED_DATA Pair (,) (,) #-} with the data variant 15/06 20:46 the same message COMPILED_DATA on non datatype when checking the pragma COMPILED_DATA Pair (,) (,) 15/06 20:47 (which basically maps Pair to (,) and _,_ to (,), one being a type, the other a value) 15/06 20:47 *type/value constructor 15/06 20:47 starclouded: well, you need to use the 'data' variant it seems 15/06 20:48 so how can I do the bind with Pair if I cant use the projection functions? 15/06 20:52 wi this {-# COMPILED_DATA Pair (,) (,) #-} 15/06 20:54 You just use Pair, fst and snd in Agda and it'll take care of translating to Haskell stuff. 15/06 20:54 Since you supplied that pragma, Agda knows she has to translate Pair a b to (a, b) in types for example 15/06 20:55 anyone know if the equivalence of context-free (non-regular) types is decidable? i'm looking at a few slideshows and they kind of connote that, but generated language equivalence for two context-free grammars is undecidable, afaik 15/06 21:43 anyone could help telling me how can I add an instance declaration for (Database.HDBC.IConnection (IO Database.HDBC.PostgreSQL.Connection)) 15/06 21:59 starclouded: don't bother, just specialize it. 15/06 22:00 I dont understand 15/06 22:01 You can include whatever code you want in COMPILED pragmas. 15/06 22:01 So if you want to interface with a function that uses classes, you can simply specialize it to the particular instance you want 15/06 22:02 For example, {-# COMPILED showInteger (show :: Integer -> String) #-} 15/06 22:03 Does that answer your question? 15/06 22:03 (I'm thinking a bit ahead of what you're asking, though) 15/06 22:04 the thing is that I need the IConnection but this type is genareted by the connectPostgreSQL I can put all this things inside the COMPILED pragmas? 15/06 22:21 any ideas? 15/06 23:03 starclouded: your IConnection is Connection 15/06 23:35 Mind IConnection is a typeclass 15/06 23:35 whose relevant instance is Connection 15/06 23:36 (from Database.HDBC.PostgreSQL) 15/06 23:36 For example, you have    commit :: Connection -> IO () 15/06 23:37 And you don't have to deal with typeclasses. 15/06 23:38 --- Day changed Thu Jun 16 2011 * copumpkin pokes xplat 16/06 03:06 * augur pokes copumpkin 16/06 03:12 * copumpkin unpokes augur 16/06 03:13 i dont even know how that works 16/06 03:13 xplat: I'm getting unsolved metas in Categories.Terminal 16/06 04:13 oh it was just something silly 16/06 04:15 copumpkin: what kinds of math do you understand? 16/06 04:21 not many 16/06 04:21 up until I started haskell I hadn't really done much math beyond early college and high school stuff 16/06 04:21 :) 16/06 04:21 why? 16/06 04:22 i want to learn the math required for GR 16/06 04:22 GR? 16/06 04:23 general relativity 16/06 04:23 oh 16/06 04:23 I'd imagine some of the people in ##categorytheory could give you some pointers there 16/06 04:23 ddarius or someone 16/06 04:23 I know ddarius has spent a lot of time reading about physics 16/06 04:23 @tell xplat I merged your port in and made some minor changes and additions, and now Everything.agda seems to typecheck fine and has nothing commented out anymore :) I did make a slight change with a non-fast-forward commit pushed, but with any luck that shouldn't mess with you pulling it 16/06 04:49 Consider it noted. 16/06 04:49 Oregon! 16/06 04:49 I managed to brick my video driver AND wireless driver installing Coq yesterday 16/06 04:50 Second is fixed, first will be fixed whenever I get around to it. :p 16/06 04:50 copumpkin: you know, freenode has memoserv 16/06 04:52 pff 16/06 04:52 djahandarie: oh nice 16/06 04:52 i only discovered memoserv itself like.. yesterday 16/06 04:52 copumpkin, see, this is why I don't try to fix Agda 16/06 04:52 16/06 04:53 16/06 04:53 I'm not sure that is valid in my excuse DTD 16/06 04:53 you've only been giving that one for over a month now 16/06 04:54 Hmm, is twitter login https? 16/06 04:54 it probably has another couple of months at least left in it 16/06 04:54 if you leave it for three or more months, the problem will clearly fix itself 16/06 04:54 That is how I solve all problems 16/06 04:55 copumpkin! 16/06 09:30 read a paper i wrote? 16/06 09:30 :D 16/06 09:30 omg xplat 16/06 16:45 Wowww 16/06 16:47 djahandarie: sup? 16/06 16:47 Rooming with Mike Shulman :o 16/06 16:47 oh nice 16/06 16:47 He is awesome! 16/06 16:48 is he telling you all about HTT? 16/06 16:48 Haha, I'm trying to force it out of him :) 16/06 16:48 and selling you coq 16/06 16:48 I think I'm going to be sold that here anyways 16/06 16:49 probably 16/06 16:49 don't forget your roots! 16/06 16:49 What do you think about the Prop Set distinction? 16/06 16:50 THE WORK OF THE DEVIL 16/06 16:51 lol 16/06 16:51 it's kind of similar to our irrelevance, really 16/06 16:51 not sure which I like better 16/06 16:51 irrelevance feels a little more fine-grained, somehow 16/06 16:51 I like irrelevance better 16/06 17:08 because the prop/set distinction makes erasure a property of the type 16/06 17:09 you have to have erased nats and unerased nats, and the are different 16/06 17:09 instead of just specifying, when you use nats, whether they should be erased 16/06 17:09 *they are 16/06 17:09 true 16/06 17:12 okay, I'm sold 16/06 17:12 (you can see I have well-formed opinions of my own here) 16/06 17:12 :) 16/06 17:12 copumpkin: read my paper? :D 16/06 17:16 sure, later 16/06 17:17 have you put a link to it up? 16/06 17:17 sure! 16/06 17:17 wellnowwhat.net/linguistics/AProgrammaticApproachToBracketingParadoxes.pdf 16/06 17:17 completely untested haskell code, btw. :D 16/06 17:17 written for a person who wont know the difference XP 16/06 17:18 lol 16/06 17:18 ok 16/06 17:18 I'll read it this evening 16/06 17:18 \o/ 16/06 17:20 augur: s/we fine/we find on first page 16/06 18:43 Mike was talking about "-1"-types, 0-types, 1-types from a 2-topos where he said he liked the prop/set distinction. I think he said "-1"-types were propositions, and 0-types were sets -- not sure, he was going too fast :p. 16/06 18:57 djahandarie: reference on -1 types? 16/06 18:58 I think they're normally called 1, 2, 3 16/06 18:59 Not -1, 0, 1 16/06 18:59 guerrilla: thank you 16/06 18:59 I don't have a reference 16/06 18:59 darn 16/06 18:59 augur: np 16/06 19:00 guerrilla: probably they relate to 'negative thinking' which you can find on nLab 16/06 19:17 xplat: You have 1 new message. '/msg lambdabot @messages' to read it. 16/06 19:17 xplat: thanks 16/06 19:18 itd be nice if lambdabot did that when you signed on 16/06 19:18 not when you said something 16/06 19:18 or just joined 16/06 19:18 well yeah. thats what i mean. :p 16/06 19:18 not what it hought at all.. was thinking of like data 0-thing : Set where;   and data 1-thing where; foo : 1-thing; or whatver 16/06 19:24 thought* 16/06 19:24 but yeh, makes sense i guess (-1)-poset is a point... 16/06 19:24 (-2)-groupoid, also a point 16/06 19:25 just starting on learning more than cat.theory vocabulary today actually :P 16/06 19:25 more than just* 16/06 19:25 really want a class on it. not motivaed enough to do it alone.. just have to now to stud coinduction it seems 16/06 19:26 reading "A Tutorial on (Co)Algebras and (Co)Induction" http://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf 16/06 19:27 for my current proof i need to prove that there is only one total function with a given type.  is that possible, and if so how do i do it? 16/06 19:27 (the given type is (A \== B) -> X A \=> X B for fixed but arbitrary families X and _\=>_ 16/06 19:28 hm, is that even true? 16/06 19:28 what if X = const Foo and \=> = -> ? 16/06 19:30 xplat: what do you mean by "only one"? 16/06 19:34 there is probably only one up to extensional equality 16/06 19:34 but not agda equality 16/06 19:34 and the proof that there is only one up to extensional equality is _hard_ 16/06 19:35 you probably can't do it inside agda 16/06 19:35 Why not? 16/06 19:35 well, it's parametricity 16/06 19:36 I think it's independent 16/06 19:36 (could be wrong) 16/06 19:36 maybe i only have a split epi and not an iso :( 16/06 19:37 What are you doing? 16/06 19:38 trying to prove the strongest form of equivalence i can between Exp C I and Functors (Discrete I) C 16/06 19:39 xplat: you just prove forall functions of that type, they are (extensionally) equal to the one you have 16/06 19:40 copumpkin: but i need propositional equality because this function is part of one of the object indices in [_]_~_ 16/06 19:41 copumpkin: how do you do that, in agda? 16/06 19:41 xplat: ouch, I hate that type 16/06 19:41 I was messing with it last night and made it a bit more pleasant 16/06 19:41 ccasin: proof : (f : SomeRestrictiveType -> SomeOtherRestrictiveType) -> forall x -> f x = myImplementation x 16/06 19:42 i guess this may be an iso in epigram, but only something weaker (adjoint equivalence?  but maybe stronger than that but still weaker than iso) in Agda 16/06 19:43 copumpkin: so my guess is there is no agda term of type proof.  but maybe I'm missing something? 16/06 19:43 ccasin: oh, in his case? I dunno :P 16/06 19:43 but I'm sure that for some functions it can be proven 16/06 19:43 even if i prove extensional equality it buys me essentially nothing 16/06 19:44 yeah, sure - I just think the general problem is a parametricity result 16/06 19:44 xplat: I simplified the Functor module a bit yesterday, not sure if I committed that 16/06 19:45 copumpkin: did you merge port into master? 16/06 19:45 yeah 16/06 19:45 and added some other stuff 16/06 19:45 Everything now typechecks with everything uncommented 16/06 19:45 xplat: but I added a more sane refl to that horrible heterogeneous morphism equality thing 16/06 19:46 and used that in various places 16/06 19:46 I'm thinking of moving that heterogeneous morphism equality out of functor 16/06 19:46 since it's conceivable that something else might want it (although I hope not) 16/06 19:46 hm, after making some changes on port i have a feeling this merge will be 'fun' 16/06 19:46 what'd you do? 16/06 19:47 :P 16/06 19:47 added a Categories.Lift for lifting categories, functors, and natural transformations 16/06 19:47 and a Categories.Power.Functorial 16/06 19:48 ah :o 16/06 19:48 you're coming to hac phi, right? 16/06 19:48 that's the plan 16/06 19:54 i'm glad to see they provide appropriate food even for metallivores 16/06 19:54 ...they do? 16/06 19:55 look at the example on the registration page :) 16/06 19:55 metallivores :o 16/06 20:04 don't look so shocked, they eat metal, not babies 16/06 20:07 metals are people too 16/06 20:08 :) 16/06 20:11 just don't leave your sentient telepathic sword lying around 16/06 20:15 but they don't usually allow swords in these kind of things anyway, so problem solved 16/06 20:16 so dolio's giving an agda tutorial at work tomorrow! 16/06 20:18 xplat: if you don't feel like doing the merge, I can merge your new changes in 16/06 22:17 copumpkin: oh, i managed to do it by stashing my changes and reapplying on the main branch 16/06 22:20 oh cool 16/06 22:21 what is your Power.Functorial thing 16/06 22:21 ? 16/06 22:21 maybe I'll just wait to read it :P 16/06 22:21 I also noticed you have a Setoids and an ISetoids 16/06 22:22 it contains translations between the regular Power stuff and functor-from-discrete-category 16/06 22:22 but both seem to contain Setoids 16/06 22:22 I see 16/06 22:22 copumpkin: Setoids has stdlib setoids, ISetoids is irrelevant setoids as defined in Categories.Support 16/06 22:22 yeah, but as far as I could see, ISetoids also contained stdlib setoids 16/06 22:23 unless it merged wrong or something 16/06 22:23 if everything compiled, then no it doesn't 16/06 22:23 https://github.com/copumpkin/categories/blob/master/Categories/Agda.agda#L74 16/06 22:23 i was originally just doing stdlib setoids, but then i realized they were being used not just for reasoning about Agda code but also for some of the purposes of Set 16/06 22:24 oh, I see 16/06 22:24 yeah, they're my poor man's Set 16/06 22:24 if you can think of a better way to make one 16/06 22:24 I'd love to have that instead 16/06 22:24 well, ISetoids seems to work okay for 'the thing that plain Categories are enriched over' 16/06 22:25 * Category·s 16/06 22:25 what confused me 16/06 22:26 is that I thought ISetoids could contain Setoids with irrelevant fields 16/06 22:26 *would 16/06 22:26 (as objects) 16/06 22:27 but it has the same objects as plain Setoids 16/06 22:27 no, it doesn't 16/06 22:27 the Setoid name in that scope is introduced by the open Categories.Support.Equivalence 16/06 22:28 oh 16/06 22:28 regular Setoids are shadowed 16/06 22:28 I'm just dumb 16/06 22:28 I see 16/06 22:28 not even shadowed, really; Setoids opens Relation.Binary itself to get the Setoid it uses 16/06 22:30 YEAH 16/06 22:30 whoops 16/06 22:30 yeah 16/06 22:30 it does make things a little obscure, i suppose, but i'm not sure what else to do there 16/06 22:30 that's fine 16/06 22:31 I was just confused 16/06 22:31 hello everybody 16/06 22:31 the import pragma works with modules created by me? 16/06 22:36 try it? 16/06 22:37 :P 16/06 22:37 yes it does 16/06 22:42 if apply to IO (dbList Row) _<<=_ in the lambda abstraction I can get something like (dbList Row) ? 16/06 23:09 starclouded: you mean _>>=_ ? 16/06 23:36 It's just like in Haskell 16/06 23:36 So yeah. 16/06 23:36 (_<<=_ is either a typo or flip cobind :) ) 16/06 23:37 yes I mean _>>=_ 16/06 23:38 --- Day changed Fri Jun 17 2011 the thing is when I apply the _>>=_ function I get Row 17/06 00:05 starclouded: can you paste? 17/06 00:26 Eduard_Munteanu: http://pastebin.com/XYQwSC72 17/06 01:04 starclouded: dbquery conn "SELECT * FROM test" [] >>= λ x →convRow {!!} 17/06 01:08 convRow       : (dbList SqlValue) → String 17/06 01:08 yes 17/06 01:09 convRow isn't a IO String as it probably should 17/06 01:09 So instead >>= there works on the list monad 17/06 01:09 s/isn't/doesn't produce/ 17/06 01:09 I dont understand the last part 17/06 01:11 starclouded: if you have something of type 'IO a' and pass it to bind, it unwraps it to an 'a' 17/06 01:13 If instead you have something of type '[a]', it unwraps it to an 'a' 17/06 01:13 String is just [Char] 17/06 01:14 Oops 17/06 01:14 dbList, but anyway 17/06 01:14 Lemme look at the API to see what you're trying to accomplish... 17/06 01:15 starclouded: what's convRow? 17/06 01:16 haskell bind to convrow :: [SqlValue] -> String 17/06 01:16 convrow = unwords . intersperse "|" . map fromSql 17/06 01:16 Ok, its type is fine. But you can't use it like that. 17/06 01:17 The thing to the right of >>= must produce an IO something 17/06 01:17 :t (>>=) 17/06 01:18 forall (m :: * -> *) a b. (Monad m) => m a -> (a -> m b) -> m b 17/06 01:18 Because 'connect' is of type IO something and you're practically ending that code with something that's not in IO 17/06 01:19 Maybe you want to print that string? 17/06 01:19 yes 17/06 01:20 Then write "[...] >>= putStrLn \$ convRow [...]" 17/06 01:20 I need the response dbquery that is [[SqlValue]] and pass it to convRow as [SqlValue] 17/06 01:23 So dbquery's type is ... -> IO [[SqlValue]] ? 17/06 01:25 yes 17/06 01:25 Then use, e.g., concat:    >>= putStrLn \o convRow \o concat 17/06 01:26 Depending on what you need. 17/06 01:27 Is it   quickQuery :: IConnection conn => conn -> String -> [SqlValue] -> IO [[SqlValue]]   in HDBC? 17/06 01:28 yes 17/06 01:28 quickQuery' 17/06 01:28 You might want to work that part out in Haskell first, the translation should be straightforward. 17/06 01:30 xplat: I have a deep question for you 17/06 03:47 or anyone, really 17/06 03:47 I have an evil heterogeneous morphism equality 17/06 03:48 it works sort of like the usual heterogeneous equality, but its one constructor accepts a proof that the morphisms are equivalent in the underlying category, and then lets you prove the heterogeneous equality 17/06 03:48 what are the ramifications of making that proof it takes irrelevant? 17/06 03:49 xplat: I've cleared up Functor quite a bit 17/06 04:08 xplat: I've pushed more changes 17/06 04:34 xplat: do you get kan extensions? 17/06 05:25 I think tomorrow sounds like a good day to hack on category stuff in Agda 17/06 05:56 oh yeah? 17/06 05:56 how was your first day of oplss? 17/06 05:57 Though that means I'll need to get Agda on my laptop... 17/06 05:57 Neat 17/06 05:57 copumpkin: Kan extensions are still pretty mysterious to me 17/06 11:56 ah, it seems that really they are just initial or final approximate inverses to precomposition of a particular functor 17/06 13:38 (Lan being the initial forward approximation, Ran being the final backward approximation) 17/06 13:40 you know what's annoying about non-observational type theory? 17/06 13:56 if two open terms are equal, it doesn't mean their lambda (or pi) abstractions are equal 17/06 13:57 so there are actually more lambdas than there are bodies for them to have 17/06 13:57 (not even counting functions not given by abstraction) 17/06 13:58 the only reason this doesn't completely break the system to begin with is that lambda is not a function 17/06 13:59 I thought functions were equal if their bodies were equal 17/06 14:19 copumpkin: how meta-linguistic of you 17/06 14:19 :P 17/06 14:23 xplat: anyway, I added left kan extensions 17/06 14:23 I might do some yoneda tonight 17/06 15:05 it's about that time 17/06 15:05 @tell copumpkin lambdas are definitionally equal iff their bodies are definitionally equal.  closed terms are propositionally equal iff they are definitionally equal.  so closed lambdas are propositionally equal iff their bodies are definitionally equal.  however, the bodies are open, hence propositionally equal iff they have the same substitution instances in the free variable.  so bodies are propositionally equal iff the functions are pointwise equal. 17/06 15:23 Consider it noted. 17/06 15:23 * copumpkin pokes xplat 17/06 16:46 copumpkin: You have 1 new message. '/msg lambdabot @messages' to read it. 17/06 16:46 so, where can i read about these "syntax" declarations in Agda? just noticed them in a post to the ML 17/06 17:59 in one of the release notes 17/06 18:26 found it 17/06 18:26 do you know if its just sugar for more of what the mixfix paper describes? or is it more? 17/06 18:26 i imagine it "just" updates parser cominator rules or something equivalent 17/06 18:27 guerrilla: there are basically two things it does 17/06 19:23 1) lets you rearrange syntactic order of arguments to not match their order in the telescope 17/06 19:24 2) lets you create syntax that binds variables 17/06 19:25 look at the syntax declarations in e.g. Data.Product for the latter 17/06 19:25 xplat: in this definition: http://snapplr.com/mhzt 17/06 19:32 oh nevermind 17/06 19:34 xplat: remember that category presheaves thing I was making? 17/06 19:36 category _of_ presheaves 17/06 19:37 How are you defining it? 17/06 19:40 As a functor category [C^op , Set] ? 17/06 19:44 copumpkin: i remember that 17/06 19:59 yeah 17/06 20:31 I was wondering what universe the Set should live in 17/06 20:31 although I think I know 17/06 20:32 I also have a feeling that my hom functors are destined to always be yellow, the way I wrote them 17/06 21:01 unless you provide implicits 17/06 21:01 I had somehow convinced myself that wasn't the case, but now I'm not convinced 17/06 21:01 :( 17/06 21:02 there's not much use in implicits that must always be provided 17/06 21:02 yeah 17/06 21:02 I was wondering if there were any cases in which they could be inferred 17/06 21:02 I'm thinking of making a module-ish version 17/06 21:03 where you open the module to fix the "implicit" 17/06 21:03 and then some de-modulified ones 17/06 21:03 i rant into that with my Lift stuff that i wrote; Agda is really bad at inferring a level variable that only appears in a lub expression 17/06 21:03 understandably! 17/06 21:03 it doesn't seem like it'd have a single solution 17/06 21:04 maybe it is understandable, i haven't worked out the details enough to know 17/06 21:04 well 17/06 21:04 if I say 6 = 5 lub x 17/06 21:05 it probably doesn't have a unique solution, but does it have a 'unique enough' one? 17/06 21:05 then x can only be 6 17/06 21:05 but 6 = 6 lub x 17/06 21:05 then x can be 0-6 17/06 21:05 I'm sure it could be unique enough, but it seems tricky to make a system that doesn't care about unique solutions 17/06 21:05 anyway there is usually enough information for a unique solution, it just doesn't flow the right places 17/06 21:06 I think I'll do the module approach 17/06 21:07 btw it turns out that my 'Power' stuff is pretty similar to the operation in http://ncatlab.org/nlab/show/power 17/06 21:08 hello everybody 17/06 21:20 xplat: neat 17/06 21:21 I have List String how can I cast it to List (Colist Char)? 17/06 21:51 starclouded: isn't there some toCostring? 17/06 21:53 yes it is 17/06 21:54 Don't you want Colist Char? You said List (Colist Char) 17/06 21:55 this is what I am trying to do I map { } listString, inside the brackets has to be String -> Colist Char, but when I wirte toCostring does not redefine 17/06 21:58 I'm not sure I understand your problem. 17/06 22:01 Anyway, listString must be of type List String. 17/06 22:01 if you type C-c C-. with toCostring in there, what does it say for the Goal and for what you have? 17/06 22:02 this is shown .Data.Colist.Colist Char != Colist Char of type Set when checking that the expression map toCostring qr has type dbList (Colist Char) 17/06 22:08 xplat: I've been rearranging stuff a bit, not sure if you've looked recently 17/06 22:15 the homs are getting moved around a bit too now 17/06 22:15 starclouded: looks like you might have two kinds of colists in play? 17/06 22:18 I think so cause I have to redefine the List in my program cause when I try to use the COMPILED prama inside the orginal list definition it thew an error 17/06 22:37 oh, then you may need to write your own toCostring 17/06 22:43 the COMPILED stuff really should just disappear level parameters, but it does not seem to 17/06 22:44 well, hm, maybe it can't do that if haskell calls back into Agda 17/06 22:46 Try defining dbList : Set -> Set    dbList = List {0} 17/06 22:53 Hrm, though I think it needs to be an actual datatype. 17/06 22:55 Anyway I suppose you could define your own dbList -> List conversion, then use toCostring 17/06 22:55 Embed : ∀ {o ℓ e} → (C : Category o ℓ e) → Functor C (Presheaves C) 17/06 23:37 does that seem reasonable? 17/06 23:37 I've implemented it 17/06 23:37 do you have a better name for it? 17/06 23:38 --- Day changed Sat Jun 18 2011 hm, i always considered Yoneda the root of Yoneda embedding 18/06 00:09 James 18/06 00:12 Oops. 18/06 00:12 xplat: ? 18/06 01:11 xplat: you mean it's named wrong, or the definition is wrong? 18/06 01:33 I guess they're different sides of the same thing :) 18/06 01:34 Hi, I need to make a parser combinator in agda 18/06 13:29 how i can do it 18/06 13:30 hello everybody 18/06 14:02 hi 18/06 20:31 ـــــــــــــــ♥♥ـــــــــــــــ♥♥♥♥ـــــــــــــــ♥♥♥ــــــــــ♥♥♥♥♥‏ 18/06 20:31 see my 18/06 20:32 Hi, we love you too, but what's the meaning of that? 18/06 20:32 this arabic 18/06 20:33 sory 18/06 20:34 spik arabic 18/06 20:34 Oh, I saw underscores and hearts :) 18/06 20:34 No, I don't. 18/06 20:34 Yuo name god 18/06 20:35 what... 18/06 20:37 thank yuo 18/06 20:39 sory 18/06 20:39 battery lo 18/06 20:40 I going 18/06 20:41 good bay 18/06 20:42 ـــــــــــــــ♥♥♥♥♥♥ـــــــــــــــ♥♥♥♥♥♥♥‏ 18/06 20:42 مرحبا 18/06 20:43 hi 18/06 20:44 Erm, you should try to speak English, I'm not sure anybody here speaks Arabic. 18/06 20:44 ok 18/06 20:45 you from country 18/06 20:47 What 18/06 20:48 copumpkin: You around? 18/06 23:54 --- Day changed Sun Jun 19 2011 copumpkin: oy... 19/06 00:05 how do I evaluate arbitrary expressions? 19/06 00:05 C-c C-n 19/06 00:05 sometimes that just results in a type though 19/06 00:06 not the actual… constructors. Say for example with natural numbers. 19/06 00:06 what 19/06 00:06 let me try to find an example 19/06 00:07 Oh, one other useful thing to know... 19/06 00:08 say here I have this 19/06 00:08 http://hpaste.org/47961 19/06 00:08 is there any way to have it (in the output) use my shorthand definitions? Say, supply rewrite rules or something of that nature? 19/06 00:09 %_% 19/06 00:09 no 19/06 00:10 not that i know of 19/06 00:10 it's natural numbers 19/06 00:10 but thats not what you asked for before 19/06 00:10 nothing complex heh. 19/06 00:10 yes i can see that its naturals 19/06 00:10 but its in hanzi! 19/06 00:10 actually it's in japanese... 19/06 00:11 but I wouldn't be surprised if the ideographs match 19/06 00:11 well they had better, for the most part 19/06 00:12 uh oh 19/06 00:13 8 - 3 is not 4... 19/06 00:13 My definition of - must be wrong 19/06 00:14 >_> 19/06 00:14 * Eduard_Munteanu sees ladder, spider web, spider web : Set :P 19/06 00:14 and 8 - 0 is not 7 :D 19/06 00:15 Eduard_Munteanu: I see self, sort of thing, number 19/06 00:16 s s s s s s s s 0 - s s s 0 = s s s s s s s 0 - s s 0 = s s s s s s 0 - s 0 = s s s s s 0 - 0 = s s s s s 0 19/06 00:16 your definition works 19/06 00:16 How exactly does one go about reading those characters on a computer screen? 19/06 00:18 Eduard_Munteanu: ? 19/06 00:18 They look way too small given the details involved. 19/06 00:18 what 19/06 00:19 Even if I zoom in the browser they still look small compared to latin script. 19/06 00:19 they look fine to me 19/06 00:19 for example 数 19/06 00:20 Can you make out the details? 19/06 00:20 Stuff like 六is fine, but the other ones seem hard to make out. 19/06 00:22 @tell dylukes you could make it use arabic numerals if you provided BUILTIN declarations, look at stdlib's Data.Nat for the details 19/06 00:22 Consider it noted. 19/06 00:22 Eduard_Munteanu: i can make out everything but the top right radical 19/06 00:25 Eduard_Munteanu: i suspect most people won't look/need the precise details to read it anyway 19/06 00:25 augur: Yeah I hadn't recompiled it. 19/06 00:26 dylukes: You have 1 new message. '/msg lambdabot @messages' to read it. 19/06 00:26 That's why :P 19/06 00:26 Saizan: So, is there any way to make it use my own number system? 19/06 00:27 I guess so. I'm not sure, maybe the char count is lower in Japanese, but there are lots of characters in Chinese at least. 19/06 00:27 dylukes: no 19/06 00:27 What if I feel like using the japanese number system for some arbitrary reason. 19/06 00:27 you'd have to patch the pretty printer :) 19/06 00:27 dylukes: make a 'show' for your numbers 19/06 00:28 And read the output as a string. 19/06 00:28 Eduard_Munteanu: That works in Agda o.0? 19/06 00:29 wait, I'd need a built-in for strings too... 19/06 00:29 I don't know how to use them 19/06 00:29 You might want to get the stdlib and look around. 19/06 00:30 Why wouldn't it work? 19/06 00:30 Is the std lib not in the default agda package? 19/06 00:30 You'd just C-c C-n showJPNum mynumber 19/06 00:30 No. 19/06 00:30 great. I'm on dialup 19/06 00:31 http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary 19/06 00:31 Ouch. 19/06 00:31 ^^ 19/06 00:33 So, how will I have to download/install it? 19/06 00:33 Oh, so before, 19/06 00:33 I tried defining Ints and Nats 19/06 00:33 You just unpack it somewhere and set the paths in Emacs. 19/06 00:34 and I had Ints as a small wrapper around Nats and a Sign... 19/06 00:34 but then I wanted overloaded _+_ 19/06 00:34 so, my solution I came up with 19/06 00:34 after spending 10 hours on it without internet TT_TT 19/06 00:34 was to have a data type Number where 19/06 00:34 nat : Number 19/06 00:34 int: Number 19/06 00:34 then 19/06 00:34 decode : Number -> Set 19/06 00:35 decode nat = Nat 19/06 00:35 decode int = Int 19/06 00:35 then had a Number implicit argument to _+_ ... 19/06 00:35 and applied decode to each of the arguments 19/06 00:35 _+_ : {Number a} -> decode a -> decode a -> decode a 19/06 00:35 congratulations, you just re-invented "universes" :) 19/06 00:35 {nat} _ + _... 19/06 00:35 is there a better way to do this? 19/06 00:36 universes....? 19/06 00:36 In fact they're like typeclasses but closed. 19/06 00:36 (I'd google but that'd take 20 minutes) 19/06 00:36 I'm basically wondering if Agda has type classes? 19/06 00:36 closed?... 19/06 00:36 In latest darcs, yeah, sortof. 19/06 00:36 your Number type is also called an universe 19/06 00:36 As in, you can't add items to them you mean? 19/06 00:36 that sounds sketchy. 19/06 00:37 Saizan: explain? 19/06 00:37 They're closed in the sense you can't add new instances 19/06 00:37 You have to edit the original definition to do so. 19/06 00:37 It seemed to me to be more a "hackish mapping of nullary type constructors as tags to types" 19/06 00:37 mmk, got it. 19/06 00:37 dylukes: there's nothing much to explain, it's sort of a design pattern for overloading, but as Eduard_Munteanu points out the problem is that you can't add new "instances" without modifying the universe type, Number in this case 19/06 00:38 mm. 19/06 00:38 The non-canonical implicits (or what are they called these days?) are more like typeclasses. 19/06 00:38 dylukes: the darcs version of agda has something much more like typeclasses instead 19/06 00:38 non-canonincal implicits?... 19/06 00:38 I have Agda 2.2.10 19/06 00:39 am I too far out of date? 19/06 00:39 that's the latest released version, but no released version has themù 19/06 00:39 They aren't in any release so far. 19/06 00:39 I see theres a Agda.TypeChecking.UniversePolymorphism module in there too 19/06 00:40 is there some sort of sugar or special library support? 19/06 00:40 (in 2.2.10) 19/06 00:40 UniversePolymorphism is unrelated 19/06 00:40 it's another notion of Universe 19/06 00:40 mmk 19/06 00:40 They're like {} (but spelled {{}}), except Agda will look in the scope for a matching definition of the "thing", and will pick that up if it's unique. 19/06 00:40 It's not like regular passing of implicits, hence non-canonical. 19/06 00:41 Explain? 19/06 00:41 or, example would be good. 19/06 00:41 Also, I'm wondering if theres a way to do something like… say I have 19/06 00:41 There's one in the stdlib 19/06 00:41 int Nat Sign 19/06 00:41 and I do 19/06 00:41 (int n1 s2) + (int n2 s2) 19/06 00:42 that doesn't work... 19/06 00:42 is there any way ,in the pattern match, to assert you want to match where two things are equal? 19/06 00:42 I guess that's asking too much... 19/06 00:42 I could define the equality myself and use with?... 19/06 00:42 you could say _+_ : {A : Set} {{add : A -> A -> A}} -> A -> A -> A; _+_ {_} {{add}} = add 19/06 00:42 the reason I ask is I'd like to match the sign being equivalent, and then use it in the match. 19/06 00:42 er, use it in the result expression 19/06 00:43 ._. 19/06 00:43 http://code.haskell.org/Agda/doc/release-notes/2-2-12.txt 19/06 00:43 then define addNat : Nat -> Nat -> Nat; addInt : Int -> Int -> Int; and then call + on Nat's or Int's and the add argument would get filled in by addNat or addInt depending on the type 19/06 00:44 Basically instances are records you define in the global scope. 19/06 00:44 Saizan: er… wait how is it "picking up" on addNat and addInt? 19/06 00:44 do they have to have a unique type? 19/06 00:44 dylukes: they just need to be in scope and uniquely match the type of add in the particular context 19/06 00:46 could you paste an example usage of that? 19/06 00:46 one would usually define a record type to distinguish different binary operations 19/06 00:46 dylukes: look in the release notes above ^ 19/06 00:46 * Instance arguments. 19/06 00:46 ah its a new feature thing 19/06 00:47 I'll hold off on 2.2.12 for now 19/06 00:47 I have plenty to work with/learn in 2.2.10 >_> 19/06 00:47 Also here: http://code.haskell.org/Agda/examples/instance-arguments/ 19/06 00:48 should I download 2.2.12 do you think? 19/06 00:49 There's no 2.2.12, just latest darcs 19/06 00:50 I run latest darcs Agda & stdlib, it's ok. 19/06 00:50 dylukes: for your question about equality of signs, you're right, you have to define the comparison function yourself and then use with 19/06 00:50 Hrm, I should revisit my automated Haskell binding generator idea. 19/06 01:06 how should i render lagda files 19/06 03:10 Verde campeon 19/06 03:12 what 19/06 03:12 sorry 19/06 03:12 also, is it possible to define type-level Fix? i couldve sworn it was but im getting a strict positivity error 19/06 03:13 also can someone point me to something that explains why strict positivity is something people like? 19/06 03:26 also also is there a standard include for lagda to get all the pretty coloring and fonts? 19/06 03:30 you can't define a Fix : (F : Set -> Set) -> Set, because there's no guarantee F will be strictly positive 19/06 03:46 http://code.haskell.org/~Saizan/UCodes.agda <- here's something that works 19/06 03:48 (Desc might not cover all the functors you are interested in though) 19/06 03:49 strict positivity is important because it guarantees consistency 19/06 03:51 i tried using conors flag that turns off strict positivity checking 19/06 04:01 but i get a file end error with that o.O 19/06 04:01 I wonder, does it lack of strict positivity imply there are terms which don't have a closed form? 19/06 04:02 s/it// 19/06 04:03 whats a closed form exactly 19/06 04:04 Something that's finite when spelled out. 19/06 04:05 ahh 19/06 04:06 e.g. 'fix succ' isn't 19/06 04:06 Eduard_Munteanu: sure but in the type domain type fixed points are ofcourse not finite because they're infinite disjunctions but .. 19/06 04:08 Eduard_Munteanu: once you get used to hanzi/kanji it becomes much easier to read them.  your brain fills in the details the pixels leave out. 19/06 04:10 I remember somebody posting that Warrior exercise in #haskell, and you can't really encode that in Agda because it's not strictly positive. In order to write a member of Warrior you'd need another one and so on. 19/06 04:10 xplat: ah, I was wondering about that. Mainly because I saw webpages written in Japanese, and the layout was odd (big spacing, large characters and so on). So I thought that might be the reason. 19/06 04:11 Eduard_Munteanu: they do need to be a little bit bigger than latin letters, but not as much as you'd think at first 19/06 04:17 so regardling the lagda questions, anyone? 19/06 04:18 i think some of the spacing stuff is more a cultural coincidence, different design sense 19/06 04:18 but then again it might be connected in a more roundabout way 19/06 04:19 augur: sorry, i haven't even looked at lagda yet 19/06 04:20 sokay :p 19/06 04:20 i think a wall of kanji might look a bit more intimidating and be easier to get lost in than a wall of english text since there are no spaces between words 19/06 04:22 so in that sense it might be better to use smaller paragraphs and more space between them 19/06 04:22 spaces are a fairly recently invention in the realm of alphabetic writing. 19/06 04:23 ancient greek and roman texts used no spaces 19/06 04:23 occassionally the romans would use interpuncts, especially later 19/06 04:24 yet another reason i'm glad to have modern technology 19/06 04:24 imagine computing with roman numerals and no spaces 19/06 04:24 augur: maybe Pandoc? 19/06 04:25 im not sure if anyones really done any studies on relative comprehension speeds and reliability 19/06 04:25 there might be tho 19/06 04:25 Eduard_Munteanu: pandoc? 19/06 04:25 or for the rendering 19/06 04:25 well, forget comprehending your own code, try getting the computer to do it 19/06 04:26 i take it theres nothing i can do from within aquamacs? 19/06 04:26 xplat: no i mean reading comprehension for normal text 19/06 04:26 say   http://flygdynamikern.blogspot.com/2009/03/blogging-with-pandoc-literate-haskell.html 19/06 04:26 I'm not sure what you meant by rendering, though. I assumed you wanted to get a PDF or whatever from the .lagda file 19/06 04:26 yeah 19/06 04:27 augur: i don't find spaceless english text that bad for straight reading even though english spelling is not designed for that and i'm not used to it.  for scanning and when you lose concentration though it seems terrible. 19/06 04:28 i mean, texshop works fine but theres no agdamode so its a pain to have to open it in texshop then render 19/06 04:28 of course, you might not want to go by me, since i am a freak of nature who can read latin text upside down and in mirrors at about half normal speed and do cryptograms in my head 19/06 04:28 ;) 19/06 04:29 looks like tmux is what i was looking for as a replacement for screen 19/06 04:36 copumpkin: surely you know about lagda 19/06 07:19 surely surely! 19/06 07:19 what about it? 19/06 07:20 I've never written any .lagda files 19/06 07:20 oh 19/06 07:20 :( 19/06 07:20 so you wouldnt know whether or not theres a standard import i could use or anything 19/06 07:20 Hello 19/06 07:23 augur: it's just another format for source code? 19/06 07:23 what do you mean imports 19/06 07:23 copumpkin: syntax highlighting stuff mostly 19/06 07:23 but also the stuff to hide inessential code, and the stuff to inline code without it being actual code 19/06 07:23 Anyone knows where are the functor laws definied in the standar library? 19/06 07:24 thanks 19/06 07:24 john___: probably in category 19/06 07:24 http://www.cse.chalmers.se/~nad/listings/lib-0.5/Category.Functor.html#1 19/06 07:25 well, there are no laws there i guess 19/06 07:25 maybe theres no proper CT stuff like that 19/06 07:25 copumpkin should know, surely! 19/06 07:26 copumpkin : any ideas? 19/06 07:27 there isn't proper CT stuff in the std lib 19/06 07:28 it's a slightly fancier version of haskell CT 19/06 07:28 ok, thanks 19/06 07:28 can you give any reference at all? 19/06 07:30 oh man 19/06 07:31 i need to get some sleep 19/06 07:31 night 19/06 07:31 john___: you can find all the functor laws in the categories library 19/06 07:35 https://github.com/copumpkin/categories 19/06 07:35 woo okay 19/06 20:25 it seems i have made some progress with lagda 19/06 20:25 augur: how did you go about rendering it? 19/06 20:29 * Eduard_Munteanu might want to do this some time... 19/06 20:30 im just using the same renderer i'd otherwise be using 19/06 20:30 blah 19/06 20:48 i dont like the current lagda formatting that comes with lhs2tex 19/06 20:48 everything is in math sansserif 19/06 20:48 ok thats fixable. good good 19/06 20:54 --- Day changed Mon Jun 20 2011 whats a good structure for a brief agda tutorial for a paper that uses agda extensively but isnt designed for an agda audience 20/06 00:25 brief as in order of introducing syntax, etc. 20/06 00:25 what programming languages ARE they familiar with? 20/06 01:01 I didn't have much trouble reading through Conor's paper on Epigram without actually knowing the language beforehand. 20/06 01:09 I suspect familiarity with lambda calculus, type theory and a vague idea about dependent types should be enough. 20/06 01:10 xplat: almost certainly none :) 20/06 01:20 Pfft... linguists. :P 20/06 01:22 Eduard_Munteanu: tell me about it 20/06 03:59 but thats part of what this paper is attempting to address 20/06 03:59 anyone know why \Sigma isnt rendering in lagda?? 20/06 04:30 using lhs2tex i mean 20/06 04:30 should i use ?s or {! !} or { }n when showing holes in an lagda file, do you think? 20/06 06:05 if they'll be used to show the process of incremental construction? 20/06 06:06 augur: back now, if you have any more questions ... 20/06 07:09 hey you 20/06 07:09 kosmikus: whats for breakfast? :D 20/06 07:10 just some muesli 20/06 07:13 muesli can be pretty good 20/06 07:28 kosmikus: do you know how to turn off latex math operator spacing? 20/06 07:52 - is showing up as a binop with the normal spacing and this is problematic 20/06 07:53 augur: not by default 20/06 07:56 k 20/06 07:56 augur: so you've probably changed the formatting of identifiers 20/06 07:57 a bit! 20/06 07:57 im using conors style 20/06 07:58 which i should probably ok with him first e.e 20/06 07:58 so what are you using for variables? 20/06 07:59 purple mathnormal 20/06 08:00 you probably want text, not math 20/06 08:00 at least if you're using -s in variable names 20/06 08:00 oh? 20/06 08:01 well, foo-bar in math will render as foo - bar. I can't do anything about it. foo-bar in text will render as foo-bar. 20/06 08:03 true true 20/06 08:03 ok 20/06 08:03 this is for latex? can't you just do \- or someting 20/06 08:03 thank you :) 20/06 08:03 yes, I could reformat all occurrences of - to something else on the lhs2TeX side, but it's unclear to me what the general default should be. 20/06 08:04 generally, text seems to work fine for me. 20/06 08:04 most "math" in identifiers is done via unicode anyway, and that works in LaTeX text mode, still. 20/06 08:05 whoa wait 20/06 08:05 you're andres loh? 20/06 08:06 yes 20/06 08:06 apparently not, \mbox{-} is the correct way 20/06 08:06 awesome. you saved me the trouble of emailing you! 20/06 08:06 lol 20/06 08:06 augur: and you are? 20/06 08:06 noone important :D 20/06 08:06 and noone you'd know 20/06 08:06 unfair :) 20/06 08:06 wow, famous people in #agda :P 20/06 08:06 :) 20/06 08:07 http://www.ling.umd.edu/people/students/ darryl mcadams 20/06 08:07 http://www.ling.umd.edu/people/person/darryl-mcadams/ 20/06 08:07 hey look at that 20/06 08:07 a direct link 20/06 08:07 ok heres a question for you, sir 20/06 08:08 ok nice :) 20/06 08:08 guerrilla: well, pigworker is on #agda ... certainly significantly more famous than I am :) 20/06 08:09 oh what.. hahaha i didnt know that was conor 20/06 08:10 :) 20/06 08:10 actually, nevermind, i see the answer is apparent. 20/06 08:10 wait whoa hello 20/06 08:10 conor is here? 20/06 08:10 pigworker: can i totally steal your color scheme 20/06 08:10 i've never seen him talk tho.. 20/06 08:11 i never saw him come in 20/06 08:11 i know you can guarantee a response if you tweet @pigworker 20/06 08:12 god what a twitter addict. get a life you nerd! 20/06 08:12 oh yeah.. cool. well i don't do anything so advanced to warrent his attention at this point :) 20/06 08:12 kosmikus: what font setup are you using for agda normally? is it all mathsf or is it text and a sans font? 20/06 08:13 augur: I'm pretty sure Conor will actually be grateful if more people start using his color scheme. 20/06 08:13 augur: here's an paper using Agda I've written, as an example: http://people.cs.uu.nl/andres/gdiff-wgp.pdf 20/06 08:15 s/an/a/ 20/06 08:15 er.. example of? :P 20/06 08:15 augur: you've been asking of my preferred layout. 20/06 08:17 no no i just meant what font do you use for agda in agda.fmt 20/06 08:18 augur: so I thought that better than just describing it, I'd show you an example. 20/06 08:18 without any customizations 20/06 08:18 is it mathbf or something else? 20/06 08:18 textsf 20/06 08:19 aha! 20/06 08:19 kosmikus: ah, heres an important question. why does [] not work properly in %format? 20/06 08:22 also, \Sigma and \lambda render as S and l, btw. 20/06 08:24 augur: [] is treated as two tokens even in Agda mode, which is probably wrong, but not so easy to fix. you can only give formatting directives for single tokens. 20/06 08:26 aha ok. 20/06 08:26 augur: \Sigma and \lambda should expand to \textSigma and \textlambda, and render as whatever you've defined these, I think. 20/06 08:27 hmm ok 20/06 08:27 augur: there's a package textgreek.sty that defines all greek characters properly. I should probably make agda.fmt depend on it. 20/06 08:27 nifty. i shall include textgreek.sty immediately! 20/06 08:28 hmm. well, im using textgreek but i still have to use a %format. 20/06 08:33 that's strange. I think it just works for me. 20/06 08:36 hm. ah well. its nothing major. 20/06 08:37 all of agda.fmt is a bit ad-hoc. 20/06 08:38 I made it as a proof of concept originally. 20/06 08:38 in other directions, do you know anything about lagda mode 20/06 08:38 and then never got around to properly redoing it. 20/06 08:38 i'd be happy to help properize it! 20/06 08:39 :) 20/06 08:39 lhs2tex is on github. you can send patches ... I'll look at them ... eventually :) 20/06 08:39 :p 20/06 08:40 kosmikus: in organizing your tex files, do you prefer to keep all your %formats at the top, or to you distribute them around where the definitions are? 20/06 08:47 augur: I usually move them to a separate file, and %include it. 20/06 08:52 aha! 20/06 08:52 hmm 20/06 09:04 \textit in %format gives me a weird error 20/06 09:04 it gives me a font warning then an undefined control sequence error 20/06 09:06 specifically http://hpaste.org/48011 20/06 09:06 augur: the use of my colour scheme (which goes back to 2000) requires no permission, but I am certainly pleased to see it 20/06 09:13 hooray! 20/06 09:14 pigworker: also, you remind me of rory williams. just fyi. 20/06 09:14 now that's a new one on me 20/06 09:20 rory, from doctor who 20/06 09:22 I have a passing acquaintance with Doctor Who... 20/06 09:25 oh man, its great. rorys totally badass 20/06 09:26 and he had great specs in one ep I remember 20/06 09:27 possibly! 20/06 09:27 is demorgan's law constructive? 20/06 10:44 hmm. kosmikus, does \savecolumns work in specs? 20/06 11:10 or in agda in general 20/06 11:10 yes 20/06 11:38 hm. 20/06 11:38 i cant seem to get it to work. 20/06 11:39 minimal example on hpaste? 20/06 11:39 eh. its not that important. ill annoy you some other time :p 20/06 11:39 well, it should be simple 20/06 11:41 augur: this works, for example: http://hpaste.org/48012 20/06 11:45 hmm 20/06 11:45 oh i see. i guess i was doing it wrong. 20/06 11:45 the the real question is why i cant seem to use whitespace to align things 20/06 11:46 which from what i saw should work 20/06 11:46 but if i do   foo : A\n    -> X   the -> isnt aligned properly 20/06 11:47 I don't understand the question. 20/06 11:47 ah 20/06 11:47 it should be under the : but it always shows up a fixed distance from the left 20/06 11:47 if there's only a single space before :, it won't work 20/06 11:47 augur: have you read any documentation? :) 20/06 11:48 some! :p 20/06 11:48 but is this for \savecolumns or in general? 20/06 11:48 general 20/06 11:48 hmm 20/06 11:48 ok ill check the docs for this. 20/06 11:48 it's simple 20/06 11:48 no dont tell me 20/06 11:48 if its in the docs ill find it 20/06 11:49 if you want things aligned, start them at the same column and precede them with at least two spaces 20/06 11:49 do  foo  :  A 20/06 11:49 er 20/06 11:49 that wen't wrong 20/06 11:49 like this: 20/06 11:51 do  foo  :   A ->  X 20/06 11:51 grr 20/06 11:51 somehow, pasting doesn't work as expected 20/06 11:51 ill check the docs :P 20/06 11:51 you'll figure it out 20/06 11:51 :) 20/06 11:52 is there a list of quail completions i can lookup? 20/06 12:25 er.. i can lookup a symbol in 20/06 12:25 augur: re demorgan 3 out of 4 variants are constructive, but "not (A and B) => (not A) or (not B)" magics up one bit from nothing! 20/06 12:43 thats what i figured. the motivation for linear logic seems a bit clearer now 20/06 12:44 since this seems very much like the "you get one of these but you dont know which" notion of disjunction 20/06 12:44 what is that, par? 20/06 12:44 or maybe its \oplus.. who knows 20/06 12:45 --- Log closed Mon Jun 20 18:39:35 2011 --- Log opened Mon Jun 20 19:00:00 2011 -!- Irssi: #agda: Total of 49 nicks [0 ops, 0 halfops, 0 voices, 49 normal] 20/06 19:00 -!- Irssi: Join to #agda was synced in 145 secs 20/06 19:02 copumpkin: http://wellnowwhat.net/linguistics/AlgebraicSyntax.pdf 20/06 19:11 PREPARE FOR TEXT 20/06 19:11 19 pages and im only about halfway into the paper. @_@ 20/06 19:12 much of the text is actually just introductory stuff 20/06 19:13 i would skip to algebraic derivationality 20/06 19:13 section 4 20/06 19:13 Nice. The typesetting looks good. 20/06 19:15 * Saizan wonders if a stable and a darcs agda installations can coexist peacefully 20/06 19:21 :) 20/06 19:21 Saizan: you can probably arrange to have different cabal prefixes 20/06 19:23 (not exactly coexisting, but close) 20/06 19:23 (cabal and ghc prefixes, probably) 20/06 19:24 cabal-dev for that maybe? 20/06 19:46 don't know how well cabal-dev works with binaries, and you'd need to do something about emacs too 20/06 19:46 yeah, emacs is what worries me, i guess i'll just have to edit the config files in a few places when i want to switch 20/06 20:50 I'm having an obnoxious bug trying to cabal install agda 2.10.11 and the std lib from head. 20/06 21:45 Pasting... 20/06 21:45 https://gist.github.com/1036540 20/06 21:46 I'm on OS X 10.7, x86_64 20/06 21:46 that'll teach you to be an early adopter of OS X 20/06 21:46 ;) 20/06 21:46 not sure anyone's looked much at making ghc work on 10.7 yet 20/06 21:46 >_> 20/06 21:46 you should talk to dankna 20/06 21:47 It's worked perfectly fine otherwise. 20/06 21:47 hmm, dunno 20/06 21:47 Hah, dankna always has my problems too ^^ 20/06 21:47 I fixed the LLVM issue btw, just not elegantly. 20/06 21:47 I removed the check for llvm-c entirely. 20/06 21:47 :o 20/06 21:47 But the only problem with that is, 20/06 21:47 you need to make sure when you build llvm you build it with --shared-lib 20/06 21:47 (even if you do, cabal won't find it/link it...) 20/06 21:48 (so have to remove the check) 20/06 21:48 anyways, it works (ish) 20/06 21:48 On a different note. 20/06 21:49 Could someone explain dot patterns and views to me ._. 20/06 21:49 for instance, as used in an equals proof/function 20/06 21:49 or in the case of finding the parity of a number. 20/06 21:49 .(2 * k + 1) 20/06 21:50 etc 20/06 21:50 pattern matching on something can give you additional information on what its indexes are 20/06 21:55 dot patterns make that info visibile in the source 20/06 21:56 do you have some sort of… canonical example 20/06 21:57 something simple and explicative? 20/06 21:57 the simplest indexed datatype is propositional equality 20/06 21:59 data _==_ (A : Set) : A -> A -> Set where refl : {x : A} -> x == x 20/06 21:59 That makes some measure of sense. 20/06 22:00 I mean, I get that. 20/06 22:00 suppose that you want to show that it's symmetric: 20/06 22:00 alright... 20/06 22:00 sym : {A : Set} -> (x y : A) -> x == y -> y == x 20/06 22:00 I like the half-indexed _==_ 20/06 22:01 data _==_ {A : Set} (x : A) : A -> Set where 20/06 22:01 refl : x == x 20/06 22:01 sym x y eq = ? 20/06 22:01 dylukes: so, we are in a situation like "sym x y eq = ?" where eq : x == y and ? : y == x 20/06 22:01 one moment >_< 20/06 22:02 "?" stand for some code we have to fill in 20/06 22:02 right, I get goals somewhat… though emacs is a bitch and keeps interpreting C-c C-SPC as C-c C-@ 20/06 22:03 >_> 20/06 22:03 and your refl isn't working for me… one moment 20/06 22:03 my _==_ you mean? 20/06 22:04 yeah... 20/06 22:04 one second 20/06 22:04 ah, sorry 20/06 22:04 I had 20/06 22:04 data _≡_ {a : Level}{A : Set a}(x : A) : A → Set where 20/06 22:04 refl : x ≡ x 20/06 22:04 in another file. 20/06 22:04 data _==_ {A : Set} : A -> A -> Set where refl : {x : A} -> x == x <- A should be implicit 20/06 22:04 yeah, that works too 20/06 22:04 Anyhow, it doesn't like your implifix. 20/06 22:04 alright so 20/06 22:05 sym x y eq = { }0 20/06 22:05 now, we want to make use of the fact that x == y, so we want to pattern match on eq 20/06 22:05 alright... 20/06 22:06 "sym x y refl = ?" doesn't work though, because x and y still appear unrelated 20/06 22:06 mmk 20/06 22:06 "sym x .x refl = ?" will 20/06 22:06 See, it seems to be that the dot is using to assert that those x's are the same… but somehow it's not... 20/06 22:07 I'm confused by it TT_TT; 20/06 22:07 the dot is not actually pattern matching, it's just exploiting the info you get from pattern matching on refl 20/06 22:08 it's not comparing x and y at runtime 20/06 22:08 dylukes: the dot means that some other pattern element is forcing them to be the same 20/06 22:09 hm 20/06 22:09 so whats the full definition of sym? 20/06 22:09 sym x .x refl = refl 20/06 22:09 it just says 20/06 22:09 Failed to infer the value of dotted pattern 20/06 22:09 when checking that the pattern .x has type A 20/06 22:09 hm 20/06 22:09 you probably don't have a refl in scope? 20/06 22:10 so… what is the definition of the . there 20/06 22:10 I do now, I fixed it 20/06 22:10 that should work then 20/06 22:10 did you put a type signature for sym? 20/06 22:10 yep, it works now. 20/06 22:10 So, what is the . asserting then? 20/06 22:10 that the second argument is the same as the first 20/06 22:11 "the same" 20/06 22:11 according to who? 20/06 22:11 according to agda 20/06 22:11 I mean, we just defined equivalence here… it's not inbuilt… it must be some type checker thing. 20/06 22:11 yeah, but the way we've defined it ends up exploiting the typechecker notion of equality 20/06 22:12 so… the type signature of sum asserts x and y are both members of the same data type. 20/06 22:12 and I guess that x == y and y == x are valid. 20/06 22:12 and x and y must be the same for == to work I guess? 20/06 22:13 I'm just used to the "if you do something wrong -> error" mentality 20/06 22:13 not the "if you do something wrong it just doesn't work" 20/06 22:13 you type too fast :\ 20/06 22:13 …in short, I don't quite get it ^^; 20/06 22:13 anyhow, the types "x == y" and "y == x" are valid just by knowing that x and y have the same type 20/06 22:14 i.e. it's perfectly fine to say (3 == 4), it's quite harder to provide a term of type (3 == 4) 20/06 22:15 :\ 20/06 22:15 still somewhat confused. 20/06 22:15 I think the whole proof mentality really hasn't sunk in quite yet ^^; 20/06 22:15 dylukes: have you come across the empty type? 20/06 22:15 nope. 20/06 22:15 data Empty : Set where 20/06 22:15 write that in 20/06 22:15 it'll typecheck 20/06 22:16 sure. 20/06 22:16 you'll never  be able to provide a value of it 20/06 22:16 right 20/06 22:16 now, what if someone asks for 20/06 22:16 Either Empty Bool 20/06 22:16 what can you give them 20/06 22:16 ahhh mkk 20/06 22:16 Right true 20/06 22:16 is perfectly fine 20/06 22:17 you just can't give them Left ... 20/06 22:17 and Right False 20/06 22:17 yeah 20/06 22:17 so there are only two inhabitants of that type 20/06 22:17 how about 20/06 22:17 (Empty, Bool) (haskell notation) 20/06 22:17 You can't provide a value of that type. 20/06 22:17 It's A -> B -> A x B 20/06 22:17 I guess. 20/06 22:18 okay, so the only possible inhabitants of the _==_ type you can provide, are those constructed via refl, which is of type x == x 20/06 22:19 so the type checker can figure out in sym that since you're using x == y -> y == x, x and y cannot be different? 20/06 22:19 …but then where does the dot come in :\ 20/06 22:19 the typechecker just looks at the type of refl. 20/06 22:20 it knows eq : x == y from the type signature, and refl : a == a from the definition of _==_ 20/06 22:20 I have 20/06 22:21 sym : {A : Set} -> (x y : A) -> x == y -> y == x 20/06 22:21 sym x .x refl = refl 20/06 22:21 correct right? 20/06 22:21 yes 20/06 22:21 I'm noticing more often than not, the point of writing a function in Agda is not to run it :\ 20/06 22:21 just to make it actually exist/work 20/06 22:21 the proofs are like that :) 20/06 22:21 like 20/06 22:22 sym : {A : Set} -> (x y : A) -> x == y -> y == x 20/06 22:22 isn't really doing anything useful :\ 20/06 22:22 except saying given two values of a type A, 20/06 22:22 and x == y 20/06 22:22 then y == x 20/06 22:22 is that correct?... 20/06 22:22 anyhow, to typecheck that code it has to unify x == y with a == a (where a is a fresh variable here), so it concludes that x and y must be the same, and the dot serves just to display the result of this unification in the source 20/06 22:22 unification means? 20/06 22:22 dylukes: in this case: find a mapping from 'a' to some term such that the two are equal 20/06 22:23 okay, this might come off as pedantry/ignorance 20/06 22:23 but what's the formal definition of term here. 20/06 22:24 term/value/type/data type/etc 20/06 22:24 by "the two" i mean "x == y"  and "a == a" 20/06 22:24 ah I see... 20/06 22:25 I guess if you were to take 20/06 22:25 sym x .x refl = refl 20/06 22:25 and substitute in the types to see if they match the type signature of sum… yeah 20/06 22:25 sym, you mean? 20/06 22:25 yeah, autocorrect 20/06 22:25 so, . is just indicating that what you put there should be the result of typechecking? 20/06 22:27 like "dear type checker, if this isn't the type you figure out, throw an exception" 20/06 22:27 except that it's not a type, but yeah 20/06 22:28 er… right 20/06 22:28 the type/value distinction gets a bit blurry sometime >_< 20/06 22:29 all types are values 20/06 22:29 but not all values are types 20/06 22:29 well, there's one type that isn't a value 20/06 22:29 most of the time i'd just say expression or term 20/06 22:29 value might mean something in WHNF in some contexts 20/06 22:30 confused >_< 20/06 22:30 so, do you have another example? 20/06 22:31 or maybe ,help me understand this one... 20/06 22:31 okay 20/06 22:31 say the nat parity example... 20/06 22:31 paste? 20/06 22:32 I am one moment 20/06 22:32 typing out Nat quickly 20/06 22:32 I wish I had std lib working >_> 20/06 22:32 okay 20/06 22:33 You know the agda tutorial pdf? 20/06 22:33 On page 22 of 41 20/06 22:33 data Parity : Nat -> Set where 20/06 22:33 even : (k : Nat) -> Parity (k * 2)