Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Student works
  4. Formalizing GADT constraint reasoning in Scala
 
master thesis

Formalizing GADT constraint reasoning in Scala

Bucev, Mario  
June 25, 2021

Generalized algebraic data types (GADTs) are a powerful tool allowing to express invariants leveraging the type system. Scala 3 considerably improves the support of GADTs with respect to its predecessor Scala 2. A unique feature of Scala 3, compared to languages integrating GADTs, is the ability to define variant GADTs. While Scala 3 GADTs support is satisfactory, some use-cases could benefit from extending it further. In this work, we lay out the necessary tools to help us understand and reason about the GADT inference problem. We propose an algorithm that incrementally refines the accumulated knowledge about the type variables and prove its soundness. We also show some examples where the proposed algorithm is able to infer interesting properties that the current Scala 3 compiler misses.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

masterthesis-mariobucev.pdf

Type

N/a

Access type

openaccess

License Condition

Copyright

Size

2.15 MB

Format

Adobe PDF

Checksum (MD5)

f51586b4da69504e3217d766b9402c0f

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés