Liste der existentiell quantifizierten Werte in Haskell

Question

Ich frage mich, warum dieses Stück Code nicht geben Prüfung:

{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}

module Main where

foo :: [forall a. a]
foo = [1]

ghc klagt:

Could not deduce (Num a) from the context ()
  arising from the literal `1' at exist5.hs:7:7

Da:

Prelude> :t 1
1 :: (Num t) => t
Prelude> 

scheint es, dass der (Num t) Kontext nicht () Kontext von arg mithalten kann. Der Punkt, den ich nicht verstehen kann, ist, dass da () allgemeiner als (Num t), letztere sollte und Einbeziehung der ehemaligen. Hat das etwas mit Mangel an Haskell Unterstützung für Unter Typisierung zu tun?

Vielen Dank für jeden Kommentar zu diesem Thema.

Answer 1

Sie verwenden nicht existentielle Quantifizierung hier. Sie verwenden Rang N-Typen.

Hier [forall a. a] bedeutet, dass jedes Element, jede mögliche Art (nicht jedes) haben muß. So [undefined, undefined] wäre eine gültige Liste dieser Art sein, und das ist im Grunde ist es.

Zur Erweiterung auf, dass etwas: Wenn ein Listentyp [forall a. a] hat das bedeutet, dass alle Elemente Typen forall a. a haben. Das bedeutet, dass jede Funktion, die jede Art von Argument nimmt, ein Element dieser Liste als Argument nehmen. Das ist nicht mehr wahr, wenn Sie in einem Element setzen, die einen spezifischeren Typ als forall a. a hat, so kann man nicht.

Um eine Liste zu erhalten, die jede Art enthalten können, müssen Sie Ihre eigene Liste Typ mit existenziellen Quantifizierung definieren. Wie so:

data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil

Natürlich, wenn Sie Elementtypen mindestens instantiate Show zurückhalten, können Sie nichts tun, mit einer Liste dieser Art.

Answer 2

Zuerst Ihr Beispiel bekommt nicht einmal, dass bei mir weit für den aktuellen GHC, da Sie ImpredecativeTypes auch aktivieren müssen. Dadurch ergibt sich eine Warnung, dass ImpredicativeTypes wird in der nächsten GHC vereinfacht oder entfernt werden. So sind wir nicht in einem guten Gebiet hier. Trotzdem die richtige Zugabe von Num-Einschränkung (foo :: [forall a. Num a => a]) erlaubt Ihrem Beispiel zu kompilieren.

Lassen wir beiseite imprädikative Typen und Blick auf ein einfacheres Beispiel:

data Foo = Foo (forall a. a)
foo = Foo 1

Dies ist kompiliert auch nicht mit dem Fehler Could not deduce (Num a) from the context ().

Warum? Nun, die Art Versprechen, dass Sie gehen zu den Foo-Konstruktor etwas mit der Qualität, die für jede Art a geben, ist es eine a produziert. Das einzige, was erfüllt diese ist unten. Ein Ganzzahlliteral, auf der anderen Seite, dass Versprechen für jede Art a , das die Klasse Num es erzeugt eine a. So sind die Typen eindeutig unvereinbar. Wir können jedoch ziehen die forall ein bisschen weiter aus, zu bekommen, was Sie wollen wahrscheinlich:

data Foo = forall a. Foo a
foo = Foo 1

Damit compiliert. Aber was können wir damit machen? Nun wollen wir versuchen, einen Extraktor Funktion zu definieren:

unFoo (Foo x) = x

Oops! Quantified type variable 'a' escapes. So können wir das definieren, aber wir können nicht mit ihm viel interessanter machen. Wenn wir einen Klassenkontext gab, dann zumindest konnten wir einige der Klassenfunktionen auf sie aus.

Es gibt eine Zeit und Ort für Existenziale, darunter auch solche, ohne Klassenkontext, aber seine ziemlich selten, vor allem, wenn Sie am Anfang. Wenn man sie am Ende noch mit, oft wird es im Rahmen der GADTs sein, die eine Ober existenzieller Typen sind, in denen aber die Art und Weise, dass Existenziale fühlt sich ganz natürlich entstehen.

Answer 3

Da die Erklärung [forall a. a] ist (in Sinn) das Äquivalent zu sagen „, habe ich eine Liste, und wenn Sie (also der Computer) einen Typ wählen, I Garantie , dass die Elemente der Liste dieser Typ wird. "

Der Compiler „ruft Ihren Bluff“, so zu sprechen, durch beschweren: „Ich weiß", dass, wenn Sie mir eine 1, dass diese Art in der Num Klasse ist, aber Sie haben gesagt, ich wählen könnte jede Art ich für diese Liste wollte. "

Im Grunde Sie versuchen, den Wert eines universellen Typs zu verwenden, als ob es die Art eines universellen Wertes war. Das ist nicht die gleiche Sache, aber.