Комментарии 24
Так и до абстрактной алгебры недалеко!
можно(и нужно) рассматривать как математические множества.Мысль хоть и очевидная
почему "нужно" и, простите, с какой стороны это "очевидно"?
наверное лучше вбрасывая такие громкие заявления как-то их мотивировать :)
про теорию типов больше всего энтузиазма я слышал со стороны пропонентов Haskell например... и кажется сейчас от хаскеля даже в Биокаде отказались...
Я бы сказал что теория множеств в упоминаемом контексте скорее вредна: это слишком конкретная модель, у неё можно «провзаимодействовать с границей».
кажется сейчас от хаскеля даже в Биокаде отказались...
А чем это так показательно?
Вы правы, звучит действительно как провокация, но таковой не является)
Мне следовало написать можно(и нужно) в том числе рассматривать как математические множества
чушь какая-то, извините.
А память это для морлоков.
Рисунок с окружностями прикольный, но не передает масштаб. Отношение радиусов должно отличается в квадрат раз.
Есть классическая уже книга - Типы в языках программирования - у нас делали перевод - Типы в языках программирования (tversu.ru)
Как говорил наш препод: "программист без знаний математики - это не программист, а переводчик".
Она называется - "Теория Типов".
Кажется вы до неё так толком и не добрались. Кстати с похожим успехом можно трогать более абстрактную теорию категорий. Заодно и мем про моноид в категории эндофункторов понять.
Улыбнуло "определение" множества через якобы более простой термин "коллекция". Это ж без определения идёт обычно.)
Лет десять назад я имел такие же представления о типах. Сейчас же у меня вызывают протест многие утверждения из начала статьи, которые формируют неформально понятийную систему у читателя и тем самым определяют путь в своих рассуждениях.
Множество — это коллекция элементов, обладающих общим свойством, которые рассматриваются как единое целое
В общепринятой математике множество — это (неформально говоря) объекты, рассматриваемые как один объект. На объектах определено отношение (двуместный предикат) принадлежности, то есть один объект или принадлежит второму, или нет. Если второй объект не множество — всегда нет.
Никакое требование об общем свойстве не накладывается: множество {1, "hello", <кот Василий>} существует. Есть множества, все элементы которого имеют только то общее свойство, что они принадлежат этому множеству.
Множества подчиняются аксиоме объёмности: если два множества состоят из одних и тех же элементов, то это одно и то же множество.
Типы в программировании можно(и нужно) рассматривать как математические множества.
Лучше бы так не делать, потому что типы не обладают вышеперечисленными свойствами множеств. Начнём с того, что нет предиката принадлежности объекта типу. Когда мы пишем x : T, мы не говорим «вот есть объект T, вот есть объект x; кстати, T — это тип; ах да, x принадлежит T». Мы вместо этого говорим или «вот есть выражение x и оно доказуемо по построению имеет T», или «вот переменная x, считать её по определению имеющей тип T».
Многие системы типов устроены так, что никакой объект не может быть экземпляром двух типов. Как в таких условиях говорить об аксиоме объёмности?
Я бы говорил о типах как о метках, которые мы ставим на выражениях. Система типов должна ограничивать нас, и через этого гарантировать, что выполняются какие-то свойства у любого правильно-типизированного выражения.
Простым примером системы типов является система цветных функций.
В качестве антитезы следует согласиться, что типы и множества связаны.
С одной стороны, развитые системы типов (вроде Agda, Coq, HoTT) считают, что множество — это частный вид типов. Но там и множество понимает не общепринято. Поскольку я плохо разбираюсь в интуиционистском варианте теории множеств, призываю малышку @Natasha_Klaus на помощь пояснить за Coq. В HoTT множеством называется тип, у которого любые два экземпляра равны не более чем одним способом.
С другой стороны, для системы типов можно построить модель, в которой каждому типу сопоставляется множество. Впрочем, для программирования более полезны другие виды моделей:
тип как топологическое пространство (точнее, решётка, см. работы Даны Скотт) — позволяет адекватно говорить о функции f : A → B как о непрерывном отображении из A в B, потому что не всякая функция из множества A во множество B может быть программой
тип как идеал — то же, но с поддержкой полиморфизма (дженериков)
тип как интервал — то же, но с нормальной поддержкой полиморфизма и типов-дополнений (т.е. «всё, что не является элементом типа A»)
тип как отношение — для бесплатных теорем, бомба
Начнём с того, что нет предиката принадлежности объекта типу. Когда мы пишем x : T […]
Уточню. Вот тут не надо путать терм (тот самый x) и его значение. Для значений нет проблем построить предикат принадлежности.
В HoTT множеством называется тип, у которого любые два экземпляра равны не более чем одним способом.
Ага, только вот во всех языках программирования, включая Agda и Idris, любой тип является множеством (есть попытки убрать аксиому K из языков, но они все за флагами). Так что, даже с точки зрения HoTT, занимаясь практическим программированием считать типы множествами не так уж и глупо.
Уточню. Вот тут не надо путать терм (тот самый x) и его значение. Для значений нет проблем построить предикат принадлежности.
Да. Я, конечно, говорю только о термах. Понятие «значения» требует определения, что мы под ним понимаем: если денотат в модели, то нужна сама модель.
Ага, только вот во всех языках программирования, включая Agda и Idris, любой тип является множеством (есть попытки убрать аксиому K из языков, но они все за флагами)
Не знал, что в Агде пытаются убрать аксиому K. Спасибо за тему.
В целом, ожидается, что в «обычных» ЯП тип является «множеством» в смысле HoTT. Просто это не совсем похоже на классические множества.
Я тут ещё вспомнил про constraint type, которые как раз интерпретируются как предикаты на универсуме значений (не разбираюсь в них, ссылок сходу не нашел, хотя упомянутый Картрайт о них говорит). Так что моя категоричность пошаталась. Я не ситх, мне можно.
занимаясь практическим программированием считать типы множествами не так уж и глупо.
Не глупо, если учитывать все оговорки. Правильно ли это дидактически? Я усомнился, поэтому высказался.
Понятие «значения» требует определения, что мы под ним понимаем: если денотат в модели, то нужна сама модель.
В практическом программировании у нас уже есть модель значений, она дана нам языком. Тут скорее применение теории типов требует усилий.
Не глупо, если учитывать все оговорки. Правильно ли это дидактически? Я усомнился, поэтому высказался.
Дидактически правильно повышать уровень сложности материала постепенно. В начальной школе ни аксиоматику Пеано, ни системы счисления не рассказывают, хотя базовая арифметика как раз из них и выводится.
Примеры буду приводить на языке C#, однако их можно воспринимать как псевдо-код
Ну это вы зря на самом деле. Конкретно на C# ваши выводы вообще не имеют смысла, как и в любом языке с номинальной типизацией (коих большинство из мейнстримных).
class Vehicle
{
public string Make { get; set; }
public string Model { get; set; }
}
Vehicle= {x | x имеет марку и модель}
Очевидно что Vehicle это не "все возможные объекты с маркой и моделью", это конкретно объекты, определённые как Vehicle, не больше и не меньше.
То есть при наличии нескольких типов со схожей структурой объект не будет волшебным образом принадлежать им всем, а будет принадлежать только тем, через которые он определён.
Поддерживаю автора. Когда мы говорим о типе переменной то в первую очередь мы имеем ввиду множество допустимых значений. А духоту из теории типов изают только в академических работах
Типы в программировании как математические множества