模式匹配rank-2类型 [英] Pattern matching on rank-2 type

问题描述

  { - ＃ LANGUAGE RankNTypes，FlexibleContexts＃ - } 
 
 module Foo其中
 
将Data.Vector.Generic.Mutable作为M 
导入Data.Vector.Generic作为V 
 import Control.Monad.ST 
 import Control.Monad.Primitive 
 
 data DimFun vmr = 
 DimFun {dim :: Int，func :: v（PrimState m）r - > m（）} 
 
 runFun1 ::（Vector v r，MVector（Mutable v）r）=> 
（m 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 
ty 
 unsafeFreeze y 
 
 runFun2 ::（Vector vr，MVector（Mutable v） r）=> 
（m m。（PrimMonad m）=> DimFun（Mutable v）m r） - > v r  - > vr 
 runFun2 tx = runST $ do 
y<  -  thaw x 
 evalFun ty 
 unsafeFreeze y 
 
 evalFun ::（PrimMonad m，MVector vr） => DimFun v m r  - > v（PrimState m）r  - > m（）
 evalFun（DimFun dim f）y | dim == M.length y = fy 
  

runFun2 编译罚款（GHC-7.8.2），但 runFun1 导致错误：

 无法从上下文（Vector vr，MVector（Mutable v）r）
引发由模式
产生的（PrimMonad m0）
由
类型签名绑定tfb： ：（Vector vr，MVector（Mutable v）r）=> 
（forall（m :: *  - > *）。PrimMonad m => TensorFunc m r） - > v r  - > vr 
在Testing / Foo.hs：（26,8） - （28,15）
类型变量'm0'不明确
注意：有几个潜在的实例：
实例PrimMonad IO  - 在'Control.Monad.Primitive'中定义
实例PrimMonad（ST s） - 在'Control.Monad.Primitive'中定义
在模式中：TensorFunc _ f 
在'tfb'的等式中：
 tfb（TensorFunc_f）x 
 = runST 
 $ do {y < -  thaw x; 
 f y; 
 unsafeFreeze y} 
 
无法将类型'm0'与'ST s'
匹配，因为类型变量's'将会转义其范围
这个（刚性的， （29,26） - （32,18）
期望的类型（$）
类型变量受上下文期望的
a类型的约束：ST s（vr）
 at Testing / Foo.hs： ：ST s（）
实际类型：m0（）
相关绑定包括
y :: Mutable vsr（绑定在Testing / Foo.hs：30：3）
f :: forall （v :: *  - > *  - > *）。 
 MVector v r => 
 v（PrimState m0）r  - > 
在'do'块的语句中：fy 
在'（$）'的第二个参数中，m0（）
（在Testing / Foo.hs：29：即
'do {y < -  thaw x; 
 f y; 
 unsafeFreeze y}'
 
从上下文（Vector vr，MVector（Mutable v）r）
无法推断出（s〜PrimState m0）
 
的类型签名tfb ::（Vector vr，MVector（Mutable v）r）=> 
（forall（m :: *  - > *）。PrimMonad m => TensorFunc m r） - > v r  - > vr 
在Testing / Foo.hs：（26,8） - （28,15）
's'是由上下文期望的
a类型限制的刚性类型变量：ST s（ vr）在Testing / Foo.hs：29：26 
期望类型：Mutable v（PrimState m0）r 
实际类型：Mutable vsr 
相关绑定包括
y :: Mutable vsr （绑定在Testing / Foo.hs：30：3）
f :: forall（v :: *  - > *  - > *）。 
 MVector v r => 
 v（PrimState m0）r  - > 
在'f'的第一个参数中，即'y'
在'do'块的句柄中，m0（）
（在Testing / Foo.hs中绑定：29：19） ：fy 
  

我非常确定2级的归咎于可能是由单态限制。但是，正如我的上一个问题中所建议的，我启用了 -XNoMonomorphismRestriction ，但得到相同的错误。

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

$ b $我认为在这里涉及的类型级管道的粗略心理模型是必不可少的，所以我要去谈论隐含的东西在稍微详细一点，然后才能仔细检查你的问题。读者只对这个问题的直接解决方案感兴趣，可以跳到对多态性值进行模式匹配小节并结束。

1。隐式函数参数

类型参数

GHC将Haskell编译为一种名为Core的小型中间语言， rank-n多态的类型lambda演算称为系统F（加上一些扩展）。下面我将使用Haskell以及有点类似于Core的符号;我希望这不是太混乱。在Core中，多态函数是将类型作为附加参数的函数，更深层次的参数可以引用这些类型或 这些类型：

   - 在Haskell中
 const :: forall（a :: * ）（b :: *）。 a  - > b  - > a 
 const x y = x 
 
  -  in pseudo-Core 
 const'::（a :: *） - > （b :: *） - > a  - > b  - > a 
 const'abxy = x 
  

这意味着我们还必须为这些类型提供参数每当我们想使用它们时都会运行。在Haskell类型推断中，通常会自动找出类型参数并提供它们，但是如果我们查看Core输出（例如，请参阅>介绍），类型参数和应用程序在任何地方都是可见的。构建一个这样的心理模型可以使得更高级的代码变得更容易：

   -  Haskell 
 poly ::（全部a  -  a> a） - > b  - > （int，b）
 poly f x =（f 0，f x）
 
  -  pseudo-Core 
 poly'::（b :: *） - > （（a :: *） - > a  - > a） - > b  - > （Int，b）
 poly'bfx =（f Int 0，fbx）
  

它清楚地表明为什么有些东西不会检测：

  wrong ::（a  - > a） - > （Int，Bool）
错误f =（f 0，f True）
 
错误'::（a :: *） - > （a  - > a） - > （Int，Bool）
错误'a f =（f？，f？） -  f需要一个a，而不是Int或Bool。 
  

类约束参数

   -  Haskell 
 show :: forall a。显示a => a  - >字符串
显示x =显示x 
 
  - 伪核心
显示'::（a :: *） - >显示 - > a  - > String 
 show'a（ShowDict showa）x = showa x 
  

什么是 ShowDict 和在这里显示一个？ ShowDict 只是一个包含 show 实例的Haskell记录，而GHC为每个类的实例生成这样的记录。 显示一个就是这个实例记录的类型：

   - 我们将类翻译为记录类型：
 class显示where show :: a  - >字符串
 
数据显示a = ShowDict（show :: a  - >字符串）
 
  - 将实例转换为类类型的具体记录：
 instance Show（）where show（）=（）
 
 showUnit :: Show（）
 showUnit = ShowDict（\（） - >（））
  

例如，无论何时我们想要应用 show ，编译器必须搜索范围才能找到合适的类型参数和该类型的实例字典。请注意，虽然实例总是处于顶层，但在多态函数中经常会将实例作为参数传递：

  data Foo = Foo 
 
  -  instance Show Foo where show _ =Foo
 showFoo :: Show Foo 
 showFoo = ShowDict（\_  - > Foo）
 
  - 编译器填充顶层实例
 fooStr :: String 
 fooStr = show'Foo showFoo Foo 
 
 polyShow ::（Show a，Show b）=> a  - > b  - >字符串
 polyShow ab =显示a ++显示b 
 
  - 在这里，我们将实例作为参数获取（另请注意（++）如何还需要额外的
  - （++）:: forall a。[a]  - > [a]  - > [a]）
 polyShow'::（a :: *） - > （b :: *） - >显示 - >显示b  - > a  - > b  - >字符串
 polyShow'a b（ShowDict showa）（ShowDict showb）a b  - > （++）char（showa a）（showb b）
  

多态值匹配模式

在Haskell中，函数的模式匹配没有意义。多态值也可以看作是函数，但我们可以在它们上模式匹配，就像在OP的错误的 runfun1 例子中一样。但是，所有隐含的参数必须在范围内可以推断，否则模式匹配仅仅是一种类型错误：

  import Data.Monoid 
 
  - 即使我们不使用a或n，也是一种类型错误。 
  -  foo ::（forall a。Monoid a =>（a，Int）） - > Int 
  -  foo（a，n）= 0 
 
 foo ::（（a :: *） - > Monoid a  - >（a，Int）） - > Int 
 foo f =？ - 我们要用什么来f？ 
  

换言之，通过对多态值进行模式匹配，我们断言所有隐式参数已被应用。在 foo 的情况下，虽然在Haskell中没有类型应用的语法，但我们可以在类型注释中使用：

  { - ＃LANGUAGE ScopedTypeVariables，RankNTypes＃ - } 
 
 foo ::（forall a。Monoid a =>（a，Int）） - > （_，n） - >的Int 
 foo x = case（x ::（String，Int）） n 
 
  - 或者
 foo（（_ :: String），n）= n 
  

同样，伪核心使情况更加清晰：

  foo ::（（a： ：*） - > Monoid a  - >（a，Int）） - > Int 
 foo f = case f（_，n） - >的字符串monoidString n 
  

这里 monoidString 是一些可用的 Monoid 字符串。

2的实例。隐式数据字段

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

• 当我们构造函数时，隐式参数在函数体中可用。
  
• 当我们应用函数时，我们有额外的义务可以完成。


• 当我们使用隐式字段构造数据时，我们必须提供这些额外的字段。
  
• 当我们的数据模式匹配时，隐式字段也包含在内。

标准示例：

  { - ＃LANGUAGE GADTs＃ - } 
 
 data Showy where 
 Showy :: forall a。显示a => a  - > Showy 
 
  - 伪核心
数据Showy在哪里
 Showy ::（a :: *） - >显示 - > a  - > Showy 
 
  - 当构造Showy时，Show a必须可用：
 someShowy :: Showy 
 someShowy = Showy（300 :: Int）
 
  - 在伪核心
 someShowy'= Showy Int showInt 300 
 
  - 当在Showy上进行模式匹配时，我们得到一个范围内的实例
 showShowy :: Showy  - > String 
 showShowy（Showy x）= show x 
 
 showShowy':: Showy  - > String 
 showShowy'（Showy a showa x）= showa x 
  

3。看看OP的例子

我们有函数

$ $ p $ runFun1 ::（Vector vr，MVector（Mutable v）r）=>
（m 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
ty
unsafeFreeze y


请记住，对多态值进行模式匹配会断言所有隐式参数都在范围中可用。除此之外，在模式匹配的地方，根本没有 m ，更不用说 PrimMonad 实例为了它。

使用GHC 7.8.x，最好使用 {b

  runFun1 ::（Vector vr，MVector（Mutable v）r）=> 
（m 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 没有被限制在任何地方。事实上，这是一个臭名昭着的模棱两可型变量，由GHC作为一个占位符变成了一个名词。

所以，为什么我们不尝试手动提供参数，就像之前的 Monoid 实例？我们知道我们将在 ST 动作中使用 t ，所以我们可以尝试修改 m 作为 ST s 和GHC自动为我们应用 PrimMonad 实例：

  runFun1 :: forall v r。 （Vector v r，M Vector（Mutable v）r）=> 
（m 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 
ty 
 unsafeFreeze y 
  

...除非它不起作用，并且我们得到错误无法与's1'匹配类型''，因为类型变量's1'会转义其范围。



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

  runST ::（全部。 ST sa） - > a 
  

我们可以想象 runST 需要一个函数类型为（（s :: PrimState ST） - > ST sa），然后我们的代码如下所示：

  runST $ \s  - > do 
 y<  -  thaw x  -  y :: Mutable v s r 
 t y  -  error：t以不同的s取代Mutable v s r。 
 unsafeFreeze y 
  

s 在 t 的参数类型中默认引入了最外层的范围：



  runFun1 :: forall vs r。 ... 
  

因此，这两个 s - 是不同的。



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

  runFun1 :: forall v r。 （Vector v r，M Vector（Mutable v）r）=> 
（所有m，PrimMonad m => DimFun（Mutable v）m r） - > v r  - > v r 
 runFun1 dimfun x = runST $ do 
 y < - 解冻x 
 $ dim $ $ b $ dimFun dim t | dim == M.length y  - > ty 
 unsafeFreeze y 
  

使某些参数明确：

  runST $ \s  - > do 
 y<  - 解冻x 
 case dimfun（ST s）primMonadST 
 DimFun dim t | dim == M.length y  - > ty 
 unsafeFreeze y 
  

作为练习，我们将所有函数转换为伪核（但是我们不要去掉 do 语法，因为这太丑陋了）：



   - 所涉及函数的完整类型，供参考
解冻:: forall mv a。 （PrimMonad m，V.Vector v a）=> v a  - > m（V.Mutable v（PrimState m）a）
 runST :: forall a。 （全部ST ST） - > 
 unsafeFreeze :: forall m v a。 （PrimMonad m，Vector v a）=>可变v（PrimState m）a  - > v a 
 M.length :: forall v s a。 MVector v s a  - > Int 
（==）:: forall a。公式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  - > （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 
 unsafeFreeze（ST s）v primMonadST vecInstance y 
  

这真是一口。

现在我们已经准备好解释为什么 runFun2 起作用了：

  runFun2 ::（Vector vr，MVector（Mutable v）r）=> 
（m m。（PrimMonad m）=> DimFun（Mutable v）m r） - > v r  - > vr 
 runFun2 tx = runST $ do 
y<  -  thaw x 
 evalFun ty 
 unsafeFreeze y 
 
 evalFun ::（PrimMonad m，MVector vr） => DimFun v m r  - > v（PrimState m）r  - > m（）
 evalFun（DimFun dim f）y | dim == M.length y = fy 
  

evalFun 只是一个多态函数，它在正确的位置被调用（我们最终在正确的地方匹配 t ），其中正确的 ST s 可用作 m 参数。

随着类型系统变得越来越复杂，模式匹配变得越来越严重，带来了深远的后果和不平凡的需求。在谱图的最后，您可以找到完全相关的语言和证明助手，例如Agda，Idris或Coq，其中对数据的模式匹配可能意味着在程序的某个分支中接受任意逻辑命题。

I'm trying to understand why one version of this code compiles, and one version does not.

{-# 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 compiles fine (GHC-7.8.2), but runFun1 results in errors:

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

I'm pretty sure the rank-2 type is to blame, possibly caused by a monomorphism restriction. However, as suggested in a previous question of mine, I enabled -XNoMonomorphismRestriction, but got the same error.

What is the difference between these seemingly identical code snippets?

解决方案

I think that having a rough mental model of the type-level plumbing involved here is essential, so I'm going go talk about "implicit things" in a bit more detail, and scrutinize your problem only after that. Readers only interested in the direct solution to the question may skip to the "Pattern matching on polymorhpic values" subsection and the end.

1. Implicit function arguments

Type arguments

GHC compiles Haskell to a small intermediate language called Core, which is essentially a rank-n polymorphic typed lambda calculus called System F (plus some extensions). Below I am going use Haskell alongside a notation somewhat resembling Core; I hope it's not overly confusing.

In Core, polymorphic functions are functions which take types as additional arguments, and arguments further down the line can refer to those types or have those types:

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

This means that we must also supply type arguments to these functions whenever we want to use them. In Haskell type inference usually figures out the type arguments and supplies them automatically, but if we look at the Core output (for example, see this introduction for how to do that), type arguments and applications are visible everywhere. Building a mental model of this makes figuring out higher-rank code a whole lot easier:

-- 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)

And it makes clear why some things don't typecheck:

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. 

Class constraint arguments

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

What is ShowDict and Show a here? ShowDict is just a Haskell record containing a show instance, and GHC generates such records for each instance of a class. Show a is just the type of this instance record:

-- 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 (\() -> "()")

For example, whenever we want to apply show, the compiler has to search the scope in order to find a suitable type argument and an instance dictionary for that type. Note that while instances are always top level, quite often in polymorphic functions the instances are passed in as arguments:

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) 

Pattern matching on polymorphic values

In Haskell, pattern matching on functions doesn't make sense. Polymorphic values can be also viewed as functions, but we can pattern match on them, just like in OP's erroneous runfun1 example. However, all the implicit arguments must be inferable in the scope, or else the mere act of pattern matching is a type error:

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?

In other words, by pattern matching on a polymorphic value, we assert that all implicit arguments have been already applied. In the case of foo here, although there isn't a syntax for type application in Haskell, we can sprinkle around type annotations:

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

Again, pseudo-Core makes the situation clearer:

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

Here monoidString is some available Monoid instance of String.

2. Implicit data fields

Implicit data fields usually correspond to the notion of "existential types" in Haskell. In a sense, they are dual to implicit function arguments with respect to term obligations:

• When we construct functions, the implicit arguments are available in the function body.
• When we apply functions, we have extra obligations to fulfill.
• When we construct data with implicit fields, we must supply those extra fields.
• When we pattern match on data, the implicit fields also come into scope.

Standard example:

{-# 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. Taking a look at OP's example

We have the function

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

Remember that pattern matching on polymorphic values asserts that all implicit arguments are available in the scope. Except that here, at the point of pattern matching there is no m at all in scope, let alone a PrimMonad instance for it.

With GHC 7.8.x it's is good practice to use type holes liberally:

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 = _

Now GHC will duly display the type of the hole, and also the types of the variables in the context. We can see that t has type Mutable v (PrimState m0) r -> m0 (), and we also see that m0 is not listed as bound anywhere. Indeed, it is a notorious "ambiguous" type variable conjured up by GHC as a placeholder.

So, why don't we try manually supplying the arguments, just as in the prior example with the Monoid instance? We know that we will use t inside an ST action, so we can try fixing m as ST s and GHC automatically applies the PrimMonad instance for us:

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

... except it doesn't work and we get the error "Couldn't match type ‘s’ with ‘s1’ because type variable ‘s1’ would escape its scope".

It turns out - comes as no surprise - that we've forgotten about yet another implicit argument. Recall the type of runST:

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

We can imagine that runST takes a function of type ((s :: PrimState ST) -> ST s a), and then our code looks like this:

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 

The s in t's argument type is silently introduced at the outermost scope:

runFun1 :: forall v s r. ...

And thus the two s-es are distinct.

A possible solution is to pattern match on the DimFun argument inside the ST action. There, the correct s is in scope, and GHC can supply ST s as 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

With some parameters made explicit:

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

As an exercise, let's convert all of the function to pseudo-Core (but let's not desugar the do syntax, because that would be way too ugly):

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

That was a mouthful.

Now we are well-equipped to explain why runFun2 worked:

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 is just a polymorphic function that gets called in the right place (we ultimately pattern match on t in the right place), where the correct ST s is available as the m argument.

As a type system gets more sophisticated, pattern matching becomes a progressively more serious affair, with far-reaching consequences and non-trivial requirements. At the end of the spectrum you find full-dependent languages and proof assistants such as Agda, Idris or Coq, where pattern matching on a piece of data can mean accepting an arbitrary logical proposition as true in a certain branch of your program.

这篇关于模式匹配rank-2类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！