--- Log opened Fri Jul 01 00:00:57 2011
copumpkinxplat: how's it going?01/07 01:26
xplatcopumpkin: was just watching tv.  what did you mean by 'that makes sense'?  :-O01/07 02:31
copumpkinI don't see anything that really ties down the choice of functor there01/07 02:31
copumpkinit talks about F101/07 02:31
copumpkinwhich is just a function01/07 02:31
xplatwell, you can't tie down the functor from just the argument01/07 02:33
xplatbut the constructor is being used in places that should tie it down via the return type01/07 02:33
xplatin all of those functions, the return type is F \== G for some definite F and G01/07 02:34
copumpkinyeah01/07 02:35
xplatit doesn't seem like giving the constructor any other F and G could be well-typed01/07 02:35
copumpkinyeah, probably not01/07 02:37
copumpkinI guess information just doesn't flow that way?01/07 02:37
copumpkinmaybe worth asking the mailing list, dunno01/07 02:37
xplatyeah, i could have sworn i saw info go that way before01/07 02:37
copumpkinit's a bit voodooish right now01/07 02:38
xplati keep thinking i understand it, then something like this happens01/07 02:39
xplatlast time it was map_*01/07 02:40
augurcopumpkin! \o/01/07 04:12
BoxoI have an elementary question. What's the role of : in a data definition? ie. why is it (data Vec (A : Set) : Nat -> Set) instead of (data Vec : (A : Set) -> Nat -> Set) or (data Vec (A : Set) Nat : Set)?01/07 12:05
pigworkerthings left of the : scope over the whole declaration01/07 12:06
pigworkerand they always appear uniformly in the return types of constructors (though not necessarily in recursive references)01/07 12:07
pigworkerthe Nat has to go to the right of the : so that nil can give zero and cons a successor01/07 12:08
pigworkerthings declared left of : don't need to be stored constructor-by-constructor (because they're determined by the type)01/07 12:11
pigworkeryou want (A : Set) left of : so that nil and cons don't have to store Sets; if they did store Sets, Vec would have to give a big ugly Set1 instead of a tidy wee Set01/07 12:13
pigworkerbeware of mistaking left/right of : with "parameter" vs "index" in Dybjer's sense (parameters are uniform for whole definition (even in recursive positions), indices vary)01/07 12:16
pigworkereverything right of :, every parameter is left of :, but an index which is instantiated only in recursive positions can (and should!) be moved left of :01/07 12:16
pigworkerBoxo: is that what you wanted to know (along with too much other information)?01/07 12:19
Boxopigworker: I think so, thanks01/07 12:20
pigworkeroops, I meant "everything right of : *is an index*, every parameter is left of :"01/07 12:21
xplataugur: i found the paper i wanted to point you at some time ago, although i forget why.  http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.ps01/07 12:25
xplatit's a bit old, but a very thorough exposition of dependent types01/07 12:27
xplatit's actually more of a book than a paper, being 378 pages01/07 12:31
copumpkinxplat: yeah, I love that book01/07 13:59
copumpkinit really made everything "click" when I read it01/07 14:00
copumpkinnot sure if that was just cause I was close to having it click from other sources before reading it01/07 14:00
copumpkinbut it seemed pretty clear01/07 14:00
augurxplat: ive read a bit through it01/07 16:01
augurpigworker: what have you been teaching but didnt learn, and what are you beatng into your computer? :P01/07 16:07
auguryou should explain these things more thoroughly. twitter is 140 chars, but that doesnt meant it has telepathic powers!01/07 16:08
copumpkinxplat: yo dawg, wassup dawg?01/07 16:36
pigworkeraugur: it's not the word limit that persuades me to abstract away from the technical points and issue status bulletins affirming recurrent moronisms in the human condition01/07 17:59
augurpigworker: :P01/07 18:06
pigworkerit's the forum01/07 18:07
pigworkerlesson - even if you're setting up a syntax with a specific representation of variables in mind, abstract over the representation of variables and exhibit the functor for renaming (and maybe even the monad for substitution)01/07 18:10
pigworkerthat functor is a, moreover a *container*, equipped with predicate transfomers "Everywhere P" and "Somewhere P"01/07 18:12
augurhmm01/07 18:13
augurim not sure i know what that means but ok!01/07 18:13
pigworkerEverywhere preserves limity things. Especially, Everywhere P /\ Everywhere Q -> Everywhere (P /\ Q)01/07 18:14
augurhm!01/07 18:14
pigworkera container is a strictly positive functor01/07 18:14
pigworkerThere are lots of equivalent ways to think about them. Here's the locally-useful one...01/07 18:15
pigworkerF : Set -> Set is not only a functor but a container if you can equip it with the following bits and pieces01/07 18:16
augurwhats with the love for strict positivity, btw.01/07 18:16
augurive seen it around, and im not sure i get it01/07 18:17
pigworkerstrictly positive functors have meaningful fixpoints and induction and stuff01/07 18:18
augurahhh i see01/07 18:18
augurthats useful!01/07 18:18
pigworkerYou get    Everywhere : (X -> Set) -> (F X -> Set)01/07 18:18
augurhmm01/07 18:19
pigworkerEverywhere P xs means "P x holds for every x in xs"01/07 18:19
augursort of a generalized universal quantifier -- everywhere for sets is just forall01/07 18:20
augur"sets"01/07 18:20
pigworkernot quite; but it is (behind the scenes) quantifying universally over *positions* in xs01/07 18:21
pigworkerso Everywhere (< 4) [1,2,3]01/07 18:22
augurno sure, i just mean if you have a set data structure (lists minus repetition and ordering), everywhere for that would just be like quantification. everywhere for lists ~ all :: (a -> Bool) -> [a] -> Bool in haskell, etc.01/07 18:23
pigworkeryeah, but with evidence01/07 18:23
auguralways with evidence! :)01/07 18:23
pigworkernow, for a given F, the Everywhere is itself a strictly positive functor, but from indexed sets (X -> Set) to (F X -> Set)01/07 18:25
augurhmm.01/07 18:25
pigworkerso if you know that (x : X) -> P x -> Q x, then you surely know (xs : F X) -> Everywhere P xs -> Everywhere Q xs01/07 18:26
pigworkeryou also know Everywhere (\ _ -> One) xs01/07 18:26
augurhm. hm hm01/07 18:29
auguras with most things you say, this is lost of me for now, but will probably blow my mind when i fully grasp it01/07 18:31
pigworkerEverywhere P xs is a bunch of P-proofs for individual elements contained in xs; you know that "always true" holds for any element; and if P x implies Q x, then you can map that across your bunch of P-proofs and get a bunch of Q-proofs01/07 18:31
pigworkeryou know that x < 4 => x < 5, so Everywhere (< 4) [1,2,3] => Everywhere (< 5) [1,2,3]01/07 18:32
augurthat makes sense01/07 18:33
pigworkerit's like map, but relevant to the individual element01/07 18:34
pigworkerwhich is also to say, it *is* map, but between predicates, not sets01/07 18:35
augurhm. what would such a thing be used for?01/07 18:36
pigworkermany things; here's one... the induction principle for Mu F  ( data Mu-F : Set where <_> : F Mu-F -> MuF ) is...01/07 18:37
pigworker(P : Mu-F -> Set) -> ((xs : F Mu-F) -> Everywhere P xs -> P < xs >) -> (x : Mu-F) -> P x01/07 18:38
pigworker"Everywhere P" means "a collection of all the relevant induction hypotheses"01/07 18:39
pigworkerStrictly positive functors give you inductive types, and their "Everywhere"s give you induction principles.01/07 18:41
pigworkerEverywhere is also useful for evidence-bearing all-like things. I use it to express variable-freshness. Using numbers for variables, if every variable in a term is < x, then it's ok to pick x as the "next" variable.01/07 18:45
augurhmmm01/07 18:45
djahandarieWhere is a definition of Everywhere?01/07 18:46
augurits probably similar to fold for Mu F's01/07 18:46
pigworkerdjahandrie: depends on the functor01/07 18:46
pigworkerfor lists (with constructors [] and _,_) it's...01/07 18:47
auguror well, the definition of the induction principle, anyway01/07 18:47
pigworkerEverywhere : {X : Set} -> (X -> Set) -> List X -> Set01/07 18:47
pigworkerEverywhere P [] = One01/07 18:47
pigworkerEverywhere P (x , xs) = P x * Everywhere P xs01/07 18:47
augur(x :: xs) surely01/07 18:48
auguroh, no you said _,_ for the constructor01/07 18:48
augurserves me for not reading!01/07 18:49
pigworkernow, let _-:>_ : {X : Set} -> (X -> Set) -> (X -> Set) -> Set ; P -:> Q = (x : _) -> P x -> Q x01/07 18:50
pigworkerwe get a category whose objects are predicates P Q : (X -> Set) and whose arrows are predicate inclusions P -:> Q01/07 18:51
augurhm01/07 18:52
pigworkerwe get this thing...  mapEverywhere : {X : Set}{P Q : X -> Set} -> P -:> Q -> Everywhere P -:> Everywhere Q01/07 18:52
pigworkerunpack definitions to see what's going on01/07 18:52
pigworkermapEverywhere : {X : Set}{P Q : X -> Set} -> ((x : X) -> P x -> Q x) -> (xs : List X) -> Everywhere P xs -> Everywhere Q xs01/07 18:53
pigworkerand now go for it (by the way _,_ is also the constructor of *, and <> is the constructor of One)...01/07 18:54
pigworkermapEverywhere f [] <> = <>01/07 18:54
pigworkermapEverywhere f (x , xs) (px , epxs) = f x px , mapEverywhere f xs epxs01/07 18:54
auguri think i've written code like this before01/07 18:55
pigworkerit's not unusual01/07 18:55
auguryes, i definitely have. as part of a derivation of the definition of relational map from its non-recursive properties, yes01/07 18:56
pigworkerbut it's boilerplate; it has to exist, because List is strictly positive01/07 18:57
pigworkerironically, Agda knows a strictly positive definition when it sees one, but it doesn't give you all the free goodies that go with strict positivity01/07 19:02
pigworkerso you either use Agda datatypes and knock out all the kit by hand, or you build a universe of datatypes and get the kit by generic programming01/07 19:03
pigworkerearlier, I reached the point where I was just doing too much work that ought to come for free; I'm dumping my Agda types and doing the job generically01/07 19:04
* guerrilla learned something new today :) thanks pigworker01/07 19:09
pigworkernp01/07 19:10
guerrillasounds like i should have used my last spot on my UCAS application for strathclyde :P01/07 19:12
guerrillahehe01/07 19:12
guerrillawent with Swansea and Nottingham as they have those nice "Mathematics for Computer Science" programs01/07 19:13
pigworkerwe have MCS as well, as it happens01/07 19:14
guerrilladoh.. :( too late i think. i dont think i can change what is submitted01/07 19:14
pigworkerI mean, we have a joint degree with the maths department01/07 19:14
pigworkeryou probably can't, but I'd happily cheer for Notts and Swansea01/07 19:15
guerrillayeah01/07 19:15
guerrillaalso did Bristol and Birmingha but they seem to have a really weak program for CS (a lot of stuff i already did independelty or have had classes for)01/07 19:16
guerrillaBirmingham*01/07 19:16
pigworkerthese things are mostly what you make them, in any case01/07 19:17
guerrillaindeed. ill still accept at Bristol as my third choice just because a) i wan the paper b) they have a lot of leeway in optional classes and c) the city looks beautiful :) hehe01/07 19:18
pigworkermust go to Bristol (apart from to change trains) sometime01/07 19:19
guerrillayeh, didnt realise it was such a beauty until lastnight. i was just looking at their programs before that :) hehe01/07 19:20
xplati always had wondered why someone would name their daughter Bristol, aside from insanity which is always a possibility with that person01/07 19:22
guerrillayeah01/07 19:23
pigworkerBristol is, of course, Cockney rhyming slang for "breast"01/07 19:23
guerrillaon the other hand, birmingham looks like a terrible place. anyone know it?01/07 19:23
guerrillahahaha01/07 19:23
pigworkerBrum? only in a going for a pint while changing trains sort of a way01/07 19:24
pigworkerthe uni's nice (and I like the CS department)01/07 19:24
guerrillayeh, not sure though, i got accepted to IHK in Copenhagen and sinc their programs are similar, i may choose that (since i have friends there and know the city)01/07 19:25
guerrillajust cant get stoked on brum01/07 19:26
pigworkermust go to Copenhagen sometime (apart from to change planes)01/07 19:26
guerrillayou must01/07 19:26
guerrillaamazing city01/07 19:26
guerrillaone of the funnest nightlifes in europe i think01/07 19:26
guerrillabetter in the summer, naturally01/07 19:27
pigworkerand I owe Carsten Schürmann a talk01/07 19:27
guerrillaah01/07 19:27
guerrillathen go! :)01/07 19:27
auguroh man i got completely distracted >_>01/07 19:34
pigworkertime to go out...01/07 20:10
augurchow pigworker01/07 20:11
BoxoI'm writing church encodings of some elementary datatypes and have a problem:01/07 21:48
BoxoI have Either : Set -> Set -> Set1; Either A B = (Z : Set) -> (A -> Z) -> (B -> Z) -> Z. The problem is the Set1, since now I can't write this:01/07 21:49
Boxoeither_assoc : (A B C : Set) → Either A (Either B C) → Either (Either A B)01/07 21:50
Boxoso can I church-encode Either while avoiding Set1, or if not what would be a proper type for either_assoc01/07 21:51
Boxo(it's not even a problem in haskell since types with forall in them are still of kind *)01/07 21:52
Boxo* that should be either_assoc : (A B C : Set) → Either A (Either B C) → Either (Either A B) C01/07 21:55
copumpkinuse universe polymorphism :)01/07 22:00
dolioYou can't make Church encodings work very well in Agda.01/07 22:06
dolioThe type is always bigger than the things it can eliminate over.01/07 22:06
dolioAnd the things it can contain.01/07 22:06
dolioChurch encoding kind of needs impredicativity to work well.01/07 22:07
yrlnryChurch numbers do have weird types.01/07 22:07
yrlnryI was reading a paper recently that used linked lists to represent numerals and I wondered why that was not done more often.01/07 22:08
xplatit's too slow for pragmatists and too compromised for purists01/07 22:13
yrlnryWith Church numerals you can do some arithmetic without a fixpoint combinator.  That seems like a benefit.  But it's not always an important benefit.01/07 22:14
xplatso it only interests people who study numerals themselves, as opposed to numbers01/07 22:14
yrlnryYeah, okay.01/07 22:14
dolioChurch numerals are fixed point combinators.01/07 22:22
yrlnryHow so?01/07 22:23
dolio5 is represented by the eliminator for 5.01/07 22:24
dolioEtc.01/07 22:24
yrlnryWhat is an eliminator?01/07 22:24
dolioIt is the function that allows one to do recursion over an inductive type.01/07 22:25
yrlnryI will have to ask you about this later.  Thanks.01/07 22:25
dolioIf you keep things abstract, you have elimNat : (r -> r) -> r -> Nat -> r01/07 22:26
dolioChurch numerals use the partial application of the eliminator to the natural number to represent the natural number.01/07 22:26
BoxoWhy are they fixed point combinators because eliminators?01/07 22:28
dolioI suppose it might depend on what you mean by fixed point combinator. They are recursion combinators.01/07 22:28
dolioBut if they're not fixed point combinators, then you don't need fixed point combinators to do arithmetic even without Church numerals.01/07 22:29
BoxoAlso, what's impredicativity?01/07 22:40
Boxo(I'm reading the stuff that comes up on google but can hardly make sense of it)01/07 22:40
pigworkerImpredicativity is defining a thing by quantifying over the sort of thing you're defining. An a example might be "Impredicativity is the most confusing concept".01/07 22:44
BoxoI mean what makes it different from being self-referential or recursive?01/07 22:45
pigworkerMore prosaically, a definition like  Bool : Set; Bool = {X : Set} -> X -> X -> X  is impredicative01/07 22:45
pigworkerit's not directly self-referential, but it does define a Set by quantifying over all Sets01/07 22:46
pigworkersuch definitions are forbidden in Agda, but Coq has an impredicative universe of propositions01/07 22:48
xplatCoq Props are more like the types in System F that way; also like System F types they can be erased at runtime01/07 22:53
pigworkerI find impredicativity perplexing. I don't find that definition of Bool to be an especially straightforward characterisation of what it means to be a bit.01/07 22:54
pigworkerxplat: it's not just the types you can erase (you can also erase the types in all the other universes at runtime, for there is no casetype)01/07 22:55
BoxoBut if it's Bool : Set1 you do?01/07 22:55
pigworkerBoxo: that only makes it worse! Bool is very small. It should not be in Set1.01/07 22:56
pigworkerthat is, Set1 should not be the smallest universe with Bool01/07 22:57
pigworkerit should be in Set, and thus embedded in Set101/07 22:57
xplatif Set has no Bool, it is very small indeed01/07 22:57
pigworkerindeed, the universe closed under Pi and 1 is not very exciting01/07 22:58
xplatChurch encoding just doesn't seem to get along well with predicativity.  you'd probably want to have universes stacked at least as high as omega^2 to get anything done.01/07 22:59
Boxowell I don't think point 5 on page 4 of this document holds the key to impredicativity... http://www.scribd.com/doc/40697621/Mathematics-Ends-in-Meaninglessness-ie-self-contradiction01/07 23:01
xplatthe title alone hardly sounds promising01/07 23:02
* xplat files this away under 'friends of the time cube society'01/07 23:04
xplatthere's nothing like self-citing under the qualification 'Australian's [sic] leading erotic poet' to add credibility to an article on mathematics01/07 23:06
copumpkinlol01/07 23:14
copumpkinyou can always tell cranks cause they feel the need to list a huge pile of unrelated qualifications01/07 23:14
xplatmany don't even try to justify them in any way when using them in other fields, like 'my phd in basket weaving proves that i have the patience to fully understand any subject no matter how trivial it may seem to casual examination', they just wave them about like a large, yet floppy, paper dong01/07 23:17
copumpkinI love that his example01/07 23:17
copumpkinis the 0.9 recurring is 101/07 23:17
xplat0.9999999... is an infinite number, it can't equal 1!!!ONE01/07 23:18
xplatsimilarly, one supposes, 0.333... can't equal 1/301/07 23:19
dolioTime to quit my job and become an erotic poet philosopher.01/07 23:20
djahandarieWho says you can't be an erotic poet philosopher at your job?01/07 23:21
dolioI bet there are corporate regulations that prohibit it.01/07 23:22
copumpkinwe violate most of the other corporate regulations anyway01/07 23:22
xplatthe required lobotomy would interfere with primary job duties, anyhow01/07 23:22
* copumpkin goes to work every day in flip flops and a short spandex suit with offensive prints on it01/07 23:22
xplathow offensive exactly?01/07 23:23
dolioBoxo: Did you find that because I mentioned impredicativity earlier?01/07 23:23
Boxodolio: yeah01/07 23:24
copumpkinxplat: things like "FUCK YOU FINANCE PERSON WHO WORKS IN THE SAME OFFICE AS ME"01/07 23:24
copumpkinor "FUCK TERRY MCGRAW"01/07 23:24
copumpkinI'm not sure those are specifically against the rules01/07 23:24
copumpkinbut the spandex suit is01/07 23:24
BoxoSo is this definition of a maximum of a finite set of numbers impredicative? max(A) = the x such that x in a and forall y in A, x >= y01/07 23:26
BoxoAfter all, it quantifies over A01/07 23:26
xplathm, "Terry" because he's "III".  what a maverick, it's supposed to be "Trip".01/07 23:27
xplatBoxo: it's impredicative if you assert the existence of x on that basis.  if you already have a completely separate condition for being in 'a' it's not01/07 23:30
xplat... i think.01/07 23:31
dolioThere are lots of different standards by which to count things as impredicative.01/07 23:31
BoxoThat was a vague definition, here's a better one:01/07 23:32
Boxox = max(A) iff x in A and forall y in A: x >= y01/07 23:33
BoxoBut that doesn't assert the existence... sorry01/07 23:34
dolioIn the specific case of Church numerals, you have (forall r. (r -> r) -> r -> r).01/07 23:36
dolioWhere r ranges over types.01/07 23:36
dolioAnd in particular, it ranges over that type, the type of Church numerals.01/07 23:36
dolioSo its definition makes reference (somewhat indirectly) to itself.01/07 23:38
dolioI find a lot of other examples of impredicativity hard to really get a hold of.01/07 23:39
nappingDoes --universe-polymorphism slow typechecking?01/07 23:40
nappingI defined propositional logic and wrote some cute reflective tactic stuff01/07 23:41
djahandarieYes, but I'm not sure how much01/07 23:41
nappingnow that I'm trying to add quantifiers, everything becomes messy01/07 23:41
nappingI can't just take a Vec Set depth of the variables that are in scope and produce a Set for the expression a term represents01/07 23:42
nappingNow I'm computing the level of the Set for what a term represents01/07 23:42
nappingI don't know if this is even going to work out01/07 23:43
nappingah, here's a nice elementary problem01/07 23:44
nappingDon't know how to parse [ (psem y Γ) , (psem y' Γ) ].01/07 23:45
nappingCould mean any one of: [ (psem y Γ) , (psem y' Γ) ] [ ((psem y Γ) , (psem y' Γ)) ]01/07 23:45
nappingI guess I can01/07 23:45
nappingI can't add "anti-parentheses" to tell it to take the first01/07 23:46
BoxoSo (forall r. (r -> r) -> r -> r) is impredicative because to determine whether (forall r. (r -> r) -> r -> r), you have to determine whether (((forall r. (r -> r) -> r -> r) -> (forall r. (r -> r) -> r -> r)) -> (forall r. (r -> r) -> r -> r) -> (forall r. (r -> r) -> r -> r)) and to determine that...01/07 23:50
nappingBoxo: I'm missing some context, but that would seem to depend on the meaning of your forall01/07 23:51
nappingyou only get that if the forall itself is impredicative, in the sense that (forall (r :: *) . t) :: *01/07 23:52
kosmikusit doesn't make much sense to say that a particular type is impredicative01/07 23:52
Boxo01:36 < dolio> In the specific case of Church numerals, you have (forall r. (r -> r) -> r -> r).01/07 23:53
Boxo01:36 < dolio> Where r ranges over types.01/07 23:53
Boxo01:36 < dolio> And in particular, it ranges over that type, the type of Church numerals.01/07 23:53
nappingIt seems to make sense to ask whether a type makes use of impredicative quantification in a system that allows it01/07 23:53
Boxo01:38 < dolio> So its definition makes reference (somewhat indirectly) to itself.01/07 23:53
kosmikusnapping: well, ok01/07 23:54
kosmikusjust wanted to make sure that it's clear that impredicativity is in the quantification, and hence a property of a type system, not of a type01/07 23:54
xplatit's hard to avoid using impredicativity in a system that allows it01/07 23:55
xplatbut some uses are more essential than others01/07 23:55
nappingkosmikus: I've been reading Luo's strong normalization proof recently. There's a lot I don't understand, but the bits I've seen to far seem to be making heroic efforts to separate out and stratify some predicative definitions01/07 23:55
xplatin particular, it's pretty hard to use church encodings if you can't feed them into each other01/07 23:55
kosmikusso the type "forall r. (r -> r) -> r -> r" is completely fine in a system without impredicativity01/07 23:56
nappingWell, my rejiggered system seems to work01/07 23:56
nappingint (ℕ ∷ []) ((prop zero ⇒ prop zero) ⇒ prop zero) computes to (ℕ → ℕ) → ℕ : Set01/07 23:59
--- Day changed Sat Jul 02 2011
xplatint for interpret?02/07 00:00
augurheyo02/07 00:00
nappingwhile int [] (All (All (prop zero ⇒ prop (suc zero)))) computes to (S S' : Set) → S' → S at type Set₁02/07 00:00
nappingyeah, that interprets a propositional statement in an environment of types02/07 00:01
nappingThere's another function which is supposed to take a proof tree and actually produce an inhabitant of the type02/07 00:01
nappingI haven't actually added axioms for quantifiers yet, though02/07 00:02
copumpkinI kind of like these presentations of any and all02/07 00:17
copumpkinany : ∀ {A} {P : Pred A} → Decider P → Decider (Any P)02/07 00:17
copumpkinall : ∀ {A} {P : A → Set} → Decider P → Decider (All P)02/07 00:18
augurcopumpkin: !02/07 00:18
copumpkinhi :)02/07 00:19
copumpkinabout to help dolio move02/07 00:19
copumpkinbbiab02/07 00:19
augurnooo i tried to send you to the terminal object02/07 00:19
augur:|02/07 00:19
copumpkinlol02/07 00:19
augurand all you do is head to dolios02/07 00:19
copumpkinxplat: send me stuff!! :)02/07 00:19
augurmaybe dolio is the terminal object in the category of category theorists02/07 00:19
augurnah thatd probably be eilenberg or saunders or mac lane or lawvere or one of them02/07 00:20
augurwheres dolio moving btw02/07 00:21
nappingHas anyone used Data.Fin.Substitution?02/07 00:32
nappingI'm not sure what I'm supposed to define02/07 00:34
nappingLooks like TermSubst is enough02/07 01:01
octorineHi everyone.02/07 21:43
octorineAnyone want to tell me why my proof isn't working?02/07 21:43
octorineI'm following the Dependently Typed Programming in Agda tutorial and trying to prove that every list is a sublist of itself.  I've got two holes in my proof, and I think I know what goes in each of them, but Agda won't accept my answers.02/07 21:46
nappingthen they have the wrong type02/07 21:51
nappingyou haven't said enough to get useful suggestions02/07 21:53
auguroctorine: post the code!02/07 21:56
nappinghow is your sublist defined?02/07 22:02
octorineHere's the code: http://hpaste.org/4864402/07 22:02
nappingAh, you should make {A : Set} a parameter02/07 22:04
nappingnone of the constructors know what A to use02/07 22:04
nappingdata _⊂_ {A : Set} : List A → List A → Set where02/07 22:05
octorineYou mean the stop drop & keep constructors?02/07 22:06
nappingand keep, yes02/07 22:06
nappingyou see the yellow, don't you?02/07 22:06
octorineWeird.  That part was copied & pasted from the tutoria.02/07 22:07
octorineI did see the yellow.  I had a feeling it was related, but didn't know.02/07 22:07
octorineHooray!02/07 22:08
nappingwith that fixed you can write ⊂-refl l = {! -c !} and solve02/07 22:09
octorineI was just reading a question in the logs about the difference between data Foo (Bar : Set) : Baz -> Set and data Foo : (Bar : Set) -> Baz -> Set.  I had no idea it was the solution to my problem.02/07 22:10
augurpigworker: this tweet sounds interesting. tell us more!02/07 22:12
pigworkerjust that concurrency requires coprogramming while programming requires ncurrency02/07 22:13
augursounds like a wonderfully interesting distinction02/07 22:19
augurcoprogramming?02/07 22:19
pigworkercoprogramming is about making systems that are responsive, where programming is about delivering answers02/07 22:20
pigworkerliveness vs termination02/07 22:20
pigworkercorecursion vs recursion02/07 22:21
pigworkerthe must-read is David Turner's paper on "Elementary Strong Functional Programming"02/07 22:22
auguri wish youd write every thought you have in a big, brilliantly understandable encyclopedia02/07 22:22
pigworkerlife's too short02/07 22:22
augureverything you say manages to be obnoxiously interesting02/07 22:22
augurstop it02/07 22:22
auguri have things to do, i cant spend my time reading about everything you meantion >_<02/07 22:23
pigworkerkind of you to say so02/07 22:25
nappingpigworker: totality wasn't actually key to what I mentioned the other night - that just came up because I was searching for intuitionistic proofs that could be turned into functoins02/07 22:25
nappingfor classical logic, resolution is sound and complete02/07 22:26
pigworkerforgive me if I'm underimpressed by completeness when unaccompanied by totality02/07 22:28
nappingAll I meant to claim was that there are programs where termination is tricky to prove, and the worst-case runtime is big enough it won't always be allowed to finish anyway02/07 22:28
nappingno, it's total for classical logic02/07 22:29
nappingor if I have that wrong, at least enumerating truth tables is obviously total02/07 22:29
pigworkersure02/07 22:30
nappingTotality is underimpressive if you actually want results, and there are cases that won't finish in practice02/07 22:31
pigworkersure02/07 22:32
pigworkerif you want results, go with sound and fast02/07 22:33
pigworkerif you can't do totality, what chance of fast?02/07 22:36
nappingoctorine: try proving ∀{A} {l l' : List A} → length l ≡ length l' → l ⊂ l' → l ≡ l'02/07 22:40
augurtotality is really useful for many purposes i find. i mean, i do linguistics and theres no reason to think that there are any partial processes in language, or non-terminating ones, so totality is quite good to have in a language02/07 23:03
BoxoIsn't "this sentence is false" like (fix not) :P02/07 23:14
augurBoxo: perhaps a little!02/07 23:22
augurBoxo: except thats on the evaluation of the truth of a sentence not the properties of language itself02/07 23:24
--- Day changed Sun Jul 03 2011
octorinenapping: I haven't seen ≡ before, but I think it's what my tutorial called ==.   Is it "data ≡ : {A : Set} -> A -> A -> Set, with one constructor, refl : a ≡ a?03/07 01:52
xplatoctorine: yeah, except _≡_, and the : is usually placed a bit further to the right03/07 05:27
mixisi just read "Elementary Strong Functional Programming" and am somewhat puzzled by the concluding remarks, which state:03/07 13:20
mixisTheorem: For any language in which all programs terminate, there are always-terminating programs which cannot be written in it - among these are the interpreter for the language itself.03/07 13:20
mixisand that no such restrictions exist for a compiler in/for that language03/07 13:21
mixisi was under the impression that one can derive a compiler from an interpreter03/07 13:22
mixisand that actually there is not much of difference between a compiler and an interpreter except that a compiler looks like a program and an interpreter like a coprogram03/07 13:24
mixiscan i assume that there exists a definition of interpreter for which this theorem is true and get on with life or do i have a fundamentel thinko?03/07 13:26
mixisas in: there really is no such way and i should goedel up03/07 13:28
xplatit might have to do with the fact that a compiler can write out a loop/non-terminating function but an interpreter cannot interpret it03/07 13:30
xplat(specifically, cannot finish interpreting it)03/07 13:32
mixiswon't a non-terminating function contradict the definition of a language in which all programs terminate?03/07 13:43
Saizanthe point is that the compiler just has to manipulate inhert representations of programs, an interpret has to act like one instead03/07 13:46
Saizan*interpreter03/07 13:46
Saizani guess you have to restrict interpreter so that the result type matches the one of the input program as if you had written the input program directly in the language03/07 13:48
mixisso, an "interpreter" written in a terminating language that ist compiled some machine code won't be an interpreter03/07 13:50
mixis*compiled to03/07 13:50
mixisi think i see the point03/07 13:51
Saizani don't get what you mean03/07 13:51
mixisi guess i could use a terminating language to generate some machine code that interprets this terminating language03/07 13:56
mixisbut that won't be an interpreter written in a terminating03/07 13:56
mixislanguage03/07 13:56
Saizanyeah, that'd be a compiler03/07 13:57
mixisbecause i'm just using the language to construct something larger in between03/07 13:58
mixisallright, thanks03/07 13:58
xplatwith these impossibility results, there are usually several ways to look at them03/07 14:01
xplatin particular, for a lot of the computational ones you can usually make the proof go through either goedel or halting at your mental convenience03/07 14:02
mixisreminds me of natural sciences. if something is wrong, you can pick which conservation law you want to violate03/07 14:24
mixiswhere ususally energy is the easy way to go03/07 14:25
mixisand you can also translate violation of one law into violation of another03/07 14:26
xplatah, if only i could violate energy conservation whenever i had a problem :)03/07 18:37
--- Day changed Mon Jul 04 2011
koninkjeDoes anyone know what the canonical paper is (if any) that higher-order unification is undecidable?04/07 02:54
koninkjeI have the paper for 3rd-order; but not for 2nd04/07 02:55
augurkoninkje!04/07 03:10
koninkjeaugur! :)04/07 03:29
koninkjealas, my internet is a bit flakey at this cafe04/07 03:29
augurwhere are you?04/07 03:30
koninkjeWilliams Cafe by McMaster04/07 03:30
augurhm!04/07 03:31
koninkjethey just have a short timeout unless you're using HTTP regularly04/07 03:31
* koninkje often forgets, when not using HTTP regularly04/07 03:31
mtemمرحبا04/07 12:25
mtemlena04/07 12:26
mtemhi04/07 12:26
mtemlispy04/07 12:27
lispymtem: hi04/07 16:30
--- Day changed Wed Jul 06 2011
copumpkinanything fun happening in agdaland these days?06/07 20:25
--- Day changed Thu Jul 07 2011
augurcopumpkin: nope!07/07 01:54
augurnothing fun07/07 01:54
augurexcept, yo know07/07 01:54
auguragda!07/07 01:54
--- Day changed Fri Jul 08 2011
dsouzaaccount off08/07 02:27
dsouzaouch, wrong window! sorry about that :-(08/07 02:28
sshcaccount off08/07 02:28
sshcthere, right window! much better :-)08/07 02:28
dsouzatrying to shut bitlbee off from the wrong place. agda is indeed powerfull but yet has no way to deal with dumb users like me :-)08/07 02:31
mezohello all08/07 11:07
copumpkinxplat: doing any interesting CT stuff these days?08/07 15:28
copumpkindjahandarie: I quite like it08/07 18:25
copumpkinof course, in practice, I wouldn't use inductive types for shapes and indices08/07 18:25
djahandarieIs this on github?08/07 18:25
copumpkindjahandarie: not yet08/07 20:47
copumpkinnot really sure it's worthy of that08/07 20:47
copumpkinfeels more like an hpaste thing :)08/07 20:47
djahandarieWell if it's more than one file, GitHub is probably the right choice :p08/07 20:48
copumpkinit isn't! :D08/07 20:48
djahandarieThen put it on hpaste? :p I just want to see it08/07 20:49
copumpkinhttp://hpaste.org/4885008/07 20:53
copumpkinthat's what I have right now08/07 20:53
copumpkinplus a lot of nasty index transformation math in another file on another computer08/07 20:53
copumpkinthere's lots of things I want to change about this though08/07 20:53
copumpkinI also started doing something similar a while back with DPH's non-regular arrays08/07 20:54
copumpkinbut it was rather painful08/07 20:54
copumpkinI'd like to understand and model slices a bit better than repa does08/07 20:57
copumpkinrepa's shape/index confusion is confusing ;)08/07 20:57
copumpkinand I think I got a pretty decent disambiguation of them in my agda version08/07 20:57
copumpkingetting the stencils right would also be fun08/07 20:58
copumpkinI think repa also has some artifacts of the shape/index confusion in its API, that I think I can get rid of in agda08/07 21:01
copumpkinlike in transform, there's a mapping between the two shapes you pass in08/07 21:01
--- Day changed Sat Jul 09 2011
jmcarthurrepa in agda wtf09/07 03:37
copumpkinjmcarthur: what? it's a perfect fit!09/07 04:39
augurwhats a repa09/07 05:59
copumpkinI proved flatten and unflatten in a much nicer way than I did last time09/07 18:52
augurcopumpkin: ?09/07 19:18
--- Day changed Mon Jul 11 2011
xplathttp://hpaste.org/4893011/07 00:15
djahandarie:o11/07 00:15
xplatthis is basically the problem i was having with functor equality in a nutshell11/07 00:16
xplatthe implicit argument of test must be equal to A, but it is equal regardless of the value of property, therefore the value of property is considered to be underdetermined11/07 00:18
xplatthis doesn't seem to happen in every circumstance, however11/07 00:22
xplatotherwise you would never be able to have a meta with an irrelevant field at all without it turning yellow11/07 00:23
nappingIs it "property" that is missing?11/07 00:36
xplatcan someone with recent darcs agda try that file and see if it has an unsolved meta?11/07 00:36
xplatnapping: yes11/07 00:36
nappingso, test {A} zero typechecks11/07 00:37
xplatyes11/07 00:37
nappingtrying A = test {record {stuff = Lame.stuff A ; property = _}} zero11/07 00:39
nappingis also yellow at the underscore11/07 00:40
xplatif you take the dot off the field definition for property, i suspect all will typecheck11/07 00:41
xplat(they do for me)11/07 00:42
xplati think what happens here is an inconsistency (not the logical kind) between what happens when records are eta-expanded before unification and when they aren't11/07 00:45
xplatsince trying A = test {record {stuff = _ ; property = 666}} zero is going to typecheck, there's an argument that the yellow is correct11/07 00:47
xplathowever, if that viewpoint were enforced uniformly everywhere, there would be a lot of yellow where there isn't today11/07 00:47
nappingIt seems more like a question of handling implicit things11/07 00:56
nappingAh, I think I'm getting it11/07 00:59
nappingThe implicit argument has to unify with A11/07 00:59
nappingnormally that would be enough to fix all the fields, but because it's implicit it will typecheck whenever11/07 00:59
nappingThat's what you just said, isn't it?11/07 00:59
nappingI think it just doesn't take the idea of irrelevant arguments far enough to realize that any provided values would be equivalent11/07 01:27
nappingpost to the list?11/07 01:27
nappingah, I think part of the issue is knowing whether or not the type is occupied11/07 01:58
nappingIf you change the type of the implicit field to \top it's inferred fine11/07 01:59
augurhappy tesla day! :D11/07 04:30
Saizanis there a paper on agda's implicit arguments?11/07 22:55
xplatSaizan: i found some slides once11/07 23:01
xplatone of the AIM presentation sets was about implicit inference11/07 23:03
--- Day changed Tue Jul 12 2011
PeakerHey, is there a good reason for a DT language not to do HM Type inference by default -- and allow type annotations for non-principal types?12/07 06:26
kosmikusPeaker: what do you mean, HM type inference? that assumes a certain type system, and current dependently typed languages are not close to that type system. I also don't understand what you mean by annotating non-principal types. If we don't have principal types, then which type do you want to infer?12/07 07:08
kosmikusPeaker: I mean, in general, it's certainly possible to have more type inference than we currently do. But I don't see that we can trivially do it by "just applying HM type inference".12/07 07:09
Peakerkosmikus: Well, Agda can trivially encode HM types -- and then you have a principal HM type by definition, iiuc?12/07 07:11
Peakerkosmikus: I guess for types composed of simple set types that can be expressed as simple forall's12/07 07:12
kosmikusPeaker: ok, I now understand what you mean. but you still have to go beyond HM automatically in the sense that annotated variables can have arbitrary types, so you'll end up with more complicated unification problems. also, HM assumes top-level quantification is implicit, whereas in Agda it's usually explicit.12/07 07:38
kosmikusPeaker: about the latter, I mean: take a simple function such as "const = \ x y -> x", which ends up with type "a -> b -> a" in Haskell. Now in Agda, it currently makes a difference if you have "forall {a b}. a -> b -> a" or "forall {b a}. a -> b -> a".12/07 07:41
Peakerkosmikus: ah, what's the difference between them?  I understand the difference if b depends on a, but here it doesn't?12/07 07:43
Peaker(if b depends on the value of a that is)12/07 07:44
kosmikusyou can instantiate implicit argument explicitly, if you want12/07 07:44
Peakerah, right12/07 07:44
kosmikusif so, you have to pass them either in order12/07 07:44
kosmikusor by name12/07 07:44
kosmikusif you infer, both options don't work12/07 07:44
Peakerwhy not?12/07 07:45
Peakerwhy not infer an arbitrary one (deterministically)?12/07 07:45
kosmikusas long as it's not easy to describe which one, I think that's very confusing12/07 07:47
copumpkinPeaker: have you been particularly annoyed by the lack of inference in agda? I've actually been amazed at how much it can do12/07 07:47
kosmikusbut in principle: if you think it can be improved, go for it. implement experimental patches and let people play with it. I'm pretty sure that the current system isn't yet optimal in practice.12/07 07:47
Peakercopumpkin: I have barely actually used Agda :-(  I just take interest and believe it is the future of PL's :)12/07 07:48
kosmikusPeaker: well, then I'd actually recommend copumpkin's approach. use it and see that the current system already works quite well.12/07 07:48
copumpkinwell, the fact that inference is undecidable doesn't stop agda from doing a pretty good job at saving you from writing types 80% of the time12/07 07:48
copumpkinif you have a function, you have to write its type, but in most cases, it's pretty breezy12/07 07:49
copumpkinonly if it's a top-level function though12/07 07:49
copumpkinyou can write lambdas up the wazoo with no type annotations (in fact, type annotations don't have a syntax in agda)12/07 07:49
copumpkinthat there's no syntax for it should go to show how little we use it :P12/07 07:50
kosmikuscopumpkin: not necessarily a good argument :)12/07 07:50
copumpkinthere's a type annotation operator written in the language12/07 07:50
copumpkin;)12/07 07:50
copumpkinkosmikus: the it might have been "the language" :P12/07 07:50
kosmikusheh12/07 07:50
copumpkinbut I'm writing some right now12/07 07:51
copumpkinso it can't be that bad12/07 07:51
kosmikusthe only thing that sometimes annoys me has in fact to do with quantifying off all the variables I use12/07 07:51
copumpkinyeah, same12/07 07:51
kosmikusI mean, it's fine to write "forall {A B C D}""12/07 07:51
kosmikusbut if A is itself dependent on three more things ...12/07 07:51
copumpkinyeah, then you have to write A out explicitly and all its dependent things12/07 07:52
kosmikusthen I get some boilerplate of three lines of implicit arguments for each function12/07 07:52
copumpkinespecially with universe polymorphism12/07 07:52
kosmikusI guess you can use modules for that12/07 07:52
kosmikusor records12/07 07:52
copumpkinforall {A} -> A -> A is yellow :/12/07 07:52
copumpkinjust because of a universe parameter that nobody cares about (or can even match on anymore)12/07 07:52
kosmikusyes12/07 07:52
* copumpkin weeps12/07 07:53
kosmikus:)12/07 07:53
copumpkinI wrote a terrifying (for me) proof12/07 08:10
copumpkinof an "obvious" fact12/07 08:10
copumpkin  quotient : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) divMod suc d ≡ result x r12/07 08:11
kosmikusterrifying in what way?12/07 08:16
copumpkinit took me a long time and lots of work :P12/07 08:17
copumpkinI'm sure there's an easier way but I couldn't find it12/07 08:17
kosmikuswhat's "result"?12/07 08:18
copumpkinthe constructor of the DivMod type12/07 08:19
copumpkinin Data.Nat.DivMod12/07 08:19
copumpkin(from std lib)12/07 08:19
kosmikusoh ok12/07 08:19
copumpkinit basically refines its indices to prove that the quotient and remainder are correct12/07 08:19
kosmikusI'm standard-library-illiterate12/07 08:19
kosmikusyeah, I can infer what it means12/07 08:19
kosmikusfrom the theorem12/07 08:19
copumpkinthere's another version that doesn't refine indices and instead carries an explicit equality proof12/07 08:19
kosmikusbut I thought it was a function12/07 08:19
kosmikusI'd probably try to prove it for div and mod separately12/07 08:22
kosmikusthen I'd try to prove that div and mod distribute over addition12/07 08:22
copumpkinwell, div and mod are simple projections out of that type12/07 08:22
kosmikusand prove the four individual cases12/07 08:22
copumpkin(in terms of the implementation)12/07 08:22
copumpkinand the actual implementation of divMod is terrifying, so I wanted to use the type as much as possible12/07 08:23
Peakerhow does  (...) divMod suc d   parse?  As (...) divMod (suc d) ?12/07 08:24
copumpkinyeah12/07 08:24
copumpkinkosmikus: have you ever used the inspect idiom?12/07 08:28
copumpkinI've found it breaks agda's train of thought12/07 08:28
kosmikuscopumpkin: yes, I think I've used it. but for some strange reason, I find it difficult to grasp. so basically, whenever I get into a situation where I can't seem to convince the typechecker of what I want to do, I look it up again :)12/07 08:29
copumpkinah yeah12/07 08:29
copumpkinby the way, I used proof-irrelevance for the first time today12/07 08:29
copumpkinand cried12/07 08:29
kosmikusbut right now (I mean, in the past 3 months or so), I'm writing much less Agda code than I'd like to12/07 08:29
kosmikusI'm getting paid for Haskell hacking, but not for Agda (yet)12/07 08:30
copumpkinaw :(12/07 08:30
Peakerkosmikus: who pays you for Haskell hacking?12/07 08:32
kosmikusPeaker: I'm a partner at well-typed.com12/07 08:34
kosmikusso our clients do :)12/07 08:34
Peaker:-)12/07 08:35
kosmikusI guess we'd accept work that involves Agda hacking, though :)12/07 08:37
kosmikuseven though we advertise with Haskell only12/07 08:37
copumpkinwell, most people there haven't hacked on much agda, right?12/07 08:37
kosmikuscopumpkin: I think I'm the only one who's actually used Agda. But Ian (Igloo) has used Coq. And I'm pretty sure everyone here is capable of learning it, and would like it.12/07 08:39
copumpkinyeah :)12/07 08:39
copumpkinah well, I should go to sleep12/07 08:39
kosmikusgood night12/07 08:43
* Saizan realizes his current agda code could be done better in haskell except for overloading of constructors12/07 15:55
augurSaizan: my agda code is so dependently typed that it cant even be approximated in haskell :(12/07 16:07
augurexcept by oleg12/07 16:07
djahandarieI'm not sure if I actually like the constructor overloading or not12/07 16:08
copumpkinI do12/07 16:08
copumpkinI consider it essential!12/07 16:08
djahandarieEssential to what?12/07 16:08
copumpkinanyone want to prove something : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) divMod suc d ≡ result x r ? :)12/07 16:08
copumpkinit's lots of fun12/07 16:08
Saizanessential to having many different refinements of the same structure12/07 16:09
copumpkinyeah, that12/07 16:09
djahandarieHuh?12/07 16:09
Saizanuntil we have a language that's more aware of them :)12/07 16:09
copumpkinwhat's the difference between List, Vec, HeterogeneousList?12/07 16:09
copumpkinor Fin and Nat?12/07 16:09
djahandarieI'm still not sure if I agree12/07 16:10
augurdjahandarie: you dont have to agree, but it's nice when you can!12/07 16:11
auguragda lets you agree if you want :)12/07 16:11
copumpkinI think writing custom datatypes that express your invariants nicely in their indices is a helpful proof process12/07 16:12
copumpkinand if you need to write the variants of your datatype with different data constructors each time, it's a pain12/07 16:12
augurcopumpkin: itd be really neat if casting could be done automatically when data types are constructor synonymous and have provably identifiable structure12/07 16:13
augurlike with fin and nat12/07 16:13
copumpkinbut what index would the Fin have when casting a Nat?12/07 16:14
copumpkinsame as toNat?12/07 16:14
augurnone, itd be forgetful12/07 16:14
copumpkin(x : Nat) -> Fin (suc x)12/07 16:14
copumpkinit can't have no index12/07 16:14
auguroh oh when castng a nat to a fin12/07 16:14
augurso you mean toFin12/07 16:14
auguri dont know if that should be transparent12/07 16:14
augurjust the forgetful kinds12/07 16:15
augurlike finToNat12/07 16:15
augurif you could use fins everywhere you use nats, transparently and without explicit conversion, that'd be useful for real programming12/07 16:15
auguritd also be useful, i think, for agda's goals12/07 16:15
augurmaybe12/07 16:15
auguri mean, at times its useful to properly identify isomorphic sets/subsets rather than just just have them be isomorphic12/07 16:16
augurso that you really can talk about _the_ singleton set12/07 16:17
auguror _the_ naturals12/07 16:17
augurnot all the time, mind you, but in some contexts its nice12/07 16:17
djahandarieI just think it's weird that the constructors are overloaded but you can't do, for example, toNat = id12/07 16:20
djahandarieBut the definition would look exactly like id12/07 16:21
augurdjahandarie: thats what i was getting at with implicit casting12/07 16:22
auguri think that epigram 2 (heh) will be ideal for that sort of thing12/07 16:22
augurthe whole ornamentation thing seems to be important to the epigram people, and its all about automatically deriving indices12/07 16:23
auguralong with automatic derivation of the forgetful functors12/07 16:23
augurwhich seems like it would make it almost natural to have automatically constructed refinements of existing types in a transparent way12/07 16:23
Saizanyou'd have toNat for free (named forget) if Fin was defined as an ornated Nat12/07 16:39
augurSaizan: indeed12/07 16:51
augurand youd have Fin for free too12/07 16:51
augurbecause the ornamentation would probably be something you can get for free12/07 16:51
Saizannot sure about that12/07 16:53
augurneither am i! :D12/07 16:54
copumpkinsay I have an indexed family12/07 19:32
copumpkindata Moo : Nat -> Set where12/07 19:32
copumpkinoi : forall x y -> Moo (x * y)12/07 19:33
copumpkinnow, I have a Moo 112/07 19:33
copumpkinI'd like to pattern match on that12/07 19:33
copumpkinhow the **** can I do that? :)12/07 19:33
Saizanyou've to pattern match on Moo n keeping a n == 1 around12/07 19:35
copumpkinah, I see12/07 19:35
Saizanyou'll end up with (x * y) == 1 after the match12/07 19:35
Saizanstill dealing with DivMod?12/07 19:36
copumpkinindirectly :)12/07 19:36
copumpkinmy DivMod woes are over12/07 19:36
copumpkinI've proved what I set out to prove12/07 19:36
copumpkinneed to figure out how it helps me now :)12/07 19:36
Saizanso you proved something from above? how?12/07 19:38
copumpkinwhich one do you mean?12/07 19:39
copumpkinyou mean the DivMod proof I mentioned earlier?12/07 19:39
Saizansomething : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) divMod suc d ≡ result x r12/07 19:39
copumpkinoh yeah12/07 19:39
copumpkinI have 99% of that, just have a tedious hole that I've written a symmetric case of12/07 19:39
copumpkinand need to generalize that12/07 19:39
copumpkindo you have a clean proof of that?12/07 19:39
copumpkinmine is terrifying12/07 19:40
Saizanmy strategy ended up requiring ∀ {n} (r r' : Fin n) q q' -> toℕ r + q * n ≡ toℕ r' + q' * n -> (r ≡ r' × q ≡ q'), which doesn't seem so easy12/07 19:40
copumpkinyeah, that's what I wrote12/07 19:40
copumpkinmy proof of that was pretty ugly, too12/07 19:41
copumpkindid you finish it?12/07 19:42
Saizanno12/07 19:42
Saizanbarely started :)12/07 19:42
copumpkinI'll show you mine12/07 19:42
copumpkinbut it will make your eyes bleed12/07 19:43
copumpkinhttp://hpaste.org/4898012/07 19:43
copumpkinthe hole in there is basically the same proof as the clause above it12/07 19:44
Saizani didn't even know you could put a where there :O12/07 19:46
copumpkinyou can even name those where blocks :D12/07 19:46
copumpkinI had to use that before because of the absurd lambda abusrdity12/07 19:46
copumpkinI wanted that pattern matching thing12/07 19:50
copumpkinfor12/07 19:50
copumpkinsingleton : ∀ {sh : Shape 1} {A} → A → Array sh A12/07 19:50
copumpkin:D12/07 19:50
copumpkinand toScalar : ∀ {sh : Shape 1} {A} → Array sh A → A12/07 19:50
copumpkinthe haskell repa one forces it to be Array Z A12/07 19:51
copumpkinbut I can make any array of size one :P12/07 19:51
copumpkinDivMod'-lemma x d r (result .x .r eq)   | refl , refl = cong (result x r) (subst (λ z → z ≡ refl) refl (proof-irrelevance eq refl)) -- holy fuck12/07 20:00
augurhow are type class like things done in agda? i dont remember seeing anything like this in papers12/07 20:05
auguri feel like it would be by some record type12/07 20:05
copumpkinyeah, just records12/07 20:05
augurlike12/07 20:06
copumpkinyou can have it magically look up the records by their parameters in {{}}12/07 20:06
augurrecord Functor (F : Set -> Set) where ...12/07 20:07
augurwith fields for fmap and the functor laws?12/07 20:07
copumpkinyeah12/07 20:07
augurso like12/07 20:08
copumpkinSaizan: did you run away screaming? :)12/07 20:08
copumpkinSaizan: I'd love to see a cleaner proof of that12/07 20:08
augurListIsAFunctor : Functor List ; ListIsAFunctor = yadda yadda12/07 20:08
copumpkinyeah12/07 20:09
augurhmm.12/07 20:09
copumpkinthen if you use double curlies12/07 20:09
copumpkinit'll look that shit up for you automagically12/07 20:09
augurive never seen double curlies, actually12/07 20:09
augurexplain?12/07 20:09
copumpkinif it's unambiguous and in scope12/07 20:09
copumpkinlike12/07 20:09
copumpkinmappyMap :: {F : Set -> Set} {A} {B} {{f : Functor F}} -> (A -> B) -> (F A -> F B)12/07 20:10
copumpkinor something like that12/07 20:10
auguro_O12/07 20:10
augurwhaa12/07 20:10
copumpkinI think it would automagically use ListIsAFunctor if it's in scope12/07 20:10
augurreally? crazy12/07 20:10
copumpkinbut not if other stuff also applies12/07 20:10
copumpkinit's gotta be unique12/07 20:10
augurwhere are these double curlies in the wiki or something12/07 20:10
augurthats nutso12/07 20:10
copumpkinhttps://lists.chalmers.se/pipermail/agda/2011/002891.html12/07 20:11
copumpkinhttp://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.InstanceArguments?from=ReferenceManual.Non-canonicalImplicitArguments12/07 20:11
Saizancopumpkin: it's a bit intimidating :D12/07 20:11
augurhm!12/07 20:11
copumpkinSaizan: I thought it was rather amusing to have to use subst on proof-irrelevance12/07 20:12
copumpkinI wonder if that's common12/07 20:12
Saizanisn't subst _ refl x denotationally equal to x?12/07 20:14
auguri wish agdamode would force unsolved constraints to the surface12/07 20:14
auguri have constraints in some code and i have no clue where they're coming from12/07 20:14
augurand they dont go away when i add all the possible implicit arguments :\12/07 20:15
copumpkinSaizan: ooh, you're right12/07 20:15
copumpkinthat simplified it a bit :)12/07 20:15
augurif i knew how to use epigram i'd be tempted to experiment with it for my purposes12/07 20:15
augurbut i dont know if its as fully usable as agda12/07 20:15
augur"usable"12/07 20:15
Saizan(btw, the proper term is not denotationally.. or is it?)12/07 20:19
augurSaizan: for what?12/07 20:19
augurdenotationally is certainly a word12/07 20:19
augurthat means what i think you want it to mean12/07 20:19
auguri feel the use of records instead of substantive things like type classes has a certain elegance to it12/07 20:24
augura sort of reduction of these concepts to their conceptual core, revealing their nature and making them potentially more powerful than the substantive stuff allows12/07 20:24
augurthe beyond-the-basics section of the link in the mailing list post makes this clear12/07 20:27
auguri dont know what most of these things are, but multi-parameter type classes is enough of a generalization to make me appreciate records-as-type-classes12/07 20:28
auguri think the one thing the records-as-typeclasses thing doesnt let you do, afaik, is method selection12/07 20:33
auguryou have to explicitly use the typeclass record in calls12/07 20:34
auguror at least open it12/07 20:34
augurwhich might get messy when you have multiple distinct possible records that would be used12/07 20:35
augurthat would at least make it clear in-code (as opposed to only in the background) which versions are being used12/07 20:35
augurit'd certainly make some code clearer, if wordier12/07 20:35
augurive found some haskell code horrendous because of the transparent selection of type class12/07 20:36
augurwhats the agdadic version of scrap your boilerplate12/07 20:54
djahandariecopumpkin, if we add locally cartesian closed categories, do you think we could show that Agda types are an internal logic for them (more powerful though, since we have inductive types and other stuff...)?12/07 21:00
djahandarieI guess the main leap is formalizing internal logic and doing something simpler, like a simply-typed lambda calculus :)12/07 21:03
djahandarieMan I wish ddarius' talk on fibrations was fully recorded so I could rewatch it :(12/07 21:14
augurarent Desc's supposed to be a solution to syb-type problems?12/07 21:22
auguranyone? agda syb?12/07 21:40
augurno12/07 21:40
augur?12/07 21:40
augur:(12/07 21:40
Saizanthere's no standard agda syb, stuff like Desc handles some datatype generic programming, though it'd work better in a language built on top of it like epigram212/07 21:44
augurhm12/07 21:50
augurgeneric programming is a fascinating topic12/07 21:50
djahandarieI've never really been sold on it12/07 21:50
augurhttp://www.seas.upenn.edu/~sweirich/ssgip/main.pdf has some interestng examples of generic problems that are obviously perfectly solvable in normal old DT fashion12/07 21:54
augurand i wouldntve thought of them as generic problems but they clearly are12/07 21:54
--- Day changed Wed Jul 13 2011
copumpkinwoot13/07 01:20
copumpkinproved both directions13/07 01:20
xplati hoped that by looking up the division algorithm i could find a nice proof of uniqueness of q and r13/07 02:33
xplatthere are lots of proofs that are not nice13/07 02:34
xplatand by not nice i mean handwavy13/07 02:34
xplatwaving your hands won't make you levitate13/07 02:35
xplatalthough if you can levitate, maybe you can wave your hands more13/07 02:35
copumpkin:O13/07 02:36
copumpkinanyway, I finished that proof13/07 02:36
copumpkinin all its horrifying glory13/07 02:36
copumpkinturned out all I needed was the toℕ r + x * suc d ≡ toℕ r′ + x′ * suc d → r ≡ r′ × x ≡ x′13/07 02:36
copumpkindidn't need the final step I was using before13/07 02:36
xplatyeah13/07 02:38
still a horrible proof for that13/07 02:39
xplatwith that lemma, you can just prove that divMod is (over)determined by its indices13/07 02:39
xplater, that DivMod is13/07 02:39
copumpkinyeah, I did that too13/07 02:39
copumpkinbut didn't need it13/07 02:39
xplatit'd be a lot easier to work with naturals in agda if you could have things like overlapping rules in functions (with a proof of conf...nce etc)13/07 02:43
xplatof course if it was doing AC unification on naturals agda might typecheck even *slower* ...13/07 02:44
copumpkinlol13/07 02:44
copumpkinAC unification?13/07 02:44
xplatassociative-commutative13/07 02:45
copumpkinah13/07 02:45
copumpkinsounds terrifying :P13/07 02:45
xplatterrifying to implement, but nice to use13/07 02:45
xplatbasically your commutative and associative laws would be true definitionally13/07 02:45
copumpkinyeah13/07 02:46
xplatso you don't have to bend over backwards to avoid ending up with types with subst in them when you index with naturals13/07 02:46
copumpkinhow would you inform the typechecker of things that are?13/07 02:46
copumpkinwhere can I read more about this?13/07 02:47
nappingI don't know that anyone has done a proper job in a typechecker13/07 02:47
xplatthat channel that was advertising a while back for unification under theories, if anyone's still there they can probably give you a better reading list than i can13/07 02:47
nappingbut rewriting languages do that13/07 02:48
nappingIn particular, there are probably good papers about the implementation in Maude13/07 02:48
xplatif typecheckers can steal from lambda-prolog they can steal from maude :)13/07 02:49
copumpkin:O13/07 02:49
nappingI was looking at confluent definitions a bit recently13/07 02:50
nappingit seems somewhat plausible to reflect enough syntax to prove that your definition is confluent13/07 02:50
nappingIf you restrict your definitions (compared to something like maude) enough that you have to give all rules for a function at once, all those rules must have a LHS headed by an application of the new function, and the non-variable parts can only mention constructors13/07 02:52
nappingthen it's enough just to prove that the new definition is confluent, without worrying that you will mess up confluence of earlier definitions13/07 02:53
nappingthe idea was to have the language provide a type of expressions, and a relation corresponding to the evaluation rules you supply13/07 03:00
nappingthen you prove the relation is confluent, and only after you supply the proof is your new function actually available as something that computes13/07 03:01
copumpkinwoot13/07 03:31
copumpkinIndex↔Fin : ∀ {n} (sh : Shape n) → Bijection (≡-setoid (Index sh)) (≡-setoid (Fin n))13/07 03:31
copumpkinman, that was painful13/07 03:31
djahandarieWhat are you working on, btw?13/07 03:31
copumpkinthat repa shit13/07 03:31
copumpkin:P13/07 03:31
copumpkincompletely pointless13/07 03:32
copumpkinbut kind of fun in a pointless kind of way13/07 03:32
copumpkinhere it is http://hpaste.org/4898513/07 03:33
copumpkinit's got some leftover stuff in it13/07 03:33
djahandarieShouldn't there be a nicer way to prove that bijection?13/07 03:35
copumpkinyou tell me :P13/07 03:35
djahandarieMaybe proving unflatten.flatten == flatten.unflatten would be easier? Probably not, it'd most likely be much harder13/07 03:37
copumpkinI'd imagine it has a minimum ugliness in it due to the divMod13/07 03:37
copumpkinand the "flatten'-fits" proof to cram the flattened index into a Fin of the right size (mostly getting that to normalize by pattern matching on things it likes)13/07 03:38
djahandarieWhat is that proof-irrelevance thing doing?13/07 03:38
copumpkinI have an equality a + b * c == d + e * c13/07 03:39
copumpkingood luck on ever pattern matching on something like that13/07 03:39
copumpkinI can bring one or both sides into scope with a with block but then it barfs in other ways13/07 03:39
copumpkinand the goal won't normalize unless I can convince agda that there's indeed a refl in there13/07 03:40
* djahandarie doesn't understand13/07 03:40
copumpkinthat proof irrelevance thing is a horrible hack, basically :P13/07 03:40
copumpkinit might be possible to do away with it13/07 03:40
copumpkinbut I've already ripped most of the hair out of my head13/07 03:40
djahandarielol13/07 03:40
xplatthe one time i used proof irrelevance it was kind of cool13/07 03:40
xplatwhen i wrote a helper function to 'enlarge' substs13/07 03:41
copumpkindjahandarie: basically it lets me say "yo, I have a proof of this thing, and you can't see it's a refl, but I'm gonna prove to you that it is cause it's equivalent to refl"13/07 03:41
xplatyo yo ma13/07 03:42
copumpkinbut I don't actually end up using that proof anyway, after all that13/07 03:42
copumpkinnow I need to figure out what to do about my indices being a pain to write literals for13/07 03:42
copumpkinhow do you enlarge substs btw?13/07 03:43
xplatwhat does a literal look like?13/07 03:43
copumpkinoh13/07 03:43
copumpkinwell13/07 03:43
copumpkinZ :: i1 :: i2 :: i313/07 03:43
copumpkinideally13/07 03:43
copumpkinhowever13/07 03:43
copumpkinit turns horribly yellow everywhere it can13/07 03:43
copumpkineven if it has a defined type13/07 03:43
copumpkindjahandarie, xplat: when do y'all get to phi?13/07 03:45
djahandarieFriday morning13/07 03:45
djahandarieGet to the station at 11, no idea when I'm actually going to appear13/07 03:46
copumpkinah13/07 03:46
xplatwell, first i wrote a sub-cong thing13/07 03:46
xplater, subst-cong13/07 03:46
xplatit proves subst (P . f) eq thing == subst P (cong f eq) thing13/07 03:48
copumpkinoh13/07 03:48
xplatthen i proved subst-irrel, which says subst's result is the same no matter what equality you give it (using proof irrelevance)13/07 03:49
copumpkinah, I see13/07 03:49
xplatso using both together, i have 'fatten', which proves subst (P . f) eq thing == subst P eq' thing13/07 03:51
xplatso it lets you move the subst along a function and change the equality it depends on13/07 03:51
xplatwhich is handy when the function is a projection that eliminates everything that wasn't definitionally equal, because then eq' is refl and the subst disappears on the RHS13/07 03:52
xplati'm pretty sure i pushed the version of Categories.Power.Functorial that uses that13/07 03:56
copumpkinah, cool13/07 03:56
copumpkinhaven't looked at CT in a while13/07 03:56
copumpkinI'm still half-aching to do the spivak categorical databases thing in it13/07 03:57
djahandarieAh, that sounds like a good idea13/07 03:57
djahandarieI'm planning on hacking on that at hac phi13/07 03:57
djahandarieNot sure what specifically I'm going to do, but there's plenty :p13/07 03:57
copumpkin:)13/07 03:59
copumpkinI'm getting in saturday morning, really early13/07 03:59
copumpkincause of the aforementioned cheapskateness13/07 03:59
nappingwhat's the story with pattern matching lambdas?13/07 04:20
nappingI'd like some for nested pairs13/07 04:21
copumpkin?13/07 04:22
nappingThere was some discussion on the list about pattern matching in anonymous functions13/07 04:24
nappingDo you remember if anything was implemented?13/07 04:24
copumpkinoh13/07 04:25
copumpkinI don't think it's been rolled in yet13/07 04:25
copumpkinnot sure, haven't heard much about that13/07 04:25
nappingwell, it's kind of annoying to write functions over Σ (Fin 5) X, if you have to write explicit patterns for the number13/07 04:27
copumpkinyeah13/07 04:27
nappingI was hoping to use something akin to lookup over a vector of cases13/07 04:27
nappingbut destructuring the argument is a bit annoying13/07 04:27
copumpkinyeah, that'd be nice13/07 04:28
copumpkinI guess you could write that vector-alike Fin-indexed heterogeneous thing13/07 04:28
nappingwell, curry works I guess13/07 04:28
copumpkinand an indexing function13/07 04:28
nappingactually, I found this works quite nicely for the vector:13/07 04:29
nappingdata IHVec : {n : ℕ}{ix : Vec Set n} → Set₁ where13/07 04:29
napping  _∷_ : ∀{A n as} → A → IHVec {n} {as} → IHVec {suc n} {A ∷ as}13/07 04:29
napping  [] : IHVec {zero} {[]}13/07 04:29
copumpkinah, fair enough13/07 04:29
copumpkinwhy implicit?13/07 04:29
copumpkinand why a Vec of types and not a List?13/07 04:29
nappingbecause they can be inferred13/07 04:29
nappinghmm, I guess I could probably use a list13/07 04:30
nappingthen lookup would be indexed by Fin (length ix)13/07 04:30
copumpkinI've used a list for similar purposes13/07 04:30
nappinghmm, I suppose I can compute better types13/07 04:33
xplatit's probably easier in agda to use a vec and infer n than use Fin (length ix)13/07 04:33
copumpkinfair enough13/07 04:33
xplatagda in general seems to work better when you pull as many common pieces out to the indices (and separate implicits) as possible rather than computing them13/07 04:35
nappingwell, here I have enough information from other arguments to compute exactly the types and shapes of the lambdas I need13/07 04:38
nappingbut I'm continuing a bit without it13/07 04:38
copumpkinwhat are you working on, by the way?13/07 04:38
nappinggeneric programming over nested data types13/07 04:38
copumpkin:O13/07 04:39
nappingmodule Nested(Ix : Set; tenv : ℕ; Env : Vec (Ix → Set) tenv) where13/07 04:39
napping  data CArg : Set where rec : (Ix → Ix) → CArg ; plain : Fin tenv → CArg13/07 04:39
nappingthen a description is just   sig = ∃ (Vec (∃ (Vec CArg)))13/07 04:39
copumpkinsounds a bit like W, minus the recursion13/07 04:39
copumpkinI guess it's just a generic product-like thing13/07 04:40
nappingsimilar to W, except all that varies is the indices13/07 04:40
xplatis this the same as what are called nested data types in haskell?13/07 04:41
nappingyes13/07 04:44
* copumpkin eats kfish 13/07 04:44
nappinginductive types without dependencies between arguments, where each constructor targets the whole family, but recursive constructor arguments can be at differeint indices13/07 04:45
* copumpkin eats seafood 13/07 04:45
nappingmy running example is de-bruijn lambda terms13/07 04:45
* seafood gets digested13/07 04:45
seafoodWho'd have thought that a pumpkin would devour seafood? If anything it should be other way around.13/07 04:45
* copumpkin burps13/07 04:46
xplatpumpkins, as fruits, are at the bottom of the food chain.  copumpkins, naturally, are top predators.13/07 04:47
kfishyow!13/07 04:48
* copumpkin eats all of #agda13/07 04:48
copumpkinxplat: does that mean I'm an initial object in the category of the eat ordering?13/07 04:49
copumpkinpumpkin on the other hand would be terminal13/07 04:58
djahandariecopumpkin, by the way, why the hell are you trying to do the trip under $200? Aren't you like swimming in cash? :p13/07 05:51
copumpkinI wouldn't say I'm swimming in cash :P I think being frugal is good!13/07 05:51
copumpkinit's also efficient!13/07 05:52
djahandarieYou work at a finance place, they pay in suitcases of cash there!13/07 05:52
copumpkinhah13/07 05:52
copumpkinfinance pays more when trading is involved, and it isn't here :)13/07 05:53
copumpkinit's not bad, though13/07 05:53
djahandarieAw, that doesn't sound as risky13/07 05:53
* Saizan wonders if there's a sensible way to mix "with" syntax and monads13/07 15:27
pigworkerSaizan: it should be no big deal to elaborate "with" via bind13/07 16:34
* pigworker plots elaboration parametrized by an ambient monad13/07 16:36
xplatheh, i want to have syntax interpretable in arbitrary categories equipped with sufficient gadgetry13/07 16:56
kosmikusxplat: oh no, you're saying just what pigworker wants to hear ;)13/07 16:58
augurpigworker: what is this elaboration you speak of13/07 16:58
pigworkerwell, you write high-level code with lots of stuff left implicit, and the poor machine is left to translate that into a more explicit language underneath -- a kernel language; "elaboration" is what we call that process13/07 17:01
augurhm13/07 17:03
pigworkerEpigram is a bit more explicit about the separation. The kernel language is always under review, but we can usually say what we think it is.13/07 17:03
Peakerpigworker: perhaps some of these "low-level" details would be interesting to a prospective reader too.. And would probably help completions in the editor/etc..  I think elaborations should probably happen interactively at edit-time13/07 17:04
Peaker(though maybe not all of the elaboration results should be visible by default)13/07 17:04
pigworkerindeed, incremental elaboration was always the Epigram model13/07 17:04
augurpigworker: when you say leaving things implicit, what are you talking about? implicit /arguments/? or something else?13/07 17:06
xplatwell, there's more than that13/07 17:07
pigworkerthere sure is13/07 17:07
xplatif you use an explicitly-typed kernel language, you usually have to add a lot of type annotations in elaboration, for just the most obvious.13/07 17:08
augurhm. im not sure i follow but o13/07 17:08
pigworkerxplat: although, with a bidirectionally typed kernel language, it's not as bad as it used to be13/07 17:08
xplateven beyond ones that are represented as implicit arguments13/07 17:08
augurwhats a bidirectionally typed language?13/07 17:09
pigworkersome syntactic constructs make it easy to infer a type, others make it easier to start from the type and then check the term13/07 17:11
augurhm13/07 17:12
pigworkerwhen we do bidirectional checking, we split the term syntax in two -- terms for inference and terms for checking13/07 17:12
xplata bidirectionally-typed language picks an explicit direction for each construct13/07 17:13
pigworkerfor example, it's a good move to *check* lambda13/07 17:13
xplatif you infer lambda instead, you need (in theory) a full type on each abstracted variable13/07 17:14
pigworker(x : S) -> T checks \ x -> t if x : S |- T checks t     the point is that you get the type of x from the Pi, so you don't need a label on the lambda13/07 17:14
augurhm..13/07 17:14
xplatand then you usually end up like in agda creating metas and letting them get injected from top down anyway13/07 17:15
augurwould that also be avoided thanks to top-down constraints, tho?13/07 17:15
auguri mean, if you have \ x -> t in an environment that requires a  (x : S) -> T you know x : S, surely13/07 17:16
auguror is that just bidirectionality13/07 17:16
pigworkeryeah, the point is that you need that requirement, or you know jack about x13/07 17:16
augurcause i feel like that would just happen with bottom up + unification13/07 17:16
pigworkeraugur: unification is too damn hard13/07 17:16
augurpigworker: ah, with dependent types, yeah13/07 17:17
xplataugur: in agda that's interpreted as \(x : _) -> t, and then that gets worked out by implicit inference13/07 17:17
augurim thinking non-dependent types i guess13/07 17:17
xplator not worked out, as the case may be, since sometimes it's too hard13/07 17:17
xplatbut even if it does get worked out, it's a lot more work to do13/07 17:18
pigworkerunification struggles outside of the first order fragment13/07 17:18
pigworkeralthough there is an art of the possible13/07 17:19
xplatthe fragment of agda without irrelevance does a pretty good job13/07 17:20
xplat...eventually.13/07 17:20
augurive only ever written unifier-based type checkers for the simply typed LC + type operators and universal quantification13/07 17:20
pigworkerxplat: agreed; sometimes it doesn't quite prune properly, I think13/07 17:21
pigworkeraugur: good place to start, but you can get a lot more done if you're a bit more prescriptive of the way you expect information to flow13/07 17:22
augurseems it. i'll have to read about this some time13/07 17:23
pigworkerwe expect to know the types of variables (and that lambda rule maintains that property)13/07 17:23
pigworkerfor application, we expect to infer the type of the function, and in that way to learn the type at which to check the argument13/07 17:24
pigworkeroh yeah, and once the argument's ok, that allows us to infer the type of the whole application13/07 17:25
augurwhat do you mean when you say "know the types of variables"?13/07 17:27
pigworkerI mean that the typechecker carries a type assignment, telling the type of every variable in scope.13/07 17:28
augurahh13/07 17:28
augurhmm13/07 17:28
augurso a type environment is carried down into substructure instead of just being synthesized from the environments passed up from substructure13/07 17:29
pigworkeryes13/07 17:29
augurand that gets you a lot more type checking flexibility?13/07 17:30
pigworkerwell, you work from a more informed perspective, certainly13/07 17:31
augurinteresting.13/07 17:31
pigworkerWe can overload constructors because concrete data occur in checking positions, so we already know which datatype we want.13/07 17:32
Saizanso you use it both for the kernel and for the user-facing language?13/07 17:34
pigworkerIn Epigram, elaboration uses type information to translate named constructors into the numeric tags we use in the kernel language.13/07 17:35
pigworkerSaizan: indeed, it makes sense to use a bidirectional strategy both for elaboration and for checking the kernel13/07 17:35
Saizanand argument reconstruction (the stuff that handles _ in expressions) ends up being part of elaboration or at least being interleaved with it?13/07 17:37
pigworkeryes13/07 17:37
pigworkeran elaborator is an operating system, terrifyingly enough13/07 17:38
pigworker_ is a non-blocking read13/07 17:39
augurunrelatedly, pigworker, do you know of any demonstrations of using dependent types for seeming magic in the coincidences-as-consequences sense?13/07 17:39
pigworkerI'm not sure what you mean.13/07 17:40
augurwell, iinm, one of your recurrent themes is that dependently typed programming lets you turn coincidences into consequences13/07 17:41
pigworkerThere are plenty of examples where more-or-less the program you would have written anyway typechecks at a richer type, guaranteeing a property you might otherwise have had to prove.13/07 17:41
augurbut, in general, your examples are things like Vec _++_ being length-summing, maps being length-preserving, etc.13/07 17:41
xplatlike 'this list just happens to always be nonempty so head won't crash the program' vs 'this is a nonempty-list so you can call head on it'13/07 17:42
augurbut i get the sense that what you're thinking of is not simply just that, but rather something more insightful and seemingly magical13/07 17:42
xplat?13/07 17:42
pigworkerthings like "the typechecker produces the well-typed version of the term that you give it (or barfs)"13/07 17:43
djahandariepigworker, I have to say that all the abbreviations in this paste make it slightly hard to follow :(13/07 17:43
pigworkerthings like "the compiler produces the bytecode that agrees with the interpreter"13/07 17:43
djahandarie(The BInx paste)13/07 17:43
xplathm, Vec _++_ is length-summing because List _++_ is length-summing because List _++_ is decorated addition13/07 17:43
augurpigworker: hm..13/07 17:44
pigworkerdjahandarie: I'm in the middle of blogging about it13/07 17:44
xplatalthough i'm not sure how well '_++_ is decorated addition works' since addition is also commutative13/07 17:44
djahandarieOh, cool :)13/07 17:44
xplatso whether you get ++ by decorating addition depends how you wrote _+_13/07 17:45
pigworkerxplat: depends on your implementation of addition13/07 17:45
pigworkersnap!13/07 17:45
xplatwell, that means the form of decoration that goes from _+_ to _++_ is non-extensional13/07 17:47
pigworkerI guess classic examples are of the form "evaluating a term of type T gives a value of type T", which is traditionally a theorem one proves about one's evaluator, rather than its type.13/07 17:47
Saizanor "normalization respects semantics"13/07 17:48
pigworkerxplat: indeed; and there's clearly a whole pile of other operations for which length has that homomorphic behaviour13/07 17:49
xplatlike interleave ...13/07 17:50
xplatthe agda stdlib has an alternate _+_ which decorates to interleave13/07 17:50
pigworkeror "if either list is nonempty, make the relevant number of copies of the leftmost element"13/07 17:50
xplatjust in order to make some proofs/types easier to write13/07 17:51
pigworkerxplat: indeed, there's a recursor on Nat * Nat which guarantees to produce commutative operations13/07 17:52
xplatoh, is there?13/07 17:52
pigworker"either one is zero or both are suc"13/07 17:52
augurpigworker: hm. i guess i got a slightly different sense of the intention behind the coincidence-consequence stuff.13/07 17:52
augurah well!13/07 17:52
pigworkerThere are other coincidences about...13/07 17:53
xplatoh, the one-is-zero case gets passed the other, and the both-are-suc case gets ... what?13/07 17:53
pigworkerxplat: the pair of predecessors13/07 17:54
pigworkerand the result of processing them13/07 17:54
pigworkerer, just the latter, until we've got quotients nailed13/07 17:54
xplatah, an unordered pair13/07 17:55
pigworkeryep13/07 17:55
xplatso you're working on quotients for epigram?13/07 17:55
pigworkeroh yes13/07 17:55
xplatthis category theory library i'm working on with copumpkin would be about a dozen times easier with quotients13/07 17:55
pigworkerinasmuch as "working" can be said to apply13/07 17:56
pigworkerI can well believe it; even extensionality would help, I suppose13/07 17:56
augurwhat are quotients :o13/07 18:06
auguroh wait, do you mean equavalence classes?13/07 18:07
pigworkeryeah, things-up-to-some-equivalence13/07 18:12
augurhmm13/07 18:15
pigworkerif R : X -> X -> Prop is an equivalence relation, then X / R is the set of R-equivalence classes13/07 18:20
pigworker(in Epigram, Prop is a proof-irrelevant fragment of Set)13/07 18:20
pigworkeryou can form equivalence classes, so if x : X, then [ x ] : X / R13/07 18:21
pigworkerbut you can only unpack the representative of a class if you can prove that it doesn't matter which representative you get13/07 18:23
pigworkerPropositional equality is type-directed, and we have that [ x ] == [ y ] in X / R  <=>  R x y.13/07 18:24
guerrillagot a reference for the some typing rules for for quotient types?13/07 18:29
djahandariepigworker, why are you doing Prop-style irrelevence rather than Agda-style irrelevence?13/07 18:30
pigworkerbecause Agda-style irrelevance doesn't work properly13/07 18:30
pigworkerin particular, I want to be sure I can eliminate equations in actual (relevant) computations13/07 18:31
pigworkery'know, like subst : {X : Set}{x y : X} -> x == y -> (P : X -> Set) -> P x -> P y13/07 18:34
pigworkerI can make that equation proof-irrelevant for definitional equality, even though I can't erase the proof in open computation. I can certainly erase it at run time.13/07 18:35
pigworkerguerilla: there's work by Maria Emilia (Milly) Maietti; there's a blog post by me http://www.e-pig.org/epilogue/?p=319 (the general notion is much older of course, and quotients work quite well in extensional type theory)13/07 18:44
guerrillaok thanks13/07 18:45
pigworkerI should, of course, admit that there are circumstances where Agda-style irrelevance is useful, and not covered by Prop or various other erasure methods. They involve putting genuine data beyond use, e.g. lengths in appending vectors.13/07 18:54
copumpkinxplat: damn right13/07 18:58
copumpkindoes pigworker have free quotients for us yet? :D13/07 18:58
pigworkerthey were in Epigram 2 at one point, and they're on the hit list for the current reconstruction13/07 18:59
pigworkerI have the basic picture, but mysteries remain.13/07 19:00
djahandarieAre we on Epigram 3 yet13/07 19:01
pigworkerthe traditional joke is that the version number is incremented at each mention in a conversation13/07 19:01
djahandarielol13/07 19:01
pigworkerso yes, we're on Epigram 413/07 19:02
djahandarieDoesn't that mean that we're all constantly lying?13/07 19:02
cayleeno, there's probably a kripke semantics where we're all good13/07 19:06
pigworker(x : Zero) -> P x holds, regardless of P13/07 19:25
pigworkerlying about the hypothetical but nonexistent can be difficult13/07 19:27
kosmikusEpigram version numbering seems to have even more inflation than that of Firefox13/07 20:24
kosmikusFirefox at least still makes a release (so far) before incrementing the major number ...13/07 20:24
augurkosmikus: version numbers are for conceptual distinctions more than anything13/07 20:33
augurEpigram 2 isnt out yet, but its still a massive design leap13/07 20:33
augurthis is how all version number works13/07 20:33
auguryou dont roll over your whole number portion of a version number without major design changes, but it doesnt have to be released yet13/07 20:34
auguri mean, its not at all a problem to talk about the Epigram 2 alpha/beta13/07 20:34
auguryou wouldnt want to call it the Epigram 1.8 alpha, that'd be misleading13/07 20:35
augurthat suggests smaller, incremental changes, whereas going from Epigram 1.x to Epigram 2 implies something major has changed13/07 20:35
dolioWait, Epigram is being rewritten again, or something?13/07 20:37
augurdolio: Epigram 3 is in the pipeline, havent you heard?13/07 20:38
djahandarieYou mean Epigram 4.13/07 20:38
augurEpigram 5 is almost ready for release doncha know13/07 20:38
dolioYes, Epigram 6.13/07 20:39
augurhonestly I think i'll stick with O'Epigram13/07 20:39
augurOEpigram is way better than Epigram Light13/07 20:41
augurholy moly what is this MetaOCaml stuff13/07 20:42
augurit looks like japanese style smilies13/07 20:42
augur.<~^_^~>.13/07 20:42
augur<(*.*<)13/07 20:43
djahandarieDon't give anyone in here any unnecessary ideas, augur.13/07 20:44
augurdjahandarie: what, you dont want to program Epifunge?13/07 20:44
augurits already 2 dimensional!13/07 20:45
djahandarieI just want to avoid any smiley faces in Agda code13/07 20:46
augurtoo late13/07 20:46
auguroh man, every time someone uses :> in haskell ...13/07 20:46
kosmikusjust for the record: I'm well aware that the amount of innvoation in each unreleased new version of Epigram is certainly significantly higher compared to the amount of innovation in a new Firefox version.13/07 20:46
augurwhat are you all smarmy about!? D:13/07 20:46
augur:> :> :>13/07 20:46
djahandarie(屮゚Д゚)屮_щ(゚д゚щ) : forall {a} {A : Set a} -> A -> A13/07 20:49
augurreasonable13/07 20:49
augurcc shan's presentation on delimited continuations that he gave in japan uses 出13/07 20:50
auguras one of the operators13/07 20:50
augurso you see shit like13/07 20:50
augur出x.foo(x)13/07 20:51
augurwhich is absolutely bizarre13/07 20:51
djahandarieAll the Japanese Agdaers I know don't actually use any Japanese in their code, thankfully13/07 20:51
djahandarieThey do use it in their comments sometimes though13/07 20:51
augurtheyre obviously not holdovers from Applescript13/07 20:53
auguragda is surprisingly useful for making fake natlang13/07 20:54
pigworkerkosmikus: I'm grateful for your confidence. We're primarily in it to generate ideas, but we now seem quite divergent from Agda as well as from Coq. So we'd better ship something sometime.13/07 21:23
kosmikuspigworker: yeah, that only makes it more interesting13/07 21:24
kosmikusI don't need three languages that are almost the same :)13/07 21:24
copumpkinxplat!!!13/07 21:24
copumpkinpigworker: I can't wait to rewrite the repa-alike in epigram!! and the CT library!13/07 21:24
copumpkinmmm13/07 21:24
copumpkin:P13/07 21:24
pigworkerMeanwhile, I've got a bizarre plan to add a limited form of internal mu and nu to the levitation universe.13/07 21:25
pigworkerI've been blogging my BInx hack, and am pausing to wonder if it's more complicated than it needs to be.13/07 21:26
djahandarieWhy limited?13/07 21:26
pigworkerThe essence of the idea is really simple. You define a recursive container like \ X . mu Y . (stuff strictly +ve in X and Y)13/07 21:27
pigworkerdjahandrie: I'll get there...13/07 21:27
pigworkerThe question is how to allow local mu inside that stuff (or local nu for that matter).13/07 21:28
cowworkerI can tell you all about mu13/07 21:29
pigworkerThe reason the general case is tricky is that it turns into a syntax with binding. All your specific encoded types work fine, but generic programming is really evil.13/07 21:29
kosmikus:)13/07 21:29
pigworkerYou end up working with substitutions that have to go under binders.13/07 21:30
djahandariecowworker, careful, we may get 'oink' introduced into the type system...13/07 21:30
kosmikuscowworker: oh, you have a repa-alike in Agda?13/07 21:30
pigworkerI have a very simple restriction. You can have another mu X inside the mu Y, shadowing the \ X, then another mu Y inside that, and so on. You get a sliding window of two variables, like a goldfish brain.13/07 21:32
pigworkerSubstituting for the outermost variable never goes under a binder!13/07 21:33
cowworkerkosmikus: yes! well, the ugly skeleton of one13/07 21:33
pigworkerIt's a shit hack, but it lets you write rose trees and stuff like that.13/07 21:34
kosmikuscowworker: nice!13/07 21:34
cowworkerhttp://hpaste.org/4898513/07 21:34
cowworkerread it and weep13/07 21:35
pigworkercowworker: repa is totally asking for it13/07 21:35
copumpkinyeah, the index/shape story in repa is rather confusing, in my opinion13/07 21:35
copumpkinI think the agda version is a lot cleaner13/07 21:35
copumpkinjust ignore the horrific Index<->Fin proof13/07 21:35
Eduard_Munteanudjahandarie: was that all Cyrillic? I can't tell13/07 21:36
copumpkinthe only problem with the agda version now is that shapes are indexed by the result of a multiplication13/07 21:36
copumpkinand that makes it hard to construct indices of a shape from scratch13/07 21:36
djahandarieEduard_Munteanu, Cyrillic?!13/07 21:37
copumpkinanyone have any ideas about that?13/07 21:37
kosmikuscopumpkin: of course. when I saw repa, I also thought how nice it would be to do it in Agda.13/07 21:37
pigworkerdon't touch the green slime...13/07 21:37
Eduard_Munteanudjahandarie: Д looks like the russian 'D' to me13/07 21:37
djahandarieEduard_Munteanu, I think it is13/07 21:37
kosmikuscopumpkin: nice work :)13/07 21:38
copumpkinthanks :P13/07 21:38
copumpkinI plan on separating it into modules and doing more nice stuff13/07 21:38
Eduard_Munteanuщ too, but 屮somehow doesn't seem Cyrillic (if I'm not misspelling it) script13/07 21:38
copumpkinmaybe an actual FFI to haskell if I'm feeling adventurous13/07 21:38
kosmikusyes, would be nice to actually put it into a proper library13/07 21:38
kosmikusand we really need a Hackage for Agda13/07 21:38
copumpkinand I'd like to explore those slices a bit more13/07 21:38
copumpkinsince I haven't quite decided how they should work13/07 21:38
djahandarieEduard_Munteanu, the second one is Japanese13/07 21:38
kosmikuscopumpkin: are you going to ICFP, by chance?13/07 21:39
Eduard_MunteanuAh. (I can't read some of those, I see some boxes, dang DejaVu)13/07 21:39
copumpkinkosmikus: sadly not :(13/07 21:39
copumpkincan't really justify a trip to japan when I have a job :)13/07 21:39
copumpkinand limited vacation days13/07 21:39
djahandarieI can't justify a trip to Japan when I don't have a job13/07 21:40
copumpkin:)13/07 21:41
kosmikuscopumpkin: yes, it's tough13/07 21:41
kosmikuscopumpkin: for me, most conference trips are unpaid time as well13/07 21:41
copumpkinyeah :/13/07 21:42
kosmikusICFP is a corner case13/07 21:42
pigworkerCUFP ?13/07 21:42
Eduard_MunteanuDamn down-to-Earth jobs don't let you leave on a sabbatical.13/07 21:42
copumpkinI would've liked to evangelize my company a bit at CUFP at least13/07 21:42
kosmikuspigworker: you're going, right? or did you say you're only going to the AIM and DTP thing?13/07 21:43
pigworkerIt turns out I can't go.13/07 21:43
kosmikusoh13/07 21:44
kosmikuswhy not?13/07 21:44
pigworkerFor maddening, partly self-inflicted reasons...13/07 21:44
copumpkinpigworker: come to hac phi instead ;)13/07 21:44
kosmikuspigworker: so you're not going to Japan at all then?13/07 21:45
pigworkerI have to attend a three-day in-service training course, 14-16 Sep, which blows a hole out of the middle of it and takes out DTP (which I'm involved with organising).13/07 21:45
kosmikuswhat's an in-service training course?13/07 21:45
pigworkerI have to go to three days of indoctrination about how to be a good university teacher.13/07 21:46
kosmikusheh13/07 21:46
kosmikusand they decide when?13/07 21:46
pigworkerIt's part of my probation process. They need to cover their arses by showing that I've been indoctrinated.13/07 21:46
kosmikusand you can't do it half a year later?13/07 21:46
pigworkerI've been doing it half a year later for the last three years. Now it's overdue.13/07 21:47
kosmikus:)13/07 21:47
kosmikusthat's a pity13/07 21:47
pigworkerIt always clashes with something more urgent/interesting.13/07 21:47
kosmikuswe'll meet at Nijmegen, though13/07 21:48
pigworkerNow it's do-it-or-get-fired.13/07 21:48
pigworkeryes, I'll be in Nijmegen13/07 21:48
kosmikusyes, I just registered13/07 21:48
kosmikusso I'll be there, too13/07 21:48
pigworkerer, um, better do that13/07 21:48
kosmikushuh?13/07 21:48
kosmikusah, you mean, you haven't registered yet?13/07 21:49
pigworkeryeah13/07 21:49
kosmikusI think the 15th is early registration deadline13/07 21:49
kosmikusbut for the workshop, it only shifts from 40 to 50 EUR13/07 21:49
kosmikusso it'll still be affordable13/07 21:49
kosmikusI don't know if you go to the whole thing13/07 21:49
kosmikusI don't13/07 21:50
pigworkerstill, that's a noticeable amount of beer13/07 21:50
pigworkerI don't know if I have the spare energy for the whole thing.13/07 21:50
kosmikusIf you're in .nl already on Friday, you might consider giving a guest lecture at the Utrecht Summer School13/07 21:50
kosmikusit's about Haskell, not dependent types13/07 21:51
djahandarieIsn't that what SHE is for?13/07 21:51
djahandarie;)13/07 21:51
kosmikusbut I'm sure you could deliver something fun :)13/07 21:51
pigworkerI might well be up for that.13/07 21:51
kosmikusah cool13/07 21:51
djahandariecopumpkin, probably a little late for Hac Phi :p13/07 21:51
xplatdidn't netscape jump straight from 4 to 6 with 5 never being released?13/07 22:34
xplatspeaking of unreleased versions13/07 22:34
copumpkinnot sure13/07 23:02
--- Day changed Thu Jul 14 2011
copumpkinomg agda14/07 01:14
djahandariezomg14/07 01:14
Peakeromg given a DependentlyTypedLanguage, expected a Fad14/07 01:29
PeakerPossible resolution: Add Fad instance declaration to DependentlyTypedLanguage14/07 01:30
xplatyo dawg i herd u like fads so i put a fad in your dependently typed language so u can fad while u type dependently14/07 02:03
copumpkin:O14/07 02:14
* copumpkin tries to decide what to do next14/07 02:15
djahandarieAttempt to do internal logic stuff so some of the work is done for me when I try to do it at hac phi :p14/07 02:16
copumpkinthen you'd be bored at hac phi14/07 02:17
copumpkinxplat: any plans for hac phi?14/07 02:18
augurcopumpkin: oh sure, ask xplat T_T14/07 02:18
copumpkinaugur: I already know what you're doing :P but what are you doing?14/07 02:19
auguroh you mean project plans14/07 02:19
copumpkinyeah14/07 02:19
augurin that case nevermind!14/07 02:20
copumpkin:)14/07 02:26
copumpkinanyone have any good ideas for what to call the repa-alike in agda?14/07 02:28
copumpkinagdarepa? :P14/07 02:29
copumpkinagdrepa14/07 02:29
dolioderp14/07 02:29
copumpkinderpa? :P14/07 02:29
djahandarieDARPA14/07 02:33
xplatData.Array.Shaped?14/07 04:55
copumpkinRegular? :)14/07 04:56
copumpkinI put it up at https://github.com/copumpkin/derpa14/07 04:59
copumpkin>_>14/07 04:59
copumpkinI need a name for another library I'm working on14/07 05:11
copumpkinI hate naming :(14/07 05:11
copumpkinI want a good powerful name14/07 05:19
xplatsay, why do we ever use T foo?14/07 13:46
xplati mean, it's useful because the T foo has a unique proof (if any) so can be inferred14/07 13:47
xplatbut if you have a Dec for some property, you can avoid going through the boolean middleman, and still get unique proof, and even get the proof reconstructor generically for all Dec14/07 13:49
Saizanyou still need a T-alike for Dec if you want it inferred14/07 13:53
xplati mean, ok, to fully replace it you'd also need a Semidec type with 'Yes' and 'PerhapsNot' constructors, but i've never seen T used in that situation anyway14/07 13:53
xplatSaizan: sure, but then you can get a function that gives you a proof of the real property for any value of the T-alike, instead of having to write a different one for each predicate14/07 13:54
xplatthus changing a design pattern to a library function14/07 13:56
Saizanyeah, though one could even go more general: T : Either A B -> Set; T (Left _) = \top; T (Right _) = \bot;14/07 13:59
xplatthat would be useful too (i'd put \top on the right though) but the Dec case would be more useful as an alternative to most existing uses of T14/07 14:02
xplatWhen : {A : Set} -> Dec A -> Set ; When (Yes _) = \top ; When (No _) = \bot ; proof : {A : Set} -> {d : Dec A} -> When d -> A ; proof {d = Yes a} _ = a ; proof {d = No _} ()14/07 14:08
Saizanperhaps one should just define Dec with Either14/07 14:15
Saizanthough i don't see Bool = Either \top \top going through :)14/07 14:15
xplatactually yoou'd need to make When a real data family for that to work14/07 14:16
Saizanwhere "that" is keeping d implicit?14/07 14:17
xplatyeah14/07 14:18
Saizanyou can wrap When in a record, so you get both the inferences14/07 14:18
xplathm, yes, a record would work14/07 14:18
xplatrecord When {A : Set} (d : Dec A) : Set where { constructor when ; field raw : WhenRaw d }14/07 14:22
xplatand proof might need (when ()) in the No case14/07 14:23
Saizanyep14/07 14:25
xplatand then it just becomes a general pattern for using nonreflective decision procedures to infer noncanonical proofs implicitly14/07 14:29
xplatbut a very simple pattern : foo : ... {wd : When d} ... ; foo ... {wd = wd} ... with proof wd14/07 14:30
xplatit'd maybe be nice to fold the semidecision version of that into the language so you could substitute your own strategy/explicit proof if you want, but it wouldn't necessarily be necessary with a full decision procedure14/07 14:35
xplatalthough some deciders can be slow, so you might want to override them in certain cases anyway14/07 14:35
xplati wonder if noncanonical implicits cover this case already14/07 14:36
xplatbut it sounds more like they were explicitly designed to not cover it14/07 14:37
xplatcome to think of it, default arguments would largely take care of everything14/07 14:49
Saizandefault?14/07 14:50
xplator at least, some kind of 'failable default'14/07 14:51
xplatyou write { foo : A = blah } where blah's type is Maybe A or something14/07 14:52
xplatand if foo isn't supplied it will use blah (in the just case) or fail (for nothing) instead of trying to infer an A14/07 14:52
xplati suppose it would also need to fail if it can't compute blah far enough to get a constructor at the head14/07 14:54
xplati wonder if it would act badly because of that14/07 14:55
xplathm, maybe it also wouldn't propagate as well as a T foo14/07 14:57
xplatin the T foo case if you call a function that uses the same T foo and foo can't be computed, the type context still indicates that there is an existing term of T foo14/07 14:59
xplatand it is unique14/07 14:59
xplatwhereas in the default argument case the default won't propagate to other functions using the same strategy to generate A's, they will just try to apply their strategy in place and foo being around isn't a guarantee it'll work since foo might have been passed explicitly14/07 15:02
xplat(Whens, however, should work as well as Ts)14/07 15:04
xplatmaybe if defauts go with NCIs, and the indeterminate case (and maybe the nothing case?) falls back to scope-scraping?  but that might be too complicated ...14/07 15:09
xplati guess in that case regular implicits with defaults could fall back to _ if a strategy fails too14/07 15:12
djahandarieHm, I just realized my school has study abroad with Glasgow, Edinburgh, and Nottingham14/07 16:30
pigworkerdjahandarie: but not Strathclyde? (we're in central Glasgow, unlike Glasgow Uni); if you're interested, though, you could get in touch with the person in charge of student exchanges for Strathclyde Computer Science; guess who that is...14/07 17:46
* pigworker wishes Agda had pattern synonyms.14/07 19:47
djahandarieSAE?14/07 19:47
pigworkerwhat does SAE? mean?14/07 19:48
djahandarieStrathclyde Agda Enhancement14/07 19:48
pigworkerI'd have to do something different with the name. SAE is Stamped-Addressed-Envelope.14/07 19:49
pigworkerI don't entirely see why I can't write expressions in left-hand sides, so long as they evaluate to patterns.14/07 19:50
augurpigworker: what do you mean expressions in the lhs14/07 20:03
pigworkerI'm working in a universe of encoded datatypes, in which zero looks like < tt , <> > and suc n looks like < ff , n > (where <_>, <>, _,_, tt and ff are constructors).14/07 20:05
pigworkerI can define zero and suc that way, but I can't use those definitions on the lhs in a pattern match14/07 20:06
pigworkerBut (suc n) would have the right type (Nat) and evaluate to a perfectly good pattern.14/07 20:06
pigworkerI'd like to be able to use ordinary definitions to make abbreviations in patterns.14/07 20:07
augurpigworker: oh you mean you cant use `zero' and `suc n' in place of < tt , <> > and < ff , n >14/07 20:10
auguri see14/07 20:10
pigworkeryeah, encoded data is unreadable, but I get lots of handy kit for free14/07 20:11
augurdont i know it.14/07 20:11
auguroaao is art14/07 20:12
augurim sure this would be relatively easy to add to agda. you should put in a request14/07 20:12
pigworkermight just do that, in an informal way...14/07 20:13
djahandarieSomething makes me suspect that since it wasn't there already there is some sort of minor blockade along the way...14/07 20:14
pigworkerwell, it makes pattern-checking a bit trickier14/07 20:14
pigworkerusually it's very easy, because all the variables occur somewhere in a tree of constructors, so you can just push types into them14/07 20:15
auguri imagine you could do it quite easily, honestly14/07 20:18
augurprior to pattern-checking, you just look for non-constructor patterns and evaluate them14/07 20:18
augurat least as far as you can14/07 20:19
augurand since you have a partial evaluator, thats not a problem14/07 20:19
augurthen just replace the original with that result, and proceed as usual14/07 20:19
pigworkerthere's some annoyance preserving dotted patterns, but that's the plan, yeah14/07 20:19
augurdotted patterns give me a headache.14/07 20:19
auguryou should also "request" that the damn thing flips up implicit arguments into explicitdom14/07 20:20
augurwhen they cant be resolved14/07 20:20
augurbecause its really annoying to end up with yellow all over something that has no fricking implicit arguments14/07 20:20
pigworkeryes, you should be able to ask for a choice of places to put any such unknown14/07 20:21
augurits supposed to be a proof assistant, sort of. but this shit makes it more like a puzzle14/07 20:21
augurive been tempted to never use implicit arguments because of that14/07 20:22
pigworkerthere's a lot of UI thinking to be done, and nobody's really on the case14/07 20:22
pigworkerto be fair, you do get some sort of a code location printed out for missing implicits14/07 20:22
pigworkerI guess the other thing is that people need a clearer idea of what's likely to work.14/07 20:23
pigworkermost of us have good intuition for first-order unification; fewer of us have Miller's pattern unification so well ingrained14/07 20:24
* djahandarie is vaguely reminded of that strange value inference that was going on awhile back14/07 20:31
djahandariehttps://lists.chalmers.se/pipermail/agda/2011/002873.html14/07 20:31
pigworkerIt strikes me as underambitious. It basically says you can fill in the leaves of a program by doing some sort of proof about it. Why only the leaves? It's worth thinking about how to codevelop progs and proofs. Like James McKinna did in 1992.14/07 20:35
augurpigworker: where can i read more about this idea of leaves/non-leaves, etc.?14/07 20:37
auguri only vaguely get a sense of what it means14/07 20:37
Saizan^-initial's code branches on the natural into the zero and suc cases which have one leaf each14/07 20:39
pigworker"The view from the left" has a clear notion of program leaves (where you return a value on the rhs) vs program nodes (where you analyse your inputs in more detail, e.g. doing another case-split)14/07 20:39
pigworkerSaizan: yes, and by an amazing coincidence, ^ performs exactly the same case analysis!14/07 20:40
augurpigworker: ill have to read vftl again. i didnt have a clear sense of what was going on with this node/left thing the first time through14/07 20:42
pigworkerthe point is that programming with equations is an illusion; programs are really decision trees whose nodes analyse input and whose leaves generate output14/07 20:45
Saizanduring typechecking a more equational view would be nice though, e.g. having both trans refl x = x and trans x refl = x in the definitional equality14/07 20:54
pigworkeryeah, with just beta-iota, you can have one but not the other14/07 20:54
pigworkerbut, says I, you can add the other one as a simplification rule in the equality check without needing to change how evaluation works14/07 20:55
augurpigworker: i still dont get the decision tree thing tho :\14/07 21:01
auguri mean i sort of do, if by decision trees you mean in the pattern matching process, but other than that i dont see it14/07 21:01
pigworkerright -- a pattern matching function can be translated into a bunch of lambdas, then a tree of case expressions which only analyse variables14/07 21:03
pigworkerthe with construct allows you to have let-nodes, introducing variables which stand for new things14/07 21:05
pigworkerI mean, "new" as in not the inputs to the function, but computed from them14/07 21:06
copumpkinthoughtpolice: how's it going?14/07 22:26
thoughtpolicecopumpkin: oh, i'm doing something else atm, but i also got sidetracked by trying to figure out how goals work :P i guess it's also a bit harder because cpdt uses lots of tactics, and i don't really know how to go about proofing yet14/07 22:33
thoughtpolicecopumpkin: http://hpaste.org/49053 for what i did so far of translating the coq examples14/07 22:34
copumpkinI'd probably approach those a bit differently14/07 23:34
copumpkinmaybe indexing the stack language by the stack size or something14/07 23:35
copumpkinso the stack language would say how big the stack is before and how big it is afterwards14/07 23:37
copumpkinor something like that14/07 23:37
copumpkinmaybe that's just a pain14/07 23:37
copumpkinanyway, that proof should be pretty easy14/07 23:37
copumpkinbut it'll be nothing like it is in coq14/07 23:39
djahandarieYeah, it will be extremely different than stuff in Coq14/07 23:41
copumpkinprobably a lot more tedious :)14/07 23:41
djahandarieCoq lets you get away with not being as expressive with your structures by providing all sorts of tactics14/07 23:41
djahandarieIn Agda the correct path is often to encode as much as you can in the structure so you have less to prove by hand14/07 23:42
--- Day changed Fri Jul 15 2011
Saizananyone still has a link to that DSL to build parametricity theorems?15/07 00:47
Saizanhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems <- found15/07 00:49
xplatpigworker: yes, patterns like that would be nice, even for 'normal' data.  match (# 3) instead of (suc (suc (suc zero)))15/07 01:55
xplator even (2 + n) instead of (suc (suc n))15/07 01:56
xplatn + k patterns (well, k + n) for free15/07 01:56
copumpkindamn you, termination checker!15/07 02:41
pigworkerI really resent inlining stuff for the termination checker.15/07 02:44
pigworkerlike fold phi < t > = phi (map (fold phi) t)15/07 02:45
copumpkinI think the termination depth flag lets you avoid that now?15/07 02:46
pigworkerI guess I should stop using an ancient version, but... what?15/07 02:46
copumpkinhttp://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-815/07 02:47
pigworkerAs if it's not already awful having a termination oracle, we have one with a boredom threshold?15/07 02:47
copumpkinlook for "depth" on there15/07 02:47
copumpkin:)15/07 02:47
pigworkerType theory as language of evidence, how are ye?15/07 02:47
copumpkinnot sure whether that actually covers your case15/07 02:48
copumpkinbut it's helped a couple of mine15/07 02:48
pigworkerIn other news, I've just done the fiddly bit of delete for red-black trees.15/07 02:49
copumpkin:O15/07 02:49
copumpkinfor what?15/07 02:50
pigworkeror rather, half of it (but the other half is symmetric)15/07 02:50
pigworkerMcKinna and I knocked off insert in about 2005; delete is similar but takes a pile more brutality.15/07 02:51
pigworkerred-black trees -- binary search trees with a balancing invariant ?15/07 02:52
Peakerhttps://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs <-- relatively heroic, for Haskell15/07 02:52
copumpkinSTILL NO DELETE :P15/07 02:53
copumpkinnobody ever writes delete15/07 02:53
Peakerhttps://github.com/yairchu/red-black-tree/blob/master/AvlTree.hs   can delete15/07 02:53
copumpkinexcept for pigworker, apparently15/07 02:53
PeakerI nagged yairchu to add delete until he did :)15/07 02:53
Peakercute almost-DT trickery in there15/07 02:54
copumpkin:)15/07 02:55
pigworkerI avoid the need to represent slightly broken trees by using the zipper15/07 02:55
pigworkerI get the zipper for free by using encoded datatypes which happen to be differentiable15/07 02:57
pigworkerAs a result, the program is full of encoding artefacts and totally unreadable15/07 02:57
Peakerheh15/07 02:57
copumpkin:P15/07 02:57
copumpkinI think someone already gave you the solution to that!15/07 02:57
copumpkinSEA ;)15/07 02:57
copumpkinSAE, even15/07 02:58
pigworkernot bleeding likely15/07 02:59
copumpkinlolwtf15/07 04:26
copumpkinhttps://gist.github.com/108397815/07 04:26
djahandarieWow.15/07 04:28
djahandarieWhere'd you find that link?15/07 04:30
copumpkinhttp://snapplr.com/2y8n15/07 04:30
copumpkinand for anyone wondering, that does look like an agda-to-ruby compiler15/07 04:30
djahandarieHeh.15/07 04:30
copumpkinlarrytheliquid: you really like opposite ends of the spectrum, eh :)15/07 04:40
copumpkinit's neat though15/07 04:40
larrytheliquidcopumpkin: haha, has the link already made it in here?15/07 04:40
copumpkinI used to be a pretty hardcore rubyist15/07 04:40
copumpkinyeah, I noticed it on my github feed15/07 04:40
copumpkina while back15/07 04:40
copumpkinwell15/07 04:40
larrytheliquidagda->ruby backend https://gist.github.com/108397815/07 04:41
copumpkina while back = 15 minutes ago :P15/07 04:41
larrytheliquidfor anyone else =p15/07 04:41
larrytheliquidi mostly see it as a way to sneak agda into my job haha15/07 04:41
copumpkin:)15/07 04:41
copumpkinsounds pretty good to me15/07 04:42
larrytheliquidfor critical things like authorization frameworks, distributing monitoring services, etc15/07 04:42
larrytheliquidwhere correctness proofs actually mean a lot15/07 04:42
copumpkinwtf, my derpa library broke with the latest agda15/07 04:43
dolioAre you seriously calling it derpa?15/07 04:46
copumpkinfor now :P15/07 04:46
copumpkindependent REPA, permuted a little :)15/07 04:47
copumpkinI wonder if the version I just built is broken15/07 04:47
djahandarielarrytheliquid, did you use the same stuff that the JS backend that was made awhile ago uses?15/07 05:00
larrytheliquiddjahandarie: ya the changes are hacked right on top and very minor15/07 05:03
larrytheliquidmost of the stuff could be lifted to a common dynamic langs backend15/07 05:05
larrytheliquidthat could pretty easily compile to a variety of things like javascript/ruby/python/erlang/etc15/07 05:06
djahandarieThat's the impression I got when I looked at it quickly15/07 05:08
djahandarieAwesome that you already did it :p15/07 05:08
larrytheliquidwell i just edited the existing backend, didnt extract common stuff, but ya i was very happy with how easy it was15/07 05:09
larrytheliquidjust wanted to see a working proof of concept15/07 05:09
Saizanany examples of proofs exploiting parametricity? the paper by bernardy doesn't have much15/07 17:51
xplatthe ruby code looks a little ... well, it could use some help.  but that could probably be in common with the js backend too ...15/07 17:58
xplati mean, at least it works15/07 18:02
xplatinteresting that it's set up so that datatypes translate into church-encodings where the algebra (packed in a dictionary) is given as an argument15/07 18:04
xplatwell, as an index actually15/07 18:07
xplatthis is not how i would have thought to compile agda15/07 18:07
augurxplat: wat15/07 19:01
copumpkinxplat: wat15/07 20:36
the_fcolarrytheliquid: people are still talking about the ruby backend15/07 20:46
larrytheliquidthe_fco: haha, people = people in this channel or what?15/07 20:49
the_fcolarrytheliquid: No one in the grocery store mentioned it, so I guess it's here in the channel15/07 20:50
larrytheliquidmaybe a bay area grocery store though15/07 20:51
larrytheliquiddoes this channel log a transcript somewhere?15/07 20:51
djahandarieIt does15/07 20:52
the_fcooh, you are so type safe in the bay, here in Montréal it's too complicated to decide if you speak in english or in french, so no types15/07 20:52
djahandariehttp://agda.orangesquash.org.uk/15/07 20:52
larrytheliquiddjahandarie: cool ty15/07 20:53
djahandarieWow, we talk a lot more in here compared to 201015/07 20:54
copumpkinit's quite a bit larger than it was in 2010 too15/07 20:54
Saizanwe should still be safe unless someone posts tryagda to reddit15/07 20:56
larrytheliquidSaizan: were safe, no box would have enough memory15/07 20:57
Saizanheh, true15/07 21:00
musteloI typically use emacs with dvorak as the input mode. does anyone know a way of combining this with agda-mode to get dvorak-like bindings?15/07 22:28
copumpkinassociate _^_ leftA test ≡ (((1 ^ 2) ^ 3) ^ 4) ^ 515/07 23:29
copumpkinassociate _^_ rightA test ≡ 1 ^ (2 ^ (3 ^ (4 ^ 5)))15/07 23:29
copumpkinwoot15/07 23:29
copumpkintest₀ : permute reverseP test ≡ 5 ∷ 4 ∷ 3 ∷ 2 ∷ 1 ∷ []15/07 23:30
--- Day changed Sat Jul 16 2011
copumpkinthis proof is tricky16/07 03:12
copumpkinanyone doing anything interesting in agda right now?16/07 03:16
augurcopumpkin: right this moment? no16/07 03:25
copumpkinyeah, this second16/07 03:26
augurx316/07 03:26
augurjust the same stuff as always16/07 03:26
augurbut its on pause16/07 03:26
copumpkinah :o16/07 03:27
augurbut when its not on pause, ill be asking whats the whats16/07 03:28
copumpkinomg it's a glguy16/07 03:32
glguyHello :)16/07 03:32
copumpkinin the mood for some agda!16/07 03:32
glguyCould someone help me think about how take two decidable predicates P and Q on Lists of A and make a decidable predicate which for a given "xs : List A" says exists a b. a ++ b === xs /\ P a /\ Q b16/07 03:33
glguyI am16/07 03:33
glguyI'm stuck trying to figure out how to formulate this16/07 03:34
glguyI know how to provide the case where there is in fact an a and b which satisfy P and Q16/07 03:34
glguybut I can't figure out how to prove when there isn't16/07 03:34
glguyI'm using "decidable predicate" as in:    forall x. P x \/ (P x -> _|_)16/07 03:35
copumpkinhmm16/07 03:39
copumpkinseems pretty convoluted :)16/07 03:44
glguy"Is there a way to split the last in half so that the left side satisfies one predicate and right another"16/07 03:45
copumpkinyeah16/07 03:45
glguyit's not *that* convoluted :-p16/07 03:45
glguycomes up all the time!16/07 03:45
copumpkinI mean that it seems convoluted to implement :P16/07 03:45
glguyspeaking of convoluted, have you played/seen the game SpaceChem?16/07 03:49
copumpkinnope16/07 03:49
copumpkin?16/07 03:49
glguyIt's a 2D programming puzzle game, in my view16/07 03:50
glguyThere is a free demo on Steam if you are interested, and lots of videos16/07 03:50
copumpkinah, I'll try it out after I tinker with your problem a bit more :)16/07 03:51
glguyLet me know if you come up with a plausible approach16/07 03:52
copumpkinit's going to be ugly16/07 03:52
copumpkinthat's how I roll16/07 03:52
copumpkin(if I come up with anything at all)16/07 03:52
copumpkinman, this is hard16/07 04:14
glguyI'm glad that I'm not the only one to find that so far16/07 04:33
copumpkinoh, I think I know what I'm missing16/07 04:37
copumpkinoh, maybe not16/07 04:38
copumpkinI feel like I need a property on the predicates on the lists16/07 04:40
copumpkinbut it also feels like I shouldn't need it16/07 04:41
glguyI think that the trick is to show that you've completely enumerated the values of:   exists a b. a ++ b === xs16/07 04:42
copumpkinman16/07 04:58
xplatso it's basically enumerating the partitions and proving you got all of them16/07 05:10
xplatit should be in the library!  but that doesn't mean it is16/07 05:10
copumpkinthe splitAt function in Vec is more useful than the one in List16/07 05:13
copumpkinoddly enough16/07 05:13
xplatmaybe it would be easiest to prove a partition is determined by the tail, and then prove all the tails are in your enumeration16/07 05:13
xplatalthough maybe that wouldn't be easier if you used splitAt16/07 05:14
russrusshey so I'm not used to emacs and I'm getting a bit confused with the agda interactive mode - in particular, what is the "case split" supposed to do?16/07 05:19
copumpkinit pattern matches for you16/07 05:19
copumpkinyou tell it a variable to split16/07 05:20
xplatit constructs pattern matches for you16/07 05:20
russrusswhat are the interactive commands that you find most useful?16/07 05:20
xplatif you have "foo bar baz = ?" and you do C-c baz and baz is a Nat, you get 'foo bar zero = ?' and 'foo bar (suc y) = ?'16/07 05:21
xplater, C-c C-c baz RET16/07 05:21
russrussoh aha, that's super useful huh16/07 05:21
copumpkinI use C-r all the time16/07 05:22
copumpkinand C-a16/07 05:22
copumpkin(C-c C-r)16/07 05:22
copumpkin(C-c C-a)16/07 05:22
glguyI use lots of C-c C-, and C-c C-.16/07 05:22
copumpkinoh yeah, definitely C-c C-,16/07 05:22
xplatof the ones that edit, i use r most and c probably second, followed by a16/07 05:22
copumpkinI occasionally use C-n or C-d16/07 05:23
xplata would probably be more often than c if i counted the times it doesn't work16/07 05:23
xplatfor information, i use , a lot and . pretty often16/07 05:23
copumpkinI don't use .16/07 05:24
copumpkinwhat's that?16/07 05:24
xplatlike , but also tells you the type of what you put in the hole16/07 05:24
copumpkinoh16/07 05:24
copumpkinrussruss: note that C-c C-r has two uses16/07 05:25
copumpkinone if you type something into the box and one if you don't16/07 05:25
russrusswhat's the difference?16/07 05:25
copumpkinif it's empty and only one thing "fits"16/07 05:25
copumpkina constructor, or a lambda or something16/07 05:25
copumpkinit'll write that for you and put more holes where necessary16/07 05:26
copumpkinif there isn't a single choice, typing a partial expression (possibly with ?s) in it16/07 05:26
copumpkinwill fill in the remaining holes16/07 05:26
russrusshrm yeah I just tried that on something it new was a non-empty vector and it did ? :: ?16/07 05:26
copumpkinyep16/07 05:26
russrussso now I want to go back to one hole16/07 05:26
russrusswhat's the fastest way to do that?16/07 05:26
copumpkinundo :P16/07 05:27
copumpkinand reload16/07 05:27
copumpkin:(16/07 05:27
russrusshehe that could be streamlined I imagine16/07 05:27
xplatunfortunately the undo support is currently ... not all that16/07 05:27
russrussin general I'm really impressed with these interactive tools though16/07 05:27
copumpkinyeah, I wish I had similar ones in haskell16/07 05:27
xplatthey wouldn't be quite as useful since haskell has too many inhabitants for some of its types16/07 05:28
xplatbut still, they'd be useful enough to carry their weight.  if they were already written :)16/07 05:29
copumpkinxplat: I just want holes and context printing :)16/07 05:29
copumpkinand goal printing16/07 05:29
xplatget dankna to do it, he's writing a tree-based editor for haskell16/07 05:29
copumpkinmmm16/07 05:29
copumpkinI'll bug him at hac phi16/07 05:30
copumpkinjust like I'll bug you16/07 05:30
glguyYou can hack that with data Goal = Goal and the putting Goal where you want it to print the goal as a type error :)16/07 05:30
copumpkinI currently use implicit params16/07 05:30
copumpkinto avoid that16/07 05:30
glguyI do that in GHCi, but for some reason I haven't been doing it in my files...16/07 05:30
glguygood idea16/07 05:30
russrusshrm okay, so another interactive mode question - I'm on the right hand side and I'm in a lambda that I realize I want to "case split" - do I just have to kill my hole somehow and add a where clause?  what's the proper thing to do in this situation?16/07 05:40
_Ray_Hi :) What would you recommend for someone interested in Agda (in general, in these sort of proof theory - functional programming hybrids), but isn't comfortable enough with Emacs?16/07 06:00
copumpkinuse emacs16/07 06:00
copumpkinI'd never used it before agda16/07 06:00
copumpkinit really isn't that hard :P16/07 06:00
russrussthere's lots of GUI versions of emacs that are less intimidating16/07 06:05
copumpkinfunctions in indices are a real pain16/07 06:23
* _Ray_ is failing at making Aquamacs Emacs work with Agda xP16/07 06:34
Saizanthat proof about partitions from 6 hours ago should be a matter of induction over xs while growing P on recursive calls, though there's a lot of case splitting16/07 09:39
mustelogiven a sublist type and a complement function, I'm trying to prove that complement . complement == id, is there any way to make this proof shorter? http://hpaste.org/4910716/07 10:45
mustelospecifically, those with statements seem unnecessary, but I can't seem to get rid of them16/07 10:46
mustelohmm, scratch that16/07 10:51
Saizanhttp://hpaste.org/49113 <- i hope there's a way to refactor all that pattern matching16/07 18:53
copumpkinthat's nice :)16/07 18:54
copumpkinI was using a datatype with index refinement for the split16/07 18:54
copumpkinwas getting to be a pain16/07 18:54
Saizanyeah, someone has to figure out a decent way to handle functions in indices, in GHC it's a little better since it just pushes a type equality into the context16/07 18:57
Saizanthough they don't exactly explain how smart ghc is in making use of those16/07 18:58
copumpkinnow someone just needs to fetch glguy to show him your short solution!16/07 19:01
copumpkinpigworker: by the way, you around?16/07 22:09
pigworkercopumpkin: I have plenty of distractions but am near a computer.16/07 23:24
glguycopumpkin: any luck with the split list predicate problem?16/07 23:40
copumpkinnot me! but Saizan solved it16/07 23:40
copumpkinin a reasonably small amount of code16/07 23:41
glguyfantastic!16/07 23:41
copumpkinhttp://hpaste.org/4911316/07 23:41
copumpkinsmall compared to what I was expecting to see for it16/07 23:41
Saizanquite a bit of repetition though16/07 23:41
copumpkinI went down the wrong path by refining an index with a function16/07 23:41
copumpkinand then gave up in frustration when trying to pattern match on it :(16/07 23:41
* copumpkin weeps16/07 23:41
glguyIt looks like he solved having the index be computed by a function by moving that equality into the record as a field16/07 23:42
glguyI like that16/07 23:42
copumpkinyeah16/07 23:43
copumpkinthey're equivalent, but one is a lot easier to work with :/16/07 23:43
copumpkinI still kind of prefer the other conceptually16/07 23:43
copumpkinbut it's close to impossible to do anything with :(16/07 23:43
copumpkinI've been fighting with it in this other project I'm working on16/07 23:43
Saizanyep, the other interesting part of the proof is how P becomes (\xs -> P (x :: xs)) in the recursive calls16/07 23:44
glguyYeah, Iavor suggested that the night I was having this problem16/07 23:44
glguyThe Predicate transformation16/07 23:44
glguybut I was too busy playing spacechem to get back to that16/07 23:44
copumpkinlol16/07 23:44
glguyYou had me confused at first with decQ as a module param and decP as a function parameter16/07 23:47
glguyI was thinking "How did he get around Q being decidable??"16/07 23:47
copumpkinwe should start writing undecidability proofs ;)16/07 23:47
Saizanheh, yeah, i've not exactly edited it for clarity :)16/07 23:48
glguyThanks for solving this problem and bringing a new technique to my attention16/07 23:49
Saizannp16/07 23:50
--- Day changed Sun Jul 17 2011
xplathm, interesting17/07 00:47
xplati think i'm finding functions with lots of withs to not be that readable though :(17/07 00:48
glguyhttp://www.galois.com/~emertens/DecSplits/DecSplits.html17/07 00:48
copumpkinxplat: yeah, I agree17/07 00:48
xplatmaybe it would be a little better if things auto-aligned17/07 00:48
glguySaizan , copumpkin : I worked back through it starting from Saizan's type signature to better understand what's going on17/07 00:48
copumpkinthat's very clean-looking :)17/07 00:48
xplatiwbni you could say (decP . (x ::)) instead of that lambda17/07 00:50
glguywell:  (_::_ x)17/07 00:51
copumpkinlet's hack up the parser to accept sections ;)17/07 00:51
xplatah, but that takes away all the extra readability17/07 00:51
glguyOH17/07 00:51
glguyit would be nice if17/07 00:51
* glguy doesn't have "iwbni" programmed in17/07 00:51
copumpkin:)17/07 00:51
copumpkinxplat: you had a chance to do the resume btw?17/07 00:56
xplatboth of the 'and we are not at the end of the list' predicates seem basically identical except for the choice of helper17/07 00:56
glguy  smash : ∀ {P Q : List A -> Set} {x xs} → Split (λ ys → P (x ∷ ys)) Q xs → Split P Q (x ∷ xs)17/07 00:57
glguy  smash {P}{Q}{x}(split a++b≡xs Px∷a Qb) = split (cong (_∷_ x) a++b≡xs) Px∷a Qb17/07 00:57
glguyIdeas for a better name?17/07 00:57
xplatcopumpkin: things have been a little crazy here.  but i can almost certainly get it to you this week17/07 00:58
copumpkin:D17/07 00:59
copumpkinthanks!17/07 00:59
copumpkinglguy: hmm17/07 00:59
copumpkinsplit-cong? :P17/07 00:59
copumpkinI'm terrible at naming17/07 00:59
xplatcopumpkin: wouldn't normally be a problem, but the things you're looking for are different enough from the other places i usually apply that i have to basically rewrite it17/07 00:59
copumpkinwrangle17/07 00:59
copumpkinxplat: yeah, makes sense17/07 01:00
copumpkinsquibble is another candidate17/07 01:00
copumpkinfor a name for that17/07 01:00
* copumpkin runs away17/07 01:01
xplatglguy: i'd call it extend-split17/07 01:01
xplator maybe left-extend17/07 01:02
glguycons-split?17/07 01:02
xplatthat could be good17/07 01:03
glguyI can't be the only one that finds naming things in Agda to be impossible :)17/07 01:03
copumpkinyeah17/07 01:03
copumpkinI often name things after their types17/07 01:03
copumpkindefinitely not ideal17/07 01:04
xplatit gives you so much freedom to pick good names, but then squanders it all by making you name umpteen million more things17/07 01:04
copumpkinlemma<n> is another option :P17/07 01:04
copumpkinthe one I usually use17/07 01:04
glguyI had so many lemma<n>'s in the Ring properties for Integer I sent in17/07 01:04
glguyI must have had 2017/07 01:04
copumpkin:P17/07 01:05
xplati use that whenever i'm doing a bunch of lemmas that form a clear sequence and that i won't use elsewhere17/07 01:05
glguypart of the reason it wasn't adopted, I suspect17/07 01:05
xplatnumbered lemmas are an old tradition in math for things like that17/07 01:05
copumpkinmodule BagO'Lemmata17/07 01:05
xplatbut it has its downsides, what with all the 'Spoonthumper's Lemma' names we're now stuck with for what turned out to be important theorems in their own right17/07 01:06
xplat(or indeed axioms, like Zorn's Lemma)17/07 01:06
copumpkinwhat was Yoneda trying to prove with his lemma?17/07 01:07
xplatmaybe ask ##categorytheory :)17/07 01:10
xplatassuming there's even anyone there who's not here ...17/07 01:10
copumpkinddarius at least17/07 01:10
xplatwell, that's enough to make it worthwhile17/07 01:11
djahandarieFor some reason edwardk hasn't joined it yet17/07 01:12
copumpkinhe's too busy with mad algebra right now17/07 01:14
djahandarieMy biggest problem with learning all that algebra stuff is that everything has the strangest names that are just really hard to remember17/07 01:15
copumpkinI want a dependent extensible record system dammit17/07 01:15
copumpkinno more fucking names, just collections of properties17/07 01:16
copumpkinmaybe I should pull out my attempt at that in agda again17/07 01:16
copumpkinbut it was so tedious to do anything with17/07 01:16
xplatit seems like the more i use agda, the more i love epigram2, but the more i read about the progress of epigram2, the more i love agda17/07 01:18
copumpkinyou don't like where epigram2 is going?17/07 01:18
xplatoh, not the direction, the speed17/07 01:18
copumpkinah :)17/07 01:18
xplati'm not totally sold on a parser anymore as a component of a language, but it sure still beats a second language for building syntax trees of the first language17/07 01:20
xplat(for a sufficiently general sense of 'syntax tree')17/07 01:20
copumpkinnot sure what you mean?17/07 01:20
xplatwell, right now the only way to do anything with epigram2 is to use a command line interface to construct terms17/07 01:21
copumpkinoh, I see17/07 01:22
copumpkincochon!17/07 01:22
* copumpkin oink17/07 01:22
xplatone thing i'm thinking of working on at hacphi, now that i've found that diagrams is almost the only thing on the project page, is porting that TeX commutative-diagram library as a frontend for it17/07 01:24
djahandarieI think we should all just hack on category theory when we're there17/07 01:24
copumpkinlol17/07 01:24
djahandarieEspecially now that I can directly bug xplat17/07 01:24
copumpkinI've already started hacking up the agda parser and highlighting code17/07 01:25
copumpkinso I can finally start writing highlighted html agda articles17/07 01:25
copumpkinand spread the agda enthusiasm wider17/07 01:25
copumpkinamong the hordes of iphone wannabe hackers17/07 01:25
copumpkin>_>17/07 01:25
xplatand then we could come up with something to automatically render our equational reasoning proofs on arrows as diagrams17/07 01:25
copumpkinooh17/07 01:25
djahandarieheh17/07 01:25
glguyhttp://www.galois.com/~emertens/DecSplits/RegExp.html17/07 01:27
glguythis is what I was working towards with the split lists stuff17/07 01:27
copumpkinaha17/07 01:27
copumpkinhis true intentions are revealed!17/07 01:27
glguyhttp://code.haskell.org/Agda/examples/AIM6/RegExp/talk/RegExps.agda17/07 01:28
glguyinspired by that17/07 01:28
copumpkinI started working on something like that17/07 01:28
copumpkinbut from a generative perspective17/07 01:28
xplatsince the uses of associative and identity laws for arrows would be invisible it would really cut through the crap in the longer proofs17/07 01:28
glguybut it had a bad type:   _∈‿⟦_⟧¿ : (xs : [ carrier ]) -> (re : RegExp) -> Maybe (xs ∈‿⟦ re ⟧)17/07 01:28
copumpkinas in, a regex generates a Colist of all strings in it17/07 01:28
xplatglguy: oh, so you couldn't prove that every possible match was caught17/07 01:30
glguyyeah17/07 01:30
glguyi still need to do the star case17/07 01:30
xplati'm sure you can handle it kleenely17/07 01:31
* copumpkin punches xplat 17/07 01:32
copumpkinman, I have violence issues17/07 01:32
glguyo.O17/07 01:33
xplatnah, i totally deserved that :)17/07 01:34
copumpkinthis associativity proof is annoying as hell17/07 01:43
copumpkinI should revisit my foundations17/07 01:43
bxchmmm getting this on agda 2.2.10 that i just upgraded and stdlib 0.517/07 22:21
bxc/Users/benc/src/roman-numeral-type/lib/src/Level.agda:27,1-3217/07 22:21
bxcLevel is not an inductive data type17/07 22:21
bxcwhen checking the pragma BUILTIN LEVEL Level17/07 22:21
bxcany clues?17/07 22:22
* bxc tries old definition of LEVEL as a data type rather than postulates17/07 22:34
bxcit compiles at least17/07 22:34
copumpkinbxc: if you use the latest stdlib, you need to use the latest agda17/07 22:35
copumpkinthey made levels postulated to avoid people pattern matching on them17/07 22:35
bxci was under the impression that 0.5 went with 2.2.1017/07 22:35
copumpkinno17/07 22:35
copumpkinor maybe17/07 22:35
copumpkinbut I don't think so17/07 22:35
bxcVersion 0.5. README. Tested with Agda 22:35
copumpkinbecause pattern matching on levels feels horribly unparametric, even though I don't think anyone has found specific issues with it beyond that17/07 22:35
copumpkinI dunno then17/07 22:35
bxci just upgraded my agda install - maybe theres some cruft from before17/07 22:36
bxccopumpkin: so its OK to change what I did back as long as I promise to not pattern match on level? ;)17/07 22:36
copumpkinnot sure if anything else breaks :)17/07 22:36
copumpkinbut yeah, I think the main goal of the change was to stop you from pattern matching on level17/07 22:37
xplati think 0.5 is the one i use with .1017/07 22:38
xplatare you sure the one you got is 0.5?17/07 22:38
bxci darcs getted it17/07 22:39
bxcmaybe i screwed that up17/07 22:39
* bxc tries that again17/07 22:39
copumpkindarcs get will get you the latest version won't it?17/07 22:39
bxc$ darcs get --tag=0.5 --lazy http://www.cse.chalmers.se/~nad/repos/lib/17/07 22:40
copumpkinor can you tell it a specific point to get at?17/07 22:40
copumpkinoh17/07 22:40
xplatpattern matching on level is the same as saying levels have an extensional equality (with K)?17/07 22:40
bxcyeah it builds this time17/07 22:40
bxcok17/07 22:40
bxcso my attempt at repositioning my darcs was b0rk17/07 22:40
bxci got the latest originally and tried ot switch it back to 0.517/07 22:40
bxcwhich apparently didn't work so well17/07 22:40
bxc0.5 has level as a datatype17/07 22:41
bxcnot as postulates17/07 22:41
xplatit does feel more than a little nonparametric to have functions that switch by level like they were actually stratified by natural number, but i'm not sure it's *wrong* per se17/07 22:43
copumpkinyeah17/07 22:43
xplatbut i wouldn't be surprised if it makes Setw contain more objects than it might otherwise17/07 22:43
xplatand that would mean it was logically stronger than just assuming Setw exists17/07 22:44
copumpkinI'm going to write a function that if given a List of things, reverses it17/07 22:44
copumpkinexcept if those things are at level 717/07 22:44
copumpkinthen it'll just switch all adjacent pairs of elements17/07 22:45
copumpkincause that's how I roll17/07 22:45
xplati wonder if agda is just noncumulative or anticumulative17/07 22:46
xplatas presently constituted17/07 22:46
--- Day changed Mon Jul 18 2011
copumpkinit'd be nice if the non-canonical implicits could look up simple constructors18/07 00:42
copumpkinsomething like18/07 00:42
copumpkindata IsCompatible : SomeFiniteType -> SomeFiniteType -> Set where18/07 00:42
copumpkinCowWithPig : IsCompatible Cow Pig18/07 00:43
copumpkinPigWithCow : IsCompatible Pig Cow18/07 00:43
copumpkinCowWithCow : IsCompatible Cow Cow18/07 00:43
copumpkinthen18/07 00:43
copumpkinf : SomeFinite18/07 00:43
copumpkinf : (x y : SomeFiniteType) -> {{IsCompatible x y}} -> ...18/07 00:43
copumpkinalthough I guess I could approach that differently18/07 00:44
copumpkinIsCompatible : SomeFiniteType -> SomeFiniteType -> Set18/07 00:44
xplatthat does go against an explicit design criterion of {{}}18/07 00:44
copumpkinIsCompatible Cow Pig = \top18/07 00:44
copumpkinIsCompatible Pig Cow = \top18/07 00:44
copumpkinIsCompatible Cow Cow = \top18/07 00:44
copumpkinIsCompatible _ _ = \bot18/07 00:45
xplatalthough i haven't read how (or if!) the authors justified that criterion18/07 00:45
copumpkinthat seems like it'd work, right?18/07 00:45
copumpkineven without non-canonical implicits18/07 00:45
xplatcopumpkin: yeah, that's just a folded-in T18/07 00:45
copumpkinstill, it feels a little primitive that one works and not the other18/07 00:46
xplatthey're different too; one is scope-dependent, one is not18/07 00:47
copumpkinscope-dependent?18/07 00:48
copumpkinoh18/07 00:48
Eduard_Munteanucopumpkin: are you trying to get MPTCs using non-canonicals?18/07 01:24
* Eduard_Munteanu hasn't looked into that18/07 01:24
stepkutI want to use ⊆ from the Membership module in Data.List.Any. but there is also a Data.List.Any.Membership file.. so doing open import Data.List.Any.Membership is ambiguous18/07 01:24
Eduard_MunteanuI'm not sure how one would go about doing stuff we normally do with fundeps.18/07 01:25
Eduard_Munteanustepkut: what about just    open Membership   ?18/07 01:27
copumpkinEduard_Munteanu: not really18/07 01:27
copumpkinEduard_Munteanu: just automatic relations of that sort18/07 01:27
copumpkinstepkut: let me check18/07 01:27
copumpkinstepkut: the .Membership module looks like properties and proofs about list membership18/07 01:28
Eduard_MunteanuIf you open-import Data.List.Any, then any modules inside would be in scope (not explicitly opened though)18/07 01:28
stepkutEduard_Munteanu: a. I tried open import Membership. Just open Membership works. Thanks18/07 01:29
copumpkinoh I see18/07 01:29
Eduard_MunteanuBTW, Membership here expects a parameter too18/07 01:29
Eduard_Munteanumodule Membership {c ℓ : Level} (S : Setoid c ℓ) where18/07 01:30
copumpkinwell, if you don't provide it one18/07 01:30
copumpkinyou just need to give the individual functions that parameter18/07 01:30
stepkutso I probably want, Membership-≡ instead18/07 01:31
copumpkinprobably18/07 01:31
glguyAm I correct that records are never indexed types?18/07 01:33
glguydata Name parameters : indexes -> setN where (assuming that these are the indexes)18/07 01:33
copumpkinyeah18/07 01:33
copumpkinyou couldn't have eta if you allowed index refinement18/07 01:33
glguyI rarely define my own records so I hadn't noticed that18/07 01:34
copumpkinthere's also no syntax that would let you actually refine the indices18/07 01:34
copumpkineven if you could write record Moo : ... -> Set18/07 01:34
Eduard_MunteanuYou mean fields wouldn't be able to specify the index?18/07 01:41
copumpkin?18/07 01:42
Eduard_Munteanulike when data constructors set the index, because the last thing to the right of -> must be something of your actual type.18/07 01:43
Eduard_Munteanu(Where did I leave my terminology? :D)18/07 01:44
copumpkinan index is just an extra field (sometimes) with implicit equality18/07 01:44
copumpkinor a refined index18/07 01:44
Eduard_Munteanu03:33 < copumpkin> you couldn't have eta if you allowed index refinement18/07 01:45
Eduard_MunteanuWhat do you mean by 'eta' there?18/07 01:45
copumpkinthe fact that I can prove stuff like18/07 01:45
copumpkin: (x : \top) -> x == tt18/07 01:45
copumpkinwith proof x = refl18/07 01:46
copumpkinnot proof tt = refl18/07 01:46
Eduard_MunteanuOh, hm.18/07 01:46
copumpkinwith a record18/07 01:46
stepkuthmm. I want to construct this proof: lem : 'c' ∈ ('c' ∷ 'd' ∷ [])18/07 01:46
copumpkinit knows for sure that the type is inhabited, and inhabited by exactly one constructor18/07 01:46
stepkutbut I am not sure what should go in the body :-/18/07 01:46
copumpkinstepkut: probably just here18/07 01:47
copumpkinif you do C-c C-a it'll probably figure it out and put "here" into the body18/07 01:47
stepkuthere gives me some big long error18/07 01:48
copumpkinhmm18/07 01:48
copumpkinoh18/07 01:48
copumpkinhere refl18/07 01:48
copumpkin(I'd guess)18/07 01:48
Eduard_Munteanu here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)18/07 01:48
Eduard_MunteanuYou could try    here ?   first, then try to fill up that hole18/07 01:49
copumpkinhere refl should work though18/07 01:50
copumpkincause I think \in is just an Any with equality18/07 01:50
stepkutthat worked18/07 01:51
Eduard_MunteanuYeah, with Membership-≡ it should be \==18/07 01:51
copumpkinstepkut: whatcha making? :)18/07 01:51
stepkutcopumpkin: attempting to construct this: lem : (purse : List Item) -> (keys ∷ wallet ∷ phone ∷ []) ⊆ purse18/07 01:53
copumpkinaha :)18/07 01:53
stepkutnot going so well though :p18/07 01:55
stepkutnot sure that type even makes sense18/07 01:55
copumpkinnot really :)18/07 01:56
stepkuti think I need to provide proofs that those items are in the purse before I can provide the result18/07 01:57
copumpkinbut those proofs would essentially be the proof you're seeking18/07 01:57
stepkutlike, lem : (purse : List Item) -> keys ∈ purse -> wallet ∈ purse -> phone ∈ purse -> (keys ∷ wallet ∷ phone ∷ []) ⊆ purse)18/07 02:00
copumpkinoh fair enough18/07 02:00
copumpkinbut the lem would then just be sticking those three proofs up into a "list"18/07 02:00
stepkutyeah..18/07 02:00
stepkutnot really what I was hoping for :)18/07 02:00
copumpkinsince All is basically a list18/07 02:00
copumpkinwhat's the bigger thing you're trying to prove? maybe there's something better you can do if you take a step back?18/07 02:01
copumpkinI find it kind of interesting how List, Vec, and All are very similar structures, and so are Nat, Fin, and Any18/07 02:01
stepkutso, in my Haskell version, I used a hetregeneous list, and then I could do, lem :: (IsElem Keys purse, IsElem Phone purse, IsElem Wallet purse) => purse -> ()18/07 02:02
stepkutlem (Keys --> Wallet --> Purse --> emptyPurse)18/07 02:02
stepkuttrying to figure out how to translate that in Agda basically18/07 02:03
stepkutbasically, I want to have a list of items, and have some assertion in the code that makes sure some essential items are in that list18/07 02:04
stepkutbut, a 'compile time' assertion18/07 02:04
stepkutin Haskell that requires the use of a heterogenous list.. not sure if the same is true in Agda18/07 02:05
stepkutin the agda tutorial I did, there is a proof that, filter p xs ⊆ xs18/07 02:07
stepkutbut, I am starting to see how, (xs : List Item) -> (keys ∷ wallet ∷ phone ∷ []) ⊆ xs, is not quite the same18/07 02:08
Eduard_MunteanuI don't think that theorem is true, like you hinted above.18/07 02:09
stepkutyeah18/07 02:10
Eduard_Munteanu(e.g. not all 'List Item's you can think of are like that)18/07 02:10
stepkutright18/07 02:10
stepkutthis is fine:18/07 02:10
stepkutlem : keys ∈ (keys ∷ [])18/07 02:10
copumpkin(IsElem Keys purse, IsElem Phone purse, IsElem Wallet purse) => is basically (keys ∷ wallet ∷ phone ∷ []) ⊆ purse) ->18/07 02:10
copumpkinno need for a heterogeneous list18/07 02:10
copumpkinunless your keys, phone, and wallet are actually different types18/07 02:10
stepkutcopumpkin: there were different types in Haskell, because that was the only way to construct the proof at compile time. I don't require that they be different in Agda18/07 02:11
copumpkinthen you pretty much have the same thing18/07 02:11
stepkuthmm18/07 02:13
copumpkin(IsElem Keys purse, IsElem Phone purse, IsElem Wallet purse) => purse -> ()18/07 02:13
stepkutright18/07 02:14
Eduard_Munteanuor    lem : (keys ∷ wallet ∷ phone ∷ []) ⊆ xs18/07 02:14
Eduard_MunteanuAssuming those are somewhere in scope.18/07 02:15
stepkutEduard_Munteanu: assuming xs is in scope?18/07 02:15
Eduard_MunteanuYeah.18/07 02:15
stepkutok18/07 02:15
stepkutso this works:18/07 02:16
stepkutpurse : List Item18/07 02:16
stepkutpurse = keys ∷ wallet ∷ phone ∷ []18/07 02:16
stepkut 18/07 02:16
stepkutcan-leave : keys ∈ purse18/07 02:16
stepkutcan-leave = here refl18/07 02:16
stepkutbut, I wanted to make can-leave take the purse as an argument18/07 02:16
stepkutlike, can-leave-1 = can-leave purse18/07 02:17
Eduard_Munteanustepkut: well, that would mean any possible purse would contain 'keys' no?18/07 02:17
Eduard_MunteanuYou could work one step above.18/07 02:17
Eduard_Munteanucan-leave-1 : can-leave purse18/07 02:18
Eduard_MunteanuSince types are theorems, and that's what you want, a parametrized theorem.18/07 02:18
Eduard_MunteanuCan you figure out the type of can-leave then?18/07 02:19
stepkutlet me see18/07 02:19
Eduard_MunteanuHowever, you'd still have to at least write something like can-leave-1 = _ for the proof18/07 02:20
copumpkinwell18/07 02:21
copumpkinyou can convince agda to find the proof for you18/07 02:21
stepkutmy initial guess would be: can-leave : (purse : List Item) -> keys ∈ purse18/07 02:21
copumpkinbut it's kind of a hack18/07 02:21
Eduard_Munteanustepkut: well, what's the type of   keys ∈ purse?18/07 02:21
copumpkinstepkut: that's saying for all purses, keys are in the purse18/07 02:21
copumpkinstepkut: you probably want18/07 02:21
copumpkincan-leave : (purse : List Item) -> Set18/07 02:22
Eduard_Munteanus/type/sort/18/07 02:22
Eduard_MunteanuYeah.18/07 02:22
copumpkincan-leave purse = keys ∈ purse18/07 02:22
copumpkinnow can-leave is itself a predicate on lists18/07 02:22
copumpkinand you can only construct a can-leave on a list if you can provide a proof that keys are in the purse18/07 02:22
copumpkinstepkut: you going to hac phi btw?18/07 02:23
stepkutcopumpkin: wasn't planning on it18/07 02:23
copumpkinah18/07 02:23
stepkuthmm18/07 02:30
copumpkinmake sense?18/07 02:32
stepkutapparently not18/07 02:32
stepkutlem = can-leave (wallet ∷ phone ∷ [])18/07 02:32
stepkutI am not really sure what I am supposed to do with can-leave I guess18/07 02:33
stepkutthere lem will have the type, lem : Set18/07 02:33
stepkutI want to use can-leave in the type?18/07 02:34
stepkutcan-leave-1 : can-leave purse-118/07 02:34
copumpkinwell, you'd use it in any function that needs to ensure that keys are in the purse18/07 02:34
copumpkinsomefunction : (purse : List Item) -> can-leave purse -> more stuff here18/07 02:34
copumpkinkeep in mind that there's a distinction between a predicate and a decidable one18/07 02:35
copumpkinat runtime, if you have a list, you want to actually provide a decision (yes or no) about whether the purse contains keys18/07 02:35
copumpkinthe purse may be provided from user input or something18/07 02:35
stepkutin this case I am looking for something like a compile time unit test18/07 02:37
stepkutlike, in the haskell version I could do:18/07 02:37
stepkutcan_leave_purse1 :: () ; can_leave_purse1 = leave_home purse118/07 02:38
copumpkinah yes18/07 02:38
stepkutand if I accidently screw up the list so that the keys are missing I will get a compile time error18/07 02:38
copumpkinyou can sort of do that in agda too, but it's a bit of a pain18/07 02:38
copumpkingotta go fetch laundry, but I'll be back in a couple of minutes18/07 02:39
stepkutk18/07 02:39
stepkuthere is the haskell version btw, http://hpaste.org/4914318/07 02:39
glguycopumpkin: i made the refactoring you suggested yesterday and i think things end up pretty clear now (i got stuck on another problem and decided to do some refactoring in the meantime) http://www.galois.com/~emertens/DecSplits/DecSplits.html#120418/07 02:40
Eduard_Munteanustepkut: well my suggestion was to write stuff like    lem : can-leave (wallet ∷ phone ∷ [])18/07 02:43
Eduard_Munteanucan-leave takes a parameter and gives you back a theorem, i.e. a type18/07 02:43
Eduard_MunteanuOf course, you still have to write   lem = ...18/07 02:44
Eduard_Munteanu(that is, a proof for that)18/07 02:45
stepkutEduard_Munteanu: yeah, I think that is closer to what I want18/07 02:47
stepkutI have this now:18/07 02:48
stepkuthttp://hpaste.org/4915318/07 02:48
stepkutbut that does not work if the keys are not the first thing in the list18/07 02:48
copumpkingah18/07 02:48
copumpkinmy mining rig or the AC is killing the circuit breaker in my living room18/07 02:48
copumpkinwhat'd I miss?18/07 02:49
stepkutcopumpkin: http://hpaste.org/4915318/07 02:49
copumpkinstepkut: did someone tell you how to convince agda to provide the proof for you?18/07 02:49
stepkutcopumpkin: C-c C-a or something?18/07 02:49
copumpkinoh I mean in code18/07 02:49
copumpkinlike, when you call it, it finds the proof for you18/07 02:50
stepkuti don't think so..18/07 02:50
copumpkinokay18/07 02:50
stepkut_ ?18/07 02:50
copumpkinjust a sec18/07 02:50
Eduard_Munteanucopumpkin: heh18/07 02:50
Eduard_Munteanustepkut: you could start by doing   can-leave-1 = ?   to open up a hole18/07 02:52
stepkutok18/07 02:53
Eduard_Munteanuthen write    here there    inside and do C-c C-a18/07 02:53
Eduard_Munteanu'here' and 'there' would be hints for the automatic prover18/07 02:53
stepkutso, the proofs that generates is depend on the order of the elements in the purse18/07 02:55
Eduard_MunteanuYeah.18/07 02:55
stepkutfor, keys ∷ wallet ∷ phone ∷ [], it will be, here refl18/07 02:55
stepkutand for, wallet ∷ keys ∷ phone ∷ [], it will be, there (here refl)18/07 02:55
stepkutI guess that is the nature of the proof though..18/07 02:56
Eduard_MunteanuOne thing which might work is having your lemma as an implicit in a type.18/07 02:56
stepkutto prove that keys is in the list, wallet ∷ keys ∷ phone ∷ [], you show that it is the second element of that list18/07 02:57
stepkutwhich lemma ?18/07 02:57
Eduard_Munteanulike    something : {_ : can-leave (wallet ∷ phone ∷ [])} -> ...18/07 02:58
Eduard_MunteanuI'm not sure if that'd work here though.18/07 02:58
copumpkinstepkut: http://hpaste.org/4915518/07 02:58
copumpkinkind of convoluted18/07 02:58
copumpkinand a bit of a hack18/07 02:59
copumpkinbut it has the same effect as the haskell compiler trying to find the proof for you by resolving instances18/07 02:59
copumpkinthe difference18/07 02:59
copumpkinis that if you made a purse-2 : List Item18/07 02:59
copumpkinand left the keys out of it18/07 02:59
copumpkinyou wouldn't get an error but the caller would turn yellow18/07 03:00
copumpkinI can explain how it works if you're interested18/07 03:00
stepkutI am interested18/07 03:01
copumpkinone absolutely crazy piece of magic18/07 03:01
copumpkinis the following18/07 03:01
copumpkinif you make18/07 03:01
copumpkinpurse-2 : List Item18/07 03:01
copumpkinpurse-2 = wallet ∷ {!!} ∷ phone ∷ []18/07 03:01
copumpkinand call18/07 03:01
copumpkintest : ⊤18/07 03:01
copumpkintest = some-function purse-218/07 03:01
copumpkinoh actually nevermind18/07 03:02
copumpkinit was pure chance :)18/07 03:02
copumpkinagda-magic--18/07 03:02
stepkut:)18/07 03:02
Eduard_Munteanucopumpkin: you mean Agda would suggest 'keys' in that hole?18/07 03:02
copumpkinit did18/07 03:02
copumpkinbut it was just chance18/07 03:02
copumpkinbrb phone18/07 03:03
Eduard_Munteanu@karma agda-magic18/07 03:03
lambdabotagda-magic has a karma of -118/07 03:03
Eduard_MunteanuAww...18/07 03:03
stepkut√agda-magic18/07 03:04
Eduard_MunteanuNow you're imagining things :P18/07 03:04
stepkut;)18/07 03:04
stepkutI need to find easier problems to solve :-/18/07 03:11
copumpkinsorry, still on phone :)18/07 03:17
copumpkinbut anyway, agda is strongly normalizing18/07 03:18
copumpkinyou know what that means?18/07 03:18
stepkutnot a clue18/07 03:18
copumpkinit basically means every expression reduces to a (single) normal form18/07 03:18
stepkutok18/07 03:18
copumpkinit essentially means you can do fairly complex compile-time computation18/07 03:19
stepkutyeah18/07 03:19
copumpkinso18/07 03:20
copumpkinremember I mentioned decidable predicates?18/07 03:21
stepkutyeah18/07 03:21
copumpkinthat's basically the equivalent of Bool18/07 03:21
stepkutok18/07 03:21
copumpkinexcept it's a fancy Bool that carries what it's saying true or false about18/07 03:21
copumpkinso true carries a proof of something18/07 03:21
copumpkinand false carries a proof of not that somethign18/07 03:21
stepkutyeah, I saw that True and False had arguments18/07 03:21
copumpkinwell18/07 03:21
copumpkinthe actual constructors of Dec18/07 03:21
copumpkinare yes and no18/07 03:21
copumpkinTrue and False take a Dec18/07 03:22
stepkutyeah, I saw that yes and no took arguments as well18/07 03:22
copumpkinand if the Dec is yes, it returns \top18/07 03:22
copumpkin\top is like () in haskell18/07 03:22
stepkutyeah18/07 03:22
copumpkinit has one inhabitant18/07 03:22
copumpkinso if you say something like18/07 03:22
copumpkinf : {x : \top} -> ...18/07 03:22
copumpkinagda can figure out that x must be tt (the constructor of \top)18/07 03:23
copumpkinautomagically18/07 03:23
stepkutah, I wondered what tt was18/07 03:23
copumpkinso tt : \top18/07 03:23
copumpkinand is the only inhabitant18/07 03:23
copumpkinnow18/07 03:23
copumpkinthe any function18/07 03:23
copumpkinit takes a decision procedure on elements of a list18/07 03:24
stepkutyeah18/07 03:24
copumpkinand provides you a decision procedure for Any of the same predicate on the list18/07 03:24
copumpkin:t find18/07 03:24
lambdabotforall a. (a -> Bool) -> [a] -> Maybe a18/07 03:24
copumpkinwell, not quite find, but similar18/07 03:24
copumpkin:t any18/07 03:24
lambdabotforall a. (a -> Bool) -> [a] -> Bool18/07 03:24
stepkutany : ∀ {a p} {A : Set a} {P : A → Set p} → (∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)18/07 03:25
copumpkin(a -> Bool) -> ([a] -> Bool)18/07 03:25
copumpkinif you squint really hard18/07 03:25
copumpkinyou'll see that they're the same in haskell and agda18/07 03:25
stepkutyeah18/07 03:25
augurerp18/07 03:25
augurim getting some sort of weird error18/07 03:25
copumpkinso you have a static list in agda18/07 03:25
copumpkinand you're calling any on it18/07 03:25
copumpkinbecause agda is strongly normalizing, it can fully evaluate any on the static list18/07 03:25
auguri havent used aquamacs in like two weeks but like18/07 03:25
copumpkinall the way down to "yes proof" or "no proof"18/07 03:25
copumpkinthen18/07 03:26
stepkutyeah18/07 03:26
copumpkinTrue can take that yes or no18/07 03:26
copumpkinand return \top or \bot18/07 03:26
copumpkinand finally18/07 03:26
copumpkinif your list contained the element, you'll end up with f : {pf : \top}18/07 03:26
copumpkinand agda will happily provide that for you18/07 03:26
augurits telling me http://hpaste.org/4915718/07 03:26
auguro_O18/07 03:26
copumpkinon the other hand, if it didn't contain the element18/07 03:26
copumpkinyou'll end up with f : {pf : \bot}18/07 03:26
copumpkinand agda says "I dunno what to give you for \bot", and rightfully so18/07 03:26
copumpkinsince there's nothing you could possibly give (assuming agda's not broken) that has that type18/07 03:26
stepkutI can also do, can-leave-3 : can-leave-home′ purse-3; can-leave-3 = tt18/07 03:27
copumpkinbut it can't determine that there isn't a solution, so it just makes it yellow18/07 03:27
copumpkinnote that I got agda to write that _≟_ for me18/07 03:28
copumpkinI wrote x ≟ y = ?18/07 03:28
stepkutah18/07 03:28
stepkutnice18/07 03:28
copumpkinand in the hole, I wrote -c and did C-c C-a18/07 03:28
stepkutthat makes it less painful18/07 03:28
copumpkinit's still pretty bad18/07 03:28
stepkutyeah18/07 03:29
copumpkin-c tells the auto proof searcher18/07 03:29
copumpkinto try pattern matching on arguments to help itself along18/07 03:29
stepkutso, _∈_, uses,   x ∈ xs = Any (_≈_ x) xs18/07 03:29
copumpkinyeah18/07 03:29
copumpkinso that's the predicate form of it18/07 03:29
stepkutis there some way to use ≈ instead of ≟?18/07 03:30
copumpkinwell, we sort of are already18/07 03:30
copumpkin≈ is whatever you opened the module with18/07 03:30
copumpkinand here you opened it with ==18/07 03:30
stepkutyeah18/07 03:30
copumpkin_≟_ is a decision procedure on ==18/07 03:30
copumpkinin case you hadn't noticed, the closest analog to the Eq class in haskell in agda18/07 03:31
copumpkinis DecSetoid18/07 03:31
stepkutthere is no easy way to get from _≡_ to Dec (x ≡ y) ?18/07 03:34
copumpkinnope! that's basically the essence of what it means to be constructive18/07 03:34
stepkutheh18/07 03:35
stepkutthere is a lot I don't know :)18/07 03:35
copumpkinDec P is basically18/07 03:35
copumpkinP or not P18/07 03:35
copumpkinconstructive logic is classical logic minus the law of excluded middle18/07 03:35
copumpkinwhich is P or not P18/07 03:35
augurno? anyone? :(18/07 03:36
copumpkinclassical logic is basically (from a constructivist's lens) saying that all questions are decidable18/07 03:36
copumpkinwhich as computer scientists we generally don't believe18/07 03:36
augur:(18/07 03:38
copumpkinaugur?18/07 03:39
augurhttp://hpaste.org/4915718/07 03:39
copumpkinglguy: that's very clean18/07 03:40
glguyand getting better every moment :)18/07 03:40
copumpkinyou'll have it down to a one-liner in no time18/07 03:40
copumpkinagda golf18/07 03:40
glguyrefactoring is one of my favorite forms of procrastination18/07 03:40
auguroh wait, i installe a new ghc18/07 03:41
copumpkinaugur: yeahl ooks like that18/07 03:41
auguri wonder if that mucked it up18/07 03:41
stepkutah.. I see.18/07 03:41
copumpkinglguy: I'd think that procrastination using agda is a fairly uncommon form of it18/07 03:41
stepkutremoving the law of excluded middle never made sense to me before :)18/07 03:41
augurcopumpkin: what should i do D:18/07 03:41
copumpkinaugur: reinstall shit until it works18/07 03:42
auguri dont remember how i installed agda! D:18/07 03:42
copumpkinstepkut: yeah, you could postulate in agda, and it would basically look like LEM : forall {A : Set} -> Dec A18/07 03:42
copumpkinin practice though, you don't get it for free, and need to provide a decision procedure (an algorithm) that provides a Dec a18/07 03:43
stepkutcopumpkin: speaking of practice.. any idea for a good source of problems to practice with using Agda? I tend to pick tricky things it seems18/07 03:43
copumpkinstepkut: I kind of go on about this a lot, but I had fun playing with even-ness and odd-ness in agda when I was getting started18/07 03:44
stepkutk18/07 03:44
copumpkinfigure out a way to come up with Even : Nat -> Set18/07 03:44
copumpkinand Odd : Nat -> Set18/07 03:44
copumpkinthen talk about addition on naturals and multiplication18/07 03:44
copumpkinand how evenness and oddness moves across them18/07 03:44
copumpkinlike the sum of two evens is even18/07 03:44
copumpkinthe sum of two odds is odd18/07 03:45
copumpkineven :P18/07 03:45
* copumpkin kicks himself18/07 03:45
stepkut1 + 1 = 2? Even russell couldn't do that :p18/07 03:45
copumpkin:)18/07 03:45
copumpkinanyway, let me know if you have trouble with those18/07 03:45
stepkutk18/07 03:45
copumpkinthere's about a dozen ways to even write Even : Nat -> Set and Odd18/07 03:46
stepkutcool18/07 03:46
copumpkinI've been meaning to write an intro series to agda18/07 03:46
copumpkinbut you know18/07 03:46
copumpkinI procrastinate a lot18/07 03:46
stepkutyeah18/07 03:46
stepkutbut Agda isn't a lazy language, is it ?18/07 03:46
copumpkinit's neither lazy nor not, really18/07 03:46
copumpkinit could compile to something lazy without affecting correctness18/07 03:47
copumpkinor strict18/07 03:47
copumpkinthe essence of actual laziness is sort of captured by codata in agda18/07 03:47
copumpkin(coinduction)18/07 03:47
stepkuthow is IO looking these days?18/07 03:48
copumpkinI wouldn't know :)18/07 03:48
stepkut:)18/07 03:48
copumpkingoes to show what kinds of things we use it for18/07 03:48
stepkutI remember one time I actually compiled and ran an Agda program18/07 03:48
glguyIs there something like   both : {A B : Set} → Dec A → Dec B → A × B ⊎ ¬ A ⊎ ¬ B in the standard library somewhere?18/07 03:50
copumpkinthat would require one fewer case match?18/07 03:51
stepkutcopumpkin: thanks for your help!18/07 03:51
copumpkinstepkut: no problem!18/07 03:51
* stepkut is off to practice contortion and write some hardstyle18/07 03:51
copumpkinenjoy :)18/07 03:51
* copumpkin runs off to 7-1118/07 03:51
copumpkinI think that Decide type should be in the std lib18/07 04:09
copumpkinI've defined it a bunch of times too18/07 04:09
copumpkinglguy: but anyway, isn't that type transforming from something that needs four case matches to something that needs three? it doesn't seem like a huge win18/07 04:10
glguycopumpkin: the point isn't to save pattern matches in general such much as to consolidate the two failure cases into one18/07 04:10
copumpkinah18/07 04:11
glguybut beyond that I figured that treating Dec's as bools would be in the library already somewhere18/07 04:11
glguy"both" is like && in a way18/07 04:11
copumpkinyou can treat them as bools18/07 04:11
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Decidable.html#59318/07 04:12
glguybut that doesn't really help to combine them like booleans, does it?18/07 04:12
copumpkinoh, no18/07 04:13
copumpkingood point18/07 04:13
copumpkinsomething like Dec A -> Dec B -> Dec (A x B) ?18/07 04:13
copumpkinand Dec A -> Dec B -> Dec (A or B)18/07 04:13
copumpkinhmm18/07 04:13
glguybut \neg (A x B) is weaker than   \neg A or \neg B18/07 04:13
copumpkintrue18/07 04:14
glguyin my particular case I think I can manage with that weaker statement18/07 04:14
glguyerr, no18/07 04:15
glguyno, I can :)18/07 04:15
copumpkinyou sure? :P18/07 04:15
* glguy increases his typing buffer time18/07 04:15
Eduard_MunteanuMm? So you don't get DeMorgan laws?18/07 04:22
copumpkinyou get three out of four of them18/07 04:22
copumpkin@djinn Either (Not a) (Not b) -> Not (a, b)18/07 04:22
lambdabotf a =18/07 04:22
lambdabot    case a of18/07 04:22
lambdabot    Left b -> \ (c, _) -> b c18/07 04:22
lambdabot    Right d -> \ (_, e) -> d e18/07 04:22
copumpkin@djinn Not (a, b) -> Either (Not a) (Not b)18/07 04:22
lambdabot-- f cannot be realized.18/07 04:22
Eduard_MunteanuAs a consequence of missing excluded middle?18/07 04:22
Eduard_MunteanuHm.18/07 04:23
copumpkin@djinn (Not a, Not b) -> Not (Either a b)18/07 04:23
lambdabotf (a, b) c =18/07 04:23
lambdabot    case c of18/07 04:23
lambdabot    Left d -> a d18/07 04:23
lambdabot    Right e -> b e18/07 04:23
copumpkin@djinn Not (Either a b) -> (Not a, Not b)18/07 04:23
lambdabotf a = (\ b -> a (Left b), \ c -> a (Right c))18/07 04:23
copumpkinderp?18/07 04:23
copumpkinoh okay18/07 04:23
Eduard_Munteanu@djinn (Not (Not x) -> x) -> Not (a, b) -> Either (Not a) (Not b)18/07 04:24
lambdabot-- f cannot be realized.18/07 04:24
Eduard_Munteanu@djinn (forall x. Not (Not x) -> x) -> Not (a, b) -> Either (Not a) (Not b)   -- maybe this...18/07 04:25
lambdabotCannot parse command18/07 04:25
Eduard_MunteanuBah.18/07 04:25
djahandarie@djinn Not (a, b) -> Not (Not (Either (Not a) (Not b)))18/07 04:25
lambdabotf a b = void (b (Right (\ c -> void (b (Left (\ d -> a (d, c)))))))18/07 04:25
copumpkin@djinn (Either (Not a) a) -> Not (a, b) -> Either (Not a) (Not b)18/07 04:26
lambdabotf a b =18/07 04:26
lambdabot    case a of18/07 04:26
lambdabot    Left c -> Left c18/07 04:26
lambdabot    Right d -> Right (\ e -> b (d, e))18/07 04:26
copumpkin@djinn (Either (Not b) b) -> Not (a, b) -> Either (Not a) (Not b)18/07 04:26
lambdabotf a b =18/07 04:26
lambdabot    case a of18/07 04:26
lambdabot    Left c -> Right c18/07 04:26
lambdabot    Right d -> Left (\ e -> b (e, d))18/07 04:26
Eduard_MunteanuAh, I see.18/07 04:26
glguynot (A and B) says that you can't have A and B at the same time, but it doesn't reveal which of the two you don't have :)18/07 04:29
Eduard_MunteanuYeah, hence you can't prove Either (Not a) (Not b) constructively either18/07 04:29
Eduard_Munteanu*from that18/07 04:29
* djahandarie liked his negative translation18/07 04:30
* Eduard_Munteanu wonders if (forall x. Not (Not x) -> x) was the right way to go about it, conceptually18/07 04:31
copumpkinyeah it was18/07 04:31
Eduard_Munteanu@djinn (forall x. Not (Not x) -> x) -> Not (a, b) -> Either (Not a) (Not b)18/07 04:32
lambdabot-- f cannot be realized.18/07 04:32
djahandariedjinn wouldn't have been able to figure that out though, even if you didn't add the comment18/07 04:32
Eduard_MunteanuAh, so it wasn't just the comment18/07 04:32
djahandarieSee? :p18/07 04:32
dolioDjinn does propositional logic, not first-order logic.18/07 04:32
Eduard_Munteanu@djinn (Not (Not x) -> x) -> Either x (Not x)18/07 04:32
lambdabot-- f cannot be realized.18/07 04:32
Eduard_Munteanu@djinn Either x (Not x) -> (Not (Not x) -> x)18/07 04:33
lambdabotf a b =18/07 04:33
copumpkinyou need to instantiate it yourself18/07 04:33
lambdabot    case a of18/07 04:33
lambdabot    Left c -> c18/07 04:33
lambdabot    Right d -> void (b d)18/07 04:33
Eduard_Munteanucopumpkin: as in @djinn a few cases and use double negation elimination myself, I suppose18/07 04:34
copumpkinbut if you actually wanted to write a proof of that in haskell, you could18/07 04:34
copumpkinwith rank-2 types18/07 04:34
Eduard_MunteanuThough I'm not sure they're really equivalent.18/07 04:34
copumpkin(forall x. Not (Not x) -> x) -> Either x (Not x)18/07 04:34
Eduard_MunteanuAh, so they are.18/07 04:35
Eduard_Munteanu(double neg elim <=> excluded middle)18/07 04:35
copumpkin(forall x. Not (Not x) -> x) -> (forall x. Either x (Not x))18/07 04:35
Eduard_MunteanuSame thing no?18/07 04:36
copumpkinyeah18/07 04:36
Eduard_MunteanuWhat would you call Agda + excluded-middle though? Constructive classical logic? Or it's still missing too much to be called "classical" vaguely?18/07 04:39
Eduard_Munteanu(IIRC it's consistent)18/07 04:39
glguy  dem : {A B : Set} → ¬ (A × B) → ¬ (¬ (¬ A ⊎ ¬ B))18/07 04:40
glguy  dem f g = g (inj₁ (λ a → g (inj₂ (λ b → f (a , b)))))18/07 04:40
dolioIt's just classical.18/07 04:40
dolioIt's not constructive.18/07 04:41
glguyI love the structure of that18/07 04:41
Eduard_MunteanuHm. I thought it'd still be constructive wrt how you go about proving stuff.18/07 04:41
dolioNo.18/07 04:42
dolioYou can, of course, still prove things constructively. That is true in any classical logic.18/07 04:43
dolioCantor's diagonal argument is constructive even though it's often presented in classical mathematics.18/07 04:43
glguyI think of classical / constructive like Haskell's pure / IO functions. You can do both in agda, but when you want to wrap things up in double negation you can prove it in the double negation monad just like you do your impure programs in haskell in the IO monad18/07 04:44
Eduard_MunteanuSo you can more or less prove stuff like the intermediate value theorem similarly to how it's done in math books? Or is that another notion of constructive (one for the underlying set theory)?18/07 04:44
dolioBut proving things via excluded middle or double negation elimination or... is not constructive.18/07 04:45
Eduard_MunteanuOh.18/07 04:45
Eduard_MunteanuSo you meant it's not constructive because something (excluded middle) made it so, but it's still not classical logic / math?18/07 04:46
dolioIsn't the intermediate value theorem usually proved non-constructively?18/07 04:46
glguyIf you are satisfied with a proof that something doesn't not exist you can prove its double negation18/07 04:46
glguybut ina classical logic you can't prove something does exist18/07 04:46
Eduard_Munteanudolio: afaik, yeah18/07 04:46
dolioConstructive arguments don't become non-constructive just because excluded middle exists in whatever logic you're writing in.18/07 04:47
dolioBecause you can port them to a constructive logic.18/07 04:47
dolioBut if a logic admits excluded middle, it's classical.18/07 04:48
glguyBut you can't show they are constructive18/07 04:48
glguywithout reading each line18/07 04:48
copumpkinif your logic's standard library includes LEM18/07 04:48
copumpkin>_>18/07 04:48
glguyjust like if you can write a pure function in haskells IO monad18/07 04:48
glguy-if18/07 04:48
glguyit just don't show itself to be pure18/07 04:49
Eduard_MunteanuYeah, the question was more along the lines of whether Agda + excluded middle gives me access to mainstream math. AFAIK there's stuff you can't prove constructively.18/07 04:49
glguyEduard: If you want to prove something clasical in Agda you just prove its double negation18/07 04:50
dolioDepends what mainstream math you want.18/07 04:50
glguyso a classical proof of "P" becomes not not P in Agda18/07 04:50
dolioAgda doesn't have quotient types, for instance.18/07 04:50
copumpkinyou can pretend you're quotiented by using a setoid though, can't you?18/07 04:51
dolioSo I don't know whether you get the classical axiom of choice.18/07 04:51
dolioMaybe you do.18/07 04:52
Eduard_MunteanuI see.18/07 04:52
dolioI think there's some paper that constructive choice + excluded middle = classical choice, though. I don't remember it requiring quotients, so maybe you'd even have that.18/07 04:54
glguycopumpkin: Did you get a chance to see what SpaceChem was?18/07 04:54
copumpkinnah, been doing lots of boring shit today, sorry :/18/07 04:55
dolioAgda is also predicative, which excluded middle doesn't really change. So it might still be weaker than ZF.18/07 04:55
glguycopumpkin: Apology unnecessary :)18/07 04:55
dolioOr, ZFC.18/07 04:55
Eduard_MunteanuThat makes me wonder if that reads as \exists x. Not (Not (P x)) <=> \classical_exists x. P x18/07 04:56
Eduard_Munteanu(given excluded middle that is)18/07 04:57
dolioGiven excluded middle, exists x. P x is classical.18/07 04:57
Eduard_MunteanuOh.18/07 04:58
Eduard_MunteanuThanks. I guess I need to try and write some theorems to see how it works.18/07 04:58
dolioIf you want to encode classical existential in a constructive logic without excluded middle, it's Not (forall x. Not (P x)), roughly.18/07 04:59
dolioAlthough you have to fiddle with P.18/07 04:59
Eduard_MunteanuHm.18/07 04:59
Eduard_MunteanuOh, right, it makes sense.18/07 05:00
copumpkinI guess I can't actually write the haskell-like stream fusion in agda18/07 05:26
copumpkinsince that skip constructor isn't productive18/07 05:27
copumpkinI wonder if it could carry a natural that tells you how long until you get a non-skip18/07 05:27
stepkutcopumpkin: by, Even : Nat → Set, do you mean, data Even : Nat → Set where .., or a function, Even : Nat → Set18/07 05:48
copumpkinboth are possible18/07 05:48
copumpkinI kind of prefer the former18/07 05:49
copumpkinbut it's kind of fun to explore both18/07 05:49
stepkutso, I am going to create something like this maybe? data Even : ℕ → Set where even : ℕ18/07 05:50
stepkuthmm, that doesn't even type check ;)18/07 05:50
cayleestepkut: the datatype should reflect the structure of a proof that n is even.18/07 05:51
stepkutyeah18/07 05:51
stepkutok. here is my first implemenation, http://hpaste.org/4916018/07 05:59
stepkuti wish I got experience points or something..18/07 06:00
stepkutYou have gained 10 experience points. You are now a Level 1 Dependent Type Hacker. You were eaten by a grue.18/07 06:01
stepkutIs it 'easy' to use agda as a library in a haskell app? For example, making a web application would could type check agda expressions?18/07 06:02
stepkutI see that there is a libghc-agda-dev...18/07 06:02
copumpkinstepkut: that's it!18/07 06:05
copumpkinstepkut: there's another way to do it that I rather like18/07 06:06
stepkutcopumpkin: I'll see what else I can think up18/07 06:06
stepkutcopumpkin: that was just the first idea that I had18/07 06:06
copumpkinit's a good one, but think how you'd define odd and avoid duplication18/07 06:06
stepkutwhat do you mean by 'avoid duplication'18/07 06:07
copumpkinwell18/07 06:07
copumpkinyou could make another type for odd18/07 06:07
copumpkinthat had the same structure18/07 06:07
stepkutright18/07 06:07
copumpkinbut had a base case of 118/07 06:07
stepkutright18/07 06:07
copumpkinhowever18/07 06:07
copumpkineven and odd can kind of be defined in terms of one another18/07 06:08
stepkutright18/07 06:08
copumpkinthere's a mutual block in agda18/07 06:08
copumpkinnot sure if you've come across it18/07 06:08
copumpkinit lets you define things that refer to each other or out of order18/07 06:08
stepkutah18/07 06:09
stepkutthat would be useful18/07 06:09
copumpkinhttp://hpaste.org/49161 is what I had in mind18/07 06:09
stepkutwell.. I'm not going to look at it yet18/07 06:10
copumpkinok :)18/07 06:10
stepkutgoing to go to bed and then figure out how to use the mutual block18/07 06:10
copumpkincool18/07 06:15
copumpkinwhen modeling a haskell API that uses rank-2 types/existentials to provide static guarantees about stuff18/07 06:19
copumpkinI wish I could prove stuff about it18/07 06:19
Eduard_Munteanucopumpkin: REPA stuff again?18/07 06:24
copumpkinnah18/07 06:25
Eduard_MunteanuBTW, is that in a Git repo somewhere?18/07 06:25
copumpkingithub.com/copumpkin/derpa18/07 06:25
Eduard_MunteanuNice.18/07 06:25
copumpkinit doesn't actually seem to work on the latest agda18/07 06:25
copumpkinbut I haven't tracked down why yet18/07 06:25
glguycopumpkin: you still up?18/07 07:39
copumpkinyep18/07 07:40
* copumpkin never sleeps18/07 07:40
glguyhttp://www.galois.com/~emertens/DecSplits/DecSplits.html#230018/07 07:40
glguythis might be obvious already, but I found a hack to use a data type instead of a record18/07 07:41
glguywhere you have the function in the index18/07 07:41
glguy"open-alt" is my hack18/07 07:41
glguyI can translated to the exact same format as the record18/07 07:42
copumpkinwhy use a Sigma for open-alt instead of the type you defined at the top?18/07 07:42
glguyno reason at all18/07 07:42
copumpkinwe've actually noted several times that nested sigmas are horribly slow18/07 07:42
glguyso I suppose what I'm showing is that you can always cast to a similar record..18/07 07:42
copumpkinnot really sure18/07 07:42
copumpkinyeah18/07 07:42
glguyI just did that as a convenience18/07 07:42
copumpkinyou can always convert back and forth with those indexed types18/07 07:42
copumpkinthey're just often a pain to work with directly18/07 07:43
* copumpkin weeps18/07 07:43
copumpkinin my CT library, I took double nested sigmas and replaced them with records18/07 07:43
copumpkinand memory usage for typechecking went down significantly18/07 07:43
copumpkin2-3x smaller18/07 07:43
glguyThat's good to know18/07 07:43
glguyIn my previous experiences records made things much slower18/07 07:44
glguyso I've avoided them18/07 07:44
copumpkinweird18/07 07:44
glguynot slower than sigmas18/07 07:44
copumpkinwho knows what's going on :)18/07 07:44
glguyjust slow in general18/07 07:44
copumpkinah18/07 07:45
copumpkinit's looking nice18/07 07:45
copumpkinvery clean18/07 07:45
copumpkina bit weird to see camelCase and hyphen-names at once18/07 07:46
glguyI'm running out of ways to procrastinate on this file18/07 07:46
glguyOH, the "decSplits" is an artifact from copying Saizan's type signature :)18/07 07:46
copumpkinwas thinking of emptySplit too18/07 07:46
copumpkinyou also have an unused dem lying around :)18/07 07:47
glguyThat's just my fault18/07 07:47
glguyfixed :)18/07 07:48
copumpkinw00t18/07 07:49
copumpkinnow prove it has a reasonable time complexity :)18/07 07:50
glguyI have to work out some lexicographic induction (I believe) to convince my match function to work on the regexp "star"18/07 07:50
glguyshow it that match is being called either on a smaller regexp or the same regexp and a smaller string18/07 07:50
copumpkinI'm sure you'll come up with a kleene implementation18/07 07:50
* copumpkin sighs at xplat18/07 07:50
glguyheh, reasonable time complexity18/07 07:51
glguynone of my agda code ever actually executes18/07 07:51
glguyafter type checking18/07 07:51
copumpkinI think the std lib contains lexicographic induction18/07 07:51
copumpkinsame here :)18/07 07:51
glguyI was trying to explain to a friend why it would be hard to provide a proof that there was *not* a way to split a list in two to satisfy the two predicates18/07 07:55
glguyHe's not an dependent type "programmer". "Just don't return a match if you don't have one" was basically where I got stuck18/07 07:55
glguyand "well, you'd have found it if there was one, so what're you trying to do?"18/07 07:56
bxcexplaining that stuff to non-mathematicians is kinda hard18/07 07:59
glguy(I think I'm inconveniencing my dog by moving while he tries to sleep on me, he keeps glaring at me when I wake him by typing...)18/07 08:07
bxcpoor puppy18/07 08:09
bxci think it probably also has the same problem as explaining monads: everyones intuition about what a computer actually does is different, so then what you have to add on to explain things is different for each person18/07 08:21
glguycopumpkin: still up?18/07 09:41
* glguy is disappoint18/07 09:42
glguycopumpkin: for when you return http://www.galois.com/~emertens/DecSplits/RegExp.html18/07 10:18
glguyI got the lexicographic induction for matching working (had to modify the splitting function to take a restricted recursive function)18/07 10:19
djahandariepigworker, :O18/07 15:09
pigworkernothing fancy18/07 15:09
pigworkerjust compatibility with new mtl18/07 15:09
djahandarieAh18/07 15:10
augur:|18/07 16:48
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda18/07 16:48
augurline 68 is highlighting :(18/07 16:48
augurthe lhs of 68, and the () on the following line18/07 16:48
Saizanprobably because _cc₂_ is still undefined18/07 16:53
augurSaizan: but its on the lhs which isnt related to _cc2_! :(18/07 16:55
Saizanexcept that a with has to abstract the pattern matches18/07 16:57
Saizan*the pattern matched expression from the goal18/07 16:57
augurwha?18/07 16:57
Saizanwhich is not that easy when the goal is undefined18/07 16:57
Saizanhave you read view from the left?18/07 16:58
auguri have, somewhat. it got a bit hard halfway through18/07 16:59
augurill read it again18/07 16:59
Saizanif you look at the rules for the elaboration of with you'll see that they mess with the goal type too18/07 17:00
augurhmm18/07 17:00
auguri havent had this problem before18/07 17:01
augurfor instance, if i just use set theoretic trees, instead of a tree type, it works fine18/07 17:01
Saizanfoo : ∀ {A : Set} -> A -> { }018/07 17:04
Saizanfoo x with x18/07 17:04
Saizan... | z = { }118/07 17:04
Saizaneven the above gets the same kind of yellow18/07 17:04
Saizanif i remove the with and/or fill the ?0 it's all fine18/07 17:04
augurhmm18/07 17:04
augurok18/07 17:05
augurbut.. it doesnt always! :P18/07 17:05
Saizanshow me :)18/07 17:05
augurSaizan: hm.. maybe you're right :O18/07 17:12
glguySaizan: With your help on Split I finished my implementation of match : Decidable (λ xs r → xs ∈ ⟦ r ⟧) where r is a regular expression http://www.galois.com/~emertens/DecSplits/RegExp.html#200718/07 17:15
Saizannice18/07 17:16
augurhmm18/07 17:34
augurSaizan: even defining root cc2 root = \bot doesnt prevent the yellow18/07 17:35
Saizani guess there's more than18/07 17:38
Saizan*then18/07 17:38
augurthats what i figured!18/07 17:49
augurbut how? its on the lhs! :(18/07 17:49
Saizanbtw, you can use \bot-elim instead of the with, as a workaround18/07 17:54
Saizanmaybe you should ask on the list, it'd be better if you can reproduce this with less code though18/07 17:56
augurSaizan: im sure someone in here has insights xp18/07 18:00
augurbut i could cut it down to a tiny little bit of code, definitely18/07 18:00
auguralso i'll try \bot-elim18/07 18:00
auguralso also WHO THE HELL IS CODENSITY >_<18/07 18:00
Saizan"who"?18/07 18:01
djahandarieaugur, it's applicative18/07 18:01
djahandarie(The person.)18/07 18:01
augurSaizan: theres someone in here named codensity18/07 18:02
Saizani see18/07 18:02
augurim being stalked by CT concepts i dont understand :(18/07 18:02
Saizanit happens18/07 18:02
* kan_extension stares at augur 18/07 18:03
augurAHHHHHH18/07 18:03
djahandarieHe was never heard from again.18/07 18:04
djahandarie@quote augur <augur> Saizan: theres someone in here named codensity <Saizan> i see <augur> im being stalked by CT concepts i dont understand :( <Saizan> it happens - Saizan is now known as kan_extension * kan_extension stares at augur <augur> AHHHHHH - augur [~augur@] has quit [] <djahandarie> He was never heard from again.18/07 18:06
lambdabotPlugin `quote' failed with: regex failed: (ReturnCode 7,"Unmatched [ or [^")18/07 18:06
djahandarie@remember augur <augur> Saizan: theres someone in here named codensity <Saizan> i see <augur> im being stalked by CT concepts i dont understand :( <Saizan> it happens - Saizan is now known as kan_extension * kan_extension stares at augur <augur> AHHHHHH - augur [~augur@] has quit [] <djahandarie> He was never heard from again.18/07 18:06
lambdabotIt is stored.18/07 18:06
augur<318/07 18:06
djahandarieYou should feel lucky I didn't /nick dagger_closed_symmetric_braided_monoidal_category18/07 18:07
augurx.x18/07 18:07
auguryou'd've ended up as18/07 18:08
augurdagger_closed_sy18/07 18:08
djahandarieFreenode obviously can't take the full power of category theory18/07 18:08
augurso if i can use \bot-elim, that means the lhs is impossible, right18/07 18:09
augureffectively, the lhs is () but its not convenient to show it18/07 18:09
augurbrb18/07 18:10
anafunctor@tell augur I'm watching you18/07 18:11
lambdabotConsider it noted.18/07 18:11
Saizanit means you can derive a contradiction18/07 18:11
glguyI'm trying to use my regexp matcher to implement test : (a b : Carrier) → a ∷ a ∷ a ∷ b ∷ [] ∈ ⟦ symb a ⋆ ⊙ symb a ⊙ symb b ⟧18/07 19:40
glguyghc is using minutes of cpu and 5 of my gigs18/07 19:40
copumpkinlol18/07 19:40
glguyas it tries to load the file18/07 19:40
copumpkinsounds about right18/07 19:40
glguyand swapping because it needs more than those 518/07 19:41
copumpkinI really want 8 or 16 gigs for agda18/07 19:41
copumpkinsince the CT stuff gets ridiculous18/07 19:41
copumpkinit took xplat a lot of effort to make the monoidal categories stuff tractable memory-wise18/07 19:41
augurhrmph18/07 19:46
lambdabotaugur: You have 1 new message. '/msg lambdabot @messages' to read it.18/07 19:46
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda 138/139 is spazzing18/07 19:47
augurgiving me red, saying it cant check that l = w when checking that x : TreeIndex w18/07 19:47
auguri have no idea where this w is coming from :|18/07 19:47
copumpkinw is annoying18/07 19:47
copumpkinsome weird desugaring artifact18/07 19:47
copumpkinthat makes it through into errors18/07 19:47
augurbut its weird, because l : Tree, so if i with l, itll be either leaf or branch18/07 19:48
augurand x : TreeIndex l already18/07 19:49
augurso why the hell cant i match on l18/07 19:49
copumpkinbecause it's more complicated than the thing can handle right now18/07 19:49
copumpkinbut with is just writing a helper function for you18/07 19:49
copumpkinyou can probably write one yourself18/07 19:49
copumpkinit's just a pain in the ass18/07 19:49
augurwhat do you mean just writing a helper function for me18/07 19:50
copumpkinif I have18/07 19:50
copumpkinsomeFunc x y z with f x y18/07 19:50
copumpkinit'll just make a new function that takes four arguments18/07 19:50
copumpkinI think four?18/07 19:51
auguri dont follow18/07 19:51
copumpkinso someFunc takes three arguments18/07 19:51
copumpkinand you want to pattern match on up to four things18/07 19:51
copumpkinsince you'd like to pattern match on the result of f x y to18/07 19:51
copumpkintoo18/07 19:51
copumpkinright?18/07 19:52
kosmikusyes, I think "with" is implemented by introducing local functions18/07 19:55
copumpkinso I think the (fairly frequent in my experience) case in which it bitches about the w18/07 19:56
copumpkinis when the additional parameter you're adding would also show up in the result type (and is thus more dependent than it might otherwise be)?18/07 19:56
copumpkinnot sure18/07 19:56
copumpkinI haven't really tried reducing it18/07 19:57
copumpkinI wonder if there's already a bug for it18/07 19:57
xplatif you see a w in an error, it means something has been abstracted by a with but something else needed it to actually be the type it was abstracted away from18/07 19:58
xplatit means you need more withs!18/07 19:58
copumpkinhmm18/07 19:58
copumpkinI thought that was more a symptom of not being able to pattern match on the with expression18/07 19:59
copumpkinthe indices getting refined aren't available, so you add more withs to make them18/07 19:59
copumpkinbut sometimes it'll bitch if you even add a with (and don't pattern match on the result at all)18/07 19:59
xplatthe pattern that starts failing isn't always the one on the right of |, sometimes one of the ones on the left will too18/07 20:00
copumpkinwell I mean18/07 20:01
copumpkinthere don't have to be pattern at all, as far as I can see18/07 20:01
xplatbecause the type of the variable it's matching has changed so the pattern no longer makes sense18/07 20:01
copumpkinoh, hmm18/07 20:01
augurcopumpkin: i see.18/07 20:02
xplatso like if you have factorial : N -> N , and you somehow get the idea in your zero case to do factorial zero with N18/07 20:03
xplatthen there is no way you can fill in factorial zero | ? = ? to get something type-correct18/07 20:04
copumpkinoh I think I see what you mean18/07 20:04
xplatbecause the zero itself is already wrong, the type of the first argument is now a variable ('w') rather than N18/07 20:04
xplati finally understood this when working with heterogenous equality, where it comes up pretty often18/07 20:07
copumpkinah18/07 20:08
copumpkinfunky :)18/07 20:08
copumpkingood to know though18/07 20:08
copumpkinthanks18/07 20:08
auguri have no idea how to write my own functions for this.. x.x18/07 20:09
copumpkinlet me write you a quick example18/07 20:09
augurcopumpkin: no i get the point, its just that theres pattern matching information that i want to carry through18/07 20:09
augurand i dont know what the type should be18/07 20:09
copumpkinah, dunno then18/07 20:09
augurwhat type does a withed function get??18/07 20:18
copumpkinthe type of the current function plus the types of the expressions the with adds to it18/07 20:18
augurhmm18/07 20:19
auguryeah thats probably why this isnt working then18/07 20:20
augurbecause the current type is like.. F x -> blah18/07 20:20
augurfor a value x18/07 20:20
augurand i want to with l, where F x ~ G l18/07 20:21
augurx : TreeIndex l   right, so the funciton is like...   foo : F x -> blah18/07 20:30
augurbut i cant just make it fooHelp : F x -> Tree -> blah18/07 20:30
augurbecause there's no connection between x and the Tree argument18/07 20:30
augurbut i cant just toss in some extra arguments to capture l and x in the right way, because then the rest of the types will get all messed up18/07 20:36
augurbecause theres no guarantee that this or that thing is inhabited18/07 20:36
auguror even definable18/07 20:36
Saizani'm pretty sure there's a way to do it18/07 20:38
Saizanyou could even just add F x \== G l as an additional argument18/07 20:38
augurSaizan: wha18/07 20:39
xplatthe key to using withs/helper functions to highly refine indices and pattern-match on your stubbornest data families is 'need to know'18/07 21:00
copumpkinsomeone should write a guide to that18/07 21:01
copumpkinI have a general feeling for what's good and what isn't18/07 21:01
copumpkinbut some pattern matches still stump me18/07 21:01
djahandarieI don't even have a general feeling18/07 21:01
augurcopumpkin: you should wrte the general guide for djahandarie and me :D18/07 21:05
xplatwell, the basic thing it comes down to is, types that are equal don't always unify18/07 21:16
xplatif you want to cast between two equal types that don't unify, or pattern-match with a constructor that has sharing in its indices, you have to erase enough information to create a local context where they do unify18/07 21:18
xplatfor a function, you want to give it evidence that the types are equal, but not what exactly they are18/07 21:24
xplatfor a with, you want to match enough patterns to erase all evidence of what one of the types was supposed to be18/07 21:24
xplatif you're lucky, that's just one.  if not, you will see errors18/07 21:25
xplatthere are basically two kinds of pattern matching that go into a with18/07 21:26
xplatthe with itself matches an expression pattern at a compile-time, syntactic level and erases/hides information about its provenance18/07 21:28
xplatthen the patterns below the with match at runtime and add in new information18/07 21:28
copumpkinin other news, http://lolpics.se/pics/19193.jpg18/07 21:36
thoughtpolicecopumpkin: that made my day, thanks18/07 21:51
copumpkinwe communicate in rage faces here at work18/07 21:52
thoughtpolicecopumpkin: you do too? we sometimes use pictures from bloodsport18/07 21:57
copumpkinlol18/07 21:57
thoughtpolicehttp://4.bp.blogspot.com/_mLlzOnL7nec/RpCJdcjMp1I/AAAAAAAAApg/MhvtTf_BsuQ/s400/bloodsport8.jpg18/07 21:57
thoughtpolicealso http://spinoff.comicbookresources.com/wp-content/uploads/2011/05/bloodsport.jpg18/07 21:57
copumpkinnice18/07 21:57
Saizanmust be a bliss18/07 21:59
--- Day changed Tue Jul 19 2011
stepcutcopumpkin: http://hpaste.org/4918919/07 01:57
copumpkinexcellent!19/07 01:57
copumpkinnow prove that two even numbers added give you another even number!19/07 01:58
stepcutk19/07 02:00
stepcutbut first, gymnastics class ;)19/07 02:00
copumpkinok :)19/07 02:00
glguyCheck out this epic proof which states that [false , false] ∉ ⟦ symb true ⊙ symb true ⟧19/07 02:47
glguyhttp://hpaste.org/4919019/07 02:47
copumpkinbeautiful19/07 02:47
glguyIt explains why almost none of my test cases which don't match never terminate19/07 02:48
glguyerrr, too many negations in that sentence19/07 02:48
glguyalmost all of my non-matching test cases fail to terminate19/07 02:48
copumpkinhave you tried compiling it to see how bad it runs?19/07 02:52
copumpkin*badly19/07 02:53
copumpkincompile it to ruby :)19/07 02:53
glguyno, i haven't tried compiling it to anything, i don't really know how to make a driver to wrap it19/07 03:02
copumpkinyou can stick a main : IO \top into that19/07 03:03
copumpkinand I think C-c C-x C-c will compile it19/07 03:03
copumpkinthere's IO in the standard library but I haven't used it19/07 03:03
auguris there any way to figure out why the goals are what they are?19/07 03:18
augurfor instance, im trying to provide a function of type   T -> left x cc_2 left y19/07 03:18
augurer, cc219/07 03:19
augurand my goal is   ?0 _cc0_ _cc1_ x y19/07 03:19
copumpkinthat just means your goal type reduces to another goal19/07 03:19
augurcopumpkin: sure, im just curious how thats coming about19/07 03:19
copumpkinfill in hole 0 and it'll give you a better goal here19/07 03:19
augurwhy left x cc2 left y reduces to ?0 _cc0_ _cc1_ x y19/07 03:19
copumpkinthe goal type normalizes to ?019/07 03:19
augurbecause the correct answer is that   left x cc2 left y  =  x cc0 y19/07 03:21
copumpkinclearly not :)19/07 03:21
augurwhich is natural given ?0 _cc0_ _cc1_ x y19/07 03:21
augurtheres only so much you can do with those four arguments given their types19/07 03:21
augurand so im curious how this reduced to something like this19/07 03:21
augurhrmph19/07 03:29
auguri have no idea how to keep this information accessible :(19/07 03:29
glguyDoes this bug exist in the development version of agda?19/07 04:06
glguyhttp://hpaste.org/4919419/07 04:06
augurglguy: i dont think thats a bug19/07 04:11
glguythe first line breaks the fact that proj\_1 is a record selector19/07 04:12
glguy"panic" shouldn't happen19/07 04:12
auguroh i see19/07 04:12
auguris it a record selector tho19/07 04:12
glguyyeah19/07 04:12
auguri mean, are you sure it works WITHOUT the proj1 on the lhs?19/07 04:13
glguyyup19/07 04:13
augurinteresting19/07 04:13
augurwell now you know not to name your arguments after stuf!19/07 04:13
glguywell, it's the Emacs mode for Agda that makes that mistake19/07 04:13
glguyI wouldn't pick that name on my own19/07 04:13
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda whats going on with in 141's go? i mean, i cant figure out a way to retain information about the identity of x' as x, and l' as l, even with x' == x constraints19/07 04:21
xplataugur: the information in a \== isn't used as a constraint until you pattern-match on it as a refl19/07 04:30
augurxplat: hmm19/07 04:30
xplataugur: (this is a good thing; otherwise you wouldn't be able to pass them around and still have your functions typecheck)19/07 04:30
augurif i math on it tho, it gives me an error saying leaf != l19/07 04:31
augurwhen checking that refl has type leaf \== l19/07 04:31
augurmatch**19/07 04:31
xplatwhich one did you match on?  l' == l i guess ...19/07 04:32
auguryeah19/07 04:32
augurif i replace the _ after leaf with ll, and then CcCc on ll, it resolves to refl19/07 04:32
augurbut then highlights it red19/07 04:32
augurthats something that frustrates the hell out of me19/07 04:33
auguri can do a case analysis using agda to decide on the cases for me19/07 04:34
xplatyou would have to match on ll first and then l' in this instance, i think.  that is, have the refl in both branches19/07 04:34
augurand the result is invalid code19/07 04:34
augurhow can agda give me invalid code! :|19/07 04:34
augurok ill try ll first19/07 04:34
auguraha there, it replaced leaf with .l19/07 04:35
augurhoorah!19/07 04:35
xplatbut why do you end up doing it this way anyway?  passing a refl and then matching on the same refl at the toplevel is a noop, you could do the same thing by just eliminating l' as a parameter and referring directly to l19/07 04:35
augursure, except i need to match on l19/07 04:36
auguri tried doing    bwd blah with l   and that just kept failing19/07 04:36
xplatdo you remember what exact error you got?19/07 04:36
augursome type error where it couldnt match the type of x with the type that was produced somehow19/07 04:36
auguryeah lemme get it for you19/07 04:37
auguragh19/07 04:37
augurwhat am i doing19/07 04:37
augurwhat does cmd-: do19/07 04:38
augurits highlighting and underlying things gold19/07 04:38
augur:O19/07 04:38
auguranyway the error i get is19/07 04:38
augurl != w of type Tree when checking that the expression x has type TreeIndex w19/07 04:38
xplathave you tried bwd blah blah with l | x?19/07 04:40
auguryeah19/07 04:40
augursame error19/07 04:40
xplator maybe x | l, sometimes the order matters19/07 04:41
augurorder only changed w to w'19/07 04:41
auguroh this is interesting19/07 04:41
augurbringing y into it fixes it19/07 04:41
xplatoh, i knew you'd have to bring y, but i'm surprised it didn't even mention y until you did.  weird.19/07 04:42
xplatthe other option, if you kept 'go' around, would be to make it nice and polymorphic.  move the l', x', y' parameters before the big fat tuple, and change all the references to x, y, and l to x', y', and l'19/07 04:45
xplatthen the call would typecheck, because in the calling environment it knows l' is l and so on, but you could match on x' and y' and l' in go because the inside of go doesn't need to know about the connection with the things in the outer scope19/07 04:46
xplatthat ends up being about the same thing the with is doing, except with a curious obsession with the letter 'w' in the latter case19/07 04:48
auguri tried to have it without any == constraints and make x' dependent on l' not l19/07 04:48
augurbut then the content of the rest of it was bad because there was no knowledge that these things could exist19/07 04:48
xplatyou need to make the tuple dependent on l' (and x' and y') too19/07 04:49
augurno sure, i did that, it just got nasty19/07 04:50
augurbut if i can bring y into it and solve it, im happy19/07 04:50
augurwow wtf is this19/07 04:54
augurif i add y, withing l x and y, instead of a : left x \== left y -> \bot19/07 04:56
auguri get some crazy underspecified type19/07 04:56
xplatwhat crazy underspecified type?19/07 04:56
augura : _653 _cc₀_ _cc₁_ x y leaf root root ≡ _673 _cc₀_ _cc₁_ x y leaf root root → ⊥19/07 04:57
augurbecause i guess it doesnt realize that if a : left x \== left y -> \bot19/07 04:58
augurand x = root19/07 04:58
augurthat that means a : left root \== left y -> \bot19/07 04:58
auguro_O19/07 04:58
augureven if i dont match on anything, if i just bind l,x,y to l',x',y' it complicates the type of a19/07 04:59
augurrather than replace x with x'19/07 05:00
xplatyeah, that will happen.  it usually wouldn't complicate that _much_ though19/07 05:01
augurthis is a pain.19/07 05:02
augurit was actually EASIER if i didnt use a tree data type19/07 05:02
augurthis is crazy19/07 05:02
augurthe purely algebraic trees didnt have this problem19/07 05:02
augurmostly i guess because i never matched on the trees19/07 05:03
auguri just proved things about what they must be using lemmas19/07 05:03
xplatwell, the zipper complicates things too19/07 05:03
augurthe zipper?19/07 05:03
xplati guess it's not really a zipper, it's an unzipper19/07 05:04
augur??19/07 05:04
xplatTreeIndex19/07 05:04
augurer19/07 05:04
augurTreeIndex is just my attempt at doing Fin but for trees19/07 05:04
augurinstead of vectors19/07 05:05
augurobviously its more complicated for trees precisely because the structure of a tree isnt directly correlated to any simple family of sets like Fin19/07 05:06
augurso the idea is that TreeIndex t is just "the set of nodes in t", basically. whereas t itself is the abstract structure, but not the nodes themselves19/07 05:07
augursince you dont want trees to have only one leaf node, even tho its represented in multiple places19/07 05:08
augurleaf = leaf, but the leaves in (branch leaf leaf) are certainly not the same node19/07 05:09
augurbecause their identity as nodes is relative to the environment they're in, not merely their internal content19/07 05:09
augurhence, tree indices.19/07 05:09
augurif i could eliminate tree indices i would19/07 05:12
augurbut i dont know how to19/07 05:12
auguri dont know how to abstractly refer to all and only the nodes of _this tree_19/07 05:12
augurknowing where they are in the tree19/07 05:13
augurbut without conflating internally identical nodes19/07 05:13
auguri worry some times that my little programs are too obnoxious. that all of this case analysis and use of where is unpleasant19/07 05:20
augurand really inelegant19/07 05:20
auguri wish i knew how to make it more elegant. i feel that would eliminate some of the stumbling blocks i come across :\19/07 05:23
djahandarieHmm, I think it might be agdatime tomorrow19/07 05:35
* djahandarie goes to bed on that note19/07 05:35
auguragdatime! :D19/07 05:36
johnnowakhello all. i have a question about the usual typed evaluator you see given in every paper on GADTs. short of using --type-in-type (or maybe disabling the universe check is enough), i believe i'm unable to give Term the type Set -> Set. I can, however, do this in Coq with the -impredicative-set option. Is there any way to manage this in Agda without cheating?19/07 08:43
kosmikusjohnnowak: I'd say the better way to do this in Agda is via a universe.19/07 10:08
johnnowakkosmikus: i'm afraid you'll have to elaborate a bit for me19/07 10:19
johnnowakhere's an example of what i'm going for: http://paste.lisp.org/display/12335019/07 10:20
auguritd be nice if i have a constraint like19/07 10:28
augurf : x \== { }019/07 10:28
augurthan i can choose f = refl19/07 10:28
augurand { }0 is automatically constrained to be x19/07 10:28
kosmikusjohnnowak: http://paste.lisp.org/+2N6E/119/07 10:34
kosmikusaugur: doesn't it work with auto?19/07 10:36
augurafaik no but ill try it at some point19/07 10:37
johnnowakkosmikus: aye, that does work in that particular case, but presumably you're still stuck if you can't easily enumerate indices like that19/07 10:38
johnnowake.g. if 'literal : (a : Set) -> a -> Term a'19/07 10:38
kosmikusaugur: works for me: http://hpaste.org/4920719/07 10:40
augurhm19/07 10:40
johnnowakmaybe i can ask a different question. is there a reason an impredicative Set cannot be added to agda or has it simply not been undertaken? i would presume you could add it with similar elimination restrictions to what coq has19/07 10:41
kosmikusjohnnowak: there are good reasons not to want that, but if you do, then yes, you have to go to Set119/07 10:43
kosmikusjohnnowak: I mean, you *can* do the GADT in Agda, it's just not what I'd recommend19/07 10:43
johnnowakaye, i understand.19/07 10:44
kosmikusjohnnowak: http://hpaste.org/4920819/07 10:44
kosmikusjohnnowak: I don't know the complete history of impredicativity in Agda, but I don't think it's currently planned to add it19/07 10:45
kosmikusjohnnowak: Agda has universe-polymorphism though, with explicit level annotations19/07 10:45
johnnowaki suppose there's not as much incentive to add impredicativity if not using agda as a programming language19/07 10:48
kosmikus?19/07 10:54
johnnowakit just seems as though impredicativity is often used for reasons of expressiveness in a language like haskell. i can, for instance, have a type like 'data Foo where Foo : forall (a : *). (Bar a, Baz a) => a -> Foo', and yet have 'Foo : *'. if i were forced to shove that in the level above, i'd be unable to do much of anything with it19/07 10:57
johnnowaki mean i'd want to be able to conditionally pass values of Foo based on user input for example19/07 10:58
kosmikusHaskell forces you to use * for everything because it lacks anything smaller you can index with on the type level19/07 11:00
kosmikusthat's not the case in Agda19/07 11:00
kosmikusso I don't think this problem ever really arises in Agda19/07 11:00
johnnowakbut i'm not talking about indexing at all there19/07 11:02
johnnowakjust an existential19/07 11:02
johnnowakfor example, i cannot do this in agda:19/07 11:02
johnnowakdata Foo : Set where19/07 11:02
johnnowak  foo : (a : Set) -> a -> Foo19/07 11:02
kosmikustrue19/07 11:03
pigworkerThat's Set in Set, right?19/07 11:03
kosmikusand you don't want Foo to live in Set1?19/07 11:03
johnnowakyes, i can with --set-in-set19/07 11:03
johnnowaker.. --type-in-type19/07 11:03
pigworkerWhy not define the set of *uninhabited* sets?19/07 11:04
johnnowakkosmikus: presumably not if i wanted to manipulate it as a value at runtime19/07 11:04
johnnowakpigworker: ?19/07 11:04
kosmikusjohnnowak: I don't see what you lose in this case by moving it to Set119/07 11:05
pigworkeryou're asking to be allowed the liar paradox19/07 11:05
kosmikusjohnnowak: but also, as I said above, in my admittedly limited programming experience it's quite rare that I actually want to quantify existentially over an arbitrary set19/07 11:05
kosmikusjohnnowak: in by far the most cases, you know quite a bit about the kind of types you're likely to have there, so quantifying over something significantly smaller than set is just fine19/07 11:06
johnnowakkosmikus: sure, in most cases that's true19/07 11:06
kosmikus(which is exactly the option you *don't* have in Haskell)19/07 11:06
johnnowakpigworker: am I? that's quite legal in haskell and doesn't do any harm19/07 11:06
pigworkerno, indeed, that's not enough for the liar paradox19/07 11:07
pigworkerif the bottom level is impredicative, there's no apparent paradox19/07 11:07
kosmikuswell, something being legal in Haskell doesn't mean it does no harm :)19/07 11:07
pigworkerif a higher level is also impredicative, you get a paradox19/07 11:07
johnnowakaye, my point was that i can get away with it in coq with -impredicative-set and, so far as anyone can tell, it doesn't cause problems with suitable restrictions in place19/07 11:07
johnnowakkosmikus: heh, fair enough19/07 11:08
johnnowakpigworker: which is why I was curious why agda's not sprouted an impredicative bottom level19/07 11:08
pigworkeruniformity of levels is valued more than impredicativity in that part of the world19/07 11:09
johnnowakslightly unrelated, but while i've got you.. what is the impact of an impredicative set on erasure? most treatments i've seen seem to assume a predicative hierarchy19/07 11:11
johnnowakthat may be an overly general question19/07 11:12
pigworkerI agree with them -- impredicativity is hard to make sense of, because it involves defining new sets by quantifying over all sets .19/07 11:12
pigworkeras long as you ain't got no typecase, the impact on erasure should be minimal.19/07 11:12
pigworkererasure works ok with set-in-set too!19/07 11:14
johnnowaki suppose i can't see why it wouldn't19/07 11:14
johnnowaki believe cayenne was type : type with no typecase19/07 11:15
johnnowakpigworker: thanks sir19/07 11:16
Saizanjohnnowak: you can still manipulate values of type Foo at runtime even if you make it : Set119/07 11:45
johnnowakSaizan: it should probably be obvious to me why that's true but i'm afraid it isn't, at least if you lack typecase. presumably there's no way to create a runtime value that depends on something of type Set1 then, correct?19/07 12:00
johnnowak(also, i just realized i was wrong before about cayenne.. it did have stratified types. was thinking of augustsson's more recent presentation where he recommends type:type.)19/07 12:01
Saizanthere's nothing special about a type being in Set (n+1) wrt how you can manipulate values of that type19/07 12:04
Saizani.e. Set1 doesn't contain only "kinds"19/07 12:04
johnnowakah, i suppose you're right19/07 12:05
johnnowakSaizan: brain is still adjusting to the lack of a phase distinction19/07 12:15
augurwark19/07 18:18
xplatis there evidence in the stdlib somewhere that toN is an injection, or that two Fins from the same range are equal if they have the same toN?19/07 20:50
copumpkinno, I needed that the other day19/07 20:51
copumpkinit's in my derpa library19/07 20:51
copumpkinbut it's pretty simple iirc19/07 20:51
copumpkinhttps://github.com/copumpkin/derpa/blob/master/REPA/Index.agda#L13419/07 20:52
copumpkinxplat: whatcha making? :o19/07 20:54
xplatjust finishing up the uniqueness of division i started for the heck of it and to learn about what the stdlib has for nats and fins19/07 22:28
copumpkinoh, the proof I have in there?19/07 22:29
xplatthe theorem, i think the proof is slightly different (but similar)19/07 22:42
xplati divided the main proof into 4 cases and used that to solve one of them19/07 22:42
xplatwell, 5 cases because i handled the zero modulus case19/07 22:43
copumpkinnice19/07 22:44
copumpkinmine is horrible19/07 22:44
xplat1) zero modulus -> impossible, there are no Fins19/07 22:45
xplat2) zero quotients -> true, because toN is injective19/07 22:45
xplat3,4) one zero quotient -> impossible, the other number is too high19/07 22:46
xplat5) neither quotient zero, recursive case, big 'where' to provide the equation argument for it19/07 22:47
xplatso i proved ∀ modulus q₁ q₂ → (r₁ r₂ : Fin modulus) → (toℕ r₁ + q₁ * modulus) ≡ (toℕ r₂ + q₂ * modulus) → (q₁ ≡ q₂) × (r₁ ≡ r₂)19/07 22:48
--- Day changed Wed Jul 20 2011
xplatcopumpkin: i proved your original lemma with the help of a couple of one-liners or so20/07 01:11
copumpkinvery nice :)20/07 01:11
xplata 2-liner to wrap my other function as a heterogeneous equality of results, another one-liner to make it homogeneous without an equation of dividends, another one-liner to prove your original lemma from uniqueness of results20/07 01:13
xplati should put it on hpaste or something20/07 01:23
xplathttp://hpaste.org/4925020/07 01:25
copumpkinthat looks quite nice :)20/07 01:27
copumpkinyou're welcome to fork derpa and patch it if you feel like playing with it at all20/07 01:27
copumpkinor I'll incorporate it later20/07 01:27
glguyThrough some unknown optimization which I have apparently done, my regexp matcher can prove non-matches in mere seconds to minutes for strings up to 6 symbols so far :)20/07 03:39
copumpkinoh man!20/07 03:39
copumpkinamazing20/07 03:39
glguyThe proofs of non-match are getting shorter, too20/07 03:40
glguyseems that refactoring into smaller functions in improving runtime20/07 03:40
glguyis*20/07 03:41
glguyha, thanks, Agda:20/07 03:52
glguyAmbiguous module name IO. It could refer to any one of20/07 03:52
glguy  IO.IO20/07 03:52
glguy  IO20/07 03:52
copumpkinlol20/07 03:52
augurwark20/07 04:17
glguyWhat was the syntax trick to get something like do notation?20/07 04:33
glguysyntax bind m (λ x → f) = x ← m , f20/07 04:33
glguysyntax bind0 a b = a , b20/07 04:33
glguyinfixr 0 bind bind020/07 04:33
glguyWas what I tried20/07 04:33
glguyhurray, the MAlonzo compiled version of the regexp matcher is much faster20/07 04:46
copumpkinyay20/07 05:00
Eduard_Munteanuglguy: yeah, the first one looks fine to me. You could look in the release notes for .8 I think20/07 05:02
Eduard_MunteanuI'm not sure what you want with bind0 though20/07 05:04
Eduard_MunteanuMmm, faster than Epic?20/07 05:04
glguyfaster than normalizing the term in emacs20/07 05:06
glguyI've never tried Epic20/07 05:06
Eduard_MunteanuAh.20/07 05:12
glguyAm I doing "loop" correctly? All of the sharps seem kind of clunky http://www.galois.com/~emertens/DecSplits/TestCase.html20/07 05:30
augurhmm hmm20/07 05:44
* kfish minimizes skewness20/07 05:56
skewness:O20/07 05:56
* variants devours everything20/07 05:57
variantskfish: you use agda?20/07 06:00
kfishno i just sit near liyang20/07 06:01
kfishso it rubs off on me sometimes20/07 06:02
variantsit does have a tendency to do that20/07 06:02
copumpkinkfish: you like natto?20/07 06:20
auguri wish i could figure out how to make this code elegant :(20/07 06:21
copumpkinuse moar custom typez20/07 06:21
copumpkinis usually my answer20/07 06:21
augurcopumpkin: no its not that really20/07 06:21
copumpkina type for everything you can imagine20/07 06:21
augurits that in order to prove anything, i have to do lots of case analysis20/07 06:21
augurlike if i want to prove something about a binary relation20/07 06:21
augurwhere each argument to the relation could have, say, 3 constructors20/07 06:22
augurill need to do 9 cases20/07 06:22
augurmost of this problem is actually nastier than that even20/07 06:23
auguri think im doing something wrong, honestly20/07 06:27
auguri cant imagine that CT-relevant code is full of case analyses20/07 06:27
augureven tho im sure it could be done that way20/07 06:27
copumpkinyeah, most of the CT has no pattern matching at all20/07 06:28
augur:(20/07 06:28
copumpkinthe only thing I can think of is xplat's power category stuff20/07 06:28
copumpkinand the functor equality20/07 06:28
copumpkinwhich is a pain anyway20/07 06:28
augurcan i see your ct code?20/07 06:28
copumpkinit's all up on github20/07 06:28
augurto get a sense of how you avoid case analysis?20/07 06:28
copumpkinhttps://github.com/copumpkin/categories20/07 06:28
copumpkinoh, I'd just say that the domain requires less case analysis20/07 06:29
copumpkinit's not like I engineered it not to need it20/07 06:29
augur"Everything.agda" is about kan extensions...20/07 06:29
auguris this cheeky or what20/07 06:29
augurlol20/07 06:29
copumpkinand I'm sure if I went and constructed concrete categorical constructs I'd need it again20/07 06:29
augursure20/07 06:29
copumpkinoh no, Everything.agda contains everything!20/07 06:29
copumpkinwow20/07 06:29
copumpkinI got some nice alliteration going there20/07 06:29
copumpkinConstructed Concrete Categorical Constructs20/07 06:30
copumpkinalthough one of those word stems is duplicated20/07 06:30
auguri just mean, i imagine that there are ways that you COULD HAVE used case analysis a lot20/07 06:30
copumpkinnot really all that much20/07 06:30
augurhmm20/07 06:30
copumpkinI'm mostly stating equational properties20/07 06:30
copumpkinand doing equational reasoning20/07 06:30
copumpkindoesn't actually involve much pattern matching at all20/07 06:30
augurhmm20/07 06:30
copumpkinall I have are records everywhere20/07 06:30
copumpkinso no cases20/07 06:31
augurwell, im doing "biconditional" reasoning, i guess20/07 06:31
augurwhere the types are of differing complexity20/07 06:31
copumpkinclearly the best solution is for you to step back, and find out what categorical structure models your problem20/07 06:31
copumpkinthen construct a category, then reuse the general proofs I've already written :P20/07 06:31
augurand so many cases require that you whittle down one type or the other, eliminating the impossible inhabitants20/07 06:32
augurXP20/07 06:32
auguri wish i knew what categorical structure models the problem!20/07 06:32
augurunfortunately, i dont know how to even answer that question20/07 06:32
copumpkin:)20/07 06:33
copumpkinI'm just being silly20/07 06:34
augurright now its just showing that some binary relation is an induction principle20/07 06:34
copumpkinwho knows if one even exists20/07 06:34
augurthe same stuff ive been working on for a while now, actually20/07 06:34
copumpkinyeah20/07 06:34
augurcan i try to get your insight, actually? not from code, but from concept?20/07 06:34
copumpkinI'm pretty out of it right now, but sure, tomorrow?20/07 06:36
copumpkinwas just about to go to bed20/07 06:37
augurk20/07 06:38
xplatcopumpkin: after looking at your proof in derpa i annotated that paste with a slightly cleaner version20/07 13:32
xplatdirect ling at http://hpaste.org/4926120/07 13:32
xplat*link20/07 13:32
xplat⊥ only knows why Data.Nat.Properties only has one canceller each for + and *20/07 13:35
xplat(and they aren't even the same side)20/07 13:36
copumpkinxplat: the other * canceller is free20/07 14:34
xplathm.  the other + one isn't, though.20/07 15:01
xplatwait, how can cancel-*-left be free?20/07 15:02
copumpkinzero * x = zero20/07 15:02
copumpkinor is that not what cancel-*-left says?20/07 15:02
copumpkinI can't remember20/07 15:02
xplatno, that's a zero law, not a cancel law20/07 15:02
copumpkinoh, you're right20/07 15:02
xplatcancel-*-left says (would say) (suc i) * j == (suc i) * k -> j == k20/07 15:03
xplatplus appropriate arguments20/07 15:03
copumpkinokay, fair enough20/07 15:03
copumpkinI guess he only needed one side of it20/07 15:03
xplatit would be easy enough to use commutativity to add the opposite-side laws20/07 15:04
xplati just had a cool idea, btw20/07 15:04
copumpkinoh?20/07 15:04
xplatyou know how a syntax declaration can include a hidden lambda?20/07 15:05
xplatwhat if they could also have a hidden goal-reflection?20/07 15:05
copumpkinhmm :o20/07 15:05
copumpkinhow would that work?20/07 15:05
Saizanbtw, i'd just provide (p q : DivMod m n) -> p == q at this point20/07 15:06
copumpkinfair enough20/07 15:06
copumpkinanyway, time for work :) bbiab20/07 15:08
djahandarieWould there be a way to 'forget' the dependent stuff in a dependent eliminator to get back to a non-dependent eliminator? Like,    elimList : (P : List -> Set) -> (P nil) -> ((a : A) -> (l : List) -> P l -> P (cons a l)) -> (l : List) -> P l      =>     foldr : (B : Set) -> B -> (A -> B -> B) -> List -> B20/07 15:45
copumpkinnot a standardized function that magically forgets any such dependencies, I don't think20/07 15:45
copumpkinwell, you could probably write something that took some sort of type specifier20/07 15:46
SaizanelimList (\ _ -> B) is a start20/07 15:46
Saizanyou get para rather than cata that way20/07 15:46
djahandarieWhat's a paramorphism again?20/07 15:55
Saizanpara :: Functor f => (f (Mu f, a) -> a) -> Mu f -> a20/07 15:57
Saizanthe "algebra" gets bot the results of the recursive calls and the corresponding substructures20/07 15:57
Saizan*both20/07 15:57
Saizanpara f = snd . cata (\x -> (In (fmap fst x) , f x))20/07 16:01
djahandarieAh, got it20/07 16:01
kosmikusok, who understands coinduction in Agda properly?20/07 16:15
djahandarieI don't!20/07 16:15
kosmikus:)20/07 16:15
djahandarieI understand how to do it though20/07 16:15
kosmikusok, so here's a challenge: either get to termination-check or tell me why it's impossible to do:20/07 16:16
kosmikusimagine you have Streams20/07 16:16
kosmikusnow you have a type that's like a Rose tree, but infinitely branching20/07 16:16
kosmikusi.e., using streams instead of lists20/07 16:16
kosmikusnow implement map over such rose trees20/07 16:16
* Saizan tries20/07 16:17
djahandarieI don't see why you wouldn't be able to prove that's productive20/07 16:17
djahandarieI don't have Agda at work so I can't try. :p20/07 16:18
* djahandarie tries to do it in PHP20/07 16:18
copumpkinkosmikus: hmm, seems like it should be possible :P but probably you need to do some of that horrible interpreter shit20/07 16:20
kosmikuscopumpkin: horrible interpreter shit? link?20/07 16:21
copumpkinhmm, not sure where I saw it first20/07 16:21
copumpkinor at all20/07 16:21
copumpkinyou basically make a data type of your operations on codata, and an interpreter on that datatype20/07 16:21
copumpkinso then when corecursing you can "guard" it by the data constructor describing your operation20/07 16:22
copumpkininstead of a function20/07 16:22
kosmikuscopumpkin: ok20/07 16:22
kosmikussounds like a plan20/07 16:22
copumpkinbut maybe Saizan can come up with something else20/07 16:22
copumpkinactually it feels like it should be possible even without that20/07 16:22
copumpkinwhat are your definitions?20/07 16:23
Saizankosmikus: http://hpaste.org/4927220/07 16:24
copumpkinthe power of Saizan strikes once more20/07 16:24
djahandarielemma is just map on streams there isn't it?20/07 16:26
Saizanspecialized to map f20/07 16:26
djahandarieYeah20/07 16:26
Saizanthe termination checker doesn't like HOFs20/07 16:26
djahandarieThe current one doesn't? Isn't the current one the kind that just gets tired after awhile? :p20/07 16:28
kosmikusSaizan: nice, thanks20/07 16:28
Saizannp20/07 16:28
kosmikusso I didn't even think about the option not to reuse map on streams20/07 16:28
kosmikusso I guess if I'd want to reuse map on streams, there's no good solution?20/07 16:28
Saizanyou'd have to go the interpreter route as copumpkin was suggesting20/07 16:29
Saizanthere's a paper by NAD on this20/07 16:29
Saizandjahandarie: it doesn't even attempt such specializations afaiu20/07 16:30
djahandarieAh. Lame20/07 16:30
copumpkinSaizan: what if you turn up termination depth?20/07 16:37
copumpkinkosmikus: you can try turning termination depth to 5 or something :P20/07 16:37
copumpkinprobably 220/07 16:38
copumpkinI think that's supposed to help it "see through" stuff like that20/07 16:38
copumpkinbut maybe not20/07 16:38
kosmikuscopumpkin: how do I do that?20/07 16:38
copumpkin{-# OPTIONS --termination-depth=4 #-} iirc20/07 16:38
kosmikusok, thanks20/07 16:38
copumpkinI haven't played with that in a while20/07 16:38
kosmikuswill try20/07 16:38
kosmikusanyway, thanks for the help20/07 16:38
copumpkinit might just be for recursion20/07 16:39
copumpkinthings like f (suc (suc x)) = f (suc x)20/07 16:39
kosmikus(this isn't actually my real problem, so I need to backport the solution)20/07 16:39
copumpkinor does it already accept that?20/07 16:39
xplatcopumpkin: syntax quoteGoal g in solve-ring r g = because r says-so20/07 16:39
kosmikusinlining is going to be very inconvenient in the other case20/07 16:39
xplatwrt this morning's question20/07 16:39
copumpkinxplat: ah20/07 16:39
Saizanf (suc (suc x)) = f (suc x) is accepted by default20/07 16:39
copumpkinoh okay20/07 16:39
copumpkinI can't remember in what situations termination depth helps then20/07 16:40
copumpkin:P20/07 16:40
Saizan..i think20/07 16:40
copumpkinyeah20/07 16:40
djahandarieWow, we should convince alan jeffrey to help with the CT library. He seems to have rolled monoidal categories on his own multiple times in his projects from the looks of it20/07 16:42
djahandariehttps://github.com/agda/agda-web-semantic/tree/master/src/Web/Semantic/DL20/07 16:42
copumpkinodd that he uses data instead of record here: https://github.com/agda/agda-web-semantic/blob/master/src/Web/Semantic/DL/Signature.agda20/07 16:44
copumpkinbut yeah20/07 16:44
copumpkinhe's done a lot of neat stuff20/07 16:44
xplatthis seems like it's specialized or something though20/07 16:47
xplatyeah, the whole categorial structure doesn't live inside a record or anything because there's only one20/07 16:48
xplatalthough it's parameterized on a signature20/07 16:48
cayleecopumpkin et al: so where's your repo for this category theory development? I seem to have lost the link...*fail*20/07 16:50
copumpkingithub.com/copumpkin/categories :)20/07 16:50
copumpkinI welcome contributions!20/07 16:50
cayleecopumpkin: I might have time again after tomorrow...20/07 16:50
copumpkincool :)20/07 16:52
xplati wonder how hard it would be to hack that quoteGoal-as-syntax into darcs agda, and if it would really do what i wanted20/07 16:56
cayleewhat's quoteGoal (or what is it supposed to be)?20/07 16:57
copumpkincaylee: agda's fancier tactics20/07 16:58
cayleecopumpkin: huh, I don't think I'd heard of it before...then again I've been using agda off and on for only a couple of months20/07 16:58
cayleecopumpkin: should I expect the Everything file to load? It failed in Categories/Power file20/07 17:04
copumpkinhmm20/07 17:08
copumpkineverything should be working, but not sure20/07 17:08
copumpkinhow did it fail?20/07 17:08
copumpkinif mine doesn't work, xplat's branch might20/07 17:09
copumpkinespecially since he's the gatekeeper of Power20/07 17:09
cayleewow, Gatekeeper of Power is an impressive title...20/07 17:11
cayleeoh, but it fails on there being unsolved goals20/07 17:11
copumpkinhmm20/07 17:12
cayleecopumpkin: it was a unresolved shed for select' s field F-resp-\==20/07 17:14
copumpkinhmm, weird20/07 17:15
copumpkinI'm pretty sure that used to work20/07 17:15
copumpkinyou on agda head?20/07 17:15
cayleeah, no, the latest released version20/07 17:15
copumpkinhmm, I think xplat is too20/07 17:15
copumpkinnot sure, I'll take a look a bit later and see if I can see what's wrong20/07 17:16
copumpkinin the mean time, you might have more luck with xplat's branch of it20/07 17:16
copumpkinyou can just add a remote for https://github.com/xplat/categories.git20/07 17:16
copumpkinand pull from there20/07 17:17
cayleekk, thanks20/07 17:17
xplatif it's that shed, the actual answer should be in it anyway20/07 17:36
xplati counted on agda-mode's excessive saving too much :( and none of my changes since that one have been folded in20/07 17:37
xplatit's fixed in my fork though20/07 17:37
copumpkinI could've sworn I'd tested it before pushing20/07 17:37
copumpkinmaybe I was just in a rush/impatient20/07 17:38
copumpkincaylee: keep in mind that even when it does work Everything.agda will probably take you 10-20 minutes to typecheck :P20/07 17:38
xplaton a good day20/07 17:43
xplatone thing i'd like to do with the quoteGoal stuff ideally is have a syntax 'repurpose <equality> with <solver>' where it would use the solver to show that the lhs and rhs of the goal equal the lhs and rhs of the equality respectively, and trans the solutions on20/07 17:46
djahandarieNo, don't pull from xplat's fork, pull from my fork!20/07 17:48
djahandarieMine is the latest! Unless xplat did more, which he probably did20/07 17:48
djahandarieDownside of using mine is that you need to deal with my shitty code20/07 17:48
djahandarieI can't wait to try and do internal logic / theory stuff to see just how bad I suck20/07 17:50
cayleeso there's three authors and three competing forks? ;-)20/07 17:55
glguywith distributed development there is at least one fork per developer20/07 17:55
cayleeglguy: what's the maximum?20/07 17:56
copumpkin20/07 17:56
cayleecrap!20/07 17:56
djahandariecopumpkin should just pull everything back into his repo20/07 17:57
copumpkinI should20/07 17:57
cayleeah well, slides ain't gonna write themselves...so I should probably quit browsing this repo20/07 18:00
copumpkinoh yeah, the talk20/07 18:01
copumpkinor should I say, The Talk20/07 18:01
djahandarieOr, THE TALK20/07 18:01
* djahandarie is not sure what we're talking about20/07 18:01
cayleecopumpkin: heh...that'd be a great way to give it. When a Martin-L\"of type theory and a two-morphism love each other very much...20/07 18:02
copumpkinlol20/07 18:02
Saizantwo-morphism one theory?20/07 18:03
copumpkinoh god20/07 18:03
copumpkinI think I let my old domain, 2naturaltransformations1functor.com expire :(20/07 18:04
caylee...20/07 18:04
djahandarieHahahaha20/07 18:04
* copumpkin looks guilty20/07 18:04
Saizan..and someone else took it?20/07 18:04
copumpkinnot sure20/07 18:05
copumpkinmaybe it didn't expire20/07 18:05
djahandarieThat is one high value domain20/07 18:05
copumpkinyeah20/07 18:05
* copumpkin was trying to think of a shocking video to put on it20/07 18:05
copumpkinI was thinking of putting eugenia cheng with the 2 girls 1 cup music in the background20/07 18:05
* glguy wonders if OS X Lion will break GHC20/07 18:05
copumpkinher talk on monads, that is20/07 18:05
copumpkinglguy: it already has20/07 18:05
copumpkinbut I think it's close to being unbroken20/07 18:06
glguyDo you have a reference?20/07 18:06
copumpkintalk to dankna, he's been working on it for a while now20/07 18:06
copumpkinI think he also sends out the occaisonal email about it to the cvs-ghc list20/07 18:06
Eduard_MunteanuIt kinda sucks when people use Git like CVS.20/07 18:24
Eduard_Munteanue.g. everybody's a commiter20/07 18:24
Eduard_MunteanuWell the rationale would be that CVS (and generally non-DVCSes) suck :)20/07 18:25
cayleeEduard_Munteanu: my research group kinda uses git like that...20/07 18:26
augurwargle20/07 18:33
Eduard_Munteanuwhargarrbl?20/07 18:34
augurno20/07 18:35
augurso copumpkin :x20/07 18:35
jlouiscaylee: I feel for you20/07 18:37
jlouisAnd I should hack more Agda!20/07 18:38
jlouisI am lost in a maze of twisted little Erlang processes, all alike20/07 18:38
augurpigworker: could the syntax keyword work for matching on nil ~ < ff , <> >  etc in the way you want ??20/07 19:16
pigworkeraugur: I don't know, but I now wish I did.20/07 20:14
augurpigworker: i was reading an agda website and the author wrote that defining types as combinations of sets is ugly for writing things out but syntax declarations can clean that up20/07 20:20
xplatsyntax isn't powerful enough, it can only change the size of expressions by at most a constant multiplier depending which symbols appear20/07 20:21
xplatwell, maybe it could be powerful enough for some things, but it doesn't replace the extension pigworker proposed earlier, i should say20/07 20:22
xplatbut maybe that was a case of asking for more than needed20/07 20:22
augurhow do i turn off the positivity checker again?20/07 20:25
auguraha!20/07 20:29
augurhmm20/07 20:32
augurit seems you cant use syntax for this because nil has to my polymorphic20/07 20:33
xplatgahh, how can i construct a Name?20/07 20:40
Eduard_Munteanuaugur: it's a parameter to the agda executable20/07 20:49
Eduard_Munteanuaugur: presumably just like with universe polymorphism, OPTIONS pragma20/07 20:50
augurEduard_Munteanu: no i got it :)20/07 20:50
xplatmore importantly, my question :)20/07 20:58
augurwhats a name!20/07 20:59
xplatName in Reflection.agda20/07 21:01
copumpkinI don't think you do20/07 21:01
copumpkinI thought you only got those when quoteGoal passes them to you20/07 21:01
auguri dont really get reflection20/07 21:02
Saizanthere's another quote primitive that gives you the name of the identifier you pass it20/07 21:02
Saizanlike ' in TH20/07 21:03
xplatah20/07 21:03
copumpkinah, neat20/07 21:03
xplati wonder if it still quotes 1 as unknown20/07 21:03
xplatthat seems like a bad idea20/07 21:03
xplati mean, 1 is a proper value with a constructor20/07 21:03
xplatugh, it does20/07 21:05
xplatwhat were they thinking?  tactics care about values20/07 21:06
copumpkinyou should look at how the presburger solver does it20/07 21:07
copumpkinit seems like it would need to care20/07 21:07
augurso copumpkin20/07 21:08
copumpkinyep20/07 21:08
augurcan i get your insights? :X20/07 21:08
xplatwait, i was wrong, it does work, i mixed up which arg was which :(20/07 21:09
xplator should that be :)20/07 21:09
copumpkinaugur: well, it's easier (and less put-on-the-spotty) to just ask the channel, and if I have time/insight, I'll respond :P or if not, I'll say no :P but sure, you can ask away. But I'm also doing other stuff20/07 21:10
augurwell yes, ofcourse :p20/07 21:10
copumpkin:)20/07 21:10
augurok so basically im trying to figure out how to reason about binary relations over positions in binary trees20/07 21:10
augurthe key relation im working on is called c-command, but really its just something like over one, then down any number of times20/07 21:12
copumpkinbinary relations over positions in binary trees?20/07 21:12
copumpkin can you expand on that?20/07 21:12
auguryeah20/07 21:12
augurso if you have the tree   branch leaf leaf20/07 21:12
copumpkinyep20/07 21:12
augurthe left leaf might be the position   left here20/07 21:13
copumpkinok20/07 21:13
augurthe right leaf would be    right here20/07 21:13
copumpkinso a position in a binary tree is a list of some 2-element set20/07 21:13
augurand you might have the relation sisters which holds of   sisters (left here) (right here)20/07 21:13
copumpkinis the binary tree balanced?20/07 21:13
augurbut its false that   sisters here here   or anything else in that tree20/07 21:13
augureh, well, a position is just the nodes in context20/07 21:13
augurso the left daughter and right daughter are distinct positions in (branch leaf leaf)20/07 21:14
augureven tho    left-daughter (branch leaf leaf) == right-daughter (branch leaf leaf) == leaf20/07 21:14
copumpkinso what does your position type look like?20/07 21:14
augurdata TreeIndex : Tree -> Set wherehere : {t : Tree} -> TreeIndex t ;20/07 21:15
augurwhoops20/07 21:15
augurdata TreeIndex : Tree -> Set where20/07 21:15
augurhere : {t : Tree} -> TreeIndex t20/07 21:15
augurleft : {l r : Tree} -> TreeIndex l -> TreeIndex (branch l r)20/07 21:15
augurright : {l r : Tree} -> TreeIndex r -> TreeIndex (branch l r)20/07 21:15
copumpkinokay, so a fancy list of booleans :)20/07 21:16
augursort of!20/07 21:16
copumpkinthat's about how I'd approach it, I think20/07 21:16
augurTree is just the type of tree structures, rather than proper trees with data20/07 21:17
copumpkinso your relations are TreeIndex t -> TreeIndex t -> Set20/07 21:17
augurso TreeIndex ~ Tree as Fin ~ Vec20/07 21:17
augurwell, more, TreeIndex ~ RealTrees as Fin ~ Vec20/07 21:17
copumpkinyeah20/07 21:17
copumpkinokay20/07 21:17
augurwhere Tree ~ Nat because neither are ornamented with data20/07 21:17
auguryeah so relations are precisely that20/07 21:18
copumpkinso what kinds of relations?20/07 21:18
copumpkindo you represent them as datatypes too?20/07 21:18
augurwell, so i know that c-command can be20/07 21:18
copumpkinwell, I'm just wondering if you represent your relations as nice friendly inductive families that refine indices too20/07 21:20
copumpkinor as crazy sigmas and such20/07 21:20
copumpkin:)20/07 21:20
djahandarieCrazy!20/07 21:21
augurdata CCommand : (t : Tree) → (x y : TreeIndex t) → Set where20/07 21:21
augur  cc-ze-lr : {l r : Tree} → CCommand (branch l r) (left here) (right here)20/07 21:21
augur  cc-ze-rl : {l r : Tree} → CCommand (branch l r) (right here) (left here)20/07 21:21
augur  cc-su : {t : Tree} {x y z : TreeIndex t} → CCommand t x y → y < z → CCommand t x z20/07 21:21
copumpkina less-than relation20/07 21:22
copumpkin:o20/07 21:22
copumpkinon tree indices?20/07 21:22
augurwell, sort of20/07 21:22
augur:P20/07 21:22
augur_<_ is parent node20/07 21:22
xplatit should really be curly <20/07 21:22
copumpkindirect parent?20/07 21:22
auguryeah20/07 21:22
copumpkinaugur: then you could avoid that20/07 21:22
copumpkinand put it into the index?20/07 21:23
augurmaybe!20/07 21:23
augurxplat: \<?20/07 21:23
augurno20/07 21:23
copumpkin20/07 21:23
copumpkin\<~20/07 21:24
copumpkinmaybe?20/07 21:24
auguroh, i thought he meant the one with bendy sides20/07 21:24
auguranyway, maybe i can indeed index that, copumpkin20/07 21:24
augurim not sure how20/07 21:24
copumpkinso what is the definition of _<_ now20/07 21:25
copumpkin?20/07 21:25
copumpkinyou have parent on the left and parent on the right?20/07 21:25
augurdata _<_ : {t : Tree} -> TreeIndex t -> TreeIndex t -> Set where20/07 21:27
augur<-ze-l : {l r : Tree} {x : TreeIndex l} -> _<_ {branch l r} here (left here)20/07 21:27
augur<-ze-r : {l r : Tree} {x : TreeIndex r} -> _<_ {branch l r} here (right here)20/07 21:27
augur<-su-l : {l r : Tree} {x y : TreeIndex l} -> _<_ {branch l r} (left x) (left y)20/07 21:27
augur<-su-r : {l r : Tree} {x y : TreeIndex r} -> _<_ {branch l r} (right x) (right y)20/07 21:27
copumpkinack20/07 21:27
auguri should paste these probably lol20/07 21:27
copumpkinyeah, can you just put this handful of types into a file?20/07 21:28
augur:P20/07 21:28
copumpkinI'd like to play with just that subset of the whole thing :P20/07 21:28
augurhttp://hpaste.org/4928320/07 21:30
copumpkinoh so it isn't just direct parenthood20/07 21:30
copumpkinit's ancestor?20/07 21:30
augurno its direct20/07 21:30
copumpkinbut those su constructors20/07 21:31
augurits just that you have to inject indices for subtrees into the higher trees20/07 21:31
copumpkinhmm20/07 21:31
augurso if x y : TreeIndex l20/07 21:31
augurthen surely left x, left y : TreeIndex (branch l r)20/07 21:31
augursince TreeIndex (branch l r) ~ 1 + l + y20/07 21:32
augur.. 1 + l + r20/07 21:32
copumpkinyeah20/07 21:32
augurso you just have to inject the l indices and the r indices20/07 21:32
copumpkinhmm20/07 21:33
copumpkinI have a feeling that type can be simpler, but I need to think about it some more, and need to do some actual work now20/07 21:33
copumpkinwill hmm some more in a couple of hours or so20/07 21:33
augurive annotated with the ancestor type20/07 21:33
auguror one of them, anyway20/07 21:33
copumpkinoh ok20/07 21:34
augurthe one that gets you from a node to its daughters20/07 21:34
copumpkindata _≤′_ (m : ℕ) : ℕ → Set where20/07 21:35
copumpkin  ≤′-refl :                         m ≤′ m20/07 21:35
copumpkin  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n20/07 21:35
copumpkindata _≤_ : Rel ℕ Level.zero where20/07 21:35
copumpkin  z≤n : ∀ {n}                 → zero  ≤ n20/07 21:35
copumpkin  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n20/07 21:35
copumpkinsame relation, different approaches20/07 21:35
augurcertainly.20/07 21:35
copumpkinI feel like you're currently taking the latter approach20/07 21:35
copumpkinthat ends up being more complicated than the former in your case20/07 21:35
augurok ill try the former20/07 21:35
augurbut my real concern is this:20/07 21:35
copumpkinsince I think you can get away without making your direct parenthood recursive at all20/07 21:35
augurccommand is an induction principle.20/07 21:35
auguri can prove this if i have ccommand defined.20/07 21:36
auguri'd like to construct it from some sort of refinement, tho20/07 21:36
copumpkinhmm20/07 21:36
copumpkinI still need to ruminate on what ccommand means first :)20/07 21:36
copumpkingimme a bit20/07 21:37
augurover-then-down-if-you-like20/07 21:37
auguror in family-tree-terms, your (great^n)-aunt c-commands you20/07 21:37
augur"sibling's descendants"20/07 21:37
augurwhatever20/07 21:37
auguri can give you the induction principle's arguments if you like.20/07 21:39
augurthe leaf case is easy enough, the branch case is more complicated.20/07 21:39
augurbut my real concern is not with showing this holds, etc. my concern is with figuring out a nice way of doing the refinement without five billion case analyses, without ugliness, etc.20/07 21:41
copumpkinyeah20/07 21:41
copumpkinI can definitely see where this would get unpleasant :)20/07 21:41
augurmost of the case analysis isnt even where you think it is20/07 21:45
augurthe propositional definition of ccommand is like so:   prop-cc t x y = not (x == y) * not (x < y) * not (y < x) * (exists z : TreeIndex t . z < x * z <+ y)20/07 21:47
augurthe first three conjuncts just enforce the over part of over-then-downifyoulike20/07 21:47
augurwell, sort of20/07 21:48
augurthe first three prevent you from c-commanding vertically20/07 21:48
augurthe last conjunct enforces that the common ancestor is x's parent20/07 21:49
augurthe case analysis is in whittling down prop-cc t x y for the different values of x and y20/07 21:49
augureg   prop-cc t here y   and   prop-cc t x here   are uninhabited20/07 21:50
augurand often is the interaction of the different conjuncts that results in uninhabitedness20/07 21:53
augurpumpkin: :O20/07 21:55
pumpkinsorry20/07 22:01
augurwhered i leave off?20/07 22:02
copumpkin[04:53:00 PM] <augur> and often is the interaction of the different conjuncts that results in uninhabitedness20/07 22:03
auguroh ok20/07 22:03
augurthat was the last thing i said :D20/07 22:03
augurbut yeah, so the case analysis is because the propositional definition is a big conjunction :\20/07 22:07
augurahaha pumpkin :)20/07 22:10
augurfor someone who works a corporate job, your internet sucks :)20/07 22:14
copumpkinI'm stealing apple wifi20/07 22:14
copumpkintheir wifi sucks20/07 22:14
augur:)20/07 22:23
augurwhy are you stealing apple wifi? dont you have your own?20/07 22:23
auguryou hippy, stop stealing the wifi of hard working americans!20/07 22:23
Saizansoo, as anyone proved evaluating an ST action won't get stuck somehow by using using parametricity?20/07 22:24
copumpkinaugur: no wifi at my office! the horror20/07 22:26
augurcopumpkin: thats lame20/07 22:27
xplatokay, first real limitation of reflection: it doesn't know anything about the environment (free variables) :(20/07 22:29
xplatyou get stuff like 'var 2' but you don't know what those indices refer to20/07 22:30
xplatyou also can't figure out the type associated with a name (never mind a variable)20/07 22:33
xplatand you can't evaluate a term20/07 22:33
xplatand if you try to arrange your variables by doing something like '(quoteGoal g in ?) x y z' the whole thing turns yellow and the ? isn't even active20/07 22:39
augurare relation combinators defined in the standard library?20/07 22:57
augurlike relation composition, etc.20/07 22:57
augur?20/07 22:57
Saizanthere's something in Relation.Binary, like union and intersection20/07 22:59
augurok20/07 22:59
--- Day changed Thu Jul 21 2011
augurok peeps21/07 01:25
augurheres a serious question21/07 01:25
augur(cause none of my other questions are seriously, right? :P)21/07 01:26
augurif i have a type F : (X -> Y) -> Set21/07 01:26
augurand i have a : F f21/07 01:26
augurhow can i use a to fill an F f hole?21/07 01:26
augurbecause currently its not working21/07 01:26
xplatwhy is agda giving me incomplete pattern matching that doesn't show up until i try to normalize something?21/07 01:49
xplathow does that even work?21/07 01:50
xplatalso, when you can't prove your stuff works in agda, it is very hard to debug ...21/07 01:50
xplati'm trying to create a nice reflective frontend for the ring solver, but i can't get the expression-reparser thingy to turn a thingy into a thingy of another kind working21/07 01:51
copumpkinxplat: :(21/07 01:56
copumpkinaugur: I see why this gets complicated, been playing with it for a bit21/07 01:57
augurcopumpkin: :)21/07 01:57
augurcopumpkin: im working on proving that derivationality is a conserved property21/07 01:57
auguri figure that'll make the proofs easier, to some degree21/07 01:57
augurbecause if i can show that Derivational P * Derivational Q -> Derivation (P * Q) then that will eliminate a lot of case analysis i think21/07 01:59
augurcopumpkin: can you help me figure this out tho? i have a goal that's like... F (f x)21/07 02:00
augurwhere f x is unknown21/07 02:00
augurand i have a witness for it21/07 02:01
augurbut i cant seem to get that to refine21/07 02:01
auguroh wait maybe i DONT have a witness for it21/07 02:01
augurhmm21/07 02:01
augurso copumpkin what did you do?21/07 02:04
copumpkinjust a sec, playing with an alternate representation21/07 02:04
augur:)21/07 02:08
auguraddictive isnt it!21/07 02:09
copumpkinyep! but I also have some things I actually need to do tonight21/07 02:09
copumpkinso I'm gonna have to stop in a few21/07 02:09
augur:p21/07 02:09
augursokay21/07 02:09
auguryou didnt have to do what youve done!21/07 02:09
augur<321/07 02:09
copumpkinokay, I failed :P21/07 02:14
copumpkingonna make some food21/07 02:14
copumpkinthen do the other stuff I need to do21/07 02:14
augurhaha21/07 02:14
augurfailed at?21/07 02:14
copumpkintrying to simplify the tree path stuff21/07 02:14
auguro21/07 02:15
augurhow were you trying to do that?21/07 02:15
copumpkinbasically state you are the child of your parent directly21/07 02:16
copumpkinrather than needing a recursive case21/07 02:16
auguri dont follow21/07 02:17
augurthe fact that theres _on_ and _-[_]-_ but nothing in between is weird to me21/07 03:20
augurwhy no \ f g _*_ x -> f x * g x ?21/07 03:21
augurits very sad.21/07 03:21
glguySpeaking of the Function module, why is it that "const x = λ _ → x"21/07 03:26
lambdabotglguy: You have 1 new message. '/msg lambdabot @messages' to read it.21/07 03:26
glguyIs there some special reason to use a lambda there?21/07 03:26
augurcopumpkin: hm21/07 06:19
augurso im trying to define the property of being an induction principle over trees21/07 06:19
augurand i end up using a biconditional for this21/07 06:20
augurdo you think this is appropriate?21/07 06:20
augurlike, will that fail for relation-valued inductive properties?21/07 06:21
copumpkinhmm, not sure21/07 06:29
copumpkinisn't the type of the induction principle sufficient? which should have only one inhabitant?21/07 06:30
augurer well, i mean something definable in terms of treeind21/07 06:30
augurso like21/07 06:31
augurf = treeind P z f21/07 06:31
dolioOf what?21/07 06:31
glguyThere are sure many "induction principles" which are interesting for each type21/07 06:32
augurdolio: ??21/07 06:33
augurer, that should be g = treeind P z f lol21/07 06:33
augurits not self referental sorry21/07 06:33
augurtreeind -- the tree induction combination21/07 06:33
augur.. combinator21/07 06:33
augurdamn fingers21/07 06:33
augurtreeind : (P : Tree -> Set) -> P leaf -> ((l r : Tree) -> P l -> P r -> P (branch l r)) -> (t : Tree) -> P t21/07 06:34
auguroh for fucks sake i hate this level crap >_<21/07 06:53
augurthis is bullshit21/07 06:56
augurit says i need something of such and such a type21/07 06:56
augurand it lets me refine with a value21/07 06:56
augurbut if i type check after i refine, it gives me a type error21/07 06:56
augurwhat the hell is this21/07 06:56
augurit shouldnt be able to refine if its going to give me a type error!21/07 06:57
augurand somehow i can restrict the type in other ways21/07 06:57
augurso that the candidate for the goal demonstrably has _exactly_ the type of the goal21/07 06:58
augurand then it refuses to refine21/07 06:58
glguyFor module imports which are not used in the top-most module declaration of a file, does it matter if I put them above or below the module declaration for anything other than style21/07 07:28
augurcopumpkin! solve all my problems for me!21/07 08:00
augur:X21/07 08:00
auguralso, copumpkin, regarding lambek's lemma: why dont you email him?21/07 08:03
auguralso also, whats this about stratifying shapes/indexes?21/07 08:05
xplatglguy: in that case it's just a matter of style, yeah21/07 12:09
xplatunless you, say, open them publicly or something, in which case they must be below21/07 12:09
xplatargh, i still can't believe i can get an 'incomplete pattern match' during normalization21/07 12:15
xplatand on top of that, the line number for the error is the original caller, not anywhere more relevant21/07 12:15
xplatit'd be nice to know at least what function it was in21/07 12:16
xplatgah, i found the problem21/07 16:26
xplati noticed earlier some of the constructors were being printed with a list of Term arguments instead of Arg Term arguments21/07 16:27
xplati thought that was a problem with printing, but it's not21/07 16:27
xplatthe arguments are actually the wrong type in the actual terms21/07 16:27
xplatso pattern matching on quoted constructors fails if they have arguments21/07 16:27
xplatand agda doesn't notice until runtime because, by the types, it should work21/07 16:28
xplatnot only that, but agda will not allow matching on the constructors that appear at runtime, since they don't fit the type21/07 16:29
xplatthis makes the entire project impossible, at least for 2.2.1021/07 16:29
xplatwell, i guess i could try doing something really gross like using primTrustMe equality on types somehow to cast the argument to the type it actually has21/07 16:32
xplatnot sure if that would work though21/07 16:32
copumpkin:o21/07 16:35
copumpkinthe entire project impossible?21/07 16:35
copumpkinyou mean to make a reflection-based semiring solver?21/07 16:35
xplatto make anything that can differentiate natural numbers in reflected terms, to be precise21/07 16:48
xplatbecause distinguishing natural numbers requires looking at arguments of suc21/07 16:49
xplatand suc is a constructor21/07 16:49
xplathm, trustMe only works for sets21/07 16:54
xplatso no trusting equality for types, no magic cast21/07 16:55
xplatis there any evil way to typecast things unsafely in agda?  anyone know?21/07 16:55
copumpkinpostulate a conversion?21/07 16:59
copumpkinit won't reduce though21/07 16:59
xplati thought of that, but it must reduce21/07 17:03
xplatif it doesn't reduce, i can't analyze the contents21/07 17:05
copumpkinoh21/07 17:05
copumpkinhave you looked at how the presburger solver does it?21/07 17:05
copumpkinit needs to look at constructors too21/07 17:05
xplati mean, the problem is that terms are being marked with an incorrect type21/07 17:05
copumpkinoh21/07 17:06
xplator actually you could say the type is right and the terms are wrong21/07 17:07
xplateither way they don't match21/07 17:07
xplatthus getting 'incomplete pattern matching' during normalization that isn't caught at compile time21/07 17:07
xplator load time anyway21/07 17:08
copumpkin:o21/07 17:08
xplatthe presburger solver itself doesn't seem to use reflection, and the associated propositional logic solver doesn't examine constructors21/07 17:10
copumpkinoh21/07 17:10
xplatreally, this goes to show how much people actually try to use reflection if this bug hit a release21/07 17:12
copumpkin:)21/07 17:12
copumpkinI don't think anyone thought anyone used it :P21/07 17:12
Saizanyeah, i don't think anyone considers it fully implemented either :)21/07 17:14
copumpkinomg hac phi!21/07 17:14
Saizan(though i guess believers are good for finding bugs)21/07 17:14
copumpkinI wouldn't mind working on that actually, assuming it's actually possible to understand how it works21/07 17:14
Saizani think you might get some pointers if you ask on the mailing list21/07 17:16
augurblargh21/07 18:39
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda21/07 18:43
augurwhat the hell do i need to do to make IsInductionPrinciple typecheck? :(21/07 18:44
augurit _should_ be    F t <-> treeind P z f t    but that refuses to check :\21/07 18:44
copumpkinI'd use a record, not a bunch of nested sigmas. It'll be faster and easier to manage21/07 18:45
copumpkinI don't know the actual answer to your question though21/07 18:45
augurok21/07 18:46
augurwtf21/07 18:51
augurthis makes no senssss :(21/07 18:53
augurcopumpkin: now im getting some absurd result21/07 18:54
augurthanks to your records >|21/07 18:54
augur /as usual/21/07 18:54
copumpkinlol21/07 18:55
augurthe record's proof field is supposed to be (t : Tree) -> F t -> treein P baseCase recursiveCase t21/07 18:55
augurbut instead its kicking up /four/ arguments for treeind21/07 18:56
augurthe first of which is a set? whats _that_21/07 18:56
augurwhere is that coming from21/07 18:56
auguri C-c C-a's and it filled with P t21/07 18:57
augurno parens21/07 18:57
augurwhich ofcourse failed21/07 18:57
auguri added parens21/07 18:57
augurand it tells me that Set l !=< Tree -> Set l21/07 18:57
augurwhats going on! T_T21/07 18:57
copumpkinxplat: did you upgrade agda?21/07 19:43
xplatcopumpkin: still at 2.2.10, maybe i'll try it21/07 20:13
xplatcopumpkin: can you try an experiment for me?21/07 20:13
xplatopen a file, put in a header and 'open import Reflection ; test : 1 == 2 ; test = quoteGoal t in {! t !}' and then load it and normalize in the hole21/07 20:15
xplatthen paste me one of the lines with suc on it21/07 20:15
copumpkinsure, just a sec21/07 20:15
copumpkinhttp://hpaste.org/4932521/07 20:17
copumpkinis that what you meant?21/07 20:17
xplatthe type of con still doesn't match the type of its actual subterms in your version :(21/07 20:20
copumpkinbug report?21/07 20:21
Saizanhah, it's con : Name -> List Term -> Term rather than Name -> List (Arg Term) -> Term21/07 20:23
xplathm, i don't think i have an active google account21/07 20:24
copumpkinif you give me something to write in there I can post it, or you could just sign up for a google account :)21/07 20:24
xplatSaizan: yep21/07 20:24
copumpkinnot sure which would be easier21/07 20:24
copumpkinoh, I see the problem21/07 20:25
copumpkinweird21/07 20:25
xplattitle 'reflection: con terms do not match type of con', quote the definition of con from Reflection.agda, link your paste, and say, er, something appropriate21/07 20:26
xplatmention that i tested pattern matching on the list elements and found the wrong type is not an artifact of printing21/07 20:27
xplathm, ffi won't work either since ffi functions act like postulates at compile time21/07 20:34
copumpkinhttp://code.google.com/p/agda/issues/detail?id=42821/07 20:34
xplatlooks great, thanks21/07 20:35
* xplat downloads a metric assload of papers about agda, macros, etc21/07 21:19
cayleesorry, what is that in American measurements?21/07 21:20
pumpkin:O21/07 21:20
cayleeerr...so what does the "." before a declaration mean? Hidden? ...wait, irrelevant somehow?21/07 21:22
pumpkinyep21/07 21:23
cayleepumpkin: is it just used the manage the size of things?21/07 21:24
pumpkinit also affects what you can prove with them21/07 21:24
cayleeright, in that once something is irrelevant one can't exactly case on its construction?21/07 21:25
xplatxplat: it's approximately 0.823 fucktons21/07 21:25
xplatcaylee:21/07 21:25
cayleexplat: good to know!21/07 21:26
xplatany two irrelevant closed terms of the same type are considered to be equal21/07 21:29
cayleeright21/07 21:29
xplatwhich can cause problems in implicit inference when eta is too eagerly applied unfortunately >:I21/07 21:30
Saizannot open ones too?21/07 21:30
xplatSaizan: i'm a little fuzzy on the details, but i think there are some restrictions with that to keep open terms from being witnesses outside their context21/07 21:31
cayleexplat: is there a place where this is written down?21/07 21:33
xplati don't know of a place where it's all down in detail21/07 21:34
cayleekk21/07 21:34
xplatsome of it is in the agda source code, some in mailing list threads, etc21/07 21:34
cayleexplat & copumpkin: so what things are ya'll still working on in the categories library?21/07 21:36
copumpkinI've taken a break recently21/07 21:37
copumpkinhad other shiny things steal my attention21/07 21:37
copumpkinbut will probably resume in a bit21/07 21:37
xplatwell, there's still a lot to do in monoidal categories, higher categories, and the like.  but i haven't been working on it in the past couple of weeks21/07 21:38
copumpkinI'd like to get all the monoidal stuff all the way up to CCCs21/07 21:38
copumpkinhigher categories would be nicer if we had a setoid on objects21/07 21:38
djahandarieSymmetric should be fairly trivial21/07 21:38
copumpkinbut that'd be a massive change21/07 21:38
copumpkinxplat: right?21/07 21:38
xplati was doing strict 2-categories and it was going pretty well, except for the ram consumption21/07 21:38
xplatthen my plan to limit ram consumption kind of didn't work21/07 21:39
djahandarieI'm not sure what additional laws you need if you're getting to CCC from symmetric by adding X -> X x X and X -> I though21/07 21:39
xplatbecause of the aforementioned problems with irrelevance/eta21/07 21:39
xplatcopumpkin: yeah, and i think the extra fields/laws/whatever would make the ram usage hurt even more21/07 21:40
copumpkinyeah :/21/07 21:40
djahandarieHm, for symmetric, you really only need one of the hexagons, how would be the best way to tell Agda that it can ignore the second proof in the braided module?21/07 21:40
djahandarieI imagine I'd need a proof proving the two proofs equiv21/07 21:41
xplati've been pondering an approach to HDA via FOLDS, maybe FOLDS with setoid models would be more reasonable by reducing the number of entities21/07 21:41
xplatdjahandarie: they're irrelevant, so they are already equivalent :)21/07 21:42
djahandarieThey aren't the same type.21/07 21:42
xplatdjahandarie: i mean the second hexagon and the version of it you get by flipping the first hexagon21/07 21:42
djahandarieRight21/07 21:42
xplatif you couldn't get a proof of the same type, you couldn't safely ignore one to begin with21/07 21:43
djahandarieYou need to actually use gamma_b,a o gamma_a,b = id /somewhere/ though, and I imagine it's when you're proving the flipped first hexagon is the same as the second21/07 21:44
djahandarieEr21/07 21:45
djahandarieWhatever21/07 21:46
djahandarie:p21/07 21:46
* djahandarie will hack on it later and see the solution then21/07 21:46
bxcis there a Show/print like way of putting things to stdout in agda?21/07 22:05
Saizanthere's putStrLn and you might write your show, though there's also C-c C-n in the emacs mode21/07 22:09
bxcright, but say i have a list of things - the show side of that I have to code the show for list and my custom type? (not that its terribly hard, presumably)21/07 22:10
Saizani think so21/07 22:11
xplatunfortunately the current implementation of reflection, even were it not buggy, is not nearly powerful enough to derive show automatically21/07 22:13
xplatso if you want to show some random terms, it's much easier to do it in emacs21/07 22:13
bxcright21/07 22:14
bxcthough i do have some interest in code running under linux os, not emacs os...21/07 22:14
bxci just don't remember from last time i touched agda what infrastructure there is and what there is not21/07 22:15
bxci only manage to get brainpower for agda between jobs...21/07 22:16
Saizanit might be worth to push these values through the haskell FFI and do the printing there21/07 22:21
glguyhttp://www.galois.com/~emertens/DecSplits/TestCase.html21/07 22:37
glguyThis is how I did printing of my custom type through IO21/07 22:37
* glguy doesn't know of a way to get a "Show" instance-like21/07 22:39
bxcmanual is fine for now21/07 22:40
bxci'm not doing very fancy output21/07 22:40
augurcan anyone suggest a way to resolve { }0 in https://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda on line 77?21/07 22:42
auguri believe i'd need some sort of proof that (X * Y)^2 -> Set ~ X^2 * Y^2 -> Set21/07 22:43
augurbut im not sure21/07 22:43
auguri mean, the goal is to show basically that if binary relations P and Q are definable in terms of induction principles, the so is P&Q21/07 22:54
augurwhich seems obvious but i cant figure out how to do it21/07 22:54
glguyaugur: That's basically what is proven in Induction.Lexicographic21/07 22:55
auguris it now21/07 22:55
augurmm21/07 22:57
augurbut this seems to be inductively defined predicates, not inductively defined relations21/07 22:57
augurhmm but relations are tuple predicates21/07 22:59
augurglguy: i dont really follow whats going on here21/07 23:02
glguyaugur: I don't really know what you are doing, I just know I've used that module :)21/07 23:10
auguryeah no i know21/07 23:10
augurcan you help me understand it tho?21/07 23:10
augurim looking at Induction.Nat trying to understand how these things work21/07 23:10
augurwhat they do, etc.21/07 23:10
glguyhttp://www.galois.com/~emertens/DecSplits/RegExp.html#313321/07 23:13
glguyI use lexicographic induction in this function21/07 23:13
glguyif you need an example21/07 23:13
copumpkinRecursorBuilder makes me feel like I'm in javaland21/07 23:13
copumpkinshould call it a Factory21/07 23:13
augurglguy: %_%21/07 23:14
augurcopumpkin: do _you_ know how this works?21/07 23:14
copumpkinI haven't worked with the lexicographic indcution, but I've played with the usual one21/07 23:14
auguri dont know what lexicographic induction is :(21/07 23:15
auguri get the sense that its induction form smaller domains to larger domains??21/07 23:16
augurif so, im not sure that'll work for induction principles over trees, since you need to go from two subtrees to the whole tree21/07 23:17
glguylexicographic recursion says that your recursive call must either be on a smaller first argument21/07 23:17
glguyor if the first argument stays the same a smaller second argument21/07 23:18
glguyin the first case you can use an arbitrarily large second argument21/07 23:18
augurim not sure i understand21/07 23:19
augurfirst argument?? to what?21/07 23:19
augurglguy: lemme clarify first. can i in principle use the induction module for tree induction?21/07 23:21
glguyYou can use it for induction on arbitrary types. You define the structure of the recursion first21/07 23:22
glguyMy regular expression type is a tree21/07 23:22
glguyhttp://www.galois.com/~emertens/DecSplits/RegExp.html#168021/07 23:22
glguysee RegExpRec21/07 23:22
auguri dont really understand what this means21/07 23:23
glguyhttp://www.galois.com/~emertens/DecSplits/Induction.List.html#121/07 23:23
glguyprovides another example21/07 23:23
glguyRegExpRec P (r₁ ⊙ r₂) = P r₁ × P r₂21/07 23:24
glguyMeans that I will be proving that P (r₁ ⊙ r₂)  holds given  P r₁ × P r₂21/07 23:24
augurhmm21/07 23:26
glguyso for your tree you would show that P (Node a b c) holds given P a, Pb P c21/07 23:26
auguris there a paper where this is discussed? someone mustve written something given that this is in the standard library21/07 23:26
glguyLook in the "Induction" module21/07 23:27
glguyit mentioned who created that, and I believe he wrote a paper21/07 23:27
auguroh, the mcbride and mckinna paper21/07 23:27
glguy-- The idea underlying Induction.* comes from Epigram 1, see Section 421/07 23:27
glguy-- of "The view from the left" by McBride and McKinna.21/07 23:27
augurok ill read this :)21/07 23:27
auguri mean, im in the process of reading VftL as it is so21/07 23:27
augurhooray justification!21/07 23:27
glguyWhy are your trees indexed by trees? Why not by an arbitrary set?21/07 23:35
glguyis the tree structure of the index significant?21/07 23:35
augurtheyre not indexed by  trees21/07 23:35
glguydata TreeIndex : Tree → Set where21/07 23:35
auguryes21/07 23:35
augurthats not a tree indexed by a tree21/07 23:35
glguyah, it doesn't have a node constructor21/07 23:36
augurits a tree index indexed by the (abstract structure of) the tree it indexes into21/07 23:36
augurin the same way fin is a vec index that is indexed by the (abstract structure of) the vector it indexes into21/07 23:36
augurTree here is just purely a shape, not a shape + content21/07 23:37
auguri should rename it TreeShape instead21/07 23:38
--- Day changed Fri Jul 22 2011
djahandarieWhere is delete for Lists in the stdlib?22/07 01:23
copumpkinI doubt it's there22/07 01:26
copumpkinyou could use filter, I guess?22/07 01:26
copumpkinor does delete only remove the first element?22/07 01:27
djahandariedelete only removes the first element22/07 01:27
djahandarie> delete 1 [2,3,4,1,5,6,7,2,1,3,2,1]22/07 01:27
lambdabot  [2,3,4,5,6,7,2,1,3,2,1]22/07 01:27
Eduard_Munteanu@src delete22/07 01:28
copumpkinjust use span or break or something :P22/07 01:28
lambdabotdelete = deleteBy (==)22/07 01:28
copumpkinlist definitions tend to be mostly the same in agda anyway22/07 01:28
Eduard_Munteanu@src deleteBy22/07 01:28
lambdabotdeleteBy eq x []        = []22/07 01:28
lambdabotdeleteBy eq x (y:ys)    = if x `eq` y then ys else y : deleteBy eq x ys22/07 01:28
copumpkinyou could just write it yourself22/07 01:28
copumpkindelete doesn't really have any elegant properties22/07 01:28
Eduard_MunteanuAh, so nothing smarter in terms of other functions.22/07 01:28
djahandarieI was mainly looking for something that avoids Booleans22/07 01:29
djahandarieNot sure if something like that exists but that is why I was looking for it rather than writing it :p22/07 01:29
Eduard_Munteanu\?== avoids booleans22/07 01:29
Eduard_Munteanuor \== if you can use it22/07 01:30
Eduard_Munteanu(e.g. using that with 'with' patterns)22/07 01:30
djahandarieI think the nicest way would be to write delete in terms of Any22/07 01:32
djahandarieWhich is what I'm going to try and do. But unfortunately I'm working in Haskell right now. Maybe I should switch to Agda for a second to make my life easier22/07 01:32
djahandarieHm, it'd be easy in Agda. Might be very annoying in Haskell, I'll see.22/07 01:34
Eduard_MunteanuYou want to avoid Bool in Haskell? :)22/07 01:35
djahandarieWow, that was UGLY!22/07 01:49
djahandarieBut I got it to work :)22/07 01:49
xplatavoiding bool in agda makes you normal.  avoiding it in haskell makes you an iconoclast.22/07 02:07
xplatof course, using agda at all ...22/07 02:08
xplatyou know, i think it would be perfectly possible to do type classes without instance arguments (the new name for non-canonical implicits) if there were a facility for open induction-recursion instead22/07 02:14
xplatboth approaches have their complications but the latter is closer to haskell typeclasses in spirit22/07 02:15
xplatthe one actually chosen is more scala-ish22/07 02:15
augurhrmph22/07 02:15
augurim not at all understanding this Recursor stuff :(22/07 02:16
xplatopen induction-recursion feels like an interesting idea in itself22/07 02:16
xplataugur: btw have you looked at the two mu, ko & jansson papers near the end of http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Publication22/07 02:22
auguryour link is busted22/07 02:22
xplat+s22/07 02:23
augurah, yes, ive looked at them22/07 02:23
augurand didnt understand them at all22/07 02:23
Eduard_Munteanuxplat: I wondered about that as well22/07 02:23
xplatthe squiggoly stuff they try to do sounds similar to some of the stuff you've tried to do22/07 02:24
augurxplat: certainly. i just dont understand what they're doing. their paper is atrociously hard to understand unless you're already steeped in this sort of stuff22/07 02:25
Eduard_Munteanuxplat: however, maybe it means you can't typecheck modules in isolation?22/07 02:25
Eduard_Munteanuor compile22/07 02:25
xplatyeah, you'd probably need to trace back through some of the lenses/bananas introductory papers22/07 02:25
augurits not so much that22/07 02:25
augurits just that i learn by talking through examples, and their paper does none of that22/07 02:26
xplatEduard_Munteanu: probably to some extent, but no more than haskell.  probably termination checking could be a problem though ...22/07 02:26
augurits all "here are some obviously correct things, now lets move on"22/07 02:26
xplatalthough in a 'nice' enough case termination is given by a conjunction of local conditions, i don't know how practical it is to program so that that's the case.  maybe with the ever-magical sized types ...22/07 02:29
Eduard_MunteanuWell, typeclasses wouldn't be coinductive data types, would they?22/07 02:31
xplatprobably the 'master code' for a typeclass would be open-inductive, like Set22/07 02:32
xplatnot open-coinductive22/07 02:32
Eduard_MunteanuThat's interesting because Set doesn't allow pattern-matching, I wonder if that also prevents you from actually building the universe function22/07 02:33
Eduard_Munteanu(if there's a fundamental reason Set can't be pattern-matched)22/07 02:34
xplatin an open universe you have to supply cases for all its eliminators along with the constructor22/07 02:35
xplatother functions couldn't pattern-match on the open type, just like with Set22/07 02:35
Eduard_MunteanuI was thinking one should always have a defaulting case.22/07 02:36
Eduard_MunteanuAh.22/07 02:36
Eduard_MunteanuWait, defaulting didn't make sense.22/07 02:36
xplatwell, you could supply a default that's parametric22/07 02:37
xplatallowing partial pattern matching on an open universe is kind of similar to overlapping instances22/07 02:37
xplatunfortunately, if you allow it on user-defined universes it can be privilege-escalated to Set22/07 02:39
xplator at least partly so, through implicit inference22/07 02:41
Eduard_MunteanuHm, I'm considering inductive types on one hand, and non-inductive types like Set (on which you can't make any assumption about its structure or members)22/07 02:43
Eduard_Munteanu.. on the other.22/07 02:43
augurhmm22/07 02:44
Eduard_MunteanuMaybe something like    universe U     data Something : U where <void / no constructors>     might make sense?22/07 02:44
auguri think im getting a set of what these recursion combinator makers do22/07 02:44
xplatit's best to consider Set as kind of a prototype for open inductive types22/07 02:45
Eduard_MunteanuOr that's what you're referring to by privilege-escalation?22/07 02:45
Eduard_MunteanuWell, Set would be some sort of implicit   universe Set22/07 02:46
xplatyou get introduction forms (type constructors) and the ability to add new ones in your own modules, and you get implicit inference by backpropagation through constructor-headed functions22/07 02:47
xplatbut you only get special-purpose eliminators that come with the type (Set itself is rather trivial that way--you just have id as an 'eliminator', or ':' if you want to get very liberal)22/07 02:48
xplatthe thing that makes me wonder is what kind of visibility rules for instances would you need to safely be able to infer codes from a constructor-headed interpretation function22/07 02:51
xplatbecause it would end up being easy to accidentally weaken the guarantee on uniqueness of implicit inference22/07 02:52
xplatjust because *you* can only see one way to get that constructor out of that function doesn't mean it'll match what the guy that handed you that could see, necessarily, or i could be wrong22/07 02:53
Eduard_MunteanuWouldn't be reasonable to assume "instances" are visible to every module / every bit of code once they're created?22/07 02:55
Eduard_Munteanu(nevermind overlapping stuff)22/07 02:55
xplatsure, if you want to completely abandon separate compilation/typechecking22/07 02:55
Eduard_MunteanuOh, right. I'm not sure how that works yet. I presume there's lots of stuff in Agda that might need to peek inside other modules to figure stuff out.22/07 02:56
Eduard_MunteanuLike getting yellow that's automagically solved by adding users for that code.22/07 02:57
xplatthat doesn't happen across modules22/07 02:58
xplatand in any case, adding more users couldn't turn the code yellow again, only cause hard type errors22/07 02:58
Eduard_MunteanuI see.22/07 02:59
xplatwith the open-disinterpretation case adding more information *could* turn things yellow22/07 02:59
xplatand i'm not sure it's okay to allow that22/07 03:00
Eduard_MunteanuYeah, not if bad code/proofs can pass through fine at least.22/07 03:02
xplatfor example, i might have a module that goes along blithely thinking it knows what the monad instance for Either String Int is, and then i use it in a module that defines an instance for flip Either, giving the same constructor22/07 03:04
xplatif i included the first module textually in the second, yellow all over the place22/07 03:04
xplatis that going to cause other problems somewhere down the road?22/07 03:06
xplat(and with open universes the flip Either monad should be perfectly possible to do, but substitute any other type with two monads if you like, the ambiguity will be more clear.)22/07 03:08
xplatstrings with case-sensitive and case-insensitive Eq, maybe22/07 03:09
xplat(note that inferring codes from an interpretation function *into* an open inductive family is no problem--it's when an open inductive family is the argument/code that things get hairy)22/07 03:12
Eduard_MunteanuHm, I see.22/07 03:14
augurhmm!22/07 03:20
augurthis is starting to make sense!22/07 03:20
glguyaugur: Did you figure out your question about induction on pairs of your Tree shapes?22/07 04:36
glguyI was at work earlier and wasn’t able to focus on it22/07 04:36
augurglguy: its not induction on pairs of treeshapes but conjunctions of inductions on the same tree shape22/07 04:36
augurbut i _am_ better understanding this induction stuff22/07 04:37
glguyCould you share the URL to the file you showed earlier?22/07 04:38
augurhttps://github.com/psygnisfive/algebraic-syntax/blob/master/TreeIndex.agda22/07 04:38
glguyThanks.22/07 04:39
augurthe aim is to show that if P and Q are induction principles, then so is P -x- Q22/07 04:39
augurcopumpkin: what are galois's hiring requirements?22/07 05:03
copumpkinI should clarify my complaint there22/07 05:04
copumpkincause it isn't as bad as I made it out to be :P22/07 05:04
copumpkinbut for the position they have listed, it's phd, or master's + 5 years of experience, or bachelor's + 14 years22/07 05:05
augurnice22/07 05:16
augurwhat does galois do, exactly22/07 05:16
copumpkinI'm sure other people in here can give you better answers :)22/07 05:17
copumpkinbut as far as I can tell, contract work (mostly for gov't) in haskell22/07 05:17
augurevil22/07 05:18
glguy“evil” is the first word that comes to mind when I think of designing DSLs for constructing Bayesian models for scientists22/07 05:41
glguyor “nifty”, it’s kind of a toss-up22/07 05:41
copumpkin:)22/07 05:42
augurhmm22/07 07:50
augurso im confused about Induction.Nat.Rec22/07 07:50
augurand more generally, about Induction.Nat.build22/07 07:51
augurit seems like they're the same22/07 07:51
augurwell, except that build isnt self referential and so might not continue to recurse22/07 07:52
shlevyHowdy! I know only small bit about Haskell and next to nothing about Agda, and I want to just dive in and learn by writing my next application in Agda. Any recommendations about which resources to use?22/07 19:48
copumpkinI wouldn't approach it as writing a real app in agda yet :P22/07 19:49
copumpkinmost of us have no idea how to actually run agda programs22/07 19:49
copumpkinnobody ever does IO or anything in it :)22/07 19:49
djahandarielarry does I think22/07 19:50
shlevycopumpkin: Really? What do people actually do with it then?22/07 19:50
djahandarieGet familiar with it and then cringe every time they have to use Haskell. :)22/07 19:50
shlevyWhy?22/07 19:51
djahandarieIf you ever want to actually prove anything, Haskell is useless for that.22/07 19:52
copumpkinshlevy: write algorithms, prove things about them. Model areas of math they're interested in. Stuff like that :)22/07 19:52
shlevyNot why do they cringe, there's a reason I wanted to see if I could try skipping getting great at Haskell to get passable with Agda, I mean why don't people do IO?22/07 19:52
djahandarieI'd really recommend getting familiar with the odd corners of Haskell type-hacking first.22/07 19:53
djahandarieI think joe6 learned Agda before learning a lot of Haskell, you could ask him what he found most helpful22/07 19:54
shlevydjahandarie: I know, and that's probably the best route to take, but despite all the really good advice people give mea bout this sort of thing I only really learn by burning my hand over and over22/07 19:54
yrlnryThe Ulf Norell tutorial has this example of an apply function: http://pastebin.com/WrZhehDM22/07 19:57
yrlnryAs I read this, it means that the return type of f could be different at different values of the argument.22/07 19:57
Saizanyep22/07 19:58
yrlnryFor example, f 1 might be 3, and f 2 might be true.22/07 19:58
yrlnryOkay, thanks.22/07 19:58
copumpkinyrlnry: you're going to hac phi, right? we'll be doing some agda there probably22/07 19:59
djahandarieIt's okay because there's a unicode character in the conference name, obviously meaning that it's an Agda hackathon22/07 20:00
yrlnryI intend to be at hac phi.22/07 20:00
yrlnryI am looking forward to meeting you.22/07 20:00
Saizanmaybe we're discouraging "real world agda" too strongly :)22/07 20:01
djahandarieThe only people who can do it are the ones who try to do it despite our warnings. ;)22/07 20:04
Saizanyeah, i guess it needs that kind of perseverance anyway22/07 20:05
yrlnry"Failure at any cost!"22/07 20:05
shlevyI'm just really curious about the whys. No good IO libraries, inherent weakness in the language or in dependent programming as such, or what?22/07 20:06
yrlnryThe Norell tutorial has many flaws. One of the least excusable is the lack of page numbers.22/07 20:12
Saizanshlevy: the I/O interface is imported from haskell via the FFI, and it's not a complete import22/07 20:15
shlevySaizan: Why not?22/07 20:17
Saizanshlevy: because the full api would have been quite big i guess22/07 20:20
copumpkinyrlnry: yay22/07 20:27
copumpkinI think academics should be required to publish the latex source to their papers :P22/07 20:28
copumpkinso we can go back and add page nubmers22/07 20:28
copumpkinor rerender shitty postscript conversions22/07 20:28
yrlnryYeah.22/07 20:28
yrlnryOr reformat it for ridiculous US letter paper instead of A4 paper.22/07 20:28
yrlnryOr correct typos and then send the diffs back to the author.22/07 20:30
yrlnryI saw a notation error in the new Gibbons-Hinze paper and really wanted to press the "Edit this page" button.22/07 20:30
copumpkinyeah22/07 20:30
augurwark22/07 20:34
augurglguy: im not so sure that Induction.Lexicographic shows that conjunction of induction principles are themselves induction principles22/07 20:34
augurwell, i suppose in a way it does because it shows that conjunction of recursorbuilders are recursor builders22/07 20:35
augursort of22/07 20:35
yrlnryHmm, the glyph my browser displays for U+2a52 LOGICAL OR WITH DOT ABOVE has the dot at the bottom.22/07 20:41
augurglguy: thank you btw for making me read this. its very interesting22/07 21:15
copumpkinare you ready to implement a RecursorBuilderFactoryFactoryFacadeVisitor?22/07 21:15
glguyDo you have a convenient URL to the paper you can share?22/07 21:15
augurcopumpkin: x322/07 21:16
augurglguy: me? no not yet.22/07 21:16
copumpkinaugur: is your scala webscale?22/07 21:16
copumpkinagda, even22/07 21:16
glguyaugur: I mean the paper22/07 21:16
copumpkingoes to show what I have on my mind22/07 21:16
glguyI can't remember if I finished it back when I started using Induction.* modules22/07 21:16
augurglguy: wait what22/07 21:17
auguroh you mean view from the left?22/07 21:17
augurits on conors site22/07 21:17
auguralso, i meant just Induction.* not the paper. the paper didnt help me XD22/07 21:17
glguyoh, ha :)22/07 21:19
glguyaugur: I think that in the context of Induction.* recursion and induction are pretty interchangable22/07 21:25
auguryeah22/07 21:25
augurrecursion ofcourse is, and always has been, just the non-dependent induction principles22/07 21:25
glguyWell the recursion in Induction.* is dependent induction, not non-dependent22/07 21:25
augurright22/07 21:26
augurbut non-dependent induction is just dependent induction that doesnt depend!22/07 21:26
glguysounds like we are on the same page, then22/07 21:26
augurP = const X22/07 21:26
augurlike the examples in Induction.Nat, which just define the usual natrec functions and some other sort of recursion function22/07 21:27
augurblargh22/07 21:46
augurthis is harder than i expected22/07 21:46
augurwhy is it so hard to show that the intersection of two relation-valued induction principles is also a relation-valued induction principle D:22/07 21:47
auguraha!22/07 21:49
augurno. :(22/07 22:08
augurstill cant get it to work22/07 22:08
augur:\22/07 22:08
augurgrr22/07 22:10
auguris there a way to define a type for relations that "know" that their witnesses are?22/07 22:43
augurlike, a relation R that knows that the proofs of R x y will have a particular structure? probably not .. hrmph22/07 22:44
augurthis is turning out to be a much harder exercise than i expected22/07 22:44
augurmaybe its just not true..22/07 23:14
Saizan?bot22/07 23:18
Saizanisn't it like foldr f1 z1 :: P; foldr f2 z2 :: Q; foldr (\x (p,q) -> (f1 x p, f2 x q)) (z1,z2) :: (P,Q) ? only dependendent and with trees instead of lists?22/07 23:19
Saizanheh, i guess i forgot the list parameters there, add xs to all the expressions :)22/07 23:20
Saizanah, but you have binary relations, not sure how that fits then22/07 23:23
augurSaizan: thats what i thought but i cant get it to work22/07 23:44
augurthe recursive calls end up having a slightly incorrect type because they're dependent22/07 23:45
--- Day changed Sat Jul 23 2011
Saizanhttp://hpaste.org/49388 <- seems to work for lists23/07 00:06
augurno, its not that i cant define the pairing part23/07 00:07
augurim trying to show that F ~ treeind P z f23/07 00:08
auguror more specifically23/07 00:09
augurthat if F ~ treeind P z f, F' ~ treeind P' z' f'23/07 00:09
augurthen F -x- F' ~ treeind ? ? ?23/07 00:09
SaizanF : (t : Tree) -> P t ?23/07 00:10
augurwell, in this case P t = Rel (T t) 0 but yes23/07 00:11
Saizanand ~ being what?23/07 00:11
augurequivalent to. so like23/07 00:12
augurF t x y <-> treeind P z f x y23/07 00:12
Saizani.e. both -> and <- ?23/07 00:12
auguryeah23/07 00:12
augurso basically: if F t, F' t are binary relations over T t's that are equivalent to some induction principles treeind P z f and treeind P' z' f', then their intersection is also equivalent to some induction principle23/07 00:13
Saizantreeind is an induction principle, treeind P z f isn't23/07 00:14
augurok, equivalent to some function defined by way of an induction principle :P23/07 00:14
auguri dont have a term for such a thing23/07 00:14
augurlets call it an induced X23/07 00:15
augurso if F t and F' t are induced relations, then so is F t -x- F' t23/07 00:15
augurthe idea is to be able to show that some complex widget is an induced relation by way of showing that its parts are23/07 00:15
augurthe big one that im working on is   CC t x y = (¬ x < y) × (¬ y < x) × (¬ x ≡ y) × (Σ[ z ∶ TreeIndex t ] z < x × z <⁺ y)23/07 00:17
augurobviously thats horribly ugly23/07 00:17
augurand itd be nice to be able to compose proofs to get that23/07 00:17
augur_<_  is induced, so  ¬_ ∘ _<_  is induced so  flip (¬_ ∘ _<_)  is induced so  < (¬_ ∘ _<_) , flip (¬_ ∘ _<_) > is induced23/07 00:19
augurthat gets us up to  R t x y = (¬ x < y) × (¬ y < x)23/07 00:19
auguryou see what im aiming for?23/07 00:19
auguri can show that _<_ is induced relatively easily, i think, so if logical combinations of relations are also induced, then its a simply matter of just using the combinators to build the larger induced relation23/07 00:23
augurSaizan: i have a /way/ of getting it to work, i think23/07 01:48
augurbut i feel like im cheating, because the recursive case doesnt make use of the recursively constructed functions at all :(23/07 01:48
auguri feel like part of the problem is that relations dont know what their witnesses are, and so even tho the recursively computed relations will have pair witnesses (since they're conjunctions), the relation itself doesnt know this23/07 01:51
augurand so i cant extract the left and right witnesses nor their types23/07 01:51
augurso i cant use just the left witnesses to compute a new left witness23/07 01:52
augurso theres no way to say with any certainty that the intersection of induced relations is also an induced relation23/07 01:53
xplatwell, you can prove this just for the case when your thing is an intersection of induction principles first (rather than equivalent to such)23/07 01:57
xplatand prove the rest with laws of logic/equivalence23/07 01:58
augurxplat: how do you mean?23/07 01:58
xplatiow, prove that an intersection of induction principles is equivalent to an induction principle23/07 01:58
augurhmm23/07 01:59
xplatthen you can just lift that to the full proof you want with laws of logic23/07 01:59
auguri dont know how that would work23/07 01:59
auguri mean, treeind & treeind is ofcourse an induction principle: treeind23/07 01:59
xplatif A ~ B and C ~ D, then A /\ B ~ C /\ D.  that, plus equivalence is transitive.23/07 02:00
auguri still dont see how that gets anywhere23/07 02:01
augurhmm wait, is the suggestion to show that like..23/07 02:01
augurtreeind P z f /\ treeind P' z' f' ~ treeind P" z" f"23/07 02:02
xplatyes23/07 02:02
augurand therefore since F ~ treeind P z f, and F' ~ treeind P' z' f'23/07 02:02
augurthen F /\ F' ~ treeind P" z" f"23/07 02:02
augurhmm!23/07 02:02
augurso then the goal is something like23/07 02:03
augurforall P z f P' z' f' -> exists P" z" f" -> treeind P z f /\ treeind P' z' f' ~ treeind P" z" f"23/07 02:04
auguror something?23/07 02:04
xplatyeah, sounds about right23/07 02:05
augurwhere X ~ Y is.. forall t. X t <-> Y t i guess23/07 02:06
xplatand the intersection here should know that its pointwise witnesses resolve to pairs23/07 02:07
augurhow would that work now23/07 02:07
augurdo you mean like with _\cup_?23/07 02:08
augurP \cup Q = \x -> P x * Q x23/07 02:08
xplatyes23/07 02:09
xplatalthough i think that's \cap23/07 02:14
augurthat too :)23/07 02:17
augurhmm23/07 02:20
augurwell, \cap would work for predicates23/07 02:21
augurso i'd need -x- for relations i guess23/07 02:21
augurand i suppose since it is indeed relations, P = P' = P'' = \t -> Rel (TreeIndex t) zero23/07 02:21
augurgrr23/07 02:30
auguri cant get the type for this thing to work :(23/07 02:30
auguraha!23/07 02:31
augurxplat: hmm23/07 02:46
augurim runing into basically the same problem i did before23/07 02:46
augurhey xplat23/07 03:22
auguri think i know why it wont be possible to do generally23/07 03:22
glguycopumpkin: I find the new scrolling behavior fits well with other things they’ve done with it, like how forward and back work in Safari23/07 04:41
copumpkinoh, I don't doubt that. I just question people making it out to be a great benefit. I think it's consistent, and don't mind learning it23/07 04:42
copumpkin(not on lion yet)23/07 04:42
copumpkin(wait, you read twitter but don't tweet?)23/07 04:43
glguyI “read Twitter” but I don’t seek it out23/07 04:43
copumpkinah :)23/07 04:43
glguyI had your Twitter page open from the last Twitter message you wrote23/07 04:43
glguystill haven’t closed the page :)23/07 04:43
copumpkin:O23/07 04:43
glguyOne of the guys I was sitting next to at work reads Twitter is how I found it to begin with23/07 04:44
copumpkinah, I see23/07 04:44
glguyto follow you I’d have to figure out what my Twitter password is23/07 04:45
copumpkinthat sounds a lot harder than your average agda proof23/07 04:45
glguyAll I remember is that I made it complicated23/07 04:46
copumpkinI often have that problem23/07 04:46
* glguy wishes more websites would support client-side certificate authentication23/07 04:46
glguypasswords are bogus tech23/07 04:46
copumpkinI agree23/07 04:46
auguris there a way to subscript non-numeric things?23/07 04:47
copumpkinnot sure what would work better for average joe though23/07 04:47
copumpkinaugur: don't think so. Go browsing around the unicode tables :P23/07 04:47
glguyaugur: it’s a font limitation23/07 04:47
augurhm23/07 04:47
glguyand yeah, unicode23/07 04:47
* copumpkin shudders23/07 04:49
copumpkinnow I actually have a real computer running windows23/07 04:49
copumpkin(the most I usually do is run it in a VM)23/07 04:49
glguyI have Windows in bootcamp for my game playing habit :)23/07 04:52
copumpkinhah23/07 04:52
copumpkinwhat do you play?23/07 04:52
glguyEve Online most recently23/07 04:54
glguybut an assortment of things, really. some of the grand theft series, neverwinter nights, crysis, magic, terraria23/07 04:55
glguyminecraft, spacechem23/07 04:56
glguyI got in spurts23/07 04:56
glguymore and more of the games I like are available on OS X, but at a performance penalty23/07 04:56
copumpkinyeah23/07 04:56
glguyI was playing The Sims and Sim City 4 this year… haven’t lately23/07 04:57
copumpkincool23/07 04:58
copumpkinI'm half tempted to install crysis on this machine just to see it run23/07 04:58
copumpkinor some other ridiculous game23/07 04:58
djahandarieI bricked my shitty Windows computer by playing Age of Kings too intensely23/07 04:58
copumpkinlol23/07 04:59
copumpkindjahandarie is too hardcore for his computer23/07 04:59
djahandarieI need to get a new beater windows computer23/07 05:00
djahandarieOr get a new good computer and move my current one to beater status23/07 05:00
auguri wish aquamacs had folding23/07 05:11
augurlinefolding, i mean23/07 05:11
glguyHow do you know if you are using Aquamacs?23/07 05:12
glguyI have an OS X version of Emacs23/07 05:13
augurgrr23/07 05:31
augurso close23/07 05:31
auguroh hey yeah im using aquamacs because it says Aquamacs :P23/07 05:31
augurwhats it called when you have a relation that has uncong defined?23/07 05:35
augurlike how you have uncong for == etc.?23/07 05:35
copumpkinglguy: the app name is aquamacs23/07 05:36
copumpkinthere's also a gui emacs for mac os23/07 05:36
copumpkinthat's uglier, in my opinion23/07 05:36
copumpkinuncong?23/07 05:36
copumpkinwhat's the type of that?23/07 05:36
auguruncong-left : forall {X} {x y : X} -> left x == left y -> x == y23/07 05:37
auguror something like that23/07 05:37
copumpkinit just means left is injective23/07 05:37
copumpkinany constructor is automagically injective, but for other functions you need to prove it23/07 05:38
copumpkinautomagically meaning that your proof there will be pretty trivial23/07 05:38
augurright but i mean23/07 05:39
augurthats if f is a function23/07 05:39
augurwhat if its a relation?23/07 05:39
augurer sorry no23/07 05:39
augurrather23/07 05:39
augurwhat about for relations other than _==_23/07 05:39
augureg x < y -> suc x < suc y23/07 05:40
augurand vice versa23/07 05:40
auguri guess x would be monotonic?23/07 05:40
augur..23/07 05:40
augur_<_23/07 05:40
augurwhy do my fingers not work. >_<23/07 05:40
augurwhats it called copumpkin! D:23/07 05:43
copumpkinbeats me23/07 05:43
auguri feel like ive seen stuff like this before23/07 05:44
copumpkinI mean, it isn't just about a relation23/07 05:44
copumpkinit's about a relation in conjunction with some function23/07 05:44
augurprobably23/07 05:44
augurwith _==_ tho i think its when _==_ is a congruence23/07 05:44
augurhence the name23/07 05:44
auguri dont know what it would be called with _<_, tho, for instance23/07 05:45
copumpkinwell, if _==_ is a congruence, it means that any function you can apply to either side still respects the relation23/07 05:45