Обсуждение:Теория типов
Эта статья тематически связана с вики-проектом «Информационные технологии», цель которого — создание и улучшение статей по темам, связанным с информационными технологиями. Вы можете её отредактировать, а также присоединиться к проекту, принять участие в его обсуждении и поработать над требуемыми статьями. |
Утверждение из первой же строки этой статьи (похоже напрямую переведённое из en.wikipedia) очень уж неточное. В качестве "какой-либо формальной системы, являющаяся альтернативой наивной теории множеств" может выступать, например, аксиоматическая теория множеств -- та же ZFC, скажем. Которую никто не рассматривает как тИповую. Очевидно стоит добавить слова про наличие разделения домена наших рассуждений на слои (типы), образующие иерархию. И, возможно, что-нибудь про нотацию выполнимости и аксиому свёртывания, с требованием для типа "свойства" быть в иерархии типов выше, чем типы объектов, для которых это свойство выполняется. Deniok 19:31, 17 декабря 2012 (UTC)Deniok
Гомотопическая теория типов править
Гомотопическая теория типов должна бы уже быть упомянута и описана. Статья теория типов есть...
- популярное введение на примере 9*2 = 2*9
- пост про саму теорию и формируемую командой математиков на гитхабе книжку по ней
--Nashev 07:56, 15 января 2014 (UTC)
- Обязательно напишем ещё и большую целостную статью про гомотопическую теорию типов — одну из самых примечательных теорий 2010-х, претендующих на основания математики («унивалентные основания математики»). Но только не на базе блогов, а по материалам авторитетных источников, которых, к сожалению, пока неоправданно мало (вроде бы была какая-то заметка в Science, но сейчас её найти не могу), bezik 10:22, 15 января 2014 (UTC)