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

[Joachim Breitner]

Hi,

I felt inspired to revive the free theorem calculator and gave it a new
home (and a modern, browser-only, FRP-based implementation):

http://free-theorems.nomeata.de/

which prints

   forall t1,t2 in TYPES, R in REL(t1,t2).
    forall (x, y) in lift{(,)}(id,R).
     (g_{t1} x, g_{t2} y) in lift{(,)}(id,R)

as the free theorem, which is (if one squints) the same as my 

  ∀ 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'))

Enjoy,
Joachim

Am Montag, den 23.07.2018, 10:56 -0700 schrieb 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
> > 
> > 
> > 
> > _______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180724/52f637f8/attachment.sig>