Untyped record calculus

untyped_record_calculus.c

// Record type
{}: `{}

// construction
{x = {}}: `{x: `{}}

// destruction
{x: `{}} = {x = {}}

// abstraction
f : `{x} | `{y} | `{a, b} -> `{}
= {
  {x} -> {}, 
  {y} -> {}, 
  {a, b} -> {}
}

// application
{{x} -> {}} {x}

// type alias
natural = 
  | `{zero: `{}}
  | `{successor: `{}, of: natural}

add = {
  {x, y = {zero = {}}} -> 
    x,

  {x, y = {successor = {}, of}} -> 
    {successor = {}, of = add {x, of}}
}

0 = {zero = {}}
1 = {successor = {}, of = {zero = {}}}
2 = {successor = {}, of = {successor = {}, zero ={}}}

shape = 
  | `{circle: `{}, radius: natural}
  | `{square: `{}, side: natural}
  | `{rectangle: `{}, height: natural, width: natural}

area
  : shape -> natural
  = {
    {circle, radius} -> 
      multiple {value = pi, by = square radius},

    {square} -> 
      natural square,

    {rectangle, height, width} -> 
      multiple {value = height, by = width}
  }

list = {
  {element: type} -> 
    | {nil: `{}}
    | {cons: `{}, current: element, next: list{element}}
}

length
  : {u: type} -> list {element= u} -> natural
  = {
    {nil = {}} -> zero,
    {cons = {}, next} -> add {value = length {u} next, by = 1}
  }

map
  : {from: type, to: type} 
    -> `{function: from -> to, over: list{element = a}} : `{function: type, over: type}
    -> list{element = b}: type
  = {
    {over = {nil = {}}} -> {
      nil = {}
    },

    {function, over = {cons = {}, current, next}} -> {
      cons = {}, 
      current = function current, 
      next = map {from, to} {function, over = next}
    }
  }