SP
ну как по мне автор проводит ложные разделения
Size: a a a
2020 April 21
SP
вводит нетипизированный язык, рассматривает его в контрасте с динамически типизированным
SP
к динамике неприменим весь этот аппарат с операционными семантиками, термами, это тупейшая машина которой что говорят то она и делает
DS
вводит нетипизированный язык, рассматривает его в контрасте с динамически типизированным
Ну и формально он прав в этом.
DS
Потому что типы в том, что обычно назвают динамически типизированными языками - есть, они проверяются в рантайме просто
SP
формально может и прав но я не почуствовал чтобы это все имело смысл
DS
А когда ты читаешь книжку по математике, то она должна быть формальной в своих определениях.
G
А я её не особо последовательно читал, скорее возвращался к паре глав, когда было желание.
и за сколько ты её прочитал?
SP
чтобы они проверялись в рантайме нужно их проверять специально, тоесть делать язык внутри языка. а по дефолту там ничего не проверяется там просто идут попытки чтото вызывать которые кидают эксепшены
DS
и за сколько ты её прочитал?
Не знаю, пару месяцев, раз в пару недель читал оттуда пару глав
DS
чтобы они проверялись в рантайме нужно их проверять специально, тоесть делать язык внутри языка. а по дефолту там ничего не проверяется там просто идут попытки чтото вызывать которые кидают эксепшены
Ну это и есть динамическая проверка
G
Не знаю, пару месяцев, раз в пару недель читал оттуда пару глав
хм, неплохо. а теорию категорий ты учил, если учил, то по какой книге?
DS
То что пришел эксепшен - это именно что и есть факт проверки
SP
А когда ты читаешь книжку по математике, то она должна быть формальной в своих определениях.
специально там искал определение статики - не нашел. и методологии почему он рассматривает все именно так - тоже не нашел. она какбудто бы написана в 19 веке когда классические математики вообще не парились над вопросами компьютейшенов
DS
хм, неплохо. а теорию категорий ты учил, если учил, то по какой книге?
Ну я читал "теорию категорий для работающего математика" и "теорию категорий для программистов"
DS
специально там искал определение статики - не нашел. и методологии почему он рассматривает все именно так - тоже не нашел. она какбудто бы написана в 19 веке когда классические математики вообще не парились над вопросами компьютейшенов
Ага-ага, то-то лямбда исчисления прям такой-то 19й век
DS
Как и системы типов, собственно, прям 19 век, 19м веком
SP
То что пришел эксепшен - это именно что и есть факт проверки
ну так это должно быть формальным. в реальности там нет никакой системы, мы просто траим и все, пальцем в небо
G
Ну я читал "теорию категорий для работающего математика" и "теорию категорий для программистов"
понятно, спасибо. первую глазами пробежался, показалась слишком сложной
G
думаю начну с пирса теория категорий