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...
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 |
env ⟦term⟧ |
pair literal | (have | field ) name := term |
env ⟦term⟧ |
let expression | let name : type := term |
env ⟦term⟧ |
* 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?)
A period (ie. .
) is used to replace or alter literals, allowing for substitutions
or projections, to be applied to terms.
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
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
- https://gist.github.com/brendanzab/d18d8054976efa867ac3a805f7a0e7c4
- https://gist.github.com/brendanzab/764f6470ca8eccc8e0da8d8695b72790
- https://gist.github.com/brendanzab/d8303f5e20a5d43b763d86e6a6b0c453
- https://gist.github.com/brendanzab/63c2d42c41c95922c0ee98e6e7a10cbb
- https://gist.github.com/brendanzab/3ba57463d96c7be06b4a2e2b72b19a3c
- https://gist.github.com/brendanzab/1409b0da579f2213751523fbb01069a5