我们可以在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是相反的。