```
From: Oleg <oleg@okmij.org>
To: josh@berdine.net
Cc: francois.pottier@inria.fr, caml-list@inria.fr
Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic
Date: Wed, 7 Oct 2020 22:17:26 +0900
Message-ID: <20201007131726.GA4913@Melchior.localnet> (raw)
In-Reply-To: <FEA35C98-1E7A-402E-9B5D-9585371E4009@berdine.net>
> What I'm unsure of is how this generalizes to additional functions on
> expressions. For instance, suppose I also wanted to define a function
> which computed the set of int literals that appear in the (unreduced)
> expression? ...
> More pressingly, I think, is what operations such as `map_ints : (int
> -> int) -> 'a exp -> 'a exp` would look like.
Frankly speaking, after re-reading the message I sent back in June, I
found it rather confusing. It didn't say what the main idea was and
the talk about Reducer was too long and unenlightening. Luckily, this
time I have your excellent questions, and so get another chance to
explain the approach, hopefully better.
The basic set up is a little language with int, float and string
literals, and the addition operation. The user should be able to add
(and keep adding) ints and floats, but attempting to add strings
should raise a clear error message. The language expressions should be
first-class, that is, we should be able to put them into a list, among
other things. (I too find Francois' example superb, but I already had
the code for the earlier example).
Here is the definition of the language: its operations. The type
parameter of t enforces the constraint: ints and floats can be
(recursively) added in any combination but strings may not.
module type exp = sig
type +'a t
val int : int -> [> `int] t
val float : float -> [> `float] t
val add : ([< `int | `float] as 'n) t -> 'n t -> [> `int | `float] t
val string : string -> [> `string] t
end
Here are sample expressions:
module Ex1(I:exp) = struct
open I
(* We can put expressions of different sorts into the same list *)
let l1 = [int 1; float 2.0; add (add (int 3) (float 1.0)) (int 4)]
(* val l1 : [> `float | `int ] I.t list *)
let l2 = string "str" :: l1
(* val l2 : [> `float | `int | `string ] I.t list *)
(* An attempt to build an invalid expression fails, with a good error message:
let x = add (int 1) (string "s")
^^^^^^^^^^^^
Error: This expression has type [> `string ] t
but an expression was expected of type [< `float | `int > `int ] t
The second variant type does not allow tag(s) `string
*)
(* We can define a function to sum up elements of a list of expressions,
returning a single expression with addition
*)
let rec sum l = List.fold_left add (int 0) l
(* val sum : [ `float | `int ] I.t list -> [ `float | `int ] I.t *)
(* We can sum up l1 *)
let l1v = sum l1
(* val l1v : [ `float | `int ] I.t *)
(* but, predictably, not l2
let l2v = sum l2
^^
Error: This expression has type [> `float | `int | `string ] t list
but an expression was expected of type [ `float | `int ] t list
The second variant type does not allow tag(s) `string
*)
end
One doesn't have to use the functor as I just did. First-class modules,
or even records/objects will work too.
It is useful to see the expressions. Hence the first implementation of
the signature exp:
module Show : (exp with type 'a t = string) = struct
type 'a t = string
let int = string_of_int
let float = string_of_float
let string x = "\"" ^ String.escaped x ^ "\""
let add x y = Printf.sprintf "Add(%s,%s)" x y
end
Here is how the sample expressions look like:
let _ = let module M = Ex1(Show) in M.l1
(* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *)
let _ = let module M = Ex1(Show) in M.l2
(* - : string list = ["\"str\""; "1"; "2."; "Add(Add(3,1.),4)"] *)
let _ = let module M = Ex1(Show) in M.l1v
(* - : string = "Add(Add(Add(0,1),2.),Add(Add(3,1.),4))" *)
Now, to your questions.
``suppose I also wanted to define a function which computed the set of
int literals that appear in the (unreduced) expression?''
That is easy: we just interpret the same expressions in a different
way: instead of showing them, we compute the set of integers that occur in
their literals.
module IntSet = Set.Make(struct type t = int let compare = compare end)
module CollectInts : (exp with type 'a t = IntSet.t) = struct
type 'a t = IntSet.t
let int x = IntSet.singleton x
let float x = IntSet.empty
let string x = IntSet.empty
let add x y = IntSet.union x y
end
let _ = let module M = Ex1(CollectInts) in List.map IntSet.elements M.l1
(* - : int list list = [[1]; []; [3; 4]] *)
let _ = let module M = Ex1(CollectInts) in IntSet.elements M.l1v
(* - : int list = [0; 1; 3; 4] *)
The second question: ``More pressingly, I think, is what operations such as
`map_ints : (int -> int) -> 'a exp -> 'a exp` would look like. With an
initial style representation, this could be defined by traversing the
abstract syntax and rebuilding it with the updated `int`s.''
In tagless-final, it looks essentially like this, only simpler.
There is no need to write any traversal (a tagless-final term
itself specifies the traversal of itself)
module MapInts(Map:sig val f : int -> int end)(I:exp) = struct
type 'a t = 'a I.t
let int x = I.int (Map.f x)
let float = I.float
let string = I.string
let add = I.add
end
let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1
(* - : string list = ["2"; "2."; "Add(Add(4,1.),5)"] *)
let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l2
(* - : string list = ["\"str\""; "2"; "2."; "Add(Add(4,1.),5)"] *)
let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1v
(* - : string = "Add(Add(Add(1,2),2.),Add(Add(4,1.),5))" *)
The central idea is this:
eval (map f exp) === (compose eval (map f)) exp ===
let eval' = compose eval (map f) in eval' exp
Instead of transforming expressions we transform interpreters
(eval). Since evaluation is essentially folding, two foldings may be
fused.
I have updated
http://okmij.org/ftp/tagless-final/subtyping.ml
to include your questions.
```

next prev parent reply indexThread overview:9+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-10-06 11:57 [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier 2020-10-06 16:01 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg 2020-10-06 16:45 ` François Pottier 2020-10-06 19:05 ` Josh Berdine 2020-10-06 19:19 ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier 2020-10-06 20:11 ` Josh Berdine 2020-10-07 13:13 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg2020-10-07 13:13 ` Oleg [this message]2020-10-07 8:11 ` David Allsopp

Reply instructions:You may reply publically to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to=20201007131726.GA4913@Melchior.localnet \ --to=oleg@okmij.org \ --cc=caml-list@inria.fr \ --cc=francois.pottier@inria.fr \ --cc=josh@berdine.net \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list AGPL code for this site: git clone https://public-inbox.org/ public-inbox