ccasin ccasin copumpkin --- Log opened Tue Jun 01 00:00:27 2010 does the agda standard library have a sorting function anywhere? 01/06 22:47 I don't see one 01/06 22:47 don't think so, but I remember dolio wrote an insertion sort at some point 01/06 22:48 I think it was an insertion sort 01/06 22:48 Yes, it was. 01/06 22:51 cool 01/06 22:52 it's pretty easy to port the merge sort from "why dependent types matter" to agda 01/06 22:53 but it would be nice to have one in the library 01/06 22:53 Well, I was attempting to do something easy to prove correct. 01/06 22:53 ah 01/06 22:53 I haven't done that :) 01/06 22:53 was the proof tricky? 01/06 22:55 It took a while. 01/06 23:03 I'm still not sure how satisfied I am with part of it. 01/06 23:04 Finding a good proof type for l-is-a-permutation-of-l' is hard. 01/06 23:05 I've always been troubled by the irony that these sort algorithms put each input exactly once in the output, but the permutation property is hard to prove. 01/06 23:19 * Saizan wonders if parametricity would help 01/06 23:31 Saizan: the function which replicates its first element is polymorphic, produces ordered output, but is not a sort 01/06 23:37 pigworker: I don't mean that the permutation property was hard to prove, actually. I mean I failed to prove that the permutation relation was symmetric or transitive (I think those were the usual sticking points) for most of the definitions I tried. 01/06 23:38 Proving that sorting was a permutation has trouble getting off the ground with those. 01/06 23:39 Without those, even. 01/06 23:39 I was mucking about with permutation proofs a while back. It was surprisingly hard... 01/06 23:40 The one I actually proved it with has a constructor for transitivity, which I don't like, but it gave me both. 01/06 23:40 I ended up, effectively, with a domain specific language for moving things around in lists... 01/06 23:40 yeah, defs of permutation tricky: James McKinna had a nice one at one stage 01/06 23:40 Having looked back at it recently, I think that the transitivity constructor isn't actually superfluous for my definition. 01/06 23:41 I want a container-generic definition of permutation. 01/06 23:41 But I don't find it satisfying. For instance, including transitivity in coinductive relations is an easy way to get forall x y. x ~ y. 01/06 23:42 At least as Agda handles it. 01/06 23:42 I guess that's the lack of mu nu. 01/06 23:43 you can always define small steps, then take transitive closure in a list-like way 01/06 23:44 Anyhow, as I recall, I've tried "x \in l' -> l ~ remove x l' -> x :: l ~ l'", but that's hard to get symmetry for. 01/06 23:45 Because pulling off the top of the left doesn't tell you anything about the top of the right. 01/06 23:45 And I've tried a more symmetric version, where you remove the same element from both lists, but that has transitivity problems, because two proofs don't necessary pull out the same element. 01/06 23:46 James always used (1) closure under (cons x) and (2) (xs ++ ys) ~ (ys ++ xs) 01/06 23:47 So I ended up with [] ~ [], l ~ l' => x :: l ~ x :: l', l ~ l' => x :: y :: l ~ y :: x :: l', + transitivity. 01/06 23:48 Well, maybe I'll try that out then. That seems promising, I guess. 01/06 23:49 how do you prove [1,2,3] ~ [3,2,1] with that? 01/06 23:49 I don't know off hand. It'd take me a while. 01/06 23:50 It'd involve lots of transitivity. 01/06 23:50 [1,2,3] ~ [2,1,3] ~ [2,3,1] ~ [3,2,1] I guess that's not so bad. 01/06 23:50 ah, I see where the transitivity comes in: it lets you swap later in the list 01/06 23:51 Yes. 01/06 23:51 yes, that's the definition I have 01/06 23:52 James' sounds neater though 01/06 23:52 it's kind of canonical: it's the least equivalence which respects the constructors and makes ++ commute 01/06 23:54 --- Day changed Wed Jun 02 2010 Well, this certainly doesn't seem easy to prove transitivity for. 02/06 00:11 http://pierre-yves.strub.nu/research/coqmt/ 02/06 00:26 chck this out guys 02/06 00:26 Fixpoint append n₁ n₂ (xs₁ : dlist n₁) (xs₂ : dlist n₂) : dlist (n₁ + n₂) := 02/06 00:26 match xs₁ in dlist n₁ return dlist (n₁ + n₂) with 02/06 00:26 | nil => xs₂ 02/06 00:26 | cons n₁ x xs₁ => cons x (append xs₁ xs₂) 02/06 00:26 end . 02/06 00:26 it's doing an arithemetic descision procedure in the conversion rule 02/06 00:26 After last night's chat with dolio, I cooked this up: http://personal.cis.strath.ac.uk/~conor/fooling/PCon.agda 02/06 11:55 It's a DSL for writing recursive functions which rearrange containers. E.g., insertion sort. 02/06 11:56 I'd better prove a theorem about it. 02/06 11:56 for added comedy, I wrote mergesort too 02/06 16:02 anyone know if there is a size limit to the number of fields in an agda record? 02/06 16:09 I'm seeing really odd behavior dealing with big ones 02/06 16:09 you get the gratuitous eta-expansion penalty? 02/06 16:26 :) 02/06 16:26 no, it's not efficiency, agda just decides neither to load the file nor given an error unless I comment out at least two fields (any two) 02/06 16:27 I'll email the list, I guess 02/06 16:27 *give an error 02/06 16:27 if you chunk your record, is it ok? 02/06 16:28 hmm, yes! 02/06 16:30 thanks, I guess I'll just do that 02/06 16:30 though sane modules and records sure would be lovely... 02/06 16:30 ccasin: can you nest the two last as an inner record and then "open public" it 02/06 16:31 npouillard: good idea, thanks.  actually the second half of my record is all specifications about the first half, so making an inner record called "Spec" works great 02/06 16:42 though, why it didn't work in the first place remains a mystery 02/06 16:42 sure this is just a workaround 02/06 16:42 (it deserve a bug report) 02/06 16:42 turns out it was some kind of memory bug 02/06 19:16 the ghc buffer reveals a stack overflow 02/06 19:16 I guess I won't use agda to write my certified space airplane controller just yet 02/06 19:17 so who here is interested in CoqMT 02/06 20:50 nobody in #coq is talking to me 02/06 20:50 what is coqmt 02/06 21:03 it adds descision procedures to the conversion rule 02/06 21:05 I am not sure what that is, I am not good at Coq/Proof Assitants. 02/06 21:06 you know how 02/06 21:10 say you have a function 02/06 21:10 g : f 3 -> X 02/06 21:11 if x : f 3 then obviously g x : X 02/06 21:11 but if f : f (1 + 1 + 1) 02/06 21:11 oops 02/06 21:11 but if y : f (1 + 1 + 1) 02/06 21:11 you can still do g y : X 02/06 21:11 because 1 + 1 + 1 is convertible with 3 02/06 21:11 so it allows equal things wrt. beta reduction, pattern matching, stuff like that... 02/06 21:11 but modulo theories adds more decision procedures to the conversion 02/06 21:12 ah, like what? 02/06 21:12 Oh noes! I have triggered an internal error. Just when I'd managed to state my claim and was hoping to prove it. 02/06 23:19 hah, on permutations? 02/06 23:22 indeed, a claim about resources 02/06 23:29 it's looking like a strict record constructor pattern problem 02/06 23:29 --- Day changed Thu Jun 03 2010 What is the formal framework underlying Agda, like the way Coq is based on the calculus of inductive constructions. 03/06 02:54 It's rather like Martin-Loef type theory. 03/06 02:57 At least, from what I understand of the latter. I've not looked into it very closely. 03/06 02:57 hmm 03/06 02:57 and would you be familiar with the underpinnings of Epigram, dolio? I heard it was similar to Agda. 03/06 02:58 They're somewhat similar, yes. 03/06 02:59 But you remove the intensional identity types, and build an alternate extensional equality very carefully. 03/06 03:00 Epigram as currently implemented has Set : Set, but they're eventually going to change that. 03/06 03:01 dolio: tried using Data.List.Any.BagAndSetEquality for permutations, btw? 03/06 15:29 Hail the Miller man! I'm astonished at what Agda is happy to infer. 03/06 21:05 I say that, then I break it. One for Ulf to look at. 03/06 21:17 I'm writing environment-dependent programs idiomatically with K and _S_ and it's getting almost all the types, even though they're environment-dependent dependent types. Wow! 03/06 21:19 what's S? 03/06 21:19 oh sorry 03/06 21:19 I know what that is 03/06 21:20 _S_ is \ f s g -> f g (s g)  ... but its type is not its Hindley-Milner type, har har 03/06 22:24 I was thinking of streicher K axiom and wondering if there was an S axiom before I realized 03/06 22:24 too many Ks 03/06 22:24 --- Day changed Fri Jun 04 2010 is it my imagination, or am I not allowed pattern matching in a let? 04/06 01:10 It is not your imagination. 04/06 01:10 lets are rather restricted. 04/06 01:11 I'm not imagining that I can't make a \ scope over a where, either 04/06 01:11 I think let is restricted to defining things of the form 'name = expression', although I think it lets you define functions with arguments to the left of the equals. 04/06 01:12 Non-recursive, too, I think. 04/06 01:13 can't think why, if I'm willing to give a signature 04/06 01:13 And its semantics are inlining the definitions, I think. 04/06 01:13 no sharing? 04/06 01:13 I don't know about that. If it does share, then change my statement to it being a beta redex. 04/06 01:14 Also as I understand it, where is sugar for an anonymous module. 04/06 01:16 I'm not sure if that answers your question about it. 04/06 01:16 I just lambda-lifted my where clause; least evil option 04/06 01:16 That can be bad if the type signature is large 04/06 01:27 It seems to me it should be feasible to allow some sort of local pattern matching which infers result type as if the whole thing was in a hope 04/06 01:28 Well, Agda could use some way to do local pattern matching period. 04/06 01:34 yeah, case statement would be nice even if it required some annotation 04/06 01:35 Once you figure out what that construct is, you can work it into let and whatnot. 04/06 01:37 that might be a bit harder. I was thinking you often end up needing pattern matching when refining holes 04/06 01:39 and to define an appropriate lemma you have to give a type signature, which is just copied from the inferred goal type 04/06 01:39 I'm not sure you have such a convenient goal type on a let 04/06 01:39 Changing subjects, I'm wondering why some of my fonts have extra space under the line 04/06 01:39 case expressions are weird with dependent types 04/06 01:39 emacs finds something with a nice ⊸ and 𝔟 but both are considerably taller than normal lines 04/06 01:40 the fraktur b is not so important, but ⊸ is nice for linear types (I 04/06 01:40 Yeah, that happens with a lot of glyphs. 04/06 01:40 I'm trying to implement a checker for Fluet's rgnURAL, or something like it) 04/06 01:41 I remain an ASCIIist. I can 't cope with tex input mode 04/06 01:41 pigworker: I'm thinking of leaning very heavily on the existing support 04/06 01:43 basically, just let you abbreviate lemma : type; lemma ; theorem = ... lemma ... 04/06 01:43 by something like theorem = ... (case ) ..., which fills in the type of the lemma from the inferred type of that position as if it were a hole 04/06 01:43 do you know of agda-input-add-translations and agda-input-translations? 04/06 01:44 The font weirdness might be due to glyphs from several different fonts getting pulled in. 04/06 01:44 Some are probably taller than others for the same point size (even though that probably doesn't make any sense). 04/06 01:44 It's still a shiny new toy for me, but it does seem to offer real benefits at least when translating from papers typed with fancy TeX 04/06 01:45 Papers involving epigram are always so pretty, colorful and nicely typeset. Using unicode in Agda lets you get part of the way there for real code, at least. 04/06 01:47 napping: at least the type-pushed-in should let you infer the type of a helper function 04/06 01:47 Well, I guess just letting you mix identifiers and operator characters in infix might get you farther, with -o and |- and the like 04/06 01:49 It seems agda doesn't support arbitrary sections of mixfix operators 04/06 01:49 I suppose that's something to do with dependency? The papers on the parsing explain how to do it 04/06 01:49 The alternative is presumably much more arduous. Type setting what people see while programming, while retaining mostly ascii. 04/06 01:49 dolio: yeah, it looks great when the fonts work out, but I just can't cope with typing it 04/06 01:50 I don't think it's a necessary limitation. They've talked about allowing sections. 04/06 01:50 M-x describe-char is a crucial ingredient 04/06 01:51 I can't think of another way to have nicely presented code than to have what you type be replaced with the fancy presentation, and then you have the problem of figuring out how to type fancy things 04/06 01:51 It's in a document somewhere where they discuss having something more like a graph for precedence, rather than a total order by labelling with integers. 04/06 01:51 But it hasn't been done yet. 04/06 01:51 It's really crucial, I think, to be sure that the code in your paper is the code you made Agda eat. It's too easy to screw up, otherwise. 04/06 01:53 Ah, I'm not talking about trying to write code and feed it to agda, but to take papers about type systems that use fancy type systems, and keep the implementation I'm writing typographically close enough that it's easy to refer back to the paper 04/06 01:54 seems like a trivial issue 04/06 01:55 I write ascii Agda, then resurface it with lhs2TeX. 04/06 01:55 that should be "that use fancy typography" 04/06 01:55 I got that. The ergonomics become important when you're still writing a program and a paper at 2am. 04/06 01:56 I like lhs2TeX. Not quite sure how to fit in Haddock comments if I wanted to, though 04/06 01:56 yeah, I don't see how they fit together 04/06 01:57 how can I pattern match on a (Maybe (x == y)) to get a refl and unify the arguments? 04/06 02:06 I write Just refl and get an error about x /= y 04/06 02:07 What's the whole line look like? 04/06 02:08 can you use with? 04/06 02:08 or is it just that you need to write .x instead of y ? 04/06 02:09 That's my theory. 04/06 02:10 oh, that's probably what I'm forgetting. 04/06 02:10 looking at one thing tells you about other things; that's why case expressions are not ideal 04/06 02:10 here's the with line: lookup-Γ v (ctx' , v' ܃ τ) with eqVVar v v' 04/06 02:12 oh, never mind 04/06 02:12 I'd changed (refl) to a variable to try matching later on the refl, and hadn't changed it back 04/06 02:13 btw, if you use C-c C-c to pattern match it'll insert dot patterns for you where appropriate 04/06 02:13 Saizan: exactly -- why keep a dog and bark yourself? 04/06 02:14 I must hack the emacs mode so I just need to click on a pattern variable to make that happen. 04/06 02:15 heh, sometimes it barks at the wrong tree though, i.e. it might add patterns for implicit arguments even if that can be avoided 04/06 02:15 how does that work with "with"? 04/06 02:16 foo x y | bar x y 04/06 02:16 ... | z = ? 04/06 02:16 and then you C-c C-c RET z RET 04/06 02:16 err, one less RET, but i hope it's clear :) 04/06 02:16 and the first | should be a with.. 04/06 02:17 I looked for something like that, but didn't see any other mode commands, and C-c C-c doesn't accept expressions 04/06 02:17 I'd like a keystroke to make a with 04/06 02:18 pigworker: dogs are well and good, but it seems you still have to meow yourself 04/06 02:18 Saizan: that comes from exactly my case I think, where it was necessary to expand the ... and dot the appropriate arguments 04/06 02:20 The ... is interpreted rather syntactically: it's promising that nothing has changed, where you might prefer to be able to not care what changes 04/06 02:21 I suppose it would be possible for the code under C-c C-c to try to reduce dots if in fact nothing changed 04/06 02:24 I don't even care to hid changes, it's just that it seems to unconditionally expand dots you have already written 04/06 02:24 I don't think C-c C-c is where Ulf's energies are focused. 04/06 02:25 i wouldn't expect them to be :) 04/06 02:26 ironic, because it's the main thing in Epigram 1 which *did* work 04/06 02:26 No, I would hope not. It's probably something I'd be competent to improve if I knew more elisp 04/06 02:27 I'm guessing the display form of the cases is chosen on the agda side, rather than the emacs side 04/06 02:28 The emacs mode was quite snazzy 04/06 02:29 Speaking of Epigram, is OTT still looking solid? 04/06 02:29 OTT is up and running, in principle, but grindingly slow in practice, for non-essential reasons 04/06 02:31 did you get the model of bisimulation for coinductive types working? 04/06 02:32 we're tuning it a bit just now 04/06 02:32 Saizan: well, something worked; I wonder where I put it 04/06 02:35 I suppose I should write in with a question about W-types - I don't understand how "judgemental" equality fits into the distinction between "propositional" and "definitional" equality that OTT seemed to carefully finesse 04/06 02:37 Saizan: I got this far http://personal.cis.strath.ac.uk/~conor/pub/JUnfold/Thm.agda 04/06 02:39 The other files are in the same directory, but there's no accessible index. Grr 04/06 02:39 darcs get solves that :) 04/06 02:40 yep 04/06 02:40 ehm, how much ram does it need to typecheck? 04/06 02:42 Judgmental equality is whatever equality is specified by the rules. Definitional equality is whatever equality is tested by the conversion algorithm. We hope they're the same. 04/06 02:43 If you specify the theory as a system of judgments, then implement conversion based on untyped evaluation, then there is something to prove. 04/06 02:44 Saizan: I never found out. 04/06 02:45 Ulf tells me it's spending all its time termination-checking the enormous eta-expansion of a massive but completely non-recursive term. 04/06 02:46 1.5GB weren't enough 04/06 02:50 Scary 04/06 02:50 Still, nice problem to have. 04/06 02:51 using --no-termination-check doesn't seem to help though 04/06 02:52 how odd; maybe Ulf was just guessing... https://lists.chalmers.se/pipermail/agda/2010/001702.html 04/06 02:53 heap exhaustion again, maybe there's more than one problem 04/06 02:58 oh well, we'll just have to implement it directly 04/06 03:01 hey folks, it's 3am again, and today's been (darcs get http://personal.cis.strath.ac.uk/~conor/pub/DepRep) a good one, but I gotta go fall over 04/06 03:06 but in epigram you'd use Desc instead of Comm/Resp, right? 04/06 03:06 ah, ok, good night :) 04/06 03:07 we'd use IDesc, yes 04/06 03:07 anyone know of a simply typed lambda calculus implemented in agda? 04/06 10:44 Someone posted pigworker's normalizer to the dependent types reddit. 04/06 10:45 Beta-normal, eta-long. 04/06 10:46 ah 04/06 10:46 thanks 04/06 10:47 found it 04/06 10:47 does anyone know a trick to avoid to eta-expand implicit arguments of fields when building record values 04/06 14:38 I keep doing record { f = λ {x} {y} → f {x} {y} ; ... } 04/06 14:38 ≡-pred : ∀ (m n : ℕ) → suc m ≡ suc n → m ≡ n 04/06 14:48 annoying that the ≡ turns yellow between the two sucs 04/06 14:48 it seems like it should be able to work out that it's on a Nat 04/06 14:48 ... (ℕ ∶ suc m) ... 04/06 14:50 should do the trick 04/06 14:50 oh, you can do that? 04/06 14:50 oh that's the backwards thingy 04/06 14:50 it's an operator defined somewhere, right? 04/06 14:51 I remember seeing it somewhere 04/06 14:51 in Function 04/06 14:51 npouillard: my savior! 04/06 14:51 thanks :) 04/06 14:51 ah, : vs. ∶ 04/06 14:52 np 04/06 14:52 I'm still puzzled why it can't figure it out though 04/06 14:52 what your type of suc there ? 04/06 14:52 it's just the usual one from Data.Nat 04/06 14:52 it's a constructor 04/06 14:52 and the other is from Fin? 04/06 14:53 hm? 04/06 14:53 nope it's all Nat 04/06 14:53 yeah, but i think the problem is that you've another suc in scope 04/06 14:53 oh, I do 04/06 14:53 but it seems like it should be able to disambiguate them based on the fact that n and m are both Nat 04/06 14:54 that's the point indeed 04/06 14:54 I have this in some module without any glitch 04/06 14:54 suc-inj : ∀ {n m : ℕ} → suc n ≡ suc m → n ≡ m 04/06 14:54 ah 04/06 14:54 is there a built-in function that says if I know (x : Fin (suc m)) and x /= m, then I can give you Fin m? 04/06 15:05 where m is actually suc m, since m could be 0 04/06 15:05 I was looking at the nice inject functions but none of them injected what I wanted 04/06 15:05 so ∀ {m} → (n : Fin (suc (suc m))) → fromℕ (suc m) ≢ n → Fin (suc m) I think 04/06 15:08 hmm, I have an absurd negation being passed in 04/06 16:03 0 /= 0 04/06 16:04 but putting in an absurd pattern, agda can't spot (understandably) that it's empty 04/06 16:04 oh I guess I'll just use ⊥-eli 04/06 16:05 m 04/06 16:05 gah, I messed up 04/06 16:34 oh no I didn't 04/06 16:38 okay, I have modular addition :P 04/06 16:39 sad that it took so long 04/06 16:40 and that it's so ugly 04/06 16:40 trouble with literate agda: you can't edit your paper while you're waiting for a type to check... 04/06 18:12 can anyone think of a good way to do modular addition on Fin n elements (interpreted as naturals mod n) without getting ugly with decidable equality on Fins? 04/06 19:18 I have something that works but it's terribly ugly 04/06 19:19 I can do basic proofs on it but I'm afraid that they'll get too painful later on 04/06 19:19 have you defined suc? 04/06 19:20 yeah, that's where most of the ugliness was 04/06 19:20 then the _+_ is the usual, using the "circular" suc 04/06 19:21 in the circular suc I use the decidable equality on Fin n to wrap it around 04/06 19:21 if you define the emb/max view, suc is easy 04/06 19:21 emb/max? :o 04/06 19:21 oh, found it 04/06 19:22 http://www.cs.nott.ac.uk/~txa/g53cfr/l04.agda ? 04/06 19:23 ha ha, my browser didn't like that 04/06 19:24 yes, those are emb and max 04/06 19:24 okay, I'll play with those and see if I can simplify it a bit :) 04/06 19:24 I sometimes call emb "fweak" 04/06 19:24 cause right now it's kind of ridiculous 04/06 19:24 exercises 13 and 21 of my AFP notes are the relevant ones 04/06 19:25 okay, will do those too! thanks :) 04/06 19:25 modular suc takes max to zero and (emb x) to (suc x) 04/06 19:25 but I'll still need decidable equality to tax max to 0, I'd assume? 04/06 19:26 http://snapplr.com/3b4j is what I have 04/06 19:26 that's what the emb/max view does: it analyses every fin as max or (emb x) 04/06 19:26 oh, I see, it's an actual view 04/06 19:27 okay, I see how it works I think 04/06 19:27 good luck 04/06 19:28 I really must port those notes to Agda 04/06 19:28 thanks :) this stuff is fascinating 04/06 19:28 the difficulty of proofs really forces one to find elegant approaches to things 04/06 19:29 mathematics is all about definition; proof is just macho posturing 04/06 19:29 :) 04/06 19:30 anyway, thanks for all the pointers, gonna go to dinner and then come back and try cleaning this mess up 04/06 19:30 --- Day changed Sat Jun 05 2010 I'm embarrassed to say that I'm having trouble with this emb/max view 05/06 07:54 oh, I think I have it 05/06 08:17 "Inaccessible (dotted) patterns from the parent clause must also be 05/06 08:23 inaccesible in the with clause, when checking the pattern {suc _}, 05/06 08:23 when checking that the clause" 05/06 08:23 pattern matching hates me 05/06 08:32 * copumpkin has defeated the pattern matcher! 05/06 08:37 muahaha 05/06 08:37 pigworker: it worked, thanks! 05/06 10:11 took me way too long to figure out 05/06 10:11 good stuff, but yeah, it's annoying writing patterns yourself 05/06 10:24 is there a good way to figure out what's preventing it from writing out my patterns from me when it gives an error like http://snapplr.com/shtn ? 05/06 11:02 more context might help, but it looks like you have max in an index, and it doesn't know how to solve unification problems involving max 05/06 11:34 the usual escapes are (1) match on something which makes max compute (emitting a constructor), or (2) use with to abstract max 05/06 11:35 yeah, I have max in the index to that view type 05/06 12:09 hmm 05/06 12:21 is there an introduction to that PreorderReasoning begin ~~< > square module anywhere? I get more or less how it works but don't have a feeling for how or when to use it in proofs 05/06 13:12 try checking Shin-Cheng Mu's blog 05/06 13:29 haven't found it yet, but there's lots of other fascinating stuff that I got drawn into in the mean time :) 05/06 13:46 I mean, haven't found that particular PreorderReasoning stuff mentioned on his blog yet, but it contains many other interesting things 05/06 13:47 hmm, I feel like http://snapplr.com/s0ks could be cleaner 05/06 15:17 and that it's making my proofs more unpleasant 05/06 15:17 aww, this commutativity proof was almost so simple and elegant, but then something got in the way :( 05/06 15:45 * copumpkin goes argh 05/06 16:05 man, dealing with Fin indices is a real pain in proofs 05/06 16:16 because you've to unify them with non-constructors, or in general? 05/06 16:21 I have a lot of Fin (suc n)s that are a pain to unify 05/06 16:36 not even sure where they all come from :P 05/06 16:37 ah, it comes from use of zero 05/06 16:39 the Fin zero 05/06 16:39 is a Fin (suc n), obviously 05/06 16:39 but some other properties are Fin n 05/06 16:40 I guess I could just move everything to Fin (suc n) since I don't really need to deal with the empty case 05/06 16:51 feels ugly though 05/06 16:51 copumpkin: I might make sense 05/06 16:52 yeah :/ 05/06 16:52 If you see Fin as "finite sets", then some properties will require a non-empty one 05/06 16:53 it makes sense, but it seems silly to make it less general than it could be, when nobody would be able to pass in a Fin 0 anyway 05/06 16:53 or less clean, I might say 05/06 16:53 since because Fin 0 is uninhabited it would make no difference whatsoever 05/06 16:54 Ok, I see. 05/06 16:54 ah, true, i often have have a "zero () .." case in proofs involving Fin 05/06 16:54 and moving everything into Fin (suc n) is breaking my very carefully crafted complicated pattern matches that took ages to get right 05/06 16:55 :P 05/06 16:56 things like succ {suc .(suc n)} .(emb i) | vemb {n} {i} y = suc i 05/06 16:56 those things are so painful to get right and even C-c C-c fails on them 05/06 16:57 can't you replace .(suc n) by ._ and .(emb i) by ._ as well 05/06 16:57 omg 05/06 16:57 thank you :P 05/06 16:57 well that cleaned up some of the cases 05/06 16:59 still breaks in a non-trivial manner when I change it to Fin (suc n) though 05/06 17:00 copumpkin: can't you keep the Fin n and add pattern match rule for {n = zero} and then use () for the fin. 05/06 17:02 well, hmm 05/06 17:02 I have something like 05/06 17:02 (succ max | view max) + zero ≡ zero 05/06 17:02 that's my goal 05/06 17:02 so I think, oh RightIdentity for _+_ 05/06 17:02 oh wait 05/06 17:03 that makes no sense, sorry 05/06 17:03 got confused with another case 05/06 17:03 okay, so I have +-comm to show commutativity of _+_ 05/06 17:05 I used a few congs in the recursive case (pattern matching on suc x and suc y) and have a goal of x+y==y+x now 05/06 17:05 however, it won't accept a recursive call to +-comm 05/06 17:05 because the Fin indices on one are suc n and on the other it's n 05/06 17:06 not sure if that makes sense 05/06 17:06 You are proving +-comm on Fin? 05/06 17:14 Is there a way to inherit +-comm from Nat? 05/06 17:17 * npouillard was asking itself the same thing 05/06 17:18 Would it help to prove + is a hom? 05/06 17:18 it sure would be nice :) 05/06 17:29 I'd love to steal the +-assoc one too, since it looks harder for the Fin case 05/06 17:30 but I can't really show that my _+_ is related to the Nat one 05/06 17:30 at least I have a trivial +-identity :P 05/06 17:30 I was hoping to build up to finite fields but given the difficulty I've had so far it seems unlikely :) 05/06 17:31 but I refuse to give up until I at least have a group addition 05/06 17:33 representing the prime power condition for multiplicative inverses and such will be for when I'm better at this stuff :P 05/06 17:34 oh no, the mysterious w term is biting me 05/06 18:48 I have a problem! 05/06 23:38 just for a change 05/06 23:38 My permutations function returns a Vec of length (n !) which is defined in the simplest way possible (fac 0 = 1, fac (s n) = s n * fac n), and selections wants a Vec of length (suc n) for any n (so at least 1). It can't unify n ! with suc n even though across all cases it could see that it's always suc n 05/06 23:38 I'd normally break up the cases so it can see through the n ! that it's always a suc n 05/06 23:39 but this is in a type 05/06 23:39 is there a standard approach to that? 05/06 23:39 can you use with to yank n ! somewhere you can work on it, then prove that anything equal to n ! is equal to a successor? 05/06 23:45 I was thinking of that, but my issue is that this is something I want to prove, so it's sitting in a type 05/06 23:46 I guess I'll need some sort of meta-type for the proof to satisfy it 05/06 23:46 but with abstracts from types 05/06 23:46 hmm 05/06 23:48 even in something like http://snapplr.com/q56b ? 05/06 23:48 (sorry if I'm being thick) 05/06 23:49 I see what you mean by "in a type" now. You'll need to write a program to compute that type. 05/06 23:51 ah okay, I think I know how to do that 05/06 23:51 or you could write the thing which takes a number x, a proof that x is not zero, and emits suc (pred x) 05/06 23:53 where pred x depends on the proof 05/06 23:53 --- Day changed Sun Jun 06 2010 hmm, something like http://snapplr.com/gn3t ? 06/06 00:04 superfluous parentheses there 06/06 00:05 oh maybe I'm doing it backwards 06/06 00:14 yeah, duh 06/06 00:15 that'd do it, but I was thinking of writing pred : (x : Nat) -> IsSuc x -> Nat, then reallySuc : (x : Nat) -> IsSuc x -> Nat; reallySuc x p = suc (pred x p) 06/06 00:29 ah, I think I see 06/06 00:33 I'll try some more in the morning :) just proved that ∀ n → n ! ≢ 0, at least :P 06/06 00:33 thanks again 06/06 00:33 can I not pattern match on _,_ in a lambda? 06/06 08:34 You can't pattern match at all in a lambda. 06/06 08:34 oh, okay 06/06 08:35 boo 06/06 08:35 can you think of any succinct way of stating that a vector has no duplicates? 06/06 08:41 I have an ugly approach that uses an All and the selections function ([a] -> [(a, [a])]) on vectors 06/06 08:41 Injective (\ i -> lookup i v) ? fsvo Injective 06/06 08:44 fsvo? 06/06 08:44 oh I see 06/06 08:44 for some value of 06/06 08:44 hmm, that could work 06/06 08:44 yeah 06/06 08:44 this agda stuff is too fun, pity I'm leaving my computer behind for a month tomorrow :( I want it on my ipad now 06/06 12:55 Install linux on your iPad 06/06 13:06 not available yet :) my friend is the guy who put it on the iphone 2g and 3g, but the ipad is harder to break into in that way 06/06 13:07 copumpkin, ah, too bad. 06/06 15:03 will I hurt myself if I try to learn agda in a non-emacs editor 06/06 22:21 omg 06/06 22:21 every single newbies asks that 06/06 22:21 I wonder how many people I've coerced (by force) into using emacs 06/06 22:22 benmachine: I tend to survive after some viper configuration 06/06 22:36 --- Day changed Mon Jun 07 2010 My draft about type safe representation is here http://personal.cis.strath.ac.uk/~conor/pub/DepRep/DepRep.pdf but the darcs repo (chop filename off) is more fun; have figured out how to chuck in a universe too... 07/06 01:27 --- Day changed Tue Jun 08 2010 dolio: hi, mind making your CT stuff available again? i'd like to check something i recall having seen there. 08/06 16:34 stevan: Done. I haven't done anything with it in a while, though, so I'm not sure how much type checks. 08/06 16:56 thanks! 08/06 16:56 agda's type inference seems to take advantage of the injectivity of functions, nice 08/06 22:14 pigworker: using IDescTT i managed to prove conOutLaw using only ~400MB of ram :) http://code.haskell.org/~Saizan/bisim/ObsEq.agda 08/06 23:28 looks very good, and it's much closer to what we'd actually like to use than the indexed W-type encoding 08/06 23:32 yeah, quite more verbose though, but apparently simpler for agda 08/06 23:40 i should probably port it to universe polymorphism 08/06 23:41 --- Day changed Wed Jun 09 2010 Saizan: by "agda's type inference seems to take advantage of the injectivity of functions, nice" do you have other examples than data constructors? 09/06 10:41 Saizan: are you sure it's not just unifying aggressively? Sometimes when you unify f ? with f t, it takes ?:=t even if f is not injective 09/06 12:07 (I think that's what's behind bug 246.) 09/06 12:10 I think Agda was detecting functions to be injective at one point in the past. Not very clever or reliable, in my experience, so I've not used the feature, and don't know if it's still there. 09/06 12:26 It's something highly desirable (we want automatic quotation, right?) but I don't know what the issues were 09/06 12:31 Idris used to do that, due to a silly error 09/06 12:46 I think I made use of it a few times before I noticed ;) 09/06 12:46 npouillard, pigworker, kosmikus, edwinb: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26042#a26042 09/06 14:41 Saizan: interesting, because it's not doing the over-aggressive thing in that example 09/06 14:58 yeah 09/06 14:59 it's actually refusing to :) 09/06 15:00 Saizan: ha! try T true = T false ... 09/06 15:06 doesn't termination-check (ha ha); is 'injective'? 09/06 15:06 yeah, b gets inferred with that :) 09/06 15:14 * Saizan was too optimistic 09/06 15:14 it just means the criteria are too loose 09/06 15:15 I wonder if it's just checking for different heads, rather than different *canonical* heads 09/06 15:16 * pigworker plots next experiment 09/06 15:17 OK, it's not unifying (x + y) with (a + b) in the tempting way. Good. 09/06 15:22 It does unify (x + y) with (x + ?). Good. _+_  is strict in first arg here, so that works. 09/06 15:23 It doesn't unify (? + y) with (x + y). Good. You have to know more about _+_ to see why that would work. 09/06 15:24 so the fact that "y" doesn't match "suc ?" is enough to tell (x +) is injective? 09/06 16:12 --- Day changed Thu Jun 10 2010 Saizan: re (x +), it's (I hope) not so much a matter of injectivity but strictness; if + is strict in first arg, then *definitionally* (x + y) = (x + z) <=> y = z 10/06 17:40 pigworker: oh, i see 10/06 17:45 that would also explain the T examples if T true = Void; T false = Void was translated to T _ = Void i guess, though C-c C-n RET T b RET doesn't normalize to Void there 10/06 17:50 wait, by just knowing T is strict T ? = T x doesn't imply ? = x definitionally because you could substitute a value that makes it compute further, like in the (? + y) = (x + y) case 10/06 18:04 i guess "Fast and Loose Reasoning is Morally Correct" doesn't apply to typechecking :) 10/06 18:05 You still don't need to think about bottoms. 10/06 18:17 Because there aren't any. 10/06 18:17 But, when it comes to definitional equality, you make intensional distinctions between things that are extensionally the same, while the latter is what you'd probably care about more. 10/06 18:19 Or else you sacrifice decidability of type checking. 10/06 18:20 pigworker: By the way, I've seen Neel Krishnaswami remark that it's important that OTT not have Martin-Loef-like intensional identity types, because they'd allow you to distinguish between observationally equal values where you shouldn't. Is that accurate? 10/06 18:27 And if so, what about Leibniz equality encoded in the usual way? 10/06 18:28 (Perhaps identity types are fancier than that, though; I haven't read much on Martin-Loef type theory proper.) 10/06 18:29 Oh, wait, with observational equality, I guess Leibniz equality is also observational, since you can write casts between predicates for observationally equal values (presumably). 10/06 18:35 yup 10/06 18:36 since you still have subst for it 10/06 18:36 dolio: Neel is correct 10/06 18:49 Saizan: I don't know what's implemented 10/06 18:50 but yeah, T ? = T x doesn't make ? = x 10/06 18:51 every neutral term t has a -- I don't know what to call it -- "nut", a variable x with the property that if a substitution makes t equal a canonical value, it must make x equal a canonical value; the nut is what makes it stuck 10/06 18:56 The nut of ((x + y) + z) is x, for example. 10/06 18:59 If the nut of a neutral term is a parameter variable, not a hole, you can treat the whole thing like a rigid term, because no metavariable instantiation can make the damn thing compute! 10/06 19:02 Of course, this is a very intensional way of looking at things. 10/06 19:03 That's good, though. It'll still be valid when homotopy lambda calculus conquers us all. 10/06 19:08 dolio: yeah, one should not define overly intensional predicates; but, ha ha, you can still define them in the sense that their signatures can be inhabited by definitions which satisfy the relevant equations 10/06 19:12 homotopy lambda calculus seems to go even further, identifying sets up to iso, meaning that equality proofs really tell you computationally important stuff 10/06 19:28 Well, maybe. I've gotten mixed impressions. 10/06 19:31 That sounds useful, but I've also heard someone say it doesn't admit extensional equality, which seems like a bummer from a programming perspective. 10/06 19:32 And K is also out. 10/06 19:32 But I like dependent pattern matching. 10/06 19:33 I must confess I don't know the details. 10/06 19:34 It seems pretty early yet, though, so who knows where it'll end up. 10/06 19:34 I think it's more in people's heads than down on paper at this point. 10/06 19:35 You don't really need K, as such, for dependent pattern matching. You need a heterogeneous equality, substitutive on its homogeneous fragment. 10/06 19:37 Ah. 10/06 19:37 K allows you to code that as Sigma Q : S = T . coerce S T Q s = t, and that's what I did in my thesis, but it's not the only option. 10/06 19:42 I see. So K was for getting an appropriate heterogeneous equality out of the homogeneous equality. 10/06 19:48 That's how I rationalised it. K as a concept predates heterogeneous equality. Thorsten posed K as a problem, Thierry defined "pattern matching" and noted that it proved K, Hofmann and Streicher showed that K was "extra", I showed that K was all that was extra about pattern matching. 10/06 19:52 It all worked (in theory and practice), using homogeneous equality with K, in 1998. I thought of JMeq only when I was writing up. 10/06 19:57 K as a computational principle, not an inert axiom, I should stress. 10/06 20:00 Sozeau, bless him, has the whole thing ready to go in Coq, just as soon as someone gives him a version of K which computes. (It works anyway, but doesn't quite go.) 10/06 20:02 :) 10/06 20:03 who (if anyone) proved it was safe to add K to CIC (or a similar system)? 10/06 20:07 safe in the sense of consistency of the logic 10/06 20:07 Martin Hofmann, effectively 10/06 20:09 So I guess K is included in his "groupoid interpretation" paper?  I've never read it (a little scared) 10/06 20:10 or perhaps that's the whole point of the paper, scanning the abstract now 10/06 20:11 he shows that a groupoid interpretation refutes K, so it ain't true in all models 10/06 20:11 but it is true in an extensional model 10/06 20:11 I see, thanks 10/06 20:11 so we know K is extra, but consistent 10/06 20:12 yes, nifty.  I should learn more semantics, sometimes it feels all I know is syntax 10/06 20:13 pigworker: Here's a follow-up question from earlier: wouldn't observational equality turn intensional identity types into observational identity types? 10/06 20:27 Since (\q -> subst q refl) : (x : S) = (y : S) -> I S x y 10/06 20:28 dolio: it would, and that's (a) why we no longer allow them, natively, and (b) how we encode them 10/06 20:31 obs. eq. says  Id (\x -> 0 + x) (\ x -> 0 + x)  is coerceable to  Id (\x -> 0 + x) (\x -> x + 0), but what should this coercion do to refl? 10/06 20:33 if refl is evidence of definitional equality, as is traditional, that's a hole below the waterline 10/06 20:35 Okay, right. So if you tried to include them, you'd have no way of defining the coercions of the observational equality type in the first place. 10/06 20:36 But assuming you could, the identity types would also be observational. 10/06 20:36 yeah, you can't help it; everything is as observational as your propositional equality 10/06 20:39 --- Day changed Fri Jun 11 2010 pigworker: You around? 11/06 14:41 physically, at least 11/06 14:41 I've been looking at the induction-induction paper, and they make a point to mention that in Agda's implementation, you can create a 'universe' with a code for itself. 11/06 14:42 But I can do the same thing with its implementation of induction-recursion. 'data U : Set where u : U ; T : U -> Set ; T u = U'. 11/06 14:42 Is that supposed to not be allowed? 11/06 14:42 Indeed, that's not supposed to be allowed 11/06 14:42 Ah. 11/06 14:43 What's wrong with this particular example? 11/06 14:45 at least for IR, the idea is to have an initial algebras for functors on Sigma X : Set . X -> D, for some (possibly large) decoder type D 11/06 14:45 I'm not sure there's anything practically wrong with it. The positivity checker catches definitions where you add something like Pi. 11/06 14:46 But I can see how it'd be bad theoretically. 11/06 14:46 U as a whole 'doesn't exist yet' during the definition. 11/06 14:46 At the time you're defining the functor, you shouldn't be able to refer to its initial algebra. 11/06 14:47 dolio: but in this particular definition T is not mutually def with U 11/06 14:47 Well, yes. But I can construct examples where it is, I think... 11/06 14:47 I can with induction-induction at least. 11/06 14:47 Perhaps not with induction-recursion. 11/06 14:49 ok, yeah, that example isn't recursive, so there's no big deal 11/06 14:49 the key question is "what's the functor?" 11/06 14:50 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26081#a26081 11/06 14:53 There we go. 11/06 14:53 yep, that's wicked; but you say Pi is forbidden? 11/06 14:56 If you try to add Pi, it will get caught by the positivity checker. 11/06 14:57 dolio: is your × constructor really meaning a Simga type 11/06 14:57 ? 11/06 14:57 hmmm, how to make this behave badly..? 11/06 14:58 Because for "Pi : (s : U) (f : T s -> U) -> U", then you have "Pi u : (U -> U) -> U". 11/06 14:58 npouillard: I don't think it's a sigma type. That was just the quickest thing that came to mind to use both parameters of x. 11/06 14:59 Ok, because the Sigma is caught as well 11/06 14:59 Yes, trying to add sigma types to the universe has the same problem as pi types. 11/06 15:00 Or W types. 11/06 15:00 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26081#a26082 11/06 15:00 They all have codes with the same type. 11/06 15:00 Which leads to (U -> U) -> U. 11/06 15:01 Of course, I'm not certain that's actually a problem. 11/06 15:01 That sort of definition is essentially how you define an impredicative object language LF-style. 11/06 15:02 Or maybe it's an indication of impredicativity being evil. :) 11/06 15:03 (U -> U) -> U is a problem if you have a strong function space 11/06 15:04 which the LF deliberately doesn't 11/06 15:04 What's strong mean in this context? 11/06 15:05 Here "strong" means "permitted to inspect arguments, not just place them" 11/06 15:06 Ah. 11/06 15:06 you know the classic wrong'un? 11/06 15:06 Should I file a report being concerned about IR universes with codes for themselves? 11/06 15:15 Or not bother unless I can figure out a way to prove false? 11/06 15:15 I suppose there may already be one. 11/06 15:16 worth a look, and if there's nothing already, you might ask on the list 11/06 15:17 Not many issues related to induction-recursion, at least. 11/06 15:19 seems not; trouble is they're just mutual definitions plus a checker, and it's easy to mess the checker up 11/06 15:25 Yes. 11/06 15:26 --- Day changed Sat Jun 12 2010 I was going back through some of my well-founded recursion stuff in preparation for a talk on the topic and I was thinking about the definition of the proof the < on naturals is well-founded. Using the combinators from Induction.WellFounded I put together an alternate way of proving that < is well-founded from a simpler relation. 12/06 08:16 http://www.galois.com/~emertens/wfbuild/wfbuilder.html#672 12/06 08:16 I just like how it feels like it is built from the simplest core 12/06 08:20 Hello, has anyone read Pouillard and Pottier's paper on name representation? 12/06 21:34 I'm having some trouble trying to reproduce their code 12/06 21:35 In short, they have a type World of environment, and a type World<-World of names binding the outer and inner worlds, and then make e.g. expressions Tm a with constructors like Lambda : {b} -> (b <- a) -> Tm b -> Tm a 12/06 21:36 Then I try to define size : {a} -> Tm a -> Nat function by structural recursion, but it seems I have to explicitly provide the world arguments 12/06 21:37 size (Lambda {b} _ body) = 1 + size {b} body and so on 12/06 21:37 I have looked at the paper, but am no expert 12/06 21:42 a couple things: 12/06 21:42 you can download the code from Pouillard's website 12/06 21:42 and I believe it requires the darcs version of agda 12/06 21:42 also it looks like he is here 12/06 21:43 npouillard: ping? 12/06 21:43 Convenient, that. I am looking through the code online, but I haven't found the size example 12/06 21:48 I'm assuming red and yellow highlights are complaints about being unable to infer arguments 12/06 21:49 red (I think it's "light salmon") means agda can't tell the function terminates 12/06 21:49 yellow means it can't infer things 12/06 21:49 Strange. Even the constructors like App : Tm a -> Tm a -> Tm a 12/06 21:50 it highlights the recursive calls on the arguments. 12/06 21:50 can you link me? 12/06 21:51 link what? 12/06 21:52 you said you were looking at it online? if you link to the part you think is strange, maybe I can explain it 12/06 21:52 http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/ 12/06 21:53 The size function on page 4 is the problem - I filled out the undefined things like World with ? 12/06 21:54 That is, gave those things a definition earlier that was just ? 12/06 21:54 Here's my code http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26108#a26108 12/06 21:54 oh, yes, sorry, I misunderstood 12/06 21:55 OK, I'll have a look 12/06 21:55 That might be the problem - type constructors are injective, but random definitions may not be 12/06 21:57 hmm, yes, it seems odd that agda can't figure out the implicit argument on size 12/06 21:57 should be able to get it from the type of l and r in that case 12/06 21:58 and filling it in makes the yellow/pink go away 12/06 21:58 Well, redefining World as a data type seems to make it work 12/06 22:00 I have no idea why, it should just need to unify variables of type World 12/06 22:00 ah, even just giving world an arbitrary definition 12/06 22:01 like nat 12/06 22:01 makes the problem go away 12/06 22:01 agda must be hesitating because it doesn't know what type to infer. 12/06 22:01 It also works if I make a record with fields like World, and a module parameterized over such a record 12/06 22:05 npouillard: the claim that occurs is efficient seems a little strong. an unsafe implementation would only need to compare variables with x, and avoid recursing into subterms where it is shadowed 12/06 22:23 Hello. I just got around to putting up a comment 12/06 22:51 awaiting moderation, it says. 12/06 22:51 In short, if I understood OTT correctly, you must explicitly indicate where you want to use a provable equality as a cast, and if you are in a context with a false hypothesis and trying to get up to trouble you can just appeal to induction on 0 12/06 22:53 npouillard: I suppose that implementation does not work in a system that strongly enforces alpha equality 12/06 23:13 napping: just approved your comment; W-type encodings work, but they don't have the property that all zeros are definitionally equal; first-order encodings of first-order data have that property 12/06 23:16 I gotta go, I'm afraid. 12/06 23:17 --- Day changed Mon Jun 14 2010 Is there a reason that _≤′_ is not implemented as:data _≤′_ (m : ℕ) : ℕ → Set where 14/06 18:33 ≤′-refl : m ≤′ m 14/06 18:34 ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n 14/06 18:34 Instead of: data _≤′_ : ℕ → ℕ → Set 14/06 18:34 It seems like the extraneous index just leads to additional dotted patterns 14/06 18:35 ain't no good reason I can see 14/06 18:35 I suppose you have to be careful in interpreting double negation when talking to constructive logic people 14/06 18:36 It makes more of a difference for equality. 14/06 18:38 dolio: Could you elaborate a bit? My simple understanding is that I should make arguments parameters over indexes when possible 14/06 18:39 There are two ways to define equality. 14/06 18:39 Or, more than two, but you get the idea. 14/06 18:39 data _==_ {A : Set} : A -> A -> Set where refl : forall {x} -> x == x 14/06 18:40 And one where you move one A to a parameter. 14/06 18:40 The latter lets you do data _==_ {A : Set i} (x : A) : A -> Set where refl : x == x 14/06 18:41 Which is interesting, because it lives in Set despite being equality for sets in arbitrarily large universes. 14/06 18:41 And they have slightly different interpretations and induction principles. 14/06 18:42 The first one is 'the least reflexive relation on A', I think. 14/06 18:42 While the latter is something more like "the least predicate that x satsifies", but parameterized by x. 14/06 18:44 The latter might actually have K as its induction principle. I'm not sure. 14/06 18:47 I was able to follow what you wrote up to this last line 14/06 18:48 I read some paper discussing this not long ago. Perhaps one of Dybjer's on inductive families. 14/06 18:48 K is the principle that all proofs of x == x are refl. 14/06 18:48 Instead of the usual J elimination where given x == y and P x, you can produce a P y. 14/06 18:49 "K : forall x P -> P (refl {x}) -> forall y -> (eq : x == y) -> P eq" ? 14/06 18:52 Oh, no, I'm wrong. 14/06 18:52 The latter has J as its elimination rule. 14/06 18:52 And the former has a more complex rule that Martin-Loef uses. 14/06 18:53 Or, maybe J is the Martin-Loef one. 14/06 18:53 J is the Martin-Loef one. 14/06 18:53 The more parametery one is due to Christine Paulin-Mohring. 14/06 18:54 Anyhow, for the first, you have: elim : (A : Set) (R : A -> A -> Set) (f : (x : A) -> R x x) (x y : A) -> x == y -> R x y 14/06 18:54 For the latter, you have: elim : (A : Set) (x : A) (P : A -> Set) -> (y : A) -> x == y -> P x -> P y, I think. 14/06 18:55 that sort of thing, but I'd expect dependency on the proof, too 14/06 18:56 Me too, but I don't see it here in Dybjer's paper. 14/06 18:56 We used to write of "relation induction" being "proof irrelevant", meaning that you didn't learn anything about the proof object by eliminating it. 14/06 18:59 That's why I thought you got K at first, since I expected one of the eliminators to take 'P refl', similar to how you'd have a 'P nil' case for vectors. 14/06 18:59 Yeah, seen as a datatype family, you should have P x refl, and R x x refl. Note that neither of those gives you K. 14/06 19:00 sorry, R x x (refl x) 14/06 19:00 I suppose, arguably, it's rather like having the eliminator for unit take a set, rather than a predicate on unit. 14/06 19:03 Yeah, but unit is mostly ok with a lazy nondependent eliminator. 14/06 19:29 unless you're trying to prove that all elements of unit are equal, of course 14/06 19:30 pigworker: Oh, by the way: it turns out my copy of the agda executable was from mid-February. So the question becomes, was the positivity checker right then, or now? 14/06 19:43 heh, it keeps getting hacked to shut it up 14/06 19:43 I looked through the changelogs, and there were a couple changes related to the guardedness-preserving type constructor stuff. 14/06 19:44 So that's probably what the difference is. 14/06 19:44 npouillard: hello? 14/06 20:36 pigworker: are you here? 14/06 20:38 It's a bit late in UTC+0, isn't it. 14/06 20:38 napping: about quarter to eight, I think? 14/06 20:51 --- Day changed Tue Jun 15 2010 what font do you use for \[[? 15/06 00:16 How can I find which fonts on my system could supply characters? 15/06 02:27 emacs seems to like -unknown-Asana Math-normal-normal-normal-*-20-*-*-*-*-0-iso10646-1 which has a hideous amount of whitespace below the line 15/06 02:28 no idea, but this is what i have in my .Xdefaults (i use emacs in urxvt) http://pastebin.com/KF8mG3VH and it works sanely for \[[ the characters used in the stdlib (some are smaller than ideal though) 15/06 02:30 copied it off some website ages ago, yay for knowing what you're doing :) 15/06 02:31 I don't use emacs in a terminal, but that helped. I just installed Kochi gothic and removed Asana, and it's much better 15/06 02:37 That mixfix unicode syntax is nice. 15/06 02:38 yup, quite sweet 15/06 02:39 I'm playing along at home with Conor's latest paper 15/06 02:39 which one? 15/06 02:40 "coincidences"\ 15/06 02:40 ah, i've played a bit with the code too 15/06 02:42 i meant to define Any/All as ornaments over Nat or List but i got distracted :) 15/06 02:43 I played some, too, although I went with LF sort of HOAS. 15/06 02:44 All that context stuff is too much work. 15/06 02:44 which context stuff? 15/06 02:46 Defining contexts, and terms with de Bruijn indices. 15/06 02:47 And all kinds of combinators to mangle contexts so your types don't look quite as awful. 15/06 02:48 How do you do a proper HOAS? 15/06 02:48 Isn't -> a bit too computational in Agda? 15/06 02:48 Yeah, probably. 15/06 02:49 I just didn't worry about it. 15/06 02:49 I've been thinking about how to do better. 15/06 02:49 Chlipala's PHOAS seems to work pretty will in Coq 15/06 02:50 Thinking about something like PHOAS, but I'm not sure you can make that work with dependent types. 15/06 02:50 And I'm not sure the fix I'm thinking about doesn't just reintroduce the inadequacy. 15/06 02:51 (ah, i was thinking of OAAO where i couldn't find any de brujin indexes) 15/06 02:53 It seems the idea is to make a shallow embedding of the language and use it to index a deep embedding. 15/06 03:27 but I don't see how that would help anything 15/06 03:28 It means your terms and types don't have to be inter-defined. 15/06 03:52 At least, less so. 15/06 03:53 * BMeph has HOAS in different Area Codes... 15/06 03:53 First you define semantic types, then you define syntactic terms indexed by semantics types. 15/06 03:54 And, if applicable, a predicate that specifies which semantic types are denoted by syntactic types. 15/06 03:54 so you let the parent function space stand in for terms in the definition of dependent types? 15/06 03:56 hmm, Conor does like the ASCII art boxes. Cute ----------- syntax 15/06 03:58 It's like Epigram. 15/06 03:58 if one tried to write a proof searcher for (Not P) given (P : Set i) would it be any easier than a proof searcher for all propositions? 15/06 17:48 I wouldn't expect that to be easier than searching for proofs of P. 15/06 18:01 But maybe I'm wrong. 15/06 18:01 Is there a way to determine or distinguish agda's evaluation order with a program that passes the termination checker? 15/06 18:13 There shouldn't be. 15/06 18:14 If you find one, it's probably a bug. 15/06 18:14 I'm pretty sure the evaluation order is lazy, though. 15/06 18:17 Or something non-eager. 15/06 18:17 afaik, there's more or less no sharing 15/06 18:22 That sort of thing is harder to determine. 15/06 18:23 Having written some interpreters myself, it seems it's not hard to get lazy-ish evaluation for free by hijacking Haskell's. Although Agda's probably more intricate than the stuff I've written. 15/06 18:25 But writing the application case like 'eval (f Ap x) stk = eval f (eval x : stk)' is non-strict. 15/06 18:26 eval x should get a stack as well, but yes 15/06 18:31 Oh, right. 15/06 18:32 --- Day changed Wed Jun 16 2010 This book seems to be a bit stale - looks like Source.fromFile(_).getLines doesn't leave the terminator any more 16/06 01:21 I'm trying to understand when you need to declare implicit arguments. 16/06 03:45 for example, in the tutorial, _::_ for Vec starts off with {n : Nat} -> A -> Vec A n -> Vec A (suc n) 16/06 03:46 it seems to me, if Agda can figure out n from Vec A n, why do I need to put it in the definition at all? 16/06 03:46 Because you have to write down all the quantifications, even if Agda can figure out what to fill in for the corresponding application later. 16/06 03:52 yeah, there's no implicit generalization like in haskell 16/06 03:53 Oh, these are quantifications! 16/06 03:53 That makes a bit more sense. 16/06 03:53 Can I override an implicit parameter? 16/06 03:53 You can apply it explicitly. 16/06 03:53 foo {n} x y 16/06 03:54 intruiging. 16/06 03:54 bar {m} {n} x y 16/06 03:54 Though I'm not sure how useful it'd be, since it'd probably conflict with the argument it derived it from? 16/06 03:54 Occasionally it's necessary. 16/06 03:55 * ezyang suspects he won't need it to understand Quicksort in Agda. 16/06 03:55 Although if you have to do it a lot, it's probably better to make it explicit, because it must not be able to be inferred. 16/06 03:55 *nod* 16/06 03:56 Anyhow, Agda does all the type/term passing GHC has to do behind the scenes. 16/06 03:56 Explicitly in the language. 16/06 03:56 Another thing I'm not quite clear about is why I want to parametrize by some types and index by others 16/06 03:56 {} just lets you not have to write it in yourself. 16/06 03:56 Although you can also have it try to infer explicit parameters with 'foo _ _ x y'. 16/06 03:57 huh, interesting. 16/06 03:57 parameters don't count towards the size of your datatype and don't need to be rebound for every constructor, indexes can vary between constructors. 16/06 04:01 Indices don't directly count to the size of the type, either. 16/06 04:02 Ok, so suppose I have data _<_ (m:Nat) : Nat -> Set where 16/06 04:02 Only if you quantify over them in constructors (which you often have to). 16/06 04:02 <-base : m < suc m 16/06 04:02 <-step : {n : Nat} -> m < n -> m  < suc n 16/06 04:02 CAn I pop the {n : Nat} to be a parameter? Would it be clearer to do so? 16/06 04:02 No. 16/06 04:03 If it were a parameter, the result of all the constructors would have to be 'm < n'. 16/06 04:03 Huh. 16/06 04:04 oh, so because m is a parameter, all of these are m<_. I see what they did there... 16/06 04:05 I guess it would have been clearer for me as something like: data m<_ (m : Nat) 16/06 04:05 You can think of parameters as being quantified outside the datatype. For instance you could use parameterized module. 16/06 04:06 'data Foo (A : Set) (x : A) : Set where ...' versus 'module (A : Set) (x : A) where { data Foo : Set where ... }'. 16/06 04:07 It's not quite that simple, because that doesn't take nested types into account. 16/06 04:07 mmmm, clever. 16/06 04:08 I forgot a module name, but you get the idea. 16/06 04:08 So, what does it mean for me to say something like a _|_? 16/06 04:09 The feeling I get is that my function is producing a type, but this seems odd. 16/06 04:10 oh wait 16/06 04:10 That's exactly what it's doing. d'oh 16/06 04:10 It's producing a value of the empty type. 16/06 04:10 dolio: ... really? 16/06 04:11 Well, not really. It must be the empty function, and a < b must also be empty. 16/06 04:11 Right; but it is inhabited if a < b is empty 16/06 04:12 _ _|_ is inhabited by the empty function. 16/06 04:13 ok, cool, I'm not too far off into teh weeds. 16/06 04:13 a < b -> A for any A is, too. 16/06 04:14 Aw, Agda doesn't support blackboard bold as Nat 16/06 05:05 or, at least, it needs an import I don't know about 16/06 05:07 Ah, I'm missing the stadnard library 16/06 05:12 I have the following module http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26273#a26273 and am getting the error "The arguments to WF does not fit the telescope". What does that mean? 16/06 05:58 (error message points to open WF ...). 16/06 05:58 Oh, that's because Nat is implicit. Removing it gives "Set should be a function type, but it isn't when checking that _<_ are valid arguments to a function of type" 16/06 06:01 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26274#a26274 <- can't figure out this type error :-/ 16/06 08:14 * ezyang is thoroughly stumped 16/06 08:33 does anybody know a companion paper for the Voevodsky's file sent by Thorsten on the mailing list? 16/06 15:45 I do not know precisely how related it is to that development 16/06 15:48 but this is a paper relating to a talk about the equivalence axiom in question: 16/06 15:48 http://www.math.ias.edu/~vladimir/Site3/home_files/CMU_talk.pdf 16/06 15:48 though you probably already found it on his website... 16/06 15:48 alas, it seems the paper doesn't mention extensionality 16/06 15:50 though most of the file is directly related to the content of the talk 16/06 15:52 ha, thanks! (note for self: google is in the top-right corner of the web-browser, not in the "xchat" window :-) ) 16/06 15:55 :) no problem 16/06 15:55 I should warn you that I tried to look at this paper before and was scared away by the heavy use of "homotopy theory" 16/06 15:56 but maybe you'll have better luck than me 16/06 15:56 well, I've no hope of understanding this thing. But the "universe polymorphism" battle is of practical interest for me. 16/06 15:59 So, I was hoping to understand just enough to port that stuff in my system. Looks like it's hopeless, tho :-) 16/06 15:59 I also thought that was interesting - I have never run up against problems with the universe checker that weren't genuine problems 16/06 16:01 are there well known examples? 16/06 16:01 the Agda library before "--universe-polymorphism", no? 16/06 16:04 the problem being that you have to duplicate code every time you need the same stuff but in a higher universe 16/06 16:04 I was thinking of coq, since that's where Voevodsky's file was written 16/06 16:04 I think that's what he complains about in the Coq file 16/06 16:05 well, I agree this problem existed in Agda 16/06 16:05 but I am surprised to see he ran up against it in coq - usually the universe checker there has left things "unresolved enough" for my purposes 16/06 16:06 then again, I guess I do more proving and less programming in coq 16/06 16:06 so far, Coq has no form of universe polymorphism, hence being in the pre-"--universe-poly" era, I suspect 16/06 16:06 is this right?  I thought coq had universe polymorphism a la Harper and Pollack 16/06 16:08 indeed, it does - you just write "Type" and it works at any level 16/06 16:08 different than agda in that the universes are nicely hidden from you 16/06 16:09 there are several calculus in Harper-Pollack, I doubt they implemented the real polymorphic one, in which we would work with principal types 16/06 16:13 but, honestly, I've not experimented with it 16/06 16:13 I'll have to spend some time understanding what they have now, what they are working on 16/06 16:14 some time ago, I was pointed to that: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2298 16/06 16:14 Observe that this passes the coq checker: 16/06 16:15 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26280#a26280 16/06 16:15 Ulf also implemented a variant of Harper-Pollack in some stage, but I've been told it was really really slow (?) 16/06 16:15 looks like lists work at different universes to me 16/06 16:15 doesn't that count as universe polymorphism? 16/06 16:15 thanks for the link, though - I am very interested to learn what they have actually implemented 16/06 16:16 indeed, that's polymorphism. I don't want to abuse your time, but if I define: f : Set0 -> Set0, am I able to apply it to x : Set2 ? (giving me something in Set2) 16/06 16:19 In coq?  This is tricky, since you can't tell it to work at a particular Type level 16/06 16:21 at best you can force it to be above some fixed level (or above the level of some other term) 16/06 16:21 you just write "Type" and it figures out which "Type n" you meant 16/06 16:21 ok, I see 16/06 16:22 But, considering that, the answer should be yes 16/06 16:22 f's type is really: 16/06 16:22 f : Set n -> Set n   (n >= 0) 16/06 16:22 (well, Type n -> Type n.   Set means something different in coq - a universe below type) 16/06 16:23 and that's polymorphism, indeed. Ok, then I'm really curious to know what prevents the file to go through! :-) 16/06 16:23 yes, me too :) 16/06 16:25 pedagand: I think I understand coq's restriction now 16/06 18:43 it seems to be that coq can't instantiate defined terms at different universe levels in checking the same expression 16/06 18:44 ccasin, I'm lurking the #coq discussion, that's indeed interesting. Please explain! :-) 16/06 18:44 ok, so they do not have Harper-Pollack ultimate system 16/06 18:45 pedagand: right 16/06 18:45 thanks a lot of having asked, I would not have dared 16/06 18:46 things are perfect just so long as you don't demand that some definition be used at two different universe levels in the same expression 16/06 18:46 mattam is always good about answering the questions of us mortals 16/06 18:46 indeed, that's were real polymorphism is need, much as ML polymorphic functions 16/06 18:46 yeah 16/06 18:47 so I guess ulf's comments about efficiency make sense - that coq bug you linked suggests it's just too slow 16/06 18:50 That's odd. I thought Coq could do things like 'List T :: Nil', which would have List at two different levels. 16/06 18:51 dolio: but definitions is different from constructors 16/06 18:51 Yes, I guess instantiating List at one level in the type and one level in the expression may be different than at two different levels in an expression. 16/06 18:52 But the full judgment is '(List T :: Nil) : List Type', or what have you. 16/06 18:53 goodo, my system accepts the id/typeof mess. ccasin, you made my day! thanks again. :-) 16/06 18:57 pedagand: no problem! does epigram have good universe polymorphism, or is this some smaller toy? 16/06 18:58 The other thing is, Coq's universe polymorphism is much more like the stuff you actually see in the literature (what little there is). 16/06 18:59 Agda's is new. 16/06 18:59 it's a toy now, tomorrow I show it to SuperConor, he will say "ha, you made a mistake here", and I will to start over again. But if there is no mistake (highly unlikely), I will try to get it in Epigram asap 16/06 19:00 Although I like Agda's more. :) 16/06 19:02 dolio: interesting - I can't stand it! 16/06 19:02 Aside from the fact that it doesn't have lifting into higher universes yet. 16/06 19:02 it makes me do so much work 16/06 19:02 (With associated inference.) 16/06 19:04 I find that just having all these extra arguments around is a big hassle 16/06 19:05 in the algebra part of the stdlib, lots of the records are parameterized by 2 or 3 universe levels, and it's hard (for me) to keep track of 16/06 19:05 Yes, well, if you could lift into other universes, you'd only need to have one. 16/06 19:06 good point 16/06 19:06 the lifting is pretty key, it really clutters code now 16/06 19:06 Yes. 16/06 19:06 so much so that I just use set-in-set 16/06 19:06 npouillard: about your paper on naming, the example could be improved 16/06 21:38 npouillard: looking for occurances of the free x by maintaining a chain of liftings imposes a cost proportional to depth at each variable encountered. 16/06 21:57 npouillard: This could be avoided by letting the implementation provide a specialized <-* type, and a proof of equivalence to the general definition. This would work nicely at least for the DeBruijn implementation 16/06 21:58 npouillard: I'm not sure how to match the optimization of not recursing under a binder which shadows your variable, without losing alpha equivalence 16/06 21:58 napping: 1/ sure it could be improved, but we also tried to keep them short 16/06 22:02 2/ We would like to be able to implement other data structures with a lower cost 16/06 22:03 We've not tried to write impelementation-specific ones though 16/06 22:04 3/ Yes we couldn't find a way to express it in a safe way 16/06 22:05 napping: Thanks for your remarks BTW 16/06 22:05 npouillard: for point 3, it seems you would need an operator taking a default value and something like a proof that the recursive call will always equal the default on a term that contains no references to the given variable. 16/06 22:15 npouillard: It sounds like the sort of thing that would be a huge pain to implement and not often useful, though 16/06 22:15 napping: We tried hard not require proofs from the user, but that may be a solution 16/06 22:17 However, providing specialized versions of environments with the implementation seems likely to let you implement environments as efficient tree maps 16/06 22:18 napping: Yes, I hope to try that at some point. The first goal was to keep the set of primitives minimal which is already not that small 16/06 22:20 I don't see any instances of pattern matching on the append, outside of the definition of export*<- 16/06 22:22 The small set of primitives is useful. One of the nice things that comes from your approach is the opportunity to show some extra operation is still sound by proving that it behaves equivalently to something implemented from the primitives 16/06 22:24 napping: sure but the paper shows only a small part of the Agda developpement 16/06 22:24 We also want to formalize that each primitive is sounds (fits the logical relation) and so we wanted to keep it small at first 16/06 22:25 Yes, you seem to have done that. 16/06 22:26 The theorem that each prim is sound is only done on paper 16/06 22:27 It seems to me that you can now add operations to any implementation without having to redo the proof, as long as you show how those operations are equivalent to something defined with the primtiives 16/06 22:29 napping: Indeed it make sense 16/06 22:29 I will have to read the rest of the development. I have only looked at the simple type checking part, and more basic foundations. 16/06 22:30 --- Day changed Fri Jun 18 2010 is there an ascii sequence for the function composition dot that I see in a helloworld example:   fromString = fromColist (dot) toCostring,  where dot is some unicode? 18/06 07:50 in agda's emacs mode you can type \o to get that 18/06 07:51 but not in a plain source file? 18/06 07:51 ∘ 18/06 07:52 * benc__ wants to know if he can reasonably program agda using ascii rather than unicode, is really the bigger question 18/06 07:53 without changing my editing environment 18/06 07:53 I don't think the standard library provides ASCII synonyms 18/06 07:54 hmm, I'm not sure you can even provide synonyms for constructords 18/06 07:55 agda works fine, of course 18/06 07:55 hmm ok 18/06 07:55 but what doesn't work in your environment? 18/06 07:55 I don't have a (dot) key on my keyboard 18/06 07:55 My understanding is you should really have a unicode input method if you want to write Agda.. 18/06 07:55 benc__: linux? 18/06 07:55 you're going to miss out on quite a few things without the emacs mode 18/06 07:55 That's what the emacs mode is for - \o turns into the dot 18/06 07:56 saizan: ok - maybe i'll play with that 18/06 07:56 er, the emacs input method at least 18/06 07:56 * ezyang uses Xcompose 18/06 07:56 the emacs mode gives you tons of stuff like looking up types, showing the context for "?" goals, building pattern matching, etc 18/06 07:57 e.g. showing the types of the goals together with the context, optionally normalized 18/06 07:57 ezyang: I deal with enough ways of getting to consoles on different platforms I like to come up with a lowest common denominator rather than customising one platform for one parlicular app 18/06 07:57 napping: yeah that looks neat. i'll play with it 18/06 07:57 ezyang: unless there's motivation not to, which the emacs mode here sounds like 18/06 07:57 benc__: Xcompose is for your X window manager. 18/06 07:57 so, if you SSH somewhere, it'll still work. 18/06 07:58 ezyang: yeah I don't have that on this machine - its running the os x gui. and I can enter stuff in unicode there just fine until I go use some machine that is not my own and is running putty 18/06 07:58 * ezyang remembers the days of the portable apps and his trusty usb key 18/06 07:59 Now I just lug my laptop around everywhere. 18/06 07:59 the input methods work on your target machine anyway, so the only question is if all the shells can display unicode 18/06 07:59 I know my linux terminals do fine 18/06 07:59 os x terms do ok too with fiddling 18/06 07:59 get confused a bout double-width characters 18/06 08:00 I don't think the library uses any of those, just a bunch of math 18/06 08:00 every few years I try out unicode again and find the experience "almost there, maybe next year" ;) 18/06 08:00 napping: yeah its mostly/only CJK that is double-width 18/06 08:00 well, everything seemed to work when I wanted to try Agda. 18/06 08:03 of course, my big fear about messing round in emacs is that I'll get sidetracked into learning elisp. 18/06 08:04 well, a little trouble with the fonts. For some reason asana has a huge descent on all the characters, but switching it out for kochi gothic fixed that 18/06 08:04 hasn't happened to me yet 18/06 08:05 Everything built-in has ascii equivalents. 18/06 08:08 Is there any way to make an inductive type with ASCII equivalents for unicode constructors? 18/06 08:09 whats the problem there? that you have synonyms for constructors? 18/06 08:09 Not that I know of. 18/06 08:09 I don't think you can define things you can pattern match on 18/06 08:11 this tutorial I am reading says: 18/06 08:26 >There is a distinction between parameters and indices of a datatype. 18/06 08:26 is the difference there that constructors can produce objects with any index they want but the parameter is fixed? 18/06 08:27 a parameter 18/06 08:27 benc__: Lol, are you reading my blog post? 18/06 08:28 no 18/06 08:28 i will if you send me the url 18/06 08:28 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 18/06 08:28 Oh, now I remember where I read that 18/06 08:28 Yeah, it's in that tutorial. I remember reading that sentence :-) 18/06 08:28 http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/ 18/06 08:29 Based off of Mertens talk, which was basically "quicksort in Agda" 18/06 08:29 subtitle "how to convince the termination checker your program terminates" 18/06 08:29 * benc__ sighs that backspace is not bound correctly in his fresh emacs installation 18/06 08:32 napping,ezyang: thats why I avoid moving away from my default edit environment ') 18/06 08:32 say i have some small haskell apps, is it feasible to pull bits of those into agda to reason about eg list lengths and sortedness but still have my app run? 18/06 09:09 it kinda seems like it can be done 18/06 09:09 i get a type checking error with this: 18/06 17:10 http://fpaste.org/sVS4/ 18/06 17:10 fromDigits s != q of type Nat 18/06 17:10 I guess i don't understand 'with' properly 18/06 17:10 (toDigits and digits from Data.Digit) 18/06 17:10 really what I'm trying to do there is extract the list of digits to pass into other functions 18/06 17:11 * benc__ discovers theDigits but still puzzling over how to use 'with' 18/06 17:25 --- Day changed Mon Jun 21 2010 Saizan: OK - good.  Though I suppose I should have more faith in the agda hackers 21/06 19:53 yeah, agda currently lacks something like a positivity check for records, but i guess that's easy to avoid :) 21/06 19:55 ccasin: too bad patch-tag is down, i wanted to ask if you think solvers could be implemented in less lines of code than those there 21/06 19:57 I'm no expert, but it would be fun to play a little golf 21/06 19:58 i guess a somewhat generic lib for syntax with binders would help a lot 21/06 19:58 yes!  I am constantly tempted to implement something like that, but the overhead just gets too high because of agda's performance issues 21/06 19:59 ouch 21/06 20:00 were you using a lot of records? 21/06 20:00 http://code.haskell.org/~Saizan/agda-reflection/ <- i've pushed my copy of the repo here, btw 21/06 20:00 yes, I was using records to be very general about the nature of variables 21/06 20:01 possibly more trouble than it's worth, though 21/06 20:01 alas, I am running agda 2.2.6, so I can't play with it until patch-tag reappears 21/06 20:03 well Agda's darcs repo is on code.haskell.org :) 21/06 20:06 oh, right, silly me 21/06 20:06 which just stopped responding? 21/06 20:07 ah, no, it's just a bit slow 21/06 20:07 --- Day changed Tue Jun 22 2010 Are there any (A B : Set n) such that A and B have the same number of members but for which agda can prove (not (A = B))? 22/06 14:42 I think I asked this months ago, but I forget if there was an easy answer :) 22/06 14:43 By = I just mean the standard defined homogeneous equality 22/06 14:44 i think i remember the discussion but not the conclusion :) 22/06 14:49 I remember at least someone showed me how to prove (not (Bool = Nat)) 22/06 14:51 but at the same size, I don't know - I think it's relevant to the current discussion on the mailing list 22/06 14:51 for (not (Bool = Nat)) you prove there can't be an injection Nat -> Bool and then use Bool = Nat to construct one? 22/06 14:53 The way we did it then was to define (P s := "s has exactly two elements") 22/06 14:54 which is simple, then you show (P Bool) but (not (P Nat)) 22/06 14:54 and get a contradiction from Bool = Nat 22/06 14:54 it's a similar idea 22/06 14:54 i see 22/06 14:58 suppose data A : Set where a : A; data B : Set where b : B, then maybe the right predicate would be "P s = exists x \in s, x == a", where == is heterogeneous equality on types, though that might be cheating in this context?:) 22/06 15:02 that works! 22/06 15:08 cool 22/06 15:08 now: do we need UIP to prove it? 22/06 15:08 s/heterogeneous equality on types/heterogeneous equality on values/ off course :) 22/06 15:09 to prove A = B? 22/06 15:09 to prove (not (A = B)) 22/06 15:09 * ccasin opens a coq file 22/06 15:09 ah, yeah, mh i don't know, i'm not that familiar with type theories without UIP :) 22/06 15:10 me either, luckily some french guys implemented one I can use to check my work :) 22/06 15:11 alas, I'm having trouble with this strategy in coq.  I don't know how to get a contradiction from (a == b) there 22/06 15:46 heh, the usual P a = \top; P b = \bot and then cast (_ : P a) to (P b) doesn't work when a and b have different types in fact 22/06 15:53 but with A = B they do have the same type 22/06 15:55 though i'm not sure how you'd write that P 22/06 15:55 ah, so I was trying to prove (not P B) (for the P you suggested before) in the empty context.  But maybe I should try it under the assumption A = B 22/06 15:56 --- Day changed Wed Jun 23 2010 can you do pattern matching of a one-constructor type in a let? 23/06 00:34 or am I getting confused with Coq again? 23/06 00:34 i don't think so 23/06 00:38 right, I want with 23/06 00:38 how can I say to emacs to invoke agda with the option "--type-in-type" ? 23/06 18:33 (or any other option actually) 23/06 18:35 you can use a pragma in the source file 23/06 18:38 can you give me the line I should write ? :) 23/06 18:45 I'm quite a newb :). 23/06 18:45 something like {-# OPTIONS --type-in-type #-} 23/06 18:51 parse error :/ 23/06 18:55 hum, no, I made it 23/06 18:55 thank you :) 23/06 18:56 you're welcome 23/06 18:56 --- Day changed Thu Jun 24 2010 I am familiar with Haskell, but have not yet tried Agda.  Question about mixfix operators. 24/06 20:24 In Agda, can one easily define new list-like operators, e.g. ? 24/06 20:25 Or tuple-like operators?  Where there are distinct start & stop tokens, and some separator between elements. 24/06 20:25 I don't know a way of doing this, no 24/06 20:27 when I want list-like things I build them cons and nil-like operators 24/06 20:27 *build them with 24/06 20:27 yeah.  I'm just curious. 24/06 20:28 syntax is important for DSLs. 24/06 20:28 I believe that - cons and nil aren't so bad though 24/06 20:29 and agda's stdlib has a good trick products 24/06 20:29 it just defines _,_ 24/06 20:29 you can put parens around it if you want, since those are already in the syntax 24/06 20:29 *good trick for products 24/06 20:29 hmm. 24/06 20:29 or of course you could do like <_,_> if you wanted different brackets 24/06 20:30 but then you could only have 2-element things? 24/06 20:31 e.g. <1, 2> but not <1, 2, 3>? 24/06 20:31 yes, though somehow the agda stdlib gets around this for the standard tuples - not sure how, may be hard coded 24/06 20:32 alas, hard-coded rules for tuples make me sad.  I guess that's a good use case for the datatype generic stuff. 24/06 20:33 oh, I know how they get around it 24/06 20:35 silly me 24/06 20:35 how's that? 24/06 20:35 since the pair syntax is just _,_ 24/06 20:35 Oooh. 24/06 20:35 if you write (a , b , c) 24/06 20:35 No triples, etc then? 24/06 20:35 it's just seeing the nesting 24/06 20:35 it's actually (a, (b, c)) 24/06 20:35 yes 24/06 20:35 That's a good way of doing it, I suppose. 24/06 20:36 I bet you could define new list-like syntax 24/06 20:37 need to define a comma-like function 24/06 20:37 _,_ 24/06 20:37 for the separator 24/06 20:37 and then make the brackets function be the identity function 24/06 20:37 the trick is ending the list 24/06 20:38 can't you write a function like 24/06 20:38 <_> 24/06 20:38 where the argument goes in the middle? 24/06 20:38 yes 24/06 20:38 (I don't know Agda syntax) 24/06 20:38 I meant that you need to stick a nil on the end of the list somehow 24/06 20:38 unlike for tuples 24/06 20:38 yeah 24/06 20:39 I suppose you could define _> as \x -> x :: nil 24/06 20:39 and _,_ as :: 24/06 20:39 and <_ as id 24/06 20:39 that might work 24/06 20:39 though the parsing priorities would be a trick 24/06 20:40 tricky! 24/06 20:40 oh, but I'm wrong 24/06 20:40 no... maybe it works?  I've confused myself :) 24/06 20:40 It's just a curiosity of mine at the moment.  I probably shouldn't obsess over syntax. 24/06 20:40 (queue some Alan Perlis aphorism here) 24/06 20:40 no, that's the best part of agda 24/06 20:40 exercise: find a way to use a unicode snowman sensibly 24/06 20:41 I've been working on an array-centric EDSL in haskell for my MS thesis 24/06 20:41 able to express linear algebra, some BLAS sort of stuff. 24/06 20:41 compiling to GPUs using CUDA 24/06 20:42 cool 24/06 20:42 trying for a `deep' embedding of a DSL in haskell is a bit unsatisfying as far as syntax goes 24/06 20:42 having been made to write matlab, I appreciate the need for a good array-centric edsl :) 24/06 20:42 my goal is for offline codegen 24/06 20:43 generate CUDA code, to be used in a larger C++ application 24/06 20:43 a more flexible language, more APL-like, would be awesome 24/06 20:43 but a lot harder to compile :-) 24/06 20:43 :) 24/06 20:45 I've never written any APL, but I think of haskell as pretty flexible! 24/06 20:45 hah, this silly syntax works! 24/06 20:50 with some help from "infixr" declarations to specify parsing priority 24/06 20:50 I've not written APL either.  It has a bunch of array primitives, like map, reduce, scan, and a bunch of others.  A lot of those you see in the various array libraries for Haskell.  Writing programs using such array primitives gives a lot of opportunities for data parallel implementations. 24/06 20:50 I'm told APL-like languages get you thinking in a different way about programming. 24/06 20:51 The array primitives are truly primitives, not defined in terms of iteration or recursion. 24/06 20:51 awesome! 24/06 20:52 so you can make your own list-like syntaxin Agda, if you wish. 24/06 20:52 thanks for your answer, ccasin 24/06 20:54 i should go do some actual work 24/06 20:54 no problem 24/06 20:54 have fun 24/06 20:54 --- Day changed Fri Jun 25 2010 Is there a good way to make this generic in its equality (say the PrefixSum module was parameterized over a Monoid rather than a IsMonoid with  _≡_)? it seems like this is going to have to change a lot 25/06 06:28 http://www.galois.com/~emertens/powerlist/powerlist.html 25/06 06:29 Does that even use \== at all? 25/06 06:55 you'd need to define the equality for trees on top of that, but then it shouldn't be very different, aside from changing the rewrite's to subst's or similar 25/06 06:56 you might need to write some lemma to prove that e.g. ps respects such an equality 25/06 06:57 maybe i'm underestimating the impact of this :) 25/06 06:57 what is "rewrite"? 25/06 06:58 rewrite takes a proof of a \== b and rewrites all occurences of a to b in the current context 25/06 06:59 where both a and b can be compound expressions 25/06 06:59 That might be a little hard to replace 25/06 07:00 since that's used only to prove other \== propositions it should work out 25/06 07:02 yeah, I'd have to be explicit about my proofs and not use rewrite 25/06 07:23 proving congruence for some of the functions seemed tricky 25/06 07:23 you'd take "cong2 _||_" and "cong [_]" as constructors for the equality, and then it should just be a matter of recursing like the function does 25/06 07:27 I started here: 25/06 07:33 _≋_ : ∀ {n} → Rel (Tree n) ℓ 25/06 07:33 [ t ] ≋ [ u ] = t ≈ u 25/06 07:33 (tˡ || tʳ) ≋ (uˡ || uʳ) = (tˡ ≋ uˡ) × (tʳ ≋ uʳ) 25/06 07:33 question about http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf : http://codepad.org/sF1aW0cx 25/06 18:52 haha 25/06 18:57 yes 25/06 18:57 hi ccasin ; glad you agree 25/06 18:58 thought i was losing it 25/06 18:59 from the tutorial: apply : (A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a 25/06 21:26 in (A : Set)(B : A -> Set) is (A : Set) context for (B : A -> Set)? 25/06 21:28 It means the same as (A : Set) -> (B : A -> Set) -> ... 25/06 21:29 sometimes you can omit the arrow 25/06 21:29 So, yes, the A is in scope for the rest of the type 25/06 21:31 oh 25/06 21:35 ah, that is explain afterwards; after the first place it is used :/ 25/06 21:51 is Agda a good language to try defining and proving all of number theory in? is there a better one? 25/06 23:20 --- Day changed Sat Jun 26 2010 Mathnerd314, I cannot answer your question, but you might want to ask the same question on #coq, with s/Agda/Coq/ 26/06 00:10 ok... :p 26/06 00:11 out of curiosity, what do you call "all of number theory"? do you have a reference book in mind you would translate? 26/06 00:11 no, just a 6-week long intensive summer program 26/06 00:11 also, maybe there are bits of that in the standard library (I believe there is a ring solver there, I don't know if that's the kind of stuff you're thinking of) 26/06 00:12 yes, I know that (Nat etc.) 26/06 00:12 I see, 6 weeks, the whole of number theory: that's indeed gonna be intensive ;-) 26/06 00:13 we probably aren't doing all of it; I'll see 26/06 00:22 * glguy generalized his proof from yesterday over an arbitrary Monoid (now with an arbitrary ==) http://www.galois.com/~emertens/powerlist/powerlist.html 26/06 02:43 so many cong function! :) 26/06 02:44 truly 26/06 02:50 i feel like those cong functions should be a corollary of parametricity 26/06 02:52 I think I get most of these congruence functions for free if I parameterize my functions a little bit better 26/06 03:15 Is there a way to get types to display as though I were in the context that my goal is in? 26/06 22:47 when I “open mymodule A" 26/06 22:47 I don’t want to see everything I imported as fully qualified 26/06 22:47 --- Day changed Sun Jun 27 2010 which commands are you talking about? i found that they don't add qualifications if you call them from the hole, or if they do that you lack some open 27/06 04:57 saizan: C-c C-, 27/06 04:58 for example 27/06 04:58 specifically for parametarized modules 27/06 04:58 i remember some ugliness associated with parametrizing by records 27/06 05:01