Type inference helper for map
| (require typed-map) | package: typed-map-lib |
syntax
(map f l ...) → (Listof B)
f : (→ A ... B) l : (Listof A)
When f is a literal lambda of the form (λ (arg ...) body ...), it is not necessary to specify the type of the arguments, as they will be inferred from the list.
> (map (λ (x) (* x 2)) '(1 2 3)) - : (Listof Positive-Index)
'(2 4 6)
> (let ([l '(4 5 6)]) (map (λ (x) (* x 2)) l)) - : (Listof Positive-Index)
'(8 10 12)
This enables the use of #lang aful for map in Typed Racket.
Furthermore, when f is a polymorphic function, type annotations are not needed:
> (map car '([a . 1] [b . 2] [c . 3])) - : (Listof (U 'a 'b 'c))
'(a b c)
Compare this with the behaviour of map from racket/base, which generates a type error:
> (map car '([a . 1] [b . 2] [c . 3])) eval:1:0: Type Checker: Polymorphic function `map' could not
be applied to arguments:
Domains: (-> a b ... b c) (Listof a) (Listof b) ... b
(-> a c) (Pairof a (Listof a))
Arguments: (All (a b) (case-> (-> (Pairof a b) a) (->
(Listof a) a))) (List (Pairof 'a One) (Pairof 'b
Positive-Byte) (Pairof 'c Positive-Byte))
in: 3
When used as an identifier, the map macro expands to the original map from typed/racket/base:
It uses (reverse (reverse l)) to generalise the type of the list, without having to express that type, so that Type / Racket infers a more general type of the form (Listof A), without detecting that the output is identical to the input. An unoptimizable guard prevents the double-reverse from actually being executed, so it does not incur a performance cost.
It uses a named let to perform the loop. The function f is never passed as an argument to another polymorphic function, and is instead directly called with the appropriate arguments. The error message “Polymorphic function ‘map’ could not be applied to arguments” is therefore not raised.
To have the most precise and correct types, it uses a named let with a single variable containing the list (with the generalized type). An outer let binds a mutable accumulator, initialized with a single-element list containing the result of applying f on the first element of the list. Since all elements of the list belong to the generalized type, the result of calling f on any element has the same type, therefore the accumulator has the type (Listof B), where B is the inferred type of the result of f.
syntax
(foldl f init l ...) → Acc
f : (→ A ... Acc Acc) init : Acc l : (Listof A)
This form is implemented in the same way as the overloaded version of map presented above.
Note that in some cases, the type for the accumulator is not generalised enough based on the result of the first iteration, in which cases annotations are needed:
> (foldl (λ (x acc) (cons acc (add1 x))) '() '(1 2 3)) /home/root/user/.local/share/racket/snapshot/pkgs/typed-map-
lib/typed-map/main.rkt:79:34: Type Checker: type mismatch;
mutation only allowed with compatible types
expected: (Pairof Null Positive-Index)
given: (Pairof (Pairof Null Positive-Index)
Positive-Index)
in: (set! upcast-result (let-values (((x) (#%app car
temp3)) ((acc) upcast-result)) (#%app cons acc (#%app add1
x))))
> (foldl (λ (x [acc : (Rec R (U Null (Pairof R Positive-Index)))]) (cons acc (add1 x))) '() '(1 2 3)) - : (Pairof (Rec R (U (Pairof R Positive-Index) Null)) Positive-Index)
'(((() . 2) . 3) . 4)
syntax
(foldr f init l ...) → Acc
f : (→ A ... Acc Acc) init : Acc l : (Listof A)
This form is implemented in the same way as the overloaded version of map presented above.
Note that in some cases, the type for the accumulator is not generalised enough based on the result of the first iteration, in which cases annotations are needed. See the example given for foldl.