代码之家 › 专栏 › 技术社区 › nicolas

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

type-conversion haskell

0

nicolas · 技术社区 · 4 年前

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

0 回复 | 直到 4 年前

1

5

Daniel Wagner 4 年前

我相信没有好的类型术语 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 相反。