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

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.

Comments

  • Enclosed in "quotes" and may span across lines
  • Are attached to the following expression, type or pattern
  • Can be used to give informal names to blocks of code "Boolean and" λBool (\Bool ...)

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