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

[David Feuer]

Thank you! Are you going to add a place for auxiliary definitions? Perhaps
also a few default definitions like lambdabot uses? As it is, there doesn't
seem to be a way to use non-Prelude to constructors. One more thing, that
was missing from the original: a good explanation of what the output means.
"lift" is particularly mysterious. Lambdabot seems to replace these with
calls to normal Haskell functions. Perhaps that can be done sometimes? One
last thing: the FRP interface seems a bit *too* responsive. It's not fun to
see error messages flashing on and off as I type. Perhaps it would make
sense to add a delay before activating one of those?

On Tue, Jul 24, 2018, 1:38 PM Joachim Breitner <mail at joachim-breitner.de>
wrote:

> 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/
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180724/565230cb/attachment.html>