AG
вот тут неплохо расписана разница https://semantic-domain.blogspot.com/2019/08/on-relationship-between-static-analysis.html
Size: a a a
2021 April 13
AG
там явно не написано, но фактически статический анализ и пересечения это традиция карри, а подход через грамматику и композиционность это традиция чёрча
˸A
Мне ещё очень понравилась книга Introduction to Functional Programming - John Harrison (1997)
AG
ну да, вот то что тут написано это типизация по чёрчу
˸A
ну очевидно же - если lambda calculus - то по Чёрчу)))
AG
совсем необязательно, те же intersection types изначально вводились как система поверх лямбды
AG
собственно вот первая работа по ним https://link.springer.com/article/10.1007/BF02011875
AG
ключевая фраза на скриншоте выше это "must have exactly the type σ"
AG
грубо говоря у терма может быть бесконечное количество типов
AG
там есть всякие разрешимые подмножества, но классическое сочетание с сабтайпингом обычно всё усугубляет
AG
ну то есть конечно любая система разрешима с достаточным количеством аннотаций, вопрос уже в удобстве
˸A
То есть, для подтипов фраза "must have exactly the type σ" означает, что все подтипы σ - это тоже σ?
AG
для подтипов эта фраза просто не работает
AG
другая идеология
˸A
а как же тогда полиморфизм без подтипов делают? я не работал с языками без подтипов
˸A
уточнение: полиморфизм не типов - полиморфизм термов как делают?
2021 April 16
Д
Лол, этот фейк из акка моей знакомой сделали ))