部分功能

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