GADT 扩展是否破坏了多态性？

问题描述

Haskell 中的扩展 GADT 是否破坏了多态性，即使是在不使用 GADT 的代码中？

这是一个有效且不使用 GADT 的示例


{-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum ys f))
                        where
                                bsum  = unRet . r

如果启用了 GADTs，我们会得到一个编译错误

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum ys f)) -- error
                        where
                                bsum  = unRet . r
-- • Occurs check: cannot construct the infinite type: i1 ~ r i1
--   Expected type: r (r i1)
--     Actual type: r i1
-- • In the first argument of ‘bsum’,namely ‘ys’
--   In the expression: bsum ys f
--   In the second argument of ‘bsum’,namely ‘(\ ys -> bsum ys f)’
-- • Relevant bindings include

可以通过复制绑定来修复

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum2 ys f))
                        where
                                bsum   = unRet . r
                                bsum2  = unRet . r

有什么深层原因吗？

解决方法

启用 GADTs 我们也隐式启用 MonoLocalBinds 以防止某些形式的 let- 和 where- 类型泛化。

这会影响类型变量部分量化（下面的i）和部分自由（下面的r）的类型。

where bsum :: forall i. r i -> (i -> Int) -> Int
      bsum = unRet . r

一个简单的解决方案是提供一个明确的类型注释，以强制实现所需的泛化。

文档提供了 MonoLocalBinds 的基本原理，说明了为什么在某些情况下限制泛化是有意义的。 2010 年的 blog post 提供了进一步的讨论。

Simon Peyton-Jones 在博客中的相关引述（稍微重新格式化，并使用与原始博客中相同的链接）：

我们为什么要这样做？

这是一个很长的故事，但简短的总结是：我不知道如何为具有两者的类型系统构建一个可靠的、可预测的类型推理引擎

(a) 本地 let/where 和
(b) 局部类型相等假设，例如 GADT 引入的假设。

这个故事在我们的论文“Let should not be generalised”中讲述，在更大的篇幅中，在期刊版本“Modular type inference with local assumptions”中。

gadt haskell haskell polymorphism polymorphism