Почему Nat тип равен Int в Liquid Haskell?

Question

Почему это проходит проверку Liquid Haskell?

{-@ sub :: Nat -> Nat -> Int @-}                                                                                                         
sub :: Int -> Int -> Int 
sub i j = i - j 

Означает ли это, что Nat совпадает с Int с точки зрения LH?

Answer 1

Предположим, вы говорите мне: «Эй, я бы хотел яблоко!».Я отвечаю: «Извините, у меня есть только красные яблоки».Ты будешь смотреть на меня довольно забавно, а?Красное яблоко - это яблоко!

Если функция запрашивает Int в качестве аргумента, не проблема передать ему Int, который, как вы знаете, не является отрицательным.