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

【问题标题】：Why do Haskell's scoped type variables not allow binding of type variables in pattern bindings?为什么 Haskell 的作用域类型变量不允许在模式绑定中绑定类型变量？
【发布时间】：2017-09-06 14:09:07
【问题描述】：

我注意到 GHC 的 ScopedTypeVariables 能够在函数模式中绑定类型变量，但不能在 let 模式中。

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

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绑定实际上是变相的函数绑定，为什么上面两个代码sn-ps不等价呢？

（在本例中，其他解决方案是使用typeOf x 创建TypeRep，或在顶级函数中直接将变量绑定为x :: a。这些选项在我的真实代码中均不可用，并且使用它们并不能回答问题。）

【问题讨论】：

您根本不需要显式引入任何类型变量：fooType (Foo x) = typeRep [x] 也可以使用，因为typeRep 的proxy 可以是任何函子：不一定是微不足道的Proxy，也可以是实际包含 a 值的东西！
@leftaroundabout 如果我们要摆脱类型变量，您可以更进一步，只需说fooType (Foo x) = typeOf x。我继续假设真正的用例是访问类型变量是重要部分。
@Carl 是的，但可能并不为人所知的是，带有 proxy x 参数的 any 函数也可以使用包含实际 x 值的具体容器来调用。
确实，我意识到在这种情况下我可以使用typeOf 或其他解决方案（请参阅括号中问题的最后一段），但在我的真实代码中不可用。我需要通过将类型变量放在类型引号中来获得模板 Haskell Type。我也不能直接在顶层函数中绑定a，因为我要获取的类型实际上是隐藏类型的函数依赖。辅助函数解决方案工作正常，我只是不明白为什么。
let 不能这样做，因为它使用惰性模式匹配，并且不能将类型类字典带入范围。这是stackoverflow.com/a/23540431/3234959的同一个问题

标签： haskell ghc

【解决方案1】：

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

不同之处在于case 匹配在继续之前评估检查者，而let 匹配会在堆上抛出一个提示“在需要结果时执行此评估”。 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)

【讨论】：

我不能在我的代码中使用提供的解决方案，但是对 case 和 let 表达式的解释确实回答了这个问题。这是一个比使用辅助函数更优雅的解决方案。谢谢！
是否还需要 STV？ fooType (Foo x) = typeOf x 或 fooType (Foo x) = typeRep [x] 如果您出于某种原因真的想使用 typeRep。