Can all constraints on data be represented as Algebraic Data Types?

Question

Can all constraints on data and state be represented as Algebraic Data Types?

I love the way that I am often able to express the constraints on system as ADTs.

i.e. All possible values of the ADT are possible states of the system, there is no scope for inconsistency.

Is this always the case, or are there constraints which cannot be represented as ADTs?

(In other words, when I cannot represent a set of constraints as an ADT, is it just me not looking hard enough, or are some types of constraints just unenforceable with ADTs?)

Are there mathematical proofs of this?

---

Update:

Here's a toy problem:

A (roguelike) 2D map consists of square cells which each have a material (rock or air).

Each cell has four boundaries (N, S, E and W). Each boundary is shared by two cells.

A boundary can optionally contain a "wall feature" only if one side is rock and the other air.

(Wall features could be levers, pictures, buttons, etc.)

What ADT design could have a place to store a wall feature only when one side is rock and the other air? i.e. the data structure cannot represent a wall feature on a boundary between two air cells or two rock cells.

Answer 1

This is clearly true for a system with a finite number of states:

data State = State1 | State2 | State3 | State4 | State5 | ...

But what about systems with a non-finite number of states? If we limit ourselves to writing finite Haskell programs, then there are only countably many Haskell programs, and thus only countably many ADTs. This is because Haskell is a language written with a finite alphabet.

Consider the following data type, a stream of bits:

data Stream = O Stream | I Stream

Now let's start writing down some random constraints on streams that can be represented as Haskell data types. (All of these must be representable as Haskell data types, or there already exists a type that can't be represented by an ADT in a finite Haskell program):

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...
...

We can write down at most a countable number of such data types in Haskell, since there are only countably many finite Haskell programs, and each finite Haskell program can only export a finite number of types that don't have a type variable. The programs that do export types with type variables might be interesting sub programs of a program that creates types that are constrained versions of Stream, but since Stream doesn't have a type variable, all of those types clearly aren't constrained versions of Stream. Therefore, if we can show that there are uncountably many possible data types, then there must exist at least one type that Haskell ADTs can't represent exactly.

Let's keep writing down data types, until we have written them all down in an infinite list of all the data types finite Haskell programs can represent. Since there are only countably many of these, they can be mapped to unique positive integers to write them down in order.

Now, consider the following data type. It admits every stream except the stream that starts with the opposite bit as the stream that isn't admitted by Type 0, has a second bit that is the opposite as the second bit of the stream that isn't admitted by Type 1, etc.

Type x admits every stream except IOIIOIOI...

This is called Cantor's diagonal.

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.
...

In fact, Type x isn't any of the data types we wrote down, and we wrote down every single data type like Stream that a finite Haskell program can represent. Therefore Type x isn't representable by a finite Haskell program.