# Free theorem for `forall z. (A,z) -> (B,z)`? Classic List Threaded 9 messages Open this post in threaded view
|

## Free theorem for `forall z. (A,z) -> (B,z)`?

 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`?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)`).Thanks,  -- Conal _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: Free theorem for `forall z. (A,z) -> (B,z)`?

 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/ftbut 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:   @free g :: forall z. (A,z) -> (B,z) \$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   [hidden email]   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-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment
Open this post in threaded view
|

## Re: Free theorem for `forall z. (A,z) -> (B,z)`?

 Thank you, Joachim! I'm refreshing my memory of free theorem construction from that blog post. Regards, -- ConalOn 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:    @free g :: forall z. (A,z) -> (B,z) \$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   [hidden email]   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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: 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 <[hidden email]> 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: > > > >   @free g :: forall z. (A,z) -> (B,z) > > \$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   [hidden email]   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-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment
Open this post in threaded view
|

## Re: Free theorem for `forall z. (A,z) -> (B,z)`?

 >>>>> "JB" == Joachim Breitner <[hidden email]> writes: JB> I felt inspired to revive the free theorem calculator and gave it a new JB> home (and a modern, browser-only, FRP-based implementation): Thank you, Joachim! I've used that calculator often, and was sad to see it shut down. -- John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (671 bytes) Download Attachment
Open this post in threaded view
|

## Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Open this post in threaded view
|

## Re: Free theorem for `forall z. (A,z) -> (B,z)`?

 Hi, Am Dienstag, den 24.07.2018, 14:22 -0400 schrieb David Feuer: > Thank you! Are you going to add a place for auxiliary definitions? You wish is my command: https://github.com/nomeata/free-theorems-static-webui/commit/eb8e820Should be online in 10mins or so. > Perhaps also a few default definitions like lambdabot uses? What do you mean? It has this background theory: https://github.com/nomeata/free-theorems-static-webui/blob/master/src/KnownDeclarations.hs(copied from free-theorems-webui) > As it is, there doesn't seem to be a way to use non-Prelude to > constructors. That is fixed now, is it? > 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? Pull requests welcome :-) > 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? I guess I can use https://hackage.haskell.org/package/reflex-dom-0.3/candidate/docs/Reflex-Dom-Time.htmlfor this somehow. But I guess I only want to delay errors, not successes – I will give it a shot. Cheers, Joachim -- Joachim Breitner   [hidden email]   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-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment
 Hi, Am Dienstag, den 24.07.2018, 14:47 -0400 schrieb Joachim Breitner: > I guess I can use > https://hackage.haskell.org/package/reflex-dom-0.3/candidate/docs/Reflex-Dom-Time.html> for this somehow. But I guess I only want to delay errors, not > successes – I will give it a shot Sure, why not: https://github.com/nomeata/free-theorems-static-webui/commit/20c9acait seems to work. If some reflex-expert could check if this makes sense, that would be great: -- | Errors are delayed, but successes go through immediatelly delayError :: (PerformEvent t m, MonadHold t m, TriggerEvent t m, MonadIO (Performable m)) =>     Dynamic t (Either a b) -> m (Dynamic t (Either a b)) delayError d = do     delayedEvents <- delay 0.5 (updated d)     d' <- holdDyn Nothing (Just <\$> delayedEvents)     return \$ do         now <- d         past <- d'         return \$ case (past, now) of             (Nothing, _)     -> now    -- before any delayed events arrive             (_, Right _ )    -> now  -- current value is good             (Just x, Left _) -> x -- current value is bad, delay Cheers, Joachim -- Joachim Breitner   [hidden email]   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-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment