我希望一些 Haskell 专家可以帮助澄清一些事情。
是否可以以Nat
通常的方式定义(通过 Haskell 中的@dorcard Singleton 类型)
data S n = Succ n
data Z = Zero
class Nat n
instance Nat Z
instance Nat n => Nat (S n)
(或其一些变体),然后定义一个LessThan
关系,使得 foralln
和m
LessThan Z (S Z)
LessThan n m => LessThan n (S m)
LessThan n m => LessThan (S n) (S m)
然后编写一个类型如下的函数:
foo :: exists n. (LessThan n m) => Nat m -> Nat n
foo (S n) = n
foo Z = foo Z
我明确地想在输出类型中使用“LessThan” foo
,我意识到人们当然可以写出类似的东西
foo :: Nat (S n) -> Nat n
但这不是我所追求的。
谢谢!
兰吉特。