Art der anonymen Identitätsfunktion in Idris

Question

Wenn die Art zu überprüfen, ob id in Idris, wir bekommen, was wir erwarten würden:

> :type id 
id : a -> a 

jedoch die Lambda-Ausdruck Versionsprüfung wirft einen schwierigen Fehler:

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

Warum ist das? Wenn ich eine Funktion den Zusammenhang von x auf eine Art zu zwingen, ich bekommen, was ich erwarten würde:

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

Answer 1

Typ-Inferenz im allgemeinen für abhängige Arten unentscheidbar ist, siehe z.B. the answers to this CS.SE question. In Idris können Sie nicht nur Typen für einige Begriffe angeben, sondern alle.

Wenn Sie Ihre Definition zu einer .idr Datei hinzufügen und versuchen, es zu laden, wie

myId = \x => x 

Sie die informative Fehlermeldung

No type declaration for Main.myId

Also mal sehen bekommen, wie weit müssen wir gehen Geben Sie einen Typ (der folgende ist mit 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, lassen Sie uns einen Funktionstyp versuchen:

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)

Ich werde Sie nachfolgende Schritte ersparen, aber im Grunde myId : {a : Type} -> a -> _ und myId : {a : Type} -> _ -> a beide nicht die gleiche Art und Weise, so dass uns mit

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

Also mussten wir den vollen Typ von myId mit Ausnahme der Universumsebene der Typvariablen a angeben.

Die endgültige Version von myId ‚Art Signatur s auch als

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