Warum muss ein Funktionstyp "umgebrochen" werden, damit der Typüberprüfer erfüllt wird?

Question

Folgende Programmtyp-Kontrollen:

{-# LANGUAGE RankNTypes #-} 

import Numeric.AD (grad) 

newtype Fun = Fun (forall a. Num a => [a] -> a) 

test1 [u, v] = (v - (u * u * u)) 
test2 [u, v] = ((u * u) + (v * v) - 1) 

main = print $ fmap (\(Fun f) -> grad f [1,1]) [Fun test1, Fun test2] 

Aber dieses Programm fehlschlägt:

main = print $ fmap (\f -> grad f [1,1]) [test1, test2] 

Mit dem Typ-Fehler:

Grad.hs:13:33: error: 
    • Couldn't match type ‘Integer’ 
        with ‘Numeric.AD.Internal.Reverse.Reverse s Integer’ 
     Expected type: [Numeric.AD.Internal.Reverse.Reverse s Integer] 
        -> Numeric.AD.Internal.Reverse.Reverse s Integer 
     Actual type: [Integer] -> Integer 
    • In the first argument of ‘grad’, namely ‘f’ 
     In the expression: grad f [1, 1] 
     In the first argument of ‘fmap’, namely ‘(\ f -> grad f [1, 1])’ 

letztere Programm sieht Intuitiv richtig. Schließlich hat die folgende, scheinbar gleichwertige Programmarbeit:

main = print $ [grad test1 [1,1], grad test2 [1,1]] 

Es sieht aus wie eine Beschränkung in Art System GHC. Ich würde gerne wissen, was den Fehler verursacht, warum diese Einschränkung existiert, und mögliche Problemumgehungen neben dem Umbruch der Funktion (per Fun oben).

. (Anmerkung: dies durch die Monomorphie Beschränkung nicht verursacht wird; Kompilieren mit NoMonomorphismRestriction hilft nicht)

Answer 1

Dies ist ein Problem mit dem Typensystem von GHC. Es ist übrigens wirklich GHC-Typ-System; Das ursprüngliche Typsystem für Haskell/ML-ähnliche Sprachen unterstützt keinen höheren Polymorphismus, geschweige denn impredikativen Polymorphismus, was wir hier verwenden.

Das Problem ist, dass, um dies zu überprüfen müssen wir forall s an jeder Position in einem Typ unterstützen. Nicht nur an der Vorderseite des Typs gebündelt (die normale Einschränkung, die Typrückschluss erlaubt).Sobald Sie diesen Bereich verlassen, wird der Typrückschluss im Allgemeinen unentscheidbar (für Rang n Polymorphismus und darüber hinaus). In unserem Fall müsste der Typ [forall a. Num a => a -> a] sein, was ein Problem ist, wenn man bedenkt, dass es nicht in das oben besprochene Schema passt. Es würde uns erfordern impredicative Polymorphismus, so genannt, weil a Bereiche über Typen mit forall s in ihnen und so a könnte mit dem Typ ersetzt werden, in dem es verwendet wird.

Also, deshalb wird es einige Fälle geben, die sich schlecht verhalten, nur weil das Problem nicht vollständig lösbar ist. GHC hat eine gewisse Unterstützung für Rang-n-Polymorphismus und ein wenig Unterstützung für imprädikativen Polymorphismus, aber es ist im Allgemeinen besser, nur Newtyp-Wrapper zu verwenden, um zuverlässiges Verhalten zu erhalten. Soweit ich weiß, rät GHC auch davon ab, dieses Feature zu verwenden, weil es so schwierig ist, genau herauszufinden, was der Typ-Inferenz-Algorithmus handhaben wird.

Zusammengefasst sagt math, dass es flockig Fälle sein werden und newtype Wrapper sind die besten, wenn auch etwas unbefriedigende Weise, mit ihm fertig zu werden.

Answer 2

Der Typ Inferenzalgorithmus nicht höheren Rang Typen schließen (die mit forall auf der linken Seite von ->). Wenn ich mich richtig erinnere, wird es unentscheidbar. Wie auch immer, betrachten Sie diesen Code

foo f = (f True, f 'a') 

was sollte sein Typ sein? Wir konnten

haben

foo :: (forall a. a -> a) -> (Bool, Char) 

aber wir auch

foo :: (forall a. a -> Int) -> (Int, Int) 

oder für jede Art Konstruktor F :: * -> *

foo :: (forall a. a -> F a) -> (F Bool, F Char) 

hier, soweit ich sehe, haben könnte, können wir eine nicht gefunden Haupttyp - Ein Typ, der dem allgemeinsten Typ entspricht, den wir foo zuweisen können.

Wenn ein Haupttyp nicht vorhanden ist, kann die Typrückschlussmaschinerie nur einen suboptimalen Typ für foo auswählen, was später zu Typfehlern führen kann. Das ist schlecht. Stattdessen verwendet GHC eine Inferenz-Engine vom Typ Hindley-Milner, die stark erweitert wurde, um erweiterte Haskell-Typen abzudecken. Dieser Mechanismus wird, im Gegensatz zu einfachem Hindley-Milner, f einem polymorphen Typ zuweisen, der vom Benutzer ausdrücklich gefordert wurde, z. indem Sie foo eine Signatur geben.

Mit einem Wrapper newtype wie Fun wird auch GHC in ähnlicher Weise angewiesen, den polymorphen Typ für f bereitzustellen.