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

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 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@joachim-breitner.de http://www.joachim-breitner.de/