# Cogita et Visa

## Dependent Types in Scala

12:42 PM Posted by Yuriy Polyulya
Dependent Types are types that depend on elements of other types. In other words it is a type that is predicated upon a value. An example is the type An of vectors of length n with components of type A and type An depends on the number n, or that A n is a family of types indexed by the number n.

"Dependent types == first-order logic" (c) Neelakantan Krishnaswami.

Motivation:
To show way of dependent type difinition in Scala by path-dependent type and implicit parameters features.

Something like:
```def mapTo[B](x : ListOf[1, Int]): (Int => B) => ListOf[1, B]
def mapTo[B](x : ListOf[2, Int]): (Int => B) => (Int => B) => ListOf[2, B]
def mapTo[B](x : ListOf[3, Int]): (Int => B) => (Int => B) => (Int => B) => ListOf[3, B]
```

#### 1. Define type ListOf what depends from it size:

Will use wrapping container as type parametr for manage type of list what depends on Size, code:
```trait Size
trait Wrap[N <: Size] extends Size

object Size {
trait _0 extends Size
type _1 = Wrap[_0]
type _2 = Wrap[_1]
type _3 = Wrap[_2]
type _4 = Wrap[_3]
// ... more '_N' if needed
}
```

And ListOf code:
```trait ListOf[+N <: Size, +H] {
def ::[N0 >: N <: Size, H0 >: H](x : H0) : ListOf[Wrap[N0], H0] = com.immediatus.::(x, this)
}

case class ::[N <: Size, H](x : H, xs : ListOf[N, H]) extends ListOf[Wrap[N], H] {
override def toString = s"\$x, \$xs"
}

trait Nill extends ListOf[Size._0, Nothing]
case object Nill extends Nill
```

Usage example:
```  val xs1 = 10 :: Nill
val xs2 = 10 :: 20 :: Nill
val xs3 = 10 :: 20 :: 30 :: Nill
```
And type test:
```  import Size._
val a : ListOf[_1, Int] = xs1
val b : ListOf[_2, Int] = xs2
//val b : ListOf[_2, Int] = xs1 // -- compilation error
```

#### 2. Define method with dependent type:

Will define method 'mapTo' what will depends on type:
```object Core {
def mapTo[N, H](xs : ListOf[N, H]): 'some_dependent_from_listOf_type' = ...
}
```

In general, 'mapTo' returned type needs to depend on type variable 'N'. This can be defined by implicit parameter, where implicit variable will contain returned type for type variable 'N' in type 'ListOf'.
Will define trait 'RET' for implicitly definition of returned type:
```trait RET[T] { type Type }
```

than 'mapTo' will be defined as:
```
def mapTo[N, H](xs : ListOf[N, H])(implicit ret : RET[ListOf[N, H]]): ret.Type = ...
```

Will define 'RET' implicit instances for 'ListOf':
```object RET {
import Size._
type R[N <: Size, H, S] = RET[(ListOf[N, H], S)]
type F[H, S] = Function1[H, S]

implicit def list1[H, S] = new R[_1, H, S] {
type Type = F[H, S] => ListOf[_1, S]
}

implicit def list2[H, S] = new R[_2, H, S] {
type Type = F[H, S] => F[H, S] => ListOf[_2, S]
}

implicit def list3[H, S] = new R[_3, H, S] {
type Type = F[H, S] => F[H, S] => F[H, S] => ListOf[_3, S]
}
}
```

'RET' is defined for tuple '(ListOf[N, H], S)' because Function type parameters needed to be defined at the moment of implicit variable substitution or delegated as type parameter.
After all code of 'Core' object with 'mapTo' method will looks like:
```object Core {
// .. RET ...

def mapTo[S] = new {
def apply[N <: Size, H](xs : ListOf[N, H])(implicit ret : RET[(ListOf[N, H], S)]): ret.Type = {
type F = H => S
def \$ret[X](r : X): ret.Type = r.asInstanceOf[ret.Type]

xs match {
case (x : H) :: Nill =>
\$ret{ (f : F) => f(x) :: Nill }

case (x : H) :: (y : H) :: Nill =>
\$ret{ (f : F) => (g : F) => f(x) :: g(y) :: Nill }

case (x : H) :: (y : H) :: (z : H) :: Nill =>
\$ret{ (f : F) => (g : F) => (h : F) => f(x) :: g(y) :: h(z) :: Nill }

case _ => throw new IllegalArgumentException
}
}
}
}
```

Method 'mapTo' was changed for more natural application, because some parameters need to set manually and some can be inferred by compiler.

#### 3. Test dependent types:

```  val xs1 = 10 :: Nill
val xs2 = 10 :: 20 :: Nill
val xs3 = 10 :: 20 :: 30 :: Nill

val map1 = Core.mapTo[String](xs1)
val map2 = Core.mapTo[String](xs2)
val map3 = Core.mapTo[String](xs3)

println {
xs1 + " ---> " + map1(_ + "!") // map1(_ + "!")(_ + "?") // -- compilation error
}

println {
xs2 + " ---> " + map2(_ + "!")(_ + "?") // map2(_ + "!")(_ + "?")(_ + "#") // -- compilation error
}

println {
xs3 + " ---> " + map3(_ + "!")(_ + "?")(_ + "#")
}
```

Note:
Scala project here.