Skip to content
A functional language with lifetimes and uniqueness types for efficiency and gc-less memory safety.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
app
src
syntax
test
LICENSE
README.md
Setup.hs
outline.md
package.yaml
stack.yaml

README.md

Redox

Functional language.

  • Compiles to C
  • Fancy types for efficiency

Why?

Imperative algorithms can be tedious to get right. e.g. reversing an array:

void reverse(int n, int *a) {
  // n / 2 is OK because if n is...
  //   ...even: there's no 'leftover' middle element, so all items get swapped
  //   ...odd: the leftover element is dead center, so no swap necessary
  for (int i = 0; i < n / 2; ++i) {
    int tmp = a[i]; // remember to store a temporary copy
    a[i] = a[n - 1 - i]; // n - 1, not n
    a[n - 1 - i] = tmp;
  }
  // you have to prove all the above to yourself, in your head (or discover
  // them by running tests), to be confident you got it right
}

I want to be able to write

rec reverse : forall n a. [a; n] -> [a; n] = fun l ->
  match l
  | [] -> [] (* n was even *)
  | [x] -> [x] (* n was odd *)
  | [x, ..mid, y] -> [y, ..reverse mid, x]
  (* no juggling of indices or temporaries, and pattern analysis forces you
     to consider the cases where n was even or odd *)

Uniqueness types can make this efficient: if we require l to be a unique pointer, then reverse can do whatever it likes to it. In particular, it can mutate l in place instead of deallocating l on scope exit and allocating a whole new array for its result. Ideally, I want to compile the above (for a ~ int) to

void reverse2(int n, int *a) {
  int tmp;
  switch (n) {
    case 0: break;
    case 1: break;
    default:
      tmp = a[0];
      a[0] = a[n - 1];
      a[n - 1] = tmp;
      reverse(n - 2, a + 1);
  }
}

Outline / progress

You can’t perform that action at this time.