Scala Constraint Based Types and Literals

Question

I was wondering if it is possible to define a type of type NegativeNumber in Scala. This type will be a negative number, and it will be checked by the compiler in the same way as Ints, Strings, etc.

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

Similarly:

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

I could use these types in the same way as other types, for example:

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

These limited types can be supported by random types (Int, String).

Is it possible to implement these types (possibly using macros)?

What about custom literals?

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

Answer 1

Unfortunately, this is not something you could easily check at compile time. Well, at least not if you don't restrict operations on your type. If your goal is to simply verify that the numeric literal is nonzero, you can easily write a macro that checks this property. However, I see no use in proving that the negative literal is really negative.

The problem is not a limitation of Scala, which has a very strong type system, but the fact that (in a rather complicated program) you cannot statically know all the possible states. However, you can try to override the set of all possible states.

Consider an example of introducing a type of NegativeNumber , which only ever represents a negative number. For simplicity, we define only one operation: plus .

Suppose you would only allow the addition of several NegativeNumber , then a type system could be used to ensure that each NegativeNumber indeed a negative number. But this seems really restrictive, so a useful example will certainly allow us to add at least NegativeNumber and a generic Int .

What if you have the expression val z: NegativeNumber = plus(x, y) , where you do not know the values ​​of x and y statically (maybe they are returned by the function). How do you know (statically) that z is indead a negative number?

The approach to solving the problem will be the introduction of an abstract interpretation that should be performed on the representation of your program (source code, abstract syntax tree, ...).

For example, you can define a Lattice for numbers with the following elements:

• Top : all numbers
• + : all positive numbers
• 0 : number 0
• - : all negative numbers
• Bottom : not a number - just entered that each pair of elements has the largest lower bound

with order Top > ( + , 0 , - )> Bottom .

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

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

The problem is

• plus - + will be Top , because you do not know a positive or negative number.

To be statically safe, you need to take a conservative approach and prohibit such an operation.

There are more complex numerical domains , but in the end they all suffer from the same problem: they represent an excessive approximation of the actual state of the program.

I would say that the problem is similar to integer overflow / underflow: As a rule, you don’t know if the operation statically shows overflow - you only know this at runtime.

Answer 2

It would be possible if SIP-23 using implicit parameters as a form of refinement types. Nevertheless, this would be doubtful, though, since the Scala system and type system are not very well equipped to prove interesting things, for example, integers. To do this, it would be much better to use a language with dependent types (Idris, etc.) Or refinement types checked by the SMT solver (LiquidHaskell, etc.).