Mike,

For those of us who aren't type theorists: What's a "negative datatype"?

A type that has a recursive call in negative position. Negative positions are the argument positions in function types. (But if a function type appears in a negative position, then its own argument position is denoted positive and its result position negative.) Cheers, Stefan