RankNTypes: gelten die gleiche Funktion zu Paaren unterschiedlicher Typen

Question

ich diese Funktion zu definieren versuchte, drei Listen von Paaren neu zu formieren:

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 


main = do 
    let x = mapAndZip3 (fst) [(1,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5,"cake"),(4,"pudding")] 
    print x -- was expecting [(1,"chips",5), (2,"rice",4)] 

Zuerst habe ich nicht die RankNTypes oder die forall umfassen, aber dann nach dem einsehen this, nämlich die liftTup definition, ich dachte, dass es genug sein sollte.

Aber klar, es war nicht, wie ich noch einen Fehler:

mapAndZip3.hs:8:25: 
Couldn't match type `x' with `(f0 x, b0)' 
    `x' is a rigid type variable bound by 
     a type expected by the context: x -> f0 x at mapAndZip3.hs:8:13 
Expected type: x -> f0 x 
    Actual type: (f0 x, b0) -> f0 x 
In the first argument of `mapAndZip3', namely `(fst)' 

ich eindeutig ein begrenztes Verständnis des forall Schlüsselwort, aber von dem, was ich verstand es soll in diesem Fall erlauben für f jeden Typ zu akzeptieren. Was ich nicht verstehe ist: Einmal innerhalb eines gegebenen Kontexts und einmal verwendet, wird die Definition für den verbleibenden Kontext "fixiert"?

Es scheint nicht so, denn wenn ich "Chips" und "Reis" mit Ints ersetze, beschwert sich der Compiler immer noch, also nehme ich an, dass etwas falsch ist (natürlich, wenn ich den Typ Annotation von entferne mapAndZip3 in diesem letzten Fall funktioniert alles, weil die Signatur auf mapAndZip3 :: (a -> t) -> [a] -> [a] -> [a] -> [(t, t, t)] vereinfacht wird, aber das ist nicht was ich will).

Ich fand auch diesen question, kann aber nicht wirklich machen, wenn diese das gleiche Problem oder nicht, da die Funktion ich nicht id anzuwenden bin versucht, aber fst oder snd, Funktionen, die tatsächlich verschiedene Arten (a -> b) zurück.

Answer 1

Das Problem in Ihrer Signatur ist die f. Sagen wir es ein wenig erweitern:

mapAndZip3 :: forall (a :: *) (b :: *) (c :: *) (f :: *->*) 
      => (forall x. x -> f x) -> [a] -> [b] -> [c] 
           -> [(f a, f b, f c)] 

f hier soll „jede Art-Level-Funktion“ sein, in Ihrem Instanziierung wäre es type f (a,b) = a sein. Aber Haskell erlaubt Ihnen nicht, über Typ-Level-Funktionen zu abstrahieren, nur über Typ-Konstruktoren, wie Maybe oder IO. So wäre mapAndZip3 Just eigentlich möglich, aber fst baut nicht aber dekonstruieren einen Tupeltyp.

Funktionen auf Typenebene gibt es in Haskell98 nicht einmal, sie sind erst seit TypeFamilies möglich. Das Problem ist im Grunde, dass die Sprache von Haskell untypisiert ist , aber Typ-Level-Funktionen sind erforderlich, um insgesamt Funktionen sein . Aber dann können Sie wirklich keine nichttriviale Funktion definieren (d. H. Eine andere als id oder Typkonstruktoren), die auf allen Typen definiert ist. Type-Level fst ist sicherlich nicht insgesamt, es funktioniert nur auf Tupel-Typen.

Um mit solchen Funktionen arbeiten zu können, müssen Sie ihren Kontext explizit anders angeben. Mit TypeFamilies könnte es wie folgt funktionieren:

class TypeFunctionDomain d where 
    type TypeFunction d :: * 

instance TypeFunctionDomain (a,b) where 
    type TypeFunction (a,b) = a 

mapAndZip3 :: (forall x. TypeFunctionDomain x => x -> TypeFunction x) 
      -> [a] -> [b] -> [c] 
        -> [(TypeFunction a, TypeFunction b, TypeFunction c)] 

Dies ist jedoch nicht wirklich das, was Sie wollen: es nicht möglich wäre, im gleichen Umfang auch eine TypeFunctionDomain Instanz definieren snd corrsponding zu, was bedeutet, dass mapAndZip3 wouldn effektiv Sie sind überhaupt nicht polymorph, sondern arbeiten nur mit einer einzigen Funktion.

Diese Probleme können nur dann richtig in abhängig typisierten Sprachen wie Agda gelöst werden, wo Arten wirklich nur Arten von Typen sind und Sie können Typ-Level-Funktionen ebenso wie Wert-Level-Funktionen definieren. Aber das kommt als etwas von einem Preis: alle Funktionen müssen Gesamtfunktionen sein! Das ist nicht wirklich eine schlechte Sache, aber es bedeutet, dass diese Sprachen im Allgemeinen nicht wirklich Turing-vollständig sind (was die Möglichkeit einer Endlosschleife/-rekursion erfordern würde; das ist jedoch ⟂ in Bezug auf die vollständige Ergebnisauswertung).

---

Die Dinge haben sich ein wenig mit dem Aufkommen von kind polymorphism etc. geändert.

Das ist anders als z.B. C++, das erlaubt - wenn auch mit sehr schrecklichen Syntax - Ente-typisierte Typ-Level-Funktionen, durch Vorlagen. Das kann eine ziemlich nette Eigenschaft sein, aber eine der Konsequenzen ist, dass Sie oft völlig unlesbare Fehlermeldungen erhalten (mit noch weniger Beziehung zum eigentlichen Problem als GHCs schlechteste "Possible fix" Hinweise ...), wenn Sie versuchen, eine Vorlage mit zu instanziieren ein Typargument außerhalb der impliziten Domäne.

Answer 2

Das Problem ist, dass fst nicht den gewünschten Typ

(forall x. x -> f x) 

Die Art der fst ist

fst :: (a, b) -> a 

und a ist nicht von der Form f (a,b) hat. Die f gibt es eine Variable, die mit einem Typkonstruktor instanziiert werden muss, etwa [], Maybe, Either Bool. f kann für keine "Typ-Funktion" wie Λ (a,b) -> a stehen, es muss ein Typkonstruktor sein.

Es funktioniert, wenn wir es eine Funktion der erforderlichen Art (sorry, dumm Beispiel) liefern:

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 

fst0 x = (True,x) 

main = do 
    let x = mapAndZip3 (fst0) [(1 :: Int,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5 :: Int,"cake"),(4,"pudding")] 
    print x 

da hier fst0 hat den Typ a -> ((,) Bool) a, die die Form x -> f x hat.