|
TypeSystem
Description of the extensions to the type system.
IntroductionValues, Types and KindsIn standard Scala, there are two levels: values and types. We say a value is classified by a type, or equivalently, that a type is inhabited by a value (or several values, more typically). In Kinded Scala, there is now a third level: the level of kinds, which classify types. To retrofit our three-level system to standard Scala, we could say there was exactly one kind. In our discussion we will call it * (as in the FP literature). The kind * classifies types that in turn classify values. E.g., Int or List[Int]. Conceptually, Kinded Scala extends the grammar of kinds to: k ::= * -- the kind of types that classify values
| k -> k -- the kind of type constructorsThis is only conceptual, in that the programmer cannot express these kinds directly. E.g., to denote that List has kind * -> * or Pair : * -> * -> *, we write class List[a] and class Pair[a, b], as we typically want to use the names of the type parameters later on. With higher-kinded types (i.e., types of kind k -> k), these names become less relevant and a concise (or at least consistent) notation becomes more relevant. This is under consideration for a future version. For now, you can already use _ as a name for type parameters that only serve to denote arity. Variance (Polarity)TODO: polarized kinds Type CheckingType AliasesWith higher-kinded types, type aliases suddenly become a very powerful feature: they correspond to type-level lambda abstraction so that we get the simply-typed lambda calculus at the type level. For example, just like we can write def fst[a, b](p: Pair[a,b]): a = p._1, we can now write type Fst[+a,+b]=a. Since Fst: *+ -> *+ -> *, it may be passed whenever a type of that kind is expected. Thus, when you have a function that takes two values and puts them in a data structure, you could abstract over the kind of structure like this: // (pasting this example as-is in the interpreter works)
type Fst[+a,+b]=a
trait DoSomethingWithTwoValues {
type Combine[+a,+b]
def combine[a, b](a: a, b: b): Combine[a, b]
}
trait OnlyCareAboutFirst extends DoSomethingWithTwoValues {
type Combine[+a,+b]=Fst[a,b]
def combine[a, b](a: a, b: b) = a
}
trait PairEm extends DoSomethingWithTwoValues {
type Combine[+a,+b]=Pair[a,b]
def combine[a, b](a: a, b: b) = (a, b)
}(If you think type Combine[+a,+b]=Pair[a,b] is unnecessarily verbose, star Issue 2.) NormalisationWe use an eta-long beta normal form. The canonical form of a type is computed by applying beta-reduction and eta-expansion as much as possible. Beta-reduction expands a fully-applied -- i.e., of kind * -- type alias. E.g., Fst[Int, String] beta-reduces to Int. Eta-expansion replaces a higher-kinded type alias by an actual type lambda: the beta-eta-normal form of Fst is "[+a, +b] a" (there is no surface syntax to express this type yet). The normal form of a type (alias) is not computed unless it is necessary; e.g., to decide subtyping. Type Equality and SubtypingKind CheckingValue must have type of kind Type application: arity, variance, bounds Ways to express application:
Type Inference |