интуиционистскую теорию типов Мартин-Лёфа, зависимые типы). Haskell немного подотстал. Его планируют развивать? Или не будут в эту сторону развиваться? Там типа своя ветка языков - proof assistance, автоматическое доказательство теорем. A Haskell идет курсом на мэйнстрим?
на Haskell можно настоящие программы писать, в отличие от Agda/Idris
но зависимые и линейные типы в Хаскель добавляют прямо сейчас
Обсуждают сегодня