Reified types in Hack

Hack is beginning to support reified types in their latest 4.17 release, which adds a very interesting dimension to Hack's type system. Its interactions with Hack's unique medley of type features can be quite subtle, and when any new type feature emerges, I always like to learn how and where it interacts with other features. To be more specific, I like to find this out by trying to break the new type system. So let's try together!

Hack's version of reified types enables two things:

new T: making an instance of the type variable provided that it's:
1. a class type, and it's
2. "<<__ConsistentConstruct>>"
These constraints are collectively represented by the <<__Newable>> annotation.
is T: typechecks of any values against a type variable, provided that it's not a function type.

This constraint is represented by the <<__Enforceable>> annotation. This tends to shine for refinement, especially of container types like vec<mixed> → vec<int>.

It's noteworthy that the second feature doesn't allow you to branch based on the type T itself, which would be akin to switch-case over types. This is the final distinct feature I've seen from runtime processing of types, implemented in Haskell as "type families". This feature completes a relatively powerful set of functionality would be complete in Hack, allowing you to create, cast and coerce the class type variable. In types, for the class type a it looks like this:

forall a. Base a => (b, c, ...) -> a b c...: all constructors
forall b. Base a => b -> m a: typesafe casts
forall a. Base a => a -> b: typesafe coercions

In terms of interacting with other types, the first feature is very intruiging. The second feature not so much, since if the runtime typecheck is sound, the types you're getting out are truly those types exactly.

In particular, the first feature introduces a new way for the calling scope to supply values of a given type into the object without going through an argument. This is interesting because sometimes, the type system prohibits some types in argument positions. This restriction arises from subtyping rules collectively known as "variance". The aside below is a very brief explanation of everything relating to variance for the unfamiliar.

High-speed variance primer

We start with the subtyping relation A <: B which means that when A is cast to B, it:

swaps its method signatures with the signatures of all B's methods (this is the definition of casting), and
the new signatures are compatible with the implementations in A because all B method signatures are subtypes of the A counterparts (this is the correctness check).

"Variance" just describes the last piece: what a subtype of a function means. A function signature gives the function assumptions it can make about its arguments, and a contract it must fulfill about its return type. The bolded words are bolded because they entirely explain the subtyping rule.

A function can be cast, and is therefore a subtype, to a signature with arguments that are subtypes of the original function's arguments. This new signature gives the function richer types that it can expect, which is less restrictive than the original definition.
A function can be cast to a signature with a return type that is a supertype of the original function's return type. This new signature expects a less rich type that the function must fulfill, also less restrictive than the original definition.

The argument types are called "contravariant" because a subtype function has supertype arguments. The return type is called "covariant" because a subtype function has subtype returns. If a type appears in both the argument and return and the two types are constrained to be equal (e.g. through a generic), no subtypes of the function may change that type, a rule known as "invariance".

Variance and reified generics have a very interesting intersection in a quirk of the Hack type system: in that it allows invariant state so long as it's obscured enough with its access modifier. To be specific, it needs to be at least object-protected, meaning it's protected to the methods on the object that the state is resident to. This is distinct from plain vanilla "protected" where objects of the same class can access each other's properties. The reason is detailed through Scala's type system here.

In fact, I lied a bit. Hack doesn't actually have object-protected, and variance violations are actually possible right now! It aspires to have it, and so if we dream a bit, would it be typesafe even then, when mixed with reified types?

It turns out it depends. As it stands, the reified types can't be co/contravariant. This is by design, complemented by another constraint: that the reified generic needs to be parameterized by a concrete type. We can't be sneaky and use a wrapper like :

class Inv<reify T> { public T $state; }
class A<+T> { private Inv<T> $inv; }

either, because reified types need to be parameterized with concrete types, presumably because the <<__Newable>> and <<__Enforceable>> constraints are checked at the parameterization site. We have to dream a bit bigger and suppose reified types can be variant.

It turns out this can be typesafe for contravariant types, but not for covariant ones! Ah, another instance of the spiciest of asymmetries. Reified variant types are just inherently contravariant — it's an example of the canonical violation for covariant types:

<?hh // strict
<<__ConsistentConstruct>>
class Base {}
class Derived extends Base { public function foo(): void {} }

class A<<<__Newable>>reify +T> {
	object protected ?T $state = null;
	public function set(): void {
		$this->state = new T();
	}
	public function get(): ?T {
		return $this->state;
	}
}
function violate(): void {
	$a = new A();
	violate_cast($a);
	$a->get()?->foo(); // *explosion noises*
}
function violate_cast(A<Base> $a): void {
	$a->set(new Base());
}

Contravariant types can receive type T through arguments, so it's already safe by the arguments that make those... well, arguments, safe. But what about the types coming from the state?

Consider the Inv<T> state from before, as well as a naive implementation of the reified types, where casting A<Derived> — A<Base> doesn't cast the Inv<Derived> state. This is where the breadth of the featureset is important. For Hack, if there were branching on types, contravariant types would no longer be sound. This is because the state could pass the original type back up to the reference that had been cast, which could then expect it to be more derived than it is (indicated by the red arrow). The converse is true in the covariant case, although that is already unsafe when reified variant parameters are allowed.

Above being a very interesting puzzle to think about, reified types bring profound and powerful changes to a type system. For example, generic programming à la Scrap your Boilerplate. And this is just the first release! Who knows, maybe it won't be long before we're doing arithmetic with types. It could just come to Hack. And that's why I love this sinking ship: its transformation into an elegant submarine.