[TYPES] a naive question on datatype declarations

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

In typical treatments of languages with recursive types, we present a
syntax with either isorecursive or equirecursive types. But we do not
have a syntax for introduction of type declarations.

This is to say that we assemble types out of constructors for e.g.,
polymorphism, recursion, sum, product, unit, exponential (give or
take).

But we do not have the equivalent of a "data" declaration in Haskell
that lets us explicitly say

data Bool = True | False

or

data List a = Nil | Cons a

It is, I suppose, expected that readers of these papers can think
through how to translate any given data datatypes in languages with
explicit declaration into the underlying fixed type calculus.

However, I am curious if there is any reference for *explicit*
treatment of the syntax for datatype declarations and semantic
modeling of such?

One reason for such would be that in the calculi I described above,
there's of course no way to distinguish between the above `data Bool`
and e.g. `1 + 1`, while it might be desirable to maintain that strict
distinction between actual equality and merely observable isomorphism.

Thanks,
Gershom