Haskell do нотация не может проверить тип - PullRequest
Новая
       28

Haskell do нотация не может проверить тип

3 голосов
/ 07 марта 2020

Я пытаюсь понять правила для do нотации.

Вот код проверки типов: 

fff :: Maybe Int
fff = do
    _ <- pure $ Just 100
    (+10)
    <$> Just 50

В основном это fff = (+10) <$> Just 50. Я бы предположил, что вышеприведенное могло бы не проверить тип - потому что наверняка каждая строка должна быть в контексте Maybe, который (+10) не является.

Почему выше typecheck? Вот более простой пример вышеприведенного: 

fff :: Int -> Maybe Int
fff i = do
    (+10)
    <$> Just i

Почему вышеуказанный допустимый синтаксис? Разве это не 'desugar' для: 

fff i = ((+10) >>= (\i -> fmap (Just i))) i

, что действительно дает ошибку проверки типов в ghci.

Вот пример, который не выполняет проверку типов отступ, аналогичный указанному выше: 

x :: Maybe Int
x = do
  _ <- Just 1
  undefined
  <$> Just 5

(Спасибо @cvlad из чата FP без ответа за приведенный выше пример)

Ответы [ 2 ]

4 голосов
/ 07 марта 2020

Это странное взаимодействие.

Я начал упрощать тестовый пример до этого, который работает нормально. 

> x = do succ ; <$> Just 1
> x
Just 2

Для сравнения, это НЕ анализирует: 

> y = do { succ ; <$> Just 1 }      
error: parse error

Однако, это анализирует: 

> z = do { succ } <$> Just 1      
> z
Just 2

Итак, вот что я думаю, что происходит. Так как токен <$> никогда не может начать выражение, синтаксический анализ не выполняется. Правило синтаксического анализатора do - это, по сути, максимальное правило munch: при сбое добавьте неявный } и попробуйте снова.

Из-за этого x выше анализируется как z. Так как succ является значением monadi c (строка (+10) в вопросе OP), оно может появляться внутри do. Это делает проверку типа успешной.

Цитирование отчета Haskell 2.7

Закрывающая скобка также вставляется всякий раз, когда категория syntacti c, содержащая макет список заканчивается; то есть, если в точке, где закрывающая скобка была бы допустимой, встречается недопустимая лексема, вставляется закрывающая скобка.

4 голосов
/ 07 марта 2020 
fff :: Int -> Maybe Int
fff i = do
    (+10)
    <$> Just i

Почему указанный выше допустимый синтаксис?

Поскольку он анализируется как 

fff i = do {        -- do { A } is just
    (+10) }         --      A
    <$> Just i

, что эквивалентно 

fff i =
    (+10) 
    <$> Just i

, поскольку <$> Just i само по себе является недопустимым выражением (поэтому fff i = ((+10) >>= (\i -> fmap (Just i))) i является неправильным переводом), и это ограничивает экстент блока do согласно правилу, указанному в ответе @ chi.

Действительно, его тип выводится как 

fff :: Num b => b -> Maybe b

Ваш второй пример работает, если добавить пробел перед <$> в последней строке. Без пробела он снова анализируется как 

inputTest :: FormInput -> IO (Either [String] (Int, Int))
inputTest fi = do {
    allErrors' <- undefined :: IO [String]
    undefined }
    <$> ((liftM2 ) (,) <$> undefined <*> undefined) fi

, поскольку само по себе <$> ... является недопустимым выражением. Действительно, когда я добавляю явные разделители, 

inputTest2 :: String -> IO (Either [String] (Int, Int))
inputTest2 fi = do {
    allErrors2 <- undefined :: IO [String] ;
    undefined  }
    <$> ((liftM2 ) (,) <$> undefined <*> undefined) fi

Я получаю точно такое же сообщение об ошибке на TIO (пришлось использовать String вместо вашего типа).

Начиная с первого undefined :: IO [String], весь блок do имеет некоторое IO t введите, и мы не можем fmap , что поверх чего-либо.

Всегда добавляйте все явные разделители (в дополнение к практике хорошего стиля отступов), чтобы избежать этой странной хрупкости синтаксиса.

Ваш новый пример: 

x :: Maybe Int
x = do          -- {     this is
  _ <- Just 1   -- ;       how it is
  undefined     -- }         parsed
  <$> Just 5

Код изменился, но ответ тот же. do блок до <$> равен Maybe t (из-за Just 1), и мы не можем fmap , что .

Опять же, сделайте отступ в последней строке еще немного, и он скомпилируется, потому что undefined <$> Just 5 теперь будет анализироваться как одно выражение.

...