haskell - 用 Haskell 编码 "Less Than"

Question

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

是否可以以通常的方式定义Nat(通过@dorchard Singleton types in Haskell)

data S n = Succ n 
data Z   = Zero

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

(或其某些变体)，然后定义一个 LessThan 关系 这样对于所有 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

我明确希望在 foo 的输出类型中使用“LessThan”， 我意识到人们肯定可以写出类似的东西

foo :: Nat (S n) -> Nat n

但这不是我所追求的。

谢谢!

兰 git 。

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 nm 类型的完全标准化值是 n 小于 m 的证明。

存在主义的解决方法

现在你问的是:

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，n 都小于 S 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