|
Syntax
Description of the current syntax and proposals for future enhancements.
Phase-Requirements, Phase-Design 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 SyntaxEssentially, 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 syntaxLauri pointed out some inconsistencies in this syntax (more on this in his proposal). The main problems are:
type MyType[+a] = List[a] instead of just type MyType = List
ProposalsLauri Alanko's proposalNow 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... |