Переменная Union в переменной типа GADT - PullRequest
Новая
       8

Переменная Union в переменной типа GADT

0 голосов
/ 28 апреля 2018

У меня есть конструктор GADT, представляющий ту же идею, но мне нужны два из них, потому что тип гибок в зависимости от контекста. Посмотрите этот надуманный пример: 

data A
data B
data C

data Thing a where
  AFoo :: String -> Thing A
  Bar  :: Float -> Thing A
  BFoo :: String -> Thing B
  Baz  :: Int -> Thing B
  Bah  :: Char -> Thing C

AFoo и BFoo представляют одну и ту же концепцию базовых данных: некоторые данные представлены строкой. Но в этом контексте это нечто большее. В идеале AFoo и BFoo должны быть объединены в Foo, потому что они представляют собой одно и то же, но мне нужен тот, который печатает как Thing A, и тот, который печатает как Thing B. Как упоминалось ранее, некоторые контексты, в которых может использоваться Foo, требуют Thing A, а некоторые требуют Thing B, поэтому для удовлетворения системы типов для каждого должен существовать один конструктор.

Конечно, я мог бы написать функцию, которая "приводит" к желаемому типу, переключая конструктор при необходимости: 

fooAsThingA :: Thing a -> Maybe (Thing A)
fooAsThingA t@(AFoo _) = Just t
fooAsThingA (BFoo s) = Just $ AFoo s
fooAsThingA _ = Nothing

(и аналогично для fooAsThingB)

Но это некрасиво, потому что это требует Maybe, что я должен размножать, потому что не все Thing B s могут стать Thing A s (на самом деле, только BFoo может).

В идеале я хотел бы написать: 

data A
data B
data C

data Thing a where
  Foo :: String -> Thing ??
  Bar :: Float -> Thing A
  Baz :: Int -> Thing B
  Bah :: Char -> Thing C

Но мне неясно, что бы я поставил вместо ??. Предположительно, это какой-то способ представления объединения A и B (и, возможно, для этого нужно изменить типы других конструкторов для этого GADT, но это нормально).

Просто для ясности, если бы вышеупомянутое было верным, я бы ожидал, учитывая следующие функции: 

processThingA :: Thing A -> String
processThingB :: Thing B -> Int
processThingC :: Thing C -> Float

Тогда я смогу сделать все следующее: 

processThingA $ Foo "Hello"
processThingB $ Foo "World"

processThingA $ Bar 3.14
processThingB $ Baz 42

processThingC $ Bah '\n'

tl; dr В первом фрагменте можно ли объединить AFoo и BFoo в Foo, который печатает как Thing A и Thing B?

edit: Примечание: есть другие EmptyDataDecls, чем A и B, которые я использую для Thing a. Я добавил C в качестве примера.

1 Ответ

0 голосов
/ 29 апреля 2018

Возможное решение заключается в следующем, даже я не считаю его элегантным.

Сначала мы определим GADT и класс типов для «A или B»: 

{-# LANGUAGE DataKinds, KindSignatures, GADTs, EmptyCase,
             ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

data Sort = A | B | C | D

data AorB (s :: Sort) where
  IsA :: AorB 'A
  IsB :: AorB 'B

class IsAorB (s :: Sort) where
  aorb :: AorB s

instance IsAorB 'A where aorb = IsA
instance IsAorB 'B where aorb = IsB

Затем мы используем наш тип в нашем типе. Это приведет к тому, что Foo потребуется больше места, так как ему нужно хранить словарь классов типов во время выполнения. Это небольшое количество накладных расходов, но это все еще неудачно. С другой стороны, это также позволит определить во время выполнения, действительно ли s, используемый в Foo, A или B. 

data Thing (s :: Sort) where
  Foo :: IsAorB s => String -> Thing s 
  Bar :: Float -> Thing 'A
  Baz :: Int -> Thing 'B
  Bah :: Char -> Thing 'C

Некоторые тесты: 

processThingA :: Thing 'A -> String
processThingA (Foo x) = x
processThingA (Bar x) = show x

processThingB :: Thing 'B -> Int
processThingB (Foo _) = 0
processThingB (Baz i) = i

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

-- This unfortunately will give a spurious warning
processThingC :: Thing 'C -> Float
processThingC (Bah _) = 42.2
-- To silence the warning we need to prove that this is indeed impossible
processThingC (Foo _) = case aorb :: AorB 'C of {}

processThingAorB :: forall s. IsAorB s => Thing s -> String
processThingAorB (Foo x) = x
processThingAorB (Bar x) = "Bar " ++ show x
processThingAorB (Baz x) = "Baz " ++ show x
-- Again, to silence the warnings
processThingAorB (Bah _) = case aorb :: AorB 'C of {}

test :: ()
test = ()
  where
  _ = processThingA $ Foo "Hello"
  _ = processThingB $ Foo "World"
  _ = processThingA $ Bar 3.14
  _ = processThingB $ Baz 42
  _ = processThingC $ Bah '\n'

Эта техника не очень хорошо масштабируется. Нам нужен собственный GADT и класс типов для любого конструктора Thing, который может генерировать любой тег в некотором «объединении». Это все еще может быть в порядке. Чтобы проверить полноту, нам нужно использовать все эти классы.

Я думаю, что это должно потребовать линейного количества шаблонов, но это все еще важно.

Возможно, в общем случае проще использовать синглтоны, чтобы сохранить значение s в конструкторе Foo и избежать всех пользовательских GADT и классов типов.

...