All notable changes to this project will be documented in this file.
0.3.6-RC1 - 2019-12-28
- Upgrade Dotty to
0.21.0-RC1
0.3.5-RC1 - 2019-11-03
- Upgrade Dotty to
0.20.0-RC1
eec-core
prototype for developing a core language
0.3.3-RC1 - 2019-08-13
- Upgrade Dotty to
0.17.0-RC1
0.3.2-RC1 - 2019-07-24
- Upgrade Dotty to
0.16.0-RC3
0.3.1-RC3 - 2019-05-7
- EEC is renamed to Mesa
0.3.0-RC1 - 2019-05-7
- A Prelude library, containing data definitions for encodings of sums and
linear coproducts in EEC+, and operators for recursion and handling of
Void#
. - Pretty printing for types with a canonical representation of universally
quantified types, e.g.
forall a b c. (a -> b -> c) -> (a, b) -> c
, from an infinite ordered stream matching/[a-z] | [a-z][1-9]/
. - Lambda terms at the top level in the REPL now type as polymorphic.
- Allow data types to be isomorphic to
()
.
- Update the representation of data types for printing in the REPL, in preparation for a standard API.
- Update the syntax for the linear arrow to
->.
, matching LinearTypes for GHC, and allowing all arrows to have the same right associative precedence. - General bug fixes in the type checker for unification of polymorphic types.
0.2.3-RC1 - 2019-04-9
- Allow the use of patterns inside both
let
term forms, with the same semantics as a singular case clause.
0.2.3-RC1 - 2019-04-9
- Allow the use of patterns inside both
let
term forms, with the same semantics as a singular case clause.
- Update eec/Isomorphisms.hs with more idiomatic terms using the new syntax.
0.2.2-RC1 - 2019-04-5
- Changed linear evaluation from a root expression to a simple expression.
- Changed linear case expressions to differ from regular case expressions only by the arrow.
- Changed linear lambda expressions to differ from regular lambda expressions only by the arrow.
- Updated tests and example files to new syntax.
0.2.1-RC1 - 2019-04-4
- Separation of scopes for data definitions and normal terms, leading to more
flexibility in defining terms. Also prevents shadowing of imported data types,
such as the bootstrapped types in the
_root_
package.
0.2.0-RC1 - 2019-04-4
- Type checking that ensures all possible cases in a match expression or linear match expression are provided.
data
definitions have been added that allow the user to define non-recursive sum types that may be used in match expressions and linear match expressions.DataTypes.hs
demo file added.
- Updated eec/Isomorphisms.hs with new data definitions,
replacing
Either A B
forL |: R
, a new data type, and providing an implementation of+:
.
Either
and+:
have been removed from the compiler's bootstrapped types. The user may now define these data types themselves and enjoy the same semantics.
0.1.2-RC1 - 2019-04-1
- Stricter semantics for type checking of linear lambdas, variables,
constants and
!
terms in linear contexts. - Addition of
?
a.k.a "why not", to summonA
fromVoid
in linear contexts.
- Updated links on README.md
- Now using minor version numbering.
- Update eec/Isomorphisms.hs after addition of
?
.
0.1-RC1 - 2019-03-31
-
Read Eval Print Loop
- Define
EEC+
terms and typecheck them. - Print the parsed AST for
EEC+
terms and source files. - Print the derived types of
EEC+
terms and source files. - Print the current environment of terms and types.
- Define
-
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 eec/Isomorphisms.hs.
-
Haskell-like syntax
- Source files use
.hs
suffix at present to benefit from syntax highlighting. - Refer to eec/src/main/antlr4/EEC.g4 for a context free grammar.
- Source files use