My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
Syntax  
Description of the current syntax and proposals for future enhancements.
Phase-Requirements, Phase-Design
Updated Feb 5, 2010 by adria...@gmail.com

This page describes how Kinded Scala's syntax deviates from the plain vanilla Scala syntax. The differences have been kept as small as possible.

Current Syntax

Essentially, the only thing that's changed from standard Scala is that any type may be parametrised and be applied to type arguments. Abstract types -- type parameters and abstract type members -- and type aliases -- i.e., concrete type members -- may now take type parameters.

Examples:

trait Iterable[+a] {
  type MyType[+a] <: Iterable[a] // a type member may now take type parameters, including variance annotation
  
  def map[b](f: a=>b): MyType[b]
}

trait Seq[+a] extends Iterable[a] {
  type MyType[+a] <: Seq[a]
}

trait List[+a] extends Seq[a] {
  type MyType[+a] = List[a]
}

Type parameters may also take type parameters, which, besides allowing variance annotations, may also be bounded:

trait Monad[T <: Bound[T], MyType[x <: Bound[x]], Bound[_]] {
  def map[S <: Bound[S]](f: T => S): MyType[S] 
// ...
}

class Set[T <: Ordered[T]] extends Monad[T, Set, Ordered] {
  def map[S <: Ordered[S]](f: T => S): Set[S] = error("not implemented") 
// ...
}

Note that type parameters of type parameters (such as x in MyType[x <: Bound[x]]) are only in scope directly in the type parameter list in which they are defined (i.e., in [x <: Bound[x]]). If a higher-order type parameter is not bounded, the wildcard symbol (_) may be used as its name (e.g., Bound[_] is a type parameter that takes one type parameter).

Issues with the current syntax

Lauri pointed out some inconsistencies in this syntax (more on this in his proposal). The main problems are:

  • type parameters that take type parameters may be passed conveniently, e.g. Monad[T, Set, Ordered] (where Ordered takes one type parameter), whereas type member definitions have to be "eta-expanded":
  • type MyType[+a] = List[a] 

instead of just

type MyType = List
  • specifying the type parameters of a type parameter is akin to specifying the type of a value. In functional programming languages values are classified by types and types are classified by kinds, with similar syntax for expressing both. The former is made explicit in Scala with type annotations such as val fun: Int => String whereas the latter is not supported. We can't write Bound: * => * for a type that takes a type to a type. We must write Bound[x] or Bound[_] where the x or the _ is just some dummy placeholder.

Proposals

Lauri Alanko's proposal

Now let's see, we have f-omega-sub with bounded type operators, and mutually recursive type parameters. Result kinds of type operators depend on their arguments, so the kind language is presumably something like

k ::= *
   |  Pi (? X1 >: T1 <: U1 :: k1), (? X2 >: T2 <: U2 :: k2), ... . k'

with ? standing for a variance annotation, and all Xn bound in all Tn and Un, and of course in k' too. We can define

? k => k'

as shorthand for

Pi (? X >: All[k] <: Any[k]). k'

with X fresh, and Allk and Anyk standing for the bottom and top types of kind k.

Then the kind of your Monad trait would be

Monad :: Pi (T <: Bound[T] :: *),
            (MyType :: Pi (x <: Bound[x] :: *). *,
            (Bound :: 0 * => *).
            *

which, granted, doesn't look too clear, even though vacuous bounds are omitted. Let's try a more palatable syntax and let kinds default to "type" (i.e. *), and variances to 0, when not explicitly specified:

Monad ::
[T <: Bound[T], MyType :: [x <: Bound[x]] type, Bound :: type => type] type

I think this is somewhat reasonable.

However, now that we have explicit Pi-kinds, we might as well have explicit type functions, too. So

type foo[x] :: k = bar

would be shorthand for

type foo :: [x] k = [x] bar

(I'm not sure if using the same bracketed type syntax for both kind-level Pi binders and type-level Lambda binders is a good idea or not.)

This is all pretty straightforward (to specify, probably not to implement). But why would this be a good idea?

The most obvious argument is syntactic consistency. Already, since we can say MonadOption, a higher-kinded type can appear by itself without immediate type arguments. However, it is a good idea for a language's syntax to be such that application can be expressed by substituting arguments for parameters in the body. (Let's forget generativity here...)

And this currently fails: if we have

trait Monad[m[x]] { ... }

then when we apply MonadOption, we replace m with Option, not mx. Clearly the actual parameter is m, but this isn't very obvious from the current syntax.

Moreover, it is rather inconsistent that currently we can use a lone higher-kinded type as a type argument, but not as the RHS of a type definition. Currently one must do:

trait Monad {
  type m[x]
  ...
}

class OptionMonad extends Monad {
  type m[x] = Option[x]
  ...
}

instead of simply

class OptionMonad extends Monad {
  type m = Option
  ...
}

This kind of forced eta-expansion means that type definitions become more and more verbose as we proceed to higher kinds.

And once we allow "type m = Option", syntactic consistency dictates that we have a way of specifying an abstract type member of this kind without fake applications, and that leads to kind annotations: "type m :: type => type".

Incidentally, type m[x] reminds me of C's declaration syntax `int (*f)(int)`. Both work by giving a "fake use case": "type mx" states: "if m were applied to some type x, the result would be a type", and `int (*f)(int)` states "if f were dereferenced, and then applied to some int, the result would be an int". I think C's declarations have been universally loathed throughout the ages, so the similarity is worrisome...

Powered by Google Project Hosting