[Haskell-cafe] Compiler's bane

[Jonathan Cast]

On Fri, 2008-08-29 at 21:48 +0100, Conor McBride wrote:
> 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.

OK.  If you have any of

1) Dynamic typing, as implemented in say Scheme, or
2) Unlimited recursion, as implemented in say Haskell, or
3) Unlimited recursive data types, as implemented in say Haskell

your language is Turing-complete.

> 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.

OK.  There are intermediate cases that involve some suitably restricted
form of recursion.  I don't actually know anything about them, so I
won't comment on the suitability of such restrictions for Andrew's
interpreter.  But I should have remembered their existence.

jcc