[Haskell-cafe] Termination of substitution
stefanor at cox.net
Wed Mar 12 17:37:35 EDT 2008
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).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080312/1cf9bc32/attachment.bin
More information about the Haskell-Cafe