Publication

Towards Improved GADT Reasoning in Scala

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki, Paolo Giosuè Giarrusso
2019
Conference Papers

Abstract

Generalized algebraic data types (GADT) have been notoriously difficult to implement correctly in Scala. Both major Scala compilers, Scalac and Dotty, are currently known to have type soundness holes related to them. In particular, covariant GADTs have exposed paradoxes due to Scala's inheritance model. We informally explore foundations for GADTs within Scala's core type system, to guide a principled understanding and implementation of GADTs in Scala.

Official source

https://infoscience.epfl.ch/entities/publication/c6869154-fe0e-4f6b-8186-1bab5dc2a924

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki, Paolo Giosuè Giarrusso
2019
Conference Papers

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/c6869154-fe0e-4f6b-8186-1bab5dc2a924

About this result

Related concepts (18)

Generalized algebraic data type

In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric algebraic data types. In a GADT, the product constructors (called data constructors in Haskell) can provide an explicit instantiation of the ADT as the type instantiation of their return value. This allows defining functions with a more advanced type behaviour.

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

Idris (programming language)

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages.

Related publications (20)

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain ...

Assoc Computing Machinery2024

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Assoc Computing Machinery2022