Yitzchak Gale gale at sefer.org
Thu Jan 25 08:44:58 EST 2007

```I wrote:
>> 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
(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