die folgenden Teilfunktion (keine Ausgabe für einen Nothing Eingang) Gegeben:Verständnis Ausgabe der Teilfunktion
f : Maybe Int -> Maybe Int
f (Just 42) = Just 42
die REPL zeigt folgendes:
*Lecture> f $ Just 42
Just 42 : Maybe Int
*Lecture> f Nothing
f Nothing : Maybe Int
Was ist die Bedeutung von f Nothing ‚s Ausgabe?
Idris reduziert Ausdrücke, die Aufrufe von Teilfunktionen ohne übereinstimmende Muster betreffen, nicht. Mit anderen Worten, dies ist nur die Art und Weise, wie die REPL einen undefinierten oder "unteren" Wert darstellt. Vermutlich, wenn Sie diesen Aufruf in einer ausführbaren Datei machen, erhalten Sie stattdessen einen Laufzeitfehler.
Von the tutorial:
Und obwohl [eine Teilfunktion] typechecks und compiliert, wird es nicht verringern (das heißt, Auswertung der Funktion wird es dazu führen, ändern):
-- 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