存在型构造函数的模式绑定

Question

在写Haskell时，他是一个以前接触过Lisp的程序员，但有些奇怪的事情引起了我的注意，但我没能理解。

这可以很好地编译：

{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ExistentialQuantification #-}
data Foo = forall a. Show a => Foo { getFoo :: a }

showfoo :: Foo -> String
showfoo Foo{getFoo} = do
  show getFoo

然而，这一做法失败了：

{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ExistentialQuantification #-}
data Foo = forall a. Show a => Foo { getFoo :: a }

showfoo :: Foo -> String
showfoo foo = do
  let Foo{getFoo} = foo
  show getFoo

对我来说，第二个片段失败的原因并不明显。

问题是：

我是因为哈斯克尔不是同性恋这一事实而错过了什么或导致了这种行为吗？

我的理由是：

1. Haskell需要实现作为编译器扩展的记录模式匹配，因为它选择使用语法而不是数据。
2. 函数头或let子句中的匹配是两个特殊情况。

很难理解这些特殊情况，因为它们既不能执行，也不能直接用语言本身查找。

因此，整个语言的一致行为得不到保障。特别是与额外的编译器扩展一起使用，例如。

ps:编译器错误：

error:
    • My brain just exploded
      I can't handle pattern bindings for existential or GADT data constructors.
      Instead, use a case-expression, or do-notation, to unpack the constructor.
    • In the pattern: Foo {getFoo}
      In a pattern binding: Foo {getFoo} = foo
      In the expression:
        do { let Foo {getFoo} = foo;
             show getFoo }

编辑:对于相同的问题，不同的编译器版本会出现此错误。

* Couldn't match expected type `p' with actual type `a'
    because type variable `a' would escape its scope
  This (rigid, skolem) type variable is bound by
    a pattern with constructor: Foo :: forall a. Show a => a -> Foo

Answer 1

我想了一下这一点，虽然行为一开始似乎很奇怪，但经过一些思考之后，我想人们或许可以这样做：

假设我以你的第二个例子(失败)为例，在进行了一些按摩和价值替换之后，我将其简化为：

data Foo = forall a. Show a => Foo { getFoo :: a }

main::IO()
main = do
    let Foo x = Foo (5::Int)
    putStrLn $ show x

它会产生错误：

无法将预期类型‘p’与实际类型‘a’匹配，因为类型变量‘a’将转义其作用域

如果允许模式匹配，x的类型是什么？好吧..。这种类型当然是Int。但是，Foo的定义表明，getFoo字段的类型是作为Show实例的任何类型。Int是Show的一个实例，但它不是任何类型。这是一个特殊的..。在这方面，封装在Foo中的值的实际特定类型将变为“可见的”(即转义)，从而违背了我们对forall a . Show a =>...的明确保证。

如果我们现在看一下通过在函数声明中使用模式匹配来工作的代码版本：

data Foo = forall a . Show a => Foo { getFoo :: !a }

unfoo :: Foo -> String
unfoo Foo{..} = show getFoo

main :: IO ()
main = do
    putStrLn . unfoo $ Foo (5::Int)

查看unfoo函数，我们看到没有任何东西说Foo内部的类型是任何特定的类型。( Int或其他) ..在该函数的范围内，我们所拥有的只是最初的保证，即getFoo可以是任何类型的Show实例。包裹价值的实际类型仍然是隐藏的和不可知的，所以没有违反任何类型的保证和幸福。

PS:我忘了提到Int位当然是一个例子。在您的示例中，getFoo值内的foo字段的类型是a类型，但这是GHC的类型推断所指的特定(不存在)类型(而不是类型声明中的存在型a )。我只是想出了一个具有特定Int类型的示例，这样就可以更容易、更直观地理解。