dependent-type - Idris:有界 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 接口(interface)。我试过这个:

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

这里有两个问题。 Double arithmetic is defined with primitive functions. idris 甚至无法证明 a <= b = True -> b <= c = True -> a <= c = True (顺便说一句，这甚至不能一直成立 - 所以这不是 idris 的错。)没有证据证明 a <= b = True其他然后只是检查它，您尝试过 ifThenElse .

当使用这种盲运行时证明时(所以只是 … = True )， Data.So 很有帮助。 ifThenElse (a <= x) … …给定 bool 检查分支，但分支中的代码不知道检查结果。与choose (a <= x)您将得到分支的结果 Left prf和prf : So (a <= x)或Right prf和prf : So (not (a <= x)) .

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

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 <= b对于每个 b : Double 。因此我们需要再次选择才能获得这些证明:

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

因为 idris 看不到 b <= b ，该函数将是部分的。我们可以作弊并使用例如 MkBoundedDouble u在?what ，因此该函数将进行类型检查并希望这种情况永远不会发生。

还可以强制类型检查器相信 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正在开发中，我会推荐。它提供了比使用原始类型更平易近人的练习。 :-)