This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Stretching the type system too far?

No replies
William Uther
Joined: 2010-09-13,
User offline. Last seen 42 years 45 weeks ago.

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
}
}

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland