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