The future of types

[distractedlambda]

I wanted to jot down thoughts that have brewed in my head since we put type-system work on hold; eventually, I'm hoping this could yield a design sketch to guide implementation.

Background

Why Types are Needed

In the strictest sense, Pille does not really need much; it needs to be able to ascribe a machine representation to each and every value produced by the program, but this can be (and is, in the bytecode language) represented by a small type grammar roughly matching a subset of LLVM.

In practice, however, I think Pille needs ways to associate an extensible set of static information with expressions and bindings; the spmd language is one concrete use-case, but more generally "type-driven metaprogramming" is ubiquitous in systems-programming languages (that aren't C), and IMO for very good reasons.

We could base our design off of the statinfo mechanism in Rhombus, but I don't think that that quite fits the Pille use-case. Rhombus does not really use static information to check assignability, and instead usually relies on runtime-checked annotations to enforce API invariants. With Pille, we need to be able to perform such checks statically by default, with runtime checking being some sort of opt-in or derived construct (if present at all). It's not immediately obvious to me how Rhombus-style static information would be adapted for assignability checks; we could get some sort of subtyping-like relation if were able to treat static information as lattice points, which seems like it might be possible, but also seems like it could introduce plenty of its own problems (especially in reporting "type mismatches"). Alternatively, I could imagine having an entry in static information that indicates some nominal type identifier, but at that point it feels like we have just added traditional types anyways.

Therefore, my current thinking is that Pille needs some sort of type system (where each value has a single type that you can talk about as its own thing, and in relation to other types in terms of assignability, convertibility, etc.).

Why The Current System Is Insufficient

Pille already has a static type system, which I attempted to make extensible and supportive of pseudo-polymorphic constructs. In particular, it supports definition of arbitrary new type constructors, it does not much constrain the arguments to those type constructors (they're just syntax objects), and it has a "type method" system that delegates certain extensible operations (such as implicit coercions) to types themselves (and which permits definition of new and arbitrary type methods).

Unfortunately, I've not found the extensibility to work out how I hoped. Type methods end up being an extremely low-level mechanism, and are somewhat error-prone in how they distribute functionality. For instance, implicit coercion is one type method, while picking "common types" (to resolve type mismatches that could be fixed with coercions) is another; it is up to the type definition to make sure these are implemented in a manner consistent with each other. Beyond what might have just been my own poor API-design choices, type methods suffer heavily from the bidirectional method problem when you try to express operations that relate multiple types (which turns out to be many useful operations).

More fundamentally, the type system does not assume any relationship between different instantiations of the same type constructor, and there is no notion of holes or type variables; accordingly, there is no way to express "partial constraints" in the bidirectional type system, which would seem to hinder its power. For instance, an operation that knows it needs some Int(...) from a subexpression, would still not be able to give an expected type for that subexpression, unless it knows that it needs exactly an Int(N) for some N. Along the same lines, there is no standardized notion of polymorphism or parametriticity, not even in the sense of e.g. C++ templates, which means that generic operations end up using hand-written type-dispatching code (for which it is not always straightforward to document a "type signature").

Design Thoughts

Research?

If a new type system is something that could itself be an interesting contribution--maybe because it does something new and interesting with types and macros, or maybe just because it does something new and interesting with types in the systems-programming context--then it would seem like something to really dig into, and plan to write a paper about.

If that's not going to be the case, then the goal changes to unblocking other avenues of exploration. To be clear, I think the current type system is a blocker, but there's possibly a large delta between what would sufficiently un-block, and what would actually be an intellectually-interesting thing.

"Checked" Generics?

Looking at prior art (C++, Zig, Rust, Swift, etc.), a major design point would seem to be whether "generic" code is type-checked on its own (Rust, Swift, seemingly Mojo), or if instead type-checking is just part of monomorphisation (C++, Zig). The former seems a massive win for tooling (and, as a consequence, language ergonomics), but in my experience languages that take that path end up playing catch-up to the latter in terms of compile-time expressiveness.

Since C++ and Zig defer much of their semantic analysis until monomorphisation, they get to keep most interesting semantics defined in terms of concrete types. Checking of type-equivalence remains trivial, overload resolution can easily incorporate priority logic and side-conditions, and type-level computation can be more or less arbitrary (which in the case of C++ and Zig, means compile-time evaluation of runtime-language code). So, for instance, a return type can be expressed as an if condition on a parameter type, but type-checking only ever actually has to deal with the branch of the if that ends up taken on a given monomorphic path.

Rust and Swift aim to do all interesting type-checking and overload resolution prior to monomorphisation, and so they end up employing sophisticated parametric polymorphism with typeclasses, including dedicated (but limited) constraint languages; even so, they struggle to do quite the same things that C++ and Zig enable. Rust is still working on support for specialization, for instance. A part of me wants to try to push the needle here, since somehow having the tooling of Rust/Swift and the power of Zig is extremely appealing; the rest of me feels in no real position to contribute, given the resources that these production languages are already putting into it.

Where Do Macros Fit In?

When I initially started exploring types in Pille, I imagined a powerful back-and-forth between macros and type-checking, and was ecstatic (well, maybe not quite) about macros that could observe and react to contextual type information (something Lean also supports). The more I dwell on this, though, the more I feel like this is probably not a good idea for Pille.

In a language in which each bit of surface syntax is type-checked once, it probably can work well (Lean would seem to be evidence); the problem I'm seeing is in Zig/C++-style typechecking-during-monomorphisation, where a piece of surface syntax in a generic context cannot be type-checked until a use-site, and may end up being type-checked multiple times (with different concrete types). If types can alter the interpretation of syntax (by way of a macro that observes the expected type), then a corollary in this context is that you don't know the interpretation of syntax at the initial definition of generic code, and also that there could be multiple interpretations in effect simultaneously in a full program. This seems like an unacceptable compromise to me.

The direction which I imagine now is somewhat less exciting: there would be a type-oblivious surface language, built out of traditional type-unaware macros, and the result of expanding those would be an intermediate form that we somehow know how to type-check and monomorphize. Then, likely, this intermediate form would also allow a different kind of macro ("typechecking" or "monomorphisation" macros?), but these would not be able to call the surface-language expander on sub-terms (because of the aforementioned issues with delaying this, and also because the original expansion-time environment of the surface-language would have been lost by this point).

[rfindler]

It looks like Aaron Turon merged something to Rust in 2015?

[distractedlambda]

It looks like Aaron Turon merged something to Rust in 2015?

That appears to "just" be the initial prototype implementation; according to the tracking issue, the TO-DO list items from the original PR still apply today (including a known soundness hole).

(Rust includes prototype features, even half-broken ones, in the main branch behind feature flags)

[rfindler]

Can you give an example why having a type system that type checks with variables is not as good as type checking after the variables have been filled in?

[distractedlambda]

Can you give an example why having a type system that type checks with variables is not as good as type checking after the variables have been filled in?

Maybe this is not the most compelling example, but I think of something like IntFittingRange in the Zig standard library. It's a type-level function that returns the minimal integer type that can represent all values in some compile-time-known range.

Since "variables have been filled in", as you say, Zig can always reduce an application of this function to a concrete integer type, even if it was called in a "generic" context (i.e. from within some other function where the range bounds were derived from comptime parameters).

If the range bounds are variables, then you can't fully reduce the application of this function, so you end up with I think a lot of the same problems as dependently-typed languages have with determining whether any two types are actually the same.

[distractedlambda]

That would be an example where the variables are integers, which is maybe not what you had in mind. But needing to do compile-time things with integers is relatively common, and those integers can often come from the sizes of things (that may have been type variables).

[distractedlambda]

On another note, I'm remembering that cross-compilation potentially interacts heavily with the type-system, depending on the tactic taken.

One approach for cross-compilation would be to "recompile the world" for each distinct target, which in our case would mean uniquely expanding each Pille module for each target it needs to run on. This is morally also the approach taken by Zig and Rust, but they had the luxury of designing their build and package-management systems with it in mind, so I suspect there would be some growing pains if we tried to do this in our (Racket-based) world. But it could work. And, if we say we're going this route, then we don't have to do anything otherwise special in the design of the language.

Another approach would be to make the entire (Pille) world implicitly parameterized on the ultimate target, such that essentially every Pille function would actually take "the target" as some sort of implicit compile-time/generic parameter. I think this would really only be tenable if we went the route of typechecking-before-monomorphisation (since otherwise I think we would struggle to provide tooling for much any Pille code, not just code that's explicitly-generic).

At the moment, I'm feeling okay with putting actual cross-compilation on a back-burner (I feel like there are much more fundamental issues blocking the writing of interesting programs), but I do want to have some notion in my head of how we expect we would introduce it later.

[rfindler]

Well, it certainly would be possible to design a language in the spirit of dependent types and use that as the language of type expressions. I'm not sure how much trouble that would be but a simple language to start wouldn't be hard, I don't think. It may not be expressive enough.

At the risk of repeating myself, this design discussion has no application mentioned and I don't think that's the right context to be doing designs in.

[distractedlambda]

At the risk of repeating myself, this design discussion has no application mentioned and I don't think that's the right context to be doing designs in.

Fair, I'm mostly going by attempted intuition and past experience with the languages I'm mentioning, which does not a refined design make (though I have to imagine it's still worth something in scoping out such a huge space).

I've had plenty of experiences where I'm using Zig/C++ and gone "not having much tooling for generic code sucks", and also plenty of experiences where I'm using Rust/Swift and gone "damn, I can't gener-ify this thing (that I know I could gener-ify in C++/Zig) because the type system isn't expressive enough". So I'm confident that the tradeoff manifests in production languages that have taken either general approach, but that's not very precise (or helpful for motivating a design to others).

Well, it certainly would be possible to design a language in the spirit of dependent types and use that as the language of type expressions. I'm not sure how much trouble that would be but a simple language to start wouldn't be hard, I don't think. It may not be expressive enough.

This seems worth scoping out at least a little. It may also hold some potential novelty?... I can't say I've seen a systems-programming language before that combines checking-before-monomorphisation with the sort of type-level computation that C++ and Zig support. Mojo might be trying to do something along these lines as well, but it's hard to tell (being startup-developed with a closed-source compiler).

Whether or not such a language would be expressive enough... that should definitely be assessed by trying to write some believable examples.

[distractedlambda]

To start to build a corpus of example programs, how about a contrived Point type? Imagine if you could write this in Pille (you can't right now, but I don't think there's anything crazy needed to make it work):

struct Point(x :: Float(32), y :: Float(32))

fun distance(p0 :: Point, p1 :: Point) :: Float(32):
 let dx = p0.x - p1.x
 let dy = p0.y - p1.y
 math.sqrt(dx*dx + dy*dy)

This is a good example of something that should be generic over the numeric type used to represent coordinates, and with a more Zig/C++-ish approach, we could imagine a generic version looking something like this:

struct Point[T](x :: T, y :: T) // All the cool kids put generic parameters in [...]

fun distance[T](p0 :: Point[T], p1 :: Point[T]) :: T:
 let dx = p0.x - p1.x
 let dy = p0.y - p1.y
 math.sqrt(dx*dx + dy*dy)

Nothing much changes except for putting the parameter in the signature; somehow we need +, -, *, and math.sqrt to work with T, but that's monomorphization's job to figure out (maybe there's an "overload" mechanism, maybe those are special primitives that accept a fixed set of types; it wouldn't really matter).

Also, nothing here guarantees that +, -, *, or math.sqrt on Ts actually results in more Ts; maybe it results in some other type! In C++, we could write the return type as decltype(auto) to allow it to be fully-deduced from the function body; since we're making up syntax, let's pretend Pille would allow _ as a return type to mean the same thing:

fun distance[T](p0 :: Point[T], p1 :: Point[T]) :: _ :
 // body elided

---

Now let's imagine we want to be able to type-check distance before monomorphization; the only thing I really have in my repertoire for this would be typeclasses, which I might imagine looking something like this:

fun distance[T](p0 :: Point[T], p1 :: Point[T]) :: T:
 ~where: Sub[T]; Mul[T]; Add[T]; Sqrt[T]
 let dx = p0.x - p1.x
 let dy = p0.y - p1.y
 math.sqrt(dx*dx + dy*dy)

Add, Sub, Mul, and Sqrt would be typeclasses, which for now we imagine taking only a single type parameter, and the ~where clause would add them all as constraints for the function (for which a caller would be obligated to provide evidence, in the form of typeclass instances). We also imagine that there is some "constraint environment" that +, -, *, and math.sqrt (and maybe macros in general?) can all look into to summon the evidence guaranteed by the ~where clause.

To fully generalize this--to a world where Add, Sub, and Mul can operate on different-typed values, and all those and Sqrt could have a result type different from any of their operands--I see a couple approaches. The first would be to add more parameters to those typeclasses:

fun distance[T1, T2, T3, T4, T5, T6](p0 :: Point[T1], p1 :: Point[T2]) :: T6:
 ~where:
 Sub[T1, T2, T3] // T1 & T2 are operands, T3 is output
 Mul[T3, T3, T4] // Likewise
 Add[T4, T4, T5]
 Sqrt[T5, T6] // T5 is input, T6 is output
 // body elided

I don't like how this makes us introduce new type parameters just to link input and output types between typeclasses, and it also feels like it could complicate instance synthesis (which would seem to be at least part of why Lean has an outParam "gadget"; note also its usage in the definition of the HAdd typeclass). The alternative I'm familiar with would be "associated types":

fun distance[T1, T2](p0 :: Point[T1], p1 :: Point[T2]) :: sqrt_inst.Output:
 ~where:
 sub_inst: Sub[T1, T2]
 mul_inst: Mul[sub_inst.Output, sub_inst.Output]
 add_inst: Add[mul_inst.Output, mul_inst.Output]
 sqrt_inst: Sqrt[add_inst.Output]
 // body elided

For the above, we imagine that evidence terms (typeclass instances) can be named, and that they may have type-valued fields that can be accessed by . notation. I'm handwaving the binding structure here, but I imagine there being a let*-like structure for ~where-bound evidence terms, and then having all of those be in scope for all parameter and result type positions in the function signature (mainly so that they can mention associated types).

[rfindler]

I am starting to think I was wrong with my "type checking after monomorophism = bad" assertion.

What is important is integrating macros into a systems language and going all in with that. If someone decides to use those tools to implement a type class system, great. (Maybe a simple one could be an example like minispc is an example.) But instead, for Pille to be successful, it is (hopefully) not necessary to have a carefully developed type class system as that is a huge challenge that will be a distraction from exploring the central thesis of Pille.

So I think we need to explore ways to integrate types into the macro expansion process in a way that is natural and enables someone to build and experiment with type class designs, as opposed to coming up with a good type class design ourselves. (At least at this point in the development of Pille.)

As for the example, I like that and I am glad to see example-driven thinking. But an example is not an application! So the search for an application should continue.

[distractedlambda]

What is important is integrating macros into a systems language and going all in with that. If someone decides to use those tools to implement a type class system, great. (Maybe a simple one could be an example like minispc is an example.) But instead, for Pille to be successful, it is (hopefully) not necessary to have a carefully developed type class system as that is a huge challenge that will be a distraction from exploring the central thesis of Pille.

So I think we need to explore ways to integrate types into the macro expansion process in a way that is natural and enables someone to build and experiment with type class designs, as opposed to coming up with a good type class design ourselves. (At least at this point in the development of Pille.)

I see this question over "type checking: you want it when?" as largely orthogonal to Pille's core thesis. There's definitely implications for macros, but if we were to seriously explore type-checking-before-monomorphization in our context, I feel we'd need to do so while framing it as an almost independent research question; the resulting paper would be about the design of a type system, and Pille would probably be more of an implementation detail (maybe with some argument that working atop Pille still made things easier).

I'm cool with pursuing a type-checking-after-monomorphization design in Pille for the time being; we know that it works for other languages. I think this has consequences for the way macros interact with types that probably leads us towards separate syntactic and type-checking macro layers, rather than the back-and-forth that Pille was trying to make work. Based on my current thinking, the end result would probably look a lot like Terra's approach to types, except with things happening at phase level 1 instead of 0.

I also think a type-checking-after-monomorphization design leads us towards a "we know the target at phase level 1" assumption, so that e.g. a hypothetical type-level size_of operator could reduce to an integer, rather than having to be carried around symbolically. The alternative would seem to be to delay lots of monomorphization (anything that ends up somehow target-dependent) until phase 0, which seems too large a compromise if we would also be giving up any type-checking until then.

[distractedlambda]

This is not a fully-formed line of reasoning, but I’ve been turning over various types-related ideas, and I’m feeling like (even with checking-after-monomorphization) there’s no easy way to get the combination of features I’d want Pille to support:

1. Constructs that require expected types (like literals whose interpretation is type-dependent)
2. Implicit conversions (like how non-varying values in pille/spmd can coerce to varying ones)
3. Function overloading with type-based overload selection

And we’re not just looking for a way to implement a system with these features, we’re looking for some set of mechanisms that would enable implementing any of them (and, in my mind, ideally all of them simultaneously in #lang pille). I’m feeling two general paths forwards:

1. Continue with bidirectional typing; this feels like it would require either substantially limiting the interaction of some features, or utilizing “backtracking” (potentially attempting to analyze the same sub-expression multiple times).
   For instance, what if you’re calling a function that’s overloaded for two types, and one of the argument subexpressions cannot synthesize a type? Do you simply say "too bad, give me an annotation", or do you go and try both possibilities? And if the latter, how do you tame a potential combinatorial blowup of backtracking?
   I can imagine some caching that might help tame the time-complexity of programs that cause lots of backtracking, but it seems like it'd be difficult to make that robust? Maybe it'd be good enough though?

2. Switch to a constraint-based view of things, where compile-time code generates systems of constraints (in some extensible way). Provided that the constraints are expressive enough, this seems like it ought to be a flexible approach, and perhaps we could get expressive constraints "for free" if we (at least initially) shipped constraint systems off to an external solver. I don't have a good feel for whether this would actually result in better time complexities than bidirectional-typing-with-backtracking, but I would hope that a mature solver would do a decent job?

[rfindler]

For instance, what if you’re calling a function that’s overloaded for two types, and one of the argument subexpressions cannot synthesize a type? Do you simply say "too bad, give me an annotation", or do you go and try both possibilities?

I would think that requiring an annotation would be the way to go here, but trying to put together a prototype to try stuff out would be a good way to go.