by codebje | 2025-05-27 00:57:54+00:00
On types, I think there's a philosophical argument about whether types can be values, and a related one on whether types should be values, but I think I disagree with the author about what a value is, because as far as I understand it a value is a piece of data manipulated by a program during execution.

Languages with type erasure obviously never have types as values. Languages without type erasure have _something_ as a value, but is that something a type, or a representation of a type, and is that a valid distinction? I don't feel well qualified to make a judgement call, largely because I favour type erasure. Types are specification, not implementation.

What the author calls values, I tend to call terms: bits of program that can be judged to be of a particular type or not. "1" is a term: you could judge "1" to be of type "int", or of type "unsigned". "factorial 8" is a term. A value is just a term that's represented at runtime. But is there a type of a type? Commonly, no: types are in a different universe, specified with a different syntax, and understood under a different semantics. The type of "factorial", eg, is a function from int to int. In a language with generics, you might have "List T" that takes some type T and produces the type of lists of Ts.

There's no particular reason why you can't say that the type of List is a function from Type to Type, why you can't use the same syntax to specify that function, or why the semantics of what that function means should be any different to the semantics of "factorial". Consider:

def factorial : Nat → Nat := fun n => if n = 0 then 1 else n * factorial (n - 1) def natty : Type := Nat → Nat

This doesn't imply any fancy-pants type system features. The above two terms are expressible in the simply typed lambda calculus. If you add only outer-most universal quantification, ie, parametric polymorphism, you get Hindley-Milner. If you an arbitrary quantification, you get System F; with coercions, System Fw.

Universal quantification, HM style, gives you functions from types to values (terms that can exist at runtime). If you have, say, "length : List a -> Int" you have a function that's universally quantified over "a": you tell "length" what type "a" is and you get back a function from one concrete type to another, something you can have at runtime. (All the functions producible here are identical, thanks to type erasure, so while this type-to-value thing actually happens in order to perform type checking the compiler will only ever produce one implementation.)

The last option, railed against in the article, is to have a function from a value to a type. This is, to agree with the article, generally pretty weird and hard to get a handle on. Where the article deliberately picks pointless examples, though, I'd like to point out two much more commonly encountered kinds: "Vector a n", the type of vectors of type a and length n. The type argument is a type, but the length argument is a value. The other example comes from C: tagged unions. You have a union type, that might be one of a handful of type, and you have a value that distinguishes which one it is. In C, there's no type system support and you just have to get it right every single time you use it. If you have functions from values to types, though, you can have the type checker get involved and tell you when you've made a mistake.

The whole point of static types is to specify your program's behaviour in a way that the compiler can reject more incorrect implementations. We know from way back in Gödel's day that no type system can be complete (accepting all correct programs) and consistent (rejecting any incorrect programs). Most type systems we can practically work with are inconsistent (you can get any program to be accepted by the compiler with the right type casts) because the incompleteness of the type system hinders expressivity. I believe it's possible to have a consistent type system with sufficient expressivity to allow all _useful_ programs to be written, and those type systems will roughly correspond to the Calculus of Constructions, ie, they will be dependently typed. I am not yet sure I believe that the cognitive load of working in such a language will make it worth doing - which as far as I can tell is the point the author of the article is making about type systems.