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

Question

我注意到 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绑定实际上是伪装成函数绑定的，那么为什么上面两个代码片段不等价呢？

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

- Theelepel

---

你根本不需要显式地引入任何类型变量：fooType (Foo x) = typeRep [x] 也可以工作，利用 typeRep 的 proxy 可以是任何函子的事实：不一定是平凡的 Proxy，它也可以是实际包含 a 值的东西！ - leftaroundabout

如果我们要摆脱类型变量，甚至可以更进一步，只需说 fooType (Foo x) =typeOf x。我假设真正的用例是需要访问类型变量的重要部分。 - Carl

@Carl，是的，但也许不是很常知道带有“proxy x”参数的任何函数也可以用包含实际“x”值的具体容器来调用。 - leftaroundabout

实际上，我意识到在这种情况下我可以使用typeOf或其他解决方案（请参见括号中问题的最后一段），但在我的真实代码中却不可用。我需要通过将类型变量放入类型引用中来获取Template Haskell Type。我也不能直接在顶层函数中绑定a，因为我正在尝试获取的类型实际上是隐藏类型的功能依赖项。辅助函数解决方案很好用，只是我真的不明白为什么。 - Theelepel

let不能做到这一点，因为它使用惰性模式匹配，而且无法将类型类字典引入作用域。这是与https://dev59.com/iGAg5IYBdhLWcg3wfrAn#23540431相同的问题。 - chi

Answer 1

重要的是，函数实际上是伪装成case表达式而不是let表达式。 case匹配和let匹配具有不同的语义。这也是为什么您无法在let表达式中匹配执行类型细化的GADT构造函数的原因。

区别在于case匹配在继续之前评估被匹配的值，而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)

- Carl

---

我不能在我的代码中使用提供的解决方案，但是关于case和let表达式的解释确实回答了我的问题。这是比使用辅助函数更优雅的解决方案。谢谢！ - Theelepel

需要使用STV吗？如果您真的想使用typeRep，则fooType（Foo x）= typeRep [x]或fooType（Foo x）= typeOf x。 - Daniel Wagner