Каковы пределы вывода типа?
Обычно новое размещение используется для избавлений от стоимости выделения 'нормальный новый'.
Другой сценарий, где я использовал его, является местом, где я хотел иметь доступ к указатель к объекту, который должен был все еще быть создан, для реализации одиночного элемента на документ.
2 ответа
Джо Уэллс показал, что вывод типа неразрешим для Системы F, которая является самым основным полиморфным лямбда-исчислением, независимо открытым Жираром и Рейнольдсом. Это наиболее важный результат, показывающий ограничения вывода типов.
Вот важная проблема, которая все еще остается открытой: как лучше всего интегрировать обобщенные алгебраические типы данных в вывод типов Хиндли-Милнера? Каждый год Саймон Пейтон Джонс придумывает новые ответы, которые предположительно лучше, чем ответ прошлого года. Я не читал версию от марта 2009 г. и поэтому не могу сказать, верю ли я, что она будет окончательной.
Система зависимых типов от значений (или, короче, система зависимых типов) может описывать типы, которые говорят что-то вроде: «Во время оценки (время выполнения) значение этой переменной всегда будет равно значению этой переменной, которое вычисляется с помощью другого процесса оценки ". Автоматическое выведение этого типа из кода влечет за собой автоматические доказательства теорем. Если набор теорем, которые вы можете выразить, ограничен автоматически доказываемыми, это не будет проблемой, но в случае языков с зависимой типизацией это обычно не так.
Таким образом, системы с зависимой типизацией не могут иметь общие ( и полный) вывод типа.
Я уверен, что кто-то может дать моральный формальный и полный ответ ...