Type de fonction identité anonyme Idris

Question

Lors de la vérification du type si id à Idris, nous obtenons ce que nous attendons:

> :type id 
id : a -> a 

Cependant, la vérification de la version d'expression lambda renvoie une erreur difficile:

> :type \x => x 
(input):Incomplete term \x => x 

Pourquoi est-ce? Si j'utilise une fonction pour forcer le contexte de x à un type, je reçois ce que j'attendais:

> :type \x => x+1 
\x => x + 1 : Integer -> Integer 

Answer 1

inférence de type, en général, est indécidable pour les types dépendants, voir par exemple the answers to this CS.SE question. Dans Idris, vous pouvez vous en passer en ne spécifiant pas les types pour certains termes, mais pas tous.

Si vous ajoutez votre définition dans un fichier .idr et essayez de le charger, comme

myId = \x => x 

vous obtiendrez le message d'erreur informatif

No type declaration for Main.myId

Voyons voir jusqu'où nous devons aller en lui donnant un type (le dessous est avec Idris 0.10.2):

myId : _ 
myId = \x => x 

When checking right hand side of myId with expected type iType

Type mismatch between _ -> _ (Type of \x => x) and iType (Expected type)

OK, nous allons essayer un type de fonction:

myId : _ -> _ 
myId = \x => x 

When checking right hand side of myId with expected type ty -> hole

Type mismatch between ty (Type of x) and hole (Expected type)

Je vous épargnerai les étapes suivantes, mais essentiellement myId : {a : Type} -> a -> _ et myId : {a : Type} -> _ -> a les deux échouent de la même façon, nous laissant avec

myId : {a : _} -> a -> a 
myId = \x => x 

Nous avons donc dû spécifier le type complet de myId à l'exception du niveau de l'univers de la variable de type a.

La version finale de la signature du type de myId peut aussi être écrit comme

myId : a -> a 
myId = \x => x