我们可以在 Haskell 中证明的类型

Question

我们可以证明 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))

Answer 1

我相信没有什么好的术语类型Leibniz Bool (Either One One)。事实上，有些“奇怪”f的地方我们无法进行这种转换；一个简单的例子是 是Bool :~: Bool有人居住的，但Bool :~: Either One One没有，所以如果f = (:~:) Bool那么 就没有类型 的函数f Bool -> f (Either One One)。

但是如果你Leibniz稍微修改一下：

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

这IsoFunctor是一个新类，Functor除了它需要双向的纯映射之外：

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

此类排除了其参数是名义性的而不是代表性的类型，例如(:~:) Bool. （并且，在另一个方向上，始终可以为具有正确类型并且在其参数中具有代表性的类型编写实例。）然后我们可以编写：

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

不幸的是，编译器不（并且通常不能）保证u和v是逆的。