Type inference helper for map
map
foldl
foldr
7.0

Type inference helper for map

Georges Dupéron <[email protected]>

 (require typed-map) package: typed-map-lib

syntax

(map f l ...)  (Listof B)

  f : ( A ... B)
  l : (Listof A)
Like map from typed/racket/base, but with better type inference for Typed Racket.

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.

Examples:
> (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:

Example:
> (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:

Example:
> (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:

Examples:
> (require (only-in racket/base [map orig:map]))
> (equal? map orig:map)

- : Boolean

#t

Note that the implementation expands to a large expression, and makes use of set! internally to build the result list. The trick used proceeds as follows:
  • 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)
Like foldl from typed/racket/base but with better type inference for Typed Racket.

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:

Examples:
> (foldl (λ (x acc) (cons acc (add1 x))) '() '(1 2 3))

/home/racket/build-pkgs/user/.racket/7.0/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)
Like foldr from typed/racket/base but with better type inference for Typed Racket.

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.