```
From: Oleg <oleg@okmij.org>
To: josh@berdine.net
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Subtyping of phantom GADT indices?
Date: Sun, 28 Jun 2020 00:36:43 +0900
Message-ID: <20200627153643.GA4954@Melchior.localnet> (raw)
In-Reply-To: <452E9622-D117-43E6-A0B1-9B8272F3C5FE@berdine.net>
Josh Berdine has posed a problem:
> As a concrete example, consider something like:
> ```
> type _ exp =
> | Integer : int -> [> `Integer] exp
> | Float : float -> [> `Float] exp
> | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp
> | String : string -> [> `String] exp
> ```
> The intent here is to use polymorphic variants to represent a small
> (upper semi-) lattice, where basically each point corresponds to a
> subset of the constructors. The type definition above is admitted, but
> while the index types allow subtyping ...
> this does not extend to the base type:
> ```
> # let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
> Line 1, characters 18-67:
> 1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: Type [ `Integer ] exp is not a subtype of
> ([> `Float | `Integer ] as 'a) exp
> The first variant type does not allow tag(s) `Float
> ```
> This makes sense since `type _ exp` is not covariant. But trying to
> declare it to be covariant doesn't fly, yielding:
> ```
> Error: In this GADT definition, the variance of some parameter
> cannot be checked
> ```
We demonstrate three solutions to this problem. The first has an
imperfection, but is easier to explain. The second removes the
imperfection. The third one is verbose, but requires the least of
language features and can be implemented in SML or perhaps even
Java. All three solutions give the end user the same static
guarantees, statically preventing building of senseless
expressions. All three rely on the tagless-final style, in effect
viewing the problem as a language design problem -- designing a DSL
with subtyping. It has been my experience that the tagless-final,
algebraic point of view typically requires less fancy
typing. Incidentally, the third solution, of explicit coercions, can
be combined with GADTs and is hence the general solution to the posed
problem, showing how to do phantom index subtyping with GADTs.
Presenting all three solutions is too long for a message, so one
should look at the complete code with many comments:
http://okmij.org/ftp/tagless-final/subtyping.ml
Below is the outline of the first solution, the easiest to
explain. (The others just add slight variations; the main
example looks almost the same in all three).
We will think of the problem as a DSL with subtyping.
Let's define its syntax and the type system, as an OCaml signature:
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
The language expressions are indexed with a subset of tags `int,
`float, `string. The language has the obvious subtyping: [> `int]
can be weakened to [> `int | `float]. This weakening, and general typechecking
of our DSL is performed by OCaml's type checker for us. Let's see an
example
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
*)
end
Now, what we can do with the expressions? We can print/show them
module Show : (exp with type 'a t = string) = struct
type 'a t = string
... elided ...
end
let _ = let module M = Ex1(Show) in M.l1
(* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *)
We can also reduce them. The following is the reducer -- although
in reality it does the normalization-by-evaluation (NBE)
A subset of expressions: values
module type vals = sig
type +'a t
val int : int -> [> `int] t
val float : float -> [> `float] t
val string : string -> [> `string] t
end
module Reducer(I:vals) :
(sig include exp val observe : ([> `float | `int ] as 'a) t -> 'a I.t end)
= struct
type 'a t = Unk of 'a I.t | Int of int | Float of float
let observe = function
| Unk x -> x
| Int x -> I.int x
| Float x -> I.float x
let int x = Int x
let float x = Float x
let string x = Unk (I.string x)
let add x y = match (x,y) with
| (Int x, Int y) -> Int (x+y)
| (Float x, Float y) -> Float (x+.y)
| (Int x, Float y) | (Float y, Int x) -> Float (float_of_int x +. y)
(* This is the imperfection. We know that the case cannot happen,
but this is not clear from the type system.
We should stress that this imperfection does not compromise the guarantees
offered to the end user, who never sees the internals of Reducer,
and can't even access them.
*)
| _ -> assert false
end
(* We can now evaluate exp to values. We need a way to show them though.
Luckily, exp is a superset of values, and we already wrote the show
interpreter for exp
*)
let _ = let module I = Reducer(Show) in
let module M = Ex1(I) in List.map I.observe M.l1
(* - : string list = ["1"; "2."; "8."] *)
The second solutions removes the imperfection in Reduce, making
Reduce.add total, by making the types more phantom. The third solution
does the obvious thing: implementing subtyping using explicit
coercions. In the given example, it doesn't add too much annoyance to
the user. It does however remove the reliance on variance and so
is applicable to GADTs in general. One can imagine more solutions
along the shown lines.
```

prev parent reply indexThread overview:2+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-06-21 16:10 Josh Berdine2020-06-27 15:33 ` Oleg [this message]

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=20200627153643.GA4954@Melchior.localnet \ --to=oleg@okmij.org \ --cc=caml-list@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