acowley acowley acowley --- Log opened Wed Jul 01 00:00:22 2009 --- Day changed Thu Jul 02 2009 Hello, can someone help me sort through the _|_ type in Nat.Divisibility? 02/07 02:18 I'm trying to extract the n \equiv m * q part of a value of that type 02/07 02:19 but I think I'm failing to get the dotted parts of the pattern matching right 02/07 02:19 Namely, I want something like f : m | n -> n \equiv q * m 02/07 02:20 hr 02/07 02:20 But I'm not really sure how to introduce the q : Nat into the type of that function 02/07 02:20 we need a bot that links to the source code 02/07 02:20 data _∣_ : ℕ → ℕ → Set where 02/07 02:21 divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n 02/07 02:21 oh right 02/07 02:21 well this is not possible:   f : m | n -> n \equiv q * m 02/07 02:21 there is no 'q' 02/07 02:21 I'm getting an m | n value from the gcd function, and I need to use the n \equiv q * m part for another lemma 02/07 02:21 Yes, I know :) 02/07 02:21 you must bring it into scope 02/07 02:21 ok so what are you saying 02/07 02:22 But if I put q as an implicit parameter 02/07 02:22 not possible 02/07 02:22 then q != .q during type checking 02/07 02:22 that's ANY q 02/07 02:22 Right 02/07 02:22 That's why I said I'm not sure how to introduce q into the type of the function 02/07 02:22 So, the m | n value implies a q, and I need that q to express the type of my return value 02/07 02:23 I'm pretty stumped at this point :/ 02/07 02:24 basically why don't you just leave it as  m | n 02/07 02:25 Right, so, some context: I need a lemma that says that if m | n and False (n \?= 0) then False (m \?= 0) 02/07 02:26 I'm getting m from the gcd function, so I have a m | n value 02/07 02:26 what does this mean:  False (n \?= 0)  ? 02/07 02:26 oh you're saying False to mean negation? 02/07 02:27 It means that n is not equal to zero 02/07 02:27 It's from Relation.Nullary.Decidable 02/07 02:27 okay 02/07 02:27 So, the m | n value seems to have everything I need 02/07 02:27 lem-div : {n m q : ℕ} → n ≡ q * m → False (n ≟ 0) → False (q ≟ 0) 02/07 02:28 is trivially provable via pattern matching 02/07 02:28 I'm guessing that I just need to go about doing this some other way, but it seemed strange to me that I couldn't really pattern match the divisibility data constructor. 02/07 02:32 Ouch, this is so close 02/07 02:44 defn-div : {m n q : ℕ} → (div : m ∣ n) → {qeq : q ≡ (quotient div)} → n ≡ q * m 02/07 02:44 defn-div {_} {_} {q} (divides _ eq) {qq} = {!!} 02/07 02:44 02/07 02:44 I have eq : .n ≡ .q * .m 02/07 02:44 qq : q ≡ .q 02/07 02:44 in the context 02/07 02:45 Goal: .n ≡ q * .m 02/07 02:45 Okay, got it done 02/07 02:49 That was painful, but it's done! 02/07 03:04 soupdragon: thanks for bearing with me 02/07 03:04 anyone awake? 02/07 22:58 --- Day changed Fri Jul 03 2009 -!- soupdragon is now known as rocketman 03/07 09:56 --- Day changed Sat Jul 04 2009 --- Day changed Sun Jul 05 2009 --- Day changed Mon Jul 06 2009 http://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.pdf 06/07 02:44 more fun from Conor 06/07 02:45 (And a use case of inverse image, which is nice to see) 06/07 02:46 rocketman: I do wish I would be allowed to write my academic papers in that style. 06/07 10:47 Or rather, get away with it. 06/07 10:48 Apparently the concensus is that it's not sufficiently academic' to w 06/07 10:48 *write in the first person. 06/07 10:48 really? 06/07 11:00 I always write in the first person, as do most others as far as I can tell 06/07 11:01 It's not academic', I keep getting told. 06/07 11:09 pfft 06/07 11:27 at least it makes it clear whether the work is yours or someone else's 06/07 11:28 if academic is meant to mean "stale and unreadable" then perhaps 3rd person is okay 06/07 11:29 I've heard Conor rant on this topic before. 06/07 11:41 --- Day changed Tue Jul 07 2009 hi 07/07 21:57 Is there a page with solutions to the excersises in Ulf Norel's 'Dependently Typed Programming in Agda'? 07/07 21:58 cheater! 07/07 21:59 rocketman: I'd be even happier with 'hints' or what not 07/07 21:59 or what else I should read 07/07 22:00 well if it's an easy one I can give you a hint 07/07 22:00 it's about excersise 2.2 b (yes, that's right, I'm stuck at the third excersise, I suck that much) 07/07 22:01 ?? 07/07 22:02 lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs 07/07 22:02 lem-tab-! xs = {! !} 07/07 22:02 okay 07/07 22:02 the basic case of xs = [] is trivial 07/07 22:02 but if xs is a cons, then what? 07/07 22:03 should I use lem-!-tab and a theorem of the form 'if for all i xs!i==ys!i, then xs==ys'? 07/07 22:03 so in the cons case you have to match on 'tabulate (_!_ xs) == xs' by recursion 07/07 22:03 yes a lemma es good 07/07 22:04 yes, I recurse on tabulate (_!_ xs) == xs with the 'with' construct 07/07 22:05 I was thinking something along the lines of 07/07 22:05 lem-tab-! (x :: xs) | p = refl \and p 07/07 22:06 (refl for x == x) 07/07 22:06 but I don't know how to create a conjunction 07/07 22:06 (maybe I'm on a totally wrong track here) 07/07 22:07 CLook at the definition of oaeu 07/07 22:07 conjunction* 07/07 22:07 that will show how 07/07 22:07 here's the definition of conjunction that I use: 07/07 22:08 data _∧_ (A B : Set) : Set where 07/07 22:08 _,_ : A -> B -> A ∧ B 07/07 22:08 so 07/07 22:08 lem-tab-! (x :: xs) | p = refl , p 07/07 22:09 I guess for this to work I have to also create a lemma of the form "if x == y and xs == ys, then x::xs == y::ys" 07/07 22:09 let me try that 07/07 22:09 (I've only started reading the Agda tutorial two days ago, so things are going a bit slow:) 07/07 22:11 OK 07/07 22:16 I think I'm getting somewhere 07/07 22:19 lem-tab-! (x :: xs) | p = lem-vec-eq-decompose x x {! !} xs (refl , p) 07/07 22:19 my god 07/07 22:20 lem-tab-! (x :: xs) | p = lem-vec-eq-decompose x x (tabulate (_!_ xs)) xs (refl , p) 07/07 22:20 this typechecks 07/07 22:21 does that mean the proof is sound? 07/07 22:21 ummmm 07/07 22:23 good question 07/07 22:23 in theory.. I think it's supposed to mean: yes 07/07 22:24 but Agda is really ad-hoc and buggy, don't trust it 07/07 22:24 but I think I'll have to set the rule of the game to be: if it typechecks, I have to accept my solution:) 07/07 22:25 anyway, thanks for your help 07/07 22:26 I'll look at the next excercise tomorrow. maybe I'll be back with more dumb questions :) 07/07 22:26 bye 07/07 22:28 --- Day changed Wed Jul 08 2009 --- Day changed Thu Jul 09 2009 -!- byorgey_ is now known as byorgey 09/07 13:59 -!- iago is now known as Guest11750 09/07 19:58 -!- Guest11750 is now known as iago 09/07 19:59 -!- byorgey_ is now known as byorgey 09/07 20:28 --- Day changed Fri Jul 10 2009 -!- byorgey_ is now known as byorgey 10/07 02:09 * soupdragon thinks it's pointless to ask heri 10/07 21:20 --- Day changed Sat Jul 11 2009 --- Day changed Sun Jul 12 2009 -!- byorgey_ is now known as byorgey 12/07 19:35 --- Day changed Mon Jul 13 2009 --- Day changed Tue Jul 14 2009 -!- codolio is now known as dolio 14/07 03:27 -!- TR2N is now known as X-Scale 14/07 11:50 -!- codolio is now known as dolio 14/07 14:11 http://www.e-pig.org/epilogue/ !!!!!!! 14/07 19:36 yay 14/07 19:36 activity 14/07 19:36 yeah :) 14/07 19:44 * edwinb just spent the afternoon plotting Epigram hacking with Conor 14/07 20:14 oooh!! 14/07 20:15 note that I said "plotting" rather than "doing" ;) 14/07 20:15 that's even juicyer 14/07 20:15 however, it's more than we've achieved for a while 14/07 20:16 you're still doing the erasure stuff? 14/07 20:16 I haven't done any more than I ever did 14/07 20:16 * soupdragon wonders what the scoop is then :) 14/07 20:17 but hopefully we'll get together next week to have a proper hacking session 14/07 20:17 we were trying to figure out how to hook up the current representation with a compiler, and then have a representation of the type theory than can be more or less stuck to... 14/07 20:19 it all seems quite easy. We just have to bother doing it ;) 14/07 20:19 edwinb: does he come on IRC? 14/07 20:25 no 14/07 20:25 he says he has enough ways to waste time... 14/07 20:25 I think I can understand that 14/07 20:25 lol 14/07 20:26 --- Day changed Wed Jul 15 2009 -!- kosmikus_ is now known as kosmikus 15/07 14:12 -!- TR2N is now known as X-Scale 15/07 16:20 -!- codolio is now known as dolio 15/07 22:15 --- Day changed Thu Jul 16 2009 -!- copumpkin is now known as pumpkin 16/07 21:17 --- Day changed Fri Jul 17 2009 --- Day changed Sat Jul 18 2009 --- Day changed Sun Jul 19 2009 -!- codolio is now known as dolio 19/07 03:45 -!- byorgey_ is now known as byorgey 19/07 20:25 --- Day changed Mon Jul 20 2009 -!- byorgey_ is now known as byorgey 20/07 02:37 -!- copumpkin is now known as pumpkin 20/07 20:34 --- Day changed Tue Jul 21 2009 -!- copumpkin is now known as RichardStallman 21/07 04:19 -!- RichardStallman is now known as copumpkin 21/07 04:19 --- Day changed Wed Jul 22 2009 --- Log opened Thu Jul 23 07:59:12 2009 -!- Irssi: #agda: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal] 23/07 07:59 -!- Irssi: Join to #agda was synced in 86 secs 23/07 08:00 Come on people, let's talk some Agda! 23/07 14:19 ok. you start? :-) 23/07 14:41 hmm, new paper added to the wiki: http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html 23/07 14:48 we're too busy hacking Epigram to talk Agda ;) 23/07 16:40 * soupdragon is reading the epig stuff 23/07 18:07 * soupdragon ... will hack epigram for cake 23/07 18:07 I'm er... hooking up my multimeter, but in Haskell. Pondering an Agda FFI library. I don't think I've ever really understood existentials until I started writing Agda programs, mind you. 23/07 18:57 what do you mean Agda FFI 23/07 18:57 Agda to Haskell. 23/07 18:59 hmmm 23/07 19:00 (I'm not actually being serious. Considering I'll actually be *running* the resulting code...) 23/07 19:00 what ??? 23/07 19:00 zomg running code? that is very inappropriate for this channel 23/07 19:00 not actually being serious -- you're not really writing this 23/07 19:01 I apologise. I'd take this to #haskell, but it's a tad noisy. 23/07 19:01 :( 23/07 19:01 I'm writing the Haskell parts at least. 23/07 19:01 Although, I'm hoping to use George Giorgidze's FMH (E)DSL for other parts of the program, and I'm not sure he's done much work porting that to Agda. 23/07 19:03 http://www.cs.nott.ac.uk/~ggg/ 23/07 19:03 --- Day changed Fri Jul 24 2009 --- Day changed Sat Jul 25 2009 -!- codolio is now known as dolio 25/07 06:50 --- Day changed Sun Jul 26 2009 -!- codolio is now known as dolio 26/07 22:54 --- Day changed Mon Jul 27 2009 -!- codolio is now known as dolio 27/07 21:41 --- Day changed Tue Jul 28 2009 -!- byorgey_ is now known as byorgey 28/07 17:48 I want to do something with deptypes 28/07 19:24 hmmm 28/07 19:24 I still don't know what is going on with epigram 28/07 19:25 how does it implement K? 28/07 19:26 I am really curious how people are doing K and having it reduce 28/07 19:26 there should be a paper on OTT that I can understand 28/07 19:28 * soupdragon read http://strictlypositive.org/ObsCoin.pdf since it's sleepy time in #agda 28/07 19:32 --- Day changed Wed Jul 29 2009 have you read it dolio? 29/07 00:18 "Let's see how things unfold" 29/07 00:19 It? 29/07 00:23 http://strictlypositive.org/ObsCoin.pdf 29/07 00:23 No, haven't read it. 29/07 00:24 Is this going to be about how observational type theory solves the problem? 29/07 00:26 I think soo 29/07 00:26 I don't really get OTT yet 29/07 00:26 It's like the Blade of dependent type theory. 29/07 00:27 :D 29/07 00:27 Anyhow, since OTT gets you nice, extensional-like equality on functions, it's not surprising that you could do it for coinductive types, too, which is what you need. 29/07 00:29 But, it's good to know he's working out the details. 29/07 00:30 "extensional-like equality on functions" like more than just beta-eta? 29/07 00:30 I'm pretty sure you get 'forall x. f x == g x -> f == g'. 29/07 00:30 woah 29/07 00:31 Since you can just add any consistent axiom to the propositional area. 29/07 00:31 And that certainly is consistent, if not intensionally provable. 29/07 00:32 The important part of OTT, as little as I really grok it, is that they separate those sorts of propositions from the types in such a way that they don't ruin everything. 29/07 00:33 Man, I want to see a new epigram with this stuff. 29/07 02:07 you're not the only one ;) 29/07 02:08 * soupdragon wonders if it will compile to assembly instead of this absolutely bizarre thing where people compile into HM-typed languages 29/07 02:10 the current version compiles to assembly via C 29/07 02:10 it just lacks a high level front end... 29/07 02:10 oh! that sounds good 29/07 02:11 That's pretty good. 29/07 02:11 Maybe it should compile to dependently typed assembly. :) 29/07 02:11 argh! ;) 29/07 02:11 Although I suspect the appeal of that sort of thing is for actually writing assembly by hand. 29/07 02:11 hehehe 29/07 02:11 I think the reason people go to HM languages is that it's cheap 29/07 02:12 lets replace java with epigram! 29/07 02:12 whereas writing a run-time system is supposedly harder work 29/07 02:12 which is probably a fair point 29/07 02:12 I thought no one ever ran their programs around here 29/07 02:18 well we don't really need to 29/07 02:18 we already know they are correct after all 29/07 02:18 :P 29/07 02:19 -!- codolio is now known as dolio 29/07 04:50 --- Day changed Thu Jul 30 2009 -!- byorgey_ is now known as byorgey 30/07 03:48 -!- rocketman is now known as soupdragon 30/07 10:19 --- Day changed Fri Jul 31 2009 -!- byorgey_ is now known as byorgey 31/07 19:59