RankNTypes und PolyKinds

Question

Was ist der Unterschied zwischen f1 und f2?

$ ghci -XRankNTypes -XPolyKinds 
Prelude> let f1 = undefined :: (forall a  m. m a -> Int) -> Int 
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
Prelude> :t f1 
f1 :: (forall   (a :: k) (m :: k -> *). m a -> Int) -> Int 
Prelude> :t f2 
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) -> Int 

Bezogen auf diese Frage auf RankNTypes and scope of forall. Beispiel aus dem GHC-Benutzerhandbuch unter kind polymorphism.

Answer 1

f2 erfordert seine Argument in der Art k polymorph zu sein, während f1 sich nur polymorphe in der Art ist. Also, wenn Sie

definieren

{-# LANGUAGE RankNTypes, PolyKinds #-} 
f1 = undefined :: (forall a m. m a -> Int) -> Int 
f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
x = undefined :: forall (a :: *) m. m a -> Int 

dann :t f1 x Typen in Ordnung, während :t f2 x klagt:

*Main> :t f2 x 

<interactive>:1:4: 
    Kind incompatibility when matching types: 
     m0 :: * -> * 
     m :: k -> * 
    Expected type: m a -> Int 
     Actual type: m0 a0 -> Int 
    In the first argument of ‘f2’, namely ‘x’ 
    In the expression: f2 x 

Answer 2

Lassen Sie uns blutig sein. Wir müssen alles quantifizieren und den Bereich der Quantifizierung angeben. Werte haben Typen; Dinge auf Typenebene haben Arten; Arten leben in BOX.

f1 :: forall (k :: BOX). 
     (forall (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

nun in keinem Beispiel Typ ist k explizit quantifiziert, so ghc entscheiden, wo diese forall (k :: BOX), legte auf der Grundlage, ob und wo k erwähnt wird. Ich bin mir nicht ganz sicher, ob ich die Politik wie gesagt verstehe oder bereit bin, sie zu verteidigen.

Ørjan gibt ein gutes Beispiel für den Unterschied in der Praxis. Lasst uns auch blutig sein. Ich schreibe /\ (a :: k). t, um die Abstraktion explizit zu machen, die forall und f @ type für die entsprechende Anwendung entspricht. Das Spiel ist, dass wir die @-Argumente auswählen, aber wir müssen bereit sein, mit allem, was der Teufel wählen kann, fertig zu werden.

Wir haben

x :: forall (a :: *) (m :: * -> *). m a -> Int 

und kann dementsprechend feststellen, dass f1 x wirklich

f1 @ * (/\ (a :: *) (m :: * -> *). x @ a @ m) 

jedoch ist, wenn wir versuchen, f2 x die gleiche Behandlung zu geben, sehen wir

f2 (/\ (k :: BOX) (a :: k) (m :: k -> *). x @ ?m0 @ ?a0) 
?m0 :: * 
?a0 :: * -> * 
where m a = m0 a0 

Die Haskell-Typ-System behandelt Typ-Anwendung als rein syntaktisch, so dass der einzige Weg, kann diese Gleichung gelöst werden soll, indem die Funktionen zu identifizieren und zu identifizieren, die Argumente

(?m0 :: * -> *) = (m :: k -> *) 
(?a0 :: *)  = (a :: k) 

aber diese Gleichungen sind nicht einmal gut kinded, weil k nicht frei gewählt werden: es ist /\ -ed nicht @ -ed.

Um sich mit diesen überpolymorphen Typen vertraut zu machen, ist es gut, alle Quantifizierer auszugeben und dann herauszufinden, wie sich das zum Spiel gegen den Teufel entwickelt. Wer wählt was und in welcher Reihenfolge. Das Verschieben eines forall innerhalb eines Argumenttyps ändert seine Auswahl und kann oft den Unterschied zwischen Sieg und Niederlage ausmachen.

Answer 3

Die Art der f1 Orte mehr Beschränkungen seiner Definition, während die Art der f2 Orte mehr Beschränkungen seines Argument.

Das heißt: die Art der f1 erfordert seine Definition in der Art k polymorph zu sein, während die Art der f2 erfordert sein Argumentk in der Art polymorph zu sein.

f1 :: forall (k::BOX). (forall   (a::k) (m::k->*). m a -> Int) -> Int 
f2 ::     (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int 

-- Show restriction on *definition* 
f1 g = g (Just True) -- NOT OK. f1 must work for all k, but this assumes k is * 
f2 g = g (Just True) -- OK 

-- Show restriction on *argument* (thanks to Ørjan) 
x = undefined :: forall (a::*) (m::*->*). m a -> Int 
f1 x -- OK 
f2 x -- NOT OK. the argument for f2 must work for all k, but x only works for *