Верны ли эти примеры или учебник содержит ошибку? - PullRequest
Новая
       22

Верны ли эти примеры или учебник содержит ошибку?

0 голосов
/ 29 мая 2019

Я читаю этот урок , и я не уверен, что правильно понимаю текст (или что он верен в целом). Вот пример:

Следующие предикаты действительны, потому что они кодируют modus ponens: если вы знаете, что a подразумевает b, и вы знаете, что a истинно, то оно должно быть в том случае, если b также верно: 

{-@ ex6 :: Bool -> Bool -> TRUE @-}
ex6 a b = (a && (a ==> b)) ==> b

{-@ ex7 :: Bool -> Bool -> TRUE @-}
ex7 a b = a ==> (a ==> b) ==> b

и ex6 в порядке, но ex7 нет, он не работает для a = false и b = false. И ЛХ сообщают это как: 

Error: Liquid Type Mismatch

 88 | ex7 a b = a ==> (a ==> b) ==> b
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Bool | v <=> ((a => (a => b)) => b)}

   not a subtype of Required type
     VV : {VV : GHC.Types.Bool | VV}

   In Context
     a : GHC.Types.Bool

     b : GHC.Types.Bool

Также я не понимаю их определения значения: «Вы должны прочитать p ==> q, как будто p истинно, тогда q также должно быть истинным». Он не звучит правильно, потому что он утверждает только один случай: T -> T = T. Что мне здесь не хватает? Может быть, учебник имеет ошибку в "ex7"?

1 Ответ

4 голосов
/ 29 мая 2019

Я подозреваю, что в примере они сделали (==>) правой ассоциативной, в то время как в ваших тестах вы оставили ее по умолчанию, которая остается ассоциативной. Сравните: 

> infixl 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
False
> infixr 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
True

Отчет содержит дополнительную информацию.

...