<div dir="ltr">Thank you, Joachim! I'm refreshing my memory of free theorem construction from that blog post. Regards, -- Conal<br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jul 23, 2018 at 8:33 AM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Conal,<br>
<span class=""><br>
Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:<br>
> Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case<br>
> that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f<br>
> a, b)`), perhaps as a free theorem for the type of `g`?<br>
<br>
</span>there used to be a free theorem calculator at<br>
<a href="http://www-ps.iai.uni-bonn.de/ft" rel="noreferrer" target="_blank">http://www-ps.iai.uni-bonn.de/<wbr>ft</a><br>
but it seems to be down :-(<br>
<br>
There is a shell client, ftshell, lets see what it says…<br>
it does not build with ghc-8.0 any more :-(<br>
<br>
Ah, but lambdabot understands @free:<br>
<br>
<nomeata>   @free g :: forall z. (A,z) -> (B,z)<br>
<lambdabot> $map_Pair $id f . g = g . $map_Pair $id f<br>
<br>
Which is basically what you are writing here:<br>
<span class=""><br>
> Note that `(A,)` and `(B,)` are functors and that `g` is a natural<br>
> transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.<br>
> Equivalently, `g . second h == second h . g` (where `second h (a,b) =<br>
> (a, h b)`).<br>
<br>
</span>Doesn’t that already answer the question? Let’s try to make it more<br>
rigorous. I define<br>
<br>
f :: A -> B<br>
f a = fst (g (a, ())<br>
<br>
and now want to prove that g = first f, using the free theorem… which<br>
is tricky, because the free theorem is actually not as strong as it<br>
could be; it should actually be phrased in terms of relations relation,<br>
which might help with the proof. <br>
<br>
So let me try to calculate the free theorem by hand, following<br>
<a href="https://www.well-typed.com/blog/2015/05/parametricity/" rel="noreferrer" target="_blank">https://www.well-typed.com/<wbr>blog/2015/05/parametricity/</a><br>
<br>
g is related to itself by the relation<br>
<br>
   [forall z. (A,z) -> (B,z)]<br>
<br>
and we can calculate<br>
<br>
  g [forall z. (A,z) -> (B,z)] g<br>
↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'<br>
↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'<br>
↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →<br>
      fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')<br>
↔ ∀ z z' Rz, ∀ a x x', x Rz x' →<br>
      fst (g (a,x)) = fst (g (a,x')) ∧<br>
snd (g (a,x)) Rz snd (g (a,x'))<br>
<br>
We can use this to show<br>
<br>
   ∀ (a,x :: z). fst (g (a,x)) = f a<br>
<br>
using (this is the tricky part that requires thinking)<br>
<br>
   z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()<br>
<br>
as then the theorem implies<br>
<br>
  fst (g (a,x)) = fst (g (a, ()) = f a.<br>
<br>
We can also use it to show <br>
<br>
   ∀ (a,x :: z). snd (g (a,x)) = x<br>
<br>
using<br>
<br>
   z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x<br>
<br>
as then the theorem implies, under the true assumption  x Rz z'<br>
<br>
  (snd (g (a,x))) Rz (snd (g (a,x')))<br>
  ↔ snd (g (a,x)) = x<br>
<br>
And from <br>
<br>
   ∀ (a,x :: z). fst (g (a,x)) = f a<br>
   ∀ (a,x :: z). snd (g (a,x)) = x<br>
<br>
we can conclude that<br>
<br>
  g = first f<br>
<br>
as intended.<br>
<br>
Cheers,<br>
Joachim<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
<br>
-- <br>
Joachim Breitner<br>
  <a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
  <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
</font></span></blockquote></div><br></div></div>