Классы экзистенциальных типов против конструкторов данных и копроизведений

Question

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

Я надеюсь, что кто-то может указать мне на лучший способ выполнить то, что я пытаюсь сделать. Позвольте мне начать с простого примера. Я моделирую систему тестирования, где вы можете иметь вложенные наборы тестов, которые в конечном итоге заканчиваются тестами. Итак, как то так:

data Node =
    Test { source::string }
    Suite { title::string, children::[Node] }

Итак, пока довольно просто, по сути, причудливое объявление Tree/Leaf. Тем не менее, я быстро понимаю, что хочу создавать функции, специально предназначенные для тестов. Поэтому я сейчас разделю это так:

data Test = Test { source::string }
data Suite = Suite { title::string, children::[Either Test Suite] }

В качестве альтернативы я мог бы бросить "пользовательский" Либо (особенно, если пример более сложный и имеет более 2 вариантов), скажем что-то вроде:

data Node =
   fromTest Test
   fromSuite Suite

Итак, уже довольно прискорбно, что просто иметь возможность Suite которые могут иметь комбинацию наборов или тестов, я в конечном итоге странные накладные расходы Either класс (будь то с фактическим Either или заказной). Если бы я использовал классы экзистенциальных типов, я мог бы сделать Test а также Suite получить "Node_", а затем иметь Suite свой список сказал Nodes. Копродукция позволила бы нечто подобное, где я бы сделал то же самое Either стратегия без многословия тегов.

Позвольте мне теперь расширить более сложный пример. Результаты тестов могут быть Пропущены (тест был отключен), Успешно, Сбой или Пропущен (тест или набор не могли быть выполнены из-за предыдущего сбоя). Опять же, я изначально начал с чего-то вроде этого:

data Result = Success | Omitted | Failure | Skipped
data ResultTree =
    Tree { children::[ResultTree], result::Result } |
    Leaf Result

Но я быстро понял, что хочу иметь возможность писать функции, которые приносят конкретные результаты, и, что более важно, иметь сам тип, обеспечивающий свойства владения: успешный набор должен иметь только дочерние элементы типа "Успешный" или "Пропущенный", дочерние элементы Failure могут быть чем угодно, "только пропущенный" Собственный опущен и т. д. Итак, теперь я получаю что-то вроде этого:

data Success = Success { children::[Either Success Skipped] }
data Failure = Failure { children::[AnyResult] }
data Omitted = Omitted { children::[Omitted] }
data Skipped = Skipped { children::[Skipped] }
data AnyResult =
  fromSuccess Success |
  fromFailure Failure |
  fromOmitted Omitted |
  fromSkipped Skipped

Опять же, теперь у меня есть такие странные типы "Wrapper", как AnyResult, но я получаю принудительное приведение типа чего-то, что раньше применялось только во время выполнения. Есть ли лучшая стратегия для этого, которая не включает в себя такие функции, как классы экзистенциальных типов?

Answer 1

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

Они позволяют принимать только некоторые значения из типа в качестве входных данных и делают эти ограничения проверкой / ошибкой во время компиляции.

Вот видео из выступления на HaskellX 2018, в котором рассказывается о LiquidHaskell, который позволяет использовать типы уточнений в Haskell:

https://skillsmatter.com/skillscasts/11068-keynote-looking-forward-to-niki-vazou-s-keynote-at-haskellx-2018

Вы должны украсить свою подпись функции haskell и установить LiquidHaskell:

f :: Int -> i : Int {i | i < 3} -> Int будет функция, которая может принимать только в качестве второго параметра Int со значением < 3, проверено во время компиляции.

Вы могли бы также наложить ограничения на ваш Result тип.

Answer 2

Я думаю, что вы можете искать это GADTs с DataKinds, Это позволяет уточнить типы каждого конструктора в типе данных до определенного набора возможных значений. Например:

data TestType = Test | Suite

data Node (t :: TestType) where
  TestNode :: { source :: String } -> Node 'Test
  SuiteNode :: { title :: String, children :: [SomeNode] } -> Node 'Suite

data SomeNode where
  SomeNode :: Node t -> SomeNode

Тогда, когда функция работает только на тестах, она может занять Node 'Test; на люксы, Node 'Suite; и на любой, полиморфный Node a, Когда сопоставление с образцом на Node a каждый case ветвь получает доступ к ограничению равенства:

useNode :: Node a -> Foo
useNode node = case node of
  TestNode source ->          {- here it’s known that (a ~ 'Test) -}
  SuiteNode title children -> {- here, (a ~ 'Suite) -}

Действительно, если вы взяли конкретный Node 'Test, SuiteNode компилятор запретил бы переход, так как он никогда не может совпадать.

SomeNode это экзистенция, которая оборачивает Node неизвестного типа; Вы можете добавить дополнительные ограничения класса, если хотите.

Вы можете сделать то же самое с Result:

data ResultType = Success | Omitted | Failure | Skipped

data Result (t :: ResultType) where
  SuccessResult
    :: [Either (Result 'Success) (Result 'Skipped)]
    -> Result 'Success
  FailureResult
    :: [SomeResult]
    -> Result 'Failure
  OmittedResult
    :: [Result 'Omitted]
    -> Result 'Omitted
  SkippedResult
    :: [Result 'Skipped]
    -> Result 'Skipped

data SomeResult where
  SomeResult :: Result t -> SomeResult

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

Чтобы работать с динамическими результатами, вам может потребоваться доказать компилятору, что два типа равны; для этого я направляю вас Data.Type.Equality, который обеспечивает тип a :~: b который населяется одним конструктором Refl когда два типа a а также b равны; Вы можете сопоставить это с шаблоном, чтобы сообщить проверщику типов о равенстве типов, или использовать различные комбинаторы для выполнения более сложных доказательств.

Также полезно в сочетании с GADTs (а также ExistentialTypes, менее обычно) RankNTypes, что в основном позволяет передавать полиморфные функции в качестве аргументов другим функциям; это необходимо, если вы хотите использовать экзистенциал в общем:

consumeResult :: SomeResult -> (forall t. Result t -> r) -> r
consumeResult (SomeResult res) k = k res

Это пример стиля прохождения продолжения (CPS), где k это продолжение.

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