Skip to content

Instantly share code, notes, and snippets.

@brendanzab
Last active July 4, 2021 06:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save brendanzab/dd2425ac078aaa8f44d811d6343b71be to your computer and use it in GitHub Desktop.
Save brendanzab/dd2425ac078aaa8f44d811d6343b71be to your computer and use it in GitHub Desktop.
Weird binder language

Weird binder language thingy

Playing around with a uniform notation for binders (eg. Π, Σ, λ, let). This is probably not the greatest language to program in directly, but I think it's fun to see if a more consistent syntax can help to expose some of the differences between dependent functions, dependent pairs, and let expressions...

Syntax

Binders

binder syntax* body occurrence**
function type (Assume | Param) name : type name
function literal (assume | param) name name
pair type (Have | Field) name : type name
pair type (manifest)*** (Have | Field) name : type := term envterm
pair literal (have | field) name := term envterm
let expression let name : type := term envterm

* I've supplied more 'proof'-style keywords (eg. assume) and more 'programming'-style keywords (eg. param). I'm not sure which I like better though!
** the value to be used for the variable occurrences during type checking or equivalence checking
*** unsure how to add manifest fields without relying on UIP (uniqueness of identity proofs - coercions maybe?)

Eliminations

A period (ie. .) is used to replace or alter literals, allowing for substitutions or projections, to be applied to terms.

Grammar

term, type ::=
  name
  binder ; term
  term . elim
  Type

binder ::=
  (Assume | Param) name : type
  (assume | param) name
  (Have | Field) name : type
  (Have | Field) name : type := term
  (have | field) name := term
  let name : type := term

elim ::=
  ( (name := term);+ )
  name

Example

Signature:

Field id : (Param A : Type; Param a : A; A);

Param Unit : Type;
Param unit : Unit;

Field Monoid : Type := (
    Field A : Type;
    Field empty : A;
    Field append : (Param a1 : A; Param a2 A; A);
    Unit
);

Field unit-monoid : Monoid;

Unit

Structure:

field id := (
    param A : Type;
    param a : A;
    a
);

param Unit;
param unit;

field Monoid := (
    Field A : Type;
    Field empty : A;
    Field append : (Param a1 : A; Param a2 A; A);
    Unit
);

field unit-monoid := (
    field A := unit;
    field empty := unit;
    field append := (param a1; param a2; empty);
    unit
);

let test-unit-id : Unit :=
    id.(A := Unit; a := unit);

let test-unit-monoid : Unit :=
    unit-monoid.append.(
        a1 := unit-monoid.empty;
        a2 := unit-monoid.empty
    );

let test-unit-monoid-app := Monoid.(A := Unit) := 
    unit-monoid;

unit

Previous experiments

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment