dandelions arcatan pedagand --- Log opened Thu Jul 01 00:00:56 2010 --- Day changed Sat Jul 03 2010 http://www.reddit.com/r/reddit.com/comments/clmax/please_boycott_this_author/ 03/07 14:44 --- Day changed Mon Jul 05 2010 i'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 that's an embarrassing question, so don't laugh too loudly: does anybody have a universe for RelaxNG schema in Agda? 07/07 15:04 usually, one starts such question with "I have a friend who would like to know...", but I'm (almost) shameless 07/07 15:05 thats not a silly question! 07/07 15:30 that's a great use for dependent types 07/07 15:30 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 ago 07/07 15:31 well, using xml those days, many people would say that it's a silly idea :-) 07/07 15:35 Saizan_, ha indeed, thanks 07/07 15:36 I 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 anyway, I'm (hopefully) almost done with mine. Pretty-printing now... 07/07 16:02 th5, out of curiosity, do you use xml or similar with dependent types? 07/07 16:46 I've been pondering about that for some time now, but I don't know what is the state of that field 07/07 16:47 the most exciting example of dependent types meets web programming I know if is Adam Chlipala's ur/web project 07/07 17:01 which is a dependently typed programming language that generates provably valid html/AJAX stuff 07/07 17:01 *know of 07/07 17:02 I believe he had a pldi paper about it, also the implementation works and is fun to play with 07/07 17:04 I'll hear about that on Friday or Saturday I think (DTP workshop in Edinburgh). That's indeed interesting 07/07 17:04 ah, I'm jealous - DTP sounds like fun 07/07 17:05 oh my, just looking at the program, now I'm really jealous 07/07 17:08 :-) 07/07 17:09 I 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 attend 07/07 17:10 but I suspect it's "value-for-money", as would a British MP put it 07/07 17:10 :) 07/07 17:11 unrelatedly, does there exist a gentle introduction to inductive types in dependently typed languages? 07/07 17:12 I learned all I know from luo's book, but it's far from gentle 07/07 17:12 conor's thesis is nice, though the syntax is a slog for non-experts 07/07 17:13 maybe, some paper by Paulin-Mohring 07/07 17:14 not 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 yes, a good thought, though 07/07 17:15 I learned from Dybjer's paper "Inductive Families" 07/07 17:15 I wouldn't call that gentle either, mind 07/07 17:15 I'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 to 07/07 17:16 someone on our trellys list asked for an introduction 07/07 17:16 there's a bit in my thesis but I'm not sure it'll be much more helpful than Conor's 07/07 17:18 edwinb: haven't read that one, thanks 07/07 17:18 the dybjer paper, I mean 07/07 17:18 I suppose it depends what you mean by "gentle" and "introduction" 07/07 17:19 (and indeed "inductive" and "types"...) ;) 07/07 17:19 :) 07/07 17:19 what are you looking for in such paper? theoretical foundations? category theory stuffs? induction principles? etc. 07/07 17:19 for instance, for a categorical characterization, you've plenty of "container" papers 07/07 17:19 including Morris's thesis 07/07 17:20 I suspect that it's where I learned about those things 07/07 17:20 yes, I was thinking in particular of the basic stuff about how to check inductive definitions and generate and type their elimination principles 07/07 17:20 there are so many theses that do it, but I guess it's intricate enough that I'm silly to hope for a "gentle" one 07/07 17:21 from a CT perspective, you might be interested in: http://personal.cis.strath.ac.uk/~patricia/csl2010.pdf 07/07 17:21 I'll just link all the papers you've recommended :) 07/07 17:21 if you're familiar with fibrations, that's "gentle" and "introductory" 07/07 17:21 ah yes, I liked this paper 07/07 17:22 thanks for your help 07/07 17:23 I see from blogland that things are happening with Trellys 07/07 17:26 yes, it's fun 07/07 17:27 though there is still some disagreement about the purpose of the language 07/07 17:27 or maybe I just disagree with what they've decided :) 07/07 17:27 anyway, still under debate is the question of what sorts of induction principles trellys should be able to prove terminating 07/07 17:28 I'm rooting for full dependent pattern matching and more, though I think I will lose 07/07 17:29 I'd have thought that would at least partly depend on what the purpose of the language was... 07/07 17:30 yes 07/07 17:30 anyway, 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 at any rate, in a development surprising to no one, proving normalization properties about these dependent type theories is very hard 07/07 17:32 and since we're fiddling with recursion, we actually have to do it 07/07 17:32 I never worried about that too much with Idris 07/07 17:33 but then, I'm not trying to make something, erm... 07/07 17:33 * edwinb fails to find the word 07/07 17:33 I'm just a hacker, is what I'm saying ;) 07/07 17:33 :) 07/07 17:35 an important goal for trellys is being able to prove that even though we allow general recursion, the things we certify as proofs really are 07/07 17:37 and, more, you should be able to talk _about_ general recursive functions in proofs, just not run them 07/07 17:40 we have a story about how we decide which terms are good proofs, but predictably it's still in flux 07/07 17:41 that would be nice 07/07 17:42 I've just decided all that can be investigated independently of using some tool to write interesting programs 07/07 17:42 it does mean you need to take some care when claiming a proof is indeed a proof though 07/07 17:43 --- Day changed Fri Jul 09 2010 * benc___ playing trying to implement something like bubblesort 09/07 07:36 I have this: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27195#a27195 09/07 07:36 it doesn't terminate according to the termination checker, but I think it does because n is decreasing? 09/07 07:37 so what am I missing? 09/07 07:37 onepass itself doesn't terminate? 09/07 07:38 tats the error i get 09/07 07:39 |Termination checking failed for the following functions: onepass. 09/07 07:39 is what agda tells me 09/07 07:39 if i compile this way: $agda -c b.agda -i . -i lib-0.3/src --no-termination-check 09/07 07:39 then on my single example case, it behaves as I would expect it to. 09/07 07:40$ agda --version 09/07 07:40 Agda version 2.2.6 09/07 07:40 If 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 It sees that as growing, despite the fact that it's overall shrinking. 09/07 07:45 does --termination-depth=2 mean it unfolds the call on onepass (suc n)? 09/07 07:47 where is --termination-depth? mine doesn't have one? 09/07 07:47 Or not. I wrote some other stuff and it isn't a problem... 09/07 07:48 Oh, I bet I know the problem. 09/07 07:48 When you use the 'with' it gets expanded into an auxiliary function, and that confuses the checker. 09/07 07:48 Yes, the with is an important part. 09/07 07:49 So, the with combined with the sort-of-growing recursive call is enough to confuse the checker. 09/07 07:50 any obvious rewrites to make it happy? 09/07 07:52 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 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27195#a27198 09/07 07:55 ok 09/07 07:56 i think thats how I would have implemented it in haskell ;) 09/07 07:56 napping: 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 So 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 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 member 09/07 08:00 * benc___ not really sure 09/07 08:00 and then ultimately use that to prove if you call onepass a bunch, the output list is ordered 09/07 08:01 weird to have that if_then_else_ that is not the same as the one in Data.Boolean 09/07 08:11 Data.Bool 09/07 08:11 shoudl I put an entry in the agda bug tracker about that with termination thing not working? 09/07 08:36 hoky moly 09/07 21:29 Lots more people on here than last I checked 09/07 21:29 all the cool kids code in agda 09/07 21:30 apparently :) 09/07 21:32 the uncool kids lurk and watch the cool kids hoping to one day be as cool as them 09/07 21:34 Is there a paper on how guardedness and recursion are calculated for agda? 09/07 23:01 The guardedness condition in agda appears to be much more fluid than in Coq 09/07 23:01 It's type-checking a lot more of my code. 09/07 23:01 I don't think there's a paper. 09/07 23:10 It'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 The ability to reuse constructor names for different types is handy 10/07 09:16 --- Day changed Sun Jul 11 2010 how would you define surreal numbers as an inductive-recursive type? 11/07 01:34 does 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 In 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 I'm having difficulty finding the solution. 11/07 10:36 jacobian: you've to use induction for that one, iirc 11/07 11:01 i.e. write a recursive function 11/07 11:02 yes, well I understood that much :) 11/07 11:11 i 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 else 11/07 11:15 right, I think I had missed that.  Here tabulate pattern matches on an implicit argument. 11/07 11:19 hello, 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 or even, does it make sense? :) 11/07 11:38 well, that's not true for every P 11/07 11:40 e.g. with "P _ = \top" you've P x == P y for every choice of x and y 11/07 11:41 ah, thanks, that example shows it very well 11/07 11:41 if that was provable it'd mean that every predicate is injective, i think 11/07 11:42 yeah.  Maybe I can prove it for the particular P I want then 11/07 11:42 thank you Saizan 11/07 11:43 np 11/07 11:43 I'm trying to use lhs2TeX, but I'm getting an error: lhs2TeX: Enum.toEnum{Word8}: ... 11/07 11:46 I assume that it's complaining about my use of utf8? 11/07 11:46 I'm using lhs2TeX 1.15 11/07 11:49 yay!  I proved it for the case I wanted and everything's good :) 11/07 12:08 Hmm, 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 Changing the locale to C resulted in a different error :) 11/07 13:06 --- Day changed Mon Jul 12 2010 Anyone use unicode fonts with lhs2TeX in agda? 12/07 13:31 s/fonts/characters/ 12/07 13:32 --- Day changed Tue Jul 13 2010 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 runtime 13/07 11:39 jacobian: There's a problem with lhs2TeX 1.15. Try 1.14 13/07 11:46 ...or this patch: http://patch-tracker.debian.org/patch/series/dl/lhs2tex/1.15-3/no-utf8-string.patch which I think might fix it 13/07 11:47 Laney: Thanks 13/07 12:39 Can 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 jacobian: 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 jacobian: regarding '@'. yes, @foo@ is inline-verbatim, similar to |foo| being inline-code. 13/07 14:51 jacobian: you can escape: @@ and || 13/07 14:51 ah, thanks 13/07 15:27 As 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 I can definitely give you an example though 13/07 15:28 It'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 http://coq.pastebin.com/c4NMxKp7 13/07 15:32 http://coq.pastebin.com/ihvAsZkn 13/07 15:33 jacobian: thanks very much. 13/07 17:18 --- Day changed Wed Jul 14 2010 Awright, how do I get started with Agda? 14/07 05:59 What do you mean? Installing stuff, or tutorials? 14/07 06:00 I'm using the ubuntu packages, what do I do after that? 14/07 06:00 Huh, there are ubuntu packages? I'd never even noticed. 14/07 06:01 OK, I can use the cabal package instead... 14/07 06:01 I guess it installed emacs and everything? 14/07 06:01 I dunno, I live in emasc. 14/07 06:01 I'm using ERC Version 5.3 with GNU Emacs 23.1.50.1 (x86_64-pc-linux-gnu, GTK+ Version 2.18.0, multi-tty) of 2009-09-27. 14/07 06:01 When you open up a .agda file in emacs, does it have an Agda menu and such? 14/07 06:02 Um, pulling the agda mode out of the cabal package now... 14/07 06:03 There seems to be an ubuntu package for agda-mode, too. 14/07 06:03 Eh, I'll stick with cabal, I'm sure it's more recent. 14/07 06:03 Anyhow, 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.TypesSummerSchool2007 14/07 06:05 Ok, where do I get a demo agda file? 14/07 06:05 Click on the lectures link, and start reading at Basics. Each file tells you what file to read next, I think. 14/07 06:05 And there are exercises. 14/07 06:05 spiffy! 14/07 06:06 Huh, looks like Haskell. 14/07 06:06 The wiki probably has something on using the emacs mode, too... 14/07 06:06 The main points you should be able to figure out from the menu I think, though. 14/07 06:06 How do I type the 1 ? 14/07 06:06 You 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 ooh, epigram style! 14/07 06:07 Unicode input starts by typing \ 14/07 06:07 \_1 is subscript 1. 14/07 06:07 aha 14/07 06:07 Most stuff can be typed by its latex name, although there are some abbreviations for stuff. 14/07 06:08 \bn instead of \bbb{N} 14/07 06:08 Is there any shortcut for the subnumber stuff? 14/07 06:10 \_N is all I know of. 14/07 06:10 ok 14/07 06:10 Once 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 C-u C-x = I think? 14/07 06:11 There's an alternate way of typing stuff that I don't use, too. 14/07 06:11 Like typing 'andd' automatically turns into a unicode conjunction symbol. 14/07 06:12 http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Documentation 14/07 06:12 Some of the stuff on that page will probably be useful. 14/07 06:12 Cool 14/07 06:13 I'm transcribing the Basics still, I'll see where that gets me. 14/07 06:13 Ooh, got my first type error. Was surprisingly friendly! 14/07 06:15 That's good. 14/07 06:18 Wait until you get something like "_87 != _93". 14/07 06:18 heh 14/07 06:18 I did get a bang and fish combo of some sort 14/07 06:18 So, what exactly does id : { A : Set } mean? 14/07 21:02 {} in type signatures is for implicit arguments. 14/07 21:05 oh 14/07 21:05 Which means you don't have to write them in when you're using the function. 14/07 21:05 um, ok 14/07 21:06 So id :: {A : Set} -> A -> A can be used like "id x" instead of "id A x". 14/07 21:06 And Agda will try to figure out what the A argument should be. 14/07 21:06 Which should be pretty easy in this case, because it's whatever the type of x is. 14/07 21:06 You can specify implicit arguments manually, though "id {A} x". 14/07 21:07 Should the last example in Basics.agda typecheck? 14/07 21:07 id6? 14/07 21:08 yup 14/07 21:08 Yes, I think so. 14/07 21:08 Oh yes, and if there's an explicit argument that you want agda to infer, you can write _. 14/07 21:09 Aha, \ is not the same as _ 14/07 21:10 yes, it is easy to make mistakes like that 14/07 21:12 also note that \:: is not the same as :: (useful for lists - \:: is often cons) 14/07 21:12 and \: is not the same as :  (since : is reserved, people often use \: when doing PL stuff) 14/07 21:12 I'm using gnumacs, is there some way to make the differences explicit? 14/07 21:14 not to my knowledge, but they do look a little different 14/07 21:15 it's just easy to get caught off-guard at first 14/07 21:15 \: is more grey than : in my font, as I recall. 14/07 21:15 underscores in type signatures represent operators? 14/07 21:16 I'm looking at Datatypes.agda 14/07 21:16 specifically _+_ 14/07 21:16 yes 14/07 21:16 Yes. Underscores go where arguments would go. 14/07 21:16 that makes + infix 14/07 21:16 Ah, interesting% 14/07 21:16 So, if_then_else_ 14/07 21:16 multiples allowed? _%__ ? 14/07 21:17 I don't think so. 14/07 21:17 though, in that case you don't need them 14/07 21:17 since foo_ is just foo 14/07 21:17 I mean, if foo is a function 14/07 21:17 Well, foo_ is useful when you don't want foo to bind as tightly as a function. 14/07 21:18 Ah, ops don't bind as tightly as functions? 14/07 21:18 they can be adjusted 14/07 21:18 I think the syntax is something like 14/07 21:19 Well, they never bind as tightly as functions. 14/07 21:19 infixl 6 _+_ 14/07 21:19 Function application has maximum precedence, like Haskell. 14/07 21:19 ah 14/07 21:20 So, why does "if false then x else y = y" work in Bool.agda, but won't typecheck in Datatypes.agda? 14/07 21:35 Oh wait, now it does work% 14/07 21:35 * shapr is confused 14/07 21:36 How do I get the upside down v from CurryHoward.agda? 14/07 22:53 Is it just a caret? 14/07 22:54 doesn't look like it't just a caret 14/07 22:54 I don't know, but: 14/07 22:54 put your cursor over it and enter 14/07 22:54 C-u C-x = 14/07 22:54 and it will tell you what \ shortcuts work 14/07 22:54 this is a good combination to remember, I think it's on the wiki on the "unicode input" page 14/07 22:55 \wedge or \intersection or \and 14/07 22:55 hmm 14/07 22:56 nifty 14/07 22:56 I'm getting a Parse Error from \all in CurryHoward.agda 14/07 23:04 I tried copying and pasting from the online version, same error. 14/07 23:05 Any ideas? 14/07 23:05 I also can't get notNotEM to type check, it gets upset about "\p -> f (inl p)" not being a function type, but instead being P 14/07 23:13 * shapr is lost 14/07 23:13 --- Day changed Thu Jul 15 2010 shapr: where do I get a copy of CurryHoward.agda? 15/07 00:14 \forall is a reserved character in agda, so it's not terribly surprising that it might cause parse errors 15/07 00:14 oh, he left 15/07 00:15 does Agda use normalization by evaluation? and anyhow, is the interpretation of a function shared between its uses? 15/07 15:13 Saizan: I don't think it does 15/07 17:48 in ulf's thesis, he gives a direct operational semantics 15/07 17:48 I'm not a NBE expert, though 15/07 17:51 The stuff in src/core looks like NBE. 15/07 18:53 dolio: which parts? 15/07 19:00 Exp and Val 15/07 19:02 That's probably the wrong stuff, though. 15/07 19:05 well, I know hardly anything about nbe, but can you explain?  This looks like a straightforward implementation of a boring big step operational semantics to me 15/07 19:05 Its only constructor for universes is "ESet" or "Set" respectively. 15/07 19:05 yes, this is definitely not what is running under the hood in agda, but I'm still curious 15/07 19:06 Normalization-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 is 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 values 15/07 19:08 I thought nbe described a strategy where you interpret the exps into some some other (maybe set theoretic) domain and then read back out values 15/07 19:08 You 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 Then you write 'eval : Syn -> Sem' and 'reflect : Sem -> Syn'. 15/07 19:09 And 'normalize : Syn -> Syn ; normalize = reflect . eval'. 15/07 19:09 Well, I suppose you could use other sets for your semantics, too. 15/07 19:13 The two term representations won't necessarily look alike. 15/07 19:14 For instance, for a combinator calculus, you might have: 15/07 19:14 data Syn = S | K | _\$_ 15/07 19:14 data Sem = K0 | K1 Sem | S0 | S1 Sem | S2 Sem Sem 15/07 19:15 interesting 15/07 19:16 I have seen this technique, but never thought of it as nbe 15/07 19:17 the src/core stuff seems to be missing the "reflect" part of this, though 15/07 19:19 Yeah. 15/07 19:19 I'm not sure what that stuff is. 15/07 19:20 hello 15/07 23:06 trying and failing to the build the standard library 15/07 23:07 using 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 You'll need an agda newer than what you've got. 15/07 23:08 using agda-2.2.7 it appears to diverge and eat memory after compiling Relation.Binary.HeterogeneousEquality 15/07 23:09 and the release-notes for the library seem to say i should use 2.2.6... 15/07 23:09 with 2.2.7, i let it run for >10 mins and it paged out the rest of my apps :/ 15/07 23:10 (and by 2.2.7 i mean the latest darcs for agda) 15/07 23:10 Heh. 15/07 23:10 any ideas? 15/07 23:10 I wouldn't have expected that for just HeterogeneousEquality. 15/07 23:10 Maybe there's a way you can get a back-dated version of the library that will work with 2.2.6 15/07 23:11 http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary 15/07 23:11 oh, i see, duh. version 0.3 is different from darcs head 15/07 23:12 that what the release-notes reported to work with 2.2.6 15/07 23:13 ok, i'll try that 15/07 23:13 --- Day changed Fri Jul 16 2010 if 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 danb: e.g. "_∈Val {t} tm" 16/07 18:39 M ∈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 Saizan: oh, yeah, ok. should have thought of that. is there any way to combine {t} and M ∈Val ? 16/07 18:40 not that i know of 16/07 18:40 ok 16/07 18:40 thx 16/07 18:40 np :) 16/07 18:40 Probably not much help but (v ∈) {t} tm would also work. 16/07 18:56 --- Day changed Wed Jul 21 2010 Hi. 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 secs 21/07 14:53 * Saizan might be able to typecheck Everything.agda with his new shiny 1GB of ram 21/07 18:06 I doubt it. 21/07 18:07 Unless that's 1GB + a bunch else you already had. 21/07 18:07 for a total of 3GB 21/07 18:07 Oh, well, I can't say for sure, then. 21/07 18:07 I still doubt it, though. 21/07 18:09 heap overflow, in fact 21/07 18:29 * Saizan iterates 21/07 18:30 yay, it completed in two runs 21/07 18:34 --- Day changed Thu Jul 22 2010 i'm trying to prove if n <= m, n != m that n < m 22/07 10:20 http://pastebin.com/BH5zrXne 22/07 10:20 like that 22/07 10:20 but I'm stuck there 22/07 10:20 i have a case that is a contradiction, but how do I make agda see the contradiction? 22/07 10:20 does neq refl give you a proof of something uninhabited? 22/07 10:23 ⊥-elim might help (from Data.Empty), if you can figure out how to type it in 22/07 10:26 yeah 22/07 10:33 reload that URL to see how i just used it 22/07 10:33 elim (neq (refl)) 22/07 10:34 oh wait pastebin doesn't work that way. anyway   bot-elim neq refl worked just fine 22/07 10:35 good; saves mucking about with helper functions and () patterns 22/07 10:37 onwards with my epic proving-bubblesort voyage 22/07 10:39 hola 22/07 22:21 hi 22/07 22:21 hello 22/07 23:26 i have an ADT with eight constructors, and i want to use Decidable equality for it 22/07 23:27 currently i've written a 64-clause _≟_ function... 22/07 23:27 is there a better solution? 22/07 23:27 Probably not, unfortunately. 22/07 23:29 :( 22/07 23:29 it's a pretty ridiculous function 22/07 23:29 Yes. 22/07 23:29 I don't think there's any way to do a "the rest of these should be absurd" thing, though. 22/07 23:30 it'd be really great if overlapping patterns could be smarter 22/07 23:31 dolio: i was hoping for compiler support, like "deriving Eq" in haskell 22/07 23:37 but smarter patterns would help the problem a lot, as well 22/07 23:38 time something generic happened; how are Agda's strings these days? 22/07 23:41 maybe someone should invent template agda? :P 22/07 23:42 it's called Agda 22/07 23:42 * benmachine is quiet again 22/07 23:43 another 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#a27968 22/07 23:45 pigworker: strings? 22/07 23:46 (look for the postulates) 22/07 23:46 is there a better way to do that? 22/07 23:46 Seriously, 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 Saizan: Can we compute a de Bruijn index in Fin n from a string and a Vec n of strings? 22/07 23:47 jdanbrown: 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 pigworker: i'd think so, Data.String.String has decidable equality 22/07 23:51 the current quote/quoteGoal won't help in giving us a description of an ADT though, right? 22/07 23:51 Saizan: ok, let me try that and see... 22/07 23:52 don't think so, but it might be possible to construct a modelled type we can cope with 22/07 23:53 btw, i'm a bit puzzled by quoteGoal giving you just the term and not the whole closure 22/07 23:55 --- Day changed Fri Jul 23 2010 for decidable equality a putative Desc would have to provide the decision procedure for the abstract types it mentions 23/07 00:14 yes, it would say "if the pieces are decidable, the whole is decidable" 23/07 00:15 is there anything like this in the epigram repo?:) 23/07 00:19 Saizan: 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 Saizan: (added the type error at the bottom of the hpaste—reload if necessary) 23/07 00:20 Saizan: decidable equality for the first-order fragment of IDesc? shouldn't be too tricky; hasn't been done 23/07 00:21 jdanbrown: C and D are variables, not constructors, right? 23/07 00:21 Saizan: right 23/07 00:21 Saizan: fancy ⏐ is the constructor 23/07 00:21 Saizan: maybe i should be quantifying instead of using the bound C, D, s, and t? 23/07 00:23 jdanbrown: quantifying would make it work 23/07 00:23 jdanbrown: otherwise you can use with C ⏐ s 23/07 00:24 f eq with C ⏐ s; ... | x = ? and then C-c C-c eq 23/07 00:25 hmm, same error when i try quantifying (updated hpaste) 23/07 00:28 let me try 'with' 23/07 00:28 * Saizan is a bit rusty 23/07 00:30 err, messed up my primes. updated. (still same error) 23/07 00:33 back to 'with'... 23/07 00:34 Saizan: no luck with 'with', either (http://hpaste.org/fastcgi/hpaste.fcgi/view?id=27968#a27975) 23/07 00:39 still refuses to unify the indices 23/07 00:39 my idea might just be flawed :) 23/07 00:40 :/ 23/07 00:40 Saizan: well thanks for trying :) 23/07 00:40 spent 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 lemma : ∀ {t1 t2 s1 s2} -> t1 => s1 ≡ t2 => s2 -> s1 ≡ s2 23/07 00:44 lemma refl = refl 23/07 00:44 you can write that though. 23/07 00:44 which, modulo constructor name, would be able to substitute your "cong un⏐₁" 23/07 00:44 hmm 23/07 00:44 i believe it's called an inversion lemma, it is really just a witness of the injectivity of the constructor 23/07 00:46 yeah, that makes sense in concept 23/07 00:47 can't make that lemma check either 23/07 00:48 also tried the --invertible-type-constructors flag ;)—but still no luck 23/07 00:49 foo : ∀ {C s D t} → C ⏐ s ≡ D ⏐ t → s ≡ t 23/07 00:49 foo refl = refl 23/07 00:49 what's the definition of Com ? 23/07 00:50 it's an existential: 23/07 00:50 Com : Set 23/07 00:50 Com = ∃ λ D → (Fun D ₀ (ι "X") ⟶̣̇  ι "X") × 23/07 00:50 (Fun D ₀ (ι "X") ⟶̣̇  D ₀ (D ₀ (ι "X"))) 23/07 00:50 'Com' for comonad 23/07 00:51 (ignore the funny dots after the long arrow) 23/07 00:51 so it's a Σ type 23/07 00:52 it shouldn't matter anyhow.. but i've no idea how foo could fail to typecheck 23/07 00:52 oops, it does matter 23/07 00:53 foo : ∀ {s t s′ t′} → s + t ≡ s′ + t′ → s ≡ s′ 23/07 00:53 foo refl = refl 23/07 00:53 that works 23/07 00:53 looks like i started with the hard case :X 23/07 00:53 heh 23/07 00:54 alright, let me see how far i can get with this 23/07 00:54 i'll defer the sigma cases for now 23/07 00:54 thanks Saizan! 23/07 00:54 np :) 23/07 00:55 jdanbrown: 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 hmm 23/07 01:16 pigworker: just updated with the latest version 23/07 01:18 Boy, even Data.Fin.Props is hard work, apparently. 23/07 01:18 pigworker: 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 method 23/07 01:19 pigworker: so you're suggesting i try matching (yes refl) instead of _? let me see... 23/07 01:19 yes, and add the .pattern ftw 23/07 01:19 k 23/07 01:20 hmm, but that's still independent of the lemma ⏐₂-inj : ∀ {C s D t} → C ⏐ s ≡ D ⏐ t → s ≡ t , right? 23/07 01:22 ok, so let me try this lemma: ⏐₂-inj : ∀ {C s t} → C ⏐ s ≡ C ⏐ t → s ≡ t 23/07 01:23 still no go 23/07 01:23 these lemmas are the uphill struggle lemmas 23/07 01:23 hmm 23/07 01:23 what do you suggest instead? 23/07 01:23 my buddies and I wrote a paper about this in 2004 "A few constructions on constructors" 23/07 01:23 there'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 tedious 23/07 01:25 ok 23/07 01:25 still 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 It is disturbing that dependent pattern matching isn't cutting it. 23/07 01:27 and 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 defined 23/07 01:28 But, 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 and 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 shouldn't make a difference 23/07 01:32 gotta go fall over; it's late in Glasgow 23/07 01:39 Well, I got decidable equality via isomorphism with finite sets. 23/07 01:47 Takes only 33 lines for a 4-constructor type instead of... 16. 23/07 01:47 heh 23/07 01:48 could you have gotten by with injection instead of isomorphism? 23/07 01:48 I tried injectivity first, but then I realized that you'd have to do all the cases to prove injectivity. 23/07 01:49 So you might as well just prove decidable equality directly. 23/07 01:49 ah, ok 23/07 01:49 iso is easier? do you just directly prove the equalities fg = 1 and gf = 1? 23/07 01:49 Yes. 23/07 01:50 So you match once per constructor per direction. 23/07 01:50 And once per constructor for each of the two functions. 23/07 01:51 So I guess it's 4*n lines instead of n*n. 23/07 01:51 Plus some extra cruft. 23/07 01:51 could you save half the work and only prove fg = 1? that should establish injectivity 23/07 01:52 dolio: i'll consider that 23/07 01:56 gtg 23/07 01:56 jdanbrown: 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.html 23/07 05:04 Lets you use naturals, too, which is less of a hassle. 23/07 05:04 dolio: nice! 23/07 05:04 '3' is so much nicer to type than 'suc (suc (suc zero))'. 23/07 05:06 this is great. i will use this and cut out most of my ugly code :) 23/07 05:08 programming with math is so much fun 23/07 05:08 Yes. :) 23/07 05:08 dolio: you should update your darcs ;) 23/07 05:13 i still see the IsoDec module 23/07 05:13 Oops, done. 23/07 05:18 thanks! 23/07 05:22 after i finish doing this the hard way i'll start over and see how much more easily i can do it with a retract 23/07 05:22 dolio: 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 dolio: let me know what you think 23/07 10:02 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 discernable 23/07 13:15 * benc___ using os x terminal 23/07 13:15 I 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.VisibilityAndEvaluation 23/07 15:15 But 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 anyone up for a small code review? ;) 23/07 21:28 i've coded up a simple model of STLC where i'm trying to make agda automatically construct proofs that variables are in scope 23/07 21:29 http://acandystore.org/agda/Lambda.html 23/07 21:29 both 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 does it work if you give the s argument to App explicitly? 23/07 21:35 ah, that's a good question 23/07 21:36 (_those_ metas!) 23/07 21:36 pigworker: 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.html 23/07 21:37 checking it out 23/07 21:38 (it might very well be a special case of the paper you pointed me to yesterday) 23/07 21:39 with a rose-tree it would have reminded me of prolog even more :) 23/07 21:39 a rose tree would probably be easier to code against—notice that my example is all 0- and 2-ary :/ 23/07 21:42 I see: a kind of dump-to-LISP strategy 23/07 21:43 should be an easy change 23/07 21:43 yeah 23/07 21:43 3n easy clauses instead of n^2 hard ones 23/07 21:43 it 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 least 23/07 21:45 As long as you have an easy time picking dummy values for the projection, you should be laughing. 23/07 21:46 why laughing? 23/07 21:46 I 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 Things get trickier if you want to play this game for datatypes which enforce stronger invariants. 23/07 21:50 hmm, ok 23/07 21:53 Saizan: yes, explicitly giving {s = o) to App works 23/07 21:56 But there ought to be a good generic programming solution (at the cost of using encoded, rather than directly declared data). 23/07 21:56 If only there were a language where directly declared data *was* encoded. :) 23/07 21:59 dolio: I'd never have thought of that! 23/07 22:00 have other systems solved this problem? it seems like it should be basic (though i'm sure that's naive) 23/07 22:01 Epigram 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 We 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 Decent sugar for finite enumerations with named elements would help a lot. 23/07 22:08 --- Day changed Sat Jul 24 2010 anyone read Knuths book Surreal Numbers? 24/07 17:26 --- Day changed Sun Jul 25 2010 conways numbers are defined like this: 25/07 10:26 {A|B} 25/07 10:26 and there is no a in A, b in B such that b <= a 25/07 10:27 that relation is defined like {X_L|X_R} <= {Y_L|Y_R} 25/07 10:28 :<=> 25/07 10:28 there is no x in X_L such that {Y_L|Y_R} <= x 25/07 10:29 and there is no y in Y_R such that y <= {X_L|X_R} 25/07 10:29 ------------------------- 25/07 10:29 so if you iterate this you quickly build up natural numbers and fractions 25/07 10:29 but if you use transfinite induction you get infinitesimals and infinite numbers, as well as trancendentals 25/07 10:30 So how would you define this in agda? Clearly it is inductive-recursive 25/07 10:30 Deciding on an {A|B} is a big part of the problem. 25/07 10:33 what do you mean 25/07 10:34 How do you represent A and B? 25/07 10:34 They're supposed to be sets. 25/07 10:35 they are what we are defining 25/07 10:35 oh wait sorry I get hwat you mean 25/07 10:35 I guess you could just use multisets and not worry about it. 25/07 10:35 they are *sets of* what's being defined 25/07 10:35 and we have no notion of a set in agda 25/07 10:35 But 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 what could I be? 25/07 10:38 We have things like sets, but they don't behave quite the way set-theoretic sets do. 25/07 10:38 realy?? 25/07 10:39 Types are like sets. 25/07 10:39 oh yeah but Sigma would be negative here 25/07 10:39 You can mimic set-theoretic sets, too. 25/07 10:41 But they can be lacking, too. 25/07 10:41 yeah short of embedding ZFC I have no idea how t o d o this 25/07 10:41 There's no good way to get powerset in Agda. 25/07 10:41 Which means your sets are limited to being a lot smaller. 25/07 10:42 I was wondering about indexing the type 25/07 10:42 like  Surreal K : * 25/07 10:42 so you could have  Surreal (Surreal K) : * 25/07 10:42 etc 25/07 10:42 but it doesn't seem to play nice 25/07 10:43 I 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 so it does not appear there is any way to do this 25/07 13:56 sets seem to be able to be any size 25/07 13:57 --- Day changed Mon Jul 26 2010 omg I've been itching to use agda for the past month 26/07 17:43 what's stopping you? 26/07 17:44 not having a computer for the past month and a bit 26/07 17:44 but now I do again! 26/07 17:45 muahaha 26/07 17:45 oh, welcome back 26/07 17:45 :) 26/07 17:45 thanks :) 26/07 17:45 in that month and a bit I've... lurked 26/07 17:45 and still done no agda whatsoever 26/07 17:45 good times. 26/07 17:45 :o 26/07 17:45 why not?!? 26/07 17:45 mostly because I have to either learn emacs or make it pretend to be vim :P 26/07 17:46 lol 26/07 17:46 people make too much of a deal about that 26/07 17:46 it's not that bad 26/07 17:46 I only use emacs for agda 26/07 17:46 yeah but it takes round tuits 26/07 17:46 * benmachine wonders if this is a vaguely common expression 26/07 17:47 :o 26/07 17:48 * copumpkin hasn't heard it 26/07 17:48 probably not then :P 26/07 17:49 basically, the idea is I won't do it until I get a round tuit 26/07 17:49 homophony pun 26/07 17:49 and now my goal is suc i == zero 26/07 18:08 mmm 26/07 18:08 a pumpkin! 26/07 18:49 Yes! 26/07 18:49 A Saizan! 26/07 18:49 :D 26/07 18:49 how's it going? 26/07 18:51 not bad, but coding more haskell than agda lately 26/07 18:51 aha 26/07 18:52 it feels dangerous, non-exhaustive pattern matches everywhere! 26/07 18:52 you?:) 26/07 18:52 oh no! 26/07 18:52 been traveling for the last month and a bit 26/07 18:52 so no agda or haskell! 26/07 18:53 back to US now? 26/07 18:53 nah, italy 26/07 18:55 why would adding a with clause but not pattern matching against its result stop the code from typechecking? 26/07 19:30 so f x = ? works fine, f x with g x \n ... | q = ? doesn't 26/07 19:30 where g x has a valid type 26/07 19:30 what kind of type error do you get? 26/07 19:34 (or perhaps just paste your code) 26/07 19:35 suc max != w of type Fin (suc (suc n)) 26/07 19:41 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28244#a28244 26/07 19:42 if I remove the with max {suc n} it doesn't complain 26/07 19:42 what if you write out "lemma₀ {suc n}" instead of ... ? 26/07 19:43 same 26/07 19:44 is there a way to see how with gets desugared, btw? 26/07 19:45 nope, but I know it involves a w! 26/07 19:45 heh 26/07 19:46 seems like a bug to me 26/07 19:46 well, more accurately, I don't understand what is happening either :) 26/07 19:47 I'd report it 26/07 19:47 it does seem like it shouldn't care about the with if it's got a valid type and I'm not pattern matching 26/07 19:49 it's probably substituing "max {suc n}" to q in the goal 26/07 19:50 I didn't see any "max {suc n}"s in the goal, though 26/07 19:50 well, the "n" in the type becomes "suc n" in that branch 26/07 19:51 yeah, you are right 26/07 19:52 copumpkin: s/| max {suc n}/| suc (max {n})/  ? 26/07 19:52 more 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 but it doesn't seem that way 26/07 19:52 Saizan: that turns yellow but works 26/07 19:52 (using with rather than |) 26/07 19:53 oh, I'm reading wrong completely... hmm 26/07 19:53 it seems there's some desync on how the patterns should affect the goal.. 26/07 19:55 is http://code.google.com/p/agda/issues/list down? 26/07 19:56 seems so 26/07 19:57 the 'with' stuff kinda sounds like problems i had with my bubblesort playing 26/07 20:03 that was not termination checking in some cases 26/07 20:03 http://www.blogger.com/post-edit.g?blogID=4983265076111025145&postID=8855595265271949166 26/07 20:04 heh not that 26/07 20:04 http://benctechnicalblog.blogspot.com/2010/07/branching-on-left-vs-branching-on-right.html 26/07 20:06 benc___: what's the disadvantage of the if version? 26/07 20:22 saizan: i had the impression that case based proofs didn't ork so well with it 26/07 21:10 maybe they do - i didn't play with that any more 26/07 21:10 it's just a function 26/07 21:10 if you're ignoring the results of your decidable yes/no thingy then it should be equivalent 26/07 21:11 i think they'd work just the same 26/07 21:11 well yes 26/07 21:11 by results I mean the attached proofs 26/07 21:11 thats what I thought 26/07 21:11 but they don't (termination-check-wise) 26/07 21:11 the if is the one that termination-checks, right? 26/07 21:12 copumpkin: yeah some of the stuf fi did later that I haven't writen about uses the resulting proofs from the decidables 26/07 21:12 saizan: 'if' termination chesk adn 'with' doesn't 26/07 21:12 i'll add the if definition ina comment 26/07 21:12 and proofs about onepass written with if shouldn't be significantly different from ones about onepass with with 26/07 21:13 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 yeah, 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 branches 26/07 21:19 ok 26/07 21:20 maybe i'll play with that some 26/07 21:21 * benc___ doesn't really grok why one works and the other doesn't, though 26/07 21:21 I'm kind of confused about my proof here 26/07 21:21 maybe I've just been away from agda for too long 26/07 21:21 lemma₀ {suc n} with succ (max {suc n}) 26/07 21:22 ...            | k = {!!} 26/07 21:22 Goal: k ≡ zero 26/07 21:22 lemma₀ : ∀ {n} → succ (max {n}) ≡ zero 26/07 21:22 the overall goal makes sense to me, but the k == zero goal does not 26/07 21:23 because if I pattern match on k I get zero == zero and suc q == zero 26/07 21:23 and the latter is obviously false 26/07 21:23 not enough obvious, otherwise you could have written lemma₀ {suc n} = refl 26/07 21:25 i think you want to recurse on n 26/07 21:25 oh I mean, it's asking me to prove something that's false 26/07 21:25 ?0 : zero ≡ zero 26/07 21:26 ?1 : suc i ≡ zero 26/07 21:26 given (lemma₀ {n}) you should be able to prove lemma₀ {suc n}, i think 26/07 21:26 I thought so but couldn't get it 26/07 21:29 so I was trying something that seemed more direct 26/07 21:29 (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 there's a "with-\==" for that in the stdlib, iirc 26/07 21:30 Saizan: but I don't really want to prove that case is impossible 26/07 21:50 it's disturbing that it is :P 26/07 21:50 disturbing that it allows that case at all? 26/07 21:51 disturbing that it's not an impossible case, and it leads to an impossible goal 26/07 21:51 it's not one of those absurd pattern situations 26/07 21:51 or _|_-elim 26/07 21:51 it sort of is an impossible case, I guess, but I can only prove that by recursion 26/07 21:52 and I haven't figured out how to convince it of that yet 26/07 21:52 not sure how to explain 26/07 21:54 i'd try to prove "view max == vmax" first 26/07 21:54 okay will try that :) 26/07 21:56 or maybe that a value of EmbMax is completely determined by the indices 26/07 21:56 hm, how so? 26/07 22:33 I can sort of see what you mean, I think 26/07 22:40 i'm not sure if it's true, but the type of that would be forall {n f} (p q : EmbMax {n} f) -> p == q 26/07 22:43 An internal error has occurred. Please report this as a bug. 26/07 22:43 Location of the error: src/full/Agda/Auto/Convert.hs:654 26/07 22:43 lol 26/07 22:43 (unrelated to what you just wrote) 26/07 22:43 --- Day changed Tue Jul 27 2010 benmachine: I used to have a round tuit. 27/07 00:56 dolio: yeah, I've seen them on sale 27/07 00:57 I think I got mine for free from a home show. 27/07 00:57 heh 27/07 00:57 I want a "HOWTO get your complicated patterns to be accepted by agda" 27/07 17:56 it's called --type-in-type 27/07 18:26 ;( 27/07 18:26 :P 27/07 18:27 So I herd you like types... 27/07 18:42 no? 27/07 19:11 I see 27/07 19:11 Cannot pattern match on constructor vemb, since the inferred 27/07 19:11 yes 27/07 19:11 indices [{suc n'}, emb i] cannot be unified with the expected 27/07 19:11 indices [{n}, max] for some y, i, n', n 27/07 19:11 when checking that the expression ? has type vmax ≡ q 27/07 19:11 maybe more informative is the wrong phrase :) 27/07 19:11 I sort of understand what it's saying but I don't know how to appease it 27/07 19:11 an error I've seen before is more accurate 27/07 19:11 you can look at the mailing list to see what they told me to do when I got a similar error in a different situation 27/07 19:12 I would just describe it, but it's complicated 27/07 19:12 what's the name of the thread? 27/07 19:12 "equality reasoning and contradictory type indices" 27/07 19:13 basically, I think we should write a lemma using "where" which just renames p but takes as a hypothesis that it is equal to vmax 27/07 19:15 then we should be able to split on q, and reason by transitivity in the non-contradictory case 27/07 19:15 ugh, this doesn't work though.  We probably also need to abstract over p's index 27/07 19:17 and q 27/07 19:17 well, that's not right either, but I'll stop talking now and just make it work first :) 27/07 19:17 lol 27/07 19:17 made it work going trough heterogeneous equality 27/07 19:23 yes, I had to as well, sadly 27/07 19:24 too many levels of indices 27/07 19:24 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28285 27/07 19:29 yeah, nice.  I'm still trying to find a way with only homogeneous equality, but it looks like maybe you win 27/07 19:31 ccasin, why? 27/07 19:31 there is an extra level of telescoping here, and it's too much for the trick I mentioned 27/07 19:32 I mean, why the preference for homogeneous equality - is it philosophical? 27/07 19:32 no, the puzzle is just more fun that what I'm supposed to be working on 27/07 19:32 lol 27/07 19:32 perhaps you can find a theorem about Fin which is equivalent to K 27/07 19:33 that would be interesting 27/07 19:33 it shouldn't be too hard to formulate one about what you can prove by pattern matching on Fin 27/07 19:34 not that I'm volunteering 27/07 19:35 :) 27/07 19:35 yeah but I did everything up to Fin injectivity by pigeonhole argument without K 27/07 19:35 hmm 27/07 19:36 so it's not a trivial thin 27/07 19:36 thing 27/07 19:36 I think proving (Fin 2) /= Bool should need K 27/07 19:38 though that's not just about Fin 27/07 19:38 you can't even prove that with K afaict 27/07 19:38 well, I can prove it in agda 27/07 19:38 are you sure?? 27/07 19:38 I think... 27/07 19:38 I've done something similar.  Let me see 27/07 19:39 definitely want to see the proof if you write this 27/07 19:39 the trick should be to define a proposition P which is true of a set just when there is an element of the set that == True 27/07 19:39 agda's typechecking of () patterns will be strong enough to see that P doesn't hold of (Fin 2) 27/07 19:40 At least, I think so.  Let me try 27/07 19:40 soupdragon: here you are 27/07 19:51 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28286#a28286 27/07 19:51 is this surprising? 27/07 19:51 The only evidence that I have of needing K for this is that I was unable to do it in coq 27/07 19:52 not a principled reason 27/07 19:52 very 27/07 19:52 I am baffled 27/07 19:52 I wish you'd done this without importing anything 27/07 19:52 it shouldn't be too hard 27/07 19:52 use two new 2-element sets instead, and reinvent the equality stuff 27/07 19:53 ? 27/07 19:53 I think this is some voodoo coming from the agda solver, not K 27/07 19:53 yes, 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 are you a K expert?  I am a novice 27/07 19:54 my intuition is all just from what I have been able to prove in agda and coq 27/07 19:55 well the thing about Coq is it actually has a theory 27/07 19:56 whereas agda is just like hack every type system rule that can fit in 27/07 19:56 :) 27/07 19:56 so 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 types 27/07 19:56 soupdragon: beware of the worker of pigs telling you to stfu ;) 27/07 19:56 I prefer to think of it as UTT + modest experimental extensions 27/07 19:56 maybe it's part of the injectivity thing 27/07 19:57 well, term constructors should be injective even in coq, right? 27/07 19:57 yeah in theory it's got a theory 27/07 19:57 :) 27/07 19:57 but in practice it's just not 27/07 19:57 yes, I'm just playing 27/07 19:57 when people prove false in agda they patch it, rather than going back to the drawing board 27/07 19:57 proving Fin n = Fin m -> n = m is a nontrivial problem 27/07 19:58 (in Coq) 27/07 19:58 you need to pigeonhole it 27/07 19:59 right - that's injectivity of type constructors though 27/07 19:59 oh sorry 27/07 19:59 I don't need that here 27/07 19:59 I don't know what 'term' means 27/07 19:59 you can prove injectivity (usually) using the methods from... 27/07 19:59 (the NoConfusion stuff) 27/07 19:59 a few construction on constructor 27/07 20:00 I meant that data constructors from datatype definitions are injective, but the types you get from datatype definitions are not 27/07 20:00 ccasin, well not all of them are injective 27/07 20:00 but you can usually prove it using a single methodical way 27/07 20:00 but injectivity of dependent pairs is equivalent to K for example, so you can't prove that 27/07 20:00 so 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 it's a little surprising to me 27/07 20:02 no 27/07 20:02 I wondre if it accepts    q : ¬ Bool ≅ Fin 2 ; q () 27/07 20:03 no, it doesn't 27/07 20:03 it used to 27/07 20:03 they took that out when it turned out to be inconsistent with LEM :) 27/07 20:03 this is interesting though 27/07 20:04 especially ¬pfin 27/07 20:04 yeah, for a while I thought agda could only prove that types of different sizes were different 27/07 20:07 I think Saizan suggested this approach, actually 27/07 20:08 what about a type with no constructors? 27/07 20:08 does it help any if you add a (Bool == Fin 2) argument to ¬pfin in Coq? 27/07 20:09 two different types with no constructors 27/07 20:09 hmm, interesting question 27/07 20:09 Saizan, well I think it's consistent to promote isomorphisms to identities 27/07 20:09 at least model theoreticallyars 27/07 20:10 you can identity them 27/07 20:10 Saizan: I'm a little confused - wouldn't that assumption only make it harder: 27/07 20:13 or, I don't see how it helps 27/07 20:13 well, in agda, (a : A) ==h (b : B) implies A == B and that's unusual, iirc 27/07 20:18 that is different from coq (it depends on K), but it's not clear to me why (Bool == Fin 2) would help in proving ¬pfin 27/07 20:33 ah, i don't know either :) 27/07 20:35 ccasin: holy crap, you proved Fin 2 /= Bool! 27/07 20:35 oh e-pig.org is updated! 27/07 20:35 what's the definition of ≅ ? 27/07 20:36 roconnor: yes, isn't type theory fun? 27/07 20:37 it's just propositional equality 27/07 20:37 refl 27/07 20:37 oh, no, sorry 27/07 20:37 hard to make out that ~ 27/07 20:37 :) 27/07 20:37 that one is John Major equality 27/07 20:37 can you paste the data definition? 27/07 20:38 sure, let me find it 27/07 20:38 data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where 27/07 20:39 refl : x ≅ x 27/07 20:39 This is the "standard" heterogeneous equality in agda, coq and epigram 27/07 20:39 well, no one (should) uses JM equality in Coq 27/07 20:39 why not? 27/07 20:39 I confess I have used it 27/07 20:40 the elimination principle in Coq is almost useless 27/07 20:40 you have to add an axiom to make it useful 27/07 20:40 yes 27/07 20:40 which axiom? 27/07 20:40 Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. 27/07 20:40 oh you mean the elimination principle of JMeq 27/07 20:40 I think you can get by with no axioms if you use a slightly different formulation 27/07 20:41 it's a waste of time though 27/07 20:41 I doubt that very much 27/07 20:41 what we really need it JMEq 27/07 20:41 eq 27/07 20:41 and K properly 27/07 20:41 roconnor: do you know if Fin 2 /= Bool is an expected consequence of K?  I really have no idea 27/07 20:42 ccasin: I'm wondering that 27/07 20:42 I find it plausible 27/07 20:42 I don't think it's a consequence of K 27/07 20:42 but if it is true, I didn't know it 27/07 20:42 it seems pecuiliar 27/07 20:43 there's a constaint solves deep in the agda source and i'm sure someone got tempted one day, and added a rule that does this 27/07 20:43 yes, the key is the type checking of () patterns 27/07 20:43 ccasin: what is the key? 27/07 20:43 and I think soupdragon is right that there are no theorems about that solver 27/07 20:43 dont get me wrong agda is BEEEEPing awesome 27/07 20:44 in ulf's thesis I think it's not elaborated into something known, or anything like that 27/07 20:44 but it upsets me that everyone uses it 27/07 20:44 roconnor: 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 that proof relies on agda's empty pattern magic 27/07 20:44 certainly I don't know how to do it in coq and think it is probably not true 27/07 20:45 ccasin: where is the empty pattern? 27/07 20:45 it's the ()s 27/07 20:45 because 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 it 27/07 20:45 when agda sees one of those, it tries to convince itself that whatever type that argument should have, it's empty 27/07 20:46 soupdragon: to be fair, there is no alternative, right? 27/07 20:46 and then you don't have to fill in an RHS 27/07 20:46 don't worry, you can't typecheck anything that could kill someone with the current memory requirements :) 27/07 20:46 yeah, 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 proof 27/07 20:47 ccasin: suc : Fin n -> Fin (S n) ? 27/07 20:47 roconnor: yes 27/07 20:47 it's the same as people using unsafePerformIO in haskell 27/07 20:47 ccasin: Agda is sound isn't it? 27/07 20:48 it just pisses me off because I don't have anything else to care about 27/07 20:48 roconnor: who knows? 27/07 20:48 we would like to think Agda is sound 27/07 20:48 I mean, it's not like Epigram 2 (currently) is 27/07 20:48 grossly unsound 27/07 20:48 huh I don't know about that 27/07 20:48 soupdragon: Epigram 2 has (Currently) type in type 27/07 20:49 ccasin: so in what way does work in Agda not count as a proof? 27/07 20:49 roconnor: 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 for 27/07 20:49 I think I'd trust Agda more than Coq. 27/07 20:49 I think that Epigram is going to have a fixed theory once it's matured a bit 27/07 20:49 to be consistent 27/07 20:49 though I don't know Agda as well 27/07 20:49 roconnor: really? 27/07 20:50 at least coq elaborates to a small core for which the theory has been done 27/07 20:50 ccasin: The impredicativity in Prop in Coq is kinda frightening. 27/07 20:50 roconnor, the number of times people have proved false in agda.... 27/07 20:50 roconnor, and the fact there is no fixed theory written down somewhere. for me that is not a good sign 27/07 20:50 s/Coq/CIC,  s/Agda/whatevers Agda's logic is/ 27/07 20:50 oh I get what you mean 27/07 20:51 it's not about Agda though 27/07 20:51 it's about CIC vs Martin Lofs stuff 27/07 20:51 roconnor: maybe, but there are PhD theses which prove CiC is consistent 27/07 20:51 agda doesn't have a well specified core logic with this property 27/07 20:51 ccasin: That's great if you think ZFC is consistent. 27/07 20:51 completely impossible to follow any normalization proofs for things like CIC :( 27/07 20:51 or even Coq 27/07 20:51 *CoC 27/07 20:51 My worries about the consistenty of Coq applies to Z as well 27/07 20:52 well, I can't help you there 27/07 20:52 maybe that makes me a little crazy :) 27/07 20:52 * soupdragon doesn't know what Z means 27/07 20:52 soupdragon: ZFC without the C and without the F (replacement). 27/07 20:53 oh yes I do 27/07 20:53 thanks 27/07 20:53 MLTT has a nice small proof theoretic ordinal. 27/07 20:53 but roconnor agda supports inductive recursive defintions 27/07 20:53 true 27/07 20:53 I don't know how much power that adds. 27/07 20:54 I'd guess it is still less than Coq, but I don't really know 27/07 20:54 part of my problem of not having studied Agda's logic 27/07 20:54 there is no logic to study 27/07 20:54 at best, it claims to be based on UTT 27/07 20:54 but UTT has an impredicative prop 27/07 20:54 yeah this is the problem really - I think agda is more just about exploring the language design space 27/07 20:55 rather than writing proofs you can beleive in 27/07 20:55 so these () in you proof 27/07 20:56 you are suggesting that the magic pattern matchin in Agda is stronger than K? 27/07 20:56 I am suggesting I don't know 27/07 20:56 I 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 K 27/07 20:56 I figured it was just K.  But soupdragon is skeptical, and I have no good evidence 27/07 20:56 soupdragon: that's interesting 27/07 20:57 I mean there is a model where bool and Fin 2 are identified right? 27/07 20:57 even one that has K 27/07 20:57 because bool and Fin 2 are in Set, rather than Prop 27/07 20:57 does it have K? 27/07 20:57 soupdragon: this model is proof irrelevent (hence implying K?) 27/07 20:58 or maybe there isn't a model with propertly.... I remember reading a scary document about how the obvious model with proof irr. was wrong 27/07 20:58 ya 27/07 20:58 well, 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 papers 27/07 20:58 yeah I think what's happening in this source file is dependent pattern matching + constraint solving 27/07 20:58 The paper Eliminating Dependent Pattern Matching 27/07 20:59 pigworker: ping 27/07 20:59 maybe we can just ask an expert... 27/07 20:59 shows how you can see that pattern matching and K are equivalent 27/07 20:59 there are sure enough of them in here 27/07 20:59 er, hello? 27/07 21:00 sorry to bug you, but we're having an argument about this: 27/07 21:00 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28286#a28286 27/07 21:00 is the proof of ¬pfin surprising? 27/07 21:00 I figured it was just standard dependent pattern matching 27/07 21:01 I'm not even sure how someone gets up to the level where they can follow a SN proof of one of these type theories 27/07 21:01 I mean I can just about see what's happening when you do candidates for reducbility on system f 27/07 21:01 but that's pushing it 27/07 21:01 let alone come up with this stuff from scratch 27/07 21:01 pigworker: wheras soupdragon and I think that  ¬pfin shouldn't be provable even with the K axiom. 27/07 21:01 it makes me just want to give up tbh 27/07 21:02 trying to figure out what's going on... 27/07 21:02 so, Fin 2 isn't Bool, because none of its elements is "true"? 27/07 21:03 yes 27/07 21:03 agda accepts that, though I think one can't do it in coq 27/07 21:04 That's more than K. 27/07 21:04 awesome, thanks 27/07 21:04 how do you reason that? 27/07 21:04 It's deducing something from a heterogeneous equation. 27/07 21:04 [15:18] well, in agda, (a : A) ==h (b : B) implies A == B and that's unusual, iirc 27/07 21:05 in Coq (a : A) ==h (b : B) implies A == B 27/07 21:05 JMeq A a B b -> A = B 27/07 21:05 soupdragon: really? 27/07 21:05 no, I think now 27/07 21:05 *not 27/07 21:05 That's one way to set up het eq (indeed, that's what I did in my thesis) 27/07 21:05 that's fine, it's  JMeq A a A a' -> a = a'  you can't prove 27/07 21:05 oh 27/07 21:05 roconnor yeah it's just the same as injective pairing, you can project the first part but not the second 27/07 21:06 Indeed, if you defined het eq as equality on Sigma Set id, that's exactly what it is. 27/07 21:06 ok, so that isn't the issue here 27/07 21:06 Agda's magic patterns are doing something more. 27/07 21:07 pigworker: 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 ccasin: let's prove  ¬ ¬ (Bool ≡ Fin 2) as well! \o/ 27/07 21:07 But here, Agda's dismissing a het equation between distinct value constructors of different types 27/07 21:07 roconnor god dammit I wish I thought of that! 27/07 21:07 That's type-constructors-distinct by the back door, I suspect, at least for datatypes. 27/07 21:09 or maybe it's just ignoring the types and comparing the constructor names? 27/07 21:10 Saizan: that's exactly what I think is happening 27/07 21:10 roconnor: sounds like fun, but how?  Here the assumption of (Bool == Fin 2) is really doing some work for us 27/07 21:11 pigworker: well, there are a few I don't know how to prove inequal still 27/07 21:12 for example, two empty datatypes 27/07 21:12 yeah, that's not gonna succumb to this trick 27/07 21:12 soupdragon: being able to define eq as a datatype is a heinous evil 27/07 21:13 really! 27/07 21:13 ? 27/07 21:13 why 27/07 21:13 because equality of codata, etc, isn't inductive 27/07 21:15 "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 I just read that in my algebra book and thought of you :p 27/07 21:17 oh yes. I am always forgetting about codata for some reason 27/07 21:17 but you also remember functions, right? 27/07 21:18 yeah 27/07 21:18 And 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 I used to think it didn't make sense to equate quicksort with mergesort 27/07 21:19 but I can see that it actually does 27/07 21:19 If you want to distinguish them, instrument their behaviour. 27/07 21:21 Looks like this channel is doing the hokey cokey. 27/07 21:29 the what?:) 27/07 21:30 oh, netsplits. 27/07 21:31 "...in, out, in, out, shake it all about..."  but this is normal, is it? 27/07 21:32 ccasin: did you have any luck with my evil pattern match btw? 27/07 21:33 ugh 27/07 21:33 lol 27/07 21:33 yeah it happens a lot 27/07 21:33 it happens from time to time on irc networks 27/07 21:33 copumpkin: Saizan pasted some code earlier using hetero eq 27/07 21:33 too little redundancy. 27/07 21:33 I found I couldn't do it with just homogeneous equality.  telescopes were too long 27/07 21:34 ccasin: ah, I must've been disconnected... I'll check the logs 27/07 21:34 and thanks to both of you :P 27/07 21:34 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28285 <- here it is 27/07 21:34 wow 27/07 21:35 cool 27/07 21:35 thanks! will play some more now :) 27/07 21:38 ccasin: couldnt' do what? 27/07 21:39 (isn't the whole point of telescopes that the lenght doesn't matter?) 27/07 21:39 np :) 27/07 21:39 soupdragon" 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 practical 27/07 21:40 what theorem?? 27/07 21:41 I wouldn't wish hom-eq telescope management on anyone. 27/07 21:41 soupdragon: the one at the bottom of my link 27/07 21:42 soupdragon: 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 cleaner 27/07 21:43 with heterogeneous equality and all 27/07 21:43 has 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 terms 27/07 21:46 I've got to run.  pigworker: thanks for your help with the pattern matching question 27/07 21:46 Saizan: where do I find import Function? 27/07 21:47 it's still in the std lib 27/07 21:47 assuming you have a fairly recent one 27/07 21:47 I go version 0.3 27/07 21:48 got 27/07 21:48 it was Data.Function in earlier versions, iirc 27/07 21:48 you can comment that import out, anyhow 27/07 21:49 I was using it further down 27/07 21:49 I only included a prefix of my file in the original paste 27/07 21:49 EmbMax is kind of painful to work with sometimes 27/07 21:59 what is the purpose of EmbMax? 27/07 22:01 it seems useless to me 27/07 22:01 I did it a while ago (at pigworker's recommendation) cause it made defining succ a lot cleaner than what I had before 27/07 22:03 okay, so it is a view 27/07 22:03 yep 27/07 22:03 It's still a struggle to reason with these things. We need a new knack, from somewhere... 27/07 22:04 ∀ {m} (n : Fin (suc m)) → view n ≡ vmax → succ n ≡ zero 27/07 22:06 something like that doesn't typecheck 27/07 22:06 view n : EmbMax n; vmax : EmbMax max, you need Het eq there, i think 27/07 22:08 yeah 27/07 22:08 I guess I'll start using it more :) 27/07 22:09 ∀ {n} -> succ (max {n}) ≡ zero <- this one is easy at least :) 27/07 22:09 to state or to prove? :o 27/07 22:09 both 27/07 22:10 ooh 27/07 22:10 (using lemma2) 27/07 22:10 I started all this yak shaving to prove that 27/07 22:10 yeah 27/07 22:10 * copumpkin tries again 27/07 22:10 wouldn't data EmbMax : {n : ℕ} → Fin (n) → Set  be easier? 27/07 22:10 I think I tried that first but had trouble because max needs Fin (suc n) 27/07 22:11 Instinctively, I'd do what roconnor just suggested. 27/07 22:12 hmm, that is what I tried 27/07 22:12 how do I get vmax : EmbMax max to work? 27/07 22:12 when max : {n} -> Fin (suc n) 27/07 22:12 vmax : forall {n} -> EmbMax (max {n}) ? 27/07 22:13 oh duh 27/07 22:14 * copumpkin kicks himself 27/07 22:14 * copumpkin cleans the rest of the code up after that 27/07 22:14 vmax : ∀ {n} → EmbMax {suc n} max 27/07 22:15 :) 27/07 22:15 oddly, that stuff just worked in Epigram 1 27/07 22:16 I mean, vmax : EmbMax max 27/07 22:16 man, this is making things so much cleaner 27/07 22:16 Now, the real question is how to construct a DSL for isos. 27/07 22:17 what 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 programming with one hand sure is a pain 27/07 22:23 voodoo or bug? 27/07 22:23 danbrown: by my reckoning, that's always a bug 27/07 22:24 is it bug 246? 27/07 22:24 I'm lost in Agda without my match-return statement 27/07 22:24 roconnor: where's the sticking point? 27/07 22:25 lemma₂ : ∀ {n f} → (p q : EmbMax {n} f) → p ≡ q 27/07 22:26 lemma₂ {.(suc _)} vmax q = {!!} 27/07 22:26 I want to do case analysis on q 27/07 22:26 but I need to generalize it's parameter first 27/07 22:26 pigworker: unclear. but doesn't this bug claim to be fixed? 27/07 22:27 oh yeah, hardwired pattern matching gives up here; can you use "with"? 27/07 22:27 danbrown: only a few days ago 27/07 22:27 pigworker: perhaps, if I knew what with does :D 27/07 22:27 roconnor: the same as Coq's Generalize tactic 27/07 22:28 more or less 27/07 22:28 pigworker: true. my agda darcs log indicates that i do have the fix 27/07 22:28 * soupdragon has never figured out how to use with 27/07 22:29 would rather the compiler typed that stuff out 27/07 22:29 anyway, i'll try to isolate it 27/07 22:29 you can always replace with by an explicit helper function (my old Lego implementation did that) 27/07 22:32 what is agda's version of eq_rec? 27/07 22:40 you need to substitute by an equation? 27/07 22:48 you can define a version of eq_rec by pattern matching, but it's probably in the library already 27/07 22:48 there's a nasty way to exploit equations with "with", but is there some fancy new "rewrite" thing? 27/07 22:50 there is, e.g. "foo x y rewrite bar x y = .." 27/07 22:54 what is the symmetry lemma? 27/07 22:55 sym 27/07 22:56 well I'm half done lemma2  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28288 27/07 23:00 I need to go home now 27/07 23:00 I'll worry about the second half later. 27/07 23:00 maxneq is my lemma0? 27/07 23:01 er 27/07 23:02 my mouse stoped working 27/07 23:04 I wrote my own, because I sort of commented out a bunch of stuff 27/07 23:04 maybe it is the same 27/07 23:04 it is a proof that emb i /= max 27/07 23:04 same type then, at least, i asked because you didn't include it in the paste 27/07 23:05 ya 27/07 23:05 I forgot 27/07 23:05 I changed the definition of EmbMax to use the n instead of suc n 27/07 23:05 er 27/07 23:05 did you fix view? 27/07 23:06 the proof is a little different 27/07 23:06 I'd paste it but my mouse doesn't work 27/07 23:06 lol 27/07 23:06 roughtly speaking it says 27/07 23:07 maxneq : forall {n} {i : Fin n} -> emv i /= max 27/07 23:07 maxneq {zero} {()} _ 27/07 23:07 maxneq {suc n} {zero} () 27/07 23:07 maxneq {suc n} {suc i} eq = maxneq (suc-inj eq) 27/07 23:07 s/emv/emb/ 27/07 23:08 oh that's nice 27/07 23:08 well 27/07 23:08 I need to head home 27/07 23:09 ttyl 27/07 23:09 ok, finally isolated it: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28290 27/07 23:15 is that error a bug, or am i abusing implicit arguments? 27/07 23:16 one would expect that the line "c : B × B; c = b , b" with the error would be ok in all contexts 27/07 23:22 i guess it typechecks with "y : X {something} × X {something}", right? 27/07 23:25 if so it looks like a bug, i'd have expected some unresolved metas rather than an error 27/07 23:26 (sorry, just changed variables: x -> b, y -> c) 27/07 23:27 it would need to be "y = x {something} × x {something}" 27/07 23:28 but that gives the same error 27/07 23:28 e.g. "y = x {A} × x {A}" 27/07 23:28 oh, true 27/07 23:32 wait, is your Σ universe polymorphic? 27/07 23:33 otherwise you'll need Σ\_1 27/07 23:33 yeah, and sometimes oracle-based checking doesn't happen until reloading 27/07 23:34 sorry, i should've loaded it into agda earlier, this "works" http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28290#a28291 27/07 23:35 you also need the explicit abstraction, it's quite annoying 27/07 23:36 Saizan: Σ is from the standard library (latest darcs), which is universe polymorphic 27/07 23:36 toggling the flag in my 'bug' module makes no difference 27/07 23:37 y : 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 bug 27/07 23:37 i see 27/07 23:38 Very interesting. This looks like one of those nasty corner cases where having "hidden Pi" in your type theory screws up. 27/07 23:39 Saizan: yes, that does solve my problem (back in the original code). thanks! 27/07 23:39 i'll file an issue 27/07 23:40 titled "Fix all the problems with hidden Pi" :P 27/07 23:40 I wound Ulf up about it in his defence, but he didn't bite... 27/07 23:40 The 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 I am familiar with this turd because I've stepped in it myself. 27/07 23:44 * copumpkin resists the temptation to @remember that 27/07 23:45 my istinct would be to add some new constraint to the system so that the decision can be postponed 27/07 23:46 jeez, i think there are three different bugs bound up in this, though the other two are more superficial 27/07 23:47 one with error reporting and one with agda-mode 27/07 23:47 Saizan: 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 I'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 Here's a nice perverse example... 27/07 23:58 y : {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 x : {! {n : Nat} -> ? !} ; x = max    does not allow the refinement 28/07 00:00 danbrown'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 Guessing where the foralls go is a weird game: I don't think machines are very good at it. 28/07 00:05 I 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 My 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 how does that mix with higher-rank ones? 28/07 00:09 My grammar of schemes is SCH ::= TYPE | {x : TYPE} -> SCH | (x : SCH) -> SCH 28/07 00:10 If schemes are known in advance, it is always clear where applications or lambdas should be inserted. 28/07 00:11 And crucially, there's no trade in scheme inference. 28/07 00:11 In effect, I'd forbid danbrown's definition of X: that's not a Set, it's a scheme. 28/07 00:13 Put differently, no hidden Pi in the underlying theory, but implicit syntax as an elaboration convention. 28/07 00:15 i see 28/07 00:16 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.ImplicitSyntax 28/07 00:17 but defining X = (_:Set) -> A; x : {_:Set} -> A; would still make "x : X" hold, right? 28/07 00:18 no; X is Set -> A, and x makes an A; A is not Set -> A 28/07 00:19 x : {_:Set} -> A  is, of course suspect  (R. Burstall: "plus can't infer its arguments") 28/07 00:20 ok, since x is really "x {_}", so we'd have to manually abstract like i did above 28/07 00:21 But you would at least get (\_ -> x) : X with some yellow. 28/07 00:21 There's no way to eliminate the manual override. 28/07 00:22 y : X × X; y = (\{s} -> x ) , (\{s} -> x ) <- works with some yellow, with the original X 28/07 00:23 And yes, the idea is that high-level x means low-level x {_}, without further debate. 28/07 00:23 Yes, that'd be enough to deflect the usual defaulting strategy. 28/07 00:24 these manual abstractions are really ugly though, i'd really expect it could do better, given the type signature 28/07 00:25 It'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 That's telepathy at work: there are too many degrees of freedom. 28/07 00:28 i guess the fundamental problem is that "\{s} -> x {s}" and "\{_} -> x {somethingelse}" are often both valid solutions, unless x's return type mentions the argument 28/07 00:31 and, more to the point, they are in this case 28/07 00:31 Genuine choice needs genuine bits. 28/07 00:32 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28294#a28294 <- i can't see why those (\{_} -> ..) shouldn't be inferrable, though 28/07 00:34 I agree. The type pushed in should supply the \{_} ->. 28/07 00:38 I wonder how bidirectional checking has been implemented. This is a funny corner. 28/07 00:38 If we separate InTm from ExTm, the question is how to push {x : S} -> T into an ExTm. 28/07 00:40 (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 so we'd have to push where we normally extract from instead? 28/07 00:44 Working 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 Worse, 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 what does yellow mean in agda? 28/07 00:50 sus pish ous 28/07 00:50 more 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 problem 28/07 00:52 for recursive definitions it might also mean that they don't pass the termination check, but that's unrelated :) 28/07 00:54 oh, does that happen now? 28/07 00:54 in older versions, termination checking only happened after reload 28/07 00:54 Mostly, if you see yellow, it's a good plan to "show constraints" 28/07 00:55 Back 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 i only use C-c C-l, so i don't really know.. 28/07 00:56 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28296 28/07 00:57 Here is my homogenous proof of lemma2 28/07 00:57 I 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 I'm not very good at Agda, so there are probably some trivial optimizations 28/07 00:58 Oh crap, it's 1998 all over again. 28/07 00:58 And there isn't really any good reason not to use hetrogenous equality 28/07 00:58 Except that in 1998, it hadn't been invented. 28/07 00:58 This was mostly an Agda exercise for me :) 28/07 00:59 It's a bad flashback for me. 28/07 00:59 The 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 I guess Fin 2 /= Bool is bad because it must not be provable in plain old type theory? 28/07 01:04 Or the homotopy folks would be up a creek. 28/07 01:04 There are models which identify them, sure. 28/07 01:04 pigworker: OTT is just syntatic sugar for setoids and homogenous equality. :) 28/07 01:05 it took me years to convince Thorsten of the untruth of that remark 28/07 01:06 roconnor: By the way, about that folding/unfolding stuff the other day... 28/07 01:06 It occurred to me that there's a difference between the fold type you linked to and what I was using. 28/07 01:06 oh? 28/07 01:07 The 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 that sounds normal 28/07 01:08 What 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 And you can use that type to build up more complex algebras out of simple ones. 28/07 01:08 That's why it was existentially quantified. 28/07 01:08 which one was yours? 28/07 01:09 The existential, algebra one. 28/07 01:09 I didn't use any of its features, though. 28/07 01:09 oh in your code? 28/07 01:09 ah 28/07 01:09 now I know what you are talking about 28/07 01:09 You can use it to build an efficient average algebra out of a sum algebra and a length algebra, though. 28/07 01:10 Or, that's the idea. 28/07 01:10 Meanwhile, 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 Saizan: 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 That 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 s/by/my 28/07 01:13 danbrown: now that's scarily flaky 28/07 01:13 dolio: ya, your existential quantifiers seemed strange 28/07 01:14 I removed it :D 28/07 01:14 pigworker: K provide that? 28/07 01:14 yeah, maybe it's more prone to eta-expand inside records? 28/07 01:14 ah what did I miss? 28/07 01:15 roconnor: 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 but it at least lets me proceed with my work in a non-disgusting way :) 28/07 01:15 Saizan: a distinct possibility; these things are so delicate 28/07 01:19 Re 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 OTT 28/07 01:23 I have trouble reading the Coq stuff that someone posted to the agda list on that a little while back... 28/07 01:24 I saw it but didn't take it in. Distractions. 28/07 01:25 But it sounded almost like they used K, only couched in homotopy language. 28/07 01:25 Maybe it's sufficiently different, though, because I thought K was supposed to blow up with that. 28/07 01:26 K says Bool = Bool in one way, but we know two isos. 28/07 01:27 Yes, but the summary of the 'equivalence axiom' given is something like "all equivalences are equivalent to identity". 28/07 01:28 isn't that more like "permutations are invertible"? 28/07 01:29 Which certainly sounds like K to me, only with all the identities involved being the homotopy kind. 28/07 01:29 All isomorphisms are the identity, up to isomorphism. Or something like that. Deep. 28/07 01:30 Right. 28/07 01:30 Of course, it's better than K, apparently, because it gets you extensionality of functions. 28/07 01:31 Uniqueness of identity proofs and extensionality of functions are certainly separable. 28/07 01:33 You can have either without the other. 28/07 01:33 I mean they proved that the equivalence principle implies extensionality. 28/07 01:34 Sounds plausible. 28/07 01:34 I guess all they need to do now is prove extensionality for codata, and you'll be out of a job. :) 28/07 01:39 Equality-wise, maybe. 28/07 01:40 I'm perfectly happy for them to believe that. 28/07 01:42 Heh. 28/07 01:43 I 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 Don'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 codata takes Pi + inductives + quotients, in general 28/07 01:47 Yeah, I'm not sure how I feel. 28/07 01:47 For instance, if you follow the category folks, heterogeneous equality is close to an abomination. 28/07 01:48 Some 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 In opposition to traditional set theory. 28/07 01:49 Depends on how you interpret het eq. 28/07 01:50 These days, I take (a : A) = (b : B) to mean the extensional TT (A = B) -> a = b 28/07 01:51 which is perfectly typable 28/07 01:51 I think that's still a problem. 28/07 01:51 Because it talks about equality of sets/types, which aren't elements of a set. They're objects in a category. 28/07 01:51 Eliminating talk about equality of arbitrary sets was the big motivation, as I understand it. 28/07 01:52 But, perhaps you could interpret the premise as 'A and B are isomorphic.' 28/07 01:53 I don't know. 28/07 01:54 that's one way, and it similarly tells you how to pull the value equation into one set 28/07 01:55 Ah, yes, that's true. 28/07 01:56 You could also consider restrictions where A = F x, B = F y, and you hypothesize that x = y. 28/07 01:57 The CT people are not used to coping with the distinction between def eq and prop eq. 28/07 01:59 Yes, that's also true. 28/07 01:59 Nor are most people, frankly. That's a type theory paranoia. 28/07 01:59 One might even say a European type theory paranoia, if bold. 28/07 02:00 TIme I wasn't here. G'night. 28/07 02:10 is there a way to convince agda to show implicits in goals and other displays of stuff? 28/07 10:48 normally I just temporarily go through my code and make implicits explicit when I need to see what they are 28/07 10:48 but that's a pain 28/07 10:48 There's C-c C-x C-h but I don't know what it actually does. 28/07 11:10 I wish I could see the with desugaring 28/07 12:17 i just got a new error that refers to the desugared form 28/07 12:18 aha finally 28/07 12:25 how did I get a conflict pulling from the agda repo 28/07 12:51 when I've never made any changes to my local copy o.O 28/07 12:51 is n : Fin 5 heterogeneously equal to n : Fin 6 for example? 28/07 13:28 say zero : Fin 5 and zero : Fin 6 28/07 13:28 zero 4 : Fin 5 28/07 13:28 zero 5 : Fin 6 28/07 13:28 isn't it 28/07 13:28 oh, makes sense 28/07 13:29 suc 5 (zero 4) : Fin 6 and so on 28/07 13:29 yeah 28/07 13:29 okay, so no :) 28/07 13:29 thanks 28/07 13:32 max != w of type Fin (suc n) 28/07 14:03 :( 28/07 14:03 Saizan: do you have any hints on how to prove succ max == zero using lemma2? 28/07 14:29 I wish I could stop encountering this damn with-desugaring issue 28/07 14:36 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 area 28/07 14:37 no == not? 28/07 14:45 as in, is that not (not (a <= b)) ? 28/07 14:45 seems like if it's one negation, you'd want b < a 28/07 14:45 but either way, it probably depends on what type this is ranging over 28/07 14:48 oh, no being the constructor of Decidable 28/07 14:48 ja 28/07 14:48 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<=a 28/07 14:49 but what I get for the no case is function from a<=b -> bottom 28/07 14:49 you can go from  no (P x -> bot)  to  P x  for any decidible P 28/07 14:49 hm 28/07 14:50 you can go from  no (P -> bot)  to  P  for any decidible P 28/07 14:50 you could also use the Ordering + compare thing on Data.Nat 28/07 14:52 yeah 28/07 14:52 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 oh I thought it means P isn't not true 28/07 14:53 you can use total probably, too 28/07 14:53 seems closer to what you want? 28/07 14:55 Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x) 28/07 14:55 total : Total _≤_ 28/07 14:55 yeah i think so 28/07 14:56 something like that 28/07 14:56 http://www.cs.nott.ac.uk/~nad/repos/lib/src/Relation/Nullary/Core.agda 28/07 14:58 data Dec {p} (P : Set p) : Set p where 28/07 14:58 yes : ( p :   P) → Dec P 28/07 14:58 no  : (¬p : ¬ P) → Dec P 28/07 14:58 so   no prf   with  prf a proof of  P -> bot,  would say that P isn't not true 28/07 14:59 I think you can prove Dec P -> ¬ ¬ P -> P 28/07 15:00 ~ 28/07 15:01 . 28/07 15:01 oops 28/07 15:01 i'll play with total a while and see what I end up with 28/07 15:03 shower first 28/07 15:03 soupdragon: yeah 28/07 15:03 copumpkin: 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 yeah, I was trying that but then encountered the with-desugaring incomprehensible error 28/07 15:10 am trying to withify it myself with a helper function now 28/07 15:10 maybe I'm overcomplicating it though 28/07 15:10 oh, it worked with with for me, but you can also use rewrite 28/07 15:11 oh it works if I take out another helper now 28/07 15:11 (you've to pass the right 'n' to lemma2, somehow) 28/07 15:12 I'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#a28325 28/07 15:16 the _|_-elim is because that case is ridiculous 28/07 15:16 and is expecting me to prove suc i == zero 28/07 15:17 I guess I'd have to incorporate the knowledge that view max /= vemb 28/07 15:17 to get a bottom out of that 28/07 15:18 well, 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 latter 28/07 15:19 oh 28/07 15:20 so the vemb case doesn't present itself at all 28/07 15:20 genius! 28/07 15:20 lol 28/07 15:20 and of course, doing that gives me the with bug 28/07 15:20 :( 28/07 15:21 what are you actually trying to prove 28/07 15:22 ? 28/07 15:22 lemma₃ : ∀ n → succ (max {n}) ≡ zero 28/07 15:22 yeah I can't read that 28/07 15:22 copumpkin: it doesn't here.. 28/07 15:22 succ max == zero 28/07 15:22 lemma4with : ∀ {n} -> succ (max {n}) ≡ zero 28/07 15:22 lemma4with {n} with view (max {n}) | lemma₂ {suc n} (view max) vmax 28/07 15:22 lemma4with | .vmax | refl = refl 28/07 15:22 ^^^ typechecks fine 28/07 15:22 soupdragon: where succ is the "circular" successor 28/07 15:22 maybe it's fixed in my version of agda 28/07 15:22 Saizan: I just darcs pulled earlier today 28/07 15:22 where are the definitions of these things then? 28/07 15:23 oh it's a bug in agda? 28/07 15:23 Saizan: 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 up 28/07 15:24 soupdragon: yeah, it's reported too but hasn't been fixed 28/07 15:24 sometimes the with desugaring conflicts with something invisible and gives you an error about a w variable that appears nowhere in your own code 28/07 15:25 lemma4 : ∀ {n} -> succ (max {n}) ≡ zero 28/07 15:25 lemma4 {n} rewrite lemma₂ {suc n} (view max) vmax = refl 28/07 15:25 nicer, btw :) 28/07 15:25 what exactly is rewrite? 28/07 15:26 so 'view' is just a normal function? 28/07 15:26 is it covered somewhere online? 28/07 15:26 soupdragon: yes 28/07 15:26 soupdragon: 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 yeah I never understood why the introduced 'rewrite', I thought pattern matching on refl was supposed to do it 28/07 15:26 I wonder why you use 'EmbMax' rather than just saying 0 is max 28/07 15:27 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28281#a28285 <- code 28/07 15:27 soupdragon: for simplicity with other arithmetic operations defined elsewhere 28/07 15:27 https://lists.chalmers.se/pipermail/agda/2009/001314.html <- rewrite explanation 28/07 15:28 thanks! 28/07 15:28 I have been handed an absurd heterogeneous equality and want to get _|_ from it 28/07 16:29 con {suc m} ~= con {suc (suc m)} 28/07 16:30 using total gets me the reversed inequality that i wanted btw 28/07 16:30 that's no cycles, tricky 28/07 16:30 you have to use induction 28/07 16:31 (to see why this needs induction consider  m = suc m  on co-natural numbers) 28/07 16:32 hm 28/07 16:33 benc___: I'm glad :) 28/07 16:33 did 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 benc 28/07 16:34 benc 28/07 16:34 oh you were addressing me in your line above 28/07 16:34 ... 28/07 16:34 soupdragon: no, i still don't undersand what you mean 28/07 16:35 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28327#a28327 28/07 16:36 thats what i did in the end 28/07 16:36 soupdragon: if I have p->bot, how do I get p? 28/07 16:37 you don't want p 28/07 16:37 you want "flip p" 28/07 16:37 you need additional information about it 28/07 16:37 ja 28/07 16:37 not all Ps have flips 28/07 16:37 that's not what I was saying 28/07 16:37 I tried to explain it in some detail earlier 28/07 16:38 soupdragon: right. i didn't think it was but i think i'm missing non-ascii characters from your pastes 28/07 16:38 i get the dec p -> not not p -> p bit 28/07 16:38 i think that would have worked for me too 28/07 16:38 yeah that was the important thing 28/07 16:39 i think i need a better irc client for this channel though. 28/07 16:40 _*_ : ∀ {n} → Fin n → Fin n → Fin n 28/07 18:00 zero * n = zero 28/07 18:00 m * zero = zero 28/07 18:00 (suc m) * (suc n) = succ (emb (m + n + m * n)) 28/07 18:00 anyone see anything wrong with that definition? 28/07 18:00 oh, there's something wrong with my addition I think 28/07 18:01 are you treating Fin n as integers mod n? 28/07 18:03 yeah 28/07 18:03 im confused why you don't define all these operations as induced by the homomorphism 28/07 18:03 how so? 28/07 18:03 since this way is a lot harder 28/07 18:03 I'd love to make it easier 28/07 18:09 oh I see what's wrong with my definitions 28/07 18:12 but am not sure how to fix them :( 28/07 18:12 well you know how  3*7+1 +  3*4+2 = 3*12+0  and mod 3 you get 1 + 2 = 0 28/07 18:15 yeah 28/07 18:15 you can use that sort of idea to define + on Z/3Z 28/07 18:15 hm 28/07 18:15 as well * and others 28/07 18:15 not really sure how to make that into an actual function 28/07 18:18 mod n : Z -> Fin n ; (nk+r) mod n = r 28/07 18:19 using the "evil" nk+r patterns 28/07 18:20 but you also have  eta : Fin n -> Z ; eta 0 = 0 ; eta 1 = 1 ; ... 28/07 18:20 then x + y  = (eta x + eta y) mod n 28/07 18:20 oh so I'd just use the standard lib mod 28/07 18:21 I considered that but it felt uglier 28/07 18:21 and harder to prove stuff about, maybe 28/07 18:21 wasn't think of the standard lib actually no 28/07 18:21 oh 28/07 18:21 what theorems are harder to prove this way 28/07 18:23 ? 28/07 18:23 not sure, I figured passing through the terrifying mod function would make things painful 28/07 18:23 given the std lib one 28/07 18:23 I can't imagine it mattering actually, because you could just prove the defining equations of either characterization 28/07 18:23 no clue about the std lib 28/07 18:23 well, how would you actually write mod? 28/07 18:23 nothing I said should dependen on that 28/07 18:23 I already defined it 28/07 18:24 you need division algorithm for the nk+r pattern 28/07 18:24 those patterns actually exist? 28/07 18:24 yeah you define it though 28/07 18:24 it's a view 28/07 18:24 oh, hm 28/07 18:24 I'll play with that then 28/07 18:25 http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.DivMod.html#184 28/07 18:25 that's what I was afraid of :) 28/07 18:25 * soupdragon doesn't use this stuff 28/07 18:25 but a view like that sounds fairly clean 28/07 18:25 the nice part is that you shouldn't need to care about the implementation of _divMod'_ because DivMod' specifies everything about it 28/07 18:35 hmm 28/07 18:38 a bit like you don't care about how view is implemented because of EmbMax and lemma2 28/07 18:41 yeah 28/07 18:41 (no idea which view makes most sense though, tbc) 28/07 18:43 peanut better than junk 28/07 18:59 should there be a difference in typechecking a function between passing a parameter implicitly via a module or adding it myself? 28/07 19:18 one typechecks and the other doesn't 28/07 19:18 is it recursive? does the recursive call use the same value for this parameter? 28/07 19:35 nope not recursive 28/07 19:35 also, maybe there's some interaction with refinements.. 28/07 19:35 it has to do with zero : Fin (suc n) 28/07 19:35 yeah, I think so 28/07 19:35 if I write f : Fin n -> Fin n 28/07 19:35 f zero = ... 28/07 19:36 with the n from a module parameter 28/07 19:36 it complains about the zero being impossible 28/07 19:36 or rather, it not matching Fin n 28/07 19:36 if instead it's f : forall {n} -> Fin n -> Fin n it works fine 28/07 19:36 i guess you'd have to put n in a with 28/07 19:36 "f i with n" 28/07 19:37 yeah 28/07 19:39 any 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/9syf 28/07 20:05 heh 28/07 20:10 i'd start by ignoring anything on the right of the | related to divMod :) 28/07 20:11 I wonder if this really will be easier than just working out the manual operations myself 28/07 20:16 that's what I do 28/07 20:48