为什么在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

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

如果一个函数要求一个Intas作为参数，则将它传递给Int您知道不是负数的an没问题。