[Haskell-cafe] Re: Problems with strictness analysis?

[Claus Reinke]

> Haskell's great strength is its equational semantics.  I would like
> Haskell programmers to think equationally, mathematically, rather than
> operationally, when writing Haskell programs.  If I were to teach a
> course in Haskell, I would like to launch off of denotational
> semantics, hopefully without ever having to say "lazy evaluation".
> (It's a pipe dream, of course, but you get the idea)
> 
> However, this strength is also a weakness when we want to analyze the
> efficiency of programs.  The denotational semantics of Haskell say
> nothing about time or space complexity, and give us no tools to reason
> about it.  A Haskell interpreter which randomly rewrites terms until
> it happens upon a normal form is considered correct (or rather,
> "correct with probability 1" :-).
> 
> How can we support analysis of time and space complexity without
> expanding ourselves into the complicated dirty world of operational
> thinking?

    equational /= denotational
    operational /= bad

Sometimes, denotational is too abstract, offering no guidelines on behaviour, 
just as abstract machine based operational thinking is too concrete, hiding
the insights in a flood of details. Sometimes, operational semantics based 
on directed equations give you the best of both worlds: equational reasoning 
and behavioural guidelines, both at a suitably "clean" and abstract level.

Claus