Frank Christoph writes: > >>>>> "Stefan" == Stefan Kahrs <[EMAIL PROTECTED]> writes: > > In a certain sense you have No. 4 already: it's called newtype. Newtypes > > can be recursive. Syntactically the constructors are still there, but > > that's only to help the type inference. > > As I understand it, the purpose of newtype is to cut down on unnecessary > performance overhead when all you want to do is make a type > abstract. Never mind what its originally intended purpose was... it _is_ just a datatype with a single constructor that has an implicit strictness attribute. > As for recursive "newtype": Really? That's news to me. "newtype" > definitions only have one constructor, so any recursive definition would be an > infinite datatype. Since a newtype constructor is unlifted, this would make > recursive newtypes pretty useless. I think Lennart sorted this out :-). The point is that recursive newtype + coproducts (e.g. the predefined Either) give us [the power of] full-blown recursive datatypes, including non-regular ones. Moreover, in type-theoretic investigations of recursive types people often keep this distinction between coproducts and recursion, because it allows to investigate both concepts separately. Typically, recursive types appear with a "fold" and an "unfold" operation, and these correspond to the application/matching of the single constructor of a newtype. See for example the paper "Functorial ML" by Belle, Jay & Moggi at last years PLILP, LNCS 1140 (there they are called "intro" and "fold"). Stefan Kahrs
