Функция может работать под первой версией сигнатуры типа
(: rember-fc (∀ (a) (-> (-> Any Any Boolean) (-> a (Listof a) (Listof a)))))
, если добавить аннотацию, в которой вы используете функцию в рекурсивном вызове, заменив
((rember-fc test?) a (cdr l))
на
(((inst rember-fc a) test?) a (cdr l))
, где аннотация типа inst позволяет выполнить проверку типов.
Это использование функции имеет два приложения: внутреннее и внешнее. Внутреннее приложение сначала проверяется по типу, а внешнее проверяется только по типу, если у него есть конкретный тип для внутреннего приложения.
Алгоритм вывода типов для типизированной ракетки достаточно умен, чтобы выяснить, в чем заключается переменная forall ((rember-fc test?) a (cdr l)), когда (rember-fc test?) имеет тип forall, а a и (cdr l) предоставляют информацию. Внутреннему приложению не требуется вывод типа, если forall находится посередине, а вывод типа внешнего приложения выполняется успешно, потому что внешние аргументы приложения предоставляют информацию.
Однако вывод типа недостаточно умен, чтобы понять, чтоout, когда rember-fc имеет тип forall, а test? не предоставляет информацию во внутреннем приложении. a и (cdr l) применяются только позже во внешнем приложении. Когда вывод типа не может понять это, он угадывает Any во внутреннем приложении, и он только обнаруживает, что догадка была неправильной позже во внешнем приложении.
Итак, две рабочие версии:
(: rember-fc (∀ (a) (-> (-> Any Any Boolean) (-> a (Listof a) (Listof a)))))
(define rember-fc
(λ (test?)
(λ (a l)
(cond [(null? l) '()]
[(test? a (car l)) (cdr l)]
[else
(cons (car l)
(((inst rember-fc a) test?) a (cdr l)))]))))
А:
(: rember-fc (-> (-> Any Any Boolean) (∀ (a) (-> a (Listof a) (Listof a)))))
(define rember-fc
(λ (test?)
(λ (a l)
(cond [(null? l) '()]
[(test? a (car l)) (cdr l)]
[else
(cons (car l)
((rember-fc test?) a (cdr l)))]))))