[Caml-list] a question about GADTs

[Caml-list] a question about GADTs

[Alan Schmitt]

[-- Attachment #1: Type: text/plain, Size: 654 bytes --]

Hello,

I'm trying to write the following:

#+begin_src ocaml
type state
type value
type literal
   
type (_,_)  term =
  | Skip : (state, state) term
  | Const : literal -> (state, value) term
  | If : expr * stat * stat -> (state,state) term
and expr = (state,value) term
and stat = (state,state) term
#+end_src

and it works well. However I would like to replace the right-hand side
with their abbreviations (stat and expr), and at that point the
typechecker complains. Is there a workaround?

Thanks,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-05: 411.25, 2017-05: 409.65

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 528 bytes --]

Re: [Caml-list] a question about GADTs

[Markus Mottl]

[-- Attachment #1: Type: text/plain, Size: 1518 bytes --]

I don't think that you can currently do this.  According to the manual
entry for GADTs: "This return type must use the same type constructor as
the type being defined, and have the same number of parameters."

But I guess it would be a supportable feature to perform type substitutions
until the above is satisfied if at all possible.  Substituting manually is
probably the only thing you can do until then.

On Fri, Jun 15, 2018 at 10:35 AM Alan Schmitt <
alan.schmitt@polytechnique.org> wrote:

> Hello,
>
> I'm trying to write the following:
>
> #+begin_src ocaml
> type state
> type value
> type literal
>
> type (_,_)  term =
>   | Skip : (state, state) term
>   | Const : literal -> (state, value) term
>   | If : expr * stat * stat -> (state,state) term
> and expr = (state,value) term
> and stat = (state,state) term
> #+end_src
>
> and it works well. However I would like to replace the right-hand side
> with their abbreviations (stat and expr), and at that point the
> typechecker complains. Is there a workaround?
>
> Thanks,
>
> Alan
>
> --
> OpenPGP Key ID : 040D0A3B4ED2E5C7
> Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-05: 411.25, 2017-05: 409.65
>


-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

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

[-- Attachment #2: Type: text/html, Size: 1840 bytes --]

Re: [Caml-list] a question about GADTs

[Alan Schmitt]

[-- Attachment #1: Type: text/plain, Size: 755 bytes --]

Hello Markus,

On 2018-06-15 11:21, Markus Mottl <markus.mottl@gmail.com> writes:

> I don't think that you can currently do this.  According to the manual
> entry for GADTs: "This return type must use the same type constructor as
> the type being defined, and have the same number of parameters."
>
> But I guess it would be a supportable feature to perform type substitutions
> until the above is satisfied if at all possible.  Substituting manually is
> probably the only thing you can do until then.

Thank you for your reply. I'll use the explicit form for the moment with
some comments on the side.

Best,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-05: 411.25, 2017-05: 409.65

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 528 bytes --]

Re: [Caml-list] a question about GADTs

[Chet Murthy]

[-- Attachment #1: Type: text/plain, Size: 425 bytes --]

I'm curious: is there any real-world use of GADTs, other than in PL
itself?  I mean, writing interpreters, compilers, and such?  Any non-PL use?

Again, not trying to start a flame-war -- just *curious*.

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

[-- Attachment #2: Type: text/html, Size: 362 bytes --]

Re: [Caml-list] a question about GADTs

[Viet Le]

[-- Attachment #1: Type: text/plain, Size: 1049 bytes --]

What is PL? I would appreciate more descriptive language.

I can see that Janestreet claim huge benefits from GADTs (check their blog).

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

String/print formatting used to rely on unsafe Obj.magic. For a few years
OCaml string/print formatting is using GADT that provide compile time
safety. Lookup format6, and OCaml GADT for string/print formatting. That’s
the most real-world usage.

Viet

On Sun, 17 Jun 2018 at 04:44, Chet Murthy <murthy.chet@gmail.com> wrote:

> I'm curious: is there any real-world use of GADTs, other than in PL
> itself?  I mean, writing interpreters, compilers, and such?  Any non-PL use?
>
> Again, not trying to start a flame-war -- just *curious*.
>
> --
Kind regards,
Viet

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

[-- Attachment #2: Type: text/html, Size: 1507 bytes --]

Re: [Caml-list] a question about GADTs

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 1156 bytes --]



On Sun, 17 Jun 2018, Viet Le wrote:

> What is PL? I would appreciate more descriptive language.

programming language, as in POPL.

julia

>
> I can see that Janestreet claim huge benefits from GADTs (check their blog).
>
> I also came across a blog about writing GraphQL server using OCaml & GADT.
> Worth checking out.
>
> String/print formatting used to rely on unsafe Obj.magic. For a few years
> OCaml string/print formatting is using GADT that provide compile time
> safety. Lookup format6, and OCaml GADT for string/print formatting. That’s
> the most real-world usage.
>
> Viet
>
> On Sun, 17 Jun 2018 at 04:44, Chet Murthy <murthy.chet@gmail.com> wrote:
>       I'm curious: is there any real-world use of GADTs, other than in
>       PL itself?  I mean, writing interpreters, compilers, and such? 
>       Any non-PL use?
>
> Again, not trying to start a flame-war -- just *curious*.
>
> --
> Kind regards,
> Viet
>
>

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

Re: [Caml-list] a question about GADTs

[Jesper Louis Andersen]

[-- Attachment #1: Type: text/plain, Size: 1915 bytes --]

On Sun, Jun 17, 2018 at 8:39 AM Viet Le <vietlq85@gmail.com> 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

[-- Attachment #2: Type: text/html, Size: 2380 bytes --]