sealing type aliases into opaque types with instances

[AlexKnauth]

What if a module declares a type alias:

M = (mod (type t = Int))

And you want to seal that module with a signature that makes it opaque:

S = (sig (type t))

But you also want to include an instance for that opaque type:

S = (sig (type t) (instance (Eq t)))

where Eq is a type class that has an instance (Eq Int).

In signature matching, does this match?

(sig (type t = Int))
matches?
(sig (type t) (instance (Eq t)))

If so, how do we deal with this?

P.S.

In Standard ML this matches:

(sig (type t = int))
matches
(sig (eqtype t))

[iitalics]

Sig matching this would be straightforward if we don't match instances pairwise. Instead, try an algorithm such as this:

• To determine S1 <: S2:
• For each instance in the given signature (S1), place this instance into the environment
• For each instance in the expected signature (S2), look up the instance in the environment (rather, the appropriate instance context)

The bigger problem is that now sealing requires further elaborating the module expression, specifically I mean we need to add the omitted instance (in your case (instance (Eq t))) into the sealed dictionary, since there was no reason for it to be there before.

[AlexKnauth]

Whatever we put in the data for a signature, it needs to be enough so that lookup-instance can produce a valid expression for the dictionary. It might produce a (hash-ref M ...) expression with the module hash-table and a unique name for the instance? Or could it produce another kind of expression that will do the right thing when it's sealed from an alias?

[iitalics]

We can't resolve instance dictionaries with a global table. In a functor they have to be resolved after the functor is applied:

(define-module F =
  (λ ([M : (sig (type T)
                (val x : T)
                (instance (Show T)))])
    ... (show M.x) ...))

(define-module M =
  (mod (type T = Int) (val x : T = 0)))

(F M) ;; how is (instance (Show Int)) communicated to the body of F?

[AlexKnauth]

When typechecking (resolve (inst show M.T)), the resolve macro calls lookup-instance with the constraint (Show M.T). It sees that the instance must come from M.T (as opposed to Show). We don't know whether M.T was originally an alias or a new type.

From F's point of view, the (Show M.T) instance comes from M.T's instance context. But from M's point of view, the (Show Int) instance comes from Show's instance context.

So what if T had an entry at run time in M's hash table, which pointed to, what? I don't know, because from M's point of view, the instance comes from Show's instance context. It's like F says "Go ask the module M", and M says "Go ask the typeclass Show", or something.

[iitalics]

This suggests that we can't determine at M's creation time, all the instances it will have:

(define-module M =
  (mod (type T = Int)))

(define-module NewContext =
  (mod
   (class (Local-C X))
   (instance (Local-C Int))
   ... (seal M :> (sig (type T) (instance (Local-C T))) ...))

Instead we might need a mutable vtable at runtime to lookup instances. Either that, or we would have to "fixup" module runtime expressions whenever we do signature matching.

[AlexKnauth]

So there are 3 phases or "times" involved:

• Compile time (functors stay independent)
• Link time (functors are applied and linked together with their arguments)
• Run time (the code inside modules and functors runs)

Having a mutable vtable at Run time would work, and it would probably be easier to implement. However, we should be able to resolve the instances before that at Link time. That would correspond to "fixing up" the modules at Link time when a functor is applied, which could happen before all of Run time if we needed that.

In practice, Link time will probably happen at the start of (Racket's notion of) run time anyway, so I'm not sure if the extra complexity is worth it. A mutable vtable would probably be easier.