A new way to type mutable data structures with opposite variance in typed racket

Show & Tell
7

After further analysis, it seems the root of this issue lies in how Typed Racket's
type checker works. When a function is called, the type checker knows the types
of both the arguments and parameters, so it can verify that the input matches the
expected type. However, after the function call, the type checker only knows the
declared return type, not the actual runtime type, since functions are treated as
"black boxes" in this context.

The Parameterof in Typed Racket addresses this issue in two ways:

  1. Static Type Enforcement in Typed Modules:
    In a Typed Racket module, make-parameter enforces that the "write type" must
    always be a subtype of the "read type":
Welcome to Racket v8.15 [cs].
> (: p (Parameter Any Number))
> (define p (make-parameter 'hi))
string:1:10: Type Checker: Polymorphic function `make-parameter' could not be applied to arguments:
Types: a  -> (Parameterof a)
       b (-> a b)  -> (Parameterof a b)
Arguments: 'hi
Expected result: (Parameterof Any Number)
  in: (make-parameter (quote hi))
 [,bt for context]
> (:print-type make-parameter)
(All (a b) (case-> (-> a (Parameterof a)) (-> b (-> a b) (Parameterof a b))))

Here, make-parameter ensures that 'hi cannot be used as an initial value for
a (Parameter Any Number).

  1. Contracts for Untyped Modules:
    For parameters imported from an untyped module, Typed Racket adds a contract to
    enforce the type at runtime. This ensures that any violation of the declared type
    is caught dynamically:
> (module m racket/base
    (provide q)
    (define q (make-parameter 'hi)))
> (require/typed 'm
    [q (Parameter Any Number)])
> (q)
q: broke its own contract
  promised: number?
  produced: 'hi
  in: the parameter of
      (parameter/c any/c number?)
  contract from: (interface for q)
  blaming: (interface for q)
   (assuming the contract is correct)
  at: string:2:3
 [,bt for context]
> (q 123)
> (q)
- : Number
123
> (q 'hi)
> (q)
q: broke its own contract
  promised: number?
  produced: 'hi
  in: the parameter of
      (parameter/c any/c number?)
  contract from: (interface for q)
  blaming: (interface for q)
   (assuming the contract is correct)
  at: string:2:3
 [,bt for context]

Here, the contract ensures that 'hi is flagged as invalid because it does not
conform to the expected Number type.

These two mechanisms together ensure that Parameter behaves correctly in both
typed and mixed-typed contexts.

1 Like