What is the difference between a type and a newtype?

Question

One can define a subset type like this

type int8 = x: int | -128 <= x < 128

and a newtype like this

newtype nint8 = x | -128 <= x < 128

What is the difference?

Answer

In both cases, the values in the type are limited to the given range, but a newtype intends to define a whole new type that, although still based on integers and allowing integer operations, is not intended to be mixed with integers.

This is evident in the allowed conversions, as shown in this example code:

type int8 = x: int | -256 <= x < 256
newtype nint8 = x : int | -256 <= x < 256

method test(i: int, i8: int8, ni8: nint8) {
  var j: int, j8: int8, nj8: nint8;
  if -256 <= i < 256 { j8 := i; } // implicit conversion OK if in range
  if -256 <= i < 256 { nj8 := i as nint8; } // explicit conversion required
  j := i8; // always allowed
  j := ni8 as int; // explicit conversion required
}
  

The other important characteristic of newtypes is that they may have a different representation in the compilation target language. Subset types are always represented in the same way as the base type. But a newtype may use a different representation. For example, the newtype defined above might use a byte representation in Java, whereas an int is a BigInteger. The representation of a newtype can be set by the program author using the {:nativeType} attribute.