[Haskell] Fixpoint combinator without recursion

[Edsko de Vries]

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