haskell - 我们可以在 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(二选一)。

但是如果你稍微修改 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 是相反的。