Functions from types using impicits

classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

Functions from types using impicits

Siddhartha Gadgil
Since there was some discussion on another thread, here is a minimal example using implicits to define a function, but via a relation, from Types to Objects (on scalafiddle at https://scalafiddle.io/sf/xPjH3Vb/0). This takes specific types, those built from Int by iterated pairing and returns lengths.

```
// 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


--
You received this message because you are subscribed to the Google Groups "scala-user" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
For more options, visit https://groups.google.com/d/optout.