Здесь я прочитал это:
У Haskell определенно нет самой продвинутой системы типов (даже близко, если считать языки исследований), но из всех языков, которые фактически используются в производстве, Haskell, вероятно, находится на вершине.
Поэтому я прошу две вещи:
- какие языки исследований имеют более мощные системы типов, чем Haskell;
- что они улучшают.
Я всего лишь программист, поэтому я не знаю много математических объектов, используемых в теории типов, пожалуйста, дайте мягкие объяснения, если можете.
programming-languages
type-theory
Виталий Олегович
источник
источник
Ответы:
Вопрос несколько проблематичен, поскольку опирается на субъективное определение «лучше».
Языки с независимой типизацией, такие как Agda , Idris и Coq, имеют более сильную систему типов, чем Haskell. Это означает, что вы можете использовать типы в этих языках, чтобы доказать больше свойств вашего кода, чем в Haskell. То есть есть более неправильные программы, которые будут пойманы.
Однако это происходит по цене: вывод типа и проверка существования каких-либо значений данного типа больше невозможны. Это означает, что для этих языков вам необходимо явно аннотировать ваш код типами. По сути это сводится к написанию собственных доказательств правильности вашего кода.
Так эти языки "лучше", чем Haskell? Они могут проверить расширенные доказательства правильности вашего кода, но не могут автоматически подтвердить свойства вашего кода, как это может сделать Haskell.
Еще один язык исследований, который "лучше", чем Haskell, - это LiquidHaskell . В основном это Haskell с типами уточнений, прикрепленными сверху, проанализированными из специальных комментариев.
Типы уточнения позволяют уточнять типы с помощью свойств. Например, вместо
Intуказания можно указать{i : Int | i > 0}тип всех положительных целых чисел. Вывод типа разрешаем с типами уточнения, но вы не можете доказать столько свойств корректности с ними, сколько вы можете с зависимыми типами.Существуют и другие системы уточнения, но я не очень знаком с любой из них.
источник
Семейство языков ML (StandardML, OCaml ) возникло по аналогии с Haskell и поэтому имеет схожие системы типов. Однако они не совсем такие же, как на Haskell, и некоторые их функции могут вам подойти лучше (не существует такой вещи, как объективно лучшая система типов, потому что системы языков в языках программирования существуют, чтобы помочь людям ). Вот некоторые особенности OCaml, которые Haskell либо не имеет (но может иметь аналогичную концепцию), либо Haskell имеет, но сделал иначе:
И, пожалуйста, нет необходимости превращать это в перестрелку ML-Haskell, иначе я начну ссылаться на сообщения в блоге Боба Харпера ;-)
источник
Исследовательский язык Clean имеет лучшую систему типов, чем Haskell, потому что он имеет уникальные типы . Идеи, лежащие в основе типов уникальности, тесно связаны с линейной логикой , которая ближе к ресурсному ограниченному «реальному миру», чем классическая логика.
Анти-исследовательский язык Rust также имеет систему типов с уникальными функциями, которые ближе к «реальному миру», чем классические системы чистого типа. Большинство идей, которые повлияли на систему типов, были опубликованы совершенно независимо от Rust задолго до того, как она появилась. Но способ, которым эти старые идеи собраны воедино, уникален и также заслуживает реальных научных публикаций, даже если существуют известные лазейки и несоответствия.
источник