[Haskell-cafe] Compiler's bane
jonathanccast at fastmail.fm
Fri Aug 29 16:49:59 EDT 2008
On Fri, 2008-08-29 at 21:48 +0100, Conor McBride wrote:
> 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.
More information about the Haskell-Cafe