Is it possible to unsafely assume sub-types in Typed Racket?

Questions & Answers
, ,
1

Typed Racket exposes unsafe primitives that make it possible to unsafely cast a value to an arbitrary type. Is it also possible to use existing unsafe utilities to somehow make Typed Racket assume that one type is another's subtype?

I imagine a few uses for such unsafe operation:

  • To implement GADT, where, within some scope, for example, we make Typed Racket assume that (Expr a) and (Expr Integer) are the same type
  • To encode higher-kinded polymorphism through type-level de-functionalization, where we make Typed Racket assume that a direct type application (e.g. (List a)) is the same as a spelled-out type application (Type-App List:Tag a)
1 Like
2

No, you can't permanently change the subtyping algorithm. That seems like it would impose some tricky implementation constraints.

1 Like