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

[Andre Nathan <andre@digirati.com.br>]

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