-
Notifications
You must be signed in to change notification settings - Fork 2
design guidelines
Description of sing design guidelines
-
MetaScala
-
Yrecursionoption proposal
-
- Michid's Weblog
- Scala Type Level Programming @kmizu (in Japanese)
-
Apocalisp
- incidentally suggests singmethod
Caution: These terms are, for now, private at all.
Roughly speaking, a type of types is called a kind.
In sing, a kind is a subtype of sing.Any:
package sing
trait Boolean extends sing.Any { ...
It represents a type in the type-level world.
The reason why sing.Any is needed will be described later.
A typemethod is a type or a type-constructor which takes kinds. A form of abstract typemethod is something like:
type not <: sing.Boolean // no parameters
type equal[that <: sing.Boolean] <: sing.Boolean // one parameter
You can override a typemethod:
override type not = ...
override type equal[that <: sing.Boolean] = ...
override modifier is optional. Note that you cannot re-override a typemethod.
You can invoke typemethod by #:
type foo[b <: sing.Boolean, c <: sing.Boolean] = b#equal[c]
A typemethod invocation is memoized.
When a typemethod invocation doesn't depend on enclosing type parameters(or abstract types in official), we call it concrete.
class X[b <: sing.Boolean] {
type bar = `true`#not
}
`true`#not is a concrete invocation, for it doesn't use enclosing type parameters.
A concrete invocation is evaluated as soon as the Scalac reads; even if you don't invoke bar.
A termmethod is a polymorphic method whose type parameters are upper-bounded by kinds.
def foo[x <: sing.Boolean](x: x) = ...
Notice the type and term have the same name x.
In sing, types and terms are intended to be isomorphic.
A singmethod is an identifier which can be used as both typemethod and termmethod. The termmethod shall return a type which is the same as typemethod invocation:
def foo[b <: sing.Boolean, c <: sing.Boolean](b: b, c: c): foo[b, c] = ...
type foo[b <: sing.Boolean, c <: sing.Boolean] = ...
Assume you are making if statement in the type-level world.
First, you might describe it for the runtime world:
def myIf[T](b: scala.Boolean, _then: => T, _else: => T): T
This is a polymorphic method(aka generics). Second, you might port it into the type-level world. (Ignore by-name parameters for now.):
type typeIf[T, b <: sing.Boolean, _then <: T, _else <: T] <: T // ???
This is considered as generics in the type-level world.
Unfortunately, trivial unit-tests reveal this doesn't work at all. Any form of type-level generics seems not to work for now. See:
Now we have to go back to the start. Imagine you live in a world which has neither generics nor by-name parameters. That's good old Java:
trait MyFunction0 {
def apply: scala.Any
}
def myIf(b: scala.Boolean, _then: MyFunction0, _else: MyFunction0): MyFunction0
We replace by-name parameters with MyFunction0.
It is useful in nested if statements to return MyFunction0.
Let's port it into the type-level world:
package sing
trait Function0 extends sing.Any {
type apply <: sing.Any
}
type `if`[b <: sing.Boolean, _then: sing.Function0, _else: sing.Function0] <: sing.Function0
Well done.
Without type-level generics, we need a way to downcast, that is,
asInstanceOf for the type-level world.
But asInstanceOf is inherently generic! What can we do?
sing.Any offers a painful way:
package sing
trait Any {
type asBoolean <: sing.Boolean
type asFunction0 <: sing.Function0
// ...
}
sealed abstract class `true` extends sing.Boolean {
type asBoolean = `true`
// ...
}
Though type-level isInstanceOf is feasible,
it has not been implemented yet.
The this.type is. But it is not well synchronized with the type-inference rule.
So you have to make it by yourself. It is called self in sing.
package sing
trait Any {
type self <: Any
// ...
}
sealed abstract class `true` extends sing.Boolean {
type self = `true`
// ...
}
As Scala doesn't contain any type-level primitives, we must implement them from scratch.
sing offers the following:
Boolean-
Nat(Natural numbers) UnitFunctionNTupleN- etc...
sing.nat.peano and sing.nat.dense implements Nat.
The former is good at small numbers, the latter at large numbers.
sing is built upon singmethods, which emulate singleton-type system;
Return types of methods vary depending on the expression.
def myAssert(a: sing.`true`) = ()
def testsingity {
import sing.nat.peano.Literal._
val i: _3 = _3
val j: _5#minus[_2] = _5.minus(_2)
myAssert(i.equal(j)) // type-level check
}
The object _3 has its own type _3(the same name).
i.equal(j) too has its own type(unspecified).
Scalac reveals the concrete invocation _5#minus[_2] to the type true.
Singleton-type system guarantees only one object has true type.
That's why a runtime check is unneeded.
Singleton-type system provides a good subset of dependent-type system,
which is not fully supported by the Scalac yet.
Though the Scalac provides the built-in way: x.type, its usage is very restricted.
For further reading, see HList in Haskell or Lightweight Dependent-type Programming.
Any sing thing can escape from the sing world by using sing.Any.unsing:
import sing.nat.peano.Literal._
def testUnsing {
val i: scala.Int = _3.times(_2).unsing
assertEquals(6, i)
}
A normal type requires a conversion into sing world by using sing.Box:
def testBox {
val j = sing.Tuple2(sing.Box(2), sing.Box(3))
assertEquals(3, j._2.unsing)
}
Unfortunately no auto-boxing is provided.
As boxing is cumbersome, several short-cuts are offered:
def testLift {
val j = sing.Tuple(2, 3) // == Tuple2(Box(2), Box(3))
val xs = 3 #:: 4 #:: 5 #:: sing.Nil // == Box(3) :: Box(4) :: Box(5) :: Nil
val y = xs.foldLeft(j._1, sing.Function.lift2((y: Int, x: Int) => y + x))
assertEquals(2+3+4+5, y.unsing)
}
Any sing data structure is heterogeneous; concrete types are preserved.
For an example, look into sing.List:
import sing.nat.peano.Literal._
object add2 extends sing.Function1 {
override type self = add2.type
override def apply[x <: sing.Any](x: x): apply[x] = x.asNat plus _2
override type apply[x <: sing.Any] = x#asNat#plus[_2]
}
def testTrivial {
val xs = _3 :: _4 :: _5 :: _6 :: sing.Nil
val u = xs.map(add2) // returns a view
assertEquals(5 :: 6 :: 7 :: 8 :: Nil, u.unsing)
locally {
import sing.::
val v: _5 :: _6 :: _7 :: _8 :: sing.Nil = u.force
}
}
Because it is unknown how to implement the sing lambda,
you have to write down sing.FunctionN implementation one by one.
Notice sing.List methods return views.
force turns a view into a concrete form.
Unlike MetaScala, sing doesn't make use of implicit.
In general, implicit is not modular. You can't build a large method from small methods.
The type-level programming in Scala is (as far as I know):
- Pure(no-side effects) object-oriented. (Have you ever seen such a language?)
- Actual parameters are fully evaluated before passed to a typemethod.
- Type equality, that is, type-level
eqis infeasible in practical performance. - A typemethod invocation is memoized.
- Greedy; a concrete type is computed in advance.
Fibonacci numbers:
type fibonacci[n <: sing.Nat] = sing.`if`[n#lt[_2], sing.const0[n], FibElse[n]]#apply#asNat
trait FibElse[n <: sing.Nat] extends sing.Function0 {
type self = FibElse[n]
override type apply = fibonacci[n#decrement]#plus[fibonacci[n#decrement#decrement]]
}
This works in O(n), but:
type fibonacci[n <: sing.Nat] = sing.`if`[n#lt[_2], sing.const0[n], FibElse[n]]#apply#asNat
trait FibElse[n <: sing.Nat] extends sing.Function0 {
type self = FibElse[n]
override type apply = fibonacci[n#minus[_1]]#plus[fibonacci[n#decrement#decrement]]
}
This is O(n^2), for n#minus[_1] escapes memoization.
See C++ Template Metaprogramming APPENDIX C.3.1 if you are a C++ programmer.
You might notice that, because termmethods are not memoized, the performance complexitiy of typemethod and termmethod is different.
Type-level asInstanceOf is implemented by sing.Any.asXXX.
As a result, it is impossible for users to define new kinds.
Users must make full use of sing.TupleN and sing.map.
It is not known to implement the type-level assertion or exception.
(In fact, one possible way is to brew up the stack-overflow in the Scalac intentionally, but it's not informative at all.)
You can use sing.Test.assertTrue, which is the same as myAssert above, only if it takes a concrete invocation.
Scalac doesn't warn for an illegal invocation of sing.Any.asXXX,
which returns something like Nothing type. Nothing is the type-level null.
null is the disaster.
(This would be fixed if type-level assertion were feasible.)
It is difficult to generate boxed types, which wraps normal scala types, with practical usefulness: type-equality, conformance-ordering, etc... Working in theory, but complication would last for a few days.
See C++ Template Metaprogramming APPENDIX C.3.7.
Compilation speed is strongly influenced by the complexity of typemethod expression structure.
Trivial benchmark shows O(n^2) with nested level n.
isGround at nsc/symtab/Types.scala seems a bottle neck.
class Outer[m <: sing.Nat](m: m) {
type apply[n <: sing.Nat] = ...
case class Inner[n <: sing.Nat](n: n) extends sing.Function0 {
type self = Inner[n]
override type apply = ...
// ...
}
}
This form possibly makes compilation significantly slower.
equals at nsc/symtab/Names.scala seems a bottle neck.
Prefer class in object.
case doesn't effect on compilation time.
You can easily implement singmethods thanks to case classes.
trait MyKind extends sing.Any {
type foo <: sing.Nat
type bar = foo#plus[foo] // !!?
}
bar possibly returns a wrong type in call-site. (The minimal condition is not known yet.)
Define intermediate classes for default typemethod implementation; as Java does in AstractXXX classes.
Shunsuke Sogame <okomok@gmail.com>