weird-field-param-language-2.md

Weird field/param language 2

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

This is a more succinct syntax than the previous gist, this time using in and out in place of param and record, and making introductions and eliminations more succinct.

Grammar

term, type ::=
  name
  let term : type := term ; term
  { former } term
  [ intro ] term
  term ( elim )
  Type

former ::=
  in name : type
  out name : type (:= term)?

intro ::=
  name
  name := term

elim ::=
  name := term
  name

Example

{out id : {in A : Type} {in a : A} A}

{out const :
    {in A : Type}
    {in B : Type}
    {in a : A}
    {in b : B}
    A
}

{out compose :
    {in A : Type} {in B : Type} {in C : Type}
    {in a-b : {in a : A} B} 
    {in b-c : {in b : A} C}
    {in a : A} C
}

{in Unit : Type}
{in unit : Unit}

{out Monoid : Type :=
    {out A : Type}
    {out empty : A}
    {out append : {in a1 : A} {in a2 : A} A}
    Unit
}

{out unit-monoid : Monoid}

Unit

Structure:

[id := [A] [a] a]

[const := [A] [B] [a] [b] a]

[compose :=
    [A] [B] [C] [a-b] [b-c]
    [a] b-c (b := a-b (a := a))
}

[Unit]
[unit]

[Monoid :=
    {out A : Type}
    {out empty : A}
    {out append : {in a1 : A} {in a2 : A} A}
    Unit
]

[unit-monoid :=
    [A := unit]
    [empty := unit]
    [append := [a1] [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));

unit