## Dependent Types & Type Level Programming

Before we start you need to know that this post is intended for a public already familiar with type classes and implicit resolution in Scala. If you’re not, please have a read at this blog post.

As the title suggests, I’m going to go through these concepts and develop them in pure Scala code with no libraries involved. However, code in other languages will be shown for demonstration purposes.

At the end of the post you will find the links to all the code that is going to be shown.

### Summary

- Dependent Types
- Path Dependent Types
- Aux Type

- Dependent Function Type (Π-Type)
- Dependent Pair Type (Σ-Type)

- Path Dependent Types
- Phantom Types
- Type Level Programming (vs. Value Level)

### Dependent Types

Quoted from its definition in Wikipedia:

A dependent type is a type whose definition depends on a value.

Let’s see a code example in a pure functional programming language with dependent types like Idris.

isSingleton : Bool -> Type isSingleton True = Nat isSingleton False = List Nat

This simple function has one input of type Bool and one output type dependent on the input value. So, in case of True the output type is **Nat** (Natural Number) and in case of False is a **List Nat** (List of natural numbers). This is possible because *types are first class* in the Idris language.

Here’s a simple use case of this type function:

mkSingle : (x : Bool) -> isSingleton x mkSingle True = 0 mkSingle False = []

Here we are making use of the type definition **isSingleton** to return either a natural number zero or an empty list of natural numbers.

All these examples are taken from the Idris official documentation.

You can even determine what the type of the second parameter will be based on the input type. See the following code:

sum : (single : Bool) -> isSingleton single -> Nat sum True x = x sum False [] = 0 sum False (x :: xs) = x + sum False xs

And something very cool are Vectors, which are lists that include the length in its type.

(++) : Vect n a -> Vect m a -> Vect (n + m) a (++) Nil ys = ys (++) (x :: xs) ys = x :: xs ++ ys

For instance, in this function we have two inputs: one Vector of value type **a** and length **n** and another Vector of value type **a** and length **m**. And we are saying that the output type will be another Vector of the same value type **a** and length **(n + m)**. This is mind blowing!

If we try to implement it like this it won’t type check since the size of the expected Vector could be different from what it’s expected:

(++) : Vect n a -> Vect m a -> Vect (n + m) a (++) Nil ys = ys (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

### Path Dependent Types

Although Scala it is not a fully dependent type language, it is still possible to emulate dependent types either with path dependent types or with type level programming. We’ll soon see how.

We can define nested classes definitions and traits for example. See the following code:

class A { class B { class C { class D } } }

And we can define some instances of B for example:

val a1: A = new A val a2: A = new A val b1: a1.B = new a1.B val b2: a2.B = new a2.B

But what happens here?

val b3: a2.B = new a1.B val b4: a1.B = new a2.B

This won’t compile since the type B is dependent on the instance of A, so the type B has to belong to the same instance of A. This is very useful but sometimes you just want to have less constraints and accept any type B that belongs to any instance of A. In this case, what you need is *type projections **(using #)*:

val b5: A#B = new a1.B val b6: A#B = new a2.B

And we can do exactly the same with the classes C and D:

val c: A#B#C = new b1.C val d: A#B#C#D = new c.D

Okay, now let’s see a more useful case where path dependent types shine. Let’s define a type class **Foo[A]** with a type member **B**:

trait Foo[A] { type B def value: B }

And we also define two implicit instances of Foo for the types Int and String and define the type member B in both cases:

object Foo { implicit def fooInt = new Foo[Int] { override type B = String override def value = "Hey!" } implicit def fooString = new Foo[String] { override type B = Boolean override def value = true } }

Now we can have a function like this where both return type and result depend on the implicit instance of Foo:

def foo[T](t: T)(implicit f: Foo[T]): f.B = f.value val a: String = foo(1) // "Hey!" val b: Boolean = foo("qwe") // true

Here we see, how depending on the value passed to foo we get a different output type based on the implicit instance. **f.B** is also called an existential type since we don’t know what the concrete type will be but we do know it exists. This is a very cool trick but it has some limitations. Let’s make it a bit more complicated by adding a dependency on the Identity Monad with a type dependent on the Foo instance:

def fooAux[T](t: T)(implicit f: Foo[T], id: Identity[f.B]): f.B = f.value

The compiler will throw an error like this:

Error:(32, 29) illegal dependent method type: parameter may only be referenced in a subsequent parameter section def fooAux[T](t: T)(implicit f: Foo[T], id: Identity[f.B]): f.B = f.value

This is not possible because the dependent type is in the same list of parameters! So here is where the *Aux type* comes in handy.

#### Aux Type

type Aux[A0, B0] = Foo[A0] { type B = B0 }

We will define this **Aux** type inside the **Foo** companion object. The type **A0** from **Aux** is mapped to **A** from **Foo** and **B0** from **Aux** is mapped to **A#B** from** Foo**. The mind blowing thing here is that **B0** will also get the type assigned to **B**, even though one would think that **B0** is being assigned to **B **and not otherwise** **(it works both ways), that’s how we can keep track of the type member **B** and help the type inference system.

After that we can redefine our method **fooAux** in the following way:

def fooAux[T, R](t: T)(implicit f: Foo.Aux[T, R], id: Identity[R]): R = f.value val a: String = fooAux(2) // "Hey!" val b: Boolean = fooAux("asd") // true

This technique is widely used in the amazing type level programming library Shapeless.

### Dependent Function Type (Π-Type)

Also called **Pi Type **or **Dependent Product Type**, it defines a function that resolves the output type based on the input value. Let’s see how it can be done in the Idris language:

depType : Int -> Type depType 0 = Int depType 1 = String depType _ = Bool

We have dependent function type and we also define our data type DepProduct:

data DepProduct : (a : Type) -> (P : a -> Type) -> Type where MakeDepProduct : {P : a -> Type} -> ((x : a) -> P x) -> DepProduct a P

Now we can make use of it, for example:

x : DepProduct Int (\n => depType n) x = MakeDepProduct (\n => case n of 0 => 10 1 => "aaa" 2 => True)

What we are saying here is that when the input value is 0 the output value will be 10 (type Int). In case of 1 it will be “aaa” (type String). And in case of 2 it will be True (type Bool).

Let’s try to translate this into Scala.

Firstly, we need to have a definition of a Natural Number:

sealed trait Nat { type This >: this.type <: Nat type ++ = Succ[This] } object Zero extends Nat { type This = Zero } type Zero = Zero.type class Succ[N <: Nat] extends Nat { type This = Succ[N] }

Secondly, we define some type aliases and values:

type One = Zero# ++ type Two = One# ++ type Three = Two# ++ val _0: Zero = Zero val _1: One = new Succ[Zero] val _2: Two = new Succ[One] val _3: Three = new Succ[Two]

Now we define our depType function for Zero, One and any other natural number:

sealed trait DepType[N <: Nat] { type T def apply(x: N): T } implicit object depType0 extends DepType[Zero] { type T = Int override def apply(x: Zero) = 10 } implicit object depType1 extends DepType[One] { type T = String override def apply(x: One) = "abc" } implicit def depType[N <: Nat] = new DepType[Succ[Succ[N]]] { type T = Boolean override def apply(x: Succ[Succ[N]]) = true }

And finally we have an apply method to create an instance of a dependent function type:

object DepFunction { def apply[N <: Nat](x: N)(implicit depType: DepType[N]): depType.T = depType(x) }

Now let’s try it out!

val x: Int = DepFunction(_0) val y: String = DepFunction(_1) val z: Boolean = DepFunction(_2) //val t: Boolean = DepFunction(_1) // This does not compile!

And again we see how the output type depends on the input value of the dependent function type.

### Dependent Pair Type (Σ-Type)

Also called **Sigma Type **or **Dependent Sum Type**, it defines a pair where the second type is dependent on the first value. Let’s see how this is represented in the Idris language:

import Data.Vect vec : DPair Nat (\n => Vect n Int) vec = MkDPair 2 [3, 4]

Here we are defining a **Pair** of type **Nat** and **Vect n Int**. Note that **‘n’** is the first input value. This same definition can be represented using the syntax sugar **(a : A ** P)**:

vec2 : (n : Nat ** Vect n Int) vec2 = (2 ** [3, 4])

Cool thing is that both the input value and type can be inferred based on the second value!

-- Type inference of first argument vec3 : (n : Nat ** Vect n Int) vec3 = (_ ** [3, 4]) -- We can even omit the type of the argument n vec4 : (n ** Vect n Int) vec4 = (_ ** [3, 4])

This is how we can define it ourselves (In Idris they are called **DPair** an **MkDPair** respectively):

data DepPair : (a : Type) -> (P : a -> Type) -> Type where MakeDepPair : {P : a -> Type} -> (x : a) -> P x -> DepPair a P

You don’t really need to understand this definition. You can think of it as a **Tuple** in Scala where the second argument’s type depends on the value of the first argument. Something like **(Int, Type)** with implementations like **(1, Boolean)**, **(2, Int)**, **(3, String)** and so on.

Here we define again a function that will be used to determine the type of the second argument of the pair based on the first value:

depType : Int -> Type depType 0 = Int depType 1 = String depType _ = Bool

x : DepPair Int (\n => depType n) x = MakeDepPair 0 10 y : DepPair Int (\n => depType n) y = MakeDepPair 1 "abc" z : DepPair Int (\n => depType n) z = MakeDepPair 2 True

Here the second type of the pair will be dependent on the definition of depType. Let’s translate this last example into Scala.

Assuming that we have the definition of **Nat** in scope plus the types and values we defined previously, we can now define our **depType** function for Zero, One and any other natural number:

sealed trait DepType[N <: Nat] { type T } implicit object depType0 extends DepType[Zero] { type T = Int } implicit object depType1 extends DepType[One] { type T = String } implicit def depType[N <: Nat] = new DepType[Succ[Succ[N]]] { type T = Boolean }

And finally our DepPair type:

case class DepPair[N <: Nat, V](x: N, value: V)(implicit depType: DepType[N] { type T = V })

Let’s try it out!

DepPair(_0, 10) DepPair(_1, "a") DepPair(_2, true) //DepPair(_3, "b") //This does not compile!

Again we are seeing how powerful dependent types are.

### Phantom Types

Phantom Types are such a simple concept but at the same time very powerful. Let’s try to understand them by example.

Here we have a definition of Effects and Roles:

trait Effect object Effect { trait Read extends Effect trait Write extends Effect trait Delete extends Effect trait Update extends Effect } trait Role object Role { trait Anonymous extends Role trait User extends Role trait Admin extends User }

Nothing fancy, just type definitions. Now, let’s say we have a File which can only be accessed having the appropriate Role:

trait File[R <: Role] object File { def apply[R <: Role] = new File[R] {} }

And now we want to perform Actions and constraint them to a particular Role:

trait Action[F <: Effect, R <: Role] object Action { def apply[F <: Effect, R <: Role] = new Action[F, R] {} def read[R <: User](db: File[R]) = new Action[Read, R] {} def write[R <: User](db: File[R]) = new Action[Write, R] {} def delete[R <: Admin](db: File[R]) = new Action[Delete, R] {} def update[R <: Admin](db: File[R]) = new Action[Update, R] {} }

And this is how we use it:

// Action.read(File[Anonymous]) // Does not compile! Action.read(File[User]) Action.write(File[User]) // Action.delete(File[User]) // Does not compile either! Action.read(File[Admin]) Action.write(File[Admin]) Action.delete(File[Admin]) Action.update(File[Admin])

In the first case that does not compile, we will get an error like this from the Scala compiler:

Error:(40, 10) inferred type arguments [com.github.gvolpe.types.phantom.PhantomTypes.Role.Anonymous] do not conform to method read's type parameter bounds [R <: com.github.gvolpe.types.phantom.PhantomTypes.Role.User] Action.read(Database[Anonymous]) Error:(40, 23) type mismatch; found : com.github.gvolpe.types.phantom.PhantomTypes.Database[com.github.gvolpe.types.phantom.PhantomTypes.Role.Anonymous] required: com.github.gvolpe.types.phantom.PhantomTypes.Database[R]

Saying that the Anonymous Role is not sufficient to invoke the read method that requires at least a User Role.

Up until now we have seen how we defined these types and used them just to add constraints to our methods but we have never created any instance of these traits, that’s why they are called Phantom Types. For further lecture, take a look at the great blog post of Daniel Westheide.

These types are also used in languages like Haskell. For example, they are useful when defining GADTs (Generic Algebraic Data Types):

data Expr a = I Int | B Bool | Add (Expr a) (Expr a) | Mul (Expr a) (Expr a) | Eq (Expr a) (Expr a)

Here **a** is a type variable where its sole purpose is to constraint operations and it actually is a phantom type since it never gets instantiated, it just marks the intended type of the expression.

### Type Level Programming (vs. Value Level)

Let’s start by defining our own Boolean type with some logical operations:

sealed trait Bool { def not: Bool def &&(b: Bool): Bool def ||(b : Bool): Bool def ifElse[C](t: => C, f: => C): C } case object True extends Bool { override def not = False override def &&(b: Bool) = b override def ||(b: Bool) = True override def ifElse[C](t: => C, f: => C) = t } case object False extends Bool { override def not = True override def &&(b: Bool) = False override def ||(b: Bool) = b override def ifElse[C](t: => C, f: => C) = f }

And then verify that behaves as we expect:

False.not == True False.&&(True) == False False.||(True) == True False.ifElse(1, 2) == 2

In a similar way, we can define the same Bool type at the type level:

sealed trait Bool { type Not <: Bool type && [B <: Bool] <: Bool type || [B <: Bool] <: Bool type IfElse [C, T <: C, F <: C] <: C } type True = True.type type False = False.type object True extends Bool { type Not = False type && [B <: Bool] = B type || [B <: Bool] = True type IfElse [C, T <: C, F <: C] = T } object False extends Bool { type Not = True type && [B <: Bool] = False type || [B <: Bool] = B type IfElse [C, T <: C, F <: C] = F }

And we can verify the behavior by using the **=:=** operator in combination with **implicitly**.

implicitly[False# Not =:= True] implicitly[False# && [True] =:= False] implicitly[False# || [True] =:= True] implicitly[False# IfElse[Any, Int, String] =:= String] // implicitly[True# IfElse[Any, Int, String] =:= String] // This does not compile!

#### Natural Numbers, Factorial and Fibonacci

Now that we have seen a simple type like Bool defined at the type level, let’s see how to implement our own representation of Natural Numbers at the type level:

sealed trait Nat { type This >: this.type <: Nat type ++ = Succ[This] type + [_ <: Nat] <: Nat type * [_ <: Nat] <: Nat } object Zero extends Nat { type This = Zero type + [X <: Nat] = X type * [X <: Nat] = Zero } class Succ[N <: Nat] extends Nat { type This = Succ[N] type + [X <: Nat] = Succ[N# + [X]] type * [X <: Nat] = (N# * [X])# + [X] }

We’ve seen this previously, but here we added two new types to perform sum and multiplication. If we also define some types, we can verify the correctness of our definition:

type Zero = Zero.type type One = Zero# ++ type Two = One# ++ type Three = Two# ++ type Four = Three# ++ type Five = Four# ++ type Six = Five# ++ implicitly[Two# + [Three] =:= Five] implicitly[One# + [Two] =:= Three] implicitly[Two# * [Two] =:= Four] // implicitly[Two# + [Three] =:= Four] // Does not compile

#### Factorial

This is how we can define it in terms of **Nat** and verify its correctness:

sealed trait Factorial[N <: Nat] { type Res <: Nat } implicit object factorial0 extends Factorial[Zero] { type Res = One } implicit def factorial[N <: Nat, X <: Nat](implicit fact: Factorial[N] { type Res = X}) = new Factorial[Succ[N]] { type Res = X# * [Succ[N]] } implicitly[Factorial[Zero] { type Res = One }] implicitly[Factorial[One] { type Res = One }] implicitly[Factorial[Two] { type Res = Two }] implicitly[Factorial[Three] { type Res = Six }] // implicitly[Factorial[Three] { type Res = Five }] // Does not compile!

#### Fibonacci

Here we can do pretty much the same we did with Factorial:

sealed trait Fibonacci[N <: Nat] { type Res <: Nat } implicit object fibonacci0 extends Fibonacci[Zero] { type Res = Zero } implicit object fibonacci1 extends Fibonacci[One] { type Res = One } implicit def fibonacci[N <: Nat, X <: Nat, Y <: Nat](implicit fib1: Fibonacci[N] { type Res = X}, fib2: Fibonacci[Succ[N]] { type Res = Y }) = new Fibonacci[Succ[Succ[N]]] { type Res = X# + [Y] }

And verify its correctness:

implicitly[Fibonacci[Two] { type Res = One }] implicitly[Fibonacci[Three] { type Res = Two }] implicitly[Fibonacci[Four] { type Res = Three }] implicitly[Fibonacci[Five] { type Res = Five }] // implicitly[Fibonacci[Five] { type Res = Two }] // Does not compile!

### Final thoughts

If you’re still processing the first paragraph, don’t worry! We went through a lot of stuff hard to digest in a single reading, I know the feeling… Anyway, I hope this post has motivated you to go for more and explore these concepts in a deeper level. Thanks for reading!

The code shown in this post is available on GitHub:

- Scala -> https://github.com/gvolpe/dependent-types
- Idris -> https://github.com/gvolpe/idris-dependent-types

*DISCLAIMER: Most of the examples were taken from the online course ThCS Introduction to programming with dependent types in Scala.*

Cheers,

Gabriel.