Есть ли способ ограничения типа соединения?

Question

В Haskell существует ли способ ИЛИ объединить несколько ограничений типа, так что объединение выполняется, если выполнено одно из них?

Например, предположим, что у меня был GADT параметризирован DataKind, и я хотел некоторые конструкторы только возвращаемые значения для некоторых конструкторов данного вида, псевдо-Haskell будет:

{-# 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 

я могу попытаться реализовать OR с помощью классов типов:

{-# 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 

но это не только многословен, он также немного отличается от того, что я намеревался в том, что первоначальный союз был закрыт, но все классы типов открыты. Там нет ничего, чтобы остановить кого-то из определения

instance OrangeColor Blue 

И потому он открыт, нет никакого способа, компилятор может сделать вывод, что [Apple, Grape, Banana] должен быть типа [Fruit Green], если не сказано.

Answer 1

Я не могу придумать способ буквально реализовать или для Constraint s, к сожалению, но если мы просто равны друг другу, как в вашем примере, мы можем подправить ваш подход к классу классов и сделать это закрыты семействами типов и подняты булевы. Это будет работать только в GHC 7.6 и выше; в конце я упомянул и то, как в GHC 7.8 будет лучше, и как сделать это в GHC 7.4.

Идея заключается в следующем: Так же, как мы могли бы объявить функцию значения уровня isBananaColor :: Color -> Bool, так же мы можем объявить функцию типа уровня IsBananaColor :: Color -> Bool:

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 

затем повторить это для каждого фруктового цвета, и определить Fruit как в вашем втором примере:

{-# 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 

(Если вы хотите, вы можете избавиться от -XConstraintKinds и type XYZColor c = IsXYZColor c ~ True типов, а просто определить конструкторы Fruit в XYZ :: IsXYZColor c ~ True => Fruit c.)

Теперь, что делает это купить вас, и что это не покупающего ? С положительной стороны вы получаете возможность определять свой тип так, как хотите, что определенно является победой; и поскольку Color закрыт, никто не может добавить больше экземпляров семейства типов и сломать это.

Однако, есть недостатки. Вы не получите вывод, который хотите сказать автоматически, что [Apple, Grape, Banana] имеет тип Fruit Green; Хуже то, что [Apple, Grape, Banana] имеет совершенно допустимый тип (AppleColor c, GrapeColor c, BananaColor c) => [Fruit c]. Да, нет возможности мономорфозировать это, но GHC не может понять это. Чтобы быть абсолютно честным, я не могу представить, какое решение вам дадут эти свойства, хотя я всегда готов удивляться. Другая очевидная проблема с этим решением заключается в том, как long - вам нужно определить все восемь цветных случаев для каждого семейства IsXYZColor! (Использование совершенно новый тип семьи для каждого также раздражает, но неизбежно с растворами этой формы.)

---

я Выше упоминалось, что GHC 7.8 будет делать это лучше; это будет сделано, устраняя необходимость перечислять каждый отдельный случай для каждого отдельного класса IsXYZColor. Как? Ну, Ричард Эйзенберг и др. введено Закрытые перекрывающиеся упорядоченные семейства типов в GHC HEAD, и он будет доступен в 7.8. Там есть a paper in sumbission to POPL 2014 (и extended version) на эту тему, и Ричард также написал an introductory blog post (который, как представляется, имеет устаревший синтаксис).

Идея состоит в том, чтобы разрешить типовые экземпляры типов объявляться как обычные функции: все уравнения должны быть объявлены в одном месте (исключая предположение открытого мира) и выполняются по порядку, что позволяет перекрывать. Что-то вроде

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 

неоднозначно, потому что IsBananaColor Green матчи обе первые и последние уравнения; но в обычной функции он будет работать нормально. Таким образом, новый синтаксис:

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

Это type family ... where { ... } блок определяет тип семьи так, как вы хотите определить его; он сигнализирует, что это семейство типов закрыто, упорядочено и перекрывается, как описано выше. Таким образом, код стал бы что-то вроде следующего в GHC 7.8 (непроверенной, так как я не он установлен на моей машине):

{-# 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, мы можем прочитать это, не засыпает от скуки! Фактически, вы заметите, что я перешел на явную версию IsXYZColor c ~ True для этого кода; Я сделал это потому, что, поскольку шаблон для дополнительных четырех синонимов стал намного более очевидным и раздражающим с этими более короткими определениями!

---

Однако, давайте перейдем в обратном направлении и сделаем этот код более уродливым. Зачем? Ну, GHC 7.4 (что, увы, у меня все еще есть на моей машине) не поддерживает типы семейств с типом результата не *. Что мы можем сделать вместо этого? Мы можем использовать классы типов и функциональные зависимости для подделки. Идея состоит в том, что вместо IsBananaColor :: Color -> Bool у нас есть класс типа IsBananaColor :: Color -> Bool -> Constraint, и мы добавляем функциональную зависимость от цвета к булевому. Тогда IsBananaColor c b выполним тогда и только тогда, когда IsBananaColor c ~ b в более приятной версии; потому что Color закрыт, и у нас есть функциональная зависимость от него, это все равно дает нам те же свойства, это просто уродливое (хотя в основном концептуально). Без дальнейших комментариев полный код:

{-# 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

Ниже я пытаюсь кодировать проблему. Основная идея состоит в том, чтобы представить свои плоды в качестве класса типа и различных видов фруктов в качестве типов, реализующих этот класс типа

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 

Ваши вопросы последняя строка указывает на то, что вы хотите что-то типа [Fruit Green] который, очевидно, означает, что Fruit Green должен быть тип, где в указанном выше коде значение «Зеленый» является конструктором значений. Мы должны сделать Green как тип, то, как показано ниже:

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]