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

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

type-conversion haskell

nicolas · 技术社区 · 2 年前

我们能证明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 回复 | 直到 2 年前

Daniel Wagner 2 年前

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

推荐文章

Azathoth · 当使用过滤器不删除任何案例时,涉及空列表的案例不会编译

2 年前

Ethan Smallwood · Haskell从列表中的记录获取数据

2 年前

trpnd · 如何定义由两个任意单声道变压器组成的单声道变压器?

2 年前

Delfin · Haskell从do符号到Applicative符号的传递(第2部分)

2 年前

Fabus1184 · Haskell mapM_不打印

2 年前

Gotthold · 基于范数约束向量的类型

2 年前

dmcdo · 有没有一种干净的方法可以在一个表达式中得到列表的开头和结尾?

2 年前

jian · haskell将另一个函数用作输入参数

2 年前

Jocafrei · 用Haskell函数实现最大公约数函数

6 年前

pcoppi · 尝试在Haskell和根据-Wall编写函数时,我需要一个匹配(\u:\ u:\ u)的模式。这个模式意味着什么,为什么我需要它?

6 年前