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

Теоретически: изоморфизм Карри-Ховарда дает нам интерпретацию этого типа как «ложного» предложения. «ложь» полезно как предложение само по себе; но также полезен для построения комбинатора «не» (как 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, и можем оставить другие ветви отключенными во время сопоставления шаблонов и т. д.

Среди соответствующих логическим false (как указано в другом ответе) они часто используются для создания дополнительных ограничений типа в сочетании с 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. где пример подробно описан.

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

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

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

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