为什么Haskell的作用域类型变量不允许在模式绑定中绑定类型变量？

Question

我注意到GHC ScopedTypeVariables能够在函数模式中绑定类型变量,但不能让模式.

作为一个最小的例子,考虑类型

data Foo where Foo :: Typeable a  => a -> Foo

如果我想访问Foo中的类型,则以下函数无法编译:

fooType :: Foo -> TypeRep
fooType (Foo x) =
    let (_ :: a) = x
    in typeRep (Proxy::Proxy a)

但是使用这个技巧将类型变量绑定移动到函数调用,它可以正常工作:

fooType (Foo x) =
    let helper (_ :: a) = typeRep (Proxy::Proxy a)
    in helper x

由于let绑定实际上是伪装的函数绑定,为什么上面两个代码片段不等同？

(在这个例子中,其他解决方案是创建TypeRepwith typeOf x,或者直接绑定变量,就像x :: a在顶级函数中一样.这些选项都不在我的实际代码中,并且使用它们不回答问题.)

Answer 1

最重要的是,函数是case伪装的let表达式,而不是表达式. case匹配和let匹配具有不同的语义.这也是您无法匹配在let表达式中进行类型细化的GADT构造函数的原因.

不同之处在于case匹配在继续之前评估scrutinee,而let匹配将thunk抛到堆上,表示"在需要结果时执行此评估".GHC不知道如何a在懒惰可能与它们交互的所有潜在方式中保留本地范围的类型(如在您的示例中),因此它不会尝试.如果涉及本地范围的类型,请使用case表达式,使懒惰不会成为问题.

至于你的代码,ScopedTypeVariables实际上为你提供了一个更简洁的选择:

{-# Language ScopedTypeVariables, GADTs #-}

import Data.Typeable
import Data.Proxy

data Foo where
    Foo :: Typeable a => a -> Foo

fooType :: Foo -> TypeRep
fooType (Foo (x :: a)) = typeRep (Proxy :: Proxy a)