使用Haskell编码"小于"

Question

我希望一些Haskell专家可以帮助澄清一些事情.

是否有可能以Nat通常的方式定义(通过Haskell中的 @dorchard Singleton类型)

data S n = Succ n 
data Z   = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

(或其一些变体)然后定义一个LessThan关系,使得forall n和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

但那不是我追求的.

谢谢!

兰吉特.

Answer 1

这是实现类似于您所询问的内容的一种方法.

纳特

首先请注意,您将其定义Nat为类,然后将其用作类型.我认为将它作为一种类型是有道理的,所以让我们这样定义它.

data Z
data S n

data Nat n where
  Zero :: Nat Z
  Succ :: Nat n -> Nat (S n)

少于

我们也可以定义LessThan为一种类型.

data LessThan n m where
  LT1 :: LessThan Z (S Z)
  LT2 :: LessThan n m -> LessThan n (S m)
  LT3 :: LessThan n m -> LessThan (S n) (S m)

请注意,我只是将您的三个属性转换为数据构造函数.这种类型的想法是类型的完全标准化值是小于LessThan n m的证明.nm

解决存在问题

现在你问:

foo :: exists n. (LessThan n m) => Nat m -> Nat n

但是Haskell中不存在.相反,我们可以为以下内容定义数据类型foo:

data Foo m where
  Foo :: Nat n -> LessThan n m -> Foo m

请注意,n这里有效地存在量化,因​​为它显示在数据构造函数的参数中,Foo但不显示在其结果中.现在我们可以说出以下类型foo:

foo :: Nat m -> Foo m

一个引理

在我们从问题中实现示例之前,我们必须证明一个小问题LessThan.引理说这n比S n所有人都要少n.我们通过归纳证明了这一点n.

lemma :: Nat n -> LessThan n (S n)
lemma Zero = LT1
lemma (Succ n) = LT3 (lemma n)

执行foo

现在我们可以从问题中编写代码:

foo :: Nat m -> Foo m
foo (Succ n) = Foo n (lemma n)
foo Zero = foo Zero