Какое значение имеют алгебраические типы данных с нулевыми конструкторами?

Question

Этот отрывок, к сожалению, не имеющий ссылок, о разработке ADT в Haskell, из "Истории Haskell: быть ленивым с классом", раздел 5.1:

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

меня удивляет, насколько такой ADT будет полезен?

Answer 1

Теоретически: изоморфизм Карри-Говарда дает нам интерпретацию этого типа как "ложного" предложения. "ложь" полезна как само по себе предложение; но также полезно для построения комбинатора "не" (как type Not a = a -> False) и другие подобные конструкции.

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

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

Это приводит к тому, что при анализе дерева игр Lines of Action, если указан набор правил, мы знаем, что его конструктор будет Unknownи может оставить другие ветви во время сопоставления с образцом и т. д.

Answer 2

Среди соответствующих логическому ложному (как указано в другом ответе) они часто используются для создания дополнительных ограничений типа в сочетании с GADT. Например:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.List (groupBy)

data Zero
data Succ n

data Vec n a where
    Nil  ::                 Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

vhead :: Vec (Succ n) a -> a
vhead (Cons v _) = v

vtail :: Vec (Succ n) a -> Vec n a
vtail (Cons _ v) = v

Здесь у нас есть два таких типа данных без конструктора. Их значение здесь просто для представления натуральных чисел: Zero, Succ Zero, Succ (Succ Zero) и т.д. Они используются в качестве фантомных типов в Vec тип данных, чтобы мы могли кодировать длину вектора в его типе. Затем мы можем написать безопасные для типов функции, такие как vhead/vtail это может быть применено только к непустым векторам.

См. Также [Haskell] Векторы фиксированной длины в Haskell: Часть 1. Использование GADT, где пример детально проработан.

Answer 3

Нет никакого способа построить "реальное" значение типа без конструктора (где под "реальным" я подразумеваю завершающее вычисление; Haskell имеет undefined :: a, error :: String -> a и возможность написания таких программ mwahaha = mwahaha что упрощенно я назову "поддельными" значениями).

Одним из примеров того, как это может быть полезно, являются версии 0.5 и более поздние библиотеки каналов. Основной тип в библиотеке Pipe l i o u m r; с разными параметрами для этих типов, Pipe может служить либо источником (который производит вывод без потребления какого-либо ввода), потребителем (потребляет ввод без производства какого-либо вывода) или каналом (потребляет ввод и производит вывод). i а также o введите параметры для Pipe типы его ввода и вывода соответственно.

Таким образом, один из способов, которым библиотека проводников реализует представление о том, что источники не потребляют ввод, а приемники не производят вывод при использовании Void введите от Data.Void в качестве типа ввода для источников и типа вывода для приемников. Опять же, не существует завершающего способа для создания значения такого типа, поэтому программа, которая пытается использовать вывод из приемника, не завершит работу (что в качестве напоминания в Haskell может означать "выдавать ошибку" и не обязательно " петля навсегда ").

Answer 4

Типы без конструкторов называются фантомными типами. Смотрите страницу в вики Haskell.