Critique of implicits

You could note that thanks to first-class modules we can make type first-class values, and mimic this behavior of Coq.

module type T = sig type t end
(* the type of types *)
type 'a typ = (module T with type t = 'a)

(* the type int as first-class value *)
let int : int typ = (module struct type t = int end)

(* the type list is a function from type to type *)
let list (type a) (t : a typ) : (a list) typ = (module struct type t = a list end)

let id (_ : 'a typ) (x : 'a) = x;;
val id : 'a typ -> 'a -> 'a = <fun>

id int 3;;
- : int = 3

id (list int) [1; 2; 3];;
- : int list = [1; 2; 3]

id int [1; 2; 3];;
Error: This expression has type 'a list but an expression was expected of type
         int
4 Likes

There is tremendous value in being able to print anything.

Imagine that you are a mere mortal walking into this universe. Not being able to inspect a running program–in a universally intuitive way–is an impassable obstacle.

On balance, this feature is a no-brainier to me.

4 Likes

Something similar works out pretty well even without first-class modules

type 'a typ = T
let int : int typ = T
let list (type a) (t : a typ) : (a list) typ = T
(* etc. *)

Indeed, that works too but, on the other hand, we’re loosing some information especially if we want to extend the usage of this encoding.

First, we do not ask the same question to the type checker:

module type T = sig type T end
type 'a typ = (module T with type t = 'a)

let list (type a) (_ : a typ): _ typ = (module struct type t = a list end);;
val list : 'a typ -> 'a list typ = <fun>

with your approach, the type infer for list will be more generic ('a typ -> 'b typ) hence we need to be more explicit in the type annotation.

Next, if we apply this trick to the sort function:

let sort (_ : 'a typ) (cmp : 'a -> 'a -> int) l = List.sort cmp l;;
val sort : 'a typ -> ('a -> 'a -> int) -> 'a list -> 'a list = <fun>

and we uncurryfied its type, we have:

val sort : 'a typ * ('a -> 'a -> int) -> 'a list -> 'a list = <fun>

the first argument has a type isomorph to the module type Ord with type t = 'a.

Fianlly, if we require that the type is also equipped with an equality function:

module type Eq = sig type t val eq : t -> t -> bool end
type 'a eq = (module Eq with type t = 'a)

let sort (_ : 'a typ) (eq : 'a eq) (cmp : 'a -> 'a -> int) l = ...

and we uncurryfied again its type, we better understand your solution to the diamond problem in section 3.3 of your article.

I don’t see why you say that. Your version looks at least as explicit to me.

On the overall the two versions are equally explicit but the information that the first-class module gives in the value language must be given in a type annotation with yours. Your proof-term is more generic hence you need to use the subtyping subsumption rule, in the form of a type coercion, to have the encoding well-typed.

module type T = sig type t end
type 'a typ = (module T with type t = 'a)

(* the return type parameter is left implicit, and inferred from the value term *)
let list (type a) (_ : a typ): _ typ = (module struct type t = a list end);;
val list : 'a typ -> 'a list typ = <fun>

with your encoding:

type 'a typ = T

(* if the return parameter is left implicit, the type inferred is more generic *)
let list (type a) (_ : a typ) : _ typ = T;;
val list : 'a typ -> 'b typ = <fun>

(* hence an explicit type coercion *)
let list (type a) (_ : a typ) : (a list) typ = T;;
val list : 'a typ -> 'a list typ = <fun>
1 Like

Hi,

I just read and watched content concerning the modular implicits and I think it’s a thrilling feature. But the activity on the development repo seems very low now, which is quite different from what people announce in their presentations. So, here are a few questions:

  • what’s the status of the feature? Is there still theoretical work to be done?
  • would it be ready for inclusion? If not, is it still on the roadmap?
  • what’s the expected process to get it merged at some point?

Thanks for any insight about what’s going on.

1 Like

There is a LOT of theoretical and typechecker-writing work to be done, which is why this thread is very premature. There was an early demo made of the feature and it got everyone excited, but it wasn’t a proper implementation. Do not expect this feature anytime soon.

4 Likes