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

Есть ли в 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

Я могу попытаться реализовать ИЛИ, используя классы типов:

{-# 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], если не указано иное.

type-constraints haskell

rampion 22.08.2013 источник

Ответы (2)

arrow_upward
4
arrow_downward

К сожалению, я не могу придумать способ буквальной реализации или для Constraints, но если мы просто объединяем равенства или, как в вашем примере, мы можем оживить ваш подход к классу типов и сделать его закрытым с семействами типов и поднятые логические значения. Это будет работать только в 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 не может этого понять. Честно говоря, я не могу себе представить какое-либо решение, дающее вам эти свойства, хотя я всегда готов удивляться. Другая очевидная проблема с этим решением заключается в том, насколько оно длинное — вам нужно определить все восемь цветовых вариантов для каждого семейства типов IsXYZColor! (Использование совершенно нового семейства типов для каждого также раздражает, но неизбежно с решениями этой формы.)

Я упоминал выше, что GHC 7.8 сделает это лучше; он сделает это, избавив от необходимости перечислять каждый отдельный случай для каждого отдельного класса IsXYZColor. Как? Итак, Ричард Айзенберг и др. представил семейства закрытых перекрывающихся упорядоченных типов в GHC HEAD, и он будет доступен в версии 7.8. Существует документ, представленный на рассмотрение POPL 2014 (и расширенную версию) по теме, и Ричард также написал вводный пост в блоге (который, похоже, имеет устаревший синтаксис).

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

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

Ура, мы можем читать это, не засыпая от скуки! Фактически, вы заметите, что я переключился на явную версию 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

Antal Spector-Zabusky 22.08.2013

arrow_upward
0
arrow_downward

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

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]

Ankur 22.08.2013

comment

Вы видели добрую функцию продвижения GHC 7.4+< /а>? Это позволяет рассматривать типы как виды, а значения как типы. С -XDataKinds Green является вполне корректной вещью типа Color на уровне типов. Это делает программирование на уровне типов более безопасным по типам (поскольку у вас есть закодированные вещи, Fruit Int хорошо подходит) и устраняет необходимость определять ложные data Green = Green типы. - Antal Spector-Zabusky; 23.08.2013

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

Ответы (2)

Похожие вопросы