Reified Generics: The Search for the Cure
gbracha.blogspot.com
gbracha.blogspot.com
Type systems are essentially an attempt to embed a logic that can prove various invariants about the code. What varies across type system to type system is A. what you can express and B. how much you can check. The issue is, most programming language designers decide these two things for you. That's why stuff like reification vs type erasure bites designers; the decision is irreversible.
But what if it wasn't? And this seems to be what this article is proposing. That if you can write compile time functions that deal with types as a construct, you can leave decisions like type erasure and reification to the programmer. Granted, that essentially forces programmers to act as language designers. And I doubt most programmers want to learn stuff like type rules or how to prove soundness.
However it does have some really cool implications. Like right now, Ruby has this whole debate over adding types. And sure, Ruby could just add normal static typing with some annotations and it'd work. But it kind of doesn't make sense for such a dynamic language to use such a static construct. What'd make more sense (to me) is some sort of metaprogramming on code that allows for checking invariants. Like being able to load a class, then run it through a checker at runtime. I've been reading a book on dependent types (The Little Typer) and the whole idea of types having types with a meta-type of sorts (universes in dependent types, meta classes in Ruby) seems very applicable to Ruby.
I've imported many a library which deadlocked, crashed, or infinite looped. In reality it's not that big a deal; it happens and you figure out the bug.
The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff.
Being able to specify your own type language is like having an untyped language governing your term language.
There are promising directions though. In 20 years they might even have matured.
That's the fundamental tradeoff.
And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
what terms have this type?
I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156
And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361
The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.
int n = 2 + 3;
cut elimination / normalization,
https://arxiv.org/abs/1607.04156
Oh please share some references :) I think in that context what matters is the progress and preservation parts of cut elimination.
> Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open?
I haven't either, but I think that's the case.
share some references
Since most interesting examples of PBE / IPS use recursion, [1] goes through a hierarchy of recursion principles, e.g. map, filter, fold, full recursion. The order of choosing recursion principles matters a great deal for controlling overfitting, the bête noire of machine learning.
The basic problem is this: the answer to the question "What terms have this type?" is almost always an infinite set with a great deal of redundancy. E.g. 2+3 and 3+2 are both an answer to "What terms have type Int?". But both answers are contextually indistinguishable, so in practise we only one to see one of them. Since contexual equivalence is typically undecidable there are limits to how clever you can be in a computer program to avoid redundancies. Moreover, in PBE / IPS you typically don't want to have just values, you are interested essentially in short programs inhabiting a type. So cut-eliminiation, at least as conventionally understood, doesn't quite do the job.
[1] J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure Transformations from Input-Output Examples.
Damas-Hindley-Milner inference is also hyper-optimised to a specific point on the design space, and does an excellent job there, but (to echo Conor McBride) I would love to see less conflation of the ideas of execution phase, parametericity, and implicitness going forward.
less conflation of
Type checking is a stage: http://lambda-the-ultimate.org/node/2575
Type systems as macros: http://lambda-the-ultimate.org/node/5426
For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.
And the vast majority of generic Haskell code does not have either of those constraints, which makes you think how important reified generics as-default really is.
Haskell has little to no RTTI, which makes erased generic a non-issue. Java/C#/Dart have a lot of RTTI, which makes erased generics problematic.
Without RTTI/reflection capabilities, generics reification become a performance tradeoff, with it they become a logic/correctness issue.
For a fairly common example, a class implementing several specializations of the same generic interface. Suppose we have Convertible<T> for something that can make a T out of itself - it would be perfectly reasonable for an object to be both Convertible<int> and Convertible<string>, but you can't do that in Java. And this doesn't require RTTI checks at call site at all - it might be that the caller is itself generic, and is just trying to accept something that's Convertible<U> for its own U.
Integer sum(List<Integer> values) { ... }
float sum(List<Float> values) { ... }
You also have no way in the language to express things like "Map<String, Option<Integer>>.class", which has some ergonomic implementations. (e.g., see: http://gafter.blogspot.com/2006/12/super-type-tokens.html)
The gotcha here, though, is that Haskell doesn't have these problems, or the one with implementing multiple specializations of the same generic type, even though it erases types much more completely than Java does.
I'm not much of an expert on language design, but that leaves me thinking that there's probably a lot of stuff we lay at the feet of Java's type erasure that is actually more properly attributable to having a type system that is broken in some fundamental way.
Or maybe it's the way that type erasure interacts with dynamic dispatch in an object-oriented language? Since the dynamic dispatch means that there are decisions about datatypes that a language like Haskell or ML can sort out at compile time, but that an OO language like Java must delay until run-time?
But I'm not sure that truly counts as type erasure. If that's how things are done, then the type class of every such value is effectively encoded by the set of function values that are passed around, and could be queried at runtime - the Java equivalent would be to tag every reference with its class, including all generic parameters used to instantiate it.
class List[T](implicit tag: ClassTag[T]) {
def elementType: Class[_] = tag.runtimeClass
}
public class List<T> {
private final Class<T> t;
public List(final Class<T> t) {
this.t = t;
}
public Class<T> elementType() {
return this.t;
}
}
Zig doesn't go all the way, though. Instead, a type parameter could be any combination of a compile-time and runtime parameter, depending how it's used.
I do wonder how that affects calling conventions, though? If have separate linking then we probably need to avoid changing the calling convention if a function is modified so that a parameter is used in a different way.
[1] https://andrewkelley.me/post/zig-programming-language-blurs-...
...but I don't see how this feeds into the compiler without a "shadow type system"[1]. If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. It's just an Object-container that has validation funcs executed at runtime, which can already be done relatively easily in basically every language. Did I miss something?
[1]: or compile-time code generation, but that isn't mentioned. and that strikes me more as a macro system than a type system (though I don't know if that's a real distinction, if your macros are sufficiently powerful™)
Specify which types everywhere? If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. If you mean type variables (e.g. `T` and `List[T]`) then I disagree: that's a perfectly valid way to do generics, and having to annotate stuff is just a deficiency of inference (no worse than, say, Java).
The key is that we're allowed to use the argument names and function/method names in our types, thanks to the 2 given rules. We don't need to lift those functions up to the type level, since we're only checking that the inputs and outputs line up.
To me, this seems to be a form of dependent types. Note that "dependent types" only refers to the ability of having types refer to values, e.g. dependent function types like `(n : Int) -> Foo n` or dependent pairs like `(n : Int, Bar n)`. Most dependently typed languages also treat types as first-class language constructs, allow the type-checker to run arbitrary code (which usually implies that computations are pure and everything terminates/coterminates). Those latter aspects don't seem to apply here: it's just about using value-level names in our types.
I think this works quite nicely, from a theoretical point of view; but I wonder what would happen in more complicated situations. When type checking is purely syntactic, we can easily get stuck with mismatched things like "should have type 'T', got type 'Pair[T, U].first()'". That's where we need type-level computation, to reduce things down to normal forms so that the syntactic checks (are more likely to) work.
Yep, that's exactly what I mean (since that's the only example in the article that seems to imply any kind of compile-time safety).
re dependent types: interesting! yeah, it does seem like normal generics could be a type-dependent type in a case like this - I hadn't really thought about that before. though that also seems like a "shadow type" tho, which the article is trying to eliminate... so we're back at the starting point :|
The type-checked example is this:
var lst : List[Integer] := List(Integer).new();
var i : Integer := lst.add(3) + 4;
List<Integer> lst = new List();
Integer i = lst.add(3) + 4;
This extra argument (a run-time representation of the type) is actually to be expected. Values (including functions) which are generic (in the Java sense), also called "parametrically polymorphic", or as you say "type-dependent types", can be understood as taking those parameters as extra arguments (which is precisely what this article is talking about); although the value itself cannot change its behaviour depending on that argument. For example, `List<T> reverse(List<T> input)` cannot work different for, say, `List<Boolean>` compared to `List<Integer>`.
This is really clear in Haskell. The Glasgow Haskell Compiler uses an intermediate language called "GHC Core", where generic values are literally represented in the same way as functions. There's a nice overview at https://alpmestan.com/posts/2013-06-27-ghc-core-by-example-e... (the "id'" example is the first generic one).
> it does seem like normal generics could be a type-dependent type in a case like this
Generics are definitely type-dependent types. However, when I said "dependent types" I was referring specifically to value-dependent types, e.g. https://en.wikipedia.org/wiki/Dependent_type
Note in that Wikipedia article's introduction "dependent types are used to encode logic's quantifiers like 'for all'". Compare that to the generic example in that GHC Core link above, where the keyword "forall" gets inserted by the compiler ;)
The Wikipedia article also states "Deciding the equality of dependent types in a program may require computations". That's what I was getting at with the system described in this article: it doesn't seem to allow for type-level computations, without which we may end up getting errors that "expected type X, given type Y" when those types are 'obviously' the same (to us, but not the the checker, since it's not able to compute).
I know Bracha is a fan of 'pluggable type systems', where we can use a variety of type systems to check things about the same program (perhaps requiring different annotations). However, I'm not sure if these 2 rules are enough to perform meaningful reductions on types (e.g. to spot that `Pair(T1, T2).secondType()` is equal to `T2`). I'd imagine we'd have to "lift" more and more expressions into the type level (e.g. `return`, then `if/then/else`, and so on) until we have a full-blown theorem prover like Agda!
These type systems are used by ML and its descendents (OCaml, Haskell, Rust, Reason, etc.) and are generally seen as a "sweet spot". They feature:
- Types depending on types (AKA type constructors)
- Values depending on types (e.g. type classes)
- Type-generic values (AKA parametric polymorphism)
- Higher-kinded types (AKA higher-order types, or generics at the type-level)
- Inference of all types
- Erasure of all types
Things which Hindley-Milner can't do include:
- Inference of values (AKA implicit arguments, as found in Scala and Idris)
- Erasure of values
- Types which depend on values (AKA dependent types)
These things are important for this article, since it represents types as values (which the two given rules let us access from our type annotations). In particular, if we could infer (some) values, we could avoid having to specify arguments like in `List(Integer)`.
Going "beyond" Hindley-Milner is a very active area of research. There's a nice talk about this at https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbri... (which i admit is a bit symbol-heavy); full disclosure, I was in the audience for that talk ;)
To circle all the way back around tho, from the intro to the article:
>A while back, I discussed the problem of shadow language constructs. I gave examples of shadow constructs such as Standard ML modules, traditional imports etc. Here is another: reified generics.
The article seems to be about trying to eliminate shadow types, e.g. meta-type info carried by the compiler but not otherwise visible. By turning generics into type-generator funcs. My question / confusion is around "it seems like you can't type-check that at compile-time without being either so explicit it's no longer generic, or with shadow types, so I don't see how this helps". Or indeed changes anything.
Generics as type-generating funcs makes sense, it lets you choose erasure-or-not however you like. Perfectly on board[1]. But how do you type-check it at compile-time without "shadow types"? (if the answer is "read my comments", I'm happy to! I haven't gone through them super carefully yet.)
[1]: well... in concept. I'm not sure how libraries would be able to use this in a standard way, seems like it'd lead to multiple competing "generics systems". But that's also useful sometimes. I like languages that let you do that kind of thing, though the ecosystem does not always benefit from it.
No problem. Most of my blog posts start out as rambling HN comments ;)
> how do you type-check it at compile-time without "shadow types"?
From my understanding of the article, the 2 rules allow type checkers to refer to the value names. To me, the key parts of the (typed) example are these lines:
public var List = (function(T : Class) {
...
public datum : T;
...
public add:(e : T) : T {
...
In the other two lines, `T` is being used as a type (again, since it's on the right-hand-side of a type annotation). This is what the first "rule" lets us do.
As far as I can tell, this (along with the second "rule", which lets us refer to method names in our types) avoids the need for "shadow types" (or a "shadow language" for types), since we only introduce/define/pass-around things using the normal value-level machinery (functions, methods, classes, etc.), and our type annotations simply refer to those value-level names (we don't re-implement functions, methods, classes, etc. for types).
My concern is that "rule 2" lets us write things like:
function pickAType(T1 : Class, T2 : Class) : Class {
if (canProve(collatzConjecture)) {
return T1;
else {
return T2;
}
}
var x : pickAType(Int, String) = 42;
This is just an example: we can replace "prove Collatz conjecture" with any arbitrarily-difficult calculation. The point is that checking these types requires running the function which, in this case, requires the type checker to understand `if/then/else`, functions like `canProve` which don't fit the constraints of "rule 2" (that inputs and output should be `Class`); presumably `canProve` will use things like recursion, and `collatzConjecture` will be some sort of datastructure, which a type checker would also need to understand. In short, we'd need an awful lot more rules than just the 2 in the article. The straightforward way to do this is to just have our type checker just invoke the normal language interpreter, but that raises more issues.
For example, side-effects: what if `pickAType` chooses its output based on, say, reading a random number from the OS kernel? It seems unwise to allow side-effects when type-checking (except maybe for "type providers" https://docs.microsoft.com/en-us/dotnet/fsharp/tutorials/typ... ). However, if we're running arbitrary value-level code as part of the type-checking process (e.g. by invoking the normal interpreter), that would require the value-level language to also be free of side-effects (or else we would need an alternative interpreter, which raises the "shadow language" problem again).
In particular, object oriented systems, especially those like Smalltalk, Self and the author's Newspeak, model function calls, property lookup, value construction, method calls, etc. as 'sending messages between objects', which is an I/O effect that can have all sorts of repercussions for the meaning of other code. For example, imagine the method call `True become: False` ( https://gbracha.blogspot.com/2009/07/miracle-of-become.html ; or in Newspeak, where booleans are immutable "value objects", some equivalent behaviour-changing call). Even in a system with no I/O, I think this would make types non-compositional, i.e. if the expression `f` type-checks to type `A -> B` and `x` type-checks to type `A`, the expression `f(x)` might not type-check, and even if it does it might not have type `B`, since the code run while type-checking one sub-expression may alter the behaviour of code run while type-checking the other.
Note that these aren't insurmountable problems: we could approach it like most other things in dynamic languages and say "yes it can be broken by doing that; so don't do that".
Alternatively, perhaps more in keeping with Bracha's ideas of pluggable type systems, we might be OK with type systems that are limited (e.g. unable to reduce `pickAType(Int, String)` to either `Int` or `String`), or uncomputable (if we do run `pickAType`), or even containing "shadow" interpreters which may, for example, over- or under-approximate types (e.g. allowing `42` since it might have type `pickAType(Int, String)`, or disallowing it because it might not), or which implement some alternative evaluation method or effect system (e.g. calling out to SMT solvers or proof assistants, mocking I/O calls, etc.). If they're pluggable, then we're free to ignore those which aren't appropriate for our project (based on how much confidence we want in the result, whether we'll be doing shenanigans like `pickAType`, etc.)
[1] https://objectcomputing.com/news/2018/10/08/micronaut-10-rc2
You inject weak typing (unexpected conversations) into a strong type system by doing that.
Are you a manager at Sun by any chance? ;) See the "tangent; tl;dr" section in the article:
"Sun management deluded themselves that Java was the ultimate programming language (though yours truly did try to hint, ever so gently, that further progress in PL was at least conceivable)."
The author has spent a lot of effort trying to improve Java specifically, via language design committees, etc. AFAIK he was one of the lead designers of Java's reflection system.
Looking through his past posts it's clear that Java was getting increasingly hampered by the consequences of past decisions, and the committees weren't aiming for the same direction Bracha would like to see, so he gave up that uphill battle in favour of working with newer languages which are either free from legacy baggage (e.g. Dart) or can serve as a demonstration that these ideas can actually be implemented and work (e.g. Newspeak). Whilst the latter is largely academic, it's basically a proof-of-principle for the former.
For example, from https://gbracha.blogspot.com/2009/05/original-sin.html (linked in the article as "There is no justification for primitive types in an object oriented language"):
"I do not favor any of these features, but we will take them as a given."
"I am not suggesting that this discussion should be reopened. This is just a mental exercise."
"One of the many reasons I left Sun was because it was increasingly impossible to make meaningful progress on the language, or anything else for that matter."