scalahigher-kinded-typestype-constructor

What is a unary type?


I am going through Higher-kinded types & ad-hoc polymorphism section of twitter's Scala School and I don't understand and can't find reference anywhere to a unary type. Here is the context of the usage:

For example, whereas “unary types” have constructors like List[A], meaning we have to satisfy one “level” of type variables in order to produce a concrete types (just like an uncurried function needs to be supplied by only one argument list to be invoked), a higher-kinded type


Solution

  • That statement doesn't really make sense.

    First off, there is no such thing as a "unary type". Types don't have parameters, so that just doesn't make sense.

    There are "unary type constructors", i.e. type constructors which have one parameter, such as List[A]. But the statement implies that all type constructors which aren't unary are higher-kinded, and that is simply not true. For example, Either[A, B] is binary (it has two parameters), but it is not higher-kinded.

    A type constructor which has a type constructor as its parameter or a type constructor which returns a type constructor as its result, that is a higher-kinded type constructor. Just like a function with two arguments is not automatically higher-order, only a function which has a function parameter or returns a function is. (Note: in some branches of mathematics, functions are called "value constructors", which is actually where the name "type constructor" comes from, because just like a function takes values and produces values, a type constructor takes types and produces types; a type constructor is kind-of like a function on the type level.)

    There is one wrinkle here, and it is the same as with functions: when we assume that all type constructors are unary, then we need to use currying to represent type constructors with more than one parameter, and in that sense (and only in that sense!) all non-unary type constructors are automatically also higher-kinded type constructors. Again, this is just like functions: add is by no means a higher-order function, but if we use currying, then we represent it as a function which takes one integer and returns a function that takes a second integer and returns an integer, which technically makes it a higher-order function.

    But that is not the case in Scala: Scala can represent type constructors with multiple parameters without the use of currying, so non-unary type constructors are not automatically higher-kinded.

    Kinds are notated similar to types, except we simple write * instead of Type, because it conveys no information: type constructors always operate on types, there is no need to type Type everywhere. So, a unary type constructor like List has kind:

    * → *
    

    A binary type constructor like Either has kind:

    (*, *) → *
    

    When you are forced to represent it using currying because your language only allows a single type parameter, then the kind of Either becomes:

    * →  * → *  // `→` is right-associative just as with function types, so this is 
    * → (* → *) // which is higher-kinded
    

    The Container type constructor from the page you linked has kind:

    Container :: (* → *) → *
    

    So, it takes a type constructor as an argument and returns a type. And that is what makes it higher-kinded. In fact, you will note that Container actually is unary! It only takes a single argument. So, the statement actually contains a counter example to its own claim. (And again, this is similar to functions. E.g. the fix function in the Haskell prelude is higher-order, but unary: it takes only one argument, but that argument is a function.)

    The reason why this is pointed out specifically in that description is that this is not true of some other mainstream languages in the field of typed OO languages like Java or C♯. Both Java and C♯ do not allow type constructors as parameters or results of type constructors. You can only pass a type to a type constructor, and the result of a type constructor is always a type. Both Java and C♯ do not support higher-kinded types. This makes Scala somewhat special in that regard, and that is why it is pointed out specifically on that page. (Of course, in the field of typed functional languages, higher-kindedness is nothing special.)

    tl;dr summary:


    There is some more information in this older answer of mine: What is a “kind” in the context of Type Systems?.