/home/laney/.irssi/irclogs/Freenode/2010/#agda/April.log

--- Log opened Thu Apr 01 00:00:57 2010
glguy_What's going on with #archlinux?01/04 06:50
glguy_rather, why are we redirecting people to archlinux backwards?01/04 06:51
glguy_Oh, is it April 1st somewhere?01/04 06:52
AdamantI think US PST is the next to get April Fool'ed.01/04 06:57
glguy_Oh, sorry. I sent that to the wrong channel01/04 06:58
--- Day changed Fri Apr 02 2010
crc__how do you get the agda console so you can test an expression?02/04 10:32
Amadirocrc__, agda -I02/04 10:40
crc__is that inside of emacs?02/04 10:53
crc__btw im a vim user02/04 10:54
AmadiroNo, on the shell. But it says that the interactive mode is not supported anymore.02/04 10:54
crc__ok thanks02/04 10:58
crc__ill ask the lecturer after the break02/04 10:58
dantenif your in emacs you can also enter c-c c-n to evaluate expressions02/04 10:59
liyangcrc__: it's not really usable on the command line. :( I'm a Vim user too but you just have to put up with the Emacs UI for Agda.02/04 11:07
crc__sorry i may have asked the wrong question. Within emacs, i just want to run a a command, say something stupid like 1 :: []. How do I do that02/04 11:08
liyangC-c C-n for ‘normalise’.02/04 11:08
liyangThough, thinking about it, I don't recall ever having to use that…02/04 11:09
crc__liyang: that was the one I was looking for, thanks02/04 11:18
crc__what does it mean if you get something along the lines of Set !=< _65 -> Set _66 of type Set102/04 11:57
liyangLooks like it's expecting something of _65 -> Set _66 where you've given it something of Set.02/04 11:59
crc__sorry, what is a set _6502/04 12:00
Saizanthe _N things are freshly generated variables02/04 12:00
Saizanand Set can take a parameter which is the universe02/04 12:01
Saizanbasically that error means that you're giving it a Set where it expects a function returning a Set02/04 12:01
liyangThe universe polymorphism is only making type errors harder to read, but you get the hang of interpreting those errors eventually. :-/02/04 12:05
Saizanit also removes quite a bit of duplication :)02/04 12:08
--- Day changed Sat Apr 03 2010
Mathnerd314does agda have bottom? (_|_ or ⊥ or whatever)03/04 00:23
faxwhat do you mean03/04 00:23
Mathnerd314Is there some value which is in all other agda types? (like undefined in haskell)03/04 00:24
faxno03/04 00:25
faxyou can turn off termination checker and define it if you want03/04 00:25
Mathnerd314no no, I'm fine03/04 00:26
Mathnerd314the standard library is no match for Haskell's, though...03/04 00:27
glguyThe standard library has a bottom and a casting function _|_-elim to whatever type you'd like03/04 00:31
glguyIn Data.Empty03/04 00:31
glguy⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever03/04 00:31
glguy⊥-elim ()03/04 00:31
Saizanthat's a bottom type though03/04 00:32
Saizanbut i guess if you get a value of that type you're done :)03/04 00:32
Saizanif you just need a placeholder you should put a "?" in there03/04 00:32
Saizanor postulate something03/04 00:32
* Mathnerd314 is confused03/04 00:34
Saizanbasically, if agda had a value of type "forall a. a" it'd be of no use as a theorem prover.03/04 00:37
glguyif you /had/ a value of ⊥ you could make it whatever you wanted :)03/04 00:37
Saizanif a context where you've assumed contradictory facts you can make one, but only there :)03/04 00:38
Saizans/if/in/03/04 00:38
glguyThe standard library has:03/04 00:38
glguytrustMe : {A : Set}{a b : A} → a ≡ b03/04 00:38
glguytrustMe = primTrustMe03/04 00:38
* fax hates that stuff03/04 00:40
wpk_Hi all, I have a function which returns the union of 2 equivalencies (=), but when I put the constructor for a union with the equiv constructor (refl) on the right hand side of a pattern match Agda complains, what am I missing?03/04 15:30
wpk_I'm using Data.Sum and Relation.Binary.PropositionalEquality.03/04 15:32
liyang*the* constructor for a union?03/04 15:33
wpk_well i match for the two constructors for the \u+ union function03/04 15:33
wpk_i think there are two, inj\_1 and inj\_203/04 15:34
liyangPaste? http://moonpatio.com/fastcgi/hpaste.fcgi/new What's the complaint?03/04 15:34
wpk_sec03/04 15:35
wpk_http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a924703/04 15:35
Saizanthat usually happens when both sides of the equality are compound expressions03/04 15:35
Saizanah, no03/04 15:36
wpk_im new to this stuff so im probably making a basic mistake03/04 15:36
wpk_did that code and error message make any sense?03/04 15:37
Saizanwpk_: what happens if you delete the {n} part?03/04 15:37
wpk_http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=9247#a924803/04 15:38
wpk_(same error)03/04 15:38
Saizanah, you didn't update the code though03/04 15:39
wpk_i did in emacs, im just really tired heh03/04 15:39
Saizanheh03/04 15:39
wpk_the new error is the first one03/04 15:39
wpk_they appear similar03/04 15:40
Saizani 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 yourself03/04 15:40
Saizanand i think you get the same problem even if you leave it implicit because you can't write ⌊ n /2⌋ * 2 without binding n03/04 15:41
Saizani'm not really sure how/if you're supposed to be able to pattern match on refl there03/04 15:42
wpk_is there any way to create a pattern match where i deconstruct the equivalency then? like it works if i use a symbol for them03/04 15:42
wpk_hmm03/04 15:42
Saizanyou could post on the mailing list03/04 15:43
liyangfor 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
Saizanhowever you can still use that equality proof without pattern matching on it03/04 15:43
liyanginstead of refl there, name it ‘A’ and write inj\_1 (cong (suc \o suc) A) on the RHS.03/04 15:45
wpk_suc \o suc means suc(suc())?03/04 15:46
wpk_sorry im a complete newbie03/04 15:46
liyangopen import Function :303/04 15:46
liyangFunction composition, yes.03/04 15:46
wpk_apparently my installation of agda2 doesnt have Function.agda?03/04 15:48
Saizandid you install the standard library?03/04 15:49
liyangOh er, Data.Function then. Or just write \lambda x \-> suc (suc x)03/04 15:49
Saizanhowever you can write a simple lambda here03/04 15:49
liyangSaizan: there's been some renaming going on lately in the stdlib.03/04 15:49
Saizantrue03/04 15:49
wpk_Data.Function works03/04 15:49
wpk_:D03/04 15:50
wpk_thanks so much guys03/04 15:52
wpk_which file is cong in so I can look at it?03/04 15:52
liyangRelation.Binary.Core probably.03/04 15:53
Saizanin emacs, move your cursor over it and press M-.03/04 15:53
liyangIf things type-check, you can cursor over the identifier and meta-.03/04 15:53
liyang(yes.)03/04 15:53
wpk_i never knew that that's cool03/04 15:55
liyangIs it coursework? (Whose course, out of interest?)03/04 15:56
wpk_Manuel Chakravartay (sp?) at UNSW, Australia.03/04 15:57
liyang*nod*03/04 15:57
wpk_course is some SEng core forget the name03/04 15:57
liyangThought so. :) He sometimes hangs out here as TacticalGrace.03/04 15:58
wpk_haha ill remember that03/04 15:59
liyang(So that's Nottingham, Swansea, and UNSW now…)03/04 15:59
wpk_where Manuel has taught agda?03/04 15:59
liyangWhere Agda has been used in teaching, that I'm aware of.03/04 16:00
wpk_oh03/04 16:01
liyangI'm sure there's more though—I haven't really being paying that much attention.03/04 16:02
wpk_a good 80% of the students are totally lost on this I think03/04 16:03
liyangThat's probably expected. You'll get an intuition for it eventually. :303/04 16:07
kosmikusliyang: I've used it in teaching, too (at UU)03/04 16:27
liyang:D03/04 16:34
Amadirokosmikus, UU?03/04 16:34
liyangWhat's the confusion percentage like?03/04 16:34
liyangAmadiro: Utrecht03/04 16:35
AmadiroAh.03/04 16:35
faxhttp://www.e-pig.org/darcsweb?r=Pig09;a=headblob;f=/models/Desc.agda03/04 20:30
faxcool03/04 20:30
fax 118 proof-map-id : (D : Desc)(X : Set)(v : [| D |] X) -> map D X X (\x -> x) v == v03/04 20:30
fax 125 proof-map-compos : (D : Desc)(X Y Z : Set)03/04 20:30
fax126 (f : X -> Y)(g : Y -> Z)03/04 20:30
fax127 (v : [| D |] X) ->03/04 20:30
fax128 map D X Z (\x -> g (f x)) v == map D Y Z g (map D X Y f v)03/04 20:30
ccasinisn't generic programming fun!03/04 20:37
ccasinwhat's this from?03/04 20:39
faxthat agda file I linked XD03/04 20:40
faxhere's a paper on it http://personal.cis.strath.ac.uk/~dagand/levitation.pdf03/04 20:40
ccasinfrom the date, I guess this is an icfp submission?03/04 20:41
ccasinoh my, from the abstract this looks really cool03/04 20:42
faxyeah it's nice stuff03/04 20:43
faxI think it's a continuation of Peter Morris' thesis03/04 20:43
faxin some ways at least03/04 20:43
ccasinthis is such a good idea03/04 20:46
ccasinI can tell because I'm jealous I didn't have it :)03/04 20:47
faxditto hehe03/04 20:47
faxsmall 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 be03/04 20:48
ccasinyes, I am anxious to see exactly how they pull this off03/04 20:49
ccasinbut I suppose I have to read the pages in order03/04 20:50
faxif you start at the bottom of http://www.cs.nott.ac.uk/~pwm/ then it just gets harder (gradually though)03/04 20:50
ccasin:)03/04 20:51
ccasinhappily, I think I have enough background03/04 20:51
SaizanDesc as described above doesn't handle mutually recursive datatypes though03/04 20:51
liyanghttp://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
faxthat's just because of the number of times I reinstalled it03/04 22:06
fax:p03/04 22:06
ccasinthis is interesting, but a little odd03/04 23:19
ccasinis agda actually classified as an application?03/04 23:19
ccasinmost people interact with it through emacs, which just loads the agda libraries into ghci, right?03/04 23:20
ccasinits cabal file calls it a library03/04 23:21
ccasinbut maybe these are just classifications he made up03/04 23:21
Saizanthere's an agda-executable package which gives you an executable03/04 23:25
Saizanotherwise it's a library used by ghci in the emacs mode03/04 23:25
ccasinyes, but I think no one uses the executable, so I'd be surprised if that's what's referred to here03/04 23:25
Saizanoh, i think i miss some context03/04 23:26
ccasinliyang had linked to this:03/04 23:27
ccasinhttp://donsbot.wordpress.com/2010/04/03/the-haskell-platform-q1-2010-report/03/04 23:27
ccasinwhere agda is listed as the 13th most cabal-installed haskell application03/04 23:27
ccasinin the last quarter03/04 23:27
ccasin(as opposed to library)03/04 23:27
Saizani think it counts as an application because of the agda-mode executable03/04 23:28
ccasinyes, this is a reasonable theory03/04 23:28
ccasinI just wonder how he made these choices03/04 23:29
ccasin(not for any particular reason)03/04 23:29
--- Day changed Sun Apr 04 2010
wpk_Hi I'm having a problem pattern matching in a function I've written, I think the type declaration is sensible but I'm not sure, it's like PA9 : ? {n} -> (P : N -> Bool) -> P 0 = true -> ((P n = true) -> (P (suc n) = true)) -> P n = true04/04 09:15
wpk_the pattern {0} p a b is rejected by agda..04/04 09:15
wpk_it seems like agda wont recognize ((P n = true) -> (P (suc n) = true)) as being an argument, and includes it in the return type04/04 09:25
Saizanwpk_: are you really using = there or \== ?04/04 13:37
stevanhellos04/04 13:38
faxhi04/04 13:38
stevantaught yourself to levitate yet?04/04 13:40
faxI think so04/04 13:41
stevan:-)04/04 13:41
fax504/04 17:05
faxsorry, I take that back04/04 17:05
stevan38 people, yet complete silence :-(.04/04 17:06
stevanglguy: are you still playing with category theory?04/04 17:07
faxI tried to implement category theory in Coq but it didn't go well04/04 17:07
faxI mean it was going quite nicely for a bit, then I started to wonder what 'equals' means and it all fell apart04/04 17:08
stevanyes04/04 17:08
faxwhat 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 it04/04 17:10
stevanyou run into situations where you need existential equality?04/04 17:10
faxwhat's existential equality?04/04 17:10
stevanforall x. f x = g x -> f = g04/04 17:11
faxoh04/04 17:11
faxwwhy do you say that? It seems very plausible04/04 17:11
stevanwell you can't prove that statement inside agda?04/04 17:12
faxI'm not sure04/04 17:12
faxI think we can prove (\x -> f x) = (\x -> g x) <-> f = g04/04 17:13
faxyes you are right, this is weaker than the forall x. we can't prove that in agda04/04 17:13
stevani only ran into that problem with equality, what problem were you refering to?04/04 17:14
faxhuh?04/04 17:17
Saizanstevan: you meant extensional?04/04 17:17
stevanprobably :-)04/04 17:17
stevanfax: you said it fell part when you started wondering what equals means?04/04 17:18
faxyeah04/04 17:18
faxyou have to get all this typeclass stuff out to make sets with equivalence relations and equivalence preserving morphisms04/04 17:18
faxit works but it's really complicated04/04 17:19
faxif we could just form types T/~, I think it would be much easier and everything would work perfectly04/04 17:19
fax(but experience tells me that does not happen :) and there are unforseen problems)04/04 17:19
Saizanwith 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
faxyeah04/04 17:20
faxI've not been able to figure out the syntax for pig so I haven't tried anything with it though04/04 17:21
Saizani defined a cofree comonad thing :)04/04 17:21
faxwow cool I wanna see04/04 17:21
faxdid you write that in haskell?04/04 17:21
stevanwhat's wrong with just using propositional equality for CT btw?04/04 17:23
stevan(i need to read up on quotients)04/04 17:23
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24653 <-04/04 17:24
faxcool Saizan04/04 17:24
Saizanfax: i just wrote it in epigram itself, i could add it as a Feature to get the comonad laws hold definitionally though04/04 17:24
faxso cofree means basically free except greatest fixed point?04/04 17:24
Saizanor, i could try at least :)04/04 17:24
Saizani'm not so sure what cofree means by itself, but it sounds something like that04/04 17:25
Saizanthough i'm pretty comfortable with the "cofree comonad" construction04/04 17:27
faxstevan - if you try to form the category of categories then when are two functors between categories equal?04/04 17:28
faxif you use propositional equality ... is that right/04/04 17:28
faxmaybe the thing to do would be define category as a feature...04/04 17:30
faxthen implement all of modern mathematics in that04/04 17:31
stevanhmm, 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
faxthat was just my thinking which led me to give up04/04 17:35
faxmaybe 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
stevanyeah, 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
faxthe reason I wanted categories is to define term algebras04/04 17:39
faxthat stuff would probably have worked but I didn't want to build a wall around myself04/04 17:40
faxstevan definitions in ada ?04/04 17:42
faxagda*04/04 17:42
stevanyes, records for what a category is, functors, etc04/04 17:43
faxcool can I see04/04 17:43
faxhmmmm I need to install agda :/04/04 17:43
stevanhttp://web.student.chalmers.se/~stevan/ctfp/html/README.html04/04 17:44
stevani wouldn't trust them to be right tho, i'm a CT noob. :-)04/04 17:45
faxI've only started to study it recently (Because of dolio ;p)04/04 17:45
stevani think it helps to code, give you something concrete...04/04 17:46
faxyeah 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 answers04/04 17:47
stevanoh, i'm surely not there yet. could you give an example?04/04 17:49
faxstevan, say you defined the category of bijective functions between finite sets04/04 17:49
faxoh04/04 17:49
faxthat's not an example04/04 17:49
faxthis is regarding the problem of equality04/04 17:49
faxI think we can have lots of different permutation functions which are extensionally equal but not identical in agda04/04 17:50
faxso 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 problems04/04 17:50
faxbut more generally, if you have any category where the objects (or morphisms) are not normal forms -- then the equality will not match up exactly right04/04 17:51
stevanhmm04/04 17:51
faxstevan ou know about Computational Category Theory? (the book is online)04/04 17:52
faxthere's lots of programs in there (which I wanted to implement.. but I got stuck)04/04 17:52
stevanby burstall and rydesomething?04/04 17:53
faxyes04/04 17:53
stevani only glanced thru it, their definitions are not very nice given that they have to make them fit into simply typed setting04/04 17:54
faxyeah but I mean that's just the SML code04/04 17:54
stevanyeah, true04/04 17:55
faxthe programs should work in a dependently typed setting, except with strong specifications04/04 17:55
fax(at least I hope so!)04/04 17:55
faxit's raelly frustrating because there's a lot of stuff I want to program but without this foundational stuff it doesn't seem possible04/04 18:14
stevanwhat sort of stuff do you want to program? what foundational stuff?04/04 19:59
faxfoundational stuff being category theory04/04 20:00
faxI've been trying to get some of the maths I know into the computer but it's has not been working well at all04/04 20:00
stevanwhat sort of maths?04/04 20:02
faxlike everything04/04 20:03
faxcalculating things, solving equations04/04 20:04
stevanhave you read about the formath project?04/04 20:04
faxyeah04/04 20:05
stevanthat sort of stuff?04/04 20:05
faxyes04/04 20:05
faxin the coq standard library there are stuff like decidibility of primality and they don't even compute :/04/04 20:05
faxand they have trichotomoy as an axiom on the real numbers04/04 20:06
faxit's pretty stupid04/04 20:06
stevani know next to nothing about coq. what about that corn thing? don't they do it propertly?04/04 20:07
faxyeah corn is cool04/04 20:07
stevandoes corn have a better solution for reals than the standard lib?04/04 20:16
faxyes04/04 20:18
faxthat's roconnors stuff it's way cool04/04 20:18
stevanwhy doesn't it replace the std lib stuff then?04/04 20:20
--- Day changed Mon Apr 05 2010
Schrodinger_Anyone here?05/04 06:57
--- Day changed Tue Apr 06 2010
agda_noobhello06/04 09:17
agda_noobi wonder how many people are trying to prove the peano axioms in agda on this channel06/04 09:18
agda_noobhello?06/04 09:21
agda_noobdoes anybody know anything about agda here?06/04 10:00
vlad__hello?06/04 10:17
vlad__can anybody help me out with agda06/04 10:18
vlad__im trying to figure out how to prove the peano axioms06/04 10:18
kosmikusvlad__: ok, so what exactly are you trying to do?06/04 10:18
vlad__ok well im trying to use the reflexive function to prove that if suc m \equiv suc n then m \equiv n06/04 10:19
vlad__but i dont think im putting the syntax right06/04 10:20
kosmikusyou get a syntax error?06/04 10:20
vlad__well my definition shoudl return suc m \equiv suc n then m \equiv n06/04 10:20
vlad__and i have PA4 {m} {n} = refl suc m \equiv suc n -> m \equiv n06/04 10:21
vlad__any ideas kosmikus?06/04 10:21
kosmikusis this a homework assignment?06/04 10:21
vlad__it is06/04 10:22
kosmikusis the original assignment online?06/04 10:22
vlad__yap06/04 10:22
kosmikuswhere?06/04 10:22
vlad__i dont think you can access it, you have to log on06/04 10:22
vlad__the gist of it is i have to prove some peano axioms06/04 10:22
vlad__i have the right idea about doing it06/04 10:23
vlad__just cant seem to get the syntax right in agda06/04 10:23
kosmikusit looks like what you're writing should be the *type* of PA406/04 10:23
vlad__right06/04 10:24
vlad__the type is  suc m \equiv suc n -> m \equiv n06/04 10:24
kosmikusyes, so then you should write:06/04 10:25
kosmikusPA4 : \forall {m n} -> suc m \equiv suc n -> m \equiv n06/04 10:26
kosmikussomething like that06/04 10:26
vlad__thats the type i have that06/04 10:27
vlad__no for all tho06/04 10:27
vlad__just {m n : \nat} -> suc m \equiv \suc n -> m \equiv n06/04 10:27
vlad__my problem is the application06/04 10:28
vlad__i think i have to use the reflexive proof  but im not sure how to provide the arguments right06/04 10:28
TacticalGracekosmikus: you can easily access the assignment at https://wiki.cse.unsw.edu.au/cs3141/10s1/Assignment%20106/04 10:29
kosmikusTacticalGrace: ah :) if you're here, then you can probably decide better what to tell or not to tell :)06/04 10:29
vlad__really? i think u have to log in06/04 10:29
vlad__i wasnt aware u can access it, in any case i always log in06/04 10:30
kosmikusI can access it.06/04 10:30
vlad__ok cool06/04 10:31
vlad__do you reken you can help me out then?06/04 10:31
kosmikuswell, the solution is quite simple, so I don't want to just give it06/04 10:32
kosmikusif you have the type, you have to think about how you can construct a value of the type06/04 10:32
vlad__i know its simple, its frustrating06/04 10:32
kosmikusyou have to provide a function from an equality to an equality06/04 10:32
vlad__yap, aint that simple , but iv tried returning that type and it doesnt like it06/04 10:32
kosmikusso you can start with06/04 10:32
kosmikusPA4 proof = ?06/04 10:32
vlad__i start with PA4 {m} {n} = ?06/04 10:33
vlad__is that right?06/04 10:33
kosmikusthat's also ok06/04 10:33
kosmikusbut then ? is of function type, right?06/04 10:33
kosmikusso, a good general tactic is to introduce an argument if you have to produce a function06/04 10:34
kosmikusso you either put it on the lhs:06/04 10:34
kosmikusPA4 {m} {n} proof = ?06/04 10:34
kosmikusor you use a lambda abstraction:06/04 10:34
kosmikusPA4 {m} {n} = \ proof -> ?06/04 10:34
kosmikusthe former is probably better06/04 10:34
vlad__what do you mean by = \ proof -> ? i thought the proof came after the equal and thats it?06/04 10:35
vlad__oh06/04 10:35
kosmikusproofs can have structure. that's the whole point.06/04 10:38
vlad__i have PA4 {m} {n} = suc m \equiv suc n -> refl m \equiv n ?06/04 10:38
kosmikusno, now you're writing a type again06/04 10:41
kosmikusbut you have to give an implementation of that type06/04 10:41
vlad__should i be using refl as proof?06/04 10:41
vlad__or cong?06/04 10:41
vlad__im soo confused06/04 10:43
stevanso am i!06/04 10:44
vlad__do you know much about agda stevan?06/04 10:44
stevana bit.06/04 10:45
kosmikusvlad__: to be honest, both refl and cong are possible here, but it's probably easier to do it directly via refl06/04 10:45
vlad__right06/04 10:46
vlad__im just not sure how to construct this function06/04 10:46
kosmikusvlad__: you should really try to construct the proof systematically06/04 10:46
vlad__how many arguments does refl take in?06/04 10:46
kosmikusvlad__: you've probably learned that in a lecture, right?06/04 10:46
kosmikusrefl doesn't take any explicit arguments06/04 10:46
vlad__ok, i just dont understand how to use refl06/04 10:46
kosmikusrefl is the constructor of the equality type06/04 10:47
kosmikushave you been able to prove any of the other axioms?06/04 10:47
vlad__only the first 306/04 10:48
kosmikusperhaps, if you do symmetry and transitivity first, this one will become clearer06/04 10:48
vlad__im really not good at math or agda, i dont understand what you mean by symetry and transitivity06/04 10:48
vlad__as in i dont get how i prove that06/04 10:48
kosmikusTacticalGrace: nice assignment, btw06/04 10:49
kosmikusvlad__: PA6 and PA706/04 10:49
kosmikusvlad__: sorry, I was assuming that you've read the assignment06/04 10:49
vlad__lol06/04 10:50
vlad__im taking it one at a time06/04 10:50
vlad__oh right , you think it would be easier to do 6 and 7 first?06/04 10:50
kosmikuswell, they have all one-line solutions06/04 10:52
kosmikusbut if you have trouble doing one, it may be easier to do one of the others first06/04 10:52
kosmikusit may also be helpful to look at notes/slides from the lecture if there are any06/04 10:53
TacticalGracekosmikus: thanks :)06/04 10:53
vlad__thats prob a good strategy06/04 10:54
kosmikusthe assignments says that propositional equality has been introduced there06/04 10:54
kosmikusso you've probably already seen how it can be used06/04 10:54
vlad__yap i have , il re-read though it06/04 10:54
kosmikusTacticalGrace: and good to see you're also trying to use Agda in teaching06/04 10:54
kosmikusTacticalGrace: what kind of course is this? I can't seem to access the course's main page.06/04 10:54
TacticalGracekosmikus: It's http://www.cse.unsw.edu.au/~cs3141/06/04 10:55
kosmikusTacticalGrace: ah, I've done http://www.cs.uu.nl/wiki/DTP a while ago06/04 10:56
TacticalGraceIt's a fairly big class actually06/04 10:56
TacticalGrace68 student06/04 10:56
kosmikusTacticalGrace: and I'm currently having two lectures of Agda at the end of "Advanced Functional Programming"06/04 10:56
kosmikusTacticalGrace: always fantastic that you get so many students. these are numbers we can only dream of.06/04 10:57
TacticalGracethe class is part of the compulsory SE cources for SE program studends and CS program students06/04 10:59
TacticalGracewhich is part of the challenges06/04 10:59
vlad__se rules06/04 10:59
vlad__go se06/04 10:59
TacticalGracevlad__: are you a SE student?  You should have done Event B in that case and actually already a bit about logic06/04 11:00
vlad__i am doing event b now06/04 11:00
vlad__2 subjects event b 3rd is this 1 which is about agda and haskell06/04 11:00
TacticalGraceic, I thought the event b stuff was supposed to be before 314106/04 11:01
vlad__tactical grace06/04 11:01
vlad__you are from nsw06/04 11:01
vlad__you are from unsw06/04 11:01
vlad__technically but its not a prerequisite06/04 11:02
vlad__cHAK06/04 11:02
vlad__u are manuel06/04 11:02
vlad__my lecturer06/04 11:02
TacticalGraceit can't be b/c of the CS students06/04 11:02
TacticalGracevlad__: indeed06/04 11:02
vlad__hahahah06/04 11:02
vlad__this is too funny06/04 11:02
vlad__cought out06/04 11:03
vlad__good assignment06/04 11:05
vlad__thanks alot for all your help kosmikus06/04 11:21
vlad__i have to go now, hopefully i will figure things out better after more practice06/04 11:21
vlad__take it easy tactical grace06/04 11:22
vlad__see you in the lectures06/04 11:22
pigworkerI was going to suggest reading "A Few Constructions on Constructors". No I wasn't.06/04 11:39
TacticalGrace;)06/04 11:41
jlouisWhats Gordon Brows equality like?06/04 12:08
jlouis*Brown06/04 12:09
jlouisThe agda tutorial declares: _or_ : Bool -> Bool -> Bool; true or x = true; false or _ = false .. does that mean the _or_ is an impostor, a cleverly disguised _and_ ?06/04 12:30
npouillard:)06/04 12:30
npouillardfalse or x = x06/04 12:31
npouillardwould be less wrong indeed06/04 12:31
npouillardit is not a and either "true or false" returns true...06/04 12:31
pigworkerI've always said that "grep Bool" is a good test of any dependently typed library.06/04 12:32
npouillardpigworker: what you mean06/04 12:32
pigworkerBool is the type of meaningless bits (hence well typed errors like the above). Bool-valued tests tend to be less useful (i.e., harder to exploit at the type level) than those which decide propositions or deliver witnesses.06/04 12:35
pigworker"A Boolean is a bit uninformative." was my old slogan.06/04 12:35
npouillardpigworker: sure, but they should not be to be completly removed06/04 12:36
npouillardfor instance vectors hold more information than lists, but we should not remove lists.06/04 12:36
npouillardbut in06/04 12:36
npouillarda dependently typed language it is evident that we should use less bools06/04 12:37
npouillardand more 'Dec P'06/04 12:37
npouillardthis is just my POV, of course...06/04 12:38
pigworkerIt'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
npouillardbut I wouldn't mind if Bool got renamed to Bit to emphasis on this06/04 12:40
pigworkerCorrespondingly, 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
npouillardsure06/04 12:41
npouillardbut it is the case in the Agda stdlib, equality returns a Deciable _≡_ and we can use ⌊_⌋ to get a bool06/04 12:42
* kosmikus 's grant proposal for dependently typed programming has been rejected in the pre-screening phase :(06/04 12:43
npouillard:(06/04 12:44
pigworkerkosmikus: rats!06/04 12:44
kosmikuspigworker: yeah. "not innovative enough" and "relatively weak CV"06/04 12:44
edwinbbah!06/04 12:45
pigworkerkosmikus: sounds like prejudice to me; or is that what "pre-screening" means?06/04 12:46
TacticalGracekosmikus: :(06/04 12:46
edwinbWe're clearly going too mainstream06/04 12:46
kosmikuspigworker: yes, that's what it means ;)06/04 12:46
kosmikuspigworker: from 49 submissions, they select 23 that even get expert reviews.06/04 12:46
kosmikusultimately, 5 get funded.06/04 12:47
kosmikusI 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
pigworkerkosmikus: not great odds, but a shame that they don't get expert reviews for all06/04 12:47
kosmikusWhere an ICFP paper is clearly less relevant for your future life than a grant proposal with 800 kEUR.06/04 12:47
pigworkerkosmikus: So you got about 100 submissions? I don't expect you to answer that...06/04 12:50
kosmikusICFP 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
TacticalGracekosmikus: so, how does a non-expert decide what is innovative?06/04 12:50
pigworkerTacticalGrace: with nipples06/04 12:50
kosmikusTacticalGrace: 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
pigworkerWhich reminds me: grant app to finish; must work on zip, pep and fizz; oh, and some technical substance.06/04 12:53
kosmikusperhaps I should start submitting grant apps in other countries.06/04 12:54
pigworkerInternational collaboration always looks good.06/04 12:56
pigworkerkosmikus: and you've got a conflict with us lot, too...06/04 12:59
jlouisAt page 8 in tutorial - first verdict: Syntax beats Twelf06/04 12:59
kosmikuspigworker: yes.06/04 12:59
pigworkerhad better go to school for a bit.06/04 13:03
jlouisAgda definitely feels a lot like Twelf, just easier06/04 16:22
Saizanuh06/04 16:22
Saizanwhen i've to prove something about a function defined with overlapping patterns i wish i could just pattern match on its cases though06/04 16:29
faxyeah it's a shame we don't get any witnesses from the pattern matching, but that's beacuse they just implement it directly06/04 16:36
fax<kosmikus> pigworker: yeah. "not innovative enough" and "relatively weak CV"06/04 16:39
faxfucking hell that is ridiculous06/04 16:39
stevanfax: 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
faxmost likely I cannot understand any of this but I will try :)))06/04 17:23
dantenI just replied :p basically giving that link and also a video of Vladimir talking in general about foundations of mathematics :)06/04 17:34
faxwe have to know category theory (that's what those squares in the video are), synthetic topology, "Homotopy theoretic models of identity types"06/04 17:42
fax'schemes' perhaps.06/04 17:43
faxa lot of things06/04 17:43
faxI'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
dantendunno06/04 17:50
faxoh and fibrations/fiber bundles get mentioned a lot06/04 17:51
fax(another thing which I have only got cheesy videos of mugs morphing into donuts rather than any actualy understanding)06/04 17:52
stevan:-)06/04 17:52
stevanslides for talk about a project i been working on with a friend: http://web.student.chalmers.se/~stevan/csallp/talk/talk.pdf06/04 18:13
stevanif someone is interested06/04 18:13
faxstevan nice!!!!!!06/04 18:14
faxthis "Dense linear orders" is why I had to put down my model theory book06/04 18:14
stevani think i can explain it now, but we haven't implemented it fully yet06/04 18:15
faxstevan I am going to ask you all about it :P06/04 18:16
stevanwould be awesome to have running examples, but that will probably take an other month or so06/04 18:16
faxpage 12,  Otherwise (inequalities) --06/04 18:19
faxthis part is basically doing a topological sort?06/04 18:19
stevani know nothing about topological sorts06/04 18:20
faxwell 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
faxnatural numbers06/04 18:21
stevanhmm06/04 18:22
fax"Ssreflect what does it do?" hehe I think the same thing06/04 18:22
faxannoying 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
faxnice in Agda they don't have such a thing (although there are good points to it as well)06/04 18:23
stevanwell 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
Saizanwhat is Qed?06/04 18:25
faxSaizan, it's meant to be used for "proofs" -- it's sort of like a poor mans proof irrelevance06/04 18:25
faxthe things defined with Qed wont reduce so it's 'in effect' proof irr.. just without the actual convertability of proofs06/04 18:26
faxit means you can go an reprove any Qed thing in a different way, without breaking stuff06/04 18:26
faxbut the bad thing is sometimes you /want/ proofs to have computational content -- like with well founded recursion06/04 18:26
npouillardfax: it does have some perfs advantages too06/04 18:26
faxand the other problem is that people use it when they shouldn't06/04 18:26
faxnpouillard oh that's true I should have thought of this as well06/04 18:27
faxthere'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
faxstevan (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
stevanok, so do you understand why qelim for dlos works now :-)?06/04 18:31
faxno06/04 18:31
stevan:-/06/04 18:32
faxim not ready to ask any intelligent questions yet :P06/04 18:32
faxjust looking at the code06/04 18:32
faxand I wish I had agda but I don't know how to install it06/04 18:32
stevanthe theory dependent part (DLOs) isn't done yet unfortunately06/04 18:33
faxDLOs 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
faxso I decided to come back to it another day06/04 18:34
faxI suppose you need decidibile equality on the carrier to prove the forall/~exists~ switch?06/04 18:34
faxor you use classical connectives?06/04 18:34
stevani 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
faxwell there's no reason to not have both.. I suppose06/04 18:34
stevanyeah, if look at the forall case in the last proof in decisionProcedure you will see what happens06/04 18:36
fax¬∃¬⇔∀ : ∀ {A : Set}{P : A → Set}(d : ∀ x → Dec (P x)) → (¬ (∃ λ x → ¬ P x)) ⇔′ (∀ x → P x)06/04 18:43
faxthis is so cool stevan06/04 18:43
stevan:-)06/04 18:43
faxagda lib doesn't have rationals?06/04 18:51
stevanit does, but it's basically only the data type Q, without any useful functions (+, -, *, etc are not implemented)06/04 18:52
fax:S06/04 18:58
faxI can't find anything, do they have setoids?06/04 18:58
faxmmm06/04 18:58
faxquotients comeing soon probably means no06/04 18:58
stevanhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.Rational.html#18006/04 18:59
faxI wonder why it has     isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1))06/04 19:01
faxah that's for ≃⇒≡ : _≃_ ⇒ _≡_06/04 19:01
faxhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf]06/04 20:35
faxhttp://sneezy.cs.nott.ac.uk/fplunch/weblog/wp-content/uploads/2009/06/numbers.pdf06/04 20:35
stevanthere 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
faxhow different?06/04 20:45
stevanit was stand alone, not reusing stuff from the std lib, so it needs some reworking to fit nicely into the std lib06/04 20:46
faxoh ok06/04 20:46
faxI was going to implement R but that would need setoids and since agda is getting quotients soon it seems like I should just not06/04 20:46
npouillardis there something to read about the near to come quotients in Agda ?06/04 20:48
stevanhow do you know they are comming soon?06/04 20:48
fax:S I hope I haven't made this up06/04 20:48
stevanthey seemed to have been discussed during last AIM, but it doesn't say anything more than that06/04 20:50
pigworkerIt's not obvious to me how to make (R x y) -> [x]=[y] hold, without re-engineering propositional equality.06/04 20:56
pigworkerwhere [_] gives equivalence classes wrt R06/04 20:56
faxit seems okay to add this stuff as an axiom06/04 21:02
faxI 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
faxthen of course the axioms don't have computational properties... I guess that is the real problem06/04 21:03
pigworkerfax: yep, that's the problem06/04 21:03
stevanwhat does corn do?06/04 21:07
faxwell corn doesn't use typeclasses but I think they are rewriting it to do so06/04 21:07
faxbut you must carry about morphism proofs with all the stuff06/04 21:10
faxlike if you defined a group with inverse : G -> G06/04 21:10
faxthen you must also have  inverseProper : forall x y, x ~ y -> inverse x ~ inverse y06/04 21:10
stevanso, the real closed fields using reflection in coq paper i posted recently, is it runnable?06/04 21:11
faxI've not tried06/04 21:11
faxthe reals in the stdlib are classical06/04 21:11
faxdid you see the bit where they used it to derive P \/ ~P for first order statements06/04 21:12
stevanand they used those?06/04 21:12
faxCoRN defines constructive reals too06/04 21:12
stevani haven't looked at it propertly yet06/04 21:12
faxI've not tried this reflection thing though06/04 21:12
faxwell06/04 21:13
faxI was going to say I don't think we can use quantifier elimination on reals06/04 21:13
fax(since we don't have that  forall/~exists~ switch)06/04 21:13
faxbut then... there is that cylindrical algebraic decomposition06/04 21:13
stevanwill it not fall out like it did in our quantifier elim library?06/04 21:14
faxI am confused :P06/04 21:14
faxhow can it work06/04 21:14
stevani don't know how qlim for RCF works, but i assumed it worked similarly to how we did it for DLOs06/04 21:15
fax"To build a decision procedure from this theorem, we have to chose a field D06/04 21:15
faxover which sign and equality is decidable."06/04 21:16
faxso in this case, they only need coefficients of the polynomial to be decidible06/04 21:16
faxthe actual variables can be real, if I understand correctly06/04 21:16
faxi.e. you could have polynomials with rational coefficients, except they are functions R^n -> R06/04 21:16
fax(please correct me if I say something wrong!!)06/04 21:17
stevani 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
faxoh there are no axioms for setoids06/04 21:21
faxyou 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 rewrites06/04 21:22
faxcoq 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 rationals06/04 21:23
stevanok06/04 21:24
faxyeah 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 wanted06/04 21:24
stevanso their RCF solver is most likely runnable then? (just making sure :-)06/04 21:26
faxwell the constructivist thing to do will be try it out :)06/04 21:26
faxlets find the source code06/04 21:26
faxI didn't manage that before06/04 21:26
stevanme neither06/04 21:26
fax#  CAD: Je travaille sur une implémentation et une preuve formelle de correction (en Coq) d' un algorithme de Décomposition Algébrique Cylindrique (CAD). Cette formalisation achevée permettrait d' obtenir une procédure de preuve automatique pour l' arithmétique réelle non linéaire, produisant des certificats formels de ses résultats.06/04 21:30
fax"#  CAD: I am working on the implementation and formal proof of correctness (in Coq) of a Cylindrical Algebraic Decomposition (CAD) algorithm. This would lead to an automated proof production decision procedure for non linear real arithmetic. "06/04 21:30
faxso maybe it's not quite finished yet06/04 21:30
stevanif i remember, i could probably ask thierry about it tomorrow...06/04 21:33
stevanbut it seems the formath people have to solve this problem (if it isn't solved already)?06/04 21:40
faxformath?06/04 21:40
stevani asked you about it yesterday? you said you had read about it? http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath06/04 21:41
faxme??06/04 21:41
stevan21:04 < stevan> have you read about the formath project?06/04 21:42
stevan21:05 < fax> yeah06/04 21:42
stevan21:05 < stevan> that sort of stuff?06/04 21:42
stevan21:05 < fax> yes06/04 21:42
stevando you have an evil twin?06/04 21:42
faxThis 'ForMath' sounds great06/04 21:43
stevanthere is more under "Research Methodology"06/04 21:44
stevanso if you had not seen this before, what were formath project were you saying you had read about yesterday? :-p06/04 21:49
faxI've seen this06/04 21:50
stevanok06/04 21:51
--- Day changed Wed Apr 07 2010
vlad__hey manuel07/04 08:52
vlad__do you recken you can help me out a little with my assignment?07/04 08:53
stevanfax: 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
stevanfrom what i could gather it's not runnable, due to Qeds.07/04 15:24
stevanand removing the Qeds makes type checking too slow.07/04 15:25
faxtarnge07/04 15:26
faxstrange07/04 15:26
stevani asked "so what's the plan?",  "i don't know, maybe CBN instead of CBV might help"07/04 15:27
npouillardstevan: what do you want to run?07/04 15:27
stevanthe solver07/04 15:27
stevanas you can run agda's (to prove things)07/04 15:28
stevans/agda's/agda's ring solver/07/04 15:29
npouillardstevan: OK, so that's more "a program written with tactics", than "a proof we want to look at", right?07/04 15:31
stevanyea, a reflective tactic07/04 15:32
stevanit 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 larger07/04 15:35
faxyou can extract f : nat -> nat from the proof forall x, exists y. x < y07/04 15:35
stevanwhen the decision procedure is written using (external) tactics?07/04 15:36
faxit should be true in general07/04 15:37
stevanwell when you do it reflectively the proof is that function?07/04 15:37
faxI just mean it shouldn't matter if how the statement is proved07/04 15:38
npouillardfax: no it does not matter, tactics just build programs07/04 15:39
stevani'm not sure what happens when the proof is an external tactic and you run it. do you pass the value down to ocaml/etc and it gives you a value back?07/04 15:39
npouillard(ugly and large ones actually)07/04 15:39
faxtactics in coq are just scripts that write out lambda terms07/04 15:40
npouillardan external tactic is an OCaml function that have to build/search a proof term that will be checked by the Coq kernel07/04 15:40
npouillardtry "Print mylemma." to see it07/04 15:40
faxbut   (forall a : A, exists b : B, aRb) <-> (exists f : A -> B, forall a, aR(f a))07/04 15:41
stevan(ah right, i remember having printed lemmas now)07/04 15:42
stevanso what does the Qed do? i didn't get that yesterday...07/04 15:43
* stevan reads logs07/04 15:45
npouillardQed, type-check the term and then hide its definition07/04 15:45
npouillardlike 'abstract' in agda07/04 15:45
npouillardDefined, keeps the definition accessible07/04 15:46
stevanso effectively it blocks type level computations?07/04 15:47
npouillardstevan: any computation that would like to unfold mylemma to its definition07/04 15:49
stevanok, interesting07/04 15:50
faxugh 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-point07/04 17:12
liyangPerhaps 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
faxwhat I don't get is why people are too shy to just say "I can't do this" and hand in nothing07/04 17:18
faxthis is sick http://stackoverflow.com/questions/476959/why-cant-programs-be-proven07/04 17:20
faxit's all "Godel Godel Godel Turing Halting Incompleteness" or "proofs are too hard and cost lots of money!"07/04 17:21
faxhehe 'How do you prove your Coq specification is correct?'07/04 17:22
maltemThat's how all those ask-a-question sites are like07/04 17:27
faxit's really a shame because all this rubbish and misinformation is the source which people learn form :|07/04 17:28
maltemNo, people learn from wikipedia :p07/04 17:28
glguyWhat is a good reference for the typing rules pertaining to the different Set levels?07/04 18:08
--- Day changed Thu Apr 08 2010
Associat0rguys what are the pro's and cons of Uniqueness typing vs Monads for IO?08/04 03:11
faxoh oh pigworker08/04 15:54
faxre "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
pigworkerfax: what's up?08/04 15:54
pigworkerfax: I've seen it. Am replying now.08/04 15:55
faxI'm wondering if that's so ? you have to do Acc in Set08/04 15:55
faxok08/04 15:55
pigworkerfax: yes, but Edwin kills it anyway!08/04 15:55
faxah!!08/04 15:55
* edwinb feels his ears burning08/04 15:57
faxroconnor <repeating>08/04 15:58
fax14:55 < fax> I'm wondering if that's so ? you have to do Acc in Set08/04 15:58
fax14:55 < fax> ok08/04 15:58
fax14:55 < pigworker> fax: yes, but Edwin kills it anyway!08/04 15:58
faxthis is that  need not store their indices  I am guessing08/04 15:58
pigworkerfax: yes08/04 15:58
edwinbindeed08/04 15:58
roconnorfax: link08/04 16:00
faxlink to what ?08/04 16:00
faxhttp://www.cs.st-andrews.ac.uk/~james/RESEARCH/indices.pdf ?08/04 16:00
roconnorneed not store their indices08/04 16:00
roconnoris acc specifically mentioned in this paper?08/04 16:01
faxactually I think it is..08/04 16:01
edwinbI think it's in my thesis08/04 16:02
edwinbI can't remember though, it was so long ago ;)08/04 16:02
fax7.3Accessibility Predicates08/04 16:02
faxbut this is Bove-Capretta08/04 16:02
faxwhich is slightly different from Acc08/04 16:02
roconnorprobably close enough08/04 16:03
edwinbaha. Page 51 of my thesis08/04 16:03
roconnordoes this mean there is no need to separate Prop and Set universes?08/04 16:04
edwinbactually, no, not page 51, that doesn't explain it08/04 16:04
faxI had always gathered that 'Prop/Set distinction' is just one way to do it08/04 16:04
edwinbwell it's still useful08/04 16:04
faxedwinb yes I am not happy about #debill too!08/04 16:05
Saizani guess it's still useful to have an equality proof for free for anything that's in Prop08/04 16:05
Saizan#debill ?08/04 16:06
* edwinb blinks08/04 16:06
faxyou twitted about it 4 hours ago and already forgot ? :p08/04 16:06
edwinbno, I just forget that people might notice the rubbish I talk on twitter ;)08/04 16:06
edwinb(It was more than 4 hours ago, that gadget is broken)08/04 16:07
faxSaizan - I think they're making up crazy laws to give them stronger control of people08/04 16:07
faxanyway a bit paranoid08/04 16:07
faxseems 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 communication08/04 16:07
Saizanah, i've read about that08/04 16:08
pigworkerroconnor: comment shipped!08/04 16:10
roconnorthanks08/04 16:10
edwinbAnyway. The intuitive reason why Acc is erasable is that the arguments to constructor just get you another Acc in the end08/04 16:10
edwinbso 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
edwinbsame goes for Bove-Capretta domain predicates08/04 16:11
faxedwinb - 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
edwinbdo you have an example in mind?08/04 16:11
edwinbThe only implementation of this I know of is in Idris, and that just picks the first erasure it sees08/04 16:11
edwinbif there's a choice between erasing an index or a constructor tag, it erases an index08/04 16:12
faxoh well I recall some on the paper there was 3 different ways to erase things from Vec-E08/04 16:12
edwinbah right08/04 16:12
edwinbyes, that didn't explain. But in practice I've found it only makes sense to erase tags if you end up erasing the entire thing08/04 16:13
faxthat sounds good yeah -- and certainly that case will apply to (zero or) one constructor types like Acc08/04 16:13
edwinbyes08/04 16:13
faxhmm08/04 16:13
faxso okay I have another question :)08/04 16:13
edwinbincidentally, I've also found doing this erasure step makes compilation faster overall08/04 16:14
edwinbbecause code generation is much easier ;)08/04 16:14
faxwhat if I defined a relation a < b then write a function  subtract : forall a b : |N, a < b -> |N08/04 16:14
Saizanit's still whole program compilation though, right?08/04 16:14
edwinbfax: 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 relation08/04 16:16
edwinbSaizan: it is, but I don't think it has to be08/04 16:16
edwinbI might have to think about that soon. Compilation times are starting to get a bit irritating for bigger things.08/04 16:17
pigworkerfax: 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 relation08/04 16:18
faxwhat's a squashed set?08/04 16:19
faxI think I read about squash types actually, and you can make a monad out of them08/04 16:19
faxbut how would you define it in say epigram ?08/04 16:19
faxor would it be a feature08/04 16:20
roconnorI like to pretend a squashed type of A is (A -> 0) -> 0, though this isn't quite true08/04 16:20
edwinbI just happen to have this example handy, hang on...08/04 16:20
pigworkerfax: it's a set with all elements identified; or in Epigram 2 (already!) it's the proposition that a set is inhabited08/04 16:21
roconnorah right, inhabited A08/04 16:21
roconnorpigworker: are there any advantages of squash types over (A -> 0) -> 0?08/04 16:22
edwinbhttp://www.cs.st-andrews.ac.uk/~eb/hacking/minus.idr08/04 16:22
edwinbhmm, something mysterious has happened there08/04 16:23
faxmysterious?08/04 16:26
edwinbI fixed it an reuploaded in the hope you wouldn't notice the bug in the optimiser that was overzealous ;)08/04 16:27
pigworkerI 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 care08/04 16:27
Saizanbtw, 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
dolioNathan 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
dolioI guess roconnor's gone now, though.08/04 16:34
faxhi dolio I have had lots of questions to ask you !! but I odn't remember them now :)))08/04 16:37
dolioHeh.08/04 16:39
pigworkerSaizan: strictly speaking, you also need to make sure simplification terminates and check uniqueness of the resulting normal forms08/04 16:40
pigworkerdolio: what happens to propositional equality in Nathan's setting?08/04 16:41
dolioI 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
Saizanpigworker: ah, yeah, makes sense :)08/04 16:42
pigworkerdolio: I had a conversation with Nathan where it became clear that erasing equality proofs in open computation caused bad things to happen08/04 16:42
doliopigworker: 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
faxit's a good way to implement unsafeCoerce in haskell08/04 16:43
dolioAh.08/04 16:43
fax(though that's about nontermination rather than open)08/04 16:43
doliopigworker: Basically, everything in it gets erased and 'refl' tokens get passed around.08/04 16:44
dolioMaybe that isn't a Prop vs. Set issue, though.08/04 16:46
pigworkerdolio: ok, three questions; is equality elimination strict? is equality proof irrelevant? are refl tokens passed in closed computation?08/04 16:46
dolioSince you've all just been discussing similar problems with erasing Props.08/04 16:46
dolioI'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
dolioAs I said, though, I haven't actually read the section on proof irrelevance yet.08/04 16:48
pigworkerdolio: 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
glguyWhat is a good reference for the typing rules pertaining to the different Set levels?08/04 18:04
faxglguy I think they just make it up as they go08/04 18:05
faxthere's a reference manual in development but I don't think it has anything about this yet08/04 18:06
faxhttp://article.gmane.org/gmane.comp.lang.agda/1092/ that's probably the most official thing, and  the source code most formal08/04 18:08
dolioWithout 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
dolioAnd the sort of (co)data types has to be big enough to type the constructors.08/04 18:23
dolioWith 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
BiscuitsLapI'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
faxdo you know haskell09/04 02:28
BiscuitsLapYes09/04 02:28
faxand GADTs?09/04 02:28
BiscuitsLapHmm, we've discussed those, but I wouldn't say I'm fluent in them :/09/04 02:28
faxyou probably saw that cheesy 'well typed evaluation' example09/04 02:28
BiscuitsLapThe only real example in the slides is one for n+0==n09/04 02:29
dolioIs that cheesey?09/04 02:30
BiscuitsLapDon't suppose anyone has a link to that cheesy example :p? might help ;)09/04 02:31
doliohttp://65.254.53.221:8000/630509/04 02:34
Saizani'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 scenes09/04 02:34
BiscuitsLapSo does anyone know of anything that might help me ?09/04 02:41
faxwith what exactly09/04 02:42
BiscuitsLapUnderstanding how to prove things with those kind of functions :/09/04 02:43
faxI don't really know what you mean09/04 02:43
BiscuitsLapWell, first assignment was to write a unitMatrix function and a transpose function for matrices (Vec (Vec A m) n),09/04 02:44
faxthat sounds cool09/04 02:44
BiscuitsLapsecond is to prove that transpose (unitMatrix {n}) == unitMatrix {n}09/04 02:44
faxoh that sounds very difficult09/04 02:44
faxcan I see these functions09/04 02:44
SaizanBiscuitsLap: are you stuck with something in particuler?09/04 02:45
BiscuitsLapthis is what I have so far: http://www.pastebin.org/14224309/04 02:45
faxI think he's stuck with the transpose proof ?09/04 02:45
faxthis proof looks incredibly difficult09/04 02:46
BiscuitsLapSaizan: 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
BiscuitsLapWell, luckily it's just an optional part of the assignment, but I'd still like to know how to approach a problem like that09/04 02:47
BiscuitsLapoh btw those ==< > and ==# helpers were from some other document I read on this, weren't part of the slides/lecture or assignment09/04 02:48
faxin the suc n case,09/04 02:48
faxit's proving:09/04 02:48
faxtranspose (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
faxprobably that will use recursion having a proof of  transpose (unitMatrix {n}) == unitMatrix {n}09/04 02:48
faxbut you can unfold the transpose to see proving that ^ is the same as proving this:09/04 02:49
faxzip 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
Saizanyeah, since unitMatrix {suc n} is defined in terms of unitMatrix {n} you want to recurse with transpose-unit too09/04 02:50
faxoops that 'toprow' should have been something else09/04 02:50
Saizan(probably)09/04 02:50
faxso , correction:09/04 02:50
faxzip (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
faxnow you can clearly see where it starts to get awkward09/04 02:51
faxhere it has got 'transpose2' but our recursive case has only mention of 'transpose'09/04 02:51
Saizanfax: i think you mixed up the defs of transpose and transpose209/04 02:52
BiscuitsLapHmm, yeah09/04 02:52
faxyou're right!!09/04 02:52
BiscuitsLaptranspose2 was just another definition I thought would help out at some point09/04 02:52
faxthat is good news because it means the proof will be easier09/04 02:52
BiscuitsLapHmm, 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
faxyes09/04 02:57
BiscuitsLapfax: Would this definition make my life easier http://www.pastebin.org/142256 ?09/04 03:01
faxit's much closer to the other thing so they the proof they are equivalent will be easier09/04 03:02
BiscuitsLapok, so with that definition I can do transpose-unit {suc n} = cong increaseUnitMatrix ?09/04 03:03
faxno09/04 03:03
BiscuitsLap?09/04 03:04
BiscuitsLapHow about:09/04 03:05
BiscuitsLaptranspose-unit {suc n} = cong (_::_ (1 :: vmap head (vmap (_::_ 0) unitMatrix))) { }3 ?09/04 03:06
BiscuitsLapboth 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
BiscuitsLapThat 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
faxthat sounds good09/04 03:09
BiscuitsLapI suspect I'd have to use trans from there09/04 03:11
BiscuitsLapWhere I'd first prove something like vmap (_::_ 0) matrix == zip (replicate n 0) matrix _::_09/04 03:12
BiscuitsLapWould that move me in the right direction ?09/04 03:15
faxyes09/04 03:15
BiscuitsLaphmm, let's try09/04 03:16
Saizanmh, how'd you call a proof of transpose (replicate n x :: m) == vmap (_::_ x) (transpose m) ?09/04 04:33
BiscuitsLap?09/04 04:40
BiscuitsLapNot sure09/04 04:40
BiscuitsLapBut you sure are going faster than I am :/09/04 04:40
Saizanwell, yeah, i've completed the proof, but i've quite more experience with Agda :)09/04 04:46
Saizanbtw, some nice properties to have about vmap are:09/04 04:47
Saizanvmap-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)) v09/04 04:47
Saizanand09/04 04:47
Saizanvmap-id : ∀ {A} {n} {v : Vec A n} -> vmap (λ x -> x) v == v09/04 04:47
BiscuitsLapooh, I was already working on the vmap-fusion one :p09/04 04:48
Saizanthose are the functor laws for "\ A -> Vec A n", btw :)09/04 04:49
BiscuitsLap:-/?09/04 04:49
Saizanoh, 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
BiscuitsLapHmm, vmap-id was easy enough :)09/04 04:54
Saizanthey are quite similar, both simple inductions on the vector09/04 04:55
BiscuitsLapHmmm, one last bit to solve09/04 04:57
BiscuitsLapcurrently I had vmap-fusion {A} {B} {C} {g} {f} {zero} {[]} = refl09/04 04:58
BiscuitsLapand vmap-fusion {A} {B} {C} {g} {f} {suc n} {v :: vs} = cong (_::_ ?) vmap-fusion09/04 04:58
BiscuitsLapstruggling to define that ?09/04 04:58
BiscuitsLapwhen I try to fill in "f ?", which should be of type C as requested, it fails :/09/04 04:59
BiscuitsLapoh09/04 04:59
BiscuitsLapnvm09/04 04:59
Saizanyou need some parentheses around that09/04 04:59
Saizani.e. cong (_::_ (f ?)) vmap-fusion09/04 05:00
BiscuitsLapWon't work either09/04 05:01
Saizanoh, you switched f and g09/04 05:01
Saizanin the patterns09/04 05:01
BiscuitsLapAh, crap, yes09/04 05:02
BiscuitsLapSorry about that :/09/04 05:02
Saizanbtw, you can bind arguments by name, rather than position09/04 05:02
BiscuitsLapoh ?09/04 05:02
Saizane.g. vmap-fusion {f = f} {g = g} {v = x :: xs} = cong (_::_ (f ?)) vmap-fusion09/04 05:03
BiscuitsLapoooh, nice :)09/04 05:03
BiscuitsLapthat certainly cleans things up09/04 05:04
BiscuitsLapGreat, I've just written my first two actual proofs in agda :p09/04 05:04
Saizan(tbc i could have said e.g. {f = foo}, since the one on the right is just bound there)09/04 05:04
BiscuitsLapYup, found out by the v = x :: xs part, thanks :)09/04 05:05
Saizancongrats for the first proofs :)09/04 05:07
BiscuitsLapwould this be a good next step: transpose-inner : forall {A} {m n : N} {matrix : Matrix A (suc m) (suc n)} -> transpose (tail (vmap tail matrix)) == tail (vmap tail (transpose matrix))09/04 05:09
BiscuitsLap?09/04 05:09
BiscuitsLapwait...09/04 05:12
BiscuitsLapthat's probably not even true :/09/04 05:12
BiscuitsLapor is it :S09/04 05:13
Saizanmh, i don't think it is in general09/04 05:14
BiscuitsLapHmmm09/04 05:14
Saizani didn't had a reason to try to prove that since i went with your original transpose09/04 05:15
BiscuitsLapthat was the (vmap head mat) :: transpose (vmap tail mat) one, right ?09/04 05:16
Saizanyeah09/04 05:21
BiscuitsLapok, let's see, what kind of properties would I need, and what kind of properties could I deduce :/09/04 05:22
Saizanwell, first of all, that transpose recurses on "n", so your proof is probably going to do the same, so you get the application to reduce09/04 05:24
Saizanthen 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
Saizani'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
BiscuitsLapgah...09/04 05:37
BiscuitsLapBeen 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
BiscuitsLapJust found out that refl suffices in both cases :/09/04 05:38
BiscuitsLapHmmm09/04 06:07
BiscuitsLapI'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
BiscuitsLapI think it should be the subst rule, since I want to substitute the vmaps with another vmap09/04 06:08
Saizanvmap-fusion is not that useful there, actually09/04 06:10
Saizanhowever you'd use trans09/04 06:11
Saizan"trans vmap-fusion ?" should fit there09/04 06:11
Saizanhowever i think that proof is easier if you generalize over the matrix09/04 06:12
Saizani could be wrong though :)09/04 06:12
BiscuitsLapHmm, currently stuck at proving09/04 06:16
BiscuitsLapsillyproof3 : {n : N} -> (vmap (\x -> 0) (unitMatrix {n})) == (replicate n 0)09/04 06:17
BiscuitsLapshould be easy enough to solve :/09/04 06:17
BiscuitsLapbut I'm just not getting it09/04 06:17
BiscuitsLapoooh, got it :)09/04 06:29
BiscuitsLapSaizan: 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
BiscuitsLapoh wait, I think I got it working09/04 06:35
BiscuitsLapHmm09/04 07:00
BiscuitsLaphow 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
roconnorSaizan, edwinb: I don't get why having a prop universe is needed in light of edwin's erasure mechinicm.09/04 10:33
roconnorisn't everything you put into prop already provably proof irrelevent?09/04 10:33
roconnoroh, but maybe not definitionally proof irrelevent.09/04 10:34
roconnorare two variables of the same proposition convertable?09/04 10:34
Saizanroconnor: it's at least trivial to prove equality of proofs09/04 12:39
Saizan make eq := (\ P Q p q -> _) : (P : Prop) (Q : Prop) ( p : :- P) (q : :- Q) -> :- p == q09/04 12:39
SaizanMade.09/04 12:39
roconnormeh09/04 12:39
roconnorit is simply *more* trivial09/04 12:39
roconnorseems better to use generic programming than bake a special universe of propositions into the language09/04 12:40
Saizanthey might be convertible too, i'm not sure09/04 12:40
roconnorya, if they are convertable then that is something more.09/04 12:43
* Saizan wonders how you test that09/04 12:44
Saizani think it's also to let coerce work without ever having to be strict on the equality proof09/04 12:50
Saizanbut that could have been guaranteed by how you define == i guess09/04 12:52
roconnorisn't coerce never strict on any equality proof?09/04 13:06
roconnorwhether it is equality of set universe or prop universe09/04 13:06
Saizanroconnor: 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 sum09/04 13:34
Saizanerr, that's not right09/04 13:34
Saizanwell, 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
Saizanso, disregard that :)09/04 13:35
pigworkerroconnor: 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 work09/04 20:34
Spockzwhat is the difference between n and .n (dot) in "n != .n"? Is it that the dot denotes some kind of type or something?09/04 22:31
fax. means that terms was inferred/forced by pattern match specialization09/04 22:31
Spockzokay thanks :)09/04 22:33
liyangif it says n != .n, those are two distinct names… (FYI.)09/04 22:37
Spockzliyang: but it is based on something right?09/04 22:41
liyangYes. 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
roconnorin OTT are two variables of the same proposition type convertable?11/04 11:29
pigworkeryes.11/04 11:29
roconnorneat11/04 11:32
roconnorso two proofs of Acc foo won't be converable since Acc won't live in Prop.11/04 11:33
roconnorah11/04 11:34
roconnorbut it has to be that way11/04 11:34
roconnoras you said11/04 11:34
roconnorotherwise open reduction may not terminate11/04 11:34
pigworkeryes.11/04 11:34
roconnorso it is impossible, at least for now11/04 11:34
pigworkerthe two Acc proofs will be provably equal11/04 11:34
roconnorsince a few years ago extentional equality and decidable type checking was also "impossible"11/04 11:35
pigworkerthe 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 irrelevant11/04 11:37
roconnorI 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
roconnormore concretely put, is there a translation of OTT to the Prop free fragment of OTT11/04 11:38
pigworkerit's just an optimization11/04 11:38
pigworkermore concretely, yes there is such a translation11/04 11:38
roconnorneat11/04 11:39
roconnorokay I will think of Prop as an optimization11/04 11:39
dolioThat's how they define OTT in most of the papers, as I recall.11/04 11:39
dolioOTT gets translated into a type theory with just 0, 1, 2, Pi, Sigma, W.11/04 11:39
pigworkeryeah, the Agda models are all in Set, with no def-prf-irr, but prop-prf-irr11/04 11:40
pigworkerThe models have all the beta-behaviour of OTT, but a weaker equality on neutral values.11/04 11:42
pigworkerWe call this weaker theory OTT-11/04 11:43
roconnorif variables of the same type are converable, then OTT must not be strongly normalizing11/04 11:44
roconnor(though even coq is not strongly normalizing)11/04 11:44
pigworkerOTT- is still extensional: it models extensional type theory (it implements Oury's API for extensionality)11/04 11:45
pigworkerThe beta-rules are strongly normalizing, but they aren't the whole story.11/04 11:47
pigworkerThere'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
liyangDoes 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
Saizanmh, i think i saw that too13/04 18:59
liyangShall wait 'til he shows up.13/04 19:03
dolioliyang: Sounds like something on the SHE page.13/04 20:03
faxthere 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 often13/04 21:16
liyangpigworker: 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
pigworkerliyang: http://img688.yfrog.com/i/3l5.jpg/13/04 21:16
faxis that from a set ?13/04 21:17
liyangpigworker: 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
pigworkerIt 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
faxset13/04 21:18
faxpigworker (I think there's a missing newline in the draft of ornaments --3. definition of Alg)13/04 21:19
pigworkerfax: if that was all that was missing, I'd be a happy man...13/04 21:19
faxthis ornament stuff is so frustrating because I totally could have come up with that if I had just trid harder ;)))13/04 21:19
faxoh what d you mean?13/04 21:20
faxthere is more to do with it13/04 21:20
pigworkerThe Ornaments draft is quite a bit of windup but no punchline.13/04 21:22
pigworkerhttp://personal.cis.strath.ac.uk/~conor/pub/OAAO/Ornament.agda13/04 21:24
pigworkerPayoff 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
pigworkerPayoff 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
faxand that (2) proves that stack compiler respects evaluation ?13/04 21:30
pigworkeryep13/04 21:31
pigworkerbut the code of the compiler is just the same as it would have been13/04 21:31
pigworkerof course, it's not always such an instant win, but it is progress13/04 21:33
kosmikusI think it's a very beautiful result.13/04 21:34
pigworkerOnce 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
faxwait this is awesome13/04 21:47
faxif I defined + on nat it induces ++ on list AND vector13/04 21:47
pigworkerfax: depends how you define +, but you should get it cheap, certainly13/04 21:48
pigworkerThe question is how to turn ornaments on functors to ornaments on their (co)algebras.13/04 21:53
fax(just noticed also that  data Data (D : Desc I) ... : [[ D ]] (Data D i) -> ... should  probably be  [[ D ]] (Data D) i13/04 22:00
faxon pg. 413/04 22:00
pigworkerfax: seems likely, thanks13/04 22:47
--- Day changed Wed Apr 14 2010
liyang(I think) I understand what it means to be parametric, but what are the immediate consequences of defining propositional equality as data _≡_ {a : Set} : a → a → Set , versus the standard library's data _≡_ {a : Set} (x : a) : a → Set ?14/04 00:47
liyangDoes 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
copumpkinhmm14/04 00:49
faxthey're logically equivalent14/04 00:50
faxdata Identity1 (A : Set) : A -> A -> Set where refl1 : forall (a : A) -> Identity1 A a a14/04 00:51
faxdata Identity2 (A : Set) (a : A) : A -> Set where refl2 : Identity2 A a a14/04 00:51
faxid12 : forall {A : Set} (a : A) -> Identity1 A a a -> Identity2 A a a14/04 00:51
faxid12 .a (refl1 a) = refl214/04 00:51
faxid21 : forall {A : Set} (a : A) -> Identity2 A a a -> Identity1 A a a14/04 00:51
faxid21 a refl2 = refl1 a14/04 00:51
liyangBut computationally?14/04 00:51
faxI don't know which one is better14/04 00:52
faxcomputationally?14/04 00:52
faxI am pretty sure you can compile them both away14/04 00:52
fax(to nothing)14/04 00:52
copumpkinwill agda?14/04 00:52
faxno14/04 00:52
liyangIt'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
faxI think 2 is easier to use14/04 00:53
faxbecause you don't have to worry about the actual element -- type inference does taht14/04 00:53
liyang(by intuitive, I mean symmetrical.)14/04 00:54
faxliyang, if you try to prove transitivity14/04 00:56
faxtrans : forall {A : Set} (a b c : A) -> Identity A a b -> Identity A b c -> Identity A a c14/04 00:56
liyangWell, you could write refl : {x} -> x == x , where type inference will fill in the actual element.14/04 00:56
faxfor both types,  that might convince you that one is nicer to use than the other14/04 00:56
liyangfax: ahhh hah. I see.14/04 00:57
faxdata JMeq (A : Set) (a : A) : forall (B : Set) (b : B) -> Set where JMrefl : JMeq A a A a14/04 00:58
faxthis is a good one for Agda14/04 00:59
faxdata 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 I14/04 01:00
faxthat is useful in Coq14/04 01:00
faxdecidible equality on U lets you prove K axiom14/04 01:00
faxbut you don't want that in agda because you can prove K from the pattern matching14/04 01:01
liyangfax: hang on, both proofs of transitivity are the same… http://moonpatio.com/fastcgi/hpaste.fcgi/view?id=1009714/04 01:21
* liyang didn't see after all.14/04 01:21
faxtrans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c14/04 01:21
faxtrans1 a .a .a (refl1 ._) (refl1 ._) = refl1 _14/04 01:21
faxtrans2 : forall {A : Set} (a b c : A) -> Identity2 A a b -> Identity2 A b c -> Identity2 A a c14/04 01:21
faxtrans2 a .a .a refl2 refl2 = refl214/04 01:22
faxwell14/04 01:22
faxtrans1 : forall {A : Set} (a b c : A) -> Identity1 A a b -> Identity1 A b c -> Identity1 A a c14/04 01:22
faxtrans1 a .a .a (refl1 .a) (refl1 .a) = refl1 a14/04 01:22
faxlet me be explicit14/04 01:22
liyangOnly if you make the argument of refl1 explicit…14/04 01:22
liyangI had defined refl : {x : X} -> x ≡ x14/04 01:23
liyangThe two definitions of == in my pastebin above seem to be interchangeable, at least with trans.14/04 01:24
faxin coq, you can still supply the parameters14/04 01:26
faxi.e. A and a in refl214/04 01:26
faxthe difference there, is there is a slightly different type of type inference -- called maximal insertion14/04 01:27
faxI think you could be right though, and given the {} annotation that these are interchangable14/04 01:28
* liyang isn't entirely au fait with Coq.14/04 01:28
faxwell I just mention it because the difference between these two versions is more apparent in Coq14/04 01:28
liyangmmkay…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
pigworkerThey 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
faxahh need to remember that14/04 01:31
liyangThat can't just be the end of it, shurely?14/04 01:31
liyangAre there any reasons to prefer one over the other, at least in the context of Agda?14/04 01:33
pigworkerYou've gotta watch the sizes of things. Parameters can be large, but indices are (currently, mysteriously) obliged to be small.14/04 01:33
pigworkerP-M eq beats M-L eq in Agda. Why make refl store more stuff?14/04 01:34
liyangSo, just “<liyang> Does it just mean that refl needn't carry around a copy of x, in order to serve as a witness to x ≡ x?” ?14/04 01:35
* liyang isn't terribly clear on the large/small distinction, and now is probably not a good time to inquire about it.14/04 01:36
faxwhat 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 indices14/04 01:36
fax(bool is a bad example I guess.... maybe bad enough it ruins the actual question, since we'd probably have Maybe/option P at least)14/04 01:37
pigworkerIIRC there is some size paranoia which stops the two presentations being equivalent under all circumstances, but usually it's no big deal14/04 01:38
liyangMmkay. I'll go with M-L equality as it seems easier to explain, storage be damned.14/04 01:40
pigworkerliyang: 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
liyangpigworker: this is just for an introductory section to dependent types. I wouldn't dream of writing untidy code. :314/04 01:47
pigworkerfax: 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 runtime14/04 01:47
pigworkerliyang: whatever gets you where you need to go14/04 01:48
pigworkerJust 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
faxequality made my attempts to implement category theory fail :(14/04 01:52
pigworkerfax: or vice versa14/04 01:52
pigworkerg'night all14/04 01:59
copumpkinoh my14/04 02:01
copumpkinI missed pigworker14/04 02:02
copumpkinit feels like forever since I last wrote any agda14/04 16:15
faxIt's been seven hours and fifteen days14/04 16:16
copumpkinlol14/04 16:16
copumpkinI'm glad you're keeping track :)14/04 16:16
Saizan_copumpkin is back!14/04 16:19
copumpkinmore or less :)14/04 16:19
stevanhello, 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
faxnot to me14/04 16:27
faxyou're turning a list [A] into [Sigma a : A, P(a)] ?14/04 16:27
faxby filtering out things which don't have property P14/04 16:28
stevanyeah something like that14/04 16:28
faxdifferent in what ways?14/04 16:28
Saizan_the part after "so that" is quite unclear14/04 16:29
stevanfax: 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
stevanSaizan_: well say you filter out all zeroes from a list, then when you go thru that filtered list every time you hit a suc constructor you could say this is absurd, because filter should have removed all non-zero nats... is that clearer?14/04 16:32
Saizan_i understand "filtering out" as "removing"14/04 16:33
Saizan_but i'm not a native speaker14/04 16:33
faxI guess you can also just have filter atke [A] -> [A]14/04 16:33
faxbut then prove sepeartetly (P1) xs >= filter xs  (P2) In x xs -> P x14/04 16:34
Saizan_http://www.google.com/dictionary?aq=f&langpair=en|en&hl=en&q=filter%20out <- google agrees with me though14/04 16:34
faxbut I don't know, that is probably harder to program with, because you'll need to construct In proofs as you o through the list14/04 16:34
faxoh and that P2 was wrong14/04 16:34
dolioStop absuring the man! :)14/04 16:35
faxSaizan, if you think about say a gold pan -- that lets water through but keeps the bits of gold ... the question is, did it filter out the gold or filter out the water?14/04 16:35
Saizan_i'd say it filtered out the water14/04 16:36
copumpkinthis is so philosophical!14/04 16:36
dolioIt filtered out the gold.14/04 16:37
dolioWhat comes out of the filter is water without gold. The gold gets caught.14/04 16:38
dolioFiltered out of the water.14/04 16:38
dolioOr mud. Or what have you.14/04 16:38
faxif I passed through a filter, was I filtered?14/04 16:38
Saizan_ooh, so what you filter out is what gets caught in the filter14/04 16:38
faxbut if you got stuck in the filter, were you filtered?14/04 16:38
faxmaybe BOTH ?14/04 16:38
Saizan_i was just thinking in terms of keeping vs. removing14/04 16:38
Saizan_i.e. seeing the filter as merely a splitter14/04 16:39
TheOnionKnightalmost sounds like you want List A -> List (Sigma (x : A) -> Dec (P x)) ?14/04 16:39
faxwell the way stevan put it was defintiely contrary ti what I thought about before14/04 16:39
dolioFiltered water is what you're left with after you filter out the impurities.14/04 16:39
faxbut I am not sure that I can say it's wrong14/04 16:39
dolioAnd the impurities get caught in the filter.14/04 16:39
copumpkinif you empty out the filter though, what are the impurities?14/04 16:39
copumpkinare they filtered impurities?14/04 16:39
Saizan_dolio: ok, i see it now14/04 16:39
faxTheOnionKnight: oh that's neat because it's just map14/04 16:40
faxthen you can use a normal filter14/04 16:40
faxhmm no14/04 16:40
stevanit reminds me of the sublist exercise in ulf's tutorial, but you need to stick the proof in there somehow14/04 16:42
faxthere's two different properties though14/04 16:42
pigworkerWhat does filter tell you about its input?14/04 16:45
faxyou 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
pigworkeran algebraic ornament, indeed!14/04 16:53
faxohh :D14/04 16:53
Saizan_you could keep "not (P x)" in there too at that point :)14/04 16:53
pigworkeryou could also index by the yes- and no-lists14/04 16:54
dolioThe types reddit is really languishing.14/04 16:58
dolioApparently the only types worth talking about these days are dependent types.14/04 16:58
faxwhy the fuck is there like 10 reddits about dependent types :/14/04 16:59
faxworse than /types/ having no activity is jbapple stopped blogging14/04 17:00
dolioI could do with more constructive gems/stones, too.14/04 17:09
fax:(14/04 17:10
faxsometimes there are "proof pearl" papers which I can't acess14/04 17:10
copumpkinI can fetch them for you if you want14/04 17:10
copumpkinif you don't rat me out14/04 17:10
faxwell something I WOULD like is a list of all of them14/04 17:10
faxbut I am not sure if that actually exists14/04 17:10
dolioThe last 'classical mathematicians confuse proof by contradiction with proof of negation' was amusing, but not particularly exciting.14/04 17:11
faxthe closest to a list of the 'functional peal's we have is that haskell wiki14/04 17:11
ccasinSo 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 language14/04 17:18
ccasinanyone know if that's right, and if anyone has actually worked out the metatheory in detail for one of the languages where we hardwire in indexed datatypes?14/04 17:18
ccasin(sorry to drag the conversation away from fun programs towards scary theory)14/04 17:18
pigworkerccasin: 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 itself14/04 17:20
pigworkerccasin: Calculus of Inductive Constructions takes a more internal view, although descriptions of datatypes are not first class14/04 17:21
ccasinpigworker: yeah, thanks.  And it seems like these new primitive types in UTT don't have parameters/indices.  He only adds those using the metatheory14/04 17:22
ccasinthat is, inductive pairs aren't a UTT type, only an LF construction (even after we add them as a primitive)14/04 17:23
ccasinI should read some of the early Cic papers, thanks14/04 17:24
pigworkerccasin: Each Sigma A B has kind Type (ie is a UTT type), but Sigma itself is a meta-level thing.14/04 17:24
pigworkerI 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
dolioLike 'f (x .:: xs) cons-proof' instead of 'f .(x :: xs) (cons-proof {x} {xs})'?14/04 17:39
pigworkerdolio: the very thing14/04 17:39
dolioYeah, I've run into that before.14/04 17:39
faxdoes  f (x :: xs) .cons-proof = ... work?14/04 17:39
pigworkerfax: no, it makes f too strict14/04 17:40
pigworkerwhat's that pastebin thing again?14/04 17:42
copumpkinmoonpatio.com14/04 17:42
pigworkerconnection trouble; made a repo on the web for fooling about; here's a filtery thing http://personal.cis.strath.ac.uk/~conor/fooling/Splice.agda14/04 17:47
copumpkinomg no unicode14/04 17:49
pigworkerI hate unicode14/04 17:50
copumpkin:)14/04 17:50
copumpkinsometimes I think NAD peruses code tables looking for the most obscure symbols for the standard library14/04 17:50
pigworkerearly adopters...14/04 17:52
npouillardpigworker: have you any good reason? sure there is some initial configuration cost but that's not that hard14/04 17:52
faxthat's neat with the split sort of like  [Either a b] -> ([a],[b])14/04 17:53
kosmikusthe 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 it14/04 17:53
copumpkinyeah14/04 17:53
pigworkernpouillard: even now, it's not a reliable exchange format14/04 17:53
faxI think unicode just delays proper typesetting longer14/04 17:54
npouillardfax: I think it is orthogonal14/04 17:54
pigworkernpouillard: and my typing isn't reliable enough, and massive keyboard shortcut customization is the road to hell14/04 17:55
faxI mean the silly bits, like little superscript 2's and fractions14/04 17:55
npouillardeven when doing proper typesetting you may want something nicer than \alpha14/04 17:55
npouillardpigworker: it becomes more reliable when people use it14/04 17:55
npouillardPersonally I use a .XCompose file under linux, so it works in any X application, and is nicely configurable14/04 17:57
kosmikusyes, ultimately I think it's good to have more symbols available14/04 17:57
kosmikusnpouillard: I'll look into that14/04 17:57
faxwhat I really want is something that looks like epigram research papers :P14/04 17:57
fax(sort of like texmacs)14/04 17:58
pigworkernpouillard: 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 too14/04 18:00
pigworkerWhen 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
kosmikusme?14/04 18:03
kosmikus:)14/04 18:04
pigworkerkosmikus: no, but you do quite well14/04 18:04
kosmikuswhen it comes to LaTeX, I'm certainly guilty14/04 18:04
kosmikusalthough I usually know what packages I'm using and try to include them if they're exotic14/04 18:05
copumpkingotta use xetex14/04 18:05
pigworkerI heard a rumour that EasyChair was starting to support LaTeX-on-the-server.14/04 18:05
copumpkinso you can include exotic fonts that people have to pay for14/04 18:05
copumpkinjust to piss them off more14/04 18:06
kosmikuspigworker: I think it does. I used it recently.14/04 18:07
pigworkerIt 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
kosmikusyes14/04 18:08
pigworkerprogress14/04 18:08
kosmikusand you can check the pdf the server generates14/04 18:08
kosmikusa bit like what arxiv does since ages14/04 18:08
pigworkeryou'd kinda need that feedback14/04 18:09
pigworkergonna catch some sun while it's still up; back later14/04 18:25
stevansorry, had friends drop by... thanks for the help with filter, guys. i like the splice solution.14/04 19:19
stevankosmikus: 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
kosmikusstevan: yes, I noted that (viper)14/04 19:55
--- Day changed Thu Apr 15 2010
sah0sHi ... 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
sah0sI 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
faxit's like normal functional programming, except the types have a logical interpretation15/04 14:34
sah0sI have read http://en.wikipedia.org/wiki/Intuitionistic_type_theory15/04 14:34
npouillardfax: you can give a logical interpretation to System F types however15/04 14:35
sah0sI got that, the Curry-Howard isomorphism, I'm happy with that, in fact I love it15/04 14:35
sah0sWhat I'm saying is that I can't model Types in my head ...15/04 14:35
npouillardsah0s: even as just being sets?15/04 14:36
faxa type is just a name, you don't need to think of it as something15/04 14:36
sah0sI 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
dolioYou don't want to write a type system in C.15/04 14:37
npouillardsah0s: a type checker in C ?15/04 14:37
sah0snpouillard: set-like is fine with me15/04 14:37
faxI agree with dolio15/04 14:37
sah0sA type system with a checker, yeah ... as a library15/04 14:38
faxsah0s no this is where you are confused15/04 14:38
sah0sIf I have a clear idea of how to construct types then I can code it15/04 14:38
npouillardfax: your are a bit rude15/04 14:38
faxI find you quite rude too15/04 14:39
dolio(My point is that there are much nicer languages than C for doing it. Of course, if C is all you know, you don't have many options.)15/04 14:39
npouillardBut I agree that C is not a language to write a type-checker15/04 14:39
npouillardfax: sorry then15/04 14:39
sah0sIgnore the C bit for the moment :)15/04 14:39
sah0sI like C15/04 14:40
faxI wasn't talking about C when I said "This is where you are confused"15/04 14:40
sah0sEach to their own :)15/04 14:40
stevansah0s: do you know any functional programming language?15/04 14:40
sah0sCan we go through this page http://en.wikipedia.org/wiki/Intuitionistic_type_theory bit by bit, please!15/04 14:40
sah0sWhat is a Π-type exactly, I don't understand what it says.15/04 14:41
faxsah0s my advice is that wikipedia sucks and the reason you are confused is proabably from reading that page15/04 14:41
sah0sokay15/04 14:41
sah0sthis could well be true15/04 14:41
npouillardThis question is relevant "do you know any functional programming language?"15/04 14:41
sah0sI know a bit of scheme15/04 14:41
sah0sfunctions as first-class citizens15/04 14:42
npouillardto get Π you need to get →15/04 14:42
sah0stail recursion15/04 14:42
sah0s→ ?15/04 14:42
npouillardsah0s: sure but not much of a type system15/04 14:42
npouillardas in [a] → Int15/04 14:42
npouillardthe type of List.length15/04 14:42
npouillardlength : ∀ a. [a] → Int -- in haskell15/04 14:43
npouillardlength : ∀ {A} → List A → ℕ -- in agda but that merely the same thing15/04 14:43
dolioIt helps to get ∀, too15/04 14:43
sah0sis A a type variable?15/04 14:43
stevanmight 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
npouillardsah0s: yes15/04 14:43
npouillardstevan: yes15/04 14:44
sah0s∀ is universal quantification15/04 14:44
faxnpouillard: 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 that15/04 14:44
sah0smy feelings are not hurt, i just wanna learn, i have a thick skin, it's just that i'm can't understand the wikipedia entry15/04 14:45
npouillardsah0s: but with dependent types it is also the type of dependent functions15/04 14:45
sah0s*I can't15/04 14:45
sah0sah15/04 14:45
faxI have dabbled a bit with implementing different dependent type systems and I tell you that is it all syntax all the way down15/04 14:45
sah0sfax:  intersting15/04 14:45
sah0sfax: I had the idea that types are nothing more than syntax sliced one way or another15/04 14:46
faxThere 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 important15/04 14:46
sah0si 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
sah0sSo if I start from simply typed lambda calculus that'll give me a good idea?15/04 14:48
stevan(the book types and programming languages by pierce is a better resource than wikipedia also)15/04 14:48
faxThe 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 else15/04 14:49
faxsah0s -- oh well if you are building up a lambda calculus to program in that is quite reasonable15/04 14:49
npouillardfax: ok, I agree the "all about syntax" but not really the "it's nothing but names"15/04 14:50
faxI would probably not recommend TaPL because it doesn't go into detail on dependent types15/04 14:50
npouillardsure it makes sense to have primitve types like machine integers...15/04 14:50
faxwell it's a good book if you haven't understood way type systems are presented or haven't got induction yet15/04 14:51
sah0si have TaPL and I'm going through it slowly15/04 14:51
sah0sWhat are the atomic or base types in Agda?15/04 14:52
faxsah0s: 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
stevani'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
solidsnackI am following the instructions on the Agda VIM page but it looks like `agda --vim' does not do anything.15/04 18:13
solidsnackIs it no longer supported?15/04 18:13
stevanit generates a .vim file for syntax highlightning.15/04 18:17
solidsnackstevan: Where does it put the file?15/04 18:18
solidsnackI can't find anything with `ls -a' and I don't get error messages, either.15/04 18:18
stevansame dir, .filename.agda.vim15/04 18:18
solidsnackOkay, interesting -- it won't handle files inside a directory.15/04 18:20
solidsnackI have to CD to the directory the file is in; that's the problem I was having.15/04 18:20
stevani 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
solidsnackstevan: I did try that; I hate Emacs.15/04 18:22
solidsnackstevan: 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
solidsnackstevan: 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
stevanok, :-/15/04 18:26
solidsnackstevan: Sorry :) I can be pretty grumpy about this particular issue.15/04 18:38
faxwhich?15/04 18:39
glguycan I merge the following lines into one statement somehow?15/04 19:25
glguyimport Module15/04 19:25
glguyopen Module xval yval using (this; that)15/04 19:25
dolioopen import Modulse xval yval using (this ; that)15/04 19:26
dolioOr did that not work?15/04 19:26
dolioI'm not sure I've ever tried an open import for a parameterized module.15/04 19:27
stevani don't think it does. you could use a semicolon if you want the two on the same line.15/04 19:27
glguythat didn't seem to work15/04 19:27
glguyIt certainly isn't a big issue15/04 19:27
glguyI just wondered15/04 19:27
glguyimport Algebra.FunctionProperties15/04 19:28
glguyopen Algebra.FunctionProperties _≡_15/04 19:28
glguy  using (Associative; _DistributesOverˡ_; _DistributesOverʳ_)15/04 19:28
glguyMine already spans 3 lines15/04 19:28
glguyno sense in using any ;'s :-D15/04 19:28
* glguy is doing some exercises for an Isabelle course in Agda http://www.galois.com/~emertens/polynomials/session2eq.html15/04 19:31
dantenmaybe using as? import Algebra.FunctionProperties as AFP; open AFP _≡_15/04 19:34
danten  using (Associative; _DistributesOverˡ_; _DistributesOverʳ_)15/04 19:34
glguyYeah, that doesn't look too bad15/04 19:41
sah0shmm, 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 Thompson15/04 19:55
sah0smy mistake15/04 19:55
--- Day changed Fri Apr 16 2010
glguy_Is there a better approach to the last definition in http://www.galois.com/~emertens/replace/replace.html ?16/04 06:44
glguy_it just feels messy...16/04 06:45
--- Day changed Sat Apr 17 2010
glguyIt seems like Data.List's definition of reverse (specifically with the where-class defined helper) makes it very difficult to use in any proofs17/04 01:11
dolioIt definitely leads to some inconvenience.17/04 01:15
dolioSince you may want to prove lemmas about rev, but you can't actually refer to rev.17/04 01:15
glguyI'm not sure you can prove anything about it as it stands beyond reverse [] == []17/04 01:26
glguy(or some other constant expression)17/04 01:27
dolioYeah, it may well not be possible to prove things about reverse without lemmas about rev.17/04 01:36
dolioSince you may need to prove things by induction that you can't refer to simply by referring to reverse.17/04 01:37
dolioI'd probably go with a foldl definition, myself.17/04 01:52
sah0sYo. 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
sah0sHowever ...17/04 15:06
sah0s(always a however, heh)17/04 15:06
sah0sHowever, it seems to me that finite types can be built up inductively so I don't see the need for finite types. Anyone got any opinions ...17/04 15:07
sah0s?17/04 15:07
faxfinite types ?17/04 15:08
faxyou mean like N3 = {0,1,2} ?17/04 15:08
sah0sI 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
sah0shi fax17/04 15:08
faxhi17/04 15:09
sah0sYup, finite types: empty, unit, booleans (bivalent), trivalent, ...17/04 15:09
faxyou can define each one inductively, and infact you can define the whole (infinite) family of types inductively17/04 15:09
sah0sBut you can do this inductively as well if I am reading the page correctly is all that I'm saying :)17/04 15:09
sah0s"nfact you can define the whole (infinite) family of types inductively", huh?17/04 15:10
faxthere is not really much difference between just having these types as built in or being able to define them in the language17/04 15:10
sah0sall the types in the system?17/04 15:10
sah0ssure17/04 15:11
faxthis family of types: empty, unit, booleans (bivalent), trivalent, ...17/04 15:11
faxyou can define them all with a single definition17/04 15:11
sah0si think so too, it's nice that they have names though like you were saying17/04 15:11
sah0swith a single definition they don't have names really, just indexed17/04 15:11
faxyeah17/04 15:11
sah0si understand product, sum, inductive, finite ... having difficulty with univers and equality, especially equality17/04 15:12
sah0si just don't see how something that looks like an operation (equality) can be a type :(17/04 15:13
faxyou can define it like17/04 15:13
faxdata Identity (A : Set) (a : A) : A -> Set where17/04 15:13
fax refl : Identity A a a17/04 15:13
sah0suniverse seem to me to give you a hierarchy of families so I think I understand universes as well17/04 15:13
faxso now,  refl : forall {A : Set} {a : A}, Identity A a a17/04 15:13
faxthat means e.g. this judgement holds:   refl N 3 : Identity N 3 317/04 15:14
faxfor example17/04 15:14
faxthere is an equality check built into the type system though17/04 15:14
faxit's syntactic congruence + beta reduction + unfolding definitions (replacing names with values that is) + eta expansions + maybe other stuff too17/04 15:15
faxthe result is that you can also have judgements like   refl N 3 : Identity 3 (1 + 2)17/04 15:15
sah0suh...17/04 15:15
sah0sdoes the equality type extend the notion of the equality of base types into the rest of the type system?17/04 15:16
sah0sthe equality of objects of the base types i mean17/04 15:16
faxthe type system has got a notion of equality in it already,  the identity data types just reifies it17/04 15:17
sah0sreify?17/04 15:17
faxit makes it into a 'first class' citizen17/04 15:17
sah0swow17/04 15:17
faxdo you know prolog?17/04 15:17
sah0sages ago, unification, rules ...17/04 15:17
sah0swhy?17/04 15:17
faxif you ever saw the definition of unification in prolog:17/04 15:17
faxX = X.17/04 15:18
faxor17/04 15:18
faxequal(X,X).17/04 15:18
sah0suhuh17/04 15:18
faxthis is the same sort of thing17/04 15:18
fax(as the identity type defined above)17/04 15:18
sah0scan you give me a non-identity practical use of the equality connective?17/04 15:20
sah0si still don't get it, sorry - it is very alien to me (at least in the syntax above)17/04 15:20
faxwhich syntax17/04 15:21
sah0sdata Identity (A : Set) (a : A) : A -> Set where17/04 15:21
sah0srefl : Identity A a a17/04 15:21
sah0sso now,  refl : forall {A : Set} {a : A}, Identity A a a17/04 15:21
faxyou're not use to the ML style? of using whitespace for application17/04 15:21
sah0sno, sorry17/04 15:21
doliosubst : (A : Set) (P : A -> Set) (x y : A) (eq : Identity A x y) -> P x -> P y17/04 15:21
faxyou are missing out17/04 15:21
faxthis is important17/04 15:22
sah0sok17/04 15:22
faxf x (y z) w17/04 15:22
faxin scheme you would write it like17/04 15:22
fax(((f x) (y z)) w)17/04 15:22
sah0swhitespace for application!17/04 15:22
sah0swow17/04 15:22
faxf(x,y(z),w) in algolish17/04 15:23
sah0sbreaks homoiconicity though17/04 15:23
sah0svery neat shorthand17/04 15:23
sah0sdolio: ?17/04 15:23
faxI think you can recover most of the important parts of homoiconicity17/04 15:23
faxbut that is sort of an advanced topic17/04 15:24
fax(specific to dependent types)17/04 15:24
dolioThat 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
dolioOf course, you do have that, because that's the only thing that inhabits identity types.17/04 15:26
dolioWhich means x is actually y, or vice versa, and you use that to do the 'substitution'.17/04 15:26
faxsah0s - write a parser for this whitespace syntax in ocaml or haskell or something :P17/04 15:27
sah0sdolio: 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 use17/04 15:28
dolioWhat other connectives produce what interesting stuff?17/04 15:30
faxsah0s um well any time you use = sign in mathematics17/04 15:30
faxit's not exactly rare :P17/04 15:30
sah0s:P17/04 15:31
sah0ssigma connective produces pairs, triplets, ...17/04 15:31
faxit's true that ground inhabitants of Identity are boring17/04 15:31
sah0sfax: that's my point17/04 15:31
faxit gets interesting when you do e.g. some stuff -> Identity x y17/04 15:31
dolioWhat about: comm : (m n : Nat) -> m + n = n + m17/04 15:31
faxwhat it means is that it computes an identity proof from the stuff17/04 15:31
sah0sdolio: i get it know!17/04 15:32
sah0sdolio: oops, *now!17/04 15:32
sah0sdolio, the + though, how is the + interpreted?17/04 15:33
sah0s+ is a function type17/04 15:33
dolioHowever addition is defined for naturals.17/04 15:33
sah0swhere is the 'code' for + ?17/04 15:34
sah0sanyway i see what you mean, you use the equality type to build up laws17/04 15:34
dolioAssuming naturals are inductive Peano numerals, it goes 'zero + n = n ; (suc m) + n = suc (m + n)'17/04 15:34
faxjust 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
faxof course + and = make it much nicer to read17/04 15:36
dolioAnyhow, 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
sah0swhat about inequality relations?17/04 15:38
sah0sdo they make any sense in ITT?17/04 15:39
dolioYou mean stuff like less than, or just not-equal?17/04 15:39
sah0s< > !=17/04 15:39
sah0sor <> or however you wanna say it :)17/04 15:39
dolioPlain 'not-equal' is usually defined as x /= y = (x = y) -> False.17/04 15:40
dolioFalse being the type with no proofs.17/04 15:40
sah0sdolio: very nice17/04 15:40
faxnot X := X -> False  is a very interesting type17/04 15:40
sah0scan I read False as Absurdity as well?17/04 15:41
dolio< and > and such can either be defined inductively, or recursively.17/04 15:41
dolioI guess, inductively only if you have inductive families.17/04 15:41
sah0si had a brainwave regarding atomic/base types17/04 15:42
sah0sfax: you said that it was syntax all the way down17/04 15:42
sah0si believe that is only strictly true for atomic types17/04 15:43
faxwhat's an atomic type?17/04 15:43
sah0sbase type17/04 15:43
sah0sbuilt-in type17/04 15:43
sah0san irreducible type17/04 15:44
faxIt's possible to just give a schema for allowing new inductive defintions/declarations, and not have ANY built in types17/04 15:44
faxwell . you need the lambda calculus, which means that forall and * are built in17/04 15:44
faxbut you can now define everything like =, true, false, and, or, not, N, Z, Q, R etc.17/04 15:45
faxexists17/04 15:45
sah0sif 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
sah0sexists? surely not ...17/04 15:46
sah0s= is a connective, not a type17/04 15:47
sah0sand surely the function type is built-in ???17/04 15:47
dolioI'm not sure you can define R, unless you don't really care about having redundant elements.17/04 15:48
sah0sdolio: for a constructivist R is a fiction17/04 15:48
sah0swith a strict ITT, R is impossible I'd say17/04 15:48
faxI'm thinking of a different R than you17/04 15:49
faxcomputable reals17/04 15:49
sah0sdifferent R, go on I'll bite :)17/04 15:49
sah0sfax: nice17/04 15:49
dolioYou can represent constructive reals as something like Q -> Q.17/04 15:49
sah0sfax: computable transcendentals like e and pi, sure :)17/04 15:50
sah0sthat's the only way I believe they exist17/04 15:50
sah0sbut the set R of all reals, not a chance17/04 15:50
dolioBut 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
faxyeah quotient is something you cannot define interally17/04 15:51
sah0si think of transcendentals as machine that are unbounded in time and generate sequences of quotients, that's it17/04 15:51
faxinternally*17/04 15:51
faxI think you can do a whole-program style transformation into the setoid stuff17/04 15:51
faxbut that is kind of hard ..17/04 15:52
sah0sthere is no Set of all of these machines, a least nothing meaningful imnsho :)17/04 15:52
sah0sI'm going to a conference in may that is exploring this stuff :) want the link?17/04 15:52
dolioroconnor actually pointed out somewhere that the quotient R can be kind of useless.17/04 15:52
sah0si would believe that17/04 15:53
dolioFor instance, any function from R to a discrete set that respects the equivalent relation is constant.17/04 15:53
* fax confused17/04 15:53
sah0shttp://www.theinfinitycomputer.com/Infinity2010/index.php17/04 15:54
sah0sdolio: but we don't have R17/04 15:55
faxhypercomputation ?17/04 15:55
doliosah0s: I mean the constructive R, as specified above.17/04 15:55
sah0shmm, 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 result17/04 15:57
sah0s"Turing's writing made it clear that oracle machines were only mathematical abstractions, and were not thought of as physically realisable."17/04 15:58
sah0sanyway, ye've been really helpful and thought-provoking17/04 15:59
sah0si think it'll be years before this stuff goes mainstream though unfortunately, until then we have VB.net, ugh17/04 16:00
faxthat church-turing thesis is really frustrating, because there doesn't seem to be any way to prove it17/04 16:00
faxthere's all this... evidence though...17/04 16:00
faxI guess that it is one problem which is right in both computing and physics17/04 16:01
faxI find it amazing that quantum computation fits the same model.. but can do some things faster -- rather than being able to compute new things17/04 16:02
fax(but that's probably a summary of everything I know about quantum theory so I wouldn't even be sure it's true)17/04 16:02
sah0sif 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
faxI enjoy e non-rigorous proof but17/04 16:03
fax... that is pushing it ;D17/04 16:03
sah0soops, even quantum apple laptops will need batteries17/04 16:05
faxhaha17/04 16:05
sah0sfax: it is amazing that it's the same model17/04 16:09
sah0si like the way that it breaks classical encryption but provides a QC solution as well17/04 16:09
sah0sso it seems we don't have to change our notion of privacy and encryption17/04 16:10
sah0sthough i was reading about an idea for provably tamper-free connections which would be stronger than what we have now17/04 16:11
faxit's wild stuff I still haven't got my head about the basics like the deutch black box thingy17/04 16:13
sah0sanyway, 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
sah0sdavid deutsch is the man, the fabric of reality is an awesome book17/04 16:14
faxcool I hadn't heard of it17/04 16:14
faxyou should check out peter morris' PhD once you have got your legs17/04 16:15
sah0sit says that there are only 4 fundamental theories: the theory of computation, virtual reality, quantum theory and the theory of evolution17/04 16:15
sah0sfax: will do, in fact I'll have a quick look right now17/04 16:16
sah0snottingham again, what's in the water in nottingham?17/04 16:17
faxlol17/04 16:17
sah0sEpigram looks wild17/04 16:17
sah0s2 dimensional syntax, bizarre17/04 16:17
faxyeah Epigram is really exciting - I am still struggling to understand the theory of it a bit17/04 16:17
sah0sconor mcbride's writing is hilarious17/04 16:17
sah0sdoesn't seem too different from agda17/04 16:18
sah0si don't use emacs though so ...17/04 16:18
sah0sthanks again for all your help, see you17/04 16:24
Mathnerd314is there a statically-typed language where I can play with capability types?17/04 16:39
faxMathnerd314 - what are they?17/04 17:52
Mathnerd314capabilities - stuff where I can say that "you can do this" or "you cannot do this", reified into types17/04 17:53
faxdo you know any intro paper on it?17/04 17:57
faxsomething that describes important bits of it in a simple way17/04 17:57
Mathnerd314hmm... wait a bit17/04 17:59
faxhttp://www.cs.st-andrews.ac.uk/~eb/drafts/icfp09.pdf17/04 18:06
Mathnerd314ok; thought something like that could happen17/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.html18/04 06:21
fax"but you can add others (parametricity?) without spannering up the engines"18/04 21:06
faxso you can't derive parametricity internally?18/04 21:06
fax(I think it should be provable for a universe but was not sure about the general case)18/04 21:07
dolioI don't know of any type theory that can derive parametricity internally.18/04 21:07
dolioIn fact, I believe I recall Neel Krishnaswami referring to that as a sort of holy grail for impredicative type theories.18/04 21:09
faxit's just this desc throws me off a bit18/04 21:09
faxoh yes? :)18/04 21:09
dolioSince 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
dolioWhich you normally lose.18/04 21:10
faxah18/04 21:10
dolioThen again, one might wonder if that doesn't doom it to failure immediately.18/04 21:13
faxwell having a data type of all the syntax of the language (with an interpretation) would certainly prove false18/04 21:13
dolioBecause inductive types include strong sums, and strong sums in an impredicative universe yield inconsistency (as I recall from Luo).18/04 21:14
fax(which is why being able to make a data type of all data types was such a surprise to me)18/04 21:14
faxI'm not sure I understand that about the strong sums18/04 21:15
faxwhat about exists in coq? which is in prop18/04 21:16
dolioYes. They avoid the problem by not allowing strong elimination into Type or something.18/04 21:16
faxoh I see18/04 21:16
faxhm18/04 21:17
dolioThe idea is that if you have strong impredicative sums, then (exists p : Type. True) : Prop lets you have [Prop, _] : Prop.18/04 21:17
faxwhat about this http://coq.inria.fr/stdlib/Coq.Logic.Description.html ?18/04 21:18
dolioBut making use of that requires strong elimination fst [Prop, _] = Prop : Type.18/04 21:18
dolioCheck the elimination principles for it.18/04 21:19
dolioThe one that eliminates into Type is weak, I think.18/04 21:19
dolioAnyhow, I'm kind of taking Luo's word for this.18/04 21:20
dolioI 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
faxI'm sure it's true I just don't understand it18/04 21:20
pigworkerWhat 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
faxoh I see18/04 21:40
faxIt'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
faxpigworker - you write so well! I wish I could18/04 21:47
pigworkerfax: thanks, it's years of practice; I write to perform18/04 21:49
fax21:00 < hpaste>  parametricity -> induction (dolio)  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2493818/04 22:01
faxif the bot could tell the difference between haskell and agda we could get that in here18/04 22:01
faxdolio - I don't understand this P : ⊤ → Set18/04 22:03
faxwhy T rather than just P : Set?18/04 22:04
faxoh wait T means it's a functor18/04 22:04
dolioWhy P : Nat -> Set instead of P : Set?18/04 22:06
faxbut Nat is not initial and I think T is?18/04 22:06
faxi.e. T -> Set ~ Set18/04 22:07
dolioThe induction principle essentially expresses that if t : T, then t = id.18/04 22:07
dolioYou can derive that with P t := t = id, even.18/04 22:09
dolioinduction (\t -> t = id) refl : (t : T) -> t = id18/04 22:10
dolioHuh, EPTS with the 'proof irrelevant' rule lets you prove K.18/04 22:30
faxEPTS ?18/04 22:31
dolioErasure pure type system.18/04 22:31
faxoh18/04 22:32
dolio"The technical means by which realizability is internalized is called ultra Σ-types."18/04 23:29
faxwhat's that from?18/04 23:31
dolioNathan Mishra-Linger's thesis.18/04 23:31
dolioIrrelevance, Polymorphism and Erasure in Type Theory18/04 23:31
faxcool18/04 23:31
dolioUltra Σ-types are someone else, though. He's just describing them.18/04 23:32
Saizanthey sound scary18/04 23:32
dolioYou mean awesome?18/04 23:33
dolioThere are things out there called "very dependent types". They should have chozen a zazzier name.18/04 23:33
dolioLike mega dependent types.18/04 23:33
faxlol18/04 23:34
dolioOr quantum dependent types. Quantum is always good.18/04 23:35
dolioTake it before someone else does.18/04 23:35
--- Day changed Mon Apr 19 2010
Mathnerd314so what's the most powerful type system ever invented?19/04 01:04
ohnobinkifood!19/04 01:06
TheOnionKnightI'd pick an inconsistent one, after all you can prove any true proposition. (along with any false one but hey ...)19/04 01:06
Mathnerd314I'm thinking inconsistent type systems are weak, because they're equivalent to untyped systems19/04 01:07
Adamantyou probably need to define 'powerful'19/04 01:38
dolioWhat do you mean equivalent to untyped systems?19/04 01:52
faxI don't think it's an interesting question19/04 02:00
faxthere's always a more powerful system19/04 02:01
faxTo 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 analysis19/04 02:02
dolioSo, apparently, in the irrelevant EPTS, you can add axioms to the 'propositional' fragment of the language.19/04 02:15
dolioVia something like: axiom : Squash P ; axiom = poof.19/04 02:16
dolioP being the proposition you want to add.19/04 02:16
dolioSo, say, ext : Squash ((forall x. f x = g x) -> f = g).19/04 02:17
dolioWhich seems somewhat similar to OTT.19/04 02:17
dolioHuh, you can interpret computationally-irelevant pi as an intersection.19/04 03:45
faxyeah that's Coq* innit19/04 03:47
dolioCoq*?19/04 03:47
dolioI'm still looking at the thesis I was reading earlier.19/04 03:47
faxThe Implicit Calculus of Constructions19/04 03:48
dolioOh, yes.19/04 03:48
dolioIt makes sense, but I hadn't thought of it.19/04 03:49
dolioSince any term with type (x : A) => B[x] gets extracted from /\x. M to just a suitably erased M'.19/04 03:50
dolioSo M' must be a single term that inhabits all B[x], so to speak.19/04 03:51
dolioI need to figure out how to implement inductive types (families).19/04 03:53
glguyso... 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
glguyin the last 6 hrs or so19/04 05:54
dolioNone.19/04 05:54
glguyphew19/04 05:54
glguyI just had a sense of "oh shit, I'm so far behind... what am I /doing/ here??"19/04 05:54
glguyOK, what should I be reading if I do want to understand more of it?19/04 05:56
dolioThe stuff I was talking about was mostly a thesis that I mentioned at some point.19/04 05:59
dolioWhere'd I leave off? "None."?19/04 06:03
glguyat some pount.19/04 06:03
dolioOkay.19/04 06:03
dolioParametricity you can read about in the Wadler paper, Theorems for Free!19/04 06:04
dolioThere are also others. It goes back to Reynolds, but his papers might be harder.19/04 06:04
dolioOh, 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
dolioAnd if you don't know about pure type systems, you should read about those first.19/04 06:05
dolioThe thesis has a lot more stuff, though. Like, it considers languages with Agda-like inductive types.19/04 06:06
glguycool, thanks for that19/04 06:06
dolioAnd 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
dolioOh, and the epigram blog.19/04 06:08
dolioAnd 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
glguyno need, i have enough to keep me busy19/04 06:10
glguymost of what I know about Agda is from experimenting with things and seeing the results. reading more about the theory behind it will be good19/04 06:11
glguyone 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 regard19/04 06:12
dolioOh, 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
dolioThe 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 bottle19/04 06:14
dolioYeah, at least if you know something like Haskell, Agda is pretty easy to edge your way into.19/04 06:16
roconnoredwinb: is Idris a sound logical system?19/04 14:38
edwinbroconnor: No. At least not at the moment. It has Set:Set...19/04 14:43
edwinbSo I wouldn't recommend going and proving anything in it...19/04 14:44
roconnorI 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
roconnoror if Set:Set is really used in a mathematical Prelude (maybe it is used for generic programming or something).19/04 14:45
edwinbFor Idris it's really just me wanting to focus on other aspets of programming with dependent types and taking the easy way out19/04 14:46
edwinbaspects, rather19/04 14:46
edwinbit probably wouldn't be so hard to add a flag that did that19/04 14:47
roconnorwell, that's also the excuse that Epigram has as well19/04 14:47
roconnorand it is totally reasonable19/04 14:47
edwinbEpigram 2 will do it right in the end19/04 14:47
roconnorexcept 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
edwinbIndeed. I wouldn't recommend trying that...19/04 14:49
roconnorBut 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
roconnorFermat's Last Theorem probably doesn't need that many universes to prove it. ;)19/04 14:50
edwinbI would think of that flag as meaning, "Right, I've finished this program now."19/04 14:50
edwinbDuring development, it's useful to cheat!19/04 14:50
roconnoredwinb: do you use Set:Set for your generative programming19/04 14:52
edwinbI don't think I've ever used anything more than Set119/04 14:52
roconnorthat's what I figured19/04 14:52
roconnorer19/04 14:52
roconnoris Set1 the smalles set, or is there a Set0?19/04 14:52
edwinbthat would be assuming Set : Set119/04 14:53
roconnorah19/04 14:53
roconnorok19/04 14:53
roconnoranyhow19/04 14:53
roconnorthanks for the info19/04 14:54
pigworkerjust read logs...19/04 16:13
pigworkeruniverse polymorphism is currently in the spotlight for us19/04 16:15
edwinbI'm glad you're doing it so I don't have to...19/04 16:20
edwinbalthough I've been writing C most of today, so maybe you'd say the same thing19/04 16:21
pigworkervery probably19/04 16:27
pigworkerI wish I knew what Agda's actual universe rules were.19/04 16:30
glguyWhere can I go to see all of the {-# BUILTIN _ _ #-} things?19/04 18:17
* glguy dives into ./src/full/Agda/TypeChecking/Monad/Builtin.hs19/04 18:19
glguyThe BUILTINs for Cons and Nil make me think that there is some syntax for list literals19/04 18:21
glguybut I'm having trouble tracking it dow19/04 18:21
glguyn19/04 18:21
codolioI 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
codolioWhich is likely more efficient.19/04 18:24
glguyIsn't that where the COMPILED_DATA pragmas come in?19/04 18:25
codolioThat allows you to hack it in yourself if it doesn't have specific support.19/04 18:25
glguySo far I've traced the BUILTIN CONS and NIL to ./src/full/Agda/TypeChecking/Primitive.hs in the "toTerm" typeclass19/04 18:26
codolioBut, for instance, using the BUILTIN pragmas for naturals means that Haskell's Integer is actually used.19/04 18:26
glguyI don't see them going any further19/04 18:26
glguyI thought that the BUILTIN was how you got integer literals int he syntax19/04 18:26
glguylike how the buILTIN refl and eq where how you bound the rewrite syntax19/04 18:26
codolioIt does that, too.l19/04 18:26
codolioBuiltin stuff for equality is important for the trustMe thing, too, I think.19/04 18:27
glguyOK, I see that "ToTerm" is the typeclass "From Agda term to Haskell value"19/04 18:27
glguyOK, so list literals are  (a :: b :: c :: [])19/04 18:29
glguyjust making sure :)19/04 18:29
glguyIs the source code currently the best place to find out about those things?19/04 18:30
codolioWell, it's possible it's on the wiki somewhere, but I didn't know where to point you.19/04 18:33
glguySometimes it seems unfortunate that Agda 2 shares its name with Agda19/04 18:36
glguyIt is easy to find irrelevant, but promising hits on google19/04 18:36
faxI don't really know what's going on with agda19/04 18:37
faxI thought it was a research/exploration language19/04 18:37
faxbut everyone is treating it like it's not19/04 18:37
glguyindependent of its intended purpose, it is still an interesting language for those simply interested in learning more about dependent types19/04 18:40
ccasinUlf's thesis being titled "towards a practical programming language..."19/04 19:00
ccasinI tend to think of it is just that - a step on the way19/04 19:00
ccasinand pretty much the best one out there so far for doing experiments in19/04 19:01
ccasinso lots of academics do lots of cool things in it19/04 19:01
--- Day changed Tue Apr 20 2010
Saizanit seems like it'd be easier to work with PHOAS if you can use parametricity in your proofs20/04 05:45
gio123does somebody knows proof irrelevance?20/04 16:07
doliopigworker: I have a pretty simple type theory implementation that has what I understand to be (approximately) Agda's universe polymorphism.20/04 16:18
doliohttp://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs20/04 16:20
dolioThe type checker is there.20/04 16:20
pigworkerdolio: I'll have a look, thanks.20/04 16:20
dolioThe 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
pigworkerI'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
dolioYeah. 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
pigworkerMy suspicion is that nailing that could make things easier. We're having a crack at it.20/04 16:28
dolioLast I checked, something like that was the actual plan. Various lifting operators, plus inference of how much lifting you need.20/04 16:28
dolioRather than actual cumulativity rules in the type system like, say, Coq.20/04 16:29
pigworkergio123: I've been experimenting with proof irrelevance20/04 16:29
pigworkerI'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
npouillardlist20/04 16:33
npouillardoops20/04 16:33
dolioAnyhow, 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
faxthat desc thing is polymorphic though20/04 16:35
faxI mean20/04 16:35
faxit's of sort Set[i+1] with Set[i] in it? or maybe I am thinking too much about how coq does universese20/04 16:36
dolioWell, if I understand the situation, you have Desc : Set, and forall T : Set. exists d : Desc. Mu d = T.20/04 16:41
dolioExcept, perhaps, T = Desc.20/04 16:41
dolioOf course, there's probably no proof of that statement in the language, since that'd be type-case.20/04 16:42
dolioActually, that may still be too strong. Desc only describes inductive types (and IDesc inductive families).20/04 16:43
pigworkerAt the moment, the actual Epigram 2 implementation exploits the collapse, but we also have a stratified Agda model.20/04 16:46
pigworkerThe descriptions of level n inductive families are a level n+1 inductive family.20/04 16:47
dolioAh.20/04 16:47
pigworkerWhen 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
faxbut what about -> and forall?20/04 16:50
pigworkerfax: IDesc is closed under Pi20/04 16:50
dolioIs that new?20/04 16:51
pigworkerI 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
faxim confused :)20/04 16:53
faxwould you have say,  forall (A : *), A -> A : IDesc Zero  ?20/04 16:53
faxoh I guess it's just something along the lines of  pi \A -> pi \a -> var (fs fz)20/04 16:54
faxshould have written   forall (A : IDesc Zero), A -> A : IDesc Zero  perhaps20/04 16:55
faxno I am definitely confused20/04 16:55
pigworkerCurrently, 'Pi : (S : Set) -> (S -> IDesc I) -> IDesc I   and 'Const : Set -> IDesc I, so you can build that type a bit at a time.20/04 16:59
pigworker'Pi Set \ A -> 'Pi A \ a -> 'Const A20/04 16:59
pigworkerbut it's not really satisfying20/04 17:00
faxdoes this mean you can quote anything?20/04 17:01
pigworkerIDesc 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
faxeverything*20/04 17:01
pigworkerfax: 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
faxoh okay20/04 17:02
pigworkerthe former needs some sort of syntax with binding; the latter needs induction-recursion20/04 17:03
dolioAh! So that's how you do induction recursion.20/04 18:55
faxhm?20/04 19:02
doliopigworker said that inspecting the domain of a Pi requires induction recursion.20/04 19:03
dolioSo presumably that's at least part of how you do induction-recursion with something like Desc.20/04 19:03
faxthere's some noteson http://www.cs.chalmers.se/~peterd/papers/inductive.html20/04 19:05
faxI think this will be the same kind of thing20/04 19:05
dolioI guess it'd make sense that he'd be working on it.20/04 19:06
dolioSo many people's publications to read.20/04 19:06
stevani 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
doliodolio is often amused when authors refer to themselves by name in academic papers.21/04 01:46
fax:)21/04 01:47
* binki wishes people used /me properly :-p21/04 01:47
doliodolio wasn't broadcasting an action. He was speaking a sentence.21/04 01:47
binkiI forgot that /me doesn't work well with passive sentences21/04 01:48
dolioMy 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
dolioWhich I suppose is hard to avoid.21/04 01:49
faxin "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
faxthis is cool ^21/04 01:50
dolioAnd 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
faxI could find very little about induction-recursion21/04 01:51
faxthere'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 something21/04 01:51
dolioFrom 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
faxI 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 this21/04 01:54
faxhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.669521/04 01:58
faxhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.610121/04 02:00
faxsecond one is the one I really meant21/04 02:00
Adamantdolio: Bob Dole does not agree, Bob Dole21/04 03:42
lpjhjdhshould Data.Rational take a really long time at 100% cpu to load?21/04 19:38
dolioHave you loaded it before?21/04 19:40
dolioThe first time you load it, it compiles lots of other module with lots of proofs.21/04 19:40
lpjhjdhI haven't21/04 19:40
lpjhjdhah, thanks, many things it did compile :)21/04 19:45
dolioYeah, it has to check all the stuff for coprimality.21/04 19:49
dolioAnd the Euclidean algorithm.21/04 19:49
copumpkinit's really slow to use, too21/04 19:49
dolioSo, rewrite is really handy.21/04 19:49
copumpkinI remember I was testing basic arithmetic on rationals and it took tens of seconds to normalize simple expressions21/04 19:49
copumpkinI wonder what happened to the Rational improvements NAD mentioned21/04 19:49
faxit's frustrating21/04 19:50
fax...waiting for quotients21/04 19:50
* Saizan wonders if they work fine in Epigram 2 21/04 19:52
faxI think they do21/04 19:53
lpjhjdhhow do you get ÷?21/04 19:56
lpjhjdhI looked through the input.el but couldn't find it21/04 19:56
dolioPut that in the buffer, move the cursor over it, and type C-u C-x =21/04 19:57
lpjhjdhah, thanks21/04 19:57
glguyIs "abstract" as it pertains to modules documented somewhere? somewhere on the wiki or a paper, perhaps?21/04 22:58
dolioInduction-recursion is pretty wild.21/04 23:46
faxoh yeah ?21/04 23:48
dolioYes.21/04 23:49
faxI only really know what it is and some basic examples..21/04 23:49
dolioI think I have what is essentially an embedding of my little type theory with (agda-style) universe polymorphism.21/04 23:49
dolioAnd it fits entirely in Set.21/04 23:50
fax:o21/04 23:50
faxI don't get it :)21/04 23:50
faxhow is that possible21/04 23:50
dolioWhat you do, is have couple of universe formers.21/04 23:51
dolioFormU : (U : Set) (T : U -> Set) -> Set ; FormT : (U : Set) (T : U -> Set) -> FormU U T -> Set21/04 23:51
dolioWhich are defined via induction recursion.21/04 23:51
dolioSo, that lets you iterate the formation of universes.21/04 23:52
dolioYou can then have U : Nat -> Set and T : (n : Nat) -> U n -> Set.21/04 23:52
faxthose two are functions?21/04 23:52
dolioU and T are.21/04 23:53
dolioMutually defined.21/04 23:53
faxokay21/04 23:53
faxthye needn't be mutually defined though?21/04 23:53
faxor is it essential that they are21/04 23:53
dolioI think it is essential.21/04 23:53
faxthen I am not sure what is going on21/04 23:53
faxFormU is both a value and a type?21/04 23:54
dolioFormU is a datatype.21/04 23:54
faxoh is FormT a type as well?21/04 23:54
faxI was reading these as constructors21/04 23:54
dolioYes. FormU and FormT are types, defined via induction-recursion.21/04 23:55
faxok21/04 23:55
dolioThen U and T are defined via mutual recursion afterward.21/04 23:55
faxwow this is confusing :)))21/04 23:55
faxhow did you come up with this?21/04 23:55
dolioThen you define an inductive-recursive universe that internalizes the entire hierarchy.21/04 23:55
faxcan you interpret it? or is that not even needed21/04 23:56
dolioIt's just me fiddling with stuff I read in one of the Dybjer papers.21/04 23:56
faxI think I get it but that is pretty wild I agree21/04 23:57
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=24994#a2499421/04 23:58
dolioThere's a snapshot.21/04 23:58
--- Day changed Thu Apr 22 2010
faxbut how is that in Set??22/04 00:02
dolioI'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
faxhow do I do something like  forall T : *, T -> T  ?22/04 00:07
faxI tried T (π υ \ u -> π (τ u) \ x -> τ x) but that doesn't work22/04 00:08
dolioYour type is forall T : *, forall X : T, X22/04 00:11
dolioThe last bit should be \tau u.22/04 00:11
faxFF : T 1 (Π 1 υ \T -> Π 1 (τ T) \T -> τ T)22/04 00:11
faxthis seems closer but not it22/04 00:11
dolioThat's the same type. You're capturing the T.22/04 00:12
faxdoh22/04 00:13
faxokay yeah that works now thanks22/04 00:13
dolioAs for how this fits in Set, it's because induction-recursion is crazy.22/04 00:16
faxim really confused by this :p22/04 00:17
dolioEssentially, Luo defines all his universes in UTT via induction recursion.22/04 00:17
dolioAnd it's equivalent to ECC + inductive types.22/04 00:17
dolioAnd LF, the meta-theory, essentially only has Set.22/04 00:18
dolioSo, by accepting inductive-recursive definitions, Agda's Set is just as powerful (minus the impredicativity).22/04 00:18
faxe : Set22/04 00:19
faxe = T 1 (Π 1 υ \T -> Π 1 (τ T) \_ -> τ T)22/04 00:19
faxFF : e22/04 00:19
faxFF = \T t -> t22/04 00:19
faxthat works22/04 00:20
faxe : Set22/04 00:20
faxe = forall (T : Set) -> T -> T22/04 00:20
faxFF : e22/04 00:20
faxFF = \T t -> t22/04 00:20
faxthat breaks22/04 00:20
faxof course T in the first FF can't be anythingin Set, it can only be ℕ, ⊥ or ⊤22/04 00:21
faxbut those are still sets22/04 00:21
fax(oh maybe it can even be some pi, sigma, w, + thing if it wants)22/04 00:21
dolioThe second one breaks because e : Set1.22/04 00:22
faxthe first one should break too :S22/04 00:22
faxfor the same reason22/04 00:23
faxhow come this doesn't introduce inconsistencies?22/04 00:23
dolioThe first type is in the inductive-recursive universe analogous to Set1.22/04 00:23
dolioU 122/04 00:23
faxbut U 1 : Set!22/04 00:23
dolioYes.22/04 00:24
dolioSet contains an infinite hierarchy (and beyond) of nested universes within itself.22/04 00:24
dolioBut all of those universes are in Set. Set1 is not such a universe.22/04 00:24
faxI can't see why this works22/04 00:25
faxyou can have a code for any Set in there, so..... oh!22/04 00:25
faxyou can have a code for any set in there _except_ the one you are defining22/04 00:25
fax(U)22/04 00:26
faxer22/04 00:26
faxΞ U T22/04 00:26
faxnot U22/04 00:26
faxyou can only put a different Ξ inside it, I think I understand why this works now22/04 00:26
dolioU 0 : U 1 : U 2 : U 3 : U 4 : ... : Uinf : Set : Set 1 : Set 2 : ...22/04 00:26
dolioSomething like that.22/04 00:27
faxthat is so cool22/04 00:27
faxI wonder how this is proved to be acceptable22/04 00:27
faxthen again I can't even understand how basic dependent types normalization works22/04 00:28
faxso I don't think I have much hope of this22/04 00:28
dolioDybjer gives a pretty intuitive argument.22/04 00:29
dolioAlong 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
dolioSo it's still predicative.22/04 00:31
faxoh I meant induction recursion in general22/04 00:31
dolioRight. U and T could be any arbitrary inductive-recursive definition.22/04 00:32
dolioUniverses are just a go-to example.22/04 00:32
dolioI guess well-formed ordinals would be a simpler example.22/04 00:33
dolioTo build well-formed ordinals, you only need ordering on smaller ordinals than the one you're building to be defined, or something.22/04 00:34
fax*nod*22/04 00:35
faxbut how do we know there isn't some crazy inductive-recursive thing you can define which lets you prove false22/04 00:35
dolioI think Dybjer has set theoretic models and stuff, too.22/04 00:36
dolioIf you trust set theory.22/04 00:36
dolioSet theory + Mahlo cardinals, apparently.22/04 00:38
faxI 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
faxbut I am terrified of them :D22/04 00:40
glguyWhy is subtraction on the naturals written as "∸"? What is the significance of that operator?22/04 00:52
dolioI'm not sure. Maybe because zero - n = zero isn't what you'd expect from standard subtraction.22/04 00:53
dolio(Unless n = zero, of course)22/04 00:53
glguywe need a pastebin that actually runs agda --html on a given input and which has the standard library included22/04 00:54
dolioTotally.22/04 00:54
glguythere could be a flag for a set of imports and module heading if you just wanted a single definition to paste22/04 00:54
dolioIf only someone here had written a Haskell pastebin or something.22/04 00:55
glguyIs 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
glguyare there some {-# OPTIONS ... #-} that could be dangerous?22/04 00:56
dolioConceivably, actually.22/04 00:56
dolioI'm not sure how much --html runs, but there are pragmas to access arbitrary Haskell, which probably includes IO.22/04 00:56
glguyhmm22/04 00:57
dolioYou'll have to ask the mailing list for a definitive answer, though, I think.22/04 01:00
pigworkerBut if there's no haskell to link to inside the pastebin..?22/04 01:02
dolioOh, that's true. I guess you may not need ghc installed to run the agda executable.22/04 01:04
Saizaneven if you can FFI import arbitrary haskell functions i'd be surprised if they get evaluated during typechecking, and you'd also need unsafePerformIO22/04 01:07
dolioType checking in a dependently typed language requires normalizing arbitrary terms.22/04 01:07
dolioSo if you do import unsafePerformIO, you can make it happen during type checking.22/04 01:07
pigworkerIt's important to have some denotational model of dangerous things, though.22/04 01:09
lpjhjdhSo 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
edwinbdoesn't that depend how you do IO though?22/04 01:09
edwinbI'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
pigworkerYeah, no open-term FFI!22/04 01:10
edwinbI have a DSL for FFI too ;)22/04 01:10
edwinbnaturally22/04 01:11
dolioWell, 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
edwinbEven if you do, it can't reduce...22/04 01:12
Saizanit 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 further22/04 01:12
edwinbsince it needs the IO to actually happen before it can22/04 01:13
dolioOh, I see.22/04 01:13
edwinbIO is just a description of what will happen when you're in a position to do it22/04 01:13
dolioKind of like pigworker's "add fix to the language, but have it opaque during type checking" idea.22/04 01:14
pigworkeredwinb: possibly with a quotient, relating equivalent things you're not going to do just now22/04 01:15
edwinbmm22/04 01:15
edwinbAnyway, I was going to bed an hour ago. Better late than never.22/04 01:15
pigworkeredwinb: it'd be a bonnus if we could do it22/04 01:15
edwinbnight ;)22/04 01:15
pigworkerI once saw a lovely talk by Tarmo about monadic packaging of general recursion, but where are the slides?22/04 01:18
dolioI have them somewhere, I think.22/04 01:18
pigworkerthe inert fix idea is the monad (Reader (forall a. (a -> a) -> a))22/04 01:19
pigworkerbut there are more subtle monads which do a better job22/04 01:19
dolioAh, I hadn't thought of it like that.22/04 01:19
dolioMaybe I don't have the slides you're thinking of.22/04 01:19
pigworkerhere's a version http://www.ioc.ee/~tarmo/tday-veskisilla/uustalu-slides.pdf22/04 01:21
dolioAh, these aren't the ones I was thinking of.22/04 01:22
pigworkerI can't find them. I'm sure they included a function called unsafePerformVenanzio.22/04 01:22
dolioHeh, well, I definitely don't recall that.22/04 01:23
pigworkeror maybe that was just a joke in the room at the time22/04 01:23
pigworkerThe 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
dolioI rather worry about whether that sort of thing could ever be efficient.22/04 01:26
pigworkerAbstracting over a mythical fix just disables computation completely.22/04 01:26
pigworkerThe termination proof gets nuked at closed-term run time.22/04 01:27
dolioWrapping all your recursive calls and such in boxes doesn't seem like it'd be free.22/04 01:28
dolioNot to mention racing combinators and such.22/04 01:28
pigworkerOn open terms, it's not free.22/04 01:28
pigworkerNow, I always asked these guys for the API, and they always wanted to give me the model.22/04 01:29
pigworkerI don't really want to implement the monad that way, although I do want it to have a model.22/04 01:30
dolioYeah.22/04 01:31
dolioI 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
dolioAt least if you want to write normal corecursive functions in the language.22/04 01:32
pigworkerI'm not sure we should conflate total corecursion with general recursion, even if that's the model.22/04 01:32
pigworkerSuppose 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
Saizanwith an oracle for the recursive occurrences or "fix", would you be able to prove always-eventually properties?22/04 01:54
Saizani guess fix's type could give something to work with22/04 01:54
pigworkerIf 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
pigworkergoodness me, is that the time? I always eventually go to bed... g'night!22/04 02:09
Saizanheh22/04 02:10
dolioSuccess!22/04 02:22
dolioNope, failure.22/04 02:36
Saizanthe double polymorphic Pi?22/04 02:37
dolioYeah. I wrote it, but almost everything gets stuck.22/04 02:38
dolioBecause, say, if you want to use it with U n => U n, the output is U (n \lub n).22/04 02:39
dolioWhich is n, but Agda doesn't reduce it.22/04 02:39
dolioSo, like, an identity schema has a type in U (suc n \lub n \lub n).22/04 02:40
dolioWhich isn't ideal.22/04 02:40
dolioGoes to show you the kind of magic that Agda's universe polymorphism does behind the scenes, I guess.22/04 02:41
Saizanand you're not even required to prove l \lub l = l22/04 02:45
dolioWell, I mean, I could prove that here, but I'd have to go around sticking subst everywhere.22/04 02:46
dolioSo, what agda does is use it as an extensional reduction rule, essentially.22/04 02:47
Saizani'm talking about the \lub one gives to Agda for --universe-polymorphism22/04 02:47
dolioI guess it's not extensional if it's used as a reduction rule.22/04 02:48
dolioThat'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
dolioFor instance, Agda (although I guess they're trying to cut down on unnecessary eta expansion).22/04 02:52
Saizanmaybe they are used to Coq?22/04 02:55
Saizan(which doesn't do eta-expansion i think)22/04 02:55
faxcut down on eta expansion? :o22/04 03:08
faxlike a performance optimiasation that produces the same results?22/04 03:08
dolioYes. Eta is apparently part of why Agda uses so much memory.22/04 03:08
faxyeah Coq doesn't do any type directed conversion22/04 03:08
fax(which is too bad!)22/04 03:08
faxdolio wow that's kind of crazy I mean it makes things a little bigger.. but didnt realize it was such a problelm22/04 03:09
dolioI 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
faxI think eta covers the records too22/04 03:10
dolioYes.22/04 03:10
faxI mean that's the whole reason to define things as records as I understand it22/04 03:10
dolioI'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
dolioHmm, I don't think I can make Desc work right in my universes.23/04 04:38
faxyou are really pushing this it's cool23/04 04:51
faxwhat's the prbolem with Desc though, and di you try simpler ones like REG & SPT first?23/04 04:51
dolioThe 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
doliomu : Desc U T -> U ; T (mu d) = Mu d23/04 04:58
dolioAnd arg : (s : U) -> (T a -> Desc U T) -> Desc U T23/04 05:04
faxyou define it normally (in Agda), then just put codes for it in the Universe?23/04 05:06
faxor were building it into the universe?23/04 05:06
dolioWell, the problem with that is that a normal Desc in Agda (codes for Sets) needs to go in Set1.23/04 05:07
dolioWhich would put all my universes in Set1, at least.23/04 05:07
dolioAnd might cascade into not working again.23/04 05:08
dolioAnyhow, I'm not sure there's anything fundamentally different with that negativity than the negativity inherent in inductive-recursive definitions.23/04 05:09
dolioBut, because it's not directly part of the inductive-recursive definition, it fails.23/04 05:09
dolioMaybe I'm wrong, though.23/04 05:10
faxoh yeah I see what you mean about Set1 that's true... hmm23/04 05:11
dolioHmm, T doesn't termination check, either.23/04 05:37
danblickCould anyone recommend a place to read about formulating category theory in intuitionistic type theory?23/04 06:33
dolioAre you familiar with formulating stuff like algebra in it?23/04 06:38
danblickActually I only know the basics23/04 06:40
dolioWell, I'd recommend finding something on dependently typed records.23/04 06:42
doliohttp://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.9569&rep=rep1&type=pdf23/04 06:43
faxby the way23/04 06:43
dolioSomething like that.23/04 06:43
faxI am not sure anyone knows how to do algebra or category theory in dependent types yet23/04 06:43
dolioOnce 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
danblickdolio: thanks, I'll take a look at that23/04 06:44
dolioThere's also some category theory people working on founding it more constructively.23/04 06:45
dolioI 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
dolioWhich, via Curry-Howard, intuitionistic type theory is rather like higher-order logic with dependent sorts.23/04 06:47
dolioBut, I haven't gotten around to reading the thing yet, so I don't know much about it.23/04 06:47
dolioAgda needs to get sum indexed induction-recursion.23/04 08:38
dolioThat would make some of my stuff nicer.23/04 08:39
dolioHeh, apparently Agda 1 had some kind of indexed induction-recursion.23/04 08:42
glguygiven: bound n y x = x <′ y × y <′ n   ,   is it possible to prove  Acc (bound 10) 5    ?   (using Induction.WellFounded)23/04 19:24
glguythese Acc proofs are bending my brain...23/04 19:24
glguyPerhaps I'm trying to use the wrong < definition?23/04 19:25
dolioI've tried writing something like that before, and found it quite difficult.23/04 21:19
faxhuh I don't undesrtand that measure23/04 21:25
faxwhy is Acc (bound 10) 5 rather than Acc (bound 10)?23/04 21:25
glguyoh, I'd be happy with forall x. x < 10 -> Acc (bound 10) x23/04 21:26
glguyI was just starting with something more concrete :)23/04 21:26
faxno  I don't understand what you are doing23/04 21:26
faxI mean what about Acc (<)?23/04 21:27
glguythat only works for chains /down/ to 023/04 21:27
faxisn't that useable in the same way?23/04 21:27
faxoh!23/04 21:27
glguyI want chains /up to/ a bound, say 1023/04 21:27
faxwell maybe you could prove  Acc R -> Acc (R`on`f)23/04 21:28
faxand have f(n) = bound - n23/04 21:28
glguyI 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 small23/04 21:30
glguyI 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 something23/04 21:32
glguyand then have a function that took them up to a bound...23/04 21:32
dolioThat's pretty much why I was trying to do the proof, too.23/04 21:38
dolioNever finished, though.23/04 21:38
faxI think my way with the subtract seems pretty good23/04 21:39
--- Day changed Sat Apr 24 2010
faxdolio?24/04 00:21
faxwhat about defining category theory in this inductive-recursive way?24/04 00:21
faxdo 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 categories24/04 00:22
faxI should probably do an experiment24/04 00:22
doliofax: Universe polymorphism is the typical solution to that, but perhaps induction-recursion can also help.24/04 01:21
faxwell I had to make everything indices instead of fields to do it with polymorphism24/04 01:22
faxso it should be interesting to see if it can be done just as fields with ind-rec24/04 01:22
dolioI 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
dolioThe 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
dolioIn a sense.24/04 01:26
faxyes!24/04 01:28
faxthat sounds great!24/04 01:28
faxthe object language being the language of categories?24/04 01:28
dolioI was thinking more like the object language being a dependent type theory with universe polymorphism.24/04 01:29
faxbut we already have one24/04 01:29
faxthis wont work will it?24/04 01:29
dolioBut it's conceivable that you could do category theory directly.24/04 01:29
dolioI'd have to actually think about it. :)24/04 01:30
dolioI've kind of been wondering how much of set theory induction-recursion lets you formalize.24/04 01:37
dolioLike, impredicativity lets you formalize something close to ZF, as I recall.24/04 01:37
faxI don't actually know what set theory induction-recursion means24/04 01:41
faxI am not sure I've ever seen this24/04 01:41
dolioWell, I think the Dybjer papers give models of it in ZF + mahlo cardinal.24/04 01:42
dolioBut I don't actually know what a Mahlo cardinal is.24/04 01:42
faxAll 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
faxhttp://www.e-pig.org/epilogue/?p=49724/04 17:31
faxhttp://www.youtube.com/watch?v=IFACrIx5SZ024/04 17:33
Mathnerd314what? how do monkeys paddling canoes have to do with Epigram?24/04 19:02
AdamantMathnerd314: I'm not sure what spies would use .45mm 'questioners' either24/04 22:34
Adamantusually those tend to be in inches24/04 22:34
* Mathnerd314 checks to ensure date is not April 124/04 22:37
Mathnerd314yep...24/04 22:37
glguyIs there anything written up specifically comparing Epigram and Agda?24/04 22:56
shaprI'd also like to see such a thing.24/04 23:00
faxthe main difference is that agda is intuitionistic but epigram is based on observational type theory24/04 23:01
faxagda is still changing (a lot though), and of course epigram is changing faster24/04 23:02
faxthe main difference (from my point of view ..)24/04 23:02
Saizan_did you mean intensional rather than intuitionistic?24/04 23:02
faxyes that's what I shoul dhave said, thanks24/04 23:03
faxthey're both intuitionistic24/04 23:03
Saizan_also, Epigram seem to aim at making the user define its datatypes from within the theory, using an universe24/04 23:04
Saizan_currently the Mu and Nu fixpoints are external from the universe though24/04 23:05
dolioThere'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
dolioDesc {n} : Set {suc n}24/04 23:11
dolioDesc {n} is descriptions of datatypes over Set n24/04 23:11
dolioD : Desc {n} ==> Mu D : Set n24/04 23:12
faxone great thing in epigram is quotient types I think that will be really useful24/04 23:12
Saizan_dolio: there's a whole collection of those models, rather :)24/04 23:12
glguyI usually see extensional as the opposite to intensional, what is observational?24/04 23:13
faxglguy it's sort "best of both worlds" :D apparently24/04 23:13
dolioBut 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
faxthere's a couple papers on it but they're quite difficult to understand... I'm hoping they write more soon24/04 23:13
dolioYou'd probably only use Desc and the like for generic programming.24/04 23:13
faxglguy: you know how Coq just has beta conversion (and similar) but Agda has some stuff like eta-expansion, which are type directed24/04 23:14
faxglguy: Well I think OTT makes use of that type-directed stuff and pushes it even further24/04 23:14
dolioglguy: Both intensional and extensional type theories treat judgmental/definitional equality as linked with the equality datatype.24/04 23:15
dolioIntensional 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
dolioExtensional 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
dolioIn OTT, the equality type is no longer pegged to the judgmental equality. So you can prove that f == g : A -> B, but that doesn't mean that the typing rules will judge that P f = P g, for P : (A -> B) -> Type, or something.24/04 23:18
Saizan_though it's still substitutive24/04 23:18
dolioHowever, 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
faxI tried to implement OTT but got completely confused & stuck24/04 23:19
dolioSo 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
dolioLike (forall x. f x == g x) -> f == g for functions.24/04 23:21
dolioOr bisimulation for coinductive types.24/04 23:21
faxit's a shame that equality is not built in! but I will get over it24/04 23:22
faxI was so excited to learn about defining eq as a data type24/04 23:22
fax(when I started to learn about coq)24/04 23:22
faxwait I mean that it IS built in24/04 23:22
Saizan_that makes me wonder what kind of beast you get if you define a standard equality type in epigram, could you call it intensional equality? you could still use == to do "extensional" coercions24/04 23:25
dolio(And of course, equality for quotients is whatever equivalence relation by which they're quotiented.)24/04 23:25
dolioI have a paper here that has a type theory with multiple equalities...24/04 23:26
dolioIntensionality, Extensionality and Proof Irrelevance in Modal Type Theory24/04 23:27
faxPfenning?24/04 23:27
dolioYes.24/04 23:27
dolioIt's a lot like the erasure pure type systems.24/04 23:27
dolioIt has three different kinds of typing judgments.24/04 23:28
dolioM :: A, which is more intensional than usual (only alpha equivalence).24/04 23:28
dolioM : A which beta-eta24/04 23:28
dolioAnd M % A which is irrelevant.24/04 23:29
fax*nod*24/04 23:29
dolioAnd 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
dolioAnyhow, 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
faxI had fun inventing my own proof irrelevant type system but eventually realized it didn't have subject reduction24/04 23:31
dolioHeh.24/04 23:31
faxtook me a long time to notice!24/04 23:31
faxbut I was using modality too24/04 23:32
dolioThe 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
faxdolio, I'm still coming to terms with this induction-recursion stuff :P24/04 23:42
dolioI sent an overzealous message about it to the agda list.24/04 23:52
faxabout what ?24/04 23:53
faxwell I will just read it actualyl24/04 23:53
Saizanis there a good explanation of canonicity somewhere? particularly wrt proof irrelevance24/04 23:53
dolioI 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
dolioWhich isn't strictly positive, but it's defining a higher universe strictly by reference to lower universes.24/04 23:55
dolioAnd I thought one of the Dybjer papers was about that, but I was mistaken.24/04 23:55
dolioIt was just about defining indexed families via induction-recursion, which Agda already allows.24/04 23:55
faxhuh24/04 23:56
faxI didn't realize that Agda didn't have IIR24/04 23:56
dolioIt does have IIR.24/04 23:56
faxoh24/04 23:56
dolioI subsequently realized that my criterion was kind of ad-hoc, and not what IIR is.24/04 23:56
dolioIt requires restrictions on the indices that aren't normally enforced for inductive families.24/04 23:58
--- Day changed Sun Apr 25 2010
faxso in category theory they call ¡ gnab25/04 04:57
fax¡ : 0 --> B25/04 04:57
--- Day changed Mon Apr 26 2010
Saizan_is there a command to get the fully normalized form of a goal displayed?26/04 01:41
dolioC-c C-, does more normalization than is shown just by C-c C-l.26/04 01:41
dolioYou type the former while the cursor is inside the goal.26/04 01:42
dolioI think it gives the fully normalized type.26/04 01:43
Saizan_except i can't input C-, on a terminal, i'll look for the function it's bound to26/04 01:44
dolioYou can't?26/04 01:44
dolioHuh, I guess it just enters ,.26/04 01:45
dolioWeird.26/04 01:45
Saizan_yeah, i wonder if one could fix that by just chaning the terminal, though maybe there's no way to communicate "C-," to a textual emacs26/04 01:48
Saizan_agda2-goal-and-context btw26/04 01:51
stevanSaizan_: try: (global-set-key (kbd "C-c ,") 'agda2-goal-and-context)26/04 19:03
stevanworks for me in terminals, had the same problem...26/04 19:04
glguyIf 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
faxglguy: that's what I was talking about yesterday26/04 19:12
faxif R is well founded then R`on`f is too26/04 19:12
glguyyeah, but now I'm trying to figure out how to do it :)26/04 19:12
faxyou'd need to prove that first26/04 19:12
faxthere's a really cool paper all about this if you want26/04 19:13
glguyoh?26/04 19:13
faxhttp://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-57.pdf26/04 19:14
glguywow, I'm just barely older than that paper :)26/04 19:14
fax(the construction we've been talking about is inverse image)26/04 19:15
glguythanks, I'll give it a look26/04 19:15
glguyfax:   lem : {A B : Set} (f : A → B) (R : B → B → Set) (x : A) → WF.Acc R (f x) → WF.Acc (R on f) x26/04 19:25
glguylem f R x (WF.acc rs) = WF.acc (λ y x' → lem f R y (rs (f y) x'))26/04 19:25
glguysomething like this?26/04 19:25
faxwow that was fast26/04 19:25
faxglguy, since WF is a proof -- if that type checks it's correct :)26/04 19:26
faxAcc*26/04 19:26
glguyyeah, it type checks26/04 19:27
glguyI just have to figure out how to make use of it now :)26/04 19:27
faxit's a bit rubbish writing out recursion using WF26/04 19:28
faxthat's something which would be nice as a language feature26/04 19:28
glguyyeah... but I want to do it today :)26/04 19:28
faxlike in coq you write  Fixpoint f ... {measure foo} := ...26/04 19:28
faxbut there isn't really anywhere to write that in the agda syntax26/04 19:29
glguyI'm learning Isabelle and the current exercise was to do a function that required an explicit measure and termination proof using the Function package26/04 19:29
glguyin parallel I'm doing the exercises in Agda26/04 19:29
glguyand I refuse to not be able to write this in Agda :)26/04 19:29
faxthe way you are doing it sounds a little different from 'define the function and then prove it terminates'26/04 19:30
faxbecause the natural way to write, in agda.. is not that way26/04 19:30
glguywell, my goal is to be able to define the function in agda and not have the ugly red "you didn't terminate" indicator come up26/04 19:31
glguyI know that this won't be the prettiest implementation26/04 19:31
faxit might be interesting if the red gave you a proof obligation26/04 19:32
faxinstead of just saying _rewrite this_26/04 19:32
glguycertainly interesting26/04 19:32
glguyThat seemed to work26/04 19:34
glguyI got a proof that all the elements in my data type are accessible now26/04 19:34
glguyusing the measure I defined26/04 19:35
glguyand Nat's allAcc proof26/04 19:35
glguyit works :) now all I have to do is plumb through an accumulator parameter26/04 19:41
glguybut the recursion structure I needed is proven to terminate using wfrec26/04 19:41
glguythanks for the nudge, fax26/04 19:41
faxokay :)26/04 19:41
glguyhttp://www.galois.com/~emertens/treerec/treerec.html26/04 19:48
glguyThe preOrder function at the bottom isn't done yet but has the right recursion structure26/04 19:48
glguyOK, I've updated it to actually do the traversal26/04 19:53
glguy(if anyone is following along at home)26/04 19:53
faxglguy, is this function equal to:26/04 19:55
faxpre (leaf y :: xs) = [y] ++ pre xs26/04 19:55
faxpre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y026/04 19:55
fax?26/04 19:55
faxoops!26/04 19:55
fax++ pre xs  to both26/04 19:55
faxoh no I got it on the first, just add it to the second line26/04 19:56
faxpre (leaf y :: xs) = [y] ++ pre xs26/04 19:56
faxpre (node y y' y0 :: xs) = [y] ++ pre y' ++ pre y0 ++ pre xs26/04 19:56
faxpre [] = []26/04 19:56
glguyyup, looks about right26/04 19:56
glguyI wanted to write it using only tail calls26/04 19:56
faxah!26/04 19:56
glguythe exercise is to write it a few different ways26/04 19:57
stevanname your constructors and get nicer names from C-c C-c!? :-)26/04 19:57
glguyI'm cleaning up the names now :)26/04 19:57
stevanif 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 etc26/04 19:58
stevanno cleaning up needed :-)26/04 19:59
glguyYeah, I know about that, I'm just always hesitant to name parameters that I don't need to be named26/04 19:59
glguyI feel like I'm lying about using them for dependent types26/04 19:59
stevanhehe26/04 19:59
stevani name everything so i don't need to write out the arrows26/04 20:00
glguyI like typing \r and seeing the arrow appear :-D26/04 20:00
glguywhen I switch from Agda back to Haskell I often get a few \r's in my code26/04 20:00
faxglguy, but a -> b is just shorthand for (_ : a) -> b26/04 20:01
glguyI know that it doesn't change the meaning26/04 20:01
glguyOK OK, I've changed my constructor :-p26/04 20:02
stevanif 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
stevani hope nobody will drive us from the unicode paradise which Agda created for us26/04 20:04
faxactually I hate unicode26/04 20:09
stevan:-(26/04 20:09
faxI'm using LaTeX a lot recently, it's bloody awful but it's better than unicode26/04 20:09
faxit's actually got support for things like super and subscripts, radicals, typefaces (very important)26/04 20:10
faxbut the way we use it sucks, and it's very slow (as is texmacs) - so it's not suitable for a programming langage26/04 20:11
faxeditor26/04 20:11
stevansure, 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
faxoh I think so!26/04 20:16
faxI never used this but I've seen a screenshot26/04 20:17
faxI think latex kind of sucks though, at least it's possible to do better26/04 20:17
stevanyeah, some here; only seen a screenshot26/04 20:17
faxmaybe we can't NOT use latex because it's so pervasive26/04 20:17
faxthat means finding a good subset26/04 20:17
faxand specifying it formall26/04 20:17
faxformally26/04 20:17
faxas I see it, support like this would be a HUGE improvement in terms of readbility of programs26/04 20:18
fax(which is important)26/04 20:18
faxbut it would also mean a slight increase in complexity of editors26/04 20:18
fax(which is a **REALLY BAD THING**)26/04 20:18
faxbut I think it's unavoidable26/04 20:18
stevana 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 atleast26/04 20:19
faxthat 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 induction26/04 22:21
faxglguy, the first thing I'd do is prove the equations that define the program26/04 22:21
fax(they should all be provable by reflexivity)26/04 22:22
glguyfax, can you give an example of what the type of that might look like26/04 22:39
glguymy first attempt with something like:  lemma-leaf : ∀ a ts xs → preOrder′ (leaf a ∷ ts) xs ≡ preOrder′ ts (xs ++ [ a ])26/04 22:39
glguyis proving harder than I'd have expected26/04 22:39
glguy preOrder′ ts xs = wfRec PreOrderPred body (ts , xs)26/04 22:39
faxlemma-leaf _ _ _ = refl26/04 22:39
faxdoesn't work ?26/04 22:39
glguyno, due to the Acc proof being different26/04 22:40
faxwait huh26/04 22:40
glguyI'll paste the goal26/04 22:40
faxoh I see26/04 22:40
glguyhttp://fpaste.org/EN7d/26/04 22:41
faxwhat's preOrder′?26/04 22:41
glguypreOrder′ ts xs = wfRec PreOrderPred body (ts , xs)26/04 22:41
faxokay that's preOrder in the file I am looking at26/04 22:41
glguyroughly26/04 22:41
glguyit exposes the accumulator26/04 22:42
faxyou could try enabling proof irrelevance26/04 22:43
fax(there's a flag for it)26/04 22:43
fax(I've never tried this)26/04 22:43
glguybecause Acc has a single constructor?26/04 22:43
glguyI thought that proof irrelevance went away in 2.2626/04 22:43
glguy2.2.626/04 22:43
faxoh that's too bad26/04 22:44
faxim sure I proved the equations with refl26/04 22:44
faxwhen I used acc26/04 22:44
glguy.Induction.Nat._.helper26/04 22:45
glguywhere class considered harmful26/04 22:45
glguyclause*26/04 22:45
dolioglguy: Perhaps this isn't helpful, but you'd likely prove your theorem by well-founded induction as well.26/04 23:14
glguydolio, 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 way26/04 23:24
dolio:)26/04 23:24
dolioIt follows the general pattern that proving something about a function involves induction shaped like the recursion in the function.26/04 23:25
glguybut it was hard enough to write the function the first time :(26/04 23:25
glguyMy "Predicate" will certainly be more interesting this time as the type of the proof will change at each recursive call26/04 23:26
dolioYeah.26/04 23:26
glguynot some boring old \ _ -> List A26/04 23:26
--- Day changed Tue Apr 27 2010
glguyfax, through some form of magic... I was able to do my program as the three equations27/04 01:07
glguyusing refl27/04 01:07
glguyand one rewrite (which I had to use in my definition)27/04 01:07
faxcool! what magic!27/04 01:07
glguywell, I started with lifting the helper for Nat's allAcc out of the where clause27/04 01:09
glguyI don't know that that fixed it, but either I had a typo in my original attempt27/04 01:09
glguyor that fixed it27/04 01:09
faxglguy, do you still have the one that doesn't work? it'd be kind of interesting to look at that27/04 01:10
fax(though I will have to do it tommorow)27/04 01:10
faxand I just mean for my own curiosity..27/04 01:10
glguyI don't have it handy, but I'll experiment tonight to reproduce27/04 01:10
glguyhttp://www.galois.com/~emertens/treerec/treerec.html27/04 01:11
glguycheck out the three definitions at the bottom of the file27/04 01:11
faxwell I am not keen on +-assoc (treeSize t₁) (treeSize t₂) (sum (map treeSize ts))27/04 01:11
faxbut the other two are good :P27/04 01:11
glguyI wouldn't have done that if it worked without it :-p27/04 01:11
Saizan_i feel a bit lost when there's an heavy use of type synonyms27/04 01:26
glguydolio, still there?27/04 03:00
dolioYes.27/04 03:00
glguyhttp://www.galois.com/~emertens/treerec/treerec.html27/04 03:00
glguyoh, it is still uploading27/04 03:01
glguyrefresh that in a moment27/04 03:01
glguyI have the WfRec implementation with all of the equations regarding how it operates on its arguments27/04 03:01
glguyOK, done27/04 03:01
* glguy needs to show someone that understands what just happened27/04 03:01
glguywith all of the equ-* functions I should be able to prove equivalence to a simpler implementation now27/04 03:03
glguypulling the implementations of those functions out of the where clause allows the simplifier to do its work27/04 03:05
glguyotherwise they have unrelated arguments from their parent function27/04 03:05
glguyand it can't see the equivalence27/04 03:05
glguyanother case of where clauses considered harmful!27/04 03:06
Saizan_it seems like the translation of where clauses could benefit from some dependency analysis then27/04 03:09
dolioglguy: What are you asking me about this?27/04 03:11
dolioAlso, doesn't preorder traversal have a structurally recursive formulation?27/04 03:12
glguyI just wanted to show someone that I managed to get something proved about a function implemented using the WfRec library :)27/04 03:12
glguysure, I'm proving equivalence to that now27/04 03:12
dolioOkay.27/04 03:12
glguythe exercise was to do a tail-recursive version27/04 03:12
glguyand prove that27/04 03:12
glguy(in Isabelle)27/04 03:12
dolioAh, okay.27/04 03:12
glguyand I wanted to show that even if it took more keystrokes that it was doable in Agda27/04 03:13
dolioI think you might even be able to do a tail-recursive structurally decreasing version.27/04 03:13
glguyoh yeah?27/04 03:13
dolioHmmm...27/04 03:14
dolioI'll let you know in a while. :)27/04 03:15
dolioApparently not.27/04 03:24
dolioUnless the new --termination-depth=N flag will accept it.27/04 03:27
glguyWhat's that flag about?27/04 03:29
dolioIt tries to be smarter about seeing arguments that grow a little, but ultimately shrink.27/04 03:29
dolioN is related to how deep it looks for shrinkage or something.27/04 03:30
dolioWell, I seem to be unable to pull from the agda repository...27/04 03:31
dolio"Caveat: On Tree-like data, it does not work so well." That's probably bad news. :)27/04 03:33
glguyha27/04 03:33
dolioWell, hopefully my last checkout has --termination-depth.27/04 03:42
glguyOK, I did the equivalence proof, uploaded to the same URL27/04 03:43
dolioYes, 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
glguyDo you think that this is worth writing up as an example for using the WfRec stuff?27/04 03:46
glguyseems like there isn't much on Google for examples of using the library27/04 03:46
dolioSure. It's possible you're the first one using it.27/04 03:50
dolioI'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
dolioDid you ever figure out the getting-closer-to-an-upper-bound thing for fibonaccis?27/04 03:52
dolioIf not I might take another crack at it.27/04 03:53
glguyNo, but  I might now that I've had a little more success using the stuff27/04 03:53
glguyI would encourage you to take your crack27/04 03:53
glguy(as I don't have confidence that I'll knock it out)27/04 03:54
dolioWell, --termination-depth doesn't magically solve all problems.27/04 03:55
glguyDid it solve some?27/04 03:56
dolioNo.27/04 03:56
dolioIt didn't make my attempt pass, anyhow.27/04 03:57
dolioNot even the simplified version that didn't worry about values at internal nodes.27/04 03:57
glguyI need to figure out why this proof breaks when I remove the "abstract" section27/04 04:15
glguyso... 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) x27/04 06:10
glguysomething about "inverse image" from the paper I was referred to earlier27/04 06:11
glguy"Constructing Recursion Operators in Intuitionistic Type Theory"27/04 06:12
dolioWell, I think I broke my agda-share darcs repository.27/04 06:50
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25086#a2508627/04 06:52
dolioI succeeded in proving accessibility for k >= n > m, though.27/04 06:52
dolioSo, go forth and write fibonacci sequences.27/04 06:53
dolioI knew that keeping html files in the repository would turn out badly one day. Oh well.27/04 06:54
Saizanwell, we couldn't have seen it anyhow, c.h.o webserver is currently broken27/04 07:03
dolioI guess that explains why I couldn't pull the latest agda earlier.27/04 07:04
dolioBut, now I have to start over, I think.27/04 07:04
dolioBecause 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
dolioSo there are 45,000 changes to view.27/04 07:04
Saizandarcs record -a ?:)27/04 07:05
dolioWell, there are about 12 changes I don't want to record.27/04 07:05
dolioAnd when I skip those, it just hangs.27/04 07:05
dolioSo I suspect record -a won't be any better.27/04 07:05
dolioAnd remove html/* takes forever, too.27/04 07:05
glguythanks for that code, dolio27/04 07:12
glguyhttp://www.galois.com/~emertens/treerec/treerec2.html27/04 07:12
glguyis my latest revision (now with less code)27/04 07:12
glguyI  better save your code somewhere before hpaste's takusen backend forgets to unlock the database :)27/04 07:14
pigworkerhow do I find out which version of Agda I'm running?27/04 16:15
npouillardpigworker: you mean something else than agda --version27/04 16:16
ccasinif you installed it from cabal, your .cabal/packages folder might provide some hints27/04 16:17
Saizanif you only have the emacs mode switch to the *ghci* buffer27/04 16:17
Saizannear the top you'll see a like like:27/04 16:17
SaizanLoading package Agda-2.2.7 ... linking ... done.27/04 16:17
Saizan"ghc-pkg list Agda" will show the versions you have installed, btw27/04 16:18
pigworkerthe *ghci* window hint did it for me, thanks; I don't have the standalone27/04 16:18
pigworkerThanks guys, version mystery solved: it pays to install after a download...27/04 16:23
Saizanheh :)27/04 16:29
kosmikuspigworker: I installed epigram yesterday :)27/04 16:32
pigworkerkosmikus: it'll be different again today27/04 16:33
kosmikus:)27/04 16:35
faxhey um27/04 16:36
faxhttp://math.etsu.edu/LaTeXMathML/27/04 16:36
faxthis is kinda cool27/04 16:36
faxhttp://www1.chapman.edu/~jipsen/mathml/asciimathcalculator.html27/04 16:37
faxinfact thats more relevant27/04 16:37
faxI am wondering if something like this could make a good editor27/04 16:38
faxrather than ascii27/04 16:38
faxsince you get colors, super and subscripts, typefaces, ..27/04 16:38
fax(ascii + unicode)27/04 16:38
faxmaybe there's a plan already (for epigram ?)27/04 16:39
glguyfax, the problem was that the <-allAcc definition used a where-clause defined helper27/04 16:39
glguythe refl definitions worked once I lifted that27/04 16:39
faxglguy -- does that make sense27/04 16:39
glguyyeah27/04 16:39
faxit sounds like a bug to me27/04 16:39
faxwhy should a where clause be any different ?27/04 16:40
glguyin 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 function27/04 16:40
pigworkerfax: I'm getting out of the UI business27/04 16:40
* glguy heads in to work27/04 16:42
faxhttp://i.imgur.com/8p6JM.png -- anyone understand that THROW rule?27/04 17:17
faxI don't get why there isn't Gamma |-_T,Delta C27/04 17:17
fax(I'm guessing the C just comes from nowhre027/04 17:17
faxthis is from http://pauillac.inria.fr/~herbelin/publis/markov.pdf An intuitionistic logic that proves Markov's principle27/04 17:18
ccasinSuppose 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 itself27/04 18:08
ccasinthough I haven't looked at the paper, so I don't know if that's the most helpful way to read them27/04 18:08
ccasinAlso I have trouble seeing how it's useful27/04 18:11
faxso you prove T by proving T?27/04 18:11
ccasinsort of27/04 18:12
ccasinI mean, your context might have changed27/04 18:12
ccasinOK, I think I have an example27/04 18:15
ccasinSuppose you want to prove (A(x) -> B(x)) \/ C(x)27/04 18:15
ccasinstart with catch27/04 18:15
ccasinthen decide to prove the left side27/04 18:15
ccasinand assume A(x)27/04 18:15
ccasinnow, with throw, say forget about proving B(x), and prove the original formula instead27/04 18:16
ccasinonly this time, prove the right subbranch.  Now you get to prove C(x) with the extra assumption A(x)27/04 18:16
faxah!27/04 18:16
faxthat makes sense27/04 18:16
ccasinseems weird though!27/04 18:17
Saizanso you can prove excluded middle27/04 18:18
ccasinyes27/04 18:18
ccasinsuspicious27/04 18:19
ccasinah, but looking at the paper27/04 18:19
ccasinT isn't all terms27/04 18:19
ccasinthey can't have foralls27/04 18:19
ccasinso you can't prove \forall x . P(x) \/ not P(x)27/04 18:20
ccasinI think?27/04 18:21
SaizanV_I?27/04 18:22
ccasin?27/04 18:23
Saizanheh, sorry, i mean using the I rule for \forall at the start, and then the catch .. throw27/04 18:25
Saizanyou'd only have to catch P(x) \/ not P(x) with x free27/04 18:25
ccasinmy guess is the freshness condition will gum up the works27/04 18:26
ccasinbut let's see27/04 18:26
ccasinyeah, I think it does27/04 18:28
ccasinbecause, in order to get anywhere, you'll have to add P(x) do your context27/04 18:29
ccasinand then x isn't fresh enough to use that assumption after you throw back to LEM27/04 18:29
ccasinperhaps that's what you said, I'm just very slow :)27/04 18:29
Saizanah, no, i didn't think about x appearing in Gamma :)27/04 18:30
--- Day changed Wed Apr 28 2010
glguy_http://www.galois.com/~emertens/recops/recops.html28/04 09:26
glguy_I'm starting to implement the operators from the paper that fax told me about28/04 09:27
glguy_I wonder if some of these ways of constructing well-founded relations shouldn't be in the library28/04 09:27
roconnorwhat's the name of Agda's logic?28/04 20:03
dolioYou mean like CIC?28/04 20:05
dolioI'm not sure it has a name.28/04 20:05
roconnorlike CIC, or OTT28/04 20:09
roconnoror MLT28/04 20:09
roconnorMLTT28/04 20:09
dolioIt's sort of grown by accretion.28/04 20:10
dolioStarted with inductive families, induction recursion and a predicative hierarchy.28/04 20:11
roconnorit seems to be MLTT with universes and induction-recursion28/04 20:11
dolioAnd it's since gotten codata and universe polymorphism.28/04 20:11
ccasinulf's thesis describes it in terms of additions to UTT28/04 20:12
ccasinwhich seems a little odd, since agda lacks an impredicative Prop and its datatype eliminators are stronger than UTT's28/04 20:12
ccasinbut, so it is28/04 20:12
faxI don't think they're ready to specify it formally since agda is about exploring the design spacec no?28/04 20:16
glguyhttp://www.galois.com/~emertens/recops/recops.html28/04 21:09
glguynow with ways to construct well-founded relations from subrelations, inverse images, transitive closures and disjoint sums!28/04 21:09
copumpkinfancy :)28/04 21:12
copumpkinhave you tried epigram yet?28/04 21:12
glguynope28/04 21:13
glguyI wasn't sure which version of it I was supposed to try28/04 21:13
glguymaybe rather than bombarding you guys with whatever agda I did that day I should just twitter it...28/04 21:20
copumpkinI don't object to you doing both :P28/04 21:20
copumpkinI think I already follow you on twitter28/04 21:20
faxglguy, transitive closure is my favorite28/04 21:21
glguyThat one was the most fun to work out28/04 21:21
glguyI had to think about what I was doing rather than just following the types28/04 21:21
fax:D28/04 21:22
faxyou can define single step recursion and take the transitive closure to get structural recursion28/04 21:23
faxsingle step recursion is easy to prove from the eliminator of a type28/04 21:23
faxthis could form the basis of an implementation of pattern matching, but there is a different approach too (Below predicate)28/04 21:24
roconnorglguy: need more ordinal operations! :D28/04 21:29
roconnorglguy: like multiplication, exponentiation, Veblen functions!28/04 21:30
faxwould love to see programs that make (essential) use of these things too :)28/04 21:33
glguyI don't know what roconnor is talking about but I can find out :)28/04 21:34
roconnorglguy: you work for galois?28/04 21:34
glguyI have a program that makes use of the inverse image w.f. relation28/04 21:34
glguyroconnor, yeah, but we aren't all formal methods experts :)28/04 21:34
roconnorwho isn't?28/04 21:35
glguyI'm not!28/04 21:35
faxglguy, on the roads though ?28/04 21:35
roconnorbut you are writing agda code!28/04 21:35
glguyI'm approaching Agda from the "is it a dependently-typed programming language?" side28/04 21:36
glguyworking my way into "Is it a proof-assistant based on intuitionistic type theory?"28/04 21:36
roconnorsame thing :)28/04 21:36
glguy¯\(°_0)/¯28/04 21:36
faxhheheheehe28/04 21:37
glguyWorking at Galois is great for having access to a number of people who can explain stuff to me as I need it28/04 21:37
glguyI sit across from Iavor who fields most of my FM questions28/04 21:38
faxglguy you should write this stuff down :P28/04 21:38
glguyYeah, I considered "blogging" some of my experiences, but I don't really know what level to approach it from28/04 21:39
fax              don't really know what level to approach it from28/04 21:39
faxoops28/04 21:39
glguy"Here is a round-about way to implement that tail recursive function in Agda that you've never had trouble implementing in any other language" :-D28/04 21:40
faxlol28/04 21:40
faxglguy: http://muaddibspace.blogspot.com/2009/03/how-to-halve-number.html28/04 21:40
glguyAnonymous said...28/04 21:41
glguy    holy jesus wtf28/04 21:41
fax:)28/04 21:41
dolioHere'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
glguyI also don't know what it obvious to the rest of people using Agda28/04 21:42
glguyor if there is even an audience28/04 21:43
glguybeyond say the 32 people in this channel28/04 21:43
copumpkinwow28/04 21:44
copumpkinyou should use twitter more28/04 21:44
glguyoh yeah?28/04 21:44
glguyis Agda all over the Twitters?28/04 21:44
faxis twitter evil or not??28/04 21:44
faxI haven't been able to figure it out28/04 21:44
copumpkinglguy: not really :P28/04 21:45
copumpkinfax: it's as evil as the people you use28/04 21:45
copumpkinI mean28/04 21:45
copumpkinactually I don't know what I meant28/04 21:45
copumpkinthere are lots of haskellers and mathy people on it, if nothing else28/04 21:45
glguymaybe you meant that my twitter account is way out of date28/04 21:45
glguyhow do I publicly open a module in my module28/04 21:49
glguyso that opening my module gives you things defined in the other module?28/04 21:49
dolioopen ... public28/04 21:50
glguyI'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#259728/04 21:56
glguyspecifically "open InverseImage ..."28/04 21:56
faxwhat does galois do?28/04 21:57
faxactually the site will tell me28/04 21:57
glguyyeah, the site will tell you better than I can28/04 21:58
glguyI always stumble along as I figure out how much detail I'm allowed to go into28/04 21:58
faxman cryptol is so cool28/04 21:58
glguyfax, no argument here :)28/04 22:03
Adamantfax: Twitter is potentially less evil that a lot of other 'social' sites28/04 22:11
copumpkinomg more twitter love28/04 22:11
Adamantfor many common values of evil28/04 22:11
Adamantcopumpkin: no, I still hates it, mostly :P28/04 22:11
copumpkinoh28/04 22:11
copumpkinwell, more twitter less-that-100%-hate then28/04 22:11
Adamantcopumpkin: but yeah, the mathy/haskell/general nerd feeds can be fun28/04 22:11
Adamantand shitmydadsays is quality28/04 22:12
AdamantI've unplugged from several of the driving-data-into-your-skull-constantly deals and I think I might have to plug back in28/04 22:12
copumpkinlike what?28/04 22:13
glguySo what was that Velben function stuff?28/04 22:13
Adamantdunno, mostly just tech news if nothing else28/04 22:13
faxVeblen heirearchy28/04 22:13
Adamantto re-plug into28/04 22:13
faxI don't find tech very interesting but its nice seeing the quantum computing number of bits go up28/04 22:14
Adamantcopumpkin: I had a huge RSS reader feed.28/04 22:14
Adamantbut I burned out once I realized it would take about a hour a day to read everything as it came it28/04 22:14
Adamantmaybe more28/04 22:15
copumpkinhah28/04 22:15
AdamantI was going to switch to just reading it on the weekends28/04 22:15
Adamantbut then I just let it crash and burn28/04 22:15
AdamantI'm gonna restrict it to a limited number of high quality sites and try again.28/04 22:16
Adamantso. back on topic28/04 22:16
faxyes has anyone figured out what agda is yet? :D28/04 22:16
AdamantI'm behind on the 'learn at least one new language a year' resolution28/04 22:16
Adamantone thing I'm gonna learn is OpenCL28/04 22:16
AdamantI think Agda should be the other28/04 22:16
* fax doesn't beleive in learning programming languages28/04 22:16
copumpkinI don't think anyone knows yet28/04 22:17
Adamantsince 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
faxthere's a PhD on it28/04 22:19
faxthat's bookish28/04 22:19
copumpkinthe agda tutorial is pretty accessible28/04 22:19
Adamantyou mean a thesis28/04 22:19
faxI don't tend to say thesis since it doesn't imply it's a PhD28/04 22:19
glguycopumpkin: accessible with respect to which relation??28/04 22:21
faxlol28/04 22:21
copumpkin:P28/04 22:21
Adamantfax: a PhD on it sounds like a PhD is working on it, at least to me :P28/04 22:23
Adamantalso 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 :P28/04 22:23
Adamantbut thanks folks, I went to the Wiki and got some stuff to read.28/04 22:24
AdamantAgda wiki, not The Wiki28/04 22:24
--- Day changed Thu Apr 29 2010
glguygo figure... proving that a value is accessible under the w.f. relation of the lexicographic product of two w.f. relations requires lexicographic induction29/04 01:29
glguyhttp://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25192#a2519229/04 01:30
copumpkinsounds hardcore29/04 01:38
Saizanah, i thought that meant you had to use well founded recursion to prove the accessibility.29/04 01:41
glguy_Any ideas for ways to structure allAcc so that the lexicographic induction can be found to terminate?29/04 03:15
glguy_woot, I did the proof for non-dependently typed pairs29/04 03:46
glguy_http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#295529/04 03:54
dolioThat requires the constituent relations to be well founded for all elements of the type?29/04 03:58
glguy_I don't know that it requires it29/04 03:59
glguy_but I decided to try to prove it first assuming that they were29/04 03:59
dolioI'm pretty sure that's what allA and allB say.29/04 03:59
glguy_oh, it certainly is29/04 03:59
glguy_OK, rephrase:29/04 03:59
glguy_My proof requires that all inhabitants of the sets A and B are accessible wrt relations R1 and R2, respectively29/04 04:00
dolioHowever, since you only use it at the top of allAcc, you can probably dispense with it and just assume that each element of the pair is accessible.29/04 04:00
glguy_I don't think I understand29/04 04:03
dolioPerhaps it isn't possible to do away with the assumption that every element of B x is accessible.29/04 04:05
dolio(Or B, as it were.)29/04 04:05
glguy_yeah... I'd love to generalize this to B x29/04 04:06
glguy_(as you can see in the odule above)29/04 04:06
dolioSince for x < x', I can choose arbitrary y' > y, and (x' , y') \prec (x , y)...29/04 04:06
glguy_yeah, it is the same kind of arbitrary choice you have to deal with in the disjoint sum case29/04 04:07
dolioBut then one needs y' accessible for all the (x' , y'') < (x' , y').29/04 04:07
glguy_when you move from inj2 to inj129/04 04:07
dolioHowever, it shouldn't be required that all x : A are accessible.29/04 04:08
glguy_that is true29/04 04:08
glguy_so I could demand an Accessibility proof for your starting 'x' valu29/04 04:09
glguy_and use that to build the initial recursor-builder29/04 04:10
glguy_from the Some module29/04 04:10
dolioI'm not sure how much that would come up in practice.29/04 04:13
dolioBut theoretically you can have relations for which not every element of the type is accessible.29/04 04:13
glguy_you can always just define a subset of your type that is accessible29/04 04:13
dolioSomething like '1 < 2 < 3 < 4 < 5 < ... < 10 < 9 < 8 < 7 < 6'.29/04 04:15
dolioBut that's pretty contrived.29/04 04:15
glguy_well... you're still free to pick your own insane relation29/04 04:16
glguy_and you can define it to leave elements that you'd have left out of the set to live on their own islands29/04 04:17
glguy_where nothing was related to them29/04 04:17
glguy_suggestions for proving Lexicographic.allAcc terminates?29/04 04:20
glguy_I figured it out29/04 08:17
glguy_http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#223629/04 08:17
glguy_The lexicographic product of two well-founded relations is well-founded (and it is time on  Sigma A B rather than A x B)29/04 08:17
npouillardglguy_: great29/04 08:33
glguy_and along the way i got a generalized Induction.Lexicographic module29/04 08:33
glguy_maybe some of this could go into the std lib29/04 08:34
npouillardnow you can add universe polymorphism29/04 08:34
glguy_almost done29/04 08:34
npouillardglguy_: I hope so29/04 08:34
glguy_done29/04 08:34
glguy_uploaded29/04 08:34
glguy_(to the same link)29/04 08:34
npouillard:)29/04 08:34
glguy_I think that the last module could be a little more level polymorphic in that A and B could have different levels29/04 08:35
glguy_however the code that I reused from Induction.Lexicographic assumed they were both at the same level29/04 08:35
glguy_and I don't know if that was necessary or not29/04 08:35
glguy_but it is the state of things29/04 08:35
npouillardYou should propose a patch to the stdlib29/04 08:37
glguy_How do I do that29/04 08:37
npouillardwould it make sense to add the Data.Star operator29/04 08:38
glguy_can't happen29/04 08:38
glguy_reflexive relations are right out29/04 08:38
npouillardso obvious sorry29/04 08:38
glguy_I was thinking that it would, however, make sense to break the transitive closure operator out into a Data.Plus module29/04 08:39
glguy_rather than defining it locally here29/04 08:39
npouillardYep29/04 08:40
npouillardI think there is already a definition like you DisjointSum._<_29/04 08:40
npouillardyou*r*29/04 08:40
glguy_oh?29/04 08:41
glguy_just the operator, not the Acc proof?29/04 08:41
npouillardsure29/04 08:41
npouillarddon't panic29/04 08:41
npouillard:)29/04 08:41
glguy_it would be OK if this work was all already done29/04 08:41
glguy_I've had a blast working my way through it29/04 08:41
npouillardRelation.Binary.Sum29/04 08:42
glguy_I'd have to make it level polymorphic29/04 08:44
glguy_but good catch!29/04 08:44
npouillardglguy_: sure but would a nice first addition29/04 08:45
pigworkerDid you see the "Induction" section of the std lib? Is it a useful starting point? (I'm biased, of course.)29/04 08:45
glguy_I've tried to build off of the stuff in Induction where possible29/04 08:50
glguy_or use it via Induction.Lexicographic29/04 08:50
glguy_Reading through the Induction namespace, starting at that module, was quite valuable (especially the examples) for learning how to do this stuff29/04 08:51
glguy_(Does that mean you are the author of these modules?)29/04 08:52
fax14: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
Saizanhow would the type of that proof look like?29/04 15:35
npouillardSaizan: ⊥29/04 15:36
Saizanah, sorry, i was referring to another quote :D29/04 15:37
npouillard:)29/04 15:37
Saizan dolio : The best proof of the inconsistency of Agda would probably be a proof of the consistency of Agda in Agda. Someone should29/04 15:37
Saizan                   work on that.29/04 15:37
npouillardhum29/04 15:37
* npouillard guessing29/04 15:38
npouillard∀ (A : `Set`) → Dec (Σ `Term` λ p → ⊢ ⟦ p ⟧t ∷ ⟦ A ⟧s)29/04 15:41
npouillard`Set` would be the type of Set descriptions, same thing for `Term`29/04 15:42
npouillard⟦_⟧t and ⟦_⟧s interpret set and terms29/04 15:43
Saizanshouldn't the term be an argument as well?29/04 15:43
npouillardand ⊢_∷_ would be a typing-derivation type29/04 15:43
Saizanotherwise that decides if a type is inhabited or not, which seems quite strong29/04 15:44
npouillardI don't think so, it would be much weaker and only telling you that the type checking is decidable29/04 15:44
Saizanoh, i guess i get to prove that you can't give proofs of empty types with that29/04 15:45
npouillard"that": which one29/04 15:46
npouillard?29/04 15:46
Saizanyours29/04 15:46
npouillardyes29/04 15:46
npouillardmaybe we can just focus one this:29/04 15:47
npouillard¬ (∃ λ p → ⊢ ⟦ p ⟧t ∷ `⊥`)29/04 15:48
npouillardupdate of the previous one: ∀ (A : `Set`) → Dec (Σ `Term` λ p → ⊢ p ∷ A)29/04 15:48
Saizani see29/04 15:49
npouillardand so: ¬ (∃ λ p → ⊢ p ∷ `⊥`)29/04 15:49
dolioSaizan: 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
npouillarddolio: this would just say that agda is stronger the embedded theory, no ?29/04 15:52
dolioThe intention would that the embedded theory would be Agda.29/04 15:53
dolioSimilar to embedding Peano arithmetic in itself.29/04 15:53
dolioAnd 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
dolioUnless I'm misunderstanding something.29/04 15:54
npouillardI think we can't avoid reasoning about agda terms without proving something weaker than the consistency of Agda29/04 15:56
ccasinwhere is Agda's universe polymorphism documented?29/04 16:27
ccasinIn particular, I am mystefied by the following:  (\ l -> Set l) has type (l : Level) -> Set (suc l)29/04 16:28
ccasinbut Set itself does not29/04 16:28
ccasinSo, is Set a function on levels or isn't it?29/04 16:28
ccasin*mystified29/04 16:29
faxprobably the source code (if you can read it... it's pretty confusing)29/04 16:29
dolioccasin: Even with universe polymorphism enabled, the token Set refers to Set 0.29/04 16:39
dolioKind of an oddity.29/04 16:39
ccasindolio: yeah, it's a little odd, but I guess I figured that29/04 16:40
ccasinI just sent a message to the list on this topic29/04 16:40
dolioI should say, the token Set when not applied to another term refers ...29/04 16:40
dolioSo I guess it's kind of context-sensitive.29/04 16:40
ccasinAgda's approach to universe polymorphism seems to be pretty unique - it would be nice to see it explicitly written out somewhere29/04 16:40
ccasineven for a much smaller system29/04 16:40
dolioYes, it's unlike stuff I've seen elsewhere in the literature.29/04 16:41
ccasinwell, where "pretty unique" means "new to me" :)29/04 16:41
dolioI wrote a small interpreter for a language with similar universe polymorphism.29/04 16:41
ccasinthat's just what I'm doing :)29/04 16:41
dolioBut I don't think I documented it any more than Agda's is.29/04 16:42
ccasinI can't believe they pay me to sit around and write little interpreters29/04 16:42
ccasinbeing a grad student is swell29/04 16:42
doliohttp://code.haskell.org/~dolio/upts/Language/UPTS/TypeCheck.hs29/04 16:42
dolioYou might be able to glean the rules from that, though.29/04 16:42
dolioIt's pretty simple.29/04 16:42
ccasinthanks, I'll have a look29/04 16:43
dolioThe sigma types in there are a little more powerful than what you can do in Agda.29/04 16:43
ccasinthis is interesting29/04 16:44
ccasinit looks like, in your language "Type" doesn't have a type itself29/04 16:44
ccasinit must always be applied to a level29/04 16:44
dolioBecause you can't write something like "data Foo : Set \omega where foo : (l : Level) -> <something with type Set l> -> Foo".29/04 16:44
ccasinor maybe I'm reading the haskell wrong29/04 16:45
ccasinoh, and you add an omega level, that's nice29/04 16:45
dolioNo, that's correct. Just like fst and snd aren't first-class.29/04 16:45
ccasinI think agda doesn't have that, right?29/04 16:45
ccasincool29/04 16:46
dolioIt might be fundamental for Type, though. I haven't really thought about it.29/04 16:46
dolioType : (l : Level) -> Type (suc l) would be kind of weird, at least.29/04 16:47
ccasinthat's what I'm doing in my little interpreter29/04 16:47
ccasinof course, who knows if it's sound29/04 16:47
dolioI wouldn't necessarily worry about it being less sound. More getting into a type-checking loop.29/04 16:48
dolioYou can write \l -> Type[l] in my interpreter, for instance.29/04 16:48
ccasinreally 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 levels29/04 16:49
faxthat's cool29/04 16:49
ccasinso, ulf responded on the mailing list - looks like agda does the same thing as your interpreter29/04 16:50
dolioYeah.29/04 16:51
dolio-> isn't a first-class operator in Agda, either.29/04 16:51
dolioUnlike Haskell.29/04 16:51
faxit's odd that29/04 16:51
dolioAnyhow, 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
ccasindolio: what will lead to a looping type checker with the (l : Level) -> Type (suc l) choice?29/04 16:54
dolioccasin: 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
dolioI haven't thought a lot about it, though. It might be fine.29/04 16:55
ccasinhmm, why do I need to check the type of (l : Level) -> Type (suc l)?29/04 16:56
ccasinI think I just return that29/04 16:56
ccasinthat is, my system has as an axiom:29/04 16:56
ccasin----------------------------29/04 16:56
ccasinType : (l : Level) -> Type (suc l)29/04 16:56
dolioIt may well be fine.29/04 16:57
dolioIt's not like I've tried it and had loops.29/04 16:57
ccasinOK, cool29/04 16:57
faxType : (l : Level) -> Type (suc l) -- doesn't make sense to me29/04 16:58
faxwell okay I guess it's fine it looks weird29/04 16:58
ccasinwell, we seem to agree (Type l : Type (suc l))29/04 16:58
dolioOh, 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
dolioSo you can actually do case analysis on the level of your function in Agda.29/04 17:00
doliofoo : (l : Level) -> Set l ; foo zero = Nat ; foo (suc l) = Set l29/04 17:01
ccasinyeah, in my little interpreter I'm just building in Nats with the standard eliminator and using them for levels29/04 17:02
dolioWhich isn't exactly 'polymorphism' in the parametricity sense.29/04 17:02
ccasinright - it's not at all29/04 17:02
ccasinthis system seems to solve a lot of the same problems as the Harper-Pollack universe polymorphism stuff29/04 17:03
ccasinbut it's very different29/04 17:03
ccasinand cool!29/04 17:03
dolioHowever, 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
faxwasn't the Harper-Pollack thing about how to infer the levels?29/04 17:04
faxoh right, I think I know what the problems were29/04 17:04
* dolio goes to get some lunch.29/04 17:05
ccasinfax: 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 polymorphism29/04 17:05
ccasinit's just what coq has, I think29/04 17:05
faxokay29/04 17:05
ccasinin that paper, l := n | \alpha29/04 17:06
ccasinwhere \alpha means "I don't know, pick something"29/04 17:06
glguyfax: I finished the accessability proof for lexicographic product last night http://www.galois.com/~emertens/recops/Induction.WellFounded.Operators.html#229729/04 17:16
glguy(you told me about the paper, you get to hear about the progress)29/04 17:17
glguyHad to extend Induction.Lexicographic to do dependently-typed lexicographic induction29/04 17:18
faxeek29/04 17:18
faxI never dared to think about the dependently-typed ones29/04 17:18
glguyit was a pretty straight forward change, actually29/04 17:19
faxLexicographic exponentiation is a really cool one29/04 17:19
faxglguy, the main thing which is missing is examples -- but I think examples are really difficult to come up with29/04 17:19
glguyI'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 relations29/04 17:20
faxoh cool what was it for ?29/04 17:20
faxI 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=229/04 17:21
glguyI used it to write merge sort29/04 17:22
glguy(kind of the obvious one)29/04 17:22
faxhm29/04 17:22
faxthat sounds like something that would be done with a measure ?29/04 17:22
glguyYou could probably also have done measure of the sum of the lengths of the two lists29/04 17:23
glguybut it was pretty straight forward to do it lexicographically29/04 17:23
glguyhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=25208#a2520829/04 17:24
faxI can't imagine how :/29/04 17:24
* glguy ^W'd the wrong application29/04 17:24
glguyYay, the lexicographic and well-founded operators got added to the std lib darcs repo29/04 20:23
faxwow cool!29/04 20:27
faxthat is good did you cite that paper in yrou code29/04 20:28
fax?29/04 20:28
glguyWhat is Nils' nick29/04 20:28
glguyNo, but Nils did29/04 20:28
faxI don't think Nils' is here29/04 20:28
glguy"Yesterday I added some functions to Induction.WellFounded, following the29/04 20:28
glguydiscussion you and fax had"29/04 20:28
faxeek29/04 20:28
glguy<_<29/04 20:29
glguy>_>29/04 20:29
faxI should watch my mouth if people like Nils are reading29/04 20:29
glguyhe could be anywhere!29/04 20:29
faxI say too much stupid stuff :p29/04 20:29
glguynow I have to install ghc-6.1229/04 20:34
glguy(so I can install development Agda, so I can use the development library)29/04 20:35
dolioOh, that reminds me. c.h.o is back up, so I can pull agda.29/04 20:36
dolioOh, but nothing particularly interesting happened, apparently.29/04 20:36
faxno quotients yet/29/04 20:37
fax?29/04 20:37
glguySo what are quotients?29/04 20:37
dolioYou take a type, and identify various elements according to an equivalence relation to get a new type.29/04 20:37
glguyIs there a simple example?29/04 20:39
dolioZ = N x N / (\(l, r) (l', r') -> l + r' == r + l')29/04 20:39
dolioAssuming I got that right.29/04 20:40
glguyand the identified elements are included or excluded?29/04 20:40
dolioThe identified elements are indistinguishable from one another.29/04 20:40
dolio(1, 0) == (2, 1) : Z29/04 20:42
faxso proving that equation woud not be reflexivity29/04 20:42
faxit would be like quotientEqual (reflexivity)29/04 20:43
faxor so ...29/04 20:43
fax?29/04 20:43
dolioI don't know how you'd add quotients to something Agda-like.29/04 20:45
* glguy finds out that Data.Function -> Function29/04 20:46
dolioI need to figure out a better way to get the html for my Agda stuff on code.haskell.org.29/04 20:49
doliodarcs is too risky.29/04 20:49
glguyscp!29/04 20:49
dolioI guess I can do that.29/04 20:49
glguyThat's how I publish my html, at least29/04 20:49
dolioThat was less painful than I expected.29/04 20:54
--- Day changed Fri Apr 30 2010
glguyDo people bother trying to get their Agda source files to stay within 80 characters?30/04 20:48
glguyIf not is there a common standard?30/04 20:48
dolioI generally don't mind going a little beyond 80.30/04 20:52
dolioIt can be difficult to fit a lot of proofs in 80.30/04 20:53
dolioI probably keep it under 100 usually, though.30/04 20:54
glguyI like being able to print them out on letter paper30/04 20:56
glguyAgda’s colored HTML output looks great with a laser print on heavy paper30/04 20:57

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