[Haskell-cafe] Termination of substitution

[Stefan O'Rear]

On Wed, Mar 12, 2008 at 02:30:41PM -0700, Taral wrote:
> On 3/12/08, Neil Mitchell <ndmitchell at gmail.com> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080312/1cf9bc32/attachment.bin