My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
TypeSystem  
Description of the extensions to the type system.
Updated Feb 5, 2010 by adria...@gmail.com

Introduction

Values, Types and Kinds

In 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 constructors

This 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 Checking

Type Aliases

With 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.)

Normalisation

We 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 Subtyping

Kind Checking

Value must have type of kind

Type application: arity, variance, bounds

Ways to express application:

  • by passing type parameters
  • overriding type members

Type Inference

Powered by Google Project Hosting