# How do Hack's reified generics play with its variance system?

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:

1. 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.

2. 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:

1. forall a. Base a => (b, c, ...) -> a b c...: all constructors
2. forall b. Base a => b -> m a: typesafe casts
3. 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.

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.