What’s Scala’s stance on general dependent types?

Question
1

Hi folks,

I’m coming from an Idris2 background and currently learning both Haskell and Scala (yes, I may have a language learning problem :sweat_smile:).

Idris2 is built around dependent types from the start. Haskell is now getting them incrementally through ongoing GHC work. Scala, on the other hand, has a lot of powerful type-level features already, and even limited support for some forms of dependent typing.

Could I ask:

What’s the current state of dependent type support in Scala?

Are there any active or long-term goals to support full dependent types like in Idris or Agda?

Or is the general direction to stay within a more practical subset?

I’m trying to understand how expressive Scala wants to be on the type level in the long run

Thanks!
Diego Rosario

on ongoing dependent haskell work : Dependent Haskell Roadmap

2

Hi there :wave:
I’m a Lean4 user myself.

I don’t think Scala can support full dependent types like Idris or Agda or Lean. Because Scala’s DOT (dependent object types) system has a vastly different type calculus, which I assume is incompatible with things like Calculus of Constructions. When you have subtyping, class hierarchies, covariance / contravariance, etc. you leave that world behind.

Scala’s DOT was the result of so many years of work and research, proving its soundness and then rewriting the compiler. Its goal from the start was to fuse OOP and FP, not a fully dependent FP-style type system. Scala’s type calculus is unique in that regard, and is not part of the Hindley-Milner family or the CoC family (to the best of my knowledge). Trying to add Idris-like type systems would require even more years of research and yet another uprooting of the whole language (like Scala 3 did).

So Scala opted to have partial support for certain dependently typed programming patterns that are suitable for its needs, like Match Types and Dependent Function Types for example. This approach seems to be powerful enough for Scala users’ needs.

I think the long-term goal is to stay more practical. This is not related to types, but you can read Evolving Scala which was posted recently (video talk version here by Martin himself). Current research is not about type systems, it’s about effect/capability systems (think of it as a more general version of Rust’s borrow checker, applied to any kind of resource / capability, not just memory management).

One can also ask, does Scala really need a fully dependently typed system? Scala’s use cases are very different than Idris / Agda / Haskell / Lean and it might not make much sense.

A more philosophical question is the meaning of this word “dependent type”. It’s a term that is used very loosely to mean many things. There isn’t a strict formal definition, there are many dependent type systems out there (CoC, Girard’s System F, and so on). From a philosophical standpoint you could argue that Scala’s type system is “fully dependent”, I mean it’s called “dependent object types” isn’t it? :laughing: (Also path dependent types play a fundamental role in DOT.) Even a parameterized type is an example of a “dependent type”: List[T] depends on T; but type parameters are everywhere and people are familiar with it, so nobody calls it “dependent type”. So, what most people mean by “dependent types” is the features and patterns available in one of those languages: Idris, Agda, Lean, etc.

That’s the best of my understanding, hope it helps! :smile:

4 Likes
3

Scala aims to have only a subset of dependent types called “Path dependent types”

Here’s a paper on the subject if you’re into that kind of reading:

(No idea if it’s the best/most recent)

2 Likes
4

Oh yes, I was going to mention that path dependent types play a big role in Scala’s type system, but I couldn’t find the link I was looking for, thanks @Sporarum

I think the link I was thinking of was this: Work-in-Progress Scala 3 Specification | The Scala Programming Language

When learning or teaching Scala, not many people would choose path-dependent types and higher-kinded types as the first concepts to explore. Yet, in the Scala 3 specification, these are the most fundamental types, which therefore come first.

5

In idris2 and haskell ( with líquid haskell at least ) i can define properties such as "output Is a permutation of input " and “output Is ordered” which can then be assigned to a function. The function Will only compile if it meets those properties. In this example it means you or the compiler must prove the function sorts it’s input.

Those languages also allow You to verify that for any finite input, a function Will never halt ( only for some functions , but there are no false positives )

Does scala allow this in the main language or with an add-on?

6

Not directly with the type system, but with some code (or libraries) it’s possible. (Scala doesn’t have language extensions in the same way Haskell does; there are experimental opt-in features, but nothing that fundamentally alters how the type system works.)

For example, for a function, requiring certain conditions can be done by having a (using evidence: ...) implicit parameter. You would define a trait that checks the condition you want, then provide a typeclass instance for it. (This blog article might be an interesting but limited example.) To do it directly for a type, you can use a library like Iron or Refined.

1 Like
7

By addon i meant a compiler plugin. Liquid haskell is one such an example. I must have been more clear, since haskell is notorious for opt in features. You could call them addons

Speaking of liquid types, java has such a plugin : GitHub - CatarinaGamboa/liquidjava

How much do the tecniques you mentioned allow you to define properties and check if they hold true for some code? I mentioned the function being total ( never halting for finite input ) and checking if a function sorts its input

With both dependent types and liquid types i can also do things like :

Define the rules of a game. Such that a match consisting of a series of moves will typecheck only if all the moves adhere to the rules of the game

You can use this scheme to run matches of a game at compile time ( you would need to embed the compiler in your game executable ). Or you could write a game interpreter and then prove it follows the rules

8

I am not aware of compiler plugins that change the type system; compiler plugins are often used for other purposes such as: build tools, different backends and code generation (Scala Native, Scala.js), source code rewriting / linting, some syntax sugar / desugar, and so on.

But it might be possible to achieve what you want with compiler plugins, I just don’t know enough about them. This repository for example, shows how to do compile-time checking of division by zero, among other things. Changing the type system however would be quite difficult. It is mentioned here that you can indeed change the type checker with a custom compiler plugin if you want.

The techniques I mentioned can be taken quite far, and this is done by some people. (I vaguely remember that rule-checking type of stuff is done at Netflix or Disney, I can’t remember exactly). I would probably go with Refined or Iron first to see how far I could take them, instead of a compiler plugin.

But I wouldn’t expect Idris/Haskell kind of capability / expressivity from the types themselves; Scala’s type system is just too different. Having used Lean quite a bit myself I’m aware of the differences.

1 Like
9

Liquid haskell doesnt change the type system. It is a way to define additional rules that are checked in addition to normal haskell type checking. In fact, it uses generic haskell annotations that any plugin or preprocessor can take advantage of, instead of dedicated syntax. Plus removing said anotations will result in no runtime difference.

I think this is a general property of refinement types. I have talked with F* devs, a language that has both dependent and refinement types. In the general case, compiling F* to non dependent languages such as ocaml, result in hacks and non idiomatic code; F# cant even handle the full language in any way . However, when only using refinement types , code is compiled as expected

There also used to be liquid types for SML. A language which lack exotic type features to an even greater extent than F#. And as mentioned above there is even liquid types for java. But i havent checked that

Besides iron and refined, there is this tool : GitHub - epfl-lara/stainless: Verification framework and tool for higher-order Scala programs

As you mentioned, scala is very different from haskell, idris and lean. However it would be very interesting if it still allowed property checking. To take advantage of scalas strengths such as interop with java and native code respectively.

10

I’m sure it does; you’ll just have to ask someone more experienced and knowledgeable with advanced Scala stuff :smiley: Maybe try Discord.

1 Like