我們可以在 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))
uj5u.com熱心網友回復：
我相信沒有好的術語型別Leibniz Bool (Either One One)。確實，有些“奇怪”f的地方我們無法進行這種轉換；一個簡單的例子是Bool :~: Bool有人居住但Bool :~: Either One One沒有，所以如果f = (:~:) Bool沒有 type 的功能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是相反的。
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/427244.html