Idris：bounded Double 的算法

Question

我是 Idris 的新手。我需要创建一个描述有界数字的数据。所以我用这样的构造函数制作了这样的数据：

data BoundedDouble : (a, b : Double) -> Type where
  MkBoundedDouble : (x : Double) -> 
                    {auto p : a <= x && x <= b = True} -> 
                    BoundedDouble a b

似乎在a和b之间创建了一个Double。这是一个简单的使用示例：

test : BoundedDouble 0.0 1.0
test = MkBoundedDouble 0.0

有效。但是现在我想为 BoundedDouble 实现 Num 接口。我试过这个：

Num (BoundedDouble a b) where
  (MkBoundedDouble x) + (MkBoundedDouble y) = 
    MkBoundedDouble (ifThenElse (x + y > b) 
                      (x + y - (b - a))
                      (ifThenElse (x + y < a)
                        (x + y + (b - a))
                        (x + y)))

但它不起作用，我猜为什么，但我无法解释。我应该如何实现加法？

我不知道我应该做什么或阅读才能理解它。

Answer 1

这里有两个问题。 Idris 甚至无法证明 a <= b = True -> b <= c = True -> a <= c = True（顺便说一句，它甚至不能一直成立 - 所以这不是 Idris 的错。）[=17= 没有证据] 除了检查它，你用 ifThenElse.

尝试了什么

在处理这种盲目运行时间证明时（因此只需 … = True），Data.So 非常有帮助。 ifThenElse (a <= x) … … 给出布尔检查分支，但分支中的代码不知道检查结果。使用 choose (a <= x) 可以得到分支的结果，使用 Left prf 和 prf : So (a <= x) 或 Right prf 和 prf : So (not (a <= x)).

我想如果将两个有界双打相加的结果会大于上限，那么结果应该是这个上限。让我们进行第一次尝试：

import Data.So

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => ?holeMin
             (_, Right _) => ?holeMax

这已经进行了类型检查，但其中有漏洞。我们想将 ?holeMin 设置为 MkBoundedDouble a，将 ?holeMax 设置为 MkBoundedDouble b。但是，MkBoundedDouble 现在需要两个证明：high 和 low。在 ?holeMax 的情况下，它们将与 x = b So (a <= b) 和 So (b <= b) 一起使用。同样，Idris 不知道每个 b : Double 对应的 b <= b。所以我们需要重新选择才能得到这些证明：

             (_, Right _) => case (choose (a <= b), choose (b <= b)) of
                  (Left _, Left _) => MkBoundedDouble b
                  _ => ?what

因为 Idris 看不到 b <= b，该函数将是偏函数。我们可以作弊并在 ?what 中使用例如 MkBoundedDouble u，因此该函数将进行类型检查并希望这确实永远不会发生。

也有可能强行让类型检查器相信b <= b总是正确的：

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto rightSize : So (a <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

DoubleEqIsSym : (x : Double) -> So (x <= x) 
DoubleEqIsSym x = believe_me (Oh)

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => MkBoundedDouble a {high=DoubleEqIsSym a}
             (_, Right _) => MkBoundedDouble b {low=DoubleEqIsSym b}

或者我们可以更安全，将上限和下限的证明放在数据构造函数中，这样我们就可以在 ?holeMin 和 ?holeMax 中使用它们。这将是：

import Data.So

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto rightSize : So (a <= b)}
                      -> {auto leftId : So (a <= a)}
                      -> {auto rightId : So (b <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => MkBoundedDouble a
             (_, Right _) => MkBoundedDouble b

您会看到，即使构造函数包含了证明，它们也不会使实现复杂化。它们应该在实际的运行时间代码中被删除。

但是，作为练习，您可以尝试为

实施 Num

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double)
                      -> {auto rightSize : So (a <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)} 
                      -> BoundedDouble a b
    Min : {auto rightSize : So (a <= b)} -> BoundedDouble a b
    Max : {auto rightSize : So (a <= b)} -> BoundedDouble a b

很遗憾，Idris 的资源还不多。除了教程之外，还有 a book 正在开发中，我会推荐。它提供了比使用原始类型更容易上手的练习。 :-)

Idris：bounded Double 的算法

Idris: arithmetics for bounded Double

dependent-type

idris