⬅ 🏠 Home
Often a distinction is made between static and dynamic typing.
If the application were dynamically typed, we would constantly have to verify that variables are indeed what they claim to be.
Say I have a variable
beethoven, can I assume that it is an instance of
# how can I be sure that this function argument is a composer? def my_function (composer) => composer.composer_method()
There are of course ways to check this, such as using the
isinstance method in Python, but this is rather tiresome.
To this end, we use types.
A user defines a class
Composer, which defines the behaviour of a composer:
stateless Composer def composer_method(): Int
And then we define the
my_function as such:
def my_function (composer: Composer): Int => composer.composer_method()
Now, in the body of the function, we can rest easy knowing that the passed variable is indeed a composer. It is actually now impossible to pass another variable type to the function, as this is statically checked by the type checker. If it sees that we try to pass something that is not a composer, will give an error, meaning that the program wil not run.
In some programming languages, we have to explicitly state the type of each variable. This however makes the application rather verbose. Take for instance:
def x: Int <- 10 # x is obviously an integer def c: Complex <- Complex(10, 20) # from the right hand side it is already clear that c is complex
Instead, we can use type inference. The type of every variable is inferred from the context in which it is used.
def x <- 10 # x has type Int, we know this because 10 is an Int def c <- Complex(10, 20) # c has type Complex def y <- 20.1 # 20.1 uses decimal notation, so we know y is a real number, or Real def z: Real <- 10.5 # In some situations however, you still might want to explicitly mention the type
The program is still statically typed, but now we don’t require the developer to write everything out in full.
We can also use type aliases and type refinement to further refine types by adding conditions to them. Say we have the following:
type DeadComposer isa Composer where self.death /= undefined else Err("Composer is not dead.")
We now rewrite my_function so it only works for
def my_function (composer: DeadComposer): Int => today.year - composer.death.year
Again, we can rest assured that
composer is a
DeadComposer in the body of the function.
To use such a function, we must explicitly cast a
def chopin <- Composer("Chopin") if chopin isa DeadComposer then def years_ago <- my_function(chopin) # chopin is dynamically casted to a DeadComposer print "[chopin.name] died [years_ago] years ago."
This draws on concepts of Design by Contract philosophy.
Furthermore, it also allows us to explicitly define the state of an object, something which is often left ambiguous. For instance, we can say a server is connected or disconnected by doing the following:
type Server def private connected: Boolean def send_message(self: ConnectedServer, message: String): String type ConnectedServer isa Server where self.connected else Err("Server is not connected")
And we may then elsewhere implement this
stateful MyServer isa Server def private connected <- false def init() => ... def connect(ip: IpAddress) => ... # You can only call this function if I am a connected server def send_message(self: ConnectedServer, message: String) => ...
This is a rather trivial example, but it shows how we can explicitly name the different states of a server.
In some cases, for readability we might want to write a type alias. Say we have the following function:
def distance_remaning(covered: Int): Int => self total - covered
The above seems simple, but there are two issues:
To solve the above two issues, we can use type aliases. Observe the following:
type Kilometer isa Int
Kilometer can do everything an
Int can (we can use all the same operators), but using such an alias allows us
to more clearly express our ideas in the codebase without relying on documentation. (This is a recurring theme, source
code ideally should speak for itself without relying heavily on documentation.) We can rewrite the function as so:
def distance_remaning(covered: Kilometer): Kilometer -> self total - covered
Type refinement expands upon type aliases by defining certain conditions an object must adhere to to be considered that type. This can also be used to enforce pre-conditions of a function or method when used as a parameter, and post-conditions when used as the return type. This is akin to the philosophy of Design by Contract.
Say we have a function:
def f (x: Int): Int => println("this number is even: [x]") x
In some situations, this function does not behave as we expect it to. It may print an uneven number. In such a situation, we often turn to the design by contract philosophy, where a function has pre and post-conditions. There are several traditional approaches to solving this problem, both if which are valid, though the preferred approach does depend on context:
x if it is uneven and don’t print anything using a simple
def f (x: Int): Int => if x mod 2 isnt 0 return x println("this number is even: [x]") x
Raise and error if
x is uneven:
def f (x: Int): Int raises [Err] => if x mod 2 isnt 0 raise Err("Expected x to be even.") println("this number is even: [x]") x
However, in the above code, we see that writing pre-conditions can get out of hand, and we might want to use the same pre-conditions for multiple functions, which results in duplicate code. This is a situation where type aliases with conditions can come in handy. Type aliases encourages decentralisation. The logic of a type is closely linked to the type itself, instead of having to manually check the a type adheres to certain conditions every time it is used.
We can use a trivial type
EvenNum to demonstrate how one would use conditions in a type alias. Say we define the
type EvenNum isa Int where self mod 2 is 0 # we can list more conditions below this one. They must all evaluate to a boolean.
Which is the same as:
type EvenNum isa Int where self mod 2 is 0 else Err()
We can also rewrite it for a more descriptive error message:
type EvenNum isa Int where self mod 2 is 0 else Err("Expected an even number but was: [self]")
This defines all
Int, or Integers, that are even. That is, the condition listed above holds. This is similar to creating
a new class
EvenNum which is a
Int, and verifying that these properties hold.
We can now redefine the function as follows:
# EvenNum has conditions, so we need to state that it may raise an error def g (x: EvenNum): Int raises[Err] => print "this number is even: [x]" x
Now, the actual type of the argument describes what conditions the argument adheres to, instead of having to manually
check these in the body of the function. We now know that these conditions hold in the body of the function. We can cast
any variable that is an
EvenNum. During casting, the defined conditions are checked, and the respective error
is thrown if a condition does not hold:
# We can cast x to an EvenNum, which might give an error def x <- random_int() # here x is an Int def y <- x as EvenNum raises [Err] def first <- g(y) # We can also pass it immediately if we want, in which case it is casted to EvenNum def z <- random_int() def second <- g(z) raises [Err] # which is the same as def second_with_case <- g(z as EvenNum) raises [Err] # Or just say that the variable is an EvenNum upon instantiation def y: EvenNum <- random_int() raises [Err] def third <- g(y) # We can also use the isa to check that the conditions holds without raising an error def a <- random_int() # notice how we don't have to cast a to an EvenNum if the condition holds. # We know that the then branch of the if is only executed if a is an EvenNum, so we assign it the type EvenNum fourth <- if a isa EvenNum then g(a) else 0 # If it can be statically verified that the propties hold, it is not necessary to handle any type specific errors def c <- 2 def fifth <- g(c) # first, second, third, fourth, and fifth all have type Int
We can also use it as a sort of post-condition of the function. We ensure that the function returns an
def g (x: EvenNum): EvenNum raises[Err] => print "this number is even: [x]" def y <- x + some_other_function(x) y as EvenNum raises [Err]
def g (x: EvenNum): EvenNum raises[Err] => print "this number is even: [x]" def y: EvenNum <- x + some_other_function(x) raises [Err] y
We can even ensure that the function never returns an error:
def h (x: EvenNum): EvenNum => print "this number is even: [x]" def y <- x + some_other_function(x) if y isa EvenNum then y # type sensitive flow ensure that this is an EvenNum else x
def x <- 10 # here x is an Int def a <- g(x as EvenNum) raises [Err] # a has type EvenNum def b <- g(a) raises Err # we don't have to cast a to an EvenNum, it is already of that type def c <- h(x) # function h never raises an error