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

[deniok]

Тут вопрос возник (не в первый раз):

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

Comments

[dmitry malikov (from livejournal.com)]

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

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

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

[deni-ok.livejournal.com]

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

> 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)

Мораль такая, что изящная расстановка кванторов всеобщности, не вытаскиваемых на верхний уровень, даёт возможность типизировать иначе нетипизируёмоё.

[dmitry malikov (from livejournal.com)]

А ок.

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

[migmit.livejournal.com]

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

[deni-ok.livejournal.com]

Пирс в 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.

[dmitry malikov (from livejournal.com)]

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

Ничотак

[migmit.livejournal.com]

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

[kodt-rsdn.livejournal.com]

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

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

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

<interactive>: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 <interactive>: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.livejournal.com]

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

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

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

[deni-ok.livejournal.com]

> :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.livejournal.com]

Никак не могу привыкнуть, что в последних 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

[kodt-rsdn.livejournal.com]

Не понял всё равно. Ну, ввели мы тип Self и конструктор MkSelf. А саму функцию self как определить?
Что-то у меня мозги недонастроены на вывод экзистенциальщины. :(