![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
Блеск и нищета просто типизированной лямбды
В чистой бестиповой лямбде обычное кодирование булевых значений таково
Напомним, что просто типизированная лямбда строится следующим образом. Берём за основу бесконечное множество переменных
Вернёмся к типизации булевых термов и функций. Если приписать булевым термам <<простой>> тип, получим
Однако, к сожалению, всё не так просто. Если посмотреть на условный оператор
Есть два выхода.
Выход (1). Расширение просто типизированной лямбды булевыми константами.
(a) ввести константы true, false и iif в термы, как атомы;
(b) ввести константу Bool в типы, как атом;
(c) ввести дополнительные правила типизации true:Bool, false:Bool и схему правил для любого типа s:
Выход (2). Расширение просто типизированной лямбды до полиморфной лямбды (System F).
UPD. Ну и для полноты картины стоит отметить, что System F должна быть <<оборудована>> ещё и абстракцией терма по типу, которая часто записывается в виде большой лямбды. При этом определение iif принимает окончательный вид
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
no subject
no subject
Безотносительно к этому каждая "хорошая" система типов хороша тем, что позволяет на своём языке делать какие-то полезные содержательные утверждения о программах.
no subject
no subject
no subject
no subject
no subject
IF NOT Type("end_date") = "D" end_date = Date() ENDIF ...Это к вопросу о том, что типы не обязательно использовать при написании.no subject
no subject
no subject
#if TYPED enum { MEAN = 365, LEAP = 366 } ndays; #else int ndays; assert((365 == ndays) || (366 == ndays); #endifОднако, если абстрагироваться от реализаций языков программирования, не меняем ли мы все-таки шило на мыло?no subject
no subject
no subject
no subject
no subject
no subject
no subject
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")no subject
no subject
no subject
no subject
вы же не пытаетесь моделировать goto через while если все
равно вполне достаточно пользоваться только while напрямую...