Implicit Type Constructor Parameters

Hemlock is currently transitioning to incorporate many of the design concepts first developed and synthesized in 1ML. Early this year we worked through some subtle design interactions between modules and algebraic effects, at the time oblivious to relevant previous work (i.e. the literature regarding applicative vs generative functors). Soon afterward this comment in an OCaml-focused discussion of polymorphic types led me to 1ML, and many epiphanies have followed as we continue to learn from the tour de force that is the primary 1ML papers [¹, ²].

A follow-on paper, “1ML with Special Effects” [³] caught our attention because although we had already arrived at a seemingly workable syntax/semantics for adding algebraic mutability/effects to the Hemlock design, 1ML’s clean, consistent abstraction for parametric types based on (skolemized) existential types caught our eye as a way to improve Hemlock. This conversion in Hemlock went well, but there was one necessary change relative to the primary 1ML papers we didn’t see coming.

What follows is all in the currently proposed Hemlock syntax; the differences with 1ML are minor. Consider the List.concat function signature, which returns the concatenation of two lists. The following two declarations are equivalent:

val concat 'a: list a -> list a -> list a
val concat: '(a: type) -> list a -> list a -> list a

The 'a parameter is an implicit inferred function parameter, but it can conceptually be thought of as a normal function parameter even though in the final executable program it has no representation. This same idea applies to type constructors. Take a hypothetical polymorphic pair type as an example:

type pair 'a 'b: pair a b =
    fst: a
    snd: b

This syntax is actually more verbose than 1ML’s, which would be something like type pair a b = {fst: a; snd: b}. Notice the lack of pair 'a 'b:. When we add parametric mutability/effects (^m/>e), it becomes clear why the implicit parameters must be explicit in the type declaration. The following declares a type for a function which operates on a parametrically mutable polymorphic array and has parametric effect.

type t 'a ^m >e: t a m e = ^m&array a >e-> uns

Without the explicit t 'a ^m >e[⁴] in the type declaration, how would we know what kinds of parameters t takes?

Now that we have a workable type constructor syntax, this all seems terribly simple, but I admit to scratching my head over multiple design sessions trying to understand how parametric type constructors could even work with mutability/effects integrated. In retrospect the following quote from the “Future Work” section of [3] should have caught our attention:

Effect Inference. In the current paper we have only investigated the explicitly-typed fragment of 1ML. We believe that it is straightforward to incorporate implicit functions over effects to full 1ML, and enable the inference of effect parameters and arguments, just like for types.

Citations & footnotes

1. Andreas Rossberg, Claudio Russo, and Derek Dreyer, “F-ing modules,” JFP 24 (5): 529-607, 2015. ↩

2. Andreas Rossberg, “1ML — Core and modules united,” JFP 28 e22, 60 pages, 2018. ↩

3. Andreas Rossberg, “1ML with Special Effects,” LNCS 9600, pages 336-355, 2016. ↩

4. It’s awfully tempting to refer to this as the TAME type system. ↩