G'day all.
Quoting David Menendez
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.