Могут ли все ограничения на данные быть представлены в виде алгебраических типов данных?

Могут ли все ограничения на данные и состояние быть представлены в виде алгебраических типов данных?

Мне нравится, как я часто могу выразить ограничения на систему в виде ADTs.

Т. е. все возможные значения АДТ являются возможными состояниями системы, нет места для несогласованности.

Всегда ли это так, или существуют ограничения, которые не могут быть представлены в виде ADTs?

(другими словами, когда я не могу представить набор ограничений в виде ADT, это просто не я глядя достаточно трудно, или некоторые типы ограничений просто неосуществимы с ADTs?)

Существуют ли математические доказательства этого?

Обновление:

Вот игрушечная проблема:

A (roguelike) 2D карта состоит из квадратных ячеек, каждая из которых имеет материал (камень или воздух). Каждая ячейка имеет четыре границы (N, S, E и W). Каждая граница разделяется двумя ячейками.

Граница может содержать "стеновой элемент" только в том случае, если одна сторона-камень, а другая-камень. воздух.

(настенные элементы могут быть рычагами, картинками, кнопками и т. д.)

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

1 2
haskell algebraic-data-types

1 ответ:

Это явно справедливо для системы с конечным числом состояний:

Состояние Данных = State1 / State2 | State3 | State4 | State5/...

Но как быть с системами с конечным числом состояний? Если мы ограничиваемся написанием конечных программ Хаскелла, то существует только счетное число программ Хаскелла и, следовательно, только счетное число ADT. Это потому, что Хаскелл-язык, написанный конечным алфавитом.

Рассмотрим следующий тип данных, поток биты: 

data Stream = O Stream | I Stream
Теперь давайте запишем некоторые случайные ограничения на потоки, которые могут быть представлены в виде типов данных Haskell. (Все они должны быть представлены в виде типов данных Haskell, или уже существует тип, который не может быть представлен ADT в конечной программе Haskell): 
Type 0 admits every stream except OIOIOIOO...
Type 1 admits every stream except IIOOOIOI...
Type 2 admits every stream except OOOIOIIO...
Type 3 admits every stream except OOOOIIIO...
Type 4 admits every stream except OOIOIOOO...
Type 5 admits every stream except OOIOOOIO...
Type 6 admits every stream except IIOIOIIO...
Type 7 admits every stream except IIIIIIIO...
...

Мы можем записать не более чем счетное число таких типов данных в Haskell, поскольку существует только счетное число конечных программ Haskell, и каждая конечная программа Haskell может экспортировать только конечное число типов, не имеющих переменной типа. Программы, которые экспортируют типы с переменными типа, могут быть интересными подпрограммами программы, которая создает типы, являющиеся ограниченными версиями Stream, но поскольку Stream не имеет переменной типа, все эти типы явно не являются ограниченными версиями Stream. Следовательно, если мы можем показать, что существует бесчисленное множество возможных типов данных, то должен существовать хотя бы один тип, который не может быть представлен Haskell ADTs именно так.

Давайте продолжим записывать типы данных, пока мы не запишем их все в бесконечный список всех типов данных, которые могут представлять конечные программы Хаскелла. Так как их только счетно много, их можно сопоставить с уникальными целыми положительными числами, чтобы записать их по порядку. Теперь рассмотрим следующий тип данных. Он допускает каждый поток, кроме потока, который начинается с противоположного бита, поскольку поток, который не допускается типом 0, имеет второй бит, который является напротив, как второй бит потока, который не допускается типом 1, и т. д.

Тип x допускает каждый поток, кроме IOIIOOI...

Это называется диагональю Кантора. 
Type x isn't Type 0, because it admits anything that starts with an O, and the only thing Type 0 excludes is one stream that starts with an O
Type x isn't type 1, because it admits anything that has a second bit of I, and the only thing Type 1 excludes is one stream that has a second but of I.
Type x isn't type 2, because it admits anything that has a third bit if O, and the only thing Type 2 excludes is one stream that has a third bit of O.
...
На самом деле, тип x не является ни одним из типов данных, которые мы записали, и мы записали каждый отдельный тип данных, например Stream, который может представлять конечная программа Хаскелла. Поэтому тип x не может быть представлен конечной программой Хаскелла.
4