Верны ли эти примеры или в учебнике есть ошибка?
Я читаю этот учебник и не уверен, что правильно понимаю текст (или что он вообще правильный). Вот пример:
The following predicates are valid because they encode modus ponens: if you know that a implies b and you know that a is true, then it must be the case that b is also true:
{-@ 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. И LH передает это как:
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
Я подозреваю, что в примере они сделали (==>) правоассоциативным, в то время как в ваших тестах вы оставили его по умолчанию, что является левоассоциативным. Сравнивать:
> 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
Отчет содержит дополнительные сведения.