Блеск и нищета просто типизированной лямбды

[deniok]

В чистой бестиповой лямбде обычное кодирование булевых значений таково

  tru = λt f. t
  fls = λt f. f

При этом условный оператор кодируется так:

  iif = λb x y. b x y

а основные булевы функции так

  not = λb t f. b f t
  and = λa b. a b fls
  or  = λa b. a tru b

Что из этого получится в просто типизированной системе?

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

  Var = {a,b,c,d,...}

Индуктивно определяем, что тип это либо переменная, либо (правоассоциативная) стрелка между типами

  Type = Var | Type -> Type

Затем задаём правила приписывания типов термам - правила вывода типов. Переменной можно приписать любой тип, абстракции - стрелочный

   x:A    M:B
----------------
(λx. M):(A -> B)

Что касается аппликации, то тип левого аппликанда должен быть стрелочным:

 M:(A -> B)  N:A
-----------------
   (M N): B

Здесь метапеременные M и N обозначают произвольные термы, а метапеременные A и B --- произвольные типы.

Вернёмся к типизации булевых термов и функций. Если приписать булевым термам <<простой>> тип, получим

  tru : a -> b -> a
  tru = λt f. t

  fls : a -> b -> b
  fls = λt f. f

Хотелось бы иметь одинаковый тип для истины и лжи, поэтому естественно приписать t и f один и тот же тип (a). Тогда, введя <<сокращение>>

  Bool = a -> a -> a

можем писать желаемые утверждения типизации

  tru : Bool
  fls : Bool

Однако, к сожалению, всё не так просто. Если посмотреть на условный оператор

  iif : Bool -> s -> s -> s
  iif = λb x y. b x y

то возникает такая проблема. Хотелось бы применять iif к значению любого конкретного типа s, но тогда правила вывода дадут

  Bool  = s -> s -> s

Получается, что наш Bool плохо инкапсулирует свои внутренности. Это приводит к проблемам с типизацией. Например, непонятно, какой тип выведется у b в

  problem = λb. pair (iif b 1 2) (iif b "Ann" "Bob")

Есть два выхода.

Выход (1). Расширение просто типизированной лямбды булевыми константами.

(a) ввести константы true, false и iif в термы, как атомы;
(b) ввести константу Bool в типы, как атом;
(c) ввести дополнительные правила типизации true:Bool, false:Bool и схему правил для любого типа s:

  iif : Bool -> s -> s -> s

(d) ввести схему аксиом δ-редукции: для любых типа s и термов x:s и y:s

  iif true  x y  -δ->  x
  iif false x y  -δ->  y

Выход (2). Расширение просто типизированной лямбды до полиморфной лямбды (System F).

  Bool = forall a. a -> a -> a

При таком подходе в терме

  iif = λb x y. b x y

в теле лямбды перед применением b к x:s происходит (неявное) применение полиморфного значения b : forall a. a -> a -> a к типу s. Эта аппликация терма к типу нужна для того, чтобы <<мономорфизировать>> дотоле полиморфный тип b для дальнейшего использования. Можно эту аппликацию (b s : s -> s -> s) писать явно:

  iif : (forall a. a -> a -> a) -> s -> s -> s
  iif = λb x y. b s x y

UPD. Ну и для полноты картины стоит отметить, что System F должна быть <<оборудована>> ещё и абстракцией терма по типу, которая часто записывается в виде большой лямбды. При этом определение iif принимает окончательный вид

  iif : forall s. (forall a. a -> a -> a) -> s -> s -> s
  iif = Λs. λb x y. b s x y

Comments

[codedot.livejournal.com]

Пожалуйста, объясните, наконец, дураку, чем же так хороши были бы типы в λ-исчислении, если бы его можно было типизировать (известно, что нельзя) полностью. Какие от этого выгоды? (Чур сильную нормализуемость в пример не приводить, так как именно из-за нее-то и нельзя.)

[deni-ok.livejournal.com]

Я, честно признаться, плохо понял вопрос. Существует масса систем, в которых любой терм типизируем. Самая простая из них - каждому терму приписывается тип (I am a lambda-term).

Безотносительно к этому каждая "хорошая" система типов хороша тем, что позволяет на своём языке делать какие-то полезные содержательные утверждения о программах.

[codedot.livejournal.com]

Ага, понял, то есть частичный (полный невозможен из-за «halting problem») анализ кода делать. Спасибо. (Я, конечно, имел в виду только λ-куб, а не более широкое понятие.)

[triampurum.livejournal.com]

У некоторых (не всех) типизированных лямбда-исчислений есть логическая интерпретация.

[codedot.livejournal.com]

Тоже хорошо. Спасибо.

[codedot.livejournal.com]

Что-то пока нет в примерах ничего, что качественно отличает типизированные варианты от бестипового λ-исчисления. А ограничений вместо этого сразу накладывается целая куча. Чтобы делать анализ программ, совсем не обязательно использовать типы при их написании. Ну, а логика разве не остановилась на конструктивной линейной, из которой, собственно, и получен теоретический предел эффективности вычислений в виде оптимальной редукции?

[deni-ok.livejournal.com]

Я в давние времена, когда писал много кода, и делал это на древнем нетипизированном языке, вынужден был начинать каждую функцию с проверки параметров

IF NOT Type("end_date") = "D"
	end_date = Date()
ENDIF
...

Это к вопросу о том, что типы не обязательно использовать при написании.

[codedot.livejournal.com]

С другой стороны, проверка аргументов на корректность и исключения так никуда из программирования и не исчезли.

[deni-ok.livejournal.com]

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

[codedot.livejournal.com]

По мотивам беседы родилась шуточная зарисовка на Си:

#if TYPED
	enum {
		MEAN = 365, LEAP = 366
	} ndays;
#else
	int ndays;

	assert((365 == ndays) || (366 == ndays);	
#endif

Однако, если абстрагироваться от реализаций языков программирования, не меняем ли мы все-таки шило на мыло?

[deni-ok.livejournal.com]

Я так полагаю, что ответ на этот вопрос зависит от проблем, которые стоят перед спрашивающим. Если для эффективной реализации оптимальной редукции, которая, как я понимаю, является предметом ваших исследований, типы не нужны, то их и не надо использовать. Вам виднее.

[thedeemon.livejournal.com]

Первая выгода - хоть какая-то практичность. Практикам нужны числа (целые и не очень), строки и т.д. и вовсе не хочется делить числа на строки. Тут и возникают типы естественным образом.

[codedot.livejournal.com]

Как именно возникли те типы, что чаще всего встречаются на практике, — понятно: по сути они понадобились в результате добавления символов в алфавит λ-исчисления. Здесь же речь шла скорее о λ-кубе, системы типизации в котором уже довольно слабо связаны с δ-функциями, примеры которых при нулевой арности включают натуральные числа и строки, а многоместные их варианты — элементарные операции над этими данными.

[migmit.livejournal.com]

Э... почему сразу до SystemF-то?

[deni-ok.livejournal.com]

А что более слабое ты считаешь годным?

[migmit.livejournal.com]

HM, как в Хаскеле.

[deni-ok.livejournal.com]

Хм?

Prelude> let iif b x y = b x y
Prelude> let problem b = (iif b 'x' 'y', iif b "Ann" "Bob")

< interactive >:1:39:
    Couldn't match expected type `Char' with actual type `[Char]'
    In the second argument of `iif', namely `"Ann"'
    In the expression: iif b "Ann" "Bob"
    In the expression: (iif b 'x' 'y', iif b "Ann" "Bob")

[migmit.livejournal.com]

Да, туплю.

[4kcheshire.livejournal.com]

http://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

[deni-ok.livejournal.com]

То что внутриязыковой Bool не сильно годен для эквационального резонёрства, это понятно. Я о том, что в просто типизированной лямбде выразить этот простейший тип "естественным образом" не очень удаётся.

[4kcheshire.livejournal.com]

ну так он и не нужен)) или вы чисто из теоретического интереса пытаетесь?
вы же не пытаетесь моделировать goto через while если все
равно вполне достаточно пользоваться только while напрямую...