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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2016/10/09 06:51, Shayne Fletcher wrote:
> 
> 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?

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

> 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 ()