Idris: arithmetics for bounded Double

Question

I am new to Idris. I need to create a data describing a bounded number. So I've made such data with such a constructor:

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

It seems to create a Double between a and b. And here is a simple example of use:

test : BoundedDouble 0.0 1.0
test = MkBoundedDouble 0.0

It works. But now I want to implement Num interface for BoundedDouble. I tried this:

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)))

But it doesn't work, I guess why, but I can't explain it. How should I implement the addition?

I don't know exactly what should I do or read to understand it.

xash xash · Accepted Answer · 2016-06-01T05:37:40

There are two problems here. Double arithmetic is defined with primitive functions. Idris can't even proof that a <= b = True -> b <= c = True -> a <= c = True (which, by the way, does not even hold all the time - so this is not Idris' fault.) There is no proof for a <= b = True other then just checking it, what you tried with the ifThenElse.

When working with such blind run-time proofs (so just … = True), Data.So is quite helpful. ifThenElse (a <= x) … … branches off given a boolean check, but the code in the branches does not know about result of the check. With choose (a <= x) you get the result for the branches, with Left prf and prf : So (a <= x) or Right prf and prf : So (not (a <= x)).

I suppose if the result of adding two bounded doubles would be bigger then the upper bound, the result should be this upper bound. Lets make a first attempt:

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

This already typechecks, but has holes in it. We want to set ?holeMin to MkBoundedDouble a and ?holeMax to MkBoundedDouble b. However, MkBoundedDouble right now needs two proofs: high and low. In the case of ?holeMax those would be with x = b So (a <= b) and So (b <= b). Again, Idris does not know that b <= b for every b : Double. So we would need to choose again to get these proofs:

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

Because Idris cannot see that b <= b, the function would be partial. We could cheat and use for example MkBoundedDouble u in ?what, so the function will typecheck and hope that this will indeed never occur.

There is also the possibility to convince the type checker with force that b <= b is always true:

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}

Or we could be even safer and put the proofs for the upper and lower bounds in the data constructor, so we can use them in ?holeMin and ?holeMax. This would be:

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

You see that even that the constructor is packed with proofs, they don't complicate the implementation. And they should get erased in the actual run-time code.

However, as an exercise you could try to implement Num for

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

Sadly, there aren't many resources for Idris yet. Besides the tutorial there is a book in development, that I would recommend. It gives more approachable exercises than working with primitive types. :-)

Idris: arithmetics for bounded Double

1 Answers