Почему `filter` работает с типизацией более высокого порядка?

На главной странице Racket они показывают этот пример:

#lang typed/racket
;; Using higher-order occurrence typing
(define-type SrN (U String Number))
(: tog ((Listof SrN) -> String))
(define (tog l)
  (apply string-append (filter string? l)))
(tog (list 5 "hello " 1/2 "world" (sqrt -1)))

Я знаю, что при вводе вхождения такое выражение, как (if (string? v) ...), пометит v как имеющее тип String в истинной ветви. Это потому, что тип string? имеет фильтр:

> string?
- : (Any -> Boolean : String)
#<procedure:string?>

Таким образом, для того, чтобы «вхождение вхождения более высокого порядка» работало с функцией filter, я ожидаю, что тип filter скажет, что фильтр по типу предиката распространяется на тип результата. Но когда я проверяю тип filter в REPL, это не отображается:

> filter
- : (All (a b) (case-> ((a -> Any) (Listof a) -> (Listof b)) ((a -> Any) (Listof a) -> (Listof a))))
#<procedure:filter>

Но это не может быть настоящий тип filter, потому что на b нет ограничений! Я ожидал что-то вроде

(All (a b) (a -> Any : b) (Listof a) -> (Listof b))

tldr: почему filter имеет переменную неограниченного типа в возвращаемом типе?

РЕДАКТИРОВАТЬ: я использую Racket v6.0


higher-order-functions racket typed-racket type-theory
person dpercy    schedule 21.11.2015    source источник
comment
Похоже, вы используете более старую версию Racket, которая не печатает дополнительную информацию о фильтре типа на filter. Если вы обновитесь, вы увидите тип, который Ренцо показывает в своем ответе.   -  person Asumu Takikawa    schedule 21.11.2015

Ответы (1)


arrow_upward
4
arrow_downward

В Typed Racket Ссылка сказано:

В некоторых случаях в фильтрах полезна информация об асимметричном типе. Например, первый аргумент функции filter указан только с положительным фильтром. Пример:

> filter
- : (All (a b)
      (case->
       (-> (-> a Any : #:+ b) (Listof a) (Listof b))
       (-> (-> a Any) (Listof a) (Listof a))))
#<procedure:filter>

Использование #:+ указывает, что когда функция, примененная к переменной, дает истинное значение, данный тип может быть принят для переменной. Однако средство проверки типов не получает информации в ветвях, в которых результат равен #f.

Другими словами, если у вас есть следующий пример:

> (filter string? '(symbol 1 2 3 "string"))
- : (Listof String)
'("string")

система может сказать, что элемент списка '(symbol 1 2 3 "string") имеет тип String только тогда, когда string? возвращает для него true. Только в этом случае распространяется тип предиката фильтра.

person Renzo    schedule 21.11.2015