Спрашивали? Отвечаем!

[deni_ok]

Тут вопрос возник (не в первый раз):
typeof λx.x x Отвечаем, например, так
> :set -XRankNTypes > let f = (\x -> x x) :: (forall a. a -> a) -> (forall a. a -> a) > f id 42 42 Или так
> let f' = (\x -> x x) :: (forall a. a) -> (forall a. a) > f' undefined *** Exception: Prelude.undefined
Originally posted at http://deniok.dreamwidth.org/49632

Comments

[ext_1517625]

Ничего не понял. Было выражение, справедливое для нетипизированного лямбда исчисления. Вы решили узнать его тип.

Проверили (α → α) → (α → α), подошло.
Проверили α → α, подошло.

А мораль какая
?

[deni_ok]

Ненене, никакой (α → α) → (α → α) не подходит

> let f = (\x -> x x) :: (a -> a) -> (a -> a)

:26:16:
Couldn't match type `a' with `a -> a'
`a' is a rigid type variable bound by
an expression type signature: (a -> a) -> a -> a
at :26:9
In the return type of a call of `x'
Probable cause: `x' is applied to too many arguments
In the expression: x x
In the expression: (\ x -> x x) :: (a -> a) -> (a -> a)
Мораль такая, что изящная расстановка кванторов всеобщности, не вытаскиваемых на верхний уровень, даёт возможность типизировать иначе нетипизируёмоё.

[ext_1517625]

А ок.

Нетипизируёмоё.

[migmit]

Классический пример отсутствия principal type.

[deni_ok]

Пирс в 23.8 пишет, что для rank2types имеется алгоритм вывода типов, ссылаясь на статью Kfoury and Wells (1999)
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.6623
Там правда речь про intersection types, но ниже Пирс ссылается на статью Trevor Jim (1995)
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.5455
где показывается, что rank2types и intersection types эквивалентны: в них типизируемы в точности одни и те же термы.

Я всё это довольно поверхностно понимаю, поручил как-то одному студенту разобраться и доложить, но он растворился :(

Мне кажется, хотя возможно я ошибаюсь, для rank2types для заданного терма ещё можно держать под контролем конечный? набор не связанных principal types.

[ext_1517625]

> Citations
> The Java Language Specification - Gosling, Joy, et al. - 2000

Ничотак

[migmit]

Чёрт его знает, если честно.

[kodt_rsdn]

Забавно.
Было нетипизированное - работало.
Добавили типы - сломалось.
Сделали типы всеобщими - опять заработало. Фактически, вернулись в исходную позицию :))

Ну, на самом деле, не в исходную, потому что минимальная конкретика всё-таки возникла: на входе должно быть не что угодно, а функция.
Однако, в нетипизированной лямбде можно написать

f = \x . x x
f id id id id 42 == (id id) id id 42 == id id id 42 == id id 42 == id 42 = 42

ans = \x . 42
f ans == ans ans == 42

self = \x . self
f self a b == self self a b == self a b == self b == self

f f == f f - зациклились!

А в твоих ответах такой фокус не пройдёт.

Prelude> :t f
f :: (forall a1. a1 -> a1) -> a -> a
Prelude> : f id
f id :: a -> a
Prelude> :t ans
ans :: b -> Integer
Prelude> :t f ans

:1:3:
Couldn't match type `a1' with `Integer'
`a1' is a rigid type variable bound by
a type expected by the context: a1 -> a1 at :1:1
Expected type: a1 -> a1
Actual type: a1 -> Integer
In the first argument of `f', namely `ans'
In the expression: f ans

[kodt_rsdn]

Да, случай с ans лечится просто:

let f (x :: forall a . a -> b) = x x

А вот как закодировать self?

[deni_ok]

> :set -XExistentialQuantification
> data Self = forall a. MkSelf (a -> Self)
> let f = (\x -> x x) :: (forall a. a -> Self) -> Self
Кстати, для самого первого примера можно задать более точную спецификацию, контролирующую минимальное количество id:

> let f = (\x -> x x) :: (forall a. (((a -> a) -> (a -> a)) -> ((a -> a) ->
(a -> a))) -> (((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a)))) -> (forall a.
(((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))) -> (((a -> a) -> (a -> a)) ->
((a -> a) -> (a -> a))))
> f id id id 42

:15:16:
No instance for (Num (a0 -> a0))
arising from the literal `42'
Possible fix: add an instance declaration for (Num (a0 -> a0))
In the fourth argument of `f', namely `42'
In the expression: f id id id 42
In an equation for `it': it = f id id id 42
> f id id id id 42
42
:)

[deni_ok]

Никак не могу привыкнуть, что в последних ghci можно и data делать, и type и newtype. Так покороче будет

> type Arr a = a -> a
> type Arr4 a = Arr (Arr (Arr (Arr a)))
> let ffff = (\x -> x x) :: (forall a. Arr4 a) -> (forall a. Arr4 a)
> ffff id id id id 42
42