Polykinded Typ Zusammensetzung

Question

Ich habe ein paar Typ-Aliasnamen bekommt, die alle ein ähnliches Muster passen:

type Foo f = Bar (Qoox f) 
type Faa f = Bar (Qaax f) 
type Moo f = Fez (Rxoo f) 
type Maa f = Fez (Rxaa f) 
-- ... 

ich die Aliase Punkt frei machen will, so kann ich sie auf ihrem eigenen nutzen. Anstatt newtypes zu definieren, dachte ich, es ordentlich sein würde, wenn ich Typ-Level-Zusammensetzung tun könnte:

type Foo = Bar `Compose1` Qoox 
type Faa = Bar `Compose1` Qaax 
type Moo = Fez `Compose2` Rxoo 
type Maa = Fez `Compose2` Rxaa 
-- ... 

Aber ich halte mit mehreren Compose Typen zu definieren, weil die Basistypen unterschiedlicher Art sind.

Was Ich mag würde eine polykinded Typ-Level-Funktion

type family (.) (m :: k1 -> k) (n :: k2 -> k1) :: k2 -> k where 

So konnte ich

type Foo = Bar . Qoox 
type Faa = Bar . Qaax 
type Moo = Fez . Rxoo 
type Maa = Fez . Rxaa 
-- ... 

nur das tun, aber ich vermute, dass über Haskell aktuelle Fähigkeiten sein könnte, und ich don‘ Ich möchte Zeit verschwenden, um das Unmögliche möglich zu machen.

Kann eine solche Zusammensetzung in Haskell mit den in GHC8 verfügbaren Erweiterungen erstellt werden?

Answer 1

Ich denke GHC ist derzeit nicht in der Lage, diese Punkt-frei zu machen.

GHCi 8.0 scheint dies zu akzeptieren.

> :set -XPolyKinds 
> type C (m :: k1 -> k) (n :: k2 -> k1) (t :: k2) = m (n t) 
> :i C 
type C (m :: k1 -> k) (n :: k2 -> k1) (t :: k2) = m (n t) :: k 

Beachten Sie jedoch, dass dies nicht teilweise angewendet werden kann, im Allgemeinen, und werden Sie benötigen, um Ihre Definitionen eta-erweitern.

z. Wir können type T = C [] [] nicht verwenden, aber wir können type T a = C [] [] a verwenden.

Ohne Eta-Erweiterung, ich glaube nicht, dass wir eine Art von Art k2 -> k zurückgeben können, es sei denn das ist ein Typ Konstruktor. Wir haben keine Lambdas auf Typenebene (oder teilweise Anwendung).