2

作为一个接触过 Lisp 的程序员,在编写 Haskell 时,我注意到了一些奇怪的东西,我没能理解。

这编译得很好:

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

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

问题是:

我是否错过了某些东西或由于 haskell 不是同音异形这一事实而导致了这种行为?

我的理由是,鉴于:

  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
4

2 回答 2

12

我是否错过了某些东西或由于 haskell 不是同音异形这一事实而导致了这种行为?

不。同音性是一条红鲱鱼:每种语言都与它的源文本和它的 AST 1同音,事实上,Haskell内部实现为各种中间语言之间的一系列脱糖传递。

真正的问题是,let...in只是case...of有根本不同的语义,这是有意的。模式匹配case...of是严格的,从某种意义上说,它强制审查员评估以选择要评估的 RHS,但let...in表单中的模式绑定是惰性的。从这个意义上说,let p = e1 in e2实际上最类似于case e1 of ~p -> e2(注意使用 ! 的惰性模式匹配~),它会产生类似但不同的错误消息:

ghci> case undefined of { ~Foo{getFoo} -> show getFoo }

<interactive>:5:22: error:
    • An existential or GADT data constructor cannot be used
        inside a lazy (~) pattern
    • In the pattern: Foo {getFoo}
      In the pattern: ~Foo {getFoo}
      In a case alternative: ~Foo {getFoo} -> show getFoo

这在对Odd ghc 错误消息“我的大脑刚刚爆炸”的回答中有更详细的解释?.


1如果这不能满足您的要求,请注意 Haskell大多数 Lispers 使用该词的意义上是谐音的,因为它支持引号quote形式的 Lisp 运算符的模拟[| ... |],这是模板 Haskell 的一部分。

于 2018-11-16T22:58:10.283 回答
0

我对此进行了一些思考,尽管起初这种行为似乎很奇怪,但经过一番思考后,我想也许可以证明这一点是合理的:

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

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。AnInt是 的一个实例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是任何特定类型..(an或其他).. 在该函数的范围内,我们所拥有的只是可以是任何类型Int的原始保证getFoo这是 的一个实例Show。包装值的实际类型仍然是隐藏的和不可知的,因此不会违反任何类型保证并且幸福随之而来。

PS:我忘了提到该Int位当然是一个示例..在您的情况下,值getFoo内部字段foo的类型是 typea但这是 GHC 的类型推断所指的特定(非存在)类型(而不是a类型声明中的存在)..我只是想出了一个具有特定Int类型的示例,以便更容易和更直观地理解。

于 2018-11-17T23:06:54.650 回答