这些定义实施了哪些操作？(==,<,>等)

Question

data Nat = Z | S Nat

例如,我们可以使用此数据类型来表示前几个数字:

Z代表0,S Z代表1,S (S Z)代表2,等等.

1. 平等(即x == y),
2. 小于(即x < y),
3. 小于或等于(即x ? y),
4. 大于(即x > y),
5. 大于或等于(即x ? y).

1.

(?) :: Nat -> Nat -> Bool
Z ? Z = True
Z ? (S n) = True
(S n) ? (S m) = n <?> m
x ? z = False

2.

? :: Nat -> Nat -> Bool
(S n) ? Z = True
(S n) ? (S m) = n <?> m
x ? z = False

我不明白它与(S n)的含义以及我们应如何区分最后的X和Z.

Answer 1

你的构造者在这里

-- zero
Z

和

-- nonzero n
S n

您的第一个示例着眼于:

(?) :: Nat -> Nat -> Bool
Z ? Z = True
Z ? (S n) = True
(S n) ? (S m) = n <?> m
x ? z = False

所以我们去试试吧.我们可以从(==)这个断言开始,看看它是否都失败了.

Z == Z = True      -- makes sense
Z == (S n) = True  -- FAIL

这不应该是真的,因为你的零不会等于任何非零值.实际上,它应该小于任何非零值!让我们再试(<)一次

Z < Z = True       -- Whoops...

坚持,零不低于自己,但它们小于或等于自己.我们来试试吧(<=).

Z <= Z = True            -- Uh huh
Z <= (S n) = True        -- Yup
(S n) <= (S m) = n <= m  -- S n <= S m when n <= m, makes sense!
x <= z = False           -- Any other construction should be False, e.g.
                         --   (S n) <= Z

我会继续把第二个问题留给你,因为你希望能够更好地理解被问到的内容!