--- Log opened Thu Apr 01 00:00:57 2010 | ||

glguy_ | What's going on with #archlinux? | 01/04 06:50 |
---|---|---|

glguy_ | rather, why are we redirecting people to archlinux backwards? | 01/04 06:51 |

glguy_ | Oh, is it April 1st somewhere? | 01/04 06:52 |

Adamant | I think US PST is the next to get April Fool'ed. | 01/04 06:57 |

glguy_ | Oh, sorry. I sent that to the wrong channel | 01/04 06:58 |

--- Day changed Fri Apr 02 2010 | ||

crc__ | how do you get the agda console so you can test an expression? | 02/04 10:32 |

Amadiro | crc__, agda -I | 02/04 10:40 |

crc__ | is that inside of emacs? | 02/04 10:53 |

crc__ | btw im a vim user | 02/04 10:54 |

Amadiro | No, on the shell. But it says that the interactive mode is not supported anymore. | 02/04 10:54 |

crc__ | ok thanks | 02/04 10:58 |

crc__ | ill ask the lecturer after the break | 02/04 10:58 |

danten | if your in emacs you can also enter c-c c-n to evaluate expressions | 02/04 10:59 |

liyang | crc__: it's not really usable on the command line. :( I'm a Vim user too but you just have to put up with the Emacs UI for Agda. | 02/04 11:07 |

crc__ | sorry i may have asked the wrong question. Within emacs, i just want to run a a command, say something stupid like 1 :: []. How do I do that | 02/04 11:08 |

liyang | C-c C-n for ‘normalise’. | 02/04 11:08 |

liyang | Though, thinking about it, I don't recall ever having to use that… | 02/04 11:09 |

crc__ | liyang: that was the one I was looking for, thanks | 02/04 11:18 |

crc__ | what does it mean if you get something along the lines of Set !=< _65 -> Set _66 of type Set1 | 02/04 11:57 |

liyang | Looks like it's expecting something of _65 -> Set _66 where you've given it something of Set. | 02/04 11:59 |

crc__ | sorry, what is a set _65 | 02/04 12:00 |

Saizan | the _N things are freshly generated variables | 02/04 12:00 |

Saizan | and Set can take a parameter which is the universe | 02/04 12:01 |

Saizan | basically that error means that you're giving it a Set where it expects a function returning a Set | 02/04 12:01 |

liyang | The universe polymorphism is only making type errors harder to read, but you get the hang of interpreting those errors eventually. :-/ | 02/04 12:05 |

Saizan | it also removes quite a bit of duplication :) | 02/04 12:08 |

--- Day changed Sat Apr 03 2010 | ||

Mathnerd314 | does agda have bottom? (_|_ or ⊥ or whatever) | 03/04 00:23 |

fax | what do you mean | 03/04 00:23 |

Mathnerd314 | Is there some value which is in all other agda types? (like undefined in haskell) | 03/04 00:24 |

fax | no | 03/04 00:25 |

fax | you can turn off termination checker and define it if you want | 03/04 00:25 |

Mathnerd314 | no no, I'm fine | 03/04 00:26 |

Mathnerd314 | the standard library is no match for Haskell's, though... | 03/04 00:27 |

glguy | The standard library has a bottom and a casting function _|_-elim to whatever type you'd like | 03/04 00:31 |

glguy | In Data.Empty | 03/04 00:31 |

glguy | ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever | 03/04 00:31 |

glguy | ⊥-elim () | 03/04 00:31 |

Saizan | that's a bottom type though | 03/04 00:32 |

Saizan | but i guess if you get a value of that type you're done :) | 03/04 00:32 |

Saizan | if you just need a placeholder you should put a "?" in there | 03/04 00:32 |

Saizan | or postulate something | 03/04 00:32 |

* Mathnerd314 is confused | 03/04 00:34 | |

Saizan | basically, if agda had a value of type "forall a. a" it'd be of no use as a theorem prover. | 03/04 00:37 |

glguy | if you /had/ a value of ⊥ you could make it whatever you wanted :) | 03/04 00:37 |

Saizan | if a context where you've assumed contradictory facts you can make one, but only there :) | 03/04 00:38 |

Saizan | s/if/in/ | 03/04 00:38 |

glguy | The standard library has: | 03/04 00:38 |

glguy | trustMe : {A : Set}{a b : A} → a ≡ b | 03/04 00:38 |

glguy | trustMe = primTrustMe | 03/04 00:38 |

* fax hates that stuff | 03/04 00:40 | |

wpk_ | Hi all, I have a function which returns the union of 2 equivalencies (=), but when I put the constructor for a union with the equiv constructor (refl) on the right hand side of a pattern match Agda complains, what am I missing? | 03/04 15:30 |

wpk_ | I'm using Data.Sum and Relation.Binary.PropositionalEquality. | 03/04 15:32 |

liyang | *the* constructor for a union? | 03/04 15:33 |

wpk_ | well i match for the two constructors for the \u+ union function | 03/04 15:33 |

wpk_ | i think there are two, inj\_1 and inj\_2 | 03/04 15:34 |

liyang | Paste? http://moonpatio.com/fastcgi/hpaste.fcgi/new What's the complaint? | 03/04 15:34 |

wpk_ | sec | 03/04 15:35 |

wpk_ | http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a9247 | 03/04 15:35 |

Saizan | that usually happens when both sides of the equality are compound expressions | 03/04 15:35 |

Saizan | ah, no | 03/04 15:36 |

wpk_ | im new to this stuff so im probably making a basic mistake | 03/04 15:36 |

wpk_ | did that code and error message make any sense? | 03/04 15:37 |

Saizan | wpk_: what happens if you delete the {n} part? | 03/04 15:37 |

wpk_ | http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a9248 | 03/04 15:38 |

wpk_ | (same error) | 03/04 15:38 |

Saizan | ah, you didn't update the code though | 03/04 15:39 |

wpk_ | i did in emacs, im just really tired heh | 03/04 15:39 |

Saizan | heh | 03/04 15:39 |

wpk_ | the new error is the first one | 03/04 15:39 |

wpk_ | they appear similar | 03/04 15:40 |

Saizan | i think the problem is that when you pattern match on refl it'd try to rewrite the n into ⌊ n /2⌋ * 2 , which it can't do if you bind it explicitly yourself | 03/04 15:40 |

Saizan | and i think you get the same problem even if you leave it implicit because you can't write ⌊ n /2⌋ * 2 without binding n | 03/04 15:41 |

Saizan | i'm not really sure how/if you're supposed to be able to pattern match on refl there | 03/04 15:42 |

wpk_ | is there any way to create a pattern match where i deconstruct the equivalency then? like it works if i use a symbol for them | 03/04 15:42 |

wpk_ | hmm | 03/04 15:42 |

Saizan | you could post on the mailing list | 03/04 15:43 |

liyang | for what you're trying to do though, you just want something like \forall {a b} -> a == b -> suc (suc a) == suc (suc b), in which case cong (suc . suc) will do. | 03/04 15:43 |

Saizan | however you can still use that equality proof without pattern matching on it | 03/04 15:43 |

liyang | instead of refl there, name it ‘A’ and write inj\_1 (cong (suc \o suc) A) on the RHS. | 03/04 15:45 |

wpk_ | suc \o suc means suc(suc())? | 03/04 15:46 |

wpk_ | sorry im a complete newbie | 03/04 15:46 |

liyang | open import Function :3 | 03/04 15:46 |

liyang | Function composition, yes. | 03/04 15:46 |

wpk_ | apparently my installation of agda2 doesnt have Function.agda? | 03/04 15:48 |

Saizan | did you install the standard library? | 03/04 15:49 |

liyang | Oh er, Data.Function then. Or just write \lambda x \-> suc (suc x) | 03/04 15:49 |

Saizan | however you can write a simple lambda here | 03/04 15:49 |

liyang | Saizan: there's been some renaming going on lately in the stdlib. | 03/04 15:49 |

Saizan | true | 03/04 15:49 |

wpk_ | Data.Function works | 03/04 15:49 |

wpk_ | :D | 03/04 15:50 |

wpk_ | thanks so much guys | 03/04 15:52 |

wpk_ | which file is cong in so I can look at it? | 03/04 15:52 |

liyang | Relation.Binary.Core probably. | 03/04 15:53 |

Saizan | in emacs, move your cursor over it and press M-. | 03/04 15:53 |

liyang | If things type-check, you can cursor over the identifier and meta-. | 03/04 15:53 |

liyang | (yes.) | 03/04 15:53 |

wpk_ | i never knew that that's cool | 03/04 15:55 |

liyang | Is it coursework? (Whose course, out of interest?) | 03/04 15:56 |

wpk_ | Manuel Chakravartay (sp?) at UNSW, Australia. | 03/04 15:57 |

liyang | *nod* | 03/04 15:57 |

wpk_ | course is some SEng core forget the name | 03/04 15:57 |

liyang | Thought so. :) He sometimes hangs out here as TacticalGrace. | 03/04 15:58 |

wpk_ | haha ill remember that | 03/04 15:59 |

liyang | (So that's Nottingham, Swansea, and UNSW now…) | 03/04 15:59 |

wpk_ | where Manuel has taught agda? | 03/04 15:59 |

liyang | Where Agda has been used in teaching, that I'm aware of. | 03/04 16:00 |

wpk_ | oh | 03/04 16:01 |

liyang | I'm sure there's more though—I haven't really being paying that much attention. | 03/04 16:02 |

wpk_ | a good 80% of the students are totally lost on this I think | 03/04 16:03 |

liyang | That's probably expected. You'll get an intuition for it eventually. :3 | 03/04 16:07 |

kosmikus | liyang: I've used it in teaching, too (at UU) | 03/04 16:27 |

liyang | :D | 03/04 16:34 |

Amadiro | kosmikus, UU? | 03/04 16:34 |

liyang | What's the confusion percentage like? | 03/04 16:34 |

liyang | Amadiro: Utrecht | 03/04 16:35 |

Amadiro | Ah. | 03/04 16:35 |

fax | http://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/models/Desc.agda | 03/04 20:30 |

fax | cool | 03/04 20:30 |

fax | 118 proof-map-id : (D : Desc)(X : Set)(v : [| D |] X) -> map D X X (\x -> x) v == v | 03/04 20:30 |

fax | 125 proof-map-compos : (D : Desc)(X Y Z : Set) | 03/04 20:30 |

fax | 126 (f : X -> Y)(g : Y -> Z) | 03/04 20:30 |

fax | 127 (v : [| D |] X) -> | 03/04 20:30 |

fax | 128 map D X Z (\x -> g (f x)) v == map D Y Z g (map D X Y f v) | 03/04 20:30 |

ccasin | isn't generic programming fun! | 03/04 20:37 |

ccasin | what's this from? | 03/04 20:39 |

fax | that agda file I linked XD | 03/04 20:40 |

fax | here's a paper on it http://personal.cis.strath.ac.uk/~dagand/levitation.pdf | 03/04 20:40 |

ccasin | from the date, I guess this is an icfp submission? | 03/04 20:41 |

ccasin | oh my, from the abstract this looks really cool | 03/04 20:42 |

fax | yeah it's nice stuff | 03/04 20:43 |

fax | I think it's a continuation of Peter Morris' thesis | 03/04 20:43 |

fax | in some ways at least | 03/04 20:43 |

ccasin | this is such a good idea | 03/04 20:46 |

ccasin | I can tell because I'm jealous I didn't have it :) | 03/04 20:47 |

fax | ditto hehe | 03/04 20:47 |

fax | small universes are quite common but the idea that you could encode all the data types reflectively just seems ridiculous and impossible.. but turns out not to be | 03/04 20:48 |

ccasin | yes, I am anxious to see exactly how they pull this off | 03/04 20:49 |

ccasin | but I suppose I have to read the pages in order | 03/04 20:50 |

fax | if you start at the bottom of http://www.cs.nott.ac.uk/~pwm/ then it just gets harder (gradually though) | 03/04 20:50 |

ccasin | :) | 03/04 20:51 |

ccasin | happily, I think I have enough background | 03/04 20:51 |

Saizan | Desc as described above doesn't handle mutually recursive datatypes though | 03/04 20:51 |

liyang | http://donsbot.wordpress.com/2010/04/03/the-haskell-platform-q1-2010-report/ ← Agda is the 13th most popular application via Cabal in Q1, apparently. | 03/04 21:47 |

fax | that's just because of the number of times I reinstalled it | 03/04 22:06 |

fax | :p | 03/04 22:06 |

ccasin | this is interesting, but a little odd | 03/04 23:19 |

ccasin | is agda actually classified as an application? | 03/04 23:19 |

ccasin | most people interact with it through emacs, which just loads the agda libraries into ghci, right? | 03/04 23:20 |

ccasin | its cabal file calls it a library | 03/04 23:21 |

ccasin | but maybe these are just classifications he made up | 03/04 23:21 |

Saizan | there's an agda-executable package which gives you an executable | 03/04 23:25 |

Saizan | otherwise it's a library used by ghci in the emacs mode | 03/04 23:25 |

ccasin | yes, but I think no one uses the executable, so I'd be surprised if that's what's referred to here | 03/04 23:25 |

Saizan | oh, i think i miss some context | 03/04 23:26 |

ccasin | liyang had linked to this: | 03/04 23:27 |

ccasin | http://donsbot.wordpress.com/2010/04/03/the-haskell-platform-q1-2010-report/ | 03/04 23:27 |

ccasin | where agda is listed as the 13th most cabal-installed haskell application | 03/04 23:27 |

ccasin | in the last quarter | 03/04 23:27 |

ccasin | (as opposed to library) | 03/04 23:27 |

Saizan | i think it counts as an application because of the agda-mode executable | 03/04 23:28 |

ccasin | yes, this is a reasonable theory | 03/04 23:28 |

ccasin | I just wonder how he made these choices | 03/04 23:29 |

ccasin | (not for any particular reason) | 03/04 23:29 |

--- Day changed Sun Apr 04 2010 | ||

wpk_ | Hi I'm having a problem pattern matching in a function I've written, I think the type declaration is sensible but I'm not sure, it's like PA9 : ? {n} -> (P : N -> Bool) -> P 0 = true -> ((P n = true) -> (P (suc n) = true)) -> P n = true | 04/04 09:15 |

wpk_ | the pattern {0} p a b is rejected by agda.. | 04/04 09:15 |

wpk_ | it seems like agda wont recognize ((P n = true) -> (P (suc n) = true)) as being an argument, and includes it in the return type | 04/04 09:25 |

Saizan | wpk_: are you really using = there or \== ? | 04/04 13:37 |

stevan | hellos | 04/04 13:38 |

fax | hi | 04/04 13:38 |

stevan | taught yourself to levitate yet? | 04/04 13:40 |

fax | I think so | 04/04 13:41 |

stevan | :-) | 04/04 13:41 |

fax | 5 | 04/04 17:05 |

fax | sorry, I take that back | 04/04 17:05 |

stevan | 38 people, yet complete silence :-(. | 04/04 17:06 |

stevan | glguy: are you still playing with category theory? | 04/04 17:07 |

fax | I tried to implement category theory in Coq but it didn't go well | 04/04 17:07 |

fax | I mean it was going quite nicely for a bit, then I started to wonder what 'equals' means and it all fell apart | 04/04 17:08 |

stevan | yes | 04/04 17:08 |

fax | what I'd like to know is what problems (there's always some problem, whatever you do) come up if you use quotients instead of setoids -- but I have not tried it | 04/04 17:10 |

stevan | you run into situations where you need existential equality? | 04/04 17:10 |

fax | what's existential equality? | 04/04 17:10 |

stevan | forall x. f x = g x -> f = g | 04/04 17:11 |

fax | oh | 04/04 17:11 |

fax | wwhy do you say that? It seems very plausible | 04/04 17:11 |

stevan | well you can't prove that statement inside agda? | 04/04 17:12 |

fax | I'm not sure | 04/04 17:12 |

fax | I think we can prove (\x -> f x) = (\x -> g x) <-> f = g | 04/04 17:13 |

fax | yes you are right, this is weaker than the forall x. we can't prove that in agda | 04/04 17:13 |

stevan | i only ran into that problem with equality, what problem were you refering to? | 04/04 17:14 |

fax | huh? | 04/04 17:17 |

Saizan | stevan: you meant extensional? | 04/04 17:17 |

stevan | probably :-) | 04/04 17:17 |

stevan | fax: you said it fell part when you started wondering what equals means? | 04/04 17:18 |

fax | yeah | 04/04 17:18 |

fax | you have to get all this typeclass stuff out to make sets with equivalence relations and equivalence preserving morphisms | 04/04 17:18 |

fax | it works but it's really complicated | 04/04 17:19 |

fax | if we could just form types T/~, I think it would be much easier and everything would work perfectly | 04/04 17:19 |

fax | (but experience tells me that does not happen :) and there are unforseen problems) | 04/04 17:19 |

Saizan | with quotients in epigram it seems you still need to prove your morphism is equivalence preserving, but at least the equality is substitutive? | 04/04 17:20 |

fax | yeah | 04/04 17:20 |

fax | I've not been able to figure out the syntax for pig so I haven't tried anything with it though | 04/04 17:21 |

Saizan | i defined a cofree comonad thing :) | 04/04 17:21 |

fax | wow cool I wanna see | 04/04 17:21 |

fax | did you write that in haskell? | 04/04 17:21 |

stevan | what's wrong with just using propositional equality for CT btw? | 04/04 17:23 |

stevan | (i need to read up on quotients) | 04/04 17:23 |

Saizan | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24653 <- | 04/04 17:24 |

fax | cool Saizan | 04/04 17:24 |

Saizan | fax: i just wrote it in epigram itself, i could add it as a Feature to get the comonad laws hold definitionally though | 04/04 17:24 |

fax | so cofree means basically free except greatest fixed point? | 04/04 17:24 |

Saizan | or, i could try at least :) | 04/04 17:24 |

Saizan | i'm not so sure what cofree means by itself, but it sounds something like that | 04/04 17:25 |

Saizan | though i'm pretty comfortable with the "cofree comonad" construction | 04/04 17:27 |

fax | stevan - if you try to form the category of categories then when are two functors between categories equal? | 04/04 17:28 |

fax | if you use propositional equality ... is that right/ | 04/04 17:28 |

fax | maybe the thing to do would be define category as a feature... | 04/04 17:30 |

fax | then implement all of modern mathematics in that | 04/04 17:31 |

stevan | hmm, i don't know. i haven't run into that problem, does it arise when trying to prove some theorem or define some? | 04/04 17:32 |

fax | that was just my thinking which led me to give up | 04/04 17:35 |

fax | maybe it wasn't really an issue but I had a couple of false starts (where you write a lot of code which seems fine then something fundamental is broken so you have to start again) | 04/04 17:36 |

stevan | yeah, i mostly have definitions so far. you don't really see if they are correct until you start using them (in theorems or when defining more complex things)... | 04/04 17:39 |

fax | the reason I wanted categories is to define term algebras | 04/04 17:39 |

fax | that stuff would probably have worked but I didn't want to build a wall around myself | 04/04 17:40 |

fax | stevan definitions in ada ? | 04/04 17:42 |

fax | agda* | 04/04 17:42 |

stevan | yes, records for what a category is, functors, etc | 04/04 17:43 |

fax | cool can I see | 04/04 17:43 |

fax | hmmmm I need to install agda :/ | 04/04 17:43 |

stevan | http://web.student.chalmers.se/~stevan/ctfp/html/README.html | 04/04 17:44 |

stevan | i wouldn't trust them to be right tho, i'm a CT noob. :-) | 04/04 17:45 |

fax | I've only started to study it recently (Because of dolio ;p) | 04/04 17:45 |

stevan | i think it helps to code, give you something concrete... | 04/04 17:46 |

fax | yeah definitely, and it's great when you get to the point where you don't have to keep writing code: You can just ask it the answers | 04/04 17:47 |

stevan | oh, i'm surely not there yet. could you give an example? | 04/04 17:49 |

fax | stevan, say you defined the category of bijective functions between finite sets | 04/04 17:49 |

fax | oh | 04/04 17:49 |

fax | that's not an example | 04/04 17:49 |

fax | this is regarding the problem of equality | 04/04 17:49 |

fax | I think we can have lots of different permutation functions which are extensionally equal but not identical in agda | 04/04 17:50 |

fax | so you take an axiom for that, but the axiom might block computation if some programs rely on certain proofs (in certain ways) -- I know it sounds like a long stretch but I think it does cause problems | 04/04 17:50 |

fax | but more generally, if you have any category where the objects (or morphisms) are not normal forms -- then the equality will not match up exactly right | 04/04 17:51 |

stevan | hmm | 04/04 17:51 |

fax | stevan ou know about Computational Category Theory? (the book is online) | 04/04 17:52 |

fax | there's lots of programs in there (which I wanted to implement.. but I got stuck) | 04/04 17:52 |

stevan | by burstall and rydesomething? | 04/04 17:53 |

fax | yes | 04/04 17:53 |

stevan | i only glanced thru it, their definitions are not very nice given that they have to make them fit into simply typed setting | 04/04 17:54 |

fax | yeah but I mean that's just the SML code | 04/04 17:54 |

stevan | yeah, true | 04/04 17:55 |

fax | the programs should work in a dependently typed setting, except with strong specifications | 04/04 17:55 |

fax | (at least I hope so!) | 04/04 17:55 |

fax | it's raelly frustrating because there's a lot of stuff I want to program but without this foundational stuff it doesn't seem possible | 04/04 18:14 |

stevan | what sort of stuff do you want to program? what foundational stuff? | 04/04 19:59 |

fax | foundational stuff being category theory | 04/04 20:00 |

fax | I've been trying to get some of the maths I know into the computer but it's has not been working well at all | 04/04 20:00 |

stevan | what sort of maths? | 04/04 20:02 |

fax | like everything | 04/04 20:03 |

fax | calculating things, solving equations | 04/04 20:04 |

stevan | have you read about the formath project? | 04/04 20:04 |

fax | yeah | 04/04 20:05 |

stevan | that sort of stuff? | 04/04 20:05 |

fax | yes | 04/04 20:05 |

fax | in the coq standard library there are stuff like decidibility of primality and they don't even compute :/ | 04/04 20:05 |

fax | and they have trichotomoy as an axiom on the real numbers | 04/04 20:06 |

fax | it's pretty stupid | 04/04 20:06 |

stevan | i know next to nothing about coq. what about that corn thing? don't they do it propertly? | 04/04 20:07 |

fax | yeah corn is cool | 04/04 20:07 |

stevan | does corn have a better solution for reals than the standard lib? | 04/04 20:16 |

fax | yes | 04/04 20:18 |

fax | that's roconnors stuff it's way cool | 04/04 20:18 |

stevan | why doesn't it replace the std lib stuff then? | 04/04 20:20 |

--- Day changed Mon Apr 05 2010 | ||

Schrodinger_ | Anyone here? | 05/04 06:57 |

--- Day changed Tue Apr 06 2010 | ||

agda_noob | hello | 06/04 09:17 |

agda_noob | i wonder how many people are trying to prove the peano axioms in agda on this channel | 06/04 09:18 |

agda_noob | hello? | 06/04 09:21 |

agda_noob | does anybody know anything about agda here? | 06/04 10:00 |

vlad__ | hello? | 06/04 10:17 |

vlad__ | can anybody help me out with agda | 06/04 10:18 |

vlad__ | im trying to figure out how to prove the peano axioms | 06/04 10:18 |

kosmikus | vlad__: ok, so what exactly are you trying to do? | 06/04 10:18 |

vlad__ | ok well im trying to use the reflexive function to prove that if suc m \equiv suc n then m \equiv n | 06/04 10:19 |

vlad__ | but i dont think im putting the syntax right | 06/04 10:20 |

kosmikus | you get a syntax error? | 06/04 10:20 |

vlad__ | well my definition shoudl return suc m \equiv suc n then m \equiv n | 06/04 10:20 |

vlad__ | and i have PA4 {m} {n} = refl suc m \equiv suc n -> m \equiv n | 06/04 10:21 |

vlad__ | any ideas kosmikus? | 06/04 10:21 |

kosmikus | is this a homework assignment? | 06/04 10:21 |

vlad__ | it is | 06/04 10:22 |

kosmikus | is the original assignment online? | 06/04 10:22 |

vlad__ | yap | 06/04 10:22 |

kosmikus | where? | 06/04 10:22 |

vlad__ | i dont think you can access it, you have to log on | 06/04 10:22 |

vlad__ | the gist of it is i have to prove some peano axioms | 06/04 10:22 |

vlad__ | i have the right idea about doing it | 06/04 10:23 |

vlad__ | just cant seem to get the syntax right in agda | 06/04 10:23 |

kosmikus | it looks like what you're writing should be the *type* of PA4 | 06/04 10:23 |

vlad__ | right | 06/04 10:24 |

vlad__ | the type is suc m \equiv suc n -> m \equiv n | 06/04 10:24 |

kosmikus | yes, so then you should write: | 06/04 10:25 |

kosmikus | PA4 : \forall {m n} -> suc m \equiv suc n -> m \equiv n | 06/04 10:26 |

kosmikus | something like that | 06/04 10:26 |

vlad__ | thats the type i have that | 06/04 10:27 |

vlad__ | no for all tho | 06/04 10:27 |

vlad__ | just {m n : \nat} -> suc m \equiv \suc n -> m \equiv n | 06/04 10:27 |

vlad__ | my problem is the application | 06/04 10:28 |

vlad__ | i think i have to use the reflexive proof but im not sure how to provide the arguments right | 06/04 10:28 |

TacticalGrace | kosmikus: you can easily access the assignment at https://wiki.cse.unsw.edu.au/cs3141/10s1/Assignment%201 | 06/04 10:29 |

kosmikus | TacticalGrace: ah :) if you're here, then you can probably decide better what to tell or not to tell :) | 06/04 10:29 |

vlad__ | really? i think u have to log in | 06/04 10:29 |

vlad__ | i wasnt aware u can access it, in any case i always log in | 06/04 10:30 |

kosmikus | I can access it. | 06/04 10:30 |

vlad__ | ok cool | 06/04 10:31 |

vlad__ | do you reken you can help me out then? | 06/04 10:31 |

kosmikus | well, the solution is quite simple, so I don't want to just give it | 06/04 10:32 |

kosmikus | if you have the type, you have to think about how you can construct a value of the type | 06/04 10:32 |

vlad__ | i know its simple, its frustrating | 06/04 10:32 |

kosmikus | you have to provide a function from an equality to an equality | 06/04 10:32 |

vlad__ | yap, aint that simple , but iv tried returning that type and it doesnt like it | 06/04 10:32 |

kosmikus | so you can start with | 06/04 10:32 |

kosmikus | PA4 proof = ? | 06/04 10:32 |

vlad__ | i start with PA4 {m} {n} = ? | 06/04 10:33 |

vlad__ | is that right? | 06/04 10:33 |

kosmikus | that's also ok | 06/04 10:33 |

kosmikus | but then ? is of function type, right? | 06/04 10:33 |

kosmikus | so, a good general tactic is to introduce an argument if you have to produce a function | 06/04 10:34 |

kosmikus | so you either put it on the lhs: | 06/04 10:34 |

kosmikus | PA4 {m} {n} proof = ? | 06/04 10:34 |

kosmikus | or you use a lambda abstraction: | 06/04 10:34 |

kosmikus | PA4 {m} {n} = \ proof -> ? | 06/04 10:34 |

kosmikus | the former is probably better | 06/04 10:34 |

vlad__ | what do you mean by = \ proof -> ? i thought the proof came after the equal and thats it? | 06/04 10:35 |

vlad__ | oh | 06/04 10:35 |

kosmikus | proofs can have structure. that's the whole point. | 06/04 10:38 |

vlad__ | i have PA4 {m} {n} = suc m \equiv suc n -> refl m \equiv n ? | 06/04 10:38 |

kosmikus | no, now you're writing a type again | 06/04 10:41 |

kosmikus | but you have to give an implementation of that type | 06/04 10:41 |

vlad__ | should i be using refl as proof? | 06/04 10:41 |

vlad__ | or cong? | 06/04 10:41 |

vlad__ | im soo confused | 06/04 10:43 |

stevan | so am i! | 06/04 10:44 |

vlad__ | do you know much about agda stevan? | 06/04 10:44 |

stevan | a bit. | 06/04 10:45 |

kosmikus | vlad__: to be honest, both refl and cong are possible here, but it's probably easier to do it directly via refl | 06/04 10:45 |

vlad__ | right | 06/04 10:46 |

vlad__ | im just not sure how to construct this function | 06/04 10:46 |

kosmikus | vlad__: you should really try to construct the proof systematically | 06/04 10:46 |

vlad__ | how many arguments does refl take in? | 06/04 10:46 |

kosmikus | vlad__: you've probably learned that in a lecture, right? | 06/04 10:46 |

kosmikus | refl doesn't take any explicit arguments | 06/04 10:46 |

vlad__ | ok, i just dont understand how to use refl | 06/04 10:46 |

kosmikus | refl is the constructor of the equality type | 06/04 10:47 |

kosmikus | have you been able to prove any of the other axioms? | 06/04 10:47 |

vlad__ | only the first 3 | 06/04 10:48 |

kosmikus | perhaps, if you do symmetry and transitivity first, this one will become clearer | 06/04 10:48 |

vlad__ | im really not good at math or agda, i dont understand what you mean by symetry and transitivity | 06/04 10:48 |

vlad__ | as in i dont get how i prove that | 06/04 10:48 |

kosmikus | TacticalGrace: nice assignment, btw | 06/04 10:49 |

kosmikus | vlad__: PA6 and PA7 | 06/04 10:49 |

kosmikus | vlad__: sorry, I was assuming that you've read the assignment | 06/04 10:49 |

vlad__ | lol | 06/04 10:50 |

vlad__ | im taking it one at a time | 06/04 10:50 |

vlad__ | oh right , you think it would be easier to do 6 and 7 first? | 06/04 10:50 |

kosmikus | well, they have all one-line solutions | 06/04 10:52 |

kosmikus | but if you have trouble doing one, it may be easier to do one of the others first | 06/04 10:52 |

kosmikus | it may also be helpful to look at notes/slides from the lecture if there are any | 06/04 10:53 |

TacticalGrace | kosmikus: thanks :) | 06/04 10:53 |

vlad__ | thats prob a good strategy | 06/04 10:54 |

kosmikus | the assignments says that propositional equality has been introduced there | 06/04 10:54 |

kosmikus | so you've probably already seen how it can be used | 06/04 10:54 |

vlad__ | yap i have , il re-read though it | 06/04 10:54 |

kosmikus | TacticalGrace: and good to see you're also trying to use Agda in teaching | 06/04 10:54 |

kosmikus | TacticalGrace: what kind of course is this? I can't seem to access the course's main page. | 06/04 10:54 |

TacticalGrace | kosmikus: It's http://www.cse.unsw.edu.au/~cs3141/ | 06/04 10:55 |

kosmikus | TacticalGrace: ah, I've done http://www.cs.uu.nl/wiki/DTP a while ago | 06/04 10:56 |

TacticalGrace | It's a fairly big class actually | 06/04 10:56 |

TacticalGrace | 68 student | 06/04 10:56 |

kosmikus | TacticalGrace: and I'm currently having two lectures of Agda at the end of "Advanced Functional Programming" | 06/04 10:56 |

kosmikus | TacticalGrace: always fantastic that you get so many students. these are numbers we can only dream of. | 06/04 10:57 |

TacticalGrace | the class is part of the compulsory SE cources for SE program studends and CS program students | 06/04 10:59 |

TacticalGrace | which is part of the challenges | 06/04 10:59 |

vlad__ | se rules | 06/04 10:59 |

vlad__ | go se | 06/04 10:59 |

TacticalGrace | vlad__: are you a SE student? You should have done Event B in that case and actually already a bit about logic | 06/04 11:00 |

vlad__ | i am doing event b now | 06/04 11:00 |

vlad__ | 2 subjects event b 3rd is this 1 which is about agda and haskell | 06/04 11:00 |

TacticalGrace | ic, I thought the event b stuff was supposed to be before 3141 | 06/04 11:01 |

vlad__ | tactical grace | 06/04 11:01 |

vlad__ | you are from nsw | 06/04 11:01 |

vlad__ | you are from unsw | 06/04 11:01 |

vlad__ | technically but its not a prerequisite | 06/04 11:02 |

vlad__ | cHAK | 06/04 11:02 |

vlad__ | u are manuel | 06/04 11:02 |

vlad__ | my lecturer | 06/04 11:02 |

TacticalGrace | it can't be b/c of the CS students | 06/04 11:02 |

TacticalGrace | vlad__: indeed | 06/04 11:02 |

vlad__ | hahahah | 06/04 11:02 |

vlad__ | this is too funny | 06/04 11:02 |

vlad__ | cought out | 06/04 11:03 |

vlad__ | good assignment | 06/04 11:05 |

vlad__ | thanks alot for all your help kosmikus | 06/04 11:21 |

vlad__ | i have to go now, hopefully i will figure things out better after more practice | 06/04 11:21 |

vlad__ | take it easy tactical grace | 06/04 11:22 |

vlad__ | see you in the lectures | 06/04 11:22 |

pigworker | I was going to suggest reading "A Few Constructions on Constructors". No I wasn't. | 06/04 11:39 |

TacticalGrace | ;) | 06/04 11:41 |

jlouis | Whats Gordon Brows equality like? | 06/04 12:08 |

jlouis | *Brown | 06/04 12:09 |

jlouis | The agda tutorial declares: _or_ : Bool -> Bool -> Bool; true or x = true; false or _ = false .. does that mean the _or_ is an impostor, a cleverly disguised _and_ ? | 06/04 12:30 |

npouillard | :) | 06/04 12:30 |

npouillard | false or x = x | 06/04 12:31 |

npouillard | would be less wrong indeed | 06/04 12:31 |

npouillard | it is not a and either "true or false" returns true... | 06/04 12:31 |

pigworker | I've always said that "grep Bool" is a good test of any dependently typed library. | 06/04 12:32 |

npouillard | pigworker: what you mean | 06/04 12:32 |

pigworker | Bool is the type of meaningless bits (hence well typed errors like the above). Bool-valued tests tend to be less useful (i.e., harder to exploit at the type level) than those which decide propositions or deliver witnesses. | 06/04 12:35 |

pigworker | "A Boolean is a bit uninformative." was my old slogan. | 06/04 12:35 |

npouillard | pigworker: sure, but they should not be to be completly removed | 06/04 12:36 |

npouillard | for instance vectors hold more information than lists, but we should not remove lists. | 06/04 12:36 |

npouillard | but in | 06/04 12:36 |

npouillard | a dependently typed language it is evident that we should use less bools | 06/04 12:37 |

npouillard | and more 'Dec P' | 06/04 12:37 |

npouillard | this is just my POV, of course... | 06/04 12:38 |

pigworker | It's probably important to facilitate Boolean "first drafts" which get refined to Dec P, for suitably chosen P (but a good choice might take a while). | 06/04 12:38 |

npouillard | but I wouldn't mind if Bool got renamed to Bit to emphasis on this | 06/04 12:40 |

pigworker | Correspondingly, Bool should probably be in the library, but libraries for other things should preferably offer more informative types for their testing operations. | 06/04 12:40 |

npouillard | sure | 06/04 12:41 |

npouillard | but it is the case in the Agda stdlib, equality returns a Deciable _≡_ and we can use ⌊_⌋ to get a bool | 06/04 12:42 |

* kosmikus 's grant proposal for dependently typed programming has been rejected in the pre-screening phase :( | 06/04 12:43 | |

npouillard | :( | 06/04 12:44 |

pigworker | kosmikus: rats! | 06/04 12:44 |

kosmikus | pigworker: yeah. "not innovative enough" and "relatively weak CV" | 06/04 12:44 |

edwinb | bah! | 06/04 12:45 |

pigworker | kosmikus: sounds like prejudice to me; or is that what "pre-screening" means? | 06/04 12:46 |

TacticalGrace | kosmikus: :( | 06/04 12:46 |

edwinb | We're clearly going too mainstream | 06/04 12:46 |

kosmikus | pigworker: yes, that's what it means ;) | 06/04 12:46 |

kosmikus | pigworker: from 49 submissions, they select 23 that even get expert reviews. | 06/04 12:46 |

kosmikus | ultimately, 5 get funded. | 06/04 12:47 |

kosmikus | I find that ridiculous. Considering that for a conference like ICFP, we get about 100 submissions and try hard to give everyone multiple expert reviews. | 06/04 12:47 |

pigworker | kosmikus: not great odds, but a shame that they don't get expert reviews for all | 06/04 12:47 |

kosmikus | Where an ICFP paper is clearly less relevant for your future life than a grant proposal with 800 kEUR. | 06/04 12:47 |

pigworker | kosmikus: So you got about 100 submissions? I don't expect you to answer that... | 06/04 12:50 |

kosmikus | ICFP reviewing is also a bit frustrating by the way: the top 5 most interesting papers (from my purely subjective view) are all papers I have conflicts with ... | 06/04 12:50 |

TacticalGrace | kosmikus: so, how does a non-expert decide what is innovative? | 06/04 12:50 |

pigworker | TacticalGrace: with nipples | 06/04 12:50 |

kosmikus | TacticalGrace: good question. something I'm going to ask in my reply as well, but of course, I can only hope that sooner or later they'll improve the system. | 06/04 12:51 |

pigworker | Which reminds me: grant app to finish; must work on zip, pep and fizz; oh, and some technical substance. | 06/04 12:53 |

kosmikus | perhaps I should start submitting grant apps in other countries. | 06/04 12:54 |

pigworker | International collaboration always looks good. | 06/04 12:56 |

pigworker | kosmikus: and you've got a conflict with us lot, too... | 06/04 12:59 |

jlouis | At page 8 in tutorial - first verdict: Syntax beats Twelf | 06/04 12:59 |

kosmikus | pigworker: yes. | 06/04 12:59 |

pigworker | had better go to school for a bit. | 06/04 13:03 |

jlouis | Agda definitely feels a lot like Twelf, just easier | 06/04 16:22 |

Saizan | uh | 06/04 16:22 |

Saizan | when i've to prove something about a function defined with overlapping patterns i wish i could just pattern match on its cases though | 06/04 16:29 |

fax | yeah it's a shame we don't get any witnesses from the pattern matching, but that's beacuse they just implement it directly | 06/04 16:36 |

fax | <kosmikus> pigworker: yeah. "not innovative enough" and "relatively weak CV" | 06/04 16:39 |

fax | fucking hell that is ridiculous | 06/04 16:39 |

stevan | fax: regarding your reddit question; just got this url from a friend: http://www.math.ias.edu/~vladimir/Site3/home.html seen it? (i asked him reply on reddit). | 06/04 17:22 |

fax | most likely I cannot understand any of this but I will try :))) | 06/04 17:23 |

danten | I just replied :p basically giving that link and also a video of Vladimir talking in general about foundations of mathematics :) | 06/04 17:34 |

fax | we have to know category theory (that's what those squares in the video are), synthetic topology, "Homotopy theoretic models of identity types" | 06/04 17:42 |

fax | 'schemes' perhaps. | 06/04 17:43 |

fax | a lot of things | 06/04 17:43 |

fax | I'm getting the impression that the normal way to interpret type theory rules into category theory gives an extensional semantics -- and we want intentional (so that we can actually implement it and have typechecking decidible for example) and that is where these homotopy things come in (?) | 06/04 17:49 |

danten | dunno | 06/04 17:50 |

fax | oh and fibrations/fiber bundles get mentioned a lot | 06/04 17:51 |

fax | (another thing which I have only got cheesy videos of mugs morphing into donuts rather than any actualy understanding) | 06/04 17:52 |

stevan | :-) | 06/04 17:52 |

stevan | slides for talk about a project i been working on with a friend: http://web.student.chalmers.se/~stevan/csallp/talk/talk.pdf | 06/04 18:13 |

stevan | if someone is interested | 06/04 18:13 |

fax | stevan nice!!!!!! | 06/04 18:14 |

fax | this "Dense linear orders" is why I had to put down my model theory book | 06/04 18:14 |

stevan | i think i can explain it now, but we haven't implemented it fully yet | 06/04 18:15 |

fax | stevan I am going to ask you all about it :P | 06/04 18:16 |

stevan | would be awesome to have running examples, but that will probably take an other month or so | 06/04 18:16 |

fax | page 12, Otherwise (inequalities) -- | 06/04 18:19 |

fax | this part is basically doing a topological sort? | 06/04 18:19 |

stevan | i know nothing about topological sorts | 06/04 18:20 |

fax | well you have a list of a < b (for all different a and b) and basically you need to find some mapping sigma from these names to numbers so that sigma(a) < sigma(b) | 06/04 18:21 |

fax | natural numbers | 06/04 18:21 |

stevan | hmm | 06/04 18:22 |

fax | "Ssreﬂect what does it do?" hehe I think the same thing | 06/04 18:22 |

fax | annoying thing about coq is the standard library uses 'Qed' everywhere so they prove a lot of decidibility results with no computational content.. which means reimplementing them if you need them for reflective proofs :| | 06/04 18:23 |

fax | nice in Agda they don't have such a thing (although there are good points to it as well) | 06/04 18:23 |

stevan | well it's a bit funny, because we been looking alot at coq code using ssreflect, and we were sort of expecting ssreflect to do some magic somewhere, but we didn't notice any of that... | 06/04 18:23 |

Saizan | what is Qed? | 06/04 18:25 |

fax | Saizan, it's meant to be used for "proofs" -- it's sort of like a poor mans proof irrelevance | 06/04 18:25 |

fax | the things defined with Qed wont reduce so it's 'in effect' proof irr.. just without the actual convertability of proofs | 06/04 18:26 |

fax | it means you can go an reprove any Qed thing in a different way, without breaking stuff | 06/04 18:26 |

fax | but the bad thing is sometimes you /want/ proofs to have computational content -- like with well founded recursion | 06/04 18:26 |

npouillard | fax: it does have some perfs advantages too | 06/04 18:26 |

fax | and the other problem is that people use it when they shouldn't | 06/04 18:26 |

fax | npouillard oh that's true I should have thought of this as well | 06/04 18:27 |

fax | there's an example in the book where they do some proof about a very large number, which breaks unless you use Qed (might be interesting to try that in agda) | 06/04 18:28 |

fax | stevan (but I think deciding if such a sigma exists is equivalent to topological sort and I tried to write this at one point but I made some mistake and didn't get around to completing it) | 06/04 18:30 |

stevan | ok, so do you understand why qelim for dlos works now :-)? | 06/04 18:31 |

fax | no | 06/04 18:31 |

stevan | :-/ | 06/04 18:32 |

fax | im not ready to ask any intelligent questions yet :P | 06/04 18:32 |

fax | just looking at the code | 06/04 18:32 |

fax | and I wish I had agda but I don't know how to install it | 06/04 18:32 |

stevan | the theory dependent part (DLOs) isn't done yet unfortunately | 06/04 18:33 |

fax | DLOs was supposed to be one of the excersises in my book (David Marker) but all it really did was tell me that I had not undersatnd anything! | 06/04 18:33 |

fax | so I decided to come back to it another day | 06/04 18:34 |

fax | I suppose you need decidibile equality on the carrier to prove the forall/~exists~ switch? | 06/04 18:34 |

fax | or you use classical connectives? | 06/04 18:34 |

stevan | i seen a couple of proofs of it in different model theory books... i didn't find any of them very helpful... | 06/04 18:34 |

fax | well there's no reason to not have both.. I suppose | 06/04 18:34 |

stevan | yeah, if look at the forall case in the last proof in decisionProcedure you will see what happens | 06/04 18:36 |

fax | ¬∃¬⇔∀ : ∀ {A : Set}{P : A → Set}(d : ∀ x → Dec (P x)) → (¬ (∃ λ x → ¬ P x)) ⇔′ (∀ x → P x) | 06/04 18:43 |

fax | this is so cool stevan | 06/04 18:43 |

stevan | :-) | 06/04 18:43 |

fax | agda lib doesn't have rationals? | 06/04 18:51 |

stevan | it does, but it's basically only the data type Q, without any useful functions (+, -, *, etc are not implemented) | 06/04 18:52 |

fax | :S | 06/04 18:58 |

fax | I can't find anything, do they have setoids? | 06/04 18:58 |

fax | mmm | 06/04 18:58 |

fax | quotients comeing soon probably means no | 06/04 18:58 |

stevan | http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Rational.html#180 | 06/04 18:59 |

fax | I wonder why it has isCoprime : True (C.coprime? ∣ numerator ∣ (suc denominator-1)) | 06/04 19:01 |

fax | ah that's for ≃⇒≡ : _≃_ ⇒ _≡_ | 06/04 19:01 |

fax | http://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf] | 06/04 20:35 |

fax | http://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf | 06/04 20:35 |

stevan | there was a student at nottingham who did Q in agda, but he choose a different way than the ways it's done in the std lib and so there is some more work needed... when i checked he said he probably wouldn't do it anytime soon. i did get the code however, if you are interested i could put it somewhere for you. | 06/04 20:43 |

fax | how different? | 06/04 20:45 |

stevan | it was stand alone, not reusing stuff from the std lib, so it needs some reworking to fit nicely into the std lib | 06/04 20:46 |

fax | oh ok | 06/04 20:46 |

fax | I was going to implement R but that would need setoids and since agda is getting quotients soon it seems like I should just not | 06/04 20:46 |

npouillard | is there something to read about the near to come quotients in Agda ? | 06/04 20:48 |

stevan | how do you know they are comming soon? | 06/04 20:48 |

fax | :S I hope I haven't made this up | 06/04 20:48 |

stevan | they seemed to have been discussed during last AIM, but it doesn't say anything more than that | 06/04 20:50 |

pigworker | It's not obvious to me how to make (R x y) -> [x]=[y] hold, without re-engineering propositional equality. | 06/04 20:56 |

pigworker | where [_] gives equivalence classes wrt R | 06/04 20:56 |

fax | it seems okay to add this stuff as an axiom | 06/04 21:02 |

fax | I gather that you can always elaborate it into setoids with morphism proofs everywhere (which is what you have to do with by hand with Coq now) | 06/04 21:02 |

fax | then of course the axioms don't have computational properties... I guess that is the real problem | 06/04 21:03 |

pigworker | fax: yep, that's the problem | 06/04 21:03 |

stevan | what does corn do? | 06/04 21:07 |

fax | well corn doesn't use typeclasses but I think they are rewriting it to do so | 06/04 21:07 |

fax | but you must carry about morphism proofs with all the stuff | 06/04 21:10 |

fax | like if you defined a group with inverse : G -> G | 06/04 21:10 |

fax | then you must also have inverseProper : forall x y, x ~ y -> inverse x ~ inverse y | 06/04 21:10 |

stevan | so, the real closed fields using reflection in coq paper i posted recently, is it runnable? | 06/04 21:11 |

fax | I've not tried | 06/04 21:11 |

fax | the reals in the stdlib are classical | 06/04 21:11 |

fax | did you see the bit where they used it to derive P \/ ~P for first order statements | 06/04 21:12 |

stevan | and they used those? | 06/04 21:12 |

fax | CoRN defines constructive reals too | 06/04 21:12 |

stevan | i haven't looked at it propertly yet | 06/04 21:12 |

fax | I've not tried this reflection thing though | 06/04 21:12 |

fax | well | 06/04 21:13 |

fax | I was going to say I don't think we can use quantifier elimination on reals | 06/04 21:13 |

fax | (since we don't have that forall/~exists~ switch) | 06/04 21:13 |

fax | but then... there is that cylindrical algebraic decomposition | 06/04 21:13 |

stevan | will it not fall out like it did in our quantifier elim library? | 06/04 21:14 |

fax | I am confused :P | 06/04 21:14 |

fax | how can it work | 06/04 21:14 |

stevan | i don't know how qlim for RCF works, but i assumed it worked similarly to how we did it for DLOs | 06/04 21:15 |

fax | "To build a decision procedure from this theorem, we have to chose a ﬁeld D | 06/04 21:15 |

fax | over which sign and equality is decidable." | 06/04 21:16 |

fax | so in this case, they only need coefficients of the polynomial to be decidible | 06/04 21:16 |

fax | the actual variables can be real, if I understand correctly | 06/04 21:16 |

fax | i.e. you could have polynomials with rational coefficients, except they are functions R^n -> R | 06/04 21:16 |

fax | (please correct me if I say something wrong!!) | 06/04 21:17 |

stevan | i don't know :-), i just thought half of the deal with reflection is to be able to run the program. would seem a bit weird if you couldn't run the RCF solver they did, you guys were talking about axioms in the implementations of R, so i was wondering if they were blocking the computations in their work or not. | 06/04 21:20 |

fax | oh there are no axioms for setoids | 06/04 21:21 |

fax | you define it as a type paired with an equivalence relation, and then prove every function from S to S' repects equality so that you can do rewrites | 06/04 21:22 |

fax | coq axiomatizes a classical (non computational) R but it seems like (whether this procedure uses that R or any other) that is not really important, since the computation is mostly symbolic -- or done on rationals | 06/04 21:23 |

stevan | ok | 06/04 21:24 |

fax | yeah if you can't run the program then you can't use it for proofs.. this is very frustrating because I had to rewriting {prime p} + {~prime p} from scratch and by the tmie I did that I was had no enegry to prove what I actually wanted | 06/04 21:24 |

stevan | so their RCF solver is most likely runnable then? (just making sure :-) | 06/04 21:26 |

fax | well the constructivist thing to do will be try it out :) | 06/04 21:26 |

fax | lets find the source code | 06/04 21:26 |

fax | I didn't manage that before | 06/04 21:26 |

stevan | me neither | 06/04 21:26 |

fax | # CAD: Je travaille sur une implémentation et une preuve formelle de correction (en Coq) d' un algorithme de Décomposition Algébrique Cylindrique (CAD). Cette formalisation achevée permettrait d' obtenir une procédure de preuve automatique pour l' arithmétique réelle non linéaire, produisant des certificats formels de ses résultats. | 06/04 21:30 |

fax | "# CAD: I am working on the implementation and formal proof of correctness (in Coq) of a Cylindrical Algebraic Decomposition (CAD) algorithm. This would lead to an automated proof production decision procedure for non linear real arithmetic. " | 06/04 21:30 |

fax | so maybe it's not quite finished yet | 06/04 21:30 |

stevan | if i remember, i could probably ask thierry about it tomorrow... | 06/04 21:33 |

stevan | but it seems the formath people have to solve this problem (if it isn't solved already)? | 06/04 21:40 |

fax | formath? | 06/04 21:40 |

stevan | i asked you about it yesterday? you said you had read about it? http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath | 06/04 21:41 |

fax | me?? | 06/04 21:41 |

stevan | 21:04 < stevan> have you read about the formath project? | 06/04 21:42 |

stevan | 21:05 < fax> yeah | 06/04 21:42 |

stevan | 21:05 < stevan> that sort of stuff? | 06/04 21:42 |

stevan | 21:05 < fax> yes | 06/04 21:42 |

stevan | do you have an evil twin? | 06/04 21:42 |

fax | This 'ForMath' sounds great | 06/04 21:43 |

stevan | there is more under "Research Methodology" | 06/04 21:44 |

stevan | so if you had not seen this before, what were formath project were you saying you had read about yesterday? :-p | 06/04 21:49 |

fax | I've seen this | 06/04 21:50 |

stevan | ok | 06/04 21:51 |

--- Day changed Wed Apr 07 2010 | ||

vlad__ | hey manuel | 07/04 08:52 |

vlad__ | do you recken you can help me out a little with my assignment? | 07/04 08:53 |

stevan | fax: i found some code: http://perso.crans.org/cohen/closedfields/ i'm not sure if it's the whole thing tho... | 07/04 15:23 |

stevan | from what i could gather it's not runnable, due to Qeds. | 07/04 15:24 |

stevan | and removing the Qeds makes type checking too slow. | 07/04 15:25 |

fax | tarnge | 07/04 15:26 |

fax | strange | 07/04 15:26 |

stevan | i asked "so what's the plan?", "i don't know, maybe CBN instead of CBV might help" | 07/04 15:27 |

npouillard | stevan: what do you want to run? | 07/04 15:27 |

stevan | the solver | 07/04 15:27 |

stevan | as you can run agda's (to prove things) | 07/04 15:28 |

stevan | s/agda's/agda's ring solver/ | 07/04 15:29 |

npouillard | stevan: OK, so that's more "a program written with tactics", than "a proof we want to look at", right? | 07/04 15:31 |

stevan | yea, a reflective tactic | 07/04 15:32 |

stevan | it might be interesting to look at it also, imagine a formula in Presburger: forall x, exists y. x < y. running the program with x = 1 will actually give you a y + the proof that that y is larger | 07/04 15:35 |

fax | you can extract f : nat -> nat from the proof forall x, exists y. x < y | 07/04 15:35 |

stevan | when the decision procedure is written using (external) tactics? | 07/04 15:36 |

fax | it should be true in general | 07/04 15:37 |

stevan | well when you do it reflectively the proof is that function? | 07/04 15:37 |

fax | I just mean it shouldn't matter if how the statement is proved | 07/04 15:38 |

npouillard | fax: no it does not matter, tactics just build programs | 07/04 15:39 |

stevan | i'm not sure what happens when the proof is an external tactic and you run it. do you pass the value down to ocaml/etc and it gives you a value back? | 07/04 15:39 |

npouillard | (ugly and large ones actually) | 07/04 15:39 |

fax | tactics in coq are just scripts that write out lambda terms | 07/04 15:40 |

npouillard | an external tactic is an OCaml function that have to build/search a proof term that will be checked by the Coq kernel | 07/04 15:40 |

npouillard | try "Print mylemma." to see it | 07/04 15:40 |

fax | but (forall a : A, exists b : B, aRb) <-> (exists f : A -> B, forall a, aR(f a)) | 07/04 15:41 |

stevan | (ah right, i remember having printed lemmas now) | 07/04 15:42 |

stevan | so what does the Qed do? i didn't get that yesterday... | 07/04 15:43 |

* stevan reads logs | 07/04 15:45 | |

npouillard | Qed, type-check the term and then hide its definition | 07/04 15:45 |

npouillard | like 'abstract' in agda | 07/04 15:45 |

npouillard | Defined, keeps the definition accessible | 07/04 15:46 |

stevan | so effectively it blocks type level computations? | 07/04 15:47 |

npouillard | stevan: any computation that would like to unfold mylemma to its definition | 07/04 15:49 |

stevan | ok, interesting | 07/04 15:50 |

fax | ugh that "peano arithmetic homework" guy is on here too http://stackoverflow.com/questions/2576870/im-working-on-peano-axioms-in-agda-and-ive-hit-a-bit-of-a-sticking-point | 07/04 17:12 |

liyang | Perhaps Manuel should add a footnote to let his students know that everyone who knows Agda knows everyone else who knows Agda. | 07/04 17:16 |

fax | what I don't get is why people are too shy to just say "I can't do this" and hand in nothing | 07/04 17:18 |

fax | this is sick http://stackoverflow.com/questions/476959/why-cant-programs-be-proven | 07/04 17:20 |

fax | it's all "Godel Godel Godel Turing Halting Incompleteness" or "proofs are too hard and cost lots of money!" | 07/04 17:21 |

fax | hehe 'How do you prove your Coq specification is correct?' | 07/04 17:22 |

maltem | That's how all those ask-a-question sites are like | 07/04 17:27 |

fax | it's really a shame because all this rubbish and misinformation is the source which people learn form :| | 07/04 17:28 |

maltem | No, people learn from wikipedia :p | 07/04 17:28 |

glguy | What is a good reference for the typing rules pertaining to the different Set levels? | 07/04 18:08 |

--- Day changed Thu Apr 08 2010 | ||

Associat0r | guys what are the pro's and cons of Uniqueness typing vs Monads for IO? | 08/04 03:11 |

fax | oh oh pigworker | 08/04 15:54 |

fax | re "Up till now I had figured that Epigram 2 with its OTT logic would have everything I want: proof irrelevance, functional extensional equality, etc. Matthieu asked me what OTT loses. I said that it loses inductive types in Prop, but I figured that was no big deal. Then Matthieu asked me how to do well-founded recursion in OTT. The problem is that Acc is inductively defined. I had assumed that there would be some non-inductive replacement for it, but now it is | 08/04 15:54 |

pigworker | fax: what's up? | 08/04 15:54 |

pigworker | fax: I've seen it. Am replying now. | 08/04 15:55 |

fax | I'm wondering if that's so ? you have to do Acc in Set | 08/04 15:55 |

fax | ok | 08/04 15:55 |

pigworker | fax: yes, but Edwin kills it anyway! | 08/04 15:55 |

fax | ah!! | 08/04 15:55 |

* edwinb feels his ears burning | 08/04 15:57 | |

fax | roconnor <repeating> | 08/04 15:58 |

fax | 14:55 < fax> I'm wondering if that's so ? you have to do Acc in Set | 08/04 15:58 |

fax | 14:55 < fax> ok | 08/04 15:58 |

fax | 14:55 < pigworker> fax: yes, but Edwin kills it anyway! | 08/04 15:58 |

fax | this is that need not store their indices I am guessing | 08/04 15:58 |

pigworker | fax: yes | 08/04 15:58 |

edwinb | indeed | 08/04 15:58 |

roconnor | fax: link | 08/04 16:00 |

fax | link to what ? | 08/04 16:00 |

fax | http://www.cs.st-andrews.ac.uk/~james/RESEARCH/indices.pdf ? | 08/04 16:00 |

roconnor | need not store their indices | 08/04 16:00 |

roconnor | is acc specifically mentioned in this paper? | 08/04 16:01 |

fax | actually I think it is.. | 08/04 16:01 |

edwinb | I think it's in my thesis | 08/04 16:02 |

edwinb | I can't remember though, it was so long ago ;) | 08/04 16:02 |

fax | 7.3Accessibility Predicates | 08/04 16:02 |

fax | but this is Bove-Capretta | 08/04 16:02 |

fax | which is slightly different from Acc | 08/04 16:02 |

roconnor | probably close enough | 08/04 16:03 |

edwinb | aha. Page 51 of my thesis | 08/04 16:03 |

roconnor | does this mean there is no need to separate Prop and Set universes? | 08/04 16:04 |

edwinb | actually, no, not page 51, that doesn't explain it | 08/04 16:04 |

fax | I had always gathered that 'Prop/Set distinction' is just one way to do it | 08/04 16:04 |

edwinb | well it's still useful | 08/04 16:04 |

fax | edwinb yes I am not happy about #debill too! | 08/04 16:05 |

Saizan | i guess it's still useful to have an equality proof for free for anything that's in Prop | 08/04 16:05 |

Saizan | #debill ? | 08/04 16:06 |

* edwinb blinks | 08/04 16:06 | |

fax | you twitted about it 4 hours ago and already forgot ? :p | 08/04 16:06 |

edwinb | no, I just forget that people might notice the rubbish I talk on twitter ;) | 08/04 16:06 |

edwinb | (It was more than 4 hours ago, that gadget is broken) | 08/04 16:07 |

fax | Saizan - I think they're making up crazy laws to give them stronger control of people | 08/04 16:07 |

fax | anyway a bit paranoid | 08/04 16:07 |

fax | seems like with this new one you could just pick an arbitrary person, 'prove' they have download a file and then disallow them to use lightspeed communication | 08/04 16:07 |

Saizan | ah, i've read about that | 08/04 16:08 |

pigworker | roconnor: comment shipped! | 08/04 16:10 |

roconnor | thanks | 08/04 16:10 |

edwinb | Anyway. The intuitive reason why Acc is erasable is that the arguments to constructor just get you another Acc in the end | 08/04 16:10 |

edwinb | so there's no content there that you can't get from the indices (which is what you're actually computing with) | 08/04 16:10 |

edwinb | same goes for Bove-Capretta domain predicates | 08/04 16:11 |

fax | edwinb - one thing I was a bit fuzzy on was when there's multiple possible ways to erase something.. but I guess there's exactly one way for Acc (is that true?) | 08/04 16:11 |

edwinb | do you have an example in mind? | 08/04 16:11 |

edwinb | The only implementation of this I know of is in Idris, and that just picks the first erasure it sees | 08/04 16:11 |

edwinb | if there's a choice between erasing an index or a constructor tag, it erases an index | 08/04 16:12 |

fax | oh well I recall some on the paper there was 3 different ways to erase things from Vec-E | 08/04 16:12 |

edwinb | ah right | 08/04 16:12 |

edwinb | yes, that didn't explain. But in practice I've found it only makes sense to erase tags if you end up erasing the entire thing | 08/04 16:13 |

fax | that sounds good yeah -- and certainly that case will apply to (zero or) one constructor types like Acc | 08/04 16:13 |

edwinb | yes | 08/04 16:13 |

fax | hmm | 08/04 16:13 |

fax | so okay I have another question :) | 08/04 16:13 |

edwinb | incidentally, I've also found doing this erasure step makes compilation faster overall | 08/04 16:14 |

edwinb | because code generation is much easier ;) | 08/04 16:14 |

fax | what if I defined a relation a < b then write a function subtract : forall a b : |N, a < b -> |N | 08/04 16:14 |

Saizan | it's still whole program compilation though, right? | 08/04 16:14 |

edwinb | fax: depends how you define the relation and the function. But you could possibly write it by induction over the relation, and still be able to erase the relation | 08/04 16:16 |

edwinb | Saizan: it is, but I don't think it has to be | 08/04 16:16 |

edwinb | I might have to think about that soon. Compilation times are starting to get a bit irritating for bigger things. | 08/04 16:17 |

pigworker | fax: intuitively, you only need the proof to dismiss the impossible case, so there's no need to retain it at runtime; you could use a squashed set for the relation | 08/04 16:18 |

fax | what's a squashed set? | 08/04 16:19 |

fax | I think I read about squash types actually, and you can make a monad out of them | 08/04 16:19 |

fax | but how would you define it in say epigram ? | 08/04 16:19 |

fax | or would it be a feature | 08/04 16:20 |

roconnor | I like to pretend a squashed type of A is (A -> 0) -> 0, though this isn't quite true | 08/04 16:20 |

edwinb | I just happen to have this example handy, hang on... | 08/04 16:20 |

pigworker | fax: it's a set with all elements identified; or in Epigram 2 (already!) it's the proposition that a set is inhabited | 08/04 16:21 |

roconnor | ah right, inhabited A | 08/04 16:21 |

roconnor | pigworker: are there any advantages of squash types over (A -> 0) -> 0? | 08/04 16:22 |

edwinb | http://www.cs.st-andrews.ac.uk/~eb/hacking/minus.idr | 08/04 16:22 |

edwinb | hmm, something mysterious has happened there | 08/04 16:23 |

fax | mysterious? | 08/04 16:26 |

edwinb | I fixed it an reuploaded in the hope you wouldn't notice the bug in the optimiser that was overzealous ;) | 08/04 16:27 |

pigworker | I wonder whether we could replace A inhabited by ((a : A) => FF) => FF; it's not clear how it would compute, but perhaps we don't care | 08/04 16:27 |

Saizan | btw, is there any additional requirement to make something into an opSimp other than proving the stuck term and the simplified one equal? | 08/04 16:31 |

dolio | Nathan Mishra-Linger's thesis argues that there's no need for a Prop vs. Set universe distinction, and because squashed vs. unsquashed covers it (roughly, I think). I'm not sure whether I believe it or not, though. | 08/04 16:34 |

dolio | I guess roconnor's gone now, though. | 08/04 16:34 |

fax | hi dolio I have had lots of questions to ask you !! but I odn't remember them now :))) | 08/04 16:37 |

dolio | Heh. | 08/04 16:39 |

pigworker | Saizan: strictly speaking, you also need to make sure simplification terminates and check uniqueness of the resulting normal forms | 08/04 16:40 |

pigworker | dolio: what happens to propositional equality in Nathan's setting? | 08/04 16:41 |

dolio | I suppose whether it's true depends on his treatment of proof irrelevance. And I seem to recall that pigworker told me he had a conversation with Tim Sheard (probably) about EPTS proof irrelevance being fatally flawed. But I haven't read that section of the thesis yet. | 08/04 16:41 |

Saizan | pigworker: ah, yeah, makes sense :) | 08/04 16:42 |

pigworker | dolio: I had a conversation with Nathan where it became clear that erasing equality proofs in open computation caused bad things to happen | 08/04 16:42 |

dolio | pigworker: I think it gets erased down to an un-erasable unit type (un-erasable without undesirable consequences for the decidability of the theory, I think). | 08/04 16:43 |

fax | it's a good way to implement unsafeCoerce in haskell | 08/04 16:43 |

dolio | Ah. | 08/04 16:43 |

fax | (though that's about nontermination rather than open) | 08/04 16:43 |

dolio | pigworker: Basically, everything in it gets erased and 'refl' tokens get passed around. | 08/04 16:44 |

dolio | Maybe that isn't a Prop vs. Set issue, though. | 08/04 16:46 |

pigworker | dolio: ok, three questions; is equality elimination strict? is equality proof irrelevant? are refl tokens passed in closed computation? | 08/04 16:46 |

dolio | Since you've all just been discussing similar problems with erasing Props. | 08/04 16:46 |

dolio | I'm not 100% sure. But in the sections I have read, I'd wager the answers are "yes", "no" and "yes". | 08/04 16:47 |

dolio | As I said, though, I haven't actually read the section on proof irrelevance yet. | 08/04 16:48 |

pigworker | dolio: if so, it should all work ok, but it won't offer as generous a definitional equality as possible or erase as much as possible at run-time; the Epigram 2 answers to those questions are "no", "yes", "no". | 08/04 16:57 |

glguy | What is a good reference for the typing rules pertaining to the different Set levels? | 08/04 18:04 |

fax | glguy I think they just make it up as they go | 08/04 18:05 |

fax | there's a reference manual in development but I don't think it has anything about this yet | 08/04 18:06 |

fax | http://article.gmane.org/gmane.comp.lang.agda/1092/ that's probably the most official thing, and the source code most formal | 08/04 18:08 |

dolio | Without universe polymorphism, it's pretty simple. You start with a pure type system, and have rules (Set i, Set j, Set (max i j)). | 08/04 18:23 |

dolio | And the sort of (co)data types has to be big enough to type the constructors. | 08/04 18:23 |

dolio | With universe polymorphism, you have things like (x : T) -> Set (f x), which get typed with a Set omega. | 08/04 18:25 |

--- Day changed Fri Apr 09 2010 | ||

BiscuitsLap | I'm having a really hard time on some home-work exercises on Agda about proofs using refl, sym, trans, cong, subst, etc. Could anyone point me to some more examples or documentation I could look at ? | 09/04 02:26 |

fax | do you know haskell | 09/04 02:28 |

BiscuitsLap | Yes | 09/04 02:28 |

fax | and GADTs? | 09/04 02:28 |

BiscuitsLap | Hmm, we've discussed those, but I wouldn't say I'm fluent in them :/ | 09/04 02:28 |

fax | you probably saw that cheesy 'well typed evaluation' example | 09/04 02:28 |

BiscuitsLap | The only real example in the slides is one for n+0==n | 09/04 02:29 |

dolio | Is that cheesey? | 09/04 02:30 |

BiscuitsLap | Don't suppose anyone has a link to that cheesy example :p? might help ;) | 09/04 02:31 |

dolio | http://65.254.53.221:8000/6305 | 09/04 02:34 |

Saizan | i'm not sure how much haskell GADTs help, since there it's the type inference mechanisms that uses refl, sym, trans, cong, subst, etc. when needed, behind the scenes | 09/04 02:34 |

BiscuitsLap | So does anyone know of anything that might help me ? | 09/04 02:41 |

fax | with what exactly | 09/04 02:42 |

BiscuitsLap | Understanding how to prove things with those kind of functions :/ | 09/04 02:43 |

fax | I don't really know what you mean | 09/04 02:43 |

BiscuitsLap | Well, first assignment was to write a unitMatrix function and a transpose function for matrices (Vec (Vec A m) n), | 09/04 02:44 |

fax | that sounds cool | 09/04 02:44 |

BiscuitsLap | second is to prove that transpose (unitMatrix {n}) == unitMatrix {n} | 09/04 02:44 |

fax | oh that sounds very difficult | 09/04 02:44 |

fax | can I see these functions | 09/04 02:44 |

Saizan | BiscuitsLap: are you stuck with something in particuler? | 09/04 02:45 |

BiscuitsLap | this is what I have so far: http://www.pastebin.org/142243 | 09/04 02:45 |

fax | I think he's stuck with the transpose proof ? | 09/04 02:45 |

fax | this proof looks incredibly difficult | 09/04 02:46 |

BiscuitsLap | Saizan: Not really, I just have no idea where to start. I tried doing cong increaseUnitMatrix ? on the transpose (unitMatrix {n}) == unitMatrix {n}, but that didn't really help me get any further :( | 09/04 02:46 |

BiscuitsLap | Well, luckily it's just an optional part of the assignment, but I'd still like to know how to approach a problem like that | 09/04 02:47 |

BiscuitsLap | oh btw those ==< > and ==# helpers were from some other document I read on this, weren't part of the slides/lecture or assignment | 09/04 02:48 |

fax | in the suc n case, | 09/04 02:48 |

fax | it's proving: | 09/04 02:48 |

fax | transpose (1 :: (vmap head (vmap (_::_ 0) (unitMatrix {n})))) :: vmap (_::_ 0) (unitMatrix {n}) == (1 :: (vmap head (vmap (_::_ 0) (unitMatrix {n})))) :: vmap (_::_ 0) (unitMatrix {n}) | 09/04 02:48 |

fax | probably that will use recursion having a proof of transpose (unitMatrix {n}) == unitMatrix {n} | 09/04 02:48 |

fax | but you can unfold the transpose to see proving that ^ is the same as proving this: | 09/04 02:49 |

fax | zip toprow (transpose2 (vmap head (vmap (_::_ 0) (unitMatrix {n})))) :: vmap (_::_ 0) (unitMatrix {n}) _::_ == (1 :: (vmap head (vmap (_::_ 0) (unitMatrix {n})))) :: vmap (_::_ 0) (unitMatrix {n}) | 09/04 02:49 |

Saizan | yeah, since unitMatrix {suc n} is defined in terms of unitMatrix {n} you want to recurse with transpose-unit too | 09/04 02:50 |

fax | oops that 'toprow' should have been something else | 09/04 02:50 |

Saizan | (probably) | 09/04 02:50 |

fax | so , correction: | 09/04 02:50 |

fax | zip (1 :: (vmap head (vmap (_::_ 0) (unitMatrix {n})))) (transpose2 (vmap (_::_ 0) (unitMatrix {n}))) _::_ == (1 :: (vmap head (vmap (_::_ 0) (unitMatrix {n})))) :: vmap (_::_ 0) (unitMatrix {n}) | 09/04 02:50 |

fax | now you can clearly see where it starts to get awkward | 09/04 02:51 |

fax | here it has got 'transpose2' but our recursive case has only mention of 'transpose' | 09/04 02:51 |

Saizan | fax: i think you mixed up the defs of transpose and transpose2 | 09/04 02:52 |

BiscuitsLap | Hmm, yeah | 09/04 02:52 |

fax | you're right!! | 09/04 02:52 |

BiscuitsLap | transpose2 was just another definition I thought would help out at some point | 09/04 02:52 |

fax | that is good news because it means the proof will be easier | 09/04 02:52 |

BiscuitsLap | Hmm, would it help to have transpose take off both a row and a column at once, just like unitMatrix adds both a row and a column at once ? | 09/04 02:57 |

fax | yes | 09/04 02:57 |

BiscuitsLap | fax: Would this definition make my life easier http://www.pastebin.org/142256 ? | 09/04 03:01 |

fax | it's much closer to the other thing so they the proof they are equivalent will be easier | 09/04 03:02 |

BiscuitsLap | ok, so with that definition I can do transpose-unit {suc n} = cong increaseUnitMatrix ? | 09/04 03:03 |

fax | no | 09/04 03:03 |

BiscuitsLap | ? | 09/04 03:04 |

BiscuitsLap | How about: | 09/04 03:05 |

BiscuitsLap | transpose-unit {suc n} = cong (_::_ (1 :: vmap head (vmap (_::_ 0) unitMatrix))) { }3 ? | 09/04 03:06 |

BiscuitsLap | both the transpose one as well as the unitMatrix one at least start with that, so I should be able to use cong like that, right ? | 09/04 03:07 |

BiscuitsLap | That would leave me to prove something to the effect of (just quoting emacs here): (zip (vmap head (vmap (_::_ 0) unitMatrix)) (transpose (vmap tail (vmap (_::_ 0) unitMatrix))) _::_ == vmap (_::_ 0) unitMatrix) | 09/04 03:09 |

fax | that sounds good | 09/04 03:09 |

BiscuitsLap | I suspect I'd have to use trans from there | 09/04 03:11 |

BiscuitsLap | Where I'd first prove something like vmap (_::_ 0) matrix == zip (replicate n 0) matrix _::_ | 09/04 03:12 |

BiscuitsLap | Would that move me in the right direction ? | 09/04 03:15 |

fax | yes | 09/04 03:15 |

BiscuitsLap | hmm, let's try | 09/04 03:16 |

Saizan | mh, how'd you call a proof of transpose (replicate n x :: m) == vmap (_::_ x) (transpose m) ? | 09/04 04:33 |

BiscuitsLap | ? | 09/04 04:40 |

BiscuitsLap | Not sure | 09/04 04:40 |

BiscuitsLap | But you sure are going faster than I am :/ | 09/04 04:40 |

Saizan | well, yeah, i've completed the proof, but i've quite more experience with Agda :) | 09/04 04:46 |

Saizan | btw, some nice properties to have about vmap are: | 09/04 04:47 |

Saizan | vmap-fusion : ∀ {A B C} {f : B -> C} {g : A -> B} {n} {v : Vec A n} -> vmap f (vmap g v) == vmap (λ x -> f (g x)) v | 09/04 04:47 |

Saizan | and | 09/04 04:47 |

Saizan | vmap-id : ∀ {A} {n} {v : Vec A n} -> vmap (λ x -> x) v == v | 09/04 04:47 |

BiscuitsLap | ooh, I was already working on the vmap-fusion one :p | 09/04 04:48 |

Saizan | those are the functor laws for "\ A -> Vec A n", btw :) | 09/04 04:49 |

BiscuitsLap | :-/? | 09/04 04:49 |

Saizan | oh, i'm referring to haskell's Functor typeclass or CT functors, but if you don't know them it's not important :) | 09/04 04:50 |

BiscuitsLap | Hmm, vmap-id was easy enough :) | 09/04 04:54 |

Saizan | they are quite similar, both simple inductions on the vector | 09/04 04:55 |

BiscuitsLap | Hmmm, one last bit to solve | 09/04 04:57 |

BiscuitsLap | currently I had vmap-fusion {A} {B} {C} {g} {f} {zero} {[]} = refl | 09/04 04:58 |

BiscuitsLap | and vmap-fusion {A} {B} {C} {g} {f} {suc n} {v :: vs} = cong (_::_ ?) vmap-fusion | 09/04 04:58 |

BiscuitsLap | struggling to define that ? | 09/04 04:58 |

BiscuitsLap | when I try to fill in "f ?", which should be of type C as requested, it fails :/ | 09/04 04:59 |

BiscuitsLap | oh | 09/04 04:59 |

BiscuitsLap | nvm | 09/04 04:59 |

Saizan | you need some parentheses around that | 09/04 04:59 |

Saizan | i.e. cong (_::_ (f ?)) vmap-fusion | 09/04 05:00 |

BiscuitsLap | Won't work either | 09/04 05:01 |

Saizan | oh, you switched f and g | 09/04 05:01 |

Saizan | in the patterns | 09/04 05:01 |

BiscuitsLap | Ah, crap, yes | 09/04 05:02 |

BiscuitsLap | Sorry about that :/ | 09/04 05:02 |

Saizan | btw, you can bind arguments by name, rather than position | 09/04 05:02 |

BiscuitsLap | oh ? | 09/04 05:02 |

Saizan | e.g. vmap-fusion {f = f} {g = g} {v = x :: xs} = cong (_::_ (f ?)) vmap-fusion | 09/04 05:03 |

BiscuitsLap | oooh, nice :) | 09/04 05:03 |

BiscuitsLap | that certainly cleans things up | 09/04 05:04 |

BiscuitsLap | Great, I've just written my first two actual proofs in agda :p | 09/04 05:04 |

Saizan | (tbc i could have said e.g. {f = foo}, since the one on the right is just bound there) | 09/04 05:04 |

BiscuitsLap | Yup, found out by the v = x :: xs part, thanks :) | 09/04 05:05 |

Saizan | congrats for the first proofs :) | 09/04 05:07 |

BiscuitsLap | would this be a good next step: transpose-inner : forall {A} {m n : N} {matrix : Matrix A (suc m) (suc n)} -> transpose (tail (vmap tail matrix)) == tail (vmap tail (transpose matrix)) | 09/04 05:09 |

BiscuitsLap | ? | 09/04 05:09 |

BiscuitsLap | wait... | 09/04 05:12 |

BiscuitsLap | that's probably not even true :/ | 09/04 05:12 |

BiscuitsLap | or is it :S | 09/04 05:13 |

Saizan | mh, i don't think it is in general | 09/04 05:14 |

BiscuitsLap | Hmmm | 09/04 05:14 |

Saizan | i didn't had a reason to try to prove that since i went with your original transpose | 09/04 05:15 |

BiscuitsLap | that was the (vmap head mat) :: transpose (vmap tail mat) one, right ? | 09/04 05:16 |

Saizan | yeah | 09/04 05:21 |

BiscuitsLap | ok, let's see, what kind of properties would I need, and what kind of properties could I deduce :/ | 09/04 05:22 |

Saizan | well, first of all, that transpose recurses on "n", so your proof is probably going to do the same, so you get the application to reduce | 09/04 05:24 |

Saizan | then in the "suc n" case you've to massage the goal into a form where you can just use transpose-unit {n} | 09/04 05:25 |

Saizan | i've looked at what "transpose (unitMatrix {suc n})" normalizes to and tried to simplify that expression, basically, but i had to prove a pair of extra properties and glue everything with cong and _==<_>_ | 09/04 05:27 |

BiscuitsLap | gah... | 09/04 05:37 |

BiscuitsLap | Been trying to deduce transpose-inner : forall {A} {m n : N} {matrix : Matrix A (suc m) (suc n)} -> transpose (vmap tail matrix) == tail (transpose matrix) | 09/04 05:37 |

BiscuitsLap | Just found out that refl suffices in both cases :/ | 09/04 05:38 |

BiscuitsLap | Hmmm | 09/04 06:07 |

BiscuitsLap | I'm not quite sure how to use vmap-fusion with sillyproof2 : {n : N} -> (vmap head (vmap (_::_ 0) (unitMatrix {n}))) == (replicate n 0) | 09/04 06:07 |

BiscuitsLap | I think it should be the subst rule, since I want to substitute the vmaps with another vmap | 09/04 06:08 |

Saizan | vmap-fusion is not that useful there, actually | 09/04 06:10 |

Saizan | however you'd use trans | 09/04 06:11 |

Saizan | "trans vmap-fusion ?" should fit there | 09/04 06:11 |

Saizan | however i think that proof is easier if you generalize over the matrix | 09/04 06:12 |

Saizan | i could be wrong though :) | 09/04 06:12 |

BiscuitsLap | Hmm, currently stuck at proving | 09/04 06:16 |

BiscuitsLap | sillyproof3 : {n : N} -> (vmap (\x -> 0) (unitMatrix {n})) == (replicate n 0) | 09/04 06:17 |

BiscuitsLap | should be easy enough to solve :/ | 09/04 06:17 |

BiscuitsLap | but I'm just not getting it | 09/04 06:17 |

BiscuitsLap | oooh, got it :) | 09/04 06:29 |

BiscuitsLap | Saizan: Would you be able to take a look and try to explain to me why the == in sillyproof is yellow in http://www.pastebin.org/142475 ? | 09/04 06:33 |

BiscuitsLap | oh wait, I think I got it working | 09/04 06:35 |

BiscuitsLap | Hmm | 09/04 07:00 |

BiscuitsLap | how would I go about defining combineproof : {A : Set} {n : N} {a b : A} {c d : Vec A n} -> (a == b) -> (c == d) -> (a :: c) == (b :: d) | 09/04 07:01 |

roconnor | Saizan, edwinb: I don't get why having a prop universe is needed in light of edwin's erasure mechinicm. | 09/04 10:33 |

roconnor | isn't everything you put into prop already provably proof irrelevent? | 09/04 10:33 |

roconnor | oh, but maybe not definitionally proof irrelevent. | 09/04 10:34 |

roconnor | are two variables of the same proposition convertable? | 09/04 10:34 |

Saizan | roconnor: it's at least trivial to prove equality of proofs | 09/04 12:39 |

Saizan | make eq := (\ P Q p q -> _) : (P : Prop) (Q : Prop) ( p : :- P) (q : :- Q) -> :- p == q | 09/04 12:39 |

Saizan | Made. | 09/04 12:39 |

roconnor | meh | 09/04 12:39 |

roconnor | it is simply *more* trivial | 09/04 12:39 |

roconnor | seems better to use generic programming than bake a special universe of propositions into the language | 09/04 12:40 |

Saizan | they might be convertible too, i'm not sure | 09/04 12:40 |

roconnor | ya, if they are convertable then that is something more. | 09/04 12:43 |

* Saizan wonders how you test that | 09/04 12:44 | |

Saizan | i think it's also to let coerce work without ever having to be strict on the equality proof | 09/04 12:50 |

Saizan | but that could have been guaranteed by how you define == i guess | 09/04 12:52 |

roconnor | isn't coerce never strict on any equality proof? | 09/04 13:06 |

roconnor | whether it is equality of set universe or prop universe | 09/04 13:06 |

Saizan | roconnor: yes, but i meant that Since the equality is of type ":- P" with P : Prop, it can only be made by pairs and foralls, no sum | 09/04 13:34 |

Saizan | err, that's not right | 09/04 13:34 |

Saizan | well, it is, taking P = A == B, however as i said that looks like it could be enforced simply by how you define == | 09/04 13:35 |

Saizan | so, disregard that :) | 09/04 13:35 |

pigworker | roconnor: sorry, we're out of sync... yes, in this setting, two variables inhabiting the same proof set are definitionally equal (if you embed Prop explicitly into Set, that's easy to implement); Prop's only an optimization of def-eq; without it, you can prove the same stuff but it's harder work | 09/04 20:34 |

Spockz | what is the difference between n and .n (dot) in "n != .n"? Is it that the dot denotes some kind of type or something? | 09/04 22:31 |

fax | . means that terms was inferred/forced by pattern match specialization | 09/04 22:31 |

Spockz | okay thanks :) | 09/04 22:33 |

liyang | if it says n != .n, those are two distinct names… (FYI.) | 09/04 22:37 |

Spockz | liyang: but it is based on something right? | 09/04 22:41 |

liyang | Yes. Often it makes sense to name constructor arguments in data declarations solely for the purpose of influencing what names the typechecker uses in its error messages. | 09/04 22:43 |

--- Day changed Sun Apr 11 2010 | ||

roconnor | in OTT are two variables of the same proposition type convertable? | 11/04 11:29 |

pigworker | yes. | 11/04 11:29 |

roconnor | neat | 11/04 11:32 |

roconnor | so two proofs of Acc foo won't be converable since Acc won't live in Prop. | 11/04 11:33 |

roconnor | ah | 11/04 11:34 |

roconnor | but it has to be that way | 11/04 11:34 |

roconnor | as you said | 11/04 11:34 |

roconnor | otherwise open reduction may not terminate | 11/04 11:34 |

pigworker | yes. | 11/04 11:34 |

roconnor | so it is impossible, at least for now | 11/04 11:34 |

pigworker | the two Acc proofs will be provably equal | 11/04 11:34 |

roconnor | since a few years ago extentional equality and decidable type checking was also "impossible" | 11/04 11:35 |

pigworker | the key problem with Acc is that strictness is the trust mechanism; if a lazier but reliable trust mechanism could be found, Acc could perhaps become proof irrelevant | 11/04 11:37 |

roconnor | I wonder if having convertablity between proof of the same propositions adds any expressive power to the language, or if it simply allows for more consice proofs. | 11/04 11:38 |

roconnor | more concretely put, is there a translation of OTT to the Prop free fragment of OTT | 11/04 11:38 |

pigworker | it's just an optimization | 11/04 11:38 |

pigworker | more concretely, yes there is such a translation | 11/04 11:38 |

roconnor | neat | 11/04 11:39 |

roconnor | okay I will think of Prop as an optimization | 11/04 11:39 |

dolio | That's how they define OTT in most of the papers, as I recall. | 11/04 11:39 |

dolio | OTT gets translated into a type theory with just 0, 1, 2, Pi, Sigma, W. | 11/04 11:39 |

pigworker | yeah, the Agda models are all in Set, with no def-prf-irr, but prop-prf-irr | 11/04 11:40 |

pigworker | The models have all the beta-behaviour of OTT, but a weaker equality on neutral values. | 11/04 11:42 |

pigworker | We call this weaker theory OTT- | 11/04 11:43 |

roconnor | if variables of the same type are converable, then OTT must not be strongly normalizing | 11/04 11:44 |

roconnor | (though even coq is not strongly normalizing) | 11/04 11:44 |

pigworker | OTT- is still extensional: it models extensional type theory (it implements Oury's API for extensionality) | 11/04 11:45 |

pigworker | The beta-rules are strongly normalizing, but they aren't the whole story. | 11/04 11:47 |

pigworker | There's a type-directed "quotation" process for beta-normal forms: that's where proofs get squashed. | 11/04 11:49 |

--- Day changed Tue Apr 13 2010 | ||

liyang | Does anyone know where I saw pigworker's acetate with a blue type saying to a couple of red terms, “You all look the same to me!” | 13/04 18:57 |

Saizan | mh, i think i saw that too | 13/04 18:59 |

liyang | Shall wait 'til he shows up. | 13/04 19:03 |

dolio | liyang: Sounds like something on the SHE page. | 13/04 20:03 |

fax | there is something I have been wondering -- there's a lot of category theory style reasoning going around but I don't tend to reified that often | 13/04 21:16 |

liyang | pigworker: evening there. Was wondering, where did I see that acetate of yours with the “You all look the same to me!” line? | 13/04 21:16 |

pigworker | liyang: http://img688.yfrog.com/i/3l5.jpg/ | 13/04 21:16 |

fax | is that from a set ? | 13/04 21:17 |

liyang | pigworker: ah right. Was struggling to find it on the SHE pages… | 13/04 21:17 |

* liyang didn't quite remember the quote right. | 13/04 21:18 | |

pigworker | It was a slide from TYPES Summer School 2005 which I found in the box of random from B3? which ended up in 7DG. It's from a small set of intro material, before I started doing live hacking. They're in a different box in Glasgow now... | 13/04 21:18 |

fax | set | 13/04 21:18 |

fax | pigworker (I think there's a missing newline in the draft of ornaments --3. definition of Alg) | 13/04 21:19 |

pigworker | fax: if that was all that was missing, I'd be a happy man... | 13/04 21:19 |

fax | this ornament stuff is so frustrating because I totally could have come up with that if I had just trid harder ;))) | 13/04 21:19 |

fax | oh what d you mean? | 13/04 21:20 |

fax | there is more to do with it | 13/04 21:20 |

pigworker | The Ornaments draft is quite a bit of windup but no punchline. | 13/04 21:22 |

pigworker | http://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.agda | 13/04 21:24 |

pigworker | Payoff 1: every ornament induces a (forgetful) algebra; every algebra induces a (labelling) ornament; so every ornament induces another ornament (e.g., the ornament which makes list from nat induces the ornament which makes vec from list) | 13/04 21:26 |

pigworker | Payoff 2, for every algebraic ornament, you get that if you erase the index, recomputing the fold by the algebra recovers the same index. (e.g., if you turn a vec into a list, then take its length, you get the vec index you forgot) | 13/04 21:30 |

fax | and that (2) proves that stack compiler respects evaluation ? | 13/04 21:30 |

pigworker | yep | 13/04 21:31 |

pigworker | but the code of the compiler is just the same as it would have been | 13/04 21:31 |

pigworker | of course, it's not always such an instant win, but it is progress | 13/04 21:33 |

kosmikus | I think it's a very beautiful result. | 13/04 21:34 |

pigworker | Once you've got indexed datatypes, you need it; once you've got a universe of indexed datatypes, you can have it! | 13/04 21:44 |

fax | wait this is awesome | 13/04 21:47 |

fax | if I defined + on nat it induces ++ on list AND vector | 13/04 21:47 |

pigworker | fax: depends how you define +, but you should get it cheap, certainly | 13/04 21:48 |

pigworker | The question is how to turn ornaments on functors to ornaments on their (co)algebras. | 13/04 21:53 |

fax | (just noticed also that data Data (D : Desc I) ... : [[ D ]] (Data D i) -> ... should probably be [[ D ]] (Data D) i | 13/04 22:00 |

fax | on pg. 4 | 13/04 22:00 |

pigworker | fax: seems likely, thanks | 13/04 22:47 |

--- Day changed Wed Apr 14 2010 | ||

liyang | (I think) I understand what it means to be parametric, but what are the immediate consequences of defining propositional equality as data _≡_ {a : Set} : a → a → Set , versus the standard library's data _≡_ {a : Set} (x : a) : a → Set ? | 14/04 00:47 |

liyang | Does it just mean that refl needn't carry around a copy of x, in order to serve as a witness to x ≡ x? | 14/04 00:48 |

copumpkin | hmm | 14/04 00:49 |

fax | they're logically equivalent | 14/04 00:50 |

fax | data Identity1 (A : Set) : A -> A -> Set where refl1 : forall (a : A) -> Identity1 A a a | 14/04 00:51 |

fax | data Identity2 (A : Set) (a : A) : A -> Set where refl2 : Identity2 A a a | 14/04 00:51 |

fax | id12 : forall {A : Set} (a : A) -> Identity1 A a a -> Identity2 A a a | 14/04 00:51 |

fax | id12 .a (refl1 a) = refl2 | 14/04 00:51 |

fax | id21 : forall {A : Set} (a : A) -> Identity2 A a a -> Identity1 A a a | 14/04 00:51 |

fax | id21 a refl2 = refl1 a | 14/04 00:51 |

liyang | But computationally? | 14/04 00:51 |

fax | I don't know which one is better | 14/04 00:52 |

fax | computationally? | 14/04 00:52 |

fax | I am pretty sure you can compile them both away | 14/04 00:52 |

fax | (to nothing) | 14/04 00:52 |

copumpkin | will agda? | 14/04 00:52 |

fax | no | 14/04 00:52 |

liyang | It's just that the former seems more intuitive to me, yet the stdlib (and various other sources) define it as the latter. | 14/04 00:53 |

fax | I think 2 is easier to use | 14/04 00:53 |

fax | because you don't have to worry about the actual element -- type inference does taht | 14/04 00:53 |

liyang | (by intuitive, I mean symmetrical.) | 14/04 00:54 |

fax | liyang, if you try to prove transitivity | 14/04 00:56 |

fax | trans : forall {A : Set} (a b c : A) -> Identity A a b -> Identity A b c -> Identity A a c | 14/04 00:56 |

liyang | Well, you could write refl : {x} -> x == x , where type inference will fill in the actual element. | 14/04 00:56 |

fax | for both types, that might convince you that one is nicer to use than the other | 14/04 00:56 |

liyang | fax: ahhh hah. I see. | 14/04 00:57 |

fax | data JMeq (A : Set) (a : A) : forall (B : Set) (b : B) -> Set where JMrefl : JMeq A a A a | 14/04 00:58 |

fax | this is a good one for Agda | 14/04 00:59 |

fax | data INeq (U : Set) (F : U -> Set) (i : U) (I : F i) : forall (j : U) (J : F j) -> Set where INrefl : INeq U F i I i I | 14/04 01:00 |

fax | that is useful in Coq | 14/04 01:00 |

fax | decidible equality on U lets you prove K axiom | 14/04 01:00 |

fax | but you don't want that in agda because you can prove K from the pattern matching | 14/04 01:01 |

liyang | fax: hang on, both proofs of transitivity are the same… http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=10097 | 14/04 01:21 |

* liyang didn't see after all. | 14/04 01:21 | |

fax | trans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c | 14/04 01:21 |

fax | trans1 a .a .a (refl1 ._) (refl1 ._) = refl1 _ | 14/04 01:21 |

fax | trans2 : forall {A : Set} (a b c : A) -> Identity2 A a b -> Identity2 A b c -> Identity2 A a c | 14/04 01:21 |

fax | trans2 a .a .a refl2 refl2 = refl2 | 14/04 01:22 |

fax | well | 14/04 01:22 |

fax | trans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c | 14/04 01:22 |

fax | trans1 a .a .a (refl1 .a) (refl1 .a) = refl1 a | 14/04 01:22 |

fax | let me be explicit | 14/04 01:22 |

liyang | Only if you make the argument of refl1 explicit… | 14/04 01:22 |

liyang | I had defined refl : {x : X} -> x ≡ x | 14/04 01:23 |

liyang | The two definitions of == in my pastebin above seem to be interchangeable, at least with trans. | 14/04 01:24 |

fax | in coq, you can still supply the parameters | 14/04 01:26 |

fax | i.e. A and a in refl2 | 14/04 01:26 |

fax | the difference there, is there is a slightly different type of type inference -- called maximal insertion | 14/04 01:27 |

fax | I think you could be right though, and given the {} annotation that these are interchangable | 14/04 01:28 |

* liyang isn't entirely au fait with Coq. | 14/04 01:28 | |

fax | well I just mention it because the difference between these two versions is more apparent in Coq | 14/04 01:28 |

liyang | mmkay… | 14/04 01:28 |

* liyang has a nagging feeling he'd asked NAD this same question at some point in the past. | 14/04 01:29 | |

pigworker | They have names. "Martin-Löf equality" takes just the set as as the parameter; "Paulin-Mohring equality" takes the set and one of the elements as parameter. | 14/04 01:30 |

fax | ahh need to remember that | 14/04 01:31 |

liyang | That can't just be the end of it, shurely? | 14/04 01:31 |

liyang | Are there any reasons to prefer one over the other, at least in the context of Agda? | 14/04 01:33 |

pigworker | You've gotta watch the sizes of things. Parameters can be large, but indices are (currently, mysteriously) obliged to be small. | 14/04 01:33 |

pigworker | P-M eq beats M-L eq in Agda. Why make refl store more stuff? | 14/04 01:34 |

liyang | So, just “<liyang> Does it just mean that refl needn't carry around a copy of x, in order to serve as a witness to x ≡ x?” ? | 14/04 01:35 |

* liyang isn't terribly clear on the large/small distinction, and now is probably not a good time to inquire about it. | 14/04 01:36 | |

fax | what you can erase during compiling is a lot more than what you can erase during typecheck time -- but that raises a question like if you have a big reflective computation that produces a bool.. does it really have to carry around all the indices | 14/04 01:36 |

fax | (bool is a bad example I guess.... maybe bad enough it ruins the actual question, since we'd probably have Maybe/option P at least) | 14/04 01:37 |

pigworker | IIRC there is some size paranoia which stops the two presentations being equivalent under all circumstances, but usually it's no big deal | 14/04 01:38 |

liyang | Mmkay. I'll go with M-L equality as it seems easier to explain, storage be damned. | 14/04 01:40 |

pigworker | liyang: Generally, it's tidier to make things parameters rather than indices if poss. That said, the point of "pattern matching" is that it doesn't matter. | 14/04 01:42 |

liyang | pigworker: this is just for an introductory section to dependent types. I wouldn't dream of writing untidy code. :3 | 14/04 01:47 |

pigworker | fax: a question on a cusp; speculation -- reflection given syntax with variables relies only on *closed* computation, and can thus be optimized, albeit at compile time, with everything you can throw at runtime | 14/04 01:47 |

pigworker | liyang: whatever gets you where you need to go | 14/04 01:48 |

pigworker | Just remember, equality is always some sort of fart. You can make a case for the necessity, but you can't get away with claiming yours is the best. | 14/04 01:50 |

fax | equality made my attempts to implement category theory fail :( | 14/04 01:52 |

pigworker | fax: or vice versa | 14/04 01:52 |

pigworker | g'night all | 14/04 01:59 |

copumpkin | oh my | 14/04 02:01 |

copumpkin | I missed pigworker | 14/04 02:02 |

copumpkin | it feels like forever since I last wrote any agda | 14/04 16:15 |

fax | It's been seven hours and fifteen days | 14/04 16:16 |

copumpkin | lol | 14/04 16:16 |

copumpkin | I'm glad you're keeping track :) | 14/04 16:16 |

Saizan_ | copumpkin is back! | 14/04 16:19 |

copumpkin | more or less :) | 14/04 16:19 |

stevan | hello, does the following make sense: a version of filter which creates a proof of what has been filtered, so that when one goes thru the resulting list one only has to pattern match on whatever one filtered out (the rest are absured patterns by the proof filter built)? | 14/04 16:25 |

fax | not to me | 14/04 16:27 |

fax | you're turning a list [A] into [Sigma a : A, P(a)] ? | 14/04 16:27 |

fax | by filtering out things which don't have property P | 14/04 16:28 |

stevan | yeah something like that | 14/04 16:28 |

fax | different in what ways? | 14/04 16:28 |

Saizan_ | the part after "so that" is quite unclear | 14/04 16:29 |

stevan | fax: i'm not sure of how it would work exactly, i didn't think of it as a list of sigmas, but i guess that could work... | 14/04 16:30 |

stevan | Saizan_: well say you filter out all zeroes from a list, then when you go thru that filtered list every time you hit a suc constructor you could say this is absurd, because filter should have removed all non-zero nats... is that clearer? | 14/04 16:32 |

Saizan_ | i understand "filtering out" as "removing" | 14/04 16:33 |

Saizan_ | but i'm not a native speaker | 14/04 16:33 |

fax | I guess you can also just have filter atke [A] -> [A] | 14/04 16:33 |

fax | but then prove sepeartetly (P1) xs >= filter xs (P2) In x xs -> P x | 14/04 16:34 |

Saizan_ | http://www.google.com/dictionary?aq=f&langpair=en|en&hl=en&q=filter%20out <- google agrees with me though | 14/04 16:34 |

fax | but I don't know, that is probably harder to program with, because you'll need to construct In proofs as you o through the list | 14/04 16:34 |

fax | oh and that P2 was wrong | 14/04 16:34 |

dolio | Stop absuring the man! :) | 14/04 16:35 |

fax | Saizan, if you think about say a gold pan -- that lets water through but keeps the bits of gold ... the question is, did it filter out the gold or filter out the water? | 14/04 16:35 |

Saizan_ | i'd say it filtered out the water | 14/04 16:36 |

copumpkin | this is so philosophical! | 14/04 16:36 |

dolio | It filtered out the gold. | 14/04 16:37 |

dolio | What comes out of the filter is water without gold. The gold gets caught. | 14/04 16:38 |

dolio | Filtered out of the water. | 14/04 16:38 |

dolio | Or mud. Or what have you. | 14/04 16:38 |

fax | if I passed through a filter, was I filtered? | 14/04 16:38 |

Saizan_ | ooh, so what you filter out is what gets caught in the filter | 14/04 16:38 |

fax | but if you got stuck in the filter, were you filtered? | 14/04 16:38 |

fax | maybe BOTH ? | 14/04 16:38 |

Saizan_ | i was just thinking in terms of keeping vs. removing | 14/04 16:38 |

Saizan_ | i.e. seeing the filter as merely a splitter | 14/04 16:39 |

TheOnionKnight | almost sounds like you want List A -> List (Sigma (x : A) -> Dec (P x)) ? | 14/04 16:39 |

fax | well the way stevan put it was defintiely contrary ti what I thought about before | 14/04 16:39 |

dolio | Filtered water is what you're left with after you filter out the impurities. | 14/04 16:39 |

fax | but I am not sure that I can say it's wrong | 14/04 16:39 |

dolio | And the impurities get caught in the filter. | 14/04 16:39 |

copumpkin | if you empty out the filter though, what are the impurities? | 14/04 16:39 |

copumpkin | are they filtered impurities? | 14/04 16:39 |

Saizan_ | dolio: ok, i see it now | 14/04 16:39 |

fax | TheOnionKnight: oh that's neat because it's just map | 14/04 16:40 |

fax | then you can use a normal filter | 14/04 16:40 |

fax | hmm no | 14/04 16:40 |

stevan | it reminds me of the sublist exercise in ulf's tutorial, but you need to stick the proof in there somehow | 14/04 16:42 |

fax | there's two different properties though | 14/04 16:42 |

pigworker | What does filter tell you about its input? | 14/04 16:45 |

fax | you could also make a data for it and write filter : (xs : [A]) -> Filter xs -- data Filter : [A] -> Set where nil : Filter nil ; yes : (x : A) -> P x -> Filter xs -> Filter (x :: xs) ; no : (x : A) -> Filter xs -> Filter (x :: xs) | 14/04 16:51 |

pigworker | an algebraic ornament, indeed! | 14/04 16:53 |

fax | ohh :D | 14/04 16:53 |

Saizan_ | you could keep "not (P x)" in there too at that point :) | 14/04 16:53 |

pigworker | you could also index by the yes- and no-lists | 14/04 16:54 |

dolio | The types reddit is really languishing. | 14/04 16:58 |

dolio | Apparently the only types worth talking about these days are dependent types. | 14/04 16:58 |

fax | why the fuck is there like 10 reddits about dependent types :/ | 14/04 16:59 |

fax | worse than /types/ having no activity is jbapple stopped blogging | 14/04 17:00 |

dolio | I could do with more constructive gems/stones, too. | 14/04 17:09 |

fax | :( | 14/04 17:10 |

fax | sometimes there are "proof pearl" papers which I can't acess | 14/04 17:10 |

copumpkin | I can fetch them for you if you want | 14/04 17:10 |

copumpkin | if you don't rat me out | 14/04 17:10 |

fax | well something I WOULD like is a list of all of them | 14/04 17:10 |

fax | but I am not sure if that actually exists | 14/04 17:10 |

dolio | The last 'classical mathematicians confuse proof by contradiction with proof of negation' was amusing, but not particularly exciting. | 14/04 17:11 |

fax | the closest to a list of the 'functional peal's we have is that haskell wiki | 14/04 17:11 |

ccasin | So I'm looking at Luo's definition of UTT, and it doesn't seem to account for indexed data types in UTT proper, but only as definitions in the meta language | 14/04 17:18 |

ccasin | anyone know if that's right, and if anyone has actually worked out the metatheory in detail for one of the languages where we hardwire in indexed datatypes? | 14/04 17:18 |

ccasin | (sorry to drag the conversation away from fun programs towards scary theory) | 14/04 17:18 |

pigworker | ccasin: that's right -- Luo considers inductive definition as a way to make a type theory with a new primitive type, not as a feature of the type theory itself | 14/04 17:20 |

pigworker | ccasin: Calculus of Inductive Constructions takes a more internal view, although descriptions of datatypes are not first class | 14/04 17:21 |

ccasin | pigworker: yeah, thanks. And it seems like these new primitive types in UTT don't have parameters/indices. He only adds those using the metatheory | 14/04 17:22 |

ccasin | that is, inductive pairs aren't a UTT type, only an LF construction (even after we add them as a primitive) | 14/04 17:23 |

ccasin | I should read some of the early Cic papers, thanks | 14/04 17:24 |

pigworker | ccasin: Each Sigma A B has kind Type (ie is a UTT type), but Sigma itself is a meta-level thing. | 14/04 17:24 |

pigworker | I want to be able to write dotted constructors in patterns, e.g. (x .:: xs), when I know it's a cons, but I still want the bits. | 14/04 17:36 |

dolio | Like 'f (x .:: xs) cons-proof' instead of 'f .(x :: xs) (cons-proof {x} {xs})'? | 14/04 17:39 |

pigworker | dolio: the very thing | 14/04 17:39 |

dolio | Yeah, I've run into that before. | 14/04 17:39 |

fax | does f (x :: xs) .cons-proof = ... work? | 14/04 17:39 |

pigworker | fax: no, it makes f too strict | 14/04 17:40 |

pigworker | what's that pastebin thing again? | 14/04 17:42 |

copumpkin | moonpatio.com | 14/04 17:42 |

pigworker | connection trouble; made a repo on the web for fooling about; here's a filtery thing http://personal.cis.strath.ac.uk/~conor/fooling/Splice.agda | 14/04 17:47 |

copumpkin | omg no unicode | 14/04 17:49 |

pigworker | I hate unicode | 14/04 17:50 |

copumpkin | :) | 14/04 17:50 |

copumpkin | sometimes I think NAD peruses code tables looking for the most obscure symbols for the standard library | 14/04 17:50 |

pigworker | early adopters... | 14/04 17:52 |

npouillard | pigworker: have you any good reason? sure there is some initial configuration cost but that's not that hard | 14/04 17:52 |

fax | that's neat with the split sort of like [Either a b] -> ([a],[b]) | 14/04 17:53 |

kosmikus | the main thing for me is that while unicode works nice in emacs, perhaps, it's difficult to use standard Unix tools (say grep, sed) with it | 14/04 17:53 |

copumpkin | yeah | 14/04 17:53 |

pigworker | npouillard: even now, it's not a reliable exchange format | 14/04 17:53 |

fax | I think unicode just delays proper typesetting longer | 14/04 17:54 |

npouillard | fax: I think it is orthogonal | 14/04 17:54 |

pigworker | npouillard: and my typing isn't reliable enough, and massive keyboard shortcut customization is the road to hell | 14/04 17:55 |

fax | I mean the silly bits, like little superscript 2's and fractions | 14/04 17:55 |

npouillard | even when doing proper typesetting you may want something nicer than \alpha | 14/04 17:55 |

npouillard | pigworker: it becomes more reliable when people use it | 14/04 17:55 |

npouillard | Personally I use a .XCompose file under linux, so it works in any X application, and is nicely configurable | 14/04 17:57 |

kosmikus | yes, ultimately I think it's good to have more symbols available | 14/04 17:57 |

kosmikus | npouillard: I'll look into that | 14/04 17:57 |

fax | what I really want is something that looks like epigram research papers :P | 14/04 17:57 |

fax | (sort of like texmacs) | 14/04 17:58 |

pigworker | npouillard: in this sense, I'm a late adopter; life's too short for installing all the necessary gadgets, and for persuading my mates to install them too | 14/04 18:00 |

pigworker | When I've been an editor of this and that, I find myself awarding KILL-DEATH-MURDER points to people whose LaTeX choices force me to go hunting for random extra files or fonts. The runaway winner is...? | 14/04 18:02 |

kosmikus | me? | 14/04 18:03 |

kosmikus | :) | 14/04 18:04 |

pigworker | kosmikus: no, but you do quite well | 14/04 18:04 |

kosmikus | when it comes to LaTeX, I'm certainly guilty | 14/04 18:04 |

kosmikus | although I usually know what packages I'm using and try to include them if they're exotic | 14/04 18:05 |

copumpkin | gotta use xetex | 14/04 18:05 |

pigworker | I heard a rumour that EasyChair was starting to support LaTeX-on-the-server. | 14/04 18:05 |

copumpkin | so you can include exotic fonts that people have to pay for | 14/04 18:05 |

copumpkin | just to piss them off more | 14/04 18:06 |

kosmikus | pigworker: I think it does. I used it recently. | 14/04 18:07 |

pigworker | It should be part of the submission process to make the damn thing compile on the server, but with the option to upload exotic goodies. Is that what they do now? | 14/04 18:07 |

kosmikus | yes | 14/04 18:08 |

pigworker | progress | 14/04 18:08 |

kosmikus | and you can check the pdf the server generates | 14/04 18:08 |

kosmikus | a bit like what arxiv does since ages | 14/04 18:08 |

pigworker | you'd kinda need that feedback | 14/04 18:09 |

pigworker | gonna catch some sun while it's still up; back later | 14/04 18:25 |

stevan | sorry, had friends drop by... thanks for the help with filter, guys. i like the splice solution. | 14/04 19:19 |

stevan | kosmikus: i think if you use grep from within emacs you can get use agda's unicode input mode there as well... agda's input mode doesn't play well with viper-mode however... | 14/04 19:26 |

kosmikus | stevan: yes, I noted that (viper) | 14/04 19:55 |

--- Day changed Thu Apr 15 2010 | ||

sah0s | Hi ... I am trying to get my head around dependently typed functional programming languages. Could anyone explain intuitionistic type theory to me in plain English and not formal mathematics so that I have a clear idea of the model in my head. | 15/04 14:33 |

sah0s | I have the idea that types are related to sets in that they have membership and equality (based on structural not membership equality) but from there I am at a loss. | 15/04 14:34 |

fax | it's like normal functional programming, except the types have a logical interpretation | 15/04 14:34 |

sah0s | I have read http://en.wikipedia.org/wiki/Intuitionistic_type_theory | 15/04 14:34 |

npouillard | fax: you can give a logical interpretation to System F types however | 15/04 14:35 |

sah0s | I got that, the Curry-Howard isomorphism, I'm happy with that, in fact I love it | 15/04 14:35 |

sah0s | What I'm saying is that I can't model Types in my head ... | 15/04 14:35 |

npouillard | sah0s: even as just being sets? | 15/04 14:36 |

fax | a type is just a name, you don't need to think of it as something | 15/04 14:36 |

sah0s | I want to write a type system in C, I need to think of them as a bit more than a name :) | 15/04 14:37 |

dolio | You don't want to write a type system in C. | 15/04 14:37 |

npouillard | sah0s: a type checker in C ? | 15/04 14:37 |

sah0s | npouillard: set-like is fine with me | 15/04 14:37 |

fax | I agree with dolio | 15/04 14:37 |

sah0s | A type system with a checker, yeah ... as a library | 15/04 14:38 |

fax | sah0s no this is where you are confused | 15/04 14:38 |

sah0s | If I have a clear idea of how to construct types then I can code it | 15/04 14:38 |

npouillard | fax: your are a bit rude | 15/04 14:38 |

fax | I find you quite rude too | 15/04 14:39 |

dolio | (My point is that there are much nicer languages than C for doing it. Of course, if C is all you know, you don't have many options.) | 15/04 14:39 |

npouillard | But I agree that C is not a language to write a type-checker | 15/04 14:39 |

npouillard | fax: sorry then | 15/04 14:39 |

sah0s | Ignore the C bit for the moment :) | 15/04 14:39 |

sah0s | I like C | 15/04 14:40 |

fax | I wasn't talking about C when I said "This is where you are confused" | 15/04 14:40 |

sah0s | Each to their own :) | 15/04 14:40 |

stevan | sah0s: do you know any functional programming language? | 15/04 14:40 |

sah0s | Can we go through this page http://en.wikipedia.org/wiki/Intuitionistic_type_theory bit by bit, please! | 15/04 14:40 |

sah0s | What is a Π-type exactly, I don't understand what it says. | 15/04 14:41 |

fax | sah0s my advice is that wikipedia sucks and the reason you are confused is proabably from reading that page | 15/04 14:41 |

sah0s | okay | 15/04 14:41 |

sah0s | this could well be true | 15/04 14:41 |

npouillard | This question is relevant "do you know any functional programming language?" | 15/04 14:41 |

sah0s | I know a bit of scheme | 15/04 14:41 |

sah0s | functions as first-class citizens | 15/04 14:42 |

npouillard | to get Π you need to get → | 15/04 14:42 |

sah0s | tail recursion | 15/04 14:42 |

sah0s | → ? | 15/04 14:42 |

npouillard | sah0s: sure but not much of a type system | 15/04 14:42 |

npouillard | as in [a] → Int | 15/04 14:42 |

npouillard | the type of List.length | 15/04 14:42 |

npouillard | length : ∀ a. [a] → Int -- in haskell | 15/04 14:43 |

npouillard | length : ∀ {A} → List A → ℕ -- in agda but that merely the same thing | 15/04 14:43 |

dolio | It helps to get ∀, too | 15/04 14:43 |

sah0s | is A a type variable? | 15/04 14:43 |

stevan | might be a good idea to start with a simpler type system than dependently typed lambda calculus (ITT), such as typed SK calculus or simply typed lambda calculus. or a typed functional programming language such as haskell. | 15/04 14:43 |

npouillard | sah0s: yes | 15/04 14:43 |

npouillard | stevan: yes | 15/04 14:44 |

sah0s | ∀ is universal quantification | 15/04 14:44 |

fax | npouillard: I am not trying to hurt his feelings or anything, but when I say "You need not conceptualize a type as anything more than a syntactic name" and he says "yes I do! I'm going to implement it", one has to make it clear that if someone is to learn something new they have to let go of any assumptions that block that | 15/04 14:44 |

sah0s | my feelings are not hurt, i just wanna learn, i have a thick skin, it's just that i'm can't understand the wikipedia entry | 15/04 14:45 |

npouillard | sah0s: but with dependent types it is also the type of dependent functions | 15/04 14:45 |

sah0s | *I can't | 15/04 14:45 |

sah0s | ah | 15/04 14:45 |

fax | I have dabbled a bit with implementing different dependent type systems and I tell you that is it all syntax all the way down | 15/04 14:45 |

sah0s | fax: intersting | 15/04 14:45 |

sah0s | fax: I had the idea that types are nothing more than syntax sliced one way or another | 15/04 14:46 |

fax | There are also technical reasons (NbE) that you would use a language which has lambda in it, rather than one that doesn't -- but this is not incredibly important | 15/04 14:46 |

sah0s | i have a nice PEG library in C and I know C very well, as soon as I build a bootstrapping functional type system then I'll have my own lambda, that's the plan! call me crazy :) | 15/04 14:47 |

sah0s | So if I start from simply typed lambda calculus that'll give me a good idea? | 15/04 14:48 |

stevan | (the book types and programming languages by pierce is a better resource than wikipedia also) | 15/04 14:48 |

fax | The reason I wanted to get across this idea of 'it's nothing but names' is because if you are used to the ad-hoc type system people have built over the years in set theory then you will be used to thinking of as a type as made of something, like when you open up |N you see {0,1,2,3,4,...} -- but as far as the type systems are presented as judgements you needn't think of anything as 'made of' anything else | 15/04 14:49 |

fax | sah0s -- oh well if you are building up a lambda calculus to program in that is quite reasonable | 15/04 14:49 |

npouillard | fax: ok, I agree the "all about syntax" but not really the "it's nothing but names" | 15/04 14:50 |

fax | I would probably not recommend TaPL because it doesn't go into detail on dependent types | 15/04 14:50 |

npouillard | sure it makes sense to have primitve types like machine integers... | 15/04 14:50 |

fax | well it's a good book if you haven't understood way type systems are presented or haven't got induction yet | 15/04 14:51 |

sah0s | i have TaPL and I'm going through it slowly | 15/04 14:51 |

sah0s | What are the atomic or base types in Agda? | 15/04 14:52 |

fax | sah0s: You only need forall/-> (they are the same thing) and a way to declare/define new (co)data types then you can define and,or,equality,etc. | 15/04 14:53 |

stevan | i'd go thru the simply typed lambda calculus part atleast before looking into dependent types. if you'd like to implement things in C, it might be good to take a look at how these things are implemented in ML as in the book also. | 15/04 14:53 |

solidsnack | I am following the instructions on the Agda VIM page but it looks like `agda --vim' does not do anything. | 15/04 18:13 |

solidsnack | Is it no longer supported? | 15/04 18:13 |

stevan | it generates a .vim file for syntax highlightning. | 15/04 18:17 |

solidsnack | stevan: Where does it put the file? | 15/04 18:18 |

solidsnack | I can't find anything with `ls -a' and I don't get error messages, either. | 15/04 18:18 |

stevan | same dir, .filename.agda.vim | 15/04 18:18 |

solidsnack | Okay, interesting -- it won't handle files inside a directory. | 15/04 18:20 |

solidsnack | I have to CD to the directory the file is in; that's the problem I was having. | 15/04 18:20 |

stevan | i wouldn't bother with vim tho; it doesn't have support for goals (which is essential), try emacs with viper-mode instead (as described at the bottom of the page)? | 15/04 18:22 |

solidsnack | stevan: I did try that; I hate Emacs. | 15/04 18:22 |

solidsnack | stevan: I will have to use it for some things, I guess; but I'm finding that I am sufficiently motivated to get all this Vim stuff working as I use Vim for everything else. | 15/04 18:23 |

solidsnack | stevan: EMACS is a strange beast. It slows down my computer quite a bit and it takes forever to actually quit it. | 15/04 18:25 |

stevan | ok, :-/ | 15/04 18:26 |

solidsnack | stevan: Sorry :) I can be pretty grumpy about this particular issue. | 15/04 18:38 |

fax | which? | 15/04 18:39 |

glguy | can I merge the following lines into one statement somehow? | 15/04 19:25 |

glguy | import Module | 15/04 19:25 |

glguy | open Module xval yval using (this; that) | 15/04 19:25 |

dolio | open import Modulse xval yval using (this ; that) | 15/04 19:26 |

dolio | Or did that not work? | 15/04 19:26 |

dolio | I'm not sure I've ever tried an open import for a parameterized module. | 15/04 19:27 |

stevan | i don't think it does. you could use a semicolon if you want the two on the same line. | 15/04 19:27 |

glguy | that didn't seem to work | 15/04 19:27 |

glguy | It certainly isn't a big issue | 15/04 19:27 |

glguy | I just wondered | 15/04 19:27 |

glguy | import Algebra.FunctionProperties | 15/04 19:28 |

glguy | open Algebra.FunctionProperties _≡_ | 15/04 19:28 |

glguy | using (Associative; _DistributesOverˡ_; _DistributesOverʳ_) | 15/04 19:28 |

glguy | Mine already spans 3 lines | 15/04 19:28 |

glguy | no sense in using any ;'s :-D | 15/04 19:28 |

* glguy is doing some exercises for an Isabelle course in Agda http://www.galois.com/~emertens/polynomials/session2eq.html | 15/04 19:31 | |

danten | maybe using as? import Algebra.FunctionProperties as AFP; open AFP _≡_ | 15/04 19:34 |

danten | using (Associative; _DistributesOverˡ_; _DistributesOverʳ_) | 15/04 19:34 |

glguy | Yeah, that doesn't look too bad | 15/04 19:41 |

sah0s | hmm, i don't have TaPL, I have Programming in Martin-Löf’s Type Theory (1990) by NordStröm, Petersson and Smith and Type Theory & Functional Programming (1999) by Simon Thompson | 15/04 19:55 |

sah0s | my mistake | 15/04 19:55 |

--- Day changed Fri Apr 16 2010 | ||

glguy_ | Is there a better approach to the last definition in http://www.galois.com/~emertens/replace/replace.html ? | 16/04 06:44 |

glguy_ | it just feels messy... | 16/04 06:45 |

--- Day changed Sat Apr 17 2010 | ||

glguy | It seems like Data.List's definition of reverse (specifically with the where-class defined helper) makes it very difficult to use in any proofs | 17/04 01:11 |

dolio | It definitely leads to some inconvenience. | 17/04 01:15 |

dolio | Since you may want to prove lemmas about rev, but you can't actually refer to rev. | 17/04 01:15 |

glguy | I'm not sure you can prove anything about it as it stands beyond reverse [] == [] | 17/04 01:26 |

glguy | (or some other constant expression) | 17/04 01:27 |

dolio | Yeah, it may well not be possible to prove things about reverse without lemmas about rev. | 17/04 01:36 |

dolio | Since you may need to prove things by induction that you can't refer to simply by referring to reverse. | 17/04 01:37 |

dolio | I'd probably go with a foldl definition, myself. | 17/04 01:52 |

sah0s | Yo. I am reading http://en.wikipedia.org/wiki/Intuitionistic_type_theory and I have nearly got my head around it: yay! | 17/04 15:06 |

sah0s | However ... | 17/04 15:06 |

sah0s | (always a however, heh) | 17/04 15:06 |

sah0s | However, it seems to me that finite types can be built up inductively so I don't see the need for finite types. Anyone got any opinions ... | 17/04 15:07 |

sah0s | ? | 17/04 15:07 |

fax | finite types ? | 17/04 15:08 |

fax | you mean like N3 = {0,1,2} ? | 17/04 15:08 |

sah0s | I suppose all type defined inductively in one group are the same type whereas all the finite types are of a different type .... | 17/04 15:08 |

sah0s | hi fax | 17/04 15:08 |

fax | hi | 17/04 15:09 |

sah0s | Yup, finite types: empty, unit, booleans (bivalent), trivalent, ... | 17/04 15:09 |

fax | you can define each one inductively, and infact you can define the whole (infinite) family of types inductively | 17/04 15:09 |

sah0s | But you can do this inductively as well if I am reading the page correctly is all that I'm saying :) | 17/04 15:09 |

sah0s | "nfact you can define the whole (infinite) family of types inductively", huh? | 17/04 15:10 |

fax | there is not really much difference between just having these types as built in or being able to define them in the language | 17/04 15:10 |

sah0s | all the types in the system? | 17/04 15:10 |

sah0s | sure | 17/04 15:11 |

fax | this family of types: empty, unit, booleans (bivalent), trivalent, ... | 17/04 15:11 |

fax | you can define them all with a single definition | 17/04 15:11 |

sah0s | i think so too, it's nice that they have names though like you were saying | 17/04 15:11 |

sah0s | with a single definition they don't have names really, just indexed | 17/04 15:11 |

fax | yeah | 17/04 15:11 |

sah0s | i understand product, sum, inductive, finite ... having difficulty with univers and equality, especially equality | 17/04 15:12 |

sah0s | i just don't see how something that looks like an operation (equality) can be a type :( | 17/04 15:13 |

fax | you can define it like | 17/04 15:13 |

fax | data Identity (A : Set) (a : A) : A -> Set where | 17/04 15:13 |

fax | refl : Identity A a a | 17/04 15:13 |

sah0s | universe seem to me to give you a hierarchy of families so I think I understand universes as well | 17/04 15:13 |

fax | so now, refl : forall {A : Set} {a : A}, Identity A a a | 17/04 15:13 |

fax | that means e.g. this judgement holds: refl N 3 : Identity N 3 3 | 17/04 15:14 |

fax | for example | 17/04 15:14 |

fax | there is an equality check built into the type system though | 17/04 15:14 |

fax | it's syntactic congruence + beta reduction + unfolding definitions (replacing names with values that is) + eta expansions + maybe other stuff too | 17/04 15:15 |

fax | the result is that you can also have judgements like refl N 3 : Identity 3 (1 + 2) | 17/04 15:15 |

sah0s | uh... | 17/04 15:15 |

sah0s | does the equality type extend the notion of the equality of base types into the rest of the type system? | 17/04 15:16 |

sah0s | the equality of objects of the base types i mean | 17/04 15:16 |

fax | the type system has got a notion of equality in it already, the identity data types just reifies it | 17/04 15:17 |

sah0s | reify? | 17/04 15:17 |

fax | it makes it into a 'first class' citizen | 17/04 15:17 |

sah0s | wow | 17/04 15:17 |

fax | do you know prolog? | 17/04 15:17 |

sah0s | ages ago, unification, rules ... | 17/04 15:17 |

sah0s | why? | 17/04 15:17 |

fax | if you ever saw the definition of unification in prolog: | 17/04 15:17 |

fax | X = X. | 17/04 15:18 |

fax | or | 17/04 15:18 |

fax | equal(X,X). | 17/04 15:18 |

sah0s | uhuh | 17/04 15:18 |

fax | this is the same sort of thing | 17/04 15:18 |

fax | (as the identity type defined above) | 17/04 15:18 |

sah0s | can you give me a non-identity practical use of the equality connective? | 17/04 15:20 |

sah0s | i still don't get it, sorry - it is very alien to me (at least in the syntax above) | 17/04 15:20 |

fax | which syntax | 17/04 15:21 |

sah0s | data Identity (A : Set) (a : A) : A -> Set where | 17/04 15:21 |

sah0s | refl : Identity A a a | 17/04 15:21 |

sah0s | so now, refl : forall {A : Set} {a : A}, Identity A a a | 17/04 15:21 |

fax | you're not use to the ML style? of using whitespace for application | 17/04 15:21 |

sah0s | no, sorry | 17/04 15:21 |

dolio | subst : (A : Set) (P : A -> Set) (x y : A) (eq : Identity A x y) -> P x -> P y | 17/04 15:21 |

fax | you are missing out | 17/04 15:21 |

fax | this is important | 17/04 15:22 |

sah0s | ok | 17/04 15:22 |

fax | f x (y z) w | 17/04 15:22 |

fax | in scheme you would write it like | 17/04 15:22 |

fax | (((f x) (y z)) w) | 17/04 15:22 |

sah0s | whitespace for application! | 17/04 15:22 |

sah0s | wow | 17/04 15:22 |

fax | f(x,y(z),w) in algolish | 17/04 15:23 |

sah0s | breaks homoiconicity though | 17/04 15:23 |

sah0s | very neat shorthand | 17/04 15:23 |

sah0s | dolio: ? | 17/04 15:23 |

fax | I think you can recover most of the important parts of homoiconicity | 17/04 15:23 |

fax | but that is sort of an advanced topic | 17/04 15:24 |

fax | (specific to dependent types) | 17/04 15:24 |

dolio | That function is a practical use of the identity type where it isn't obvious that you have something like Identity A x x. | 17/04 15:26 |

dolio | Of course, you do have that, because that's the only thing that inhabits identity types. | 17/04 15:26 |

dolio | Which means x is actually y, or vice versa, and you use that to do the 'substitution'. | 17/04 15:26 |

fax | sah0s - write a parser for this whitespace syntax in ocaml or haskell or something :P | 17/04 15:27 |

sah0s | dolio: i can see that but the thing is all the other connectives seem to produce interesting stuff but the equality connective seems to have only a single use | 17/04 15:28 |

dolio | What other connectives produce what interesting stuff? | 17/04 15:30 |

fax | sah0s um well any time you use = sign in mathematics | 17/04 15:30 |

fax | it's not exactly rare :P | 17/04 15:30 |

sah0s | :P | 17/04 15:31 |

sah0s | sigma connective produces pairs, triplets, ... | 17/04 15:31 |

fax | it's true that ground inhabitants of Identity are boring | 17/04 15:31 |

sah0s | fax: that's my point | 17/04 15:31 |

fax | it gets interesting when you do e.g. some stuff -> Identity x y | 17/04 15:31 |

dolio | What about: comm : (m n : Nat) -> m + n = n + m | 17/04 15:31 |

fax | what it means is that it computes an identity proof from the stuff | 17/04 15:31 |

sah0s | dolio: i get it know! | 17/04 15:32 |

sah0s | dolio: oops, *now! | 17/04 15:32 |

sah0s | dolio, the + though, how is the + interpreted? | 17/04 15:33 |

sah0s | + is a function type | 17/04 15:33 |

dolio | However addition is defined for naturals. | 17/04 15:33 |

sah0s | where is the 'code' for + ? | 17/04 15:34 |

sah0s | anyway i see what you mean, you use the equality type to build up laws | 17/04 15:34 |

dolio | Assuming naturals are inductive Peano numerals, it goes 'zero + n = n ; (suc m) + n = suc (m + n)' | 17/04 15:34 |

fax | just to emphasise the syntax this is what dolios term would look like if you didn't use the infix names comm : (m n : Nat) -> Identity (plus m n) (plus n m) | 17/04 15:35 |

fax | of course + and = make it much nicer to read | 17/04 15:36 |

dolio | Anyhow, you can't just say 'refl (m + n)' or something as a definition of comm, because they don't just reduce to some common normal form. | 17/04 15:37 |

sah0s | what about inequality relations? | 17/04 15:38 |

sah0s | do they make any sense in ITT? | 17/04 15:39 |

dolio | You mean stuff like less than, or just not-equal? | 17/04 15:39 |

sah0s | < > != | 17/04 15:39 |

sah0s | or <> or however you wanna say it :) | 17/04 15:39 |

dolio | Plain 'not-equal' is usually defined as x /= y = (x = y) -> False. | 17/04 15:40 |

dolio | False being the type with no proofs. | 17/04 15:40 |

sah0s | dolio: very nice | 17/04 15:40 |

fax | not X := X -> False is a very interesting type | 17/04 15:40 |

sah0s | can I read False as Absurdity as well? | 17/04 15:41 |

dolio | < and > and such can either be defined inductively, or recursively. | 17/04 15:41 |

dolio | I guess, inductively only if you have inductive families. | 17/04 15:41 |

sah0s | i had a brainwave regarding atomic/base types | 17/04 15:42 |

sah0s | fax: you said that it was syntax all the way down | 17/04 15:42 |

sah0s | i believe that is only strictly true for atomic types | 17/04 15:43 |

fax | what's an atomic type? | 17/04 15:43 |

sah0s | base type | 17/04 15:43 |

sah0s | built-in type | 17/04 15:43 |

sah0s | an irreducible type | 17/04 15:44 |

fax | It's possible to just give a schema for allowing new inductive defintions/declarations, and not have ANY built in types | 17/04 15:44 |

fax | well . you need the lambda calculus, which means that forall and * are built in | 17/04 15:44 |

fax | but you can now define everything like =, true, false, and, or, not, N, Z, Q, R etc. | 17/04 15:45 |

fax | exists | 17/04 15:45 |

sah0s | if you have the concept of sub-typing you can make * your universal type and not have it built-in but the you need to make all your other types sub-types of * | 17/04 15:46 |

sah0s | exists? surely not ... | 17/04 15:46 |

sah0s | = is a connective, not a type | 17/04 15:47 |

sah0s | and surely the function type is built-in ??? | 17/04 15:47 |

dolio | I'm not sure you can define R, unless you don't really care about having redundant elements. | 17/04 15:48 |

sah0s | dolio: for a constructivist R is a fiction | 17/04 15:48 |

sah0s | with a strict ITT, R is impossible I'd say | 17/04 15:48 |

fax | I'm thinking of a different R than you | 17/04 15:49 |

fax | computable reals | 17/04 15:49 |

sah0s | different R, go on I'll bite :) | 17/04 15:49 |

sah0s | fax: nice | 17/04 15:49 |

dolio | You can represent constructive reals as something like Q -> Q. | 17/04 15:49 |

sah0s | fax: computable transcendentals like e and pi, sure :) | 17/04 15:50 |

sah0s | that's the only way I believe they exist | 17/04 15:50 |

sah0s | but the set R of all reals, not a chance | 17/04 15:50 |

dolio | But to get an R type, you'd need to quotient that, because you'll have different Q -> Q that represent the same real number. | 17/04 15:50 |

fax | yeah quotient is something you cannot define interally | 17/04 15:51 |

sah0s | i think of transcendentals as machine that are unbounded in time and generate sequences of quotients, that's it | 17/04 15:51 |

fax | internally* | 17/04 15:51 |

fax | I think you can do a whole-program style transformation into the setoid stuff | 17/04 15:51 |

fax | but that is kind of hard .. | 17/04 15:52 |

sah0s | there is no Set of all of these machines, a least nothing meaningful imnsho :) | 17/04 15:52 |

sah0s | I'm going to a conference in may that is exploring this stuff :) want the link? | 17/04 15:52 |

dolio | roconnor actually pointed out somewhere that the quotient R can be kind of useless. | 17/04 15:52 |

sah0s | i would believe that | 17/04 15:53 |

dolio | For instance, any function from R to a discrete set that respects the equivalent relation is constant. | 17/04 15:53 |

* fax confused | 17/04 15:53 | |

sah0s | http://www.theinfinitycomputer.com/Infinity2010/index.php | 17/04 15:54 |

sah0s | dolio: but we don't have R | 17/04 15:55 |

fax | hypercomputation ? | 17/04 15:55 |

dolio | sah0s: I mean the constructive R, as specified above. | 17/04 15:55 |

sah0s | hmm, i think the individuals are compute-able but that there is no abstract set that enumerates them all meaningfully - if there is it would be a huge mathematical result | 17/04 15:57 |

sah0s | "Turing's writing made it clear that oracle machines were only mathematical abstractions, and were not thought of as physically realisable." | 17/04 15:58 |

sah0s | anyway, ye've been really helpful and thought-provoking | 17/04 15:59 |

sah0s | i think it'll be years before this stuff goes mainstream though unfortunately, until then we have VB.net, ugh | 17/04 16:00 |

fax | that church-turing thesis is really frustrating, because there doesn't seem to be any way to prove it | 17/04 16:00 |

fax | there's all this... evidence though... | 17/04 16:00 |

fax | I guess that it is one problem which is right in both computing and physics | 17/04 16:01 |

fax | I find it amazing that quantum computation fits the same model.. but can do some things faster -- rather than being able to compute new things | 17/04 16:02 |

fax | (but that's probably a summary of everything I know about quantum theory so I wouldn't even be sure it's true) | 17/04 16:02 |

sah0s | if it looks like a duck and quacks like a duck then it's probably a duck. that's my proof to myself. | 17/04 16:02 |

fax | I enjoy e non-rigorous proof but | 17/04 16:03 |

fax | ... that is pushing it ;D | 17/04 16:03 |

sah0s | oops, even quantum apple laptops will need batteries | 17/04 16:05 |

fax | haha | 17/04 16:05 |

sah0s | fax: it is amazing that it's the same model | 17/04 16:09 |

sah0s | i like the way that it breaks classical encryption but provides a QC solution as well | 17/04 16:09 |

sah0s | so it seems we don't have to change our notion of privacy and encryption | 17/04 16:10 |

sah0s | though i was reading about an idea for provably tamper-free connections which would be stronger than what we have now | 17/04 16:11 |

fax | it's wild stuff I still haven't got my head about the basics like the deutch black box thingy | 17/04 16:13 |

sah0s | anyway, what do you people work at? i have a degree in philosophy but i'm not 'working' at the moment, i'm researching the state of the art in programming languages ... | 17/04 16:13 |

sah0s | david deutsch is the man, the fabric of reality is an awesome book | 17/04 16:14 |

fax | cool I hadn't heard of it | 17/04 16:14 |

fax | you should check out peter morris' PhD once you have got your legs | 17/04 16:15 |

sah0s | it says that there are only 4 fundamental theories: the theory of computation, virtual reality, quantum theory and the theory of evolution | 17/04 16:15 |

sah0s | fax: will do, in fact I'll have a quick look right now | 17/04 16:16 |

sah0s | nottingham again, what's in the water in nottingham? | 17/04 16:17 |

fax | lol | 17/04 16:17 |

sah0s | Epigram looks wild | 17/04 16:17 |

sah0s | 2 dimensional syntax, bizarre | 17/04 16:17 |

fax | yeah Epigram is really exciting - I am still struggling to understand the theory of it a bit | 17/04 16:17 |

sah0s | conor mcbride's writing is hilarious | 17/04 16:17 |

sah0s | doesn't seem too different from agda | 17/04 16:18 |

sah0s | i don't use emacs though so ... | 17/04 16:18 |

sah0s | thanks again for all your help, see you | 17/04 16:24 |

Mathnerd314 | is there a statically-typed language where I can play with capability types? | 17/04 16:39 |

fax | Mathnerd314 - what are they? | 17/04 17:52 |

Mathnerd314 | capabilities - stuff where I can say that "you can do this" or "you cannot do this", reified into types | 17/04 17:53 |

fax | do you know any intro paper on it? | 17/04 17:57 |

fax | something that describes important bits of it in a simple way | 17/04 17:57 |

Mathnerd314 | hmm... wait a bit | 17/04 17:59 |

fax | http://www.cs.st-andrews.ac.uk/~eb/drafts/icfp09.pdf | 17/04 18:06 |

Mathnerd314 | ok; thought something like that could happen | 17/04 18:14 |

--- Day changed Sun Apr 18 2010 | ||

* glguy shares some code using EqReasoning on an arbitrary Semiring... http://www.galois.com/~emertens/polynomial-eqreasoning/session2.html | 18/04 06:21 | |

fax | "but you can add others (parametricity?) without spannering up the engines" | 18/04 21:06 |

fax | so you can't derive parametricity internally? | 18/04 21:06 |

fax | (I think it should be provable for a universe but was not sure about the general case) | 18/04 21:07 |

dolio | I don't know of any type theory that can derive parametricity internally. | 18/04 21:07 |

dolio | In fact, I believe I recall Neel Krishnaswami referring to that as a sort of holy grail for impredicative type theories. | 18/04 21:09 |

fax | it's just this desc throws me off a bit | 18/04 21:09 |

fax | oh yes? :) | 18/04 21:09 |

dolio | Since I think it lets you use impredicative codings of inductive types while also getting back some of the stronger induction principles. | 18/04 21:10 |

dolio | Which you normally lose. | 18/04 21:10 |

fax | ah | 18/04 21:10 |

dolio | Then again, one might wonder if that doesn't doom it to failure immediately. | 18/04 21:13 |

fax | well having a data type of all the syntax of the language (with an interpretation) would certainly prove false | 18/04 21:13 |

dolio | Because inductive types include strong sums, and strong sums in an impredicative universe yield inconsistency (as I recall from Luo). | 18/04 21:14 |

fax | (which is why being able to make a data type of all data types was such a surprise to me) | 18/04 21:14 |

fax | I'm not sure I understand that about the strong sums | 18/04 21:15 |

fax | what about exists in coq? which is in prop | 18/04 21:16 |

dolio | Yes. They avoid the problem by not allowing strong elimination into Type or something. | 18/04 21:16 |

fax | oh I see | 18/04 21:16 |

fax | hm | 18/04 21:17 |

dolio | The idea is that if you have strong impredicative sums, then (exists p : Type. True) : Prop lets you have [Prop, _] : Prop. | 18/04 21:17 |

fax | what about this http://coq.inria.fr/stdlib/Coq.Logic.Description.html ? | 18/04 21:18 |

dolio | But making use of that requires strong elimination fst [Prop, _] = Prop : Type. | 18/04 21:18 |

dolio | Check the elimination principles for it. | 18/04 21:19 |

dolio | The one that eliminates into Type is weak, I think. | 18/04 21:19 |

dolio | Anyhow, I'm kind of taking Luo's word for this. | 18/04 21:20 |

dolio | I tried modifying Hurkens' paradox for this, but got lost, since I don't really understand the paradox in the first place. | 18/04 21:20 |

fax | I'm sure it's true I just don't understand it | 18/04 21:20 |

pigworker | What I meant by "(parametricity?)" was that you might implement a "free theorem calculator", then just postulate that all the calculated propositions hold. You don't lose canonicity by doing that (unless one of your free "theorems" is false). | 18/04 21:38 |

fax | oh I see | 18/04 21:40 |

fax | It's just that I have been wanting to implement parametricity as a reflective thing for a while (but I got theory problems when I tried in coq) | 18/04 21:41 |

fax | pigworker - you write so well! I wish I could | 18/04 21:47 |

pigworker | fax: thanks, it's years of practice; I write to perform | 18/04 21:49 |

fax | 21:00 < hpaste> parametricity -> induction (dolio) http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24938 | 18/04 22:01 |

fax | if the bot could tell the difference between haskell and agda we could get that in here | 18/04 22:01 |

fax | dolio - I don't understand this P : ⊤ → Set | 18/04 22:03 |

fax | why T rather than just P : Set? | 18/04 22:04 |

fax | oh wait T means it's a functor | 18/04 22:04 |

dolio | Why P : Nat -> Set instead of P : Set? | 18/04 22:06 |

fax | but Nat is not initial and I think T is? | 18/04 22:06 |

fax | i.e. T -> Set ~ Set | 18/04 22:07 |

dolio | The induction principle essentially expresses that if t : T, then t = id. | 18/04 22:07 |

dolio | You can derive that with P t := t = id, even. | 18/04 22:09 |

dolio | induction (\t -> t = id) refl : (t : T) -> t = id | 18/04 22:10 |

dolio | Huh, EPTS with the 'proof irrelevant' rule lets you prove K. | 18/04 22:30 |

fax | EPTS ? | 18/04 22:31 |

dolio | Erasure pure type system. | 18/04 22:31 |

fax | oh | 18/04 22:32 |

dolio | "The technical means by which realizability is internalized is called ultra Σ-types." | 18/04 23:29 |

fax | what's that from? | 18/04 23:31 |

dolio | Nathan Mishra-Linger's thesis. | 18/04 23:31 |

dolio | Irrelevance, Polymorphism and Erasure in Type Theory | 18/04 23:31 |

fax | cool | 18/04 23:31 |

dolio | Ultra Σ-types are someone else, though. He's just describing them. | 18/04 23:32 |

Saizan | they sound scary | 18/04 23:32 |

dolio | You mean awesome? | 18/04 23:33 |

dolio | There are things out there called "very dependent types". They should have chozen a zazzier name. | 18/04 23:33 |

dolio | Like mega dependent types. | 18/04 23:33 |

fax | lol | 18/04 23:34 |

dolio | Or quantum dependent types. Quantum is always good. | 18/04 23:35 |

dolio | Take it before someone else does. | 18/04 23:35 |

--- Day changed Mon Apr 19 2010 | ||

Mathnerd314 | so what's the most powerful type system ever invented? | 19/04 01:04 |

ohnobinki | food! | 19/04 01:06 |

TheOnionKnight | I'd pick an inconsistent one, after all you can prove any true proposition. (along with any false one but hey ...) | 19/04 01:06 |

Mathnerd314 | I'm thinking inconsistent type systems are weak, because they're equivalent to untyped systems | 19/04 01:07 |

Adamant | you probably need to define 'powerful' | 19/04 01:38 |

dolio | What do you mean equivalent to untyped systems? | 19/04 01:52 |

fax | I don't think it's an interesting question | 19/04 02:00 |

fax | there's always a more powerful system | 19/04 02:01 |

fax | To get insight about the strength of things I think you have to turn the question around and ask what is the weakest theory which can e.g. do analysis | 19/04 02:02 |

dolio | So, apparently, in the irrelevant EPTS, you can add axioms to the 'propositional' fragment of the language. | 19/04 02:15 |

dolio | Via something like: axiom : Squash P ; axiom = poof. | 19/04 02:16 |

dolio | P being the proposition you want to add. | 19/04 02:16 |

dolio | So, say, ext : Squash ((forall x. f x = g x) -> f = g). | 19/04 02:17 |

dolio | Which seems somewhat similar to OTT. | 19/04 02:17 |

dolio | Huh, you can interpret computationally-irelevant pi as an intersection. | 19/04 03:45 |

fax | yeah that's Coq* innit | 19/04 03:47 |

dolio | Coq*? | 19/04 03:47 |

dolio | I'm still looking at the thesis I was reading earlier. | 19/04 03:47 |

fax | The Implicit Calculus of Constructions | 19/04 03:48 |

dolio | Oh, yes. | 19/04 03:48 |

dolio | It makes sense, but I hadn't thought of it. | 19/04 03:49 |

dolio | Since any term with type (x : A) => B[x] gets extracted from /\x. M to just a suitably erased M'. | 19/04 03:50 |

dolio | So M' must be a single term that inhabits all B[x], so to speak. | 19/04 03:51 |

dolio | I need to figure out how to implement inductive types (families). | 19/04 03:53 |

glguy | so... how much of the conversation between fax, dolio, pigworker, et al do I need to have understood to have a chance at getting any further with Agda... | 19/04 05:54 |

glguy | in the last 6 hrs or so | 19/04 05:54 |

dolio | None. | 19/04 05:54 |

glguy | phew | 19/04 05:54 |

glguy | I just had a sense of "oh shit, I'm so far behind... what am I /doing/ here??" | 19/04 05:54 |

glguy | OK, what should I be reading if I do want to understand more of it? | 19/04 05:56 |

dolio | The stuff I was talking about was mostly a thesis that I mentioned at some point. | 19/04 05:59 |

dolio | Where'd I leave off? "None."? | 19/04 06:03 |

glguy | at some pount. | 19/04 06:03 |

dolio | Okay. | 19/04 06:03 |

dolio | Parametricity you can read about in the Wadler paper, Theorems for Free! | 19/04 06:04 |

dolio | There are also others. It goes back to Reynolds, but his papers might be harder. | 19/04 06:04 |

dolio | Oh, there are shorter papers than the thesis if you want something short to chew on. Erasure and Polymorphism in Pure Type Systems, I think, by Sheard and Mishra-Linger. | 19/04 06:05 |

dolio | And if you don't know about pure type systems, you should read about those first. | 19/04 06:05 |

dolio | The thesis has a lot more stuff, though. Like, it considers languages with Agda-like inductive types. | 19/04 06:06 |

glguy | cool, thanks for that | 19/04 06:06 |

dolio | And OTT and the stuff pigworker was talking about are related to the theoretical foundation for Epigram 2. So you can find stuff about all that at e-pig.org, or on Conor McBride's (pigworker's, I believe) website. | 19/04 06:08 |

dolio | Oh, and the epigram blog. | 19/04 06:08 |

dolio | And the thing I mentioned about parametricity and inductive types was a random comment neelk made at the n-category cafe. I could probably find it if I really had to, but I don't have it handy. | 19/04 06:09 |

glguy | no need, i have enough to keep me busy | 19/04 06:10 |

glguy | most of what I know about Agda is from experimenting with things and seeing the results. reading more about the theory behind it will be good | 19/04 06:11 |

glguy | one of the requirements for formal methods to become useful is for people that don't understand them to be able to use them... I think that Agda helps a lot in that regard | 19/04 06:12 |

dolio | Oh, there was also some stuff about Luo. He's wrote a thesis and a book (and probably other stuff) on a couple type systems that are commonly referenced. ECC (extended calculus of constructions) and UTT (universal (?) type theory). | 19/04 06:13 |

dolio | The thesis only covers ECC, I think, and the book is hard to find. | 19/04 06:13 |

* glguy isn't responding much because he is trying to get his son to drink his bottle | 19/04 06:14 | |

dolio | Yeah, at least if you know something like Haskell, Agda is pretty easy to edge your way into. | 19/04 06:16 |

roconnor | edwinb: is Idris a sound logical system? | 19/04 14:38 |

edwinb | roconnor: No. At least not at the moment. It has Set:Set... | 19/04 14:43 |

edwinb | So I wouldn't recommend going and proving anything in it... | 19/04 14:44 |

roconnor | I wonder how practical it would be for Idris and/or Epigram 2 to have a flag to disallow quantification over Set (and hence remove Set:Set) to make a small but sound system. | 19/04 14:44 |

roconnor | or if Set:Set is really used in a mathematical Prelude (maybe it is used for generic programming or something). | 19/04 14:45 |

edwinb | For Idris it's really just me wanting to focus on other aspets of programming with dependent types and taking the easy way out | 19/04 14:46 |

edwinb | aspects, rather | 19/04 14:46 |

edwinb | it probably wouldn't be so hard to add a flag that did that | 19/04 14:47 |

roconnor | well, that's also the excuse that Epigram has as well | 19/04 14:47 |

roconnor | and it is totally reasonable | 19/04 14:47 |

edwinb | Epigram 2 will do it right in the end | 19/04 14:47 |

roconnor | except that it kinda limits research in the language for proof. For example proofs developed in the languages would sort of be unacceptable in the journal of formalized reasoning I'd expect. | 19/04 14:49 |

edwinb | Indeed. I wouldn't recommend trying that... | 19/04 14:49 |

roconnor | But if there was a flag that made these safe, even without universe there is probably still quite a bit of room to explore ideas on using the systems as theorem provers. | 19/04 14:49 |

roconnor | Fermat's Last Theorem probably doesn't need that many universes to prove it. ;) | 19/04 14:50 |

edwinb | I would think of that flag as meaning, "Right, I've finished this program now." | 19/04 14:50 |

edwinb | During development, it's useful to cheat! | 19/04 14:50 |

roconnor | edwinb: do you use Set:Set for your generative programming | 19/04 14:52 |

edwinb | I don't think I've ever used anything more than Set1 | 19/04 14:52 |

roconnor | that's what I figured | 19/04 14:52 |

roconnor | er | 19/04 14:52 |

roconnor | is Set1 the smalles set, or is there a Set0? | 19/04 14:52 |

edwinb | that would be assuming Set : Set1 | 19/04 14:53 |

roconnor | ah | 19/04 14:53 |

roconnor | ok | 19/04 14:53 |

roconnor | anyhow | 19/04 14:53 |

roconnor | thanks for the info | 19/04 14:54 |

pigworker | just read logs... | 19/04 16:13 |

pigworker | universe polymorphism is currently in the spotlight for us | 19/04 16:15 |

edwinb | I'm glad you're doing it so I don't have to... | 19/04 16:20 |

edwinb | although I've been writing C most of today, so maybe you'd say the same thing | 19/04 16:21 |

pigworker | very probably | 19/04 16:27 |

pigworker | I wish I knew what Agda's actual universe rules were. | 19/04 16:30 |

glguy | Where can I go to see all of the {-# BUILTIN _ _ #-} things? | 19/04 18:17 |

* glguy dives into ./src/full/Agda/TypeChecking/Monad/Builtin.hs | 19/04 18:19 | |

glguy | The BUILTINs for Cons and Nil make me think that there is some syntax for list literals | 19/04 18:21 |

glguy | but I'm having trouble tracking it dow | 19/04 18:21 |

glguy | n | 19/04 18:21 |

codolio | I don't recall there being list literals, but I think in that case what you're using are actually Haskell lists, rather than your Agda definition. | 19/04 18:24 |

codolio | Which is likely more efficient. | 19/04 18:24 |

glguy | Isn't that where the COMPILED_DATA pragmas come in? | 19/04 18:25 |

codolio | That allows you to hack it in yourself if it doesn't have specific support. | 19/04 18:25 |

glguy | So far I've traced the BUILTIN CONS and NIL to ./src/full/Agda/TypeChecking/Primitive.hs in the "toTerm" typeclass | 19/04 18:26 |

codolio | But, for instance, using the BUILTIN pragmas for naturals means that Haskell's Integer is actually used. | 19/04 18:26 |

glguy | I don't see them going any further | 19/04 18:26 |

glguy | I thought that the BUILTIN was how you got integer literals int he syntax | 19/04 18:26 |

glguy | like how the buILTIN refl and eq where how you bound the rewrite syntax | 19/04 18:26 |

codolio | It does that, too.l | 19/04 18:26 |

codolio | Builtin stuff for equality is important for the trustMe thing, too, I think. | 19/04 18:27 |

glguy | OK, I see that "ToTerm" is the typeclass "From Agda term to Haskell value" | 19/04 18:27 |

glguy | OK, so list literals are (a :: b :: c :: []) | 19/04 18:29 |

glguy | just making sure :) | 19/04 18:29 |

glguy | Is the source code currently the best place to find out about those things? | 19/04 18:30 |

codolio | Well, it's possible it's on the wiki somewhere, but I didn't know where to point you. | 19/04 18:33 |

glguy | Sometimes it seems unfortunate that Agda 2 shares its name with Agda | 19/04 18:36 |

glguy | It is easy to find irrelevant, but promising hits on google | 19/04 18:36 |

fax | I don't really know what's going on with agda | 19/04 18:37 |

fax | I thought it was a research/exploration language | 19/04 18:37 |

fax | but everyone is treating it like it's not | 19/04 18:37 |

glguy | independent of its intended purpose, it is still an interesting language for those simply interested in learning more about dependent types | 19/04 18:40 |

ccasin | Ulf's thesis being titled "towards a practical programming language..." | 19/04 19:00 |

ccasin | I tend to think of it is just that - a step on the way | 19/04 19:00 |

ccasin | and pretty much the best one out there so far for doing experiments in | 19/04 19:01 |

ccasin | so lots of academics do lots of cool things in it | 19/04 19:01 |

--- Day changed Tue Apr 20 2010 | ||

Saizan | it seems like it'd be easier to work with PHOAS if you can use parametricity in your proofs | 20/04 05:45 |

gio123 | does somebody knows proof irrelevance? | 20/04 16:07 |

dolio | pigworker: I have a pretty simple type theory implementation that has what I understand to be (approximately) Agda's universe polymorphism. | 20/04 16:18 |

dolio | http://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs | 20/04 16:20 |

dolio | The type checker is there. | 20/04 16:20 |

pigworker | dolio: I'll have a look, thanks. | 20/04 16:20 |

dolio | The main difference (that I know of) is that it allows quantification over levels in sigma types, which there's no way to do in Agda (unless it's changed recently). | 20/04 16:21 |

pigworker | I've seen quite a few types with multiple level vars (and max) in them. Are they needed because it's hard to shift stuff between layers? | 20/04 16:22 |

dolio | Yeah. There's currently no way to get from A : Set i to (say) ^A : Set (suc i). That's been on their to-do list for a while. | 20/04 16:23 |

pigworker | My suspicion is that nailing that could make things easier. We're having a crack at it. | 20/04 16:28 |

dolio | Last I checked, something like that was the actual plan. Various lifting operators, plus inference of how much lifting you need. | 20/04 16:28 |

dolio | Rather than actual cumulativity rules in the type system like, say, Coq. | 20/04 16:29 |

pigworker | gio123: I've been experimenting with proof irrelevance | 20/04 16:29 |

pigworker | I've always valued universe polymorphism more than cumulativity, which is why I held off implementing a stratified system. Set:Set gives polymorphism by collapse! | 20/04 16:31 |

npouillard | list | 20/04 16:33 |

npouillard | oops | 20/04 16:33 |

dolio | Anyhow, I thought the universe rules were weird (and interesting) enough to play around with by themselves. It's not obvious that having universes indexed by a universe-0 type isn't inconsistent somehow. Then again, you guys are working on having all datatypes being generated by (essentially) a universe datatype, so maybe it's not that wacky. | 20/04 16:34 |

fax | that desc thing is polymorphic though | 20/04 16:35 |

fax | I mean | 20/04 16:35 |

fax | it's of sort Set[i+1] with Set[i] in it? or maybe I am thinking too much about how coq does universese | 20/04 16:36 |

dolio | Well, if I understand the situation, you have Desc : Set, and forall T : Set. exists d : Desc. Mu d = T. | 20/04 16:41 |

dolio | Except, perhaps, T = Desc. | 20/04 16:41 |

dolio | Of course, there's probably no proof of that statement in the language, since that'd be type-case. | 20/04 16:42 |

dolio | Actually, that may still be too strong. Desc only describes inductive types (and IDesc inductive families). | 20/04 16:43 |

pigworker | At the moment, the actual Epigram 2 implementation exploits the collapse, but we also have a stratified Agda model. | 20/04 16:46 |

pigworker | The descriptions of level n inductive families are a level n+1 inductive family. | 20/04 16:47 |

dolio | Ah. | 20/04 16:47 |

pigworker | When we eventually close IDesc under internal fixpoints, then IDesc Zero at level n will be remarkably like Set[n]. The resemblance may be too strong to resist. | 20/04 16:49 |

fax | but what about -> and forall? | 20/04 16:50 |

pigworker | fax: IDesc is closed under Pi | 20/04 16:50 |

dolio | Is that new? | 20/04 16:51 |

pigworker | I mean, it's closed under (x : S) -> for S in Set, so you don't have negative occurrences of the variable. It gives you functional recursive arguments, as in W-types. | 20/04 16:52 |

fax | im confused :) | 20/04 16:53 |

fax | would you have say, forall (A : *), A -> A : IDesc Zero ? | 20/04 16:53 |

fax | oh I guess it's just something along the lines of pi \A -> pi \a -> var (fs fz) | 20/04 16:54 |

fax | should have written forall (A : IDesc Zero), A -> A : IDesc Zero perhaps | 20/04 16:55 |

fax | no I am definitely confused | 20/04 16:55 |

pigworker | Currently, 'Pi : (S : Set) -> (S -> IDesc I) -> IDesc I and 'Const : Set -> IDesc I, so you can build that type a bit at a time. | 20/04 16:59 |

pigworker | 'Pi Set \ A -> 'Pi A \ a -> 'Const A | 20/04 16:59 |

pigworker | but it's not really satisfying | 20/04 17:00 |

fax | does this mean you can quote anything? | 20/04 17:01 |

pigworker | IDesc needs quite a lot of extra thought if it's going to grow up to be the main universe, rather than just *a* universe. | 20/04 17:01 |

fax | everything* | 20/04 17:01 |

pigworker | fax: you can't currently quote Mu (no internal fixpoint), nor can you inspect the domain of a 'Pi (because it's a Set, not a description) | 20/04 17:02 |

fax | oh okay | 20/04 17:02 |

pigworker | the former needs some sort of syntax with binding; the latter needs induction-recursion | 20/04 17:03 |

dolio | Ah! So that's how you do induction recursion. | 20/04 18:55 |

fax | hm? | 20/04 19:02 |

dolio | pigworker said that inspecting the domain of a Pi requires induction recursion. | 20/04 19:03 |

dolio | So presumably that's at least part of how you do induction-recursion with something like Desc. | 20/04 19:03 |

fax | there's some noteson http://www.cs.chalmers.se/~peterd/papers/inductive.html | 20/04 19:05 |

fax | I think this will be the same kind of thing | 20/04 19:05 |

dolio | I guess it'd make sense that he'd be working on it. | 20/04 19:06 |

dolio | So many people's publications to read. | 20/04 19:06 |

stevan | i have a question regarding the dependency thing on the mailing list; it seems to me that the only thing that needs cabal 1.8.x is the agda-cabal stuff (which doesn't work yet anyways) so why not have a flag in the .cabal file to enable agda-cabal support and leave that flag off by default? | 20/04 19:15 |

--- Day changed Wed Apr 21 2010 | ||

dolio | dolio is often amused when authors refer to themselves by name in academic papers. | 21/04 01:46 |

fax | :) | 21/04 01:47 |

* binki wishes people used /me properly :-p | 21/04 01:47 | |

dolio | dolio wasn't broadcasting an action. He was speaking a sentence. | 21/04 01:47 |

binki | I forgot that /me doesn't work well with passive sentences | 21/04 01:48 |

dolio | My point was that it's weird to refer to yourself by name, but people do it when citing their own papers. | 21/04 01:49 |

dolio | Which I suppose is hard to avoid. | 21/04 01:49 |

fax | in "Category Theory Applied to Neural Modeling and Graphical Representations" [Healy 2000], Michael Healy shows how to build compound neural nets from simpler components using colimits. (He also shows how to combine several neural representations of the same concept into one by using "natural transformations".) | 21/04 01:50 |

fax | this is cool ^ | 21/04 01:50 |

dolio | And Peter Dybjer cites a lot of his own papers, because he's apparently done most of the significant work on induction-related stuff in type theory. :) | 21/04 01:50 |

fax | I could find very little about induction-recursion | 21/04 01:51 |

fax | there's a nice bit by Caterina Coquand, and Martin Lof (apperently) wrote about it.. but I can't get that because I'm not a university or something | 21/04 01:51 |

dolio | From what I can gather, Martin-Loef didn't really write about it. But he wrote about defining Tarski-style universes, of which induction-recursion is a generalization. | 21/04 01:53 |

fax | I think he used it to give a normalization proof of one of the type theories, and the article I'm failing to find also does this | 21/04 01:54 |

fax | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.6695 | 21/04 01:58 |

fax | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.6101 | 21/04 02:00 |

fax | second one is the one I really meant | 21/04 02:00 |

Adamant | dolio: Bob Dole does not agree, Bob Dole | 21/04 03:42 |

lpjhjdh | should Data.Rational take a really long time at 100% cpu to load? | 21/04 19:38 |

dolio | Have you loaded it before? | 21/04 19:40 |

dolio | The first time you load it, it compiles lots of other module with lots of proofs. | 21/04 19:40 |

lpjhjdh | I haven't | 21/04 19:40 |

lpjhjdh | ah, thanks, many things it did compile :) | 21/04 19:45 |

dolio | Yeah, it has to check all the stuff for coprimality. | 21/04 19:49 |

dolio | And the Euclidean algorithm. | 21/04 19:49 |

copumpkin | it's really slow to use, too | 21/04 19:49 |

dolio | So, rewrite is really handy. | 21/04 19:49 |

copumpkin | I remember I was testing basic arithmetic on rationals and it took tens of seconds to normalize simple expressions | 21/04 19:49 |

copumpkin | I wonder what happened to the Rational improvements NAD mentioned | 21/04 19:49 |

fax | it's frustrating | 21/04 19:50 |

fax | ...waiting for quotients | 21/04 19:50 |

* Saizan wonders if they work fine in Epigram 2 | 21/04 19:52 | |

fax | I think they do | 21/04 19:53 |

lpjhjdh | how do you get ÷? | 21/04 19:56 |

lpjhjdh | I looked through the input.el but couldn't find it | 21/04 19:56 |

dolio | Put that in the buffer, move the cursor over it, and type C-u C-x = | 21/04 19:57 |

lpjhjdh | ah, thanks | 21/04 19:57 |

glguy | Is "abstract" as it pertains to modules documented somewhere? somewhere on the wiki or a paper, perhaps? | 21/04 22:58 |

dolio | Induction-recursion is pretty wild. | 21/04 23:46 |

fax | oh yeah ? | 21/04 23:48 |

dolio | Yes. | 21/04 23:49 |

fax | I only really know what it is and some basic examples.. | 21/04 23:49 |

dolio | I think I have what is essentially an embedding of my little type theory with (agda-style) universe polymorphism. | 21/04 23:49 |

dolio | And it fits entirely in Set. | 21/04 23:50 |

fax | :o | 21/04 23:50 |

fax | I don't get it :) | 21/04 23:50 |

fax | how is that possible | 21/04 23:50 |

dolio | What you do, is have couple of universe formers. | 21/04 23:51 |

dolio | FormU : (U : Set) (T : U -> Set) -> Set ; FormT : (U : Set) (T : U -> Set) -> FormU U T -> Set | 21/04 23:51 |

dolio | Which are defined via induction recursion. | 21/04 23:51 |

dolio | So, that lets you iterate the formation of universes. | 21/04 23:52 |

dolio | You can then have U : Nat -> Set and T : (n : Nat) -> U n -> Set. | 21/04 23:52 |

fax | those two are functions? | 21/04 23:52 |

dolio | U and T are. | 21/04 23:53 |

dolio | Mutually defined. | 21/04 23:53 |

fax | okay | 21/04 23:53 |

fax | thye needn't be mutually defined though? | 21/04 23:53 |

fax | or is it essential that they are | 21/04 23:53 |

dolio | I think it is essential. | 21/04 23:53 |

fax | then I am not sure what is going on | 21/04 23:53 |

fax | FormU is both a value and a type? | 21/04 23:54 |

dolio | FormU is a datatype. | 21/04 23:54 |

fax | oh is FormT a type as well? | 21/04 23:54 |

fax | I was reading these as constructors | 21/04 23:54 |

dolio | Yes. FormU and FormT are types, defined via induction-recursion. | 21/04 23:55 |

fax | ok | 21/04 23:55 |

dolio | Then U and T are defined via mutual recursion afterward. | 21/04 23:55 |

fax | wow this is confusing :))) | 21/04 23:55 |

fax | how did you come up with this? | 21/04 23:55 |

dolio | Then you define an inductive-recursive universe that internalizes the entire hierarchy. | 21/04 23:55 |

fax | can you interpret it? or is that not even needed | 21/04 23:56 |

dolio | It's just me fiddling with stuff I read in one of the Dybjer papers. | 21/04 23:56 |

fax | I think I get it but that is pretty wild I agree | 21/04 23:57 |

dolio | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24994#a24994 | 21/04 23:58 |

dolio | There's a snapshot. | 21/04 23:58 |

--- Day changed Thu Apr 22 2010 | ||

fax | but how is that in Set?? | 22/04 00:02 |

dolio | I'm having trouble defining Pi : (m n : Nat) (s : U m) (t : T n s -> U n) -> U (max m n), though. | 22/04 00:03 |

fax | how do I do something like forall T : *, T -> T ? | 22/04 00:07 |

fax | I tried T (π υ \ u -> π (τ u) \ x -> τ x) but that doesn't work | 22/04 00:08 |

dolio | Your type is forall T : *, forall X : T, X | 22/04 00:11 |

dolio | The last bit should be \tau u. | 22/04 00:11 |

fax | FF : T 1 (Π 1 υ \T -> Π 1 (τ T) \T -> τ T) | 22/04 00:11 |

fax | this seems closer but not it | 22/04 00:11 |

dolio | That's the same type. You're capturing the T. | 22/04 00:12 |

fax | doh | 22/04 00:13 |

fax | okay yeah that works now thanks | 22/04 00:13 |

dolio | As for how this fits in Set, it's because induction-recursion is crazy. | 22/04 00:16 |

fax | im really confused by this :p | 22/04 00:17 |

dolio | Essentially, Luo defines all his universes in UTT via induction recursion. | 22/04 00:17 |

dolio | And it's equivalent to ECC + inductive types. | 22/04 00:17 |

dolio | And LF, the meta-theory, essentially only has Set. | 22/04 00:18 |

dolio | So, by accepting inductive-recursive definitions, Agda's Set is just as powerful (minus the impredicativity). | 22/04 00:18 |

fax | e : Set | 22/04 00:19 |

fax | e = T 1 (Π 1 υ \T -> Π 1 (τ T) \_ -> τ T) | 22/04 00:19 |

fax | FF : e | 22/04 00:19 |

fax | FF = \T t -> t | 22/04 00:19 |

fax | that works | 22/04 00:20 |

fax | e : Set | 22/04 00:20 |

fax | e = forall (T : Set) -> T -> T | 22/04 00:20 |

fax | FF : e | 22/04 00:20 |

fax | FF = \T t -> t | 22/04 00:20 |

fax | that breaks | 22/04 00:20 |

fax | of course T in the first FF can't be anythingin Set, it can only be ℕ, ⊥ or ⊤ | 22/04 00:21 |

fax | but those are still sets | 22/04 00:21 |

fax | (oh maybe it can even be some pi, sigma, w, + thing if it wants) | 22/04 00:21 |

dolio | The second one breaks because e : Set1. | 22/04 00:22 |

fax | the first one should break too :S | 22/04 00:22 |

fax | for the same reason | 22/04 00:23 |

fax | how come this doesn't introduce inconsistencies? | 22/04 00:23 |

dolio | The first type is in the inductive-recursive universe analogous to Set1. | 22/04 00:23 |

dolio | U 1 | 22/04 00:23 |

fax | but U 1 : Set! | 22/04 00:23 |

dolio | Yes. | 22/04 00:24 |

dolio | Set contains an infinite hierarchy (and beyond) of nested universes within itself. | 22/04 00:24 |

dolio | But all of those universes are in Set. Set1 is not such a universe. | 22/04 00:24 |

fax | I can't see why this works | 22/04 00:25 |

fax | you can have a code for any Set in there, so..... oh! | 22/04 00:25 |

fax | you can have a code for any set in there _except_ the one you are defining | 22/04 00:25 |

fax | (U) | 22/04 00:26 |

fax | er | 22/04 00:26 |

fax | Ξ U T | 22/04 00:26 |

fax | not U | 22/04 00:26 |

fax | you can only put a different Ξ inside it, I think I understand why this works now | 22/04 00:26 |

dolio | U 0 : U 1 : U 2 : U 3 : U 4 : ... : Uinf : Set : Set 1 : Set 2 : ... | 22/04 00:26 |

dolio | Something like that. | 22/04 00:27 |

fax | that is so cool | 22/04 00:27 |

fax | I wonder how this is proved to be acceptable | 22/04 00:27 |

fax | then again I can't even understand how basic dependent types normalization works | 22/04 00:28 |

fax | so I don't think I have much hope of this | 22/04 00:28 |

dolio | Dybjer gives a pretty intuitive argument. | 22/04 00:29 |

dolio | Along the lines of, if you've successfully constructed u : U, you should be able to recurse over u, so T u is admissable, and you can use u and T u to build up additional elements of U. | 22/04 00:30 |

dolio | So it's still predicative. | 22/04 00:31 |

fax | oh I meant induction recursion in general | 22/04 00:31 |

dolio | Right. U and T could be any arbitrary inductive-recursive definition. | 22/04 00:32 |

dolio | Universes are just a go-to example. | 22/04 00:32 |

dolio | I guess well-formed ordinals would be a simpler example. | 22/04 00:33 |

dolio | To build well-formed ordinals, you only need ordering on smaller ordinals than the one you're building to be defined, or something. | 22/04 00:34 |

fax | *nod* | 22/04 00:35 |

fax | but how do we know there isn't some crazy inductive-recursive thing you can define which lets you prove false | 22/04 00:35 |

dolio | I think Dybjer has set theoretic models and stuff, too. | 22/04 00:36 |

dolio | If you trust set theory. | 22/04 00:36 |

dolio | Set theory + Mahlo cardinals, apparently. | 22/04 00:38 |

fax | I don't want to say that's just replacing the problem with another one because I haven't worked through any real details of Mahlo cardinals. | 22/04 00:40 |

fax | but I am terrified of them :D | 22/04 00:40 |

glguy | Why is subtraction on the naturals written as "∸"? What is the significance of that operator? | 22/04 00:52 |

dolio | I'm not sure. Maybe because zero - n = zero isn't what you'd expect from standard subtraction. | 22/04 00:53 |

dolio | (Unless n = zero, of course) | 22/04 00:53 |

glguy | we need a pastebin that actually runs agda --html on a given input and which has the standard library included | 22/04 00:54 |

dolio | Totally. | 22/04 00:54 |

glguy | there could be a flag for a set of imports and module heading if you just wanted a single definition to paste | 22/04 00:54 |

dolio | If only someone here had written a Haskell pastebin or something. | 22/04 00:55 |

glguy | Is there anything a malicious user could do to the "agda --html" execution with an arbitrary (up to a size bound) source file? | 22/04 00:55 |

glguy | are there some {-# OPTIONS ... #-} that could be dangerous? | 22/04 00:56 |

dolio | Conceivably, actually. | 22/04 00:56 |

dolio | I'm not sure how much --html runs, but there are pragmas to access arbitrary Haskell, which probably includes IO. | 22/04 00:56 |

glguy | hmm | 22/04 00:57 |

dolio | You'll have to ask the mailing list for a definitive answer, though, I think. | 22/04 01:00 |

pigworker | But if there's no haskell to link to inside the pastebin..? | 22/04 01:02 |

dolio | Oh, that's true. I guess you may not need ghc installed to run the agda executable. | 22/04 01:04 |

Saizan | even if you can FFI import arbitrary haskell functions i'd be surprised if they get evaluated during typechecking, and you'd also need unsafePerformIO | 22/04 01:07 |

dolio | Type checking in a dependently typed language requires normalizing arbitrary terms. | 22/04 01:07 |

dolio | So if you do import unsafePerformIO, you can make it happen during type checking. | 22/04 01:07 |

pigworker | It's important to have some denotational model of dangerous things, though. | 22/04 01:09 |

lpjhjdh | So I need to branch on the equality of two things which get compared in a with. I tried writing the term with "T | no prf" but it says typechecking of with applications is not implemented, is there a trick or do I just have to factor it out? | 22/04 01:09 |

edwinb | doesn't that depend how you do IO though? | 22/04 01:09 |

edwinb | I've never had any trouble with arbitrary IO in types, because effectively IO is just an EDSL that gets interpreted only at run-time... | 22/04 01:10 |

pigworker | Yeah, no open-term FFI! | 22/04 01:10 |

edwinb | I have a DSL for FFI too ;) | 22/04 01:10 |

edwinb | naturally | 22/04 01:11 |

dolio | Well, if you don't have unsafePerformIO, or something analogous, I don't imagine having IO in your language would be a danger during type checking. | 22/04 01:12 |

edwinb | Even if you do, it can't reduce... | 22/04 01:12 |

Saizan | it seems IO operations get postulated and then {-# COMPILED .. #-} to the haskell equivalent, so even if you FFI imported something like Data.List.length i think it'd just work as any other postulate and not compute further | 22/04 01:12 |

edwinb | since it needs the IO to actually happen before it can | 22/04 01:13 |

dolio | Oh, I see. | 22/04 01:13 |

edwinb | IO is just a description of what will happen when you're in a position to do it | 22/04 01:13 |

dolio | Kind of like pigworker's "add fix to the language, but have it opaque during type checking" idea. | 22/04 01:14 |

pigworker | edwinb: possibly with a quotient, relating equivalent things you're not going to do just now | 22/04 01:15 |

edwinb | mm | 22/04 01:15 |

edwinb | Anyway, I was going to bed an hour ago. Better late than never. | 22/04 01:15 |

pigworker | edwinb: it'd be a bonnus if we could do it | 22/04 01:15 |

edwinb | night ;) | 22/04 01:15 |

pigworker | I once saw a lovely talk by Tarmo about monadic packaging of general recursion, but where are the slides? | 22/04 01:18 |

dolio | I have them somewhere, I think. | 22/04 01:18 |

pigworker | the inert fix idea is the monad (Reader (forall a. (a -> a) -> a)) | 22/04 01:19 |

pigworker | but there are more subtle monads which do a better job | 22/04 01:19 |

dolio | Ah, I hadn't thought of it like that. | 22/04 01:19 |

dolio | Maybe I don't have the slides you're thinking of. | 22/04 01:19 |

pigworker | here's a version http://www.ioc.ee/~tarmo/tday-veskisilla/uustalu-slides.pdf | 22/04 01:21 |

dolio | Ah, these aren't the ones I was thinking of. | 22/04 01:22 |

pigworker | I can't find them. I'm sure they included a function called unsafePerformVenanzio. | 22/04 01:22 |

dolio | Heh, well, I definitely don't recall that. | 22/04 01:23 |

pigworker | or maybe that was just a joke in the room at the time | 22/04 01:23 |

pigworker | The nice thing about delay monads is that you can shake a value out of them safely with an always-eventually proof. | 22/04 01:25 |

dolio | I rather worry about whether that sort of thing could ever be efficient. | 22/04 01:26 |

pigworker | Abstracting over a mythical fix just disables computation completely. | 22/04 01:26 |

pigworker | The termination proof gets nuked at closed-term run time. | 22/04 01:27 |

dolio | Wrapping all your recursive calls and such in boxes doesn't seem like it'd be free. | 22/04 01:28 |

dolio | Not to mention racing combinators and such. | 22/04 01:28 |

pigworker | On open terms, it's not free. | 22/04 01:28 |

pigworker | Now, I always asked these guys for the API, and they always wanted to give me the model. | 22/04 01:29 |

pigworker | I don't really want to implement the monad that way, although I do want it to have a model. | 22/04 01:30 |

dolio | Yeah. | 22/04 01:31 |

dolio | I suppose part of the problem is that writing in the 'guarded by coconstructors' style pretty much requires you to know about the model. | 22/04 01:31 |

dolio | At least if you want to write normal corecursive functions in the language. | 22/04 01:32 |

pigworker | I'm not sure we should conflate total corecursion with general recursion, even if that's the model. | 22/04 01:32 |

pigworker | Suppose you wanted to build some f : T by general recursion. If I gave you a monad with f : T as an operation, you could probably do it. General recursion, seen as calling out to an oracle for recursive calls. | 22/04 01:35 |

Saizan | with an oracle for the recursive occurrences or "fix", would you be able to prove always-eventually properties? | 22/04 01:54 |

Saizan | i guess fix's type could give something to work with | 22/04 01:54 |

pigworker | If you take the monad lambda X. nu Y. X + T -> Y, that lets you ask for T's indefinitely. If you prove you always eventually stop asking, you can pull out whatever it is you've made X (T, I suspect). | 22/04 02:06 |

pigworker | goodness me, is that the time? I always eventually go to bed... g'night! | 22/04 02:09 |

Saizan | heh | 22/04 02:10 |

dolio | Success! | 22/04 02:22 |

dolio | Nope, failure. | 22/04 02:36 |

Saizan | the double polymorphic Pi? | 22/04 02:37 |

dolio | Yeah. I wrote it, but almost everything gets stuck. | 22/04 02:38 |

dolio | Because, say, if you want to use it with U n => U n, the output is U (n \lub n). | 22/04 02:39 |

dolio | Which is n, but Agda doesn't reduce it. | 22/04 02:39 |

dolio | So, like, an identity schema has a type in U (suc n \lub n \lub n). | 22/04 02:40 |

dolio | Which isn't ideal. | 22/04 02:40 |

dolio | Goes to show you the kind of magic that Agda's universe polymorphism does behind the scenes, I guess. | 22/04 02:41 |

Saizan | and you're not even required to prove l \lub l = l | 22/04 02:45 |

dolio | Well, I mean, I could prove that here, but I'd have to go around sticking subst everywhere. | 22/04 02:46 |

dolio | So, what agda does is use it as an extensional reduction rule, essentially. | 22/04 02:47 |

Saizan | i'm talking about the \lub one gives to Agda for --universe-polymorphism | 22/04 02:47 |

dolio | I guess it's not extensional if it's used as a reduction rule. | 22/04 02:48 |

dolio | That's something I've never really been clear on. Lots of people refer to eta equality as 'extensional', but then some theories actually do eta expansion as part of their normal forms. | 22/04 02:51 |

dolio | For instance, Agda (although I guess they're trying to cut down on unnecessary eta expansion). | 22/04 02:52 |

Saizan | maybe they are used to Coq? | 22/04 02:55 |

Saizan | (which doesn't do eta-expansion i think) | 22/04 02:55 |

fax | cut down on eta expansion? :o | 22/04 03:08 |

fax | like a performance optimiasation that produces the same results? | 22/04 03:08 |

dolio | Yes. Eta is apparently part of why Agda uses so much memory. | 22/04 03:08 |

fax | yeah Coq doesn't do any type directed conversion | 22/04 03:08 |

fax | (which is too bad!) | 22/04 03:08 |

fax | dolio wow that's kind of crazy I mean it makes things a little bigger.. but didnt realize it was such a problelm | 22/04 03:09 |

dolio | I think they said they tried just turning it off for a bit (and there may still be a flag for that), but that breaks a lot of stuff that people actually use. | 22/04 03:10 |

fax | I think eta covers the records too | 22/04 03:10 |

dolio | Yes. | 22/04 03:10 |

fax | I mean that's the whole reason to define things as records as I understand it | 22/04 03:10 |

dolio | I'm not sure how much eta for functions contributes to memory usage. I think the concern is more with using lots of records. | 22/04 03:11 |

--- Day changed Fri Apr 23 2010 | ||

dolio | Hmm, I don't think I can make Desc work right in my universes. | 23/04 04:38 |

fax | you are really pushing this it's cool | 23/04 04:51 |

fax | what's the prbolem with Desc though, and di you try simpler ones like REG & SPT first? | 23/04 04:51 |

dolio | The problem is that fixed points of codes over U are supposed to be in U, but I get complaints that my types aren't strictly positive when I try that. | 23/04 04:56 |

dolio | mu : Desc U T -> U ; T (mu d) = Mu d | 23/04 04:58 |

dolio | And arg : (s : U) -> (T a -> Desc U T) -> Desc U T | 23/04 05:04 |

fax | you define it normally (in Agda), then just put codes for it in the Universe? | 23/04 05:06 |

fax | or were building it into the universe? | 23/04 05:06 |

dolio | Well, the problem with that is that a normal Desc in Agda (codes for Sets) needs to go in Set1. | 23/04 05:07 |

dolio | Which would put all my universes in Set1, at least. | 23/04 05:07 |

dolio | And might cascade into not working again. | 23/04 05:08 |

dolio | Anyhow, I'm not sure there's anything fundamentally different with that negativity than the negativity inherent in inductive-recursive definitions. | 23/04 05:09 |

dolio | But, because it's not directly part of the inductive-recursive definition, it fails. | 23/04 05:09 |

dolio | Maybe I'm wrong, though. | 23/04 05:10 |

fax | oh yeah I see what you mean about Set1 that's true... hmm | 23/04 05:11 |

dolio | Hmm, T doesn't termination check, either. | 23/04 05:37 |

danblick | Could anyone recommend a place to read about formulating category theory in intuitionistic type theory? | 23/04 06:33 |

dolio | Are you familiar with formulating stuff like algebra in it? | 23/04 06:38 |

danblick | Actually I only know the basics | 23/04 06:40 |

dolio | Well, I'd recommend finding something on dependently typed records. | 23/04 06:42 |

dolio | http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.9569&rep=rep1&type=pdf | 23/04 06:43 |

fax | by the way | 23/04 06:43 |

dolio | Something like that. | 23/04 06:43 |

fax | I am not sure anyone knows how to do algebra or category theory in dependent types yet | 23/04 06:43 |

dolio | Once you get the gist of that, it's just a matter of substituting definitions in category theory for the definitions about groups/rings/whatever. | 23/04 06:43 |

danblick | dolio: thanks, I'll take a look at that | 23/04 06:44 |

dolio | There's also some category theory people working on founding it more constructively. | 23/04 06:45 |

dolio | I have a large paper/book on FOLDS, which is the author's attempt. It stands for first-order logic with dependent sorts. | 23/04 06:46 |

dolio | Which, via Curry-Howard, intuitionistic type theory is rather like higher-order logic with dependent sorts. | 23/04 06:47 |

dolio | But, I haven't gotten around to reading the thing yet, so I don't know much about it. | 23/04 06:47 |

dolio | Agda needs to get sum indexed induction-recursion. | 23/04 08:38 |

dolio | That would make some of my stuff nicer. | 23/04 08:39 |

dolio | Heh, apparently Agda 1 had some kind of indexed induction-recursion. | 23/04 08:42 |

glguy | given: bound n y x = x <′ y × y <′ n , is it possible to prove Acc (bound 10) 5 ? (using Induction.WellFounded) | 23/04 19:24 |

glguy | these Acc proofs are bending my brain... | 23/04 19:24 |

glguy | Perhaps I'm trying to use the wrong < definition? | 23/04 19:25 |

dolio | I've tried writing something like that before, and found it quite difficult. | 23/04 21:19 |

fax | huh I don't undesrtand that measure | 23/04 21:25 |

fax | why is Acc (bound 10) 5 rather than Acc (bound 10)? | 23/04 21:25 |

glguy | oh, I'd be happy with forall x. x < 10 -> Acc (bound 10) x | 23/04 21:26 |

glguy | I was just starting with something more concrete :) | 23/04 21:26 |

fax | no I don't understand what you are doing | 23/04 21:26 |

fax | I mean what about Acc (<)? | 23/04 21:27 |

glguy | that only works for chains /down/ to 0 | 23/04 21:27 |

fax | isn't that useable in the same way? | 23/04 21:27 |

fax | oh! | 23/04 21:27 |

glguy | I want chains /up to/ a bound, say 10 | 23/04 21:27 |

fax | well maybe you could prove Acc R -> Acc (R`on`f) | 23/04 21:28 |

fax | and have f(n) = bound - n | 23/04 21:28 |

glguy | I wanted to sum the even elements of the Fibonacci sequence up to some bound (easy Project Euler problem) without introducing some artificial measure that would cause me to have to make a fake case for when my measure was too small | 23/04 21:30 |

glguy | I was thinking that I could do something like compute fibs as a Colist and then prove that the elements of the list were strictly increasing or something | 23/04 21:32 |

glguy | and then have a function that took them up to a bound... | 23/04 21:32 |

dolio | That's pretty much why I was trying to do the proof, too. | 23/04 21:38 |

dolio | Never finished, though. | 23/04 21:38 |

fax | I think my way with the subtract seems pretty good | 23/04 21:39 |

--- Day changed Sat Apr 24 2010 | ||

fax | dolio? | 24/04 00:21 |

fax | what about defining category theory in this inductive-recursive way? | 24/04 00:21 |

fax | do you think that would be good? There was this problem I encountered (and Huet is talking about it in this paper) where you have to define the Record Category twice, to define the category of categories | 24/04 00:22 |

fax | I should probably do an experiment | 24/04 00:22 |

dolio | fax: Universe polymorphism is the typical solution to that, but perhaps induction-recursion can also help. | 24/04 01:21 |

fax | well I had to make everything indices instead of fields to do it with polymorphism | 24/04 01:22 |

fax | so it should be interesting to see if it can be done just as fields with ind-rec | 24/04 01:22 |

dolio | I mean, a fair amount of the stuff you can do with universe polymorphism can instead be done by defining inductive-recursive universes. | 24/04 01:25 |

dolio | The issue with that is that at that point, you're not formalizing category theory in Agda. You're using Agda like the logical framework, to formalize an object language, and formalizing category theory in that object language. | 24/04 01:26 |

dolio | In a sense. | 24/04 01:26 |

fax | yes! | 24/04 01:28 |

fax | that sounds great! | 24/04 01:28 |

fax | the object language being the language of categories? | 24/04 01:28 |

dolio | I was thinking more like the object language being a dependent type theory with universe polymorphism. | 24/04 01:29 |

fax | but we already have one | 24/04 01:29 |

fax | this wont work will it? | 24/04 01:29 |

dolio | But it's conceivable that you could do category theory directly. | 24/04 01:29 |

dolio | I'd have to actually think about it. :) | 24/04 01:30 |

dolio | I've kind of been wondering how much of set theory induction-recursion lets you formalize. | 24/04 01:37 |

dolio | Like, impredicativity lets you formalize something close to ZF, as I recall. | 24/04 01:37 |

fax | I don't actually know what set theory induction-recursion means | 24/04 01:41 |

fax | I am not sure I've ever seen this | 24/04 01:41 |

dolio | Well, I think the Dybjer papers give models of it in ZF + mahlo cardinal. | 24/04 01:42 |

dolio | But I don't actually know what a Mahlo cardinal is. | 24/04 01:42 |

fax | All in all, we came to the conclusion that, out there, there are people working harder on Epigram than we do. So, here is the kit for you to become an Epigram implementor: | 24/04 17:31 |

fax | http://www.e-pig.org/epilogue/?p=497 | 24/04 17:31 |

fax | http://www.youtube.com/watch?v=IFACrIx5SZ0 | 24/04 17:33 |

Mathnerd314 | what? how do monkeys paddling canoes have to do with Epigram? | 24/04 19:02 |

Adamant | Mathnerd314: I'm not sure what spies would use .45mm 'questioners' either | 24/04 22:34 |

Adamant | usually those tend to be in inches | 24/04 22:34 |

* Mathnerd314 checks to ensure date is not April 1 | 24/04 22:37 | |

Mathnerd314 | yep... | 24/04 22:37 |

glguy | Is there anything written up specifically comparing Epigram and Agda? | 24/04 22:56 |

shapr | I'd also like to see such a thing. | 24/04 23:00 |

fax | the main difference is that agda is intuitionistic but epigram is based on observational type theory | 24/04 23:01 |

fax | agda is still changing (a lot though), and of course epigram is changing faster | 24/04 23:02 |

fax | the main difference (from my point of view ..) | 24/04 23:02 |

Saizan_ | did you mean intensional rather than intuitionistic? | 24/04 23:02 |

fax | yes that's what I shoul dhave said, thanks | 24/04 23:03 |

fax | they're both intuitionistic | 24/04 23:03 |

Saizan_ | also, Epigram seem to aim at making the user define its datatypes from within the theory, using an universe | 24/04 23:04 |

Saizan_ | currently the Mu and Nu fixpoints are external from the universe though | 24/04 23:05 |

dolio | There's a model written in Agda for the datatype descriptions that's approximately how it would work in real Epigram with a hierarchy of universes. | 24/04 23:11 |

dolio | Desc {n} : Set {suc n} | 24/04 23:11 |

dolio | Desc {n} is descriptions of datatypes over Set n | 24/04 23:11 |

dolio | D : Desc {n} ==> Mu D : Set n | 24/04 23:12 |

fax | one great thing in epigram is quotient types I think that will be really useful | 24/04 23:12 |

Saizan_ | dolio: there's a whole collection of those models, rather :) | 24/04 23:12 |

glguy | I usually see extensional as the opposite to intensional, what is observational? | 24/04 23:13 |

fax | glguy it's sort "best of both worlds" :D apparently | 24/04 23:13 |

dolio | But that's just the core type theory. In a real, for-use language, you'd write more Agda-like declarations (or Epigram 1-like), and it'd get elaborated into that Desc stuff. | 24/04 23:13 |

fax | there's a couple papers on it but they're quite difficult to understand... I'm hoping they write more soon | 24/04 23:13 |

dolio | You'd probably only use Desc and the like for generic programming. | 24/04 23:13 |

fax | glguy: you know how Coq just has beta conversion (and similar) but Agda has some stuff like eta-expansion, which are type directed | 24/04 23:14 |

fax | glguy: Well I think OTT makes use of that type-directed stuff and pushes it even further | 24/04 23:14 |

dolio | glguy: Both intensional and extensional type theories treat judgmental/definitional equality as linked with the equality datatype. | 24/04 23:15 |

dolio | Intensional type theory does that by making equality weak, so only things that reduce to the same normal form are equal, even according to the equality type. | 24/04 23:15 |

dolio | Extensional type theory lets you define custom equalities for each type, and then reflects them into the typing judgments, using them as actual reduction rules, essentially. | 24/04 23:16 |

dolio | In OTT, the equality type is no longer pegged to the judgmental equality. So you can prove that f == g : A -> B, but that doesn't mean that the typing rules will judge that P f = P g, for P : (A -> B) -> Type, or something. | 24/04 23:18 |

Saizan_ | though it's still substitutive | 24/04 23:18 |

dolio | However, due to the OTT folks taking some care, the equality type does have an elimination rule similar to the elimination rule for intensional equality. | 24/04 23:19 |

fax | I tried to implement OTT but got completely confused & stuck | 24/04 23:19 |

dolio | So it works a lot like the equality type you get in Agda, but it allows you to prove things you'd have to postulate in Agda, because they're extensional. | 24/04 23:21 |

dolio | Like (forall x. f x == g x) -> f == g for functions. | 24/04 23:21 |

dolio | Or bisimulation for coinductive types. | 24/04 23:21 |

fax | it's a shame that equality is not built in! but I will get over it | 24/04 23:22 |

fax | I was so excited to learn about defining eq as a data type | 24/04 23:22 |

fax | (when I started to learn about coq) | 24/04 23:22 |

fax | wait I mean that it IS built in | 24/04 23:22 |

Saizan_ | that makes me wonder what kind of beast you get if you define a standard equality type in epigram, could you call it intensional equality? you could still use == to do "extensional" coercions | 24/04 23:25 |

dolio | (And of course, equality for quotients is whatever equivalence relation by which they're quotiented.) | 24/04 23:25 |

dolio | I have a paper here that has a type theory with multiple equalities... | 24/04 23:26 |

dolio | Intensionality, Extensionality and Proof Irrelevance in Modal Type Theory | 24/04 23:27 |

fax | Pfenning? | 24/04 23:27 |

dolio | Yes. | 24/04 23:27 |

dolio | It's a lot like the erasure pure type systems. | 24/04 23:27 |

dolio | It has three different kinds of typing judgments. | 24/04 23:28 |

dolio | M :: A, which is more intensional than usual (only alpha equivalence). | 24/04 23:28 |

dolio | M : A which beta-eta | 24/04 23:28 |

dolio | And M % A which is irrelevant. | 24/04 23:29 |

fax | *nod* | 24/04 23:29 |

dolio | And then there's == for intensional equality and = for extensional (which in this context just means that functions are eta-equivalent, I think). | 24/04 23:29 |

dolio | Anyhow, the idea is that you don't need an A : Set and an A' : Prop with nearly the same definition just to get one to be irrelevant. It's all in how you use the type, same as EPTS. | 24/04 23:30 |

fax | I had fun inventing my own proof irrelevant type system but eventually realized it didn't have subject reduction | 24/04 23:31 |

dolio | Heh. | 24/04 23:31 |

fax | took me a long time to notice! | 24/04 23:31 |

fax | but I was using modality too | 24/04 23:32 |

dolio | The paper mentions that you'd probably want actual modal operators as part of a language for programming, but they leave that for further work. | 24/04 23:34 |

fax | dolio, I'm still coming to terms with this induction-recursion stuff :P | 24/04 23:42 |

dolio | I sent an overzealous message about it to the agda list. | 24/04 23:52 |

fax | about what ? | 24/04 23:53 |

fax | well I will just read it actualyl | 24/04 23:53 |

Saizan | is there a good explanation of canonicity somewhere? particularly wrt proof irrelevance | 24/04 23:53 |

dolio | I was thinking one could define an indexed family of universes U : N -> Set, T : (n : N) -> U n -> Set all at once by allowing T (suc n) (u n) = U n... | 24/04 23:54 |

dolio | Which isn't strictly positive, but it's defining a higher universe strictly by reference to lower universes. | 24/04 23:55 |

dolio | And I thought one of the Dybjer papers was about that, but I was mistaken. | 24/04 23:55 |

dolio | It was just about defining indexed families via induction-recursion, which Agda already allows. | 24/04 23:55 |

fax | huh | 24/04 23:56 |

fax | I didn't realize that Agda didn't have IIR | 24/04 23:56 |

dolio | It does have IIR. | 24/04 23:56 |

fax | oh | 24/04 23:56 |

dolio | I subsequently realized that my criterion was kind of ad-hoc, and not what IIR is. | 24/04 23:56 |

dolio | It requires restrictions on the indices that aren't normally enforced for inductive families. | 24/04 23:58 |

--- Day changed Sun Apr 25 2010 | ||

fax | so in category theory they call ¡ gnab | 25/04 04:57 |

fax | ¡ : 0 --> B | 25/04 04:57 |

--- Day changed Mon Apr 26 2010 | ||

Saizan_ | is there a command to get the fully normalized form of a goal displayed? | 26/04 01:41 |

dolio | C-c C-, does more normalization than is shown just by C-c C-l. | 26/04 01:41 |

dolio | You type the former while the cursor is inside the goal. | 26/04 01:42 |

dolio | I think it gives the fully normalized type. | 26/04 01:43 |

Saizan_ | except i can't input C-, on a terminal, i'll look for the function it's bound to | 26/04 01:44 |

dolio | You can't? | 26/04 01:44 |

dolio | Huh, I guess it just enters ,. | 26/04 01:45 |

dolio | Weird. | 26/04 01:45 |

Saizan_ | yeah, i wonder if one could fix that by just chaning the terminal, though maybe there's no way to communicate "C-," to a textual emacs | 26/04 01:48 |

Saizan_ | agda2-goal-and-context btw | 26/04 01:51 |

stevan | Saizan_: try: (global-set-key (kbd "C-c ,") 'agda2-goal-and-context) | 26/04 19:03 |

stevan | works for me in terminals, had the same problem... | 26/04 19:04 |

glguy | If I create a "measure" on my data type that returns a natural, shouldn't I be able to reuse the well-founded induction proofs defined for Nat with my measure? | 26/04 19:06 |

fax | glguy: that's what I was talking about yesterday | 26/04 19:12 |

fax | if R is well founded then R`on`f is too | 26/04 19:12 |

glguy | yeah, but now I'm trying to figure out how to do it :) | 26/04 19:12 |

fax | you'd need to prove that first | 26/04 19:12 |

fax | there's a really cool paper all about this if you want | 26/04 19:13 |

glguy | oh? | 26/04 19:13 |

fax | http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-57.pdf | 26/04 19:14 |

glguy | wow, I'm just barely older than that paper :) | 26/04 19:14 |

fax | (the construction we've been talking about is inverse image) | 26/04 19:15 |

glguy | thanks, I'll give it a look | 26/04 19:15 |

glguy | fax: lem : {A B : Set} (f : A → B) (R : B → B → Set) (x : A) → WF.Acc R (f x) → WF.Acc (R on f) x | 26/04 19:25 |

glguy | lem f R x (WF.acc rs) = WF.acc (λ y x' → lem f R y (rs (f y) x')) | 26/04 19:25 |

glguy | something like this? | 26/04 19:25 |

fax | wow that was fast | 26/04 19:25 |

fax | glguy, since WF is a proof -- if that type checks it's correct :) | 26/04 19:26 |

fax | Acc* | 26/04 19:26 |

glguy | yeah, it type checks | 26/04 19:27 |

glguy | I just have to figure out how to make use of it now :) | 26/04 19:27 |

fax | it's a bit rubbish writing out recursion using WF | 26/04 19:28 |

fax | that's something which would be nice as a language feature | 26/04 19:28 |

glguy | yeah... but I want to do it today :) | 26/04 19:28 |

fax | like in coq you write Fixpoint f ... {measure foo} := ... | 26/04 19:28 |

fax | but there isn't really anywhere to write that in the agda syntax | 26/04 19:29 |

glguy | I'm learning Isabelle and the current exercise was to do a function that required an explicit measure and termination proof using the Function package | 26/04 19:29 |

glguy | in parallel I'm doing the exercises in Agda | 26/04 19:29 |

glguy | and I refuse to not be able to write this in Agda :) | 26/04 19:29 |

fax | the way you are doing it sounds a little different from 'define the function and then prove it terminates' | 26/04 19:30 |

fax | because the natural way to write, in agda.. is not that way | 26/04 19:30 |

glguy | well, my goal is to be able to define the function in agda and not have the ugly red "you didn't terminate" indicator come up | 26/04 19:31 |

glguy | I know that this won't be the prettiest implementation | 26/04 19:31 |

fax | it might be interesting if the red gave you a proof obligation | 26/04 19:32 |

fax | instead of just saying _rewrite this_ | 26/04 19:32 |

glguy | certainly interesting | 26/04 19:32 |

glguy | That seemed to work | 26/04 19:34 |

glguy | I got a proof that all the elements in my data type are accessible now | 26/04 19:34 |

glguy | using the measure I defined | 26/04 19:35 |

glguy | and Nat's allAcc proof | 26/04 19:35 |

glguy | it works :) now all I have to do is plumb through an accumulator parameter | 26/04 19:41 |

glguy | but the recursion structure I needed is proven to terminate using wfrec | 26/04 19:41 |

glguy | thanks for the nudge, fax | 26/04 19:41 |

fax | okay :) | 26/04 19:41 |

glguy | http://www.galois.com/~emertens/treerec/treerec.html | 26/04 19:48 |

glguy | The preOrder function at the bottom isn't done yet but has the right recursion structure | 26/04 19:48 |

glguy | OK, I've updated it to actually do the traversal | 26/04 19:53 |

glguy | (if anyone is following along at home) | 26/04 19:53 |

fax | glguy, is this function equal to: | 26/04 19:55 |

fax | pre (leaf y :: xs) = [y] ++ pre xs | 26/04 19:55 |

fax | pre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y0 | 26/04 19:55 |

fax | ? | 26/04 19:55 |

fax | oops! | 26/04 19:55 |

fax | ++ pre xs to both | 26/04 19:55 |

fax | oh no I got it on the first, just add it to the second line | 26/04 19:56 |

fax | pre (leaf y :: xs) = [y] ++ pre xs | 26/04 19:56 |

fax | pre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y0 ++ pre xs | 26/04 19:56 |

fax | pre [] = [] | 26/04 19:56 |

glguy | yup, looks about right | 26/04 19:56 |

glguy | I wanted to write it using only tail calls | 26/04 19:56 |

fax | ah! | 26/04 19:56 |

glguy | the exercise is to write it a few different ways | 26/04 19:57 |

stevan | name your constructors and get nicer names from C-c C-c!? :-) | 26/04 19:57 |

glguy | I'm cleaning up the names now :) | 26/04 19:57 |

stevan | if you do, node : (x : A)(l r : Tree A) -> Tree A then C-c C-c will use x, l, r instead of x, y', y0 etc | 26/04 19:58 |

stevan | no cleaning up needed :-) | 26/04 19:59 |

glguy | Yeah, I know about that, I'm just always hesitant to name parameters that I don't need to be named | 26/04 19:59 |

glguy | I feel like I'm lying about using them for dependent types | 26/04 19:59 |

stevan | hehe | 26/04 19:59 |

stevan | i name everything so i don't need to write out the arrows | 26/04 20:00 |

glguy | I like typing \r and seeing the arrow appear :-D | 26/04 20:00 |

glguy | when I switch from Agda back to Haskell I often get a few \r's in my code | 26/04 20:00 |

fax | glguy, but a -> b is just shorthand for (_ : a) -> b | 26/04 20:01 |

glguy | I know that it doesn't change the meaning | 26/04 20:01 |

glguy | OK OK, I've changed my constructor :-p | 26/04 20:02 |

stevan | if you use UnicodeSyntax and agda-input mode you can have \r in haskell too! :-) too bad \Gl doesn't work however :-/ | 26/04 20:02 |

stevan | i hope nobody will drive us from the unicode paradise which Agda created for us | 26/04 20:04 |

fax | actually I hate unicode | 26/04 20:09 |

stevan | :-( | 26/04 20:09 |

fax | I'm using LaTeX a lot recently, it's bloody awful but it's better than unicode | 26/04 20:09 |

fax | it's actually got support for things like super and subscripts, radicals, typefaces (very important) | 26/04 20:10 |

fax | but the way we use it sucks, and it's very slow (as is texmacs) - so it's not suitable for a programming langage | 26/04 20:11 |

fax | editor | 26/04 20:11 |

stevan | sure, having the power of latex in source code would be even better than unicode of course... didn't alfa have something like that? | 26/04 20:15 |

fax | oh I think so! | 26/04 20:16 |

fax | I never used this but I've seen a screenshot | 26/04 20:17 |

fax | I think latex kind of sucks though, at least it's possible to do better | 26/04 20:17 |

stevan | yeah, some here; only seen a screenshot | 26/04 20:17 |

fax | maybe we can't NOT use latex because it's so pervasive | 26/04 20:17 |

fax | that means finding a good subset | 26/04 20:17 |

fax | and specifying it formall | 26/04 20:17 |

fax | formally | 26/04 20:17 |

fax | as I see it, support like this would be a HUGE improvement in terms of readbility of programs | 26/04 20:18 |

fax | (which is important) | 26/04 20:18 |

fax | but it would also mean a slight increase in complexity of editors | 26/04 20:18 |

fax | (which is a **REALLY BAD THING**) | 26/04 20:18 |

fax | but I think it's unavoidable | 26/04 20:18 |

stevan | a friend had an idea to use webkit and mathml as base for an editor, not sure how well that would work, but you would get the rendering for free atleast | 26/04 20:19 |

fax | that sounds like a good project (I really really hate mathml but if it's only being used for rendering that is cool) | 26/04 20:21 |

* glguy wonders how you would go about proving anything about a function defined with well-founded induction | 26/04 22:21 | |

fax | glguy, the first thing I'd do is prove the equations that define the program | 26/04 22:21 |

fax | (they should all be provable by reflexivity) | 26/04 22:22 |

glguy | fax, can you give an example of what the type of that might look like | 26/04 22:39 |

glguy | my first attempt with something like: lemma-leaf : ∀ a ts xs → preOrder′ (leaf a ∷ ts) xs ≡ preOrder′ ts (xs ++ [ a ]) | 26/04 22:39 |

glguy | is proving harder than I'd have expected | 26/04 22:39 |

glguy | preOrder′ ts xs = wfRec PreOrderPred body (ts , xs) | 26/04 22:39 |

fax | lemma-leaf _ _ _ = refl | 26/04 22:39 |

fax | doesn't work ? | 26/04 22:39 |

glguy | no, due to the Acc proof being different | 26/04 22:40 |

fax | wait huh | 26/04 22:40 |

glguy | I'll paste the goal | 26/04 22:40 |

fax | oh I see | 26/04 22:40 |

glguy | http://fpaste.org/EN7d/ | 26/04 22:41 |

fax | what's preOrder′? | 26/04 22:41 |

glguy | preOrder′ ts xs = wfRec PreOrderPred body (ts , xs) | 26/04 22:41 |

fax | okay that's preOrder in the file I am looking at | 26/04 22:41 |

glguy | roughly | 26/04 22:41 |

glguy | it exposes the accumulator | 26/04 22:42 |

fax | you could try enabling proof irrelevance | 26/04 22:43 |

fax | (there's a flag for it) | 26/04 22:43 |

fax | (I've never tried this) | 26/04 22:43 |

glguy | because Acc has a single constructor? | 26/04 22:43 |

glguy | I thought that proof irrelevance went away in 2.26 | 26/04 22:43 |

glguy | 2.2.6 | 26/04 22:43 |

fax | oh that's too bad | 26/04 22:44 |

fax | im sure I proved the equations with refl | 26/04 22:44 |

fax | when I used acc | 26/04 22:44 |

glguy | .Induction.Nat._.helper | 26/04 22:45 |

glguy | where class considered harmful | 26/04 22:45 |

glguy | clause* | 26/04 22:45 |

dolio | glguy: Perhaps this isn't helpful, but you'd likely prove your theorem by well-founded induction as well. | 26/04 23:14 |

glguy | dolio, well it is certainly helpful in the sense that it confirms what I originally assumed last time I tried to prove anything about a function defined in this way | 26/04 23:24 |

dolio | :) | 26/04 23:24 |

dolio | It follows the general pattern that proving something about a function involves induction shaped like the recursion in the function. | 26/04 23:25 |

glguy | but it was hard enough to write the function the first time :( | 26/04 23:25 |

glguy | My "Predicate" will certainly be more interesting this time as the type of the proof will change at each recursive call | 26/04 23:26 |

dolio | Yeah. | 26/04 23:26 |

glguy | not some boring old \ _ -> List A | 26/04 23:26 |

--- Day changed Tue Apr 27 2010 | ||

glguy | fax, through some form of magic... I was able to do my program as the three equations | 27/04 01:07 |

glguy | using refl | 27/04 01:07 |

glguy | and one rewrite (which I had to use in my definition) | 27/04 01:07 |

fax | cool! what magic! | 27/04 01:07 |

glguy | well, I started with lifting the helper for Nat's allAcc out of the where clause | 27/04 01:09 |

glguy | I don't know that that fixed it, but either I had a typo in my original attempt | 27/04 01:09 |

glguy | or that fixed it | 27/04 01:09 |

fax | glguy, do you still have the one that doesn't work? it'd be kind of interesting to look at that | 27/04 01:10 |

fax | (though I will have to do it tommorow) | 27/04 01:10 |

fax | and I just mean for my own curiosity.. | 27/04 01:10 |

glguy | I don't have it handy, but I'll experiment tonight to reproduce | 27/04 01:10 |

glguy | http://www.galois.com/~emertens/treerec/treerec.html | 27/04 01:11 |

glguy | check out the three definitions at the bottom of the file | 27/04 01:11 |

fax | well I am not keen on +-assoc (treeSize t₁) (treeSize t₂) (sum (map treeSize ts)) | 27/04 01:11 |

fax | but the other two are good :P | 27/04 01:11 |

glguy | I wouldn't have done that if it worked without it :-p | 27/04 01:11 |

Saizan_ | i feel a bit lost when there's an heavy use of type synonyms | 27/04 01:26 |

glguy | dolio, still there? | 27/04 03:00 |

dolio | Yes. | 27/04 03:00 |

glguy | http://www.galois.com/~emertens/treerec/treerec.html | 27/04 03:00 |

glguy | oh, it is still uploading | 27/04 03:01 |

glguy | refresh that in a moment | 27/04 03:01 |

glguy | I have the WfRec implementation with all of the equations regarding how it operates on its arguments | 27/04 03:01 |

glguy | OK, done | 27/04 03:01 |

* glguy needs to show someone that understands what just happened | 27/04 03:01 | |

glguy | with all of the equ-* functions I should be able to prove equivalence to a simpler implementation now | 27/04 03:03 |

glguy | pulling the implementations of those functions out of the where clause allows the simplifier to do its work | 27/04 03:05 |

glguy | otherwise they have unrelated arguments from their parent function | 27/04 03:05 |

glguy | and it can't see the equivalence | 27/04 03:05 |

glguy | another case of where clauses considered harmful! | 27/04 03:06 |

Saizan_ | it seems like the translation of where clauses could benefit from some dependency analysis then | 27/04 03:09 |

dolio | glguy: What are you asking me about this? | 27/04 03:11 |

dolio | Also, doesn't preorder traversal have a structurally recursive formulation? | 27/04 03:12 |

glguy | I just wanted to show someone that I managed to get something proved about a function implemented using the WfRec library :) | 27/04 03:12 |

glguy | sure, I'm proving equivalence to that now | 27/04 03:12 |

dolio | Okay. | 27/04 03:12 |

glguy | the exercise was to do a tail-recursive version | 27/04 03:12 |

glguy | and prove that | 27/04 03:12 |

glguy | (in Isabelle) | 27/04 03:12 |

dolio | Ah, okay. | 27/04 03:12 |

glguy | and I wanted to show that even if it took more keystrokes that it was doable in Agda | 27/04 03:13 |

dolio | I think you might even be able to do a tail-recursive structurally decreasing version. | 27/04 03:13 |

glguy | oh yeah? | 27/04 03:13 |

dolio | Hmmm... | 27/04 03:14 |

dolio | I'll let you know in a while. :) | 27/04 03:15 |

dolio | Apparently not. | 27/04 03:24 |

dolio | Unless the new --termination-depth=N flag will accept it. | 27/04 03:27 |

glguy | What's that flag about? | 27/04 03:29 |

dolio | It tries to be smarter about seeing arguments that grow a little, but ultimately shrink. | 27/04 03:29 |

dolio | N is related to how deep it looks for shrinkage or something. | 27/04 03:30 |

dolio | Well, I seem to be unable to pull from the agda repository... | 27/04 03:31 |

dolio | "Caveat: On Tree-like data, it does not work so well." That's probably bad news. :) | 27/04 03:33 |

glguy | ha | 27/04 03:33 |

dolio | Well, hopefully my last checkout has --termination-depth. | 27/04 03:42 |

glguy | OK, I did the equivalence proof, uploaded to the same URL | 27/04 03:43 |

dolio | Yes, if you're trying to prove that a function using well-founded recursion is the same as one using structural recursion, it's probably a better strategy to prove that they do the same thing in each case, and prove by (normal) induction. | 27/04 03:46 |

glguy | Do you think that this is worth writing up as an example for using the WfRec stuff? | 27/04 03:46 |

glguy | seems like there isn't much on Google for examples of using the library | 27/04 03:46 |

dolio | Sure. It's possible you're the first one using it. | 27/04 03:50 |

dolio | I've done some stuff with well-founded recursion/induction, but I just wrote down the specific stuff I needed instead of looking in the library. | 27/04 03:50 |

dolio | Did you ever figure out the getting-closer-to-an-upper-bound thing for fibonaccis? | 27/04 03:52 |

dolio | If not I might take another crack at it. | 27/04 03:53 |

glguy | No, but I might now that I've had a little more success using the stuff | 27/04 03:53 |

glguy | I would encourage you to take your crack | 27/04 03:53 |

glguy | (as I don't have confidence that I'll knock it out) | 27/04 03:54 |

dolio | Well, --termination-depth doesn't magically solve all problems. | 27/04 03:55 |

glguy | Did it solve some? | 27/04 03:56 |

dolio | No. | 27/04 03:56 |

dolio | It didn't make my attempt pass, anyhow. | 27/04 03:57 |

dolio | Not even the simplified version that didn't worry about values at internal nodes. | 27/04 03:57 |

glguy | I need to figure out why this proof breaks when I remove the "abstract" section | 27/04 04:15 |

glguy | so... any suggestions for a name for this? lem : {A B : Set} {R : Rel B _} (f : A → B) (x : A) → WF.Acc R (f x) → WF.Acc (R on f) x | 27/04 06:10 |

glguy | something about "inverse image" from the paper I was referred to earlier | 27/04 06:11 |

glguy | "Constructing Recursion Operators in Intuitionistic Type Theory" | 27/04 06:12 |

dolio | Well, I think I broke my agda-share darcs repository. | 27/04 06:50 |

dolio | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25086#a25086 | 27/04 06:52 |

dolio | I succeeded in proving accessibility for k >= n > m, though. | 27/04 06:52 |

dolio | So, go forth and write fibonacci sequences. | 27/04 06:53 |

dolio | I knew that keeping html files in the repository would turn out badly one day. Oh well. | 27/04 06:54 |

Saizan | well, we couldn't have seen it anyhow, c.h.o webserver is currently broken | 27/04 07:03 |

dolio | I guess that explains why I couldn't pull the latest agda earlier. | 27/04 07:04 |

dolio | But, now I have to start over, I think. | 27/04 07:04 |

dolio | Because that file caused the regeneration of a lot of the html pages, and the output contains lots of randomly generated (as far as I can tell) stuff. | 27/04 07:04 |

dolio | So there are 45,000 changes to view. | 27/04 07:04 |

Saizan | darcs record -a ?:) | 27/04 07:05 |

dolio | Well, there are about 12 changes I don't want to record. | 27/04 07:05 |

dolio | And when I skip those, it just hangs. | 27/04 07:05 |

dolio | So I suspect record -a won't be any better. | 27/04 07:05 |

dolio | And remove html/* takes forever, too. | 27/04 07:05 |

glguy | thanks for that code, dolio | 27/04 07:12 |

glguy | http://www.galois.com/~emertens/treerec/treerec2.html | 27/04 07:12 |

glguy | is my latest revision (now with less code) | 27/04 07:12 |

glguy | I better save your code somewhere before hpaste's takusen backend forgets to unlock the database :) | 27/04 07:14 |

pigworker | how do I find out which version of Agda I'm running? | 27/04 16:15 |

npouillard | pigworker: you mean something else than agda --version | 27/04 16:16 |

ccasin | if you installed it from cabal, your .cabal/packages folder might provide some hints | 27/04 16:17 |

Saizan | if you only have the emacs mode switch to the *ghci* buffer | 27/04 16:17 |

Saizan | near the top you'll see a like like: | 27/04 16:17 |

Saizan | Loading package Agda-2.2.7 ... linking ... done. | 27/04 16:17 |

Saizan | "ghc-pkg list Agda" will show the versions you have installed, btw | 27/04 16:18 |

pigworker | the *ghci* window hint did it for me, thanks; I don't have the standalone | 27/04 16:18 |

pigworker | Thanks guys, version mystery solved: it pays to install after a download... | 27/04 16:23 |

Saizan | heh :) | 27/04 16:29 |

kosmikus | pigworker: I installed epigram yesterday :) | 27/04 16:32 |

pigworker | kosmikus: it'll be different again today | 27/04 16:33 |

kosmikus | :) | 27/04 16:35 |

fax | hey um | 27/04 16:36 |

fax | http://math.etsu.edu/LaTeXMathML/ | 27/04 16:36 |

fax | this is kinda cool | 27/04 16:36 |

fax | http://www1.chapman.edu/~jipsen/mathml/asciimathcalculator.html | 27/04 16:37 |

fax | infact thats more relevant | 27/04 16:37 |

fax | I am wondering if something like this could make a good editor | 27/04 16:38 |

fax | rather than ascii | 27/04 16:38 |

fax | since you get colors, super and subscripts, typefaces, .. | 27/04 16:38 |

fax | (ascii + unicode) | 27/04 16:38 |

fax | maybe there's a plan already (for epigram ?) | 27/04 16:39 |

glguy | fax, the problem was that the <-allAcc definition used a where-clause defined helper | 27/04 16:39 |

glguy | the refl definitions worked once I lifted that | 27/04 16:39 |

fax | glguy -- does that make sense | 27/04 16:39 |

glguy | yeah | 27/04 16:39 |

fax | it sounds like a bug to me | 27/04 16:39 |

fax | why should a where clause be any different ? | 27/04 16:40 |

glguy | in the inductive case the simplifier couldn't see that the two calls to helper were the same because they were indexed by unused arguments to their parent function | 27/04 16:40 |

pigworker | fax: I'm getting out of the UI business | 27/04 16:40 |

* glguy heads in to work | 27/04 16:42 | |

fax | http://i.imgur.com/8p6JM.png -- anyone understand that THROW rule? | 27/04 17:17 |

fax | I don't get why there isn't Gamma |-_T,Delta C | 27/04 17:17 |

fax | (I'm guessing the C just comes from nowhre0 | 27/04 17:17 |

fax | this is from http://pauillac.inria.fr/~herbelin/publis/markov.pdf An intuitionistic logic that proves Markov's principle | 27/04 17:18 |

ccasin | Suppose you are trying to prove T. Start by using Catch. Then, in any subgoal of the proof of T, it's always enough to prove T itself | 27/04 18:08 |

ccasin | though I haven't looked at the paper, so I don't know if that's the most helpful way to read them | 27/04 18:08 |

ccasin | Also I have trouble seeing how it's useful | 27/04 18:11 |

fax | so you prove T by proving T? | 27/04 18:11 |

ccasin | sort of | 27/04 18:12 |

ccasin | I mean, your context might have changed | 27/04 18:12 |

ccasin | OK, I think I have an example | 27/04 18:15 |

ccasin | Suppose you want to prove (A(x) -> B(x)) \/ C(x) | 27/04 18:15 |

ccasin | start with catch | 27/04 18:15 |

ccasin | then decide to prove the left side | 27/04 18:15 |

ccasin | and assume A(x) | 27/04 18:15 |

ccasin | now, with throw, say forget about proving B(x), and prove the original formula instead | 27/04 18:16 |

ccasin | only this time, prove the right subbranch. Now you get to prove C(x) with the extra assumption A(x) | 27/04 18:16 |

fax | ah! | 27/04 18:16 |

fax | that makes sense | 27/04 18:16 |

ccasin | seems weird though! | 27/04 18:17 |

Saizan | so you can prove excluded middle | 27/04 18:18 |

ccasin | yes | 27/04 18:18 |

ccasin | suspicious | 27/04 18:19 |

ccasin | ah, but looking at the paper | 27/04 18:19 |

ccasin | T isn't all terms | 27/04 18:19 |

ccasin | they can't have foralls | 27/04 18:19 |

ccasin | so you can't prove \forall x . P(x) \/ not P(x) | 27/04 18:20 |

ccasin | I think? | 27/04 18:21 |

Saizan | V_I? | 27/04 18:22 |

ccasin | ? | 27/04 18:23 |

Saizan | heh, sorry, i mean using the I rule for \forall at the start, and then the catch .. throw | 27/04 18:25 |

Saizan | you'd only have to catch P(x) \/ not P(x) with x free | 27/04 18:25 |

ccasin | my guess is the freshness condition will gum up the works | 27/04 18:26 |

ccasin | but let's see | 27/04 18:26 |

ccasin | yeah, I think it does | 27/04 18:28 |

ccasin | because, in order to get anywhere, you'll have to add P(x) do your context | 27/04 18:29 |

ccasin | and then x isn't fresh enough to use that assumption after you throw back to LEM | 27/04 18:29 |

ccasin | perhaps that's what you said, I'm just very slow :) | 27/04 18:29 |

Saizan | ah, no, i didn't think about x appearing in Gamma :) | 27/04 18:30 |

--- Day changed Wed Apr 28 2010 | ||

glguy_ | http://www.galois.com/~emertens/recops/recops.html | 28/04 09:26 |

glguy_ | I'm starting to implement the operators from the paper that fax told me about | 28/04 09:27 |

glguy_ | I wonder if some of these ways of constructing well-founded relations shouldn't be in the library | 28/04 09:27 |

roconnor | what's the name of Agda's logic? | 28/04 20:03 |

dolio | You mean like CIC? | 28/04 20:05 |

dolio | I'm not sure it has a name. | 28/04 20:05 |

roconnor | like CIC, or OTT | 28/04 20:09 |

roconnor | or MLT | 28/04 20:09 |

roconnor | MLTT | 28/04 20:09 |

dolio | It's sort of grown by accretion. | 28/04 20:10 |

dolio | Started with inductive families, induction recursion and a predicative hierarchy. | 28/04 20:11 |

roconnor | it seems to be MLTT with universes and induction-recursion | 28/04 20:11 |

dolio | And it's since gotten codata and universe polymorphism. | 28/04 20:11 |

ccasin | ulf's thesis describes it in terms of additions to UTT | 28/04 20:12 |

ccasin | which seems a little odd, since agda lacks an impredicative Prop and its datatype eliminators are stronger than UTT's | 28/04 20:12 |

ccasin | but, so it is | 28/04 20:12 |

fax | I don't think they're ready to specify it formally since agda is about exploring the design spacec no? | 28/04 20:16 |

glguy | http://www.galois.com/~emertens/recops/recops.html | 28/04 21:09 |

glguy | now with ways to construct well-founded relations from subrelations, inverse images, transitive closures and disjoint sums! | 28/04 21:09 |

copumpkin | fancy :) | 28/04 21:12 |

copumpkin | have you tried epigram yet? | 28/04 21:12 |

glguy | nope | 28/04 21:13 |

glguy | I wasn't sure which version of it I was supposed to try | 28/04 21:13 |

glguy | maybe rather than bombarding you guys with whatever agda I did that day I should just twitter it... | 28/04 21:20 |

copumpkin | I don't object to you doing both :P | 28/04 21:20 |

copumpkin | I think I already follow you on twitter | 28/04 21:20 |

fax | glguy, transitive closure is my favorite | 28/04 21:21 |

glguy | That one was the most fun to work out | 28/04 21:21 |

glguy | I had to think about what I was doing rather than just following the types | 28/04 21:21 |

fax | :D | 28/04 21:22 |

fax | you can define single step recursion and take the transitive closure to get structural recursion | 28/04 21:23 |

fax | single step recursion is easy to prove from the eliminator of a type | 28/04 21:23 |

fax | this could form the basis of an implementation of pattern matching, but there is a different approach too (Below predicate) | 28/04 21:24 |

roconnor | glguy: need more ordinal operations! :D | 28/04 21:29 |

roconnor | glguy: like multiplication, exponentiation, Veblen functions! | 28/04 21:30 |

fax | would love to see programs that make (essential) use of these things too :) | 28/04 21:33 |

glguy | I don't know what roconnor is talking about but I can find out :) | 28/04 21:34 |

roconnor | glguy: you work for galois? | 28/04 21:34 |

glguy | I have a program that makes use of the inverse image w.f. relation | 28/04 21:34 |

glguy | roconnor, yeah, but we aren't all formal methods experts :) | 28/04 21:34 |

roconnor | who isn't? | 28/04 21:35 |

glguy | I'm not! | 28/04 21:35 |

fax | glguy, on the roads though ? | 28/04 21:35 |

roconnor | but you are writing agda code! | 28/04 21:35 |

glguy | I'm approaching Agda from the "is it a dependently-typed programming language?" side | 28/04 21:36 |

glguy | working my way into "Is it a proof-assistant based on intuitionistic type theory?" | 28/04 21:36 |

roconnor | same thing :) | 28/04 21:36 |

glguy | ¯\(°_0)/¯ | 28/04 21:36 |

fax | hheheheehe | 28/04 21:37 |

glguy | Working at Galois is great for having access to a number of people who can explain stuff to me as I need it | 28/04 21:37 |

glguy | I sit across from Iavor who fields most of my FM questions | 28/04 21:38 |

fax | glguy you should write this stuff down :P | 28/04 21:38 |

glguy | Yeah, I considered "blogging" some of my experiences, but I don't really know what level to approach it from | 28/04 21:39 |

fax | don't really know what level to approach it from | 28/04 21:39 |

fax | oops | 28/04 21:39 |

glguy | "Here is a round-about way to implement that tail recursive function in Agda that you've never had trouble implementing in any other language" :-D | 28/04 21:40 |

fax | lol | 28/04 21:40 |

fax | glguy: http://muaddibspace.blogspot.com/2009/03/how-to-halve-number.html | 28/04 21:40 |

glguy | Anonymous said... | 28/04 21:41 |

glguy | holy jesus wtf | 28/04 21:41 |

fax | :) | 28/04 21:41 |

dolio | Here's how to prove that tail recursive function is total in every other language. Oh wait, you can't do that. | 28/04 21:41 |

glguy | I also don't know what it obvious to the rest of people using Agda | 28/04 21:42 |

glguy | or if there is even an audience | 28/04 21:43 |

glguy | beyond say the 32 people in this channel | 28/04 21:43 |

copumpkin | wow | 28/04 21:44 |

copumpkin | you should use twitter more | 28/04 21:44 |

glguy | oh yeah? | 28/04 21:44 |

glguy | is Agda all over the Twitters? | 28/04 21:44 |

fax | is twitter evil or not?? | 28/04 21:44 |

fax | I haven't been able to figure it out | 28/04 21:44 |

copumpkin | glguy: not really :P | 28/04 21:45 |

copumpkin | fax: it's as evil as the people you use | 28/04 21:45 |

copumpkin | I mean | 28/04 21:45 |

copumpkin | actually I don't know what I meant | 28/04 21:45 |

copumpkin | there are lots of haskellers and mathy people on it, if nothing else | 28/04 21:45 |

glguy | maybe you meant that my twitter account is way out of date | 28/04 21:45 |

glguy | how do I publicly open a module in my module | 28/04 21:49 |

glguy | so that opening my module gives you things defined in the other module? | 28/04 21:49 |

dolio | open ... public | 28/04 21:50 |

glguy | I've shared this implementation before, but I wanted to show how it now uses the WF Operators module I'm working on http://www.galois.com/~emertens/treerec/treerec.html#2597 | 28/04 21:56 |

glguy | specifically "open InverseImage ..." | 28/04 21:56 |

fax | what does galois do? | 28/04 21:57 |

fax | actually the site will tell me | 28/04 21:57 |

glguy | yeah, the site will tell you better than I can | 28/04 21:58 |

glguy | I always stumble along as I figure out how much detail I'm allowed to go into | 28/04 21:58 |

fax | man cryptol is so cool | 28/04 21:58 |

glguy | fax, no argument here :) | 28/04 22:03 |

Adamant | fax: Twitter is potentially less evil that a lot of other 'social' sites | 28/04 22:11 |

copumpkin | omg more twitter love | 28/04 22:11 |

Adamant | for many common values of evil | 28/04 22:11 |

Adamant | copumpkin: no, I still hates it, mostly :P | 28/04 22:11 |

copumpkin | oh | 28/04 22:11 |

copumpkin | well, more twitter less-that-100%-hate then | 28/04 22:11 |

Adamant | copumpkin: but yeah, the mathy/haskell/general nerd feeds can be fun | 28/04 22:11 |

Adamant | and shitmydadsays is quality | 28/04 22:12 |

Adamant | I've unplugged from several of the driving-data-into-your-skull-constantly deals and I think I might have to plug back in | 28/04 22:12 |

copumpkin | like what? | 28/04 22:13 |

glguy | So what was that Velben function stuff? | 28/04 22:13 |

Adamant | dunno, mostly just tech news if nothing else | 28/04 22:13 |

fax | Veblen heirearchy | 28/04 22:13 |

Adamant | to re-plug into | 28/04 22:13 |

fax | I don't find tech very interesting but its nice seeing the quantum computing number of bits go up | 28/04 22:14 |

Adamant | copumpkin: I had a huge RSS reader feed. | 28/04 22:14 |

Adamant | but I burned out once I realized it would take about a hour a day to read everything as it came it | 28/04 22:14 |

Adamant | maybe more | 28/04 22:15 |

copumpkin | hah | 28/04 22:15 |

Adamant | I was going to switch to just reading it on the weekends | 28/04 22:15 |

Adamant | but then I just let it crash and burn | 28/04 22:15 |

Adamant | I'm gonna restrict it to a limited number of high quality sites and try again. | 28/04 22:16 |

Adamant | so. back on topic | 28/04 22:16 |

fax | yes has anyone figured out what agda is yet? :D | 28/04 22:16 |

Adamant | I'm behind on the 'learn at least one new language a year' resolution | 28/04 22:16 |

Adamant | one thing I'm gonna learn is OpenCL | 28/04 22:16 |

Adamant | I think Agda should be the other | 28/04 22:16 |

* fax doesn't beleive in learning programming languages | 28/04 22:16 | |

copumpkin | I don't think anyone knows yet | 28/04 22:17 |

Adamant | since i assume there are no books on Agda the language yet, what are the best resources for Agda and higher-level type theory like it uses? (I may need a remedial course in Haskell/ML-level type stuff) | 28/04 22:18 |

fax | there's a PhD on it | 28/04 22:19 |

fax | that's bookish | 28/04 22:19 |

copumpkin | the agda tutorial is pretty accessible | 28/04 22:19 |

Adamant | you mean a thesis | 28/04 22:19 |

fax | I don't tend to say thesis since it doesn't imply it's a PhD | 28/04 22:19 |

glguy | copumpkin: accessible with respect to which relation?? | 28/04 22:21 |

fax | lol | 28/04 22:21 |

copumpkin | :P | 28/04 22:21 |

Adamant | fax: a PhD on it sounds like a PhD is working on it, at least to me :P | 28/04 22:23 |

Adamant | also I don't care that much if something is a Master's thesis or a PhD thesis, as long as it is a good and useful thesis :P | 28/04 22:23 |

Adamant | but thanks folks, I went to the Wiki and got some stuff to read. | 28/04 22:24 |

Adamant | Agda wiki, not The Wiki | 28/04 22:24 |

--- Day changed Thu Apr 29 2010 | ||

glguy | go figure... proving that a value is accessible under the w.f. relation of the lexicographic product of two w.f. relations requires lexicographic induction | 29/04 01:29 |

glguy | http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25192#a25192 | 29/04 01:30 |

copumpkin | sounds hardcore | 29/04 01:38 |

Saizan | ah, i thought that meant you had to use well founded recursion to prove the accessibility. | 29/04 01:41 |

glguy_ | Any ideas for ways to structure allAcc so that the lexicographic induction can be found to terminate? | 29/04 03:15 |

glguy_ | woot, I did the proof for non-dependently typed pairs | 29/04 03:46 |

glguy_ | http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#2955 | 29/04 03:54 |

dolio | That requires the constituent relations to be well founded for all elements of the type? | 29/04 03:58 |

glguy_ | I don't know that it requires it | 29/04 03:59 |

glguy_ | but I decided to try to prove it first assuming that they were | 29/04 03:59 |

dolio | I'm pretty sure that's what allA and allB say. | 29/04 03:59 |

glguy_ | oh, it certainly is | 29/04 03:59 |

glguy_ | OK, rephrase: | 29/04 03:59 |

glguy_ | My proof requires that all inhabitants of the sets A and B are accessible wrt relations R1 and R2, respectively | 29/04 04:00 |

dolio | However, since you only use it at the top of allAcc, you can probably dispense with it and just assume that each element of the pair is accessible. | 29/04 04:00 |

glguy_ | I don't think I understand | 29/04 04:03 |

dolio | Perhaps it isn't possible to do away with the assumption that every element of B x is accessible. | 29/04 04:05 |

dolio | (Or B, as it were.) | 29/04 04:05 |

glguy_ | yeah... I'd love to generalize this to B x | 29/04 04:06 |

glguy_ | (as you can see in the odule above) | 29/04 04:06 |

dolio | Since for x < x', I can choose arbitrary y' > y, and (x' , y') \prec (x , y)... | 29/04 04:06 |

glguy_ | yeah, it is the same kind of arbitrary choice you have to deal with in the disjoint sum case | 29/04 04:07 |

dolio | But then one needs y' accessible for all the (x' , y'') < (x' , y'). | 29/04 04:07 |

glguy_ | when you move from inj2 to inj1 | 29/04 04:07 |

dolio | However, it shouldn't be required that all x : A are accessible. | 29/04 04:08 |

glguy_ | that is true | 29/04 04:08 |

glguy_ | so I could demand an Accessibility proof for your starting 'x' valu | 29/04 04:09 |

glguy_ | and use that to build the initial recursor-builder | 29/04 04:10 |

glguy_ | from the Some module | 29/04 04:10 |

dolio | I'm not sure how much that would come up in practice. | 29/04 04:13 |

dolio | But theoretically you can have relations for which not every element of the type is accessible. | 29/04 04:13 |

glguy_ | you can always just define a subset of your type that is accessible | 29/04 04:13 |

dolio | Something like '1 < 2 < 3 < 4 < 5 < ... < 10 < 9 < 8 < 7 < 6'. | 29/04 04:15 |

dolio | But that's pretty contrived. | 29/04 04:15 |

glguy_ | well... you're still free to pick your own insane relation | 29/04 04:16 |

glguy_ | and you can define it to leave elements that you'd have left out of the set to live on their own islands | 29/04 04:17 |

glguy_ | where nothing was related to them | 29/04 04:17 |

glguy_ | suggestions for proving Lexicographic.allAcc terminates? | 29/04 04:20 |

glguy_ | I figured it out | 29/04 08:17 |

glguy_ | http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#2236 | 29/04 08:17 |

glguy_ | The lexicographic product of two well-founded relations is well-founded (and it is time on Sigma A B rather than A x B) | 29/04 08:17 |

npouillard | glguy_: great | 29/04 08:33 |

glguy_ | and along the way i got a generalized Induction.Lexicographic module | 29/04 08:33 |

glguy_ | maybe some of this could go into the std lib | 29/04 08:34 |

npouillard | now you can add universe polymorphism | 29/04 08:34 |

glguy_ | almost done | 29/04 08:34 |

npouillard | glguy_: I hope so | 29/04 08:34 |

glguy_ | done | 29/04 08:34 |

glguy_ | uploaded | 29/04 08:34 |

glguy_ | (to the same link) | 29/04 08:34 |

npouillard | :) | 29/04 08:34 |

glguy_ | I think that the last module could be a little more level polymorphic in that A and B could have different levels | 29/04 08:35 |

glguy_ | however the code that I reused from Induction.Lexicographic assumed they were both at the same level | 29/04 08:35 |

glguy_ | and I don't know if that was necessary or not | 29/04 08:35 |

glguy_ | but it is the state of things | 29/04 08:35 |

npouillard | You should propose a patch to the stdlib | 29/04 08:37 |

glguy_ | How do I do that | 29/04 08:37 |

npouillard | would it make sense to add the Data.Star operator | 29/04 08:38 |

glguy_ | can't happen | 29/04 08:38 |

glguy_ | reflexive relations are right out | 29/04 08:38 |

npouillard | so obvious sorry | 29/04 08:38 |

glguy_ | I was thinking that it would, however, make sense to break the transitive closure operator out into a Data.Plus module | 29/04 08:39 |

glguy_ | rather than defining it locally here | 29/04 08:39 |

npouillard | Yep | 29/04 08:40 |

npouillard | I think there is already a definition like you DisjointSum._<_ | 29/04 08:40 |

npouillard | you*r* | 29/04 08:40 |

glguy_ | oh? | 29/04 08:41 |

glguy_ | just the operator, not the Acc proof? | 29/04 08:41 |

npouillard | sure | 29/04 08:41 |

npouillard | don't panic | 29/04 08:41 |

npouillard | :) | 29/04 08:41 |

glguy_ | it would be OK if this work was all already done | 29/04 08:41 |

glguy_ | I've had a blast working my way through it | 29/04 08:41 |

npouillard | Relation.Binary.Sum | 29/04 08:42 |

glguy_ | I'd have to make it level polymorphic | 29/04 08:44 |

glguy_ | but good catch! | 29/04 08:44 |

npouillard | glguy_: sure but would a nice first addition | 29/04 08:45 |

pigworker | Did you see the "Induction" section of the std lib? Is it a useful starting point? (I'm biased, of course.) | 29/04 08:45 |

glguy_ | I've tried to build off of the stuff in Induction where possible | 29/04 08:50 |

glguy_ | or use it via Induction.Lexicographic | 29/04 08:50 |

glguy_ | Reading through the Induction namespace, starting at that module, was quite valuable (especially the examples) for learning how to do this stuff | 29/04 08:51 |

glguy_ | (Does that mean you are the author of these modules?) | 29/04 08:52 |

fax | 14:19 < edwardk> proving false in agda is the purpose of agda, it is the game of oneupsmanship that defines that community ;) | 29/04 15:32 |

Saizan | how would the type of that proof look like? | 29/04 15:35 |

npouillard | Saizan: ⊥ | 29/04 15:36 |

Saizan | ah, sorry, i was referring to another quote :D | 29/04 15:37 |

npouillard | :) | 29/04 15:37 |

Saizan | dolio : The best proof of the inconsistency of Agda would probably be a proof of the consistency of Agda in Agda. Someone should | 29/04 15:37 |

Saizan | work on that. | 29/04 15:37 |

npouillard | hum | 29/04 15:37 |

* npouillard guessing | 29/04 15:38 | |

npouillard | ∀ (A : `Set`) → Dec (Σ `Term` λ p → ⊢ ⟦ p ⟧t ∷ ⟦ A ⟧s) | 29/04 15:41 |

npouillard | `Set` would be the type of Set descriptions, same thing for `Term` | 29/04 15:42 |

npouillard | ⟦_⟧t and ⟦_⟧s interpret set and terms | 29/04 15:43 |

Saizan | shouldn't the term be an argument as well? | 29/04 15:43 |

npouillard | and ⊢_∷_ would be a typing-derivation type | 29/04 15:43 |

Saizan | otherwise that decides if a type is inhabited or not, which seems quite strong | 29/04 15:44 |

npouillard | I don't think so, it would be much weaker and only telling you that the type checking is decidable | 29/04 15:44 |

Saizan | oh, i guess i get to prove that you can't give proofs of empty types with that | 29/04 15:45 |

npouillard | "that": which one | 29/04 15:46 |

npouillard | ? | 29/04 15:46 |

Saizan | yours | 29/04 15:46 |

npouillard | yes | 29/04 15:46 |

npouillard | maybe we can just focus one this: | 29/04 15:47 |

npouillard | ¬ (∃ λ p → ⊢ ⟦ p ⟧t ∷ `⊥`) | 29/04 15:48 |

npouillard | update of the previous one: ∀ (A : `Set`) → Dec (Σ `Term` λ p → ⊢ p ∷ A) | 29/04 15:48 |

Saizan | i see | 29/04 15:49 |

npouillard | and so: ¬ (∃ λ p → ⊢ p ∷ `⊥`) | 29/04 15:49 |

dolio | Saizan: It would involve creating some type that could be used to reason about Agda terms, Goedel style (only easier, since inductive datatypes/families are nicer than encoding things as integers), and proving that there are no terms that prove false in that model, essentially. | 29/04 15:51 |

npouillard | dolio: this would just say that agda is stronger the embedded theory, no ? | 29/04 15:52 |

dolio | The intention would that the embedded theory would be Agda. | 29/04 15:53 |

dolio | Similar to embedding Peano arithmetic in itself. | 29/04 15:53 |

dolio | And since Agda contains Peano arithmetic, it should be impossible to show that Agda is consistent in itself unless it is inconsistent. | 29/04 15:54 |

dolio | Unless I'm misunderstanding something. | 29/04 15:54 |

npouillard | I think we can't avoid reasoning about agda terms without proving something weaker than the consistency of Agda | 29/04 15:56 |

ccasin | where is Agda's universe polymorphism documented? | 29/04 16:27 |

ccasin | In particular, I am mystefied by the following: (\ l -> Set l) has type (l : Level) -> Set (suc l) | 29/04 16:28 |

ccasin | but Set itself does not | 29/04 16:28 |

ccasin | So, is Set a function on levels or isn't it? | 29/04 16:28 |

ccasin | *mystified | 29/04 16:29 |

fax | probably the source code (if you can read it... it's pretty confusing) | 29/04 16:29 |

dolio | ccasin: Even with universe polymorphism enabled, the token Set refers to Set 0. | 29/04 16:39 |

dolio | Kind of an oddity. | 29/04 16:39 |

ccasin | dolio: yeah, it's a little odd, but I guess I figured that | 29/04 16:40 |

ccasin | I just sent a message to the list on this topic | 29/04 16:40 |

dolio | I should say, the token Set when not applied to another term refers ... | 29/04 16:40 |

dolio | So I guess it's kind of context-sensitive. | 29/04 16:40 |

ccasin | Agda's approach to universe polymorphism seems to be pretty unique - it would be nice to see it explicitly written out somewhere | 29/04 16:40 |

ccasin | even for a much smaller system | 29/04 16:40 |

dolio | Yes, it's unlike stuff I've seen elsewhere in the literature. | 29/04 16:41 |

ccasin | well, where "pretty unique" means "new to me" :) | 29/04 16:41 |

dolio | I wrote a small interpreter for a language with similar universe polymorphism. | 29/04 16:41 |

ccasin | that's just what I'm doing :) | 29/04 16:41 |

dolio | But I don't think I documented it any more than Agda's is. | 29/04 16:42 |

ccasin | I can't believe they pay me to sit around and write little interpreters | 29/04 16:42 |

ccasin | being a grad student is swell | 29/04 16:42 |

dolio | http://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs | 29/04 16:42 |

dolio | You might be able to glean the rules from that, though. | 29/04 16:42 |

dolio | It's pretty simple. | 29/04 16:42 |

ccasin | thanks, I'll have a look | 29/04 16:43 |

dolio | The sigma types in there are a little more powerful than what you can do in Agda. | 29/04 16:43 |

ccasin | this is interesting | 29/04 16:44 |

ccasin | it looks like, in your language "Type" doesn't have a type itself | 29/04 16:44 |

ccasin | it must always be applied to a level | 29/04 16:44 |

dolio | Because you can't write something like "data Foo : Set \omega where foo : (l : Level) -> <something with type Set l> -> Foo". | 29/04 16:44 |

ccasin | or maybe I'm reading the haskell wrong | 29/04 16:45 |

ccasin | oh, and you add an omega level, that's nice | 29/04 16:45 |

dolio | No, that's correct. Just like fst and snd aren't first-class. | 29/04 16:45 |

ccasin | I think agda doesn't have that, right? | 29/04 16:45 |

ccasin | cool | 29/04 16:46 |

dolio | It might be fundamental for Type, though. I haven't really thought about it. | 29/04 16:46 |

dolio | Type : (l : Level) -> Type (suc l) would be kind of weird, at least. | 29/04 16:47 |

ccasin | that's what I'm doing in my little interpreter | 29/04 16:47 |

ccasin | of course, who knows if it's sound | 29/04 16:47 |

dolio | I wouldn't necessarily worry about it being less sound. More getting into a type-checking loop. | 29/04 16:48 |

dolio | You can write \l -> Type[l] in my interpreter, for instance. | 29/04 16:48 |

ccasin | really I would like to skip universe polymorphism all together. But I can't figure out what type the eliminators for datatypes should have if I can't quantify over levels | 29/04 16:49 |

fax | that's cool | 29/04 16:49 |

ccasin | so, ulf responded on the mailing list - looks like agda does the same thing as your interpreter | 29/04 16:50 |

dolio | Yeah. | 29/04 16:51 |

dolio | -> isn't a first-class operator in Agda, either. | 29/04 16:51 |

dolio | Unlike Haskell. | 29/04 16:51 |

fax | it's odd that | 29/04 16:51 |

dolio | Anyhow, my interpreter has a lot of special cases like that because it's a little easier to structure the syntax that way. I don't think you fundamentally need to do that in a lot of the cases I do, though. | 29/04 16:54 |

ccasin | dolio: what will lead to a looping type checker with the (l : Level) -> Type (suc l) choice? | 29/04 16:54 |

dolio | ccasin: To check the type of Type, you check the type of (l : Level) -> Type (suc l), so check the type of App Type (suc l), so check the type of Type. | 29/04 16:55 |

dolio | I haven't thought a lot about it, though. It might be fine. | 29/04 16:55 |

ccasin | hmm, why do I need to check the type of (l : Level) -> Type (suc l)? | 29/04 16:56 |

ccasin | I think I just return that | 29/04 16:56 |

ccasin | that is, my system has as an axiom: | 29/04 16:56 |

ccasin | ---------------------------- | 29/04 16:56 |

ccasin | Type : (l : Level) -> Type (suc l) | 29/04 16:56 |

dolio | It may well be fine. | 29/04 16:57 |

dolio | It's not like I've tried it and had loops. | 29/04 16:57 |

ccasin | OK, cool | 29/04 16:57 |

fax | Type : (l : Level) -> Type (suc l) -- doesn't make sense to me | 29/04 16:58 |

fax | well okay I guess it's fine it looks weird | 29/04 16:58 |

ccasin | well, we seem to agree (Type l : Type (suc l)) | 29/04 16:58 |

dolio | Oh, another difference between my interpreter and Agda's situation is that my Level is a built-in type with no eliminator, but Agda's Level is an ordinary inductive type. | 29/04 17:00 |

dolio | So you can actually do case analysis on the level of your function in Agda. | 29/04 17:00 |

dolio | foo : (l : Level) -> Set l ; foo zero = Nat ; foo (suc l) = Set l | 29/04 17:01 |

ccasin | yeah, in my little interpreter I'm just building in Nats with the standard eliminator and using them for levels | 29/04 17:02 |

dolio | Which isn't exactly 'polymorphism' in the parametricity sense. | 29/04 17:02 |

ccasin | right - it's not at all | 29/04 17:02 |

ccasin | this system seems to solve a lot of the same problems as the Harper-Pollack universe polymorphism stuff | 29/04 17:03 |

ccasin | but it's very different | 29/04 17:03 |

ccasin | and cool! | 29/04 17:03 |

dolio | However, you can eliminate into Level in my theory, so you could probably write "foo : (n : Nat) -> Set (toLevel n)", which isn't very different. | 29/04 17:03 |

fax | wasn't the Harper-Pollack thing about how to infer the levels? | 29/04 17:04 |

fax | oh right, I think I know what the problems were | 29/04 17:04 |

* dolio goes to get some lunch. | 29/04 17:05 | |

ccasin | fax: well, it's partially about how to infer the levels, but also partially about a new type of ambiguous level that could be used for polymorphism | 29/04 17:05 |

ccasin | it's just what coq has, I think | 29/04 17:05 |

fax | okay | 29/04 17:05 |

ccasin | in that paper, l := n | \alpha | 29/04 17:06 |

ccasin | where \alpha means "I don't know, pick something" | 29/04 17:06 |

glguy | fax: I finished the accessability proof for lexicographic product last night http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#2297 | 29/04 17:16 |

glguy | (you told me about the paper, you get to hear about the progress) | 29/04 17:17 |

glguy | Had to extend Induction.Lexicographic to do dependently-typed lexicographic induction | 29/04 17:18 |

fax | eek | 29/04 17:18 |

fax | I never dared to think about the dependently-typed ones | 29/04 17:18 |

glguy | it was a pretty straight forward change, actually | 29/04 17:19 |

fax | Lexicographic exponentiation is a really cool one | 29/04 17:19 |

fax | glguy, the main thing which is missing is examples -- but I think examples are really difficult to come up with | 29/04 17:19 |

glguy | I've used lexicographic induction before, I'm going to have to see about extending that example to make use of the extra freedom you get with lexicographic product of well-founded relations | 29/04 17:20 |

fax | oh cool what was it for ? | 29/04 17:20 |

fax | I know a proof of beta reduciton for STLC using a > b \/ (a = b /\ p < q) but that's not really lexicographic because it's always n=2 | 29/04 17:21 |

glguy | I used it to write merge sort | 29/04 17:22 |

glguy | (kind of the obvious one) | 29/04 17:22 |

fax | hm | 29/04 17:22 |

fax | that sounds like something that would be done with a measure ? | 29/04 17:22 |

glguy | You could probably also have done measure of the sum of the lengths of the two lists | 29/04 17:23 |

glguy | but it was pretty straight forward to do it lexicographically | 29/04 17:23 |

glguy | http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25208#a25208 | 29/04 17:24 |

fax | I can't imagine how :/ | 29/04 17:24 |

* glguy ^W'd the wrong application | 29/04 17:24 | |

glguy | Yay, the lexicographic and well-founded operators got added to the std lib darcs repo | 29/04 20:23 |

fax | wow cool! | 29/04 20:27 |

fax | that is good did you cite that paper in yrou code | 29/04 20:28 |

fax | ? | 29/04 20:28 |

glguy | What is Nils' nick | 29/04 20:28 |

glguy | No, but Nils did | 29/04 20:28 |

fax | I don't think Nils' is here | 29/04 20:28 |

glguy | "Yesterday I added some functions to Induction.WellFounded, following the | 29/04 20:28 |

glguy | discussion you and fax had" | 29/04 20:28 |

fax | eek | 29/04 20:28 |

glguy | <_< | 29/04 20:29 |

glguy | >_> | 29/04 20:29 |

fax | I should watch my mouth if people like Nils are reading | 29/04 20:29 |

glguy | he could be anywhere! | 29/04 20:29 |

fax | I say too much stupid stuff :p | 29/04 20:29 |

glguy | now I have to install ghc-6.12 | 29/04 20:34 |

glguy | (so I can install development Agda, so I can use the development library) | 29/04 20:35 |

dolio | Oh, that reminds me. c.h.o is back up, so I can pull agda. | 29/04 20:36 |

dolio | Oh, but nothing particularly interesting happened, apparently. | 29/04 20:36 |

fax | no quotients yet/ | 29/04 20:37 |

fax | ? | 29/04 20:37 |

glguy | So what are quotients? | 29/04 20:37 |

dolio | You take a type, and identify various elements according to an equivalence relation to get a new type. | 29/04 20:37 |

glguy | Is there a simple example? | 29/04 20:39 |

dolio | Z = N x N / (\(l, r) (l', r') -> l + r' == r + l') | 29/04 20:39 |

dolio | Assuming I got that right. | 29/04 20:40 |

glguy | and the identified elements are included or excluded? | 29/04 20:40 |

dolio | The identified elements are indistinguishable from one another. | 29/04 20:40 |

dolio | (1, 0) == (2, 1) : Z | 29/04 20:42 |

fax | so proving that equation woud not be reflexivity | 29/04 20:42 |

fax | it would be like quotientEqual (reflexivity) | 29/04 20:43 |

fax | or so ... | 29/04 20:43 |

fax | ? | 29/04 20:43 |

dolio | I don't know how you'd add quotients to something Agda-like. | 29/04 20:45 |

* glguy finds out that Data.Function -> Function | 29/04 20:46 | |

dolio | I need to figure out a better way to get the html for my Agda stuff on code.haskell.org. | 29/04 20:49 |

dolio | darcs is too risky. | 29/04 20:49 |

glguy | scp! | 29/04 20:49 |

dolio | I guess I can do that. | 29/04 20:49 |

glguy | That's how I publish my html, at least | 29/04 20:49 |

dolio | That was less painful than I expected. | 29/04 20:54 |

--- Day changed Fri Apr 30 2010 | ||

glguy | Do people bother trying to get their Agda source files to stay within 80 characters? | 30/04 20:48 |

glguy | If not is there a common standard? | 30/04 20:48 |

dolio | I generally don't mind going a little beyond 80. | 30/04 20:52 |

dolio | It can be difficult to fit a lot of proofs in 80. | 30/04 20:53 |

dolio | I probably keep it under 100 usually, though. | 30/04 20:54 |

glguy | I like being able to print them out on letter paper | 30/04 20:56 |

glguy | Agda’s colored HTML output looks great with a laser print on heavy paper | 30/04 20:57 |

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