Semantic Subtyping for Maps in Erlang

TL;DR

This paper develops a set-theoretic semantic model for map types in Erlang, introducing a novel subtyping relation for parameterized map types based on set containment.

Contribution

It presents the first semantic subtyping framework for parameterized map types in Erlang, expanding type theory in functional programming languages.

Findings

Defined a set-theoretic model of Erlang map types

Established a semantic subtyping relation based on set containment

Enabled reasoning about subtype relations in Erlang maps

Abstract

In this paper we will construct a set-theoretic model of types featuring type variables, base types, set-theoretic types and map types. Syntax of map types spans all the map types available in Erlang. The model of types is used to define a semantic subtyping relation based on set containment. The novelty of this work is the definition of subtyping over parameteric map types.