--- Log opened Thu Jul 01 00:00:56 2010
--- Day changed Sat Jul 03 2010
dandelionshttp://www.reddit.com/r/reddit.com/comments/clmax/please_boycott_this_author/03/07 14:44
--- Day changed Mon Jul 05 2010
arcatani'm using agda-mode with emacs 23.2 on OS X, and the symbols are ridiculously small. do you any ideas how to make them bigger?05/07 21:04
--- Day changed Wed Jul 07 2010
pedagandthat's an embarrassing question, so don't laugh too loudly: does anybody have a universe for RelaxNG schema in Agda?07/07 15:04
pedagandusually, one starts such question with "I have a friend who would like to know...", but I'm (almost) shameless07/07 15:05
th5thats not a silly question!07/07 15:30
th5that's a great use for dependent types07/07 15:30
Saizan_no idea if it has anything like that, but someone posted a link to an agda web framework to the mailing list not so long ago07/07 15:31
pedagandwell, using xml those days, many people would say that it's a silly idea :-)07/07 15:35
pedagandSaizan_, ha indeed, thanks07/07 15:36
pedagandI cannot find such a universe, or equivalent, in the Lemmachine. It seems to be lower-level (http-level) than where I am.07/07 16:01
pedagandanyway, I'm (hopefully) almost done with mine. Pretty-printing now...07/07 16:02
pedagandth5, out of curiosity, do you use xml or similar with dependent types?07/07 16:46
pedagandI've been pondering about that for some time now, but I don't know what is the state of that field07/07 16:47
ccasinthe most exciting example of dependent types meets web programming I know if is Adam Chlipala's ur/web project07/07 17:01
ccasinwhich is a dependently typed programming language that generates provably valid html/AJAX stuff07/07 17:01
ccasin*know of07/07 17:02
ccasinI believe he had a pldi paper about it, also the implementation works and is fun to play with07/07 17:04
pedagandI'll hear about that on Friday or Saturday I think (DTP workshop in Edinburgh). That's indeed interesting07/07 17:04
ccasinah, I'm jealous - DTP sounds like fun07/07 17:05
ccasinoh my, just looking at the program, now I'm really jealous07/07 17:08
pedagand:-)07/07 17:09
pedagandI paid the "very late" fee to join it, because I was supposed to be working on a paper and wouldn't have been able to attend07/07 17:10
pedagandbut I suspect it's "value-for-money", as would a British MP put it07/07 17:10
ccasin:)07/07 17:11
ccasinunrelatedly, does there exist a gentle introduction to inductive types in dependently typed languages?07/07 17:12
ccasinI learned all I know from luo's book, but it's far from gentle07/07 17:12
ccasinconor's thesis is nice, though the syntax is a slog for non-experts07/07 17:13
pedagandmaybe, some paper by Paulin-Mohring07/07 17:14
pedagandnot that I've read much of it, but she has done a lot on that in Coq. Sadly, her thesis and "habilitation" are in French, tho.07/07 17:15
ccasinyes, a good thought, though07/07 17:15
edwinbI learned from Dybjer's paper "Inductive Families"07/07 17:15
edwinbI wouldn't call that gentle either, mind07/07 17:15
ccasinI've read her paper with pfenning, though it wasn't super helpful.  And I have had trouble finding an electronic copy of her paper with coquand, though that is what the coq reference manual refers to07/07 17:16
ccasinsomeone on our trellys list asked for an introduction07/07 17:16
edwinbthere's a bit in my thesis but I'm not sure it'll be much more helpful than Conor's07/07 17:18
ccasinedwinb: haven't read that one, thanks07/07 17:18
ccasinthe dybjer paper, I mean07/07 17:18
edwinbI suppose it depends what you mean by "gentle" and "introduction"07/07 17:19
edwinb(and indeed "inductive" and "types"...) ;)07/07 17:19
ccasin:)07/07 17:19
pedagandwhat are you looking for in such paper? theoretical foundations? category theory stuffs? induction principles? etc.07/07 17:19
pedagandfor instance, for a categorical characterization, you've plenty of "container" papers07/07 17:19
pedagandincluding Morris's thesis07/07 17:20
pedagandI suspect that it's where I learned about those things07/07 17:20
ccasinyes, I was thinking in particular of the basic stuff about how to check inductive definitions and generate and type their elimination principles07/07 17:20
ccasinthere are so many theses that do it, but I guess it's intricate enough that I'm silly to hope for a "gentle" one07/07 17:21
pedagandfrom a CT perspective, you might be interested in: http://personal.cis.strath.ac.uk/~patricia/csl2010.pdf07/07 17:21
ccasinI'll just link all the papers you've recommended :)07/07 17:21
pedagandif you're familiar with fibrations, that's "gentle" and "introductory"07/07 17:21
ccasinah yes, I liked this paper07/07 17:22
ccasinthanks for your help07/07 17:23
edwinbI see from blogland that things are happening with Trellys07/07 17:26
ccasinyes, it's fun07/07 17:27
ccasinthough there is still some disagreement about the purpose of the language07/07 17:27
ccasinor maybe I just disagree with what they've decided :)07/07 17:27
ccasinanyway, still under debate is the question of what sorts of induction principles trellys should be able to prove terminating07/07 17:28
ccasinI'm rooting for full dependent pattern matching and more, though I think I will lose07/07 17:29
edwinbI'd have thought that would at least partly depend on what the purpose of the language was...07/07 17:30
ccasinyes07/07 17:30
ccasinanyway, aaron's latest blog entry no doubt explains whatever the official stance is on that - maybe I should keep my mouth shut :)07/07 17:31
ccasinat any rate, in a development surprising to no one, proving normalization properties about these dependent type theories is very hard07/07 17:32
ccasinand since we're fiddling with recursion, we actually have to do it07/07 17:32
edwinbI never worried about that too much with Idris07/07 17:33
edwinbbut then, I'm not trying to make something, erm...07/07 17:33
* edwinb fails to find the word07/07 17:33
edwinbI'm just a hacker, is what I'm saying ;)07/07 17:33
ccasin:)07/07 17:35
ccasinan important goal for trellys is being able to prove that even though we allow general recursion, the things we certify as proofs really are07/07 17:37
ccasinand, more, you should be able to talk _about_ general recursive functions in proofs, just not run them07/07 17:40
ccasinwe have a story about how we decide which terms are good proofs, but predictably it's still in flux07/07 17:41
edwinbthat would be nice07/07 17:42
edwinbI've just decided all that can be investigated independently of using some tool to write interesting programs07/07 17:42
edwinbit does mean you need to take some care when claiming a proof is indeed a proof though07/07 17:43
--- Day changed Fri Jul 09 2010
* benc___ playing trying to implement something like bubblesort09/07 07:36
benc___I have this: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27195#a2719509/07 07:36
benc___it doesn't terminate according to the termination checker, but I think it does because n is decreasing?09/07 07:37
benc___so what am I missing?09/07 07:37
dolioonepass itself doesn't terminate?09/07 07:38
benc___tats the error i get09/07 07:39
benc___|Termination checking failed for the following functions: onepass.09/07 07:39
benc___is what agda tells me09/07 07:39
benc___if i compile this way: $ agda -c b.agda -i . -i lib-0.3/src --no-termination-check09/07 07:39
benc___then on my single example case, it behaves as I would expect it to.09/07 07:40
benc___$ agda --version09/07 07:40
benc___Agda version 2.2.609/07 07:40
dolioIf I use --termination-depth=2, it's accepted. So I suspect it doesn't like 'onepass (suc (suc n) ... = ... onepass (suc n)'.09/07 07:44
dolioIt sees that as growing, despite the fact that it's overall shrinking.09/07 07:45
nappingdoes --termination-depth=2 mean it unfolds the call on onepass (suc n)?09/07 07:47
benc___where is --termination-depth? mine doesn't have one?09/07 07:47
dolioOr not. I wrote some other stuff and it isn't a problem...09/07 07:48
dolioOh, I bet I know the problem.09/07 07:48
dolioWhen you use the 'with' it gets expanded into an auxiliary function, and that confuses the checker.09/07 07:48
dolioYes, the with is an important part.09/07 07:49
dolioSo, the with combined with the sort-of-growing recursive call is enough to confuse the checker.09/07 07:50
benc___any obvious rewrites to make it happy?09/07 07:52
benc___this is meant to be the inner loop of a bubble sort: go along a fixed length list, maybe swapping elements pairwise. so my termination is "eventually you'll reach the end of the list"09/07 07:55
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=27195#a2719809/07 07:55
benc___ok09/07 07:56
benc___i think thats how I would have implemented it in haskell ;)09/07 07:56
dolionapping: I'm not sure what exactly it does, but the idea is that it tracks the structural change through more function calls to see whether it decreases.09/07 07:58
dolioSo you can have arguments that get a little bigger before shrinking by more than was added to them, and it will still recognize that this is an overall decrease.09/07 08:00
benc___i had this idea that I was going to have it prove that onepass always moves the largest element to the end of the list, which I thought maybe I'd need some kind of ordering proof for each member09/07 08:00
* benc___ not really sure09/07 08:00
benc___and then ultimately use that to prove if you call onepass a bunch, the output list is ordered09/07 08:01
benc___weird to have that if_then_else_ that is not the same as the one in Data.Boolean09/07 08:11
benc___Data.Bool09/07 08:11
benc___shoudl I put an entry in the agda bug tracker about that with termination thing not working?09/07 08:36
jacobianhoky moly09/07 21:29
jacobianLots more people on here than last I checked09/07 21:29
ccasinall the cool kids code in agda09/07 21:30
jacobianapparently :)09/07 21:32
benmachinethe uncool kids lurk and watch the cool kids hoping to one day be as cool as them09/07 21:34
jacobianIs there a paper on how guardedness and recursion are calculated for agda?09/07 23:01
jacobianThe guardedness condition in agda appears to be much more fluid than in Coq09/07 23:01
jacobianIt's type-checking a lot more of my code.09/07 23:01
dolioI don't think there's a paper.09/07 23:10
dolioIt's something like: guarded by any number of constructors, one of which must be coinductive.09/07 23:16
* dolio has to go now, though.09/07 23:16
--- Day changed Sat Jul 10 2010
jacobianThe ability to reuse constructor names for different types is handy10/07 09:16
--- Day changed Sun Jul 11 2010
soupdragonhow would you define surreal numbers as an inductive-recursive type?11/07 01:34
jacobiandoes anyone have a good example of a chain of equation reasoning?  I'm having a hard time getting a handle on showing refl.11/07 09:58
jacobianIn the Agda tutorial I'm reading, the exercises are quite straight forward except for one having to do with tabulate and _!_.11/07 10:35
jacobianI'm having difficulty finding the solution.11/07 10:36
Saizanjacobian: you've to use induction for that one, iirc11/07 11:01
Saizani.e. write a recursive function11/07 11:02
jacobianyes, well I understood that much :)11/07 11:11
Saizani generally look for the argument(s) that the functions in my goal are strict in, so that if i pattern match on the corresponding variable the goal will reduce to something else11/07 11:15
jacobianright, I think I had missed that.  Here tabulate pattern matches on an implicit argument.11/07 11:19
benshello, I've been playing with Agda and I've gotten to a point where a function like (∀ {A : Set} (P : A → Set) (x y : A) → P x ≡ P y → x ≡ y) would let me prove what I want, is there a function in the stdlib somewhere like that?11/07 11:37
bensor even, does it make sense? :)11/07 11:38
Saizanwell, that's not true for every P11/07 11:40
Saizane.g. with "P _ = \top" you've P x == P y for every choice of x and y11/07 11:41
bensah, thanks, that example shows it very well11/07 11:41
Saizanif that was provable it'd mean that every predicate is injective, i think11/07 11:42
bensyeah.  Maybe I can prove it for the particular P I want then11/07 11:42
bensthank you Saizan11/07 11:43
Saizannp11/07 11:43
jacobianI'm trying to use lhs2TeX, but I'm getting an error: lhs2TeX: Enum.toEnum{Word8}: ...11/07 11:46
jacobianI assume that it's complaining about my use of utf8?11/07 11:46
jacobianI'm using lhs2TeX 1.1511/07 11:49
bensyay!  I proved it for the case I wanted and everything's good :)11/07 12:08
jacobianHmm, it appears to be annoyed with my use of unicode.  I wonder if there is some magic incantation I'm suppose to make to fix it.11/07 12:34
jacobianChanging the locale to C resulted in a different error :)11/07 13:06
--- Day changed Mon Jul 12 2010
jacobianAnyone use unicode fonts with lhs2TeX in agda?12/07 13:31
jacobians/fonts/characters/12/07 13:32
--- Day changed Tue Jul 13 2010
benc___is there an easy way to get HTML syntax colouring of agda code? (so that I can put stuff in blog posting that is coloured similar to how emacs does it?)13/07 11:37
* benc___ discovers --html option to agda runtime13/07 11:39
Laneyjacobian: There's a problem with lhs2TeX 1.15. Try 1.1413/07 11:46
Laney...or this patch: http://patch-tracker.debian.org/patch/series/dl/lhs2tex/1.15-3/no-utf8-string.patch which I think might fix it13/07 11:47
jacobianLaney: Thanks13/07 12:39
jacobianCan you have the @ char in your files when using lhs2TeX?  I'm getting an error for one of my tabular decls which appears to be caused by lhs2TeX.13/07 14:17
kosmikusjacobian: can you send me an example file demonstrating the lhs2TeX/unicode problem? I finally wanted to apply the patch, but it turns out I can't even reproduce the problem.13/07 14:51
kosmikusjacobian: regarding '@'. yes, @foo@ is inline-verbatim, similar to |foo| being inline-code.13/07 14:51
kosmikusjacobian: you can escape: @@ and ||13/07 14:51
jacobianah, thanks13/07 15:27
jacobianAs per a file that reproduces it, *any* use of unicode, including one that only uses \rightarrow in the file, will cause a crash on my system.13/07 15:27
jacobianI can definitely give you an example though13/07 15:28
jacobianIt's not actually a big deal for me since I can just use formatting directives in lhs2TeX to recover the same effect.13/07 15:29
jacobianhttp://coq.pastebin.com/c4NMxKp713/07 15:32
jacobianhttp://coq.pastebin.com/ihvAsZkn13/07 15:33
kosmikusjacobian: thanks very much.13/07 17:18
--- Day changed Wed Jul 14 2010
shaprAwright, how do I get started with Agda?14/07 05:59
dolioWhat do you mean? Installing stuff, or tutorials?14/07 06:00
shaprI'm using the ubuntu packages, what do I do after that?14/07 06:00
dolioHuh, there are ubuntu packages? I'd never even noticed.14/07 06:01
shaprOK, I can use the cabal package instead...14/07 06:01
dolioI guess it installed emacs and everything?14/07 06:01
shaprI dunno, I live in emasc.14/07 06:01
shaprI'm using ERC Version 5.3 with GNU Emacs (x86_64-pc-linux-gnu, GTK+ Version 2.18.0, multi-tty) of 2009-09-27.14/07 06:01
dolioWhen you open up a .agda file in emacs, does it have an Agda menu and such?14/07 06:02
shaprUm, pulling the agda mode out of the cabal package now...14/07 06:03
dolioThere seems to be an ubuntu package for agda-mode, too.14/07 06:03
shaprEh, I'll stick with cabal, I'm sure it's more recent.14/07 06:03
dolioAnyhow, once you get everything set up, I think this is a pretty good intro to the basics: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.TypesSummerSchool200714/07 06:05
shaprOk, where do I get a demo agda file?14/07 06:05
dolioClick on the lectures link, and start reading at Basics. Each file tells you what file to read next, I think.14/07 06:05
dolioAnd there are exercises.14/07 06:05
shaprspiffy!14/07 06:06
shaprHuh, looks like Haskell.14/07 06:06
dolioThe wiki probably has something on using the emacs mode, too...14/07 06:06
dolioThe main points you should be able to figure out from the menu I think, though.14/07 06:06
shaprHow do I type the <sub>1</sub> ?14/07 06:06
dolioYou can write 'foo = ?' and load the file, and the ? will turn into a hole for you to fill with an appropriately typed term.14/07 06:07
shaprooh, epigram style!14/07 06:07
dolioUnicode input starts by typing \14/07 06:07
dolio\_1 is subscript 1.14/07 06:07
shapraha14/07 06:07
dolioMost stuff can be typed by its latex name, although there are some abbreviations for stuff.14/07 06:08
dolio\bn instead of \bbb{N}14/07 06:08
shaprIs there any shortcut for the subnumber stuff?14/07 06:10
dolio\_N is all I know of.14/07 06:10
shaprok14/07 06:10
dolioOnce you've typed something there's a shortcut that will make emacs tell you all the ways to type it, though.14/07 06:11
dolioC-u C-x = I think?14/07 06:11
dolioThere's an alternate way of typing stuff that I don't use, too.14/07 06:11
dolioLike typing 'andd' automatically turns into a unicode conjunction symbol.14/07 06:12
doliohttp://wiki.portal.chalmers.se/agda/agda.php?n=Main.Documentation14/07 06:12
dolioSome of the stuff on that page will probably be useful.14/07 06:12
shaprCool14/07 06:13
shaprI'm transcribing the Basics still, I'll see where that gets me.14/07 06:13
shaprOoh, got my first type error. Was surprisingly friendly!14/07 06:15
dolioThat's good.14/07 06:18
dolioWait until you get something like "_87 != _93".14/07 06:18
shaprheh14/07 06:18
shaprI did get a bang and fish combo of some sort14/07 06:18
shaprSo, what exactly does id : { A : Set } mean?14/07 21:02
dolio{} in type signatures is for implicit arguments.14/07 21:05
shaproh14/07 21:05
dolioWhich means you don't have to write them in when you're using the function.14/07 21:05
shaprum, ok14/07 21:06
dolioSo id :: {A : Set} -> A -> A can be used like "id x" instead of "id A x".14/07 21:06
dolioAnd Agda will try to figure out what the A argument should be.14/07 21:06
dolioWhich should be pretty easy in this case, because it's whatever the type of x is.14/07 21:06
dolioYou can specify implicit arguments manually, though "id {A} x".14/07 21:07
shaprShould the last example in Basics.agda typecheck?14/07 21:07
dolioid6?14/07 21:08
shapryup14/07 21:08
dolioYes, I think so.14/07 21:08
dolioOh yes, and if there's an explicit argument that you want agda to infer, you can write _.14/07 21:09
shaprAha, \<space> is not the same as _14/07 21:10
ccasinyes, it is easy to make mistakes like that14/07 21:12
ccasinalso note that \:: is not the same as :: (useful for lists - \:: is often cons)14/07 21:12
ccasinand \: is not the same as :  (since : is reserved, people often use \: when doing PL stuff)14/07 21:12
shaprI'm using gnumacs, is there some way to make the differences explicit?14/07 21:14
ccasinnot to my knowledge, but they do look a little different14/07 21:15
ccasinit's just easy to get caught off-guard at first14/07 21:15
dolio\: is more grey than : in my font, as I recall.14/07 21:15
shaprunderscores in type signatures represent operators?14/07 21:16
shaprI'm looking at Datatypes.agda14/07 21:16
shaprspecifically _+_14/07 21:16
ccasinyes14/07 21:16
dolioYes. Underscores go where arguments would go.14/07 21:16
ccasinthat makes + infix14/07 21:16
shaprAh, interesting%14/07 21:16
dolioSo, if_then_else_14/07 21:16
shaprmultiples allowed? _%__ ?14/07 21:17
dolioI don't think so.14/07 21:17
ccasinthough, in that case you don't need them14/07 21:17
ccasinsince foo_ is just foo14/07 21:17
ccasinI mean, if foo is a function14/07 21:17
dolioWell, foo_ is useful when you don't want foo to bind as tightly as a function.14/07 21:18
shaprAh, ops don't bind as tightly as functions?14/07 21:18
ccasinthey can be adjusted14/07 21:18
ccasinI think the syntax is something like14/07 21:19
dolioWell, they never bind as tightly as functions.14/07 21:19
ccasininfixl 6 _+_14/07 21:19
dolioFunction application has maximum precedence, like Haskell.14/07 21:19
ccasinah14/07 21:20
shaprSo, why does "if false then x else y = y" work in Bool.agda, but won't typecheck in Datatypes.agda?14/07 21:35
shaprOh wait, now it does work%14/07 21:35
* shapr is confused14/07 21:36
shaprHow do I get the upside down v from CurryHoward.agda?14/07 22:53
shaprIs it just a caret?14/07 22:54
shaprdoesn't look like it't just a caret14/07 22:54
ccasinI don't know, but:14/07 22:54
ccasinput your cursor over it and enter14/07 22:54
ccasinC-u C-x =14/07 22:54
ccasinand it will tell you what \ shortcuts work14/07 22:54
ccasinthis is a good combination to remember, I think it's on the wiki on the "unicode input" page14/07 22:55
shapr\wedge or \intersection or \and14/07 22:55
shaprhmm14/07 22:56
shaprnifty14/07 22:56
shaprI'm getting a Parse Error from \all in CurryHoward.agda14/07 23:04
shaprI tried copying and pasting from the online version, same error.14/07 23:05
shaprAny ideas?14/07 23:05
shaprI also can't get notNotEM to type check, it gets upset about "\p -> f (inl p)" not being a function type, but instead being P14/07 23:13
* shapr is lost14/07 23:13
--- Day changed Thu Jul 15 2010
ccasinshapr: where do I get a copy of CurryHoward.agda?15/07 00:14
ccasin\forall is a reserved character in agda, so it's not terribly surprising that it might cause parse errors15/07 00:14
ccasinoh, he left15/07 00:15
Saizandoes Agda use normalization by evaluation? and anyhow, is the interpretation of a function shared between its uses?15/07 15:13
ccasinSaizan: I don't think it does15/07 17:48
ccasinin ulf's thesis, he gives a direct operational semantics15/07 17:48
ccasinI'm not a NBE expert, though15/07 17:51
dolioThe stuff in src/core looks like NBE.15/07 18:53
ccasindolio: which parts?15/07 19:00
dolioExp and Val15/07 19:02
dolioThat's probably the wrong stuff, though.15/07 19:05
ccasinwell, I know hardly anything about nbe, but can you explain?  This looks like a straightforward implementation of a boring big step operational semantics to me15/07 19:05
dolioIts only constructor for universes is "ESet" or "Set" respectively.15/07 19:05
ccasinyes, this is definitely not what is running under the hood in agda, but I'm still curious15/07 19:06
dolioNormalization-by-evaluation is where you have essentially two syntaxes. One is syntax trees of un-normalized terms, and the other is a syntax that admits, ideally, only normal forms, although that's not necessary.15/07 19:07
ccasinis that right?  I mean, I do this all the time - it's convenient to use the type system to check the difference between exps and values15/07 19:08
ccasinI thought nbe described a strategy where you interpret the exps into some some other (maybe set theoretic) domain and then read back out values15/07 19:08
dolioYou could call them Syn and Sem, the idea being that Syn is syntactic terms, and Sem is semantic terms which are kept in normal form, and don't represent things like '(\x -> x) e'. Instead you have a functin 'apply : Sem -> Sem -> Sem' which computes the normal form of applying one semantic term to another.15/07 19:09
dolioThen you write 'eval : Syn -> Sem' and 'reflect : Sem -> Syn'.15/07 19:09
dolioAnd 'normalize : Syn -> Syn ; normalize = reflect . eval'.15/07 19:09
dolioWell, I suppose you could use other sets for your semantics, too.15/07 19:13
dolioThe two term representations won't necessarily look alike.15/07 19:14
dolioFor instance, for a combinator calculus, you might have:15/07 19:14
doliodata Syn = S | K | _$_15/07 19:14
doliodata Sem = K0 | K1 Sem | S0 | S1 Sem | S2 Sem Sem15/07 19:15
ccasininteresting15/07 19:16
ccasinI have seen this technique, but never thought of it as nbe15/07 19:17
ccasinthe src/core stuff seems to be missing the "reflect" part of this, though15/07 19:19
dolioYeah.15/07 19:19
dolioI'm not sure what that stuff is.15/07 19:20
danbhello15/07 23:06
danbtrying and failing to the build the standard library15/07 23:07
danbusing agda-2.2.6 and the latest darcs for the standard library, i get an error in Data.List: "Not implemented: pattern matching for records"15/07 23:07
dolioYou'll need an agda newer than what you've got.15/07 23:08
danbusing agda-2.2.7 it appears to diverge and eat memory after compiling Relation.Binary.HeterogeneousEquality15/07 23:09
danband the release-notes for the library seem to say i should use 2.2.6...15/07 23:09
danbwith 2.2.7, i let it run for >10 mins and it paged out the rest of my apps :/15/07 23:10
danb(and by 2.2.7 i mean the latest darcs for agda)15/07 23:10
dolioHeh.15/07 23:10
danbany ideas?15/07 23:10
dolioI wouldn't have expected that for just HeterogeneousEquality.15/07 23:10
dolioMaybe there's a way you can get a back-dated version of the library that will work with 2.2.615/07 23:11
doliohttp://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary15/07 23:11
danboh, i see, duh. version 0.3 is different from darcs head15/07 23:12
danbthat what the release-notes reported to work with 2.2.615/07 23:13
danbok, i'll try that15/07 23:13
--- Day changed Fri Jul 16 2010
danbif i have a mixfix operator `data _∈Val : {t : type} → Term t → Set`, how can i call it with an explicit t argument?16/07 18:38
Saizandanb: e.g. "_∈Val {t} tm"16/07 18:39
danbM ∈Val works fine, of course, but where do i put {t}? {t} M ∈Val and M {t} ∈Val and M ∈Val {t} all seem to not work (or i'm just doing something else wrong at the same time somewhere)16/07 18:39
danbSaizan: oh, yeah, ok. should have thought of that. is there any way to combine {t} and M ∈Val ?16/07 18:40
Saizannot that i know of16/07 18:40
danbok16/07 18:40
danbthx16/07 18:40
Saizannp :)16/07 18:40
TheOnionKnightProbably not much help but (v ∈) {t} tm would also work.16/07 18:56
--- Day changed Wed Jul 21 2010
Eduard_MunteanuHi.21/07 01:23
--- Log closed Wed Jul 21 14:28:16 2010
--- Log opened Wed Jul 21 14:52:22 2010
-!- Irssi: #agda: Total of 28 nicks [0 ops, 0 halfops, 0 voices, 28 normal]21/07 14:52
-!- Irssi: Join to #agda was synced in 67 secs21/07 14:53
* Saizan might be able to typecheck Everything.agda with his new shiny 1GB of ram21/07 18:06
dolioI doubt it.21/07 18:07
dolioUnless that's 1GB + a bunch else you already had.21/07 18:07
Saizanfor a total of 3GB21/07 18:07
dolioOh, well, I can't say for sure, then.21/07 18:07
dolioI still doubt it, though.21/07 18:09
Saizanheap overflow, in fact21/07 18:29
* Saizan iterates21/07 18:30
Saizanyay, it completed in two runs21/07 18:34
--- Day changed Thu Jul 22 2010
benc___i'm trying to prove if n <= m, n != m that n < m22/07 10:20
benc___http://pastebin.com/BH5zrXne22/07 10:20
benc___like that22/07 10:20
benc___but I'm stuck there22/07 10:20
benc___i have a case that is a contradiction, but how do I make agda see the contradiction?22/07 10:20
pigworkerdoes neq refl give you a proof of something uninhabited?22/07 10:23
pigworker⊥-elim might help (from Data.Empty), if you can figure out how to type it in22/07 10:26
benc___yeah22/07 10:33
benc___reload that URL to see how i just used it22/07 10:33
benc___elim (neq (refl))22/07 10:34
benc___oh wait pastebin doesn't work that way. anyway   bot-elim neq refl worked just fine22/07 10:35
pigworkergood; saves mucking about with helper functions and () patterns22/07 10:37
benc___onwards with my epic proving-bubblesort voyage22/07 10:39
rubihola22/07 22:21
Saizanhi22/07 22:21
jdanbrownhello22/07 23:26
jdanbrowni have an ADT with eight constructors, and i want to use Decidable equality for it22/07 23:27
jdanbrowncurrently i've written a 64-clause _≟_ function...22/07 23:27
jdanbrownis there a better solution?22/07 23:27
dolioProbably not, unfortunately.22/07 23:29
jdanbrown:(22/07 23:29
jdanbrownit's a pretty ridiculous function22/07 23:29
dolioYes.22/07 23:29
dolioI don't think there's any way to do a "the rest of these should be absurd" thing, though.22/07 23:30
Saizanit'd be really great if overlapping patterns could be smarter22/07 23:31
jdanbrowndolio: i was hoping for compiler support, like "deriving Eq" in haskell22/07 23:37
jdanbrownbut smarter patterns would help the problem a lot, as well22/07 23:38
pigworkertime something generic happened; how are Agda's strings these days?22/07 23:41
benmachinemaybe someone should invent template agda? :P22/07 23:42
pigworkerit's called Agda22/07 23:42
* benmachine is quiet again22/07 23:43
jdanbrownanother question regarding ADT's and PropEq: in constructing the proofs of ¬p for the 'no' constructor of Dec, i have to write a bunch of logically silly functions that strip off one constructor: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27968#a2796822/07 23:45
Saizanpigworker: strings?22/07 23:46
jdanbrown(look for the postulates)22/07 23:46
jdanbrownis there a better way to do that?22/07 23:46
pigworkerSeriously, if we can't program our way out of this wet paper bag, we're doing it wrong. That's not to say there's an off-the-peg solution just yet. Part of the point of being Agda is to be reflective enough not to need template machinery.22/07 23:47
pigworkerSaizan: Can we compute a de Bruijn index in Fin n from a string and a Vec n of strings?22/07 23:47
Saizanjdanbrown: a more agdy way, i think, would be to write the whole ¬p proof as a function in the where, so that you can pattern match on the equality proof it gives, and then you should be able to call "C≢D refl"22/07 23:49
Saizanpigworker: i'd think so, Data.String.String has decidable equality22/07 23:51
Saizanthe current quote/quoteGoal won't help in giving us a description of an ADT though, right?22/07 23:51
jdanbrownSaizan: ok, let me try that and see...22/07 23:52
pigworkerdon't think so, but it might be possible to construct a modelled type we can cope with22/07 23:53
Saizanbtw, i'm a bit puzzled by quoteGoal giving you just the term and not the whole closure22/07 23:55
--- Day changed Fri Jul 23 2010
Saizanfor decidable equality a putative Desc would have to provide the decision procedure for the abstract types it mentions23/07 00:14
pigworkeryes, it would say "if the pieces are decidable, the whole is decidable"23/07 00:15
Saizanis there anything like this in the epigram repo?:)23/07 00:19
jdanbrownSaizan: having trouble with that. tried your suggestion at the bottom of http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27968#a27968 but agda complains when i try to pattern match on 'refl'23/07 00:19
jdanbrownSaizan: (added the type error at the bottom of the hpaste—reload if necessary)23/07 00:20
pigworkerSaizan: decidable equality for the first-order fragment of IDesc? shouldn't be too tricky; hasn't been done23/07 00:21
Saizanjdanbrown: C and D are variables, not constructors, right?23/07 00:21
jdanbrownSaizan: right23/07 00:21
jdanbrownSaizan: fancy ⏐ is the constructor23/07 00:21
jdanbrownSaizan: maybe i should be quantifying instead of using the bound C, D, s, and t?23/07 00:23
Saizanjdanbrown: quantifying would make it work23/07 00:23
Saizanjdanbrown: otherwise you can use with C ⏐ s23/07 00:24
Saizanf eq with C ⏐ s; ... | x = ? and then C-c C-c eq23/07 00:25
jdanbrownhmm, same error when i try quantifying (updated hpaste)23/07 00:28
jdanbrownlet me try 'with'23/07 00:28
* Saizan is a bit rusty23/07 00:30
jdanbrownerr, messed up my primes. updated. (still same error)23/07 00:33
jdanbrownback to 'with'...23/07 00:34
jdanbrownSaizan: no luck with 'with', either (http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27968#a27975)23/07 00:39
jdanbrownstill refuses to unify the indices23/07 00:39
Saizanmy idea might just be flawed :)23/07 00:40
jdanbrown:/23/07 00:40
jdanbrownSaizan: well thanks for trying :)23/07 00:40
jdanbrownspent three days learning agda and building most of my model, and now i've spent another three days failing to compare two things for equality :(23/07 00:42
Saizanlemma : ∀ {t1 t2 s1 s2} -> t1 `=>` s1 ≡ t2 `=>` s2 -> s1 ≡ s223/07 00:44
Saizanlemma refl = refl23/07 00:44
Saizanyou can write that though.23/07 00:44
Saizanwhich, modulo constructor name, would be able to substitute your "cong un⏐₁"23/07 00:44
jdanbrownhmm23/07 00:44
Saizani believe it's called an inversion lemma, it is really just a witness of the injectivity of the constructor23/07 00:46
jdanbrownyeah, that makes sense in concept23/07 00:47
jdanbrowncan't make that lemma check either23/07 00:48
jdanbrownalso tried the --invertible-type-constructors flag ;)—but still no luck23/07 00:49
jdanbrownfoo : ∀ {C s D t} → C ⏐ s ≡ D ⏐ t → s ≡ t23/07 00:49
jdanbrownfoo refl = refl23/07 00:49
Saizanwhat's the definition of Com ?23/07 00:50
jdanbrownit's an existential:23/07 00:50
jdanbrown  Com : Set23/07 00:50
jdanbrown  Com = ∃ λ D → (Fun D ₀ (ι "X") ⟶̣̇  ι "X") ×23/07 00:50
jdanbrown                (Fun D ₀ (ι "X") ⟶̣̇  D ₀ (D ₀ (ι "X")))23/07 00:50
jdanbrown'Com' for comonad23/07 00:51
jdanbrown(ignore the funny dots after the long arrow)23/07 00:51
jdanbrownso it's a Σ type23/07 00:52
Saizanit shouldn't matter anyhow.. but i've no idea how foo could fail to typecheck23/07 00:52
jdanbrownoops, it does matter23/07 00:53
jdanbrownfoo : ∀ {s t s′ t′} → s + t ≡ s′ + t′ → s ≡ s′23/07 00:53
jdanbrownfoo refl = refl23/07 00:53
jdanbrownthat works23/07 00:53
jdanbrownlooks like i started with the hard case :X23/07 00:53
Saizanheh23/07 00:54
jdanbrownalright, let me see how far i can get with this23/07 00:54
jdanbrowni'll defer the sigma cases for now23/07 00:54
jdanbrownthanks Saizan!23/07 00:54
Saizannp :)23/07 00:55
pigworkerjdanbrown: had a quick look in your pastebin - in the last entry I can see, you have _ in the with column where (yes refl) might allow you some progress (replacing D with .C at the same time)23/07 01:16
jdanbrownhmm23/07 01:16
jdanbrownpigworker: just updated with the latest version23/07 01:18
dolioBoy, even Data.Fin.Props is hard work, apparently.23/07 01:18
jdanbrownpigworker: the short cases in the middle work fine, but the top case (χ χ' : String) and the bottom case (C D : Σ ...) are stuck using the silly postulate method23/07 01:19
jdanbrownpigworker: so you're suggesting i try matching (yes refl) instead of _? let me see...23/07 01:19
pigworkeryes, and add the .pattern ftw23/07 01:19
jdanbrownk23/07 01:20
jdanbrownhmm, but that's still independent of the lemma ⏐₂-inj : ∀ {C s D t} → C ⏐ s ≡ D ⏐ t → s ≡ t , right?23/07 01:22
jdanbrownok, so let me try this lemma: ⏐₂-inj : ∀ {C s t} → C ⏐ s ≡ C ⏐ t → s ≡ t23/07 01:23
jdanbrownstill no go23/07 01:23
pigworkerthese lemmas are the uphill struggle lemmas23/07 01:23
jdanbrownhmm23/07 01:23
jdanbrownwhat do you suggest instead?23/07 01:23
pigworkermy buddies and I wrote a paper about this in 2004 "A few constructions on constructors"23/07 01:23
pigworkerthere's a way to prove constructors injective and disjoint in one go; but it's still annoying that you even need to, and it's tediously quadratic; but at least it's only tedious23/07 01:25
jdanbrownok23/07 01:25
Saizanstill if we can't even prove one constructor injective, i'm not sure how that's going to work for all of them :)23/07 01:25
pigworkerIt is disturbing that dependent pattern matching isn't cutting it.23/07 01:27
jdanbrownand it appears that the constructors that simply recur work fine. all and only the ones that pull from a different datatype refuse to pass the injectivity lemma—one datatype is the Σ-type Com from above, another is String, and another is a different ADT i defined23/07 01:28
pigworkerBut, by the way, in old fashioned type theory, with old fashioned eliminators, proving all constructors injective is way easier than proving just one of them injective.23/07 01:28
jdanbrownand maybe i should note that this is all in a large 'mutual' block (though i really hope that doesn't matter!)23/07 01:28
pigworkershouldn't make a difference23/07 01:32
pigworkergotta go fall over; it's late in Glasgow23/07 01:39
dolioWell, I got decidable equality via isomorphism with finite sets.23/07 01:47
dolioTakes only 33 lines for a 4-constructor type instead of... 16.23/07 01:47
jdanbrownheh23/07 01:48
jdanbrowncould you have gotten by with injection instead of isomorphism?23/07 01:48
dolioI tried injectivity first, but then I realized that you'd have to do all the cases to prove injectivity.23/07 01:49
dolioSo you might as well just prove decidable equality directly.23/07 01:49
jdanbrownah, ok23/07 01:49
jdanbrowniso is easier? do you just directly prove the equalities fg = 1 and gf = 1?23/07 01:49
dolioYes.23/07 01:50
dolioSo you match once per constructor per direction.23/07 01:50
dolioAnd once per constructor for each of the two functions.23/07 01:51
dolioSo I guess it's 4*n lines instead of n*n.23/07 01:51
dolioPlus some extra cruft.23/07 01:51
jdanbrowncould you save half the work and only prove fg = 1? that should establish injectivity23/07 01:52
jdanbrowndolio: i'll consider that23/07 01:56
jdanbrowngtg23/07 01:56
doliojdanbrown: You were right, by the way. You only need a retract, not isomorphism. So I redid it a bit: http://code.haskell.org/~dolio/agda-share/html/DecEq.html23/07 05:04
dolioLets you use naturals, too, which is less of a hassle.23/07 05:04
jdanbrowndolio: nice!23/07 05:04
dolio'3' is so much nicer to type than 'suc (suc (suc zero))'.23/07 05:06
jdanbrownthis is great. i will use this and cut out most of my ugly code :)23/07 05:08
jdanbrownprogramming with math is so much fun23/07 05:08
dolioYes. :)23/07 05:08
jdanbrowndolio: you should update your darcs ;)23/07 05:13
jdanbrowni still see the IsoDec module23/07 05:13
dolioOops, done.23/07 05:18
jdanbrownthanks!23/07 05:22
jdanbrownafter i finish doing this the hard way i'll start over and see how much more easily i can do it with a retract23/07 05:22
jdanbrowndolio: i hacked on your retraction module a little. i added binary trees as a convenient space to retract from for basic ADTs—check out the example at the bottom. :)23/07 10:02
jdanbrowndolio: let me know what you think23/07 10:02
benc___anyone have favourite font/window settings for textmode display of agda-style unicode?23/07 13:15
* benc___ finds even with a big font some stuff, like = with questionmark above it, is barely discernable23/07 13:15
* benc___ using os x terminal23/07 13:15
liyangI was going to ask what point of the abstract keyword is, but I seem to have found an answer already: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VisibilityAndEvaluation23/07 15:15
liyangBut what's the point of an abstract postulate? Surely if x is only postulated, you can't evaluate/inspect it anyway…23/07 15:16
danbrownanyone up for a small code review? ;)23/07 21:28
danbrowni've coded up a simple model of STLC where i'm trying to make agda automatically construct proofs that variables are in scope23/07 21:29
danbrownhttp://acandystore.org/agda/Lambda.html23/07 21:29
danbrownboth the Var and the Lam case work fine in isolation, but i get "unsolved metas" in some cases when i use App—see example terms M3 and M8 at the bottom (both commented out)23/07 21:31
Saizandoes it work if you give the s argument to App explicitly?23/07 21:35
danbrownah, that's a good question23/07 21:36
danbrown(_those_ metas!)23/07 21:36
danbrownpigworker: dolio and i came up with a way to code up propositional equality for ADT's that is slightly less horrible than what i was trying yesterday: http://acandystore.org/agda/Retract.html23/07 21:37
pigworkerchecking it out23/07 21:38
danbrown(it might very well be a special case of the paper you pointed me to yesterday)23/07 21:39
Saizanwith a rose-tree it would have reminded me of prolog even more :)23/07 21:39
danbrowna rose tree would probably be easier to code against—notice that my example is all 0- and 2-ary :/23/07 21:42
pigworkerI see: a kind of dump-to-LISP strategy23/07 21:43
danbrownshould be an easy change23/07 21:43
danbrownyeah23/07 21:43
danbrown3n easy clauses instead of n^2 hard ones23/07 21:43
danbrownit breaks down when you start putting funny things like function spaces in your constructors. but i think it shouldn't' have a problem with mutual recursion, at least23/07 21:45
pigworkerAs long as you have an easy time picking dummy values for the projection, you should be laughing.23/07 21:46
danbrownwhy laughing?23/07 21:46
pigworkerI mean, for first-order data (including mutual datatypes), embedding to trees (or S-expressions) will be fine; projecting will also be fine, provided you can think of where to send the junk.23/07 21:49
pigworkerThings get trickier if you want to play this game for datatypes which enforce stronger invariants.23/07 21:50
danbrownhmm, ok23/07 21:53
danbrownSaizan: yes, explicitly giving {s = o) to App works23/07 21:56
pigworkerBut there ought to be a good generic programming solution (at the cost of using encoded, rather than directly declared data).23/07 21:56
dolioIf only there were a language where directly declared data *was* encoded. :)23/07 21:59
pigworkerdolio: I'd never have thought of that!23/07 22:00
danbrownhave other systems solved this problem? it seems like it should be basic (though i'm sure that's naive)23/07 22:01
pigworkerEpigram 2, which is so not ready for serious use in lots of other ways, has encoded data from the get-go.23/07 22:02
pigworkerWe do a lot of experiments in Agda, so we have kit for making Agda types, at the cost of seeing the encoding.23/07 22:06
pigworkerDecent sugar for finite enumerations with named elements would help a lot.23/07 22:08
--- Day changed Sat Jul 24 2010
soupdragonanyone read Knuths book Surreal Numbers?24/07 17:26
--- Day changed Sun Jul 25 2010
soupdragonconways numbers are defined like this:25/07 10:26
soupdragon{A|B}25/07 10:26
soupdragonand there is no a in A, b in B such that b <= a25/07 10:27
soupdragonthat relation is defined like {X_L|X_R} <= {Y_L|Y_R}25/07 10:28
soupdragon:<=>25/07 10:28
soupdragonthere is no x in X_L such that {Y_L|Y_R} <= x25/07 10:29
soupdragonand there is no y in Y_R such that y <= {X_L|X_R}25/07 10:29
soupdragon-------------------------25/07 10:29
soupdragonso if you iterate this you quickly build up natural numbers and fractions25/07 10:29
soupdragonbut if you use transfinite induction you get infinitesimals and infinite numbers, as well as trancendentals25/07 10:30
soupdragonSo how would you define this in agda? Clearly it is inductive-recursive25/07 10:30
dolioDeciding on an {A|B} is a big part of the problem.25/07 10:33
soupdragonwhat do you mean25/07 10:34
dolioHow do you represent A and B?25/07 10:34
dolioThey're supposed to be sets.25/07 10:35
soupdragonthey are what we are defining25/07 10:35
soupdragonoh wait sorry I get hwat you mean25/07 10:35
dolioI guess you could just use multisets and not worry about it.25/07 10:35
soupdragonthey are *sets of* what's being defined25/07 10:35
soupdragonand we have no notion of a set in agda25/07 10:35
dolioBut they're potentially infinite, so you need big-enough index sets if you're going to use something like I -> S.25/07 10:36
soupdragonwhat could I be?25/07 10:38
dolioWe have things like sets, but they don't behave quite the way set-theoretic sets do.25/07 10:38
soupdragonrealy??25/07 10:39
dolioTypes are like sets.25/07 10:39
soupdragonoh yeah but Sigma would be negative here25/07 10:39
dolioYou can mimic set-theoretic sets, too.25/07 10:41
dolioBut they can be lacking, too.25/07 10:41
soupdragonyeah short of embedding ZFC I have no idea how t o d o this25/07 10:41
dolioThere's no good way to get powerset in Agda.25/07 10:41
dolioWhich means your sets are limited to being a lot smaller.25/07 10:42
soupdragonI was wondering about indexing the type25/07 10:42
soupdragonlike  Surreal K : *25/07 10:42
soupdragonso you could have  Surreal (Surreal K) : *25/07 10:42
soupdragonetc25/07 10:42
soupdragonbut it doesn't seem to play nice25/07 10:43
dolioI think the best you can do with regard to powersets is have, for x : V i, P x : V (suc i).25/07 10:43
soupdragonso it does not appear there is any way to do this25/07 13:56
soupdragonsets seem to be able to be any size25/07 13:57
--- Day changed Mon Jul 26 2010
copumpkinomg I've been itching to use agda for the past month26/07 17:43
ccasinwhat's stopping you?26/07 17:44
copumpkinnot having a computer for the past month and a bit26/07 17:44
copumpkinbut now I do again!26/07 17:45
copumpkinmuahaha26/07 17:45
benmachineoh, welcome back26/07 17:45
ccasin:)26/07 17:45
copumpkinthanks :)26/07 17:45
benmachinein that month and a bit I've... lurked26/07 17:45
benmachineand still done no agda whatsoever26/07 17:45
benmachinegood times.26/07 17:45
copumpkin:o26/07 17:45
copumpkinwhy not?!?26/07 17:45
benmachinemostly because I have to either learn emacs or make it pretend to be vim :P26/07 17:46
copumpkinlol26/07 17:46
copumpkinpeople make too much of a deal about that26/07 17:46
copumpkinit's not that bad26/07 17:46
copumpkinI only use emacs for agda26/07 17:46
benmachineyeah but it takes round tuits26/07 17:46
* benmachine wonders if this is a vaguely common expression26/07 17:47
copumpkin:o26/07 17:48
* copumpkin hasn't heard it26/07 17:48
benmachineprobably not then :P26/07 17:49
benmachinebasically, the idea is I won't do it until I get a round tuit26/07 17:49
benmachinehomophony pun26/07 17:49
copumpkinand now my goal is suc i == zero26/07 18:08
copumpkinmmm26/07 18:08
Saizana pumpkin!26/07 18:49
copumpkinYes!26/07 18:49
copumpkinA Saizan!26/07 18:49
Saizan:D26/07 18:49
copumpkinhow's it going?26/07 18:51
Saizannot bad, but coding more haskell than agda lately26/07 18:51
copumpkinaha26/07 18:52
Saizanit feels dangerous, non-exhaustive pattern matches everywhere!26/07 18:52
Saizanyou?:)26/07 18:52
copumpkinoh no!26/07 18:52
copumpkinbeen traveling for the last month and a bit26/07 18:52
copumpkinso no agda or haskell!26/07 18:53
Saizanback to US now?26/07 18:53
copumpkinnah, italy26/07 18:55
copumpkinwhy would adding a with clause but not pattern matching against its result stop the code from typechecking?26/07 19:30
copumpkinso f x = ? works fine, f x with g x \n ... | q = ? doesn't26/07 19:30
copumpkinwhere g x has a valid type26/07 19:30
ccasinwhat kind of type error do you get?26/07 19:34
ccasin(or perhaps just paste your code)26/07 19:35
copumpkinsuc max != w of type Fin (suc (suc n))26/07 19:41
copumpkinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28244#a2824426/07 19:42
copumpkinif I remove the with max {suc n} it doesn't complain26/07 19:42
Saizanwhat if you write out "lemma₀ {suc n}" instead of ... ?26/07 19:43
copumpkinsame26/07 19:44
Saizanis there a way to see how with gets desugared, btw?26/07 19:45
copumpkinnope, but I know it involves a w!26/07 19:45
Saizanheh26/07 19:46
ccasinseems like a bug to me26/07 19:46
ccasinwell, more accurately, I don't understand what is happening either :)26/07 19:47
ccasinI'd report it26/07 19:47
copumpkinit does seem like it shouldn't care about the with if it's got a valid type and I'm not pattern matching26/07 19:49
Saizanit's probably substituing "max {suc n}" to q in the goal26/07 19:50
ccasinI didn't see any "max {suc n}"s in the goal, though26/07 19:50
Saizanwell, the "n" in the type becomes "suc n" in that branch26/07 19:51
ccasinyeah, you are right26/07 19:52
Saizancopumpkin: s/| max {suc n}/| suc (max {n})/  ?26/07 19:52
ccasinmore precisely, when I turned on implicit arguments I was hoping to see that computation was stuck on a "max {suc n}"26/07 19:52
ccasinbut it doesn't seem that way26/07 19:52
copumpkinSaizan: that turns yellow but works26/07 19:52
Saizan(using with rather than |)26/07 19:53
ccasinoh, I'm reading wrong completely... hmm26/07 19:53
Saizanit seems there's some desync on how the patterns should affect the goal..26/07 19:55
copumpkinis http://code.google.com/p/agda/issues/list down?26/07 19:56
Saizanseems so26/07 19:57
benc___the 'with' stuff kinda sounds like problems i had with my bubblesort playing26/07 20:03
benc___that was not termination checking in some cases26/07 20:03
benc___http://www.blogger.com/post-edit.g?blogID=4983265076111025145&postID=885559526527194916626/07 20:04
benc___heh not that26/07 20:04
benc___http://benctechnicalblog.blogspot.com/2010/07/branching-on-left-vs-branching-on-right.html26/07 20:06
Saizanbenc___: what's the disadvantage of the if version?26/07 20:22
benc___saizan: i had the impression that case based proofs didn't ork so well with it26/07 21:10
benc___maybe they do - i didn't play with that any more26/07 21:10
kptit's just a function26/07 21:10
copumpkinif you're ignoring the results of your decidable yes/no thingy then it should be equivalent26/07 21:11
Saizani think they'd work just the same26/07 21:11
benc___well yes26/07 21:11
copumpkinby results I mean the attached proofs26/07 21:11
benc___thats what I thought26/07 21:11
benc___but they don't (termination-check-wise)26/07 21:11
Saizanthe if is the one that termination-checks, right?26/07 21:12
benc___copumpkin: yeah some of the stuf fi did later that I haven't writen about uses the resulting proofs from the decidables26/07 21:12
benc___saizan: 'if' termination chesk adn 'with' doesn't26/07 21:12
benc___i'll add the if definition ina comment26/07 21:12
Saizanand proofs about onepass written with if shouldn't be significantly different from ones about onepass with with26/07 21:13
benc___i use proof from the 'with' in at least one case (to derive a contradiction to show that path won't happen) .. is that still going to work with if?26/07 21:17
Saizanyeah, and if pattern matching on the Dec in the proof also gives you the same problem about termination checking you can write a version of if that passes the two proofs to the branches26/07 21:19
benc___ok26/07 21:20
benc___maybe i'll play with that some26/07 21:21
* benc___ doesn't really grok why one works and the other doesn't, though26/07 21:21
copumpkinI'm kind of confused about my proof here26/07 21:21
copumpkinmaybe I've just been away from agda for too long26/07 21:21
copumpkinlemma₀ {suc n} with succ (max {suc n})26/07 21:22
copumpkin...            | k = {!!}26/07 21:22
copumpkinGoal: k ≡ zero26/07 21:22
copumpkinlemma₀ : ∀ {n} → succ (max {n}) ≡ zero26/07 21:22
copumpkinthe overall goal makes sense to me, but the k == zero goal does not26/07 21:23
copumpkinbecause if I pattern match on k I get zero == zero and suc q == zero26/07 21:23
copumpkinand the latter is obviously false26/07 21:23
Saizannot enough obvious, otherwise you could have written lemma₀ {suc n} = refl26/07 21:25
Saizani think you want to recurse on n26/07 21:25
copumpkinoh I mean, it's asking me to prove something that's false26/07 21:25
copumpkin?0 : zero ≡ zero26/07 21:26
copumpkin?1 : suc i ≡ zero26/07 21:26
Saizangiven (lemma₀ {n}) you should be able to prove lemma₀ {suc n}, i think26/07 21:26
copumpkinI thought so but couldn't get it26/07 21:29
copumpkinso I was trying something that seemed more direct26/07 21:29
Saizan(if you remember that suc i == succ (max {suc n}) usign a separate equality you might be able to prove that case is impossible..)26/07 21:29
Saizanthere's a "with-\==" for that in the stdlib, iirc26/07 21:30
copumpkinSaizan: but I don't really want to prove that case is impossible26/07 21:50
copumpkinit's disturbing that it is :P26/07 21:50
Saizandisturbing that it allows that case at all?26/07 21:51
copumpkindisturbing that it's not an impossible case, and it leads to an impossible goal26/07 21:51
copumpkinit's not one of those absurd pattern situations26/07 21:51
copumpkinor _|_-elim26/07 21:51
copumpkinit sort of is an impossible case, I guess, but I can only prove that by recursion26/07 21:52
copumpkinand I haven't figured out how to convince it of that yet26/07 21:52
copumpkinnot sure how to explain26/07 21:54
Saizani'd try to prove "view max == vmax" first26/07 21:54
copumpkinokay will try that :)26/07 21:56
Saizanor maybe that a value of EmbMax is completely determined by the indices26/07 21:56
copumpkinhm, how so?26/07 22:33
copumpkinI can sort of see what you mean, I think26/07 22:40
Saizani'm not sure if it's true, but the type of that would be forall {n f} (p q : EmbMax {n} f) -> p == q26/07 22:43
copumpkinAn internal error has occurred. Please report this as a bug.26/07 22:43
copumpkinLocation of the error: src/full/Agda/Auto/Convert.hs:65426/07 22:43
copumpkinlol26/07 22:43
copumpkin(unrelated to what you just wrote)26/07 22:43
--- Day changed Tue Jul 27 2010
doliobenmachine: I used to have a round tuit.27/07 00:56
benmachinedolio: yeah, I've seen them on sale27/07 00:57
dolioI think I got mine for free from a home show.27/07 00:57
benmachineheh27/07 00:57
copumpkinI want a "HOWTO get your complicated patterns to be accepted by agda"27/07 17:56
ccasinit's called --type-in-type27/07 18:26
soupdragon;(27/07 18:26
copumpkin:P27/07 18:27
AmadiroSo I herd you like types...27/07 18:42
ccasinno?27/07 19:11
ccasinI see27/07 19:11
copumpkinCannot pattern match on constructor vemb, since the inferred27/07 19:11
ccasinyes27/07 19:11
copumpkinindices [{suc n'}, emb i] cannot be unified with the expected27/07 19:11
copumpkinindices [{n}, max] for some y, i, n', n27/07 19:11
copumpkinwhen checking that the expression ? has type vmax ≡ q27/07 19:11
ccasinmaybe more informative is the wrong phrase :)27/07 19:11
copumpkinI sort of understand what it's saying but I don't know how to appease it27/07 19:11
ccasinan error I've seen before is more accurate27/07 19:11
ccasinyou can look at the mailing list to see what they told me to do when I got a similar error in a different situation27/07 19:12
ccasinI would just describe it, but it's complicated27/07 19:12
Saizanwhat's the name of the thread?27/07 19:12
ccasin"equality reasoning and contradictory type indices"27/07 19:13
ccasinbasically, I think we should write a lemma using "where" which just renames p but takes as a hypothesis that it is equal to vmax27/07 19:15
ccasinthen we should be able to split on q, and reason by transitivity in the non-contradictory case27/07 19:15
ccasinugh, this doesn't work though.  We probably also need to abstract over p's index27/07 19:17
ccasinand q27/07 19:17
ccasinwell, that's not right either, but I'll stop talking now and just make it work first :)27/07 19:17
copumpkinlol27/07 19:17
Saizanmade it work going trough heterogeneous equality27/07 19:23
ccasinyes, I had to as well, sadly27/07 19:24
ccasintoo many levels of indices27/07 19:24
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a2828527/07 19:29
ccasinyeah, nice.  I'm still trying to find a way with only homogeneous equality, but it looks like maybe you win27/07 19:31
soupdragonccasin, why?27/07 19:31
ccasinthere is an extra level of telescoping here, and it's too much for the trick I mentioned27/07 19:32
soupdragonI mean, why the preference for homogeneous equality - is it philosophical?27/07 19:32
ccasinno, the puzzle is just more fun that what I'm supposed to be working on27/07 19:32
soupdragonlol27/07 19:32
soupdragonperhaps you can find a theorem about Fin which is equivalent to K27/07 19:33
soupdragonthat would be interesting27/07 19:33
ccasinit shouldn't be too hard to formulate one about what you can prove by pattern matching on Fin27/07 19:34
ccasinnot that I'm volunteering27/07 19:35
ccasin:)27/07 19:35
soupdragonyeah but I did everything up to Fin injectivity by pigeonhole argument without K27/07 19:35
ccasinhmm27/07 19:36
soupdragonso it's not a trivial thin27/07 19:36
soupdragonthing27/07 19:36
ccasinI think proving (Fin 2) /= Bool should need K27/07 19:38
ccasinthough that's not just about Fin27/07 19:38
soupdragonyou can't even prove that with K afaict27/07 19:38
ccasinwell, I can prove it in agda27/07 19:38
soupdragonare you sure??27/07 19:38
ccasinI think...27/07 19:38
ccasinI've done something similar.  Let me see27/07 19:39
soupdragondefinitely want to see the proof if you write this27/07 19:39
ccasinthe trick should be to define a proposition P which is true of a set just when there is an element of the set that == True27/07 19:39
ccasinagda's typechecking of () patterns will be strong enough to see that P doesn't hold of (Fin 2)27/07 19:40
ccasinAt least, I think so.  Let me try27/07 19:40
ccasinsoupdragon: here you are27/07 19:51
ccasinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28286#a2828627/07 19:51
ccasinis this surprising?27/07 19:51
ccasinThe only evidence that I have of needing K for this is that I was unable to do it in coq27/07 19:52
ccasinnot a principled reason27/07 19:52
soupdragonvery27/07 19:52
soupdragonI am baffled27/07 19:52
soupdragonI wish you'd done this without importing anything27/07 19:52
ccasinit shouldn't be too hard27/07 19:52
ccasinuse two new 2-element sets instead, and reinvent the equality stuff27/07 19:53
copumpkin?27/07 19:53
soupdragonI think this is some voodoo coming from the agda solver, not K27/07 19:53
ccasinyes, I'd believe that.  proving that P is not true of (Fin 2) is just where I get stuck in coq.27/07 19:54
ccasinare you a K expert?  I am a novice27/07 19:54
ccasinmy intuition is all just from what I have been able to prove in agda and coq27/07 19:55
soupdragonwell the thing about Coq is it actually has a theory27/07 19:56
soupdragonwhereas agda is just like hack every type system rule that can fit in27/07 19:56
ccasin:)27/07 19:56
soupdragonso anyway I think there's probably a rule in there (if you can find it deep in the haskell source files) which compares equality of names of types27/07 19:56
copumpkinsoupdragon: beware of the worker of pigs telling you to stfu ;)27/07 19:56
ccasinI prefer to think of it as UTT + modest experimental extensions27/07 19:56
soupdragonmaybe it's part of the injectivity thing27/07 19:57
ccasinwell, term constructors should be injective even in coq, right?27/07 19:57
soupdragonyeah in theory it's got a theory27/07 19:57
ccasin:)27/07 19:57
soupdragonbut in practice it's just not27/07 19:57
ccasinyes, I'm just playing27/07 19:57
soupdragonwhen people prove false in agda they patch it, rather than going back to the drawing board27/07 19:57
soupdragonproving Fin n = Fin m -> n = m is a nontrivial problem27/07 19:58
soupdragon(in Coq)27/07 19:58
soupdragonyou need to pigeonhole it27/07 19:59
ccasinright - that's injectivity of type constructors though27/07 19:59
soupdragonoh sorry27/07 19:59
ccasinI don't need that here27/07 19:59
soupdragonI don't know what 'term' means27/07 19:59
soupdragonyou can prove injectivity (usually) using the methods from...27/07 19:59
soupdragon(the NoConfusion stuff)27/07 19:59
soupdragona few construction on constructor27/07 20:00
ccasinI meant that data constructors from datatype definitions are injective, but the types you get from datatype definitions are not27/07 20:00
soupdragonccasin, well not all of them are injective27/07 20:00
soupdragonbut you can usually prove it using a single methodical way27/07 20:00
soupdragonbut injectivity of dependent pairs is equivalent to K for example, so you can't prove that27/07 20:00
ccasinso I guess you are saying that you think something about the way agda typechecks my ()s is equivalent to the injectivity of Fin?27/07 20:01
ccasinit's a little surprising to me27/07 20:02
soupdragonno27/07 20:02
soupdragonI wondre if it accepts    q : ¬ Bool ≅ Fin 2 ; q ()27/07 20:03
ccasinno, it doesn't27/07 20:03
ccasinit used to27/07 20:03
ccasinthey took that out when it turned out to be inconsistent with LEM :)27/07 20:03
soupdragonthis is interesting though27/07 20:04
soupdragonespecially ¬pfin27/07 20:04
ccasinyeah, for a while I thought agda could only prove that types of different sizes were different27/07 20:07
ccasinI think Saizan suggested this approach, actually27/07 20:08
soupdragonwhat about a type with no constructors?27/07 20:08
Saizandoes it help any if you add a (Bool == Fin 2) argument to ¬pfin in Coq?27/07 20:09
soupdragontwo different types with no constructors27/07 20:09
ccasinhmm, interesting question27/07 20:09
soupdragonSaizan, well I think it's consistent to promote isomorphisms to identities27/07 20:09
soupdragonat least model theoreticallyars27/07 20:10
soupdragonyou can identity them27/07 20:10
ccasinSaizan: I'm a little confused - wouldn't that assumption only make it harder:27/07 20:13
ccasinor, I don't see how it helps27/07 20:13
Saizanwell, in agda, (a : A) ==h (b : B) implies A == B and that's unusual, iirc27/07 20:18
ccasinthat is different from coq (it depends on K), but it's not clear to me why (Bool == Fin 2) would help in proving ¬pfin27/07 20:33
Saizanah, i don't know either :)27/07 20:35
roconnorccasin: holy crap, you proved Fin 2 /= Bool!27/07 20:35
copumpkinoh e-pig.org is updated!27/07 20:35
roconnorwhat's the definition of ≅ ?27/07 20:36
ccasinroconnor: yes, isn't type theory fun?27/07 20:37
ccasinit's just propositional equality27/07 20:37
ccasinrefl27/07 20:37
ccasinoh, no, sorry27/07 20:37
ccasinhard to make out that ~27/07 20:37
roconnor:)27/07 20:37
ccasinthat one is John Major equality27/07 20:37
roconnorcan you paste the data definition?27/07 20:38
ccasinsure, let me find it27/07 20:38
ccasindata _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where27/07 20:39
ccasin  refl : x ≅ x27/07 20:39
ccasinThis is the "standard" heterogeneous equality in agda, coq and epigram27/07 20:39
roconnorwell, no one (should) uses JM equality in Coq27/07 20:39
ccasinwhy not?27/07 20:39
ccasinI confess I have used it27/07 20:40
roconnorthe elimination principle in Coq is almost useless27/07 20:40
roconnoryou have to add an axiom to make it useful27/07 20:40
ccasinyes27/07 20:40
soupdragonwhich axiom?27/07 20:40
roconnorAxiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.27/07 20:40
soupdragonoh you mean the elimination principle of JMeq27/07 20:40
soupdragonI think you can get by with no axioms if you use a slightly different formulation27/07 20:41
soupdragonit's a waste of time though27/07 20:41
roconnorI doubt that very much27/07 20:41
soupdragonwhat we really need it JMEq27/07 20:41
soupdragoneq27/07 20:41
soupdragonand K properly27/07 20:41
ccasinroconnor: do you know if Fin 2 /= Bool is an expected consequence of K?  I really have no idea27/07 20:42
roconnorccasin: I'm wondering that27/07 20:42
roconnorI find it plausible27/07 20:42
soupdragonI don't think it's a consequence of K27/07 20:42
roconnorbut if it is true, I didn't know it27/07 20:42
roconnorit seems pecuiliar27/07 20:43
soupdragonthere's a constaint solves deep in the agda source and i'm sure someone got tempted one day, and added a rule that does this27/07 20:43
ccasinyes, the key is the type checking of () patterns27/07 20:43
roconnorccasin: what is the key?27/07 20:43
ccasinand I think soupdragon is right that there are no theorems about that solver27/07 20:43
soupdragondont get me wrong agda is BEEEEPing awesome27/07 20:44
ccasinin ulf's thesis I think it's not elaborated into something known, or anything like that27/07 20:44
soupdragonbut it upsets me that everyone uses it27/07 20:44
ccasinroconnor: if you look at the pasted code, it comes down to the proof that some property is false about (Fin 2)27/07 20:44
ccasinthat proof relies on agda's empty pattern magic27/07 20:44
ccasincertainly I don't know how to do it in coq and think it is probably not true27/07 20:45
roconnorccasin: where is the empty pattern?27/07 20:45
ccasinit's the ()s27/07 20:45
soupdragonbecause everyone is like "oh I'll learn about type theory which lets you do proofs" and they use something which is more about exploring the design space than writing software that could kill smoeone if it had a bug in it27/07 20:45
ccasinwhen agda sees one of those, it tries to convince itself that whatever type that argument should have, it's empty27/07 20:46
roconnorsoupdragon: to be fair, there is no alternative, right?27/07 20:46
ccasinand then you don't have to fill in an RHS27/07 20:46
Saizandon't worry, you can't typecheck anything that could kill someone with the current memory requirements :)27/07 20:46
ccasinyeah, I don't think too many people are writing critical code in agda :)  It's just for playing.  Though paper reviewers are pretty generous about interpreting "I did it in agda" as a proof27/07 20:47
roconnorccasin: suc : Fin n -> Fin (S n) ?27/07 20:47
ccasinroconnor: yes27/07 20:47
soupdragonit's the same as people using unsafePerformIO in haskell27/07 20:47
roconnorccasin: Agda is sound isn't it?27/07 20:48
soupdragonit just pisses me off because I don't have anything else to care about27/07 20:48
ccasinroconnor: who knows?27/07 20:48
soupdragonwe would like to think Agda is sound27/07 20:48
roconnorI mean, it's not like Epigram 2 (currently) is27/07 20:48
roconnorgrossly unsound27/07 20:48
soupdragonhuh I don't know about that27/07 20:48
roconnorsoupdragon: Epigram 2 has (Currently) type in type27/07 20:49
roconnorccasin: so in what way does work in Agda not count as a proof?27/07 20:49
ccasinroconnor: no one knows how to prove bottom in agda right now.  but, it definitely has some extensions to well-understood type theories that no one has done the metatheory for27/07 20:49
roconnorI think I'd trust Agda more than Coq.27/07 20:49
soupdragonI think that Epigram is going to have a fixed theory once it's matured a bit27/07 20:49
roconnorto be consistent27/07 20:49
roconnorthough I don't know Agda as well27/07 20:49
ccasinroconnor: really?27/07 20:50
ccasinat least coq elaborates to a small core for which the theory has been done27/07 20:50
roconnorccasin: The impredicativity in Prop in Coq is kinda frightening.27/07 20:50
soupdragonroconnor, the number of times people have proved false in agda....27/07 20:50
soupdragonroconnor, and the fact there is no fixed theory written down somewhere. for me that is not a good sign27/07 20:50
roconnors/Coq/CIC,  s/Agda/whatevers Agda's logic is/27/07 20:50
soupdragonoh I get what you mean27/07 20:51
soupdragonit's not about Agda though27/07 20:51
soupdragonit's about CIC vs Martin Lofs stuff27/07 20:51
ccasinroconnor: maybe, but there are PhD theses which prove CiC is consistent27/07 20:51
ccasinagda doesn't have a well specified core logic with this property27/07 20:51
roconnorccasin: That's great if you think ZFC is consistent.27/07 20:51
soupdragoncompletely impossible to follow any normalization proofs for things like CIC :(27/07 20:51
soupdragonor even Coq27/07 20:51
soupdragon*CoC27/07 20:51
roconnorMy worries about the consistenty of Coq applies to Z as well27/07 20:52
ccasinwell, I can't help you there27/07 20:52
roconnormaybe that makes me a little crazy :)27/07 20:52
* soupdragon doesn't know what Z means27/07 20:52
roconnorsoupdragon: ZFC without the C and without the F (replacement).27/07 20:53
soupdragonoh yes I do27/07 20:53
soupdragonthanks27/07 20:53
roconnorMLTT has a nice small proof theoretic ordinal.27/07 20:53
soupdragonbut roconnor agda supports inductive recursive defintions27/07 20:53
roconnortrue27/07 20:53
roconnorI don't know how much power that adds.27/07 20:54
roconnorI'd guess it is still less than Coq, but I don't really know27/07 20:54
roconnorpart of my problem of not having studied Agda's logic27/07 20:54
ccasinthere is no logic to study27/07 20:54
ccasinat best, it claims to be based on UTT27/07 20:54
ccasinbut UTT has an impredicative prop27/07 20:54
soupdragonyeah this is the problem really - I think agda is more just about exploring the language design space27/07 20:55
soupdragonrather than writing proofs you can beleive in27/07 20:55
roconnorso these () in you proof27/07 20:56
roconnoryou are suggesting that the magic pattern matchin in Agda is stronger than K?27/07 20:56
ccasinI am suggesting I don't know27/07 20:56
roconnorI thought the Agda thesis proved that it was equivalent to something or other plus K.27/07 20:56
* soupdragon thinks it is stronger than K27/07 20:56
ccasinI figured it was just K.  But soupdragon is skeptical, and I have no good evidence27/07 20:56
roconnorsoupdragon: that's interesting27/07 20:57
soupdragonI mean there is a model where bool and Fin 2 are identified right?27/07 20:57
soupdragoneven one that has K27/07 20:57
soupdragonbecause bool and Fin 2 are in Set, rather than Prop27/07 20:57
roconnordoes it have K?27/07 20:57
roconnorsoupdragon: this model is proof irrelevent (hence implying K?)27/07 20:58
soupdragonor maybe there isn't a model with propertly.... I remember reading a scary document about how the obvious model with proof irr. was wrong27/07 20:58
roconnorya27/07 20:58
ccasinwell, you make a good point: "dependent pattern matching" is coq + K.  But, I don't know exactly how empty patterns are dealt with in those papers27/07 20:58
soupdragonyeah I think what's happening in this source file is dependent pattern matching + constraint solving27/07 20:58
soupdragonThe paper Eliminating Dependent Pattern Matching27/07 20:59
ccasinpigworker: ping27/07 20:59
ccasinmaybe we can just ask an expert...27/07 20:59
soupdragonshows how you can see that pattern matching and K are equivalent27/07 20:59
ccasinthere are sure enough of them in here27/07 20:59
pigworkerer, hello?27/07 21:00
ccasinsorry to bug you, but we're having an argument about this:27/07 21:00
ccasinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28286#a2828627/07 21:00
ccasinis the proof of ¬pfin surprising?27/07 21:00
ccasinI figured it was just standard dependent pattern matching27/07 21:01
soupdragonI'm not even sure how someone gets up to the level where they can follow a SN proof of one of these type theories27/07 21:01
soupdragonI mean I can just about see what's happening when you do candidates for reducbility on system f27/07 21:01
soupdragonbut that's pushing it27/07 21:01
soupdragonlet alone come up with this stuff from scratch27/07 21:01
roconnorpigworker: wheras soupdragon and I think that  ¬pfin shouldn't be provable even with the K axiom.27/07 21:01
soupdragonit makes me just want to give up tbh27/07 21:02
pigworkertrying to figure out what's going on...27/07 21:02
pigworkerso, Fin 2 isn't Bool, because none of its elements is "true"?27/07 21:03
ccasinyes27/07 21:03
ccasinagda accepts that, though I think one can't do it in coq27/07 21:04
pigworkerThat's more than K.27/07 21:04
ccasinawesome, thanks27/07 21:04
soupdragonhow do you reason that?27/07 21:04
pigworkerIt's deducing something from a heterogeneous equation.27/07 21:04
roconnor[15:18] <Saizan> well, in agda, (a : A) ==h (b : B) implies A == B and that's unusual, iirc27/07 21:05
soupdragonin Coq (a : A) ==h (b : B) implies A == B27/07 21:05
soupdragonJMeq A a B b -> A = B27/07 21:05
roconnorsoupdragon: really?27/07 21:05
ccasinno, I think now27/07 21:05
ccasin*not27/07 21:05
pigworkerThat's one way to set up het eq (indeed, that's what I did in my thesis)27/07 21:05
soupdragonthat's fine, it's  JMeq A a A a' -> a = a'  you can't prove27/07 21:05
roconnoroh27/07 21:05
soupdragonroconnor yeah it's just the same as injective pairing, you can project the first part but not the second27/07 21:06
pigworkerIndeed, if you defined het eq as equality on Sigma Set id, that's exactly what it is.27/07 21:06
roconnorok, so that isn't the issue here27/07 21:06
roconnorAgda's magic patterns are doing something more.27/07 21:07
soupdragonpigworker: when I first learned about type theory I thought that being able to define eq as a data type was so beautiful and Right... but it built in in OTT  :(27/07 21:07
roconnorccasin: let's prove  ¬ ¬ (Bool ≡ Fin 2) as well! \o/27/07 21:07
pigworkerBut here, Agda's dismissing a het equation between distinct value constructors of different types27/07 21:07
soupdragonroconnor god dammit I wish I thought of that!27/07 21:07
pigworkerThat's type-constructors-distinct by the back door, I suspect, at least for datatypes.27/07 21:09
Saizanor maybe it's just ignoring the types and comparing the constructor names?27/07 21:10
pigworkerSaizan: that's exactly what I think is happening27/07 21:10
ccasinroconnor: sounds like fun, but how?  Here the assumption of (Bool == Fin 2) is really doing some work for us27/07 21:11
ccasinpigworker: well, there are a few I don't know how to prove inequal still27/07 21:12
ccasinfor example, two empty datatypes27/07 21:12
pigworkeryeah, that's not gonna succumb to this trick27/07 21:12
pigworkersoupdragon: being able to define eq as a datatype is a heinous evil27/07 21:13
soupdragonreally!27/07 21:13
soupdragon?27/07 21:13
soupdragonwhy27/07 21:13
pigworkerbecause equality of codata, etc, isn't inductive27/07 21:15
soupdragon"It is tempting to think of isomorphic objects in a category as 'the same', but this is also problematic and does not lead (as far as we know) to a workable alternative. For example ... and this information would be discarded if we simply chopped up the category into isomorphism classes, draconially promoting all isomorphism to identity morphisms"27/07 21:17
soupdragonI just read that in my algebra book and thought of you :p27/07 21:17
soupdragonoh yes. I am always forgetting about codata for some reason27/07 21:17
pigworkerbut you also remember functions, right?27/07 21:18
soupdragonyeah27/07 21:18
pigworkerAnd yes, I'm very wary of any attempt to be casual about isomorphisms. I don't think you learn the structure of a set by counting.27/07 21:19
soupdragonI used to think it didn't make sense to equate quicksort with mergesort27/07 21:19
soupdragonbut I can see that it actually does27/07 21:19
pigworkerIf you want to distinguish them, instrument their behaviour.27/07 21:21
pigworkerLooks like this channel is doing the hokey cokey.27/07 21:29
Saizanthe what?:)27/07 21:30
Saizanoh, netsplits.27/07 21:31
pigworker"...in, out, in, out, shake it all about..."  but this is normal, is it?27/07 21:32
copumpkinccasin: did you have any luck with my evil pattern match btw?27/07 21:33
copumpkinugh27/07 21:33
soupdragonlol27/07 21:33
soupdragonyeah it happens a lot27/07 21:33
Saizanit happens from time to time on irc networks27/07 21:33
ccasincopumpkin: Saizan pasted some code earlier using hetero eq27/07 21:33
Saizantoo little redundancy.27/07 21:33
ccasinI found I couldn't do it with just homogeneous equality.  telescopes were too long27/07 21:34
copumpkinccasin: ah, I must've been disconnected... I'll check the logs27/07 21:34
copumpkinand thanks to both of you :P27/07 21:34
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28285 <- here it is27/07 21:34
copumpkinwow27/07 21:35
copumpkincool27/07 21:35
copumpkinthanks! will play some more now :)27/07 21:38
soupdragonccasin: couldnt' do what?27/07 21:39
soupdragon(isn't the whole point of telescopes that the lenght doesn't matter?)27/07 21:39
Saizannp :)27/07 21:39
ccasinsoupdragon" right, but to represent a telescope you need heterogeneous equality.  I was curious if I could prove the theorem in question using just homogeneous equality, but there were too many levels of type indices to make it practical27/07 21:40
soupdragonwhat theorem??27/07 21:41
pigworkerI wouldn't wish hom-eq telescope management on anyone.27/07 21:41
Saizansoupdragon: the one at the bottom of my link27/07 21:42
ccasinsoupdragon: the one in copumpkin's file.  See the lemma2 in the thing saizan just pasted.  I'm not saying it can't be done, just that because of the number of indices using a telescope is much cleaner27/07 21:43
ccasinwith heterogeneous equality and all27/07 21:43
copumpkinhas anyone had any success with C-c C-a yet? I keep trying it every so often on simple things and I don't think I've ever had it work on non-trivial terms27/07 21:46
ccasinI've got to run.  pigworker: thanks for your help with the pattern matching question27/07 21:46
roconnorSaizan: where do I find import Function?27/07 21:47
copumpkinit's still in the std lib27/07 21:47
copumpkinassuming you have a fairly recent one27/07 21:47
roconnorI go version 0.327/07 21:48
roconnorgot27/07 21:48
Saizanit was Data.Function in earlier versions, iirc27/07 21:48
Saizanyou can comment that import out, anyhow27/07 21:49
copumpkinI was using it further down27/07 21:49
copumpkinI only included a prefix of my file in the original paste27/07 21:49
copumpkinEmbMax is kind of painful to work with sometimes27/07 21:59
roconnorwhat is the purpose of EmbMax?27/07 22:01
roconnorit seems useless to me27/07 22:01
copumpkinI did it a while ago (at pigworker's recommendation) cause it made defining succ a lot cleaner than what I had before27/07 22:03
roconnorokay, so it is a view27/07 22:03
copumpkinyep27/07 22:03
pigworkerIt's still a struggle to reason with these things. We need a new knack, from somewhere...27/07 22:04
copumpkin ∀ {m} (n : Fin (suc m)) → view n ≡ vmax → succ n ≡ zero27/07 22:06
copumpkinsomething like that doesn't typecheck27/07 22:06
Saizanview n : EmbMax n; vmax : EmbMax max, you need Het eq there, i think27/07 22:08
copumpkinyeah27/07 22:08
copumpkinI guess I'll start using it more :)27/07 22:09
Saizan∀ {n} -> succ (max {n}) ≡ zero <- this one is easy at least :)27/07 22:09
copumpkinto state or to prove? :o27/07 22:09
Saizanboth27/07 22:10
copumpkinooh27/07 22:10
Saizan(using lemma2)27/07 22:10
copumpkinI started all this yak shaving to prove that27/07 22:10
copumpkinyeah27/07 22:10
* copumpkin tries again27/07 22:10
roconnorwouldn't data EmbMax : {n : ℕ} → Fin (n) → Set  be easier?27/07 22:10
copumpkinI think I tried that first but had trouble because max needs Fin (suc n)27/07 22:11
pigworkerInstinctively, I'd do what roconnor just suggested.27/07 22:12
copumpkinhmm, that is what I tried27/07 22:12
copumpkinhow do I get vmax : EmbMax max to work?27/07 22:12
copumpkinwhen max : {n} -> Fin (suc n)27/07 22:12
pigworkervmax : forall {n} -> EmbMax (max {n}) ?27/07 22:13
copumpkinoh duh27/07 22:14
* copumpkin kicks himself27/07 22:14
* copumpkin cleans the rest of the code up after that27/07 22:14
roconnor vmax : ∀ {n} → EmbMax {suc n} max27/07 22:15
roconnor:)27/07 22:15
pigworkeroddly, that stuff just worked in Epigram 127/07 22:16
pigworkerI mean, vmax : EmbMax max27/07 22:16
copumpkinman, this is making things so much cleaner27/07 22:16
pigworkerNow, the real question is how to construct a DSL for isos.27/07 22:17
danbrownwhat does it mean when agda2-mode accepts an agda2-give (C-c C-SPC), but immediately afterward checking again (C-c C-l) gives a type error?27/07 22:23
copumpkinprogramming with one hand sure is a pain27/07 22:23
danbrownvoodoo or bug?27/07 22:23
pigworkerdanbrown: by my reckoning, that's always a bug27/07 22:24
pigworkeris it bug 246?27/07 22:24
roconnorI'm lost in Agda without my match-return statement27/07 22:24
pigworkerroconnor: where's the sticking point?27/07 22:25
roconnorlemma₂ : ∀ {n f} → (p q : EmbMax {n} f) → p ≡ q27/07 22:26
roconnorlemma₂ {.(suc _)} vmax q = {!!}27/07 22:26
roconnorI want to do case analysis on q27/07 22:26
roconnorbut I need to generalize it's parameter first27/07 22:26
danbrownpigworker: unclear. but doesn't this bug claim to be fixed?27/07 22:27
pigworkeroh yeah, hardwired pattern matching gives up here; can you use "with"?27/07 22:27
pigworkerdanbrown: only a few days ago27/07 22:27
roconnorpigworker: perhaps, if I knew what with does :D27/07 22:27
pigworkerroconnor: the same as Coq's Generalize tactic27/07 22:28
pigworkermore or less27/07 22:28
danbrownpigworker: true. my agda darcs log indicates that i do have the fix27/07 22:28
* soupdragon has never figured out how to use with27/07 22:29
soupdragonwould rather the compiler typed that stuff out27/07 22:29
danbrownanyway, i'll try to isolate it27/07 22:29
pigworkeryou can always replace with by an explicit helper function (my old Lego implementation did that)27/07 22:32
roconnorwhat is agda's version of eq_rec?27/07 22:40
pigworkeryou need to substitute by an equation?27/07 22:48
pigworkeryou can define a version of eq_rec by pattern matching, but it's probably in the library already27/07 22:48
pigworkerthere's a nasty way to exploit equations with "with", but is there some fancy new "rewrite" thing?27/07 22:50
Saizanthere is, e.g. "foo x y rewrite bar x y = .."27/07 22:54
roconnorwhat is the symmetry lemma?27/07 22:55
Saizansym27/07 22:56
roconnorwell I'm half done lemma2  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a2828827/07 23:00
roconnorI need to go home now27/07 23:00
roconnorI'll worry about the second half later.27/07 23:00
Saizanmaxneq is my lemma0?27/07 23:01
roconnorer27/07 23:02
roconnormy mouse stoped working27/07 23:04
roconnorI wrote my own, because I sort of commented out a bunch of stuff27/07 23:04
roconnormaybe it is the same27/07 23:04
roconnorit is a proof that emb i /= max27/07 23:04
Saizansame type then, at least, i asked because you didn't include it in the paste27/07 23:05
roconnorya27/07 23:05
roconnorI forgot27/07 23:05
roconnorI changed the definition of EmbMax to use the n instead of suc n27/07 23:05
roconnorer27/07 23:05
copumpkindid you fix view?27/07 23:06
roconnorthe proof is a little different27/07 23:06
roconnorI'd paste it but my mouse doesn't work27/07 23:06
copumpkinlol27/07 23:06
roconnorroughtly speaking it says27/07 23:07
roconnormaxneq : forall {n} {i : Fin n} -> emv i /= max27/07 23:07
roconnormaxneq {zero} {()} _27/07 23:07
roconnormaxneq {suc n} {zero} ()27/07 23:07
roconnormaxneq {suc n} {suc i} eq = maxneq (suc-inj eq)27/07 23:07
roconnors/emv/emb/27/07 23:08
copumpkinoh that's nice27/07 23:08
copumpkinwell27/07 23:08
roconnorI need to head home27/07 23:09
roconnorttyl27/07 23:09
danbrownok, finally isolated it: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=2829027/07 23:15
danbrownis that error a bug, or am i abusing implicit arguments?27/07 23:16
danbrownone would expect that the line "c : B × B; c = b , b" with the error would be ok in all contexts27/07 23:22
Saizani guess it typechecks with "y : X {something} × X {something}", right?27/07 23:25
Saizanif so it looks like a bug, i'd have expected some unresolved metas rather than an error27/07 23:26
danbrown(sorry, just changed variables: x -> b, y -> c)27/07 23:27
danbrownit would need to be "y = x {something} × x {something}"27/07 23:28
danbrownbut that gives the same error27/07 23:28
danbrowne.g. "y = x {A} × x {A}"27/07 23:28
Saizanoh, true27/07 23:32
Saizanwait, is your Σ universe polymorphic?27/07 23:33
Saizanotherwise you'll need Σ\_127/07 23:33
pigworkeryeah, and sometimes oracle-based checking doesn't happen until reloading27/07 23:34
Saizansorry, i should've loaded it into agda earlier, this "works" http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28290#a2829127/07 23:35
Saizanyou also need the explicit abstraction, it's quite annoying27/07 23:36
danbrownSaizan: Σ is from the standard library (latest darcs), which is universe polymorphic27/07 23:36
danbrowntoggling the flag in my 'bug' module makes no difference27/07 23:37
Saizany : X × X; y = (\{s} -> x {s}) , (\{s} -> x {s}) <- i guess this is what really makes sense, don't know if the fact that x is not expanded to that automatically can be considered a bug27/07 23:37
danbrowni see27/07 23:38
pigworkerVery interesting. This looks like one of those nasty corner cases where having "hidden Pi" in your type theory screws up.27/07 23:39
danbrownSaizan: yes, that does solve my problem (back in the original code). thanks!27/07 23:39
danbrowni'll file an issue27/07 23:40
danbrowntitled "Fix all the problems with hidden Pi" :P27/07 23:40
pigworkerI wound Ulf up about it in his defence, but he didn't bite...27/07 23:40
pigworkerThe problem comes when you're trying to solve blah : ?A and blah has a hidden Pi type. Do you take ?A to be the hidden Pi-type, or its instance with an unknown argument? Neither strategy is most general.27/07 23:42
pigworkerI am familiar with this turd because I've stepped in it myself.27/07 23:44
* copumpkin resists the temptation to @remember that27/07 23:45
Saizanmy istinct would be to add some new constraint to the system so that the decision can be postponed27/07 23:46
danbrownjeez, i think there are three different bugs bound up in this, though the other two are more superficial27/07 23:47
danbrownone with error reporting and one with agda-mode27/07 23:47
pigworkerSaizan: mine too, but it sometimes causes a deadlock to postpone it -- if you use (blah : ?A) where a B is expected, you don't know whether ?A is B, or whether ?A is a hidden Pi which specialises to B...27/07 23:51
pigworkerI'm pretty sure Agda commits too early on this. Choosing less than most general solutions means order of constraint-solving is important, which can then result in stuff checking interactively but not reloading.27/07 23:54
pigworkerHere's a nice perverse example...27/07 23:58
pigworkery : {n : Nat} -> ? ; y = max     (where max : {n : Nat} -> Fin (suc n)) is accepted, with some yellow, but...27/07 23:59
--- Day changed Wed Jul 28 2010
pigworkerx : {! {n : Nat} -> ? !} ; x = max    does not allow the refinement28/07 00:00
Saizandanbrown's example works in GHC with ImpredicativeTypes, but they are going to scrap that in 6.14 because it's ugly :)28/07 00:03
pigworkerGuessing where the foralls go is a weird game: I don't think machines are very good at it.28/07 00:05
pigworkerI think we need a bit of Milner, here. My plan is to make "hidden Pi" a feature of type *schemes*, rather than types.28/07 00:07
pigworkerMy difference with Milner is that I don't think type schemes should be restricted artificially so that machines can guess them, and that they should always be pushed in.28/07 00:09
Saizanhow does that mix with higher-rank ones?28/07 00:09
pigworkerMy grammar of schemes is SCH ::= TYPE | {x : TYPE} -> SCH | (x : SCH) -> SCH28/07 00:10
pigworkerIf schemes are known in advance, it is always clear where applications or lambdas should be inserted.28/07 00:11
pigworkerAnd crucially, there's no trade in scheme inference.28/07 00:11
pigworkerIn effect, I'd forbid danbrown's definition of X: that's not a Set, it's a scheme.28/07 00:13
pigworkerPut differently, no hidden Pi in the underlying theory, but implicit syntax as an elaboration convention.28/07 00:15
Saizani see28/07 00:16
pigworkerhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.ImplicitSyntax28/07 00:17
Saizanbut defining X = (_:Set) -> A; x : {_:Set} -> A; would still make "x : X" hold, right?28/07 00:18
pigworkerno; X is Set -> A, and x makes an A; A is not Set -> A28/07 00:19
pigworkerx : {_:Set} -> A  is, of course suspect  (R. Burstall: "plus can't infer its arguments")28/07 00:20
Saizanok, since x is really "x {_}", so we'd have to manually abstract like i did above28/07 00:21
pigworkerBut you would at least get (\_ -> x) : X with some yellow.28/07 00:21
pigworkerThere's no way to eliminate the manual override.28/07 00:22
Saizany : X × X; y = (\{s} -> x ) , (\{s} -> x ) <- works with some yellow, with the original X28/07 00:23
pigworkerAnd yes, the idea is that high-level x means low-level x {_}, without further debate.28/07 00:23
pigworkerYes, that'd be enough to deflect the usual defaulting strategy.28/07 00:24
Saizanthese manual abstractions are really ugly though, i'd really expect it could do better, given the type signature28/07 00:25
pigworkerIt's not a popular observation, but in real H-M languages, with bottom, type inference isn't complete -- but by parametricity, the uninferred types don't matter!28/07 00:26
pigworkerThat's telepathy at work: there are too many degrees of freedom.28/07 00:28
Saizani guess the fundamental problem is that "\{s} -> x {s}" and "\{_} -> x {somethingelse}" are often both valid solutions, unless x's return type mentions the argument28/07 00:31
Saizanand, more to the point, they are in this case28/07 00:31
pigworkerGenuine choice needs genuine bits.28/07 00:32
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28294#a28294 <- i can't see why those (\{_} -> ..) shouldn't be inferrable, though28/07 00:34
pigworkerI agree. The type pushed in should supply the \{_} ->.28/07 00:38
pigworkerI wonder how bidirectional checking has been implemented. This is a funny corner.28/07 00:38
pigworkerIf we separate InTm from ExTm, the question is how to push {x : S} -> T into an ExTm.28/07 00:40
pigworker(that's ExTm ::= Var | ExTm InTm | ...    InTm ::= ExTm | \Var -> InTm | ...   if you were wondering; types get pushed into InTm and extracted from ExTm)28/07 00:41
Saizanso we'd have to push where we normally extract from instead?28/07 00:44
pigworkerWorking from the outside in, the question is which happens first, "completion" (i.e. inserting the \{_} ->) or "change of direction", inferring the type of the ExTm, then checking type equality? I don't know what actually happens.28/07 00:46
pigworkerWorse, if the type you're pushing is ?A, do you change direction immediately, or do you wait to see if some other constraint instantiates ?A with {x : S} -> T ? It's a rat's nest.28/07 00:47
roconnorwhat does yellow mean in agda?28/07 00:50
pigworkersus pish ous28/07 00:50
pigworkermore seriously, it means that the highlighted term does not currently have the type it needs to go where it has been put, but that future metavariable instantiations could perhaps fix that problem28/07 00:52
Saizanfor recursive definitions it might also mean that they don't pass the termination check, but that's unrelated :)28/07 00:54
pigworkeroh, does that happen now?28/07 00:54
pigworkerin older versions, termination checking only happened after reload28/07 00:54
pigworkerMostly, if you see yellow, it's a good plan to "show constraints"28/07 00:55
pigworkerBack in the day, Alf and Agda 1 would accept the term anyway, but tell you the constraints. God help you if you ran it.28/07 00:56
Saizani only use C-c C-l, so i don't really know..28/07 00:56
roconnorhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a2829628/07 00:57
roconnorHere is my homogenous proof of lemma228/07 00:57
pigworkerI like a bit more interaction, but I don't go very far without reloading. I need colour, apart from anything else.28/07 00:57
roconnorI'm not very good at Agda, so there are probably some trivial optimizations28/07 00:58
pigworkerOh crap, it's 1998 all over again.28/07 00:58
roconnorAnd there isn't really any good reason not to use hetrogenous equality28/07 00:58
pigworkerExcept that in 1998, it hadn't been invented.28/07 00:58
roconnorThis was mostly an Agda exercise for me :)28/07 00:59
pigworkerIt's a bad flashback for me.28/07 00:59
pigworkerThe truth, not told in my thesis (or maybe in a footnote) is that I implemented pattern matching on top of homogeneous equality, with K and its computation rule, and all those hairy substs. It all worked. I demoed it at TYPES '98. And then I invented JMeq and felt really stupid.28/07 01:02
* dolio finally catches up.28/07 01:03
dolioI guess Fin 2 /= Bool is bad because it must not be provable in plain old type theory?28/07 01:04
dolioOr the homotopy folks would be up a creek.28/07 01:04
pigworkerThere are models which identify them, sure.28/07 01:04
roconnorpigworker: OTT is just syntatic sugar for setoids and homogenous equality. :)28/07 01:05
pigworkerit took me years to convince Thorsten of the untruth of that remark28/07 01:06
dolioroconnor: By the way, about that folding/unfolding stuff the other day...28/07 01:06
dolioIt occurred to me that there's a difference between the fold type you linked to and what I was using.28/07 01:06
roconnoroh?28/07 01:07
dolioThe fold you linked to was a Church-encoding, so it represented a list. It did so by building a function that would accept an algebra, and produce a result.28/07 01:07
roconnorthat sounds normal28/07 01:08
dolioWhat I was using was a wrapper around the algebra. So it didn't represent a list, but a way of eliminating the list.28/07 01:08
dolioAnd you can use that type to build up more complex algebras out of simple ones.28/07 01:08
dolioThat's why it was existentially quantified.28/07 01:08
roconnorwhich one was yours?28/07 01:09
dolioThe existential, algebra one.28/07 01:09
dolioI didn't use any of its features, though.28/07 01:09
roconnoroh in your code?28/07 01:09
roconnorah28/07 01:09
roconnornow I know what you are talking about28/07 01:09
dolioYou can use it to build an efficient average algebra out of a sum algebra and a length algebra, though.28/07 01:10
dolioOr, that's the idea.28/07 01:10
pigworkerMeanwhile, in equality land, Thorsten's 1999 paper gives you extensional equality by supplying syntactic sugar for setoids with homogeneous equality, provided definitional proof irrelevance is available.28/07 01:10
danbrownSaizan: pigworker: a different syntactic workaround for the problem earlier: "record { proj₁ = x; proj₂ = x }" instead of "(λ {s} → x {s}), (λ {s} → x {s})"28/07 01:12
pigworkerThat system, however, lost the property that subst refl = id. It gained extensional propositional equations but lost intensional definitional equations, and broke by translation of pattern matching.28/07 01:12
pigworkers/by/my28/07 01:13
pigworkerdanbrown: now that's scarily flaky28/07 01:13
roconnordolio: ya, your existential quantifiers seemed strange28/07 01:14
roconnorI removed it :D28/07 01:14
roconnorpigworker: K provide that?28/07 01:14
Saizanyeah, maybe it's more prone to eta-expand inside records?28/07 01:14
roconnor_ah what did I miss?28/07 01:15
pigworkerroconnor: I was just about to speculate that K (rather than full P-I) might be enough for Thorsten's 1999 system to go through, but it wouldn't fix subst refl /= id.28/07 01:15
danbrownbut it at least lets me proceed with my work in a non-disgusting way :)28/07 01:15
pigworkerSaizan: a distinct possibility; these things are so delicate28/07 01:19
pigworkerRe equality again, moving to het eq got rid of the need for P-I (more reason to suspect K is enough); homotopy TT reminds me a little of proof-relevant OTT28/07 01:23
dolioI have trouble reading the Coq stuff that someone posted to the agda list on that a little while back...28/07 01:24
pigworkerI saw it but didn't take it in. Distractions.28/07 01:25
dolioBut it sounded almost like they used K, only couched in homotopy language.28/07 01:25
dolioMaybe it's sufficiently different, though, because I thought K was supposed to blow up with that.28/07 01:26
pigworkerK says Bool = Bool in one way, but we know two isos.28/07 01:27
dolioYes, but the summary of the 'equivalence axiom' given is something like "all equivalences are equivalent to identity".28/07 01:28
pigworkerisn't that more like "permutations are invertible"?28/07 01:29
dolioWhich certainly sounds like K to me, only with all the identities involved being the homotopy kind.28/07 01:29
pigworkerAll isomorphisms are the identity, up to isomorphism. Or something like that. Deep.28/07 01:30
dolioRight.28/07 01:30
dolioOf course, it's better than K, apparently, because it gets you extensionality of functions.28/07 01:31
pigworkerUniqueness of identity proofs and extensionality of functions are certainly separable.28/07 01:33
pigworkerYou can have either without the other.28/07 01:33
dolioI mean they proved that the equivalence principle implies extensionality.28/07 01:34
pigworkerSounds plausible.28/07 01:34
dolioI guess all they need to do now is prove extensionality for codata, and you'll be out of a job. :)28/07 01:39
dolioEquality-wise, maybe.28/07 01:40
pigworkerI'm perfectly happy for them to believe that.28/07 01:42
dolioHeh.28/07 01:43
dolioI guess functions get you part of the way there, even, in that you can encode quite a lot of codata as Pi + inductives.28/07 01:45
pigworkerDon't get me wrong. I'm very interested in being able to work up to iso; I'm nervous about ignoring finer distinctions.28/07 01:46
pigworkercodata takes Pi + inductives + quotients, in general28/07 01:47
dolioYeah, I'm not sure how I feel.28/07 01:47
dolioFor instance, if you follow the category folks, heterogeneous equality is close to an abomination.28/07 01:48
dolioSome of them have done a lot of work developing the idea that it only makes sense to talk about equality of things if you already know they're in the same set.28/07 01:49
dolioIn opposition to traditional set theory.28/07 01:49
pigworkerDepends on how you interpret het eq.28/07 01:50
pigworkerThese days, I take (a : A) = (b : B) to mean the extensional TT (A = B) -> a = b28/07 01:51
pigworkerwhich is perfectly typable28/07 01:51
dolioI think that's still a problem.28/07 01:51
dolioBecause it talks about equality of sets/types, which aren't elements of a set. They're objects in a category.28/07 01:51
dolioEliminating talk about equality of arbitrary sets was the big motivation, as I understand it.28/07 01:52
dolioBut, perhaps you could interpret the premise as 'A and B are isomorphic.'28/07 01:53
dolioI don't know.28/07 01:54
pigworkerthat's one way, and it similarly tells you how to pull the value equation into one set28/07 01:55
dolioAh, yes, that's true.28/07 01:56
pigworkerYou could also consider restrictions where A = F x, B = F y, and you hypothesize that x = y.28/07 01:57
pigworkerThe CT people are not used to coping with the distinction between def eq and prop eq.28/07 01:59
dolioYes, that's also true.28/07 01:59
pigworkerNor are most people, frankly. That's a type theory paranoia.28/07 01:59
pigworkerOne might even say a European type theory paranoia, if bold.28/07 02:00
pigworkerTIme I wasn't here. G'night.28/07 02:10
copumpkinis there a way to convince agda to show implicits in goals and other displays of stuff?28/07 10:48
copumpkinnormally I just temporarily go through my code and make implicits explicit when I need to see what they are28/07 10:48
copumpkinbut that's a pain28/07 10:48
pigworkerThere's C-c C-x C-h but I don't know what it actually does.28/07 11:10
copumpkinI wish I could see the with desugaring28/07 12:17
copumpkini just got a new error that refers to the desugared form28/07 12:18
copumpkinaha finally28/07 12:25
copumpkinhow did I get a conflict pulling from the agda repo28/07 12:51
copumpkinwhen I've never made any changes to my local copy o.O28/07 12:51
copumpkinis n : Fin 5 heterogeneously equal to n : Fin 6 for example?28/07 13:28
copumpkinsay zero : Fin 5 and zero : Fin 628/07 13:28
soupdragonzero 4 : Fin 528/07 13:28
soupdragonzero 5 : Fin 628/07 13:28
soupdragonisn't it28/07 13:28
copumpkinoh, makes sense28/07 13:29
soupdragonsuc 5 (zero 4) : Fin 6 and so on28/07 13:29
copumpkinyeah28/07 13:29
copumpkinokay, so no :)28/07 13:29
copumpkinthanks28/07 13:32
copumpkinmax != w of type Fin (suc n)28/07 14:03
copumpkin:(28/07 14:03
copumpkinSaizan: do you have any hints on how to prove succ max == zero using lemma2?28/07 14:29
copumpkinI wish I could stop encountering this damn with-desugaring issue28/07 14:36
benc___is there a library function that will take  (no (a<=b -> bot)) and give me b<=a  (or something similar?)28/07 14:37
* benc___ sees a lot of stuff in lib-0.3 vaguely in that area28/07 14:37
copumpkinno == not?28/07 14:45
copumpkinas in, is that not (not (a <= b)) ?28/07 14:45
copumpkinseems like if it's one negation, you'd want b < a28/07 14:45
copumpkinbut either way, it probably depends on what type this is ranging over28/07 14:48
copumpkinoh, no being the constructor of Decidable28/07 14:48
benc___ja28/07 14:48
benc___so what i was thinking of is a case where I compare a and b and eitehr get a proof a<=b or a proof b<=a28/07 14:49
benc___but what I get for the no case is function from a<=b -> bottom28/07 14:49
soupdragonyou can go from  no (P x -> bot)  to  P x  for any decidible P28/07 14:49
soupdragonhm28/07 14:50
soupdragonyou can go from  no (P -> bot)  to  P  for any decidible P28/07 14:50
copumpkinyou could also use the Ordering + compare thing on Data.Nat28/07 14:52
benc___yeah28/07 14:52
benc___soupdragon: am i missing characters? no (P-> bot) means that P is not true, so how can you go to P?28/07 14:52
soupdragonoh I thought it means P isn't not true28/07 14:53
copumpkinyou can use total probably, too28/07 14:53
copumpkinseems closer to what you want?28/07 14:55
copumpkinTotal _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)28/07 14:55
copumpkin  total : Total _≤_28/07 14:55
benc___yeah i think so28/07 14:56
benc___something like that28/07 14:56
soupdragonhttp://www.cs.nott.ac.uk/~nad/repos/lib/src/Relation/Nullary/Core.agda28/07 14:58
soupdragondata Dec {p} (P : Set p) : Set p where28/07 14:58
soupdragon  yes : ( p :   P) → Dec P28/07 14:58
soupdragon  no  : (¬p : ¬ P) → Dec P28/07 14:58
soupdragonso   no prf   with  prf a proof of  P -> bot,  would say that P isn't not true28/07 14:59
soupdragonI think you can prove Dec P -> ¬ ¬ P -> P28/07 15:00
benc___~28/07 15:01
benc___.28/07 15:01
benc___oops28/07 15:01
benc___i'll play with total a while and see what I end up with28/07 15:03
benc___shower first28/07 15:03
copumpkinsoupdragon: yeah28/07 15:03
Saizancopumpkin: the main point is that succ max directly pattern matches on view max, so in your proof you can do the same, and lemma2 tells you what to expect.28/07 15:09
copumpkinyeah, I was trying that but then encountered the with-desugaring incomprehensible error28/07 15:10
copumpkinam trying to withify it myself with a helper function now28/07 15:10
copumpkinmaybe I'm overcomplicating it though28/07 15:10
Saizanoh, it worked with with for me, but you can also use rewrite28/07 15:11
copumpkinoh it works if I take out another helper now28/07 15:11
Saizan(you've to pass the right 'n' to lemma2, somehow)28/07 15:12
copumpkinI'm still not too sure how to incorporate the "lemma2 tells you what to expect" though... right now I have http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28325#a2832528/07 15:16
copumpkinthe _|_-elim is because that case is ridiculous28/07 15:16
copumpkinand is expecting me to prove suc i == zero28/07 15:17
copumpkinI guess I'd have to incorporate the knowledge that view max /= vemb28/07 15:17
copumpkinto get a bottom out of that28/07 15:18
Saizanwell, if you pattern match on "lemma₂ {suc n} (view max) vmax" at the same time as "view (max {n})", the refl let you put .vmax as pattern for the latter28/07 15:19
copumpkinoh28/07 15:20
Saizanso the vemb case doesn't present itself at all28/07 15:20
copumpkingenius!28/07 15:20
copumpkinlol28/07 15:20
copumpkinand of course, doing that gives me the with bug28/07 15:20
copumpkin:(28/07 15:21
soupdragonwhat are you actually trying to prove28/07 15:22
soupdragon?28/07 15:22
copumpkinlemma₃ : ∀ n → succ (max {n}) ≡ zero28/07 15:22
soupdragonyeah I can't read that28/07 15:22
Saizancopumpkin: it doesn't here..28/07 15:22
copumpkinsucc max == zero28/07 15:22
Saizanlemma4with : ∀ {n} -> succ (max {n}) ≡ zero28/07 15:22
Saizanlemma4with {n} with view (max {n}) | lemma₂ {suc n} (view max) vmax28/07 15:22
Saizanlemma4with | .vmax | refl = refl28/07 15:22
Saizan^^^ typechecks fine28/07 15:22
copumpkinsoupdragon: where succ is the "circular" successor28/07 15:22
Saizanmaybe it's fixed in my version of agda28/07 15:22
copumpkinSaizan: I just darcs pulled earlier today28/07 15:22
soupdragonwhere are the definitions of these things then?28/07 15:23
soupdragonoh it's a bug in agda?28/07 15:23
copumpkinSaizan: ah, that works for me... I had a remaining with on just max {n} from when I was breaking up view (max {n}) and that was messing it up28/07 15:24
copumpkinsoupdragon: yeah, it's reported too but hasn't been fixed28/07 15:24
copumpkinsometimes the with desugaring conflicts with something invisible and gives you an error about a w variable that appears nowhere in your own code28/07 15:25
Saizanlemma4 : ∀ {n} -> succ (max {n}) ≡ zero28/07 15:25
Saizanlemma4 {n} rewrite lemma₂ {suc n} (view max) vmax = refl28/07 15:25
Saizannicer, btw :)28/07 15:25
copumpkinwhat exactly is rewrite?28/07 15:26
soupdragonso 'view' is just a normal function?28/07 15:26
copumpkinis it covered somewhere online?28/07 15:26
Saizansoupdragon: yes28/07 15:26
copumpkinsoupdragon: yeah, it takes a Fin into an EmbMax (which tells you whether you have the largest value in the Fin or not)28/07 15:26
soupdragonyeah I never understood why the introduced 'rewrite', I thought pattern matching on refl was supposed to do it28/07 15:26
soupdragonI wonder why you use 'EmbMax' rather than just saying 0 is max28/07 15:27
Saizanhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28285 <- code28/07 15:27
copumpkinsoupdragon: for simplicity with other arithmetic operations defined elsewhere28/07 15:27
Saizanhttps://lists.chalmers.se/pipermail/agda/2009/001314.html <- rewrite explanation28/07 15:28
copumpkinthanks!28/07 15:28
copumpkinI have been handed an absurd heterogeneous equality and want to get _|_ from it28/07 16:29
copumpkincon {suc m} ~= con {suc (suc m)}28/07 16:30
benc___using total gets me the reversed inequality that i wanted btw28/07 16:30
soupdragonthat's no cycles, tricky28/07 16:30
soupdragonyou have to use induction28/07 16:31
soupdragon(to see why this needs induction consider  m = suc m  on co-natural numbers)28/07 16:32
copumpkinhm28/07 16:33
copumpkinbenc___: I'm glad :)28/07 16:33
soupdragondid you resolve "am i missing characters? no (P-> bot) means that P is not true, so how can you go to P?"28/07 16:34
soupdragonbenc28/07 16:34
benc___benc28/07 16:34
benc___oh you were addressing me in your line above28/07 16:34
soupdragon...28/07 16:34
benc___soupdragon: no, i still don't undersand what you mean28/07 16:35
benc___http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28327#a2832728/07 16:36
benc___thats what i did in the end28/07 16:36
benc___soupdragon: if I have p->bot, how do I get p?28/07 16:37
copumpkinyou don't want p28/07 16:37
copumpkinyou want "flip p"28/07 16:37
copumpkinyou need additional information about it28/07 16:37
benc___ja28/07 16:37
copumpkinnot all Ps have flips28/07 16:37
soupdragonthat's not what I was saying28/07 16:37
soupdragonI tried to explain it in some detail earlier28/07 16:38
benc___soupdragon: right. i didn't think it was but i think i'm missing non-ascii characters from your pastes28/07 16:38
benc___i get the dec p -> not not p -> p bit28/07 16:38
benc___i think that would have worked for me too28/07 16:38
soupdragonyeah that was the important thing28/07 16:39
benc___i think i need a better irc client for this channel though.28/07 16:40
copumpkin_*_ : ∀ {n} → Fin n → Fin n → Fin n28/07 18:00
copumpkinzero * n = zero28/07 18:00
copumpkinm * zero = zero28/07 18:00
copumpkin(suc m) * (suc n) = succ (emb (m + n + m * n))28/07 18:00
copumpkinanyone see anything wrong with that definition?28/07 18:00
copumpkinoh, there's something wrong with my addition I think28/07 18:01
soupdragonare you treating Fin n as integers mod n?28/07 18:03
copumpkinyeah28/07 18:03
soupdragonim confused why you don't define all these operations as induced by the homomorphism28/07 18:03
copumpkinhow so?28/07 18:03
soupdragonsince this way is a lot harder28/07 18:03
copumpkinI'd love to make it easier28/07 18:09
copumpkinoh I see what's wrong with my definitions28/07 18:12
copumpkinbut am not sure how to fix them :(28/07 18:12
soupdragonwell you know how  3*7+1 +  3*4+2 = 3*12+0  and mod 3 you get 1 + 2 = 028/07 18:15
copumpkinyeah28/07 18:15
soupdragonyou can use that sort of idea to define + on Z/3Z28/07 18:15
copumpkinhm28/07 18:15
soupdragonas well * and others28/07 18:15
copumpkinnot really sure how to make that into an actual function28/07 18:18
soupdragonmod n : Z -> Fin n ; (nk+r) mod n = r28/07 18:19
soupdragonusing the "evil" nk+r patterns28/07 18:20
soupdragonbut you also have  eta : Fin n -> Z ; eta 0 = 0 ; eta 1 = 1 ; ...28/07 18:20
soupdragonthen x + y  = (eta x + eta y) mod n28/07 18:20
copumpkinoh so I'd just use the standard lib mod28/07 18:21
copumpkinI considered that but it felt uglier28/07 18:21
copumpkinand harder to prove stuff about, maybe28/07 18:21
soupdragonwasn't think of the standard lib actually no28/07 18:21
copumpkinoh28/07 18:21
soupdragonwhat theorems are harder to prove this way28/07 18:23
soupdragon?28/07 18:23
copumpkinnot sure, I figured passing through the terrifying mod function would make things painful28/07 18:23
copumpkingiven the std lib one28/07 18:23
soupdragonI can't imagine it mattering actually, because you could just prove the defining equations of either characterization28/07 18:23
soupdragonno clue about the std lib28/07 18:23
copumpkinwell, how would you actually write mod?28/07 18:23
soupdragonnothing I said should dependen on that28/07 18:23
soupdragonI already defined it28/07 18:24
soupdragonyou need division algorithm for the nk+r pattern28/07 18:24
copumpkinthose patterns actually exist?28/07 18:24
soupdragonyeah you define it though28/07 18:24
soupdragonit's a view28/07 18:24
copumpkinoh, hm28/07 18:24
copumpkinI'll play with that then28/07 18:25
copumpkinhttp://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.DivMod.html#18428/07 18:25
copumpkinthat's what I was afraid of :)28/07 18:25
* soupdragon doesn't use this stuff28/07 18:25
copumpkinbut a view like that sounds fairly clean28/07 18:25
Saizanthe nice part is that you shouldn't need to care about the implementation of _divMod'_ because DivMod' specifies everything about it28/07 18:35
copumpkinhmm28/07 18:38
Saizana bit like you don't care about how view is implemented because of EmbMax and lemma228/07 18:41
copumpkinyeah28/07 18:41
Saizan(no idea which view makes most sense though, tbc)28/07 18:43
soupdragonpeanut better than junk28/07 18:59
copumpkinshould there be a difference in typechecking a function between passing a parameter implicitly via a module or adding it myself?28/07 19:18
copumpkinone typechecks and the other doesn't28/07 19:18
Saizanis it recursive? does the recursive call use the same value for this parameter?28/07 19:35
copumpkinnope not recursive28/07 19:35
Saizanalso, maybe there's some interaction with refinements..28/07 19:35
copumpkinit has to do with zero : Fin (suc n)28/07 19:35
copumpkinyeah, I think so28/07 19:35
copumpkinif I write f : Fin n -> Fin n28/07 19:35
copumpkinf zero = ...28/07 19:36
copumpkinwith the n from a module parameter28/07 19:36
copumpkinit complains about the zero being impossible28/07 19:36
copumpkinor rather, it not matching Fin n28/07 19:36
copumpkinif instead it's f : forall {n} -> Fin n -> Fin n it works fine28/07 19:36
Saizani guess you'd have to put n in a with28/07 19:36
Saizan"f i with n"28/07 19:37
copumpkinyeah28/07 19:39
copumpkinany way to "close" a top-level module in a file so I can pass its parameter?28/07 19:44
* copumpkin coughs: http://snapplr.com/9syf28/07 20:05
Saizanheh28/07 20:10
Saizani'd start by ignoring anything on the right of the | related to divMod :)28/07 20:11
copumpkinI wonder if this really will be easier than just working out the manual operations myself28/07 20:16
soupdragonthat's what I do28/07 20:48

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