People say a dependent type language is slow in type checking so I think it is slow in running type functions.
Use the classic example on https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
and run
mkSingle True
How many times does isSingleton run?
In a traditional language, I can print to console. But Idris doesn't appear to execute the IO machinery when type checking. I can increase a global counter or set a breakpoint at the beginning of isSingleton and count how many times the breakpoint is hit.
Can I do something in idris 2 to easily convince people, "hey, during the time isSingleton has been called x times"?
Update
f : (x : Bool) -> isSingleton x -> Nat
f True n = 0
f False ls = 1
I set the multiplicity of isSingleton to 0, add the above code to my file and run
Main> f True []
Error: When unifying:
List ?a
and:
isSingleton True
Mismatch between: List ?a and Nat.
(Interactive):1:8--1:10
1 | f True []
^^
idris knows the second argument should be Nat, which is provided by isSingleton, right? But isSingleton is erased at runtime, how is isSingleton called?
Erase isSingleton
0 isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
then you know it doesn't exist at runtime and is never called. I imagine it's also never called (in this example) if you don't erase it, but by erasing it you can be sure.