Types we can prove things about in Haskell-CodePudding

Can we prove isomorphism involving native types in Haskell ?

import Prelude

newtype Leibniz a b = Leibniz {unLeibniz :: forall f. f a -> f b}


data One = One

-- `u` and `v` are inverse
u :: Bool -> Either One One
u b = if b then Right One else Left One

v :: Either One One -> Bool
v = \case
  (Left _) -> False
  (Right _) -> True

--- Can we prove proof that ?
p :: Leibniz Bool (Either One One)
p = Leibniz (\(x :: f Bool) -> __ :: f (Either One One))

CodePudding user response：

I believe there is no good term of type Leibniz Bool (Either One One). Indeed, there are "strange" fs where we can't do that conversion; the trivial example is that Bool :~: Bool is inhabited but Bool :~: Either One One isn't, and so if f = (:~:) Bool then there is no function of type f Bool -> f (Either One One).

BUT if you modify Leibniz slightly:

newtype Leibniz a b = Leibniz {unLeibniz :: forall f. IsoFunctor f => f a -> f b}

Here, IsoFunctor is a new class like Functor except it demands pure mappings in both directions:

class IsoFunctor f where isomap :: (a -> b) -> (b -> a) -> f a -> f b

This class rules out types whose argument is nominal, rather than representational, like (:~:) Bool. (And, in the other direction, an instance can always be written for types that have the right kind and are representational in their argument.) Then we can write:

p :: Leibniz Bool (Either One One)
p = Leibniz (isomap u v)

Unfortunately, the compiler doesn't (and in general, can't) guarantee that u and v are inverse.