Miles Sabin and Edwin Brady compare the expression of dependent types in Scala and Idris.
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 Sabin
Precog
@milessabin
milessabin
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 hom
Why it's here
2 people recommend this
What people say. Recommended for comparing how Scala and Idris handle dependent types and resource management at the type level.
b
u/bss03in r/haskell • Recommends
On “Scala has dependent types now”
Has effectively had them for 8 years: https://www.reddit.com/r/scala/comments/1s5eg3/scala_vs_idris_dependent_types_now_and_in_the/
It's quite a bit uglier than Idris, even the Scala developers admit it, but it was able to go proof vs. proof against a real dependently typed langauge in 2013, without experiencing "too much" code explosion.
It doesn't have purity though. It's hard enough to wrangle for the stuff I can do simply in Haskell; I'd never want to combine my DT code with unrestricted effects and deal with that snarl of code.
EDIT: The 2013 video has been recently uploaded to YouTube.
On “A language-level solution to detect "I did X but forgot to do Y" at compile time”
This reminds me of Idris where you enforce the release of resource at type level. They also use linear type.
There's a talk on it that compares Idris and Scala: link to this video
I take example from them to here:
```
testFile : FileIO ()
testFile = catch (
do open "testFile" Read
str <- readFile
putStrLn (show str)
ls <- Count :- get
close
putStrLn (show ls))
(\err => putStrLn ("Handled: " ++ show err))
```
In this example, if you remove the "close" line, the program simplely won't compile.
> weak
I think they can express all the same invariants, they just take a lot more code to do it in. link to this video (video is uploaded to YT recently, but the talk is from a while ago).
