Hi Gabriel

This is an interesting way to derive the GADT, at least for me, as I
have never did any logic programming. The resulting API is a bit easier
to use than the one from Jeremy's idea, at least for my use case.

I'm using this idea to experiment with a type-safe SQL query builder,
which so far looks like this:

  from Team.table
    |> belonging_to Team.owner   Here
    |> having_one Project.leader Here
    |> select
        |> fields [field User.id; field User.name] (Next Here)
        |> fields [field Team.id; field Team.name] (Next (Next Here))
        |> fields [all Project.table]              Here

This generates the following query:

  SELECT
    users.id, users.name,
    teams.id, teams.name,
    projects.*
  FROM
    teams
  LEFT JOIN
    users ON users.id = teams.owner_id
  LEFT JOIN
    projects ON projects.leader_id = users.id

I'm not sure if this will ever be of use in practice, as the Next/Here
stuff might be too complicated for users, but overall I'm quite happy
with the result and what I've learned, though of course it's far from
complete (e.g. no support for WHERE clauses).

Thanks for the hints!

Andre

On 09/30/2016 10:54 AM, Gabriel Scherer wrote:
> I came back to this thread thanks to Alan Schmitt's Caml Weekly News.
> 
> Here is a fairly systematic approach to the problem, contrasting
> Jeremy's more virtuoso approach. It works well when the whole set is
> statically defined in the source code, but I'm not sure about more
> dynamic scenarios (when a lot of the type variables involved become
> existentially quantified.
> 
> The idea is to first formulate a solution using logic programming. A
> link set can be represented as a list of accepted sinks, and I can write
> a small Prolog program, "insert" that takes a new link, and a link set,
> and traverses the link set to find the link's sink in the list, and add
> the link's source to the list in passing.
> 
>    set([sink]) :- link(source, sink).
>    set(sinks) :-
>      set(prev_sinks),
>      link(source, sink),
>      insert(prev_sinks, source, sink, sinks).
> 
>    (* either the sink we want to insert is first in the list *)
>    insert([sink | _], source, sink, [source, sink | sinks]).
> 
>    (* or it is to be found somewhere, recursively, under some other sink
> [s] *)
>    insert([s | prev_sinks], source, sink, [s | sinks]) :-
>      insert(prev_sinks, source, sink, sinks).
> 
> Once you have this logic program, it is straightforward to translate it
> to a GADT declaration:
> 
> type 's linkset =
>   | Init : ('source, 'sink) link -> ('source -> ('sink -> unit)) linkset
>   | Insert : ('source, 'sink) link * 'set1 linkset * ('set1, 'source,
> 'sink, 'set2) insert -> 'set2 linkset
> and ('set1, 'source, 'sink, 'set2) insert =
>   | Here : (('sink -> _) as 'set1, 'source, 'sink, 'source -> 'set1) insert
>   | Next : ('set1, 'source, 'sink, 'set2) insert -> ('a -> 'set1,
> 'source, 'sink, 'a -> 'set2) insert
> 
> let _ = fun (type t1 t2 t3) (lnk1 : (t2, t1) link) (lnk2 : (t3, t1)
> link) (lnk3 : (t3, t2) link) ->
>   let set = Init lnk1 in
>   let set = Insert (lnk2, set, Next Here) in
>   let set = Insert (lnk3, set, Here) in
>   set
> 
> 
> On Wed, Sep 21, 2016 at 8:50 PM, Andre Nathan <andre@digirati.com.br
> <mailto:andre@digirati.com.br>> wrote:
> 
>     Em 21 de set de 2016, às 19:22, Jeremy Yallop <yallop@gmail.com
>     <mailto:yallop@gmail.com>> escreveu:
>>     It is!  Here's one approach, which is based on two ideas:
> 
>     Wow, there's a lot to digest here :) Most of it is new to me,
>     including the use of "evidence" types... I'll have to re-read it and
>     try to work it out after a night of sleep.
> 
>     Thanks,
>     Andre 
> 
>