function - 了解偏函数的输出

Question

给定以下部分函数(Nothing 输入没有输出):

f : Maybe Int -> Maybe Int
f (Just 42) = Just 42

REPL 显示以下内容:

*Lecture> f $ Just 42
Just 42 : Maybe Int

*Lecture> f Nothing
f Nothing : Maybe Int

f Nothing 的输出含义是什么？

Answer 1

Idris 不会减少涉及调用不匹配模式的部分函数的表达式。换句话说，这只是 REPL 呈现未定义或“底部”值的方式。据推测，如果您在可执行文件中进行该调用，那么您将收到运行时错误。

来自the tutorial :

And although [a partial function] typechecks and compiles, it will not reduce (that is, evaluation of the function will cause it to change):

-- Unsafe head example!
unsafeHead : List a -> a
unsafeHead (x::xs) = x

unsafe> the Integer $ unsafeHead [1, 2, 3]
1 : Integer
unsafe> the Integer $ unsafeHead []
unsafeHead [] : Integer