Typ Deconstruction

Question

Meine Datentypen müssen immer mindestens zwei Parameter, und die letzten beiden Parameter sind immer ‚q‘ und ‚m‘ jeweils:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances #-} 

data D1 q m = D1 q 
data D2 t q m = D2 q 

class Foo a where -- a has kind * -> * 
    f :: a x -> a x 

class (Foo b) => Bar b where -- b has kind * -> * 
    -- the purpose of g is to change ONE type parameter, while fixing the rest 
    -- the intent of the equality constraints is to decompose the parameter b into 
    -- its base type and 'q' parameter, then use the same base type with a *different* 
    -- `q` parameter for the answer 
    g :: (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    g (D2 q) = D2 $ fromIntegral q -- LINE 1 

Dieses Programm führt zu dem Fehler

Could not deduce (bBase ~ D2 t0) (LINE 1) 

Als ich die Instanz schrieb, hatte ich bestimmt bBase ~ D2 t. Ich denke, dass t irgendwie nicht gebunden ist (daher die Einführung von t0), und ich weiß nicht, ob GHC diesen Typ überhaupt dekonstruieren kann. Oder vielleicht mache ich nur etwas Dummes.

Mehr zu diesem Punkt, diese Art von Typ Gleichheit/Typ Dekonstruktion wäre nicht notwendig, wenn ich den Parameter auf Bar haben Art * -> * -> *. Aber dann erzwingen konnte ich nicht die Einschränkung Foo:

class (Foo (b q)) => Bar b where -- b has kind * -> * -> * 
    g :: b q m -> q b' -- this signature is now quite simple, and I would have no problem implementing it 

Das wird nicht funktionieren, weil q kein Parameter Bar ist, und ich will nicht es auf einen Parameter zu Bar.

fand ich eine Lösung, die zwei extra „Dummy“ zugeordnet Typen, aber ich weiß nicht wirklich, wie sie um sich zu haben, wenn ich sie nicht brauchen:

class (Foo b, b ~ (BBase b) (BMod b)) => Bar b where -- b has kind * -> * 
    type BBase b :: * -> * -> * 
    type BMod b :: * 

    g :: (Qux (BMod b), Qux q') => b m -> (BBase b) q' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    type BBase (D2 t q) = D2 t 
    type BMod (D2 t q) = q 

    g (D2 q) = D2 $ fromIntegral q 

Dies funktioniert, aber es beläuft sich ausdrücklich auf den Typ dekonstruieren, was ich angesichts des einfachen Typs der Instanz für unnötig halte.

Ich bin auf der Suche nach einer Lösung für beide Ansätze: entweder sagen Sie mir, wie ich eine Klassenbeschränkung auf eine "mehr angewandte" Art erzwingen kann, oder sagen Sie mir, wie GHC dekonstruieren Typen.

Danke!

Answer 1

Von dem, was Sie beschreiben, haben Sie die Typen b' :: * -> * -> *, für die Sie die angewandte b' t :: * -> * (für alle t) beschränken möchten.

Wie Sie summise, benötigen Sie entweder einen Typ dekonstruieren, die hier Ihren Versuch von einem b :: * -> * beginnt, ist davon ausgegangen, das Ergebnis einer Art Anwendung b = b' t, sein oder eine Einschränkung für eine „mehr-Anwendung“ zu erzwingen Geben Sie stattdessen vom Anfangspunkt einer b' :: * -> * -> * ein.

Dekonstruieren eines Typs ist nicht möglich, da der Compiler nicht weiß, ob b sogar "dekonstruierbar" ist. Tatsächlich kann es nicht sein, z.B. kann ich eine Instanz instance Bar Maybe machen, aber Maybe kann nicht in einen Typ b' :: * -> * -> * und einen Typ t :: * dekonstruiert werden.

anstelle von einem Typ Ab b' :: * -> * -> * können die Einschränkungen für eine Anwendung von b' in den Körper der Klasse bewegt werden, wobei die Variablen quantifiziert werden:

class Bar (b :: * -> * -> *) where 
     g :: (Foo (b q1), Foo (b q2)) => b q1 m -> b q2 m 

Für Ihr Beispiel ist eine weitere Falte dort: q1 und q2 können ihre eigenen Nebenbedingungen haben, zB Für die D2 Instanz benötigen Sie die Integral Einschränkung. Bar behebt jedoch die Einschränkungen für q1 und q2 für alle Instanzen (in diesem Fall die leere Einschränkung).Eine Lösung ist „Constraint-kinded Typ Familien“ zu verwenden, die Instanzen erlauben, ihre eigenen Einschränkungen zu spezifizieren:

class Bar (b :: * -> * -> *) where 
     type Constr b t :: Constraint 
     g :: (Foo (b q1), Foo (b q2), Constr b q1, Constr b q2) => b q1 m -> b q2 m 

(enthalten {-# LANGUAGE ConstraintKinds #-} und importieren GHC.Prim)

Dann können Sie Ihre D2 Beispiel schreiben:

instance Bar (D2 t) where 
     type Constr (D2 t) q = Integral q 
     g (D2 q) = D2 $ fromIntegral q