Search code examples
haskellliquid-haskell

Why is Nat type equal to Int in Liquid Haskell?

Why does this pass Liquid Haskell verification?

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

Does it mean that Nat is the same as Int from LH's point of view?

Solution

  • Suppose you say to me, "Hey, I'd like an apple!". I reply: "Sorry, I only have red apples.". You're going to look at me pretty funny, huh? A red apple is an apple!

    If a function asks for an Int as an argument, it's no problem to hand it an Int that you know is not negative.