--- 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 secs | 20/06 01:15 | |

Saizan | https://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 |

jonsterling | Saizan: 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 |

Saizan | ziman: yep, do you have the draft? | 20/06 17:46 |

ziman | I don't, I'd welcome one :) | 20/06 17:52 |

ziman | I'm working on a somewhat related topic -- erasure in dependently typed programming, but from a more applied point of view | 20/06 17:54 |

ziman | and since erasable binders are parametric, there is a close connection :) | 20/06 17:54 |

Saizan | is this on top of ICC? | 20/06 18:13 |

ziman | yes, that's the starting point, more or less | 20/06 18:50 |

ziman | I add inductive types, pattern matching functions, erasure inference (and a form of erasure polymorphism) | 20/06 18:54 |

ziman | you mention that erasability is stronger than parametricity -- is it strictly stronger? | 20/06 19:05 |

Saizan | ziman: 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 identity | 20/06 19:15 |

ziman | oh, I see, very interesting | 20/06 19:19 |

dolio | What is your notion of relation? | 20/06 19:21 |

Saizan | mostly 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-style | 20/06 19:24 |

dolio | I don't think that works for Nat -> Nat. | 20/06 19:25 |

dolio | I guess you could use maps from the interval into Nat, but that's boring. | 20/06 19:25 |

dolio | Although valid. | 20/06 19:26 |

Saizan | i mean, Nat's relation is equality, so there isn't much to preserve | 20/06 19:26 |

dolio | You 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 |

dolio | You need a relation between e.g. 2 and 3. | 20/06 19:27 |

dolio | To be analogous to parametricity. | 20/06 19:27 |

Saizan | the 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 related | 20/06 19:28 |

dolio | Anyhow, you're missing out, because there's a more interesting answer. | 20/06 19:28 |

Saizan | then you get some theorems out of a function taking a Size as a parametric argument | 20/06 19:28 |

Saizan | dolio: what?:) | 20/06 19:28 |

dolio | The incremental lambda calculus. | 20/06 19:28 |

dolio | Where you have change structures on types. | 20/06 19:29 |

dolio | And the analogue of parametricity is the derivative of the function. | 20/06 19:29 |

dolio | So a 'relation from 2 to 3' is `+1`. | 20/06 19:30 |

dolio | And the derivative of id : Nat -> Nat is d id : Nat -> D Nat -> D Nat, d id n dn = dn. | 20/06 19:31 |

dolio | That type isn't actually fancy enough, but... | 20/06 19:32 |

Saizan | do you get free theorems out of this? | 20/06 19:32 |

dolio | If you define 'change structures' on the universe to be relations, you get parametricity. | 20/06 19:32 |

Saizan | interesting | 20/06 19:33 |

dolio | https://plus.google.com/+DanDoel/posts/caXnw5kGVKp | 20/06 19:33 |

Saizan | we can also have (+1) as a relation, but i'm not sure of the applications in our theory | 20/06 19:34 |

dolio | At least, the type signatures work out. | 20/06 19:34 |

dolio | Having it be computationally meaningful is the hard part. | 20/06 19:34 |

dolio | :) | 20/06 19:34 |

dolio | Anyhow, that always stymied me thinking about parametricity, even for the erasure case. | 20/06 19:44 |

dolio | Because if you think about e.g. `reverse : (n : Nat) -> Vec T n -> Vec T n` | 20/06 19:45 |

dolio | And 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 |

dolio | And 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 |

dolio | And unrelated to the choice to use = as the relation from a concrete type to itself in parametricity. | 20/06 19:54 |

dolio | I think. | 20/06 19:54 |

dolio | Also picking = means you don't really have two different numbers at all. | 20/06 19:55 |

Saizan | well, 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 |

dolio | So 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 |

Saizan | i see | 20/06 19:57 |

Saizan | i guess the theorem you get then would be more dependent on the actual function then | 20/06 19:57 |

dolio | Yeah. | 20/06 19:57 |

dolio | Although I'm not sure how that case works out. | 20/06 19:59 |

dolio | Because the 'n' there is ostensibly irrelevant. | 20/06 19:59 |

dolio | So you would hope that there is some kind of result independent of the number. | 20/06 20:00 |

dolio | But every change in number happens to correllate with a change in the other arguments, so I don't know. | 20/06 20:00 |

Saizan | right | 20/06 20:03 |

dolio | The other cool thing, though, is that you don't even need the 'n' to be irrelevant. | 20/06 20:04 |

dolio | Functions have derivatives regardless, they just depend on the function. | 20/06 20:05 |

Saizan | however the more you depend on the function the more it's just what you get from plain dependent type theory | 20/06 20:07 |

dolio | Yeah, I mean, the original paper wanted to use this stuff for incremental updates of function results. | 20/06 20:09 |

dolio | And the connection with parametricity was something someone noticed later. | 20/06 20:10 |

Saizan | on 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 model | 20/06 20:12 |

Saizan | (or wherever else derivatives make sense, i'm not great at any kind of geometry) | 20/06 20:14 |

dolio | Yeah, 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 |

dolio | And also (forward mode) automatic differentiation can be understood in those terms, too. | 20/06 20:17 |

Saizan | yep, i noticed those parts, i will have to go over them again | 20/06 20:18 |

dolio | Like, 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 |

Saizan | oh, i see, like in bernardy's unary parametricity with the colored sigma | 20/06 20:22 |

dolio | Possibly. I haven't actually read that. | 20/06 20:22 |

dolio | I think the tangent bundle map would be like the type pairing values with their parametricity witnesses, though. | 20/06 20:24 |

dolio | If that's what the sigma you're talking about does. | 20/06 20:24 |

dolio | Or, wait. | 20/06 20:24 |

Saizan | something 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 |

dolio | Yeah, I'm not exactly sure how to fit dependent types into the differential geometry stuff. | 20/06 20:29 |

Saizan | heh | 20/06 20:29 |

dolio | Yes, that is very similar to the differential geometry stuff. | 20/06 20:30 |

dolio | The 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 |

dolio | Thanks. 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 |

Saizan | actuall 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 |

dolio | Oh, by the way... | 20/06 20:50 |

dolio | One 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 |

dolio | But A -> B -> Set has things that aren't "relations". | 20/06 20:52 |

dolio | Do 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 |

dolio | I guess profunctor is the wrong term. But anyway. | 20/06 20:58 |

mietek | https://lirias.kuleuven.be/bitstream/123456789/583556/1/thesis-final-digital.pdf looks amazing | 20/06 21:01 |

mietek | is that in Agda yet? | 20/06 21:02 |

dolio | Oh, cool. | 20/06 21:12 |

dolio | Does dependent pattern matching still rely on disjointness of constructors, though? | 20/06 21:13 |

dolio | That's the other assumption people always forget about. :) | 20/06 21:13 |

carter | That's the no confusion one? Does that relate to injectivity? | 20/06 21:14 |

dolio | Injectivity is slightly different. | 20/06 21:14 |

carter | dolio: do you or other folks have thoughts on what scale proofs does tactics programming starts paying off? | 20/06 21:15 |

dolio | I've never used tactics, so no. :) | 20/06 21:15 |

carter | It 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 level | 20/06 21:16 |

mietek | carter: my position is that itβs metaprogramming and we should have a language that lets you do it *in* the language | 20/06 21:17 |

mietek | carter: very slowly working towards that | 20/06 21:17 |

carter | Mietek not very useful if I wanna use proof automation this week :( | 20/06 21:18 |

mietek | I know :( | 20/06 21:18 |

mietek | carter: you know that Swierstra paper? | 20/06 21:18 |

carter | He has more than one paper | 20/06 21:19 |

mietek | carter: http://www.staff.science.uu.nl/~swier004/publications/2015-mpc.pdf | 20/06 21:19 |

carter | Thx | 20/06 21:19 |

carter | Looks like the reflection examples in the prelude and std lib repos is more up to date though ;) | 20/06 21:22 |

mietek | the reflection adhocery probably changed three times since 2015 ;p | 20/06 21:22 |

pgiarrusso | carter: do you have numbers? inequality? Can you get Coq to accept your datatypes without too many hacks? | 20/06 21:54 |

pgiarrusso | the more yeses, the more likely is that Coq helps | 20/06 21:55 |

pgiarrusso | I'm sorry that's not a real answer | 20/06 21:55 |

pgiarrusso | dolio: Hi! you say 'But A -> B -> Set has things that aren't "relations".', but that seems confusing in a sense | 20/06 22:01 |

pgiarrusso | can't you read *all* members of A -> B -> Set as relations? | 20/06 22:02 |

dolio | In 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 |

dolio | Or all values of R a b are equal for each a and b. | 20/06 22:03 |

dolio | 'equal' | 20/06 22:03 |

dolio | Anyhow, the question is whether that fact is somehow essential to making computational parametricity work. | 20/06 22:04 |

pgiarrusso | dolio: 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 |

pgiarrusso | if *you* care about the difference, the internal parametricity function might not give you the proof you'd want | 20/06 22:04 |

dolio | I suspect it doesn't matter, either. | 20/06 22:06 |

pgiarrusso | dolio: are you familiar with Bernardy's parametricity transformation? because I'd strongly think that one does not require that equality | 20/06 22:06 |

pgiarrusso | oh yeah you mention it | 20/06 22:07 |

dolio | I know of it, but I haven't gotten around to reading the paper yet. :) | 20/06 22:07 |

pgiarrusso | what matters: for any term t of type T you can produce a proof term derive(t) that t satisfies the parametricity property for T | 20/06 22:08 |

pgiarrusso | and with arbitrary PTSs, IIRC, the parametricity property is produced with a related/the same transformation | 20/06 22:08 |

dolio | It 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 |

dolio | Because it's kind of doing the same thing as the function it's a proof about. | 20/06 22:09 |

pgiarrusso | that's already what happens | 20/06 22:09 |

dolio | Just shoving around indexed values instead of the base values. | 20/06 22:09 |

pgiarrusso | the proof term depends on the specific term, the same way the proof of parametricity is done by induction on terms | 20/06 22:09 |

pgiarrusso | dolio: let me dig the realizer showing id is parametric :-) | 20/06 22:10 |

carter | Ok so agda it is ;) | 20/06 22:12 |

dolio | Or, 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 |

dolio | And that obviously makes sense even if R isn't propositional. | 20/06 22:14 |

dolio | List is kind of its own lifting on 'relations'. | 20/06 22:15 |

pgiarrusso | dolio: OK, let's use Bernardy's transformation on T : β β¦ π x : T . x | 20/06 22:18 |

pgiarrusso | for 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 |

pgiarrusso | where idβ = π x : Tβ . x and idβ = π x : Tβ . x | 20/06 22:18 |

pgiarrusso | so, if your T' has multiple members, you'll get your particular witness back | 20/06 22:19 |

dolio | Right. | 20/06 22:19 |

pgiarrusso | dolio: You're right though in a different way: parametricity defines a *program equivalence* (though few will tell you) | 20/06 22:20 |

pgiarrusso | and for that it's essential that for all concrete types the relation is an equality | 20/06 22:20 |

dolio | The witness for parametricity of id is a fancy id, basically. | 20/06 22:20 |

pgiarrusso | having a single witness for it doesn't matter, being equality does | 20/06 22:20 |

pgiarrusso | dolio: yes | 20/06 22:20 |

pgiarrusso | and if you look at it and are familiar with derive, you might recognize it's very similar :-) | 20/06 22:21 |

pgiarrusso | dolio: 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 parametricity | 20/06 22:22 |

pgiarrusso | dolio: if you drop the requirement for equality (which is, technically, the identity extension lemma), you get generic "logical relations" proofs | 20/06 22:23 |

dolio | Okay, cool. | 20/06 22:24 |

pgiarrusso | the key theorem (the fundamental property or basic lemmas) says that all all terms are related to themselves, and is proved with the same strategy | 20/06 22:25 |

pgiarrusso | usually only for well-typed terms | 20/06 22:25 |

pgiarrusso | but with a bit more magic (like step-indexes), you can prove it for untyped languages as well | 20/06 22:26 |

pgiarrusso | I 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 |

dolio | Okay, thanks. | 20/06 22:27 |

dolio | I 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 |

pgiarrusso | dolio: please do tell | 20/06 22:29 |

pgiarrusso | BTW, 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 |

dolio | Well, the usual way to think about families T : A -> Set in category theory is as display maps T -> A. | 20/06 22:30 |

dolio | Where the latter T is like (Sigma A T) (with the former T), and the map is fst. | 20/06 22:31 |

dolio | But you can just consider any type with a map into A as a family over A. | 20/06 22:31 |

dolio | So, Nat-indexed families are maps into Nat. | 20/06 22:32 |

dolio | And 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 |

dolio | Which goes: (Nat -> Set) -> (Nat -> Set). | 20/06 22:36 |

dolio | But in category theory, it's still just 1+ with a sort of different interpretation. | 20/06 22:36 |

dolio | So 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 |

dolio | But 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 |

dolio | Which 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 |

dolio | Gotta go. | 20/06 22:39 |

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