Почему среди программистов на Haskell бытует легенда, что если программа компилируется, то она верна? Почему мало смысла в споре между приверженцами статической и динамической типизации? Как превратить тип функции в теорему, а программу — в еë доказательство? Об этом и многом другом мы поговорим в мини-серии статей, посвящённой теории типов. Зачем? Когда речь заходит о типах и типизации в программировании, то в ход идут самые разные аналогии. Кто во что горазд! Типы сравнивают с наклейками на...

Семантическая алгебра разделяется на статическую семантику и динамическую семантику. Статическая семантика изучает отношения между понятиями (была введена операция семантического умножения). Динамическая семантика изучает понятия о процессах (здесь вводится операция семантического сложения). Обратите внимание на эти формулировки. Их отличие отражает то, что процессы мы можем изучать только опосредованно, через понятия. Если статическая семантика изучает парные отношения, то для изучения процессов проще всего пользоваться трёхчленной формулой: «Понятие 1 + Понятие 2 = Понятие 3». В такой формуле «+» означает наличие и слияние, а «–» означает отсутствие и потребность...