How to include module-type with variant-type?

Learning
1

Hello dear OCaml-ers,

    (* categorical fonctor *)
    module type Fonctor =
    sig
       type 'a t
       val map : ('a -> 'b) -> 'a t -> 'b t
    end

    (* minimalist intuition about a polymorph data collection *)
    module type DataCollection =
    sig
       include Fonctor
       val size : 'a t -> int 
       type index
       val member : index -> 'a t -> 'a
    end

Compiles Ok.

    (* Stdlib.List *)
    module StdList
    :
    sig
       include DataCollection
       with type 'a t = 'a list 
       with type index = int 
    end
    =
    struct
       type 'a t =
          'a list
       let map =
          List.map
       let size =
          List.length
       type index =
          int
       let member n l =
          List.nth l n
    end

    (* Stdlib.Array *)
    module StdArray
    :
    sig
       include DataCollection
       with type 'a t = 'a array
       with type index = int 
    end
    =
    struct
       type 'a t =
          'a array
       let map =
          Array.map
       let size =
          Array.length
       type index =
          int
       let member n a =
          Array.get a n
    end

Compiles Ok.

    (* type PairIndex.index *)
    module PairIndex
    =
    struct
       type index = Fst | Snd
    end

    (* a pair of values *)
    module Pair
    :
    sig
       include DataCollection
       with type 'a t = 'a * 'a
       with type index = PairIndex.index
    end
    =
    struct
       type 'a t =
          'a * 'a
       let map f (x,y) =
          (f x,f y)
       let size t =
          2
       type index =
          | Fst
          | Snd
       let member i (x,y) =
          match i with
          | Fst -> x
          | Snd -> y
    end

Does not compile because of a module-type with limitation.

Now a nested datatype from the paper Nested Datatypes by Richard Bird and Lambert Meertens 1998.

    (* type 'a NestT.t *)
    module NestT
    =
    struct
       type 'a t =
          | Nil
          | Cons of 'a * ('a * 'a) t
    end

    (* one nested datatype from the paper "Nested Datatypes"
     * by Richard Bird and Lambert Meertens 1998
     *)
    module Nest
    :
    sig
       include DataCollection
       with type 'a t = 'a NestT.t
       with type index = int
    end
    =
    struct
       type 'a t =
          | Nil
          | Cons of 'a * ('a * 'a) t
       (* same as Pair.map *)
       let pair_map f (x,y) =
          (f x,f y)
       let rec map : 'a 'b . ('a -> 'b) -> 'a t -> 'b t = 
          fun f -> function
          | Nil -> Nil
          | Cons(h,t) -> Cons(f h,map (pair_map f) t)
       let rec size : 'a . 'a t -> int = function
          | Nil -> 0
          | Cons(_,t) -> 1 + 2 * size t
       type index =
          int
       let rec member : 'a . index -> 'a t -> 'a =
          fun n -> function
          | Nil -> failwith "Nest.member"
          | Cons(h,t) ->
                if n=0 then h else 
                let x,y = member (n/2) t in
                if n mod 2 = 0 then x else y
    end

Does not compile because of the same module-type with limitation.

Is there a workaround that i can’t see ?
If not then i fear not even 1ML could solve my case because i don’t do computation at the language-module-level.

Thanks :slightly_smiling_face:

1 Like
2

Your first broken example is not compiling because variant types are nominal: any two definitions are non-equal, even if they are syntactically identical. (The same is true of record types and exceptions.) The result is that your Pair module doesn’t meet the signature that it claims to meet:

module PairIndex = struct
  type index = Fst | Snd
end

module Pair : sig
  include
    DataCollection with type 'a t = 'a * 'a with type index = PairIndex.index
end = struct
  ...
  type index = Fst | Snd (* This type looks like [PairIndex.index], but
                            it's not equal to it. *)
end

This is not so much a “limitation” of with type as it is an intentional property of the type system. The compiler gives a correct (but somewhat opaque) message:

Error: Signature mismatch:
       ...
       Type declarations do not match:
         type index = Fst | Snd
       is not included in
         type index = PairIndex.index

The following fixes are possible:

  • change the type inside Pair to be defined by type index = Pair.index (aliasing a nominal type preserves equality);
  • change both types to [ `Fst | `Snd ] (polymorphic variants are structural, not nominal, so equal-looking polymorphic variants actually are equal).

Your second example fails for the same reason: two (non-equal) nested list types of the same shape are defined, and then you assert that they are equal. The same solutions should also work in this case.

Hope this helps :slight_smile:

3 Likes
3

@SpiceGuid One more trick that might be useful in a more complete example: you can define index and reexport the constructors at the same time.

type index = Pair.index = Fst | Snd

Using this you declare the type index to be a nominal alias for the type Pair.index but also declare the constructors Fst and Snd to be aliases for Pair.Fst and Pair.Snd.

Note the following:

  • “Constructor aliasing” is in fact called “re-exported type definition”.
  • This constructor aliasing is local to the module unless you also mention it in the signature. However, doing so in a with type constraint on a module type requires some indirection.
  • It doesn’t help in this specific example, but if your expand your shrunk example back to your original problem, you find a use for it.
4 Likes