[Haskell-cafe] Compiler's bane

[Conor McBride]

Hi

On 29 Aug 2008, at 21:12, Jonathan Cast wrote:

>
> If you want to avoid infinite normal forms (or just plain lack of  
> normal
> forms, as in let x = x in x or (\x -> x x) (\ x -> x x)), you need to
> follow three rules:
>
> 1) Static typing

With you there.

> 2) No value recursion

Mostly with you: might allow productive corecursion
computing only on demand.

> 3) If you allow data types, no recursive data types

I can think of a few Turing incomplete languages with
(co)recursive data types, so

> Otherwise, your language will be Turing-complete,

seems suspect to me.

It's quite possible to identify a total fragment of
Haskell, eg, by seeing which of your Haskell programs
compile in Agda.

Things aren't as hopeless as you suggest.

Cheers

Conor