Sketch of possible typelevel extension of principled metaprogramming

[odersky]

This is a sketch of a possible extension to support functional typelevel programming.
It's prose only, there is no implementation. The intention is that, before embarking
on an implementation we discuss the approach in general and the specific details.

[senia-psm]

Typo. Should be n - 1

[senia-psm]

There is no case _ => '0 brunch. Should it be something like "If the search fails it results in compilation failure"?

[liufengyun]

It's not clear to me how the typer checks that the result type is Concat[Xs, Ys] at the definition site of concat?

[odersky]

Very good question. I added a section explaining this. Essentially, we use only approximate typing for definitions and do the full typecheck at all expansion sites.

[senia-psm]

Typo "aupper"

[senia-psm]

Typo to to

[smarter]

Falsesy?

[Blaisorblade]

I’m reading and commenting as I go along. This is confusing. It is similar but not identical to “singleton types” à la Haskell (from Tim Sheard’s Ωmega), but unlike those it seems to mix type-level and value level. For numbers this seems to work, but how do you encode correctly the type Eq[A, B] so that it’s only inhabited if A and B are equal? It’s OK to use Peano numbers as examples, but I’d be wary of using them as evaluation.

With singletons you have both type-level numbers:

trait TNat
case object TZ extends TNat
case class TS(n: TNat) extends TNat

and value-level numbers, indexed by type-level numbers, so that Nat[N] has one inhabitant which is isomorphic to N, and so that you can operate on this number at both value and type-level since you have the number at both levels.

trait Nat[N <: TNat]
case object Z extends Nat[TZ]
case object S[TN](n: Nat[TN]) extends Nat[TS[TN]]

EDIT: before implementation it’d be nice to at least state a conjecture on what can be encoded. It’d be nice to get at least to inductive families.

EDIT: doh, I screwed up the code samples...

[odersky]

There's one bit of information I glossed over here: In the definition of case object Z I assumed it defines a type as well as an object. I.e. that we expand to

 lazy val Z: Z = new Z
 class Z extends Nat

Current Scala does not do this. We could of course always write the more explicit definition, in which case type Nat would become:

trait Nat
class Z extends Nat
val Z = new Z
class S[N <: Nat] extends Nat
object S {
  def apply[N <: Nat] = new S[N]
}

So that's what I meant in painful detail when I wrote the definitions of Nat. The other types are analogous.

[Blaisorblade]

I was assuming that Z.type exists; but S[N] surprised me because it is partly static and partly dynamic. So for instance I can’t convert Nat to a normal number at runtime. Anyway, I’ll try to figure out concretely what can be encoded in this style.

[odersky]

So for instance I can’t convert Nat to a normal number at runtime.

Indeed. Type arguments are erased, so there is not enough information available at runtime.

[Blaisorblade]

Are these macros or type-level functions? And if the latter, is it F/FOmega functions or can you also pattern-match on types? Here you just show pattern-matching on compile-time values.

[odersky]

They are macros that give rise to typelevel functions, as is explained in the following.

[Blaisorblade]

Dependently-typed languages give one answer, Ωmega gives a slightly different one, SMT solvers yet another one. There can be reasons to ignore all that, but I’m curious which ones they are.

[Blaisorblade]

I forgot to mention the application of SMT solvers, refinement types and Liquid Haskell/“Liquid Scala” (is that the name @gsps?), like in @gsps Scala’16 paper (https://conf.researchr.org/event/scala-2016/scala-2016-smt-based-checking-of-qualified-types-for-scala). I suspect refinement types have closer to industrial use than dependent types, since their typecheckers end up being “smarter” in many common scenarios.

[odersky]

I believe the fact that you cite in one sentence three different and competing approaches is sufficient reason to be wary whether any of them is ready. If one works out satisfactorily, fine. But right now we do not know, and unless you provide me with proof that one of these approaches would work in all cases at good efficiency without restricting the language in any way, I will stay with my position that "it is not yet clear".

[Blaisorblade]

In this case, we would not be typechecking the macro, we would be writing a contract on it and enforcing it at “macro runtime” (where “runtime” means the runtime of the staged code, so it’s still while Dotty runs, but it’s not when defining the type function but when running it; as usual with staging, we don’t have just compile-time and runtime). This is an interesting idea and it has certain advantages, but there are well-understood tradeoffs between typechecking and (macro) runtime enforcements of contracts and we should make sure those tradeoffs are appropriate.

It’d be IMHO important to not talk about types because they suggest the wrong assumptions. I can already foresee an example puzzler: “my type function ‘typechecks’ but fails at this new call site”. More annoyingly, bugs in a type-level library might be detected by some user. Calling these “contracts” might reduce the confusion a bit (though it might not be enough); but would this be worth using?
But since many languages can type-check type-level functions, I’d like a reason to do instead research on something new and unproven.
Maybe dealing with a typechecker for type functions is too hard for our target users?
But are there really people who want type-level programming but are willing to admit the downsides of typecheckers (beyond me)?

And if those people exist, are they willing to give up separate typechecking of type-level functions to avoid those downsides? I’m not. Sometimes it’s too hard faking dependent types, as Chlipala will tell to anybody who listens — but then, just don’t fake them at all.

[Blaisorblade]

Uh, the last paragraph was misleading — I just meant “looks like I’m not the target user”, which might be wrong. I’m not expecting Scala = Idris/Agda/..., I could rant about those langs for hours :-). But I’d like to tease out advantages and disadvantages as early as possible.

[odersky]

I think it's OK to use the contract analogy. But for me these are still types. It's quite analogous to (predicate) refinement types a la Liquid Haskell. Here again we might check them early or late, or check them at run-time.

[Blaisorblade]

It might be good to see more examples of the core language before choosing what’s the sugar we need.

I’ll need to think about this and I might well be wrong, but I doubt non-recursive desugarings are worth the surprises and bugs they cause. Doesn’t type inference on LMS already do better?
As a rule of thumb, metaprograms that aren’t structurally recursive are bugs. When TAing our programming language lab, it was easy to show bugs just by reading the metaprogram; here it’d take longer to figure out if there’s any and which they are.

[odersky]

Not sure what you are getting at here. How is this not structurally recursive?

[Blaisorblade]

What I was concerned about was “if the right hand side consists of a conditional”. What if the conditional is only part of the RHS, or nested inside other conditionals?

[odersky]

What I was concerned about was “if the right hand side consists of a conditional”. What if the conditional is only part of the RHS, or nested inside other conditionals?

Yes, we need to be more precise here. Any nested tree of conditionals (both if-then-else and query) qualifies.

[Blaisorblade]

If the goal is to avoid needing logic programming, why not allow matching on types? Allowing for implicit searches is pretty interesting idea, but detracts from that goal... and requiring implicit search to use pattern-matching/unification on types seems pretty roundabout?

[odersky]

Matching on types is problematic because that's super fragile for a rich type system with subtyping. This observation was the blocker why we did not do any of this before. Implicit search overcomes this blocker, so is IMO really important.

[Blaisorblade]

This sounds like a mixture of logic and functional programming. How does this interact with backtracking in implicit search? After some experiences with this mixture I’d like a good answer, because this sort of combination can be pretty tricky to program (or too hard to use) with if you don’t have control of backtracking.

[odersky]

The implicit query must be resolved at this point. If it is ambiguous it's an error. There is no backtracking over query conditionals.

[Blaisorblade]

Why can’t we just use _ and <:< together, and write Xs =:= HCons[_, type Xs1]? The semantics would be a conventional match, followed by throwing away X, per the usual semantics of _. No subtyping should be necessary.

Subtyping might instead be needed if Xs were a subtype of HCons[X, Xs1]. It’d be good to check how =:= and subtyping interact and if the interaction is acceptable in a wider range of use cases.

[odersky]

We could probably introduce

Xs =:= HCons[type _, type Xs1]

if we want to be fancy. But

Xs =:= HCons[_, type Xs1]

already means something else: That the type Xs is equal to the type HCons[_, T] for some T, where _ is a wildcard. If we write this out in terms of DOT it would be something like

HCons { type Hd; type Tl = T }

[Blaisorblade]

Good point, but doesn’t _ in Xs <:< HCons[_, type Xs1] also refer to a wildcard? Or what do I miss?

[odersky]

HCons[Int, Nil] <:< HCons[_, Nil] but =:= between the types does not hold.

[Blaisorblade]

Ah the existing example is already using the wildcard semantics, not the throw-away semantics! Hadn’t realized. For later: a syntax less ambiguous for readers might be nice.

[Blaisorblade]

Let me assume concat is a def not an inline def (see above).

We also need to make sure that the recursive call to concat typechecks — I can imagine ways in which it’d work, but one needs to pick a typechecking algorithm.

The sketched process does not seem to use type refinement — in particular, it seems that in this branch we don’t know that Xs is equal to HCons[X, Xs1], only that they’re convertible both ways. But then, the type of the RHS is HCons[X, Concat[Xs1, Ys]], while the desired return type is Concat[Xs, Ys] — without unifying Xs with HCons[X, Xs1], why would the two coincide? I now see concat is here a query conditional, but see above for why that might not work well enough.

Also, will the code still typecheck if I write the following?

    inline def concat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys): Concat[Xs, Ys] = ~ {
      case Xs <:< HNil => 'ys
      case Xs <:< HCons[_, type Xs1] => 'HCons(xs.hd, concat(xs.tl, ys))
    }

[odersky]

Good question. I would assume yes, but without coming up with a detailed algorithm I would not know for sure.

[LPTK]

This is a really important problem in practice, and not just in the context of metaprogramming – the type-checker does not leverage <:< evidence to refine the set of known subtyping relations.

One way I've found that works in Dotty (but not scalac) to help work around this problem is to define <:< as:

abstract class <:< [-A,+B] { type Ev >: A <: B }

Then we can use explicit type ascriptions to lead the type from one side to the other, as in:

def foo[S,T](xs: List[S])(implicit ev: S <:< T): List[T] = (xs: List[ev.Ev])

[Blaisorblade]

IIRC the Scala’17 paper on algorithmic DOT describes the very need for such ascriptions.

Though in Scala you can call <:< to use it as a coercion function, though IIRC Scalac (used to?) produce for this an actual method call (which JIT can probably inline).

[LPTK]

IIRC the Scala’17 paper on algorithmic DOT describes the very need for such ascriptions.

That's right! I was probably inspired by that talk when I found the trick.

Though in Scala you can call <:< to use it as a coercion function

Note that this is not sufficient by any account. In my example, it means we have to rebuild a new list xs.map(ev) which is purely accidental runtime overhead (not present in foo above). In some cases, it's not even possible to rebuild the value this way.

An even harder case is to use S in type argument position where a bound <: T is required. To make that one work, I think we'd need to use ev.Ev instead of S but also make ev.Ev equivalent to S, as in:

abstract class <:< [A,+B] { type Ev >: A <: B & A }

[Blaisorblade]

[On removing Ev]
Sure.

[automatically leverage subtype relations]

I should look at the paper again, but guessing for now: we can’t look arbitrarily deep into objects to find these relations (I guess), but a limited search might be useful?

I've tried that too, but it doesn't work with how subtyping knowledge is propagated:

One could then write foo[A, B <: A], and you have to with Scalac, but I thought Dotty tried to accept code like yours? If you can call foo, then A <:< B already proves that A <: B, no need to propagate the constraint at all call sites.

[sstucki]

Note that this is not sufficient by any account.

Good point, so I suspect I’m in favor of adding Ev. I think scalaz/cats have replacements for <:< (Liskov?), implemented with casts.

I just wanted to mention that as of v2.13 of the standard library, <:< finally behaves like Liskov inequality, i.e. you can now do casts at almost no costs (they are the identity function) even if the related types are deeply nested in other type operators, using substitute of liftCo/liftContra. E.g. if you have evidence p: A <:< B you get p.liftCo[List]: List[A] <: List[B] for "free" (you still need to call liftCo manually).

Adding Ev to <:< seems appealing, but – as you discussed – has the drawback of working only in dotty. It's also potentially brittle since it uses inconsistent bounds. Since the Ev version is "extensional" (i.e. the type checker can reason about Ev directly), it might cover more cases, but I'm not sure about this. Maybe someone has an example where the Ev version works but the Liskov version (liftCo/liftContra + explicit cast) does not work?

[LPTK]

Thanks @sstucki, I had missed that. It's good to know!

It's true that liftCo/liftContra are sufficient in the List example, but they can become quite more cumbersome to use, as the user needs to pass in a type lambda when the coerced type does not have the straightforward one-argument shape of T[_].

Here is an example where liftCo/liftContra actually cannot be used but where our approach works – or at least I don't see an easy way to use liftCo/liftContra in that case:

abstract class <:<[A, B] {
  type ConstrainedB >: A <: A & B // = B with constraints
  type ConstrainedA >: A | B <: B // = A with constraints
}
def foo[A,B<:A] = Set.empty[(A,B)]
def bar[A,B](implicit ev: B <:< A): Set[(A,B)] = foo[A,ev.ConstrainedB]

Not sure I understand why you say the bounds in <:< are inconsistent. Having an instance of it is a proof that they are indeed consistent. This might not happen in practice (for runtime performance reasons), but conceptually we would create a new instance of A<:<B for any A and B where we know A<:B, and encode that knowledge in the abstract type members.

EDIT: maybe you meant that they are not syntactically consistent.

[sstucki]

You welcome @LPTK! Regarding your comments:

Here is an example where liftCo/liftContra actually cannot be used (...)

Actually, this is a case for liftContra, but it's very cumbersome indeed. Here's a possible implementation:

trait QFun[A, -X] { def apply[Y <: X]: Set[(A, Y)] }
def bar[A,B](implicit ev: B <:< A): Set[(A,B)] = {
  type Ctx[-X] = QFun[A, X]
  def qFoo[A] = new QFun[A, A] { def apply[Y <: A]: Set[(A, Y)] = foo }
  liftContra[B, A, Ctx](ev)(qFoo).apply
}

The QFun and qFoo machinery is necessary because polymorphism/universal quantification is restricted to trait and method definitions in Scala. If the language had System-F-style quantifiers, we could have written the example as follows:

def bar[A,B](implicit ev: B <:< A): Set[(A,B)] = {
  type Ctx[-X] = ∀Y <: X. Set[(A, Y)]
  liftContra[B, A, Ctx](ev)(ΛY <: A.foo[A, Y])
}

But that's still much more clumsy than your version using bounds-based evidence directly.

Not sure I understand why you say the bounds in <:< are inconsistent.

Sorry for the confusion re. consistency. I'm using the following terminology (adopted from my thesis): the bounds A, B of an abstract type X >: A <: B are

• consistent if we can prove that A <: B (in the context where X is defined),
• inconsistent if we cannot prove that A <: B,
• absurd if they are inconsistent even as closed types.

The difference between inconsistent and absurd bounds has to do with assumptions. E.g. the bounds of X >: Any <: Nothing are inconsistent, no matter the context, so we say they are absurd. But in your definition of <:<, we can neither prove that the bounds of Ev >: A <: B are consistent nor that they are absurd because we really don't know anything about A and B (they are abstract).

One could instead write "possibly inconsistent" but, personally, I prefer the shorter version.

As for the safety of inconsistent assumptions, note that, while inconsistency doesn't break safety of DOT, it can make your compiler crash. In essence: reduction of open expressions under inconsistent bounds is unsafe, both for open terms and open types. And contrary to open terms, open types are routinely being reduced (at compile time).

[LPTK]

@sstucki

The QFun and qFoo machinery is necessary because polymorphism/universal quantification is restricted to trait and method definitions in Scala

Interestingly, since the recent introduction of dependent function types, we now have a lightweight way to do first-class polymorphism! Indeed, we can write types such as (x: {type T}) => List[x.T] => x.T...

So, using it to define liftContra as in:

abstract class <:<[-From, +To] {
  protected type Ev >: From <: To
  def liftContra[F[-_]](f: F[To]): F[From] = f: F[Ev]
}

We can, today, write with Dotty:

def bar[A,B](implicit ev: B <:< A): Set[(A,B)] =
  ev.liftContra[
    [-X] => (p:{type T<:X}) => Set[(A,p.T)]
  ](p => foo[A,p.T])(new Poly{type T=B})

Where trait Poly { type T } is just used to avoid a type inference problem we run into with a bare new{type T=B}.

[Blaisorblade]

Making concat inline allows using the rules for typechecking query conditionals, but it does not seem expressive enough. Usually type-level programming lets me define a proper runtime function concat and typecheck it once and for all; if we can’t do that, it seems we forbid lots of applications of HList. And to write a runtime concat we have to either do contract-checking for concat at the actual runtime, and define erasure for types like Concat[Xs, Ys] (so that type errors might manifest not just while running macros but while running functions), or to introduce symbolic evaluation.

[odersky]

I think this point illustrates that we have different expectations. Defining a runtime concat is possible only if the representation of types is homogeneous, so HLists or tuples are represented as normal lists at runtime. But there's no way we can or want to do this! So compile-time is the only option.

I think the root issue is that you are coming from a world that is not very applicable to our constraints. We want to achieve similar expressiveness as dependently typed languages, but in a language where efficiency matters, representations have to be specialized, and everything is subject to suptyping. This means we need to be inspired by the likes of C++ or D as well as the sources you cite.

Also, the whole proposal really makes sense only in conjunction with the new meta-programming proposal:

http://dotty.epfl.ch/docs/reference/symmetric-meta-programming.html

That's where the synergy comes from! Seeing this as an isolated approach to typelevel programming will lead you astray, IMO.

[Blaisorblade]

Thanks for linking to http://dotty.epfl.ch/docs/reference/symmetric-meta-programming.html, I’ll catch up and sorry if I jumped ahead too much. I also had to look at #2199 to understand the plans for tuples—but there seems to be a common Tuple type?

Overall, I’d just like to (help) understand and clarify limitations and tradeoffs of proposals like this, and get to some sweet spot — that is, try to remove any limitations that don’t buy something in exchange — not impose my preference about a certain sweet spot. Of course I’ll compare with related work I’m familiar with, even though that’s not perfect.

Here, you talk about usual type-level programming and standard HLists. So just to understand: is this meant to subsume existing Scala approaches, as the introduction suggests, or is this specialized for a few common scenarios? Current Scala designs allow a runtime concat in Scala today.* Now that you mention C++, maybe I understand better what you have in mind; I might later propose edits to the introduction to clarify what you mean. Yet, in C++ having to specialize everything can cause excessive code bloat, so I’d be afraid if we have to go there.

And is a runtime concat impossible also if I use some other data structure where I make different choices?

*I checked again https://apocalisp.wordpress.com/2010/07/08/type-level-programming-in-scala-part-6b-hlist%C2%A0folds/ and there are runtime operations—where the type is computed statically. Copy-pasted sample:

// construct a heterogeneous list of length 3 and type
//  Int :: String :: List[Char] :: HNil
val a = 3 :: "ai4" :: List('r','H') :: HNil
 
// construct a heterogeneous list of length 4 and type
//  Char :: Int :: Char :: String :: HNil
val b = '3' :: 2 :: 'j' :: "sdfh" :: HNil
 
   // append the two HLists
val ab = a ::: b

[senia-psm]

@Blaisorblade please take a look at this code sample, I hope you'll find it useful: https://scastie.scala-lang.org/senia-psm/zqIQMbtgTk6YQj6nlY7Ppw/13

In object concat_using_=:= you can find code that works in current version of dotty, but looks similar to concat implementation from this PR.

In part "using type macro" I described my understanding of possible runtime representations of concat(a, b).

Also you may take a look at manual_concatter for runtime representation of a ::: b.

[odersky]

Here's a tongue in cheek version to do a runtime concat:

trait Concatenizer[Xs <: HList, Ys <: HList] {
   def apply(xs: Xs, ys: Ys): Concat[Xs, Ys]
}

implicit inline def concatenizer[Xs <: HList, Ys <: HList]: Concatenizer[Xs, Ys] = new {
   def apply(xs: Xs, ys: Ys) = concat(xs, ys)
}

def runtimeConcat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys)(implicit conc: Concatenizer[Xs, Ys]) = 
  conc.apply(xs, ys)

That's indeed a runtime concat but it defers to an implicit that does the actual work and that is synthesized at compile time. The example you were pasting is the same in spirit. And yes, that can generate lots of code.

[Blaisorblade]

Well, here at least the values can be picked at runtime, so we keep a phase distinction and specialize per shape and not per values. I’m curious how much of the shape one needs to reify at compile-time, and if staging lets us have control of this.

But I’ll have to study more closely both HList and @senia-psm’s snippet!

[LPTK]

What's not explicit in the proposal is when a case-defined type like Concat[A,B] is expanded. In trait Concatenizer, it can clearly not be expanded because we don't know Xs and Ys yet. This seems to imply that expansion of a case-defined type T would happen only while checking that a term t has type T, as in the definition of apply in concatenizer where we check that concat(xs, ys) has type Concat[Xs, Ys]. Is that right?

[LPTK]

The status of the Concat[Xs, Ys] type in trait Concatenizer in relation with logic programming makes it appear that this approach is somewhat related to type projections.

A case-defined type such as Concat[A,B] can be encoded as type Concat[A,B] { type Out } (as in @senia-psm's code) where Out is the result of the type-level computation and where each case of the case-defined type is an implicit definition (potentially mutually-recursive with the other cases). Then Concat[Xs, Ys] in trait Concatenizer has to be Concat[Xs, Ys] # Out because there is no implicit value in scope at this point.

So this seems to regain some of the extra flexibility that we had with type projections (which was arguably one reason why they were so pervasive in type-level programming). Hopefully this new approach does not have the same soundness problems as type projections.

[senia-psm]

Usage of Concat in trait looks really confusing for me. I would expect something like this:

trait Concatenizer[Xs <: HList, Ys <: HList] {
  type Out <: HList
  def apply(xs: Xs, ys: Ys): Out
}
implicit inline def concatenizer[Xs <: HList,
                             Ys <: HList]: Concatenizer[Xs, Ys] { type Out = Concat[Xs, Ys] } = new {
  type Out = Concat[Xs, Ys]
   def apply(xs: Xs, ys: Ys): Out = concat(xs, ys)
}

[odersky]

Let's forget about the example, which was anyway tongue-in-cheek.

[Blaisorblade]

The intention is that, before embarking on an implementation we discuss the approach in general and the specific details.

I think that’s an excellent approach, and that’s probably necessary for an extension of such meta-theoretic complexity. I couldn’t resist making some comments as I read the proposal; apologies for any misunderstandings or nonsense I wrote — and sorry if I was too harsh at times.

I’ll get back to preparing for my defense, I hope we’ll have a chance to talk more about this!

[senia-psm]

Typo: =:

[nafg]

Possibly somewhat relevant: microsoft/TypeScript#21316

[DanielRosenwasser]

nornalizations -> normalizations

[Jasper-M]

I'm guessing you meant inline type def.

[Jasper-M]

Same here.

[odersky]

The current state of my thinking is now a part of #4616.