haskell - GADT 扩展会破坏多态性吗？

Question

是分机GADT在 Haskell 中破坏多态性，即使在不使用 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

可以通过复制绑定(bind)来修复

{-# 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

这有什么深层次的原因吗？

Answer 1

启用 GADTs我们还隐式启用 MonoLocalBinds 这可以防止某些形式的 let - 和 where - 类型概括。
这会影响类型变量部分量化(i 下文)和部分自由(r 下文)的类型。

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

一个简单的解决方案是提供显式类型注释以强制进行所需的泛化。
文档提供了 MonoLocalBinds 的基本原理，说明为什么在某些情况下限制泛化是有意义的。一个 blog post从 2010 年开始提供进一步的讨论。
博客中 Simon Peyton-Jones 的相关引用(稍微重新格式化，并使用与原始博客中相同的链接):

Why did we make it?

It’s a long story, but the short summary is this: I don’t know how to build a reliable, predictable type inference engine for a type system that has both

• (a) generalisation of local let/where and
• (b) local type equality assumptions, such as those introduced by GADTs.

The story is told in our paper “Let should not be generalised” and, at greater length, in the journal version “Modular type inference with local assumptions”.