© 2020 Strange Loop
Scala is a modern hybrid object-functional programming language for the Java Virtual Machine. It has seen growing popularity and near-mainstream acceptance in recent years, in part because it can be viewed as a “better Java” and has been successfully used in that way. But focussing only on this aspect would be selling the language short. It has a rich (some would say to the point of indigestibility) type system with sufficient expressive power to capture static constraints and programme properties in ways which can only be matched by Haskell, amongst near-mainstream languages, and the upcoming generation of full spectrum dependently typed programming languages such as Agda and Idris.
I (Miles) have been exploring this perspective on Scala for the last few years in my project shapeless, and have become convinced both that powerful type systems in general (and dependent types in particular) are the way forward, and that Scala offers us a tantalizing glimpse of what will be possible in the very near future. Tantalizing, but also often frustrating: Scala’s type system is sophisticated enough to make the previously impossible, possible, but not to make it easy. For that we need to look elsewhere …
Idris is an experimental functional programming language with full spectrum dependent types, meaning that types can be predicated on any value. Its syntax is influenced by Haskell. As well as full dependent types it supports records, type classes, tactic based theorem proving, totality checking, and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to functional programmers while still supporting efficient systems programming via an optimising compiler and interaction with external libraries.
I (Edwin) have been designing and using Idris to experiment with verification of functional properties (i.e. whether a program gives the correct answer) and non-functional program properties (i.e. whether the program behaves correctly with respect to its environment). For example, a functional property we can verify is whether a binary adder calculates a correct answer by relating it to a unary adder with known properties. Non-functional properties we can verify include static checking of resource usage such as files, locks in concurrent programming, and network sockets.
In this talk, we will demonstrate what is possible with modern, rich type systems. We will show, by example, what can be achieved in a near-mainstream language now, discuss its limitations, and see what may be possible in the future as languages with full dependent types reach maturity.
Miles does stuff with Scala for Precog. When not working on Precog, he does his utmost to break Scala’s typechecker with his project shapeless and is a regular speaker at Scala and functional programming events. He can often be found walking in the South Downs around his home in Brighton with a camera and an unfeasibly energetic English Springer Spaniel named Tigger.
Edwin Brady is a Lecturer in Computer Science at the University of St Andrews in Scotland, UK. His research interests there include programming language design, in particular type systems and domain specific languages. Since 2008, he has been designing and implementing the Idris programming language (http://idris-lang.org), a general purpose functional programming language with dependent types, which he uses to implement verified domain specific languages. When he’s not doing that, he’s likely to be playing a game of Go, wrestling with the Guardian crossword, or stuck on a train somewhere in Britain.