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

[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

[kodt-rsdn.livejournal.com]

Про ручки - такой ещё момент.
Вот у нас есть куча переменных.
Каждой из них мы можем присвоить тип forall a.a или не присвоить, и посмотреть, как решатель будет выкручиваться.

Поскольку количество переменных конечно, то у нас есть 2ⁿ вариантов.
Какие-то из этих вариантов (v :: forall a . a) являются решениями-ловушками, оценкой снизу.

Остаётся только выбрать, что из всего этого подходит нам лучше всего.
Например, по количеству вынужденно задействованных кванторов. Чем меньше (или: чем глубже от корня), тем лучше.
Могут ли при этом возникать равнозначные варианты, между которыми мы просто не можем сделать выбор? Ну, скажем, forall a . a -> b и forall b . a -> b, при том, что xz -> yt у нас не получился.

Можно ли такое пространство равнозначных вариантов объединить в один надтип?
Я понимаю, что это, в любом случае, комбинаторный взрыв. Но, чисто теоретически, не?

(Извини, если задаю ламерские вопросы: в недра лямбда-куба не вкурил)

[deni-ok.livejournal.com]

> Каждой из них мы можем присвоить тип forall a.a

нет, не можем:

> let good = (\(y::forall a.a->a)->y y) (\x->x)
> :t good
good :: a -> a
> let bad  = (\(y::forall a.a   )->y y) (\x->x)

Второе не выводится в системе F: левый аппликанд имеет тип (∀α.α)→(∀β.β), а правый - несовместимый никоим образом ∀α.α→α.