Funcords

funcords.js

/*
Funcords is a feature that combine functions and records.

If you think about it, record is actually a dependently typed function, 
where the output type depends on the input type.

For example,

  r = {'x': 1, 'y': 'yo'}
  
 r['x'] has the type of number, while r['y'] has the type of string. 
 Even the syntax of record lookup is very similar to function application, 
 except using square brackets rather than parenthesis.
 
 However, record do not have the ability to abstract.
 For example we cannot create a record that behaves like the identity function, x => x.
 
 In other words, function is actually a record with the ability to abstract, but without dependent type.
 Although generic function is also dependently typed to a certain degree, 
 it is still not as powerful as the dependent type of record, 
 i.e. we cannot create a division function that is safe yet without returning a monad (e.g. Maybe/Result/Either).

Therefore, this Gist tries to demonstrate a new feature named "Funcords", that 
combines the capabilities of both function and records.

The following code assumes that the reader already know the following:
1) JSON
2) Javascript object construction and destructuring

To demonstrate Funcords, we will use a very minimal language that looks like Javascript.
The only expressions in this language are funcords and variable.
The only statement is variable assignment.

At the moment, this language is untyped, but that is not to say that it cannot be typed soundly.
*/

// Empty funcord
// It is a function that cannot be applied
{}

// Funcord construction/abstraction
f = {
  {a: {}}: {b: {}},
  {c: {d}}: {d},
  {x}: {y: x}
}

// Funcord deconstruction/applicationn
f {a: {}} // {b: {}}
f {c: {d: {}}} // {d: {}}
f {c: {d: {z: {}}}} // {d: {z: {}}}
f {x: {}} // {y: {}}
f {x: {a: {}}} // {y: {a: {}}}
f {z: {}} // Error: cannot access `{z: {}}` of `f`

// Example of Peano numbers
add = {
  {value, by: {zero}}: value,
  {value, by: {succ: n}}: {succ: add {value, by: n}}
}

0 = {zero: {}}
add {value: {succ: {succ: 0}}, by: 0} // {succ: {succ: 0}}
add {value: {succ: 0}, by: {succ: 0}} // {succ: {succ: 0}}

// Safe division without returning monad
div = {
  {value, by: {zero}}: {error_cannot_divide_by_zero: {}},
  {value, by: n}: n // Just return `n` for the sake of simplicity
}

div{value: {succ: 0}, by: 0} // {error_cannot_divide_by_zero: {}}
div{value: 0, by: {succ: 0}} // 0


// Example of Linked list
length = {
  {of: {nil}}: 0,
  {of: {cons: {current, next}}}: add{value: length{of: next}, by: {succ: 0}},
}

length{of: {cons: {current: 0, next: {cons: {current: 0, next: {nil: {}}}}}}} // {succ: {succ: 0}}