Gibt es einen Weg zu Union-Typ-Einschränkungen?

Question

Gibt es in Haskell eine Möglichkeit, mehrere Typenbeschränkungen miteinander zu verknüpfen, so dass die Vereinigung erfüllt ist, wenn einer von ihnen erfüllt ist?

Beispiel: Angenommen, ich hatte ein GADT durch eine DataKind parametriert, und ich wollte einige Konstrukteure nur Werte zurück für bestimmte Konstrukteuren der gegebenen Art, die pseudo-Haskell wäre:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
module Temp where 

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

data Fruit (c :: Color) where 
    Banana :: (c ~ Green | c ~ Yellow | c ~ Black) => Fruit c 
    Apple :: (c ~ Red | c ~ Green)    => Fruit c 
    Grape :: (c ~ Red | c ~ Green | c ~ White)  => Fruit c 
    Orange :: (c ~ Tawny)       => Fruit c 

ich kann versuchen, die OR mit typeclasses zu implementieren:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
module Temp where 

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

data Fruit (c :: Color) where 
    Banana :: BananaColor c => Fruit c 
    Apple :: AppleColor c => Fruit c 
    Grape :: GrapeColor c => Fruit c 
    Orange :: OrangeColor c => Fruit c 

class BananaColor (c :: Color) 
instance BananaColor Green 
instance BananaColor Yellow 
instance BananaColor Black 

class AppleColor (c :: Color) 
instance AppleColor Red 
instance AppleColor Green 

class GrapeColor (c :: Color) 
instance GrapeColor Red 
instance GrapeColor Green 
instance GrapeColor White 

class OrangeColor (c :: Color) 
instance OrangeColor Tawny 

doch nicht nur diese ausführlich, es ist auch etwas anders als das, was ich wollte, dass die ursprüngliche Vereinigung war geschlossen, aber die typeclasses sind alle offen. Es gibt nichts, jemanden zu stoppen von der Definition

instance OrangeColor Blue 

Und weil es geöffnet ist, gibt es keine Möglichkeit der Compiler ableiten könnte, dass [Apple, Grape, Banana][Fruit Green] es sei denn, sagte der Typ sein müssen.

Answer 1

Ich kann mir leider keinen Weg vorstellen, um wörtlich zu implementieren oder für Constraint s, aber wenn wir einfach Gleichheiten zusammenführen, wie in Ihrem Beispiel, können wir Ihren Typklassenansatz aufpeppen und es schaffen geschlossen mit Typfamilien und gehobenen Booleans. Dies funktioniert nur in GHC 7.6 und höher; Am Ende erwähne ich, wie es in GHC 7.8 schöner wird und wie es auf GHC 7.4 zurückportiert wird.

Die Idee ist folgende: So wie wir Wert-Level-Funktion isBananaColor :: Color -> Bool erklären konnte, so können auch wir einen Typ-Level-Funktion IsBananaColor :: Color -> Bool erklären:

type family IsBananaColor (c :: Color) :: Bool 
type instance IsBananaColor Green = True 
type instance IsBananaColor Yellow = True 
type instance IsBananaColor Black = True 
type instance IsBananaColor White = False 
type instance IsBananaColor Red = False 
type instance IsBananaColor Blue = False 
type instance IsBananaColor Tawny = False 
type instance IsBananaColor Purple = False 

Wenn wir wollen, können wir auch hinzufügen

type BananaColor c = IsBananaColor c ~ True 

Wir wiederholen diese dann für jede Fruchtfarbe und Fruit wie in Ihrem zweiten Beispiel definieren:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE TypeFamilies #-} 

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

data Fruit (c :: Color) where 
    Banana :: BananaColor c => Fruit c 
    Apple :: AppleColor c => Fruit c 
    Grape :: GrapeColor c => Fruit c 
    Orange :: OrangeColor c => Fruit c 

type family IsBananaColor (c :: Color) :: Bool 
type instance IsBananaColor Green = True 
type instance IsBananaColor Yellow = True 
type instance IsBananaColor Black = True 
type instance IsBananaColor White = False 
type instance IsBananaColor Red = False 
type instance IsBananaColor Blue = False 
type instance IsBananaColor Tawny = False 
type instance IsBananaColor Purple = False 
type BananaColor c = IsBananaColor c ~ True 

type family IsAppleColor (c :: Color) :: Bool 
type instance IsAppleColor Red = True 
type instance IsAppleColor Green = True 
type instance IsAppleColor White = False 
type instance IsAppleColor Blue = False 
type instance IsAppleColor Yellow = False 
type instance IsAppleColor Tawny = False 
type instance IsAppleColor Purple = False 
type instance IsAppleColor Black = False 
type AppleColor c = IsAppleColor c ~ True 

type family IsGrapeColor (c :: Color) :: Bool 
type instance IsGrapeColor Red = True 
type instance IsGrapeColor Green = True 
type instance IsGrapeColor White = True 
type instance IsGrapeColor Blue = False 
type instance IsGrapeColor Yellow = False 
type instance IsGrapeColor Tawny = False 
type instance IsGrapeColor Purple = False 
type instance IsGrapeColor Black = False 
type GrapeColor c = IsGrapeColor c ~ True 

-- For consistency 
type family IsOrangeColor (c :: Color) :: Bool 
type instance IsOrangeColor Tawny = True 
type instance IsOrangeColor White = False 
type instance IsOrangeColor Red = False 
type instance IsOrangeColor Blue = False 
type instance IsOrangeColor Yellow = False 
type instance IsOrangeColor Green = False 
type instance IsOrangeColor Purple = False 
type instance IsOrangeColor Black = False 
type OrangeColor c = IsOrangeColor c ~ True 

(Wenn Sie möchten, können Sie von -XConstraintKinds und die type XYZColor c = IsXYZColor c ~ True Typen loszuwerden, und definieren nur die Konstrukteure von Fruit als XYZ :: IsXYZColor c ~ True => Fruit c.)

Nun, was das Sie tut kaufen, und was es Sie nicht kaufen ? Auf der positiven Seite haben Sie die Möglichkeit, Ihren Typ zu definieren, wie Sie wollen, was definitiv ein Gewinn ist; und da Color geschlossen ist, kann niemand mehr type family instances hinzufügen und das brechen.

Allerdings gibt es Nachteile. Sie erhalten nicht die Inferenz, die Sie wollten, dass Sie automatisch wissen, dass [Apple, Grape, Banana] vom Typ Fruit Green ist; Was noch schlimmer ist, ist, dass den perfekt gültigen Typ (AppleColor c, GrapeColor c, BananaColor c) => [Fruit c] hat. Ja, es gibt keine Möglichkeit, dies zu monomorphisieren, aber GHC kann das nicht herausfinden. Um ehrlich zu sein, kann ich mir keine Lösung vorstellen, die Ihnen diese Eigenschaften verleiht, obwohl ich immer bereit bin, überrascht zu werden. Das andere offensichtliche Problem mit dieser Lösung ist, wie lang es ist, müssen Sie alle acht Farbgehäuse für jede IsXYZColor Typfamilie definieren! (Die Verwendung einer Marke neue Schriftfamilie für jeden ist auch ärgerlich, aber unvermeidlich mit Lösungen dieser Form.)

---

ich über diesem GHC 7 erwähnt.8 wird das schöner machen; Es wird dafür sorgen, dass nicht jeder einzelne Fall für jede einzelne IsXYZColor-Klasse aufgelistet werden muss. Wie? Nun, Richard Eisenberg et al. eingeführt geschlossen überlappende geordnete Typ Familien in GHC HEAD, und es wird in 7.8 verfügbar sein. Es gibt a paper in sumbission to POPL 2014 (und eine extended version) zum Thema, und Richard schrieb auch an introductory blog post (die scheinen, veraltete Syntax zu haben).

Die Idee besteht darin, Typfamilieninstanzen wie gewöhnliche Funktionen zu deklarieren: Die Gleichungen müssen alle an einer Stelle deklariert werden (die Open-World-Annahme wird entfernt) und in der Reihenfolge versucht, was Überlappungen erlaubt. So etwas wie

type family IsBananaColor (c :: Color) :: Bool 
type instance IsBananaColor Green = True 
type instance IsBananaColor Yellow = True 
type instance IsBananaColor Black = True 
type instance IsBananaColor c  = False 

ist mehrdeutig, weil IsBananaColor Green Matches sowohl die ersten und letzten Gleichungen; aber in einer normalen Funktion würde es gut funktionieren. So ist die neue Syntax:

type family IsBananaColor (c :: Color) :: Bool where 
    IsBananaColor Green = True 
    IsBananaColor Yellow = True 
    IsBananaColor Black = True 
    IsBananaColor c  = False 

Die type family ... where { ... } Block der Art Familie, die Art und Weise definiert Sie wollen es definieren; Es signalisiert, dass diese Typfamilie wie oben beschrieben geschlossen, geordnet und überlappend ist. Somit würde der Code in etwa wie folgt in GHC 7.8 werden (nicht getestet, da ich es nicht auf meinem Rechner installiert haben):

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

data Fruit (c :: Color) where 
    Banana :: IsBananaColor c ~ True => Fruit c 
    Apple :: IsAppleColor c ~ True => Fruit c 
    Grape :: IsGrapeColor c ~ True => Fruit c 
    Orange :: IsOrangeColor c ~ True => Fruit c 

type family IsBananaColor (c :: Color) :: Bool where 
    IsBananaColor Green = True 
    IsBananaColor Yellow = True 
    IsBananaColor Black = True 
    IsBananaColor c  = False 

type family IsAppleColor (c :: Color) :: Bool where 
    IsAppleColor Red = True 
    IsAppleColor Green = True 
    IsAppleColor c  = False 

type IsGrapeColor (c :: Color) :: Bool where 
    IsGrapeColor Red = True 
    IsGrapeColor Green = True 
    IsGrapeColor White = True 
    IsGrapeColor c  = False 

type family IsOrangeColor (c :: Color) :: Bool where 
    IsOrangeColor Tawny = True 
    IsOrangeColor c  = False 

Hooray, können wir dies lesen, ohne einschlafen aus Langeweile zu fallen! In der Tat werden Sie bemerken, dass ich für diesen Code auf die explizite IsXYZColor c ~ True Version umschaltete; Ich habe das getan, weil das Vorwort für die vier zusätzlichen Synonymen mit diesen kürzeren Definitionen viel offensichtlicher und ärgerlicher wurde!

---

Allerdings gehen wir in die entgegengesetzte Richtung und machen diesen Code hässlicher. Warum? Nun, GHC 7.4 (was leider immer noch auf meinem Rechner steht) unterstützt keine Typenfamilien mit einem Ergebnistyp von *. Was können wir stattdessen tun? Wir können Typklassen und funktionale Abhängigkeiten verwenden, um es zu fälschen. Die Idee ist, dass wir anstelle von IsBananaColor :: Color -> Bool eine Typklasse IsBananaColor :: Color -> Bool -> Constraint haben, und wir fügen eine funktionale Abhängigkeit von der Farbe zum booleschen Wert hinzu. Dann IsBananaColor c b ist erfüllbar wenn und nur wenn IsBananaColor c ~ b in der netteren Version; weil Color geschlossen ist und wir eine funktionale Abhängigkeit davon haben, gibt uns das immer noch die gleichen Eigenschaften, es ist nur hässlicher (obwohl meistens konzeptionell so). Ohne weitere Umschweife, der vollständige Code:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE FlexibleContexts #-} 

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

data Fruit (c :: Color) where 
    Banana :: BananaColor c => Fruit c 
    Apple :: AppleColor c => Fruit c 
    Grape :: GrapeColor c => Fruit c 
    Orange :: OrangeColor c => Fruit c 

class IsBananaColor (c :: Color) (b :: Bool) | c -> b 
instance IsBananaColor Green True 
instance IsBananaColor Yellow True 
instance IsBananaColor Black True 
instance IsBananaColor White False 
instance IsBananaColor Red False 
instance IsBananaColor Blue False 
instance IsBananaColor Tawny False 
instance IsBananaColor Purple False 
type BananaColor c = IsBananaColor c True 

class IsAppleColor (c :: Color) (b :: Bool) | c -> b 
instance IsAppleColor Red True 
instance IsAppleColor Green True 
instance IsAppleColor White False 
instance IsAppleColor Blue False 
instance IsAppleColor Yellow False 
instance IsAppleColor Tawny False 
instance IsAppleColor Purple False 
instance IsAppleColor Black False 
type AppleColor c = IsAppleColor c True 

class IsGrapeColor (c :: Color) (b :: Bool) | c -> b 
instance IsGrapeColor Red True 
instance IsGrapeColor Green True 
instance IsGrapeColor White True 
instance IsGrapeColor Blue False 
instance IsGrapeColor Yellow False 
instance IsGrapeColor Tawny False 
instance IsGrapeColor Purple False 
instance IsGrapeColor Black False 
type GrapeColor c = IsGrapeColor c True 

class IsOrangeColor (c :: Color) (b :: Bool) | c -> b 
instance IsOrangeColor Tawny True 
instance IsOrangeColor White False 
instance IsOrangeColor Red False 
instance IsOrangeColor Blue False 
instance IsOrangeColor Yellow False 
instance IsOrangeColor Green False 
instance IsOrangeColor Purple False 
instance IsOrangeColor Black False 
type OrangeColor c = IsOrangeColor c True 

Answer 2

Unten ist mein Versuch, das Problem zu kodieren. Die Hauptidee ist Frucht als Typklasse und verschiedene Arten von Früchten als Typen darzustellen, die diese Art Klasse implementieren

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black 

class Fruit a where 
    getColor :: a -> Color 

data Banana where 
    GreenBanana :: Banana 
    YellowBanana :: Banana 
    BlackBanana :: Banana 

instance Fruit Banana where 
    getColor GreenBanana = Green 
    getColor YellowBanana = Yellow 
    getColor BlackBanana = Black 

data Apple where 
    GreenApple :: Apple 
    RedApple :: Apple 

instance Fruit Apple where 
    getColor GreenApple = Green 
    getColor RedApple = Red 

Ihre Fragen letzte Zeile zeigt an, dass Sie etwas vom Typ [Fruit Green] wollen die natürlich bedeutet, dass Fruit Green eine sein sollte, Geben Sie where wie Green in dem obigen Code ein Wertkonstruktor ein. Wir müssen Green als eine Art, so etwas wie unten dargestellt:

data Red = Red 
data Green = Green 
data Black = Black 

data Fruit c where 
    GreenBanana :: Fruit Green 
    BlackBanana :: Fruit Black 
    RedApple :: Fruit Red 
    GreenApple :: Fruit Green 


greenFruits :: [Fruit Green] 
greenFruits = [GreenBanana, GreenApple]