haskell - 为什么在 Liquid Haskell 中 Nat 类型等于 Int？

Question

为什么能通过 Liquid Haskell 验证？

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

这是否意味着从 LH 的角度来看，Nat 与 Int 相同？

Answer 1

假设你对我说，“嘿，我想要一个苹果!”。我回答:“对不起，我只有红苹果。”。你会很有趣地看着我，是吗？一个红苹果是一个苹果!

如果一个函数要求一个 Int 作为参数，给它一个你知道不是负数的 Int 是没有问题的。