Mesa

Current Release

0.3.6-SNAPSHOT

About

This repository is for implementing a programming language based on the enriched effect calculus by Egger, Ejlers and Simpson (2014).

Changes

• Refer to CHANGELOG.md

Features

• Read Eval Print Loop

  • Define Mesa terms and type-check them.
  • Print the meta AST for Mesa terms and source files.
  • Print the derived types of Mesa terms and source files.
  • Print the current environment of terms and types.

• Linear types that enforce the linear usage of effects.

  • Proof of isomorphisms in Proposition 4.1. of Egger, Ejlers and Simpson (2014) can be found in mesa/Isomorphisms.hs.

• Haskell-like syntax

  • Source files use .hs suffix at present to benefit from syntax highlighting.
  • Refer to mesa/src/main/antlr4/Mesa.g4 for a context free grammar.

Author

• James Thompson, BSc. University of Bath.

Usage

• Load sbt with sbt
• To run tests, in the sbt CLI use test.
• To launch the EEC REPL, in the sbt CLI use run -e.

REPL

• :help to get a list of commands available.
• :tf to type check a file in the current directory, e.g. mesa/Isomorphisms.hs; adding any definitions to the environment.
• :ctx to print the current environment after defining terms.
• :reset to clear all definitions in the environment.
• :def to define a new top level definition.
• :t to type an expression.
• :ast to print the AST of an expression.
• :astt to print the AST of a top level definition.
• :astf to print the AST of a source file in the current directory.
• :cd to change the working directory
• :pwd to print the working directory
• :q to quit the REPL.

References

• Egger, J., Ejlers, R. and Simpson, A., 2014. The enriched effect calculus: syntax and semantics. Journal of Logic and Computation, 24(3), pp.615-654.