[MLton-user] a new approach to type-indexed values in SML

[Vesa Karvonen]

Quoting Stephen Weeks <sweeks at sweeks.com>:
> I've been thinking about how to define type-indexed values in a more
> modular/extensible way, closer to how Haskell type classes are done.
> The lack of first-class polymorphism in SML might make it seem
> impossible, but I've come up with an approach that I am happy with and
> I think will be useful in practice, once the initial infrastructure is
> digested.  The following note describes the approach.  I would be
> happy to answer questions or take feedback.

I still haven't had the time to really look into the implementation and
play with it, but I've reread your post and I believe I now have a
reasonable basic understanding of the approach.  I'll refer to this
technique as the "tiv-separating" technique, because it makes tivs
independent of the set of tycons, and the technique based on value
dependent encodings and pairing + lifting functors as the "tiv-pairing"
technique.  In this post I'll mainly compare the techniques.

The tiv-separating technique does, indeed, seem quite similar to the type
class mechanism.  Here is how I see the correspondence:

     type classes            ~    tiv-separating
    ----------------------------------------------------
      class                  ~     Tiv
      instance               ~     DefCase
      data/newtype           ~     Tycon
      (C1 a, ..., CN a) =>   ~     'a Type.t ->

There are differences, of course.  (The last line in the above table
ignores the possibility of using phantom witnesses.  The framework doesn't
really know anything about them.)

> This note shows a method to define tivs within SML that has the
> following properties:
> 
>   * There is a single representation of types as values and a
>     one-to-one correspondence between the SML type "t" and its
>     representation as a value of type "t Type.t".  Here are some
>     example values representing types.
> 
>       BoolTycon.ty: bool Type.t
>       ListTycon.ty BoolTycon.ty: bool list Type.t
>       ArrowTycon.ty (IntTycon.ty, BoolTycon.ty): (int -> bool) Type.t

IIUC, this property does not hold in general.  In particular it does not
hold for mutable (or imperative) types.  When one constructs a ti for a
mutable type (ref or array) the implementation may need to perform
side-effects.  If you build more than one ti for a mutable type you will
get multiple observationally different tis for that type.  IOW, the
construction of tis for mutable types is not, in general, referentially
transparent.  Thus for each mutable type "u", there can be more than one
representation of that type as a value of type "u Type.t".

[from another post]
> > However, when one wants to build a type-index for an imperative type
> > (ref or array) one sometimes really needs to perform a side-effect
> > and one needs to be able to control when side-effects occure.
> > Consider the show function for instance.  Cycle detection relies on
> > performing a side-effect.
> 
> I don't get your point here.  The cycle detection in show is not at
> tiv construction time, it happens once the value is supplied. [...]

Consider this snippet (from main.sml)

  val () =
     let
        val t = let open Type in array int end
        val r = dummy t
     in
        pl (show (Type.tuple2 (t, t)) (r, r))
     end

The output generated by the above snippet is:

  (@0=[|13, 13, 13|], #0)

Now, if we change it to

  val () =
     let
        val t  = let open Type in array int end
        val t' = let open Type in array int end
        val r = dummy t
     in
        pl (show (Type.tuple2 (t, t')) (r, r))
     end

we instead get the output

  (@0=[|13, 13, 13|], @1=[|13, 13, 13|])

So, we have two observationally distinguishable tis, t and t', for a
single type (int array).

>   * A tiv is a polymorphic function from (the representation of) types
>     to an ordinary SML value of the appropriate type.  For example,
>     equality has the following specification:
> 
>       val equals: 'a Type.t -> 'a * 'a -> bool

This also holds for the tiv-pairing technique.

>   * Users of tivs are statically prevented from making type errors.
>     For example, the following is a type error.
> 
>       equals BoolTycon.ty (13, 14)

This also holds for the tiv-pairing technique.

>   * A new type constructor of any arity can be defined at any 
>     toplevel-declaration point in the program, [...]

In the tiv-pairing technique tycons do not play a similar role.  In the
tiv-pairing technique new tis, whether they use new tycons or not, can be
defined at any "expression point" in the program.  No declaration is
necessary and no extra space (beyond evaluation of the ti expression) is
used (with the sole exception of registering handlers for new exception
constructors).

>    [...] and can subsequently be used to define tivs.

In the tiv-pairing technique, once you have a ti for a new type (whether
it uses a new tycon or not) you also have implementations of all the
(paired) tivs for that ti (whether it uses a new tycons or not).  There is
no need to subsequently define (or implement) the existing tivs for the ti
(whether it uses a new tycon or not).  Indeed, the set of specialized
tycons is fixed in the tiv-pairing technique.  New tycons are supported
through isomorphism.

This also means that defining a new tycon and using tivs with that tycon
does not cause a space leak.  (The only thing that may cause undesirable
space leaks is the registration of new exception (data) constructors.)

Indeed, the tiv-separating technique seems to support a kind of open
type-indexed values, while the tiv-pairing technique (is specifically
designed to) supports a kind of closed type-indexed values.  Due to the
way tycons need to be "registered" with the framework, I'm not entirely
sure whether one can build a framework for closed type-indexed values on
top of the tiv-separating framework.  Is it possible?

>   * Type constructors for mutable types (array, ref, etc.) and
>     recursive types (list) are supported as well as type constructors
>     for nonrecursive immutable types (option) and ground types (bool,
>     int, etc.).

The tiv-pairing technique only supports specializing tivs for a fixed set
of tycons.  However, as the fixed set of tycons is chosen carefully, one
can embedd all other tycons into that fixed set through appropriately
defined isomorphisms (and embeddings).  Also, it is possible to perform a
posteriori specialization of tivs given a ti by performing a functional
record update on the ti.  For example, here is the (current, likely to
change slightly) signature of the Arbitrary tiv from our utility library:

signature ARBITRARY =
   sig
      type 'a arbitrary_t

      val arbitrary : 'a arbitrary_t -> 'a RanQD1Gen.gen
      (** Extracts the random value generator. *)

      val withGen : 'a RanQD1Gen.gen -> 'a arbitrary_t uop
      (** Functionally updates the random value generator. *)
   end

The withGen function is there to allow one to (functionally) replace the
generator with a custom generator.  (The functions in the above signature
are lifted to the combined type-index using functors.)  To generate sorted
lists, for example, one can write (this is from example test code):

   val sortedList : int list Type.t =
       let
          val l = list int
       in
          withGen (RanQD1Gen.prj (arbitrary l) stableSort) l
       end

One can then use the specialized ti to specify tests (again from example
test code):

          (chk (all (int &` sortedList)
                    (fn x & xs =>
                        that o isSorted |< insert x xs)))

(The above is basically a translation of the last example (prop_Insert) in
section 2.4 of the ICFP'00 QuickCheck paper.  You can read the above as:

  "Check for all pairs of an integer x and a sorted list of integers xs
   that inserting x into xs results in a sorted list.")

>   * A new tiv can be declared at any toplevel-declaration point
>     in the program. 

This doesn't hold for the tiv-pairing technique.  If one wants to use a
set of tivs through a single ti, the individual tivs need to be defined
before they are paired into the combined tiv and before the single ti is
constructed.  While I agree that this is clearly an important issue and
the tiv-separating framework is superior in this respect, I'm not sure how
big of an issue this really is from a practical pov.

There are two extreme scenarios.  In one extreme scenario there is only a
small number of really globally useful, and usually nearly total, tivs and
those tivs can be easily defined in a library.  The other less useful, and
usually partial or otherwise specialized, tivs are only used in localized
cases and it is not a huge practical problem that combining those with the
globally useful tivs requires more effort.  In the other scenario there is
a large number of globally useful tivs that everyone wants to use and new
tivs pop up every week or so.  If this is the case, then the tiv-pairing
technique can become somewhat painful.  In the worst case you would
probably need to functorize everything that wants to use tivs.

The more specialized (locally useful) tivs are often partial.  For such
tivs neither framework provides particularly good support.  Our (small
SML) code base currently has one such specialized tiv.  The tis (or, more
accurately, type-index constructors) used by that tiv do not really follow
the SML type system but rather follow the types of a particular C library.
However, inside the implementation, we build a ti of the combined utility
lib on the side and provide access to it for convenience.  So, after
you've built the specialized ti, you can get the combined ti of the
utility lib by calling a function with a spec of the form:

      val getType : 'a SpecializedPartialType.t -> 'a Type.t

>   * A tiv is inductively defined over type constructors by a global
>     collection of rules, with at most one rule for each type
>     constructor.

In the tiv-pairing technique tycons do not play a similar role.

>   * The inductive rule for a particular tiv and a particular type
>     constructor can be given at any toplevel-declaration point in the
>     program after the tiv and type constructor have been defined.  In
>     particular, one need neither group together all the rules for a
>     tiv nor group together all the rules for a type constructor.

In the tiv-pairing technique, the fixed set of rules for a given tiv are
grouped together.  On the other hand, the fixed set of rules is generally
sufficient to implement the tiv for all tis whether or not the new tis use
new tycons or not.  Tycons do not play a similar role in the tiv-pairing
technique.

The cost (in source code size) of the tiv-pairing technique is O(m+n)
where m is the number of tivs and n is the number of tis.  IIUC, the cost
of the tiv-separating technique, at least when used in its full
generality, is O(m*k+n) where m is the number of tivs, k is number of
tycons, and n is the number of tis.

>   * Each inductive rule is specified by a polymorphic function,
>     checked by the SML type system, mapping type(s) corresponding to
>     the type constructor's arguments to a value of the desired type.
>     An inductive rule for a tiv may refer to the same tiv, other tivs,
>     both, or neither.  This is done by applying the necessary tivs to
>     the supplied types in the body of the rule.  For example, the
>     equality rule for options is as follows.
> 
>       val rule: 'a Type.t -> 'a option * 'a option -> bool =
>          fn t =>
>          let
>             val eltEquals = equals t
>          in
>             fn (NONE, NONE) => true
>              | (SOME x, SOME y) => eltEquals (x, y)
>              | _ => false
>          end

This does not hold in the same way for the tiv-pairing technique.  While
it is possible to use previously defined tivs to define a particular tiv,
one needs to explicitly build the tis of the previously defined tivs on
the side.  One could probably make some utilities (functors) to make it
easier.

>   * The infrastructure automatically applies the inductive rules to
>     build a tiv indexed at a particular type.

In the tiv-pairing technique, evaluation of the ti expression builds all
the tivs for that ti.  In many cases the compiler should be able to drop
unused elements (unused tivs) from the product.  There is no lookup
overhead to access a particular tiv given a ti.

>   * Different tivs can be combined and used at the same type index.

The tiv-pairing technique also makes this possible through the use of
functors, although the particular (combined) set of tivs needs to defined
at some specific point in the program.  Currently our utility lib has a
combined Type module:

structure Type :>
   sig
      include TYPE

      (** == STRUCTURAL TYPE-INDEXED VALUES == *)

      include ARBITRARY
      (* ... *)

      (** == NOMINAL TYPE-INDEXED VALUES == *)

      include SHOW
      (* ... *)

      (* Sharing constraints *)

      sharing type t
                 = arbitrary_t
                 (* ... *)
                 = show_t
                 (* ... *)
      sharing type s
                 = show_s
                 (* ... *)
      sharing type p
                 = show_p
                 (* ... *)
   end = struct
     (* ... *)
   end

In order to add a new tiv, one needs to modify the signature and the
implementation of the structure, which is clearly undesirable.  OTOH,
there only seems to be a handful of really globally useful tivs that fit
nicely into the framework, so while the need to modify code to add new
tivs is unfortunate, I don't see this as a major problem, because there
isn't going to be an avalanche of new tivs (or so I believe).

If we would functorise the modules that use tivs, we could push the ad hoc
combination of tivs to the applications and make the library code
independent of the combined set of tivs.  I'm not sure if that kind of
flexibility is really needed.

>   * Because the sets of tivs and type constructors are open and the
>     inductive rules can be defined anywhere (or not at all), it is
>     dynamically checked whether the application of a tiv to a type
>     succeeds.  If needed, one can layer phantom witnesses on top to
>     statically ensure safety.

This aspect works differently in the tiv-pairing technique.  While one can
have partial functions in the tiv-pairing technique, there is no lookup of
rules, so dynamic checks in the same sense aren't needed.  All the "rules"
(structural cases) are defined as a group.

However, as a tiv becomes more and more specialized it makes less and less
sense to define it in terms of a framework designed to encompass the
entire SML type system.  For example, in the one specialized tiv (it is an
application specific tiv) that we have ATM, there are two different
notions of products.  One notion is like tuples (positional elements)
while the other is like records with optional elements (labelled option
elements).  While there is a trivial mapping from the specialized tis to
the utility lib tis (remember getType above), there is no simple mapping
from utility lib tis to the specialized tis.

>   * The application of a tiv to a type is staged so that one can
>     cache the application of the inductive rules and so that one can
>     get early (dynamic) warning if a tiv is not defined for a
>     particular type.

Similar caching isn't needed in the tiv-pairing technique as there is no
lookup.  There also is no need for similar dynamic "warnings" as all the
"rules" (structural cases) for a tiv are grouped together so for each tiv
one can document in one place which kinds of tis will/will not work.

>   * Because rules can be defined anywhere, it is dynamically checked
>     whether there have been multiple definitions of a rule for the
>     same tiv and type constructor.

In the tiv-pairing technique all the "rules" (structural cases) for a tiv
are collected together so there is no need for similar dynamic checks.

>   * The implementation of tivs uses an extensible universal type
>     underneath.  The only uses of a universal type use constant-time
>     wrap and unwrap functions.

The tiv-pairing technique doesn't use such a universal type.  However, one
does need to provide (to the iso combinator whose purpose is to support
user defined types) isomorphisms between the types used in tis and
encodings of those types as generic sums and products (and arrows,
etc...).

>   * The implementation is portable SML and uses no unsafe features or
>     extensions.

The same holds for the tiv-pairing technique.

[...]

At any rate, it seems to me that neither approach is clearly superior.
The tiv-separating technique is definitely more flexible than the
tiv-pairing technique, but the extra flexibility doesn't come for free.

-Vesa Karvonen