On Wed, Apr 04, 2007 at 02:57:06PM -0700, Dan Weston wrote: > What is it called if it's both? Is this even legal in Haskell? It seems > as though this would not be a grounded type, going on forever in both > directions.
I guess "negative datatype" is being a bit loose with terminology; the function constructor (->) has a negative (also called contravariant) and a positive (covariant) argument; I used "negative datatype" to mean a datatype that has a negative occurence of the data type being defined. It is perfectly valid Haskell and can be quite useful, for instance to define streams, or higher order abstract syntax (HOAS) - but it does have some strange properties, not the least of which is that it gives you recursion :) For that reason, Coq for example forbids negative occurences (because all functions must terminate); this is known as the positivity condition. I don't know which terminology (positive/negative, contravariant/covariant) is more common; I guess it depends on the community. Note that even in a definition where the type being defined is used in both the negative and the positive location, there are perfectly valid and terminating terms of that type: data Foo = Foo (Foo -> Foo ) Here is an instance of Foo: Foo id Edsko _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
