FCM and modular implicits type system

Learning
, ,
1

I was reading the implicits paper again and playing with the explicits PR, but I couldn’t find a good answer for a question. Why implicits require a new way to deal with modules, besides of the syntax improvement? Can’t we just expand inference on FCM, maybe with restrictions?

Does expanding FCM to support better HKT makes the type inference undecidable somewhere?

Comparision

Some examples that are not currently possible, but I wonder if they’re possible.

module type Show = sig
  type t
  val show: t -> string
end
module type S = sig
  val show: (module S: Show) -> S.t
  val show: {S: Show} -> S.t
end

(* maybe needs a symbol to resolve the ambiguity when `v` itself is a FCM that implements Show? *)
let show (module S: Show) v = S.show v
let show {S: Show} v = S.show v

(* can we infer this? *)
let show md v =
  let module S = (val md: Show) in
  S.show v

Code

When I was looking on the explicits PR I noticed also that a Tfunctor is essentially a Tarrow where the left type is a packed module, the AST stuff is a problem tho, because currently unpack is an express

3 Likes