我可以在函数中间打印一些内容吗

Question

https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.htmlsays isSingleton在参数为True时返回Nat，在参数为False时返回列表。

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

现在，我可以以某种方式插入putStrLn"吗；你好世界"；到isSingleton True = Nat，以便它首先打印我的字符串，然后返回Nat？

Answer 1

Ish。。。

你可以在那条线上打印东西，放弃安全，

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

它打印

hi
foo

然而，似乎不能在函数签名中使用isSingleton，因为Idris在类型检查时似乎不会执行IO机制。我得到

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
^

但实际上，我很不清楚你为什么要这么做。如果你想检查你正在使用哪个分支，你可以用the进行注释。如果您想打印值而不是类型，Debug模块中的功能与上面的第一个示例相同。