Skip to content
Hallway
0:00 / 0:00

#scala#refinementtypes#typesystems

[Scala'25] Logically Qualified Types for Scala 3

ACM SIGPLAN

11K subscribers • 65 videos on Hallway

YouTube
  • Recommended by 1 person: 1 in engineering communities.
  • Presented by Matt Bovel, EPFL

Advanced. Deep dive for people who know the field.

95 views11 months ago1 recommendation

Programming languagesComputer scienceLanguage design and type systemsComputation and complexityScala

Matt Bovel presents a design and prototype implementation of refinement types for Scala 3, integrated directly into the type checker.

Logically Qualified Types for Scala 3 (Video, Scala 2025) Matt Bovel (EPFL) Abstract: We present a new design and prototype implementation of refinement types for Scala, enabling types to be refined with logical predicates and statically checked by the compiler. Unlike previous work, our system integrates qualified types directly into the Scala type checker and performs subtyping via a lightweight, compiler-internal solver based on E-Graphs and expression normalization. The implementation builds on earlier student work, which explored syntax design and runtime checking mechanisms. Presentation at the Scala 2025 Workshop, Oct 13-14, 2025, 2025.workshop.scala-lang.org/ Sponsored by ACM SIGPLAN.

Why it's here

1 person recommends this

What people say. Cited as an example of active, impressive type system research and development in Scala 3.

u/phazer99in r/rust • Recommends

On “Rust and the price of ignoring theory”

The rumors about Scala's death are greatly exaggerated. Sure, it's lost some popularity due to the rise of other languages (Kotlin, Go, Rust etc.), but Scala 3 is still being developed at an impressive rate with new features like effects system/capabilities, refinement types etc. Personally, I really hope it sticks around for a long time.
11View on Reddit

u/phazer99in r/rust • Mentions

On “What is the type of a type in Rust?”

I think the closest we can hope for in a language like Rust is refinement types similar to what's been researched for Haskell and Scala. Even that would be very useful and solve most common use cases (bounded integers, index out bounds etc.) without the need to write manual proofs.
1View on Reddit