Skip to content

Instantly share code, notes, and snippets.

@wongjiahau
Created January 10, 2020 02:00
Show Gist options
  • Save wongjiahau/28ed3c7151c136643eedc1b4d9ee3e13 to your computer and use it in GitHub Desktop.
Save wongjiahau/28ed3c7151c136643eedc1b4d9ee3e13 to your computer and use it in GitHub Desktop.
Untyped record calculus
// 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}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment