Re: [Caml-list] Encoding "links" with the type system

[Jeremy Yallop <yallop@gmail.com>]

Dear Andre,

On 21 September 2016 at 20:12, Andre Nathan <andre@digirati.com.br> wrote:
> I'm trying to encode links (an example would be directed graph edges)
> using the type system.
>
> The idea is to have types such as
>
>   module Source = struct
>     type 'a t = { name : string }
>     let create name = { name }
>   end
>
>   module Sink = struct
>     type 'a t = { name : string }
>     let create name = { name }
>   end
>
>   module Link = struct
>     type ('a, 'b) t = 'a Source.t * 'b Sink.t
>   end
>
>
> and then define a "link set" with the following characteristics:
>
> * You initialize a link set with a sink;
> * You can add links to set such that
>     * The first link's sink must be of the type of the sink;
>     * Additional links can have as sink types the original sink type
>       from the set creation, or the source types of previously added
>       links.
>
> In other words, if a set is created from a "t1 Sink.t", the first link
> on the set must be of type "t2 Source.t * t1 Sink.t", the second link
> can be either "t3 Source.t * t1 Sink.t" or "t3 Source.t * t2 Sink.t" and
> so on.
>
> Is it possible at all to encode such invariants using the type system?

It is!  Here's one approach, which is based on two ideas:

   1. generating a fresh, unique type for each set
      (the paper "Lightweight Static Capabilities" calls these "type
eigenvariables")

   2. an encoding of a set as a collection of evidence about membership.

I'll describe an interface based on these ideas that maintains the
properties you stipulate.  I'll leave the problem of building an
implementation that satisfies the interface to you.  (In fact, the
interface is the tricky part and the implementation is straightforward
if you can treat all the type parameters as phantom.)

First, we'll need types for the objects in the domain: sources, sinks,
sets and links.

  type _ source and _ sink and _ set and ('source, 'sink) link

Besides these we'll also need a type of membership evidence.  A value
of type '(sink, set) accepts' is evidence that 'set' will accept a
link with sink type 'sink':

  type ('sink, 'set) accepts

Then there are two operations on sets: creating a fresh set and adding
a link to a set.  In both cases the operation returns multiple values,
so I'll use records for the return types.  Furthermore, both
operations create fresh types (since sets have unique types), so I'll
use records with existential types.

First, here's the type of the result of the create_set operation:

  type 'sink fresh_set = Fresh_set :{    (* :{  *)
      set: 't set;
      accepts: ('sink, 't) accepts;
    } -> 'sink fresh_set

There's a type parameter 'sink, which'll be instantiated with the type
of the sink used to create the set, and two fields:

   1. 'set' is the new set
   2. 'accepts' is evidence that 'set' will accept a link with sink type 'sink'
      (or, if you like, a capability that will allow us to add such a link)

Note that 'sink is a type parameter, since we need to ensure that it
is the same as another type in the program (the sink used to create
the set), but 't is existential, since we need to ensure that it is
distinct from every other type in the program (since it uniquely
identifies 'set').

The create_set operation builds a fresh set from a sink:

  val create_set : 'sink sink -> 'sink fresh_set

Next, here's the type of the result of the add_link operation:

  type ('sink, 'parent) augmented_set = Augmented_set :{
      set: 't set;
      accepts: ('sink, 't) accepts;
      cc: 's. ('s, 'parent) accepts -> ('s, 't) accepts;
    } -> ('sink, 'parent) augmented_set

This time there are three elements to the result:
   1. 'set' is the new set (as before)
   2. 'accepts' is evidence that 'set' will accept a link with sink
type 'sink' (as before)
   3. 'cc' is a capability converter, that turns evidence that the
"parent" set will accept a link into evidence that 'set' will accept
the same link.

(Another of looking at this is that 'augmented_set' bundles the new
set up along with evidence that 'sink' is a member and evidence that
every member of the parent set is also a member.)

(And it's again worth looking at the scope of the type variables:
'sink and 'parent are parameters, since they correspond to the types
of inputs to the operation;  't is fresh, and 's is
universally-quantified, since the capability converter must work for
any piece of evidence involving the parent.)

The insert_link operation takes three arguments: the link to insert,
the set into which the link is inserted, and evidence that the
insertion is acceptable:

  val insert_link :
    ('source, 'sink) link ->  (* the link *)
    't set ->                 (* the set *)
    ('sink, 't) accepts ->    (* evidence that the set accepts the link *)
    ('source, 't) augmented_set

Here's the interface in action.  Let's assume that we have your sinks,
sources and links:

    type t1 and t2 and t3
    val snk1 : t1 sink
    val src1 : t2 source
    val src2 : t3 source
    val lnk1 : (t2, t1) link
    val lnk2 : (t3, t1) link
    val lnk3 : (t3, t2) link

Let's start by building a set from snk1:

    let Fresh_set { set = set; accepts = a } =
        create_set snk1 in

Now, since 'set' accepts links with sink type 't1' (as attested by
'a') we can insert a new link:

    let Augmented_set { set = set1; accepts = a1; cc = cc1 } =
        insert_link lnk1 set a in

We now have the following evidence available:

    'a' says that 'set' accepts 't1'
    'a1' says that 'set1' accepts 't2'
    'cc1' says that 'set1' accepts anything that 'set' accepts, and so
    'cc1 a' says that set1' accepts 't1'

and so we can insert links with sink type either 't1' or 't2' into 'set1':

    insert_link lnk3 set1 a1
    insert_link lnk2 set1 (cc1 a)

And, of course, since we can only insert links when we have evidence
that the set will accept them, there's no way to perform invalid
insertions.

One drawback of the above is a possible lack of efficiency, mostly
depending on how 'cc' is implemented.  In fact, there's also a
cost-free approach to capability conversions based on evidence
subtyping and private types, but I'll leave it as an exercise for the
reader.

I hope that helps!

Kind regards,

Jeremy.