Compte tenu de la fonction partielle suivante (pas de sortie pour une entrée Nothing):sortie compréhension de la fonction partielle
f : Maybe Int -> Maybe Int
f (Just 42) = Just 42
REPL affiche les éléments suivants:
*Lecture> f $ Just 42
Just 42 : Maybe Int
*Lecture> f Nothing
f Nothing : Maybe Int
Quel est le sens de f Nothing « s sortie?
Idris ne réduira pas les expressions impliquant des appels à des fonctions partielles sans motifs correspondants. En d'autres termes, il s'agit simplement de la façon dont REPL présente une valeur non définie ou «en bas». Vraisemblablement si vous faites cet appel dans un exécutable alors vous obtiendrez une erreur d'exécution à la place.
De the tutorial:
Et bien que [fonction partielle] typable et compiles, il ne réduira pas (à savoir l'évaluation de la fonction lui fera changer):
-- 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