29 Aug
2008
29 Aug
'08
8:48 p.m.
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