PL Repl
For an overview of what this project is, see the project README
TL;DR: The REPL embedded below allows parsing, type-checking and
reducing a typed lambda calculus with Sums, Products, Unions, anonymous
Recursive Types and Functions at both the Expression and Type level.
Variables are referenced by how far away they were bound (rather than names)
and while there are built in Named types (Nat, Bool, Maybe, etc) users
cannot currently assign names. Anonymous types can be used to define
compatible recursive types.
Expressions and types can be referred to by unambiguous hashes of their content.
Typing is structural and so expressions of a named/ recursive type can be constructed from the constituent Products, Sums, etc.
Consult the Syntax reference for elaboration of the syntax of expressions, types and patterns
- Expressions:
Lambdas,
Variable Bindings,
Products,
Function Application,
Sums,
Unions,
Big Lambdas,
Big Application
- Types:
Named,
Type Variable Bindings,
Arrows,
Sums,
Products,
Unions,
Type Lambdas,
Type Application,
Big Arrows
- Case analysis and Patterns:
Bind,
Sums,
Products,
Unions
To interpret the type context, consult the documentation for Named Types
To see some examples, mash the Random expression
button
Cheatsheet
Naming
Content Addressed
- Expressions and Types can be referenced by the hash of their contents like
#sha512/LONGHASH
- Shorter hashes can be used when unambiguous, like
#LO
- Content Addresses are returned when expressions are successfully entered
Type Names
- Types can be named with an uppercase first character like
Bool
- Names are currently built in - you cannot assign them. Sorry.
- See the Type Context for Name definitions written after the
=
in type syntax
- Names are structural - conforming expressions are compatible with a type name automatically
Bindings
- Bindings are numbers which count the number of abstractions away something was bound
- Expressions are referenced with numbers like
0
,1
etc rather than variable names x
,y
etc.
- Types are referenced like expressions but with a preceeding
?
like ?0
, ?1
rather than type variables like T
,A
etc.
Data Types
Products
- Combine multiple expressions into one - like n-tuples
- Expression:
* EXPR EXPR
- Typed:
* TYPE TYPE
- Pattern:
* PATTERN PATTERN
(*)
is the empty product. Singleton products are allowed.
Sums
- Combine expressions into ordered alternatives - like tagged enums/ the either type
- Indexed numerically by their (left-to-right) position in the sum
- Duplicate types permitted
- Expression:
+ INDEX EXPR TYPE...
- Typed:
+ TYPE TYPE
- Pattern:
+ INDEX PATTERN
Unions
- Combine expressions into unordered alternatives with unique types
- Expressions are indexed by their type in the union
- Expression:
U TYPE EXPR TYPE...
- Typed:
U TYPE...
- Pattern:
U TYPE EXPR
Recursive Self-Types
- Wrap a type with an anonymous name like:
μKIND TYPE
- Refer to self with
%
- Construct/ match against the definition to construct/ match the Self-Type
- Nat and List are named examples in the type context
Functions
Abstractions
- Abstractions are unnamed. Bindings will refer to them by distance
- Lambdas are anonymous functions which abstract expression inside each other
- Expression:
λTYPE EXPR
- Typed:
-> TYPE TYPE
- Big Lambdas abstract types inside expressions
- Expression:
ΛKIND EXPR
- Typed:
- Type Lambdas abstract types inside types
- Type:
ΛKIND TYPE
- Kinded:
->KIND KIND
Applications
- Applications supply values to Abstractions
- Lambda application is performed with
@
like: @ EXPR EXPR
- Big application is performed with
#
like: # EXPR TYPE
- Type application is performed with
#
like: # TYPE TYPE
Comments
"quotes"
and may span across lines"Boolean and" λBool (\Bool ...)