How can we deal with typed/untyped interaction?

Our language boundary between typed and untyped is as the dotted line below.

Typed land
houston-talk.problem.typed
-----------------------------
Untyped land
houston-talk.problem.untyped

houston-talk.problem.untyped imports code from houston-talk.problem.untyped, so we need to safely import the untyped vars such that the type system is not violated by untyped code.

The first approach is simple to think about. Simply convert houston-talk.approach1.untyped to be fully typed and houston-talk.approach1.typed uses the inferred static types to determine safe usages of external vars.

Typed land
houston-talk.approach1.typed
houston-talk.approach1.untyped
-----------------------------
Untyped land

(require 'houston-talk.approach1.typed)

In this approach, we use t/untyped-var to assign expected types to imported vars.

Typed land
houston-talk.approach2.typed
-----------------------------
Untyped land
houston-talk.approach2.untyped

For example, in houston-talk.approach2.typed we write

(t/untyped-var u/a t/Int)

so that every occurrence of u/a is converted to

(cast Int u/a)

Notice, we can import vars to more sophisticated types, such as [Int :-> Int].

We can also relax the checking in our typed module.

Typed land
-----------------------------
Untyped land
houston-talk.approach3.typed
houston-talk.approach3.untyped

In the typed module we use the use the :runtime-check feature to convert our annotations to runtime checks.

This is not in core.typed 0.3.19, but here is a demo.

We basically ask core.typed to give us the annotations needed for approach 2.

We could feasibly always use this approach, but it breaks soundness (untyped vars can now flow anywhere!).

Copyright © 2015 Ambrose Bonnaire-Sergeant

Distributed under the Eclipse Public License either version 1.0 or (at your option) any later version.