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

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

[Andre Nathan]

[-- Attachment #1.1: Type: text/plain, Size: 2209 bytes --]

Hi

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? I
couldn't get past something like

  module Set = struct
    type _ t =
      | S : 'a Sink.t -> 'a t
      | L : 'a t * ('b, 'a) Link.t -> ('a * 'b) t
    let create sink = S sink
    let add_link link set = L (set, link)
  end

This allows me to insert the first link:

  type t1
  type t2
  type t3

  let _ =
    let snk1 : t1 Sink.t = Sink.create "sink1" in
    let set = Set.create snk1 in

    let src1 : t2 Source.t = Source.create "source1" in
    let lnk1 = (src1, snk1) in
    let set1 = Set.add_link lnk1 set in
    ...

but now "set1" has type "(t1 * t2) Set.t" and I can't call "add_link" on
it anymore:

    ...
    let src2 : t3 Source.t = Source.create "source2" in
    let lnk2 = (src2, snk1) in
    let set2 = Set.add_link lnk2 set1 in
    ...

which gives me "This expression has type (t1 * t2) Set.t but an
expression was expected of type t1 Set.t" when passing "set1" to "add_link".

I also tried to come up with a solution using difference lists for the
set but hit basically the same problem as above.

Any help would be appreciated.

Thanks,
Andre


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

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

[Jeremy Yallop]

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.

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

[Andre Nathan]

[-- Attachment #1: Type: text/plain, Size: 336 bytes --]

> Em 21 de set de 2016, às 19:22, Jeremy Yallop <yallop@gmail.com> escreveu:
> It is!  Here's one approach, which is based on two ideas:

Wow, there's a lot to digest here :) Most of it is new to me, including the use of "evidence" types... I'll have to re-read it and try to work it out after a night of sleep.

Thanks,
Andre 

[-- Attachment #2: Type: text/html, Size: 1432 bytes --]

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 2380 bytes --]

I came back to this thread thanks to Alan Schmitt's Caml Weekly News.

Here is a fairly systematic approach to the problem, contrasting Jeremy's
more virtuoso approach. It works well when the whole set is statically
defined in the source code, but I'm not sure about more dynamic scenarios
(when a lot of the type variables involved become existentially quantified.

The idea is to first formulate a solution using logic programming. A link
set can be represented as a list of accepted sinks, and I can write a small
Prolog program, "insert" that takes a new link, and a link set, and
traverses the link set to find the link's sink in the list, and add the
link's source to the list in passing.

   set([sink]) :- link(source, sink).
   set(sinks) :-
     set(prev_sinks),
     link(source, sink),
     insert(prev_sinks, source, sink, sinks).

   (* either the sink we want to insert is first in the list *)
   insert([sink | _], source, sink, [source, sink | sinks]).

   (* or it is to be found somewhere, recursively, under some other sink
[s] *)
   insert([s | prev_sinks], source, sink, [s | sinks]) :-
     insert(prev_sinks, source, sink, sinks).

Once you have this logic program, it is straightforward to translate it to
a GADT declaration:

type 's linkset =
  | Init : ('source, 'sink) link -> ('source -> ('sink -> unit)) linkset
  | Insert : ('source, 'sink) link * 'set1 linkset * ('set1, 'source,
'sink, 'set2) insert -> 'set2 linkset
and ('set1, 'source, 'sink, 'set2) insert =
  | Here : (('sink -> _) as 'set1, 'source, 'sink, 'source -> 'set1) insert
  | Next : ('set1, 'source, 'sink, 'set2) insert -> ('a -> 'set1, 'source,
'sink, 'a -> 'set2) insert

let _ = fun (type t1 t2 t3) (lnk1 : (t2, t1) link) (lnk2 : (t3, t1) link)
(lnk3 : (t3, t2) link) ->
  let set = Init lnk1 in
  let set = Insert (lnk2, set, Next Here) in
  let set = Insert (lnk3, set, Here) in
  set


On Wed, Sep 21, 2016 at 8:50 PM, Andre Nathan <andre@digirati.com.br> wrote:

> Em 21 de set de 2016, às 19:22, Jeremy Yallop <yallop@gmail.com> escreveu:
>
> It is!  Here's one approach, which is based on two ideas:
>
>
> Wow, there's a lot to digest here :) Most of it is new to me, including
> the use of "evidence" types... I'll have to re-read it and try to work it
> out after a night of sleep.
>
> Thanks,
> Andre
>
>

[-- Attachment #2: Type: text/html, Size: 4041 bytes --]

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

[Andre Nathan]

[-- Attachment #1.1: Type: text/plain, Size: 3814 bytes --]

Hi Gabriel

This is an interesting way to derive the GADT, at least for me, as I
have never did any logic programming. The resulting API is a bit easier
to use than the one from Jeremy's idea, at least for my use case.

I'm using this idea to experiment with a type-safe SQL query builder,
which so far looks like this:

  from Team.table
    |> belonging_to Team.owner   Here
    |> having_one Project.leader Here
    |> select
        |> fields [field User.id; field User.name] (Next Here)
        |> fields [field Team.id; field Team.name] (Next (Next Here))
        |> fields [all Project.table]              Here

This generates the following query:

  SELECT
    users.id, users.name,
    teams.id, teams.name,
    projects.*
  FROM
    teams
  LEFT JOIN
    users ON users.id = teams.owner_id
  LEFT JOIN
    projects ON projects.leader_id = users.id

I'm not sure if this will ever be of use in practice, as the Next/Here
stuff might be too complicated for users, but overall I'm quite happy
with the result and what I've learned, though of course it's far from
complete (e.g. no support for WHERE clauses).

Thanks for the hints!

Andre

On 09/30/2016 10:54 AM, Gabriel Scherer wrote:
> I came back to this thread thanks to Alan Schmitt's Caml Weekly News.
> 
> Here is a fairly systematic approach to the problem, contrasting
> Jeremy's more virtuoso approach. It works well when the whole set is
> statically defined in the source code, but I'm not sure about more
> dynamic scenarios (when a lot of the type variables involved become
> existentially quantified.
> 
> The idea is to first formulate a solution using logic programming. A
> link set can be represented as a list of accepted sinks, and I can write
> a small Prolog program, "insert" that takes a new link, and a link set,
> and traverses the link set to find the link's sink in the list, and add
> the link's source to the list in passing.
> 
>    set([sink]) :- link(source, sink).
>    set(sinks) :-
>      set(prev_sinks),
>      link(source, sink),
>      insert(prev_sinks, source, sink, sinks).
> 
>    (* either the sink we want to insert is first in the list *)
>    insert([sink | _], source, sink, [source, sink | sinks]).
> 
>    (* or it is to be found somewhere, recursively, under some other sink
> [s] *)
>    insert([s | prev_sinks], source, sink, [s | sinks]) :-
>      insert(prev_sinks, source, sink, sinks).
> 
> Once you have this logic program, it is straightforward to translate it
> to a GADT declaration:
> 
> type 's linkset =
>   | Init : ('source, 'sink) link -> ('source -> ('sink -> unit)) linkset
>   | Insert : ('source, 'sink) link * 'set1 linkset * ('set1, 'source,
> 'sink, 'set2) insert -> 'set2 linkset
> and ('set1, 'source, 'sink, 'set2) insert =
>   | Here : (('sink -> _) as 'set1, 'source, 'sink, 'source -> 'set1) insert
>   | Next : ('set1, 'source, 'sink, 'set2) insert -> ('a -> 'set1,
> 'source, 'sink, 'a -> 'set2) insert
> 
> let _ = fun (type t1 t2 t3) (lnk1 : (t2, t1) link) (lnk2 : (t3, t1)
> link) (lnk3 : (t3, t2) link) ->
>   let set = Init lnk1 in
>   let set = Insert (lnk2, set, Next Here) in
>   let set = Insert (lnk3, set, Here) in
>   set
> 
> 
> On Wed, Sep 21, 2016 at 8:50 PM, Andre Nathan <andre@digirati.com.br
> <mailto:andre@digirati.com.br>> wrote:
> 
>     Em 21 de set de 2016, às 19:22, Jeremy Yallop <yallop@gmail.com
>     <mailto:yallop@gmail.com>> escreveu:
>>     It is!  Here's one approach, which is based on two ideas:
> 
>     Wow, there's a lot to digest here :) Most of it is new to me,
>     including the use of "evidence" types... I'll have to re-read it and
>     try to work it out after a night of sleep.
> 
>     Thanks,
>     Andre 
> 
> 



[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

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

[Daniel Bünzli]

On Wednesday 5 October 2016 at 21:46, Andre Nathan wrote:
> I'm using this idea to experiment with a type-safe SQL query builder,
> which so far looks like this:

You may be interested in looking at this 

http://okmij.org/ftp/meta-programming/#QUEL

Best,

Daniel

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

[Shayne Fletcher]

[-- Attachment #1: Type: text/plain, Size: 1677 bytes --]

On Wed, Sep 21, 2016 at 6:22 PM, Jeremy Yallop <yallop@gmail.com> wrote:

> 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.)
>

​How's this?

module M : S = struct

  type _ sink = { name : string }
  type _ source = { name : string }
  type _ set = (string * string) list
  type ('source, 'sink) link = ('source source * 'sink sink)

  type ('sink, 'set) accepts =
  | Accepts : ('sink, 'set) accepts

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

  let create_set (s : 'sink sink) : 'sink fresh_set =
    Fresh_set { set = ([] : 't set);
                accepts = (Accepts : ('sink, 't) accepts) }

  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

  let insert_link
      (l : ('source, 'sink) link)
      (s : 't set)
      (a : ('sink, 't) accepts)  : ('source, 't) augmented_set =
    let ({name = src}, {name = dst}) = l in
    Augmented_set {
      set : 'tt set = (src, dst) :: s;
      accepts = (Accepts : ('source, 'tt) accepts);
      cc = fun (_ : (_, 't) accepts) -> (Accepts : (_, 't) accepts)
    }

end
​
​This melts my brain Jeremy! :)

-- 
Shayne Fletcher

[-- Attachment #2: Type: text/html, Size: 5339 bytes --]

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

[Shayne Fletcher]

[-- Attachment #1: Type: text/plain, Size: 5922 bytes --]

On Fri, Oct 7, 2016 at 1:02 PM, Shayne Fletcher <
shayne.fletcher.50@gmail.com> wrote:

> On Wed, Sep 21, 2016 at 6:22 PM, Jeremy Yallop <yallop@gmail.com> wrote:
>
>> 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.)
>>
>
> ​How's this?
>
> module M : S = struct
> ...
>
​
I've hit a problem with my attempt at an implementation actually :(

The issue is, the program below as written seems to work, but, if the type
[_ set] is made abstract in the signature [S], typing breaks. Can somebody
explain where I'm going wrong?

module type S = sig

  type _ sink
  type _ source
  type _ set = (string * string) list (*Why can't this be abstract?*)
  type ('source, 'sink) link

  type ('sink, 'set) accepts

  val mk_sink : string -> 'sink sink
  val mk_source : string -> 'source source
  val mk_link : 'source source * 'sink sink -> ('source, 'sink) link

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

  val create_set : 'sink sink -> 'sink fresh_set

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

  val insert_link :
    ('source, 'sink) link ->
    'parent set ->
    ('sink, 'parent) accepts ->
    ('source, 'parent) augmented_set

end

module M : S = struct

  type 'sink sink = { name : string }
  type 'source source = { name : string }

  type 'set set = (string * string) list
  type ('source, 'sink) link = ('source source * 'sink sink)

  let mk_sink (name : string) : 'sink sink = {name}
  let mk_source (name : string) : 'source source = {name}
  let mk_link ((source, sink) : 'source source * 'sink sink)
      : ('source, 'sink) link = (source, sink)

  type ('sink, 'set) accepts =
  | Accepts : ('sink, 'set) accepts

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

  let create_set (s : 'sink sink) : 'sink fresh_set =
    Fresh_set { set = ([] : 'set set);
                accepts = (Accepts : ('sink, 'set) accepts) }

  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

  let insert_link
      (l : ('source, 'sink) link)
      (s : 'parent set)
      (a : ('sink, 'parent) accepts)  : ('source, 'parent) augmented_set =
    let {name = src} : 'source source = fst l in
    let {name = dst} : 'sink sink  = snd l in
    Augmented_set {
      set : 't set = (src, dst) :: s;
      accepts = (Accepts : ('source, 't) accepts);
      cc = fun (_ : (_, 'parent) accepts) -> (Accepts : (_, 'parent)
accepts)
    }

end

module Test (E : S) = struct

  open E

  type t1 and t2 and t3 and t4

  let snk1 : t1 sink = mk_sink "sink1"
  let snk2 : t2 sink = mk_sink "sink2"
  let snk3 : t4 sink = mk_sink "sink3"

  let src1 : t2 source = mk_source "source1"
  let src2 : t3 source = mk_source "source2"

  let link1 : (t2,  t1) link = mk_link (src1, snk1) (*t2 src, t1 sink*)
  let link2 : (t3,  t1) link = mk_link (src2, snk1) (*t3 src, t1 sink*)
  let link3 : (t3,  t2) link = mk_link (src2, snk2) (*t3 src, t2 sink*)
  let link4 : (t3,  t4) link = mk_link (src2, snk3) (*t3 src, t4 sink*)

  let test () =

    (*Create a fresh set from a sink of type [t1]*)
    let (Fresh_set {set; accepts = a} : t1 fresh_set) =
      create_set snk1 in
    (*
      - [a] is evidence [set] accepts links with sink type [t1]
    *)

    (*Insert a [(t2, t1) link]*)
    let Augmented_set
        {set = set1; accepts = a1; cc = cc1} =
      insert_link link1 set a in
    (*
      - [a1] is evidence [set1] accepts links with sink type [t2] ([t2] is
        the source type of [link1])
      - [cc] says that [set1] accepts links with sink types that its
        parent [set] does:
        - [cc1 a] provides evidence that says that [set1] will accept
          [link2] which has sink type [t1] *)

    (*Insert a [(t3, t1)] link*)
    let Augmented_set
        {set = set2; accepts = a2; cc = cc2} =
      insert_link link2 set (cc1 a) in
    (*
      - [a2] says that [set2] accepts links with sink type [t3] ([t3] is
        the source type of [link2])
        - [cc2] says that [set2] accepts links with sink types that its
          parent does:
        - [cc2 a1] provides evidence that says that [set2] will accept
          [link3] which has sink type [t2]
    *)

    (*Insert a [(t3, t2)] link*)
    let (Augmented_set
        {set = set3; accepts = a3; cc = cc3} : (t3, _) augmented_set) =
      insert_link link3 set (cc2 a1) in
    (*
      - [a3] says that [set3] accepts links with sink type [t3] ([t3]is
        the source type of [link3])
      - [cc3] says that [set3] accepts links with sink types that its
        parent does (that is, any links with sink types [t1], [t2] or [t3])
    *)

    (*There is just no way we can get insert [link4] into [set3]. The
      is no evidence we can produce that will allow a link with sink
      type [t4]. Try the below with any of [a1], [a2], [a3])*)
    (*
    let (Augmented_set
       {set = set4; accepts = a4; cc = cc4} =
       insert_link link4 set (cc3 a3) : (t3, _) augmented_set) in
    *)

    ()
end

let _ = let module T = Test (M) in T.test ()

-- 
Shayne Fletcher

[-- Attachment #2: Type: text/html, Size: 19233 bytes --]

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

[Jacques Garrigue]

On 2016/10/09 06:51, Shayne Fletcher wrote:
> 
> On Fri, Oct 7, 2016 at 1:02 PM, Shayne Fletcher <shayne.fletcher.50@gmail.com> wrote:
> On Wed, Sep 21, 2016 at 6:22 PM, Jeremy Yallop <yallop@gmail.com> wrote:
> 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.)
> 
> ​How's this?
> 
> module M : S = struct
> ...
> ​
> I've hit a problem with my attempt at an implementation actually :(
> 
> The issue is, the program below as written seems to work, but, if the type [_ set] is made abstract in the signature [S], typing breaks. Can somebody explain where I'm going wrong?

Making a type abstract loses some information (independently of hiding the precise definition):
* its uniqueness (i.e. it could be equal to any other type)
* its injectivity (i.e. whether "t1 t = t2 t” implies “t1 = t2”)
* its contractiveness (i.e. whether “t1 t” might actually be equal to to “t1”)
All of these properties have an impact of the behavior of type indices of GADTs.

If you want to use a type as GADT index, it is fine to hide the actual implementation, but it
is better to have a visible constructor.
For instance, you could define in the interface:

	type set_impl
	type _ set = private Set of set_impl  (* private ensure that the type parameter is invariant *)

and in the implementation:

	type set_impl = (string * string) list
	type _ set = Set of set_impl

Jacques

> module type S = sig
> 
>   type _ sink
>   type _ source
>   type _ set = (string * string) list (*Why can't this be abstract?*)
>   type ('source, 'sink) link
> 
>   type ('sink, 'set) accepts 
> 
>   val mk_sink : string -> 'sink sink
>   val mk_source : string -> 'source source
>   val mk_link : 'source source * 'sink sink -> ('source, 'sink) link
> 
>   type 'sink fresh_set = 
>   | Fresh_set : {
>     set : 'set set;
>     accepts : ('sink, 'set) accepts;
>   } -> 'sink fresh_set
> 
>   val create_set : 'sink sink -> 'sink fresh_set
> 
>   type ('sink, 'parent) augmented_set =
>   | Augmented_set : {
>     set : 'set set;
>     accepts: ('sink, 'set) accepts;
>     cc : 's. ('s, 'parent) accepts -> ('s, 'set) accepts
>   } -> ('sink, 'parent) augmented_set
> 
>   val insert_link : 
>     ('source, 'sink) link ->
>     'parent set -> 
>     ('sink, 'parent) accepts ->
>     ('source, 'parent) augmented_set
> 
> end
> 
> module M : S = struct
> 
>   type 'sink sink = { name : string }
>   type 'source source = { name : string }
> 
>   type 'set set = (string * string) list
>   type ('source, 'sink) link = ('source source * 'sink sink)
> 
>   let mk_sink (name : string) : 'sink sink = {name}
>   let mk_source (name : string) : 'source source = {name}
>   let mk_link ((source, sink) : 'source source * 'sink sink) 
>       : ('source, 'sink) link = (source, sink)
> 
>   type ('sink, 'set) accepts = 
>   | Accepts : ('sink, 'set) accepts
> 
>   type 'sink fresh_set = 
>   | Fresh_set : {
>     set : 'set set;
>     accepts : ('sink, 'set) accepts; 
>     }                        -> 'sink fresh_set
> 
>   let create_set (s : 'sink sink) : 'sink fresh_set =
>     Fresh_set { set = ([] : 'set set); 
>                 accepts = (Accepts : ('sink, 'set) accepts) }
>   
>   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
> 
>   let insert_link 
>       (l : ('source, 'sink) link) 
>       (s : 'parent set)
>       (a : ('sink, 'parent) accepts)  : ('source, 'parent) augmented_set =
>     let {name = src} : 'source source = fst l in
>     let {name = dst} : 'sink sink  = snd l in
>     Augmented_set {
>       set : 't set = (src, dst) :: s;
>       accepts = (Accepts : ('source, 't) accepts);
>       cc = fun (_ : (_, 'parent) accepts) -> (Accepts : (_, 'parent) accepts)
>     }
> 
> end
> 
> module Test (E : S) = struct
> 
>   open E
> 
>   type t1 and t2 and t3 and t4
> 
>   let snk1 : t1 sink = mk_sink "sink1"
>   let snk2 : t2 sink = mk_sink "sink2"
>   let snk3 : t4 sink = mk_sink "sink3"
> 
>   let src1 : t2 source = mk_source "source1"
>   let src2 : t3 source = mk_source "source2"
> 
>   let link1 : (t2,  t1) link = mk_link (src1, snk1) (*t2 src, t1 sink*)
>   let link2 : (t3,  t1) link = mk_link (src2, snk1) (*t3 src, t1 sink*)
>   let link3 : (t3,  t2) link = mk_link (src2, snk2) (*t3 src, t2 sink*)
>   let link4 : (t3,  t4) link = mk_link (src2, snk3) (*t3 src, t4 sink*)
> 
>   let test () = 
> 
>     (*Create a fresh set from a sink of type [t1]*)
>     let (Fresh_set {set; accepts = a} : t1 fresh_set) = 
>       create_set snk1 in
>     (*
>       - [a] is evidence [set] accepts links with sink type [t1]
>     *)
> 
>     (*Insert a [(t2, t1) link]*)
>     let Augmented_set 
>         {set = set1; accepts = a1; cc = cc1} = 
>       insert_link link1 set a in
>     (*
>       - [a1] is evidence [set1] accepts links with sink type [t2] ([t2] is
>         the source type of [link1])
>       - [cc] says that [set1] accepts links with sink types that its
>         parent [set] does:
>         - [cc1 a] provides evidence that says that [set1] will accept
>           [link2] which has sink type [t1] *)
> 
>     (*Insert a [(t3, t1)] link*)
>     let Augmented_set
>         {set = set2; accepts = a2; cc = cc2} =
>       insert_link link2 set (cc1 a) in
>     (*
>       - [a2] says that [set2] accepts links with sink type [t3] ([t3] is
>         the source type of [link2])
>         - [cc2] says that [set2] accepts links with sink types that its
>           parent does:
>         - [cc2 a1] provides evidence that says that [set2] will accept
>           [link3] which has sink type [t2]
>     *)
> 
>     (*Insert a [(t3, t2)] link*)
>     let (Augmented_set
>         {set = set3; accepts = a3; cc = cc3} : (t3, _) augmented_set) =
>       insert_link link3 set (cc2 a1) in
>     (*
>       - [a3] says that [set3] accepts links with sink type [t3] ([t3]is
>         the source type of [link3])
>       - [cc3] says that [set3] accepts links with sink types that its
>         parent does (that is, any links with sink types [t1], [t2] or [t3])
>     *)
> 
>     (*There is just no way we can get insert [link4] into [set3]. The
>       is no evidence we can produce that will allow a link with sink
>       type [t4]. Try the below with any of [a1], [a2], [a3])*)
>     (*
>     let (Augmented_set
>        {set = set4; accepts = a4; cc = cc4} =
>        insert_link link4 set (cc3 a3) : (t3, _) augmented_set) in
>     *)
> 
>     ()
> end
> 
> let _ = let module T = Test (M) in T.test ()