A simple implementation of a call-by-value
language with explicit parametric polymorphism
Author: Frank Pfenning,
Aug 2020 (v0.1)
Oct 5, 2020 (v0.3)
Oct 12, 2020 (v0.4)
Sep 29, 2021 (v0.8)
  - added conv e1 = e2 to cbv language
Oct 1, 2021 (v0.9)
  - allowed redundant branches when --subtyping=true
Oct 25, 2021 (v1.0)
  - default is now no subtyping to get errors for incorrect code
  - redundant or extraneous patterns only give warning with --subtyping=true
Nov 5, 2021 (v1.1)
  - added .prf extension for (hopefully sound) proof checking

If binary is available (on linux.andrew.cmu.edu, at ~fp/bin)

$ $bindir/lambda examples/comb.lam

To build (requires mlton, see mlton.org)

$ cd src
$ make lambda
$ ./lambda ../examples/comb.lam

See examples/*.{lam,poly,cbv} for some simple examples 

To see options, invoke

$ ./lambda -h

All options can be given on the command line or at the
beginning of the file.  For example,

$ ./lambda --abort=warning <file>.cbv

or in <file>.cbv

#options --abort=warning

Tokens
======

<whitespace> ::= ' ' | \n | \t | \r | \v | \f

<alpha> ::= [a-zA-Z]
<decor> ::= [_']
<digit> ::= [0-9]
<id>    ::= (<alpha> | '_') (<alpha> | <decor> | <digit>)*
<tag>   ::= '<id>       [cbv0]
<nat>   ::= <digit>*

Comments
========

single line:        % ... \n
nested delimited:   (* ... *)

Expressions and declarations
============================

Types (in order of precedence)
tau1 tau2         left associative (prec. 4)
*                 right associative (prec. 3)
+                 right associative (prec. 2)
->                right associative (prec. 1)
!a. ?a. $a. 'i    weak prefixes, binding a (max scope) (prec. 0)

Terms (in order of precedence)
e1 e2   e [tau]              left associative, strongest precedence
fold unfold 'i \x. $x. fst snd  prefix
, ;                          right associative, weakest precedence

Tagged and untagged sums and products [cbv3]
  sum('i:tau_i) + sum('j:tau_i) is flattened to sum('k:tau_k)
  otherwise tau + sigma is parsed into ('l:tau) + ('r:sigma)

  prod('i:tau_i) & sum('j:tau_k) is flattened to prod('k:tau_k)
  otherwise tau & sigma is parsed into ('l:tau) & ('r:sigma)

  () stands for empty tagged sum or product sum() or prod()

Type functions and applications can be used only for type definitions
  type d = \a1. ... \an. tau (defines d : type -> ... -> type)
  d tau1 ... taun            (is a type)

<tp> ::= '!' <id> '.' <tp>   % !a. tau
      |  <tp> '->' <tp>      % tau1 -> tau2
      |  <tp> '*' <tp>       % tau1 * tau2 [cbv0]
      |  '1'                 % 1           [cbv0]
      |  <tp> '+' <tp>       % tau1 + tau2 [cbv0]
      |  '0'                 % 0           [cbv0]
      |  <tag> : <tp>        % 'i : tau    [cbv1]
      |  <tp> '&' <tp>       % tau1 & tau2 [cbv3]
      |  '(' ')'             % ()          [cbv3]
      |  '$' <id> '.' <tp>   % $a. tau     [cbv0]
      |  '?' <id> '.' <tp>   % ?a. tau     [cbv2]
      |  '\' <id> '.' <tp>   % \a. tau     [cbv4]
      |  <tp> <tp>           % tau1 tau2   [cbv4]
      |  '(' <tp> ')'        % (tau)
      |  <id>                % a

<exp> ::= <id>                            % x            (variable)
       |  '\' <id> [':' <tp> ] '.' <exp>  % \x. e        (lambda abstraction)
       |  <exp> <exp>                     % e1 e2        (application)
       |  '(' <exp> ')'                   % (e)          (scoping)
       |  '/\' <id> '.' <exp>             % /\a. e       (type abstraction)
       |  <exp> '[' <tp> ']'              % e [tau]      (type application)
       |  <exp> ',' <exp>                 % (e1,e2)      (pair)     [cbv0]
       |  '(' ')'                         % ()           (unit)     [cbv0]
       |  <tag> <exp>                     % 'i e         (tag)      [cbv0/1]
       |  '(|' <record> '|)'              % (| r |)      (record)   [cbv3]
       |  <exp> '.' <tag>                 % e.'i         (projection)    [cbv3]
       |  'case' <exp> 'of' '(' [ <brs> ] ')'  % case e of (brs) (case)  [cbv0]
       |  'fold' <exp>                    % fold e       (fold)     [cbv0]
       |  'unfold' <exp>                  % unfold e     (unfold)   [cbv0]
       |  '[' <tp> ']' ',' <exp>          % ([tau], e)   (pack)     [cbv2]
       |  '$' <id> [ ':' <tp> ] '.' <exp> % $x. e        (fix)      [cbv0]

<brs> ::= <pat> '=>' <exp> [ '|' <brs> ]  % p1 => e1 | ...  [cbv0]

<record> ::= <tag> '=>' <exp> [ '|' <record> ] % 'i1 => e1 | ... [cbv3]

<pat> ::= <id>                            % x            (variable)    [cbv1]
       |  <pat> ',' <pat>                 % (p1,p2)      (pair)        [cbv1]
       |  '(' ')'                         % ()           (unit)        [cbv1]
       |  <tag> <pat>                     % 'i p         (injection)   [cbv1]
       |  'fold' <pat>                    % fold p       (fold)        [cbv1]
       |  '[' <id> ']' ',' <pat>          % ([a],p)      (pack)        [cbv2]
       |  '(' <pat> ')'

<dec> ::= 'type' <id> '=' <tp>             % type a = tau 
       |  'decl' <id> ':' <tp>             % decl x : tau 
       |  'defn' <id> '=' <exp>            % defn x = e
       |  'norm' [ <nat> ] <id> '=' <exp>  % norm x = e  -->  defn x = norm(e)
       |  'conv' <exp> '=' <exp>           % conv e1 = e2     verify norm(e1) = norm(e2)
       |  'fail' <dec>                     % fail <dec>       succeeds if <dec> fails
       |  'eval' [ <nat> ] <id> '=' <exp>  % eval x = e  -->  defn x = eval(e)  [cbv0]

<pragma> ::= '#' ... \n            % for regression testing

<prog> ::= <pragma>* <dec>*

Statics for --lang=prf
======================

Recursion at the level of types or expressions is disallowed,
as are nonexhaustive or redundant pattern matches.  Also, this option
is incompatible with --subtyping=true

Statics for --lang=cbv
======================

See rule sheet for Lecture 20 at
http://www.cs.cmu.edu/~fp/courses/15814-f20/lectures/20-negatives-rules.pdf

Cases in the grammar above new for [cbv] are marked as such

Variables in patterns or tags in sums may not be repeated

Patterns in a case expression that are not exhaustive
or redundant generate warnings with --subtyping=true and
errors with --subtyping=false.  With --abort=warning (either
on the command line or at the beginning of a .cbv file with
#options --abort=warning) warnings will turn into an error.

The bidirectional typechecker uses subtyping, unless
disabled with --subtyping=false.

conv e1 = e2  requires Sigma ; . |- e1 => tau
                   and Sigma ; . |- e2 => tau
and checks that if e1 |->* v1 and e2 |->* v2 then v1 = v2
where v1 and v2 may not contain values of negative type,
that is, \x.e, /\a.e, or (| r |)

Statics for --lang=poly
=======================
Signature Sigma refers to all preceding successful declarations and definitions
redefinition is not allowed

Sigma ::= . | Sigma, a = tau | Sigma, x : tau

type a = tau  requires Sigma ; . |- tau type
decl x : tau  requires Sigma ; . |- tau type
defn x = e    requires Sigma ; . |- x : tau and Sigma ; . |- e <= tau
                    or Sigma ; . |- e => tau for some tau
norm x = e    requires Sigma ; . |- x : tau and Sigma ; . |- e <= tau
                    or Sigma ; . |- e => tau for some tau

conv e1 = e2  requires Sigma ; . |- e1 => tau
                   and Sigma ; . |- e2 => tau
              for some tau

Statics for --lang=lam
======================
Vars refers to all preceding successfully defined variables
redefinition is not allowed

Vars ::= . | Vars, x     (x <> '_', all x distinct)

type a = tau  disallowed
decl x : tau  disallowed

defn x = e    requires Vars ; . |- e closed  (unless x = '_')
norm x = e    requires Vars ; . |- e closed  (unless x = '_')
conv e1 = e2