Aith is a programming language created in 2020 by Superstar64.
git clone https://github.com/Superstar64/aith| #1594on PLDB | 4Years Old |
[Early Stages] Low level functional programming language with linear types, first class inline functions, levity polymorphism and regions.
module ::
inline runtimeCall = \f => \x => f (x);
module combinators = {
inline flip = \f => \x => \y => f !y !x;
inline compose = \f => \g => \x => f !(g !x);
inline readerPure = \x => \r => x;
inline readerBind = \m => \f => \r => f !(m !r) !r;
inline readerMap = \f => \m => readerBind !m !(compose !readerPure !f);
};
module systemf = {
inline ignored <B : type> : <A : type> B -> B;
inline ignored <B : type> = <A : type> \(x : B) => x;
inline idSysF = <A : type> \x : A => x;
inline runIdSysF = \f {
|< f : <A : type> A -> A >|
};
inline id = runIdSysF !idSysF;
type natural = <A : type> A -> (A -> A) -> A;
inline zero<> : natural;
inline zero = <A : type> \z : A => \inc : A -> A => z;
inline inc<> : natural -> natural;
inline inc = \n => <A : type> \z : A => \inc : A -> A => inc !(|< n : natural >| !z !inc);
inline one<> : natural;
inline one = inc !zero;
inline two<> : natural;
inline two = inc !one;
};
module varSub = {
inline sub<R : pretype<pointer, unrestricted>, A : region, B : region >= A, C:type>
: R in A -> R in B -> C -[linear]> C;
inline sub = \a => \b => \x => x;
inline cycle = \a => \b => \c {
sub !a !b !(
sub !b !c !(
sub !c !a !(
\x => x
)
)
)
};
};
module default = {
add = function(x,y) {
x + y
};
ambigous = function(x) {
inline y = 1;
x
};
};
module unit = {
idUnit = function () {
()
};
};
module boolean = {
inline yes = true;
branch = function(b) {
if b {
1
} else {
2
}
};
complex = function(b) {
if (if (b) { true } else {false} ) {
1
} else {
if yes {
2
} else {
4
}
}
};
not = function(b) {
!b
};
inBounds = function(x1, x2, x3) {
x1 <= x2 & x2 < x3
};
};
module pair = {
fst = function(x, y) => x;
snd = function(x, y) => y;
pattern = function (pair) {
(fst(pair), snd(pair))
};
};
module ptr = {
derefTriple = function(x) {
***x
};
deref <RA : region, RB : region >= RA, T : pretype<pointer, unrestricted>> : function (T* @ RA) => T uses RB;
deref <RA : region, RB : region >= RA, T : pretype<pointer, unrestricted>> = function (x) {
*x
};
write<A:region, B:region >= A> : function(int* @ A) => () uses B;
write<A:region, B:region >= A> = function(x :: int* @ A) {
*x = (1 :: int)
};
writeTriple = function(x) {
***x = 1
};
swap = function(x,y) {
let xp = *x;
*x = (*y);
*y = xp;
()
};
};
module number = {
type point = (int, int, int);
dotProduct <R : region> : function(point, point) => int uses R;
dotProduct = function((x1,y1,z1), (x2, y2, z2)) {
(x1 * x2 + y1 * y2 + z1 * z2)
};
mid <R : region> : function(uint, uint) => uint uses R;
mid <R : region> = function(x,y) {
(x + y) / 2
};
inline divGen = function(x,y) {
(x + y - 1) / y
};
div = divGen;
lessEqual = function(x,y) {
x <= y
};
factorial<R : region> : function(ulong) => ulong uses R;
factorial<R : region> = function(x) {
if (x == 0) {
1
} else {
x * factorial (x - 1)
}
};
};
module fptr = {
call = function(f) {
f (1)
};
callUnit <R : region> : function(function*(uint) => () uses R) => () uses R;
callUnit <R : region> = function(f) {
f (2)
};
};
module recurse = {
explode<L : multiplicity, R:region, A:pretype<pointer, L>> : function() => A uses R;
explode<L : multiplicity, R:region, A:pretype<pointer, L>> = function() {
explode ()
};
};
module world = {
inline putchar<A:region> : function*(int) => int uses io in A;
inline putchar<A:region> = extern "putchar";
putPtr<A:region >= io> : function(int* @ A) => int uses A;
putPtr = function(ptr) {
putchar (*ptr)
};
};
module arrays = {
inline get = \x => \i {
* &* &x[i]
};
inline set = \x => \i => \a {
* &* &x[i] = a
};
swap = function(a, b, i) {
let tmp = get !a !i;
set !a !i !(get !b !i);
set !b !i !tmp;
()
};
memcpyPtr = function(dst, src, i) {
loop (let (dst, src, i) = (dst, src, i)) {
if(i != 0) {
* &* dst = (* &* src);
continue (&dst[1], &src[1], i - 1)
} else {
break ()
}
}
};
};
module sort = {
inline get = /arrays/get;
inline set = /arrays/set;
insert<R : region> : function(int[] @ R, unsigned integer(native)) => () uses R;
insert<R : region> = function(array, index) {
loop (let (array, index) = (array,index)) {
if (index > 0 & get !array !index < get !array !(index - 1) ) {
let tmp = get !array !index;
set !array !index !(get !array !(index - 1));
set !array !(index - 1) !tmp;
continue (array, index - 1)
} else {
break ()
}
}
};
sort <R : region> : function(int[] @ R, unsigned integer(native)) => () uses R;
sort <R : region> = function(array, length) {
if (length > 1) {
sort(array, length - 1);
insert(array, length - 1)
} else {
()
}
};
};
module borrowed = {
increment <R : region> : function(unique int*) => unique int* uses R;
increment <R : region> = function(p :: unique int*) {
let ((), p) = borrow p as <A : region >= R>(x :: int* @ A) {
*x = (*x + 1)
};
p
};
};
module partial = {
inline auto = \x => x;
inline semi<A : type> = \x : A => x;
inline scoped<A : type> : A -> A;
inline scoped = \x : A => x;
inline manual<A : type> : A -> A;
inline manual<A : type> = \x => x;
};
module import = {
inline id = \x => x;
module b = {
inline const = \y => /import/id;
};
};
module levity = {
idPolyPair<A : pretype<struct(pointer, 32bit word) ,linear>> = function(x :: A) {
x
};
idPolyUnion<A : pretype<union(pointer, 32bit word) ,linear>> = function(x :: A) {
x
};
useId = function(ptr) {
idPolyPair(ptr, 0)
};
};
module sum = {
triangular = function(start, end) {
loop (let (i, total) = (start, 0)) {
if (i <= end) {
continue (i + 1, total + i)
} else {
break (total)
}
}
};
};
module newtype = {
wrapper num : pretype<32bit word, unrestricted>;
wrapper num = int;
makeNum = function() {
wrap 1 :: num
};
wrapper linked : pretype<pointer, unrestricted>;
wrapper linked = linked2* @ io;
type linked2 = linked;
read = function (x) {
*unwrap (x :: linked)
};
};as bool borrow boxed break byte capacity continue copy else existence extern false function if in inline int integer invariant io kind let linear long loop module multiarg multiplicity native opaque pointer pretype region representation short signed signedness size step struct subtypable transparent true type ubyte uint ulong union unique unrestricted unsigned unwrap used uses ushort word wrap wrapper