CODEWITHSUNDEEP
scalatypesconstraintsscala-macros
David Frank
David Frank

Reputation: 6092

Scala constraint based types and literals

I was thinking whether it would be possible in Scala to define a type like NegativeNumber. This type would represent a negative number and it would be checked by the compiler similarly to Ints, Strings etc.

val x: NegativeNumber = -34
val y: NegativeNumber = 34 // should not compile

Likewise:

val s: ContainsHello = "hello world"
val s: ContainsHello = "foo bar" // this should not compile either

I could use these types just like other types, eg:

def myFunc(x: ContainsHello): Unit = println(s"$x contains hello")

These constrained types could be backed by casual types (Int, String).

Is it possible to implement these types (maybe with macros)?

How about custom literals?

val neg = -34n  //neg is of type NegativeNumber because of the suffix
val pos = 34n  // compile error

Upvotes: 6

Views: 247

Answers (2)

Jesper Nordenberg
Jesper Nordenberg

Reputation: 2104

It could be possible if SIP-23 was implemented, using implicit parameters as a form of refinement types. However, it would be of questionable value though as the Scala compiler and type system is not really not well equipped for proving interesting things about for example integers. For that it would be much nicer to use a language with dependent types (Idris etc.) or refinement types checked by an SMT solver (LiquidHaskell etc.).

Upvotes: 0

Kulu Limpa
Kulu Limpa

Reputation: 3541

Unfortunately, no this isn't something you could easily check at compile time. Well - at least not if you aren't restricting the operations on your type. If your goal is simply to check that a number literal is non-zero, you could easily write a macro that checks this property. However, I do not see any benefit in proving that a negative literal is indeed negative.

The problem isn't a limitation of Scala - which has a very strong type system - but the fact that (in a reasonably complex program) you can't statically know every possible state. You can however try to overapproximate the set of all possible states.

Let us consider the example of introducing a type NegativeNumber that only ever represents a negative number. For simplicity, we define only one operation: plus.

Say you would only allow addition of multiple NegativeNumber, then, the type system could be used to guarantee that each NegativeNumber is indeed a negative number. But this seems really restrictive, so a useful example would certainly allow us to add at least a NegativeNumber and a general Int.

What if you had an expression val z: NegativeNumber = plus(x, y) where you don't know the value of x and y statically (maybe they are returned by a function). How do you know (statically) that z is indead a negative number?

An approach to solve the problem would be to introduce Abstract Interpretation which must be run on a representation of your program (Source Code, Abstract Syntax Tree, ...).

For example, you could define a Lattice on the numbers with the following elements:

  • Top: all numbers
  • +: all positive numbers
  • 0: the number 0
  • -: all negative numbers
  • Bottom: not a number - only introduced that each pair of elements has a greatest lower bound

with the ordering Top > (+, 0, -) > Bottom.

Sign-Lattice

Then you'd need to define semantics for your operations. Taking the commutative method plus from our example:

  • plus(Bottom, something) is always Bottom, as you cannot calculate something using invalid numbers
  • plus(Top, x), x != Bottom is always Top, because adding an arbitrary number to any number is always an arbitrary number
  • plus(+, +) is +, because adding two positive numbers will always yield a positive number
  • plus(-, -) is -, because adding two negative numbers will always yield a negative number
  • plus(0, x), x != Bottom is x, because 0 is the identity of the addition.

The problem is that

  • plus - + will be Top, because you don't know if it's a positive or negative number.

So to be statically safe, you'd have to take the conservative approach and disallow such an operation.

There are more sophisticated numerical domains but ultimately, they all suffer from the same problem: They represent an overapproximation to the actual program state.

I'd say the problem is similar to integer overflow/underflow: Generally, you don't know statically whether an operation exhibits an overflow - you only know this at runtime.

Upvotes: 3

Related Questions