[Caml-list] Question on the covariance of a GADT (polymorphic variants involved)

[Caml-list] Question on the covariance of a GADT (polymorphic variants involved)

[François Pottier]

Dear all,

I have a problem convincing OCaml that a GADT is covariant in one of its
parameters.

Here is a simplified version of what I am trying to do:

type 'a t =
   | Wine: [> `Wine ] t
   | Food: [> `Food ] t
   | Box : 'a t * 'a t -> 'a t
   | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t

In this definition, the type parameter 'a is a phantom parameter. It is not
used to describe the type of a value; it is used only to restrict the set of
values of type "t" that can be constructed.

The goal here is to allow storing wine and food (and boxes containing boxes
containing wine and food) in a fridge, but forbid storing a fridge in a 
fridge
(or a fridge in a box in a fridge, etc.).

The lower bounds >`Wine and >`Food and >`Fridge are used to keep track 
of the
basic objects that are (transitively) contained in a box. The Box 
constructor
takes the conjunction of these lower bounds. The Fridge constructor imposes
the upper bound <`Wine|`Food, thereby forbidding a fridge to appear
(transitively) inside a fridge.

You may be wondering why I am using an algebraic data type whose index is
constrained by abusing polymorphic variants, instead of using polymorphic
variants directly. The answer is that is the real type definition I am 
working
with is more complex than this: it has more parameters and it is actually a
(real) GADT in these other parameters, so (I think) I cannot turn it into a
polymorphic variant.

Now, the problem is, the OCaml type-checker does not recognize that the type
'a t is covariant in 'a.

Intuitively, it seems clear that this type is covariant in 'a: the
constructors Wine, Food, Fridge impose lower bounds on 'a only, and the
constructor Box uses 'a in a covariant position (if one admits, inductively,
that 'a t is covariant in 'a).

I would like OCaml to accept the fact that t is covariant in 'a because 
I have
several functions (smart constructors) that produce values of type 'a t. 
When
an application of such a function produces a result of type _'a t, I would
like it to be generalized, so as to obtain 'a t. Currently, this does not
work.

This lack of generalization is not just a minor inconvenience. It leads to
pollution (that is, lower bounds and upper bounds bearing on the same type
variable, when they should normally bear on two distinct type 
variables). For
instance, if an object whose type has not been generalized is once placed
*beside* a fridge, then it can no longer be put *inside* a fridge:

   let food() = Food
   let meat = food()              (* weak type variable appears *)
   let _ = Box(meat, Fridge Wine) (* place the meat beside a fridge *)
   let _ = Fridge meat            (* meat can no longer be put into 
fridge *)
                  ^^^^
Error: This expression has type [> `Food | `Fridge ] t
        but an expression was expected of type [< `Food | `Wine ] t
        The second variant type does not allow tag(s) `Fridge

An explanation of why OCaml cannot recognize that this type is 
covariant, or a
suggestion of a workaround, would be very much appreciated. Thanks!

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg]

> type 'a t =
>    | Wine: [> `Wine ] t
>    | Food: [> `Food ] t
>    | Box : 'a t * 'a t -> 'a t
>    | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t
>
> In this definition, the type parameter 'a is a phantom parameter. It is not
> used to describe the type of a value; it is used only to restrict the set of
> values of type "t" that can be constructed.
>
> The goal here is to allow storing wine and food (and boxes containing
> boxes containing wine and food) in a fridge, but forbid storing a
> fridge in a fridge (or a fridge in a box in a fridge, etc.).

This is indeed a very `popular' problem. On June 21 this year Josh
Berdine posed almost the same question (without wine and food, alas).
On 28 June 2020 I sent the reply with three solutions. Perhaps it
would be easier to point to the code, which also has many comments and
explanations:

        http://okmij.org/ftp/tagless-final/subtyping.ml

The gist of the first two solutions is to exploit the fact that
tagless-final is sort of isomorphic to GADTs. That is, lots of things
that can be done with GADTs can be done without (or with GADTs hidden
away). That hiding has benefit of no longer bringing the problems with
variance. No GADTs (at least, not in the part facing the user), no
variance problems, at least, not for the end user. The library author
may use regular ADT, which are also non-problematic. A regular ADT
doesn't have the same typing guarantees -- but the typing is enforced
by the signature (at the module level), so there is no loss.

I was going to write an article for my web site explaining this and a
few earlier answers to the similar problems. Maybe I will eventually
get to it.

Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[François Pottier]

Dear Oleg,

Le 06/10/2020 à 18:05, Oleg a écrit :
> This is indeed a very `popular' problem. On June 21 this year Josh
> Berdine posed almost the same question (without wine and food, alas).
> On 28 June 2020 I sent the reply with three solutions.

Great, thanks for your quick reply!

Now I have to go do my homework and study your solutions :-)
I'll be in touch.

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Josh Berdine]

> On Oct 6, 2020, at 5:05 PM, Oleg <oleg@okmij.org> wrote:
> 
>> type 'a t =
>>   | Wine: [> `Wine ] t
>>   | Food: [> `Food ] t
>>   | Box : 'a t * 'a t -> 'a t
>>   | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t
>> 
>> In this definition, the type parameter 'a is a phantom parameter. It is not
>> used to describe the type of a value; it is used only to restrict the set of
>> values of type "t" that can be constructed.
>> 
>> The goal here is to allow storing wine and food (and boxes containing
>> boxes containing wine and food) in a fridge, but forbid storing a
>> fridge in a fridge (or a fridge in a box in a fridge, etc.).
> 
> This is indeed a very `popular' problem. On June 21 this year Josh
> Berdine posed almost the same question (without wine and food, alas).
> On 28 June 2020 I sent the reply with three solutions. Perhaps it
> would be easier to point to the code, which also has many comments and
> explanations:
> 
>        http://okmij.org/ftp/tagless-final/subtyping.ml
> 
> The gist of the first two solutions is to exploit the fact that
> tagless-final is sort of isomorphic to GADTs. That is, lots of things
> that can be done with GADTs can be done without (or with GADTs hidden
> away). That hiding has benefit of no longer bringing the problems with
> variance. No GADTs (at least, not in the part facing the user), no
> variance problems, at least, not for the end user. The library author
> may use regular ADT, which are also non-problematic. A regular ADT
> doesn't have the same typing guarantees -- but the typing is enforced
> by the signature (at the module level), so there is no loss.
> 
> I was going to write an article for my web site explaining this and a
> few earlier answers to the similar problems. Maybe I will eventually
> get to it.

Francois, your examples is way better than mine! :-)

Apologies for dropping the ball before, I got busy and there was some chaos going on.

But Oleg, thank you very much for digging into this so thoroughly and making such concrete suggestions!

There are some points I'm unsure of. My understanding of `Reducer` is that it is a way of implementing a particular (reduction) function on expressions from this little language, where rather than the "initial" approach of defining an explicit datatype for the expressions and then reducing them, you use constructor functions that eagerly perform the reduction, and extract the result with `observe`.

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? One possibility would seem to be to revise your second solution (say) so that `'a Reducer.t` is `'a * int list` instead of `'a`, and revise the constructor functions to compute this list of ints eagerly.

My working assumption is that which operation on the expression will be performed isn't known at the time when they are constructed. Otherwise a variant of the whole `Reducer` module could be defined for each operation, each with its own `'a t` type defined as appropriate.

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. One approach would be to change `Reducer.t` to a sort of abstract syntax, but this seems to me to lead straight back to the original `'a exp` type. This is, as far as I understand, coming up against the usual situation where the "initial" representation is syntactic in nature and the "final" representation is semantic. I don't know how much is known about handling such cases in the final style though.

Does it sound like I simply have not understood your solution? :-)

Cheers, Josh


> On Jun 27, 2020, at 4:36 PM, Oleg <oleg@okmij.org> wrote:
> 
> 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.
> 

Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved)

[François Pottier]

On 06/10/2020 at 21:04, Josh Berdine wrote:
 > Francois, your examples is way better than mine!:-)

Thanks :-)

As far as I understand Oleg's solutions, they all boil down to the same 
idea,
which I have considered, but is only half satisfactory: that is, to 
publish a
covariant abstract type +'a t which internally is implemented as an
abbreviation for an unparameterized type u. (See the food/wine/fridge 
example,
rewritten in this style, below.)

As far as the user is concerned, this works: the relaxed value restriction
works, so in my example, "meat" receives a polymorphic type, and I am happy.

The reason why this solution is only half satisfactory is that inside the
abstraction barrier, we have an unparameterized type u that does not express
the desired data invariant, so we cannot exploit the invariant to prove that
certain branches in the code are dead.

Also, the user cannot perform case analysis, since the type 'a t is 
abstract.
This is not a problem for me, but could be a problem in other situations.

Certainly, this is better than nothing, so I may end up adopting this 
approach
(thanks again Oleg!).

I am still curious, though, to know why my original type +'a t is not
recognized as covariant by the OCaml type-checker...

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

module T : sig

   type +'a t

   val wine: [> `Wine ] t
   val food: [> `Food ] t
   val box: 'a t * 'a t -> 'a t
   val fridge: [< `Wine | `Food ] t -> [> `Fridge ] t

end = struct

   type u =
     | Wine: u
     | Food: u
     | Box : u * u -> u
     | Fridge: u -> u

   type 'a t = u

   let wine = Wine
   let food = Food
   let box (t1, t2) = Box (t1, t2)
   let fridge t = Fridge t

end

open T

let food() = food
let meat = food()              (* the relaxed value restriction works *)
let _ = box(meat, fridge wine) (* place the meat beside a fridge *)
let _ = fridge meat            (* meat can still be put into fridge *)

Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved)

[Josh Berdine]

> On Oct 6, 2020, at 8:18 PM, François Pottier <francois.pottier@inria.fr> wrote:
> 
> I am still curious, though, to know why my original type +'a t is not
> recognized as covariant by the OCaml type-checker...

Jacques helpfully gave a precise answer earlier:

> On Jun 22, 2020, at 8:39 AM, Jacques Garrigue <jacques.garrigue@gmail.com> wrote:
> 
> The best I can say is that this combination of GADTs and polymorphic variants is not supported.
> There are actually two distinct problems:
> * GADT indices must be invariant
> * refinement of row types (both polymorphic variants and object types) is only partially supported
>  (you can instantiate an existential row only once)
> 
> So I wouldn’t suggest investing time in trying to outsmart the type system in this direction.
> The best you could achieve would be discovering a soundness bug (which should of course be promptly reported).
> 
> If your goal is just to move the polymorphism from the type itself to its parameter, using normal phantom types (maybe combined with phantom types to allow pattern matching) could help you, even if it may leave a few runtime checks.
> 
> Otherwise, you may try to encode your domain in a proper GADT, not using polymorphic variants.
> There are ways to keep some degree of subsumption.
> 
> By the way, I’m not sure what you mean by “weaker exhaustiveness” of polymorphic variants.
> I agree that polymorphic variants give weaker typing, it that they infer the declarations, but at least closed pattern-mathcing on them do guarantee exhaustiveness.

Jacques, I am sorry that I failed to address this before. I did not mean to imply that there was a problem, by "weaker exhaustiveness" I only mean that for a pattern match that is missing an intended case, the type error involving the inferred type can end up "far away" from the point of the mistake in the code. One way around this is to add type more annotations so that an incompatibility cannot propagate as far. But this relies on programmer-discipline rather than being irrefutably enforced by the type system.

Cheers, Josh


> Jacques
> 
> P.S. Here is an example of specific domain encoding:
> 
> type ‘a number = Number of ‘a
> 
> type _ exp =
> | Integer : int -> int number exp
> | Float : float -> float number exp
> | Add : ‘a number exp * ‘a number exp -> ‘a number exp
> | String : string -> string exp
> 
> or
> 
> type number = Number
> 
> type _ exp =
> | Integer : int -> number exp
> | Float : float -> number exp
> | Add : number exp * number exp -> number exp
> | String : string -> string exp
> 
> Basically, you must choose between what is static and what is dynamic.
> 
> On 21 Jun 2020, at 18:10, Josh Berdine <josh@berdine.net> wrote:
>> 
>> I wonder if anyone has any suggestions on approaches to use GADTs with a type parameter that is phantom and allows subtyping.
>> 
>> (My understanding is that the approach described in 
>> "Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013"
>> hasn't entirely been settled on as something that ought to be implemented in the compiler. Right? Is there anything more recent describing alternatives, concerns or limitations, etc.?)
>> 
>> 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:
>> ```
>> let widen_index x = (x : [`Integer] :> [> `Integer | `Float])
>> ```
>> 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
>> ```
>> 
>> I'm not wedded to using polymorphic variants here, but I have essentially the same trouble using a hierarchy of class types (with different sets of `unit` methods to induce the intended subtype relation) to express the index lattice. Are there other options?
>> 
>> I also tried using trunk's injectivity annotations (`type +!_ exp = ...`) on a lark since I'm not confident that I fully understand what happens to the anonymous type variables for the rows in the polymorphic variants. But that doesn't seem to change things.
>> 
>> Is this sort of use case something for which there are known encodings? In a way I'm trying to benefit from some of the advantages of polymorphic variants (subtyping) without the drawbacks such as weaker exhaustiveness and less compact memory representation by keeping the polymorphic variants in a phantom index. Is this approach doomed?
>> 
>> Cheers, Josh
>> 
> 

Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg]

> As far as I understand Oleg's solutions, they all boil down to the
> same idea, which I have considered, but is only half satisfactory:
> that is, to publish a covariant abstract type +'a t which internally
> is implemented as an abbreviation for an unparameterized type u. (See
> the food/wine/fridge example, rewritten in this style, below.)
Good summary!

> The reason why this solution is only half satisfactory is that inside the
> abstraction barrier, we have an unparameterized type u that does not express
> the desired data invariant, so we cannot exploit the invariant to prove that
> certain branches in the code are dead.

Indeed. That was the `imperfection' that I have referred to in my
message. I have two comments: first, there is the second solution,
which does exploit the invariant. Second, there may be more than one
abstraction barrier... That is, many implementations of the wine_food
signature may be in terms of some `more basic' signature -- or just
the same signature, if we are talking about term transformations (as I
have just replied to Josh Berdine).  Eventually we have to implement
the `most basic signature', and indeed we have to drop the indices and
fall into the `untyped' universe, so to speak. One hopes though that
this `security kernel' is really `most basic' and its operations are
few and primitive, so the correctness could be relatively easily
ascertained.

> Also, the user cannot perform case analysis, since the type 'a t is
> abstract.  This is not a problem for me, but could be a problem in
> other situations.

When I first mentioned tagless-final, in passing at a some conference
in Oxford a decade ago, an old Oxford professor (one of fathers of
SML) exclaimed: ``Isn't it bloody obvious that you cannot do
pattern-matching in this style!?''. I liked his phrase. Now I like to
say that pattern-matching in tagless-final style is not bloody, is not
obvious and is not impossible.

That it is always possible was proven by Boehm and Berarducci (their
proof was one inspiration for the development of Coq, as I heard). 
        http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
Although their general method works always, often one may design
simpler methods for particular pattern-matching tasks.

Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg]

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

RE: [Caml-list] Question on the covariance of a GADT (polymorphic

[David Allsopp]

Oleg wrote:
> > type 'a t =
> >    | Wine: [> `Wine ] t
> >    | Food: [> `Food ] t
> >    | Box : 'a t * 'a t -> 'a t
> >    | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t
> >
> > In this definition, the type parameter 'a is a phantom parameter. It 
> > is not used to describe the type of a value; it is used only to 
> > restrict the set of values of type "t" that can be constructed.
> >
> > The goal here is to allow storing wine and food (and boxes 
> > containing boxes containing wine and food) in a fridge, but forbid 
> > storing a fridge in a fridge (or a fridge in a box in a fridge, etc.).
> 
> This is indeed a very `popular' problem. On June 21 this year Josh 
> Berdine posed almost the same question (without wine and food, alas).
> On 28 June 2020 I sent the reply with three solutions. Perhaps it 
> would be easier to point to the code, which also has many comments and
> explanations:
> 
>         http://okmij.org/ftp/tagless-final/subtyping.ml
> 
> The gist of the first two solutions is to exploit the fact that 
> tagless- final is sort of isomorphic to GADTs. That is, lots of things 
> that can be done with GADTs can be done without (or with GADTs hidden 
> away). That hiding has benefit of no longer bringing the problems with 
> variance. No GADTs (at least, not in the part facing the user), no 
> variance problems, at least, not for the end user. The library author 
> may use regular ADT, which are also non-problematic. A regular ADT 
> doesn't have the same typing guarantees -- but the typing is enforced 
> by the signature (at the module level), so there is no loss.
> 
> I was going to write an article for my web site explaining this and a 
> few earlier answers to the similar problems. Maybe I will eventually 
> get to it.

It is indeed popular - as are your historic answers, too :)
https://inbox.ocaml.org/caml-list/20130705102138.98516.qmail@www1.g3.pair.co
m/


--dra