aith.scroll

import ../code/conceptPage.scroll

id aith
name Aith
appeared 2020
creators Superstar64
tags pl
website https://github.com/Superstar64/aith
conceptDescription Aith is a perfomant systems programming language with am empathises on type systems. As of now Aith is very early stages and very little is implemented.

writtenIn haskell tex make markdown python xml
repoStats
 firstCommit 2020
 commits 369
 committers 1
 files 53
 newestCommit 2024
country Unknown
originCommunity https://github.com/Superstar64/aith

example
 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)
     };
 };

keywords 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
githubRepo https://github.com/Superstar64/aith
 stars 41
 forks 0
 subscribers 5
 created 2020
 updated 2022
 description [Early Stages] Low level functional programming language with linear types, first class inline functions, levity polymorphism and regions.