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

[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

[migmit.livejournal.com]

Так вот зачем нужна динамическая типизация...

[kodt-rsdn.livejournal.com]

А там нельзя налепить что-то с горой forall'ов?

Поскольку есть yy, то
y :: forall y1 . y1 -> y2
Поэтому и yy, и yz :: y2

ww
w :: forall w1 . w1 -> w2
ww :: w2

x xv v
x :: forall x1 . x1 -> v -> x3

Ну и так далее

[deni-ok.livejournal.com]

Вот это как раз тот случай, когда нельзя. Потом же нужно решить систему на типовые переменные (унифицировать их). А тут она окажется неразрешимой.

[kodt-rsdn.livejournal.com]

Я, всё-таки, чего-то не понимаю.
Из терма мы можем извлечь информацию об арности каждой переменной.

ww - понятно, что арность w ≥1, и первый аргумент рекурсивного типа (избавляемся от рекурсии, заявляя, что там forall)
обозначим это, для краткости, звёздочкой, как с кайндами:
w :: * → wr (w-result)
ww :: wr

v yy yz - арность v ≥2, арность y ≥1 и первый аргумент рекурсивный:
y :: * → yr
yy :: yr
yz :: yr
v :: yr → yr → vr
v(yy)(yz) :: vr

\a.\b.a :: a → b → a — старый добрый const

x xv v — арность x ≥2,
x :: * → v → xr
xv :: v → xr
x xv v :: xr

const x (x xv v)
:t a = :t x
:t b = :t x xv v
обозначим тип результата :t сr = :t x = * → v → vr

(v yy yz) (\x.const...) (\w.ww)
:t vr = (* → v → vr) → (* → wr)

:t v = yr → yr → ((* → v → vr) → (* → wr))
возникла рекурсия более затейливого вида, а мы возьмём да и изведём её через forall:
:t v = yr → yr → (* → * → vr) → * → wr

чтобы в звёздочках не путаться, восстановим forall'ы
:t v = forall v. forall x. forall w. yr → yr → (x → v → vr) → w → wr

Что-то, чем больше стрелок, тем сильнее глаза разбегаются, и у меня сейчас нет сил додумать, что там в итоге получается...
ghci на мои жалкие попытки пишет что-то вида "y is rigid type..." (там, где идёт сопоставление с forall y.y)

Это и есть то самое место спотыкания системы F?

[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]

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

[deni-ok.livejournal.com]

Если говорить очень грубо, то здесь возникает система неравенств на типы, в отличие от обычного Хиндли-Милнера, где мы имеем дело с системой уравнений. В последнем случае мы дальше делаем унификацию по Робинсону и все чики. А для неравенств дело дрянь. Джо Уэллс показал, что эта задача с помощью специальной тета-редукции сводится к SUP (Semiunification Problem), которая неразрешима. То есть ручками, конечно, можно терм перебирать, но важно понимать, что, даже составив правильную систему неравенств, мы не имеем универсального механизма решения.

[kodt-rsdn.livejournal.com]

Но мы ведь можем в любой момент спрыгнуть до галимой динамики.
Сказать: "чёрт его знает, что там за точный тип, но, как минимум, forall a b . a-> b на самом верхнем уровне".
Или сам момент принятия решения "пора валить" не определён, и получается, как с шампунем: намылить-смыть-повторить?

[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: левый аппликанд имеет тип (∀α.α)→(∀β.β), а правый - несовместимый никоим образом ∀α.α→α.