Какой тип вывода делает Typed Racket? Я нашел следующий фрагмент в списке рассылки Racket:
Система типа Typed Racket содержит ряд функций, которые идут помимо того, что поддерживается системами типа Hindley/Milner, и поэтому мы не можем использовать эту систему вывода. В настоящее время Typed Racket использует локальный тип вывода для вывода многих типов в вашей программе, но мы хотели бы сделать из них больше - это постоянная область исследование.
В приведенном выше фрагменте используется термин "вывод локального типа", и я также слышал, что "написание ввода" используется много, но я не совсем уверен, что означают эти термины.
Мне кажется, что система вывода типов, которую Typed Racket использует в настоящее время, неоправданно слаба. Вот пример того, что я имею в виду. Не проверяется следующее:
(struct: pt ([x : Real] [y : Real]))
(define (midpoint p1 p2)
(pt (/ (+ (pt-x p1) (pt-x p2)) 2)
(/ (+ (pt-y p1) (pt-y p2)) 2)))
Вы должны явно аннотировать midpoint с помощью (: midpoint (pt pt -> pt)), иначе вы получите сообщение об ошибке: Type Checker: Expected pt, but got Any in: p1. Почему метод проверки типов не может заключить из этого, что типы p1 и p2 должны быть pt? Является ли это фундаментальным ограничением того, как Racket реализует типы (т.е. Эта линия рассуждений на самом деле ошибочна иногда из-за некоторых из более сложных типов Racket), или это то, что может быть реализовано в будущем?
По умолчанию предполагается, что неаннотированные функции верхнего уровня имеют типы ввода и вывода Any. Я предлагаю это неопределенное объяснение: поскольку система типа Racket настолько гибкая, она иногда может выводить типы, которых вы не ожидали, и разрешать некоторым программам тип typecheck, если вы предпочитаете, чтобы они выдавали ошибку типа.
Tangent: вы также можете использовать форму define:, если это вам подходит.
(define: (midpoint [p1 : pt] [p2 : pt]) : pt
...)