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

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

0 голосов
/ 17 ноября 2018

Когда я писал на 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 - это два особых случая.

Трудно понять эти особые случаи, поскольку их нельзя ни реализовать, ни найти непосредственно в самом языке.

В результате этого не гарантируется согласованное поведение по всему языку. Особенно вместе с дополнительными расширениями компилятора, как в примере.

пс: ошибка компилятора: 

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

Ответы [ 2 ]

0 голосов
/ 18 ноября 2018

Я немного подумал об этом, и поначалу поведение кажется странным, после некоторых размышлений, я думаю, можно оправдать это, возможно, так:

Скажем, я беру ваш второй (неудачный) пример и после некоторого массажа изамены значений Я уменьшаю это до: 

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, чтобы его было легче и интуитивно понять.

0 голосов
/ 17 ноября 2018

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

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

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

...