Привязки шаблонов для экзистенциальных конструкторов

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

Для меня не очевидно, почему второй фрагмент не работает.

Вопрос будет:

Я что-то упускаю или это поведение связано с тем, что 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 }

edit: другая версия компилятора выдает эту ошибку для той же проблемы

* 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' вышла бы за пределы своей области

если сопоставление с образцом будет разрешено, какой будет тип х? ну.. типа бы конечно 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 напечатайте так, чтобы было проще и понятнее понять.

Answer 2

Я что-то упускаю или это поведение связано с тем, что haskell не гомоичен?

Нет. Homoiconicity - это красная сельдь: каждый язык гомоичен со своим исходным текстом и его AST¹, и, действительно, 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

Это объясняется более подробно в ответе на странное сообщение об ошибке GHC, "Мой мозг только что взорвался"?,

---

^{1 Если вас это не устраивает, обратите внимание, что Хаскелл гомоичен в том смысле, что большинство Лисперсов используют это слово, так как он поддерживает аналог Лиспа.}quote^{оператор в виде} [| ... |] ^{кавычки, которые являются частью шаблона Haskell.}