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

Question

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

这有什么深层原因吗？

Answer 1

启用 GADTs 我们也隐含地启用了 MonoLocalBinds 以防止某些形式的 let- 和 where- 类型概括。

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

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

一个简单的解决方案是提供显式类型注释，以强制进行所需的泛化。

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

博客中 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”.

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

Is GADT extension destroying polymorphism?

haskell

polymorphism

gadt