[Haskell-cafe] Basic question concerning data constructors

[ajb at spamcop.net]

G'day all.

Quoting David Menendez <dave at zednenem.com>:

>    data A = B
>
> means that "B" constructs a value of type "A". The "=" acts more like the
> "::=" in a BNF grammar.

And, indeed, that was the syntax for it in Miranda.

> It is *not* a claim that A equals B, since A is a
> type and B is a data constructor.

Wrong.  It _is_ a claim that A equals B.  Or, rather, that the set of
values[*] A is defined as the least-fixpoint solution of the equation
A = B.

Think of this:

data IntList = Nil | Cons Int IntList

This corresponds to an equation:

IntList = { Nil } + { Cons } * Int * IntLIst

where plus denotes union (or disjoint union; either works in this
case) and star denotes Cartesian product.

The least fixpoint of this equation is precisely the set of values[*]
in IntList.

> Furthermore, types and data constructors
> have disjoint namespaces, hence the common idiom of using the same name for
> the type and the constructor when the type has only one constructor.

I think that's the major source of the confusion here, yes.

Cheers,
Andrew Bromage

[*] Theoretical nit: It's not technically a "set".

Consider the data type:

     data Foo = Foo (Foo -> Bool)

This declaration states that there's a bijection between the elements of
Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot
be true for any set.  That's because we only allow computable functions,
and Foo -> Bool is actually an exponential object in the category Hask.