The purpose of this post is to demonstrate the interaction between dependent types and IO in Idris.
In the examples, for a given IO string, we will pass it through a total and a non-total function to demonstrate how Idris handles both cases.
We will define a dependent type called Vect which will allow us to work with lists, but additionally it will contain the length of the list at type level as follows:
data Vect : Nat -> Type -> Type where VNil : Vect Z a VCons : a -> Vect k a -> Vect (S k) a
So, in the following demonstration we will see how both the safe and unsafe code pass compile-time, but the latter may fail on run-time.
Safe:
total
wat_total : List Char -> Vect 2 Char
wat_total (x :: y :: []) = VCons x (VCons y VNil)
wat_total _ = VCons 'a' (VCons 'b' VNil)
unwat : Vect 2 Char -> List Char
unwat (VCons a (VCons b VNil)) = a :: b :: []
wrapunwrap_safe : String -> String
wrapunwrap_safe name = pack (unwat (wat_total (unpack name)))
greet_safe : IO ()
greet_safe = do
putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ (wrapunwrap_safe name))
main : IO ()
main = do
putStrLn "Following safe greet, enter any number of chars"
greet_safe
If we specify total to the wat_total function, it must produce a value for all possible inputs, and this is okay and safe. All the rest of the checks are done on compile time and the compiler will force you to be sure that any callers to wat_total have the types flow correctly.
Unsafe:
wat : List Char -> Vect 2 Char
wat (x :: y :: []) = VCons x (VCons y VNil)
unwat : Vect 2 Char -> List Char
unwat (VCons a (VCons b VNil)) = a :: b :: []
wrapunwrap : String -> String
wrapunwrap name = pack (unwat (wat (unpack name)))
greet : IO ()
greet = do
putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ (wrapunwrap name))
main : IO ()
main = do
putStrLn "Following unsafe greet, you can only enter chars of size 2"
greet
The tricky case is when we’re dealing with non-total functions. Let’s check a few return values:
*wat> wat [] wat [] : Vect 2 Char *wat> wat ['a'] wat ['a'] : Vect 2 Char *wat> wat ['a','b'] VCons 'a' (VCons 'b' VNil) : Vect 2 Char *wat> wat ['a','b','c'] wat ['a', 'b', 'c'] : Vect 2 Char
We only see that we get a correct value for wat ['a', 'b']. The rest of the examples we can see that the value is “not computed”, kind of.
But, how does Idris handle this at run-time?
*wat> :exec Following unsafe greet, you can only enter chars of size 2 What is your name? Hello *wat> :exec Following unsafe greet, you can only enter chars of size 2 What is your name? Hi Hello Hi *wat>
We see that Idris stopped the execution of the process. What happens if we use the `node` target for compiling?
boro@bor0:~/idris-test$ idris --codegen node wat.idr -o wat.js
boro@bor0:~/idris-test$ node wat.js
Following unsafe greet, you can only enter chars of size 2
What is your name? Hello
/Users/boro/idris-test/wat.js:177
$cg$7 = new $HC_2_1$Prelude__List___58__58_($cg$2.$1, new $HC_2_1$Prelude__List___58__58_($cg$9.$1, $HC_0_0$Prelude__List__Nil));
^
TypeError: Cannot read property '$1' of undefined
at Main__greet (/Users/boro/idris-test/wat.js:177:101)
at Main__main (/Users/boro/idris-test/wat.js:187:12)
at $_0_runMain (/Users/boro/idris-test/wat.js:231:25)
at Object.<anonymous> (/Users/boro/idris-test/wat.js:235:1)
at Object.<anonymous> (/Users/boro/idris-test/wat.js:236:3)
at Module._compile (module.js:660:30)
at Object.Module._extensions..js (module.js:671:10)
at Module.load (module.js:573:32)
at tryModuleLoad (module.js:513:12)
at Function.Module._load (module.js:505:3)
boro@bor0:~/idris-test$ node wat.js
Following unsafe greet, you can only enter chars of size 2
What is your name? Hi
Hello Hi
Whoops. What about C?
boro@bor0:~/Desktop/idris-test$ idris --codegen C wat.idr -o wat boro@bor0:~/Desktop/idris-test$ ./wat Following unsafe greet, you can only enter chars of size 2 What is your name? Hello Segmentation fault: 11 boro@bor0:~/Desktop/idris-test$ ./wat Following unsafe greet, you can only enter chars of size 2 What is your name? Hi Hello Hi
It segfaults on the bad case.
As a conclusion, make sure your non-total functions have checks on the run-time as well.
Alternatively, if we want to take full advantage of the type safety that dependent types may offer, we need to make sure that all of our functions are total 🙂
bor0's reflective blog 