The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van Laarhoven representation of isomorphisms uses this representation of a pair of function to capture the notion of an isomorphism.

Given a value of type ∀ f, g : Functor. (g a → f b) → g s → f t, the normal way of extracting the two components is to instantiate the value twice using Identity and Constant functors.

extractPair :: (forall f g. (Functor f, Functor g) => (g a -> f b) -> g s -> f t)
-> (s -> a, b -> t)
extractPair l = (getConstant . (l (Constant . runIdentity)) . Identity
,runIdentity . (l (Identity . getConstant)) . Constant)

However, it is possible to extract the two components in one shot.

data PStore i j x = PStore {peek :: j -> x, pos :: i}
instance Functor (PStore i j) where
fmap f (Pstore h i) = PStore (f . h) i
extractPair :: (((s -> a) -> PStore (s -> a) b b) -> (s -> s) -> PStore (s -> a) b t)
-> (s -> a, b -> t)
extractPair l = (f, g)
where
PStore g f = l (PStore id) id

There has been some debate for some time as to whether there should be a superclass for Applicative with just the pure function should exist:

-- Natural law:
-- fmap f . pure = pure . f
class Functor f => Pointed f where
pure :: a -> f a

The charge laid against this class is that there are no laws for this single function beyond the single law that is naturally implied. Compare this to a more reasonable class

-- Natural laws:
-- distRight . right . fmap f = fmap (right f) . distRight
-- distRight . left f = fmap (left f) . distRight
--
-- Other laws:
-- 1. either absurd (fmap Right) = distRight :: Either Void (f a) -> f (Either Void a)
-- 2. fmap assocL . distRight . right distRight . assocR = distRight :: Either (Either a b) (f c) -> f (Either (Either a b) c)
-- where
-- assocL :: Either a (Either b c) -> Either (Either a b) c
-- assocL (Left a) = Left (Left a)
-- assocL (Right (Left a)) = Left (Right a)
-- assocL (Right (Right a)) = Right a
-- assocR :: Either (Either a b) c -> Either a (Either b c)
-- assocR (Left (Left a)) = Left a
-- assocR (Left (Right a)) = Right (Left a)
-- assocR (Right a) = Right (Right a)
class Functor f => StrongSum f where
distRight :: Either a (f b) -> f (Either a b)
distLeft :: Either (f a) b -> f (Either a b)
distLeft = fmap switch . distRight . switch
where
switch :: Either a b -> Either b a
switch = Right ||| Left

StrongSum is a honest class with two additional real laws in addition to its natural laws. No one would object to creating and using such a class.

What if I told you that Pointed and StrongSum are in fact the same class?

class Functor f => Pointed f where
pure :: a -> f a
pure = fmap (id ||| absurd) . distRight . Left
distRight : Either a (f b) -> f (Either a b)
distRight = either (fmap Left . pure) (fmap Right)

Theorem 1. If we define pure, then the distRight automatically satisfies the 2 required laws.

Proof. Law 1:

either absurd (fmap Right)
= { extensionality of absurd }
either (fmap Left . pure) (fmap Right)
= { definition in terms of pure }
distRight :: Either Void (f a) -> f (Either Void a)

Law 2:
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR = either (fmap Left . pure) (fmap Right)

case 1: Right x

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Right x
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Right (Right x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (either (fmap Left . pure) (fmap Right) (Right x))
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (fmap Right x)
=
fmap assocL $ fmap Right (fmap Right x)
=
fmap (assocL . Right . Right) x
=
fmap Right x
=
either (fmap Left . pure) (fmap Right) $ Right x

case 2: Left (Right x)

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Left (Right x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Right (Left x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (either (fmap Left . pure) (fmap Right) (Left x))
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (fmap Left (pure x))
=
fmap assocL $ fmap Right (fmap Left (pure x))
=
fmap (assocL . Right . Left) (pure x)
=
fmap (Left . Right) (pure x)
=
fmap Left . fmap Right . pure $ x
=
fmap Left . pure . Right $ x
=
fmap Left . pure $ Right x
=
either (fmap Left . pure) (fmap Right) $ Left (Right x)

case 3: Left (Left x)

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Left (Left x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Left x
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Left x
=
fmap assocL . fmap Left . pure $ x
=
fmap (assocL . Left) . pure $ x
=
fmap (Left . Left) . pure $ x
=
fmap Left . fmap Left . pure $ x
=
fmap Left . pure . Left $ x
=
fmap Left . pure $ Left x
=
either (fmap Left . pure) (fmap Right) $ Left (Left x)

Theorem 2. If we define pure, then pure = fmap (id ||| absurd) . distRight . Left where distRight = either (fmap Left . pure) (fmap Right)

Proof.

fmap (id ||| absurd) . distRight . Left
=
fmap (id ||| absurd) . either (fmap Left . pure) (fmap Right) . Left
=
fmap (id ||| absurd) . fmap Left . pure
=
fmap ((id ||| absurd) . Left) . pure
=
fmap id . pure
=
pure

Theorem 3. If we define distRight such that distRight satisfies its two laws then distRight = either (fmap Left . pure) (fmap Right) where pure = fmap (id ||| absurd) . distRight . Left.

Proof. either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right) = distRight

case 1: Left x

either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right) $ Left x
=
fmap Left . fmap (id ||| absurd) . distRight $ Left x
=
fmap (Left . (id ||| absurd)) $ distRight (Left x)
=
fmap (Left ||| (Left . absurd)) $ distRight (Left x)
=
fmap (Left ||| absurd) $ distRight (Left x)
= { extensionality of absurd }
fmap (Left ||| Right) $ distRight (Left x)
=
fmap id $ distRight (Left x)
=
distRight (Left x)

case 2: Right x

either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right) $ Right x
=
fmap Right x
=
fmap (left absurd . Right) x
=
fmap (left absurd) $ fmap Right x
=
fmap (left absurd) . either absurd (fmap Right) $ Right x
= { Law 1 for distRight }
fmap (left absurd) . distRight $ Right x
= { Natural law for distRight }
distRight . left absurd $ Right x
=
distRight $ Right x

Interestingly we only ever used the first law for distRight. By composing these proofs together we should be able to show that the second law for distRight holds whenever the first law does.

In conclusion we have seen that the StrongSum class and the Pointed class are equivalent classes. The pure function contains the heart of what a law abiding distRight function is, such that whenever we have a law abiding distRight function it can be written in terms of pure and every instance of pure yields a law abiding distRight function. Given that I think people would welcome a StrongSum class, it only makes sense to equally welcome the Pointed class.

James Deikun (known as xplat on freenode) and I discovered a new kind of Optic today. If not discovered, then at least characterized it.

We know that lenses correspond to optics over strong profunctors, and prisms correspond to optics over choice profuctors. The open question was, what corresponds to optics over closed profuctors?

> -- Natural laws for closed profunctors:
> -- closed . dimap l r = dimap (closed . l) (closed . r) . closed
> -- rmap (lmap f) . closed = lmap (lmap f) . closed
> -- Other laws for closed profunctors:
> -- dimap ($ ()) const = closed :: p a b -> p (() -> a) (() -> b)
> -- dimap curry uncurry . closed . closed = closed :: p a b -> p ((x,y) -> a) ((x,y) -> b)
> class Profunctor p => Closed p where
> closed :: p a b -> p (x -> a) (x -> b)
>
> instance Closed (->) where
> closed = (.)

After all, closed profunctors are a very nice class of profunctors. They let you lift a profunctor through any Naperian container. A Naperian container (also known as a representable functor) is a container with a fixed shape. If it is finitary then it is a fixed length vector, but Naperian containers can also be of infinite size. The identity container is Naperian, and Naperian containers are closed under composition.
Until Edward Kmett comes up with a better name, let's call this new optic a Grate:

∀ P:Closed. P a b -> P s t

From the last post we saw that this is isomorphic to the free closed profunctor generated by Iso(a,b) s t := (s -> a)×(b -> t).

∀ P:Closed. P a b -> P s t
≅
FreeClosed Iso(a,b) s t

And by generalizing the pattern we saw in Pastro and co-Pastro for strong and choice profunctors, we anticipate we can define FreeClosed as follows.

FreeClosed p s t := ∃ x y z. (s -> (z -> x)) × p x y × ((z -> y) -> t)

This is known as Enviroment in the profunctor library. Applying this to Iso(a,b), we can simplify to get the normal form of the type for Grates.

∀ P:Closed. P a b -> P s t
≅
FreeClosed Iso(a,b) s t
=
∃ x y z. (s -> (z -> x)) × Iso(a,b) x y × ((z -> y) -> t)
≅ [flip]
∃ x y z. (z -> (s -> x)) × Iso(a,b) x y × ((z -> y) -> t)
≅ [co-yoneda]
∃ x y. Iso(a,b) x y × (((s -> x) -> y) -> t)
=
∃ x y. (x -> a) × (b -> y) × (((s -> x) -> y) -> t)
≅ [co-yoneda]
∃ y. (b -> y) × (((s -> a) -> y) -> t)
≅ [contravariant co-yoneda]
((s -> a) -> b) -> t

For our exploration, we will take this normal form as the definition of a Grate (though, of course, in a profuctor optical library we would use the closed optic defininition).

> type Grate s t a b = ((s -> a) -> b) -> t

Still, this object seems pretty opaque. At least it was to me. The Grate optic sits between isomorphisms and semantic editor combinators. Given a Grate from s to a we can modify the a's.

> modGrate :: Grate s t a b -> (a -> b) -> (s -> t)
> modGrate grate adj s = grate (\get -> adj (get s))

And every isomorphism is a grate.

> isoToGrate :: (s -> a) -> (b -> t) -> Grate s t a b
> isoToGrate get beget build = beget (build get)

But what is the fundamental operation that Grates can do? What can we do with Naperian containers that we cannot do with other types of containers? James figured out that we can zip two Naperian containers.

> zipWithOf :: Grate s t a b -> (a -> a -> b) -> (s -> s -> t)
> zipWithOf grate op s1 s2 = grate (\get -> get s1 `op` get s2)

For example, if we consider the triple Naperian container,

> data Triple a = Triple a a a

we can build a Grate for it.

> tripleGrate :: Grate (Triple a) (Triple b) a b
> tripleGrate build = Triple (build one) (build two) (build three)
> where
> one (Triple x y z) = x
> two (Triple x y z) = y
> three (Triple x y z) = z

> zip3WithOf :: Grate s t a b -> (a -> a -> a -> b) -> (s -> s -> s -> t)
> zip3WithOf grate comb s1 s2 s3 = grate (\get -> comb (get s1) (get s2) (get s3))

including zip0WithOf which is better known as review, but I like to call beget.

> beget :: Grate s t a b -> b -> t
> beget grate b = grate (const b)
λ> beget tripleGrate 0
Triple 0 0 0

If fact, James noted we can zip over an entire functors worth of values.

> zipFWithOf :: Functor f => Grate s t a b -> (f a -> b) -> (f s -> t)
> zipFWithOf grate comb fs = grate (\get -> comb (fmap get fs))
λ> zipFWithOf tripleGrate sum [Triple 1 2 3, Triple 4 5 6, Triple 7 8 9]
Triple 12 15 18
λ> zipFWithOf tripleGrate id [Triple 1 2 3, Triple 4 5 6, Triple 7 8 9]
Triple [1,4,7] [2,5,8] [3,6,9]

This is essentially all we can do because Grate s t a b and ∀ F:Functor. (F a -> b) -> (F s -> t) are isomorphic. We can show this using the same technique from a representation theorem for second-order functionals.

∀ F:Functor. (F a -> b) -> (F s -> t)
≅ [ flip ]
∀ F:Functor. F s -> (F a -> b) -> t
≅ [ yoneda ]
∀ F:Functor. (∀ c. (s -> c) -> F c) -> (F a -> b) -> t
= [ definition of natural transformation ]
∀ F:Functor. (((->) s) :~> F) -> (F a -> b) -> t
≅ [ higher-order yoneda]
((->) s a -> b) -> t
=
((s -> a) -> b) -> t
=
Grate s t a b
> -- unzipFWithOf :: (forall F. Functor F => (F a -> b) -> F s -> t) -> Grate s t a b
> unzipFWithOf :: (((s -> a) -> b) -> (s -> s) -> t) -> Grate s t a b
> unzipFWithOf f = flip f id

That makes Functor F => (F a -> b) -> F s -> b the van Laarhoven represenation of Grates, or the type of "van Laarhoven Grates" for short. Unexpectedly, the van Laarhoven form of Grates is probably the easiest of our three representation of Grates to comprehend.

Profunctor Grates: Closed p => p a b -> p s t

Van Laarhoven Grates: Functor F => (F a -> b) -> (F s -> t)

Normal Grates: ((s -> a) -> b) -> t

Of course, we have the usual optical laws for Grates. For example, given a van Laarhoven Grate, grate :: Functor F => (F a -> b) -> (F s -> t) we expect the following to hold.

grate runIdentity = runIdentity

grate (g . fmap f . getCompose) = grate g . fmap (grate f) . getCompose

The title of this post does not actually make sense; it is a joke based on the title of a recently published paper of Jaskelioff and myself.
Here I will show that the same deduction found in that paper can be applied to the profunctor representation of lenses and other optics.
This came out of some recent discussions I had with Bartosz Milewski.

I will use the language of Haskell, but be warned, I have not run this code through a compiler to typecheck it.

> -- The usual laws:
> -- 1) dimap id id = id
> -- 2) dimap l1 r1 . dimap l2 r2 = dimap (l2 . l1) (r1 . r2)
> class Profunctor p where
> dimap :: (s -> a) -> (b -> t) -> p a b -> p s t
> lmap :: (s -> a) -> p a t -> p s t
> lmap l = dimap l id
> rmap :: (b -> t) -> p s b -> p s t
> rmap r = dimap id r
>
> instance Profunctor (->) where
> dimap l r f = r . f . l
>
> -- Iso(a,b) s t := (s -> a) × (b -> t)
> data Iso a b s t = Iso (s -> a) (b -> t)
>
> instance Profunctor (Iso a b) where
> dimap l r (Iso f g) = Iso (f . l) (r . g)
>
> type p :~> q = forall x y. p x y -> q x y

As usual, by two applications of Yoneda we have

∀ P:Profunctor. P a b -> P s t
≅ [Yoneda for profunctors]
∀ P:Profunctor. (∀ c d. ((c -> a)×(b -> d)) -> P c d) -> P s t
= [Definition of Iso]
∀ P:Profunctor. (∀ c d. Iso(a,b) c d -> P c d) -> P s t
= [Definition of :~>]
∀ P:Profunctor. (Iso(a,b) :~> P) -> P s t
≅ [Higher-order Yoneda]
Iso(a,b) s t

Say * ⊣ U is some adjuction between profunctors.
For example, consider * ⊣ U as the free strong profunctor functor / forgetful functor, or as the free choice profunctor functor / forgetful functor.
For now let us focus on Free Strong Profuctors.

> -- Natural laws for Strong profunctors:
> -- first . dimap l r = dimap (first l) (first r) . first
> -- rmap (second f) . first = lmap (second f) . first
> --
> -- Other laws:
> -- 1) dimap fst (,()) = first :: p a b -> p (a,()) (b, ())
> -- 2) dimap assocL assocR . first . first = first :: p a b -> p (a,(x,y)) (b,(x,y))
> -- where
> assocL (a,(x,y)) = ((a,x),y)
> assocR ((a,x),y) = (a,(x,y))
>
> class Profunctor p => Strong p where
> first :: p a b -> p (a, c) (b, c)
> second :: p a b -> p (c, a) (c, b)
> second = dimap swap swap . first
>
> instance Strong (->) where
> first f (a, c) = (f a, c)

By combining Yondea with the adjuction we get the following.

∀ P:Strong. UP a b -> UP s t
≅ [Yoneda for profunctors]
∀ P:Strong. (∀ c d. ((c -> a)×(b -> d)) -> UP c d) -> UP s t
= [Definition of Iso]
∀ P:Strong. (∀ c d. Iso(a,b) c d -> UP c d) -> UP s t
= [Definition of :~>]
∀ P:Strong. (Iso(a,b) :~> UP) -> UP s t
≅ [Adjunction]
∀ P:Strong. (Iso(a,b)* :~> P) -> UP s t
≅ [Higher-order Yoneda]
U(Iso(a,b)*) s t

Now all that remains is to show that the free strong profunctor generated by Iso(a,b) is what we want. In otherwords, we want to show that
Iso(a,b)* s t ≅ (s -> a) × (b -> s -> t), and similarly for free choice profunctors.

I am not sure what the best way of proving things are free, but I will provide unit and counits here. The case for free strong profuctors is particularly nice.

> diag :: a -> (a, a)
> diag x = (x, x)
>
> eval :: (b -> c, b) -> c
> eval (f, b) = f b
>
> newtype FreeStrong p s t = FreeStrong (p s (s -> t))
>
> instance Profunctor p => Profunctor (FreeStrong p) where
> dimap l r (FreeStrong p) = FreeStrong (dimap l (dimap l r) p)
>
> instance Profunctor p => Strong (FreeStrong p) where
> first (FreeStrong p) = FreeStrong (dimap fst first p)
>
> mapFreeStrong :: (Profunctor p, Profunctor q) => (p :~> q) -> (FreeStrong p :~> FreeStrong q)
> mapFreeStrong eta (FreeStrong p) = FreeStrong (eta p)
>
> unit :: Profunctor p => p :~> FreeStrong p
> unit p = FreeStrong (rmap const p)
>
> -- counit :: Strong p => FreeStrong p :~[preserving strength]~> p
> counit :: Strong p => FreeStrong p :~> p
> counit (FreeStrong p) => dimap diag eval (first p)

counit (mapFreeStrong unit (FreeStrong p))
=
counit (FreeStrong (unit p))
=
dimap diag eval (first (unit p))
=
dimap diag eval (first (FreeStrong (rmap const p)))
=
dimap diag eval (FreeStrong (dimap fst first (rmap const p)))
=
FreeStrong (dimap diag (dimap diag eval) (dimap fst first (rmap const p))))
= [ dimap compositions ]
FreeStrong (dimap (fst . diag) (dimap diag eval . first . const) p)
= [ fst . diag = id && Lemma 3 ]
FreeStrong (dimap id id p)
= [ dimap id law ]
FreeStrong p
Lemma 3: dimap diag eval (first (const f))
= \x -> dimap diag eval (first (const f)) x
= \x -> eval (first (const f) (diag x))
= \x -> eval (first (const f) (x,x))
= \x -> eval (const f x,x)
= \x -> eval (f, x)
= \x -> f x
= f

Proof of map-counit-unit law:

counit (unit p)
=
counit (FreeStrong (rmap const p))
=
dimap diag eval (first (rmap const p))
= [ natural law for strength ]
dimap diag eval (rmap (first const) (first p))
= [ dimap compositon ]
dimap diag (eval . first const) (first p)
= [ eval (first const (x,y)) = eval (const x, y) = const x y = x = fst (x,y) ]
dimap diag fst (first p)
= [ fst (x,y) = x = fst (x,f y) = fst (second f (x,y))]
dimap diag (fst . second (const ())) (first p)
= [ uncompose dimap ]
dimap diag fst (rmap (second (const ())) (first p))
= [ natural law for strength ]
dimap diag fst (lmap (second (const ())) (first p))
= [ compose dimap ]
dimap (second (const ()) . diag) fst (first p)
= [ second (const ()) (diag x) = second (const ()) (x,x) = (x, const () x) = (x,()) = (,()) x ]
dimap (,()) fst (first p)
= [ strength law 1 ]
dimap (,()) fst (dimap fst (,()) p)
= [ dimap composition ]
dimap (fst . (,())) (fst . (,())) p
=
dimap id id p
= [ dimap id ]
p

In conclusion we have

FreeStrong (Iso a b) s t
=
Iso a b s (s -> t)
=
(s -> a, b -> s -> t)

as required.

The case for choice profunctors is a little harder because there is no simple construction for creating a free choice profuctor from a profuctor by subsitution (I assume we would need a co-exponential to make it easy).
Still, I do not doubt that we can show that the free choice profunctor generated from Iso a b is FreeChoice Iso(a,b) s t ≅ (s -> (Either a t), b -> t).

At the bottom of the optical hierarchy rests the humble Semantic Editor
Combinator (SEC) also known as a Setter, which denotes an isomorphism between sₓ and F(aₓ) for
some Functor F. The types s and a are possibly parametrized which we indicate
by a subscript x.
The rest of the mainline optical hierarchy consists of various refinements of the class of functors being quantified over.

SEC

::

∃ F: Functor. sₓ ~ F(aₓ)

Traversal

::

∃ F: FinitaryContainer. sₓ ~ F(aₓ)

AffineTraversal

::

∃ c₀ c₁. sₓ ~ c₀ + c₁ × aₓ

Prism

::

∃ c₀ . sₓ ~ c₀ + aₓ

Lens

::

∃ c₁. sₓ ~ c₁ × aₓ

Iso

::

sₓ ~ aₓ

For lenses and prisms the functors are of the form (c₁×) and (c₀+) respectively for some residual type.
At the top of the hierarchy we have ‘Iso’, where we are quantifying over only the Identity functor, so the existential appears to disappear.
All these classes of functors are closed under composition, though I am not sure how important this fact is.

To build profunctor implementations of these optics, we add additional methods that allow profunctors to be lifted through these various classes of functors

> class Profunctor p where
> dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
> class Profunctor p => Strong p where
> first :: p a b -> p (a, c) (b, c)
> second :: p a b -> p (c, a) (c, b)
> second = dimap swap swap . first
> where
> swap (a,b) = (b,a)
> class Profunctor p => Choice p where
> left :: p a b -> p (Either a c) (Either b c)
> right :: p a b -> p (Either c a) (Either c b)
> right = dimap switch switch . left
> where
> switch (Left x) = Right x
> switch (Right y) = Left y
> class (Choice p, Strong p) => Step p where
> step :: p a b -> p (Either c (a,d)) (Either c (b,d))
> step = right . first
> class Step p => Walk p where
> walk :: Traversable f => p a b -> p (f a) (f b)

> class Walk p => Settable p where
> mapping :: Functor f => p a b -> p (f a) (f b)

The profunctor implementation of the optical hierarchy quantifies over these various extensions of profunctors

> type Optic p s t a b = p a b -> p s t
> type Iso s t a b = forall p. Profunctor p => Optic p s t a b
> type Lens s t a b = forall p. Strong p => Optic p s t a b
> type Prism s t a b = forall p. Choice p => Optic p s t a b
> type AffineTraversal s t a b = forall p. Step p => Optic p s t a b
> type Traversal s t a b = forall p. Walk p => Optic p s t a b
> type SEC s t a b = forall p. Settable p => Optic p s t a b

Now we want to show that these optics actually correspond to their canonical definitions.
The functions below are all isomorphisms, but I will only give the hard directions for now.

> iso :: forall s t a b. (s -> a) -> (b -> t) -> Iso s t a b
> iso = dimap
> lens :: forall s t a b. (s -> a) -> (s -> b -> t) -> Lens s t a b
> lens f g = dimap (f &&& id) (uncurry $ flip g) . first
> prism :: forall s t a b. (s -> Either t a) -> (b -> t) -> Prism s t a b
> prism f g = dimap f (either id g) . right
> affineTraversal :: forall s t a b. (s -> Either t a) -> (s -> b -> t) -> AffineTraversal s t a b
> affineTraversal f g = dimap from (either id (uncurry $ flip g)) . right . first
> where
> from :: s -> Either t (a,s)
> from s = (id +++ (,s)) (f s)
> traversal :: forall s t a b. (forall f. Applicative f => (a -> f b) -> s -> f t) -> Traversal s t a b
> traversal f = dimap (Rotate . from) (to . unrotate) . walk
> where
> from :: s -> PKStore a b t
> from = f (Battery (Unit id))
> to :: PKStore b b t -> t
> to = extract
> sec :: forall s t a b. ((a -> b) -> s -> t) -> SEC s t a b
> sec f = dimap from to . mapping
> where
> from :: s -> PStore s a a
> from = PStore id
> to :: PStore s a b -> t
> to (PStore g s) = f g s

The sec solution places the argument f on the to side, while the traversal places the argument f on the from side.
I suspect there is lots of wiggle room to slide f from one side to the other side.
I also suspect that there are much more elegant solutions to traversal and sec, possibly using different characterizations of the Walk and Settable classes.

This just leaves Views and Reviews, which are created my making one of the two variables of a profunctor into a phantom variable.

> class Strong p => PhantomR p where
> contrarmap :: (b -> a) -> p c a -> p c b
> coerceRight :: p c a -> p c b
> coerceRight = dimap id absurd . contrarmap absurd
>
> firstDefault :: PhantomR p => p a b -> p (a,c) (b,c)
> firstDefault = coerceRight . dimap fst id
> class Choice p => PhantomL p where
> colmap :: (a -> b) -> p a c -> p b c
> coerceLeft :: p a c -> p b c
> coerceLeft = colmap absurd . dimap absurd id
>
> leftDefault :: PhantomL p => p a b -> p (Either a c) (Either b c)
> leftDefault = coerceLeft . dimap id Left
> type View s t a b = forall p. PhantomR p => Optic p s t a b
> type Review s t a b = forall p. PhantomL p => Optic p s t a b
> view :: forall s t a b. (s -> a) -> View s t a b
> view f = coerceRight . dimap f id
> review :: forall s t a b. (b -> t) -> Review s t a b
> review f = coerceLeft . dimap id f

This file is effectively a copy of part of bennofs's profunctor lenses library.
He is the one who figured out how to implement 'sec', which I had no idea how to do and thought was impossible.
His library is more extensive and is in turn based on his many discussions on the #haskell-lens channel on freenode.
Once he demonstrated to me that sec was in fact possible, I felt that travesal must be possible.
The trick was noticing that PKStore i j a is applicative in its third argument and traversable in its first argument.
This lets us use the PKStore functor in both contexts.

Edward Kmett hinted to me that all this is known and has been derived many times (but nobody told me).
Readers should work under the assumption that everything presented here is not novel and I am simply writing this down for me so that when I do build a profunctor based optics library in the future, I can reference it.

Nothing in this post is tested, none of the laws for the classes have been presented, and I have no proofs that anything is correct.
All I know is that it all typechecks, so it is probably close to correct.

> newtype Void = Void Void
>
> absurd :: Void -> a
> absurd (Void x) = absurd x
>
> data PStore i j x = PStore (j -> x) i
>
> instance Functor (PStore i j) where
> fmap f (PStore g i) = PStore (f . g) i

> data PKStore i j x = Unit x
> | Battery (PKStore i j (j -> x)) i
>
> instance Functor (PKStore i j) where
> fmap f (Unit x) = Unit (f x)
> fmap f (Battery g i) = Battery (fmap (f .) g) i
>
> instance Applicative (PKStore i j) where
> pure = Unit
> Unit x <*> c = fmap x c
> Battery g i <*> c = Battery (flip <$> g <*> c) i
>
> newtype RotatePKStore j x i = Rotate { unrotate :: PKStore i j x }
>
> instance Functor (RotatePKStore j x) where
> fmap f (Rotate (Unit x)) = Rotate (Unit x)
> fmap f (Rotate (Battery g i)) = Rotate (Battery (unrotate (fmap f (Rotate g))) (f i))
>
> -- I am not 100% certain that the Foldable and Traversable instances are not reversed.
> instance Foldable (RotatePKStore j x) where
> foldMap f (Rotate (Unit x)) = mempty
> foldMap f (Rotate (Battery g i)) = f i <> foldMap f (Rotate g)
>
> instance Traversable (RotatePKStore j x) where
> traverse f (Rotate (Unit x)) = pure (Rotate (Unit x))
> traverse f (Rotate (Battery g i)) = Rotate <$> (f i <**> (Battery . unrotate <$> traverse f (Rotate g)))
>
> extract :: PKStore i i x -> x
> extract (Unit x) = x
> extract (Battery g i) = extract g i

shachaf taught me prisms today! Here is what I learned.

A prism is dual to the notion of lens. A lens lets you access a field of a record by letting you get and set its value. A prism lets you access a component of a sum by letting you beget and match the component. Lenses are composable, letting you access fields inside deeply nested records. Prisms are composable, letting you access components of deep hierarchy of sums.

For example, you may have a large hierarchy of exception types. Using prisms you can compose together the basic prisms that reference components from one level of your hierarchy to the next. The composite prism will let you make an exception by injecting the contents of your specific exception and generating an object of your top level exception type. On the flip side, you can also use the prism to match and catch a specific subtype of exceptions at a particular level of your hierarchy and automatically re-throw exceptions that do not match. Thus prisms can let you have your statically typed extensible exception mechanism without the pain. You can even make prisms that allow you to make and match virtual exception types that aren't part of your concrete representation, just like you can use make lenses to access virtual fields of your records that are not actual concrete fields of your records.

A lens a b type is an abstract representation of ∃c. a ~ b×c, while a prism a b is an abstract representation of ∃c. a ~ b+c.

The simple concrete implementation of a prism has two components: beget and match.

data Prism a b = Prism { beget :: b -> a, match :: a -> Either a b }

An example of a prism is the value held in a Maybe type:

_just :: Prism (Maybe a) a
_just = Prism {beget = Just; match = maybe (Left Nothing) Right}

There are three laws for prisms which are dual to the three laws for lens. Given a prism, p, we require:

1. match p . beget p === Right
2. id ||| (beget p) . match p === id
3. left (match p) . match p === left Left . match p

To help see the duality, consider the following definition of a lens.

data Lens a b = Lens { get :: a -> b, set :: (a,b) -> a }

Given a lens, l, we can write the lens laws as:

1. get l . set l = snd
2. set l . (id &&& get l) = id
3. set l . first (set l) = set l . first fst

which admittedly is quite awkward, but it makes the duality apparent.

I am not yet aware of any nice, algebra or coalgebra representation of prisms, but there is a van Laarhoven representation of prisms.

class Functor f => Costrong f where
costrength :: f (Either a b) -> Either a (f b)
type PrismVL a b = forall g f. (Costrong g, Pointed f) => (g b -> f b) -> g a -> f a

The van Laarhoven representation of a prism family is straightforward.

We can build a PrismVL from a Prism.

toVL :: Prism a b -> PrismVL a b
toVL p f = either pure (fmap (beget p) . f) . costrength . fmap (match p)

In reverse, we can convert a Prism to a PrismVL.

instance Costrong (Const b) where
costrength (Const x) = Right (Const x)
instance Costrong Identity where
costrength (Identity x) = right Identity x
fromVL :: PrismVL a b -> Prism a b
fromVL vlp = Prism begetVL matchVL
where
begetVL = runIdentity . vlp (Identity . getConst) . Const
matchVL = (Right ||| Left) . vlp (Left . runIdentity) . Identity

We can check that fromVL . toVL === id by letting vlp = toVL p in

begetVL x = runIdentity . vlp (Identity . getConst) $ Const x
= runIdentity . toVL p (Identity . getConst) $ (Const x)
= runIdentity . either pure (fmap (beget p) . Identity . getConst) . costrength . fmap (match p) $ (Const x)
= runIdentity . either pure (fmap (beget p) . Identity . getConst) . costrength $ (Const x)
= runIdentity . either pure (fmap (beget p) . Identity . getConst) $ Right (Const x)
= runIdentity (fmap (beget p) . Identity . getConst $ Const x)
= runIdentity (fmap (beget p) . Identity $ x)
= runIdentity (Identity (beget p x))
= beget p x
matchVL x = (Right ||| Left) . vlp (Left . runIdentity) $ Identity x
= (Right ||| Left) . toVL p (Left . runIdentity) $ Identity x
= (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) . costrength . fmap (match p) $ Identity x
= (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) . costrength $ Identity (match p x)
= (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) $ right Identity (match p x)
= (Right ||| Left) $ either pure (fmap (beget p) . Left . runIdentity . Identity) (match p x)
= (Right ||| Left) $ either pure (fmap (beget p) . Left) (match p x)
= either (fmap (beget p) . Left) pure (match p x)
= either Left Right (match p x)
= match p x

To check that toVL . fromVL === id will likely require some heavy use of parametricity theorems, so I will leave that for later.

Lastly I expect that the prism laws in the van Laarhoven representation to something nice. Probably

(* This files proves that the Identity and Composition laws of traversals
are equivalent to the laws of coalgebroid for an indexed Kleene store comonad.
Assumptions:
- functional extensionality
- an instance of a parametricity law
*)
Require Import FunctionalExtensionality.
Set Implicit Arguments.
Unset Strict Implicit.
Record Applicative := applicative
{ carrier :> Type -> Type
; pure : forall a, a -> carrier a
; ap : forall a b, carrier (a -> b) -> carrier a -> carrier b
; map := fun a b (f : a -> b) x => ap (pure f) x
; _ : forall (a : Type) x, map _ _ (fun (y : a) => y) x = x
; _ : forall a b c x y z,
ap (ap (map _ _ (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)) x) y) z =
ap x (ap y z)
; _ : forall a b (f : a -> b) x, map _ _ f (pure x) = pure (f x)
; _ : forall a b (f : carrier (a -> b)) x,
ap f (pure x) = map _ _ (fun g => g x) f
}.
Record IdiomaticTransformation (F G:Applicative) := idomaticTransformation
{ transform :> forall a, F a -> G a
; _ : forall a (x:a), transform (pure F x) = pure G x
; _ : forall a b (f : F (a -> b)) x, transform (ap f x) = ap (transform f) (transform x)
}.
Definition TraversableSig a a' b b' := forall (f:Applicative), (b -> f b') -> (a -> f a').
Axiom parametricity_instance :
forall a a' b b' (t : TraversableSig a a' b b') F G (eta : IdiomaticTransformation F G) f x,
eta _ (t F f x) = t G (fun a => eta _ (f a)) x.
Lemma identity_law (F : Applicative) a (x : F a) : map (fun (y : a) => y) x = x.
Proof.
destruct F.
auto.
Qed.
Lemma composition_law (F : Applicative) a b c x y (z : F a) :
ap (ap (map (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)) x) y) z =
ap x (ap y z).
Proof.
destruct F.
auto.
Qed.
Lemma homomorphism_law (F : Applicative) a b (f : a -> b) x :
ap (pure F f) (pure F x) = pure F (f x).
Proof.
fold (map f (pure F x)).
destruct F.
auto.
Qed.
Lemma interchange_law (F : Applicative) a b (f : F (a -> b)) x :
ap f (pure F x) = map (fun g => g x) f.
Proof.
destruct F.
auto.
Qed.
Definition IdApplicative : Applicative.
exists (fun A => A) (fun a (x : a) => x) (fun a b (f : a -> b) => f);
try reflexivity.
Defined.
Section ComposeApplicative.
Variable (F G :Applicative).
Let FG (a:Type) := F (G a).
Definition Compose_pure (a:Type) (x:a) : FG a :=
pure F (pure G x).
Definition Compose_ap (a b:Type) (f:FG (a -> b)) (x:FG a) : FG b :=
ap (ap (pure F (fun g x => ap g x)) f) x.
Lemma Compose_identity (a:Type) (x : FG a):
Compose_ap (Compose_pure (fun y : a => y)) x = x.
Proof.
unfold Compose_ap, Compose_pure.
rewrite homomorphism_law.
replace (fun x0 : G a => ap (a:=G) (a0:=a) (b:=a) (pure G (fun y : a => y)) x0)
with (fun (y : G a) => y).
apply identity_law.
apply functional_extensionality; intro y.
symmetry.
apply identity_law.
Qed.
Lemma Compose_composition (a b c:Type) x y (z : FG a) :
Compose_ap (Compose_ap (Compose_ap (Compose_pure (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)))
x) y) z =
Compose_ap x (Compose_ap y z).
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun (w : G (b -> c)) (w0 : G (a -> b)) (x0 : G a) =>
ap (a:=G) (a0:=a) (b:=c)
(ap (a:=G) (a0:=a -> b) (b:=a -> c)
(ap (a:=G) (a0:=b -> c) (b:=(a -> b) -> a -> c)
(pure G
(fun (f : b -> c) (g : a -> b) (w1 : a) => f (g w1)))
w) w0) x0)
with (fun (w : G (b -> c)) (w0 : G (a -> b)) (w1 : G a) =>
ap (a:=G) (a0:=b) (b:=c) w (ap (a:=G) (a0:=a) (b:=b) w0 w1)).
reflexivity.
repeat (apply functional_extensionality; intro).
symmetry.
apply composition_law.
Qed.
Lemma Compose_homomorphism a b (f : a -> b) x :
Compose_ap (Compose_pure f) (Compose_pure x) = Compose_pure (f x).
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
reflexivity.
Qed.
Lemma Compose_interchange a b (f : FG (a -> b)) x :
Compose_ap f (Compose_pure x) = Compose_ap (Compose_pure (fun g => g x)) f.
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
repeat rewrite interchange_law.
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun w : G (a -> b) => ap (a:=G) (a0:=a) (b:=b) w (pure G x))
with (fun x0 : G (a -> b) =>
ap (a:=G) (a0:=a -> b) (b:=b) (pure G (fun g : a -> b => g x)) x0).
reflexivity.
apply functional_extensionality; intro.
symmetry.
apply interchange_law.
Qed.
Definition ComposeApplicative : Applicative.
exists FG Compose_pure Compose_ap.
apply Compose_identity.
apply Compose_composition.
apply Compose_homomorphism.
apply Compose_interchange.
Defined.
End ComposeApplicative.
Inductive KleeneStore (i j a : Type) :=
| Unit : a -> KleeneStore i j a
| Battery : KleeneStore i j (j -> a) -> i -> KleeneStore i j a.
Fixpoint KleeneStore_map (i j a b: Type) (f : (a -> b))
(x : KleeneStore i j a) : KleeneStore i j b :=
match x with
| Unit y => Unit _ _ (f y)
| Battery v a => Battery (KleeneStore_map (fun g z => f (g z)) v) a
end.
Lemma KleeneStore_map_id (i j a : Type) (x : KleeneStore i j a) :
KleeneStore_map (fun a => a) x = x.
Proof.
induction x.
reflexivity.
simpl.
replace (fun (g : j -> a) (z : j) => g z) with (fun (g : j -> a) => g).
rewrite IHx.
reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.
Lemma KleeneStore_map_comp (i j a b c : Type) (f : b -> c) (g : a -> b)
(x : KleeneStore i j a) :
KleeneStore_map f (KleeneStore_map g x) = KleeneStore_map (fun a => f (g a)) x.
Proof.
revert b c f g.
induction x.
reflexivity.
simpl.
intros b c f g.
rewrite IHx.
reflexivity.
Qed.
Fixpoint KleeneStore_apH (i j a b c : Type) (h : c -> a -> b) (f : KleeneStore i j c) {struct f} :
KleeneStore i j a -> KleeneStore i j b :=
match f with
| Unit g => KleeneStore_map (h g)
| Battery v a => fun y =>
Battery (KleeneStore_apH (fun r s t => (h (r t) s)) v y) a
end.
Definition KleeneStore_ap (i j a b : Type) :
KleeneStore i j (a -> b) -> KleeneStore i j a -> KleeneStore i j b
:= KleeneStore_apH (fun x => x).
Lemma KleeneStore_map_ap i j a b (f : a -> b) x : KleeneStore_map f x =
KleeneStore_ap (Unit i j f) x.
Proof.
reflexivity.
Qed.
Lemma KleeneStore_identity i j a x : KleeneStore_ap (Unit i j (fun (y : a) => y)) x = x.
Proof.
induction x.
reflexivity.
unfold KleeneStore_ap in *; simpl in *.
replace (fun (g : j -> a) (z : j) => g z) with (fun (g : j -> a) => g).
rewrite IHx; reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.
Lemma KleeneStore_apH_ap i j a b c h f x : @KleeneStore_apH i j a b c h f x =
KleeneStore_ap (KleeneStore_map h f) x.
Proof.
cut (forall i j a b c d h (g : d -> c) f x,
@KleeneStore_apH i j a b c h (KleeneStore_map g f) x =
KleeneStore_ap (KleeneStore_map (fun z => h (g z)) f) x).
intros H.
assert (H0 := H i j a b c c h (fun z => z) f x).
rewrite KleeneStore_map_ap, KleeneStore_identity in H0.
rewrite H0.
rewrite (eta_expansion h).
reflexivity.
clear i j a b c h f x.
intros i j a b c d h g f x.
revert b c g h.
induction f.
reflexivity.
intros b c g h.
unfold KleeneStore_ap; simpl.
rewrite IHf, IHf.
reflexivity.
Qed.
Lemma KleeneStore_interchange i j a b (f : KleeneStore i j (a -> b)) x :
KleeneStore_ap f (Unit i j x) = KleeneStore_ap (Unit i j (fun g => g x)) f.
Proof.
cut (forall i j a b c (h : c -> a -> b) (f : KleeneStore i j c) x,
KleeneStore_apH h f (Unit i j x) = KleeneStore_ap (Unit i j (fun g => h g x)) f).
intros H.
apply H.
clear i j a b f x.
intros i j a b c h f.
revert a b h.
induction f.
reflexivity.
intros a0 b h x.
unfold KleeneStore_ap; simpl.
rewrite IHf.
reflexivity.
Qed.
Lemma KleeneStore_composition i j a b c x y z :
KleeneStore_ap (KleeneStore_ap (KleeneStore_ap (Unit i j (fun (f : b -> c) (g : a -> b) (w:a) => f (g w))) x) y) z =
KleeneStore_ap x (KleeneStore_ap y z).
Proof.
unfold KleeneStore_ap; simpl.
cut (forall c0 c1 (h0 : c0 -> b -> c) (x0 : KleeneStore i j c0) (h1 : c1 -> a -> b) (y0 : KleeneStore i j c1),
KleeneStore_ap
(KleeneStore_ap
(KleeneStore_ap
(Unit i j (fun (f : b -> c) (g : a -> b) (w : a) => f (g w)))
(KleeneStore_map h0 x0)) (KleeneStore_map h1 y0)) z =
KleeneStore_apH h0 x0 (KleeneStore_apH h1 y0 z)).
intros H.
rewrite <- H, <- KleeneStore_map_ap.
do 2 rewrite (KleeneStore_map_ap (fun g => g)), KleeneStore_identity.
reflexivity.
clear x y.
assert (H : forall (a b c : Type) (h0 : b -> c) c0 (h1 : c0 -> a -> b) (z : KleeneStore i j a) (y : KleeneStore i j c0),
KleeneStore_ap
(KleeneStore_map (fun (a' : c0) (w : a) => h0 (h1 a' w)) y) z =
KleeneStore_map h0 (KleeneStore_apH h1 y z)).
clear - i j.
intros a b c h0 c0 h1 z y.
revert a b c h0 h1 z.
induction y; intros a' b c h0 h1 z; simpl.
rewrite KleeneStore_map_comp.
reflexivity.
rewrite <- IHy.
unfold KleeneStore_ap; simpl.
repeat rewrite KleeneStore_apH_ap.
repeat rewrite KleeneStore_map_comp.
reflexivity.
intros c0 c1 h0 x.
revert b c h0 c1 a z.
unfold KleeneStore_ap; simpl.
induction x; intros b c h0 c1 a' z h1 y; simpl.
generalize (h0 a0).
clear a h0 a0.
intros h0.
rewrite KleeneStore_map_comp.
apply H.
rewrite <- IHx.
repeat rewrite KleeneStore_map_comp.
repeat rewrite KleeneStore_apH_ap.
repeat rewrite KleeneStore_map_comp.
unfold KleeneStore_ap; simpl.
repeat (rewrite <- H; repeat rewrite KleeneStore_map_comp).
reflexivity.
Qed.
Definition KleeneStoreApplicative (i j : Type) : Applicative.
exists (KleeneStore i j) (Unit i j) (@KleeneStore_ap i j).
apply KleeneStore_identity.
apply KleeneStore_composition.
reflexivity.
apply KleeneStore_interchange.
Defined.
Canonical Structure KleeneStoreApplicative.
Fixpoint KleeneExtract i a (f : KleeneStore i i a) : a :=
match f with
| Unit x => x
| Battery v y => KleeneExtract v y
end.
Fixpoint KleeneDuplicate i j k a (f : KleeneStore i k a) :
KleeneStore i j (KleeneStore j k a) :=
match f with
| Unit x => Unit i j (Unit j k x)
| Battery v y => Battery (KleeneStore_map (@Battery _ _ _) (KleeneDuplicate j v)) y
end.
Lemma KleeneExtract_map i a b (f : a -> b) (x : KleeneStore i i a) :
KleeneExtract (KleeneStore_map f x) = f (KleeneExtract x).
Proof.
revert b f.
induction x; intros b f.
reflexivity.
simpl.
rewrite IHx.
reflexivity.
Qed.
Lemma KleeneDuplicate_map i j k a b (f : a -> b) (x : KleeneStore i k a) :
KleeneDuplicate j (KleeneStore_map f x) = KleeneStore_map (KleeneStore_map f) (KleeneDuplicate j x).
Proof.
revert b f.
induction x; intros b f.
reflexivity.
simpl.
rewrite IHx.
repeat rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j k (k -> a)) (z : j) =>
Battery (KleeneStore_map (fun (g : k -> a) (z0 : k) => f (g z0)) a0) z)
with (fun a0 : KleeneStore j k (k -> a) =>
Battery (KleeneStore_map (fun (g : k -> a) (z : k) => f (g z)) a0)).
reflexivity.
apply functional_extensionality; intro.
apply eta_expansion.
Qed.
Lemma KleeneStore_law1 i j a (x : KleeneStore i j a) :
KleeneExtract (KleeneDuplicate _ x) = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneExtract_map.
rewrite IHx.
reflexivity.
Qed.
Lemma KleeneStore_law2 i j a (x : KleeneStore i j a) :
KleeneStore_map (@KleeneExtract _ _) (KleeneDuplicate _ x) = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j j (j -> a)) (z : j) => KleeneExtract a0 z)
with (@KleeneExtract j (j -> a)).
rewrite IHx.
reflexivity.
do 2 (apply functional_extensionality; intro).
reflexivity.
Qed.
Lemma KleeneStore_law3 i j k l a (x : KleeneStore i l a) :
KleeneDuplicate j (KleeneDuplicate k x) = KleeneStore_map (fun z => KleeneDuplicate k z) (KleeneDuplicate j x).
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneDuplicate_map, IHx.
repeat rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j l (l -> a)) (z : j) =>
@Battery j k (KleeneStore k l a)
(@KleeneStore_map j k (KleeneStore k l (l -> a))
(k -> KleeneStore k l a) (@Battery k l a)
(@KleeneDuplicate j k l (l -> a) a0)) z)
with (fun (a0 : KleeneStore j l (l -> a)) =>
Battery (KleeneStore_map (@Battery k l a) (KleeneDuplicate k a0))).
reflexivity.
do 2 (apply functional_extensionality; intro); reflexivity.
Qed.
Fixpoint experiment i j (F : Applicative) (g : i -> F j) a (k : KleeneStore i j a) :
F a :=
match k with
| Unit x => pure F x
| Battery v b => ap (map (fun x f => f x) (g b)) (experiment g v)
end.
Lemma experiment_map i j a b (F : Applicative) (g : i -> F j) (f : a -> b) (x : KleeneStore i j a) :
experiment g (KleeneStore_map f x) = map f (experiment g x).
Proof.
revert b f.
induction x; intros b f; simpl.
rewrite <- homomorphism_law.
reflexivity.
rewrite IHx.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
reflexivity.
Qed.
Lemma experiment_ap i j a b (f : Applicative) (g : i -> f j)
(h : KleeneStore i j (a -> b)) (x : KleeneStore i j a) :
experiment g (ap h x) = ap (experiment g h) (experiment g x).
Proof.
cut (forall c (h0 : c -> a -> b) (h : KleeneStore i j c),
experiment g (KleeneStore_apH h0 h x) = ap (experiment g (map h0 h)) (experiment g x)).
intros H.
simpl; unfold KleeneStore_ap; simpl.
rewrite H, identity_law.
reflexivity.
clear h.
intros c h0 h.
revert b h0.
induction h; intros b h0; simpl.
apply experiment_map.
rewrite IHh.
simpl.
rewrite <- KleeneStore_map_ap.
rewrite experiment_map, experiment_map.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun (w : j) (w0 : j -> a0) (w1 : a) => h0 (w0 w) w1)
with (fun (w : j) (w0 : j -> a0) => h0 (w0 w)).
reflexivity.
do 2 (apply functional_extensionality; intro); apply eta_expansion.
Qed.
Definition experiment_idomaticTransformation i j (F : Applicative) (g : i -> F j) :
IdiomaticTransformation (KleeneStoreApplicative i j) F.
exists (@experiment i j F g).
reflexivity.
intros a b f x.
apply experiment_ap.
Defined.
Definition impure i j : i -> KleeneStore i j j :=
Battery (Unit _ _ (fun x => x)).
Lemma experiment_impure i j a (x: KleeneStore i j a) : experiment (impure j) x = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite IHx.
unfold KleeneStore_ap; simpl.
replace (fun (s : j -> a) (t : j) => s t) with (fun x : j -> a => x).
rewrite KleeneStore_map_id.
reflexivity.
repeat (apply functional_extensionality; intro); reflexivity.
Qed.
Lemma experiment_duplicate i j k a (x: KleeneStore i k a) :
experiment (F:=ComposeApplicative (KleeneStoreApplicative i j)
(KleeneStoreApplicative j k)) (fun z : i => Battery (Unit i j (impure k)) z) x = KleeneDuplicate j x.
Proof.
induction x.
reflexivity.
simpl; rewrite <- IHx.
simpl; unfold KleeneStore_ap; simpl.
replace (fun (s : KleeneStore j k (k -> a)) (t : j) =>
Battery (KleeneStore_map (fun (s0 : k -> a) (t0 : k) => s0 t0) s) t)
with (@Battery j k a).
reflexivity.
repeat (apply functional_extensionality; intros).
replace (fun (s0 : k -> a) (t0 : k) => s0 t0)
with (fun s0 : k -> a => s0).
rewrite KleeneStore_map_id.
reflexivity.
repeat (apply functional_extensionality; intros).
reflexivity.
Qed.
Definition CoalgebroidSig a a' b b' := a -> KleeneStore b b' a'.
(*** TraversableSig and CoalgebraSig are isomorphic ***)
Definition Traversable_to_Coalgebroid a a' b b'
(f : TraversableSig a a' b b') : CoalgebroidSig a a' b b' :=
f (KleeneStoreApplicative b b') (Battery (Unit b b' (fun x => x))).
Definition Coalgebroid_to_Traversable a a' b b'
(g : CoalgebroidSig a a' b b') : TraversableSig a a' b b' :=
fun f h x => experiment h (g x).
Lemma Traversable_Coalgebroid_iso1 a a' b b' (x : CoalgebroidSig a a' b b') y :
Traversable_to_Coalgebroid (Coalgebroid_to_Traversable x) y = x y.
Proof.
unfold Traversable_to_Coalgebroid, Coalgebroid_to_Traversable.
generalize (x y).
clear x y.
induction k.
reflexivity.
simpl.
rewrite IHk.
clear a IHk.
unfold KleeneStore_ap; simpl.
rewrite KleeneStore_map_ap.
replace (fun (s : b' -> a0) (t : b') => s t) with (fun (s : b' -> a0) => s).
rewrite KleeneStore_identity.
reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.
Lemma Traversable_Coalgebroid_iso2 a a' b b' (x : TraversableSig a a' b b') F g y :
Coalgebroid_to_Traversable (Traversable_to_Coalgebroid x) g y = x F g y.
Proof.
unfold Traversable_to_Coalgebroid, Coalgebroid_to_Traversable.
assert (P := (@parametricity_instance _ _ _ _ x _ _ (experiment_idomaticTransformation g) (Battery (Unit b b' (fun y => y))))) .
simpl in P.
rewrite P.
clear P.
replace (fun a0 : b =>
ap (a:=F) (a0:=b' -> b') (b:=b')
(map (a:=F) (fun (x0 : b') (f : b' -> b') => f x0) (g a0))
(pure F (fun y0 : b' => y0))) with g.
reflexivity.
apply functional_extensionality; intros z.
rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
fold (map (fun w => w) (g z)).
rewrite identity_law.
reflexivity.
Qed.
Definition TraversableIdLaw a b (t : TraversableSig a a b b) :=
(forall x, t IdApplicative (fun a => a) x = x).
Definition CoalgebroidExtractLaw a b (t : CoalgebroidSig a a b b) :=
(forall x, KleeneExtract (t x) = x).
Lemma equiv_law1 a b (t : CoalgebroidSig a a b b) :
TraversableIdLaw (Coalgebroid_to_Traversable t) <->
CoalgebroidExtractLaw t.
Proof.
cut (forall x, (Coalgebroid_to_Traversable t) IdApplicative (fun a => a) x =
KleeneExtract (t x)).
intros E.
split; intros H x; simpl; rewrite <- H; auto.
intros x.
unfold Coalgebroid_to_Traversable.
generalize (t x).
clear t x.
induction k.
reflexivity.
simpl.
rewrite IHk.
reflexivity.
Qed.
Definition TraversableComposeLaw (i o : Type -> Type)
(t : forall (a b : Type), TraversableSig (o a) (o b) (i a) (i b)) :=
(forall a b c (F G:Applicative) (f : i a -> F (i b)) (g : i b -> G (i c)) x,
t a c (ComposeApplicative F G) (fun z => map g (f z)) x = map (t _ _ _ g) (t _ _ _ f x)).
Definition CoalgebroidDuplicateLaw (i o : Type -> Type)
(t : forall (a b : Type), CoalgebroidSig (o a) (o b) (i a) (i b)) :=
forall a b c x, KleeneDuplicate _ (t a c x) = KleeneStore_map (t _ _) (t a b x).
Lemma equiv_law2 i o t :
@TraversableComposeLaw i o (fun a b => Coalgebroid_to_Traversable (t a b)) <->
@CoalgebroidDuplicateLaw i o t.
Proof.
split.
intros H a b c x.
assert (H0 := H a b c _ _ (impure _) (impure _) x).
unfold impure in H0; simpl in H0.
unfold KleeneStore_ap in H0; simpl in H0.
unfold Coalgebroid_to_Traversable in H0; simpl in H0.
rewrite experiment_impure in H0.
replace (fun x : o b =>
experiment (F:=KleeneStoreApplicative (i b) (i c))
(Battery (Unit (i b) (i c) (fun x0 : i c => x0))) (t b c x))
with (t b c) in H0.
rewrite <- H0.
rewrite <- experiment_duplicate.
unfold impure; simpl.
replace (fun z0 : i b => Battery (Unit (i b) (i c) (fun x0 : i c => x0)) z0)
with (Battery (Unit (i b) (i c) (fun x0 : i c => x0))).
reflexivity.
apply functional_extensionality; reflexivity.
apply functional_extensionality; intros z.
rewrite experiment_impure.
reflexivity.
intros H a b c F G f g x.
assert (H0 := H a b c x).
unfold Coalgebroid_to_Traversable.
set (fg := (fun z : i a => map (a:=F) g (f z))).
rewrite <- experiment_map.
rewrite <- KleeneStore_map_comp.
rewrite <- H0.
generalize (t a c x).
revert f g fg.
clear H0.
generalize (i a) (i b) (i c) (o c).
clear - F G.
(* This probably should be its own algebraic law but...*)
intros a b c x f g fg k.
induction k.
reflexivity.
simpl.
rewrite IHk.
unfold Compose_ap, Compose_pure, map; simpl.
rewrite KleeneStore_map_comp.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite experiment_map.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
unfold fg.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
reflexivity.
Qed.

Modules After attending the second St Jacob's workshop I think I now understand all the pieces that make up a good module system; though I might not understand how they all fit together yet.

There is also a notable distinction between modular programming and module systems, which turn out to only be loosely related. Modular programming is about isolating software components and using narrow interfaces to communicate between them, while a module system is about assembling larger software modules from smaller modules.

Modules are dependent records / typing contexts for some type system. Modules are abstract over the the exact details of the type system which makes the notion quite versatile. All that is needed for the type system is that it supports variable declarations and substitution. It is also very convenient from both a theoretical and a practical point of view that modules support manifest entries / definitions.

Modules are related to each other through views. A view from a module A to a module B is an assignment of expressions of the type theory in the context A for every declaration in the module B. Thus if you have an instance of a module A you can derive an instance of a module B by substituting the free variables in the expression in B with the value in A. Indeed, one can define an instance of a module A to be a view from the empty context to a module A.

Extensions form an important class of views. An extension from module A to module B is a view where each expression for module B is a unique variable name from module A.

Modules can be combined together to create new modules. I think the Mathscheme project has found a good set of combinators that can be used to create new modules: extend, combine extensions, and mixin a view over an extension (I will discuss rename later as it isn't exactly a combinator, since it only produces isomorphic modules). The empty module gets things started. Arguably combine can be defined as a mixin, but it is probably better to consider it as a separate operation.

It strikes me that where most existing module systems go wrong is by taking inclusions too seriously. Inclusions are special types of extensions where each variable assignment is identical to the variable being assigned (note, it is only possible to define inclusions when modules are *not* take up to alpha equivalence). Inclusions have several nice properties: in particular there is at most one inclusion between any two modules, so inclusions form a partial order out of the modules.

I think module systems tend to only allow combine and mixins over inclusions rather than arbitrary extensions. The problem is that a structure like Ring, is an extension of Monoid in two different ways. Both cannot be inclusions since there is a most one inclusion between two modules. The usual symptom of this problem is that abelian monoids are unrelated to monoids, and rings become a composition of these two distinct structures.

Typeclasses are dependent records that are combined with a type inference mechanism. While type inference is important, it is an orthogonal issue. SSreflect type classes are dependent records that use coercions and canonical structures to define extensions and views (in some way that haven't fully worked out). Coq's coercion mechanism works best when they form a partial order, so ssreflect appears to suffer from the inclusion problem.

Spitters and van der Weegen's pebble style type-classes is a combination of modules being dependent records and typing contexts. The domain of a view is a typing context while the codomain is a dependent record. I haven't considered their module system in detail yet.

Bill and I have worked out an approach to using a GMP algorithmic theory to do natural number computation using trustable communication.

To begin with we assume we are given an algebraic theory of integer arithmetic called GMP.
GMP contains transformers for various integer operations, such as addition, multiplication, integer square root, etc. There are meaning formulas for these transformers whose instances are all Δ_{0}, which makes all the "axioms" of GMP these Δ_{0} sentences.

What does it mean for GMP to be correct? It means that all these meaning formulas are theorems of a theory of integer arithmetic. Define IA to be a theory of integer arithmetic in the same vein as Peano arithmetic. For completeness, let us assume that we have some full induction principle for integer arithmetic.

There is a trivial translation from GMP to IA, which is the identity translation, since the two theories share the same language. GMP is "correct" if this identity translation is a theory interpretation. Proving that GMP is "correct" is an extremely difficult task, and so at this point we will simply trust that it is correct.

I think in practice one might unify GMP and IA into one theory, but the separation between the two theories in the above presentation, at the very least, helps to clarify what is going on and what is trusted.

As it stands GMP and IA only do integer arithmetic, but we want to do natural number arithmetic. Natural number arithmetic is compatible with integer arithmetic, but this fact requires justification. To this end we extend IA and GMP to IA' and GMP' to support natural number arithmetic.

IA' defines a type of natural numbers as a subset of integers and defines natural number operations on this type of natural numbers. From this, one should be able to prove Peano's axioms. We also extend GMP to GMP', by again defining a type of natural numbers. We define a second set of meaning formulas for natural number addition. These meaning formulas quantify over numerals for natural numbers and relate natural number operations to the integer transformers.

The new meaning formulas provide a whole host of new "axioms" for GMP', and we need to check that they are correct. We could again trust that it is correct by assuming the identity translation to IA' is an interpretation. However, instead we can prove that it is relatively correct to GMP. That is, we can prove that if GMP is correct then GMP' is correct. To do this we simply prove that all the "new axioms" of GMP' are theorems of IA' under the assumption that the "axioms" of GMP hold. Each "new axiom" of GMP' should follow from the corresponding integer "axiom" of GMP by the theory of IA'.

From here on out, we closely follow the old trustable communication framework. To use this newly created natural number service, say from PA, we first build a translation from PA to GMP', which is easy since GMP' contains the language of PA. We "run the service" which means using the translated data to pick out an instance of a meaning formula for one of the natural number operations in GMP'. Call this instance φ. Next we send φ through the semi-trusted identity interpretation to IA'.

To complete the query we need an interpretation from IA' to PA, but this requires some preparation. We extend PA to PA' to define the integers from the natural numbers using the ambient set theory of Chiron to construct them. It is important to construct the integers in such a way that the natural numbers are a subset of them, not just isomorphic to a subset of them. We include definitions for all the integer operations.

Now we can translate from IA' to PA'. We claim that this translation is an interpretation. In order to prove this, it suffices to prove that the translations of all the axioms of IA' hold in PA', which should be the case. Finally we interpret φ to PA' and then expand away all the definitions of PA' to get a final answer in PA. This expansion of definitions in practice will do nothing since φ will actually already be in the language of PA.

I’m working on this idea of considering theory signatures as contexts of some dependent type theory and theory presentations as a category fibred over the category of contexts. A model of a theory presentation corresponds to a point of said object, that is a morphism from the terminal theory presentation (i.e. the empty context with no axioms) to said object. The fibration projects models down their underlying structure, which is a point in the corresponding theory signature, that is a morphisms from the terminal theory signature (i.e. the empty context) to said theory signature, which in turn corresponds to a term fulfilling the theory signature.

Given that two structures for signature S are arrows M N : 1 → S, it seems natural to represent homomorphisms from M to N as a 2-cell F : M ⇒ N.

If our category of theory signatures is going to actually be a 2-category then we need to consider 2-fibrations, which seem to have been worked out in Claudio Hermida’s paper entitled "Some Properties of Fib as a fibred 2-category".

More importantly I need to work out what a 2-cell in the category of contexts would be exactly. Some things are pretty clear; for the context containing x:Type and when the corresponding components of the structures, M and N, are ⊢ s:Type and ⊢ t:Type, we want the corresponding component F : M ⇒ N to be a term ⊢ F_{x} : s → t. If the context contains an operation f : x → x, and the corresponding components of the structures are ⊢ g : s → s and ⊢ h : t → t, then we want the corresponding component of F : M ⇒ N to be the constraint ⊢ F_{f} : F_{x}∘g =_{s → t} h∘F_{x}. But to work it out for the general case of dependent type boggles my mind.

There is an interesting downward transformation going on here where types in the signature turn are realized by (function) terms in the 2-cells, and terms in the signatures are realized by (equality) propositions in the 2-cells, and propositions (in theory presentations) will come for free in the 2-cells (is this always true?). Perhaps kinds will realized by types?

This all vaguely resembles Reynold's abstraction theorem.

A : Type;
B : A -> Type;
f : forall x : A. B x
=====================
|- f =_{η} fun (x:A) => f x
A : Type;
B : A -> Type;
C : SigT A B -> Type;
f : forall p : SigT A B. C p
============================
p : SigT A B |- f p =_{η} match p as p0 return C p0 with existT x t => f (existT A B x t) end
f : unit
========
|- f =_{η} tt
A : Type;
x, y : A;
C : forall y, Eq A x y -> Type;
f : forall e : Eq A x y -> C y e
================================
e : Eq A x y |- f e =_{η} match e as e0 in Eq _ _ z return C z e0 with refl => f (refl A x) end
A, B : Type;
C : A + B -> Type;
f : forall p : A + B. C p
=========================
p : A + B |- f p =_{η} match p as p0 return C p0 with left x => f (left x) | right y -> f (right y) end
C : Void -> Type;
f : forall p : Void . C p
=========================
p : Void |- f p =_{η} match p as p0 return C p0 with end
Inductive W (A:Type) (B:A -> Type) : Type :=
node : forall (a:A) (f:B a -> W A B), W A B
A : Type;
B : A -> Type;
C : W A B -> Type;
f0 : forall p : W A B. C p;
f1 : forall (a : A) (f:B a -> W A B), (forall b:B a. C (f b)) -> C (node a f)
-----------------------------------------------------------------------------
a : A, f: B a -> W A B |- f0 (node a f) =_{βη} f1 a f (fun b => f0 (f b))
=============================================================================
p : W A B |- f0 p =_{η} W_rect A B C f1 p
C : nat -> Type;
f0 : forall n : nat. C n;
f1 : forall n : nat. C n -> C (S n)
-----------------------------------
n:nat |- f0 (S n) =_{βη} f1 (f0 n))
===================================
n:nat |- f0 n =_{η} nat_rect C (f0 O) f1 n

A container is a specification of S and P and is given by the dependent type s:S ⊢ P s a.k.a. the telescope ΣS:★. S → ★. A container specifies the (strictly positive) functor λX:★. Σs:S. (P s) → X.

An indexed container over I is a specification of S and P and is given by the dependent type ΣS:★. I → S → ★.
An indexed container specifies an indexed Functor λX:I → ★. Σs:S. Πi:I. (P i s) → X i.

Containers form a commutative ★-semi-algebra a.k.a. a ★-semiring (not to be confused with a *-semiring) with the following operations:

0 := ⟨⊥, []⟩

1 := ⟨⊤, λs. ⊥⟩

⟨A, P⟩ + ⟨B,Q⟩ := ⟨A + B, [P, Q]⟩

⟨A, P⟩ × ⟨B,Q⟩ := ⟨A × B, λ⟨a,b⟩. P a + Q b⟩.

R·⟨A,P⟩ := ⟨R × A, λ⟨_,a⟩. P a⟩

Containers (aka ⊤-indexed containers) form a ★-bi-semiring. The tensor of I indexed containers with J indexed containers is (I + J)-indexed containers. The identity of this tensor are the ⊥-indexed containers which are isomorphic to ★. The tensor of an I indexed container and a J indexed container is:

⟨A,P⟩ ⊗ ⟨B,Q⟩ := ⟨A × B, λ(ĳ:I+J) ⟨a,b⟩. [λi. P i a, λj. Q j b](ĳ)⟩.

In particular the tensor of containers with themselves are the 𝔹-indexed containers. The following are the ★-bi-semiring operations on containers

ε^{+}⟨A,P⟩ := Σa:A. P a → ⊥ (≜ Σa:A. ¬(P a))

ε^{×}⟨A,P⟩ := Σa:A. P a → ⊤ (≅ A)

Δ^{+}⟨A,P⟩ := ⟨Σa:A. P a → 𝔹, λ(i:𝔹) (⟨a,f⟩:Σa:A. P a → 𝔹). Σp:P a. i = f p⟩

Δ^{×}⟨A,P⟩ := ⟨A, λ(i:𝔹). P⟩

β(R)⟨A,P⟩ := Σa:A. P a → R

The composition product of I-indexed containers with J-indexed containers are the (I × J)-indexed containers, with containers (ie ⊤-indexed containers) as the unit for the composition product. The composition product of an I-indexed container with a J-indexed container is as follows.

⟨A,P⟩ ⊙ ⟨B,Q⟩ := ⟨Σa:A. Πi:I. P i a → B, λ⟨i,j⟩ ⟨a,f⟩. Σp : P i a. Q j (f i p)⟩

Now containers trivially form a semi-plethory since ⊤-indexed containers are clearly isomorphic to (⊤ × ⊤)-indexed containers.

ι⟨A,P⟩ := ⟨A,λ⟨⟩. P⟩

(∘)⟨A,P⟩ := ⟨A,λ⟨⟩.
P⟨⟨⟩,⟨⟩⟩⟩

For convenience we define the infix composition of two containers as:

⟨A,P⟩ ∘ ⟨B,Q⟩ := ⟨Σa:A. P a → B, λ⟨a,f⟩. Σp : P a. Q (f p)⟩ (≅ (∘)(⟨A,P⟩ ⊙ ⟨B,Q⟩))

Composition has an identity element, I, which doesn't appear to be a primitive semi-plethory operation for some reason. Nor do I know how to derive it from other operations. But here it is anyways.

I := ⟨⊤, λs. ⊤⟩

TODO: Actually verify these operations are correct by checking that all the required laws hold (upto isomorphism).

P.S. Actually containers do form a *-semiring, which makes it a ★-*-semiring. Actually we can get a ★-bi-*-semiring with the following asteration operation on containers and its dual.

⟨A,P⟩* := ⟨ℕ, Fin⟩ ∘ ⟨A,P⟩ (≅ ⟨List A, sum ∘ map P⟩)

⟨A,P⟩⁎ := ⟨A,P⟩ ∘ ⟨ℕ, Fin⟩ (≜ ⟨Σa:A. P a → ℕ, λ⟨a,f⟩. Σp:P a. Fin (f p)⟩)

Recalling the problem: On one side we have a computational theory call GMP that consists entirely of Δ_{0} theorems. On the other side we have a purely axiomatic theory called PA that is a high-level theory of Peano Arithmetic that has been conservatively extended to support decimal notation and whatever other reasonable conveniences for the natural numbers we want. The task is to use trustable communication to use the computational ability of GMP to solve simple arithmetic problems in PA.

The idea here is to extend GMP to a stronger theory GMP0 that is strong enough to define PA. Next we make a conservative extension of GMP0 to GMP' that defines the language of PA and proves the axioms of PA. Specifically GMP' defines

nat := { a : int | 0 ≤_{int} a}

+_{nat} := λ (a,b) : nat × nat. ι c : nat. c = a +_{int} b

…

Here we note that PA is a subtheory in the sense that it uses a sublanguage of GMP' and every theorem of PA is a theorem of GMP' (since GMP' proves all the axioms of PA).

The next step is to prove that GMP' is, in fact, a conservative extension of PA (thus GMP0 shouldn't be more powerful than PA). The idea here is to make an interpretation from GMP' into PA that fixes the language of PA. Unfortunately we cannot directly do this because interpretations in Chiron must be injective. So instead we note that if we make an interpretation from GMP' into a conservative extension of PA, called PA', that fixes the language of PA, then we can conclude that GMP' is a conservative extension of PA

To build this interpretation we extend PA to PA' with definitions:

int := nat×{0} ∪ {0}×nat

+_{int} := λ ((ap,an),(bp,bn)) : int × int. ι (cp,cn) : int.
cp + an + bn = ap + bp + cn ∧ (cp = 0 ∨ cn = 0)

…

Out interpretation sends int to int, +_{int} to +_{int}, etc. and fixes the lanuage of PA, so it sends nat to nat, and +_{nat} to +_{nat}.

Unfortunately this doesn't work. GMP' has a theorem (actually a definition) that nat = { a : int | 0 <=_{int} a}. If we look at this theorem under the above alleged interpretation, it is equivalent to nat = nat×{0}, which is clearly false. So our alleged interpretation isn't actually an interpretation because it isn't actually truth preserving.

Let us suppose for the sake of argument that we somehow prove that GMP' is a conservative extension of PA. What we then need to do is to write new services for PA that use GMP' services internally to help. We need to do something like writing new services because someone has to be responsible for proving that the operations on integers are, in fact, compatible with the operations on natural numbers. In our case it will be the responsibility of the person writing these new services to prove that the services are conservative (i.e. all the meaning formulas of the services are theorems). (More details on how to make this service is needed). With new services and new meaning formulas, there is no problem with translating the meaning formula through trustable communication since the meaning formula is no longer passed through the trustable communication framework.

In this sense we have sort of failed at our task which was to use the trustable communication framework; however I'm inclined to think that the original trustable communication framework cannot actually solve this particular communication problem since it leaves no room for the required proof that the computation of the natural numbers is compatible with computation on the integers. Therefore, I think it is inevitable that something beyond trustable communication is needed in this particular situation.

Other situations that do not have this compatibility issue are likely more amiable to using trustable communication. In particular our new natural number services could be served through a trustable communication channel.

An R-R'-biring is an R-ring A such that for every other R-ring B the set of homomorphisms from A to B has the structure of an R'-ring. This is equivalent to giving the following additional operations on A with the following laws:

This gives us enough structure to show that for any R-ring B, the homomorphisms from A to B have a R'-ring structure. For instance given R-ring homomorphisms f, g : A → B and r : R' we can define

0 : A → B is 0(a) = ε^{+}(a)⋅1

1 : A → B is 1(a) = ε^{×}(a)⋅1

f + g : A → B is f + g = ∇ ∘ (f⊗g) ∘ Δ^{+}

-f : A → B is -f = f ∘ σ

fg : A → B is fg = ∇ ∘ (f⊗g) ∘ Δ^{×}

r⋅f : A → B is r⋅f = f ∘ λ ∘ (β(r)⊗id) ∘ Δ^{×}

A biring over R is an R-R-biring.

A plain biring is a biring over ℤ just like a plain ring is a ℤ-ring.

R itself can be made into a trivial R-R'-biring over R where

ε^{+}(a) = ε^{×}(a) = a

σ(a) = a

Δ^{+}(a) = Δ^{×}(a) = a⊗1 = 1⊗a

β(r)(a) = a

R[X] is a biring over R where

ε^{+}(X) = 0 (polynomial evaluation at 0)

ε^{×}(X) = 1 (polynomial evaluation at 1)

σ(X) = -X (polynomial evaluation at -X)

Δ^{+}(X) = X⊗1 + 1⊗X (polynomial evaluation at X+Y)

Δ^{×}(X) = X⊗X (polynomial evaluation at XY)

β(r)(X) = r (polynomial evaluation at r)

A R-R'-biring A inducts a functor from R-Rings to R'-Rings that takes an R-Ring B to the R'-Ring of homomorphisms from A to B.

Birings are composable. Given an R-R'-biring A and and R'-R''-biring B, then there exists an R-R''-bring A⊙_{R'}B. (⊙_{R'}) is called the composition product.
First we define a R-ring A⊙_{R'}B for an R-R'-biring A and an R'-ring B in a way similar to the definition of a tensor product: A⊙_{R'}B can be constructed as A×B modulo the following equalities:

(a + b)⊙x = (a⊙x) + (b⊙x)

ab⊙x = (a⊙x)(b⊙x)

(r⋅1)⊙x = r⋅(1⊙y) (this y is not a typo: 0⊙x = 0⊙y = 0 and 1⊙x = 1⊙y = 1)

Think of a⊙x as the polynomial a evaluated at the point x.
If B also happens to be a R'-R''-biring, then we can make A⊙_{R'}B into an R-R''-biring.

ε^{+}(a⊙x) = a⊙(ε^{+}(x)) where a⊙r = β(r)(a)

ε^{×}(a⊙x) = a⊙(ε^{×}(x))

σ(a⊙x) = a⊙σ(x)

Δ^{+}(a⊙x) = a⊙Δ^{+}(x) where a⊙(w_{1}⊗w_{2}) = (a⊙w_{1})⊗(a⊙w_{2})

Δ^{×}(a⊙x) = a⊙Δ^{×}(x)

β(r)(a⊙x) = β(β(r)(x))(a)

(⊙_{R}) and R[X] make the category of birings over R into a monoidal category. (TODO: Why is this the Tall-Wraith monoid?). We want to check first that B is isomorphic to R[X]⊙_{R}B. The isomorphism maps x ↔ (X⊙x) (the reverse map extends by the composition product laws). Similarly we want to check that A is isomorphic to A⊙_{R}R[X]. Again, the isomorphism maps a ↔ (a⊙X).

an R-plethory is a monoid in this monoidal category of birings over R. This means that an R-plethory is a biring over R, call it A, that also has the following operations forming a monoid:

(∘) : A⊙_{R}A → A

ι : R[X] → A

R[X] is an R-plethory with ι the identity function and (∘)(X⊙X) = X which is effectively entails polyonomial composition.

According to the mathoverflow answer, R[X] is an initial R-plethory which seems reasonable.

I am not entirely sure this is all correct. But I'm moderately confident.

I will (hopefully) continue to update this post with further notes.

Here I present what I think is a slightly simpler proof of the Primitive Element Theorem's so called "finite case" than the one found in A Course in Constructive Algebra. It still follows the most important ideas presented in that book. In particular it is important to use the correct constructive phrasing of the "finite case".

Theorem:Primitive Element Theorem: Finite Case Given a discrete field F and two algebraic values a and b over F of degrees m and n respectively then forall N either #|F| > N or there exists some g in F[a,b] such that F[a,b] = F[g].

Of course by #|F| > N we really mean the statement that there exists some finite set of elements of F that has cardinality greater than N.

We can assume that a ≠ 0 and b ≠ 0 since in these cases F[a, b] = F[b] and F[a, b] = F[a] respectively.

Every element x ∈ F[a] is a linear combination of a^{0}, …, a^{m-1} with coefficents in F. Say x = Σx_{i}a^{i}. Consider the list [a^{0}, …, a^{Nm}], and then consider the finite set of coefficients S = {(a^{i})_{j} | i ≤ N^{m}, j < m}. If S has cardinality greater than N then we are done.

Suppose S has cardinality less than or equal to N. Then there are at most N^{m} linear combinations of the coefficients from S on [a^{0}, …, a^{m-1}], and since the list [a^{0}, …, a^{Nm}] has length N^{m}+1 then there must be two elements of this list that are the same. By dividing these two elements we conclude there is some i such that a^{i} = 1a has multiplicative order i.

By a similar argument we can conclude that either #|F| > N or there is some j such that b^{j} = 1b has multiplicative order j. Now we can proceed under the assumption that both a^{i} = 1a has multiplicative order i and b^{j} = 1b has multiplicative order j. The rest of the argument is standard.

Let f : ℤ_{i}×ℤ_{j} → F[a,b] be the function that sends (x,y) to a^{x}b^{y}. The function f is a group homomorphism into the multiplicative group of F[a,b], and therefore ℤ_{i}×ℤ_{j} must be cyclic and is generated by some z. Let g = f(z). Then there is some k_{a} and k_{a} such that g^{ka} = a and g^{kb} = b, and thus F[a, b] = F[g]. That concludes the proof.

The infinite case of the Primitive Element Theorem states that there exists some N (specifically I think m*(n-1)+1 should work) such that if #|F|>N and b is separable over F then there exists some g in F[a,b] such that F[a,b] = F[g]. This can be proved as done in A Course in Constructive Algebra or if you want to avoid the construction of splitting fields you can follow the argument in David Speyer or Boyarsky's proof. The infinite case combined with the finite case allow us to prove the primitive element theorem:

Theorem:Primitive Element Theorem Given a discrete field F and two algebraic values a and b with b separable over F, then there exists some g in F[a,b] such that F[a,b] = F[g].

Inspired by how Bas and Eelis handle morphisms in their work, I've rethought how morphisms can be implemented in Mathscheme.

Consider how to build a theory of monoid morphisms. One can build this theory by first taking a pushout of the theory of monoids with itself over the empty theory (i.e. take the disjoint union of the theory of monoids with itself) this gives us two copies of the theory of monoids and each copy has a separate universe: U_{1} and U_{2}. Then we extend this theory with a function f : U_{1} → U_{2} and axioms that says that f preserves each operation. This procedure works in general for algebraic theories.

Notice that this gives us a theory of monoid morphisms between some monoids, but not the theory a theory of monoid morphisms between two particular monoids, which is what we are usually interested in. However, by considering this theory of monoid morphisms as parameterized by two monoids in the sense of my last post one can build models of the theory of monoid morphisms between particular monoids.

This way of developing theories of morphisms has some nice properties. For example, we usually only care about vector space morphisms (aka linear transformations) between two vector spaces over the same field. This sharing of the same field is easy to do with the above technique. Instead of taking the pushout of the theory of vector spaces with itself over the empty theory, one would take the pushout of the theory of vector spaces with itself over the theory of fields. This forces the theory of fields to be shared between the two copies of vector spaces, ensuring that the domain and codomain of a field morphism are both vector spaces over the same field.

Some algebraic theories are parameterized by other algebraic theories. The most common example would be vector spaces, which are parameterized by a field that acts on the vector space by scalar multiplication.

In mathscheme, the theory of vector spaces contains types for both the field and the vector space, and provides (via inheritance) all the axioms of a field for the field type and then goes on to provide the vector space axioms (via various mix-ins). When this theory is reflected as a type we get a record for both the field component and the vector space component.

However, in may cases we want to reason about vector spaces whose field component is fixed to some particular value. One idea to support this sort of thing is to not reflect the theory as a type, but as a dependent function type. In this case, a function from the type of field to a type. Loosely speaking it would be

VS : {U:type; +, *: U*U -> U; -, inv : U -> U; 0 1 : U } -> type
VS F = {V:type, + : V*V -> V; - : V -> V; 0: V; *: (F.U)*V -> V}

I have left out the axioms above for simplicity, but the axioms would bring the operations of F into play. These parameterized models can probably be created for any theory morphism between theories.

Unparameterized models could then be simply a degenerate case of parameterized models over the initial empty theory. The models of the empty theory have type {} and there is exactly one value of this type {}.

To further help modularize theory development, it may be useful to take pushouts of not just theory presentations themselves, but to take pushouts of diagrams of theory presentations. The following is an elaboration of what Douglas Smith describes in his various papers on SpecWare including "Mechanizing the Development of Software". Although we are interested in diagrams of theory presentations, this development is generic for diagrams for any category with sufficient structure (ie, categories that have colimits.).

First we define what a graph is. A graph is a finite collection of nodes and a finite collection of directed edges between those nodes with a composition operation on edges (composition requires the target node of the first edge be the same as the source node of the second edge). The set of edges is closed under composition and for each node there is an identity edge from the node to itself. We require that the identity edge be an identity for the composition operation in the usual sense.

Actually, an graph is just a category, and I could have simply said that from the beginning. However, I will use the name graph in the cases where we don't really care about the semantics of the category and we only care about the shape of the category.

This definition of a graph differs notably from the definition of directed multigraph from graph theory because our definition of a graph says whether following two paths from a source node to a target node when composed together give equal edges or not. In particular our graphs tell you whether two particular squares commute or not. Usually this information is left implicit when a diagram is drawn on a board, but such information is a vital component of the definition.

Loosely speaking, a diagram is a graph where the nodes and edges are given labels from another category C in a way that is compatible with the category C. In our particular case, we are interested in C = the category of theory presentations, but this development is generic in C.
More formally speaking, a diagram is a functor d : G → C. where G is a graph that gives the shape of the diagram. The image of a node of G under d labels the node by an object from C, and the image of an edge of G under d labels the edge by an arrow from C. The law for a functor ensure that the labeling of nodes and edges is compatible with C.

Note that is definition of a diagram differs notably from the definition of a subcategory. In a diagram two different nodes could be get the same label, and two different edges could also get the same label. In otherwords, the functor d : G → C need not be injective.

All diagrams are functors (which are arrows in the category of categories) with codomain C. The arrows of a category with a constant codomain form the objects of a slice category, so that is an obvious choice for turning diagrams into a category, but we need something a bit more lax: a lax slice category.

The objects of a lax slice category are all functors that have the same codomain (in this case C). A morphism between d_{1} : G_{1} → C and d_{2} : G_{2} → C in a lax slice category is a functor f : G_{1} → G_{2} along with a natural transformation η_{f} from d_{1} to d_{2}∘f.

What does this definition mean for our diagrams? Given two diagrams d_{1} and d_{2}, a diagram morphism between these two diagrams states two things. Firstly it assigns for each node in the graph G_{1}, a node in the graph G_{2}, and for each edge in the graph G_{1}, an edge in the graph G_{2} in a way that is compatible. This first part is the information held by the functor f : G_{1} → G_{2} from the previous paragraph. The second part of a diagram morphism is a collection of arrows from C (in our case theory morphisms), one for each node in G_{1}. These arrows map the label for a node in G_{1} to the label for the corresponding node (under f) in G_{2}. This collection of arrows is given by the natural transformation η in the previous paragraph. Lastly, this collection of arrows is subject to a compatibility constraint that for every edge e : p → q in G_{1}, there is a commutative square that states that f(q)∘e = η(e)∘f(p). This condition is what makes the transformation η natural.

The laxness of the lax slice category is important. Without it we would end up with the stricter requirement that d_{1} = d_{2}∘f or in other words that the natural transformation is always the identity transformation. This stricter requirement would mean that the collection of arrows between diagrams always be identity arrows, and the only diagram arrows that would exist would be diagram inclusions. We require this laxness to get pushouts to generate a collection of novel theories. Without laxness we could only create the union of diagrams, which is not so interesting.

I believe it is true that if the category C has colimits, then this (lax) category of diagrams will have colimits, but I don't have a reference that proves this.

Now I will show how to use pushouts of diagrams to generate large batches of novel theories. For simplicity consider the diagram B generated from the theories: Semigroup, Monoid, and LeftNearSemiring with the usual arrow from Semigroup to Monoid, and the "multiplicative" arrow from Semigroup to LeftNearSemiring and the "additive" arrow from Monoid to LeftNearSemiring. This example is small enough to be easy to picture, but large enough to be a non-commutative diagram.

We want to use diagram pushouts to create commutative versions of these theories. To do this we will take as base A, the diagram consisting of the single node Semigroup (which implies the single identity arrow on that node), and for C we will take the single node CommutativeSemigroup. The diagram arrow from A to B will map the Semigroup node in A to the Semigroup node in B via the identity morphism. The diagram arrow from A to C will make the Semigroup noda in A to the CommutativeSemigroup node in B via the theory inclusion.

When we take the pushout of this span we get a new diagram D along with diagram arrows from B to D and C to D with the universal properties that pushouts have. What will the contents of D be? The shape of the diagram D will be the the disjoint union of the shapes of B and the shapes of C modulo the shape of A. So in this case that gives us the shape of B plus another point that in this case will be identified with the semigroup node of B. This moding out leaves us with a diagram with the same shape as B that we started with.

What are the contents of D? In this case, what was the semigroup of B has been transformed into the commutative semigroup that we gave in C. The morphisms of the diagram arrow from B to D includes our inclusion from semigroup to commutativeSemigroup. And the diagram arrow from C to D consists of the identity arrow from commutativeSemigroup to commutativeSemigroup. What was a monoid in B is a commutativeMonoid in D, and the diagram arrow from B to D contains a morphism from group to commutativeGroup. There is no morphism in the diagram arrow from C to D that targets commutativeMroup. Finally what was a LeftNearRing in B becomes a commutativeLeftNearRing where both multiplication and addition are commutative. Both operations are commutative because the two squares generated by the "multiplicative" arrow and the "additive" arrow must be commutative.

Now suppose we don't want to make both operations commutative. Say we only want to make the additive operation commutative. To achieve this we need to remove the multiplicative arrow from the diagram B yielding a diagram B′. Now the pushout of B′ and C over A yields a new diagram D′ which is similar to D, but where the LeftNearRing has been replaced with a LeftNearRing theory that only has addition commutative.

To be sure, we are not deleting the "multiplicative" arrow from our theory development. We are simply deciding to not include it in the diagram B′ we use to generate the pushout. This shows that we need to take arrows very seriously. Which arrows we include in our diagrams when doing diagram pushouts can have significant consequences on the generated theories.

Now suppose we want to have our cake and eat it too. We want to build all three extensions of LeftNearRing, one making the additive operation commutative, one making the multiplicative operation commutative, and one making both operations commutative. This is possible by creating duplicate copies of LeftNearRing in our diagram. One copy of LeftNearRing has only one arrow pointing to it from Monoid corresponding to the "additive" arrow, and another copy of LeftNearRing has only one arrow pointing to it from Semigroup corresponding to the "multiplicative" arrow. Finally we put in a third copy of LeftNearRing with two arrows from the other two LeftNearRing nodes are labeled with the identity morphism.

When we pushout with this diagram, each different copy of LeftNearRing will be assigned to a different resulting theory. The first will get commutative addition only, the second will get commutative multiplication only, and the last will get both commutative addition and commutative multiplication. The two arrows labeled with identity morphisms will transform into inclusions.

Suppose we have a diagram d of theories starting from Magma, and we want to extend this diagram with commutativity, associativity, and both commutativity and associativity. To do this we would use the above pushout mechanism twice, once to create d_{c} the diagram with commutative structures, and another time to create d_{a} the diagram with associative structures. Then to create the diagram d_{ac} of commutative and associative structures, we do the pushout of d_{c} and d_{a} over d, using the diagram morphisms from d when we created d_{c} and d_{a}.

The store comonad (better known as the costate comonad) can be defined as

data Store b a = Store (b -> a) b

with the following comonadic operations

extract :: Store b a -> a
extract (Store v b) = v b
fmap :: (a -> c) -> Store b a -> Store b c
fmap f (Store v b) = Store (f . v) b
duplicate :: Store b a -> Store b (Store b a)
duplicate (Store v b) = Store (Store v) b
extend :: (Store b a -> c) -> Store b a -> Store b c
extend f x = fmap f (duplicate x)

Given this we can define a lens (aka a functional reference) as follows

type Lens a b = a -> Store b a

A lens can be used as an accessor to a field of a record, though they have many uses beyond this.

data Entry = { name_ :: String
; city_ :: String
; birthdate_ :: Data
}
name :: Lens Entry String
name entry = Store (\newName -> entry {name_ = newName})) (name_ entry)

Above we create a lens to access the name field of this Entry structure. We can build similar lenses to access other the fields.

We can write getter and setter functions for an arbitrary lenses.

get :: Lens a b -> a -> b
get lens a = b
where
Store v b = lens a
set :: Lens a b -> a -> b -> a
set lens a = v
where
Store v b = lens a

However, we expect the get and set functions to obey certain laws. Here are the three laws that Koji Kagawa gives in his paper "Compositional References for Stateful Functional Programming". They are the laws that any second year computer science student would intuitively write down.

get l (set l s b) = b

set l s (get l s) = s

set l (set l s b1) b2 = set l s b2

Today I was trying to rewrite these lens laws to use our comonadic operations on the store comonad instead of get and set. So after playing around I came up with the following alternative set of laws

extract . l = id

fmap l . l = duplicate . l

Interestingly these laws no longer depend on any special operations of the store comonad. They only use the operations generic for any comonad.

Do these laws look familiar? They should. They are exactly the laws of a coalgebra for a comonad!

I was floored by this. These three, almost arbitrary, set of laws that every computer scientist intuits are exactly the set of laws implied by this abstract nonsense from category theory. I honestly wrote these laws out completely before noticing what they were. I do not recall this fact noted on any paper about lenses that I have read, but it will definitely be mentioned in my upcoming paper.

Below is the Coq code that proves that these two sets of laws are equivalent.

Set Implicit Arguments.
Section Lens.
Variable B : Type.
Definition W a := ((B -> a) * B)%type.
Definition extract (a:Type) (x : W a) : a := fst x (snd x).
Definition fmap (a b:Type) (f : a -> b) (x : W a) : W b := pair (fun z => f (fst x z)) (snd x).
Definition duplicate (a:Type) (x : W a) : W (W a) := pair (pair (fst x)) (snd x) .
Definition extend (a b:Type) (f : W a -> b) (x : W a) : W b := fmap f (duplicate x).
Variable A : Type.
Variable l : A -> W A.
Definition rd (r : A -> W A) (a:A) : B := snd (r a).
Definition wr (r : A -> W A) (a:A) (b:B) : A := fst (r a) b.
Section Iso1.
Hypothesis coalgebra1 : forall a, extract (l a) = a.
Hypothesis coalgebra2 : forall a, fmap l (l a) = duplicate (l a).
Lemma lawA : forall s t, rd l (wr l s t) = t.
Proof.
intros s t.
generalize (coalgebra2 s).
unfold rd, wr.
destruct (l s) as [f b].
unfold fmap, duplicate.
simpl.
inversion 1.
change (l (f t)) with ((fun z => l (f z)) t).
rewrite H1.
reflexivity.
Qed.
Lemma lawB : forall s, wr l s (rd l s) = s.
Proof.
firstorder.
Qed.
Lemma lawC : forall s t1 t2, wr l (wr l s t1) t2 = wr l s t2.
Proof.
intros s t.
generalize (coalgebra2 s).
unfold rd, wr.
destruct (l s) as [f b].
unfold fmap, duplicate.
simpl.
inversion 1.
change (l (f t)) with ((fun z => l (f z)) t).
rewrite H1.
reflexivity.
Qed.
End Iso1.
Section Iso2.
Hypothesis law1 : forall s t, rd l (wr l s t) = t.
Hypothesis law2 : forall s, wr l s (rd l s) = s.
Hypothesis law3 : forall s t1 t2, wr l (wr l s t1) t2 = wr l s t2.
Lemma coalgebraA : forall a, extract (l a) = a.
Proof.
firstorder.
Qed.
(* One day we will have observational type theory, but for now ... *)
Require Import FunctionalExtensionality.
Lemma coalgebraB : forall a, fmap l (l a) = duplicate (l a).
Proof.
intros a.
apply injective_projections; auto.
apply functional_extensionality; intros x.
simpl.
apply injective_projections.
apply functional_extensionality; intros y.
firstorder.
firstorder.
Qed.
End Iso2.
End Lens.

Edit (2011-01-19): I renamed the Selection comonad to the Store comonad and rearranged the order of some parameters to make it more compatible with Control.Comonad.Trans.Store. Some of the comments below use to the old name.

Free theorems were popularized by Wadler in his 1989 paper "Theorems for Free!". In that paper only polymorphism over types is considered. In 2009, Voigtländer illustrates how this can be extended to polymorphism over type constructors with class constraints in his paper "Free Theorems Involving Type Constructor Classes". He uses polymorphism over Monads for his example. In order to learn to apply this theory I will use a very simple exercise only involving Functors. Be aware that our reasoning will be "fast and loose" which is a technical term that means that our results only apply to total values.

The exercise here is to prove that the type A → B and the polymorphic type ∀κ:Functor. κA → κB are isomorphic. The intuition is that all a polymorphic function of type ∀κ:Functor. κA → κB can do is map some internally held function of type A → B. The claim is that the following pair of functions witness the isomorphism:

iso_{1} : (A → B) → ∀κ:Functor. κA → κB iso_{1}x := Λκ. λl. map_{κ}xl

iso_{2} : (∀κ:Functor. κA → κB) → A → B iso_{2}y := y Id

In the above we use Id, which is the identity functor.

To prove this we need to show that both ways of composing these two functions produce the identity function. One way is easy:

iso_{2} (iso_{1}x) a =
map_{Id}xa =
xa

So we see that iso_{2} (iso_{1}x) = x as required. The other direction is harder.

iso_{1} (iso_{2}y) κl =
map_{κ} (y Id) l

At this point we get stuck. We need to show that map_{κ} (y Id) l = yκl for an arbitrary functor κ and arbitrary l : κA. To continue the proof, we are going to have to use the parametricity of y : ∀κ:Functor. κA → κB.

Parametricity of y gives us a free theorem which states that given two functors F_{1} and F_{2} and a functor morphism η : ∀α. F_{1}α → F_{2}α we have that:

η_{B} ∘ yF_{1} = yF_{2} ∘ η_{A}

A functor morphism is better known as a natural transformation. A natural transformation η : ∀α. F_{1}α → F_{2}α is required to satisfy the following law: For any types C and D and any function g : C → D, we require that,

map_{F2}g ∘ η_{C} = η_{D} ∘ map_{F1}g

My proof will proceed in two stages. The first lemma I will prove is:

Lemma 1

y Id = y (Env A) id_{A}

Here Env A is the environment functor (it is also a monad) aka the reader functor, and id is the identity function. To prove our lemma it suffices to show that y Id a = y (Env A) id a for an arbitrary a : A. We will use the free theorem to prove this with a natural transformation from (Env A) to Id defined as

η_{1} : ∀α. Env Aα → Id α η_{1} := Λα. λh. ha

However, we must first prove that this is a natural transformation; i.e. we need to prove that map_{Id}g ∘ η_{1C} = η_{1D} ∘ map_{(Env A)}g:

map_{Id}g (η_{1C}h) =
g (ha) =
(g ∘ h) a =
η_{1D} (map_{(Env A)}gh)

Now we can apply our free theorem using the natural transformation &eta_{1} to prove the lemma.

y Id a =
y Id (η_{1A} id_{A}) =
η_{1B} (y (Env A) id_{A}) =
y (Env A) id_{A}a

This completes Lemma 1. To finish our proof of the isomorphism we only need to prove Lemma 2:

Lemma 2

map_{κ} (y (Env A) id_{A}) l = yκl

To prove this we use the free theorem with a new natural transformation from Env A to κ:

Now we can apply our free theorem using the natural transformation η_{2} to prove Lemma 2.

map_{κ} (y (Env A) id_{A}) l =
η_{2B} (y (Env A) id_{A}) =
yκ (η_{2A} id_{A}) =
yκ (map_{κ} id_{A} l) =
yκl

This completes the proof of the isomorphism. Perhaps it can be simplified by combining the two step into one, but I am satisfied with this two step process.