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
- Dependent Function Type (Π-Type)
- Dependent Pair Type (Σ-Type)
- 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:
DISCLAIMER: Most of the examples were taken from the online course ThCS Introduction to programming with dependent types in Scala.
Cheers,
Gabriel.
PartialFlow 