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 c5ff346549e7 (Postfix) with ESMTP id 7349A5D4 for ; Sun, 17 Jun 2018 09:51:23 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.51,234,1526335200"; d="scan'208,217";a="332111844" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jun 2018 11:51:20 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id DB85982495; Sun, 17 Jun 2018 11:51:20 +0200 (CEST) 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 3113A82474 for ; Sun, 17 Jun 2018 11:51:10 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jesper.louis.andersen@gmail.com; spf=Pass smtp.mailfrom=jesper.louis.andersen@gmail.com; spf=None smtp.helo=postmaster@mail-oi0-f52.google.com IronPort-PHdr: =?us-ascii?q?9a23=3ASwaqzRQoft9eSd6UynvX+xA0iNpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6yZh2N2/xhgRfzUJnB7Loc0qyK6/2mATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfbN/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0li?= =?us-ascii?q?gIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRODYOy?= =?us-ascii?q?bYQBD+QPM+VFoYfju1QDtgGxCRW2Ce711jNEmn370Ksn2OohCwHG2wkgEsoKvn?= =?us-ascii?q?vKt9X1LLkdUfqox6fOyjXDcvJW2Szg44XUdBAuvO+DXahrccXPz0kkCgTIjleO?= =?us-ascii?q?poz+JzOayP4Nv3Kf7+pnSOKvinUnpxtrrTip28gjlJPJhpkLxVDC7ih5z4M1Ks?= =?us-ascii?q?e5SE5/e9KrDJxQtySDOoZwX8gsQHlotT4kxrEavZO3ZisHxZQ9yxLBdvCKcJKE?= =?us-ascii?q?7xL9WOuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2xzU68iLVu?= =?us-ascii?q?Jx/kmh1DqRzQzT5eZEIUc7larfNZEt2KI/lp0WsUjbHy/2nlv5jLOOe0k65uSl?= =?us-ascii?q?7/7rb7bmq5OGKYN4lwLzPr4ul8ChGeg4NxIBX2mf+eSyzr3j+kj5Ta1IjvIoia?= =?us-ascii?q?nZqI7VJd4Bqq69BA9Vz4cj6w2lAzi81tQXgGcILEheeB2ZiYjkIF7OIPXiAve+?= =?us-ascii?q?h1Sgiitkx/fDPrH5GJXCMmDDkKv9fbZ680NT1BA8zdVb555NDrEBIenzWlPqud?= =?us-ascii?q?zDDh45NhS0zPz9BNV80IMeQ2OPDbWDPKPcq1/brt4odteNaZNdnDu1f+Yk6uLq?= =?us-ascii?q?lC9ksVAYdKitm5AQbSbrMO5hJhC7bGH0j81JNWAXvxF2ZermhUeZXDgbM3S/RL?= =?us-ascii?q?ox/Hc/D5+nFsHKQIygmqeM2g+0G5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFR?= =?us-ascii?q?EOH5E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090svr/ckBgz8Xp/CMHPijjRHVExpX?= =?us-ascii?q?sBQnoN5I46uVZ0kw7R3q1xgvgeHttWtasQD1UKcKXExuk/MOjcHwLMetDTFQSj?= =?us-ascii?q?S9SiRDYwFpc/noVIbEF6FNGvyBvE2njyDg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BaAgB8LiZbhjTaVdFbHQEBBQELAYNsg?= =?us-ascii?q?T0VE4N5gR2CUIQXjFKBf4gpgTCGGYR/gXgLhGwCglIZBwEEMBgBAgEBAQEBAQE?= =?us-ascii?q?BARMBAQEICwsIKSMMgjUkAYJPAQQBIx0BGx0BAwwGBQQHNwICIQEBEQEFARwGE?= =?us-ascii?q?4MlgWgBAw0Inmc8iwiBfwUBF4JyBYNIChkmDVVXgWACBhKIQoITgQ+DDIJRgg6?= =?us-ascii?q?DF4JVAphqLAcCgk6JM4MIjTuKX4ZfDyGBIIIKMxojUDGCEoIVDA4Jg0WKVD0wj?= =?us-ascii?q?W8rghsBAQ?= X-IPAS-Result: =?us-ascii?q?A0BaAgB8LiZbhjTaVdFbHQEBBQELAYNsgT0VE4N5gR2CUIQ?= =?us-ascii?q?XjFKBf4gpgTCGGYR/gXgLhGwCglIZBwEEMBgBAgEBAQEBAQEBARMBAQEICwsIK?= =?us-ascii?q?SMMgjUkAYJPAQQBIx0BGx0BAwwGBQQHNwICIQEBEQEFARwGE4MlgWgBAw0Inmc?= =?us-ascii?q?8iwiBfwUBF4JyBYNIChkmDVVXgWACBhKIQoITgQ+DDIJRgg6DF4JVAphqLAcCg?= =?us-ascii?q?k6JM4MIjTuKX4ZfDyGBIIIKMxojUDGCEoIVDA4Jg0WKVD0wjW8rghsBAQ?= X-IronPort-AV: E=Sophos;i="5.51,234,1526335200"; d="scan'208,217";a="332111798" Received: from mail-oi0-f52.google.com ([209.85.218.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Jun 2018 11:51:09 +0200 Received: by mail-oi0-f52.google.com with SMTP id e8-v6so12416061oii.2 for ; Sun, 17 Jun 2018 02:51:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=H8Cb4ejwQbZzZlRAijkIPRq7F/Cuh3qWHR6+ZW+wODY=; b=pBx7wpSb8qvmf97tYI2omBaBdf5ikyfgTLasXLuodulFwSqImTLr6TTPuS6Xxt38Hc 1+kao/PS3ONnTyKI0dJ6NgK2wn1HwwyBRErYgG4zYnlBKMDk/isYNFNjC7IUfzt4HRHp av/UF/1PhP97FvjgolaGvhEV7xMCVYm5c41CcRX6smPwYVXHGeh2xg1eGOP8yIi+ukhE w2/GAcUPYmIDwjPy/E/FCswijI0ZGFKUUMwt4pc4Ek/GIx9W8SYVM4Wd4jVYMDDnsWAF BL9bgXJmmagDh3p0sOJzixoMzjML/CDDVhZJJNJM0AOMWA9+Iz2C86BSPHkgRFdjULqL gDGg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=H8Cb4ejwQbZzZlRAijkIPRq7F/Cuh3qWHR6+ZW+wODY=; b=IGH2wULcr2hSu0PuOnIzmszpffzAPZMAMS2sTGHG+z+FdfxugyHCizx2hvMyEeJAqc lXe4+z4N6wZPjPFramZOzilx3eR2wviXIaMWwTvtL5rfTBDHK8S7mTKRTix1NYaGrEap 80x4h+PFgWXc5gJ37fFpIN1FDBrecm8SYoMLFhgTQ2z7E5j+S2U1qrzvI7Z9wCnGYBm5 5s0dPwSY+rfOrbCTVsrAaMuXwGmS3K2ayKJQ9uBAGk+WTel7NGoPNZQeJKLzy+A6zqzV 28fBFkJ+PZJ+6tt1EoHpeAv+IcfDzedOKAiRoYDvXNgcqtHSPGQd116TfIgBnCYqxBky NO7A== X-Gm-Message-State: APt69E1XPJZcZAuL9befVEyxZtlTBXmQgAmO5A8M02OrMYHmDPrsxW64 7oNf5GMu6nUhVXZlRQiQplpzsoSUrEKJQ01HZNOE X-Google-Smtp-Source: ADUXVKJ+gNdFXWbNElwBgBimV1tmcFy626pFcyvG420XBGvgMn4DDvF5O/7Cyt5eWFXNQVlg2x0jGyCl4eKK0o3uFiw= X-Received: by 2002:aca:df54:: with SMTP id w81-v6mr4844343oig.104.1529229067775; Sun, 17 Jun 2018 02:51:07 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Jesper Louis Andersen Date: Sun, 17 Jun 2018 11:50:56 +0200 Message-ID: To: Viet Le Cc: Chet Murthy , OCaml Mailing List Content-Type: multipart/alternative; boundary="0000000000005d767d056ed363db" Subject: Re: [Caml-list] a question about GADTs Reply-To: Jesper Louis Andersen X-Loop: caml-list@inria.fr X-Sequence: 16947 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --0000000000005d767d056ed363db Content-Type: text/plain; charset="UTF-8" On Sun, Jun 17, 2018 at 8:39 AM Viet Le wrote: > > I also came across a blog about writing GraphQL server using OCaml & GADT. > Worth checking out. > > The use there is pretty good. In GraphQL you have a query language in which fields are bound to functions with arguments. Andreas (the GraphQL author) takes the graphql schema and uses a GADT to derive the correct type for said function. In short: the function will have the correct type and schema changes will require updates on the necessary functions. But you could argue this is still within the bounds of PL: GraphQL is a language Their spec doesn't show it, but it is best implemented as such: have a statics phase and a dynamics phase, type check vigorously in the statics phase. Most of what they call "validations" are just standard type checking hygiene. Also, the types are moded/polarized in that certain types flows from the client to the server (which means you shouldn't trust the client) and other types flows from the server to the client (which means you shouldn't trust the server). I have a hunch that there is a small core language within GraphQL best realized as a lambda-calculus (with added primops corresponding to execution of user-defined code). But I have yet to try implementing that. --------- A use I've seen Janes St. doing is to use a GADT as a witness for a given implementation. This allows the programmer to define a generic implementation of, say 'a array, and then later specialize the bool array variant into a bitset on words, or a more advanced data structure where the bitset is a tree of some kind. The GADT then "selects" for the given implementation in the code base. -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs --0000000000005d767d056ed363db Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sun, Jun 17= , 2018 at 8:39 AM Viet Le <vietlq8= 5@gmail.com> wrote:

I also came across a blog = about writing GraphQL server using OCaml & GADT. Worth checking out.


The use the= re is pretty good. In GraphQL you have a query language in which fields are= bound to functions with arguments. Andreas (the GraphQL author) takes the = graphql schema and uses a GADT to derive the correct type for said function= . In short: the function will have the correct type and schema changes will= require updates on the necessary functions.

But y= ou could argue this is still within the bounds of PL:

<= div>GraphQL is a language

Their spec doesn't s= how it, but it is best implemented as such: have a statics phase and a dyna= mics phase, type check vigorously in the statics phase. Most of what they c= all "validations" are just standard type checking hygiene.=C2=A0= =C2=A0
Also, the types are moded/polarized in that certain types = flows from the client to the server (which means you shouldn't trust th= e client) and other types flows from the server to the client (which means = you shouldn't trust the server).

I have a hunc= h that there is a small core language within GraphQL best realized as a lam= bda-calculus (with added primops corresponding to execution of user-defined= code). But I have yet to try implementing that.

-= --------

A use I've seen Janes St. doing is to= use a GADT as a witness for a given implementation. This allows the progra= mmer to define a generic implementation of, say 'a array, and then late= r specialize the bool array variant into a bitset on words, or a more advan= ced data structure where the bitset is a tree of some kind. The GADT then &= quot;selects" for the given implementation in the code base.


--0000000000005d767d056ed363db--