В REPL это то, что я получаю, когда проверяю тип car
> car
- : (All (a b) (case-> (-> (Pairof a b) a) (-> (Listof a) a)))
Он возвращает элемент первого типа в паре при передаче пары, где второе значение может не существовать.
Теперь я хотел бы использовать его в функции, которая отображает список пар и получает первый элемент
(: f (-> (Listof (Pairof Integer Symbol)) (Listof Integer))
Когда я пытаюсь написать свою функцию, как показано ниже, проверка типов не выполняется.
(define (f l) (map car l))
; stdin::9317: Type Checker: Polymorphic function `map' could not be applied to arguments:
; Types: (-> a c) (Pairof a (Listof a)) -> (Pairof c (Listof c))
; (-> a b ... b c) (Listof a) (Listof b) ... b -> (Listof c)
; Arguments: (All (a b) (case-> (-> (Pairof a b) a) (-> (Listof a) a))) (Listof (Pairof Integer Symbol))
; Expected result: (Listof Integer)
;
; in: (map car l)
Однако, если я оборачиваю функцию автомобиля в лямбда-выражение, которое приводит к указанию типа ввода как car, то моя реализация отлично проверяет тип
(define (f l) (map (lambda ([x : (Pairof Integer Symbol)]) (car x)) l))
Что именно здесь происходит и почему программа проверки типов недостаточно умна, чтобы сделать вывод из аннотации типа аргумента функции, что она должна использовать первый из двух случаев в функции car?
