Есть ли типизированное исчисление SKI?

Большинство из нас знает соответствие между комбинаторной логикой и лямбда-исчислением . Но я никогда не видел (может быть, я недостаточно глубоко изучил) эквивалент «типизированных комбинаторов», соответствующих простейшему типу лямбда-исчисления. Существует ли такая вещь? Где можно найти информацию об этом?

reference-request logic lambda-calculus type-theory combinatory-logic Уго Серено Феррейра
источник

Возможно, вас заинтересует Устранение монады и абстракции в The Monad.Reader, выпуск 17 . Монада Reader (или, точнее, ее аппликативный функтор) тесно связана с типизированным SKI.

Петр Пудлак

Ответы:

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

$\mathbf{I}_{\alpha\to\alpha}$
$\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
$\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$

для всех комбинаций простых типов и . $\alpha,\beta$ $\gamma$

В качестве альтернативы, просто представьте типы как схемы типов (или полиморфные типы) и введите их в Haskell и вуаля: комбинаторы .

Дэйв Кларк
источник

Я никогда не думал, что комбинатор

действует как монада! Это так?

S

$\mathbf{S}$

Уго Серено Феррейра

На самом деле, я указал, что

соответствует оператору Аппликативные функторов и в

S

$\mathbf{S}$ <*>pure

K

$\mathbf{K}$

Уго Серено Феррейра

вполне фундаментален, поэтому может соответствовать многим вещам.

имеет тот же тип, чтофункция монадного

для функтора

S

$\mathbf{S}$

S

$\mathbf{S}$

a p

$ap$

Λ X . α \to X

$\Lambda X.\alpha\to X$

Дейв Кларк