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