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

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

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