存在性构造函数的模式绑定 [英] Pattern bindings for existential constructors

问题描述

在以以前接触过Lisp的程序员的身份编写Haskell的过程中，有些奇怪的事情引起了我的注意，但我不明白.

While writing Haskell as a programmer that had exposure to Lisp before, something odd came to my attention, which I failed to understand.

这可以很好地编译:

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

对我来说，第二个片段为什么失败并不明显.

To me it's not obvious why the second snippet fails.

问题可能是:

我是否错过了某些东西，或者是由于haskell不是谐音这一事实引起的?

Do I miss something or stems this behaviour from the fact that haskell is not homoiconic?

鉴于以下原因，我的推理是:

My reasoning is, given that:

1. Haskell需要将记录模式匹配实现为编译器扩展，因为可以选择使用语法而不是数据.

1. Haskell needs to implement record pattern matching as a compiler extension, because of it's choice to use syntax rather than data.

在函数头或let子句中进行匹配是两种特殊情况.

Matching in a function head or in a let clause are two special cases.

很难理解这些特殊情况，因为它们既无法实现也无法直接在语言本身中查找.

It is difficult to understand those special cases, as they cannot be either implemented nor looked up directly in the language itself.

因此，不能保证整个语言的行为一致.根据示例，尤其是与其他编译器扩展一起使用.

As an effect of this, consistent behaviour throughout the language is not guaranteed. Especially together with additional compiler extensions, as per example.

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 }

对于相同的问题，不同的编译器版本会给出此错误

edit: A different compiler version gives this error for the same problem

* 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

推荐答案

我对此进行了一些思考，尽管起初该行为似乎很奇怪，但经过一番思考，我想一个人也许可以证明这一点:

I thought about this a bit and albeit the behaviour seems odd at first, after some thinking I guess one can justify it perhaps thus:

假设我举第二个(失败)的例子，经过一些按摩和价值替换后，我将其简化为:

Say I take your second (failing) example and after some massaging and value replacements I reduce it to this:

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"会逃避其作用域

Couldn't match expected type ‘p’ with actual type ‘a’ because type variable ‘a’ would escape its scope

如果允许模式匹配，那么x的类型是什么?嗯..当然，类型应该是 Int .但是， Foo 的定义表明， getFoo 字段的类型为任何类型，是 Show 的一个实例.. Int 是 Show 的实例，但不是任何类型..它是特定类型..在这方面，包装在其中的值的实际特定类型该 Foo 将变为可见"(即转义)，因此违反了我们明确保证 forall a.显示一个=> ...

if the pattern matching would be allowed, what would be the type of x? well.. the type would be of course Int. However the definition of Foo says that the type of the getFoo field is any type that is an instance of Show. An Int is an instance of Show, but it is not any type.. it is a specific one.. in this regard, the actual specific type of the value wrapped in that Foo would become "visible" (i.e. escape) and thus violate our explicit guarantee that forall a . Show a =>...

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

If we now look at a version of the code that works by using a pattern match in the function declaration:

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 内部的类型是任何特定类型./code>或其他方式)..在该功能范围内，我们唯一能保证的是 getFoo 可以是 Show 实例的任何类型.包装值的实际类型保持隐藏和不可知，因此不会违反任何类型的保证和幸福感.

Looking at the unfoo function we see that there is nothing there saying that the type inside of the Foo is any specific type.. (an Int or otherwise) .. in the scope of that function all we have is the original guarantee that getFoo can be of any type which is an instance of Show. The actual type of the wrapped value remains hidden and unknowable so there are no violations of any type guarantees and happiness ensues.

PS:我忘了提到 Int 位当然是一个例子..在您的情况下，内部的 getFoo 字段的类型foo 值的类型为 a ，但这是GHC类型推断所引用的特定(非存在)类型(而不是GHC中的存在性 a ).类型声明)..我只是想出一个具有特定 Int 类型的示例，因此它更容易理解.

PS: I forgot to mention that the Int bit was of course an example.. in your case, the type of the getFoo field inside of the foo value is of type a but this is a specific (non existential) type to which GHC's type inference is referring to (and not the existential a in the type declaration).. I just came up with an example with a specific Int type so that it would be easier and more intuitive to understand.

这篇关于存在性构造函数的模式绑定的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！