--- Log opened Sat Aug 01 00:00:43 2009
--- Day changed Sun Aug 02 2009
--- Day changed Mon Aug 03 2009
--- Day changed Tue Aug 04 2009
Joker_iz_Sikhttp://random345.mybrute.com04/08 18:35
-!- copumpkin is now known as pumpkin04/08 22:10
-!- pumpkin is now known as copumpkin04/08 22:10
--- Day changed Wed Aug 05 2009
--- Day changed Thu Aug 06 2009
--- Day changed Fri Aug 07 2009
-!- byorgey_ is now known as byorgey07/08 19:19
yakovhey07/08 20:08
yakovguys, I've tried to compile Standard library with `make' at the top-level dir and it has failed with `agda: Command not found' and indeed there's no agda07/08 20:35
yakovI only have agda-mode batch executable to use with Emacs07/08 20:35
yakovwhat is plain `agda' might be? :-)07/08 20:36
* yakov is back07/08 21:27
yakovI've managed to install Agda-executable but anyway I could not compile simple one-liner `main = putStrLn "hello"' with following error ``/home/yakov/src/agda2/lib-0.2/src/Coinduction.agda:21,16-2007/08 21:28
yakovNot in scope:07/08 21:28
yakov  Set₁ at /home/yakov/src/agda2/lib-0.2/src/Coinduction.agda:21,16-2007/08 21:28
yakovwhen scope checking Set₁''07/08 21:28
yakovhere's plain Hello world which I've tried to Load http://hpaste.org/fastcgi/hpaste.fcgi/view?id=7989#a798907/08 21:29
yakovCould anybody take a look? I have agda from cabal-install07/08 21:30
--- Day changed Sat Aug 08 2009
--- Day changed Sun Aug 09 2009
-!- codolio is now known as dolio09/08 03:14
-!- byorgey_ is now known as byorgey09/08 19:20
--- Day changed Mon Aug 10 2009
-!- copumpkin is now known as TokenVillainCat10/08 04:31
--- Day changed Tue Aug 11 2009
-!- Irssi: #agda: Total of 10 nicks [0 ops, 0 halfops, 0 voices, 10 normal]11/08 00:43
Laneyhttp://lists.alioth.debian.org/pipermail/pkg-haskell-maintainers/2009-August/000101.html11/08 00:43
Laneywoop woop11/08 00:44
soupdragonThank you for your contribution to #agda.11/08 00:45
Laneyquite welcome11/08 00:46
liyangIs that a hashtag or are you referring to this IRC channel?11/08 00:46
liyangsoupdragon: seems that you already know how to twit.11/08 00:46
soupdragonI have been making fun of people for ussing twitter :p11/08 00:47
edwinb#apparently you #have to #tag #everything11/08 00:47
Laneyhttp://www.whatthetrend.com/11/08 00:48
liyangI'm waiting for the day when #twat will trend. http://liyang.hu/#twit11/08 00:50
stevanplease update us on epi2, edwinb? :-)11/08 00:53
edwinbI have no news since pigweek11/08 00:54
edwinbalthough I see some darcs activity11/08 00:55
soupdragonwhat will we doo!!!11/08 00:55
* soupdragon thinks we should have an 'what the hell is OTT' thing in #agda11/08 00:55
stevani'm not sure i understand it, but the practical implications of it seem very interesting11/08 00:57
liyangoblivious type theory.11/08 00:57
liyangBasically, you just discard any and all typing information and hope for the best.11/08 00:57
stevanwhat major changes, apart from OTT, will there be between epig 1 and 2?11/08 01:04
* soupdragon thinks they got generic programming down11/08 01:04
stevanhow so?11/08 01:06
liyangUniverses, and language support for making its use less likely to make one tear one's hair out. Note that I don't know what I'm talking about, though I'm sure edwinb will correct me.11/08 01:09
* soupdragon feels like it's time I implement dependent pattern matching11/08 01:09
stevanusing the method ulf does in his tutorial, except there is no need for merging map and fold now?11/08 01:09
soupdragonwhat?11/08 01:10
soupdragonhm11/08 01:10
stevandunno, just guessing :-)11/08 01:11
* liyang 's laptop is getting uncomfortably hot.11/08 01:13
stevani have a hard time grasping the intuition of depentent pattern matching... what's the difference? dot patterns? does epigram have a similar facility?11/08 01:30
soupdragonstevan did you use GADTs in Haskell?11/08 01:33
stevanyes11/08 01:33
soupdragonwell it's like that.. the constructor you see can refine the type of other data11/08 01:34
stevanyou mean that you get type info as you pattern match?11/08 01:36
soupdragonyes11/08 01:36
soupdragonwith GADTs that's not THAT interesting11/08 01:36
soupdragonwith dependent types there is a feedback, and Agda does it as dot patterns11/08 01:37
stevanwhat would happen if we didn't have dot patterns? the type checker wouldn't be able to infere as much info, yes?11/08 01:39
soupdragonI think the idea in epigram is, instead of writing out dot patterns .. when you make a refinement they get written for you11/08 01:42
stevanhmm, wouldn't that mean that they are inferable?11/08 01:44
soupdragonwell I think it's possible to do pattern matching without writing any .{}11/08 01:45
soupdragonI mean theoretically (not in Agda)11/08 01:45
stevanwonder what cayenne did...11/08 01:47
stevanhmm, it had explicit type annotations on every case expression... "the reason for having this type is that with DT it's not in general possible to figure out the type of the case expr"11/08 01:54
--- Day changed Wed Aug 12 2009
soupdragonksf lets talk about it here then12/08 00:02
ksfwell, I don't think there's anyone here who isn't in #haskell, too.12/08 00:03
ksfI'd rather use sexprs than smash my fingers repeatedly onto the keys to use unicode symbols that still suffer from name clashes...12/08 20:19
copumpkin:o12/08 20:19
stevanhuh?12/08 20:21
ksf⟦_*_⟧ : ℚ → ℚ → ℚ12/08 20:21
ksf⟦ ⟦ a % b ⟧ * ⟦ c % d ⟧ ⟧ = ⟦ a * c % b * d ⟧12/08 20:21
ksfdo you know how long it took me to type that?12/08 20:21
copumpkinif you used agda mode in vim, not long12/08 20:21
copumpkinI mean12/08 20:21
copumpkinemacs :P12/08 20:21
soupdragonhahahaaha12/08 20:21
soupdragonbut its sooo pretty come on it's worth it12/08 20:22
soupdragondoes vim have agda support?12/08 20:22
copumpkindon't think so, not sure why I confused them12/08 20:22
ksfhmmm I'd rather have * be a typeclass member and use it for rationals, too.12/08 20:23
copumpkinbut yeah, I wish haskell would use more unicode :P12/08 20:23
copumpkinksf: except we don't have typeclasses in agda :P12/08 20:23
ksfvim has unicode input, if you mean that.12/08 20:23
copumpkin(I hope that will change)12/08 20:23
ksfinfix syntax is kind of pointless if you have to bracket everything using mixfix.12/08 20:24
soupdragonksf you don't12/08 20:25
soupdragonbtw I find s-exps horribly awful for MLs ....12/08 20:25
soupdragonjust doesn't work well,  f x y z  style is much better12/08 20:25
ksfwell there's not _that_ much difference between f x y z and (f x y z)...12/08 20:26
soupdragonno12/08 20:26
soupdragon(((f x) y) z)12/08 20:26
ksfwell yes, that's what lisp syntax desugars into12/08 20:27
ksfah no.12/08 20:27
ksf(f . (x . ( y . ( z . nil))))12/08 20:27
soupdragonI don't like the mixfix though :(12/08 20:29
soupdragonNotations ala Coq are better..12/08 20:29
soupdragon(the type dependency is fixed with mixfix)12/08 20:30
soupdragonleft to rigth ..12/08 20:30
stevanbrowsing thru a book on constructive logic... they prove: ---P <-> -P... how would you do that in agda? p : forall {P} -> ---P -> -P ?12/08 20:52
stevan(plus the other way around also)12/08 20:53
soupdragonwell remember that ~P = P -> False12/08 20:59
soupdragonso you have to prove:12/08 20:59
soupdragon((P -> F) -> F) -> F) -> (P -> F)12/08 20:59
stevanyeah12/08 20:59
soupdragon= ((P -> F) -> F) -> F) -> P -> F12/08 20:59
soupdragonso we have to hyp,  a : ((P -> F) -> F) -> F), b : P12/08 21:00
stevanor P -> F -> F?12/08 21:00
soupdragonhuh?12/08 21:00
kosmikusit's a nice exercise12/08 21:01
kosmikusjust do the only thing you can do :)12/08 21:01
stevansoupdragon: does that mean we have to assume a and b?12/08 21:02
soupdragonno no12/08 21:02
soupdragonwhen you want to prove:12/08 21:02
soupdragonA -> B -> C12/08 21:02
soupdragonthis is proving C given hypothesis A and B12/08 21:03
stevanok12/08 21:03
stevanhmm12/08 21:03
stevani didn't know we hade b : P, but now i can see it12/08 21:04
soupdragonit's ((P -> F) -> F) -> F) -> (P -> F), you see is equal to ((P -> F) -> F) -> F) -> P -> F12/08 21:05
soupdragona bit confusing with the extra ()'s but once you unfold the def of negation and simplify that's what is left12/08 21:05
kosmikusbtw, the other way round is trivial. that even holds without the extra negation.12/08 21:10
ksf...as long as you don't define ((P -> F) -> F) -> T...12/08 21:11
kosmikus?12/08 21:12
ksfer ratther ((P -> F) -> F) -> P or ((P -> F) -> F) -> (P -> T)12/08 21:12
ksfdon't listen to me, though, I'm a logics nuab.12/08 21:13
kosmikusI was just saying that P -> ~~P holds constructively12/08 21:13
kosmikushence also ~P -> ~~~P12/08 21:13
kosmikuswhereas ~~P -> P is not true in constructive logic, whereas ~~~P -> ~P is12/08 21:14
stevansolved it using the following type: {P : Set} -> (f : P -> F -> F) -> (b : F) -> (p : P) -> F12/08 21:23
stevanseems it doesn't work with (f : --P) etc?12/08 21:23
kosmikusstevan: but that's not the same statement12/08 21:24
stevanhmm?12/08 21:26
soupdragonstevan,12/08 21:26
soupdragonwhy have you written this way12/08 21:26
stevanwhat way?12/08 21:29
soupdragonannotated the type with names12/08 21:29
stevanso i could refer to them12/08 21:30
soupdragonhm12/08 21:30
stevan(in here), the parenthesis around f seem to be needed otherwise the annotations are not needed...12/08 21:32
soupdragonbtw12/08 21:32
soupdragonif you define  ~_ P = P -> F12/08 21:33
soupdragonfor example..12/08 21:33
soupdragonyou may know this but  ~~~P doesn't work, it should be  ~ ~ ~ P12/08 21:33
stevanyea12/08 21:33
stevankosmikus: what do you mean it's not the same statement? i thought -P = P -> F, --P = P -> F -> F?12/08 21:33
kosmikusdoesn't matter, the main point is that (P -> F -> F) -> F -> P -> F is not the same as (((P -> F) -> F) -> F) -> P -> F12/08 21:34
kosmikusP -> F -> F is not (P -> F) -> F12/08 21:35
kosmikusif you use the notation soupdragon suggests, you won't get into trouble with the parentheses12/08 21:36
stevani use the Relation.Nullary definition btw12/08 21:38
kosmikusthat's the same except for the symbol12/08 21:39
stevanok, i got a solution for apa : (--P) -> F -> P -> F; apa f b p = F-elim f ((\p -> b) p))  but there is an unresolved meta in it... i can't figure out a solution at all for ---P, is it possible?12/08 21:46
soupdragon:(12/08 21:46
soupdragonwhat are you doing12/08 21:46
soupdragonI don't think you should write 'F'12/08 21:46
soupdragonit's only part of the def. of negation12/08 21:46
stevansorry, i can't follow12/08 21:48
soupdragonI mean why12/08 21:48
soupdragon(--P) -> F -> P -> F12/08 21:48
soupdragonbut not12/08 21:48
soupdragon(--P) -> F -> ~P12/08 21:49
soupdragon?12/08 21:49
stevansure, i expanded all negations first. trying to colapse them now... (starting with the first one)12/08 21:50
soupdragonwell, it's not quite right12/08 21:50
soupdragonthe F there is not good12/08 21:51
soupdragonbut expanding the negation is a bad idea anyway.. that's just soemthing that could happen in your mind12/08 21:51
stevanyes, that's why im trying to colapse them now :-) but it isn't going well...12/08 21:56
soupdragon:p12/08 21:56
soupdragondon't expaind them at all12/08 21:56
stevanit would be nice to have a feature that when you had; f a = ?  you could check the type of a or some function applied to a, that only works on globals (as in you could check the type of f or f applied to some function) now yes?12/08 22:29
stevani can't figure out how to do it without expanding the negations, could someone please show me?12/08 22:57
soupdragonum12/08 22:57
soupdragonyou want to prove:12/08 22:57
soupdragon~ ~ ~ P -> ~ P12/08 22:57
soupdragonis that right?12/08 22:57
stevanyes12/08 22:57
soupdragonso then go12/08 22:57
soupdragonproof : {P} -> ~ ~ ~ P -> ~ P12/08 22:58
stevanyes12/08 22:58
soupdragonor whatever it is that pleases agda today12/08 22:58
soupdragonthen remember what I said about the hyps,12/08 22:58
soupdragonwe can go:12/08 22:58
soupdragonproof = \pCont p -> ...12/08 22:58
soupdragonnow '...' has to be a proof of false (because if the ~ P bit)12/08 22:59
soupdragonp : P, and do you know the type of pCont?12/08 22:59
kosmikusoh. still the same topic :)12/08 23:00
soupdragonoh am I in the past?12/08 23:00
stevanpCont : ((P -> F) -> F) -> F12/08 23:03
soupdragonyeah12/08 23:04
soupdragonso like12/08 23:04
soupdragonyou want to prove F12/08 23:04
soupdragonlike kosmikus said... just follow your nose12/08 23:04
soupdragonit's got to be:12/08 23:04
soupdragonproof = \pCont p -> pCont ...12/08 23:04
soupdragonwith pCont being something with type (P -> F) -> F12/08 23:05
soupdragonnow p : P, you know what to do nexxt12/08 23:05
stevani need some x : (P -> F) -> F    or y : P -> F    and z : F    so i can do pCont x or pCont y z ?12/08 23:08
soupdragonyes x : (P -> F) -> F12/08 23:09
soupdragonyou have p : P so x is easy to define12/08 23:09
stevanfinally12/08 23:18
soupdragonstevan btw in a realy proof language you can solve things like this autonomously using a proof search tactic12/08 23:18
kosmikusbut then there's no learning effect ;)12/08 23:20
stevanthat step from P -> --P wasn't very intuitive for me... i was trying to introduce one negation at the time...12/08 23:20
soupdragonkosmikus, hm I think I learned this stuff pretty well without agda12/08 23:21
soupdragonstevan, btw12/08 23:23
soupdragonyou wanted to prove:  (P -> F) -> F12/08 23:23
kosmikussoupdragon: sure, I'm obviously not saying you need Agda, but you won't learn it by typing "auto" either ...12/08 23:23
soupdragonif you look at is as:12/08 23:24
soupdragon(->) (P -> F) F12/08 23:24
soupdragonthe head is (->)... so this MUST be a function/implication12/08 23:24
soupdragonthat means you can start with12/08 23:24
soupdragon\pToF -> ...12/08 23:24
soupdragonand then prove F with the context p : P, pToF : P -> F12/08 23:24
soupdragonwhen you have all that going on it's much clearer what do to I think12/08 23:25
* soupdragon isn't sure if Agda can display that sort of thing.. but I think it does12/08 23:25
kosmikusyes, in the emacs mode you can display the context for a goal12/08 23:26
stevanit's kinda obvious now. of course you can get --P from P.12/08 23:27
-!- codolio is now known as dolio12/08 23:29
stevani was trying to get the chunks y and z rather than the whole x at once... not seeing that P -> ((P -> F) -> F) is actually P -> (P -> F) -> F where you got all parts... anyways thanks.12/08 23:37
stevani'm taking a course in logic this autumn, if one were to postulate the laws that can't be proved construtivly, do you figure it would be useful or distractive to use agda?12/08 23:46
--- Day changed Thu Aug 13 2009
ksfi'd like to see automatic ascii <-> unicode mapping13/08 07:22
ksflike it works for "->" right now, just for every single unicode char that's used as ident.13/08 07:22
stevanwhat do you mean with automatic?13/08 07:23
ksfpre-defined.13/08 07:24
stevanthey all are?13/08 07:24
ksf...or simply _require_ ascii-equivalents to be defined alongside with unicode identifiers.13/08 07:24
copumpkinksf's on an anti-unicode coding crusade :P13/08 07:25
ksfwell I don't want to type 'DOUBLE-STROKE CAPITAL N' if I could just type Nat...13/08 07:25
stevan\bn13/08 07:25
stevan\r is smoother than \-> also13/08 07:26
ksfI'd even be willing to run a script over my sources to convert form Nat and Ratio to ℕ and  ℚ.13/08 07:27
stevani don't understand, it's the same number of keystrokes?13/08 07:28
ksf{-# SYNTAX ≥ >= #}13/08 07:28
ksfunicode is a bugger to input.13/08 07:28
stevanare you using emacs unicode input mode?13/08 07:29
ksfI'd rather smash my head repeatedly into a wall than suffer the agony of using emacs.13/08 07:29
copumpkinheh13/08 07:30
stevanwell no wonder then... with emacs it's smooth to insert unicode.13/08 07:31
ksfAh I see the .el file has definitions.13/08 07:31
ksfwhat about supporting yi instead of emacs?13/08 07:33
stevanare you using agda --interactive now?13/08 07:34
ksfthat and a quick makefile13/08 07:34
copumpkinemacs isn't that bad, I don't really enjoy it but I've started using it for agda only13/08 07:36
stevanit's an entirely different thing when you use agda from emacs13/08 07:36
copumpkinbecause it makes things so much easier :P13/08 07:36
ksfhey you could script yi in agda!13/08 07:36
stevanthere is a master project proposal to add agda mode to yi here, but nobody has wanted to do it yet13/08 07:38
stevanare you a vi user?13/08 07:51
kosmikusstevan: somebody should take it, really. yi is a cool editor, I can't understand why there's no student in Chalmers who'd want to work with it.13/08 08:06
stevanthere were two master projects on yi this year, one improving haskell mode and one added javascript mode13/08 08:11
stevanthe guy who did js mode actually started at agda mode, but backed out and choose js instead :-/13/08 08:12
kosmikushmm13/08 08:24
stevanhe didn't know agda well enough... i hope they introduce agda into more courses13/08 08:29
kosmikusUlf would probably be happy to do so13/08 08:38
stevani think he should atleast mention it in the AFP course which he teaches13/08 08:41
* liyang is amused by the earlier exchange13/08 14:31
* liyang was like that not so long ago, but then figured Emacs has its uses. He still uses Vim for everything else though.13/08 15:04
Laneyxword plx13/08 15:09
liyangwhere?13/08 15:14
-!- copumpkin is now known as TheHunter13/08 19:43
-!- TheHunter is now known as copumpkin13/08 19:43
-!- copumpkin is now known as TheHunter13/08 19:50
-!- TheHunter is now known as copumpkin13/08 19:50
--- Day changed Fri Aug 14 2009
-!- codolio is now known as dolio14/08 04:33
stevanhi all, if i want to prove: apa : forall x -> (P x -> Q x) -> (bepa : exists (\x -> P x)) -> exists \x -> Q x; apa x f (x' , px') = (x' , f px')  i run into the problem of x /= x'  which makes sense, but how can i get around it? do i have to change the bepa type into: exists \y -> x == y & P y  or is there a better way to do it? thanks.14/08 04:41
soupdragonapa : forall x -> (P x -> Q x) -> (bepa : exists (\x -> P x)) -> exists \x -> Q x14/08 04:41
soupdragonhmmmm14/08 04:42
soupdragonyou can'd prove this14/08 04:43
soupdragonI'm pretty sure you can't prove is let me explain why14/08 04:43
soupdragonimagine x : 2, and 0 : 2, 1 : 2 are the only valus14/08 04:43
soupdragonnow bepa might be, say  (0, prf)14/08 04:44
soupdragonbut if you  apa 1 : (P 1 -> Q 1) -> ...14/08 04:44
soupdragonso it's impossible to cast the prf14/08 04:44
soupdragonof couse you DO have (P x -> Q x) forall x... just it's not possible to use it :S14/08 04:45
soupdragonthat last bit is a little confusing and I think that deserves more thought, but...14/08 04:45
soupdragonif you just have (forall x -> P x -> Q x)  then you can complete the proof14/08 04:45
stevanhmm14/08 04:46
soupdragonaha,  <soupdragon> of couse you DO have (P x -> Q x) forall x... just it's not possible to use it :S -- that is not true, I was just bit mistaken14/08 04:47
stevanwould it be hard to prove the soundness and completeness of propositional logic?14/08 05:05
soupdragonyeah :P14/08 05:09
soupdragondo it14/08 05:09
dolioProbaly not.14/08 05:09
dolioAt least, taking cues from a book I recently got on mathematical logic.14/08 05:10
dolioBut they choose axioms specifically to make the proofs easy, apparently. :)14/08 05:10
soupdragoncan you give the formal statements for sound and completet14/08 05:11
stevansound : G |- A -> G ||- A, where |- == ->, yes?14/08 05:11
stevan(i know very little about this)   but, ||- would seem to me to be a data _||-_ ...  which captures the kripke semantics, yes?14/08 05:14
dolioSoundness is "∀{B} → ⊢ B → Tautology B"14/08 05:15
soupdragonyes14/08 05:15
dolioCompleteness is the reverse.14/08 05:15
soupdragonhm and it'll be an easy induction over the syntax (of open terms)14/08 05:16
dolioYeah.14/08 05:16
soupdragonokay it's not hard like I thought at first14/08 05:16
stevan(sorry i can't see unicode, i ought to fix that soon...), whats the second unicode char? forall {B} -> ? B -> Taut...14/08 05:17
dolio|-14/08 05:17
dolioI haven't actually bothered to get as far as the deduction theorem, though.14/08 05:19
soupdragononce you did proplog do lambda pi :)14/08 05:19
dolioFooling about with proofs about lists of premises and stuff gets you into stuff that reminds me of proofs about sorting being a premutation.14/08 05:20
dolioWhich is no picnic.14/08 05:20
dolioAlthough the deduction theorem is probably less arduous.14/08 05:20
soupdragonyeah one is happy that these things come in a std lib :P14/08 05:21
stevanin coq?14/08 05:21
soupdragonyeah14/08 05:21
dolioIf proving soundness and completeness is hard, that'd be the reason.14/08 05:21
soupdragonwould be an easy port14/08 05:22
soupdragonjust extract to haskell and then fix it up14/08 05:22
soupdragonooh someone should made Coq -> Agda thingy14/08 05:22
stevani found this permutation proof of insertion sort in coq some time ago, but failed to port it to agda: http://www.cs.nott.ac.uk/~txa/g54cfr/l14.v14/08 05:24
soupdragonwell you must have Coq14/08 05:25
soupdragonfor snoc_perm you can Print snoc_perm and then you can see the proof14/08 05:25
stevanoh, learning a bit of coq probably wouldn't hurt me14/08 05:31
* soupdragon is still itching to implement DPM14/08 05:32
eriadorhello everyone14/08 09:48
Saizanhi14/08 09:48
eriadorI need some help with Agda input mode14/08 09:48
eriadorit doesn't seem to be working14/08 09:49
eriadoris there a way to manually turn it on?14/08 09:50
soupdragonany luck stevan?14/08 16:40
soupdragonwant to see your proofs if you wrote it :p14/08 16:40
ksfhttp://www.plpv.org/plpv07/obseqnow.pdf   why weren't I told such a thing exists?14/08 16:50
soupdragonheh you should get the glorious full color version14/08 16:50
--- Day changed Sat Aug 15 2009
-!- opdolio is now known as dolio15/08 00:37
stevanhi15/08 05:12
soupdragonhi15/08 05:12
copumpkinhi15/08 05:13
stevansoupdragon: you were asking if i had any luck? which problem were you refering to :-p?15/08 05:14
soupdragonyour idea for proplog15/08 05:19
stevani first thought i could do it using agda terms directly, as in G |- P -> G ||- P where |- would simply be agdas ->... it seemed to me you guys were suggesting to model prop logic as a data type first?15/08 05:27
stevanbut like i said, i dunno anything about these things15/08 05:28
soupdragonyeah I think it must be [[ G ]]' |- [[ P ]]15/08 05:28
soupdragonwhere [[ _ ]] interpet syntax into (Agda) semantics15/08 05:29
soupdragonbut ||- can be a syntactic relation15/08 05:29
stevanseems sensible15/08 05:32
stevanand G would be a list of some kind?15/08 05:33
dolioI've been fooling with some propositional logic, but I ran into an impasse on the proof of the deduction theorem.15/08 05:36
dolioBecause the one in my book uses induction on the length (in number of statements statements) of deductions, and I've been using lists of deductions.15/08 05:37
dolioSo I run into termination checker violations.15/08 05:37
soupdragonit is possible to do induction on the length like that using an accessability predicate, rather a lot of tedium to have it work though15/08 05:38
dolioYeah, exactly my concern. :)15/08 05:39
soupdragonthen use Coq :)15/08 05:39
dolioMaybe sized types can help.15/08 05:39
soupdragonI've not understood how sized types are anything different than just indexing your data by a number type15/08 05:40
soupdragonis there some important difference?15/08 05:40
dolioIt has built-in support that makes it somewhat nicer.15/08 05:40
dolioBut I'm not really clear on how exactly you use them.15/08 05:41
soupdragonI think an important thing for a new DT language is being able to add new language constructs15/08 05:41
soupdragon(at least in some much more convenient and more to the point verified way .. than currently015/08 05:41
dolioLike, there's an infinity element, that unifies with 'succ s'.15/08 05:42
dolioAnd some kind of constraint solver or something, I think.15/08 05:42
soupdragonall the stuff they did in foetus about mutual recursion termination has been implementend in Agda I think15/08 05:45
soupdragonI guess the constraint stuff really matters when you don't have any automation15/08 05:45
stevani seen some twelf examples when they do something like: data Expr ... Lam (Expr -> Expr). that sort of thing wouldn't count as positive in agda, yes? how does twelf solve that? could sized types help here?15/08 05:58
-!- Saizan_ is now known as Saizan15/08 07:06
soupdragonyeah I can't remember why HOAS is okay in twelf15/08 20:44
soupdragonprobably because there's no reduction ?15/08 20:48
--- Day changed Sun Aug 16 2009
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=8224#a822416/08 05:21
soupdragonhmf16/08 05:23
soupdragonI don't have agda set up16/08 05:24
soupdragonis there an easy way to install it yet?16/08 05:24
dolioAgda is displaying blatant anti-recursion bigotry. :)16/08 05:24
doliocabal install works.16/08 05:24
soupdragonhaha16/08 05:24
soupdragonzsh: command not found: cabal16/08 05:24
soupdragonhey so what's the deal?16/08 05:46
soupdragonyou have wf-induction16/08 05:47
soupdragonwhy wf-induction'?16/08 05:47
soupdragonoh it's because it's a function rather than a data16/08 05:48
dolioYeah. <' is a recursive type definition.16/08 05:49
soupdragonhelper : ∀ {n m m'} → m <' n -> m' ≤' m -> s m' ≤' n16/08 05:54
soupdragonif you can write that... then it works16/08 05:54
soupdragonlike  wf-aux' (s n) (s m) m<'n = p (s m) (λ m' m'-leq-m → wf-aux' n m' (helper m<'n m'-leq-m))16/08 05:54
dolioOh, yeah.16/08 05:59
dolioThat's just transitivity, though. With a specialized type to make things not blow up.16/08 06:00
soupdragonis it :S16/08 06:01
soupdragonI can't prove it16/08 06:01
dolioYou might run into the same problem trying to write helper.16/08 06:02
soupdragonthat'sweird16/08 06:13
soupdragonhelper : ∀ {n m m'} → s m ≤' n -> m' ≤' m -> s m' ≤' n16/08 06:13
soupdragonhelper {n} {m} {m'} p q = ≤'-trans {s m'} {s m} {n} q p16/08 06:13
soupdragonworks16/08 06:13
soupdragonhelper {n} {m} {m'} p q = ≤'-trans q p16/08 06:14
soupdragondoesn't16/08 06:14
soupdragonI guess it's just a type inference not being complete enough thing16/08 06:14
dolioHuh.16/08 06:15
stevanhi, i'm clueless about well-founded induction, but i have seen it in the std lib (Data.Nat and Induction.Nat), might help?16/08 06:16
copumpkinone thing I was wondering today is how could you express "if you sum the outputs of this function over its entire domain, the sum is 1" in types?16/08 06:16
soupdragonwell-founded induction is a work of genious  ...16/08 06:17
dolioIt's not really a problem with implementing it. It's just an oddity with a recursive definition of <= on naturals that I happened across while writing it.16/08 06:17
soupdragoncopumpkin: I think it would have to have a finite domain16/08 06:17
soupdragonor you're doing some calculus thing..16/08 06:17
copumpkinI can live with that, but then what?16/08 06:17
dolioI need to fill in something with type "s m' <= s m", but agda keeps reducing my values to have type "m' <= m", and then complaining about it.16/08 06:18
copumpkinwell, I originally thought of it as a continuous probability distribution16/08 06:18
copumpkinbut a finite domain isn't the end of the world16/08 06:18
soupdragondolio: well I think with a better type inference the obvious def would typecheck16/08 06:18
copumpkinhow would you go about modeling reals in a language like agda by the way?16/08 06:19
soupdragonlook at how it's done in Coq16/08 06:19
soupdragonwould not even attempt in agda16/08 06:19
copumpkinpainful?16/08 06:19
soupdragonjust insanity16/08 06:20
stevanhttp://wiki.portal.chalmers.se/cse/pmwiki.php/CS/ExactRealNumberComputationInAgda16/08 06:20
copumpkinoh lookie http://repository.ubn.ru.nl/bitstream/2066/32281/1/certextrr.pdf16/08 06:23
soupdragonbtw well founded is quite simple too16/08 06:56
dolioI must confess, I had to look up how to prove it. I failed to do so on my own.16/08 06:57
dolioAlthough in retrospect, I came fairly close.16/08 06:58
soupdragonoh I mean the inductive definition16/08 06:58
soupdragonwoah wait a sec16/08 07:05
soupdragonI was talking about the Acc data whose eliminator gives this kind of recursion16/08 07:06
soupdragonjust realize that you didn't use one!16/08 07:06
soupdragonI suppose that is possible because of pattern matching16/08 07:07
dolioI just wrote what you get if you eliminate out all the Acc stuff.16/08 07:10
soupdragonyeah that's wild I've never seen that16/08 07:10
soupdragondata Acc (x : A) : prop where16/08 07:20
soupdragon below : (forall {y : A} -> y R a -> Acc y) -> Acc x16/08 07:21
soupdragonoops16/08 07:21
soupdragon below : (forall {y : A} -> y R x -> Acc y) -> Acc x16/08 07:21
soupdragonthat's the one I am used to16/08 07:21
soupdragonyou can show that WF R -> WF (transitive_closure R)16/08 07:21
soupdragonif R is just forall n, n R (S n), then transitive_closure R = (<)16/08 07:22
dolioWell, doing it that way is probably more useful, since it sets up infrastructure for reusing things.16/08 07:22
soupdragonyeah I'd like to implement DPM this way16/08 07:23
soupdragonit's a bit tricky to support dependently typed data though16/08 07:23
soupdragontelescopes and all that16/08 07:23
dolioAlthough I don't think it technically saves you any typing on the one side, since every time you write "well-founded-induction-with-R", you instead write "proof-of-well-foundedness-of-R".16/08 07:25
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=8234#a8236 Finally!16/08 12:36
stevannice, add it to the wiki?16/08 12:59
dolioI still need to do soundness and completeness.16/08 13:03
dolioWhich also use well-founded induction in my book, apparently.16/08 13:04
dolioMuch to my chagrin.16/08 13:04
dolioActually, the completeness theorem doesn't, but it's even funkier.16/08 13:05
stevanhow does well-founded differ from normal induction? what does it do that helps you with your proof?16/08 13:07
dolioNormal Agda induction lets you make a recursive call as long as one of the arguments is being supplied a sub-structure of what was given in that argument.16/08 13:10
dolioSo in "foo (s n) = bar (foo n)" the recursive call is okay because it's called with 'n', when 's n' is passed in.16/08 13:10
stevanyes16/08 13:11
dolioHowever, I need to make recursive calls like "foo n = foo (bar n)" where 'bar n' is in fact a sub-structure of n, but there's no way for the termination checker to figure that out.16/08 13:12
stevanoh16/08 13:12
dolioHowever, it's easy to make bar return a proof that what it returns is shorter than what it receives.16/08 13:12
dolioSo well-founded induction gives you "(forall v (forall v' -> v' is shorter than v -> P v')) -> (v : T) -> P v".16/08 13:14
dolioOops, I messed that up slightly.16/08 13:14
dolioAnyhow, it gives me more liberty with my recursive calls.16/08 13:15
stevani see, i have to try that out16/08 13:17
dolioIn my book, both the deduction and soundness theorems look like, "if |- B, then there must be some deduction B_1 ... B_n." and then do induction on n, and in the modus ponens case, there are i and j less than n for which you need the theorem to hold.16/08 13:20
dolioWhich is pretty simple, but doesn't really translate to structural recursion in Agda.16/08 13:20
stevando informal proofs ever deal with well-founded induction, given that they can come away with it being obviously smaller?16/08 13:30
stevanwould be nice to have a "paste bin" for agda which would simply generate the html... i wonder if there are any security risks involved?16/08 13:46
soupdragon    = begin16/08 21:09
soupdragon       - T         ⟨ axiom ⟩16/08 21:09
soupdragon       - T ⊃ A ⊃ T ⟨ axiom₁ ⟩16/08 21:09
soupdragon       - A ⊃ T     ⟨ modus-ponens now (before now) ⟩16/08 21:09
soupdragon       ∎16/08 21:09
soupdragonvery nice16/08 21:10
--- Day changed Mon Aug 17 2009
-!- codolio is now known as dolio17/08 03:26
-!- pumpkin is now known as copumpkin17/08 23:03
--- Day changed Tue Aug 18 2009
-!- copumpkin is now known as newbie18/08 01:22
-!- newbie is now known as copumpkin18/08 01:29
-!- EnglishGentv2 is now known as contrapumpkin18/08 18:04
-!- contrapumpkin is now known as copumpkin18/08 18:40
--- Day changed Wed Aug 19 2009
--- Day changed Thu Aug 20 2009
-!- Saizan_ is now known as Saizan20/08 09:16
greenrdI am trying to use a "with" clause, but I'm getting this error:20/08 15:58
greenrdMissing type signature for left hand side … | refl20/08 15:59
greenrdThere's no type signature for the with clause in these examples: http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.With-expression20/08 16:00
greenrdIs this something that's changed, or is it only needed for certain with clauses?20/08 16:01
stepcutwhen I invoke agda2-load and aga2-compile, I get a message like, Wrote /tmp/agda2-mode17066AfT, but nothing else happens. It used to work, but I think there is something I had to do get things started...20/08 16:03
stepcutmaybe I should just upgrade everything, my installing is a bitold20/08 16:06
greenrdhmm, I get the same error I got before, with the examples from the reference manual20/08 16:16
greenrdfiled it as a bug: http://code.google.com/p/agda/issues/detail?id=18920/08 16:20
-!- eldragon2_ is now known as eldragon220/08 16:29
soupdragonliyang20/08 22:41
soupdragonI have something for you20/08 22:41
soupdragonthis --> ヽ(。_°)ノ20/08 22:41
--- Day changed Fri Aug 21 2009
-!- ksf_ is now known as ksf21/08 18:55
--- Day changed Sat Aug 22 2009
copumpkinhmm, when I try to compile an agda module with only the module ... where line in it22/08 20:32
copumpkinafter I just installed the latest version22/08 20:32
copumpkinmy emacs freezes up completely22/08 20:32
copumpkinnothing's pegging the CPU or anything22/08 20:33
-!- copumpkin is now known as valleypumpkin22/08 22:06
-!- valleypumpkin is now known as copumpkin22/08 22:09
--- Day changed Sun Aug 23 2009
stepcutI am trying to translate this code in agda, http://contracts.scheming.org/#process-prims23/08 23:37
stepcutbut it relies on lazy infinite lists. So, I am thinking I need to look into using codata ?23/08 23:37
rocketmanstepcut why into agda?23/08 23:38
stepcutrocketman: hopefully to prove that it is correct? Mostly a learning experience...23/08 23:39
rocketmanyou trust agda proofs?23/08 23:40
stepcutno23/08 23:40
copumpkin:o23/08 23:41
stepcutI should change that from 'Mostly' to 'Entirely'23/08 23:43
rocketmanI think it's crazy anyone uses Agda for more than prototyping or playing like a sandbox23/08 23:44
stepcutwell, right now I do all my real work in Haskell -- but maybe that is because I don't know agda very well yet ;)23/08 23:44
edwinb"Playing like a sandbox" == "Research" ;)23/08 23:45
stepcut.. or maybe it's because Epigram 2 isn't out yet :p23/08 23:45
edwinbI think we're at least onto Epigram 3 now23/08 23:46
stepcutheh23/08 23:46
copumpkinedwinb: how's that going? I got all excited by the epilogue posts, but then they stopped :(23/08 23:46
edwinbI don't know, we all went on holiday23/08 23:46
copumpkinah :)23/08 23:47
rocketmanget back to work!!!23/08 23:47
edwinbthat was a nice burst of activity23/08 23:47
edwinbBack tomorrow ;)23/08 23:47
copumpkinooh23/08 23:47
rocketmanaw sorry23/08 23:47
dolioThe "process primitives" section all looks doable with codata.23/08 23:47
dolioAt a skim.23/08 23:47
stepcutdolio: spiffy. Now I just need to read this presentation on codata :)23/08 23:47
edwinbI hope and expect ICFP to prompt a burst of activity23/08 23:47
edwinbor possibly just a lot of hot air, who knows23/08 23:47
dolioAlthough timeSlices is a bit weird.23/08 23:48
rocketmanthe next ICFP contest: Implement epigram23/08 23:48
* edwinb looks forward to the day an Epigram program wins it ;)23/08 23:48
* stepcut too.23/08 23:48
* rocketman wishes james would publish some PhD thesis :/23/08 23:49
edwinbwhich James?23/08 23:49
copumpkinjames?23/08 23:49
rocketmanah excellent!23/08 23:49
rocketmanhttp://cs.ioc.ee/~james/PUBLICATION.html23/08 23:49
rocketmanhe has put it up23/08 23:49
edwinbah, that james23/08 23:49
edwinbI was going to say it ought to be available since he's graduated now!23/08 23:50
rocketmantait2 is good as well23/08 23:51
rocketmanedwinb, by the way do you know what the plans are for editing epigram?23/08 23:51
rocketmanlike it's going to be xemacs again :/ or something else23/08 23:52
edwinbEpigram itself will be text23/08 23:52
* rocketman (wishes for some kind of interactive TeX editor)23/08 23:52
edwinbbut set up so that if anyone wants to make a nice front end, they're welcome to make one23/08 23:52
copumpkinmmm23/08 23:52
dolioAt least we already got she out of Conor's epigram musing.23/08 23:52
rocketmanmight have a bash once there's a build that does something good23/08 23:52
edwinbEpigram is being implemented in She, naturally23/08 23:53
rocketmanatm I don't know how to use ecce or whatever23/08 23:53
dolioIt already looks like it's got some nice stuff.23/08 23:53
copumpkinedwinb: any short-term plans to cram she into the 6.12 GHC release? (/me crosses his fingers) :P23/08 23:53
edwinbI don't believe so23/08 23:53
edwinbalthugh GHC HQ are being kept informed23/08 23:53
stepcutwhat is she? (it's a bit hard to google)23/08 23:54
edwinbyou probably wouldn't find much anyway...23/08 23:54
copumpkin@hackage she23/08 23:54
edwinbit's a preprocessor for GHC23/08 23:54
copumpkinomg no lambdabot23/08 23:54
edwinbthat does various bits of type magic23/08 23:54
stepcutcopumpkin: need agdabot...23/08 23:54
copumpkinyeah :)23/08 23:54
edwinbhttp://www.e-pig.org/epilogue/?p=21223/08 23:55
* rocketman thinks most of the people here grew out of writing an IRC bot in every language they use23/08 23:56
rocketmanwhich is the problem.. :/23/08 23:56
* copumpkin is amazed by http://personal.cis.strath.ac.uk/~conor/pub/she/examples/Vec.lhs23/08 23:56
copumpkinI was trying to write that by hand the other day and it's a pain to get GHC to accept a definition for vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x23/08 23:57
--- Day changed Mon Aug 24 2009
stepcutthis Colist.agda module is very musical ... ♯ and ♭ all over the place..24/08 00:11
stepcutwhat do ♯ and ♭ mean ?24/08 00:14
copumpkinit's from Coinduction24/08 00:14
* edwinb wonders if he has the wrong character set on this terminal24/08 00:14
copumpkin(those are sharp and flat characters)24/08 00:15
stepcutcopumpkin: ah, thanks24/08 00:15
edwinbThis is one reason I'm not keen on gratuitous use of unicode in Agda...24/08 00:15
copumpkinstepcut: the documentation should be hyperlinked24/08 00:15
rocketmanUTF-8?24/08 00:16
edwinbit's too easy to make up crazy identifiers with no obvious meaning24/08 00:16
edwinbalso, I never know how to set up my terminal or emacs...24/08 00:16
stepcutcopumpkin: I guess I should find the documentation instead of just looking at the source. thanks.24/08 00:16
copumpkinstepcut: oh that's what I meant :P I don't think there's much documentation24/08 00:16
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Coinduction.html#42224/08 00:16
doliostepcut: The short version is that there's problems with using codata in a naive way similar to pattern matching and lazy evaluation in Haskell.24/08 00:17
stepcutcopumpkin: well, I am looking at the source files directly in emacs right now, so..24/08 00:17
doliostepcut: But those problems are solved by following a discipline where all codata values have a single 'observe' function that yields a shape functor for the codata.24/08 00:18
dolioSo either flat or sharp is the observe function, I forget which.24/08 00:18
dolioAnd the other one is the corresponding codata constructor.24/08 00:18
stepcutok24/08 00:19
stepcutis this similar to using newtypes in Haskell to avoid issues with infinitely recursive types?24/08 00:20
rocketmann.a.d's parsing stuff goes into a bit of detail about this doesn't it?24/08 00:21
rocketmanor is it ulf :/24/08 00:21
rocketmanhttp://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinators.pdf24/08 00:22
doliostepcut: Due to the discipline you follow to make codata follow the actual categorical coinduction, you only ever need one 'codata' declaration, I think.24/08 00:23
rocketmanI don't see any use of ♯ or ♭ in that actually... but they use  ~  in a pattern match24/08 00:23
doliostepcut: Instead you declare something similar to the shape functor (not quite), and use the single coinduction type in it. So it's similar to defining a fixpoint newtype.24/08 00:24
stepcutdolio: ok, I vaguely understand. I have played around with fixpoint newtypes before24/08 00:25
stepcutColist.agda as replicate but not repeat. Is that because you would just define, repeat = replicate ∞ℕ ?24/08 00:48
dolioDoes replicate use conat?24/08 00:49
stepcutreplicate : ∀ {A} → Coℕ → A → Colist A24/08 00:49
dolioThen, yes, you can use infinity. :)24/08 00:50
stepcutthat's cool24/08 00:50
stepcutsweet, got konstSlices implemented. next time: timeSlices.24/08 01:16
-!- British0zzy_ is now known as British0zzy24/08 01:23
stepcutare there any example of heterogenous lists (or similar) in agda?24/08 01:26
dolioWhat do you mean by that?24/08 01:37
dolioDynamic type stuff, or more like HList?24/08 01:37
rocketmanstepcut use tuples24/08 01:44
rocketman(a, (b, (c, ())))24/08 01:44
rocketmanhttp://www.eecs.harvard.edu/~nr/cs252r/archive/conor-mcbride/epigram-pearl.pdf24/08 01:48
rocketmanstepcut24/08 01:48
stepcutdolio: more like HList24/08 01:53
copumpkinrocketman: 40324/08 01:53
rocketmanhttp://muaddibspace.blogspot.com/2008/06/correctness-of-expression-compiler-in.html24/08 01:53
doliostepcut: Then they're essentially tuples, as rocketman said. Although you can make type lists and an inductive family indexed by them if youw ant.24/08 01:53
rocketmanstepcut look at INST24/08 01:53
stepcutok24/08 01:56
rocketmandoes it make sense?24/08 02:07
stepcuthaven't looked to deeply yet, was practicing tai chi24/08 02:09
stepcutI think the interesting part of HList is be able to do things like write a function that takes an HList that has exactly one element of a certain time, and then extract the value of that type.24/08 02:10
rocketmanI think HList SUCKS24/08 02:10
rocketman:)24/08 02:10
dolioWell, yeah, in that sense, HList is a full implementation of extensible records.24/08 02:11
stepcutwell, HList in Haskell does pretty much suck. Hence my interest in finding out what Agda can provide instead ;)24/08 02:11
rocketmanwell that post has some things you can do24/08 02:12
stepcutok24/08 02:12
stepcutI'm not really running into a problem that needs heterogeneous collections at the moment, so maybe I'll hold off until I know what I actually want24/08 02:12
stepcutmy next challenge will be translating this into agda:24/08 02:13
stepcuttimeSlices :: (Num t, Enum t) => [(s, t)] -> [[(s, t)]]24/08 02:13
stepcuttimeSlices sl@((s,t):_) = sl : timeSlices [(s,t+1) | _ <- [0..t+1]]24/08 02:13
copumpkin:o24/08 02:13
stepcutto some sensible degree.24/08 02:13
rocketmanwhy don't you read the thing I linked24/08 02:13
dolioThat one might not actually be possible.24/08 02:14
stepcutrocketman: the correctness of expression or the epigram pearl?24/08 02:14
rocketmanhttp://muaddibspace.blogspot.com/2008/06/correctness-of-expression-compiler-in.html24/08 02:14
dolioActually, scratch that, it looks productive.24/08 02:14
rocketmanparticulary INST and things that use INST24/08 02:14
copumpkindolio: what kinds of things aren't possible?24/08 02:14
stepcutrocketman: ok24/08 02:14
doliocopumpkin: Things that aren't guarded corecursion, without a fair amount of work, at least.24/08 02:15
copumpkinah24/08 02:16
dolioI was thinking of inductive data for a second there, though, where that function looks bad.24/08 02:18
dolioSince timeSlices is called in a way that's not structurally recursive.24/08 02:19
Saizanis the criteria used to check productivity documented somewhere?24/08 02:22
dolioProbably somewhere.24/08 02:24
Saizanheh24/08 02:24
dolio:)24/08 02:24
rocketmanwww.cs.nott.ac.uk/~nad/publications/danielsson-aim9-talk.pdf24/08 02:30
dolioIt's something like: recursive calls must be the arguments to a co-constructor.24/08 02:31
dolioOr, corecursive. :)24/08 02:31
rocketmanthe talk talks about it a bit24/08 02:32
rocketmanthey use a bad way24/08 02:32
rocketmanConor has a new way24/08 02:32
copumpkinnstructor?24/08 02:32
rocketman:|24/08 02:32
dolioThe problem with my example criteria is that it sucks for actually writing functions.24/08 02:35
dolioLike "fibs = 1 : 1 : zipWith (+) fibs (tail fibs)" doesn't qualify.24/08 02:35
rocketmandoes that work in agda?24/08 02:36
dolioNo.24/08 02:36
Saizanah, you need something like complete induction, but for co-induction?24/08 02:36
dolioYou have to use some finessing to make it guarded.24/08 02:37
dolioLet me see if I can remember how to do it.24/08 02:37
rocketmanCoq doesn't accept it either24/08 02:40
rocketmanI never use coinductives so I don't know what to di24/08 02:40
rocketmando*24/08 02:40
dolioWell, I seem to be drawing a blank now.24/08 02:44
rocketmanI tried to make fibs and fibs' (fibs = tail fibs) corecursive but that didn't work either24/08 02:45
dolioI thought you could do something like "fibs = 0 :: zipWith _+_ fibs (1 :: fibs)", but that's not passing the checker.24/08 02:45
dolioWhich I acknowledge doesn't satisfy my criterion, either, but I thought the trick was something like that.24/08 02:45
rocketmanwell I guess this is a puzzle :)24/08 02:47
dolioThat doesn't work in Coq, I assume?24/08 02:47
rocketmanthinking about:24/08 02:47
rocketmanlist = 1 :: 2 :: 3 :: drop 1 list -- ok24/08 02:47
rocketmanlist = 1 :: 2 :: 3 :: drop 2 list -- ok24/08 02:47
rocketmanlist = 1 :: 2 :: 3 :: drop 3 list -- bad!24/08 02:47
rocketman(list not having a nil, in this case)24/08 02:47
rocketmanCoFixpoint fibs := cons 0 (zipWith plus fibs (cons 1 fibs)).24/08 02:48
rocketmanis not let trough24/08 02:48
rocketmanthrough24/08 02:48
stepcutDoes this function terminate, and why ?24/08 02:51
stepcuttake5 : ∀ {A} -> A -> BoundedVec A 524/08 02:51
stepcuttake5 x = take 5 (replicate ∞ℕ x)24/08 02:51
stepcut 24/08 02:51
dolioAgda doesn't even like "fibs = 0 :: zipWith _+_ (1 :: fibs) ?"24/08 02:51
rocketmanI don't have agda24/08 02:52
copumpkinmy agda is broken somehow24/08 02:52
rocketmanoh yes I do actually24/08 02:52
doliostepcut: Why wouldn't it?24/08 02:52
stepcutdolio: In something like ML, it wouldn't because replicate would have to be fully evaluated before the take 5. In Haskell it would due to lazy evaluation. I assume it will in Agda, but I am not really clear why...24/08 02:53
dolioCoinductive types have evaluation characteristics that are similar to lazy evaluation.24/08 02:54
stepcutdolio: but it's not actually lazy evaluation?24/08 02:54
dolioOr, more specifically, if 't' is a term of coinductive type, it is never subject to further evaluation.24/08 02:54
dolio'replicate ∞ℕ x' doesn't reduce to anything.24/08 02:55
dolioIt's only "observe (replicate ∞ℕ x)" which is subject to reduction (observe being flat, or whatever).24/08 02:55
dolioAnd it reduces to 'x :: replicate ∞ℕ x' or something similar.24/08 02:56
dolioAt least, that's what you'd expect from the categorical formalism. When you actually pattern match on co-constructors, the above isn't true, which leads to oddities.24/08 02:57
stepcutI guess I feel a bit 'lost' because I have written a basic stg to assembly compiler before, so I sort-of know how Haskell works under the hood, and how laziness actually works in practice. With agda it how it works is magic, even if I understand what is supposed to happen :)24/08 02:59
rocketmanjust ignore how it works24/08 02:59
stepcutyeah, I don't really need to know how, it just feels funny not to ;)24/08 02:59
dolioIf you want further explanation of the semantic stuff..24/08 03:02
dolioInductive data is about how things are built up, which gives you constructors, and case distinction. And all values are made out of one of the constructors (except in Haskell, which is evil, and has fix).24/08 03:03
dolioCoinductive data isn't about what things are built of, but what observations you can make on a given value. So it's not correct to say that you can do a case distinction on a coinductive value, or evaluate it to see what constructor it's made of.24/08 03:05
dolioAll you can do is make an observation, and see what that returns. They're kind of like functions in that way. All you can do with a function is apply it to something of the right type.24/08 03:05
dolioExcept in Haskell, which is evil and has seq. :)24/08 03:06
stepcut:P24/08 03:06
dolioAnd in dependently typed languages, problems arise when you treat coinductive data like it is built out of co-constructors, even though that seems like a natural way to write code.24/08 03:07
rocketmanis there something like Acc for codata?24/08 03:07
dolioBecause then you do get coinductive values evaluating to constructors, which can change the types of other values (since values can appear in types), but the type system still doesn't treat "v :: replicate (n-1) v" as being equal to "replicate n v", because, strictly semantically speaking, they're not the same.24/08 03:08
stepcutso when you observe a coinductive value like (replicate ∞ℕ x), you get back a value like, (x :: replicate ∞ℕ x). You can pattern match on that and extract the value x and another coinductive value replicate ∞ℕ x ?24/08 03:09
dolioRight.24/08 03:09
stepcutso, this gives you the ability to some of the nifty laziness type things, like infinite lists. But you don't need things like seq.24/08 03:10
doliorocketman: I don't know. Presumably there's something dual.24/08 03:10
rocketmanwell I don't know I never came across such a thing24/08 03:11
dolioNor have I. Coinduction seems much less explored than induction, though, so that's probably not surprising.24/08 03:11
dolioI don't really have any ideas for the fibonaccis. I could have sworn it was "fibs = 0 :: zipWith _+_ fibs (1 :: fibs)", but now I'm not sure why that'd be accepted.24/08 03:14
rocketmanyou can do fibs = map fib nats :p24/08 03:14
rocketmanbut that's obviously avoiding the problem24/08 03:14
dolioMaybe the termination checker used to be more lenient.24/08 03:14
stepcutdolio: i think it works for me. No compiler errors, though emacs did highlight fibs in orange..24/08 03:17
dolioYeah. Orange means it failed the termination/productivity checker.24/08 03:18
rocketmanorange means it didn't work :p24/08 03:18
dolioIt's not actually a fatal error.24/08 03:18
stepcutah24/08 03:19
stepcutso, you can have infinite Lists not just infinite Colists ?24/08 03:19
-!- British0zzy_ is now known as British0zzy24/08 03:20
stepcutor is fibs a Colist ?24/08 03:20
dolioColist.24/08 03:21
stepcutmy Data.Colist (from lib-0.2) lacks a zipWith function24/08 03:21
dolioWell, I was writing my own.24/08 03:21
stepcutah ok.24/08 03:21
dolioI don't use the library that much. I like poking around on my own.24/08 03:22
stepcutfib : Prog ℕ24/08 03:27
stepcutfib = 0 ≺ ♯₁ zipWith _+_ fib (1 ≺ ♯₁ fib)24/08 03:27
stepcut 24/08 03:27
stepcutfrom24/08 03:27
stepcuthttp://www.cs.nott.ac.uk/~nad/repos/codata/StreamProg.agda24/08 03:27
dolioAnyhow, you can write 'fibs = unfoldr (\(i , j) -> (i , (j , i + j))) (0 , 1)' or something like that, but that's obviously not the point. :)24/08 03:27
rocketmanwhat about  fib = 0 ≺ 1 ≺ ♯₁ zipWith _+_ fib (tail fib)24/08 03:28
rocketmandoes something along those lines work?24/08 03:28
rocketman(maybe needs more/less/other ♯₁ I don't know about that)24/08 03:28
dolioWell, the whole point of the unusual version was that something about the 'zipWith _+_ fib (tail fib)' failed for some reason.24/08 03:29
dolioLike, it couldn't see that 'tail fib' was okay or something.24/08 03:30
soupdragondid you work out fibs yet?24/08 06:51
soupdragonCoFixpoint fibo_str (a b:nat) : stream nat := Cons a (fibo_str b (a + b)).24/08 06:52
soupdragonthat works but it's still not what we wanted24/08 06:52
dolioNo. I even tried that example you found, but it doesn't work anymore if it ever did.24/08 07:04
soupdragonthe fibo_str one?24/08 07:04
dolioThe one that actually uses the one-coinduction-type version with the sharps.24/08 07:07
dolioI had been using the more traditional naive coinduction version of colists.24/08 07:07
dolioBut it doesn't make a difference.24/08 07:07
soupdragonI am just wondering, if you forget type theory for a bit24/08 07:09
soupdragonHow would you prove this at all24/08 07:09
dolioAll what?24/08 07:10
soupdragonI mean just on paper, how would you formally prove the fibs thing24/08 07:10
soupdragonthe way I might do it is thinking about the object as a computation.. and show that there is no bottom in it24/08 07:10
soupdragonthat'd work in agda to but soooo much machinary to just get that list in24/08 07:10
dolioI don't know. You could probably use the coinductive analogue of well-founded induction. With some proof that 'zipWith f s t' is as productive as the least productive of s and t.24/08 07:12
dolioBut, then again, I don't know what that analogue is.24/08 07:13
soupdragonafaik there is no well-founded coinduction24/08 07:14
--- Day changed Tue Aug 25 2009
soupdragonupdates? :p25/08 02:52
--- Day changed Wed Aug 26 2009
-!- koninkje_away is now known as koninkje26/08 01:33
-!- koninkje is now known as koninkje_away26/08 02:58
soupdragonhttp://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html26/08 05:59
soupdragonpage 3 has fibs26/08 05:59
dolioWow.26/08 06:01
soupdragonwhat do you mean?26/08 08:11
dolioIt's rather involved.26/08 08:15
soupdragonit's simpler than my idea26/08 08:15
--- Day changed Thu Aug 27 2009
-!- codolio is now known as dolio27/08 10:22
-!- copumpkin is now known as AdmiralAckbar27/08 23:48
-!- AdmiralAckbar is now known as copumpkin27/08 23:48
--- Day changed Fri Aug 28 2009
-!- koninkje_away is now known as koninkje28/08 03:28
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=8758#a875828/08 07:45
soupdragonclever!!28/08 07:48
soupdragonI have failed to define that before because I was insisting that ≤ be decidible -- the way you use is so much simpler28/08 07:49
dolioCan you even have decidable ordering on ordinals?28/08 07:49
soupdragonprobably not :p  I think thats where I went wrong28/08 07:50
dolio:)28/08 07:50
soupdragonwhat programs do you write using transfinite? or what theorems can you prove28/08 07:50
dolioNone. I just wrote transfinite.28/08 07:50
soupdragonyou could do some nice consistency theorem28/08 07:51
dolioOr, I haven't written any, that is.28/08 07:51
dolioI'm not exactly sure what all ordinals you can represent, although I found a paper that seemed to talk about it in very fuzzy terms.28/08 07:51
dolioI think it may have been more like slides for a talk than an actual paper.28/08 07:52
dolioThey mentioned some ordinal omega^CK_1 that's the smallest ordinal you can't represent computably.28/08 07:52
soupdragonyeah I think the limit is mumble, and you need to use an inductive recursive thingy to make higher ones28/08 07:53
dolioBut I'm not sure if you can't represent any above it, or if it's spotty.28/08 07:53
soupdragonhttp://www.cs.nott.ac.uk/~pgh/nc.agda28/08 07:54
dolioThe slides/paper were also about how it was difficult to represent stuff like omega^omega and epsilon_0, but they don't seem that hard to me.28/08 07:54
dolioBut maybe I'm doing something wrong.28/08 07:54
dolioOh good, W.28/08 07:55
dolioI still haven't figured out W.28/08 07:55
dolioThis is apparently a different W than the one in Observational Equality, Now!28/08 08:24
soupdragonoh that's funny28/08 08:29
soupdragonI didn't expect that28/08 08:29
soupdragonit's not like a container version in Obs. Eq. ?28/08 08:29
dolioThe one in nc.agda has extra constructors.28/08 08:30
dolioW0 : W a T and WS : W a T -> W a T.28/08 08:30
copumpkinedwinb: you around?28/08 08:38
-!- koninkje is now known as koninkje_away28/08 09:02
-!- codolio is now known as dolio28/08 09:52
edwinbcopumpkin: hello28/08 10:16
-!- soupdragon is now known as sharada28/08 13:01
-!- byorgey_ is now known as byorgey28/08 21:33
-!- opdolio is now known as dolio28/08 23:18
--- Day changed Sat Aug 29 2009
* sharada wonders anyone around?29/08 07:54
sharadanobody in #coq :/29/08 07:54
sharadaI want to find out more about coinduction.. what shoudl I do?29/08 07:54
copumpkinthere's a good tutorial paper somewhere on it, but I can't remember what to look for29/08 07:55
copumpkinhttp://tfs.cs.tu-berlin.de/~wolter/papiere/tutorial.ps.gz29/08 07:58
-!- mode/#agda [+o sharada] by ChanServ29/08 07:58
-!- sharada changed the topic of #agda to: Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol. | Wiki: http://wiki.portal.chalmers.se/agda/ | Logs: http://agda.orangesquash.org.uk/ | http://news.gmane.org/gmane.comp.lang.agda29/08 07:58
-!- mode/#agda [-o sharada] by sharada29/08 07:58
sharadacheers29/08 07:58
copumpkin:)29/08 07:58
copumpkinsharada: a new nick :o29/08 07:59
sharadahttp://article.gmane.org/gmane.comp.lang.agda/95229/08 08:02
copumpkinhis MuNu file is missing :o29/08 08:04
stepcutsharada: I have not read this yet, but maybe it will help, http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html29/08 13:11
--- Day changed Sun Aug 30 2009
sharadaanyone implemented OTT?30/08 14:53
-!- EnglishGentv2 is now known as copumpkin30/08 19:36
--- Day changed Mon Aug 31 2009
-!- codolio is now known as dolio31/08 02:56
-!- Saizan_ is now known as Saizan31/08 03:06
sharadawwhat about just never comparing codata for convertability?31/08 08:14
sharadathat would be stupid31/08 08:14
dolioWhat?31/08 08:24
sharadajust a dumb idea I didn't think through31/08 08:25
sharadaI don't know how coinduciton should be, in a type theory31/08 09:20
sharadadoes anyone know a use of dependent case analysis,31/08 09:25
sharada?31/08 09:25
sharadaI'm confused about codata, types _must_ be finite, inductive data is okay in types -- but surely coinductive data should be banned31/08 09:46
sharadathe problem with that is that you can't say things about codata and it's pretty useless,  (maybe)?31/08 09:46
Saizanmaybe types need only to have a finite representation rather than a finite "unfolding" ?31/08 09:49
sharadaokay but we can't have decidible equality on arbitrary terms that have finite unfolding31/08 09:51
sharadaso how can you have proofs about codata31/08 09:53
sharadaa strategy like, unfold 300 times then stop .. is not really appropriate (is it?)31/08 09:54
codolioProofs about codata involve coinduction and bisimulation.31/08 10:15
-!- codolio is now known as dolio31/08 10:19
dolioThe problem with codata is that (useful) equality on it is pretty much doomed to be extensional.31/08 10:21
dolioThat isn't much diffrent than functions, though, except that you can go a fair way just through normalization rules of the lambda calculus.31/08 10:21
dolioBut that doesn't get you real equality on functions, just equality of functions that you can rewrite into one another via a limited set of rules.31/08 10:24
sharadaoh right, and equality proof for two coinductive values may be an infinite object!31/08 10:25
sharadathat's really obvious I should have know that31/08 10:25
* Saizan is reminded of his mu-calculus classes31/08 10:26
sharadaso mixed induction-coinduction is a necessity31/08 10:26
sharada(recursion-corecusion)31/08 10:27
dolioI was thinking about the encoding of the ordinals I was fooling with the other day, and it occurred to me that there are lots of bad elements, and lots that represent the same ordinal, but wouldn't be considered (intensionally) equal to one another.31/08 10:28
dolioBecause, for instance, 1, 2, 3, ... has a limit of omega, but so does (I think) 2, 3, 4, ....31/08 10:30
dolioSo there are infinitely many unequal representation of omega.31/08 10:30
sharadayeah31/08 10:31
dolioAnd I'm not sure what '1, 2, 1, 2, 1, 2, ...' would mean as a limit ordinal.31/08 10:38
sharadaI think it's invalid31/08 10:38
dolioProbably.31/08 10:38
dolioYou can, of course, rule those out.31/08 10:40
sharadadolio now we are getting to the horrific ind-rec version I worked on :P31/08 10:40
dolioAnd you can prove that '1, 2, 3 ...' and '2, 3, 4 ...' are equal through anti-symmetry, but that doesn't get you intensional equality.31/08 10:41

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