```

// Computing the length of a type of the form (Int, (Int, Int)) etc

sealed trait LengthComputer[T]{

val length : Int

}

object LengthComputer{

implicit object One extends LengthComputer[Int]{

val length = 1

}

implicit def plusOne[T : LengthComputer] : LengthComputer[(Int, T)] =

new LengthComputer[(Int, T)]{

val length = implicitly[LengthComputer[T]].length + 1

}

}

def length[T : LengthComputer] = implicitly[LengthComputer[T]].length

println(length[Int]) // 1

println(length[(Int, (Int, Int))]) // 3

```

A more natural example (which I actually use) will be Currying in a similar context. I will write a minimal version later.

"Relation, not function:" We can model the key step by the relation {(T, LengthComputer[T])} on types. This is a function on the appropriate domain. But,

* the domain is not specified.

* More seriously, there is no guarantee that for an argument x in the domain, there is a single y with (x, y) in the relation, i.e., the relation is a function.

* Another problem with a relation based definition is that _composition_ becomes painful, one literally has to write the definition of composition at the relation level and use the implicit resolver.

All this makes it hard work to use functions from types to objects or other types, but as in the official foundations of mathematics functions are not first-class but are modelled from set membership via relations, in principle we should be able to work with scala as a dependently typed language. This is assuming the compiler is smart enough.

For a true dependently typed language (a la Agda), we need objects to be computed at compile-time, since types should be known at compile time and types can depend on objects. By definition this is meta-programming.

with regards,

Siddhartha