суббота, 21 августа 2021 г.

Тема ТИП

Типизация — классификация, таксономия, семантика, грамматика, спецификация, атрибуция, характеристика, дефиниция, идентификация, параметризация … В программировании, где, прежде всего, парсинг осуществляется с цепочкой символов некоторого алфавита, то количество символов в цепочке — тип. Элементарный тип — номер, индекс, натуральное число (но и позиция тоже определяет тип). Процесс нумерации можно интерпретировать как именование упорядоченных элементов, а само именование как выделение, фиксация. Фактически, типизация, суть абстрагирования или классификации. Поэтому, с одной стороны, любые попытки конструирования теорий типов, привлекают внимание, как метатеория, а с другой, они же демонстрируют, что сам по себе термин ТИП — предельная категория, без которой вполне можно обойтись. То, что понимают под формализмом «тип» теоретики (собственно, сам «формализм»), имеет косвенное отношение к проблеме организации памяти в программировании. Вся политика программирования сводится к вопросу ответственности за приведение к формату протокола, до использования сервиса или сервис должен верифицировать валидность своих параметров. Эти две проблемы следует отделить друг от друга как обозначение и значение. Из теории типов следует, что тип — предикат. Под предикатом в традиционной математике понимают высказывание с характеристикой "истина" и "ложь", а эта конструкция - синтаксический сахар. Нет смысла разделять высказывание, синонимом которого просто предикация или пропозиция. В этом ключе можно было бы считать типы атрибутами, то есть типизацию атрибуцией объекта, если бы мы не классифицировали сами объекты с позиции организации в памяти и определенных операций. Кстати, две эти точки зрения по существу принципиально разные. Типы не нужны, типизация по-существу и есть конструирование абстрактной и гетерогенной структуры и как следствие поиск по ней. Здесь уместно вернуться к изначальным реальным проблемам и их дескрипциям, тупо идентифицировать. Что, когда и зачем. Обычное дело, когда теория оторвалась от практики и превратилась в интеллектуальную игру вместо моделирования реальной практики. А то что предикация описывает по сути отношение, то да ... это по сути функция и в случае "типизации" тоже. А когда функция отображает структуру в структуру, то типизация уже функции становится все равно не понятным.

https://telegra.ph/Tip-08-21

https://t.me/KODIFIKATION/933

https://t.me/KODIFIKATION/921

https://t.me/KODIFIKATION/920

3 комментария:

  1. SPSc: суперкомпилятор на языке Scala
    https://cyberleninka.ru/article/n/spsc-superkompilyator-na-yazyke-scala
    Самостоятельное изучение Рефала-5. Взгляд студента
    https://web.archive.org/web/20101009092138/http://ulm.uni.udm.ru/~soft/wiki/doku.php?id=refal-5:korsa
    Язык Рефал-05, его отличия от Рефала-5 и общее подмножество
    https://mazdaywik.github.io/Refal-05/2-syntax.html
    Делаем Refal на Prolog. Магия в семь строк
    https://habr.com/ru/post/198972
    БАЗИСНЫЙ РЕФАЛ
    http://ilt.kharkov.ua/bvi/rf/doc/ark_klimov/refal6/M1-basic.htm
    https://github.com/STrusov/refal-machine
    https://github.com/bmstu-iu9/refal-5-lambda/blob/master/docs/2-intro.md
    Запахи кода и антипаттерны в Рефале
    https://www.mail-archive.com/refal@botik.ru/msg00902.html
    Об оценке производительности некоторых языковых процессоров символьной обработки (РЕФАЛ, ЛИСП, ПРОЛОГ)
    https://library.keldysh.ru/preprint.asp?id=1993-33
    https://ru.m.wikipedia.org/wiki/Гомоиконичность
    https://en.m.wikipedia.org/wiki/Meta-circular_evaluator

    ОтветитьУдалить
  2. https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов

    ОтветитьУдалить
  3. https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов

    ОтветитьУдалить