weird-field-param-language.md

Weird field/param language

Further messing around on top of some ideas in the previous gist.

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

Grammar

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

former ::=
  param name : type
  field name : type
  field name : type := term

intro ::=
  param name
  field name := term

elim ::=
  param name := term
  field name

Example

{field id : {param A : Type} {param a : A} A}

{field const :
    {param A : Type}
    {param B : Type}
    {param a : A}
    {param b : B}
    A
}

{field compose :
    {param A : Type}
    {param B : Type}
    {param C : Type}
    {param a-b : {param a : A} B}
    {param b-c : {param b : A} C}
    {param a : A} 
    C
}

{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] [param a] a
]

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

[field compose :=
    [param A] [param B] [param C]
    [param a-b] [param b-c]
    [param a] b-c (param b := a-b (param 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
    (param A := Unit)
    (param a := unit);

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

unit