Languages I have had to invoke Greenspun's tenth rule on

[maradydd]

• C
• Lua

Comments

[kragen.livejournal.com]

Hindley-Milner type inference is decidable and therefore can't do anything interesting.

[maradydd.livejournal.com]

Say what? You can do a lot of interesting things with decidable languages. Sure, you can't do everything, but there's a lot you can express with linear-bounded automata.

[mentalguy.livejournal.com]

For that matter, with common Haskell extensions, type inference isn't strictly decidable either.

[kragen.livejournal.com]

When I posted that comment I thought someone might respond this way.

The extent to which HM type inference falls short of Turing-completeness is a bigger difference between it and Prolog than almost any other conceivable language feature. I'm pretty sure you can't emulate an LBA with HM type inference. You can't emulate a PDA or even a DPDA, as far as I know. You don't even have definite iteration (for i = 1 to 10).

I'd be on pretty shaky ground saying you can't emulate a FSM with HM type inference, but I also don't see how to do it.

[maradydd.livejournal.com]

This is the part where my knowledge of type systems falls down, and where I'd go dig out my copy of Pierce's Types and Programming Languages if I knew which box it was in, because I know Pierce gets into the decidability of the simply typed lambda calculus and what you can do with it, but I don't remember much of that chapter. It's one of those books I need to read five or six times before I really understand it.