Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir

Document detail

ID

oai:arXiv.org:2408.14345

Topic

Computer Science - Programming Lan...

Author

Castagna, Giuseppe Duboc, Guillaume

Year

2024

listing date

9/11/2024

Keywords

typing gradual languages

Metrics

Abstract

We define several techniques to extend gradual typing with semantic subtyping, specifically targeting dynamic languages.

Focusing on the Elixir programming language, we provide the theoretical foundations for its type system.

Our approach demonstrates how to achieve type soundness for gradual typing in existing dynamic languages without modifying their compilation, while still maintaining high precision.

This is accomplished through the static detection of "strong functions", which leverage runtime checks inserted by the programmer or performed by the virtual machine, and through a fine-grained type analysis of pattern-matching expressions with guards.

Castagna, Giuseppe,Duboc, Guillaume, 2024, Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir

Document

Open

Source

Articles recommended by ES/IODE AI

Computer Science