Exisential types and types variables equality

Learning
,
1

I try to write an heterogenous formatter for learning purpose, and i’m stuck on a type variable equality issue i think, here the code :

module IdList = struct
  type (_, _) t =
    | [] : (_,Peano.zero) t
    | ( :: ) : 'a * (_, 'n) t -> (_, 'n Peano.succ) t
end

module FList = struct
  type _ t =
    | [] : Peano.zero t
    | Literal : string * 'n t -> 'n t
    | Hole : ('a -> string) * 'n t -> 'n Peano.succ t

  let ( ^ ) str fmt = Literal (str, fmt)
  let string fmt = Hole ((fun x -> x),fmt)
  let int fmt = Hole (string_of_int,fmt)
  let bool fmt = Hole (string_of_bool, fmt)
  let ( ^^ ) f x = f x
end

let mprintf fmt args =
  let rec aux : type n a. n FList.t * (a, n) IdList.t -> _ = function
    | FList.[], IdList.[] -> ""
    | FList.Literal (x, xs), args -> x ^ aux (xs, args)
    | FList.Hole (to_string,xs), IdList.(x :: args) -> (to_string x) ^ aux (xs, args)

In particular : | FList.Hole (to_string,xs), IdList.(x :: args) -> (to_string x) ^ aux (xs, args)

I got this error :

This expression has type $::_'a but an expression was expected of type
         $Hole_'a

What I think I’ve understood from this error is that the type variable introduced by the definition of the Hole constructor, is not equal to the one introduced by the definition of the ( :: ) constructor. This seems normal to me, but how do I tell the compiler that I want these two variables to be equal? Is this feasible?

At first glance, I naively thought that this would be an opportunity to use Refl, which I’ve just learned. But no, the two type variables are hidden inside the two existential types. If I had to take them out, I’d be stuck too, since I’m simulating heterogeneity.

Any help is welcome !

2

Your problem starts with this definition

that makes the type of elements existentially quantified. Notice in particular, that the first parameter of the type constructor is never specified: it is a is phantom type parameter. Consequently a value of type (_, 'nat) t is a list of elements of unknown types with length equal to the integer represented by 'nat.

Since the type of the elements of the list is unknown (and can never be recovered), elements of the list can only be manipulated by polymorphic functions which is not what you wanted.

The solution is thus to avoid hiding type information by introducing existential types. This means that the types of the elements of the list must be reflected in the type of the lists. If we remove the peano encoding of the list length, your first definition can be simplified to

type void = |
type 'a hlist =
| []:  void hlist
| (::): 'a * 'b hlist ->  ?? hlist

The important point is then that the type of the hlist constructed by (::) needs to keep track of both the type of the inner list and the type of the first element.

The simpler solution is thus to concatenate the two types with *:

type 'a hlist =
| [ ]:  void hlist
| (::): 'a * 'b hlist ->  ('a * 'b) hlist

(which is unsurprisingly building a list of types at the type level).

4 Likes