One example code on https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html says isSingleton returns Nat when the parameter is True, and returns a list when the parameter is False.
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
Now, can I somehow insert putStrLn "hello world" into isSingleton True = Nat
so that it first prints my string, then returns Nat?
Ish ...
You can print things on that line with, forgoing safety,
module Main
isSingleton : Bool -> Type
isSingleton True = unsafePerformIO $ do putStrLn "hi"
pure Nat
isSingleton False = List Nat
foo : Type -> String
foo _ = "foo"
main : IO ()
main = putStrLn $ foo $ isSingleton True
which prints
hi
foo
However, it appears you can't then use isSingleton
in function signatures because Idris doesn't appear to execute the IO machinery when type checking. I get
Error: While processing right hand side of mkSingle. Can't find an implementation for Num (unsafePerformIO (putStrLn "hi" >> Delay (pure Nat))).
Main:11:17--11:18
07 | foo : Type -> String
08 | foo _ = "foo"
09 |
10 | mkSingle : (x : Bool) -> isSingleton x
11 | mkSingle True = 0
^
But really, I'm very unclear why you'd want to do this at all. If you want to check which branch you're using you could just annotate with the
. If you wanted to print values not types, there is functionality in the Debug
module which does the same as the first example above.