Path dependent types

Modeling algebraic structures has never been easier

Marcin Rzeźnicki
May 5, 2015 · 7 min read

Path dependent types

You need to know that Scala has a notion of a type dependent on a value. Only that the notion of dependency is not expressed in type signature but rather in type placement. Martin Odersky outlined this idea in a co-authored paper Foundations of Path-Dependent Types where we read:

Problem to solve

When I feel my algorithmic skills are getting rusty, I usually end up checking Codility’s web page and finding myself a challenging problem to work on (BTW, I recommend it to everyone — it simply makes you a better programmer). I always try not only to solve a problem, but also to write the most idiomatic code in a language I am using. This way you can enjoy two benefits simultaneously: your problem solving fu is going up and the mastery of your language of choice is skyrocketing.

Solution

To summarize, we need to devise a system that lets us:

  1. be sure that compiler won’t let us use int mod N as int mod M.

Epilogue

I hope I showed you how various flavors of dependent typing can be useful in everyday programming. While we can’t yet enjoy expressiveness of type systems with full dependent types, Scala has enough to control type dependencies in amazing ways you’d think are only possible at the run time. If you’re wondering what is the precise relation between path-dependent types and dependent types, let me point you to Miles Sabin’s thoughtful and detailed reply to similar question on Stack Overflow:

VirtusLab

Virtus Lab company blog

Marcin Rzeźnicki

Written by

Using Scala to build most composable and concise business logic @ iterato.rs

VirtusLab

VirtusLab

Virtus Lab company blog