- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers
Stretching the type system too far?
Tue, 2012-02-07, 08:02
Hi,
I have some code where I'd like to type system to enforce some
constraints for me, but I also want to maintain separation between two
sections of code. This means that I don't want some sections of code
to have to know about (and annotate with) specific types from other
sections of the code. Below is a cut-down example. Is there any way
to get something like one of the SpecificBallUserCommander classes to
a) compile, b) enforce the constraints on the types of balls passed
around at compile time so that BallUsers only every use their
preferred ball types, and c) not have any specific references to
anything below Ball[P]? Or am I asking to much of the type system?
Thanks,
Will :-}
trait Ball[P] {
def getThing: P
def bouncing: Boolean
def bouncing_=(b: Boolean): Unit
}
trait BallUser[P] {
type KBall <: Ball[P]
def preferredBall: KBall
}
trait BallUserCommander[P, B <: Ball[P]] {
def startBouncing(b: B): Unit
}
// -------- now some specific instances
class RoundBall[P](var bouncing: Boolean) extends Ball[P] {
def getThing: P = sys.error("not implemented")
}
class EggBall[P](var bouncing: Boolean) extends Ball[P] {
def getThing: P = sys.error("not implemented")
}
class RoundBallUser[P] extends BallUser[P] {
type KBall = RoundBall[P]
def preferredBall: KBall = new RoundBall[P](false)
}
// ----------
// everything up until here compiles
// I do not want the following code to have to know about any specific
ball instances.
// The only type of Ball it can use is u.KBall <: Ball[P]
// But I also want the type system to stop me from passing to
startBouncing a ball that
// is not a u.KBall. (e.g. if u is a RoundBallUser then I can't pass
an EggBall to startBouncing()).
// I've included two approaches to the problem. Neither compiles.
// First, try and use u.KBall as the type as much as possible
// this seems to fail because the path dependent type cannot be used
as an argument in the extends clause
class SpecificBallUserCommanderA[P](val u: BallUser[P]) extends
BallUserCommander[P, u.KBall] {
type B = u.KBall
startBouncing(u.preferredBall)
// startBouncing(new EggBall[P](false)) // <-- should error
def startBouncing(b: B) {
b.bouncing = true
}
}
// Second, introduce a new type parameter, B, but then constrain it to
be u.KBall
// This was less likely to work, the implicitly would have to fail
when a
// SpecificBallUserCommanderB was constructed with B not the same as
u.BallUser[P]. That
// seems like quite complex reasoning for the type system.
class SpecificBallUserCommanderB[P, B <: Ball[P]](val u: BallUser[P])
extends BallUserCommander[P, B] {
implicitly[B =:= u.KBall]
startBouncing(u.preferredBall)
// startBouncing(new EggBall[P](false)) // <-- should error
def startBouncing(b: B) {
b.bouncing = true
}
}