Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A type system for data flow and alias analysis in ReScript

Nicky Ask Lund, Hans Hüttel

TL;DR

The paper develops a $\lambda$-calculus-based local data-flow analysis for a subset of ReScript, focusing on bindings and aliasing in a language with mutability and pattern matching. It introduces labelled expressions, a binding store model, and a dependency function to collect data-flow and alias information at program points, supported by a big-step collection semantics. Types are built from base types $(\delta,\kappa)$ and function types, together with an alias basis $\kappa^0$ and an approximated program-point order $\Pi$, enabling a sound abstraction of dependencies and aliasing. Soundness is established via environment/dependency agreements and supporting lemmas (History, Strengthening), showing that type judgments correctly approximate the operational semantics. The work outlines practical extensions, including a type checker, polymorphism, richer reference handling, type inference, and broader language constructs to enhance applicability.

Abstract

ReScript introduces a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a type system for data-flow analysis for a subset of the ReScript language, more specific for a lambda-calculus with mutability and pattern matching. The type system is a local analysis that collects information about what variables are used and alias information.

A type system for data flow and alias analysis in ReScript

TL;DR

The paper develops a -calculus-based local data-flow analysis for a subset of ReScript, focusing on bindings and aliasing in a language with mutability and pattern matching. It introduces labelled expressions, a binding store model, and a dependency function to collect data-flow and alias information at program points, supported by a big-step collection semantics. Types are built from base types and function types, together with an alias basis and an approximated program-point order , enabling a sound abstraction of dependencies and aliasing. Soundness is established via environment/dependency agreements and supporting lemmas (History, Strengthening), showing that type judgments correctly approximate the operational semantics. The work outlines practical extensions, including a type checker, polymorphism, richer reference handling, type inference, and broader language constructs to enhance applicability.

Abstract

ReScript introduces a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a type system for data-flow analysis for a subset of the ReScript language, more specific for a lambda-calculus with mutability and pattern matching. The type system is a local analysis that collects information about what variables are used and alias information.
Paper Structure (47 sections, 15 theorems, 60 equations, 9 figures)

This paper contains 47 sections, 15 theorems, 60 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Language
  3. Syntax
  4. Environments and stores
  5. Dependencies
  6. Collection semantics
  7. Type system for data-flow analysis
  8. Types
  9. Basis and type environment
  10. The type system
  11. Soundness
  12. Type rules for values
  13. Agreement
  14. Properties
  15. Conclusion
  16. ...and 32 more sections

Key Result

lemma 1

Suppose $e^p$ is an occurrence, that and $x^{p_1}\in dom(w')\backslash dom(w)$. Then $x\notin fv(e^{p})$

Figures (9)

  • Figure 1: Abstract syntax
  • Figure 2: Selected rules from the semantics
  • Figure 3: Selected rules from the type system
  • Figure 4: Abstraction type example
  • Figure 5: Reference type example
  • ...and 4 more figures

Theorems & Definitions (67)

  • Example 2.1
  • Definition 2.1: Free variables
  • Definition 2.2
  • Definition 2.3: Update of environments
  • Definition 2.4: inverse env
  • Definition 2.5
  • Definition 2.6: Update of stores
  • Definition 2.7: Dependency function
  • Definition 2.8: Update of dependency functions
  • Example 2.2
  • ...and 57 more