[Haskell-cafe] Compiler's bane

Conor McBride conor at strictlypositive.org
Fri Aug 29 16:48:03 EDT 2008


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.



More information about the Haskell-Cafe mailing list