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

假设你对我说：“嘿，我想要一个苹果！”。我回答：“对不起，我只有红苹果。”。你会看着我很有趣，是吧？红苹果就是苹果！

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