--- Log closed Tue Jun 20 01:13:00 2017
--- Log opened Tue Jun 20 01:13:09 2017
-!- Irssi: #agda: Total of 116 nicks [0 ops, 0 halfops, 0 voices, 116 normal]20/06 01:13
-!- Irssi: Join to #agda was synced in 122 secs20/06 01:15
Saizanhttps://github.com/Saizan/parametric-demo/blob/master/Yoneda.agda <- yoneda lemma as a free theorem :)20/06 13:51
{AS}Saizan: what is :{#} ?20/06 14:14
{AS}But otherwise cool :)20/06 14:14
jonsterlingSaizan: that's pretty cool!20/06 16:15
ziman_Saizan: is agda/parametric written up somewhere? in your icfp'17 paper?20/06 17:03
Saizanziman: yep, do you have the draft?20/06 17:46
zimanI don't, I'd welcome one :)20/06 17:52
zimanI'm working on a somewhat related topic -- erasure in dependently typed programming, but from a more applied point of view20/06 17:54
zimanand since erasable binders are parametric, there is a close connection :)20/06 17:54
Saizanis this on top of ICC?20/06 18:13
zimanyes, that's the starting point, more or less20/06 18:50
zimanI add inductive types, pattern matching functions, erasure inference (and a form of erasure polymorphism)20/06 18:54
zimanyou mention that erasability is stronger than parametricity -- is it strictly stronger?20/06 19:05
Saizanziman: yeah, i mean in our case it even makes sense to have a function Nat -> Nat parametric in the first argument which is prop. equal to the identity20/06 19:15
zimanoh, I see, very interesting20/06 19:19
dolioWhat is your notion of relation?20/06 19:21
Saizanmostly we have primitives to build "relations" as the graph of given functions, and internally they are like maps from an interval type into the universe, cubical-style20/06 19:24
dolioI don't think that works for Nat -> Nat.20/06 19:25
dolioI guess you could use maps from the interval into Nat, but that's boring.20/06 19:25
dolioAlthough valid.20/06 19:26
Saizani mean, Nat's relation is equality, so there isn't much to preserve20/06 19:26
dolioYou don't need a relation on Nat.20/06 19:27
{AS}If the function is constant it will always be parametric over its argument right? 20/06 19:27
dolioYou need a relation between e.g. 2 and 3.20/06 19:27
dolioTo be analogous to parametricity.20/06 19:27
Saizanthe idea is that for some types parametricity really does nothing, other types sure, we have a "Size" which is like Nat but where all the elements are related20/06 19:28
dolioAnyhow, you're missing out, because there's a more interesting answer.20/06 19:28
Saizanthen you get some theorems out of a function taking a Size as a parametric argument20/06 19:28
Saizandolio: what?:)20/06 19:28
dolioThe incremental lambda calculus.20/06 19:28
dolioWhere you have change structures on types.20/06 19:29
dolioAnd the analogue of parametricity is the derivative of the function.20/06 19:29
dolioSo a 'relation from 2 to 3' is `+1`.20/06 19:30
dolioAnd the derivative of id : Nat -> Nat is d id : Nat -> D Nat -> D Nat, d id n dn = dn.20/06 19:31
dolioThat type isn't actually fancy enough, but...20/06 19:32
Saizando you get free theorems out of this?20/06 19:32
dolioIf you define 'change structures' on the universe to be relations, you get parametricity.20/06 19:32
Saizaninteresting20/06 19:33
doliohttps://plus.google.com/+DanDoel/posts/caXnw5kGVKp20/06 19:33
Saizanwe can also have (+1) as a relation, but i'm not sure of the applications in our theory20/06 19:34
dolioAt least, the type signatures work out.20/06 19:34
dolioHaving it be computationally meaningful is the hard part.20/06 19:34
dolio:)20/06 19:34
dolioAnyhow, that always stymied me thinking about parametricity, even for the erasure case.20/06 19:44
dolioBecause if you think about e.g. `reverse : (n : Nat) -> Vec T n -> Vec T n`20/06 19:45
dolioAnd start writing down the equivalent of the parametricity type, you write: (m n : Nat) -> (R : m <=> n) -> ...20/06 19:46
Saizan..and?20/06 19:52
Saizan(i've been going through the google+ thread)20/06 19:53
dolioAnd it was unclear to me what a 'relation' between two particular natural numbers should be, and it's arbitrary to pick m <=> n to be m = n.20/06 19:53
dolioAnd unrelated to the choice to use = as the relation from a concrete type to itself in parametricity.20/06 19:54
dolioI think.20/06 19:54
dolioAlso picking = means you don't really have two different numbers at all.20/06 19:55
Saizanwell, since a function of that type can return quite different results for different natural numbers then it's hard to pick m <=> n be something else and still have a "free theorem"20/06 19:55
dolioSo it ends up being not interesting. I was happy when I saw something where every number is 'related' to every other number via their difference.20/06 19:55
Saizani see20/06 19:57
Saizani guess the theorem you get then would be more dependent on the actual function then20/06 19:57
dolioYeah.20/06 19:57
dolioAlthough I'm not sure how that case works out.20/06 19:59
dolioBecause the 'n' there is ostensibly irrelevant.20/06 19:59
dolioSo you would hope that there is some kind of result independent of the number.20/06 20:00
dolioBut every change in number happens to correllate with a change in the other arguments, so I don't know.20/06 20:00
Saizanright20/06 20:03
dolioThe other cool thing, though, is that you don't even need the 'n' to be irrelevant.20/06 20:04
dolioFunctions have derivatives regardless, they just depend on the function.20/06 20:05
Saizanhowever the more you depend on the function the more it's just what you get from plain dependent type theory20/06 20:07
dolioYeah, I mean, the original paper wanted to use this stuff for incremental updates of function results.20/06 20:09
dolioAnd the connection with parametricity was something someone noticed later.20/06 20:10
Saizanon the other hand we wish we had some topological meaning for our extra parametricity primitives, and it would be nice if manifolds and derivatives would be a model20/06 20:12
Saizan(or wherever else derivatives make sense, i'm not great at any kind of geometry)20/06 20:14
dolioYeah, I don't know if you read far enough into my rambling and conversation with the ILC author, but there's some similarity to differential geometry, too.20/06 20:14
dolioAnd also (forward mode) automatic differentiation can be understood in those terms, too.20/06 20:17
Saizanyep, i noticed those parts, i will have to go over them again20/06 20:18
dolioLike, in differential geometry, you have manifolds, and at each point t in a manifold T, a tangent space DT(t). And you can assemble those into a tangent bundle which is like `Sigma T DT`. And the derivative of f is a map between tangent bundles that commutes with f and the first projections.20/06 20:20
Saizanoh, i see, like in bernardy's unary parametricity with the colored sigma20/06 20:22
dolioPossibly. I haven't actually read that.20/06 20:22
dolioI think the tangent bundle map would be like the type pairing values with their parametricity witnesses, though.20/06 20:24
dolioIf that's what the sigma you're talking about does.20/06 20:24
dolioOr, wait.20/06 20:24
Saizansomething like a map "f_c : Sigma_c A P -> Sigma_c B Q" could be projected down to a map f_0 : A -> B, and a parametricity proof that it sends P x to Q (f_0 x)   20/06 20:29
dolioYeah, I'm not exactly sure how to fit dependent types into the differential geometry stuff.20/06 20:29
Saizanheh20/06 20:29
dolioYes, that is very similar to the differential geometry stuff.20/06 20:30
dolioThe tangent bundle functor is also a monad. Not sure what that translates to.20/06 20:32
Saizan(btw this is the best incarnation of the colored stuff imo http://publications.lib.chalmers.se/publication/230735)20/06 20:34
dolioThanks. I meant to read about it a long time ago, but it's just been sitting in my ever growing folder of papers, I think.20/06 20:35
Saizanactuall i lied, i like the last chapter of the thesis better :) didn't realize they changed it so much from the article http://publications.lib.chalmers.se/publication/235758 , but still fodder for the pile of papers anyway :)20/06 20:46
dolioOh, by the way...20/06 20:50
dolioOne thing I've wondered for a while, which you might know off hand. Obviously parametricity is usually stated in terms of relations. When you naively postulate that in Agda, you use A <=> B = A -> B -> Set.20/06 20:52
dolioBut A -> B -> Set has things that aren't "relations".20/06 20:52
dolioDo any systems with internal parametricity make sense when you use arbitrary profunctors (basically) instead? Or do they all restrict things to propositional things?20/06 20:54
dolioI guess profunctor is the wrong term. But anyway.20/06 20:58
mietekhttps://lirias.kuleuven.be/bitstream/123456789/583556/1/thesis-final-digital.pdf looks amazing20/06 21:01
mietekis that in Agda yet?20/06 21:02
dolioOh, cool.20/06 21:12
dolioDoes dependent pattern matching still rely on disjointness of constructors, though?20/06 21:13
dolioThat's the other assumption people always forget about. :)20/06 21:13
carterThat's the no confusion one?  Does that relate to injectivity?20/06 21:14
dolioInjectivity is slightly different.20/06 21:14
carterdolio: do you or other folks have thoughts on what scale proofs does tactics programming starts paying off?20/06 21:15
dolioI've never used tactics, so no. :)20/06 21:15
carterIt looks like the Tc monad stuff in agda almost gets you there. But the stuff can do with ltac etc is on a crazy other level20/06 21:16
mietekcarter: my position is that it’s metaprogramming and we should have a language that lets you do it *in* the language20/06 21:17
mietekcarter: very slowly working towards that20/06 21:17
carterMietek not very useful if I wanna use proof automation this week :(20/06 21:18
mietekI know :(20/06 21:18
mietekcarter: you know that Swierstra paper?20/06 21:18
carterHe has more than one paper20/06 21:19
mietekcarter: http://www.staff.science.uu.nl/~swier004/publications/2015-mpc.pdf20/06 21:19
carterThx20/06 21:19
carterLooks like the reflection examples in the prelude and std lib repos is more up to date though ;)20/06 21:22
mietekthe reflection adhocery probably changed three times since 2015 ;p20/06 21:22
pgiarrussocarter: do you have numbers? inequality? Can you get Coq to accept your datatypes without too many hacks?20/06 21:54
pgiarrussothe more yeses, the more likely is that Coq helps20/06 21:55
pgiarrussoI'm sorry that's not a real answer20/06 21:55
pgiarrussodolio: Hi! you say 'But A -> B -> Set has things that aren't "relations".', but that seems confusing in a sense20/06 22:01
pgiarrussocan't you read *all* members of A -> B -> Set as relations?20/06 22:02
dolioIn a sense. But I mean in the strict sense where there is at most 1 value of R a b for each a and b.20/06 22:02
dolioOr all values of R a b are equal for each a and b.20/06 22:03
dolio'equal'20/06 22:03
dolioAnyhow, the question is whether that fact is somehow essential to making computational parametricity work.20/06 22:04
pgiarrussodolio: I'd guess internal parametricity does not require all values to be equal, but it doesn't distinguish much between them Β— 20/06 22:04
pgiarrussoif *you* care about the difference, the internal parametricity function might not give you the proof you'd want20/06 22:04
dolioI suspect it doesn't matter, either.20/06 22:06
pgiarrussodolio: are you familiar with Bernardy's parametricity transformation? because I'd strongly think that one does not require that equality20/06 22:06
pgiarrussooh yeah you mention it20/06 22:07
dolioI know of it, but I haven't gotten around to reading the paper yet. :)20/06 22:07
pgiarrussowhat matters: for any term t of type T you can produce a proof term derive(t) that t satisfies the parametricity property for T20/06 22:08
pgiarrussoand with arbitrary PTSs, IIRC, the parametricity property is produced with a related/the same transformation20/06 22:08
dolioIt seems like the proof-relevant parametricity (if you want to call the arbitrary A -> B -> Set version that) might depend more on the content of the functions for the specific value of the parametricity term, though.20/06 22:09
dolioBecause it's kind of doing the same thing as the function it's a proof about.20/06 22:09
pgiarrussothat's already what happens20/06 22:09
dolioJust shoving around indexed values instead of the base values.20/06 22:09
pgiarrussothe proof term depends on the specific term, the same way the proof of parametricity is done by induction on terms20/06 22:09
pgiarrussodolio: let me dig the realizer showing id is parametric :-)20/06 22:10
carterOk so agda it is ;)20/06 22:12
dolioOr, like, if you say you have a relation R : A <=> B, and you want to promote that to a relation R' : List A <=> List B, you can say that R' relates equally sized list of values related index-wise. But another way to look at R' is to say it's a list of Sigma a:A b:B. R a b values.20/06 22:13
dolioAnd that obviously makes sense even if R isn't propositional.20/06 22:14
dolioList is kind of its own lifting on 'relations'.20/06 22:15
pgiarrussodolio: OK, let's use Bernardy's transformation on T : ⋆ ⊦ πœ† x : T . x20/06 22:18
pgiarrussofor binary parametricity, what you get is (T₁ Tβ‚‚ : *) (T' : T₁ β†’ Tβ‚‚ β†’ [s]) ⊦ (πœ† (x₁ : T₁) (xβ‚‚ : Tβ‚‚) (x' : T' x₁ xβ‚‚). x') : (Ξ  (x₁ : T₁) (xβ‚‚ : Tβ‚‚) (x' : T' x₁ xβ‚‚). (T' (id₁ x₁) (idβ‚‚ xβ‚‚))20/06 22:18
pgiarrussowhere id₁ = πœ† x : T₁ . x and idβ‚‚ = πœ† x : Tβ‚‚ . x20/06 22:18
pgiarrussoso, if your T' has multiple members, you'll get your particular witness back20/06 22:19
dolioRight.20/06 22:19
pgiarrussodolio: You're right though in a different way: parametricity defines a *program equivalence* (though few will tell you)20/06 22:20
pgiarrussoand for that it's essential that for all concrete types the relation is an equality20/06 22:20
dolioThe witness for parametricity of id is a fancy id, basically.20/06 22:20
pgiarrussohaving a single witness for it doesn't matter, being equality does20/06 22:20
pgiarrussodolio: yes20/06 22:20
pgiarrussoand if you look at it and are familiar with derive, you might recognize it's very similar :-)20/06 22:21
pgiarrussodolio: in fact, if you know that compilers are staged interpreters, Bernardy's work essentially just *staged* the relational interpreters/semantics of the other works on parametricity20/06 22:22
pgiarrussodolio: if you drop the requirement for equality (which is, technically, the identity extension lemma), you get generic "logical relations" proofs20/06 22:23
dolioOkay, cool.20/06 22:24
pgiarrussothe key theorem (the fundamental property or basic lemmas) says that all all terms are related to themselves, and is proved with the same strategy20/06 22:25
pgiarrussousually only for well-typed terms20/06 22:25
pgiarrussobut with a bit more magic (like step-indexes), you can prove it for untyped languages as well20/06 22:26
pgiarrussoI can recommend to anybody interested ezyang's notes from Ahmed's course here: https://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html (for me, they only open in Adobe Reader and look mangled elsewhere, but they're worth it)20/06 22:27
dolioOkay, thanks.20/06 22:27
dolioI guess my expectation that things would work out that way clicked recently with some thinking I was doing about induction in category theory.20/06 22:29
pgiarrussodolio: please do tell20/06 22:29
pgiarrussoBTW, I'm also wondering about other applications of these sort of transformations... does anybody care for a witness to the difference between two executions?20/06 22:30
dolioWell, the usual way to think about families T : A -> Set in category theory is as display maps T -> A.20/06 22:30
dolioWhere the latter T is like (Sigma A T) (with the former T), and the map is fst.20/06 22:31
dolioBut you can just consider any type with a map into A as a family over A.20/06 22:31
dolioSo, Nat-indexed families are maps into Nat.20/06 22:32
dolioAnd the proof obligation `T 0 * (forall n. T n -> T (suc n))` can actually be seen as a map of these things `1 + T -> T` where t : T -> Nat shows you how to get T : Nat -> Set, and `in . 1 + t : 1 + T -> Nat` corresponds to an indexed version of the 1+ functor.20/06 22:36
dolioWhich goes: (Nat -> Set) -> (Nat -> Set).20/06 22:36
dolioBut in category theory, it's still just 1+ with a sort of different interpretation.20/06 22:36
dolioSo the indexed version of induction corresponds to the usual derivation of recursion, but considering only cases where you commute with these display maps, and use uniqueness a bit.20/06 22:37
dolioBut you don't have to worry about, like, 'what is the lifting of my functor F to families?' It's just F with a modified display.20/06 22:38
dolioWhich is similar to relations between lists being lists of relations, or the identity parametricity witness being identity on the relations involved.20/06 22:39
dolioGotta go.20/06 22:39

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