/home/laney/.irssi/irclogs/Freenode/2009/#agda/July.log

--- Log opened Wed Jul 01 00:00:22 2009
--- Day changed Thu Jul 02 2009
acowleyHello, can someone help me sort through the _|_ type in Nat.Divisibility?02/07 02:18
acowleyI'm trying to extract the n \equiv m * q part of a value of that type02/07 02:19
acowleybut I think I'm failing to get the dotted parts of the pattern matching right02/07 02:19
acowleyNamely, I want something like f : m | n -> n \equiv q * m02/07 02:20
soupdragonhr02/07 02:20
acowleyBut I'm not really sure how to introduce the q : Nat into the type of that function02/07 02:20
soupdragonwe need a bot that links to the source code02/07 02:20
acowleydata _∣_ : ℕ → ℕ → Set where02/07 02:21
acowley  divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n02/07 02:21
soupdragonoh right02/07 02:21
soupdragonwell this is not possible:   f : m | n -> n \equiv q * m02/07 02:21
soupdragonthere is no 'q'02/07 02:21
acowleyI'm getting an m | n value from the gcd function, and I need to use the n \equiv q * m part for another lemma02/07 02:21
acowleyYes, I know :)02/07 02:21
soupdragonyou must bring it into scope02/07 02:21
soupdragonok so what are you saying02/07 02:22
acowleyBut if I put q as an implicit parameter02/07 02:22
soupdragonnot possible02/07 02:22
acowleythen q != .q during type checking02/07 02:22
soupdragonthat's ANY q02/07 02:22
acowleyRight02/07 02:22
acowleyThat's why I said I'm not sure how to introduce q into the type of the function02/07 02:22
acowleySo, the m | n value implies a q, and I need that q to express the type of my return value02/07 02:23
acowleyI'm pretty stumped at this point :/02/07 02:24
soupdragonbasically why don't you just leave it as  m | n02/07 02:25
acowleyRight, 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
acowleyI'm getting m from the gcd function, so I have a m | n value02/07 02:26
soupdragonwhat does this mean:  False (n \?= 0)  ?02/07 02:26
soupdragonoh you're saying False to mean negation?02/07 02:27
acowleyIt means that n is not equal to zero02/07 02:27
acowleyIt's from Relation.Nullary.Decidable02/07 02:27
soupdragonokay02/07 02:27
acowleySo, the m | n value seems to have everything I need02/07 02:27
acowleylem-div : {n m q : ℕ} → n ≡ q * m → False (n ≟ 0) → False (q ≟ 0)02/07 02:28
acowleyis trivially provable via pattern matching02/07 02:28
acowleyI'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
acowley_Ouch, this is so close02/07 02:44
acowley_defn-div : {m n q : ℕ} → (div : m ∣ n) → {qeq : q ≡ (quotient div)} → n ≡ q * m02/07 02:44
acowley_  defn-div {_} {_} {q} (divides _ eq) {qq} = {!!}02/07 02:44
acowley_  02/07 02:44
acowley_I have eq : .n ≡ .q * .m02/07 02:44
acowley_qq : q ≡ .q02/07 02:44
acowley_in the context02/07 02:45
acowley_Goal: .n ≡ q * .m02/07 02:45
acowley_Okay, got it done02/07 02:49
acowley_That was painful, but it's done!02/07 03:04
acowley_soupdragon: thanks for bearing with me02/07 03:04
HairyDudeanyone awake?02/07 22:58
--- Day changed Fri Jul 03 2009
-!- soupdragon is now known as rocketman03/07 09:56
--- Day changed Sat Jul 04 2009
--- Day changed Sun Jul 05 2009
--- Day changed Mon Jul 06 2009
rocketmanhttp://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.pdf06/07 02:44
rocketmanmore fun from Conor06/07 02:45
rocketman(And a use case of inverse image, which is nice to see)06/07 02:46
liyangrocketman: I do wish I would be allowed to write my academic papers in that style.06/07 10:47
liyangOr rather, get away with it.06/07 10:48
liyangApparently the concensus is that it's not sufficiently `academic' to w06/07 10:48
liyang*write in the first person.06/07 10:48
edwinbreally?06/07 11:00
edwinbI always write in the first person, as do most others as far as I can tell06/07 11:01
liyangIt's not `academic', I keep getting told.06/07 11:09
edwinbpfft06/07 11:27
edwinbat least it makes it clear whether the work is yours or someone else's06/07 11:28
edwinbif academic is meant to mean "stale and unreadable" then perhaps 3rd person is okay06/07 11:29
liyangI've heard Conor rant on this topic before.06/07 11:41
--- Day changed Tue Jul 07 2009
_Cactus_hi07/07 21:57
_Cactus_Is there a page with solutions to the excersises in Ulf Norel's 'Dependently Typed Programming in Agda'?07/07 21:58
rocketmancheater!07/07 21:59
_Cactus_rocketman: I'd be even happier with 'hints' or what not07/07 21:59
_Cactus_or what else I should read07/07 22:00
rocketmanwell if it's an easy one I can give you a hint07/07 22:00
_Cactus_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
rocketman??07/07 22:02
_Cactus_lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs07/07 22:02
_Cactus_lem-tab-! xs = {! !}07/07 22:02
rocketmanokay07/07 22:02
_Cactus_the basic case of xs = [] is trivial07/07 22:02
_Cactus_but if xs is a cons, then what?07/07 22:03
_Cactus_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
rocketmanso in the cons case you have to match on 'tabulate (_!_ xs) == xs' by recursion07/07 22:03
rocketmanyes a lemma es good07/07 22:04
_Cactus_yes, I recurse on tabulate (_!_ xs) == xs with the 'with' construct07/07 22:05
_Cactus_I was thinking something along the lines of07/07 22:05
_Cactus_lem-tab-! (x :: xs) | p = refl \and p07/07 22:06
_Cactus_(refl for x == x)07/07 22:06
_Cactus_but I don't know how to create a conjunction07/07 22:06
_Cactus_(maybe I'm on a totally wrong track here)07/07 22:07
rocketmanCLook at the definition of oaeu07/07 22:07
rocketmanconjunction*07/07 22:07
rocketmanthat will show how07/07 22:07
_Cactus_here's the definition of conjunction that I use:07/07 22:08
_Cactus_data _∧_ (A B : Set) : Set where07/07 22:08
_Cactus_  _,_ : A -> B -> A ∧ B07/07 22:08
rocketmanso07/07 22:08
rocketmanlem-tab-! (x :: xs) | p = refl , p07/07 22:09
_Cactus_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
_Cactus_let me try that07/07 22:09
_Cactus_(I've only started reading the Agda tutorial two days ago, so things are going a bit slow:)07/07 22:11
_Cactus_OK07/07 22:16
_Cactus_I think I'm getting somewhere07/07 22:19
_Cactus_lem-tab-! (x :: xs) | p = lem-vec-eq-decompose x x {! !} xs (refl , p)07/07 22:19
_Cactus_my god07/07 22:20
_Cactus_lem-tab-! (x :: xs) | p = lem-vec-eq-decompose x x (tabulate (_!_ xs)) xs (refl , p)07/07 22:20
_Cactus_this typechecks07/07 22:21
_Cactus_does that mean the proof is sound?07/07 22:21
rocketmanummmm07/07 22:23
rocketmangood question07/07 22:23
rocketmanin theory.. I think it's supposed to mean: yes07/07 22:24
rocketmanbut Agda is really ad-hoc and buggy, don't trust it07/07 22:24
_Cactus_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
_Cactus_anyway, thanks for your help07/07 22:26
_Cactus_I'll look at the next excercise tomorrow. maybe I'll be back with more dumb questions :)07/07 22:26
_Cactus_bye07/07 22:28
--- Day changed Wed Jul 08 2009
--- Day changed Thu Jul 09 2009
-!- byorgey_ is now known as byorgey09/07 13:59
-!- iago is now known as Guest1175009/07 19:58
-!- Guest11750 is now known as iago09/07 19:59
-!- byorgey_ is now known as byorgey09/07 20:28
--- Day changed Fri Jul 10 2009
-!- byorgey_ is now known as byorgey10/07 02:09
* soupdragon thinks it's pointless to ask heri10/07 21:20
--- Day changed Sat Jul 11 2009
--- Day changed Sun Jul 12 2009
-!- byorgey_ is now known as byorgey12/07 19:35
--- Day changed Mon Jul 13 2009
--- Day changed Tue Jul 14 2009
-!- codolio is now known as dolio14/07 03:27
-!- TR2N is now known as X-Scale14/07 11:50
-!- codolio is now known as dolio14/07 14:11
soupdragonhttp://www.e-pig.org/epilogue/ !!!!!!!14/07 19:36
soupdragonyay14/07 19:36
soupdragonactivity14/07 19:36
copumpkinyeah :)14/07 19:44
* edwinb just spent the afternoon plotting Epigram hacking with Conor14/07 20:14
soupdragonoooh!!14/07 20:15
edwinbnote that I said "plotting" rather than "doing" ;)14/07 20:15
soupdragonthat's even juicyer14/07 20:15
edwinbhowever, it's more than we've achieved for a while14/07 20:16
soupdragonyou're still doing the erasure stuff?14/07 20:16
edwinbI haven't done any more than I ever did14/07 20:16
* soupdragon wonders what the scoop is then :)14/07 20:17
edwinbbut hopefully we'll get together next week to have a proper hacking session14/07 20:17
edwinbwe 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
edwinbit all seems quite easy. We just have to bother doing it ;)14/07 20:19
copumpkinedwinb: does he come on IRC?14/07 20:25
edwinbno14/07 20:25
edwinbhe says he has enough ways to waste time...14/07 20:25
edwinbI think I can understand that14/07 20:25
copumpkinlol14/07 20:26
--- Day changed Wed Jul 15 2009
-!- kosmikus_ is now known as kosmikus15/07 14:12
-!- TR2N is now known as X-Scale15/07 16:20
-!- codolio is now known as dolio15/07 22:15
--- Day changed Thu Jul 16 2009
-!- copumpkin is now known as pumpkin16/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 dolio19/07 03:45
-!- byorgey_ is now known as byorgey19/07 20:25
--- Day changed Mon Jul 20 2009
-!- byorgey_ is now known as byorgey20/07 02:37
-!- copumpkin is now known as pumpkin20/07 20:34
--- Day changed Tue Jul 21 2009
-!- copumpkin is now known as RichardStallman21/07 04:19
-!- RichardStallman is now known as copumpkin21/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 secs23/07 08:00
liyangCome on people, let's talk some Agda!23/07 14:19
stevanok. you start? :-)23/07 14:41
stevanhmm, new paper added to the wiki: http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html23/07 14:48
edwinbwe're too busy hacking Epigram to talk Agda ;)23/07 16:40
* soupdragon is reading the epig stuff23/07 18:07
* soupdragon ... will hack epigram for cake23/07 18:07
liyangI'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
soupdragonwhat do you mean Agda FFI23/07 18:57
liyangAgda to Haskell.23/07 18:59
soupdragonhmmm23/07 19:00
liyang(I'm not actually being serious. Considering I'll actually be *running* the resulting code...)23/07 19:00
soupdragonwhat ???23/07 19:00
copumpkinzomg running code? that is very inappropriate for this channel23/07 19:00
soupdragonnot actually being serious -- you're not really writing this23/07 19:01
liyangI apologise. I'd take this to #haskell, but it's a tad noisy.23/07 19:01
soupdragon:(23/07 19:01
liyangI'm writing the Haskell parts at least.23/07 19:01
liyangAlthough, 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
liyanghttp://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 dolio25/07 06:50
--- Day changed Sun Jul 26 2009
-!- codolio is now known as dolio26/07 22:54
--- Day changed Mon Jul 27 2009
-!- codolio is now known as dolio27/07 21:41
--- Day changed Tue Jul 28 2009
-!- byorgey_ is now known as byorgey28/07 17:48
soupdragonI want to do something with deptypes28/07 19:24
soupdragonhmmm28/07 19:24
soupdragonI still don't know what is going on with epigram28/07 19:25
soupdragonhow does it implement K?28/07 19:26
soupdragonI am really curious how people are doing K and having it reduce28/07 19:26
soupdragonthere should be a paper on OTT that I can understand28/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
soupdragonhave you read it dolio?29/07 00:18
soupdragon"Let's see how things unfold"29/07 00:19
dolioIt?29/07 00:23
soupdragonhttp://strictlypositive.org/ObsCoin.pdf29/07 00:23
dolioNo, haven't read it.29/07 00:24
dolioIs this going to be about how observational type theory solves the problem?29/07 00:26
soupdragonI think soo29/07 00:26
soupdragonI don't really get OTT yet29/07 00:26
dolioIt's like the Blade of dependent type theory.29/07 00:27
soupdragon:D29/07 00:27
dolioAnyhow, 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
dolioBut, it's good to know he's working out the details.29/07 00:30
soupdragon"extensional-like equality on functions" like more than just beta-eta?29/07 00:30
dolioI'm pretty sure you get 'forall x. f x == g x -> f == g'.29/07 00:30
soupdragonwoah29/07 00:31
dolioSince you can just add any consistent axiom to the propositional area.29/07 00:31
dolioAnd that certainly is consistent, if not intensionally provable.29/07 00:32
dolioThe 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
dolioMan, I want to see a new epigram with this stuff.29/07 02:07
edwinbyou'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 languages29/07 02:10
edwinbthe current version compiles to assembly via C29/07 02:10
edwinbit just lacks a high level front end...29/07 02:10
soupdragonoh! that sounds good29/07 02:11
dolioThat's pretty good.29/07 02:11
dolioMaybe it should compile to dependently typed assembly. :)29/07 02:11
edwinbargh! ;)29/07 02:11
dolioAlthough I suspect the appeal of that sort of thing is for actually writing assembly by hand.29/07 02:11
soupdragonhehehe29/07 02:11
edwinbI think the reason people go to HM languages is that it's cheap29/07 02:12
soupdragonlets replace java with epigram!29/07 02:12
edwinbwhereas writing a run-time system is supposedly harder work29/07 02:12
edwinbwhich is probably a fair point29/07 02:12
copumpkinI thought no one ever ran their programs around here29/07 02:18
edwinbwell we don't really need to29/07 02:18
edwinbwe already know they are correct after all29/07 02:18
copumpkin:P29/07 02:19
-!- codolio is now known as dolio29/07 04:50
--- Day changed Thu Jul 30 2009
-!- byorgey_ is now known as byorgey30/07 03:48
-!- rocketman is now known as soupdragon30/07 10:19
--- Day changed Fri Jul 31 2009
-!- byorgey_ is now known as byorgey31/07 19:59

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