--- Log opened Tue Jun 01 00:00:27 2010
ccasindoes the agda standard library have a sorting function anywhere?01/06 22:47
ccasinI don't see one01/06 22:47
copumpkindon't think so, but I remember dolio wrote an insertion sort at some point01/06 22:48
copumpkinI think it was an insertion sort01/06 22:48
dolioYes, it was.01/06 22:51
ccasincool01/06 22:52
ccasinit's pretty easy to port the merge sort from "why dependent types matter" to agda01/06 22:53
ccasinbut it would be nice to have one in the library01/06 22:53
dolioWell, I was attempting to do something easy to prove correct.01/06 22:53
ccasinah01/06 22:53
ccasinI haven't done that :)01/06 22:53
ccasinwas the proof tricky?01/06 22:55
dolioIt took a while.01/06 23:03
dolioI'm still not sure how satisfied I am with part of it.01/06 23:04
dolioFinding a good proof type for l-is-a-permutation-of-l' is hard.01/06 23:05
pigworkerI'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 help01/06 23:31
pigworkerSaizan: the function which replicates its first element is polymorphic, produces ordered output, but is not a sort01/06 23:37
doliopigworker: 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
dolioProving that sorting was a permutation has trouble getting off the ground with those.01/06 23:39
dolioWithout those, even.01/06 23:39
edwinbI was mucking about with permutation proofs a while back. It was surprisingly hard...01/06 23:40
dolioThe 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
edwinbI ended up, effectively, with a domain specific language for moving things around in lists...01/06 23:40
pigworkeryeah, defs of permutation tricky: James McKinna had a nice one at one stage01/06 23:40
dolioHaving looked back at it recently, I think that the transitivity constructor isn't actually superfluous for my definition.01/06 23:41
pigworkerI want a container-generic definition of permutation.01/06 23:41
dolioBut 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
dolioAt least as Agda handles it.01/06 23:42
dolioI guess that's the lack of mu nu.01/06 23:43
pigworkeryou can always define small steps, then take transitive closure in a list-like way01/06 23:44
dolioAnyhow, 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
dolioBecause pulling off the top of the left doesn't tell you anything about the top of the right.01/06 23:45
dolioAnd 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
pigworkerJames always used (1) closure under (cons x) and (2) (xs ++ ys) ~ (ys ++ xs)01/06 23:47
dolioSo I ended up with [] ~ [], l ~ l' => x :: l ~ x :: l', l ~ l' => x :: y :: l ~ y :: x :: l', + transitivity.01/06 23:48
dolioWell, maybe I'll try that out then. That seems promising, I guess.01/06 23:49
pigworkerhow do you prove [1,2,3] ~ [3,2,1] with that?01/06 23:49
dolioI don't know off hand. It'd take me a while.01/06 23:50
dolioIt'd involve lots of transitivity.01/06 23:50
dolio[1,2,3] ~ [2,1,3] ~ [2,3,1] ~ [3,2,1] I guess that's not so bad.01/06 23:50
pigworkerah, I see where the transitivity comes in: it lets you swap later in the list01/06 23:51
dolioYes.01/06 23:51
edwinbyes, that's the definition I have01/06 23:52
edwinbJames' sounds neater though01/06 23:52
pigworkerit's kind of canonical: it's the least equivalence which respects the constructors and makes ++ commute01/06 23:54
--- Day changed Wed Jun 02 2010
dolioWell, this certainly doesn't seem easy to prove transitivity for.02/06 00:11
soupdragonhttp://pierre-yves.strub.nu/research/coqmt/02/06 00:26
soupdragonchck this out guys02/06 00:26
soupdragon  Fixpoint append n₁ n₂ (xs₁ : dlist n₁) (xs₂ : dlist n₂) : dlist (n₁ + n₂) :=02/06 00:26
soupdragon  match xs₁ in dlist n₁ return dlist (n₁ + n₂) with02/06 00:26
soupdragon  | nil => xs₂02/06 00:26
soupdragon  | cons n₁ x xs₁ => cons x (append xs₁ xs₂)02/06 00:26
soupdragon  end .02/06 00:26
soupdragonit's doing an arithemetic descision procedure in the conversion rule02/06 00:26
pigworkerAfter last night's chat with dolio, I cooked this up: http://personal.cis.strath.ac.uk/~conor/fooling/PCon.agda02/06 11:55
pigworkerIt's a DSL for writing recursive functions which rearrange containers. E.g., insertion sort.02/06 11:56
pigworkerI'd better prove a theorem about it.02/06 11:56
pigworkerfor added comedy, I wrote mergesort too02/06 16:02
ccasinanyone know if there is a size limit to the number of fields in an agda record?02/06 16:09
ccasinI'm seeing really odd behavior dealing with big ones02/06 16:09
pigworkeryou get the gratuitous eta-expansion penalty?02/06 16:26
ccasin:)02/06 16:26
ccasinno, 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
ccasinI'll email the list, I guess02/06 16:27
ccasin*give an error02/06 16:27
pigworkerif you chunk your record, is it ok?02/06 16:28
ccasinhmm, yes!02/06 16:30
ccasinthanks, I guess I'll just do that02/06 16:30
ccasinthough sane modules and records sure would be lovely...02/06 16:30
npouillardccasin: can you nest the two last as an inner record and then "open public" it02/06 16:31
ccasinnpouillard: 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 great02/06 16:42
ccasinthough, why it didn't work in the first place remains a mystery02/06 16:42
npouillardsure this is just a workaround02/06 16:42
npouillard(it deserve a bug report)02/06 16:42
ccasinturns out it was some kind of memory bug02/06 19:16
ccasinthe ghc buffer reveals a stack overflow02/06 19:16
ccasinI guess I won't use agda to write my certified space airplane controller just yet02/06 19:17
soupdragonso who here is interested in CoqMT02/06 20:50
soupdragonnobody in #coq is talking to me02/06 20:50
danharajwhat is coqmt02/06 21:03
soupdragonit adds descision procedures to the conversion rule02/06 21:05
danharajI am not sure what that is, I am not good at Coq/Proof Assitants.02/06 21:06
soupdragonyou know how02/06 21:10
soupdragonsay you have a function02/06 21:10
soupdragong : f 3 -> X02/06 21:11
soupdragonif x : f 3 then obviously g x : X02/06 21:11
soupdragonbut if f : f (1 + 1 + 1)02/06 21:11
soupdragonoops02/06 21:11
soupdragonbut if y : f (1 + 1 + 1)02/06 21:11
soupdragonyou can still do g y : X02/06 21:11
soupdragonbecause 1 + 1 + 1 is convertible with 302/06 21:11
soupdragonso it allows equal things wrt. beta reduction, pattern matching, stuff like that...02/06 21:11
soupdragonbut modulo theories adds more decision procedures to the conversion02/06 21:12
danharajah, like what?02/06 21:12
pigworkerOh 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
Saizanhah, on permutations?02/06 23:22
pigworkerindeed, a claim about resources02/06 23:29
pigworkerit's looking like a strict record constructor pattern problem02/06 23:29
--- Day changed Thu Jun 03 2010
danharajWhat is the formal framework underlying Agda, like the way Coq is based on the calculus of inductive constructions.03/06 02:54
dolioIt's rather like Martin-Loef type theory.03/06 02:57
dolioAt least, from what I understand of the latter. I've not looked into it very closely.03/06 02:57
danharajhmm03/06 02:57
danharajand would you be familiar with the underpinnings of Epigram, dolio? I heard it was similar to Agda.03/06 02:58
dolioThey're somewhat similar, yes.03/06 02:59
dolioBut you remove the intensional identity types, and build an alternate extensional equality very carefully.03/06 03:00
dolioEpigram as currently implemented has Set : Set, but they're eventually going to change that.03/06 03:01
Saizandolio: tried using Data.List.Any.BagAndSetEquality for permutations, btw?03/06 15:29
pigworkerHail the Miller man! I'm astonished at what Agda is happy to infer.03/06 21:05
pigworkerI say that, then I break it. One for Ulf to look at.03/06 21:17
pigworkerI'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
soupdragonwhat's S?03/06 21:19
soupdragonoh sorry03/06 21:19
soupdragonI know what that is03/06 21:20
pigworker_S_ is \ f s g -> f g (s g)  ... but its type is not its Hindley-Milner type, har har03/06 22:24
soupdragonI was thinking of streicher K axiom and wondering if there was an S axiom before I realized03/06 22:24
pigworkertoo many Ks03/06 22:24
--- Day changed Fri Jun 04 2010
pigworkeris it my imagination, or am I not allowed pattern matching in a let?04/06 01:10
dolioIt is not your imagination.04/06 01:10
doliolets are rather restricted.04/06 01:11
pigworkerI'm not imagining that I can't make a \ scope over a where, either04/06 01:11
dolioI 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
dolioNon-recursive, too, I think.04/06 01:13
pigworkercan't think why, if I'm willing to give a signature04/06 01:13
dolioAnd its semantics are inlining the definitions, I think.04/06 01:13
pigworkerno sharing?04/06 01:13
dolioI don't know about that. If it does share, then change my statement to it being a beta redex.04/06 01:14
dolioAlso as I understand it, where is sugar for an anonymous module.04/06 01:16
dolioI'm not sure if that answers your question about it.04/06 01:16
pigworkerI just lambda-lifted my where clause; least evil option04/06 01:16
nappingThat can be bad if the type signature is large04/06 01:27
nappingIt 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 hope04/06 01:28
dolioWell, Agda could use some way to do local pattern matching period.04/06 01:34
Saizanyeah, case statement would be nice even if it required some annotation04/06 01:35
dolioOnce you figure out what that construct is, you can work it into let and whatnot.04/06 01:37
nappingthat might be a bit harder. I was thinking you often end up needing pattern matching when refining holes04/06 01:39
nappingand to define an appropriate lemma you have to give a type signature, which is just copied from the inferred goal type04/06 01:39
nappingI'm not sure you have such a convenient goal type on a let04/06 01:39
nappingChanging subjects, I'm wondering why some of my fonts have extra space under the line04/06 01:39
pigworkercase expressions are weird with dependent types04/06 01:39
nappingemacs finds something with a nice ⊸ and 𝔟 but both are considerably taller than normal lines04/06 01:40
nappingthe fraktur b is not so important, but ⊸ is nice for linear types (I04/06 01:40
dolioYeah, that happens with a lot of glyphs.04/06 01:40
nappingI'm trying to implement a checker for Fluet's rgnURAL, or something like it)04/06 01:41
pigworkerI remain an ASCIIist. I can 't cope with tex input mode04/06 01:41
nappingpigworker: I'm thinking of leaning very heavily on the existing support04/06 01:43
nappingbasically, just let you abbreviate lemma : type; lemma <alts>; theorem = ... lemma ...04/06 01:43
nappingby something like theorem = ... (case <alts>) ..., which fills in the type of the lemma from the inferred type of that position as if it were a hole04/06 01:43
nappingdo you know of agda-input-add-translations and agda-input-translations?04/06 01:44
dolioThe font weirdness might be due to glyphs from several different fonts getting pulled in.04/06 01:44
dolioSome are probably taller than others for the same point size (even though that probably doesn't make any sense).04/06 01:44
nappingIt'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 TeX04/06 01:45
dolioPapers 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
pigworkernapping: at least the type-pushed-in should let you infer the type of a helper function04/06 01:47
nappingWell, I guess just letting you mix identifiers and operator characters in infix might get you farther, with -o and |- and the like04/06 01:49
nappingIt seems agda doesn't support arbitrary sections of mixfix operators04/06 01:49
nappingI suppose that's something to do with dependency? The papers on the parsing explain how to do it04/06 01:49
dolioThe alternative is presumably much more arduous. Type setting what people see while programming, while retaining mostly ascii.04/06 01:49
pigworkerdolio: yeah, it looks great when the fonts work out, but I just can't cope with typing it04/06 01:50
dolioI don't think it's a necessary limitation. They've talked about allowing sections.04/06 01:50
nappingM-x describe-char is a crucial ingredient04/06 01:51
nappingI 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 things04/06 01:51
dolioIt'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
dolioBut it hasn't been done yet.04/06 01:51
pigworkerIt'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
nappingAh, 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 paper04/06 01:54
soupdragonseems like a trivial issue04/06 01:55
pigworkerI write ascii Agda, then resurface it with lhs2TeX.04/06 01:55
nappingthat should be "that use fancy typography"04/06 01:55
pigworkerI got that. The ergonomics become important when you're still writing a program and a paper at 2am.04/06 01:56
nappingI like lhs2TeX. Not quite sure how to fit in Haddock comments if I wanted to, though04/06 01:56
pigworkeryeah, I don't see how they fit together04/06 01:57
nappinghow can I pattern match on a (Maybe (x == y)) to get a refl and unify the arguments?04/06 02:06
nappingI write Just refl and get an error about x /= y04/06 02:07
dolioWhat's the whole line look like?04/06 02:08
pigworkercan you use with?04/06 02:08
pigworkeror is it just that you need to write .x instead of y ?04/06 02:09
dolioThat's my theory.04/06 02:10
nappingoh, that's probably what I'm forgetting.04/06 02:10
pigworkerlooking at one thing tells you about other things; that's why case expressions are not ideal04/06 02:10
nappinghere's the with line: lookup-Γ v (ctx' , v' ܃ τ) with eqVVar v v'04/06 02:12
nappingoh, never mind04/06 02:12
nappingI'd changed (refl) to a variable to try matching later on the refl, and hadn't changed it back04/06 02:13
Saizanbtw, if you use C-c C-c to pattern match it'll insert dot patterns for you where appropriate04/06 02:13
pigworkerSaizan: exactly -- why keep a dog and bark yourself?04/06 02:14
pigworkerI must hack the emacs mode so I just need to click on a pattern variable to make that happen.04/06 02:15
Saizanheh, sometimes it barks at the wrong tree though, i.e. it might add patterns for implicit arguments even if that can be avoided04/06 02:15
nappinghow does that work with "with"?04/06 02:16
Saizanfoo x y | bar x y04/06 02:16
Saizan... | z = ?04/06 02:16
Saizanand then you C-c C-c RET z RET04/06 02:16
Saizanerr, one less RET, but i hope it's clear :)04/06 02:16
Saizanand the first | should be a with..04/06 02:17
nappingI looked for something like that, but didn't see any other mode commands, and C-c C-c doesn't accept expressions04/06 02:17
pigworkerI'd like a keystroke to make a with04/06 02:18
nappingpigworker: dogs are well and good, but it seems you still have to meow yourself04/06 02:18
nappingSaizan: that comes from exactly my case I think, where it was necessary to expand the ... and dot the appropriate arguments04/06 02:20
pigworkerThe ... is interpreted rather syntactically: it's promising that nothing has changed, where you might prefer to be able to not care what changes04/06 02:21
nappingI suppose it would be possible for the code under C-c C-c to try to reduce dots if in fact nothing changed04/06 02:24
nappingI don't even care to hid changes, it's just that it seems to unconditionally expand dots you have already written04/06 02:24
pigworkerI don't think C-c C-c is where Ulf's energies are focused.04/06 02:25
Saizani wouldn't expect them to be :)04/06 02:26
pigworkerironic, because it's the main thing in Epigram 1 which *did* work04/06 02:26
nappingNo, I would hope not. It's probably something I'd be competent to improve if I knew more elisp04/06 02:27
pigworkerI'm guessing the display form of the cases is chosen on the agda side, rather than the emacs side04/06 02:28
nappingThe emacs mode was quite snazzy04/06 02:29
nappingSpeaking of Epigram, is OTT still looking solid?04/06 02:29
pigworkerOTT is up and running, in principle, but grindingly slow in practice, for non-essential reasons04/06 02:31
Saizandid you get the model of bisimulation for coinductive types working?04/06 02:32
pigworkerwe're tuning it a bit just now04/06 02:32
pigworkerSaizan: well, something worked; I wonder where I put it04/06 02:35
nappingI 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 finesse04/06 02:37
pigworkerSaizan: I got this far http://personal.cis.strath.ac.uk/~conor/pub/JUnfold/Thm.agda04/06 02:39
pigworkerThe other files are in the same directory, but there's no accessible index. Grr04/06 02:39
Saizandarcs get solves that :)04/06 02:40
pigworkeryep04/06 02:40
Saizanehm, how much ram does it need to typecheck?04/06 02:42
pigworkerJudgmental 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
pigworkerIf 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
pigworkerSaizan: I never found out.04/06 02:45
pigworkerUlf 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
Saizan1.5GB weren't enough04/06 02:50
pigworkerScary04/06 02:50
pigworkerStill, nice problem to have.04/06 02:51
Saizanusing --no-termination-check doesn't seem to help though04/06 02:52
pigworkerhow odd; maybe Ulf was just guessing... https://lists.chalmers.se/pipermail/agda/2010/001702.html04/06 02:53
Saizanheap exhaustion again, maybe there's more than one problem04/06 02:58
pigworkeroh well, we'll just have to implement it directly04/06 03:01
pigworkerhey 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 over04/06 03:06
Saizanbut in epigram you'd use Desc instead of Comm/Resp, right?04/06 03:06
Saizanah, ok, good night :)04/06 03:07
pigworkerwe'd use IDesc, yes04/06 03:07
copumpkinanyone know of a simply typed lambda calculus implemented in agda?04/06 10:44
dolioSomeone posted pigworker's normalizer to the dependent types reddit.04/06 10:45
dolioBeta-normal, eta-long.04/06 10:46
copumpkinah04/06 10:46
copumpkinthanks04/06 10:47
copumpkinfound it04/06 10:47
npouillarddoes anyone know a trick to avoid to eta-expand implicit arguments of fields when building record values04/06 14:38
npouillardI keep doing record { f = λ {x} {y} → f {x} {y} ; ... }04/06 14:38
copumpkin≡-pred : ∀ (m n : ℕ) → suc m ≡ suc n → m ≡ n04/06 14:48
copumpkinannoying that the ≡ turns yellow between the two sucs04/06 14:48
copumpkinit seems like it should be able to work out that it's on a Nat04/06 14:48
npouillard... (ℕ ∶ suc m) ...04/06 14:50
npouillardshould do the trick04/06 14:50
Saizanoh, you can do that?04/06 14:50
copumpkinoh that's the backwards thingy04/06 14:50
copumpkinit's an operator defined somewhere, right?04/06 14:51
copumpkinI remember seeing it somewhere04/06 14:51
copumpkinin Function04/06 14:51
copumpkinnpouillard: my savior!04/06 14:51
copumpkinthanks :)04/06 14:51
Saizanah, : vs. ∶04/06 14:52
npouillardnp04/06 14:52
copumpkinI'm still puzzled why it can't figure it out though04/06 14:52
npouillardwhat your type of suc there ?04/06 14:52
copumpkinit's just the usual one from Data.Nat04/06 14:52
copumpkinit's a constructor04/06 14:52
Saizanand the other is from Fin?04/06 14:53
copumpkinhm?04/06 14:53
copumpkinnope it's all Nat04/06 14:53
Saizanyeah, but i think the problem is that you've another suc in scope04/06 14:53
copumpkinoh, I do04/06 14:53
copumpkinbut it seems like it should be able to disambiguate them based on the fact that n and m are both Nat04/06 14:54
npouillardthat's the point indeed04/06 14:54
npouillardI have this in some module without any glitch04/06 14:54
npouillardsuc-inj : ∀ {n m : ℕ} → suc n ≡ suc m → n ≡ m04/06 14:54
copumpkinah04/06 14:54
copumpkinis 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
copumpkinwhere m is actually suc m, since m could be 004/06 15:05
copumpkinI was looking at the nice inject functions but none of them injected what I wanted04/06 15:05
copumpkinso ∀ {m} → (n : Fin (suc (suc m))) → fromℕ (suc m) ≢ n → Fin (suc m) I think04/06 15:08
copumpkinhmm, I have an absurd negation being passed in04/06 16:03
copumpkin0 /= 004/06 16:04
copumpkinbut putting in an absurd pattern, agda can't spot (understandably) that it's empty04/06 16:04
copumpkinoh I guess I'll just use ⊥-eli04/06 16:05
copumpkinm04/06 16:05
copumpkingah, I messed up04/06 16:34
copumpkinoh no I didn't04/06 16:38
copumpkinokay, I have modular addition :P04/06 16:39
copumpkinsad that it took so long04/06 16:40
copumpkinand that it's so ugly04/06 16:40
pigworkertrouble with literate agda: you can't edit your paper while you're waiting for a type to check...04/06 18:12
copumpkincan 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
copumpkinI have something that works but it's terribly ugly04/06 19:19
copumpkinI can do basic proofs on it but I'm afraid that they'll get too painful later on04/06 19:19
pigworkerhave you defined suc?04/06 19:20
copumpkinyeah, that's where most of the ugliness was04/06 19:20
copumpkinthen the _+_ is the usual, using the "circular" suc04/06 19:21
copumpkinin the circular suc I use the decidable equality on Fin n to wrap it around04/06 19:21
pigworkerif you define the emb/max view, suc is easy04/06 19:21
copumpkinemb/max? :o04/06 19:21
copumpkinoh, found it04/06 19:22
copumpkinhttp://www.cs.nott.ac.uk/~txa/g53cfr/l04.agda ?04/06 19:23
pigworkerha ha, my browser didn't like that04/06 19:24
pigworkeryes, those are emb and max04/06 19:24
copumpkinokay, I'll play with those and see if I can simplify it a bit :)04/06 19:24
pigworkerI sometimes call emb "fweak"04/06 19:24
copumpkincause right now it's kind of ridiculous04/06 19:24
pigworkerexercises 13 and 21 of my AFP notes are the relevant ones04/06 19:25
copumpkinokay, will do those too! thanks :)04/06 19:25
pigworkermodular suc takes max to zero and (emb x) to (suc x)04/06 19:25
copumpkinbut I'll still need decidable equality to tax max to 0, I'd assume?04/06 19:26
copumpkinhttp://snapplr.com/3b4j is what I have04/06 19:26
pigworkerthat's what the emb/max view does: it analyses every fin as max or (emb x)04/06 19:26
copumpkinoh, I see, it's an actual view04/06 19:27
copumpkinokay, I see how it works I think04/06 19:27
pigworkergood luck04/06 19:28
pigworkerI really must port those notes to Agda04/06 19:28
copumpkinthanks :) this stuff is fascinating04/06 19:28
copumpkinthe difficulty of proofs really forces one to find elegant approaches to things04/06 19:29
pigworkermathematics is all about definition; proof is just macho posturing04/06 19:29
copumpkin:)04/06 19:30
copumpkinanyway, thanks for all the pointers, gonna go to dinner and then come back and try cleaning this mess up04/06 19:30
--- Day changed Sat Jun 05 2010
copumpkinI'm embarrassed to say that I'm having trouble with this emb/max view05/06 07:54
copumpkinoh, I think I have it05/06 08:17
copumpkin"Inaccessible (dotted) patterns from the parent clause must also be05/06 08:23
copumpkininaccesible in the with clause, when checking the pattern {suc _},05/06 08:23
copumpkinwhen checking that the clause"05/06 08:23
copumpkinpattern matching hates me05/06 08:32
* copumpkin has defeated the pattern matcher!05/06 08:37
copumpkinmuahaha05/06 08:37
copumpkinpigworker: it worked, thanks!05/06 10:11
copumpkintook me way too long to figure out05/06 10:11
pigworkergood stuff, but yeah, it's annoying writing patterns yourself05/06 10:24
copumpkinis 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
pigworkermore context might help, but it looks like you have max in an index, and it doesn't know how to solve unification problems involving max05/06 11:34
pigworkerthe usual escapes are (1) match on something which makes max compute (emitting a constructor), or (2) use with to abstract max05/06 11:35
copumpkinyeah, I have max in the index to that view type05/06 12:09
copumpkinhmm05/06 12:21
copumpkinis 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 proofs05/06 13:12
pigworkertry checking Shin-Cheng Mu's blog05/06 13:29
copumpkinhaven'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
copumpkinI mean, haven't found that particular PreorderReasoning stuff mentioned on his blog yet, but it contains many other interesting things05/06 13:47
copumpkinhmm, I feel like http://snapplr.com/s0ks could be cleaner05/06 15:17
copumpkinand that it's making my proofs more unpleasant05/06 15:17
copumpkinaww, this commutativity proof was almost so simple and elegant, but then something got in the way :(05/06 15:45
* copumpkin goes argh05/06 16:05
copumpkinman, dealing with Fin indices is a real pain in proofs05/06 16:16
Saizanbecause you've to unify them with non-constructors, or in general?05/06 16:21
copumpkinI have a lot of Fin (suc n)s that are a pain to unify05/06 16:36
copumpkinnot even sure where they all come from :P05/06 16:37
copumpkinah, it comes from use of zero05/06 16:39
copumpkinthe Fin zero05/06 16:39
copumpkinis a Fin (suc n), obviously05/06 16:39
copumpkinbut some other properties are Fin n05/06 16:40
copumpkinI guess I could just move everything to Fin (suc n) since I don't really need to deal with the empty case05/06 16:51
copumpkinfeels ugly though05/06 16:51
npouillardcopumpkin: I might make sense05/06 16:52
copumpkinyeah :/05/06 16:52
npouillardIf you see Fin as "finite sets", then some properties will require a non-empty one05/06 16:53
copumpkinit 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 anyway05/06 16:53
copumpkinor less clean, I might say05/06 16:53
copumpkinsince because Fin 0 is uninhabited it would make no difference whatsoever05/06 16:54
npouillardOk, I see.05/06 16:54
Saizanah, true, i often have have a "zero () .." case in proofs involving Fin05/06 16:54
copumpkinand moving everything into Fin (suc n) is breaking my very carefully crafted complicated pattern matches that took ages to get right05/06 16:55
copumpkin:P05/06 16:56
copumpkinthings like succ {suc .(suc n)} .(emb i) | vemb {n} {i} y = suc i05/06 16:56
copumpkinthose things are so painful to get right and even C-c C-c fails on them05/06 16:57
npouillardcan't you replace .(suc n) by ._ and .(emb i) by ._ as well05/06 16:57
copumpkinomg05/06 16:57
copumpkinthank you :P05/06 16:57
copumpkinwell that cleaned up some of the cases05/06 16:59
copumpkinstill breaks in a non-trivial manner when I change it to Fin (suc n) though05/06 17:00
npouillardcopumpkin: 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
copumpkinwell, hmm05/06 17:02
copumpkinI have something like05/06 17:02
copumpkin(succ max | view max) + zero ≡ zero05/06 17:02
copumpkinthat's my goal05/06 17:02
copumpkinso I think, oh RightIdentity for _+_05/06 17:02
copumpkinoh wait05/06 17:03
copumpkinthat makes no sense, sorry05/06 17:03
copumpkingot confused with another case05/06 17:03
copumpkinokay, so I have +-comm to show commutativity of _+_05/06 17:05
copumpkinI 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 now05/06 17:05
copumpkinhowever, it won't accept a recursive call to +-comm05/06 17:05
copumpkinbecause the Fin indices on one are suc n and on the other it's n05/06 17:06
copumpkinnot sure if that makes sense05/06 17:06
npouillardYou are proving +-comm on Fin?05/06 17:14
pigworkerIs there a way to inherit +-comm from Nat?05/06 17:17
* npouillard was asking itself the same thing05/06 17:18
pigworkerWould it help to prove + is a hom?05/06 17:18
copumpkinit sure would be nice :)05/06 17:29
copumpkinI'd love to steal the +-assoc one too, since it looks harder for the Fin case05/06 17:30
copumpkinbut I can't really show that my _+_ is related to the Nat one05/06 17:30
copumpkinat least I have a trivial +-identity :P05/06 17:30
copumpkinI was hoping to build up to finite fields but given the difficulty I've had so far it seems unlikely :)05/06 17:31
copumpkinbut I refuse to give up until I at least have a group addition05/06 17:33
copumpkinrepresenting the prime power condition for multiplicative inverses and such will be for when I'm better at this stuff :P05/06 17:34
copumpkinoh no, the mysterious w term is biting me05/06 18:48
copumpkinI have a problem!05/06 23:38
copumpkinjust for a change05/06 23:38
copumpkinMy 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 n05/06 23:38
copumpkinI'd normally break up the cases so it can see through the n ! that it's always a suc n05/06 23:39
copumpkinbut this is in a type05/06 23:39
copumpkinis there a standard approach to that?05/06 23:39
pigworkercan 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
copumpkinI was thinking of that, but my issue is that this is something I want to prove, so it's sitting in a type05/06 23:46
copumpkinI guess I'll need some sort of meta-type for the proof to satisfy it05/06 23:46
pigworkerbut with abstracts from types05/06 23:46
copumpkinhmm05/06 23:48
copumpkineven in something like http://snapplr.com/q56b ?05/06 23:48
copumpkin(sorry if I'm being thick)05/06 23:49
pigworkerI see what you mean by "in a type" now. You'll need to write a program to compute that type.05/06 23:51
copumpkinah okay, I think I know how to do that05/06 23:51
pigworkeror 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
pigworkerwhere pred x depends on the proof05/06 23:53
--- Day changed Sun Jun 06 2010
copumpkinhmm, something like http://snapplr.com/gn3t ?06/06 00:04
copumpkinsuperfluous parentheses there06/06 00:05
copumpkinoh maybe I'm doing it backwards06/06 00:14
copumpkinyeah, duh06/06 00:15
pigworkerthat'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
copumpkinah, I think I see06/06 00:33
copumpkinI'll try some more in the morning :) just proved that ∀ n → n ! ≢ 0, at least :P06/06 00:33
copumpkinthanks again06/06 00:33
copumpkincan I not pattern match on _,_ in a lambda?06/06 08:34
dolioYou can't pattern match at all in a lambda.06/06 08:34
copumpkinoh, okay06/06 08:35
copumpkinboo06/06 08:35
copumpkincan you think of any succinct way of stating that a vector has no duplicates?06/06 08:41
copumpkinI have an ugly approach that uses an All and the selections function ([a] -> [(a, [a])]) on vectors06/06 08:41
SaizanInjective (\ i -> lookup i v) ? fsvo Injective06/06 08:44
copumpkinfsvo?06/06 08:44
copumpkinoh I see06/06 08:44
Saizanfor some value of06/06 08:44
copumpkinhmm, that could work06/06 08:44
copumpkinyeah06/06 08:44
copumpkinthis agda stuff is too fun, pity I'm leaving my computer behind for a month tomorrow :( I want it on my ipad now06/06 12:55
AmadiroInstall linux on your iPad06/06 13:06
copumpkinnot 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 way06/06 13:07
Amadirocopumpkin, ah, too bad.06/06 15:03
benmachinewill I hurt myself if I try to learn agda in a non-emacs editor06/06 22:21
soupdragonomg06/06 22:21
soupdragonevery single newbies asks that06/06 22:21
soupdragonI wonder how many people I've coerced (by force) into using emacs06/06 22:22
npouillardbenmachine: I tend to survive after some viper configuration06/06 22:36
--- Day changed Mon Jun 07 2010
pigworkerMy 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
stevandolio: hi, mind making your CT stuff available again? i'd like to check something i recall having seen there.08/06 16:34
doliostevan: 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
stevanthanks!08/06 16:56
Saizanagda's type inference seems to take advantage of the injectivity of functions, nice08/06 22:14
Saizanpigworker: using IDescTT i managed to prove conOutLaw using only ~400MB of ram :) http://code.haskell.org/~Saizan/bisim/ObsEq.agda08/06 23:28
pigworkerlooks very good, and it's much closer to what we'd actually like to use than the indexed W-type encoding08/06 23:32
Saizanyeah, quite more verbose though, but apparently simpler for agda08/06 23:40
Saizani should probably port it to universe polymorphism08/06 23:41
--- Day changed Wed Jun 09 2010
npouillardSaizan: 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
pigworkerSaizan: 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 injective09/06 12:07
pigworker(I think that's what's behind bug 246.)09/06 12:10
kosmikusI 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
pigworkerIt's something highly desirable (we want automatic quotation, right?) but I don't know what the issues were09/06 12:31
edwinbIdris used to do that, due to a silly error09/06 12:46
edwinbI think I made use of it a few times before I noticed ;)09/06 12:46
Saizannpouillard, pigworker, kosmikus, edwinb: http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26042#a2604209/06 14:41
pigworkerSaizan: interesting, because it's not doing the over-aggressive thing in that example09/06 14:58
Saizanyeah09/06 14:59
Saizanit's actually refusing to :)09/06 15:00
pigworkerSaizan: ha! try T true = T false ...09/06 15:06
pigworkerdoesn't termination-check (ha ha); is 'injective'?09/06 15:06
Saizanyeah, b gets inferred with that :)09/06 15:14
* Saizan was too optimistic09/06 15:14
pigworkerit just means the criteria are too loose09/06 15:15
pigworkerI wonder if it's just checking for different heads, rather than different *canonical* heads09/06 15:16
* pigworker plots next experiment09/06 15:17
pigworkerOK, it's not unifying (x + y) with (a + b) in the tempting way. Good.09/06 15:22
pigworkerIt does unify (x + y) with (x + ?). Good. _+_  is strict in first arg here, so that works.09/06 15:23
pigworkerIt doesn't unify (? + y) with (x + y). Good. You have to know more about _+_ to see why that would work.09/06 15:24
Saizanso 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
pigworkerSaizan: 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 = z10/06 17:40
Saizanpigworker: oh, i see10/06 17:45
Saizanthat 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 there10/06 17:50
Saizanwait, 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) case10/06 18:04
Saizani guess "Fast and Loose Reasoning is Morally Correct" doesn't apply to typechecking :)10/06 18:05
dolioYou still don't need to think about bottoms.10/06 18:17
dolioBecause there aren't any.10/06 18:17
dolioBut, 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
dolioOr else you sacrifice decidability of type checking.10/06 18:20
doliopigworker: 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
dolioAnd if so, what about Leibniz equality encoded in the usual way?10/06 18:28
dolio(Perhaps identity types are fancier than that, though; I haven't read much on Martin-Loef type theory proper.)10/06 18:29
dolioOh, 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
Saizanyup10/06 18:36
Saizansince you still have subst for it10/06 18:36
pigworkerdolio: Neel is correct10/06 18:49
pigworkerSaizan: I don't know what's implemented10/06 18:50
pigworkerbut yeah, T ? = T x doesn't make ? = x10/06 18:51
pigworkerevery 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 stuck10/06 18:56
pigworkerThe nut of ((x + y) + z) is x, for example.10/06 18:59
pigworkerIf 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
pigworkerOf course, this is a very intensional way of looking at things.10/06 19:03
dolioThat's good, though. It'll still be valid when homotopy lambda calculus conquers us all.10/06 19:08
pigworkerdolio: 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 equations10/06 19:12
pigworkerhomotopy lambda calculus seems to go even further, identifying sets up to iso, meaning that equality proofs really tell you computationally important stuff10/06 19:28
dolioWell, maybe. I've gotten mixed impressions.10/06 19:31
dolioThat 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
dolioAnd K is also out.10/06 19:32
dolioBut I like dependent pattern matching.10/06 19:33
pigworkerI must confess I don't know the details.10/06 19:34
dolioIt seems pretty early yet, though, so who knows where it'll end up.10/06 19:34
dolioI think it's more in people's heads than down on paper at this point.10/06 19:35
pigworkerYou 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
dolioAh.10/06 19:37
pigworkerK 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
dolioI see. So K was for getting an appropriate heterogeneous equality out of the homogeneous equality.10/06 19:48
pigworkerThat'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
pigworkerIt 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
pigworkerK as a computational principle, not an inert axiom, I should stress.10/06 20:00
pigworkerSozeau, 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
dolio:)10/06 20:03
ccasinwho (if anyone) proved it was safe to add K to CIC (or a similar system)?10/06 20:07
ccasinsafe in the sense of consistency of the logic10/06 20:07
pigworkerMartin Hofmann, effectively10/06 20:09
ccasinSo I guess K is included in his "groupoid interpretation" paper?  I've never read it (a little scared)10/06 20:10
ccasinor perhaps that's the whole point of the paper, scanning the abstract now10/06 20:11
pigworkerhe shows that a groupoid interpretation refutes K, so it ain't true in all models10/06 20:11
pigworkerbut it is true in an extensional model10/06 20:11
ccasinI see, thanks10/06 20:11
pigworkerso we know K is extra, but consistent10/06 20:12
ccasinyes, nifty.  I should learn more semantics, sometimes it feels all I know is syntax10/06 20:13
doliopigworker: Here's a follow-up question from earlier: wouldn't observational equality turn intensional identity types into observational identity types?10/06 20:27
dolioSince (\q -> subst q refl) : (x : S) = (y : S) -> I S x y10/06 20:28
pigworkerdolio: it would, and that's (a) why we no longer allow them, natively, and (b) how we encode them10/06 20:31
pigworkerobs. 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
pigworkerif refl is evidence of definitional equality, as is traditional, that's a hole below the waterline10/06 20:35
dolioOkay, 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
dolioBut assuming you could, the identity types would also be observational.10/06 20:36
pigworkeryeah, you can't help it; everything is as observational as your propositional equality10/06 20:39
--- Day changed Fri Jun 11 2010
doliopigworker: You around?11/06 14:41
pigworkerphysically, at least11/06 14:41
dolioI'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
dolioBut 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
dolioIs that supposed to not be allowed?11/06 14:42
pigworkerIndeed, that's not supposed to be allowed11/06 14:42
dolioAh.11/06 14:43
npouillardWhat's wrong with this particular example?11/06 14:45
pigworkerat 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 D11/06 14:45
dolioI'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
dolioBut I can see how it'd be bad theoretically.11/06 14:46
dolioU as a whole 'doesn't exist yet' during the definition.11/06 14:46
pigworkerAt the time you're defining the functor, you shouldn't be able to refer to its initial algebra.11/06 14:47
npouillarddolio: but in this particular definition T is not mutually def with U11/06 14:47
dolioWell, yes. But I can construct examples where it is, I think...11/06 14:47
dolioI can with induction-induction at least.11/06 14:47
dolioPerhaps not with induction-recursion.11/06 14:49
pigworkerok, yeah, that example isn't recursive, so there's no big deal11/06 14:49
pigworkerthe key question is "what's the functor?"11/06 14:50
doliohttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=26081#a2608111/06 14:53
dolioThere we go.11/06 14:53
pigworkeryep, that's wicked; but you say Pi is forbidden?11/06 14:56
dolioIf you try to add Pi, it will get caught by the positivity checker.11/06 14:57
npouillarddolio: is your × constructor really meaning a Simga type11/06 14:57
npouillard?11/06 14:57
pigworkerhmmm, how to make this behave badly..?11/06 14:58
dolioBecause for "Pi : (s : U) (f : T s -> U) -> U", then you have "Pi u : (U -> U) -> U".11/06 14:58
dolionpouillard: 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
npouillardOk, because the Sigma is caught as well11/06 14:59
dolioYes, trying to add sigma types to the universe has the same problem as pi types.11/06 15:00
dolioOr W types.11/06 15:00
npouillardhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=26081#a2608211/06 15:00
dolioThey all have codes with the same type.11/06 15:00
dolioWhich leads to (U -> U) -> U.11/06 15:01
dolioOf course, I'm not certain that's actually a problem.11/06 15:01
dolioThat sort of definition is essentially how you define an impredicative object language LF-style.11/06 15:02
dolioOr maybe it's an indication of impredicativity being evil. :)11/06 15:03
pigworker(U -> U) -> U is a problem if you have a strong function space11/06 15:04
pigworkerwhich the LF deliberately doesn't11/06 15:04
dolioWhat's strong mean in this context?11/06 15:05
pigworkerHere "strong" means "permitted to inspect arguments, not just place them"11/06 15:06
dolioAh.11/06 15:06
pigworkeryou know the classic wrong'un?11/06 15:06
dolioShould I file a report being concerned about IR universes with codes for themselves?11/06 15:15
dolioOr not bother unless I can figure out a way to prove false?11/06 15:15
dolioI suppose there may already be one.11/06 15:16
pigworkerworth a look, and if there's nothing already, you might ask on the list11/06 15:17
dolioNot many issues related to induction-recursion, at least.11/06 15:19
pigworkerseems not; trouble is they're just mutual definitions plus a checker, and it's easy to mess the checker up11/06 15:25
dolioYes.11/06 15:26
--- Day changed Sat Jun 12 2010
glguyI 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
glguyhttp://www.galois.com/~emertens/wfbuild/wfbuilder.html#67212/06 08:16
glguyI just like how it feels like it is built from the simplest core12/06 08:20
nappingHello, has anyone read Pouillard and Pottier's paper on name representation?12/06 21:34
nappingI'm having some trouble trying to reproduce their code12/06 21:35
nappingIn 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 a12/06 21:36
nappingThen I try to define size : {a} -> Tm a -> Nat function by structural recursion, but it seems I have to explicitly provide the world arguments12/06 21:37
nappingsize (Lambda {b} _ body) = 1 + size {b} body and so on12/06 21:37
ccasinI have looked at the paper, but am no expert12/06 21:42
ccasina couple things:12/06 21:42
ccasinyou can download the code from Pouillard's website12/06 21:42
ccasinand I believe it requires the darcs version of agda12/06 21:42
ccasinalso it looks like he is here12/06 21:43
ccasinnpouillard: ping?12/06 21:43
nappingConvenient, that. I am looking through the code online, but I haven't found the size example12/06 21:48
nappingI'm assuming red and yellow highlights are complaints about being unable to infer arguments12/06 21:49
ccasinred (I think it's "light salmon") means agda can't tell the function terminates12/06 21:49
ccasinyellow means it can't infer things12/06 21:49
nappingStrange. Even the constructors like App : Tm a -> Tm a -> Tm a12/06 21:50
nappingit highlights the recursive calls on the arguments.12/06 21:50
ccasincan you link me?12/06 21:51
nappinglink what?12/06 21:52
ccasinyou said you were looking at it online? if you link to the part you think is strange, maybe I can explain it12/06 21:52
nappinghttp://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/12/06 21:53
nappingThe size function on page 4 is the problem - I filled out the undefined things like World with ?12/06 21:54
nappingThat is, gave those things a definition earlier that was just ?12/06 21:54
nappingHere's my code http://hpaste.org/fastcgi/hpaste.fcgi/view?id=26108#a2610812/06 21:54
ccasinoh, yes, sorry, I misunderstood12/06 21:55
ccasinOK, I'll have a look12/06 21:55
nappingThat might be the problem - type constructors are injective, but random definitions may not be12/06 21:57
ccasinhmm, yes, it seems odd that agda can't figure out the implicit argument on size12/06 21:57
ccasinshould be able to get it from the type of l and r in that case12/06 21:58
ccasinand filling it in makes the yellow/pink go away12/06 21:58
nappingWell, redefining World as a data type seems to make it work12/06 22:00
nappingI have no idea why, it should just need to unify variables of type World12/06 22:00
ccasinah, even just giving world an arbitrary definition12/06 22:01
ccasinlike nat12/06 22:01
ccasinmakes the problem go away12/06 22:01
ccasinagda must be hesitating because it doesn't know what type to infer.12/06 22:01
nappingIt also works if I make a record with fields like World, and a module parameterized over such a record12/06 22:05
nappingnpouillard: 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 shadowed12/06 22:23
nappingHello. I just got around to putting up a comment12/06 22:51
nappingawaiting moderation, it says.12/06 22:51
nappingIn 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 012/06 22:53
nappingnpouillard: I suppose that implementation does not work in a system that strongly enforces alpha equality12/06 23:13
pigworkernapping: 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 property12/06 23:16
pigworkerI gotta go, I'm afraid.12/06 23:17
--- Day changed Mon Jun 14 2010
glguyIs there a reason that _≤′_ is not implemented as:data _≤′_ (m : ℕ) : ℕ → Set where14/06 18:33
glguy  ≤′-refl : m ≤′ m14/06 18:34
glguy  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n14/06 18:34
glguyInstead of: data _≤′_ : ℕ → ℕ → Set14/06 18:34
glguyIt seems like the extraneous index just leads to additional dotted patterns14/06 18:35
pigworkerain't no good reason I can see14/06 18:35
glguyI suppose you have to be careful in interpreting double negation when talking to constructive logic people14/06 18:36
dolioIt makes more of a difference for equality.14/06 18:38
glguydolio: Could you elaborate a bit? My simple understanding is that I should make arguments parameters over indexes when possible14/06 18:39
dolioThere are two ways to define equality.14/06 18:39
dolioOr, more than two, but you get the idea.14/06 18:39
doliodata _==_ {A : Set} : A -> A -> Set where refl : forall {x} -> x == x14/06 18:40
dolioAnd one where you move one A to a parameter.14/06 18:40
dolioThe latter lets you do data _==_ {A : Set i} (x : A) : A -> Set where refl : x == x14/06 18:41
dolioWhich is interesting, because it lives in Set despite being equality for sets in arbitrarily large universes.14/06 18:41
dolioAnd they have slightly different interpretations and induction principles.14/06 18:42
dolioThe first one is 'the least reflexive relation on A', I think.14/06 18:42
dolioWhile the latter is something more like "the least predicate that x satsifies", but parameterized by x.14/06 18:44
dolioThe latter might actually have K as its induction principle. I'm not sure.14/06 18:47
glguyI was able to follow what you wrote up to this last line14/06 18:48
dolioI read some paper discussing this not long ago. Perhaps one of Dybjer's on inductive families.14/06 18:48
dolioK is the principle that all proofs of x == x are refl.14/06 18:48
dolioInstead of the usual J elimination where given x == y and P x, you can produce a P y.14/06 18:49
Saizan"K : forall x P -> P (refl {x}) -> forall y -> (eq : x == y) -> P eq" ?14/06 18:52
dolioOh, no, I'm wrong.14/06 18:52
dolioThe latter has J as its elimination rule.14/06 18:52
dolioAnd the former has a more complex rule that Martin-Loef uses.14/06 18:53
dolioOr, maybe J is the Martin-Loef one.14/06 18:53
pigworkerJ is the Martin-Loef one.14/06 18:53
pigworkerThe more parametery one is due to Christine Paulin-Mohring.14/06 18:54
dolioAnyhow, 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 y14/06 18:54
dolioFor 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
pigworkerthat sort of thing, but I'd expect dependency on the proof, too14/06 18:56
dolioMe too, but I don't see it here in Dybjer's paper.14/06 18:56
pigworkerWe 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
dolioThat'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
pigworkerYeah, 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
pigworkersorry, R x x (refl x)14/06 19:00
dolioI suppose, arguably, it's rather like having the eliminator for unit take a set, rather than a predicate on unit.14/06 19:03
pigworkerYeah, but unit is mostly ok with a lazy nondependent eliminator.14/06 19:29
pigworkerunless you're trying to prove that all elements of unit are equal, of course14/06 19:30
doliopigworker: 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
pigworkerheh, it keeps getting hacked to shut it up14/06 19:43
dolioI looked through the changelogs, and there were a couple changes related to the guardedness-preserving type constructor stuff.14/06 19:44
dolioSo that's probably what the difference is.14/06 19:44
nappingnpouillard: hello?14/06 20:36
nappingpigworker: are you here?14/06 20:38
nappingIt's a bit late in UTC+0, isn't it.14/06 20:38
benmachinenapping: about quarter to eight, I think?14/06 20:51
--- Day changed Tue Jun 15 2010
nappingwhat font do you use for \[[?15/06 00:16
nappingHow can I find which fonts on my system could supply characters?15/06 02:27
nappingemacs seems to like -unknown-Asana Math-normal-normal-normal-*-20-*-*-*-*-0-iso10646-1 which has a hideous amount of whitespace below the line15/06 02:28
Saizanno 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
Saizancopied it off some website ages ago, yay for knowing what you're doing :)15/06 02:31
nappingI don't use emacs in a terminal, but that helped. I just installed Kochi gothic and removed Asana, and it's much better15/06 02:37
nappingThat mixfix unicode syntax is nice.15/06 02:38
Saizanyup, quite sweet15/06 02:39
nappingI'm playing along at home with Conor's latest paper15/06 02:39
Saizanwhich one?15/06 02:40
napping"coincidences"\15/06 02:40
Saizanah, i've played a bit with the code too15/06 02:42
Saizani meant to define Any/All as ornaments over Nat or List but i got distracted :)15/06 02:43
dolioI played some, too, although I went with LF sort of HOAS.15/06 02:44
dolioAll that context stuff is too much work.15/06 02:44
Saizanwhich context stuff?15/06 02:46
dolioDefining contexts, and terms with de Bruijn indices.15/06 02:47
dolioAnd all kinds of combinators to mangle contexts so your types don't look quite as awful.15/06 02:48
nappingHow do you do a proper HOAS?15/06 02:48
nappingIsn't -> a bit too computational in Agda?15/06 02:48
dolioYeah, probably.15/06 02:49
dolioI just didn't worry about it.15/06 02:49
dolioI've been thinking about how to do better.15/06 02:49
nappingChlipala's PHOAS seems to work pretty will in Coq15/06 02:50
dolioThinking about something like PHOAS, but I'm not sure you can make that work with dependent types.15/06 02:50
dolioAnd I'm not sure the fix I'm thinking about doesn't just reintroduce the inadequacy.15/06 02:51
Saizan(ah, i was thinking of OAAO where i couldn't find any de brujin indexes)15/06 02:53
nappingIt seems the idea is to make a shallow embedding of the language and use it to index a deep embedding.15/06 03:27
nappingbut I don't see how that would help anything15/06 03:28
dolioIt means your terms and types don't have to be inter-defined.15/06 03:52
dolioAt least, less so.15/06 03:53
* BMeph has HOAS in different Area Codes...15/06 03:53
dolioFirst you define semantic types, then you define syntactic terms indexed by semantics types.15/06 03:54
dolioAnd, if applicable, a predicate that specifies which semantic types are denoted by syntactic types.15/06 03:54
nappingso you let the parent function space stand in for terms in the definition of dependent types?15/06 03:56
nappinghmm, Conor does like the ASCII art boxes. Cute ----------- syntax15/06 03:58
dolioIt's like Epigram.15/06 03:58
Saizanif 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
dolioI wouldn't expect that to be easier than searching for proofs of P.15/06 18:01
dolioBut maybe I'm wrong.15/06 18:01
glguyIs there a way to determine or distinguish agda's evaluation order with a program that passes the termination checker?15/06 18:13
dolioThere shouldn't be.15/06 18:14
dolioIf you find one, it's probably a bug.15/06 18:14
dolioI'm pretty sure the evaluation order is lazy, though.15/06 18:17
dolioOr something non-eager.15/06 18:17
kosmikusafaik, there's more or less no sharing15/06 18:22
dolioThat sort of thing is harder to determine.15/06 18:23
dolioHaving 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
dolioBut writing the application case like 'eval (f `Ap` x) stk = eval f (eval x : stk)' is non-strict.15/06 18:26
kosmikuseval x should get a stack as well, but yes15/06 18:31
dolioOh, right.15/06 18:32
--- Day changed Wed Jun 16 2010
nappingThis book seems to be a bit stale - looks like Source.fromFile(_).getLines doesn't leave the terminator any more16/06 01:21
ezyangI'm trying to understand when you need to declare implicit arguments.16/06 03:45
ezyangfor example, in the tutorial, _::_ for Vec starts off with {n : Nat} -> A -> Vec A n -> Vec A (suc n)16/06 03:46
ezyangit 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
dolioBecause 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
Saizanyeah, there's no implicit generalization like in haskell16/06 03:53
ezyangOh, these are quantifications!16/06 03:53
ezyangThat makes a bit more sense.16/06 03:53
ezyangCan I override an implicit parameter?16/06 03:53
dolioYou can apply it explicitly.16/06 03:53
doliofoo {n} x y16/06 03:54
ezyangintruiging.16/06 03:54
doliobar {m} {n} x y16/06 03:54
ezyangThough 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
dolioOccasionally it's necessary.16/06 03:55
* ezyang suspects he won't need it to understand Quicksort in Agda. 16/06 03:55
dolioAlthough 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
ezyang*nod*16/06 03:56
dolioAnyhow, Agda does all the type/term passing GHC has to do behind the scenes.16/06 03:56
dolioExplicitly in the language.16/06 03:56
ezyangAnother thing I'm not quite clear about is why I want to parametrize by some types and index by others16/06 03:56
dolio{} just lets you not have to write it in yourself.16/06 03:56
dolioAlthough you can also have it try to infer explicit parameters with 'foo _ _ x y'.16/06 03:57
ezyanghuh, interesting.16/06 03:57
Saizanparameters 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
dolioIndices don't directly count to the size of the type, either.16/06 04:02
ezyangOk, so suppose I have data _<_ (m:Nat) : Nat -> Set where16/06 04:02
dolioOnly if you quantify over them in constructors (which you often have to).16/06 04:02
ezyang<-base : m < suc m16/06 04:02
ezyang<-step : {n : Nat} -> m < n -> m  < suc n16/06 04:02
ezyangCAn I pop the {n : Nat} to be a parameter? Would it be clearer to do so?16/06 04:02
dolioNo.16/06 04:03
dolioIf it were a parameter, the result of all the constructors would have to be 'm < n'.16/06 04:03
ezyangHuh.16/06 04:04
ezyangoh, so because m is a parameter, all of these are m<_. I see what they did there...16/06 04:05
ezyangI guess it would have been clearer for me as something like: data m<_ (m : Nat)16/06 04:05
dolioYou can think of parameters as being quantified outside the datatype. For instance you could use parameterized module.16/06 04:06
dolio'data Foo (A : Set) (x : A) : Set where ...' versus 'module (A : Set) (x : A) where { data Foo : Set where ... }'.16/06 04:07
dolioIt's not quite that simple, because that doesn't take nested types into account.16/06 04:07
ezyangmmmm, clever.16/06 04:08
dolioI forgot a module name, but you get the idea.16/06 04:08
ezyangSo, what does it mean for me to say something like a </ b = a < b -> _|_?16/06 04:09
ezyangThe feeling I get is that my function is producing a type, but this seems odd.16/06 04:10
ezyangoh wait16/06 04:10
ezyangThat's exactly what it's doing. d'oh16/06 04:10
dolioIt's producing a value of the empty type.16/06 04:10
ezyangdolio: ... really?16/06 04:11
dolioWell, not really. It must be the empty function, and a < b must also be empty.16/06 04:11
ezyangRight; but it is inhabited if a < b is empty16/06 04:12
Saizan_</_ is a function from to Nat's to a type16/06 04:12
Saizan*two Nat's16/06 04:12
dolioIf a < b is empty, then a < b -> _|_ is inhabited by the empty function.16/06 04:13
ezyangok, cool, I'm not too far off into teh weeds.16/06 04:13
dolioa < b -> A for any A is, too.16/06 04:14
ezyangAw, Agda doesn't support blackboard bold as Nat16/06 05:05
ezyangor, at least, it needs an import I don't know about16/06 05:07
ezyangAh, I'm missing the stadnard library16/06 05:12
ezyangI 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
ezyang(error message points to open WF ...).16/06 05:58
ezyangOh, 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
ezyanghttp://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
pedaganddoes anybody know a companion paper for the Voevodsky's file sent by Thorsten on the mailing list?16/06 15:45
ccasinI do not know precisely how related it is to that development16/06 15:48
ccasinbut this is a paper relating to a talk about the equivalence axiom in question:16/06 15:48
ccasinhttp://www.math.ias.edu/~vladimir/Site3/home_files/CMU_talk.pdf16/06 15:48
ccasinthough you probably already found it on his website...16/06 15:48
ccasinalas, it seems the paper doesn't mention extensionality16/06 15:50
ccasinthough most of the file is directly related to the content of the talk16/06 15:52
pedagandha, thanks! (note for self: google is in the top-right corner of the web-browser, not in the "xchat" window :-) )16/06 15:55
ccasin:) no problem16/06 15:55
ccasinI 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
ccasinbut maybe you'll have better luck than me16/06 15:56
pedagandwell, I've no hope of understanding this thing. But the "universe polymorphism" battle is of practical interest for me.16/06 15:59
pedagandSo, I was hoping to understand just enough to port that stuff in my system. Looks like it's hopeless, tho :-)16/06 15:59
ccasinI also thought that was interesting - I have never run up against problems with the universe checker that weren't genuine problems16/06 16:01
ccasinare there well known examples?16/06 16:01
pedagandthe Agda library before "--universe-polymorphism", no?16/06 16:04
pedagandthe problem being that you have to duplicate code every time you need the same stuff but in a higher universe16/06 16:04
ccasinI was thinking of coq, since that's where Voevodsky's file was written16/06 16:04
pedagandI think that's what he complains about in the Coq file16/06 16:05
ccasinwell, I agree this problem existed in Agda16/06 16:05
ccasinbut I am surprised to see he ran up against it in coq - usually the universe checker there has left things "unresolved enough" for my purposes16/06 16:06
ccasinthen again, I guess I do more proving and less programming in coq16/06 16:06
pedagandso far, Coq has no form of universe polymorphism, hence being in the pre-"--universe-poly" era, I suspect16/06 16:06
ccasinis this right?  I thought coq had universe polymorphism a la Harper and Pollack16/06 16:08
ccasinindeed, it does - you just write "Type" and it works at any level16/06 16:08
ccasindifferent than agda in that the universes are nicely hidden from you16/06 16:09
pedagandthere are several calculus in Harper-Pollack, I doubt they implemented the real polymorphic one, in which we would work with principal types16/06 16:13
pedagandbut, honestly, I've not experimented with it16/06 16:13
pedagandI'll have to spend some time understanding what they have now, what they are working on16/06 16:14
pedagandsome time ago, I was pointed to that: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=229816/06 16:14
ccasinObserve that this passes the coq checker:16/06 16:15
ccasinhttp://hpaste.org/fastcgi/hpaste.fcgi/view?id=26280#a2628016/06 16:15
pedagandUlf also implemented a variant of Harper-Pollack in some stage, but I've been told it was really really slow (?)16/06 16:15
ccasinlooks like lists work at different universes to me16/06 16:15
ccasindoesn't that count as universe polymorphism?16/06 16:15
ccasinthanks for the link, though - I am very interested to learn what they have actually implemented16/06 16:16
pedagandindeed, 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
ccasinIn coq?  This is tricky, since you can't tell it to work at a particular Type level16/06 16:21
ccasinat best you can force it to be above some fixed level (or above the level of some other term)16/06 16:21
ccasinyou just write "Type" and it figures out which "Type n" you meant16/06 16:21
pedagandok, I see16/06 16:22
ccasinBut, considering that, the answer should be yes16/06 16:22
ccasinf's type is really:16/06 16:22
ccasinf : Set n -> Set n   (n >= 0)16/06 16:22
ccasin(well, Type n -> Type n.   Set means something different in coq - a universe below type)16/06 16:23
pedagandand that's polymorphism, indeed. Ok, then I'm really curious to know what prevents the file to go through! :-)16/06 16:23
ccasinyes, me too :)16/06 16:25
ccasinpedagand: I think I understand coq's restriction now16/06 18:43
ccasinit seems to be that coq can't instantiate defined terms at different universe levels in checking the same expression16/06 18:44
pedagandccasin, I'm lurking the #coq discussion, that's indeed interesting. Please explain! :-)16/06 18:44
pedagandok, so they do not have Harper-Pollack ultimate system16/06 18:45
ccasinpedagand: right16/06 18:45
pedagandthanks a lot of having asked, I would not have dared16/06 18:46
ccasinthings are perfect just so long as you don't demand that some definition be used at two different universe levels in the same expression16/06 18:46
ccasinmattam is always good about answering the questions of us mortals16/06 18:46
pedagandindeed, that's were real polymorphism is need, much as ML polymorphic functions16/06 18:46
ccasinyeah16/06 18:47
ccasinso I guess ulf's comments about efficiency make sense - that coq bug you linked suggests it's just too slow16/06 18:50
dolioThat's odd. I thought Coq could do things like 'List T :: Nil', which would have List at two different levels.16/06 18:51
npouillarddolio: but definitions is different from constructors16/06 18:51
dolioYes, 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
dolioBut the full judgment is '(List T :: Nil) : List Type', or what have you.16/06 18:53
pedagandgoodo, my system accepts the id/typeof mess. ccasin, you made my day! thanks again. :-)16/06 18:57
ccasinpedagand: no problem! does epigram have good universe polymorphism, or is this some smaller toy?16/06 18:58
dolioThe 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
dolioAgda's is new.16/06 18:59
pedagandit'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 asap16/06 19:00
dolioAlthough I like Agda's more. :)16/06 19:02
ccasindolio: interesting - I can't stand it!16/06 19:02
dolioAside from the fact that it doesn't have lifting into higher universes yet.16/06 19:02
ccasinit makes me do so much work16/06 19:02
dolio(With associated inference.)16/06 19:04
ccasinI find that just having all these extra arguments around is a big hassle16/06 19:05
ccasinin 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 of16/06 19:05
dolioYes, well, if you could lift into other universes, you'd only need to have one.16/06 19:06
ccasingood point16/06 19:06
ccasinthe lifting is pretty key, it really clutters code now16/06 19:06
dolioYes.16/06 19:06
ccasinso much so that I just use set-in-set16/06 19:06
nappingnpouillard: about your paper on naming, the example could be improved16/06 21:38
nappingnpouillard: 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
nappingnpouillard: 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 implementation16/06 21:58
nappingnpouillard: I'm not sure how to match the optimization of not recursing under a binder which shadows your variable, without losing alpha equivalence16/06 21:58
npouillardnapping: 1/ sure it could be improved, but we also tried to keep them short16/06 22:02
npouillard2/ We would like to be able to implement other data structures with a lower cost16/06 22:03
npouillardWe've not tried to write impelementation-specific ones though16/06 22:04
npouillard3/ Yes we couldn't find a way to express it in a safe way16/06 22:05
npouillardnapping: Thanks for your remarks BTW16/06 22:05
nappingnpouillard: 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
nappingnpouillard: It sounds like the sort of thing that would be a huge pain to implement and not often useful, though16/06 22:15
npouillardnapping: We tried hard not require proofs from the user, but that may be a solution16/06 22:17
nappingHowever, providing specialized versions of environments with the implementation seems likely to let you implement environments as efficient tree maps16/06 22:18
npouillardnapping: 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 small16/06 22:20
nappingI don't see any instances of pattern matching on the append, outside of the definition of export*<-16/06 22:22
nappingThe 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 primitives16/06 22:24
npouillardnapping: sure but the paper shows only a small part of the Agda developpement16/06 22:24
npouillardWe also want to formalize that each primitive is sounds (fits the logical relation) and so we wanted to keep it small at first16/06 22:25
nappingYes, you seem to have done that.16/06 22:26
npouillardThe theorem that each prim is sound is only done on paper16/06 22:27
nappingIt 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 primtiives16/06 22:29
npouillardnapping: Indeed it make sense16/06 22:29
nappingI 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
benc__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
Saizan_in agda's emacs mode you can type \o to get that18/06 07:51
benc__but not in a plain source file?18/06 07:51
ezyang18/06 07:52
* benc__ wants to know if he can reasonably program agda using ascii rather than unicode, is really the bigger question18/06 07:53
benc__without changing my editing environment18/06 07:53
nappingI don't think the standard library provides ASCII synonyms18/06 07:54
nappinghmm, I'm not sure you can even provide synonyms for constructords18/06 07:55
nappingagda works fine, of course18/06 07:55
benc__hmm ok18/06 07:55
nappingbut what doesn't work in your environment?18/06 07:55
benc__I don't have a (dot) key on my keyboard18/06 07:55
ezyangMy understanding is you should really have a unicode input method if you want to write Agda..18/06 07:55
ezyangbenc__: linux?18/06 07:55
Saizan_you're going to miss out on quite a few things without the emacs mode18/06 07:55
nappingThat's what the emacs mode is for - \o turns into the dot18/06 07:56
benc__saizan: ok - maybe i'll play with that18/06 07:56
nappinger, the emacs input method at least18/06 07:56
* ezyang uses Xcompose 18/06 07:56
nappingthe emacs mode gives you tons of stuff like looking up types, showing the context for "?" goals, building pattern matching, etc18/06 07:57
Saizan_e.g. showing the types of the goals together with the context, optionally normalized18/06 07:57
benc__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 app18/06 07:57
benc__napping: yeah that looks neat. i'll play with it18/06 07:57
benc__ezyang: unless there's motivation not to, which the emacs mode here sounds like18/06 07:57
ezyangbenc__: Xcompose is for your X window manager.18/06 07:57
ezyangso, if you SSH somewhere, it'll still work.18/06 07:58
benc__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 putty18/06 07:58
* ezyang remembers the days of the portable apps and his trusty usb key 18/06 07:59
ezyangNow I just lug my laptop around everywhere.18/06 07:59
nappingthe input methods work on your target machine anyway, so the only question is if all the shells can display unicode18/06 07:59
nappingI know my linux terminals do fine18/06 07:59
benc__os x terms do ok too with fiddling18/06 07:59
benc__get confused a bout double-width characters18/06 08:00
nappingI don't think the library uses any of those, just a bunch of math18/06 08:00
benc__every few years I try out unicode again and find the experience "almost there, maybe next year" ;)18/06 08:00
benc__napping: yeah its mostly/only CJK that is double-width18/06 08:00
nappingwell, everything seemed to work when I wanted to try Agda.18/06 08:03
benc__of course, my big fear about messing round in emacs is that I'll get sidetracked into learning elisp.18/06 08:04
nappingwell, 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 that18/06 08:04
nappinghasn't happened to me yet18/06 08:05
dolioEverything built-in has ascii equivalents.18/06 08:08
nappingIs there any way to make an inductive type with ASCII equivalents for unicode constructors?18/06 08:09
benc__whats the problem there? that you have synonyms for constructors?18/06 08:09
dolioNot that I know of.18/06 08:09
nappingI don't think you can define things you can pattern match on18/06 08:11
benc__this tutorial I am reading says:18/06 08:26
benc__>There is a distinction between parameters and indices of a datatype.18/06 08:26
benc__is the difference there that constructors can produce objects with any index they want but the parameter is fixed?18/06 08:27
benc__a parameter18/06 08:27
ezyangbenc__: Lol, are you reading my blog post?18/06 08:28
benc__no18/06 08:28
benc__i will if you send me the url18/06 08:28
benc__http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf18/06 08:28
ezyangOh, now I remember where I read that18/06 08:28
ezyangYeah, it's in that tutorial. I remember reading that sentence :-)18/06 08:28
ezyanghttp://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/18/06 08:29
ezyangBased off of Mertens talk, which was basically "quicksort in Agda"18/06 08:29
ezyangsubtitle "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 installation18/06 08:32
benc__napping,ezyang: thats why I avoid moving away from my default edit environment ')18/06 08:32
benc__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
benc__it kinda seems like it can be done18/06 09:09
benc__i get a type checking error with this:18/06 17:10
benc__http://fpaste.org/sVS4/18/06 17:10
benc__fromDigits s != q of type Nat18/06 17:10
benc__I guess i don't understand 'with' properly18/06 17:10
benc__(toDigits and digits from Data.Digit)18/06 17:10
benc__really what I'm trying to do there is extract the list of digits to pass into other functions18/06 17:11
* benc__ discovers theDigits but still puzzling over how to use 'with'18/06 17:25
--- Day changed Mon Jun 21 2010
ccasinSaizan: OK - good.  Though I suppose I should have more faith in the agda hackers21/06 19:53
Saizanyeah, agda currently lacks something like a positivity check for records, but i guess that's easy to avoid :)21/06 19:55
Saizanccasin: too bad patch-tag is down, i wanted to ask if you think solvers could be implemented in less lines of code than those there21/06 19:57
ccasinI'm no expert, but it would be fun to play a little golf21/06 19:58
Saizani guess a somewhat generic lib for syntax with binders would help a lot21/06 19:58
ccasinyes!  I am constantly tempted to implement something like that, but the overhead just gets too high because of agda's performance issues21/06 19:59
Saizanouch21/06 20:00
Saizanwere you using a lot of records?21/06 20:00
Saizanhttp://code.haskell.org/~Saizan/agda-reflection/ <- i've pushed my copy of the repo here, btw21/06 20:00
ccasinyes, I was using records to be very general about the nature of variables21/06 20:01
ccasinpossibly more trouble than it's worth, though21/06 20:01
ccasinalas, I am running agda 2.2.6, so I can't play with it until patch-tag reappears21/06 20:03
Saizanwell Agda's darcs repo is on code.haskell.org :)21/06 20:06
ccasinoh, right, silly me21/06 20:06
Saizanwhich just stopped responding?21/06 20:07
Saizanah, no, it's just a bit slow21/06 20:07
--- Day changed Tue Jun 22 2010
ccasinAre 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
ccasinI think I asked this months ago, but I forget if there was an easy answer :)22/06 14:43
ccasinBy = I just mean the standard defined homogeneous equality22/06 14:44
Saizan_i think i remember the discussion but not the conclusion :)22/06 14:49
ccasinI remember at least someone showed me how to prove (not (Bool = Nat))22/06 14:51
ccasinbut at the same size, I don't know - I think it's relevant to the current discussion on the mailing list22/06 14:51
Saizan_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
ccasinThe way we did it then was to define (P s := "s has exactly two elements")22/06 14:54
ccasinwhich is simple, then you show (P Bool) but (not (P Nat))22/06 14:54
ccasinand get a contradiction from Bool = Nat22/06 14:54
ccasinit's a similar idea22/06 14:54
Saizan_i see22/06 14:58
Saizan_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
ccasinthat works!22/06 15:08
ccasincool22/06 15:08
ccasinnow: do we need UIP to prove it?22/06 15:08
Saizan_s/heterogeneous equality on types/heterogeneous equality on values/ off course :)22/06 15:09
Saizan_to prove A = B?22/06 15:09
ccasinto prove (not (A = B))22/06 15:09
* ccasin opens a coq file22/06 15:09
Saizan_ah, yeah, mh i don't know, i'm not that familiar with type theories without UIP :)22/06 15:10
ccasinme either, luckily some french guys implemented one I can use to check my work :)22/06 15:11
ccasinalas, I'm having trouble with this strategy in coq.  I don't know how to get a contradiction from (a == b) there22/06 15:46
Saizan_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 fact22/06 15:53
Saizan_but with A = B they do have the same type22/06 15:55
Saizan_though i'm not sure how you'd write that P22/06 15:55
ccasinah, 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 = B22/06 15:56
--- Day changed Wed Jun 23 2010
nappingcan you do pattern matching of a one-constructor type in a let?23/06 00:34
nappingor am I getting confused with Coq again?23/06 00:34
Saizani don't think so23/06 00:38
nappingright, I want with23/06 00:38
mlarssonhow can I say to emacs to invoke agda with the option "--type-in-type" ?23/06 18:33
mlarsson(or any other option actually)23/06 18:35
kosmikusyou can use a pragma in the source file23/06 18:38
mlarssoncan you give me the line I should write ? :)23/06 18:45
mlarssonI'm quite a newb :).23/06 18:45
kosmikussomething like {-# OPTIONS --type-in-type #-}23/06 18:51
mlarssonparse error :/23/06 18:55
mlarssonhum, no, I made it23/06 18:55
mlarssonthank you :)23/06 18:56
kosmikusyou're welcome23/06 18:56
--- Day changed Thu Jun 24 2010
brad_larsenI am familiar with Haskell, but have not yet tried Agda.  Question about mixfix operators.24/06 20:24
brad_larsenIn Agda, can one easily define new list-like operators, e.g. <a, b, c, d>?24/06 20:25
brad_larsenOr tuple-like operators?  Where there are distinct start & stop tokens, and some separator between elements.24/06 20:25
ccasinI don't know a way of doing this, no24/06 20:27
ccasinwhen I want list-like things I build them cons and nil-like operators24/06 20:27
ccasin*build them with24/06 20:27
brad_larsenyeah.  I'm just curious.24/06 20:28
brad_larsensyntax is important for DSLs.24/06 20:28
ccasinI believe that - cons and nil aren't so bad though24/06 20:29
ccasinand agda's stdlib has a good trick products24/06 20:29
ccasinit just defines _,_24/06 20:29
ccasinyou can put parens around it if you want, since those are already in the syntax24/06 20:29
ccasin*good trick for products24/06 20:29
brad_larsenhmm.24/06 20:29
ccasinor of course you could do like <_,_> if you wanted different brackets24/06 20:30
brad_larsenbut then you could only have 2-element things?24/06 20:31
brad_larsene.g. <1, 2> but not <1, 2, 3>?24/06 20:31
ccasinyes, though somehow the agda stdlib gets around this for the standard tuples - not sure how, may be hard coded24/06 20:32
brad_larsenalas, 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
ccasinoh, I know how they get around it24/06 20:35
ccasinsilly me24/06 20:35
brad_larsenhow's that?24/06 20:35
ccasinsince the pair syntax is just _,_24/06 20:35
brad_larsenOooh.24/06 20:35
ccasinif you write (a , b , c)24/06 20:35
brad_larsenNo triples, etc then?24/06 20:35
ccasinit's just seeing the nesting24/06 20:35
brad_larsenit's actually (a, (b, c))24/06 20:35
ccasinyes24/06 20:35
brad_larsenThat's a good way of doing it, I suppose.24/06 20:36
brad_larsenI bet you could define new list-like syntax24/06 20:37
brad_larsenneed to define a comma-like function24/06 20:37
brad_larsen_,_24/06 20:37
brad_larsenfor the separator24/06 20:37
brad_larsenand then make the brackets function be the identity function24/06 20:37
ccasinthe trick is ending the list24/06 20:38
brad_larsencan't you write a function like24/06 20:38
brad_larsen<_>24/06 20:38
brad_larsenwhere the argument goes in the middle?24/06 20:38
ccasinyes24/06 20:38
brad_larsen(I don't know Agda syntax)24/06 20:38
ccasinI meant that you need to stick a nil on the end of the list somehow24/06 20:38
ccasinunlike for tuples24/06 20:38
brad_larsenyeah24/06 20:39
ccasinI suppose you could define _> as \x -> x :: nil24/06 20:39
ccasinand _,_ as ::24/06 20:39
ccasinand <_ as id24/06 20:39
ccasinthat might work24/06 20:39
ccasinthough the parsing priorities would be a trick24/06 20:40
brad_larsentricky!24/06 20:40
ccasinoh, but I'm wrong24/06 20:40
ccasinno... maybe it works?  I've confused myself :)24/06 20:40
brad_larsenIt's just a curiosity of mine at the moment.  I probably shouldn't obsess over syntax.24/06 20:40
brad_larsen(queue some Alan Perlis aphorism here)24/06 20:40
ccasinno, that's the best part of agda24/06 20:40
ccasinexercise: find a way to use a unicode snowman sensibly24/06 20:41
brad_larsenI've been working on an array-centric EDSL in haskell for my MS thesis24/06 20:41
brad_larsenable to express linear algebra, some BLAS sort of stuff.24/06 20:41
brad_larsencompiling to GPUs using CUDA24/06 20:42
ccasincool24/06 20:42
brad_larsentrying for a `deep' embedding of a DSL in haskell is a bit unsatisfying as far as syntax goes24/06 20:42
ccasinhaving been made to write matlab, I appreciate the need for a good array-centric edsl :)24/06 20:42
brad_larsenmy goal is for offline codegen24/06 20:43
brad_larsengenerate CUDA code, to be used in a larger C++ application24/06 20:43
brad_larsena more flexible language, more APL-like, would be awesome24/06 20:43
brad_larsenbut a lot harder to compile :-)24/06 20:43
ccasin:)24/06 20:45
ccasinI've never written any APL, but I think of haskell as pretty flexible!24/06 20:45
ccasinhah, this silly syntax works!24/06 20:50
ccasinwith some help from "infixr" declarations to specify parsing priority24/06 20:50
brad_larsenI'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
brad_larsenI'm told APL-like languages get you thinking in a different way about programming.24/06 20:51
brad_larsenThe array primitives are truly primitives, not defined in terms of iteration or recursion.24/06 20:51
brad_larsenawesome!24/06 20:52
brad_larsenso you can make your own list-like syntaxin Agda, if you wish.24/06 20:52
brad_larsenthanks for your answer, ccasin24/06 20:54
brad_larseni should go do some actual work24/06 20:54
ccasinno problem24/06 20:54
ccasinhave fun24/06 20:54
--- Day changed Fri Jun 25 2010
glguyIs 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 lot25/06 06:28
glguyhttp://www.galois.com/~emertens/powerlist/powerlist.html25/06 06:29
nappingDoes that even use \== at all?25/06 06:55
Saizanyou'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 similar25/06 06:56
Saizanyou might need to write some lemma to prove that e.g. ps respects such an equality25/06 06:57
Saizanmaybe i'm underestimating the impact of this :)25/06 06:57
nappingwhat is "rewrite"?25/06 06:58
Saizanrewrite takes a proof of a \== b and rewrites all occurences of a to b in the current context25/06 06:59
Saizanwhere both a and b can be compound expressions25/06 06:59
nappingThat might be a little hard to replace25/06 07:00
Saizansince that's used only to prove other \== propositions it should work out25/06 07:02
glguyyeah, I'd have to be explicit about my proofs and not use rewrite25/06 07:23
glguyproving congruence for some of the functions seemed tricky25/06 07:23
Saizanyou'd take "cong2 _||_" and "cong [_]" as constructors for the equality, and then it should just be a matter of recursing like the function does25/06 07:27
glguyI started here:25/06 07:33
glguy  _≋_ : ∀ {n} → Rel (Tree n) ℓ25/06 07:33
glguy  [ t ] ≋ [ u ] = t ≈ u25/06 07:33
glguy  (tˡ || tʳ) ≋ (uˡ || uʳ) = (tˡ ≋ uˡ) × (tʳ ≋ uʳ)25/06 07:33
pizza_question about http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf : http://codepad.org/sF1aW0cx25/06 18:52
ccasinhaha25/06 18:57
ccasinyes25/06 18:57
pizza_hi ccasin ; glad you agree25/06 18:58
pizza_thought i was losing it25/06 18:59
pizza_from the tutorial: apply : (A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a25/06 21:26
pizza_in (A : Set)(B : A -> Set) is (A : Set) context for (B : A -> Set)?25/06 21:28
ccasinIt means the same as (A : Set) -> (B : A -> Set) -> ...25/06 21:29
ccasinsometimes you can omit the arrow25/06 21:29
ccasinSo, yes, the A is in scope for the rest of the type25/06 21:31
pizza_oh25/06 21:35
pizza_ah, that is explain afterwards; after the first place it is used :/25/06 21:51
Mathnerd314is 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
pedagandMathnerd314, I cannot answer your question, but you might want to ask the same question on #coq, with s/Agda/Coq/26/06 00:10
Mathnerd314ok... :p26/06 00:11
pedagandout 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
Mathnerd314no, just a 6-week long intensive summer program26/06 00:11
pedagandalso, 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
Mathnerd314yes, I know that (Nat etc.)26/06 00:12
pedagandI see, 6 weeks, the whole of number theory: that's indeed gonna be intensive ;-)26/06 00:13
Mathnerd314we probably aren't doing all of it; I'll see26/06 00:22
* glguy generalized his proof from yesterday over an arbitrary Monoid (now with an arbitrary ==) http://www.galois.com/~emertens/powerlist/powerlist.html26/06 02:43
glguyso many cong function! :)26/06 02:44
Saizantruly26/06 02:50
Saizani feel like those cong functions should be a corollary of parametricity26/06 02:52
glguyI think I get most of these congruence functions for free if I parameterize my functions a little bit better26/06 03:15
glguyIs there a way to get types to display as though I were in the context that my goal is in?26/06 22:47
glguywhen I “open mymodule A"26/06 22:47
glguyI don’t want to see everything I imported as fully qualified26/06 22:47
--- Day changed Sun Jun 27 2010
Saizanwhich 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 open27/06 04:57
glguysaizan: C-c C-,27/06 04:58
glguyfor example27/06 04:58
glguyspecifically for parametarized modules27/06 04:58
Saizani remember some ugliness associated with parametrizing by records27/06 05:01

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