[Haskell-cafe] Free theorem for `forall z. (A,z) -> (B,z)`?

[Conal Elliott]

Thank you, Joachim! I'm refreshing my memory of free theorem construction
from that blog post. Regards, -- Conal

On Mon, Jul 23, 2018 at 8:33 AM, Joachim Breitner <mail at joachim-breitner.de>
wrote:

> Hi Conal,
>
> Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:
> > Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case
> > that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f
> > a, b)`), perhaps as a free theorem for the type of `g`?
>
> there used to be a free theorem calculator at
> http://www-ps.iai.uni-bonn.de/ft
> but it seems to be down :-(
>
> There is a shell client, ftshell, lets see what it says…
> it does not build with ghc-8.0 any more :-(
>
> Ah, but lambdabot understands @free:
>
> <nomeata>   @free g :: forall z. (A,z) -> (B,z)
> <lambdabot> $map_Pair $id f . g = g . $map_Pair $id f
>
> Which is basically what you are writing here:
>
> > Note that `(A,)` and `(B,)` are functors and that `g` is a natural
> > transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
> > Equivalently, `g . second h == second h . g` (where `second h (a,b) =
> > (a, h b)`).
>
> Doesn’t that already answer the question? Let’s try to make it more
> rigorous. I define
>
> f :: A -> B
> f a = fst (g (a, ())
>
> and now want to prove that g = first f, using the free theorem… which
> is tricky, because the free theorem is actually not as strong as it
> could be; it should actually be phrased in terms of relations relation,
> which might help with the proof.
>
> So let me try to calculate the free theorem by hand, following
> https://www.well-typed.com/blog/2015/05/parametricity/
>
> g is related to itself by the relation
>
>    [forall z. (A,z) -> (B,z)]
>
> and we can calculate
>
>   g [forall z. (A,z) -> (B,z)] g
> ↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'
> ↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'
> ↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →
>       fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')
> ↔ ∀ z z' Rz, ∀ a x x', x Rz x' →
>       fst (g (a,x)) = fst (g (a,x')) ∧
> snd (g (a,x)) Rz snd (g (a,x'))
>
> We can use this to show
>
>    ∀ (a,x :: z). fst (g (a,x)) = f a
>
> using (this is the tricky part that requires thinking)
>
>    z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()
>
> as then the theorem implies
>
>   fst (g (a,x)) = fst (g (a, ()) = f a.
>
> We can also use it to show
>
>    ∀ (a,x :: z). snd (g (a,x)) = x
>
> using
>
>    z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x
>
> as then the theorem implies, under the true assumption  x Rz z'
>
>   (snd (g (a,x))) Rz (snd (g (a,x')))
>   ↔ snd (g (a,x)) = x
>
> And from
>
>    ∀ (a,x :: z). fst (g (a,x)) = f a
>    ∀ (a,x :: z). snd (g (a,x)) = x
>
> we can conclude that
>
>   g = first f
>
> as intended.
>
> Cheers,
> Joachim
>
>
>
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180723/e9e517a1/attachment.html>