部分功能

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：

尽管[部分功能] typechecks和编译，也不会降低（也就是说，该函数的评估将导致其改变）：

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