если никто не возражает, я тут буду тихо бредить
в связи с обзором по обозначенной тематике типов, множеств и классов,
пытаясь сообразить, что такое тип.
Теорию типов от Рассела, которую часто упоминают
можно найти в обзоре
Аксиоматические системы теории множеств, Ван Хао, Мак-Нотон, Сборник Математика, Иностранная литература, 1963;
Программисткое введение в теорию типов в
Introduction to Type Theory, Herman Geuvers, Radboud University Nijmegen and Technical University Eindhoven, The Netherlands, 2008.
http://agp.hx0.ru/arts/IntroTT.pdf
При этом, автор ссылается на простую теорию типов от Черча
A Formulation of the Simple Theory of Types, Alonzo Church, The Journal of Symbolic Logic, Vol. 5, No. 2., 1940;
http://agp.hx0.ru/arts/church-1940.pdf

)) я ее помагал переводить.
Не сильно напрягался, но пару раз шото ляпнул.

Сейчас пока бестипное лямбда исчисление мучаю.


выложил
Аксиоматические системы теории множества, Ван Хао, Мак-Нотон, Издательство иностранной литературы, Москва, 1963. 11 - 15 страница содержит теорию типов Рассела;
http://agp.hx0.ru/arts/Mnoj_hao.djvu

русскоязычное описание вариации простой системы типов Черча
от Дехтяренко
http://www.softcraft.ru/paradigm/dp/dp04.shtml

явное или не явное определение типов как множество
есть у
Харпера, введение в стандартный ML

и у Филда И Харрисона Функциональное программирование 1993,
Мир
В самом деле, по видимому, слово 'оперировать' означает, что
функции определены на некоторых основных типах и вырабатывают значения из
этих же типов. Но функции задаются только на множестве допустимых значений и
вырабатывают значения из множества допустимых значений.

Лямбда- исчисление. Его синтаксис и семантика, Барендрегт, Мир, 1985 - с 548 страницы излагается типизированное лямбда - исчисление.
http://agp.hx0.ru/arts/Barendregt.Lambda-ischislenie.Mir.1985.djvu

простая теория типов Черча в работе за 40 год из первого поста непонятно куда попадает,
то ли в противоречивую теорию 32-33, толи в непротиворечивую за 41.
Наверно, во вторую, поскольку парадоск напечатан в 35.

у Дехтяренко, Рассела и Барендрегта
1
тип это символ
2
есть правило, позволяющее задать по типу х множество всех элементов типа х.

Барендрегт облегчил чтение Черча.

и это у Черча так и написано
множество символов типа описывается правилами, что
\iota и \o есть символы типов и если \alpha и \beta - символы типов,
то (\alpha \beta) тоже символ типа.
с тем отличием от Барендрегта, что функция, повидимому, записывается наоборот
(\alpha \beta) это тип функций \beta \to \alpha

\o - это тип propositional - (пропозициональных высказываний) видимо булеан,
\iota - тип сущностей

ZyK_BotaNtchingiz,

а я сегодня начал читать Пирса "Типы в языках программирования". Не смотрел?

0.3.5. Типы Пирса

Типы в \cite[Простые типы]{Pierce1Ru} вводятся по уже
знакомой схеме. Вводятся два символа
$Nat$ и $Bool$ и правила, задающие отношение типизации между
произвольными термами языка $t$ и символом типа $T$, где $T$ -
либо $Bool$, либо $Nat$. Причем контекст использования термина
тип близок к использованию термина множества. Отношения
типизации, записываемое в виде $t$ : $T$ читается как:
терм $t$ является элементом $T$;
терм $t$ имеет тип $T$;
$t$ принадлежит типу $T$.
В силу того, что уже решено отличать термин 'тип' от термина
'множество', фразу 'терм $t$ является элементом $T$' будем
считать сокращением от фразы 'терм $t$ является элементом
множества всех элементов, имеющих тип $T$'.

ZyK_BotaNtchingiz,

а я сегодня начал читать Пирса "Типы в языках программирования". Не смотрел?


на сайте поддержики продолжает жить 106 версия

автор
Types and Programming Languages: перевод

Это сайт, предназначенный для поддержки русского перевода книги Бенджамина Пирса "Типы в языках программирования" (Benjamin C. Pierce, Types and Programming Languages)
http://newstar.rinet.ru/~goga/tapl/


построил 123-ю
http://agp.hx0.ru/arts/tapl.pdf

блин, :(( :)) они родили новую, но она не пишет ревизию у меня.


http://agp.hx0.ru/arts/tapl.28.06.2010.pdf

а на http://newstar.rinet.ru/~goga/tapl/
положили 123ю



http://dl.dropbox.com/u/132983/tapl.pdf

210 ревизия от 25 июля
http://newstar.rinet.ru/~goga/tapl/tapl.pdf

Карделли со ссылкой на Дану Скотта (ученик Черча и премия тьюринга)
утверждает, что тип это множество со свойством идеала

перевод понимания Карделли
http://www.k-press.ru/cs/2006/2/onunderstand/OnUnderstand.asp

что такое идеал у Скотта пока не совсем понятно,
но понятно, что целые числа не являются идеалом для рациональных и вещественных
http://ru.math.wikia.com/wiki/%D0%98%D0%B4%D0%B5%D0%B0%D0%BB_%28%D0%B0%D0%BB%D0%B3%D0%B5%D0%B1%D1%80%D0%B0%29
и, поэтому, не могут быть подтипом.
Наследовать целые из вещественных - нельзя

типы данных как решетки, Дана Скотт

http://agp.hx0.ru/arts/Scott.Datatypesaslattices.1975.pdf

шо тут не понятно может быть?
авторИдеалом кольца A называется такое подмножество I кольца A, что

1. для любых элементов i и j из I, их сумма i+j также лежит в I;
2. для любого элемента i из I его противоположный элемент -i также лежит в I;
3. (условие на правые идеалы) для любого элемента i из I и любого элемента a из A произведение ia также лежит в I;
4. (условие на левые идеалы) для любого элемента i из I и любого элемента a из A произведение ai также лежит в I.

Рациональные это кольцо относительно сложения и умножения.
Пытаемся взять целые
целые удовлетворяют условию 1 - сумма двух целых - целое
целые удовлетворяют условию 2 - для каждого целого есть число сложив с которым получаем 0
целые не удовлетворяют условию 3 - берем любое целое 1 и любое с плав.точко 1/2
произведение по условию должно принадлежать целым, а оно не принадлежит.
Целые - не идеал.

в идеале обе операции замкнуты - применение первой операции к двум операндам из подмножества
пдает в результате элемент из подмножества.
применение второй к элементу подмножества и надмножества выдает элемент подмножества

можно попытаться, я его работу для этого и раскопал

Robert C. Martin, The Liskov Substitution Principle, C++ Report, March 1996. An article popular in the object-oriented programming community that gives several examples of LSP violations.

русско язычное обсуждение принципа замещения лисков
http://blog.byndyu.ru/2009/10/blog-post_29.html