Ensuring that computers can check the consistency of programs in advanced languages like Scala

What is it about?

New programming languages like Scala and Wyvern have introduced path-dependent types. With path-dependent types, programmers can distinguish objects created by different modules, for example two different implementations of a Table type. Unfortunately, Scala's compiler might fail to typecheck programs sometimes due to the complexity of checking path-dependent types. We describe an approach that places some restrictions on Scala--restrictions that are easy to understand, and which we believe don't prohibit programs that developers want to write--and in turn guarantees that the compiler can always typecheck programs with path-dependent types.

Featured Image

Why is it important?

Path-dependent types can help programmers make sure their programs do what is intended, so helping compilers deal with them successfully can make a big difference to the future of software development.