Re: [Caml-list] Calling a single function on every member of a GADT?

[Ivan Gotovchits <ivg@ieee.org>]

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

On Tue, Jan 7, 2020 at 2:25 PM <rixed@happyleptic.org> wrote:

> ... but using a GADT:
>
> ---
> module Gadt =
> struct
>   type _ term =
>      | Int : int -> int term
>      | Add : (int -> int -> int) term
>      | App : ('b -> 'a) term * 'b term -> 'a term
>
>   let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f ->
> function
>     | Int _ as t -> f i t
>     | Add -> f i Add
> (*
>      ^ Error: This pattern matches values of type (int -> int -> int) term
>         but a pattern was expected which matches values of type int term
>         Type int -> int -> int is not compatible with type int
> *)
>     | App (x, y) as t -> f (fold (fold i f x) f y) t
> end
> ---
>
> I've tried other variants of the syntax and got many encouragements but no
> green flag from the type-checker.
> Why is the compiler expecting an int term in there? I though the whole
> point of the `type a. ...` syntax was to allow the matched type to vary
> from one pattern to the next?
> Is there a way to do this?
>

It is the limitation of the let-bound polymorphism. A parameter of a
function is monomorphic in its body. The classical example doesn't even
reference any GADT,

    let example f  = f "hello", f 42

It won't compile even though we can provide a polymorphic function that can
applied both to integers and to strings, e.g., `exampe (fun x -> x)` should
be possible, but not, because of the let-bounded polymorphism. There are a
few solutions available in OCaml, the simplest is to use records, e.g.,

    type app = {apply : 'a. 'a -> 'a}

    let example {apply} = apply "hello", apply 42;;

    val example : app -> string * int = <fun>

Now we have `app` that is polymorphic.
In your case, I would define a visitor type, e.g.,

  type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}

  let rec fold : type a. 'r -> 'r visitor -> a term -> 'r =
    fun i f t -> match t with
      | Int _ as t -> f.visit i t
      | Add as t -> f.visit i t
      | App (x,y) as t ->
          let i = fold i f x in
          let i = fold i f y in
          f.visit i t


Cheers,
Ivan Gotovchits

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