haskell - rank-2 类型的模式匹配

Question

我试图理解为什么这个代码的一个版本可以编译，而一个版本不能。

{-# LANGUAGE RankNTypes, FlexibleContexts #-}

module Foo where

import Data.Vector.Generic.Mutable as M
import Data.Vector.Generic as V
import Control.Monad.ST
import Control.Monad.Primitive

data DimFun v m r = 
  DimFun {dim::Int, func :: v (PrimState m) r -> m ()}

runFun1 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 (DimFun dim t) x | V.length x == dim = runST $ do
  y <- thaw x
  t y
  unsafeFreeze y

runFun2 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun2 t x = runST $ do
  y <- thaw x
  evalFun t y
  unsafeFreeze y

evalFun :: (PrimMonad m, MVector v r) => DimFun v m r -> v (PrimState m) r -> m ()
evalFun (DimFun dim f) y | dim == M.length y = f y

runFun2编译良好 (GHC-7.8.2)，但 runFun1导致错误:

Could not deduce (PrimMonad m0) arising from a pattern
from the context (Vector v r, MVector (Mutable v) r)
  bound by the type signature for
             tfb :: (Vector v r, MVector (Mutable v) r) =>
                    (forall (m :: * -> *). PrimMonad m => TensorFunc m r) -> v r -> v r
  at Testing/Foo.hs:(26,8)-(28,15)
The type variable ‘m0’ is ambiguous
Note: there are several potential instances:
  instance PrimMonad IO -- Defined in ‘Control.Monad.Primitive’
  instance PrimMonad (ST s) -- Defined in ‘Control.Monad.Primitive’
In the pattern: TensorFunc _ f
In an equation for ‘tfb’:
    tfb (TensorFunc _ f) x
      = runST
        $ do { y <- thaw x;
               f y;
               unsafeFreeze y }

Couldn't match type ‘m0’ with ‘ST s’
  because type variable ‘s’ would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context: ST s (v r)
  at Testing/Foo.hs:(29,26)-(32,18)
Expected type: ST s ()
  Actual type: m0 ()
Relevant bindings include
  y :: Mutable v s r (bound at Testing/Foo.hs:30:3)
  f :: forall (v :: * -> * -> *).
       MVector v r =>
       v (PrimState m0) r -> m0 ()
    (bound at Testing/Foo.hs:29:19)
In a stmt of a 'do' block: f y
In the second argument of ‘($)’, namely
  ‘do { y <- thaw x;
        f y;
        unsafeFreeze y }’

Could not deduce (s ~ PrimState m0)
from the context (Vector v r, MVector (Mutable v) r)
  bound by the type signature for
             tfb :: (Vector v r, MVector (Mutable v) r) =>
                    (forall (m :: * -> *). PrimMonad m => TensorFunc m r) -> v r -> v r
  at Testing/Foo.hs:(26,8)-(28,15)
  ‘s’ is a rigid type variable bound by
      a type expected by the context: ST s (v r) at Testing/Foo.hs:29:26
Expected type: Mutable v (PrimState m0) r
  Actual type: Mutable v s r
Relevant bindings include
  y :: Mutable v s r (bound at Testing/Foo.hs:30:3)
  f :: forall (v :: * -> * -> *).
       MVector v r =>
       v (PrimState m0) r -> m0 ()
    (bound at Testing/Foo.hs:29:19)
In the first argument of ‘f’, namely ‘y’
In a stmt of a 'do' block: f y

我很确定 rank-2 类型是罪魁祸首，可能是由单态限制引起的。但是，正如 previous question 中所建议的那样我的，我启用了 -XNoMonomorphismRestriction ，但得到了同样的错误。

这些看似相同的代码片段有什么区别？

Answer 1

我认为这里涉及的类型级别管道的粗略思维模型是必不可少的，因此我将更详细地讨论“隐式事物”，然后再仔细检查您的问题。只对问题的直接解决方案感兴趣的读者可以跳到“多态值的模式匹配”小节和结尾。

1. 隐式函数参数

类型参数

GHC 将 Haskell 编译为一种称为 Core 的小型中间语言，它本质上是一种称为 System F(加上一些扩展)的 rank-n 多态类型 lambda 演算。下面我将使用 Haskell 和类似于 Core 的符号；我希望它不会过于困惑。

在 Core 中，多态函数是将类型作为附加参数的函数，并且进一步向下的参数可以引用这些类型或具有这些类型:

-- in Haskell
const :: forall (a :: *) (b :: *). a -> b -> a
const x y = x

-- in pseudo-Core
const' :: (a :: *) -> (b :: *) -> a -> b -> a
const' a b x y = x 

这意味着我们还必须在需要使用这些函数时为其提供类型参数。在 Haskell 类型推断中，通常会计算出类型参数并自动提供它们，但是如果我们查看 Core 输出(例如，请参阅此 introduction 了解如何执行此操作)，类型参数和应用程序随处可见。建立一个这样的心智模型可以更容易地找出更高级别的代码:

-- Haskell
poly :: (forall a. a -> a) -> b -> (Int, b)
poly f x = (f 0, f x)

-- pseudo-Core
poly' :: (b :: *) -> ((a :: *) -> a -> a) -> b -> (Int, b)
poly' b f x = (f Int 0, f b x)

它清楚地说明了为什么有些东西不进行类型检查:

wrong :: (a -> a) -> (Int, Bool)
wrong f = (f 0, f True)

wrong' :: (a :: *) -> (a -> a) -> (Int, Bool)
wrong' a f = (f ?, f ?) -- f takes an "a", not Int or Bool. 

类约束参数

-- Haskell
show :: forall a. Show a => a -> String
show x = show x

-- pseudo-Core
show' :: (a :: *) -> Show a -> a -> String
show' a (ShowDict showa) x = showa x 

什么是 ShowDict和 Show a这里？ ShowDict只是一个包含 show 的 Haskell 记录实例，GHC 为类的每个实例生成这样的记录。 Show a只是这个实例记录的类型:

-- We translate classes to a record type:
class Show a where show :: a -> string

data Show a = ShowDict (show :: a -> String)

-- And translate instances to concrete records of the class type:
instance Show () where show () = "()"

showUnit :: Show ()
showUnit = ShowDict (\() -> "()")

例如，每当我们想申请 show ，编译器必须搜索范围以找到合适的类型参数和该类型的实例字典。请注意，虽然实例总是顶级的，但在多态函数中，实例通常作为参数传入:

data Foo = Foo

-- instance Show Foo where show _ = "Foo"
showFoo :: Show Foo
showFoo = ShowDict (\_ -> "Foo")

-- The compiler fills in an instance from top level
fooStr :: String
fooStr = show' Foo showFoo Foo 

polyShow :: (Show a, Show b) => a -> b -> String
polyShow a b = show a ++ show b

-- Here we get the instances as arguments (also, note how (++) also takes an extra
-- type argument, since (++) :: forall a. [a] -> [a] -> [a])
polyShow' :: (a :: *) -> (b :: *) -> Show a -> Show b -> a -> b -> String
polyShow' a b (ShowDict showa) (ShowDict showb) a b -> (++) Char (showa a) (showb b) 

多态值的模式匹配

在 Haskell 中，函数的模式匹配没有意义。多态值也可以被视为函数，但我们可以对它们进行模式匹配，就像 OP 的错误 runfun1例子。但是，所有隐式参数都必须在范围内是可推断的，否则模式匹配的简单行为就是类型错误:

import Data.Monoid

-- it's a type error even if we don't use "a" or "n".
-- foo :: (forall a. Monoid a => (a, Int)) -> Int
-- foo (a, n) = 0 

foo :: ((a :: *) -> Monoid a -> (a, Int)) -> Int
foo f = ? -- What are we going to apply f to?

换句话说，通过对多态值进行模式匹配，我们断言所有隐式参数都已经应用。在 foo的情况下在这里，虽然 Haskell 中没有类型应用的语法，但我们可以散布类型注释:

{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}

foo :: (forall a. Monoid a => (a, Int)) -> Int
foo x = case (x :: (String, Int)) of (_, n) -> n

-- or alternatively
foo ((_ :: String), n) = n 

再次，伪核心使情况更清晰:

foo :: ((a :: *) -> Monoid a -> (a, Int)) -> Int
foo f = case f String monoidString of (_ , n) -> n 

这里 monoidString有没有可用的 Monoid String 的实例.

2.隐式数据字段

隐式数据字段通常对应于 Haskell 中“存在类型”的概念。从某种意义上说，它们是关于术语义务的隐式函数参数的对偶:

当我们构造函数时，隐式参数在函数体中可用。

当我们应用函数时，我们有额外的义务要履行。

当我们用隐式字段构造数据时，我们必须提供那些额外的字段。

当我们对数据进行模式匹配时，隐式字段也进入范围。

标准示例:

{-# LANGUAGE GADTs #-}

data Showy where
    Showy :: forall a. Show a => a -> Showy

-- pseudo-Core
data Showy where
    Showy :: (a :: *) -> Show a -> a -> Showy

-- when constructing "Showy", "Show a" must be also available:
someShowy :: Showy
someShowy = Showy (300 :: Int)

-- in pseudo-Core
someShowy' = Showy Int showInt 300 

-- When pattern matching on "Showy", we get an instance in scope too
showShowy :: Showy -> String
showShowy (Showy x) = show x 

showShowy' :: Showy -> String
showShowy' (Showy a showa x) = showa x

3.看一下OP的例子

我们有这个功能

runFun1 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 dfun@(DimFun dim t) x | V.length x == dim = runST $ do
    y <- thaw x
    t y
    unsafeFreeze y

请记住，多态值的模式匹配断言所有隐式参数都在范围内可用。除了这里，在模式匹配点没有 m在所有范围内，更不用说 PrimMonad例如。

对于 GHC 7.8.x，最好使用 type holes宽松地:

runFun1 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 (DimFun dim t) x | V.length x == dim = _

现在 GHC 将适时显示孔的类型，以及上下文中变量的类型。我们可以看到 t有类型 Mutable v (PrimState m0) r -> m0 () ，我们还看到 m0未在任何地方列为绑定(bind)。事实上，它是一个臭名昭著的“模棱两可”类型变量，由 GHC 作为占位符变出。

那么，为什么我们不尝试手动提供参数，就像在前面的示例中使用 Monoid 一样实例？我们知道我们将使用 t在 ST 内行动，所以我们可以尝试修复 m如 ST s并且 GHC 会自动应用 PrimMonad我们的例子:

runFun1 :: forall v r. (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 (DimFun dim (t :: Mutable v s r -> ST s ())) x 
    | V.length x == dim = runST $ do 
        y <- thaw x
        t y
        unsafeFreeze y

...除了它不起作用，我们收到错误 "Couldn't match type ‘s’ with ‘s1’ because type variable ‘s1’ would escape its scope" .

事实证明——这并不奇怪——我们已经忘记了另一个隐含的论点。回想一下 runST的类型:

runST :: (forall s. ST s a) -> a

我们可以想象 runST采用 ((s :: PrimState ST) -> ST s a) 类型的函数，然后我们的代码如下所示:

runST $ \s -> do
    y <- thaw x   -- y :: Mutable v s r
    t y           -- error: "t" takes a "Mutable v s r" with a different "s". 
    unsafeFreeze y 

s在 t的参数类型是在最外层的范围内默默引入的:

runFun1 :: forall v s r. ...

因此两个 s -es 是不同的。

一个可能的解决方案是在 DimFun 上进行模式匹配ST 操作中的参数。在那里，正确的 s在范围内，GHC 可以提供 ST s如 m :

runFun1 :: forall v r. (Vector v r, MVector (Mutable v) r) => 
    (forall m . PrimMonad m => DimFun (Mutable v) m r) -> v r -> v r
runFun1 dimfun x = runST $ do
    y <- thaw x
    case dimfun of
        DimFun dim t | dim == M.length y -> t y
    unsafeFreeze y

一些参数明确:

runST $ \s -> do
    y <- thaw x
    case dimfun (ST s) primMonadST of
         DimFun dim t | dim == M.length y -> t y
    unsafeFreeze y 

作为练习，让我们将所有函数转换为伪核心(但我们不要对 do 语法进行脱糖，因为那太难看了):

-- the full types of the functions involved, for reference
thaw :: forall m v a. (PrimMonad m, V.Vector v a) => v a -> m (V.Mutable v (PrimState m) a)
runST :: forall a. (forall s. ST s a) -> a
unsafeFreeze :: forall m v a. (PrimMonad m, Vector v a) => Mutable v (PrimState m) a -> v a 
M.length :: forall v s a. MVector v s a -> Int
(==) :: forall a. Eq a => a -> a -> Bool

runFun1 :: 
    (v :: * -> *) -> (r :: *) 
    -> Vector v r -> MVector (Mutable v) r
    -> ((m :: (* -> *)) -> PrimMonad m -> DimFun (Mutable v) m r)
    -> v r -> v r
runFun1 v r vecInstance mvecInstance dimfun x = runST r $ \s -> do
    y <- thaw (ST s) v r primMonadST vecInstance x
    case dimFun (ST s) primMonadST of
        DimFun dim t | (==) Int eqInt dim (M.length v s r y) -> t y
    unsafeFreeze (ST s) v r primMonadST vecInstance y

那是一口。

现在我们已经准备好解释为什么 runFun2工作:

runFun2 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun2 t x = runST $ do
  y <- thaw x
  evalFun t y
  unsafeFreeze y

evalFun :: (PrimMonad m, MVector v r) => DimFun v m r -> v (PrimState m) r -> m ()
evalFun (DimFun dim f) y | dim == M.length y = f y

evalFun只是一个在正确位置调用的多态函数(我们最终在正确的位置对 t 进行模式匹配)，其中正确的 ST s可用作 m争论。

随着类型系统变得越来越复杂，模式匹配变得越来越严重，具有深远的影响和非平凡的要求。在频谱的尽头，您会发现完全依赖的语言和证明助手，例如 Agda、Idris 或 Coq，其中对一段数据进行模式匹配可能意味着在程序的某个分支中接受任意逻辑命题为真。