'impossibles'

Question

Type-Driven Development with Idris présente:

twoPlusTwoNotFive : 2 + 2 = 5 -> Void 
twoPlusTwoNotFive Refl impossible 

est-ce qui précède une fonction ou de la valeur? Si c'est le premier, pourquoi n'y a-t-il pas d'arguments variables, par ex.

add1 : Int -> Int 
add1 x = x + 1 

En particulier, je suis confus au manque de = dans twoPlusTwoNotFive.

Answer 1

impossible appelle des combinaisons d'arguments qui sont, bien, impossibles. Idris vous absout de la responsabilité de fournir un côté droit quand un cas est impossible.

Dans cet exemple, nous écrivons une fonction de type (2 + 2 = 5) -> Void. Void est un type sans valeur, donc si nous réussissons à implémenter une telle fonction, nous devrions nous attendre à ce que tous ses cas soient impossibles. Maintenant, = a seulement un constructeur (Refl : x = x), et il ne peut pas être utilisé ici, car il exige que les arguments de = soient égaux en définition - ils doivent être le même x. Donc, naturellement, c'est impossible. Personne ne peut appeler cette fonction avec succès lors de l'exécution, et nous sommes sauvés de devoir prouver quelque chose qui n'est pas vrai, ce qui aurait été une grosse question.

Voici un autre exemple: vous ne pouvez pas indexer dans un vecteur vide. En scrutant le Vect et en le trouvant pour être [] nous dit que n ~ Z; puisque Fin n est le type de nombres naturels inférieur à n, il n'y a aucune valeur qu'un appelant pourrait utiliser pour remplir le deuxième argument.

at : Vect n a -> Fin n -> a 
at [] FZ impossible 
at [] (FS i) impossible 
at (x::xs) FZ = x 
at (x::xs) (FS i) = at xs i 

La plupart du temps, vous pouvez omettre des cas impossibles.

Je préfère légèrement la notation d'Agda pour le même concept, qui utilise le symbole () pour identifier explicitement quel bit de l'expression d'entrée est impossible. Je l'aime parce que parfois vous apprenez seulement qu'un cas est impossible après avoir fait une autre correspondance de modèle sur les arguments; Quand la chose impossible est enterrée plusieurs couches, il est bon d'avoir une aide visuelle pour vous aider à repérer où elle était.