From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 41B1F7FFE1 for ; Wed, 5 Oct 2016 21:47:25 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andre@digirati.com.br; spf=Pass smtp.mailfrom=andre@digirati.com.br; spf=Pass smtp.helo=postmaster@mta112.f1.k8.com.br Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of andre@digirati.com.br) identity=pra; client-ip=187.73.32.184; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of andre@digirati.com.br designates 187.73.32.184 as permitted sender) identity=mailfrom; client-ip=187.73.32.184; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@mta112.f1.k8.com.br designates 187.73.32.184 as permitted sender) identity=helo; client-ip=187.73.32.184; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="postmaster@mta112.f1.k8.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3AAKQobBDaxTVE4CQVDlm/UyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP38o8bcNUDSrc9gkEXOFd2CrakV0ayN6+u5BTRIoc7Y9itdINoUD15NoP?= =?us-ascii?q?5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9?= =?us-ascii?q?fbytScaBx/iwguu7/pmWZwRTmBK8Z6lzJVO4t1b/rM4T1KJkJrw8gj3AvntBfa?= =?us-ascii?q?wCzGVkP1+7kxfz59254J8l+CNV/fg7oZ0TGZ7mdrg1GOQLRA8tNHo4sZXm?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AwAQCcV/VXh7ggSbtdRwEBFgEBBQEBB?= =?us-ascii?q?oJ/AQEBAQF1KgNPpDGHWIxRggkehgICgXQ4FAEBAQEBAQEBAQEBEgEBAQgNCQk?= =?us-ascii?q?ZL4IyGIIYAQEEIwQZAQE4DwsYJwMCAiABCgIBGBESAQYCAQEWAYgZAxmuG2eES?= =?us-ascii?q?QEBBYQ0DYNbIwYJiDkIglCCR4RMOIJajjyFaoUkNYNBgXZwhkqDIE2BB06HGhI?= =?us-ascii?q?jXoUKiGCEE4N8Ah51BQeCaxELgWxYiDYBAQE?= X-IPAS-Result: =?us-ascii?q?A0AwAQCcV/VXh7ggSbtdRwEBFgEBBQEBBoJ/AQEBAQF1KgN?= =?us-ascii?q?PpDGHWIxRggkehgICgXQ4FAEBAQEBAQEBAQEBEgEBAQgNCQkZL4IyGIIYAQEEI?= =?us-ascii?q?wQZAQE4DwsYJwMCAiABCgIBGBESAQYCAQEWAYgZAxmuG2eESQEBBYQ0DYNbIwY?= =?us-ascii?q?JiDkIglCCR4RMOIJajjyFaoUkNYNBgXZwhkqDIE2BB06HGhIjXoUKiGCEE4N8A?= =?us-ascii?q?h51BQeCaxELgWxYiDYBAQE?= X-IronPort-AV: E=Sophos;i="5.31,302,1473112800"; d="asc'?scan'208";a="239561691" Received: from mta112.f1.k8.com.br ([187.73.32.184]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 05 Oct 2016 21:47:22 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id E63088033A for ; Wed, 5 Oct 2016 19:47:16 +0000 (UTC) X-Virus-Scanned: amavisd-new at k8.com.br Received: from smtpz.f1.k8.com.br ([127.0.0.1]) by localhost (mta112.f1.k8.com.br [127.0.0.1]) (amavisd-new, port 10024) with LMTP id lsB0VtRvrTE6 for ; Wed, 5 Oct 2016 19:47:04 +0000 (UTC) Received: from [10.200.12.21] (unknown [201.76.188.234]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtpz.f1.k8.com.br (Postfix) with ESMTPSA id 35C788030C for ; Wed, 5 Oct 2016 19:47:03 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br 35C788030C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1475696824; bh=9eH1l5O3OrpBKScp3vclgmmERwW0bdmskXzYQ3l5xXk=; h=Subject:To:References:From:Date:In-Reply-To; b=sJOeRPNPo+W0ykkJrCij5pdGzHe/SpgoiOTlFe8QDCqVoNXDIDuCIs7wkH1BG7j5C 4KS8oQKUglS9QwLS2vo2e/Oq+R0j/nXoXRmSraMIbT9tIE0b0IshLD+Kf8OkIwLmit shVStZejmrBXPVWD4kthlOPOXwZaXCyiFqeZI79I= To: caml-list@inria.fr References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> <4B4C9521-010D-4FB7-80C0-0F2192D93614@digirati.com.br> From: Andre Nathan Message-ID: <8a4909ff-67dc-58c0-0974-1d35c8fce091@digirati.com.br> Date: Wed, 5 Oct 2016 16:46:56 -0300 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="fbGsmQqiieQUeLWIsnugxGKKfHKr8RB1E" Subject: Re: [Caml-list] Encoding "links" with the type system This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --fbGsmQqiieQUeLWIsnugxGKKfHKr8RB1E Content-Type: multipart/mixed; boundary="lCbiWA4peR6IRGxJr6le87vhPEAp2U62G"; protected-headers="v1" From: Andre Nathan To: caml-list@inria.fr Message-ID: <8a4909ff-67dc-58c0-0974-1d35c8fce091@digirati.com.br> Subject: Re: [Caml-list] Encoding "links" with the type system References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> <4B4C9521-010D-4FB7-80C0-0F2192D93614@digirati.com.br> In-Reply-To: --lCbiWA4peR6IRGxJr6le87vhPEAp2U62G Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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 =3D teams.owner_id LEFT JOIN projects ON projects.leader_id =3D 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. >=20 > 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. >=20 > 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. >=20 > set([sink]) :- link(source, sink). > set(sinks) :- > set(prev_sinks), > link(source, sink), > insert(prev_sinks, source, sink, sinks). >=20 > (* either the sink we want to insert is first in the list *) > insert([sink | _], source, sink, [source, sink | sinks]). >=20 > (* 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). >=20 > Once you have this logic program, it is straightforward to translate it > to a GADT declaration: >=20 > type 's linkset =3D > | 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 =3D > | Here : (('sink -> _) as 'set1, 'source, 'sink, 'source -> 'set1) inse= rt > | Next : ('set1, 'source, 'sink, 'set2) insert -> ('a -> 'set1, > 'source, 'sink, 'a -> 'set2) insert >=20 > let _ =3D fun (type t1 t2 t3) (lnk1 : (t2, t1) link) (lnk2 : (t3, t1) > link) (lnk3 : (t3, t2) link) -> > let set =3D Init lnk1 in > let set =3D Insert (lnk2, set, Next Here) in > let set =3D Insert (lnk3, set, Here) in > set >=20 >=20 > On Wed, Sep 21, 2016 at 8:50 PM, Andre Nathan > wrote: >=20 > Em 21 de set de 2016, =C3=A0s 19:22, Jeremy Yallop > escreveu: >> It is! Here's one approach, which is based on two ideas: >=20 > 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. >=20 > Thanks, > Andre=20 >=20 >=20 --lCbiWA4peR6IRGxJr6le87vhPEAp2U62G-- --fbGsmQqiieQUeLWIsnugxGKKfHKr8RB1E Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAEBCAAGBQJX9ViwAAoJED4JW1qwFY2cITEH/jFBCq7mkvAGu6h9G6UPikm1 K+Uv4iQxvYh7Fw8p/Ljg3WeBhEePWNuOXPTGOFwOtC5xHlCFQ7PLGHv/rcGZ2Dnj oYEzz9hqyzWL41eXemBNEQ1MC4FsBe0FU3QSdwqdrSLjUeGzjIxDqwLD+t4M4VNk +FOzF+TfVHiaMTpCzJ+6IMRtXehdiMXlGpz41C1gwyVkI0AOK21pgBbC51HAROe5 WIlVwV/Rns4qy/YYSk+VGfW0phe+OgqEHuT5JaMSrOfkVTV12bvxEW0zgsSnAW2E I1T8gI8SOdU/jPHmMXPFQjdmI6VQGZrTKyMJwAp/0k1pq5BY2fwn+9YCYKrfcdk= =UhGv -----END PGP SIGNATURE----- --fbGsmQqiieQUeLWIsnugxGKKfHKr8RB1E--