Skip to content

[Early Stages] Low level functional programming language with linear types, first class inline functions, levity polymorphism and regions.

License

Notifications You must be signed in to change notification settings

Superstar64/aith

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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. Link to typing rules.

visualization of compiler internals
visualization of type system
pure type system subset

Features

(todo: expand on all of these)

Levity Polymorphic System-F

In languages like in C++ or Rust, generics perform monomorphization. When a generic is used in these languages they will generate code for each instante of type they use.

Rather then do this, Aith uses levity polymorphism, which can be seen as a generalization of Java's type erasure generics. In Aith, a type's kind, which is the type of a type, determines how (and if) it will be represented at runtime.

First Class Inline Functions (staging)

Aith has first class inline functions, a unique (as far as I can tell) take on staging. In Aith, inline functions can take inline functions as argument and return inline functions, all of which is completely erased at runtime.

Inline functions that type check always generate valid code and inline functions are prevented from appearing at runtime though kind checking.

Linear / Unique Types

Aith supports linear types and unique types. These are types that limit how copying of variables. Linear types promise that a variable of a linear type will be used exactly once. Unique types promise that a variable of a unique type will has not been aliased.

Aith has linear types at the inline level with multiplicity in the arrow like Linear Haskell. Aith has necessarily unique types at the runtime level with multiplicity via kinds.

Effectful Regions

Aith has support for effectful regions, similar to Rust's lifetimes. Regions allow programs to reason about borrowing and scoping resources (like memory). Conceptually, an executing program has a stack of regions that it accessing at any given time (think stack frames). If a region is alive, then that region and all it's parent regions are valid.

In Aith, regions are effectful, meaning that all runtime expressions are attached to a region that they live in. These expressions can only access memory in their region or regions proven to be parents of said region.

Type Inference

Aith is built on top of Hindley Milner type inference, similiar to Haskell and OCaml. Hindley Milner is a rather fancy type inference scheme that allows the majority of a program to be without type annotations but still statically typed.

First Class Polymorpism (System-F)

Aith implements first class polymorphism at the meta level. This allows treating generic (inline) functions (or more specifically any generic term) as if they where first class. Generic inline functions can be passed to other inline functions and returned from them. As of now, first class polymorphism is only implmented at the meta level for inline functions and not for runtime functions.

As type inference for first class polymorphism is undeciable, some compromises must be made. Aith implements it's own variant of PolyML, which requires explicit boxing and unboxing and requires annotations for variables who's types are instancited.

Boolean Unification

Aith extends Hindley Milner with boolean unification. This allows certain types to contain boolean expressions (and only boolean expressions). Boolean unification is used by Aith to type check both regions and linear types.

Hindley Milner extended with boolean unification preserves it's nice properties such as principle types. This means that types that use booleans infer as nicely as types that don't. The main trade off is that now type checking now involves what is effectively a generalization of SAT solving.

Building and Running Tests

Install ghc, cabal and make. Run make to build aith, make tests to run the tests and make test.c to generate the test c source file.

Todo List

  • Proper Documentation
  • Algebraic data types
  • Newtypes
  • Add higher kinded types (System-F A)
  • Runtime level higher rank polymorphism
  • Simplify boolean types to DNF rather then ANF
  • Refactoring and syntax changes as usual

Syntax

Files are lists of declarations, where these declarations could be a plain variable declaration or a path declaration. For example f(x) { x } is a plain declaration and example/f(x) { x } is a path declaration.

Folders concatenates all it's contents where the folder name is prepend to all the declarations. A folder named abc prepends abc/ to all it's contents.

Declarations(code)

Description Syntax
Inline Term inline x = e;
Inline Term Ascribe inline x : σ = e;
Function x(pm, pm', ...) { e }
Function Ascribe x(pm, pm', ...) : σ in π { e }
Function Ascribe x(pm, pm', ...) :: σ { e }
Synonym type x = σ;
New Type Declaration newtype x : κ;

Terms(e)

Description Syntax
Variable x
Variable x @_
Variable x @<σ, σ', ...>
Global Variable /x/x'/...
Inline Abstraction \pm -> e
Inline Application e {e'}
Inline Binding inline pm = e; e'
Extern extern [arity] "sym"
Function Application e (e', e'', ...)
Runtime Binding let pm = e; e'
Tuple Construction (e, e', ...)
Read Pointer *e
Write Pointer *e = (e')
Array Increment &e[e']
Array to Pointer &*e
Number Literal n
Addition e + e'
Subtraction e - e'
Multiplication e * e'
Divsion e / e'
Modulus e % e'
Equality e == e'
Inequality e != e'
Less e < e'
Less or Equal e <= e'
Greater e > e'
Greater or Equal e >= e'
Integer Resize resize e
True true
False false
Switch switch e { pm -> e; pm' -> e'; ... }
Poly Introduction ς e
Poly Elimination e @_
Poly Elimination e @<σ, σ', ...>
Type Annotation e : σ
Pretype Annotation e :: σ
Continue continue e
Break break e
Loop loop (let pm = e) { e' }
Unsafe Cast cast e

Terms (Syntax Sugar) (e)

Description Syntax Meaning
Not !e if e { false } else { true }
And e & e' if e { e' } else { false }
Or e | e' if e { true } else { e' }
Do e; e' let () = e; e'
If if e { e' } else { e''} switch (e) { true -> e; false -> e'; }

Meta Patterns(pm)

Description Syntax
Linear Variable x
Linear Variable Abscribe x : σ
Unrestricted Variable Abscribe x :* σ
Polymorphic Variable Abscribe x :^τ σ

Runtime Patterns(pm)

Description Syntax
Variable x
Variable Abscribe x : σ
Tuple Destruction (pm, pm', ...)
True true
False false

Scheme(ς)

Description Syntax
TypeScheme <pmσ, pmσ', ...>

Types(σ, τ, π, κ, ρ)

Description Syntax
Hole _
Variable x
Linear Inline Function σ -> τ
Unrestricted Inline Function σ -* τ
Polymorphic Inline Function σ -π τ
Poly ς σ
Function Pointer function(σ, σ', ...) -> τ uses π
Tuple (σ, σ', ...)
Effect σ in π
Unique unique σ
Shared σ @ π
Pointer σ*
Array σ[]
Number ρ integer(ρ')
Boolean boolean
IO Region io
Step step<σ, τ>
Meta Type metatype
Type type<σ, τ>
Boxed boxed
Capacity capacity
Region region
Pointer Representation pointer
Struct Representation struct (ρ, ρ', ...)
Union Representation union (ρ, ρ', ...)
Word Representation ρ word
Signed signed
Unsigned unsigned
Byte Size 8bit
Short Size 16bit
Int Size 32bit
Long Size 64bit
Native Size native
Representation representation
Signedness signedness
Size size
Type True true
Type False false
Type And σ & τ
Type Or σ | τ
Type Not
Type Xor σ (+) τ

Types (Internal) (σ, τ, π, κ, ρ)

Description Syntax
Unification unification
Kind kind<σ>
Syntactic syntactic
Propositional propositional
Top /|\
Function Literal Type function literal(σ) -> τ uses π
Label label
Ambiguous Label ambiguous

Types (Syntax Sugar) (σ, τ, π, κ, ρ)

Description Syntax Meaning
Byte byte signed integer(8bit)
Short short signed integer(16bit)
Int int signed integer(32bit)
Long long signed integer(64bit)
PtrDiff ptrdiff signed integer(native)
UByte ubyte unsigned integer(8bit)
UShort ushort unsigned integer(16bit)
UInt uint unsigned integer(32bit)
ULong ulong unsigned integer(64bit)
Integer integer(σ) signed integer(σ)
Natural natural(σ) unsigned integer(σ)
Native Integer integer signed integer(native)
Native Natural natural unsigned integer(native)

Type Pattern(pmσ)

Description Syntax
Variable x : κ
Concrete Variable x :* κ

C Compiler Requirements

This list may be incomplete.

  • All pointers must have the same representation (including function pointers).
  • Signed integers must have 2's complement wrapping. (-fwrapv on gcc)

Papers

Useful / Inspirational papers:

Implemented

Linear / Unique Types

Levity polymorphism

Compiler Design

Reduction

Unification

Type Inference (First Class Polymorphism)

PolyML is implemented, but with scope type variables are used rather then schematic ones.

Compiler Design

Regions

Inspirational, and / or Formerly Used

General Introductions

Pure Type Systems

Linear / Unique Types

Effect Tracking

Type Inference (First Class Polymorphism)

Type Inference (Subtyping)

Unification

Internals

Copyright

Copyright © Freddy A Cubas, "Superstar64"

Licensed under GPL3 only. See LICENSE for more info.

About

[Early Stages] Low level functional programming language with linear types, first class inline functions, levity polymorphism and regions.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages