Re: [Haskell-cafe] Termination of substitution

On Wed, Mar 12, 2008 at 02:30:41PM -0700, Taral wrote:

On 3/12/08, Neil Mitchell wrote:

...

However, I don't believe this expression is type safe in Haskell.

Using higher-order polymorphism:

f (x :: forall a. a -> a) = x x

Interestingly, this doesn't work - f is a self-application function, but it does not have a type that can be made to look like forall a. a -> a. Indeed, higher-order polymorphism as implemented in GHC can be implemented in System F-omega, a strongly normalizing calculus. (The usual datatype caveats apply). Stefan