Wann (wenn überhaupt) können Synonyme teilweise eingegeben werden?

Question

Offenbar ein wenig abwesend, schrieb ich something like folgendes:

{-# LANGUAGE ConstraintKinds  #-} 
{-# LANGUAGE TypeFamilies  #-} 

class Foo f where 
    type Bar f :: * 
    retbar :: Bar f -> IO f 

type Baz f = (Foo f, Eq f) 

    -- WithBar :: * -> (*->Constraint) -> * -> Constraint 
type WithBar b c f = (c f, Bar f ~ b) 

instance Foo() where 
    type Bar() =() 
    retbar = return 

naim :: WithBar() Baz u => IO u -- why can I do this? 
naim = retbar() 

main = naim :: IO() 

Erst nach erfolgreich kompilieren, erkannte ich, diese sollte nicht tatsächlich funktionieren: Baz als eine Art Synonym mit einem Argument definiert ist, aber hier benutze ich es ohne ein direktes Argument. Normalerweise bellt mich GHC an Type synonym ‘Baz’ should have 1 argument, but has been given none wenn ich sowas versuche.

Nun versteh mich nicht falsch: Ich würde wirklich gerne in der Lage sein, das zu schreiben, und es ist einfach genug zu sehen, wie es in diesem bestimmten Beispiel funktionieren könnte (WithBar würde die Signatur naim :: (Foo u, Bar u ~()) => IO u ergeben, die sicherlich ist gut), aber was ich nicht verstehe, warum es eigentlich genau so hier funktioniert. Ist es vielleicht nur ein Bug in ghc-7.8.2 dies zu erlauben?

Answer 1

Ich weiß nicht, was die offiziellen Regeln sind, aber es scheint vernünftig für diese Art von Sache zu arbeiten auf der Basis einer äußersten linken Synonym Expansionsstrategie. Es kommt nur darauf an, dass Typ-Synonyme in einer separaten und abschließenden Phase entsorgt werden können, bevor der Rest der Typ-Prüfung stattfindet. Ich weiß nicht, ob man ein teilweise angewendetes Synonym F als Argument für ein anderes Typ-Synonym G verwenden kann, solange G sicherstellt, dass F seine fehlenden Argumente erhält, aber das stimmt sicherlich mit der Idee überein, dass Synonyme synonym sind sind eine flache Bequemlichkeit.

Answer 2

Teilanwendung sollte durch die LiberalTypeSynonyms Erweiterung aktiviert werden.

Grundsätzlich verschiebt dies die meisten Konsistenzprüfung von Typ Synonyme, bis sie erweitert wurden, so dass Ihre "Inlining" Erklärung im Wesentlichen die richtige Idee ist.

Die seltsame Sache hier ist jedoch, dass diese Erweiterung nicht impliziert von denen in Ihrem Modul ist. Ich habe gerade getestet, und teilweise Anwendung funktioniert im Allgemeinen nicht nur mit ConstraintKinds, TypeFamilies und PolyKinds. (Ich habe letzteres hinzugefügt, weil die Typen vor der Erweiterung überprüft wurden und meine Testtypen sonst die falschen erhalten haben.)

Trotzdem lädt sich Ihre Datei in GHCi 7.8.3 gut. Vielleicht ist diese irgendeine Art von Fehler, auch wenn es eine Erweiterung gibt, um es legal zu machen.

Answer 3

Ihre Datei kompiliert in GHC 7.8, aber in GHC 7.10 Ich erhalte eine Fehlermeldung:

Type synonym ‘Baz’ should have 1 argument, but has been given none

In the type signature for ‘naim’: naim :: WithBar() Baz u => IO u

Hinzufügen -XLiberalTypeSynonyms behebt den Fehler. Daher ist dies ein Fehler in 7.8.