Diese min -Definition arbeitet an zwei Kirchennummern und gibt am wenigsten groß aus. Jede Zahl wird zu einer Fortsetzung, die ihr pred zum anderen schickt, zig und zag, bis Null erreicht ist. Darüber hinaus hängt eine der Zahlen jedes Mal, wenn f aufgerufen wird, f an das Ergebnis an, so dass am Ende (\ f x -> f (... (f (f x)) ...)) steht, wobei die Anzahl der fs auf der rechten Seite die Häufigkeit ist, mit der die erste Fortsetzung aufgerufen wurde.
Es scheint, als ob min nicht in System-F eingegeben werden kann. Um es beispielsweise auf GHC auszuführen, musste ich unsafeCoerce zweimal verwenden:
Ist es möglich, min auf System-F (oder den Kalkül von Konstruktionen) einzugeben?
Die Funktion (ist es bekannt? Es sieht wirklich schlau aus) ist typisierbar, es funktioniert einfach nicht mit Church-encoded nats.
Hier ist der Typ, den GHC leitet:
%Vor%Hier kommt der gewünschte Typ am nächsten:
%Vor% Um mit Church-encoded nats min zu arbeiten, müssen zwei Argumente vom Typ (a -> a) -> a -> a akzeptiert werden, d. h. A muss vom Typ a -> a sein, d. h.
d. t2 ~ (t2 -> t1) -> t1 , was eine Schleife ist. Es gibt keine rekursiven Typen in System F oder CoC und daher ist der Begriff nicht typisierbar.
Allerdings habe ich das Rank2Types Zeug ignoriert. Wie auch immer,
ist ebenfalls ein Fehler vom Typ unendlich.
Tags und Links haskell types agda dependent-type type-theory