Type safe division

divide.idr

module Main
  
{- Divide x by y, as long as there is a proof that y is non-zero. The
   'auto' keyword on the 'p' argument means that when safe_div is called,
   Idris will search for a proof. Either y will be statically known, in
   which case this is easy, otherwise there must be a proof in the context.

   'so : Bool -> Type' is a predicate on booleans which only holds if the
   boolean is true. Essentially, we are making it a requirement in the type
   that a necessary dynamic type is done before we call the function -}
  
safe_div : (x : Int) -> (y : Int) -> {auto p : so (y /= 0)} -> Int
safe_div x y = div x y
  
{- We can use the following function from the library to do a dynamic check 
   on a boolean which returns either a proof that the input is true, or not 
   true:

   choose : (b : Bool) -> Either (so b) (so (not b))
-}

main : IO ()
main = do -- Read from console
          putStr "Dividend: "
          x_in <- getLine
          putStr "Divisor: "
          y_in <- getLine
  
          -- Cast does a type safe cast from the Strings that were input
          -- to an equivalent integer (0 if it doesn't parse (yes, I know))
          let x : Int = cast x_in
          let y : Int = cast y_in
  
          -- Now do the dynamic check with choose
          case choose (y/=0) of
               Left pn => -- Safe to call 'safe_div' because proof search will
                          -- find 'pn', the proof that y is non-zero
                          print (x `safe_div` y)
               Right pz => -- pz is a proof that y is zero, so we can't call i
                           print "Attempt to divide by zero!"
{-
What if we didn't call 'choose' first? We get:
  
When elaborating argument p to function Main.safe_div:
        Can't solve goal 
           so (y /= fromInteger 0)
-}