infinite types

[Ross Paterson]

On Wed, Jul 16, 2003 at 02:01:36PM +0200, blaat blaat wrote:
> Sorry if this mail starts a new thread. I am not subscribed to haskell-cafe 
> and am new to hotmail.
> 
> Uhm, as far as the example goes. I was trying to define a small (shallow 
> encoding of) a reactive systems language. Because I wanted to try something 
> else than monads I defined the following recursive type for a reactive 
> system.
> 
>  type R m = m -> Maybe (R m, [m])

I don't think there's an extension of Haskell with regular type
unification.  It's certainly possible, but there's an equivalent in
standard Haskell:

   newtype R m = MkR (m -> Maybe (R m, [m]))

except for the nuisance of adding and removing the MkR constructor.  Also,
regular type trees would make type errors more hairy, and in Haskell one
tends to write a lot of data's and newtype's anyway in order to define
class instances.

So co-algebraic programs are nothing special in Haskell, if you ignore
that constructor.

> A version for a ?Meally? machine embedding (always take an incoming 
> message, and respond with one outgoing message) could be written as
> 
> type Meally i o = i -> (Meally i o, o)

This particular example is an instance of an arrow type, and is handy
for simulating synchronous circuits, cf

	http://www.soi.city.ac.uk/~ross/papers/fop.html
	(look for "Simple automata" on the 3rd page)

A more bizarre example is "hyperfunctions":

  newtype Hyper i o = Hyper (i -> Hyper o i)

cf http://www.cse.ogi.edu/~krstic/psfiles/hyperfunctions.ps