glguy_ glguy_ glguy_ --- Log opened Thu Apr 01 00:00:57 2010 What's going on with #archlinux? 01/04 06:50 rather, why are we redirecting people to archlinux backwards? 01/04 06:51 Oh, is it April 1st somewhere? 01/04 06:52 I think US PST is the next to get April Fool'ed. 01/04 06:57 Oh, sorry. I sent that to the wrong channel 01/04 06:58 --- Day changed Fri Apr 02 2010 how do you get the agda console so you can test an expression? 02/04 10:32 crc__, agda -I 02/04 10:40 is that inside of emacs? 02/04 10:53 btw im a vim user 02/04 10:54 No, on the shell. But it says that the interactive mode is not supported anymore. 02/04 10:54 ok thanks 02/04 10:58 ill ask the lecturer after the break 02/04 10:58 if your in emacs you can also enter c-c c-n to evaluate expressions 02/04 10:59 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 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 C-c C-n for ‘normalise’. 02/04 11:08 Though, thinking about it, I don't recall ever having to use that… 02/04 11:09 liyang: that was the one I was looking for, thanks 02/04 11:18 what does it mean if you get something along the lines of Set !=< _65 -> Set _66 of type Set1 02/04 11:57 Looks like it's expecting something of _65 -> Set _66 where you've given it something of Set. 02/04 11:59 sorry, what is a set _65 02/04 12:00 the _N things are freshly generated variables 02/04 12:00 and Set can take a parameter which is the universe 02/04 12:01 basically that error means that you're giving it a Set where it expects a function returning a Set 02/04 12:01 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 it also removes quite a bit of duplication :) 02/04 12:08 --- Day changed Sat Apr 03 2010 does agda have bottom? (_|_ or ⊥ or whatever) 03/04 00:23 what do you mean 03/04 00:23 Is there some value which is in all other agda types? (like undefined in haskell) 03/04 00:24 no 03/04 00:25 you can turn off termination checker and define it if you want 03/04 00:25 no no, I'm fine 03/04 00:26 the standard library is no match for Haskell's, though... 03/04 00:27 The standard library has a bottom and a casting function _|_-elim to whatever type you'd like 03/04 00:31 In Data.Empty 03/04 00:31 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever 03/04 00:31 ⊥-elim () 03/04 00:31 that's a bottom type though 03/04 00:32 but i guess if you get a value of that type you're done :) 03/04 00:32 if you just need a placeholder you should put a "?" in there 03/04 00:32 or postulate something 03/04 00:32 * Mathnerd314 is confused 03/04 00:34 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 if you /had/ a value of ⊥ you could make it whatever you wanted :) 03/04 00:37 if a context where you've assumed contradictory facts you can make one, but only there :) 03/04 00:38 s/if/in/ 03/04 00:38 The standard library has: 03/04 00:38 trustMe : {A : Set}{a b : A} → a ≡ b 03/04 00:38 trustMe = primTrustMe 03/04 00:38 * fax hates that stuff 03/04 00:40 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 I'm using Data.Sum and Relation.Binary.PropositionalEquality. 03/04 15:32 *the* constructor for a union? 03/04 15:33 well i match for the two constructors for the \u+ union function 03/04 15:33 i think there are two, inj\_1 and inj\_2 03/04 15:34 Paste? http://moonpatio.com/fastcgi/hpaste.fcgi/new What's the complaint? 03/04 15:34 sec 03/04 15:35 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a9247 03/04 15:35 that usually happens when both sides of the equality are compound expressions 03/04 15:35 ah, no 03/04 15:36 im new to this stuff so im probably making a basic mistake 03/04 15:36 did that code and error message make any sense? 03/04 15:37 wpk_: what happens if you delete the {n} part? 03/04 15:37 http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a9248 03/04 15:38 (same error) 03/04 15:38 ah, you didn't update the code though 03/04 15:39 i did in emacs, im just really tired heh 03/04 15:39 heh 03/04 15:39 the new error is the first one 03/04 15:39 they appear similar 03/04 15:40 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 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 i'm not really sure how/if you're supposed to be able to pattern match on refl there 03/04 15:42 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 hmm 03/04 15:42 you could post on the mailing list 03/04 15:43 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 however you can still use that equality proof without pattern matching on it 03/04 15:43 instead of refl there, name it ‘A’ and write inj\_1 (cong (suc \o suc) A) on the RHS. 03/04 15:45 suc \o suc means suc(suc())? 03/04 15:46 sorry im a complete newbie 03/04 15:46 open import Function :3 03/04 15:46 Function composition, yes. 03/04 15:46 apparently my installation of agda2 doesnt have Function.agda? 03/04 15:48 did you install the standard library? 03/04 15:49 Oh er, Data.Function then. Or just write \lambda x \-> suc (suc x) 03/04 15:49 however you can write a simple lambda here 03/04 15:49 Saizan: there's been some renaming going on lately in the stdlib. 03/04 15:49 true 03/04 15:49 Data.Function works 03/04 15:49 :D 03/04 15:50 thanks so much guys 03/04 15:52 which file is cong in so I can look at it? 03/04 15:52 Relation.Binary.Core probably. 03/04 15:53 in emacs, move your cursor over it and press M-. 03/04 15:53 If things type-check, you can cursor over the identifier and meta-. 03/04 15:53 (yes.) 03/04 15:53 i never knew that that's cool 03/04 15:55 Is it coursework? (Whose course, out of interest?) 03/04 15:56 Manuel Chakravartay (sp?) at UNSW, Australia. 03/04 15:57 *nod* 03/04 15:57 course is some SEng core forget the name 03/04 15:57 Thought so. :) He sometimes hangs out here as TacticalGrace. 03/04 15:58 haha ill remember that 03/04 15:59 (So that's Nottingham, Swansea, and UNSW now…) 03/04 15:59 where Manuel has taught agda? 03/04 15:59 Where Agda has been used in teaching, that I'm aware of. 03/04 16:00 oh 03/04 16:01 I'm sure there's more though—I haven't really being paying that much attention. 03/04 16:02 a good 80% of the students are totally lost on this I think 03/04 16:03 That's probably expected. You'll get an intuition for it eventually. :3 03/04 16:07 liyang: I've used it in teaching, too (at UU) 03/04 16:27 :D 03/04 16:34 kosmikus, UU? 03/04 16:34 What's the confusion percentage like? 03/04 16:34 Amadiro: Utrecht 03/04 16:35 Ah. 03/04 16:35 http://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/models/Desc.agda 03/04 20:30 cool 03/04 20:30 118 proof-map-id : (D : Desc)(X : Set)(v : [| D |] X) -> map D X X (\x -> x) v == v 03/04 20:30 125 proof-map-compos : (D : Desc)(X Y Z : Set) 03/04 20:30 126 (f : X -> Y)(g : Y -> Z) 03/04 20:30 127 (v : [| D |] X) -> 03/04 20:30 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 isn't generic programming fun! 03/04 20:37 what's this from? 03/04 20:39 that agda file I linked XD 03/04 20:40 here's a paper on it http://personal.cis.strath.ac.uk/~dagand/levitation.pdf 03/04 20:40 from the date, I guess this is an icfp submission? 03/04 20:41 oh my, from the abstract this looks really cool 03/04 20:42 yeah it's nice stuff 03/04 20:43 I think it's a continuation of Peter Morris' thesis 03/04 20:43 in some ways at least 03/04 20:43 this is such a good idea 03/04 20:46 I can tell because I'm jealous I didn't have it :) 03/04 20:47 ditto hehe 03/04 20:47 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 yes, I am anxious to see exactly how they pull this off 03/04 20:49 but I suppose I have to read the pages in order 03/04 20:50 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 :) 03/04 20:51 happily, I think I have enough background 03/04 20:51 Desc as described above doesn't handle mutually recursive datatypes though 03/04 20:51 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 that's just because of the number of times I reinstalled it 03/04 22:06 :p 03/04 22:06 this is interesting, but a little odd 03/04 23:19 is agda actually classified as an application? 03/04 23:19 most people interact with it through emacs, which just loads the agda libraries into ghci, right? 03/04 23:20 its cabal file calls it a library 03/04 23:21 but maybe these are just classifications he made up 03/04 23:21 there's an agda-executable package which gives you an executable 03/04 23:25 otherwise it's a library used by ghci in the emacs mode 03/04 23:25 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 oh, i think i miss some context 03/04 23:26 liyang had linked to this: 03/04 23:27 http://donsbot.wordpress.com/2010/04/03/the-haskell-platform-q1-2010-report/ 03/04 23:27 where agda is listed as the 13th most cabal-installed haskell application 03/04 23:27 in the last quarter 03/04 23:27 (as opposed to library) 03/04 23:27 i think it counts as an application because of the agda-mode executable 03/04 23:28 yes, this is a reasonable theory 03/04 23:28 I just wonder how he made these choices 03/04 23:29 (not for any particular reason) 03/04 23:29 --- Day changed Sun Apr 04 2010 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 the pattern {0} p a b is rejected by agda.. 04/04 09:15 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 wpk_: are you really using = there or \== ? 04/04 13:37 hellos 04/04 13:38 hi 04/04 13:38 taught yourself to levitate yet? 04/04 13:40 I think so 04/04 13:41 :-) 04/04 13:41 5 04/04 17:05 sorry, I take that back 04/04 17:05 38 people, yet complete silence :-(. 04/04 17:06 glguy: are you still playing with category theory? 04/04 17:07 I tried to implement category theory in Coq but it didn't go well 04/04 17:07 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 yes 04/04 17:08 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 you run into situations where you need existential equality? 04/04 17:10 what's existential equality? 04/04 17:10 forall x. f x = g x -> f = g 04/04 17:11 oh 04/04 17:11 wwhy do you say that? It seems very plausible 04/04 17:11 well you can't prove that statement inside agda? 04/04 17:12 I'm not sure 04/04 17:12 I think we can prove (\x -> f x) = (\x -> g x) <-> f = g 04/04 17:13 yes you are right, this is weaker than the forall x. we can't prove that in agda 04/04 17:13 i only ran into that problem with equality, what problem were you refering to? 04/04 17:14 huh? 04/04 17:17 stevan: you meant extensional? 04/04 17:17 probably :-) 04/04 17:17 fax: you said it fell part when you started wondering what equals means? 04/04 17:18 yeah 04/04 17:18 you have to get all this typeclass stuff out to make sets with equivalence relations and equivalence preserving morphisms 04/04 17:18 it works but it's really complicated 04/04 17:19 if we could just form types T/~, I think it would be much easier and everything would work perfectly 04/04 17:19 (but experience tells me that does not happen :) and there are unforseen problems) 04/04 17:19 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 yeah 04/04 17:20 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 i defined a cofree comonad thing :) 04/04 17:21 wow cool I wanna see 04/04 17:21 did you write that in haskell? 04/04 17:21 what's wrong with just using propositional equality for CT btw? 04/04 17:23 (i need to read up on quotients) 04/04 17:23 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24653 <- 04/04 17:24 cool Saizan 04/04 17:24 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 so cofree means basically free except greatest fixed point? 04/04 17:24 or, i could try at least :) 04/04 17:24 i'm not so sure what cofree means by itself, but it sounds something like that 04/04 17:25 though i'm pretty comfortable with the "cofree comonad" construction 04/04 17:27 stevan - if you try to form the category of categories then when are two functors between categories equal? 04/04 17:28 if you use propositional equality ... is that right/ 04/04 17:28 maybe the thing to do would be define category as a feature... 04/04 17:30 then implement all of modern mathematics in that 04/04 17:31 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 that was just my thinking which led me to give up 04/04 17:35 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 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 the reason I wanted categories is to define term algebras 04/04 17:39 that stuff would probably have worked but I didn't want to build a wall around myself 04/04 17:40 stevan definitions in ada ? 04/04 17:42 agda* 04/04 17:42 yes, records for what a category is, functors, etc 04/04 17:43 cool can I see 04/04 17:43 hmmmm I need to install agda :/ 04/04 17:43 http://web.student.chalmers.se/~stevan/ctfp/html/README.html 04/04 17:44 i wouldn't trust them to be right tho, i'm a CT noob. :-) 04/04 17:45 I've only started to study it recently (Because of dolio ;p) 04/04 17:45 i think it helps to code, give you something concrete... 04/04 17:46 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 oh, i'm surely not there yet. could you give an example? 04/04 17:49 stevan, say you defined the category of bijective functions between finite sets 04/04 17:49 oh 04/04 17:49 that's not an example 04/04 17:49 this is regarding the problem of equality 04/04 17:49 I think we can have lots of different permutation functions which are extensionally equal but not identical in agda 04/04 17:50 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 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 hmm 04/04 17:51 stevan ou know about Computational Category Theory? (the book is online) 04/04 17:52 there's lots of programs in there (which I wanted to implement.. but I got stuck) 04/04 17:52 by burstall and rydesomething? 04/04 17:53 yes 04/04 17:53 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 yeah but I mean that's just the SML code 04/04 17:54 yeah, true 04/04 17:55 the programs should work in a dependently typed setting, except with strong specifications 04/04 17:55 (at least I hope so!) 04/04 17:55 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 what sort of stuff do you want to program? what foundational stuff? 04/04 19:59 foundational stuff being category theory 04/04 20:00 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 what sort of maths? 04/04 20:02 like everything 04/04 20:03 calculating things, solving equations 04/04 20:04 have you read about the formath project? 04/04 20:04 yeah 04/04 20:05 that sort of stuff? 04/04 20:05 yes 04/04 20:05 in the coq standard library there are stuff like decidibility of primality and they don't even compute :/ 04/04 20:05 and they have trichotomoy as an axiom on the real numbers 04/04 20:06 it's pretty stupid 04/04 20:06 i know next to nothing about coq. what about that corn thing? don't they do it propertly? 04/04 20:07 yeah corn is cool 04/04 20:07 does corn have a better solution for reals than the standard lib? 04/04 20:16 yes 04/04 20:18 that's roconnors stuff it's way cool 04/04 20:18 why doesn't it replace the std lib stuff then? 04/04 20:20 --- Day changed Mon Apr 05 2010 Anyone here? 05/04 06:57 --- Day changed Tue Apr 06 2010 hello 06/04 09:17 i wonder how many people are trying to prove the peano axioms in agda on this channel 06/04 09:18 hello? 06/04 09:21 does anybody know anything about agda here? 06/04 10:00 hello? 06/04 10:17 can anybody help me out with agda 06/04 10:18 im trying to figure out how to prove the peano axioms 06/04 10:18 vlad__: ok, so what exactly are you trying to do? 06/04 10:18 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 but i dont think im putting the syntax right 06/04 10:20 you get a syntax error? 06/04 10:20 well my definition shoudl return suc m \equiv suc n then m \equiv n 06/04 10:20 and i have PA4 {m} {n} = refl suc m \equiv suc n -> m \equiv n 06/04 10:21 any ideas kosmikus? 06/04 10:21 is this a homework assignment? 06/04 10:21 it is 06/04 10:22 is the original assignment online? 06/04 10:22 yap 06/04 10:22 where? 06/04 10:22 i dont think you can access it, you have to log on 06/04 10:22 the gist of it is i have to prove some peano axioms 06/04 10:22 i have the right idea about doing it 06/04 10:23 just cant seem to get the syntax right in agda 06/04 10:23 it looks like what you're writing should be the *type* of PA4 06/04 10:23 right 06/04 10:24 the type is  suc m \equiv suc n -> m \equiv n 06/04 10:24 yes, so then you should write: 06/04 10:25 PA4 : \forall {m n} -> suc m \equiv suc n -> m \equiv n 06/04 10:26 something like that 06/04 10:26 thats the type i have that 06/04 10:27 no for all tho 06/04 10:27 just {m n : \nat} -> suc m \equiv \suc n -> m \equiv n 06/04 10:27 my problem is the application 06/04 10:28 i think i have to use the reflexive proof  but im not sure how to provide the arguments right 06/04 10:28 kosmikus: you can easily access the assignment at https://wiki.cse.unsw.edu.au/cs3141/10s1/Assignment%201 06/04 10:29 TacticalGrace: ah :) if you're here, then you can probably decide better what to tell or not to tell :) 06/04 10:29 really? i think u have to log in 06/04 10:29 i wasnt aware u can access it, in any case i always log in 06/04 10:30 I can access it. 06/04 10:30 ok cool 06/04 10:31 do you reken you can help me out then? 06/04 10:31 well, the solution is quite simple, so I don't want to just give it 06/04 10:32 if you have the type, you have to think about how you can construct a value of the type 06/04 10:32 i know its simple, its frustrating 06/04 10:32 you have to provide a function from an equality to an equality 06/04 10:32 yap, aint that simple , but iv tried returning that type and it doesnt like it 06/04 10:32 so you can start with 06/04 10:32 PA4 proof = ? 06/04 10:32 i start with PA4 {m} {n} = ? 06/04 10:33 is that right? 06/04 10:33 that's also ok 06/04 10:33 but then ? is of function type, right? 06/04 10:33 so, a good general tactic is to introduce an argument if you have to produce a function 06/04 10:34 so you either put it on the lhs: 06/04 10:34 PA4 {m} {n} proof = ? 06/04 10:34 or you use a lambda abstraction: 06/04 10:34 PA4 {m} {n} = \ proof -> ? 06/04 10:34 the former is probably better 06/04 10:34 what do you mean by = \ proof -> ? i thought the proof came after the equal and thats it? 06/04 10:35 oh 06/04 10:35 proofs can have structure. that's the whole point. 06/04 10:38 i have PA4 {m} {n} = suc m \equiv suc n -> refl m \equiv n ? 06/04 10:38 no, now you're writing a type again 06/04 10:41 but you have to give an implementation of that type 06/04 10:41 should i be using refl as proof? 06/04 10:41 or cong? 06/04 10:41 im soo confused 06/04 10:43 so am i! 06/04 10:44 do you know much about agda stevan? 06/04 10:44 a bit. 06/04 10:45 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 right 06/04 10:46 im just not sure how to construct this function 06/04 10:46 vlad__: you should really try to construct the proof systematically 06/04 10:46 how many arguments does refl take in? 06/04 10:46 vlad__: you've probably learned that in a lecture, right? 06/04 10:46 refl doesn't take any explicit arguments 06/04 10:46 ok, i just dont understand how to use refl 06/04 10:46 refl is the constructor of the equality type 06/04 10:47 have you been able to prove any of the other axioms? 06/04 10:47 only the first 3 06/04 10:48 perhaps, if you do symmetry and transitivity first, this one will become clearer 06/04 10:48 im really not good at math or agda, i dont understand what you mean by symetry and transitivity 06/04 10:48 as in i dont get how i prove that 06/04 10:48 TacticalGrace: nice assignment, btw 06/04 10:49 vlad__: PA6 and PA7 06/04 10:49 vlad__: sorry, I was assuming that you've read the assignment 06/04 10:49 lol 06/04 10:50 im taking it one at a time 06/04 10:50 oh right , you think it would be easier to do 6 and 7 first? 06/04 10:50 well, they have all one-line solutions 06/04 10:52 but if you have trouble doing one, it may be easier to do one of the others first 06/04 10:52 it may also be helpful to look at notes/slides from the lecture if there are any 06/04 10:53 kosmikus: thanks :) 06/04 10:53 thats prob a good strategy 06/04 10:54 the assignments says that propositional equality has been introduced there 06/04 10:54 so you've probably already seen how it can be used 06/04 10:54 yap i have , il re-read though it 06/04 10:54 TacticalGrace: and good to see you're also trying to use Agda in teaching 06/04 10:54 TacticalGrace: what kind of course is this? I can't seem to access the course's main page. 06/04 10:54 kosmikus: It's http://www.cse.unsw.edu.au/~cs3141/ 06/04 10:55 TacticalGrace: ah, I've done http://www.cs.uu.nl/wiki/DTP a while ago 06/04 10:56 It's a fairly big class actually 06/04 10:56 68 student 06/04 10:56 TacticalGrace: and I'm currently having two lectures of Agda at the end of "Advanced Functional Programming" 06/04 10:56 TacticalGrace: always fantastic that you get so many students. these are numbers we can only dream of. 06/04 10:57 the class is part of the compulsory SE cources for SE program studends and CS program students 06/04 10:59 which is part of the challenges 06/04 10:59 se rules 06/04 10:59 go se 06/04 10:59 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 i am doing event b now 06/04 11:00 2 subjects event b 3rd is this 1 which is about agda and haskell 06/04 11:00 ic, I thought the event b stuff was supposed to be before 3141 06/04 11:01 tactical grace 06/04 11:01 you are from nsw 06/04 11:01 you are from unsw 06/04 11:01 technically but its not a prerequisite 06/04 11:02 cHAK 06/04 11:02 u are manuel 06/04 11:02 my lecturer 06/04 11:02 it can't be b/c of the CS students 06/04 11:02 vlad__: indeed 06/04 11:02 hahahah 06/04 11:02 this is too funny 06/04 11:02 cought out 06/04 11:03 good assignment 06/04 11:05 thanks alot for all your help kosmikus 06/04 11:21 i have to go now, hopefully i will figure things out better after more practice 06/04 11:21 take it easy tactical grace 06/04 11:22 see you in the lectures 06/04 11:22 I was going to suggest reading "A Few Constructions on Constructors". No I wasn't. 06/04 11:39 ;) 06/04 11:41 Whats Gordon Brows equality like? 06/04 12:08 *Brown 06/04 12:09 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 :) 06/04 12:30 false or x = x 06/04 12:31 would be less wrong indeed 06/04 12:31 it is not a and either "true or false" returns true... 06/04 12:31 I've always said that "grep Bool" is a good test of any dependently typed library. 06/04 12:32 pigworker: what you mean 06/04 12:32 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 "A Boolean is a bit uninformative." was my old slogan. 06/04 12:35 pigworker: sure, but they should not be to be completly removed 06/04 12:36 for instance vectors hold more information than lists, but we should not remove lists. 06/04 12:36 but in 06/04 12:36 a dependently typed language it is evident that we should use less bools 06/04 12:37 and more 'Dec P' 06/04 12:37 this is just my POV, of course... 06/04 12:38 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 but I wouldn't mind if Bool got renamed to Bit to emphasis on this 06/04 12:40 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 sure 06/04 12:41 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 :( 06/04 12:44 kosmikus: rats! 06/04 12:44 pigworker: yeah. "not innovative enough" and "relatively weak CV" 06/04 12:44 bah! 06/04 12:45 kosmikus: sounds like prejudice to me; or is that what "pre-screening" means? 06/04 12:46 kosmikus: :( 06/04 12:46 We're clearly going too mainstream 06/04 12:46 pigworker: yes, that's what it means ;) 06/04 12:46 pigworker: from 49 submissions, they select 23 that even get expert reviews. 06/04 12:46 ultimately, 5 get funded. 06/04 12:47 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 kosmikus: not great odds, but a shame that they don't get expert reviews for all 06/04 12:47 Where an ICFP paper is clearly less relevant for your future life than a grant proposal with 800 kEUR. 06/04 12:47 kosmikus: So you got about 100 submissions? I don't expect you to answer that... 06/04 12:50 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 kosmikus: so, how does a non-expert decide what is innovative? 06/04 12:50 TacticalGrace: with nipples 06/04 12:50 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 Which reminds me: grant app to finish; must work on zip, pep and fizz; oh, and some technical substance. 06/04 12:53 perhaps I should start submitting grant apps in other countries. 06/04 12:54 International collaboration always looks good. 06/04 12:56 kosmikus: and you've got a conflict with us lot, too... 06/04 12:59 At page 8 in tutorial - first verdict: Syntax beats Twelf 06/04 12:59 pigworker: yes. 06/04 12:59 had better go to school for a bit. 06/04 13:03 Agda definitely feels a lot like Twelf, just easier 06/04 16:22 uh 06/04 16:22 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 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 pigworker: yeah. "not innovative enough" and "relatively weak CV" 06/04 16:39 fucking hell that is ridiculous 06/04 16:39 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 most likely I cannot understand any of this but I will try :))) 06/04 17:23 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 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 'schemes' perhaps. 06/04 17:43 a lot of things 06/04 17:43 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 dunno 06/04 17:50 oh and fibrations/fiber bundles get mentioned a lot 06/04 17:51 (another thing which I have only got cheesy videos of mugs morphing into donuts rather than any actualy understanding) 06/04 17:52 :-) 06/04 17:52 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 if someone is interested 06/04 18:13 stevan nice!!!!!! 06/04 18:14 this "Dense linear orders" is why I had to put down my model theory book 06/04 18:14 i think i can explain it now, but we haven't implemented it fully yet 06/04 18:15 stevan I am going to ask you all about it :P 06/04 18:16 would be awesome to have running examples, but that will probably take an other month or so 06/04 18:16 page 12,  Otherwise (inequalities) -- 06/04 18:19 this part is basically doing a topological sort? 06/04 18:19 i know nothing about topological sorts 06/04 18:20 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 natural numbers 06/04 18:21 hmm 06/04 18:22 "Ssreﬂect what does it do?" hehe I think the same thing 06/04 18:22 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 nice in Agda they don't have such a thing (although there are good points to it as well) 06/04 18:23 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 what is Qed? 06/04 18:25 Saizan, it's meant to be used for "proofs" -- it's sort of like a poor mans proof irrelevance 06/04 18:25 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 it means you can go an reprove any Qed thing in a different way, without breaking stuff 06/04 18:26 but the bad thing is sometimes you /want/ proofs to have computational content -- like with well founded recursion 06/04 18:26 fax: it does have some perfs advantages too 06/04 18:26 and the other problem is that people use it when they shouldn't 06/04 18:26 npouillard oh that's true I should have thought of this as well 06/04 18:27 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 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 ok, so do you understand why qelim for dlos works now :-)? 06/04 18:31 no 06/04 18:31 :-/ 06/04 18:32 im not ready to ask any intelligent questions yet :P 06/04 18:32 just looking at the code 06/04 18:32 and I wish I had agda but I don't know how to install it 06/04 18:32 the theory dependent part (DLOs) isn't done yet unfortunately 06/04 18:33 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 so I decided to come back to it another day 06/04 18:34 I suppose you need decidibile equality on the carrier to prove the forall/~exists~ switch? 06/04 18:34 or you use classical connectives? 06/04 18:34 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 well there's no reason to not have both.. I suppose 06/04 18:34 yeah, if look at the forall case in the last proof in decisionProcedure you will see what happens 06/04 18:36 ¬∃¬⇔∀ : ∀ {A : Set}{P : A → Set}(d : ∀ x → Dec (P x)) → (¬ (∃ λ x → ¬ P x)) ⇔′ (∀ x → P x) 06/04 18:43 this is so cool stevan 06/04 18:43 :-) 06/04 18:43 agda lib doesn't have rationals? 06/04 18:51 it does, but it's basically only the data type Q, without any useful functions (+, -, *, etc are not implemented) 06/04 18:52 :S 06/04 18:58 I can't find anything, do they have setoids? 06/04 18:58 mmm 06/04 18:58 quotients comeing soon probably means no 06/04 18:58 http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Rational.html#180 06/04 18:59 I wonder why it has     isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1)) 06/04 19:01 ah that's for ≃⇒≡ : _≃_ ⇒ _≡_ 06/04 19:01 http://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf] 06/04 20:35 http://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf 06/04 20:35 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 how different? 06/04 20:45 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 oh ok 06/04 20:46 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 is there something to read about the near to come quotients in Agda ? 06/04 20:48 how do you know they are comming soon? 06/04 20:48 :S I hope I haven't made this up 06/04 20:48 they seemed to have been discussed during last AIM, but it doesn't say anything more than that 06/04 20:50 It's not obvious to me how to make (R x y) -> [x]=[y] hold, without re-engineering propositional equality. 06/04 20:56 where [_] gives equivalence classes wrt R 06/04 20:56 it seems okay to add this stuff as an axiom 06/04 21:02 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 then of course the axioms don't have computational properties... I guess that is the real problem 06/04 21:03 fax: yep, that's the problem 06/04 21:03 what does corn do? 06/04 21:07 well corn doesn't use typeclasses but I think they are rewriting it to do so 06/04 21:07 but you must carry about morphism proofs with all the stuff 06/04 21:10 like if you defined a group with inverse : G -> G 06/04 21:10 then you must also have  inverseProper : forall x y, x ~ y -> inverse x ~ inverse y 06/04 21:10 so, the real closed fields using reflection in coq paper i posted recently, is it runnable? 06/04 21:11 I've not tried 06/04 21:11 the reals in the stdlib are classical 06/04 21:11 did you see the bit where they used it to derive P \/ ~P for first order statements 06/04 21:12 and they used those? 06/04 21:12 CoRN defines constructive reals too 06/04 21:12 i haven't looked at it propertly yet 06/04 21:12 I've not tried this reflection thing though 06/04 21:12 well 06/04 21:13 I was going to say I don't think we can use quantifier elimination on reals 06/04 21:13 (since we don't have that  forall/~exists~ switch) 06/04 21:13 but then... there is that cylindrical algebraic decomposition 06/04 21:13 will it not fall out like it did in our quantifier elim library? 06/04 21:14 I am confused :P 06/04 21:14 how can it work 06/04 21:14 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 "To build a decision procedure from this theorem, we have to chose a ﬁeld D 06/04 21:15 over which sign and equality is decidable." 06/04 21:16 so in this case, they only need coefficients of the polynomial to be decidible 06/04 21:16 the actual variables can be real, if I understand correctly 06/04 21:16 i.e. you could have polynomials with rational coefficients, except they are functions R^n -> R 06/04 21:16 (please correct me if I say something wrong!!) 06/04 21:17 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 oh there are no axioms for setoids 06/04 21:21 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 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 ok 06/04 21:24 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 so their RCF solver is most likely runnable then? (just making sure :-) 06/04 21:26 well the constructivist thing to do will be try it out :) 06/04 21:26 lets find the source code 06/04 21:26 I didn't manage that before 06/04 21:26 me neither 06/04 21:26 #  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 "#  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 so maybe it's not quite finished yet 06/04 21:30 if i remember, i could probably ask thierry about it tomorrow... 06/04 21:33 but it seems the formath people have to solve this problem (if it isn't solved already)? 06/04 21:40 formath? 06/04 21:40 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 me?? 06/04 21:41 21:04 < stevan> have you read about the formath project? 06/04 21:42 21:05 < fax> yeah 06/04 21:42 21:05 < stevan> that sort of stuff? 06/04 21:42 21:05 < fax> yes 06/04 21:42 do you have an evil twin? 06/04 21:42 This 'ForMath' sounds great 06/04 21:43 there is more under "Research Methodology" 06/04 21:44 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 I've seen this 06/04 21:50 ok 06/04 21:51 --- Day changed Wed Apr 07 2010 hey manuel 07/04 08:52 do you recken you can help me out a little with my assignment? 07/04 08:53 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 from what i could gather it's not runnable, due to Qeds. 07/04 15:24 and removing the Qeds makes type checking too slow. 07/04 15:25 tarnge 07/04 15:26 strange 07/04 15:26 i asked "so what's the plan?",  "i don't know, maybe CBN instead of CBV might help" 07/04 15:27 stevan: what do you want to run? 07/04 15:27 the solver 07/04 15:27 as you can run agda's (to prove things) 07/04 15:28 s/agda's/agda's ring solver/ 07/04 15:29 stevan: OK, so that's more "a program written with tactics", than "a proof we want to look at", right? 07/04 15:31 yea, a reflective tactic 07/04 15:32 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 you can extract f : nat -> nat from the proof forall x, exists y. x < y 07/04 15:35 when the decision procedure is written using (external) tactics? 07/04 15:36 it should be true in general 07/04 15:37 well when you do it reflectively the proof is that function? 07/04 15:37 I just mean it shouldn't matter if how the statement is proved 07/04 15:38 fax: no it does not matter, tactics just build programs 07/04 15:39 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 (ugly and large ones actually) 07/04 15:39 tactics in coq are just scripts that write out lambda terms 07/04 15:40 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 try "Print mylemma." to see it 07/04 15:40 but   (forall a : A, exists b : B, aRb) <-> (exists f : A -> B, forall a, aR(f a)) 07/04 15:41 (ah right, i remember having printed lemmas now) 07/04 15:42 so what does the Qed do? i didn't get that yesterday... 07/04 15:43 * stevan reads logs 07/04 15:45 Qed, type-check the term and then hide its definition 07/04 15:45 like 'abstract' in agda 07/04 15:45 Defined, keeps the definition accessible 07/04 15:46 so effectively it blocks type level computations? 07/04 15:47 stevan: any computation that would like to unfold mylemma to its definition 07/04 15:49 ok, interesting 07/04 15:50 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 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 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 this is sick http://stackoverflow.com/questions/476959/why-cant-programs-be-proven 07/04 17:20 it's all "Godel Godel Godel Turing Halting Incompleteness" or "proofs are too hard and cost lots of money!" 07/04 17:21 hehe 'How do you prove your Coq specification is correct?' 07/04 17:22 That's how all those ask-a-question sites are like 07/04 17:27 it's really a shame because all this rubbish and misinformation is the source which people learn form :| 07/04 17:28 No, people learn from wikipedia :p 07/04 17:28 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 guys what are the pro's and cons of Uniqueness typing vs Monads for IO? 08/04 03:11 oh oh pigworker 08/04 15:54 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 fax: what's up? 08/04 15:54 fax: I've seen it. Am replying now. 08/04 15:55 I'm wondering if that's so ? you have to do Acc in Set 08/04 15:55 ok 08/04 15:55 fax: yes, but Edwin kills it anyway! 08/04 15:55 ah!! 08/04 15:55 * edwinb feels his ears burning 08/04 15:57 roconnor 08/04 15:58 14:55 < fax> I'm wondering if that's so ? you have to do Acc in Set 08/04 15:58 14:55 < fax> ok 08/04 15:58 14:55 < pigworker> fax: yes, but Edwin kills it anyway! 08/04 15:58 this is that  need not store their indices  I am guessing 08/04 15:58 fax: yes 08/04 15:58 indeed 08/04 15:58 fax: link 08/04 16:00 link to what ? 08/04 16:00 http://www.cs.st-andrews.ac.uk/~james/RESEARCH/indices.pdf ? 08/04 16:00 need not store their indices 08/04 16:00 is acc specifically mentioned in this paper? 08/04 16:01 actually I think it is.. 08/04 16:01 I think it's in my thesis 08/04 16:02 I can't remember though, it was so long ago ;) 08/04 16:02 7.3Accessibility Predicates 08/04 16:02 but this is Bove-Capretta 08/04 16:02 which is slightly different from Acc 08/04 16:02 probably close enough 08/04 16:03 aha. Page 51 of my thesis 08/04 16:03 does this mean there is no need to separate Prop and Set universes? 08/04 16:04 actually, no, not page 51, that doesn't explain it 08/04 16:04 I had always gathered that 'Prop/Set distinction' is just one way to do it 08/04 16:04 well it's still useful 08/04 16:04 edwinb yes I am not happy about #debill too! 08/04 16:05 i guess it's still useful to have an equality proof for free for anything that's in Prop 08/04 16:05 #debill ? 08/04 16:06 * edwinb blinks 08/04 16:06 you twitted about it 4 hours ago and already forgot ? :p 08/04 16:06 no, I just forget that people might notice the rubbish I talk on twitter ;) 08/04 16:06 (It was more than 4 hours ago, that gadget is broken) 08/04 16:07 Saizan - I think they're making up crazy laws to give them stronger control of people 08/04 16:07 anyway a bit paranoid 08/04 16:07 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 ah, i've read about that 08/04 16:08 roconnor: comment shipped! 08/04 16:10 thanks 08/04 16:10 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 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 same goes for Bove-Capretta domain predicates 08/04 16:11 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 do you have an example in mind? 08/04 16:11 The only implementation of this I know of is in Idris, and that just picks the first erasure it sees 08/04 16:11 if there's a choice between erasing an index or a constructor tag, it erases an index 08/04 16:12 oh well I recall some on the paper there was 3 different ways to erase things from Vec-E 08/04 16:12 ah right 08/04 16:12 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 that sounds good yeah -- and certainly that case will apply to (zero or) one constructor types like Acc 08/04 16:13 yes 08/04 16:13 hmm 08/04 16:13 so okay I have another question :) 08/04 16:13 incidentally, I've also found doing this erasure step makes compilation faster overall 08/04 16:14 because code generation is much easier ;) 08/04 16:14 what if I defined a relation a < b then write a function  subtract : forall a b : |N, a < b -> |N 08/04 16:14 it's still whole program compilation though, right? 08/04 16:14 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 Saizan: it is, but I don't think it has to be 08/04 16:16 I might have to think about that soon. Compilation times are starting to get a bit irritating for bigger things. 08/04 16:17 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 what's a squashed set? 08/04 16:19 I think I read about squash types actually, and you can make a monad out of them 08/04 16:19 but how would you define it in say epigram ? 08/04 16:19 or would it be a feature 08/04 16:20 I like to pretend a squashed type of A is (A -> 0) -> 0, though this isn't quite true 08/04 16:20 I just happen to have this example handy, hang on... 08/04 16:20 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 ah right, inhabited A 08/04 16:21 pigworker: are there any advantages of squash types over (A -> 0) -> 0? 08/04 16:22 http://www.cs.st-andrews.ac.uk/~eb/hacking/minus.idr 08/04 16:22 hmm, something mysterious has happened there 08/04 16:23 mysterious? 08/04 16:26 I fixed it an reuploaded in the hope you wouldn't notice the bug in the optimiser that was overzealous ;) 08/04 16:27 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 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 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 I guess roconnor's gone now, though. 08/04 16:34 hi dolio I have had lots of questions to ask you !! but I odn't remember them now :))) 08/04 16:37 Heh. 08/04 16:39 Saizan: strictly speaking, you also need to make sure simplification terminates and check uniqueness of the resulting normal forms 08/04 16:40 dolio: what happens to propositional equality in Nathan's setting? 08/04 16:41 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 pigworker: ah, yeah, makes sense :) 08/04 16:42 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 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 it's a good way to implement unsafeCoerce in haskell 08/04 16:43 Ah. 08/04 16:43 (though that's about nontermination rather than open) 08/04 16:43 pigworker: Basically, everything in it gets erased and 'refl' tokens get passed around. 08/04 16:44 Maybe that isn't a Prop vs. Set issue, though. 08/04 16:46 dolio: ok, three questions; is equality elimination strict? is equality proof irrelevant? are refl tokens passed in closed computation? 08/04 16:46 Since you've all just been discussing similar problems with erasing Props. 08/04 16:46 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 As I said, though, I haven't actually read the section on proof irrelevance yet. 08/04 16:48 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 What is a good reference for the typing rules pertaining to the different Set levels? 08/04 18:04 glguy I think they just make it up as they go 08/04 18:05 there's a reference manual in development but I don't think it has anything about this yet 08/04 18:06 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 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 And the sort of (co)data types has to be big enough to type the constructors. 08/04 18:23 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 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 do you know haskell 09/04 02:28 Yes 09/04 02:28 and GADTs? 09/04 02:28 Hmm, we've discussed those, but I wouldn't say I'm fluent in them :/ 09/04 02:28 you probably saw that cheesy 'well typed evaluation' example 09/04 02:28 The only real example in the slides is one for n+0==n 09/04 02:29 Is that cheesey? 09/04 02:30 Don't suppose anyone has a link to that cheesy example :p? might help ;) 09/04 02:31 http://65.254.53.221:8000/6305 09/04 02:34 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 So does anyone know of anything that might help me ? 09/04 02:41 with what exactly 09/04 02:42 Understanding how to prove things with those kind of functions :/ 09/04 02:43 I don't really know what you mean 09/04 02:43 Well, first assignment was to write a unitMatrix function and a transpose function for matrices (Vec (Vec A m) n), 09/04 02:44 that sounds cool 09/04 02:44 second is to prove that transpose (unitMatrix {n}) == unitMatrix {n} 09/04 02:44 oh that sounds very difficult 09/04 02:44 can I see these functions 09/04 02:44 BiscuitsLap: are you stuck with something in particuler? 09/04 02:45 this is what I have so far: http://www.pastebin.org/142243 09/04 02:45 I think he's stuck with the transpose proof ? 09/04 02:45 this proof looks incredibly difficult 09/04 02:46 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 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 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 in the suc n case, 09/04 02:48 it's proving: 09/04 02:48 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 probably that will use recursion having a proof of  transpose (unitMatrix {n}) == unitMatrix {n} 09/04 02:48 but you can unfold the transpose to see proving that ^ is the same as proving this: 09/04 02:49 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 yeah, since unitMatrix {suc n} is defined in terms of unitMatrix {n} you want to recurse with transpose-unit too 09/04 02:50 oops that 'toprow' should have been something else 09/04 02:50 (probably) 09/04 02:50 so , correction: 09/04 02:50 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 now you can clearly see where it starts to get awkward 09/04 02:51 here it has got 'transpose2' but our recursive case has only mention of 'transpose' 09/04 02:51 fax: i think you mixed up the defs of transpose and transpose2 09/04 02:52 Hmm, yeah 09/04 02:52 you're right!! 09/04 02:52 transpose2 was just another definition I thought would help out at some point 09/04 02:52 that is good news because it means the proof will be easier 09/04 02:52 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 yes 09/04 02:57 fax: Would this definition make my life easier http://www.pastebin.org/142256 ? 09/04 03:01 it's much closer to the other thing so they the proof they are equivalent will be easier 09/04 03:02 ok, so with that definition I can do transpose-unit {suc n} = cong increaseUnitMatrix ? 09/04 03:03 no 09/04 03:03 ? 09/04 03:04 How about: 09/04 03:05 transpose-unit {suc n} = cong (_::_ (1 :: vmap head (vmap (_::_ 0) unitMatrix))) { }3 ? 09/04 03:06 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 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 that sounds good 09/04 03:09 I suspect I'd have to use trans from there 09/04 03:11 Where I'd first prove something like vmap (_::_ 0) matrix == zip (replicate n 0) matrix _::_ 09/04 03:12 Would that move me in the right direction ? 09/04 03:15 yes 09/04 03:15 hmm, let's try 09/04 03:16 mh, how'd you call a proof of transpose (replicate n x :: m) == vmap (_::_ x) (transpose m) ? 09/04 04:33 ? 09/04 04:40 Not sure 09/04 04:40 But you sure are going faster than I am :/ 09/04 04:40 well, yeah, i've completed the proof, but i've quite more experience with Agda :) 09/04 04:46 btw, some nice properties to have about vmap are: 09/04 04:47 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 and 09/04 04:47 vmap-id : ∀ {A} {n} {v : Vec A n} -> vmap (λ x -> x) v == v 09/04 04:47 ooh, I was already working on the vmap-fusion one :p 09/04 04:48 those are the functor laws for "\ A -> Vec A n", btw :) 09/04 04:49 :-/? 09/04 04:49 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 Hmm, vmap-id was easy enough :) 09/04 04:54 they are quite similar, both simple inductions on the vector 09/04 04:55 Hmmm, one last bit to solve 09/04 04:57 currently I had vmap-fusion {A} {B} {C} {g} {f} {zero} {[]} = refl 09/04 04:58 and vmap-fusion {A} {B} {C} {g} {f} {suc n} {v :: vs} = cong (_::_ ?) vmap-fusion 09/04 04:58 struggling to define that ? 09/04 04:58 when I try to fill in "f ?", which should be of type C as requested, it fails :/ 09/04 04:59 oh 09/04 04:59 nvm 09/04 04:59 you need some parentheses around that 09/04 04:59 i.e. cong (_::_ (f ?)) vmap-fusion 09/04 05:00 Won't work either 09/04 05:01 oh, you switched f and g 09/04 05:01 in the patterns 09/04 05:01 Ah, crap, yes 09/04 05:02 Sorry about that :/ 09/04 05:02 btw, you can bind arguments by name, rather than position 09/04 05:02 oh ? 09/04 05:02 e.g. vmap-fusion {f = f} {g = g} {v = x :: xs} = cong (_::_ (f ?)) vmap-fusion 09/04 05:03 oooh, nice :) 09/04 05:03 that certainly cleans things up 09/04 05:04 Great, I've just written my first two actual proofs in agda :p 09/04 05:04 (tbc i could have said e.g. {f = foo}, since the one on the right is just bound there) 09/04 05:04 Yup, found out by the v = x :: xs part, thanks :) 09/04 05:05 congrats for the first proofs :) 09/04 05:07 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 ? 09/04 05:09 wait... 09/04 05:12 that's probably not even true :/ 09/04 05:12 or is it :S 09/04 05:13 mh, i don't think it is in general 09/04 05:14 Hmmm 09/04 05:14 i didn't had a reason to try to prove that since i went with your original transpose 09/04 05:15 that was the (vmap head mat) :: transpose (vmap tail mat) one, right ? 09/04 05:16 yeah 09/04 05:21 ok, let's see, what kind of properties would I need, and what kind of properties could I deduce :/ 09/04 05:22 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 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 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 gah... 09/04 05:37 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 Just found out that refl suffices in both cases :/ 09/04 05:38 Hmmm 09/04 06:07 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 I think it should be the subst rule, since I want to substitute the vmaps with another vmap 09/04 06:08 vmap-fusion is not that useful there, actually 09/04 06:10 however you'd use trans 09/04 06:11 "trans vmap-fusion ?" should fit there 09/04 06:11 however i think that proof is easier if you generalize over the matrix 09/04 06:12 i could be wrong though :) 09/04 06:12 Hmm, currently stuck at proving 09/04 06:16 sillyproof3 : {n : N} -> (vmap (\x -> 0) (unitMatrix {n})) == (replicate n 0) 09/04 06:17 should be easy enough to solve :/ 09/04 06:17 but I'm just not getting it 09/04 06:17 oooh, got it :) 09/04 06:29 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 oh wait, I think I got it working 09/04 06:35 Hmm 09/04 07:00 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 Saizan, edwinb: I don't get why having a prop universe is needed in light of edwin's erasure mechinicm. 09/04 10:33 isn't everything you put into prop already provably proof irrelevent? 09/04 10:33 oh, but maybe not definitionally proof irrelevent. 09/04 10:34 are two variables of the same proposition convertable? 09/04 10:34 roconnor: it's at least trivial to prove equality of proofs 09/04 12:39 make eq := (\ P Q p q -> _) : (P : Prop) (Q : Prop) ( p : :- P) (q : :- Q) -> :- p == q 09/04 12:39 Made. 09/04 12:39 meh 09/04 12:39 it is simply *more* trivial 09/04 12:39 seems better to use generic programming than bake a special universe of propositions into the language 09/04 12:40 they might be convertible too, i'm not sure 09/04 12:40 ya, if they are convertable then that is something more. 09/04 12:43 * Saizan wonders how you test that 09/04 12:44 i think it's also to let coerce work without ever having to be strict on the equality proof 09/04 12:50 but that could have been guaranteed by how you define == i guess 09/04 12:52 isn't coerce never strict on any equality proof? 09/04 13:06 whether it is equality of set universe or prop universe 09/04 13:06 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 err, that's not right 09/04 13:34 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 so, disregard that :) 09/04 13:35 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 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 . means that terms was inferred/forced by pattern match specialization 09/04 22:31 okay thanks :) 09/04 22:33 if it says n != .n, those are two distinct names… (FYI.) 09/04 22:37 liyang: but it is based on something right? 09/04 22:41 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 in OTT are two variables of the same proposition type convertable? 11/04 11:29 yes. 11/04 11:29 neat 11/04 11:32 so two proofs of Acc foo won't be converable since Acc won't live in Prop. 11/04 11:33 ah 11/04 11:34 but it has to be that way 11/04 11:34 as you said 11/04 11:34 otherwise open reduction may not terminate 11/04 11:34 yes. 11/04 11:34 so it is impossible, at least for now 11/04 11:34 the two Acc proofs will be provably equal 11/04 11:34 since a few years ago extentional equality and decidable type checking was also "impossible" 11/04 11:35 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 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 more concretely put, is there a translation of OTT to the Prop free fragment of OTT 11/04 11:38 it's just an optimization 11/04 11:38 more concretely, yes there is such a translation 11/04 11:38 neat 11/04 11:39 okay I will think of Prop as an optimization 11/04 11:39 That's how they define OTT in most of the papers, as I recall. 11/04 11:39 OTT gets translated into a type theory with just 0, 1, 2, Pi, Sigma, W. 11/04 11:39 yeah, the Agda models are all in Set, with no def-prf-irr, but prop-prf-irr 11/04 11:40 The models have all the beta-behaviour of OTT, but a weaker equality on neutral values. 11/04 11:42 We call this weaker theory OTT- 11/04 11:43 if variables of the same type are converable, then OTT must not be strongly normalizing 11/04 11:44 (though even coq is not strongly normalizing) 11/04 11:44 OTT- is still extensional: it models extensional type theory (it implements Oury's API for extensionality) 11/04 11:45 The beta-rules are strongly normalizing, but they aren't the whole story. 11/04 11:47 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 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 mh, i think i saw that too 13/04 18:59 Shall wait 'til he shows up. 13/04 19:03 liyang: Sounds like something on the SHE page. 13/04 20:03 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 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 liyang: http://img688.yfrog.com/i/3l5.jpg/ 13/04 21:16 is that from a set ? 13/04 21:17 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 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 set 13/04 21:18 pigworker (I think there's a missing newline in the draft of ornaments --3. definition of Alg) 13/04 21:19 fax: if that was all that was missing, I'd be a happy man... 13/04 21:19 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 oh what d you mean? 13/04 21:20 there is more to do with it 13/04 21:20 The Ornaments draft is quite a bit of windup but no punchline. 13/04 21:22 http://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.agda 13/04 21:24 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 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 and that (2) proves that stack compiler respects evaluation ? 13/04 21:30 yep 13/04 21:31 but the code of the compiler is just the same as it would have been 13/04 21:31 of course, it's not always such an instant win, but it is progress 13/04 21:33 I think it's a very beautiful result. 13/04 21:34 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 wait this is awesome 13/04 21:47 if I defined + on nat it induces ++ on list AND vector 13/04 21:47 fax: depends how you define +, but you should get it cheap, certainly 13/04 21:48 The question is how to turn ornaments on functors to ornaments on their (co)algebras. 13/04 21:53 (just noticed also that  data Data (D : Desc I) ... : [[ D ]] (Data D i) -> ... should  probably be  [[ D ]] (Data D) i 13/04 22:00 on pg. 4 13/04 22:00 fax: seems likely, thanks 13/04 22:47 --- Day changed Wed Apr 14 2010 (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 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 hmm 14/04 00:49 they're logically equivalent 14/04 00:50 data Identity1 (A : Set) : A -> A -> Set where refl1 : forall (a : A) -> Identity1 A a a 14/04 00:51 data Identity2 (A : Set) (a : A) : A -> Set where refl2 : Identity2 A a a 14/04 00:51 id12 : forall {A : Set} (a : A) -> Identity1 A a a -> Identity2 A a a 14/04 00:51 id12 .a (refl1 a) = refl2 14/04 00:51 id21 : forall {A : Set} (a : A) -> Identity2 A a a -> Identity1 A a a 14/04 00:51 id21 a refl2 = refl1 a 14/04 00:51 But computationally? 14/04 00:51 I don't know which one is better 14/04 00:52 computationally? 14/04 00:52 I am pretty sure you can compile them both away 14/04 00:52 (to nothing) 14/04 00:52 will agda? 14/04 00:52 no 14/04 00:52 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 I think 2 is easier to use 14/04 00:53 because you don't have to worry about the actual element -- type inference does taht 14/04 00:53 (by intuitive, I mean symmetrical.) 14/04 00:54 liyang, if you try to prove transitivity 14/04 00:56 trans : forall {A : Set} (a b c : A) -> Identity A a b -> Identity A b c -> Identity A a c 14/04 00:56 Well, you could write refl : {x} -> x == x , where type inference will fill in the actual element. 14/04 00:56 for both types,  that might convince you that one is nicer to use than the other 14/04 00:56 fax: ahhh hah. I see. 14/04 00:57 data JMeq (A : Set) (a : A) : forall (B : Set) (b : B) -> Set where JMrefl : JMeq A a A a 14/04 00:58 this is a good one for Agda 14/04 00:59 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 that is useful in Coq 14/04 01:00 decidible equality on U lets you prove K axiom 14/04 01:00 but you don't want that in agda because you can prove K from the pattern matching 14/04 01:01 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 trans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c 14/04 01:21 trans1 a .a .a (refl1 ._) (refl1 ._) = refl1 _ 14/04 01:21 trans2 : forall {A : Set} (a b c : A) -> Identity2 A a b -> Identity2 A b c -> Identity2 A a c 14/04 01:21 trans2 a .a .a refl2 refl2 = refl2 14/04 01:22 well 14/04 01:22 trans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c 14/04 01:22 trans1 a .a .a (refl1 .a) (refl1 .a) = refl1 a 14/04 01:22 let me be explicit 14/04 01:22 Only if you make the argument of refl1 explicit… 14/04 01:22 I had defined refl : {x : X} -> x ≡ x 14/04 01:23 The two definitions of == in my pastebin above seem to be interchangeable, at least with trans. 14/04 01:24 in coq, you can still supply the parameters 14/04 01:26 i.e. A and a in refl2 14/04 01:26 the difference there, is there is a slightly different type of type inference -- called maximal insertion 14/04 01:27 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 well I just mention it because the difference between these two versions is more apparent in Coq 14/04 01:28 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 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 ahh need to remember that 14/04 01:31 That can't just be the end of it, shurely? 14/04 01:31 Are there any reasons to prefer one over the other, at least in the context of Agda? 14/04 01:33 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 P-M eq beats M-L eq in Agda. Why make refl store more stuff? 14/04 01:34 So, just “ 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 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 (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 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 Mmkay. I'll go with M-L equality as it seems easier to explain, storage be damned. 14/04 01:40 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 pigworker: this is just for an introductory section to dependent types. I wouldn't dream of writing untidy code. :3 14/04 01:47 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 liyang: whatever gets you where you need to go 14/04 01:48 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 equality made my attempts to implement category theory fail :( 14/04 01:52 fax: or vice versa 14/04 01:52 g'night all 14/04 01:59 oh my 14/04 02:01 I missed pigworker 14/04 02:02 it feels like forever since I last wrote any agda 14/04 16:15 It's been seven hours and fifteen days 14/04 16:16 lol 14/04 16:16 I'm glad you're keeping track :) 14/04 16:16 copumpkin is back! 14/04 16:19 more or less :) 14/04 16:19 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 not to me 14/04 16:27 you're turning a list [A] into [Sigma a : A, P(a)] ? 14/04 16:27 by filtering out things which don't have property P 14/04 16:28 yeah something like that 14/04 16:28 different in what ways? 14/04 16:28 the part after "so that" is quite unclear 14/04 16:29 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 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 i understand "filtering out" as "removing" 14/04 16:33 but i'm not a native speaker 14/04 16:33 I guess you can also just have filter atke [A] -> [A] 14/04 16:33 but then prove sepeartetly (P1) xs >= filter xs  (P2) In x xs -> P x 14/04 16:34 http://www.google.com/dictionary?aq=f&langpair=en|en&hl=en&q=filter%20out <- google agrees with me though 14/04 16:34 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 oh and that P2 was wrong 14/04 16:34 Stop absuring the man! :) 14/04 16:35 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 i'd say it filtered out the water 14/04 16:36 this is so philosophical! 14/04 16:36 It filtered out the gold. 14/04 16:37 What comes out of the filter is water without gold. The gold gets caught. 14/04 16:38 Filtered out of the water. 14/04 16:38 Or mud. Or what have you. 14/04 16:38 if I passed through a filter, was I filtered? 14/04 16:38 ooh, so what you filter out is what gets caught in the filter 14/04 16:38 but if you got stuck in the filter, were you filtered? 14/04 16:38 maybe BOTH ? 14/04 16:38 i was just thinking in terms of keeping vs. removing 14/04 16:38 i.e. seeing the filter as merely a splitter 14/04 16:39 almost sounds like you want List A -> List (Sigma (x : A) -> Dec (P x)) ? 14/04 16:39 well the way stevan put it was defintiely contrary ti what I thought about before 14/04 16:39 Filtered water is what you're left with after you filter out the impurities. 14/04 16:39 but I am not sure that I can say it's wrong 14/04 16:39 And the impurities get caught in the filter. 14/04 16:39 if you empty out the filter though, what are the impurities? 14/04 16:39 are they filtered impurities? 14/04 16:39 dolio: ok, i see it now 14/04 16:39 TheOnionKnight: oh that's neat because it's just map 14/04 16:40 then you can use a normal filter 14/04 16:40 hmm no 14/04 16:40 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 there's two different properties though 14/04 16:42 What does filter tell you about its input? 14/04 16:45 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 an algebraic ornament, indeed! 14/04 16:53 ohh :D 14/04 16:53 you could keep "not (P x)" in there too at that point :) 14/04 16:53 you could also index by the yes- and no-lists 14/04 16:54 The types reddit is really languishing. 14/04 16:58 Apparently the only types worth talking about these days are dependent types. 14/04 16:58 why the fuck is there like 10 reddits about dependent types :/ 14/04 16:59 worse than /types/ having no activity is jbapple stopped blogging 14/04 17:00 I could do with more constructive gems/stones, too. 14/04 17:09 :( 14/04 17:10 sometimes there are "proof pearl" papers which I can't acess 14/04 17:10 I can fetch them for you if you want 14/04 17:10 if you don't rat me out 14/04 17:10 well something I WOULD like is a list of all of them 14/04 17:10 but I am not sure if that actually exists 14/04 17:10 The last 'classical mathematicians confuse proof by contradiction with proof of negation' was amusing, but not particularly exciting. 14/04 17:11 the closest to a list of the 'functional peal's we have is that haskell wiki 14/04 17:11 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 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 (sorry to drag the conversation away from fun programs towards scary theory) 14/04 17:18 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 ccasin: Calculus of Inductive Constructions takes a more internal view, although descriptions of datatypes are not first class 14/04 17:21 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 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 I should read some of the early Cic papers, thanks 14/04 17:24 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 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 Like 'f (x .:: xs) cons-proof' instead of 'f .(x :: xs) (cons-proof {x} {xs})'? 14/04 17:39 dolio: the very thing 14/04 17:39 Yeah, I've run into that before. 14/04 17:39 does  f (x :: xs) .cons-proof = ... work? 14/04 17:39 fax: no, it makes f too strict 14/04 17:40 what's that pastebin thing again? 14/04 17:42 moonpatio.com 14/04 17:42 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 omg no unicode 14/04 17:49 I hate unicode 14/04 17:50 :) 14/04 17:50 sometimes I think NAD peruses code tables looking for the most obscure symbols for the standard library 14/04 17:50 early adopters... 14/04 17:52 pigworker: have you any good reason? sure there is some initial configuration cost but that's not that hard 14/04 17:52 that's neat with the split sort of like  [Either a b] -> ([a],[b]) 14/04 17:53 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 yeah 14/04 17:53 npouillard: even now, it's not a reliable exchange format 14/04 17:53 I think unicode just delays proper typesetting longer 14/04 17:54 fax: I think it is orthogonal 14/04 17:54 npouillard: and my typing isn't reliable enough, and massive keyboard shortcut customization is the road to hell 14/04 17:55 I mean the silly bits, like little superscript 2's and fractions 14/04 17:55 even when doing proper typesetting you may want something nicer than \alpha 14/04 17:55 pigworker: it becomes more reliable when people use it 14/04 17:55 Personally I use a .XCompose file under linux, so it works in any X application, and is nicely configurable 14/04 17:57 yes, ultimately I think it's good to have more symbols available 14/04 17:57 npouillard: I'll look into that 14/04 17:57 what I really want is something that looks like epigram research papers :P 14/04 17:57 (sort of like texmacs) 14/04 17:58 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 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 me? 14/04 18:03 :) 14/04 18:04 kosmikus: no, but you do quite well 14/04 18:04 when it comes to LaTeX, I'm certainly guilty 14/04 18:04 although I usually know what packages I'm using and try to include them if they're exotic 14/04 18:05 gotta use xetex 14/04 18:05 I heard a rumour that EasyChair was starting to support LaTeX-on-the-server. 14/04 18:05 so you can include exotic fonts that people have to pay for 14/04 18:05 just to piss them off more 14/04 18:06 pigworker: I think it does. I used it recently. 14/04 18:07 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 yes 14/04 18:08 progress 14/04 18:08 and you can check the pdf the server generates 14/04 18:08 a bit like what arxiv does since ages 14/04 18:08 you'd kinda need that feedback 14/04 18:09 gonna catch some sun while it's still up; back later 14/04 18:25 sorry, had friends drop by... thanks for the help with filter, guys. i like the splice solution. 14/04 19:19 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 stevan: yes, I noted that (viper) 14/04 19:55 --- Day changed Thu Apr 15 2010 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 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 it's like normal functional programming, except the types have a logical interpretation 15/04 14:34 I have read http://en.wikipedia.org/wiki/Intuitionistic_type_theory 15/04 14:34 fax: you can give a logical interpretation to System F types however 15/04 14:35 I got that, the Curry-Howard isomorphism, I'm happy with that, in fact I love it 15/04 14:35 What I'm saying is that I can't model Types in my head ... 15/04 14:35 sah0s: even as just being sets? 15/04 14:36 a type is just a name, you don't need to think of it as something 15/04 14:36 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 You don't want to write a type system in C. 15/04 14:37 sah0s: a type checker in C ? 15/04 14:37 npouillard: set-like is fine with me 15/04 14:37 I agree with dolio 15/04 14:37 A type system with a checker, yeah ... as a library 15/04 14:38 sah0s no this is where you are confused 15/04 14:38 If I have a clear idea of how to construct types then I can code it 15/04 14:38 fax: your are a bit rude 15/04 14:38 I find you quite rude too 15/04 14:39 (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 But I agree that C is not a language to write a type-checker 15/04 14:39 fax: sorry then 15/04 14:39 Ignore the C bit for the moment :) 15/04 14:39 I like C 15/04 14:40 I wasn't talking about C when I said "This is where you are confused" 15/04 14:40 Each to their own :) 15/04 14:40 sah0s: do you know any functional programming language? 15/04 14:40 Can we go through this page http://en.wikipedia.org/wiki/Intuitionistic_type_theory bit by bit, please! 15/04 14:40 What is a Π-type exactly, I don't understand what it says. 15/04 14:41 sah0s my advice is that wikipedia sucks and the reason you are confused is proabably from reading that page 15/04 14:41 okay 15/04 14:41 this could well be true 15/04 14:41 This question is relevant "do you know any functional programming language?" 15/04 14:41 I know a bit of scheme 15/04 14:41 functions as first-class citizens 15/04 14:42 to get Π you need to get → 15/04 14:42 tail recursion 15/04 14:42 → ? 15/04 14:42 sah0s: sure but not much of a type system 15/04 14:42 as in [a] → Int 15/04 14:42 the type of List.length 15/04 14:42 length : ∀ a. [a] → Int -- in haskell 15/04 14:43 length : ∀ {A} → List A → ℕ -- in agda but that merely the same thing 15/04 14:43 It helps to get ∀, too 15/04 14:43 is A a type variable? 15/04 14:43 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 sah0s: yes 15/04 14:43 stevan: yes 15/04 14:44 ∀ is universal quantification 15/04 14:44 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 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 sah0s: but with dependent types it is also the type of dependent functions 15/04 14:45 *I can't 15/04 14:45 ah 15/04 14:45 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 fax:  intersting 15/04 14:45 fax: I had the idea that types are nothing more than syntax sliced one way or another 15/04 14:46 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 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 So if I start from simply typed lambda calculus that'll give me a good idea? 15/04 14:48 (the book types and programming languages by pierce is a better resource than wikipedia also) 15/04 14:48 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 sah0s -- oh well if you are building up a lambda calculus to program in that is quite reasonable 15/04 14:49 fax: ok, I agree the "all about syntax" but not really the "it's nothing but names" 15/04 14:50 I would probably not recommend TaPL because it doesn't go into detail on dependent types 15/04 14:50 sure it makes sense to have primitve types like machine integers... 15/04 14:50 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 i have TaPL and I'm going through it slowly 15/04 14:51 What are the atomic or base types in Agda? 15/04 14:52 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 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 I am following the instructions on the Agda VIM page but it looks like agda --vim' does not do anything. 15/04 18:13 Is it no longer supported? 15/04 18:13 it generates a .vim file for syntax highlightning. 15/04 18:17 stevan: Where does it put the file? 15/04 18:18 I can't find anything with ls -a' and I don't get error messages, either. 15/04 18:18 same dir, .filename.agda.vim 15/04 18:18 Okay, interesting -- it won't handle files inside a directory. 15/04 18:20 I have to CD to the directory the file is in; that's the problem I was having. 15/04 18:20 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 stevan: I did try that; I hate Emacs. 15/04 18:22 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 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 ok, :-/ 15/04 18:26 stevan: Sorry :) I can be pretty grumpy about this particular issue. 15/04 18:38 which? 15/04 18:39 can I merge the following lines into one statement somehow? 15/04 19:25 import Module 15/04 19:25 open Module xval yval using (this; that) 15/04 19:25 open import Modulse xval yval using (this ; that) 15/04 19:26 Or did that not work? 15/04 19:26 I'm not sure I've ever tried an open import for a parameterized module. 15/04 19:27 i don't think it does. you could use a semicolon if you want the two on the same line. 15/04 19:27 that didn't seem to work 15/04 19:27 It certainly isn't a big issue 15/04 19:27 I just wondered 15/04 19:27 import Algebra.FunctionProperties 15/04 19:28 open Algebra.FunctionProperties _≡_ 15/04 19:28 using (Associative; _DistributesOverˡ_; _DistributesOverʳ_) 15/04 19:28 Mine already spans 3 lines 15/04 19:28 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 maybe using as? import Algebra.FunctionProperties as AFP; open AFP _≡_ 15/04 19:34 using (Associative; _DistributesOverˡ_; _DistributesOverʳ_) 15/04 19:34 Yeah, that doesn't look too bad 15/04 19:41 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 my mistake 15/04 19:55 --- Day changed Fri Apr 16 2010 Is there a better approach to the last definition in http://www.galois.com/~emertens/replace/replace.html ? 16/04 06:44 it just feels messy... 16/04 06:45 --- Day changed Sat Apr 17 2010 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 It definitely leads to some inconvenience. 17/04 01:15 Since you may want to prove lemmas about rev, but you can't actually refer to rev. 17/04 01:15 I'm not sure you can prove anything about it as it stands beyond reverse [] == [] 17/04 01:26 (or some other constant expression) 17/04 01:27 Yeah, it may well not be possible to prove things about reverse without lemmas about rev. 17/04 01:36 Since you may need to prove things by induction that you can't refer to simply by referring to reverse. 17/04 01:37 I'd probably go with a foldl definition, myself. 17/04 01:52 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 However ... 17/04 15:06 (always a however, heh) 17/04 15:06 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 ? 17/04 15:07 finite types ? 17/04 15:08 you mean like N3 = {0,1,2} ? 17/04 15:08 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 hi fax 17/04 15:08 hi 17/04 15:09 Yup, finite types: empty, unit, booleans (bivalent), trivalent, ... 17/04 15:09 you can define each one inductively, and infact you can define the whole (infinite) family of types inductively 17/04 15:09 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 "nfact you can define the whole (infinite) family of types inductively", huh? 17/04 15:10 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 all the types in the system? 17/04 15:10 sure 17/04 15:11 this family of types: empty, unit, booleans (bivalent), trivalent, ... 17/04 15:11 you can define them all with a single definition 17/04 15:11 i think so too, it's nice that they have names though like you were saying 17/04 15:11 with a single definition they don't have names really, just indexed 17/04 15:11 yeah 17/04 15:11 i understand product, sum, inductive, finite ... having difficulty with univers and equality, especially equality 17/04 15:12 i just don't see how something that looks like an operation (equality) can be a type :( 17/04 15:13 you can define it like 17/04 15:13 data Identity (A : Set) (a : A) : A -> Set where 17/04 15:13 refl : Identity A a a 17/04 15:13 universe seem to me to give you a hierarchy of families so I think I understand universes as well 17/04 15:13 so now,  refl : forall {A : Set} {a : A}, Identity A a a 17/04 15:13 that means e.g. this judgement holds:   refl N 3 : Identity N 3 3 17/04 15:14 for example 17/04 15:14 there is an equality check built into the type system though 17/04 15:14 it's syntactic congruence + beta reduction + unfolding definitions (replacing names with values that is) + eta expansions + maybe other stuff too 17/04 15:15 the result is that you can also have judgements like   refl N 3 : Identity 3 (1 + 2) 17/04 15:15 uh... 17/04 15:15 does the equality type extend the notion of the equality of base types into the rest of the type system? 17/04 15:16 the equality of objects of the base types i mean 17/04 15:16 the type system has got a notion of equality in it already,  the identity data types just reifies it 17/04 15:17 reify? 17/04 15:17 it makes it into a 'first class' citizen 17/04 15:17 wow 17/04 15:17 do you know prolog? 17/04 15:17 ages ago, unification, rules ... 17/04 15:17 why? 17/04 15:17 if you ever saw the definition of unification in prolog: 17/04 15:17 X = X. 17/04 15:18 or 17/04 15:18 equal(X,X). 17/04 15:18 uhuh 17/04 15:18 this is the same sort of thing 17/04 15:18 (as the identity type defined above) 17/04 15:18 can you give me a non-identity practical use of the equality connective? 17/04 15:20 i still don't get it, sorry - it is very alien to me (at least in the syntax above) 17/04 15:20 which syntax 17/04 15:21 data Identity (A : Set) (a : A) : A -> Set where 17/04 15:21 refl : Identity A a a 17/04 15:21 so now,  refl : forall {A : Set} {a : A}, Identity A a a 17/04 15:21 you're not use to the ML style? of using whitespace for application 17/04 15:21 no, sorry 17/04 15:21 subst : (A : Set) (P : A -> Set) (x y : A) (eq : Identity A x y) -> P x -> P y 17/04 15:21 you are missing out 17/04 15:21 this is important 17/04 15:22 ok 17/04 15:22 f x (y z) w 17/04 15:22 in scheme you would write it like 17/04 15:22 (((f x) (y z)) w) 17/04 15:22 whitespace for application! 17/04 15:22 wow 17/04 15:22 f(x,y(z),w) in algolish 17/04 15:23 breaks homoiconicity though 17/04 15:23 very neat shorthand 17/04 15:23 dolio: ? 17/04 15:23 I think you can recover most of the important parts of homoiconicity 17/04 15:23 but that is sort of an advanced topic 17/04 15:24 (specific to dependent types) 17/04 15:24 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 Of course, you do have that, because that's the only thing that inhabits identity types. 17/04 15:26 Which means x is actually y, or vice versa, and you use that to do the 'substitution'. 17/04 15:26 sah0s - write a parser for this whitespace syntax in ocaml or haskell or something :P 17/04 15:27 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 What other connectives produce what interesting stuff? 17/04 15:30 sah0s um well any time you use = sign in mathematics 17/04 15:30 it's not exactly rare :P 17/04 15:30 :P 17/04 15:31 sigma connective produces pairs, triplets, ... 17/04 15:31 it's true that ground inhabitants of Identity are boring 17/04 15:31 fax: that's my point 17/04 15:31 it gets interesting when you do e.g. some stuff -> Identity x y 17/04 15:31 What about: comm : (m n : Nat) -> m + n = n + m 17/04 15:31 what it means is that it computes an identity proof from the stuff 17/04 15:31 dolio: i get it know! 17/04 15:32 dolio: oops, *now! 17/04 15:32 dolio, the + though, how is the + interpreted? 17/04 15:33 + is a function type 17/04 15:33 However addition is defined for naturals. 17/04 15:33 where is the 'code' for + ? 17/04 15:34 anyway i see what you mean, you use the equality type to build up laws 17/04 15:34 Assuming naturals are inductive Peano numerals, it goes 'zero + n = n ; (suc m) + n = suc (m + n)' 17/04 15:34 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 of course + and = make it much nicer to read 17/04 15:36 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 what about inequality relations? 17/04 15:38 do they make any sense in ITT? 17/04 15:39 You mean stuff like less than, or just not-equal? 17/04 15:39 < > != 17/04 15:39 or <> or however you wanna say it :) 17/04 15:39 Plain 'not-equal' is usually defined as x /= y = (x = y) -> False. 17/04 15:40 False being the type with no proofs. 17/04 15:40 dolio: very nice 17/04 15:40 not X := X -> False  is a very interesting type 17/04 15:40 can I read False as Absurdity as well? 17/04 15:41 < and > and such can either be defined inductively, or recursively. 17/04 15:41 I guess, inductively only if you have inductive families. 17/04 15:41 i had a brainwave regarding atomic/base types 17/04 15:42 fax: you said that it was syntax all the way down 17/04 15:42 i believe that is only strictly true for atomic types 17/04 15:43 what's an atomic type? 17/04 15:43 base type 17/04 15:43 built-in type 17/04 15:43 an irreducible type 17/04 15:44 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 well . you need the lambda calculus, which means that forall and * are built in 17/04 15:44 but you can now define everything like =, true, false, and, or, not, N, Z, Q, R etc. 17/04 15:45 exists 17/04 15:45 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 exists? surely not ... 17/04 15:46 = is a connective, not a type 17/04 15:47 and surely the function type is built-in ??? 17/04 15:47 I'm not sure you can define R, unless you don't really care about having redundant elements. 17/04 15:48 dolio: for a constructivist R is a fiction 17/04 15:48 with a strict ITT, R is impossible I'd say 17/04 15:48 I'm thinking of a different R than you 17/04 15:49 computable reals 17/04 15:49 different R, go on I'll bite :) 17/04 15:49 fax: nice 17/04 15:49 You can represent constructive reals as something like Q -> Q. 17/04 15:49 fax: computable transcendentals like e and pi, sure :) 17/04 15:50 that's the only way I believe they exist 17/04 15:50 but the set R of all reals, not a chance 17/04 15:50 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 yeah quotient is something you cannot define interally 17/04 15:51 i think of transcendentals as machine that are unbounded in time and generate sequences of quotients, that's it 17/04 15:51 internally* 17/04 15:51 I think you can do a whole-program style transformation into the setoid stuff 17/04 15:51 but that is kind of hard .. 17/04 15:52 there is no Set of all of these machines, a least nothing meaningful imnsho :) 17/04 15:52 I'm going to a conference in may that is exploring this stuff :) want the link? 17/04 15:52 roconnor actually pointed out somewhere that the quotient R can be kind of useless. 17/04 15:52 i would believe that 17/04 15:53 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 http://www.theinfinitycomputer.com/Infinity2010/index.php 17/04 15:54 dolio: but we don't have R 17/04 15:55 hypercomputation ? 17/04 15:55 sah0s: I mean the constructive R, as specified above. 17/04 15:55 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 "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 anyway, ye've been really helpful and thought-provoking 17/04 15:59 i think it'll be years before this stuff goes mainstream though unfortunately, until then we have VB.net, ugh 17/04 16:00 that church-turing thesis is really frustrating, because there doesn't seem to be any way to prove it 17/04 16:00 there's all this... evidence though... 17/04 16:00 I guess that it is one problem which is right in both computing and physics 17/04 16:01 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 (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 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 I enjoy e non-rigorous proof but 17/04 16:03 ... that is pushing it ;D 17/04 16:03 oops, even quantum apple laptops will need batteries 17/04 16:05 haha 17/04 16:05 fax: it is amazing that it's the same model 17/04 16:09 i like the way that it breaks classical encryption but provides a QC solution as well 17/04 16:09 so it seems we don't have to change our notion of privacy and encryption 17/04 16:10 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 it's wild stuff I still haven't got my head about the basics like the deutch black box thingy 17/04 16:13 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 david deutsch is the man, the fabric of reality is an awesome book 17/04 16:14 cool I hadn't heard of it 17/04 16:14 you should check out peter morris' PhD once you have got your legs 17/04 16:15 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 fax: will do, in fact I'll have a quick look right now 17/04 16:16 nottingham again, what's in the water in nottingham? 17/04 16:17 lol 17/04 16:17 Epigram looks wild 17/04 16:17 2 dimensional syntax, bizarre 17/04 16:17 yeah Epigram is really exciting - I am still struggling to understand the theory of it a bit 17/04 16:17 conor mcbride's writing is hilarious 17/04 16:17 doesn't seem too different from agda 17/04 16:18 i don't use emacs though so ... 17/04 16:18 thanks again for all your help, see you 17/04 16:24 is there a statically-typed language where I can play with capability types? 17/04 16:39 Mathnerd314 - what are they? 17/04 17:52 capabilities - stuff where I can say that "you can do this" or "you cannot do this", reified into types 17/04 17:53 do you know any intro paper on it? 17/04 17:57 something that describes important bits of it in a simple way 17/04 17:57 hmm... wait a bit 17/04 17:59 http://www.cs.st-andrews.ac.uk/~eb/drafts/icfp09.pdf 17/04 18:06 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 "but you can add others (parametricity?) without spannering up the engines" 18/04 21:06 so you can't derive parametricity internally? 18/04 21:06 (I think it should be provable for a universe but was not sure about the general case) 18/04 21:07 I don't know of any type theory that can derive parametricity internally. 18/04 21:07 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 it's just this desc throws me off a bit 18/04 21:09 oh yes? :) 18/04 21:09 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 Which you normally lose. 18/04 21:10 ah 18/04 21:10 Then again, one might wonder if that doesn't doom it to failure immediately. 18/04 21:13 well having a data type of all the syntax of the language (with an interpretation) would certainly prove false 18/04 21:13 Because inductive types include strong sums, and strong sums in an impredicative universe yield inconsistency (as I recall from Luo). 18/04 21:14 (which is why being able to make a data type of all data types was such a surprise to me) 18/04 21:14 I'm not sure I understand that about the strong sums 18/04 21:15 what about exists in coq? which is in prop 18/04 21:16 Yes. They avoid the problem by not allowing strong elimination into Type or something. 18/04 21:16 oh I see 18/04 21:16 hm 18/04 21:17 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 what about this http://coq.inria.fr/stdlib/Coq.Logic.Description.html ? 18/04 21:18 But making use of that requires strong elimination fst [Prop, _] = Prop : Type. 18/04 21:18 Check the elimination principles for it. 18/04 21:19 The one that eliminates into Type is weak, I think. 18/04 21:19 Anyhow, I'm kind of taking Luo's word for this. 18/04 21:20 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 I'm sure it's true I just don't understand it 18/04 21:20 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 oh I see 18/04 21:40 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 pigworker - you write so well! I wish I could 18/04 21:47 fax: thanks, it's years of practice; I write to perform 18/04 21:49 21:00 < hpaste>  parametricity -> induction (dolio)  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24938 18/04 22:01 if the bot could tell the difference between haskell and agda we could get that in here 18/04 22:01 dolio - I don't understand this P : ⊤ → Set 18/04 22:03 why T rather than just P : Set? 18/04 22:04 oh wait T means it's a functor 18/04 22:04 Why P : Nat -> Set instead of P : Set? 18/04 22:06 but Nat is not initial and I think T is? 18/04 22:06 i.e. T -> Set ~ Set 18/04 22:07 The induction principle essentially expresses that if t : T, then t = id. 18/04 22:07 You can derive that with P t := t = id, even. 18/04 22:09 induction (\t -> t = id) refl : (t : T) -> t = id 18/04 22:10 Huh, EPTS with the 'proof irrelevant' rule lets you prove K. 18/04 22:30 EPTS ? 18/04 22:31 Erasure pure type system. 18/04 22:31 oh 18/04 22:32 "The technical means by which realizability is internalized is called ultra Σ-types." 18/04 23:29 what's that from? 18/04 23:31 Nathan Mishra-Linger's thesis. 18/04 23:31 Irrelevance, Polymorphism and Erasure in Type Theory 18/04 23:31 cool 18/04 23:31 Ultra Σ-types are someone else, though. He's just describing them. 18/04 23:32 they sound scary 18/04 23:32 You mean awesome? 18/04 23:33 There are things out there called "very dependent types". They should have chozen a zazzier name. 18/04 23:33 Like mega dependent types. 18/04 23:33 lol 18/04 23:34 Or quantum dependent types. Quantum is always good. 18/04 23:35 Take it before someone else does. 18/04 23:35 --- Day changed Mon Apr 19 2010 so what's the most powerful type system ever invented? 19/04 01:04 food! 19/04 01:06 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 I'm thinking inconsistent type systems are weak, because they're equivalent to untyped systems 19/04 01:07 you probably need to define 'powerful' 19/04 01:38 What do you mean equivalent to untyped systems? 19/04 01:52 I don't think it's an interesting question 19/04 02:00 there's always a more powerful system 19/04 02:01 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 So, apparently, in the irrelevant EPTS, you can add axioms to the 'propositional' fragment of the language. 19/04 02:15 Via something like: axiom : Squash P ; axiom = poof. 19/04 02:16 P being the proposition you want to add. 19/04 02:16 So, say, ext : Squash ((forall x. f x = g x) -> f = g). 19/04 02:17 Which seems somewhat similar to OTT. 19/04 02:17 Huh, you can interpret computationally-irelevant pi as an intersection. 19/04 03:45 yeah that's Coq* innit 19/04 03:47 Coq*? 19/04 03:47 I'm still looking at the thesis I was reading earlier. 19/04 03:47 The Implicit Calculus of Constructions 19/04 03:48 Oh, yes. 19/04 03:48 It makes sense, but I hadn't thought of it. 19/04 03:49 Since any term with type (x : A) => B[x] gets extracted from /\x. M to just a suitably erased M'. 19/04 03:50 So M' must be a single term that inhabits all B[x], so to speak. 19/04 03:51 I need to figure out how to implement inductive types (families). 19/04 03:53 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 in the last 6 hrs or so 19/04 05:54 None. 19/04 05:54 phew 19/04 05:54 I just had a sense of "oh shit, I'm so far behind... what am I /doing/ here??" 19/04 05:54 OK, what should I be reading if I do want to understand more of it? 19/04 05:56 The stuff I was talking about was mostly a thesis that I mentioned at some point. 19/04 05:59 Where'd I leave off? "None."? 19/04 06:03 at some pount. 19/04 06:03 Okay. 19/04 06:03 Parametricity you can read about in the Wadler paper, Theorems for Free! 19/04 06:04 There are also others. It goes back to Reynolds, but his papers might be harder. 19/04 06:04 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 And if you don't know about pure type systems, you should read about those first. 19/04 06:05 The thesis has a lot more stuff, though. Like, it considers languages with Agda-like inductive types. 19/04 06:06 cool, thanks for that 19/04 06:06 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 Oh, and the epigram blog. 19/04 06:08 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 no need, i have enough to keep me busy 19/04 06:10 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 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 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 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 Yeah, at least if you know something like Haskell, Agda is pretty easy to edge your way into. 19/04 06:16 edwinb: is Idris a sound logical system? 19/04 14:38 roconnor: No. At least not at the moment. It has Set:Set... 19/04 14:43 So I wouldn't recommend going and proving anything in it... 19/04 14:44 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 or if Set:Set is really used in a mathematical Prelude (maybe it is used for generic programming or something). 19/04 14:45 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 aspects, rather 19/04 14:46 it probably wouldn't be so hard to add a flag that did that 19/04 14:47 well, that's also the excuse that Epigram has as well 19/04 14:47 and it is totally reasonable 19/04 14:47 Epigram 2 will do it right in the end 19/04 14:47 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 Indeed. I wouldn't recommend trying that... 19/04 14:49 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 Fermat's Last Theorem probably doesn't need that many universes to prove it. ;) 19/04 14:50 I would think of that flag as meaning, "Right, I've finished this program now." 19/04 14:50 During development, it's useful to cheat! 19/04 14:50 edwinb: do you use Set:Set for your generative programming 19/04 14:52 I don't think I've ever used anything more than Set1 19/04 14:52 that's what I figured 19/04 14:52 er 19/04 14:52 is Set1 the smalles set, or is there a Set0? 19/04 14:52 that would be assuming Set : Set1 19/04 14:53 ah 19/04 14:53 ok 19/04 14:53 anyhow 19/04 14:53 thanks for the info 19/04 14:54 just read logs... 19/04 16:13 universe polymorphism is currently in the spotlight for us 19/04 16:15 I'm glad you're doing it so I don't have to... 19/04 16:20 although I've been writing C most of today, so maybe you'd say the same thing 19/04 16:21 very probably 19/04 16:27 I wish I knew what Agda's actual universe rules were. 19/04 16:30 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 The BUILTINs for Cons and Nil make me think that there is some syntax for list literals 19/04 18:21 but I'm having trouble tracking it dow 19/04 18:21 n 19/04 18:21 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 Which is likely more efficient. 19/04 18:24 Isn't that where the COMPILED_DATA pragmas come in? 19/04 18:25 That allows you to hack it in yourself if it doesn't have specific support. 19/04 18:25 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 But, for instance, using the BUILTIN pragmas for naturals means that Haskell's Integer is actually used. 19/04 18:26 I don't see them going any further 19/04 18:26 I thought that the BUILTIN was how you got integer literals int he syntax 19/04 18:26 like how the buILTIN refl and eq where how you bound the rewrite syntax 19/04 18:26 It does that, too.l 19/04 18:26 Builtin stuff for equality is important for the trustMe thing, too, I think. 19/04 18:27 OK, I see that "ToTerm" is the typeclass "From Agda term to Haskell value" 19/04 18:27 OK, so list literals are  (a :: b :: c :: []) 19/04 18:29 just making sure :) 19/04 18:29 Is the source code currently the best place to find out about those things? 19/04 18:30 Well, it's possible it's on the wiki somewhere, but I didn't know where to point you. 19/04 18:33 Sometimes it seems unfortunate that Agda 2 shares its name with Agda 19/04 18:36 It is easy to find irrelevant, but promising hits on google 19/04 18:36 I don't really know what's going on with agda 19/04 18:37 I thought it was a research/exploration language 19/04 18:37 but everyone is treating it like it's not 19/04 18:37 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 Ulf's thesis being titled "towards a practical programming language..." 19/04 19:00 I tend to think of it is just that - a step on the way 19/04 19:00 and pretty much the best one out there so far for doing experiments in 19/04 19:01 so lots of academics do lots of cool things in it 19/04 19:01 --- Day changed Tue Apr 20 2010 it seems like it'd be easier to work with PHOAS if you can use parametricity in your proofs 20/04 05:45 does somebody knows proof irrelevance? 20/04 16:07 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 http://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs 20/04 16:20 The type checker is there. 20/04 16:20 dolio: I'll have a look, thanks. 20/04 16:20 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 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 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 My suspicion is that nailing that could make things easier. We're having a crack at it. 20/04 16:28 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 Rather than actual cumulativity rules in the type system like, say, Coq. 20/04 16:29 gio123: I've been experimenting with proof irrelevance 20/04 16:29 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 list 20/04 16:33 oops 20/04 16:33 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 that desc thing is polymorphic though 20/04 16:35 I mean 20/04 16:35 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 Well, if I understand the situation, you have Desc : Set, and forall T : Set. exists d : Desc. Mu d = T. 20/04 16:41 Except, perhaps, T = Desc. 20/04 16:41 Of course, there's probably no proof of that statement in the language, since that'd be type-case. 20/04 16:42 Actually, that may still be too strong. Desc only describes inductive types (and IDesc inductive families). 20/04 16:43 At the moment, the actual Epigram 2 implementation exploits the collapse, but we also have a stratified Agda model. 20/04 16:46 The descriptions of level n inductive families are a level n+1 inductive family. 20/04 16:47 Ah. 20/04 16:47 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 but what about -> and forall? 20/04 16:50 fax: IDesc is closed under Pi 20/04 16:50 Is that new? 20/04 16:51 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 im confused :) 20/04 16:53 would you have say,  forall (A : *), A -> A : IDesc Zero  ? 20/04 16:53 oh I guess it's just something along the lines of  pi \A -> pi \a -> var (fs fz) 20/04 16:54 should have written   forall (A : IDesc Zero), A -> A : IDesc Zero  perhaps 20/04 16:55 no I am definitely confused 20/04 16:55 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 'Pi Set \ A -> 'Pi A \ a -> 'Const A 20/04 16:59 but it's not really satisfying 20/04 17:00 does this mean you can quote anything? 20/04 17:01 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 everything* 20/04 17:01 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 oh okay 20/04 17:02 the former needs some sort of syntax with binding; the latter needs induction-recursion 20/04 17:03 Ah! So that's how you do induction recursion. 20/04 18:55 hm? 20/04 19:02 pigworker said that inspecting the domain of a Pi requires induction recursion. 20/04 19:03 So presumably that's at least part of how you do induction-recursion with something like Desc. 20/04 19:03 there's some noteson http://www.cs.chalmers.se/~peterd/papers/inductive.html 20/04 19:05 I think this will be the same kind of thing 20/04 19:05 I guess it'd make sense that he'd be working on it. 20/04 19:06 So many people's publications to read. 20/04 19:06 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 is often amused when authors refer to themselves by name in academic papers. 21/04 01:46 :) 21/04 01:47 * binki wishes people used /me properly :-p 21/04 01:47 dolio wasn't broadcasting an action. He was speaking a sentence. 21/04 01:47 I forgot that /me doesn't work well with passive sentences 21/04 01:48 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 Which I suppose is hard to avoid. 21/04 01:49 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 this is cool ^ 21/04 01:50 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 I could find very little about induction-recursion 21/04 01:51 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 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 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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.6695 21/04 01:58 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.6101 21/04 02:00 second one is the one I really meant 21/04 02:00 dolio: Bob Dole does not agree, Bob Dole 21/04 03:42 should Data.Rational take a really long time at 100% cpu to load? 21/04 19:38 Have you loaded it before? 21/04 19:40 The first time you load it, it compiles lots of other module with lots of proofs. 21/04 19:40 I haven't 21/04 19:40 ah, thanks, many things it did compile :) 21/04 19:45 Yeah, it has to check all the stuff for coprimality. 21/04 19:49 And the Euclidean algorithm. 21/04 19:49 it's really slow to use, too 21/04 19:49 So, rewrite is really handy. 21/04 19:49 I remember I was testing basic arithmetic on rationals and it took tens of seconds to normalize simple expressions 21/04 19:49 I wonder what happened to the Rational improvements NAD mentioned 21/04 19:49 it's frustrating 21/04 19:50 ...waiting for quotients 21/04 19:50 * Saizan wonders if they work fine in Epigram 2 21/04 19:52 I think they do 21/04 19:53 how do you get ÷? 21/04 19:56 I looked through the input.el but couldn't find it 21/04 19:56 Put that in the buffer, move the cursor over it, and type C-u C-x = 21/04 19:57 ah, thanks 21/04 19:57 Is "abstract" as it pertains to modules documented somewhere? somewhere on the wiki or a paper, perhaps? 21/04 22:58 Induction-recursion is pretty wild. 21/04 23:46 oh yeah ? 21/04 23:48 Yes. 21/04 23:49 I only really know what it is and some basic examples.. 21/04 23:49 I think I have what is essentially an embedding of my little type theory with (agda-style) universe polymorphism. 21/04 23:49 And it fits entirely in Set. 21/04 23:50 :o 21/04 23:50 I don't get it :) 21/04 23:50 how is that possible 21/04 23:50 What you do, is have couple of universe formers. 21/04 23:51 FormU : (U : Set) (T : U -> Set) -> Set ; FormT : (U : Set) (T : U -> Set) -> FormU U T -> Set 21/04 23:51 Which are defined via induction recursion. 21/04 23:51 So, that lets you iterate the formation of universes. 21/04 23:52 You can then have U : Nat -> Set and T : (n : Nat) -> U n -> Set. 21/04 23:52 those two are functions? 21/04 23:52 U and T are. 21/04 23:53 Mutually defined. 21/04 23:53 okay 21/04 23:53 thye needn't be mutually defined though? 21/04 23:53 or is it essential that they are 21/04 23:53 I think it is essential. 21/04 23:53 then I am not sure what is going on 21/04 23:53 FormU is both a value and a type? 21/04 23:54 FormU is a datatype. 21/04 23:54 oh is FormT a type as well? 21/04 23:54 I was reading these as constructors 21/04 23:54 Yes. FormU and FormT are types, defined via induction-recursion. 21/04 23:55 ok 21/04 23:55 Then U and T are defined via mutual recursion afterward. 21/04 23:55 wow this is confusing :))) 21/04 23:55 how did you come up with this? 21/04 23:55 Then you define an inductive-recursive universe that internalizes the entire hierarchy. 21/04 23:55 can you interpret it? or is that not even needed 21/04 23:56 It's just me fiddling with stuff I read in one of the Dybjer papers. 21/04 23:56 I think I get it but that is pretty wild I agree 21/04 23:57 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24994#a24994 21/04 23:58 There's a snapshot. 21/04 23:58 --- Day changed Thu Apr 22 2010 but how is that in Set?? 22/04 00:02 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 how do I do something like  forall T : *, T -> T  ? 22/04 00:07 I tried T (π υ \ u -> π (τ u) \ x -> τ x) but that doesn't work 22/04 00:08 Your type is forall T : *, forall X : T, X 22/04 00:11 The last bit should be \tau u. 22/04 00:11 FF : T 1 (Π 1 υ \T -> Π 1 (τ T) \T -> τ T) 22/04 00:11 this seems closer but not it 22/04 00:11 That's the same type. You're capturing the T. 22/04 00:12 doh 22/04 00:13 okay yeah that works now thanks 22/04 00:13 As for how this fits in Set, it's because induction-recursion is crazy. 22/04 00:16 im really confused by this :p 22/04 00:17 Essentially, Luo defines all his universes in UTT via induction recursion. 22/04 00:17 And it's equivalent to ECC + inductive types. 22/04 00:17 And LF, the meta-theory, essentially only has Set. 22/04 00:18 So, by accepting inductive-recursive definitions, Agda's Set is just as powerful (minus the impredicativity). 22/04 00:18 e : Set 22/04 00:19 e = T 1 (Π 1 υ \T -> Π 1 (τ T) \_ -> τ T) 22/04 00:19 FF : e 22/04 00:19 FF = \T t -> t 22/04 00:19 that works 22/04 00:20 e : Set 22/04 00:20 e = forall (T : Set) -> T -> T 22/04 00:20 FF : e 22/04 00:20 FF = \T t -> t 22/04 00:20 that breaks 22/04 00:20 of course T in the first FF can't be anythingin Set, it can only be ℕ, ⊥ or ⊤ 22/04 00:21 but those are still sets 22/04 00:21 (oh maybe it can even be some pi, sigma, w, + thing if it wants) 22/04 00:21 The second one breaks because e : Set1. 22/04 00:22 the first one should break too :S 22/04 00:22 for the same reason 22/04 00:23 how come this doesn't introduce inconsistencies? 22/04 00:23 The first type is in the inductive-recursive universe analogous to Set1. 22/04 00:23 U 1 22/04 00:23 but U 1 : Set! 22/04 00:23 Yes. 22/04 00:24 Set contains an infinite hierarchy (and beyond) of nested universes within itself. 22/04 00:24 But all of those universes are in Set. Set1 is not such a universe. 22/04 00:24 I can't see why this works 22/04 00:25 you can have a code for any Set in there, so..... oh! 22/04 00:25 you can have a code for any set in there _except_ the one you are defining 22/04 00:25 (U) 22/04 00:26 er 22/04 00:26 Ξ U T 22/04 00:26 not U 22/04 00:26 you can only put a different Ξ inside it, I think I understand why this works now 22/04 00:26 U 0 : U 1 : U 2 : U 3 : U 4 : ... : Uinf : Set : Set 1 : Set 2 : ... 22/04 00:26 Something like that. 22/04 00:27 that is so cool 22/04 00:27 I wonder how this is proved to be acceptable 22/04 00:27 then again I can't even understand how basic dependent types normalization works 22/04 00:28 so I don't think I have much hope of this 22/04 00:28 Dybjer gives a pretty intuitive argument. 22/04 00:29 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 So it's still predicative. 22/04 00:31 oh I meant induction recursion in general 22/04 00:31 Right. U and T could be any arbitrary inductive-recursive definition. 22/04 00:32 Universes are just a go-to example. 22/04 00:32 I guess well-formed ordinals would be a simpler example. 22/04 00:33 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 *nod* 22/04 00:35 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 I think Dybjer has set theoretic models and stuff, too. 22/04 00:36 If you trust set theory. 22/04 00:36 Set theory + Mahlo cardinals, apparently. 22/04 00:38 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 but I am terrified of them :D 22/04 00:40 Why is subtraction on the naturals written as "∸"? What is the significance of that operator? 22/04 00:52 I'm not sure. Maybe because zero - n = zero isn't what you'd expect from standard subtraction. 22/04 00:53 (Unless n = zero, of course) 22/04 00:53 we need a pastebin that actually runs agda --html on a given input and which has the standard library included 22/04 00:54 Totally. 22/04 00:54 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 If only someone here had written a Haskell pastebin or something. 22/04 00:55 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 are there some {-# OPTIONS ... #-} that could be dangerous? 22/04 00:56 Conceivably, actually. 22/04 00:56 I'm not sure how much --html runs, but there are pragmas to access arbitrary Haskell, which probably includes IO. 22/04 00:56 hmm 22/04 00:57 You'll have to ask the mailing list for a definitive answer, though, I think. 22/04 01:00 But if there's no haskell to link to inside the pastebin..? 22/04 01:02 Oh, that's true. I guess you may not need ghc installed to run the agda executable. 22/04 01:04 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 Type checking in a dependently typed language requires normalizing arbitrary terms. 22/04 01:07 So if you do import unsafePerformIO, you can make it happen during type checking. 22/04 01:07 It's important to have some denotational model of dangerous things, though. 22/04 01:09 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 doesn't that depend how you do IO though? 22/04 01:09 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 Yeah, no open-term FFI! 22/04 01:10 I have a DSL for FFI too ;) 22/04 01:10 naturally 22/04 01:11 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 Even if you do, it can't reduce... 22/04 01:12 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 since it needs the IO to actually happen before it can 22/04 01:13 Oh, I see. 22/04 01:13 IO is just a description of what will happen when you're in a position to do it 22/04 01:13 Kind of like pigworker's "add fix to the language, but have it opaque during type checking" idea. 22/04 01:14 edwinb: possibly with a quotient, relating equivalent things you're not going to do just now 22/04 01:15 mm 22/04 01:15 Anyway, I was going to bed an hour ago. Better late than never. 22/04 01:15 edwinb: it'd be a bonnus if we could do it 22/04 01:15 night ;) 22/04 01:15 I once saw a lovely talk by Tarmo about monadic packaging of general recursion, but where are the slides? 22/04 01:18 I have them somewhere, I think. 22/04 01:18 the inert fix idea is the monad (Reader (forall a. (a -> a) -> a)) 22/04 01:19 but there are more subtle monads which do a better job 22/04 01:19 Ah, I hadn't thought of it like that. 22/04 01:19 Maybe I don't have the slides you're thinking of. 22/04 01:19 here's a version http://www.ioc.ee/~tarmo/tday-veskisilla/uustalu-slides.pdf 22/04 01:21 Ah, these aren't the ones I was thinking of. 22/04 01:22 I can't find them. I'm sure they included a function called unsafePerformVenanzio. 22/04 01:22 Heh, well, I definitely don't recall that. 22/04 01:23 or maybe that was just a joke in the room at the time 22/04 01:23 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 I rather worry about whether that sort of thing could ever be efficient. 22/04 01:26 Abstracting over a mythical fix just disables computation completely. 22/04 01:26 The termination proof gets nuked at closed-term run time. 22/04 01:27 Wrapping all your recursive calls and such in boxes doesn't seem like it'd be free. 22/04 01:28 Not to mention racing combinators and such. 22/04 01:28 On open terms, it's not free. 22/04 01:28 Now, I always asked these guys for the API, and they always wanted to give me the model. 22/04 01:29 I don't really want to implement the monad that way, although I do want it to have a model. 22/04 01:30 Yeah. 22/04 01:31 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 At least if you want to write normal corecursive functions in the language. 22/04 01:32 I'm not sure we should conflate total corecursion with general recursion, even if that's the model. 22/04 01:32 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 with an oracle for the recursive occurrences or "fix", would you be able to prove always-eventually properties? 22/04 01:54 i guess fix's type could give something to work with 22/04 01:54 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 goodness me, is that the time? I always eventually go to bed... g'night! 22/04 02:09 heh 22/04 02:10 Success! 22/04 02:22 Nope, failure. 22/04 02:36 the double polymorphic Pi? 22/04 02:37 Yeah. I wrote it, but almost everything gets stuck. 22/04 02:38 Because, say, if you want to use it with U n => U n, the output is U (n \lub n). 22/04 02:39 Which is n, but Agda doesn't reduce it. 22/04 02:39 So, like, an identity schema has a type in U (suc n \lub n \lub n). 22/04 02:40 Which isn't ideal. 22/04 02:40 Goes to show you the kind of magic that Agda's universe polymorphism does behind the scenes, I guess. 22/04 02:41 and you're not even required to prove l \lub l = l 22/04 02:45 Well, I mean, I could prove that here, but I'd have to go around sticking subst everywhere. 22/04 02:46 So, what agda does is use it as an extensional reduction rule, essentially. 22/04 02:47 i'm talking about the \lub one gives to Agda for --universe-polymorphism 22/04 02:47 I guess it's not extensional if it's used as a reduction rule. 22/04 02:48 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 For instance, Agda (although I guess they're trying to cut down on unnecessary eta expansion). 22/04 02:52 maybe they are used to Coq? 22/04 02:55 (which doesn't do eta-expansion i think) 22/04 02:55 cut down on eta expansion? :o 22/04 03:08 like a performance optimiasation that produces the same results? 22/04 03:08 Yes. Eta is apparently part of why Agda uses so much memory. 22/04 03:08 yeah Coq doesn't do any type directed conversion 22/04 03:08 (which is too bad!) 22/04 03:08 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 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 I think eta covers the records too 22/04 03:10 Yes. 22/04 03:10 I mean that's the whole reason to define things as records as I understand it 22/04 03:10 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 Hmm, I don't think I can make Desc work right in my universes. 23/04 04:38 you are really pushing this it's cool 23/04 04:51 what's the prbolem with Desc though, and di you try simpler ones like REG & SPT first? 23/04 04:51 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 mu : Desc U T -> U ; T (mu d) = Mu d 23/04 04:58 And arg : (s : U) -> (T a -> Desc U T) -> Desc U T 23/04 05:04 you define it normally (in Agda), then just put codes for it in the Universe? 23/04 05:06 or were building it into the universe? 23/04 05:06 Well, the problem with that is that a normal Desc in Agda (codes for Sets) needs to go in Set1. 23/04 05:07 Which would put all my universes in Set1, at least. 23/04 05:07 And might cascade into not working again. 23/04 05:08 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 But, because it's not directly part of the inductive-recursive definition, it fails. 23/04 05:09 Maybe I'm wrong, though. 23/04 05:10 oh yeah I see what you mean about Set1 that's true... hmm 23/04 05:11 Hmm, T doesn't termination check, either. 23/04 05:37 Could anyone recommend a place to read about formulating category theory in intuitionistic type theory? 23/04 06:33 Are you familiar with formulating stuff like algebra in it? 23/04 06:38 Actually I only know the basics 23/04 06:40 Well, I'd recommend finding something on dependently typed records. 23/04 06:42 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.9569&rep=rep1&type=pdf 23/04 06:43 by the way 23/04 06:43 Something like that. 23/04 06:43 I am not sure anyone knows how to do algebra or category theory in dependent types yet 23/04 06:43 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 dolio: thanks, I'll take a look at that 23/04 06:44 There's also some category theory people working on founding it more constructively. 23/04 06:45 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 Which, via Curry-Howard, intuitionistic type theory is rather like higher-order logic with dependent sorts. 23/04 06:47 But, I haven't gotten around to reading the thing yet, so I don't know much about it. 23/04 06:47 Agda needs to get sum indexed induction-recursion. 23/04 08:38 That would make some of my stuff nicer. 23/04 08:39 Heh, apparently Agda 1 had some kind of indexed induction-recursion. 23/04 08:42 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 these Acc proofs are bending my brain... 23/04 19:24 Perhaps I'm trying to use the wrong < definition? 23/04 19:25 I've tried writing something like that before, and found it quite difficult. 23/04 21:19 huh I don't undesrtand that measure 23/04 21:25 why is Acc (bound 10) 5 rather than Acc (bound 10)? 23/04 21:25 oh, I'd be happy with forall x. x < 10 -> Acc (bound 10) x 23/04 21:26 I was just starting with something more concrete :) 23/04 21:26 no  I don't understand what you are doing 23/04 21:26 I mean what about Acc (<)? 23/04 21:27 that only works for chains /down/ to 0 23/04 21:27 isn't that useable in the same way? 23/04 21:27 oh! 23/04 21:27 I want chains /up to/ a bound, say 10 23/04 21:27 well maybe you could prove  Acc R -> Acc (Ronf) 23/04 21:28 and have f(n) = bound - n 23/04 21:28 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 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 and then have a function that took them up to a bound... 23/04 21:32 That's pretty much why I was trying to do the proof, too. 23/04 21:38 Never finished, though. 23/04 21:38 I think my way with the subtract seems pretty good 23/04 21:39 --- Day changed Sat Apr 24 2010 dolio? 24/04 00:21 what about defining category theory in this inductive-recursive way? 24/04 00:21 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 I should probably do an experiment 24/04 00:22 fax: Universe polymorphism is the typical solution to that, but perhaps induction-recursion can also help. 24/04 01:21 well I had to make everything indices instead of fields to do it with polymorphism 24/04 01:22 so it should be interesting to see if it can be done just as fields with ind-rec 24/04 01:22 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 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 In a sense. 24/04 01:26 yes! 24/04 01:28 that sounds great! 24/04 01:28 the object language being the language of categories? 24/04 01:28 I was thinking more like the object language being a dependent type theory with universe polymorphism. 24/04 01:29 but we already have one 24/04 01:29 this wont work will it? 24/04 01:29 But it's conceivable that you could do category theory directly. 24/04 01:29 I'd have to actually think about it. :) 24/04 01:30 I've kind of been wondering how much of set theory induction-recursion lets you formalize. 24/04 01:37 Like, impredicativity lets you formalize something close to ZF, as I recall. 24/04 01:37 I don't actually know what set theory induction-recursion means 24/04 01:41 I am not sure I've ever seen this 24/04 01:41 Well, I think the Dybjer papers give models of it in ZF + mahlo cardinal. 24/04 01:42 But I don't actually know what a Mahlo cardinal is. 24/04 01:42 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 http://www.e-pig.org/epilogue/?p=497 24/04 17:31 http://www.youtube.com/watch?v=IFACrIx5SZ0 24/04 17:33 what? how do monkeys paddling canoes have to do with Epigram? 24/04 19:02 Mathnerd314: I'm not sure what spies would use .45mm 'questioners' either 24/04 22:34 usually those tend to be in inches 24/04 22:34 * Mathnerd314 checks to ensure date is not April 1 24/04 22:37 yep... 24/04 22:37 Is there anything written up specifically comparing Epigram and Agda? 24/04 22:56 I'd also like to see such a thing. 24/04 23:00 the main difference is that agda is intuitionistic but epigram is based on observational type theory 24/04 23:01 agda is still changing (a lot though), and of course epigram is changing faster 24/04 23:02 the main difference (from my point of view ..) 24/04 23:02 did you mean intensional rather than intuitionistic? 24/04 23:02 yes that's what I shoul dhave said, thanks 24/04 23:03 they're both intuitionistic 24/04 23:03 also, Epigram seem to aim at making the user define its datatypes from within the theory, using an universe 24/04 23:04 currently the Mu and Nu fixpoints are external from the universe though 24/04 23:05 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 Desc {n} : Set {suc n} 24/04 23:11 Desc {n} is descriptions of datatypes over Set n 24/04 23:11 D : Desc {n} ==> Mu D : Set n 24/04 23:12 one great thing in epigram is quotient types I think that will be really useful 24/04 23:12 dolio: there's a whole collection of those models, rather :) 24/04 23:12 I usually see extensional as the opposite to intensional, what is observational? 24/04 23:13 glguy it's sort "best of both worlds" :D apparently 24/04 23:13 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 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 You'd probably only use Desc and the like for generic programming. 24/04 23:13 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 glguy: Well I think OTT makes use of that type-directed stuff and pushes it even further 24/04 23:14 glguy: Both intensional and extensional type theories treat judgmental/definitional equality as linked with the equality datatype. 24/04 23:15 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 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 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 though it's still substitutive 24/04 23:18 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 I tried to implement OTT but got completely confused & stuck 24/04 23:19 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 Like (forall x. f x == g x) -> f == g for functions. 24/04 23:21 Or bisimulation for coinductive types. 24/04 23:21 it's a shame that equality is not built in! but I will get over it 24/04 23:22 I was so excited to learn about defining eq as a data type 24/04 23:22 (when I started to learn about coq) 24/04 23:22 wait I mean that it IS built in 24/04 23:22 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 (And of course, equality for quotients is whatever equivalence relation by which they're quotiented.) 24/04 23:25 I have a paper here that has a type theory with multiple equalities... 24/04 23:26 Intensionality, Extensionality and Proof Irrelevance in Modal Type Theory 24/04 23:27 Pfenning? 24/04 23:27 Yes. 24/04 23:27 It's a lot like the erasure pure type systems. 24/04 23:27 It has three different kinds of typing judgments. 24/04 23:28 M :: A, which is more intensional than usual (only alpha equivalence). 24/04 23:28 M : A which beta-eta 24/04 23:28 And M % A which is irrelevant. 24/04 23:29 *nod* 24/04 23:29 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 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 I had fun inventing my own proof irrelevant type system but eventually realized it didn't have subject reduction 24/04 23:31 Heh. 24/04 23:31 took me a long time to notice! 24/04 23:31 but I was using modality too 24/04 23:32 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 dolio, I'm still coming to terms with this induction-recursion stuff :P 24/04 23:42 I sent an overzealous message about it to the agda list. 24/04 23:52 about what ? 24/04 23:53 well I will just read it actualyl 24/04 23:53 is there a good explanation of canonicity somewhere? particularly wrt proof irrelevance 24/04 23:53 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 Which isn't strictly positive, but it's defining a higher universe strictly by reference to lower universes. 24/04 23:55 And I thought one of the Dybjer papers was about that, but I was mistaken. 24/04 23:55 It was just about defining indexed families via induction-recursion, which Agda already allows. 24/04 23:55 huh 24/04 23:56 I didn't realize that Agda didn't have IIR 24/04 23:56 It does have IIR. 24/04 23:56 oh 24/04 23:56 I subsequently realized that my criterion was kind of ad-hoc, and not what IIR is. 24/04 23:56 It requires restrictions on the indices that aren't normally enforced for inductive families. 24/04 23:58 --- Day changed Sun Apr 25 2010 so in category theory they call ¡ gnab 25/04 04:57 ¡ : 0 --> B 25/04 04:57 --- Day changed Mon Apr 26 2010 is there a command to get the fully normalized form of a goal displayed? 26/04 01:41 C-c C-, does more normalization than is shown just by C-c C-l. 26/04 01:41 You type the former while the cursor is inside the goal. 26/04 01:42 I think it gives the fully normalized type. 26/04 01:43 except i can't input C-, on a terminal, i'll look for the function it's bound to 26/04 01:44 You can't? 26/04 01:44 Huh, I guess it just enters ,. 26/04 01:45 Weird. 26/04 01:45 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 agda2-goal-and-context btw 26/04 01:51 Saizan_: try: (global-set-key (kbd "C-c ,") 'agda2-goal-and-context) 26/04 19:03 works for me in terminals, had the same problem... 26/04 19:04 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 glguy: that's what I was talking about yesterday 26/04 19:12 if R is well founded then Ronf is too 26/04 19:12 yeah, but now I'm trying to figure out how to do it :) 26/04 19:12 you'd need to prove that first 26/04 19:12 there's a really cool paper all about this if you want 26/04 19:13 oh? 26/04 19:13 http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-57.pdf 26/04 19:14 wow, I'm just barely older than that paper :) 26/04 19:14 (the construction we've been talking about is inverse image) 26/04 19:15 thanks, I'll give it a look 26/04 19:15 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 lem f R x (WF.acc rs) = WF.acc (λ y x' → lem f R y (rs (f y) x')) 26/04 19:25 something like this? 26/04 19:25 wow that was fast 26/04 19:25 glguy, since WF is a proof -- if that type checks it's correct :) 26/04 19:26 Acc* 26/04 19:26 yeah, it type checks 26/04 19:27 I just have to figure out how to make use of it now :) 26/04 19:27 it's a bit rubbish writing out recursion using WF 26/04 19:28 that's something which would be nice as a language feature 26/04 19:28 yeah... but I want to do it today :) 26/04 19:28 like in coq you write  Fixpoint f ... {measure foo} := ... 26/04 19:28 but there isn't really anywhere to write that in the agda syntax 26/04 19:29 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 in parallel I'm doing the exercises in Agda 26/04 19:29 and I refuse to not be able to write this in Agda :) 26/04 19:29 the way you are doing it sounds a little different from 'define the function and then prove it terminates' 26/04 19:30 because the natural way to write, in agda.. is not that way 26/04 19:30 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 I know that this won't be the prettiest implementation 26/04 19:31 it might be interesting if the red gave you a proof obligation 26/04 19:32 instead of just saying _rewrite this_ 26/04 19:32 certainly interesting 26/04 19:32 That seemed to work 26/04 19:34 I got a proof that all the elements in my data type are accessible now 26/04 19:34 using the measure I defined 26/04 19:35 and Nat's allAcc proof 26/04 19:35 it works :) now all I have to do is plumb through an accumulator parameter 26/04 19:41 but the recursion structure I needed is proven to terminate using wfrec 26/04 19:41 thanks for the nudge, fax 26/04 19:41 okay :) 26/04 19:41 http://www.galois.com/~emertens/treerec/treerec.html 26/04 19:48 The preOrder function at the bottom isn't done yet but has the right recursion structure 26/04 19:48 OK, I've updated it to actually do the traversal 26/04 19:53 (if anyone is following along at home) 26/04 19:53 glguy, is this function equal to: 26/04 19:55 pre (leaf y :: xs) = [y] ++ pre xs 26/04 19:55 pre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y0 26/04 19:55 ? 26/04 19:55 oops! 26/04 19:55 ++ pre xs  to both 26/04 19:55 oh no I got it on the first, just add it to the second line 26/04 19:56 pre (leaf y :: xs) = [y] ++ pre xs 26/04 19:56 pre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y0 ++ pre xs 26/04 19:56 pre [] = [] 26/04 19:56 yup, looks about right 26/04 19:56 I wanted to write it using only tail calls 26/04 19:56 ah! 26/04 19:56 the exercise is to write it a few different ways 26/04 19:57 name your constructors and get nicer names from C-c C-c!? :-) 26/04 19:57 I'm cleaning up the names now :) 26/04 19:57 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 no cleaning up needed :-) 26/04 19:59 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 I feel like I'm lying about using them for dependent types 26/04 19:59 hehe 26/04 19:59 i name everything so i don't need to write out the arrows 26/04 20:00 I like typing \r and seeing the arrow appear :-D 26/04 20:00 when I switch from Agda back to Haskell I often get a few \r's in my code 26/04 20:00 glguy, but a -> b is just shorthand for (_ : a) -> b 26/04 20:01 I know that it doesn't change the meaning 26/04 20:01 OK OK, I've changed my constructor :-p 26/04 20:02 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 i hope nobody will drive us from the unicode paradise which Agda created for us 26/04 20:04 actually I hate unicode 26/04 20:09 :-( 26/04 20:09 I'm using LaTeX a lot recently, it's bloody awful but it's better than unicode 26/04 20:09 it's actually got support for things like super and subscripts, radicals, typefaces (very important) 26/04 20:10 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 editor 26/04 20:11 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 oh I think so! 26/04 20:16 I never used this but I've seen a screenshot 26/04 20:17 I think latex kind of sucks though, at least it's possible to do better 26/04 20:17 yeah, some here; only seen a screenshot 26/04 20:17 maybe we can't NOT use latex because it's so pervasive 26/04 20:17 that means finding a good subset 26/04 20:17 and specifying it formall 26/04 20:17 formally 26/04 20:17 as I see it, support like this would be a HUGE improvement in terms of readbility of programs 26/04 20:18 (which is important) 26/04 20:18 but it would also mean a slight increase in complexity of editors 26/04 20:18 (which is a **REALLY BAD THING**) 26/04 20:18 but I think it's unavoidable 26/04 20:18 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 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 glguy, the first thing I'd do is prove the equations that define the program 26/04 22:21 (they should all be provable by reflexivity) 26/04 22:22 fax, can you give an example of what the type of that might look like 26/04 22:39 my first attempt with something like:  lemma-leaf : ∀ a ts xs → preOrder′ (leaf a ∷ ts) xs ≡ preOrder′ ts (xs ++ [ a ]) 26/04 22:39 is proving harder than I'd have expected 26/04 22:39 preOrder′ ts xs = wfRec PreOrderPred body (ts , xs) 26/04 22:39 lemma-leaf _ _ _ = refl 26/04 22:39 doesn't work ? 26/04 22:39 no, due to the Acc proof being different 26/04 22:40 wait huh 26/04 22:40 I'll paste the goal 26/04 22:40 oh I see 26/04 22:40 http://fpaste.org/EN7d/ 26/04 22:41 what's preOrder′? 26/04 22:41 preOrder′ ts xs = wfRec PreOrderPred body (ts , xs) 26/04 22:41 okay that's preOrder in the file I am looking at 26/04 22:41 roughly 26/04 22:41 it exposes the accumulator 26/04 22:42 you could try enabling proof irrelevance 26/04 22:43 (there's a flag for it) 26/04 22:43 (I've never tried this) 26/04 22:43 because Acc has a single constructor? 26/04 22:43 I thought that proof irrelevance went away in 2.26 26/04 22:43 2.2.6 26/04 22:43 oh that's too bad 26/04 22:44 im sure I proved the equations with refl 26/04 22:44 when I used acc 26/04 22:44 .Induction.Nat._.helper 26/04 22:45 where class considered harmful 26/04 22:45 clause* 26/04 22:45 glguy: Perhaps this isn't helpful, but you'd likely prove your theorem by well-founded induction as well. 26/04 23:14 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 :) 26/04 23:24 It follows the general pattern that proving something about a function involves induction shaped like the recursion in the function. 26/04 23:25 but it was hard enough to write the function the first time :( 26/04 23:25 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 Yeah. 26/04 23:26 not some boring old \ _ -> List A 26/04 23:26 --- Day changed Tue Apr 27 2010 fax, through some form of magic... I was able to do my program as the three equations 27/04 01:07 using refl 27/04 01:07 and one rewrite (which I had to use in my definition) 27/04 01:07 cool! what magic! 27/04 01:07 well, I started with lifting the helper for Nat's allAcc out of the where clause 27/04 01:09 I don't know that that fixed it, but either I had a typo in my original attempt 27/04 01:09 or that fixed it 27/04 01:09 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 (though I will have to do it tommorow) 27/04 01:10 and I just mean for my own curiosity.. 27/04 01:10 I don't have it handy, but I'll experiment tonight to reproduce 27/04 01:10 http://www.galois.com/~emertens/treerec/treerec.html 27/04 01:11 check out the three definitions at the bottom of the file 27/04 01:11 well I am not keen on +-assoc (treeSize t₁) (treeSize t₂) (sum (map treeSize ts)) 27/04 01:11 but the other two are good :P 27/04 01:11 I wouldn't have done that if it worked without it :-p 27/04 01:11 i feel a bit lost when there's an heavy use of type synonyms 27/04 01:26 dolio, still there? 27/04 03:00 Yes. 27/04 03:00 http://www.galois.com/~emertens/treerec/treerec.html 27/04 03:00 oh, it is still uploading 27/04 03:01 refresh that in a moment 27/04 03:01 I have the WfRec implementation with all of the equations regarding how it operates on its arguments 27/04 03:01 OK, done 27/04 03:01 * glguy needs to show someone that understands what just happened 27/04 03:01 with all of the equ-* functions I should be able to prove equivalence to a simpler implementation now 27/04 03:03 pulling the implementations of those functions out of the where clause allows the simplifier to do its work 27/04 03:05 otherwise they have unrelated arguments from their parent function 27/04 03:05 and it can't see the equivalence 27/04 03:05 another case of where clauses considered harmful! 27/04 03:06 it seems like the translation of where clauses could benefit from some dependency analysis then 27/04 03:09 glguy: What are you asking me about this? 27/04 03:11 Also, doesn't preorder traversal have a structurally recursive formulation? 27/04 03:12 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 sure, I'm proving equivalence to that now 27/04 03:12 Okay. 27/04 03:12 the exercise was to do a tail-recursive version 27/04 03:12 and prove that 27/04 03:12 (in Isabelle) 27/04 03:12 Ah, okay. 27/04 03:12 and I wanted to show that even if it took more keystrokes that it was doable in Agda 27/04 03:13 I think you might even be able to do a tail-recursive structurally decreasing version. 27/04 03:13 oh yeah? 27/04 03:13 Hmmm... 27/04 03:14 I'll let you know in a while. :) 27/04 03:15 Apparently not. 27/04 03:24 Unless the new --termination-depth=N flag will accept it. 27/04 03:27 What's that flag about? 27/04 03:29 It tries to be smarter about seeing arguments that grow a little, but ultimately shrink. 27/04 03:29 N is related to how deep it looks for shrinkage or something. 27/04 03:30 Well, I seem to be unable to pull from the agda repository... 27/04 03:31 "Caveat: On Tree-like data, it does not work so well." That's probably bad news. :) 27/04 03:33 ha 27/04 03:33 Well, hopefully my last checkout has --termination-depth. 27/04 03:42 OK, I did the equivalence proof, uploaded to the same URL 27/04 03:43 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 Do you think that this is worth writing up as an example for using the WfRec stuff? 27/04 03:46 seems like there isn't much on Google for examples of using the library 27/04 03:46 Sure. It's possible you're the first one using it. 27/04 03:50 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 Did you ever figure out the getting-closer-to-an-upper-bound thing for fibonaccis? 27/04 03:52 If not I might take another crack at it. 27/04 03:53 No, but  I might now that I've had a little more success using the stuff 27/04 03:53 I would encourage you to take your crack 27/04 03:53 (as I don't have confidence that I'll knock it out) 27/04 03:54 Well, --termination-depth doesn't magically solve all problems. 27/04 03:55 Did it solve some? 27/04 03:56 No. 27/04 03:56 It didn't make my attempt pass, anyhow. 27/04 03:57 Not even the simplified version that didn't worry about values at internal nodes. 27/04 03:57 I need to figure out why this proof breaks when I remove the "abstract" section 27/04 04:15 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 something about "inverse image" from the paper I was referred to earlier 27/04 06:11 "Constructing Recursion Operators in Intuitionistic Type Theory" 27/04 06:12 Well, I think I broke my agda-share darcs repository. 27/04 06:50 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25086#a25086 27/04 06:52 I succeeded in proving accessibility for k >= n > m, though. 27/04 06:52 So, go forth and write fibonacci sequences. 27/04 06:53 I knew that keeping html files in the repository would turn out badly one day. Oh well. 27/04 06:54 well, we couldn't have seen it anyhow, c.h.o webserver is currently broken 27/04 07:03 I guess that explains why I couldn't pull the latest agda earlier. 27/04 07:04 But, now I have to start over, I think. 27/04 07:04 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 So there are 45,000 changes to view. 27/04 07:04 darcs record -a ?:) 27/04 07:05 Well, there are about 12 changes I don't want to record. 27/04 07:05 And when I skip those, it just hangs. 27/04 07:05 So I suspect record -a won't be any better. 27/04 07:05 And remove html/* takes forever, too. 27/04 07:05 thanks for that code, dolio 27/04 07:12 http://www.galois.com/~emertens/treerec/treerec2.html 27/04 07:12 is my latest revision (now with less code) 27/04 07:12 I  better save your code somewhere before hpaste's takusen backend forgets to unlock the database :) 27/04 07:14 how do I find out which version of Agda I'm running? 27/04 16:15 pigworker: you mean something else than agda --version 27/04 16:16 if you installed it from cabal, your .cabal/packages folder might provide some hints 27/04 16:17 if you only have the emacs mode switch to the *ghci* buffer 27/04 16:17 near the top you'll see a like like: 27/04 16:17 Loading package Agda-2.2.7 ... linking ... done. 27/04 16:17 "ghc-pkg list Agda" will show the versions you have installed, btw 27/04 16:18 the *ghci* window hint did it for me, thanks; I don't have the standalone 27/04 16:18 Thanks guys, version mystery solved: it pays to install after a download... 27/04 16:23 heh :) 27/04 16:29 pigworker: I installed epigram yesterday :) 27/04 16:32 kosmikus: it'll be different again today 27/04 16:33 :) 27/04 16:35 hey um 27/04 16:36 http://math.etsu.edu/LaTeXMathML/ 27/04 16:36 this is kinda cool 27/04 16:36 http://www1.chapman.edu/~jipsen/mathml/asciimathcalculator.html 27/04 16:37 infact thats more relevant 27/04 16:37 I am wondering if something like this could make a good editor 27/04 16:38 rather than ascii 27/04 16:38 since you get colors, super and subscripts, typefaces, .. 27/04 16:38 (ascii + unicode) 27/04 16:38 maybe there's a plan already (for epigram ?) 27/04 16:39 fax, the problem was that the <-allAcc definition used a where-clause defined helper 27/04 16:39 the refl definitions worked once I lifted that 27/04 16:39 glguy -- does that make sense 27/04 16:39 yeah 27/04 16:39 it sounds like a bug to me 27/04 16:39 why should a where clause be any different ? 27/04 16:40 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 fax: I'm getting out of the UI business 27/04 16:40 * glguy heads in to work 27/04 16:42 http://i.imgur.com/8p6JM.png -- anyone understand that THROW rule? 27/04 17:17 I don't get why there isn't Gamma |-_T,Delta C 27/04 17:17 (I'm guessing the C just comes from nowhre0 27/04 17:17 this is from http://pauillac.inria.fr/~herbelin/publis/markov.pdf An intuitionistic logic that proves Markov's principle 27/04 17:18 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 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 Also I have trouble seeing how it's useful 27/04 18:11 so you prove T by proving T? 27/04 18:11 sort of 27/04 18:12 I mean, your context might have changed 27/04 18:12 OK, I think I have an example 27/04 18:15 Suppose you want to prove (A(x) -> B(x)) \/ C(x) 27/04 18:15 start with catch 27/04 18:15 then decide to prove the left side 27/04 18:15 and assume A(x) 27/04 18:15 now, with throw, say forget about proving B(x), and prove the original formula instead 27/04 18:16 only this time, prove the right subbranch.  Now you get to prove C(x) with the extra assumption A(x) 27/04 18:16 ah! 27/04 18:16 that makes sense 27/04 18:16 seems weird though! 27/04 18:17 so you can prove excluded middle 27/04 18:18 yes 27/04 18:18 suspicious 27/04 18:19 ah, but looking at the paper 27/04 18:19 T isn't all terms 27/04 18:19 they can't have foralls 27/04 18:19 so you can't prove \forall x . P(x) \/ not P(x) 27/04 18:20 I think? 27/04 18:21 V_I? 27/04 18:22 ? 27/04 18:23 heh, sorry, i mean using the I rule for \forall at the start, and then the catch .. throw 27/04 18:25 you'd only have to catch P(x) \/ not P(x) with x free 27/04 18:25 my guess is the freshness condition will gum up the works 27/04 18:26 but let's see 27/04 18:26 yeah, I think it does 27/04 18:28 because, in order to get anywhere, you'll have to add P(x) do your context 27/04 18:29 and then x isn't fresh enough to use that assumption after you throw back to LEM 27/04 18:29 perhaps that's what you said, I'm just very slow :) 27/04 18:29 ah, no, i didn't think about x appearing in Gamma :) 27/04 18:30 --- Day changed Wed Apr 28 2010 http://www.galois.com/~emertens/recops/recops.html 28/04 09:26 I'm starting to implement the operators from the paper that fax told me about 28/04 09:27 I wonder if some of these ways of constructing well-founded relations shouldn't be in the library 28/04 09:27 what's the name of Agda's logic? 28/04 20:03 You mean like CIC? 28/04 20:05 I'm not sure it has a name. 28/04 20:05 like CIC, or OTT 28/04 20:09 or MLT 28/04 20:09 MLTT 28/04 20:09 It's sort of grown by accretion. 28/04 20:10 Started with inductive families, induction recursion and a predicative hierarchy. 28/04 20:11 it seems to be MLTT with universes and induction-recursion 28/04 20:11 And it's since gotten codata and universe polymorphism. 28/04 20:11 ulf's thesis describes it in terms of additions to UTT 28/04 20:12 which seems a little odd, since agda lacks an impredicative Prop and its datatype eliminators are stronger than UTT's 28/04 20:12 but, so it is 28/04 20:12 I don't think they're ready to specify it formally since agda is about exploring the design spacec no? 28/04 20:16 http://www.galois.com/~emertens/recops/recops.html 28/04 21:09 now with ways to construct well-founded relations from subrelations, inverse images, transitive closures and disjoint sums! 28/04 21:09 fancy :) 28/04 21:12 have you tried epigram yet? 28/04 21:12 nope 28/04 21:13 I wasn't sure which version of it I was supposed to try 28/04 21:13 maybe rather than bombarding you guys with whatever agda I did that day I should just twitter it... 28/04 21:20 I don't object to you doing both :P 28/04 21:20 I think I already follow you on twitter 28/04 21:20 glguy, transitive closure is my favorite 28/04 21:21 That one was the most fun to work out 28/04 21:21 I had to think about what I was doing rather than just following the types 28/04 21:21 :D 28/04 21:22 you can define single step recursion and take the transitive closure to get structural recursion 28/04 21:23 single step recursion is easy to prove from the eliminator of a type 28/04 21:23 this could form the basis of an implementation of pattern matching, but there is a different approach too (Below predicate) 28/04 21:24 glguy: need more ordinal operations! :D 28/04 21:29 glguy: like multiplication, exponentiation, Veblen functions! 28/04 21:30 would love to see programs that make (essential) use of these things too :) 28/04 21:33 I don't know what roconnor is talking about but I can find out :) 28/04 21:34 glguy: you work for galois? 28/04 21:34 I have a program that makes use of the inverse image w.f. relation 28/04 21:34 roconnor, yeah, but we aren't all formal methods experts :) 28/04 21:34 who isn't? 28/04 21:35 I'm not! 28/04 21:35 glguy, on the roads though ? 28/04 21:35 but you are writing agda code! 28/04 21:35 I'm approaching Agda from the "is it a dependently-typed programming language?" side 28/04 21:36 working my way into "Is it a proof-assistant based on intuitionistic type theory?" 28/04 21:36 same thing :) 28/04 21:36 ¯\(°_0)/¯ 28/04 21:36 hheheheehe 28/04 21:37 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 I sit across from Iavor who fields most of my FM questions 28/04 21:38 glguy you should write this stuff down :P 28/04 21:38 Yeah, I considered "blogging" some of my experiences, but I don't really know what level to approach it from 28/04 21:39 don't really know what level to approach it from 28/04 21:39 oops 28/04 21:39 "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 lol 28/04 21:40 glguy: http://muaddibspace.blogspot.com/2009/03/how-to-halve-number.html 28/04 21:40 Anonymous said... 28/04 21:41 holy jesus wtf 28/04 21:41 :) 28/04 21:41 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 I also don't know what it obvious to the rest of people using Agda 28/04 21:42 or if there is even an audience 28/04 21:43 beyond say the 32 people in this channel 28/04 21:43 wow 28/04 21:44 you should use twitter more 28/04 21:44 oh yeah? 28/04 21:44 is Agda all over the Twitters? 28/04 21:44 is twitter evil or not?? 28/04 21:44 I haven't been able to figure it out 28/04 21:44 glguy: not really :P 28/04 21:45 fax: it's as evil as the people you use 28/04 21:45 I mean 28/04 21:45 actually I don't know what I meant 28/04 21:45 there are lots of haskellers and mathy people on it, if nothing else 28/04 21:45 maybe you meant that my twitter account is way out of date 28/04 21:45 how do I publicly open a module in my module 28/04 21:49 so that opening my module gives you things defined in the other module? 28/04 21:49 open ... public 28/04 21:50 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 specifically "open InverseImage ..." 28/04 21:56 what does galois do? 28/04 21:57 actually the site will tell me 28/04 21:57 yeah, the site will tell you better than I can 28/04 21:58 I always stumble along as I figure out how much detail I'm allowed to go into 28/04 21:58 man cryptol is so cool 28/04 21:58 fax, no argument here :) 28/04 22:03 fax: Twitter is potentially less evil that a lot of other 'social' sites 28/04 22:11 omg more twitter love 28/04 22:11 for many common values of evil 28/04 22:11 copumpkin: no, I still hates it, mostly :P 28/04 22:11 oh 28/04 22:11 well, more twitter less-that-100%-hate then 28/04 22:11 copumpkin: but yeah, the mathy/haskell/general nerd feeds can be fun 28/04 22:11 and shitmydadsays is quality 28/04 22:12 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 like what? 28/04 22:13 So what was that Velben function stuff? 28/04 22:13 dunno, mostly just tech news if nothing else 28/04 22:13 Veblen heirearchy 28/04 22:13 to re-plug into 28/04 22:13 I don't find tech very interesting but its nice seeing the quantum computing number of bits go up 28/04 22:14 copumpkin: I had a huge RSS reader feed. 28/04 22:14 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 maybe more 28/04 22:15 hah 28/04 22:15 I was going to switch to just reading it on the weekends 28/04 22:15 but then I just let it crash and burn 28/04 22:15 I'm gonna restrict it to a limited number of high quality sites and try again. 28/04 22:16 so. back on topic 28/04 22:16 yes has anyone figured out what agda is yet? :D 28/04 22:16 I'm behind on the 'learn at least one new language a year' resolution 28/04 22:16 one thing I'm gonna learn is OpenCL 28/04 22:16 I think Agda should be the other 28/04 22:16 * fax doesn't beleive in learning programming languages 28/04 22:16 I don't think anyone knows yet 28/04 22:17 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 there's a PhD on it 28/04 22:19 that's bookish 28/04 22:19 the agda tutorial is pretty accessible 28/04 22:19 you mean a thesis 28/04 22:19 I don't tend to say thesis since it doesn't imply it's a PhD 28/04 22:19 copumpkin: accessible with respect to which relation?? 28/04 22:21 lol 28/04 22:21 :P 28/04 22:21 fax: a PhD on it sounds like a PhD is working on it, at least to me :P 28/04 22:23 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 but thanks folks, I went to the Wiki and got some stuff to read. 28/04 22:24 Agda wiki, not The Wiki 28/04 22:24 --- Day changed Thu Apr 29 2010 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 http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25192#a25192 29/04 01:30 sounds hardcore 29/04 01:38 ah, i thought that meant you had to use well founded recursion to prove the accessibility. 29/04 01:41 Any ideas for ways to structure allAcc so that the lexicographic induction can be found to terminate? 29/04 03:15 woot, I did the proof for non-dependently typed pairs 29/04 03:46 http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#2955 29/04 03:54 That requires the constituent relations to be well founded for all elements of the type? 29/04 03:58 I don't know that it requires it 29/04 03:59 but I decided to try to prove it first assuming that they were 29/04 03:59 I'm pretty sure that's what allA and allB say. 29/04 03:59 oh, it certainly is 29/04 03:59 OK, rephrase: 29/04 03:59 My proof requires that all inhabitants of the sets A and B are accessible wrt relations R1 and R2, respectively 29/04 04:00 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 I don't think I understand 29/04 04:03 Perhaps it isn't possible to do away with the assumption that every element of B x is accessible. 29/04 04:05 (Or B, as it were.) 29/04 04:05 yeah... I'd love to generalize this to B x 29/04 04:06 (as you can see in the odule above) 29/04 04:06 Since for x < x', I can choose arbitrary y' > y, and (x' , y') \prec (x , y)... 29/04 04:06 yeah, it is the same kind of arbitrary choice you have to deal with in the disjoint sum case 29/04 04:07 But then one needs y' accessible for all the (x' , y'') < (x' , y'). 29/04 04:07 when you move from inj2 to inj1 29/04 04:07 However, it shouldn't be required that all x : A are accessible. 29/04 04:08 that is true 29/04 04:08 so I could demand an Accessibility proof for your starting 'x' valu 29/04 04:09 and use that to build the initial recursor-builder 29/04 04:10 from the Some module 29/04 04:10 I'm not sure how much that would come up in practice. 29/04 04:13 But theoretically you can have relations for which not every element of the type is accessible. 29/04 04:13 you can always just define a subset of your type that is accessible 29/04 04:13 Something like '1 < 2 < 3 < 4 < 5 < ... < 10 < 9 < 8 < 7 < 6'. 29/04 04:15 But that's pretty contrived. 29/04 04:15 well... you're still free to pick your own insane relation 29/04 04:16 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 where nothing was related to them 29/04 04:17 suggestions for proving Lexicographic.allAcc terminates? 29/04 04:20 I figured it out 29/04 08:17 http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#2236 29/04 08:17 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 glguy_: great 29/04 08:33 and along the way i got a generalized Induction.Lexicographic module 29/04 08:33 maybe some of this could go into the std lib 29/04 08:34 now you can add universe polymorphism 29/04 08:34 almost done 29/04 08:34 glguy_: I hope so 29/04 08:34 done 29/04 08:34 uploaded 29/04 08:34 (to the same link) 29/04 08:34 :) 29/04 08:34 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 however the code that I reused from Induction.Lexicographic assumed they were both at the same level 29/04 08:35 and I don't know if that was necessary or not 29/04 08:35 but it is the state of things 29/04 08:35 You should propose a patch to the stdlib 29/04 08:37 How do I do that 29/04 08:37 would it make sense to add the Data.Star operator 29/04 08:38 can't happen 29/04 08:38 reflexive relations are right out 29/04 08:38 so obvious sorry 29/04 08:38 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 rather than defining it locally here 29/04 08:39 Yep 29/04 08:40 I think there is already a definition like you DisjointSum._<_ 29/04 08:40 you*r* 29/04 08:40 oh? 29/04 08:41 just the operator, not the Acc proof? 29/04 08:41 sure 29/04 08:41 don't panic 29/04 08:41 :) 29/04 08:41 it would be OK if this work was all already done 29/04 08:41 I've had a blast working my way through it 29/04 08:41 Relation.Binary.Sum 29/04 08:42 I'd have to make it level polymorphic 29/04 08:44 but good catch! 29/04 08:44 glguy_: sure but would a nice first addition 29/04 08:45 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 I've tried to build off of the stuff in Induction where possible 29/04 08:50 or use it via Induction.Lexicographic 29/04 08:50 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 (Does that mean you are the author of these modules?) 29/04 08:52 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 how would the type of that proof look like? 29/04 15:35 Saizan: ⊥ 29/04 15:36 ah, sorry, i was referring to another quote :D 29/04 15:37 :) 29/04 15:37 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 work on that. 29/04 15:37 hum 29/04 15:37 * npouillard guessing 29/04 15:38 ∀ (A : Set) → Dec (Σ Term λ p → ⊢ ⟦ p ⟧t ∷ ⟦ A ⟧s) 29/04 15:41 Set would be the type of Set descriptions, same thing for Term 29/04 15:42 ⟦_⟧t and ⟦_⟧s interpret set and terms 29/04 15:43 shouldn't the term be an argument as well? 29/04 15:43 and ⊢_∷_ would be a typing-derivation type 29/04 15:43 otherwise that decides if a type is inhabited or not, which seems quite strong 29/04 15:44 I don't think so, it would be much weaker and only telling you that the type checking is decidable 29/04 15:44 oh, i guess i get to prove that you can't give proofs of empty types with that 29/04 15:45 "that": which one 29/04 15:46 ? 29/04 15:46 yours 29/04 15:46 yes 29/04 15:46 maybe we can just focus one this: 29/04 15:47 ¬ (∃ λ p → ⊢ ⟦ p ⟧t ∷ ⊥) 29/04 15:48 update of the previous one: ∀ (A : Set) → Dec (Σ Term λ p → ⊢ p ∷ A) 29/04 15:48 i see 29/04 15:49 and so: ¬ (∃ λ p → ⊢ p ∷ ⊥) 29/04 15:49 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 dolio: this would just say that agda is stronger the embedded theory, no ? 29/04 15:52 The intention would that the embedded theory would be Agda. 29/04 15:53 Similar to embedding Peano arithmetic in itself. 29/04 15:53 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 Unless I'm misunderstanding something. 29/04 15:54 I think we can't avoid reasoning about agda terms without proving something weaker than the consistency of Agda 29/04 15:56 where is Agda's universe polymorphism documented? 29/04 16:27 In particular, I am mystefied by the following:  (\ l -> Set l) has type (l : Level) -> Set (suc l) 29/04 16:28 but Set itself does not 29/04 16:28 So, is Set a function on levels or isn't it? 29/04 16:28 *mystified 29/04 16:29 probably the source code (if you can read it... it's pretty confusing) 29/04 16:29 ccasin: Even with universe polymorphism enabled, the token Set refers to Set 0. 29/04 16:39 Kind of an oddity. 29/04 16:39 dolio: yeah, it's a little odd, but I guess I figured that 29/04 16:40 I just sent a message to the list on this topic 29/04 16:40 I should say, the token Set when not applied to another term refers ... 29/04 16:40 So I guess it's kind of context-sensitive. 29/04 16:40 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 even for a much smaller system 29/04 16:40 Yes, it's unlike stuff I've seen elsewhere in the literature. 29/04 16:41 well, where "pretty unique" means "new to me" :) 29/04 16:41 I wrote a small interpreter for a language with similar universe polymorphism. 29/04 16:41 that's just what I'm doing :) 29/04 16:41 But I don't think I documented it any more than Agda's is. 29/04 16:42 I can't believe they pay me to sit around and write little interpreters 29/04 16:42 being a grad student is swell 29/04 16:42 http://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs 29/04 16:42 You might be able to glean the rules from that, though. 29/04 16:42 It's pretty simple. 29/04 16:42 thanks, I'll have a look 29/04 16:43 The sigma types in there are a little more powerful than what you can do in Agda. 29/04 16:43 this is interesting 29/04 16:44 it looks like, in your language "Type" doesn't have a type itself 29/04 16:44 it must always be applied to a level 29/04 16:44 Because you can't write something like "data Foo : Set \omega where foo : (l : Level) -> -> Foo". 29/04 16:44 or maybe I'm reading the haskell wrong 29/04 16:45 oh, and you add an omega level, that's nice 29/04 16:45 No, that's correct. Just like fst and snd aren't first-class. 29/04 16:45 I think agda doesn't have that, right? 29/04 16:45 cool 29/04 16:46 It might be fundamental for Type, though. I haven't really thought about it. 29/04 16:46 Type : (l : Level) -> Type (suc l) would be kind of weird, at least. 29/04 16:47 that's what I'm doing in my little interpreter 29/04 16:47 of course, who knows if it's sound 29/04 16:47 I wouldn't necessarily worry about it being less sound. More getting into a type-checking loop. 29/04 16:48 You can write \l -> Type[l] in my interpreter, for instance. 29/04 16:48 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 that's cool 29/04 16:49 so, ulf responded on the mailing list - looks like agda does the same thing as your interpreter 29/04 16:50 Yeah. 29/04 16:51 -> isn't a first-class operator in Agda, either. 29/04 16:51 Unlike Haskell. 29/04 16:51 it's odd that 29/04 16:51 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 dolio: what will lead to a looping type checker with the (l : Level) -> Type (suc l) choice? 29/04 16:54 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 I haven't thought a lot about it, though. It might be fine. 29/04 16:55 hmm, why do I need to check the type of (l : Level) -> Type (suc l)? 29/04 16:56 I think I just return that 29/04 16:56 that is, my system has as an axiom: 29/04 16:56 ---------------------------- 29/04 16:56 Type : (l : Level) -> Type (suc l) 29/04 16:56 It may well be fine. 29/04 16:57 It's not like I've tried it and had loops. 29/04 16:57 OK, cool 29/04 16:57 Type : (l : Level) -> Type (suc l) -- doesn't make sense to me 29/04 16:58 well okay I guess it's fine it looks weird 29/04 16:58 well, we seem to agree (Type l : Type (suc l)) 29/04 16:58 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 So you can actually do case analysis on the level of your function in Agda. 29/04 17:00 foo : (l : Level) -> Set l ; foo zero = Nat ; foo (suc l) = Set l 29/04 17:01 yeah, in my little interpreter I'm just building in Nats with the standard eliminator and using them for levels 29/04 17:02 Which isn't exactly 'polymorphism' in the parametricity sense. 29/04 17:02 right - it's not at all 29/04 17:02 this system seems to solve a lot of the same problems as the Harper-Pollack universe polymorphism stuff 29/04 17:03 but it's very different 29/04 17:03 and cool! 29/04 17:03 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 wasn't the Harper-Pollack thing about how to infer the levels? 29/04 17:04 oh right, I think I know what the problems were 29/04 17:04 * dolio goes to get some lunch. 29/04 17:05 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 it's just what coq has, I think 29/04 17:05 okay 29/04 17:05 in that paper, l := n | \alpha 29/04 17:06 where \alpha means "I don't know, pick something" 29/04 17:06 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 (you told me about the paper, you get to hear about the progress) 29/04 17:17 Had to extend Induction.Lexicographic to do dependently-typed lexicographic induction 29/04 17:18 eek 29/04 17:18 I never dared to think about the dependently-typed ones 29/04 17:18 it was a pretty straight forward change, actually 29/04 17:19 Lexicographic exponentiation is a really cool one 29/04 17:19 glguy, the main thing which is missing is examples -- but I think examples are really difficult to come up with 29/04 17:19 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 oh cool what was it for ? 29/04 17:20 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 I used it to write merge sort 29/04 17:22 (kind of the obvious one) 29/04 17:22 hm 29/04 17:22 that sounds like something that would be done with a measure ? 29/04 17:22 You could probably also have done measure of the sum of the lengths of the two lists 29/04 17:23 but it was pretty straight forward to do it lexicographically 29/04 17:23 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25208#a25208 29/04 17:24 I can't imagine how :/ 29/04 17:24 * glguy ^W'd the wrong application 29/04 17:24 Yay, the lexicographic and well-founded operators got added to the std lib darcs repo 29/04 20:23 wow cool! 29/04 20:27 that is good did you cite that paper in yrou code 29/04 20:28 ? 29/04 20:28 What is Nils' nick 29/04 20:28 No, but Nils did 29/04 20:28 I don't think Nils' is here 29/04 20:28 "Yesterday I added some functions to Induction.WellFounded, following the 29/04 20:28 discussion you and fax had" 29/04 20:28 eek 29/04 20:28 <_< 29/04 20:29 >_> 29/04 20:29 I should watch my mouth if people like Nils are reading 29/04 20:29 he could be anywhere! 29/04 20:29 I say too much stupid stuff :p 29/04 20:29 now I have to install ghc-6.12 29/04 20:34 (so I can install development Agda, so I can use the development library) 29/04 20:35 Oh, that reminds me. c.h.o is back up, so I can pull agda. 29/04 20:36 Oh, but nothing particularly interesting happened, apparently. 29/04 20:36 no quotients yet/ 29/04 20:37 ? 29/04 20:37 So what are quotients? 29/04 20:37 You take a type, and identify various elements according to an equivalence relation to get a new type. 29/04 20:37 Is there a simple example? 29/04 20:39 Z = N x N / (\(l, r) (l', r') -> l + r' == r + l') 29/04 20:39 Assuming I got that right. 29/04 20:40 and the identified elements are included or excluded? 29/04 20:40 The identified elements are indistinguishable from one another. 29/04 20:40 (1, 0) == (2, 1) : Z 29/04 20:42 so proving that equation woud not be reflexivity 29/04 20:42 it would be like quotientEqual (reflexivity) 29/04 20:43 or so ... 29/04 20:43 ? 29/04 20:43 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 I need to figure out a better way to get the html for my Agda stuff on code.haskell.org. 29/04 20:49 darcs is too risky. 29/04 20:49 scp! 29/04 20:49 I guess I can do that. 29/04 20:49 That's how I publish my html, at least 29/04 20:49 That was less painful than I expected. 29/04 20:54 --- Day changed Fri Apr 30 2010 Do people bother trying to get their Agda source files to stay within 80 characters? 30/04 20:48 If not is there a common standard? 30/04 20:48 I generally don't mind going a little beyond 80. 30/04 20:52 It can be difficult to fit a lot of proofs in 80. 30/04 20:53 I probably keep it under 100 usually, though. 30/04 20:54 I like being able to print them out on letter paper 30/04 20:56 Agda’s colored HTML output looks great with a laser print on heavy paper 30/04 20:57