Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Type safe division
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
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment