From: Oleg <firstname.lastname@example.org> To: email@example.com Cc: firstname.lastname@example.org, email@example.com 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 = [; ; [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 other threads:[~2020-10-07 13:13 UTC|newest] Thread 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:05 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg 2020-10-06 16:45 ` François Pottier 2020-10-06 19:04 ` Josh Berdine 2020-10-06 19:18 ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier 2020-10-06 20:10 ` Josh Berdine 2020-10-07 13:17 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg 2020-10-07 13:17 ` Oleg [this message] 2020-10-07 8:10 ` David Allsopp
Reply instructions: You may reply publicly 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-to switches of git-send-email(1): git send-email \ --in-reply-to=20201007131726.GA4913@Melchior.localnet \ --firstname.lastname@example.org \ --email@example.com \ --firstname.lastname@example.org \ --email@example.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: link
caml-list - the Caml user's mailing list This inbox may be cloned and mirrored by anyone: git clone --mirror http://inbox.vuxu.org/caml-list git clone --mirror https://inbox.ocaml.org/caml-list # If you have public-inbox 1.1+ installed, you may # initialize and index your mirror using the following commands: public-inbox-init -V1 caml-list caml-list/ http://inbox.vuxu.org/caml-list \ firstname.lastname@example.org public-inbox-index caml-list Example config snippet for mirrors. Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.caml-list AGPL code for this site: git clone https://public-inbox.org/public-inbox.git