[Haskell-cafe] IO is not a monad
gale at sefer.org
Thu Jan 25 08:44:58 EST 2007
>> 1. Find a way to model strictness/laziness properties
>> of Haskell functions in a category in a way that is
>> reasonably rich.
Duncan Coutts wrote:
> The reason it's not obvious for categories is because
> the semantics for Haskell comes from domain theory
>(CPOs etc) not categories.
The category we have been discussing seems to
do the trick quite easily for (1):
Let Empty be the empty type. Let undef = \x -> undefined,
and as before,
f .! g = f `seq` g `seq` (\x -> f (g x))
Then we can take HaskL - Haskell with Laziness - to be
the category Haskell types and Haskell functions
(including seq), with .! as composition. It is easy to
check that this is a category, using the left-monoid
laws for seq:
(x `seq` y) `seq` z = x `seq` (y `seq` z)
(x `seq` y) `seq` z = (y `seq` x) `seq` z
(\x -> expr) `seq` y = y
Empty is bi-universal in HaskL, with undef
the unique morphism in either direction. We
have undef .! f = undef for any three types and
any morphism f.
We say that a morphism f is strict iff f .! undef = undef.
We will only consider functors (F, fmap) on HaskL that are natural,
in the sense that fmap is a morphism from (A -> B) to
(F(A) -> F(B)) for all A, B. Similarly for return and
join with monads.
It is easy to show that a functor (F, fmap) preserves
strictness if fmap is strict as a morphism.
More information about the Haskell-Cafe