Союзы DataKind - PullRequest
Новая
       78

Союзы DataKind

0 голосов
/ 16 февраля 2019

Я не уверен, что это правильная терминология, но возможно ли объявить типы функций, которые принимают «объединение» типов данных?

Например, я знаю, что могу сделать следующее:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}

...

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Shape Circle' -> Int
test1 = undefined

Однако, что если я захочу принять форму, которая является либо кругом, либо квадратом?Что, если я также хочу взять все фигуры для отдельной функции?

Есть ли способ для меня определить набор Shape' видов для использования или способ разрешить несколько определений типа данныхна данные?

Редактировать:

Использование союзов, похоже, не работает: 

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

...

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 Circle {} = undefined
test1 Triangle {} = undefined
test1 Square {} = undefined

Часть выше компилируется

Ответы [ 4 ]

0 голосов
/ 17 февраля 2019

Еще одно решение, которое я заметил, хотя и довольно многословное, - это создать вид, содержащий список логических функций.Затем вы можете сопоставить шаблон с функциями при ограничении типа: 

-- [circleOrSquare] [triangleOrSquare]
data Shape' =
  Shape'' Bool
          Bool

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape (Shape'' True False)
  Square :: { side :: Int} -> Shape (Shape'' True True)
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape (Shape'' False True)

test1 :: Shape (Shape'' True x) -> Int
test1 Circle {}   = 2
test1 Square {}   = 2
test1 Triangle {} = 2

Здесь треугольник не будет соответствовать: 

    • Couldn't match type ‘'True’ with ‘'False’
      Inaccessible code in
        a pattern with constructor:
          Triangle :: Int -> Int -> Int -> Shape ('Shape'' 'False 'True),
        in an equation for ‘test1’
    • In the pattern: Triangle {}
      In an equation for ‘test1’: test1 Triangle {} = 2
   |
52 | test1 Triangle {} = 2
   |       ^^^^^^^^^^^

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

Это может быть использовано в сочетании с примерами классов для удобства чтения.

0 голосов
/ 16 февраля 2019

Это становится ужасно, но я думаю, вам может потребоваться доказательство того, что это либо круг, либо квадрат, используя Data.Type.Equality: 

test1 :: Either (s :~: Circle') (s :~: Square') -> Shape s -> Int

Теперь у пользователя естьдать дополнительный аргумент («доказательный термин»), говорящий, какой это.

Фактически вы можете использовать идею проверочного термина для «завершения» решения Брэдма с помощью: 

class MyOpClass sh where
    myOp :: Shape sh -> Int
    shapeConstraint :: Either (sh :~: Circle') (sh :~: Square')

Теперь никто не может добавлять дополнительные экземпляры (если они не используют undefined, что было бы невежливо).

0 голосов
/ 16 февраля 2019

Вы можете сделать что-то подобное в (я думаю) достаточно чистом способе, используя семейство типов вместе с ConstraintKinds и PolyKinds: 

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 = undefined

Выше () является пустым ограничением(это похоже на пустой «список» ограничений класса типов).

В первом «уравнении» семейства типов используется нелинейное сопоставление с образцом, доступное в семействах типов (дважды слева используется x)со стороны).Семейство типов также использует тот факт, что, если ни один из случаев не совпадает, оно не даст вам действительного ограничения.

Вы также сможете использовать логический тип уровня вместо ConstraintKinds.Это было бы немного более громоздко, и я думаю, что было бы лучше избегать здесь использования логического уровня на уровне типов (если вы можете).

Примечание (я никогда не могу вспомнить это, и мне пришлось посмотреть его)на этот ответ): вы получаете Constraint в области видимости, импортируя его из GHC.Exts.

Редактировать: Частичное запрещение недоступных определений

Вот модификация, чтобы получить его (частично) запрещать недостижимые определения, а также недействительные вызовы.Это немного более круговое движение, но, похоже, это работает.

Измените Union, чтобы получить * вместо ограничения, например: 

type family Union (a :: [k]) (r :: k) :: * where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

Это не имеет значенияслишком много, что это за тип, если у него есть обитатель, с которым вы можете сопоставить образец, поэтому я возвращаю тип () (тип устройства).

Вот как вы его используете: 

test1 :: Shape s -> Union [Circle', Triangle'] s -> Int
test1 Circle {}   () = undefined
test1 Triangle {} () = undefined
-- test1 Square {} () = undefined -- This line won't compile

Если вы забыли сопоставить его (например, если вместо конструктора () вместо имени сопоставить имя переменной, например, x), возможно, будет определен недостижимый случай.Тем не менее, он все равно выдаст ошибку типа на сайте вызова, когда вы на самом деле попытаетесь достичь этого случая (поэтому, даже если вы не соответствуете аргументу Union, вызов test1 (Square undefined) () не будет проверять тип).

Обратите внимание, что, по-видимому, аргумент Union должен идти после аргумента Shape, чтобы это работало (в любом случае полностью, как описано).

0 голосов
/ 16 февраля 2019

Вы можете использовать классы типов: 

class MyOpClass sh where
    myOp :: Shape sh -> Int

instance MyOpClass Circle' where
    myOp (Circle r) = _

instance MyOpClass Square' where
    myOP (Square s) = _

Это не кажется мне особенно «полным» решением - любой может вернуться и добавить еще один instance MyOpClass Triangle' - но я не могу вспомнитьлюбое другое решение.Потенциально вы можете избежать этой проблемы, просто не экспортировав класс типов.

...