idrisidris2

Can I print something in the middle of a function?


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?


Solution

  • 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.