Help me understanding this nested functor that creates unique types each time is called

Learning
1

Hello!
The other day, I asked for help on the reason discord about how to generate several Units modules without repeating a lot of boilerplate. Someone proposed a great solution that works exactly as I needed. for reference, here it is:

module Unit: {
  type t('a);
  let (+): (t('a), t('a)) => t('a);
  module Make: () => {
       type id;
       let fromInt: int => t(id);
    };
} = {
  include Float;
  type t('a) = float;
  let (+) = (+.);

  module Make = (()) => {
    type id;
    let fromInt = float_of_int;
  };
};

Then I can easily use it to create units that are just floats, but that I can’t mix, exactly what I needed:

module Seconds =
  Unit.Make({});
module Milliseconds =
  Unit.Make({});

While the code works wonderfully, I don’t fully understand it and that is where I want help. I consider that the person that provide this helped me enough already, and I also prefer the forum format to the chat one, so that’s why I’m asking my questioning here. So far I understand the code with my intuition, this means that I see the code and think: yes, this obviously does what I want, I feel it. But when I try to analyse it the details go blurry and I feel confused and frustrated, just like what happens when you try to remember a dream and tell it to someone else. Using something that I don’t understand fully is something my brain does not allow me to do :smile:

Sorry if I rubber ducky you a bit, but this is what I understand:

The nested functor Make captures its context, just like a closure will do, so it knows about the fact that t(a) is just a float (more questions about this latter). Because Make is a functor, it is creating a new version of it’s contents every time it is called, that is how every time you call it you get a different type id that are not compatible between them, even though they are all just empty.
Maybe my understanding of Ocaml type system is too rigid or archaic, but the thing that confuses me the most is the assignment of type t('a) = float. For me the type variable should always be filed, otherwise it does not make much sense, but here it is just completely being re-assigned to a plain type :crazy_face:
If I put the more abstract hat and I decide that types and code are just two different programming languages I can calm down my anxiety enough to understand how the types work: the Unit.t type is both, generic and abstract, and the Make.id one is just abstract (phantom, opaque), making them impossible to see from the outside. Make.fromInt then puts the unique Make.id into Unit.t binding this two to create a third type unique to each module, but because we latter declare Unit.t to be just a float, including the type parameter like this: t('a) = float, this effectively turns all the types contained on it to also be just plain floats. This is why latter there is no need (probably not even possible) to concrete/declare the type id at all, it serves no purpose in the “implementation world”, it is just a needed artifact in the types parallel universe.

Am I correct in my understanding?
Is this a common practice? Does it have any particular name? Where can I learn more about neat type tricks like this one?

2

This code makes use of three features:

  1. Abstract types. While the module body defines type t('a) = float;, it has the ascribed signature type t('a);, which prevents clients from seeing the actual implementation’s type. Therefore, the typechecker cannot know that t('a) = t('b) even if 'a and 'b are different.
  2. Generative functors. Generative functors generate new types whenever they are applied. Unit.Make is a generative functor because it takes a () input. If you have module Seconds = Unit.Make({}); and module Milliseconds = Unit.Make({});, Seconds.id and Milliseconds.id are different types.
  3. Phantom types. This is a technique of defining a type parameter as a “tag,” which does not appear in the actual type definition, to distinguish between two types that are internally the same. In the type t('a), 'a is a phantom type parameter, and t(Seconds.id) and t(Milliseconds.id) are different types, despite both being float internally, because the id types of the two modules are different.

To answer your train of thought:

The nested functor Make captures its context, just like a closure will do, so it knows about the fact that t(a) is just a float

Yes. Nested modules can see the implementation details of the outer module.

Because Make is a functor, it is creating a new version of it’s contents every time it is called, that is how every time you call it you get a different type id that are not compatible between them, even though they are all just empty.

Not quite. By default, functors are applicative, meaning that all types defined by all applications of the functor to the same input will be equal. However, the (()) => part makes the Make functor generative, so it does create new types upon each application.

Maybe my understanding of Ocaml type system is too rigid or archaic, but the thing that confuses me the most is the assignment of type t('a) = float. For me the type variable should always be filed, otherwise it does not make much sense, but here it is just completely being re-assigned to a plain type

This is what a phantom type parameter is. It’s no more complicated than doing let f _a = 0. in the term-level language: _a does not appear on the right side of the =.

If I put the more abstract hat and I decide that types and code are just two different programming languages I can calm down my anxiety enough to understand how the types work: the Unit.t type is both, generic and abstract, and the Make.id one is just abstract (phantom, opaque), making them impossible to see from the outside.

The term “phantom” specifically refers to the use case I describe above, where a type parameter does not appear in the actual type definition, but acts as a “tag.”

2 Likes
3

What do you think of this approach?

 module Unit : sig
    type _ t = private float
    type _ w = ..
    val (+) : 'a t -> 'a t -> 'a t
    val from_float : float -> 'a w -> 'a t
  end = struct
    type _ t = float
    type _ w = ..
    let (+) = (+.)
    let from_float x _ = x
  end

usage:

type min
type kilo

type _ Unit.w += M : min Unit.w | Kg : kilo Unit.w

let m = Unit.from_float 4.33 M
let k = Unit.from_float 23.0 Kg

let fails = Unit.(m + k)

It achieves similar type strength but using a different route from generative functors: witnesses and extensible variants. I’m not experienced enough to weigh its advantages from an API designer’s standpoint though.

1 Like
4

I don’t know about them,will investigate it. Why does the from float take an extra argument?

5

you need to fill the 'a in 'a t somehow. float alone doesn’t give the type system enough information to fill it. the functor solution gives you it via functor application, bringing an abstract unique id, and this gives you it via function application on some witness data.type which carries the type info by definition.

1 Like
6

@hyphenrf your variant don’t guarantee that units cannot be added to a any unit

type m
type s
type _ Unit.w += Any: 'a Unit.w | M: m Unit.w | S: s Unit.w
let poison () = Unit.from_float 4.33 Any
let s = Unit.from_float 1. S
let m = Unit.from_float 1. M
let accepted = Unit.( poison () +  m)
let still_accepted = Unit.( poison () + s)
1 Like
7

Thinking about generative functors… Does that mean that I can not parametrize the generated module? Is there any way to get both things?

8

Generative functors have their last (right-most) argument as unit, that is (). That doesn’t stop you having preceding arguments.

9

That’s perfect, thanks

10

How does the functor version ensure such intentional subversion by the programmer is not expressible? I’m not familiar with the module language enough, is it not possible to inject poison in the functor definition at all?

11

The important point is that the Make functor is part of the trusted core of the Unit module.

The users of the Unit module cannot modify the existing Make functor and they cannot implement their own Make: each application of the inner generative functor Make creates a fresh type id and an unique function of type int -> id tand this function is the one and only way to create a value of type id t.

1 Like