[TYPES] Issues regarding typeclasses and modular languages like ML

[Derek Dreyer]

> Thanks for elucidating the relevance of [2] and [3] to my questions. If I've now understood things right, then I assume that in the example below (in the language of [3]), the sealing operation has actually done something quite interesting: not only has it created a new statically distinct type (t) but it has also created a new instance declaration (instance t C) that is implemented by the instance declaration (instance int C) inside M.
>
>
>   class 'a C with ...
>
>   structure M = struct
>      type t = int
>      instance int C with ...
>   end
>
>   structure N = M :> sig
>        type t
>        instance t C
>   end

Hmm...well, just to clarify: MTC does not include explicit "class" or
"instance" declarations...that's the whole point.

But you can certainly define a module M with a type t = int and a
substructure C_Int, let's say, of signature "C where type t = int".
Then, you can make M.C_Int the "canonical" instance of C at type int
via a "using" declaration.

Then, later on, you can define N as you did, except where "instance t
C" is replaced by "structure C_t : C where type t = t", and then make
N.C_t the "canonical" instance of C at type N.t (\neq int) via a
"using" declaration.  So in the end you have two non-overlapping
canonical instances of C whose t's are represented underneath by the
same representation type int.

Derek