Parametrized types in first class module

Learning
1

Hello everyone !

I’m trying to transpose a parametrized enum type into a first class module, but I’m stuck with a limitation from the compiler.

Let say I have this type:

type 'a expression =
  | Litteral of string
  | Path of 'a
  | Concat of 'a expression list

In order to remove this enum, I’ve moved each case in a dedicated module, with a common signature in order to unify them:

module type EXPRESSION = sig
  type 'a t

  type ('a, 'b) of_t = ('a -> 'b) -> 'a t -> 'b

  val to_string : ('a, string) of_t
end

Now I want to build a type which allow me to work with thoses values, but the compiler refuse to let me do this:

type 'b expression = 
    E:(module EXPRESSION with type 'a t = 'b t ) * 'b t -> 'b expression

Error: invalid package type: parametrized types are not supported

I understand that OCaml does not have higher kinded-type variables, and I would like if there is a workaround which allow me to encode this type.

Thanks !

1 Like
2

What is 'b t here?

Cheers,
Nicolas

3

What is 'b t here?

It’s a constraint type, which tell the compiler that for any instance of E, you have a consistency between:

  • the first element in the pair (the module)
  • the second element in the pair (the type)

and with this constraint, you should be allowed to call any function of EXPRESSION without knowing the type carried in the existancial:

let print_expression
   : ('a -> string) -> expr -> string
   = fun f (E ((module E), t)) -> 
            E.to_string f t

It is like the example given in the OCaml manual, but the both types are inside an existancial type instead of being to two arguments given in the function. This kind of pattern works fine… except when you have a parametrized type! As I’m pointing the manual, I know this not working:

his subset consists of named module types with optional constraints of a limited form: only non-parametrized types can be specified.

So this why I’m looking for a workaround! (let me know if I’m not clear enough)

4

As you noted, higher-kinded types are unavailable and these kinds of parameterized types cannot be specified in package-type constraints. However, you could use the following (potential) workaround:

module type Expression = sig
  type a
  type t

  type 'b of_t = (a -> 'b) -> t -> 'b

  val to_string : string of_t
end

This removes the parameterization from t adding it to the module using the type a.

You could then have the following definition for expression:

type 'a expression = 
  | Expr : (module Expression with type a = 'a and t = 't) * 't -> 'a expression
2 Likes
5

Thanks ! This is working.

For the thread completeness, here is a how to unpack the value and call the function:

let print_expression : type a. (a -> string) -> a expression -> string =
 fun f (Expr ((module E), t)) -> E.to_string f t
1 Like
6

So, finally this solution does not work as expected as I can’t build create a module with the expected signature, because the type a is local in each module (and abstract):

(* an example type for my ['a] *)
type content

let build : unit -> content expr =
 fun () -> 
(* Create the existancial type. I try to coerce the type [a] into my local type as I would do with a polymorphic type *)
Expr ( (module Litteral : EXPRESSION with type t = string and type a = content)
  , "value")

Error: This expression has type
         (module EXPRESSION with type a = Litteral.a and type t = string)
       but an expression was expected of type
         (module EXPRESSION with type a = content and type t = string)
       Type Litteral.a is not compatible with type content

I will see if I can switch to objects or records. But I think there is no solution for this problem here, sooner or later I will stuck again.

7

Another fix for this would be to parameterize Literal with a type for a. e.g.

module Literal (T : sig type t end) : Expression with type a = T.t and type t = string = struct
  type a = T.t

  type t = string

  ...
end

You could then write build as follows:

type content 

let build : unit -> context expression = 
  let lit = 
    (module Literal (struct type t = content end) 
      : Expression with type a = content and type t = string)
  in  fun () -> (lit, "value")

However, this is probably a bit heavyweight for what you’re looking for. This type of openness and extensibility could be more easily and naturally achieved using objects or extensible variant types.

1 Like
8

It’s not clear from your example that you should even consider first-class modules. In the end, you are currently ending up with a type isomorphic to:

type 'a expression = ('a -> string) -> string

… as the existential 't in the GADT (module S with type t = 't) * 't is unusable for anything, except as the single possible argument for to_string, so you may as well pre-apply it (and get rid of it)… Even if your signature is a bit more complex and actually requires the explicit 't, this sort of code generally ends up reimplementing a half-baked object oriented style. Did you really need to get rid of the original type sum? (why do you need the extensibility?)

(If you are doing this for fun and learning, then you might be interested in the Lightweight higher-kinded polymorphism paper and its implementation by the brands library for the original issue with a polymorphic type constructor.)

9

This is for a semi-personnal project, and I am in the phase of cleaning the code. Right now the sum type is exposed and used in differents modules in the application. If I add a new case, I have to update the code in differents location — and I know I will need to add more cases later.

I could just keep the code as is but it is also a way to go deeper in OCaml and switch from the “utility code” into a “learning session”. Here I have an actual example of a pattern I could reuse later, so it’s better to see what I can do or not :slight_smile:

Thanks for the pointer, I’ll take a look in this!