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

[Andre Nathan]

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

[Jeremy Yallop]

Dear Andre,

Post by Andre Nathan
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
* 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.

[Andre Nathan]

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

[Gabriel Scherer]

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

Post by Andre Nathan
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

[Andre Nathan]

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

Post by Gabriel Scherer
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
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
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

[Daniel Bünzli]

Post by Andre Nathan
I'm using this idea to experiment with a type-safe SQL query builder,

You may be interested in looking at this

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

Best,

Daniel

[Shayne Fletcher]

Post by Jeremy Yallop
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]

On Fri, Oct 7, 2016 at 1:02 PM, Shayne Fletcher <

Post by Shayne Fletcher

Post by Jeremy Yallop
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 ()

[Jacques Garrigue]

Post by Jeremy Yallop
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

Post by Jeremy Yallop
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
('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
- [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
- [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 ()