[Haskell-cafe] Termination of substitution

[Stefan O'Rear]

On Wed, Mar 12, 2008 at 09:05:03PM +0000, Neil Mitchell wrote:
> Hi
> 
> I'm trying to show that a system of rules for manipulating Haskell
> expressions is terminating. The rules can be applied in any order, to
> any subexpression - and there is a problem if there is any possible
> infinite sequence.
> 
> The rule that is giving me particular problems is:
> 
> (\v -> x) y   =>   x[v/y]
> 
> (I realise this rule may duplicate the computation of y, but that is
> not relevant for this purpose.)
> 
> In particular, given the expression
> 
> (\x -> x x) (\x -> x x)
> 
> we can keep applying this rule infinitely.
> 
> However, I don't believe this expression is type safe in Haskell. Are
> any such expressions that would cause this to non-terminate not type
> safe?

I think you mean all, and the answer is "no, but".  (Very interesting
topic here, for me at least.)

Haskell's core type system (let, lambda, and application) can be mapped
into the simply-typed lambda calculus by macro-expanding lets, and (by
the construction of the Hindley-Milner type system) this mapping is
typability-preserving.  The simply-typed lambda calculus is not only
terminating, it is strongly normalizing - ALL possible reduction
sequences stop eventually.   (There is a very elegant proof of this).

The addition of data types in full generality breaks this:

newtype Curry o = Curry { unCurry :: Curry o -> o }

loop :: o
loop = (\c -> unCurry c c) (Curry (\c -> unCurry c c))

Systems like Coq, which need to preserve strong normalization for
logical soundness, adopt a variety of syntactic restrictions.  Coq
specifically forbids contravariant recursion in types.


> What are the necessary conditions for this to be safe? Does GHC
> perform lambda reduction, probably by introducing a let binding? Does
> the combination of reducing lambdas and creating let bindings give
> similar problems, particularly if bindings are inlined?

Yes.  If you feed that example into GHC, GHC will crash (even with the
optimizer off).  Works fine in Hugs/Yhc.

http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#bugs-ghc

> I'm wondering if this rule is genuinely unsafe in Haskell. If it is,
> why isn't it an issue in real simplifiers. If it isn't, what makes it
> safe.

Nobody but us logic fans actually writes encodings of Curry's Paradox.

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/54c14816/attachment.bin