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

html5 • • 问答

GADTHaskell 中的扩展是否破坏了多态性，即使在不使用 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 年的一篇博客文章提供了进一步的讨论。

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

为什么我们做到了？

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

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

这个故事在我们的论文“ Let不应该被概括”以及更详细的期刊版本“具有局部假设的模块化类型推断”中讲述。

  • To note : adding type signature mentioning `r` requires : 1) `ScopedTypeVariables` extension and 2) an explicit quantification on `forall r.` at some level above
以上是GADT扩展是否会破坏多态性？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>