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

[Shayne Fletcher <shayne.fletcher.50@gmail.com>]

[-- 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 --]