Читая Джо Уэллса

[deniok]

Знаете ли вы, чем замечателен этот λ-терм?

λv.(λy.λz.v(yy)(yz))(λx.(λa.λb.a)x(x(xv)v))(λw.ww)

Он нормализуем, его нормальная форма

λv.v(λx.x)(λw.ww)

Более того он нормализуем сильно, то есть независимо от редукционной стратегии. Однако ему нельзя приписать никакого типа, даже в полной версии System F.

Первый такой терм придумали P. Giannini, F. Honsell и S. Ronchi Della Rocca из Миланского университета в 1987 году. А этот я взял из статьи J. B. Wells, Typability and Type Checking in System F Are Equivalent and Undecidable (1998).

Comments

[deni-ok.livejournal.com]

Уже в анализе v(yy)(yz) вижу сужение возможностей. Если тип y полиморфный, то типы аргументов v могут и не совпадать:

> :set -XRankNTypes
> :set -XScopedTypeVariables
> :t \v (y :: forall a. a -> a) z -> v (y y) (y z)
\v (y :: forall a. a -> a) z -> v (y y) (y z)
  :: ((a -> a) -> a1 -> t) -> (forall a2. a2 -> a2) -> a1 -> t

[kodt-rsdn.livejournal.com]

Почему y :: forall a.a->a, а не forall a.a->b?
Он же может что угодно вернуть.

[deni-ok.livejournal.com]

Тогда уж forall a b. a -> b

[kodt-rsdn.livejournal.com]

Ненене. forall a b означает, что на входе чёрте-что и на выходе такая же непредсказуемая фигня. Причём эта фигня зависит даже не от типа аргумента, а от его значений, то есть, динамика в полный рост.

forall a . a -> b - функция всеядная (void*, если по-сишному), а на выходе что-то определённое.
Что именно определённое - это предстоит решить выводителю типов...

[deni-ok.livejournal.com]

Это уже какое-то ограничение на System F. В ней можно и так, и сяк пробовать - важно, чтобы в результате типизации всех подтермов вышли согласованными по аппликациям.

[kodt-rsdn.livejournal.com]

Попробовать-то можно, просто зачем заранее пессимизировать?