Лень/строгость между данными и новым типом

Я пытаюсь понять, почему эти два фрагмента дают разные результаты при так называемом "анализе строгости человека".

В первом примере используется data (при условии правильного аппликативного экземпляра):

data Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }

> getParser (pure (,) <*> literal ';' <*> undefined ) "abc"
*** Exception: Prelude.undefined

Второй использует newtype. Нет другой разницы:

newtype Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }

> getParser (pure (,) <*> literal ';' <*> undefined ) "abc"
Nothing

literal x - это синтаксический анализатор, который успешно использует один токен ввода, если его аргумент соответствует первому токену. Поэтому в этом примере он терпит неудачу, поскольку ; не соответствует a. Тем не менее, пример data все еще видит, что следующий синтаксический анализатор undefined, в то время как пример newtype не работает.

Я прочитал этот, этот и это, но не понимайте их достаточно хорошо, чтобы понять, почему первый пример - undefined. Мне кажется, что в этом примере newtype более ленив, чем data, что противоположно сказанному. (По крайней мере еще один человек тоже был смущен).

Почему переход от data в newtype изменяет определенность этого примера?

Вот еще одна вещь, которую я обнаружил: с этим аппликативным экземпляром анализатор data выше выводит undefined:

instance Applicative (Parser s) where
  Parser f <*> Parser x = Parser h
    where
      h xs = 
        f xs >>= \(ys, f') -> 
        x ys >>= \(zs, x') ->
        Just (zs, f' x')

  pure a = Parser (\xs -> Just (xs, a))

тогда как с этим экземпляром анализатор data выше не выводит undefined (при условии правильного экземпляра Monad для Parser s):

instance Applicative (Parser s) where
  f <*> x =
      f >>= \f' ->
      x >>= \x' ->
      pure (f' x')

  pure = pure a = Parser (\xs -> Just (xs, a))

Полный фрагмент кода:

import Control.Applicative
import Control.Monad (liftM)

data Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }


instance Functor (Parser s) where
  fmap = liftM

instance Applicative (Parser s) where
  Parser f <*> Parser x = Parser h
    where
      h xs = f xs >>= \(ys, f') -> 
        x ys >>= \(zs, x') ->
        Just (zs, f' x')

  pure = return


instance Monad (Parser s) where
  Parser m >>= f = Parser h
    where
      h xs =
          m xs >>= \(ys,y) ->
          getParser (f y) ys

  return a = Parser (\xs -> Just (xs, a))


literal :: Eq t => t -> Parser t t
literal x = Parser f
  where
    f (y:ys)
      | x == y = Just (ys, x)
      | otherwise = Nothing
    f [] = Nothing

Ответы

Ответ 1

Как вы, вероятно, знаете, основное различие между data и newtype заключается в том, что при data это конструкторы data ленивы, а newtype является строгим, т.е. заданы следующие типы

data    D a = D a 
newtype N a = N a

затем D ⊥ `seq` x = x, но N ⊥ `seq` x = ⊥.

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

constD x (D y) = x
constN x (N y) = x

затем constD x ⊥ = ⊥, но constN x ⊥ = x.

Это то, что происходит в вашем примере.

Parser f <*> Parser x = Parser h where ...

С data совпадение шаблона в определении <*> будет расходиться сразу, если аргументов ⊥, но с newtype конструкторы игнорируются, и это как если бы вы написали

f <*> x = h where

который будет отклоняться только для x = ⊥, если требуется x.

Ответ 2

Разница между data и newtype заключается в том, что data "снят", а newtype - нет. Это означает, что data имеет дополнительный ⊥ - в этом случае это означает, что undefined/= Parser undefined. Когда ваш шаблон кода Applicative совпадает с Parser x, он заставляет значение ⊥, если конструктор.

Когда вы сопоставляете шаблон с конструктором data, он оценивается и разбирается, чтобы убедиться, что он не ⊥. Например:

λ> data Foo = Foo Int deriving Show
λ> case undefined of Foo _ -> True
*** Exception: Prelude.undefined

Таким образом, сопоставление шаблонов в конструкторе data является строгим и будет принудительным. A newtype, с другой стороны, представляется точно так же, как и тип его конструктора. Поэтому сопоставление в конструкторе newtype ничего не делает:

λ> newtype Foo = Foo Int deriving Show
λ> case undefined of Foo _ -> True
True

Возможно, есть два способа изменить вашу программу data так, чтобы она не разбилась. Можно было бы использовать неопровержимое соответствие шаблонов в вашем экземпляре Applicative, который всегда будет "успешным" (но использование согласованных значений в любом месте позже может завершиться неудачей). Каждое совпадение newtype ведет себя как неопровержимый шаблон (поскольку нет конструктора для соответствия, строгости).

λ> data Foo = Foo Int deriving Show
λ> case undefined of ~(Foo _) -> True
True

Другим будет использование Parser undefined вместо undefined:

λ> case Foo undefined of Foo _ -> True
True

Это совпадение будет успешным, потому что существует допустимое значение Foo, которое соответствует. Это происходит с undefined, но это не имеет значения, так как мы его не используем - мы смотрим только на самый верхний конструктор.

В дополнение ко всем ссылкам, которые вы указали, вы можете найти эту статью.