CODEWITHSUNDEEP
scalatypes
Synesso
Synesso

Reputation: 38998

How to constrain a type to a subset of another?

I have that this is a dumb question feeling, but here goes ... Can I define a type that is a subset of the elements of a another type? Here's a simplified example.

scala> class Even(i: Int) {
     | assert(i % 2 == 0)  
     | }
defined class Even

scala> new Even(3)
java.lang.AssertionError: assertion failed

This is a runtime check. Can I define a type such that this is checked at compilation? IE, that the input parameter i is provably always even?

Upvotes: 3

Views: 182

Answers (1)

Kevin Wright
Kevin Wright

Reputation: 49705

Value-dependent typing in languages such as Coq and Agda can do this, though not Scala.

Depending on the exact use-case, there are ways of encoding peano numbers in the type system that may, however, help you.

You might also want to try defining both Even and Odd along with some sealed abstract supertype (OddOrEven perhaps) and a factory method that returns the correct instance from any given Integer.

Another possibility is to define Even as an extractor.

Upvotes: 7

Related Questions