7
Ich versuche, die Art des folgenden Ausdrucks zu folgern:Herleitung rekursive Ausdrücke Hindley Milner & Zwänge
let rec fix f = f (fix f)
, die den Typ (a -> a) -> a
unten nach oben Algorithmus Nach der Verwendung von (beschrieben gegeben werden sollte, in verallgemeinernde hindley-milner Typ Inferenzalgorithmen) mit der zusätzlichen Regel unter:
a1, c1 |-BU e1 : t1 B = fresh var
---------------------------------------------------------
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t
i mit folgenden Art bin übrig geblieben: t1 -> t2
und die folgenden Einschränkungen:
t0 = fix
t1 = f
t2 = f (fix f)
t3 = f
t4 = fix f
t5 = fix
t6 = f
t3 = t1
t3 = t4 -> t2
t5 = t0
t5 = t6 -> t4
t6 = t1
Ich kann nicht sehen, wie diese Einschränkungen so gelöst werden können, dass i (a -> a) -> a mit dem Typ links bin. Ich hoffe, es ist offensichtlich für jemanden zu sehen, wo ich falsch liege.
Bitte beachten Sie, dass 'let rec' einfach' let' sein sollte, ansonsten definieren Sie einfach eine Funktion 'rec :: ((a -> b) -> a) -> (a -> b) -> b'. –
@ Pthariens'Flame Entschuldigung Code Beispiel war nicht in Haskell, sondern eine ML-Stil Sprache. –
Okay, es ist nur so, dass du die Frage mit "haskell" versehen hast, also nahm ich an, dass das die Sprache war mit der du gearbeitet hast. Es tut uns leid! –