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 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 except that Aith uses subtyping rather then multiplication. 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

(todo)

First Class Polymorpism (System-F)

(todo)

Subtyping

(todo)

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.

Road Map (subject to change)

• Essentials
  • Runtime Primitives
    • Booleans
      • Boolean Type
      • Boolean Literals
      • If expression
      • Logical Operators
    • Integers
      • Arithmatic
      • Relational Operators
    • Pointers
      • Shared
        • Type
        • Stack Allocation
        • Get
        • Set
      • Unique
        • Type
        • Heap Allocation
      • Borrowing
    • Arrays
      • Shared
        • Type
        • Array to Pointer
        • Pointer Addition
        • Pointer Difference
        • Heap Allocation
      • Unique
        • Type
        • Heap Allocation
      • Borrowing
    • Tuples
      • Type
      • Construction
      • Destruction
      • Multiplicity Polymorphism
      • Multiplicity Inference
    • Function Pointers
    • Records
    • Tagged Unions
      • Union Representation
      • Tagged Union Type
    • Loops
  • New Types
  • Type Synonyms
  • Modules
  • Hindley Milner
    • Syntatical Unification
    • Typeclasses
  • Pattern Matching
    • Destructure Products
    • Literals
    • Destructure Unions
• Inline Lambda Calculus
• System-F
  • Levity Polymorphism
  • Type Lambda / Application
  • Type Lambda / Application for Runtime Terms
  • Higher Order Unification (System-F ω)
• Linear / Unique Types
• Effectful Regions
  • Effects
  • References
    • Type
    • Read
    • Write
  • Let Region
  • Region Subtyping
• C Code Generation

Syntax

Files start with code ::.

Modules(code)

Terms(e)

Terms (Syntax Sugar) (e)

Meta Patterns(pm)

Runtime Patterns(pm)

Scheme(ς)

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

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

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

Type Pattern(pmσ)

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

• Linear Haskell (video)
  • Implemented but with subtyping rather then multiplication

Levity polymorphism

• Levity Polymorphism (video)
  • Implemented with more restrictive representation lambda.

Compiler Design

• Invertible Syntax Descriptions: Unifying Parsing and Pretty Printing
  • Implemented with prisms instead of partial isomorphisms.

Algorithms

• Demonstrating Lambda Calculus Reduction
  • Applicative order reduction used for reduction.
• Unification Theory
  • Pointer for Robinson unification algorithm

Type Inference (First Class Polymorphism)

The idea of having an implicit type scheme and explicit type scheme is taken from these two papers (QML and the Explicit Poly-ML variant). The major modification is that scope type variables are used rather then schematic ones.

• Semi-Explicit First-Class Polymorphism for ML
• QML : Explicit First-Class Polymorphism for ML

Type Inference (Subtyping)

• The Simple Essence of Algebraic Subtyping (video)
  • A tiny subset is implemented for type checking regions. See my var sub repo.

Compiler Design

• How OCaml type checker works -- or what polymorphism and garbage collection have in common
  • Only implemented for checking escaping skolem variables. Still need to implement let generalization.

Planned

Linear / Unique Types

• The Best of Both Worlds: Linear Functional Programming without Compromise (video)
  • Un typeclass implemented as a builtin currently.

Regions

• • Monadic and Substructural Type Systems for Region-Based Memory Management
    • Implementation of single effect region calculus is in progress
  • Monadic Regions
  • A Step-Indexed Model of Substructural State
  • Linear Regions Are All You Need

Related / Unused

General Introductions

• Practical Foundations for Programming Languages
• Type Systems

Pure Type Systems

• An Introduction to Generalized Type Systems
• The Structural Theory of Pure Type Systems (video)

Linear / Unique Types

• • Making Uniqueness Typing Less Unique
  • Uniqueness Typing Redefined
  • Equality-Based Uniqueness Typing
  • Uniqueness Typing Simplified
  • Modelling Unique and Affine Typing using Polymorphism
• A taste of linear logic
• Linearity and Uniqueness: An Entente Cordiale

Type Inference (First Class Polymorphism)

• • HMF: Simple type inference for first-class polymorphism
  • Flexible types: robust type inference for first-class polymorphism
• FreezeML : Complete and Easy Type Inference for First-Class Polymorphism (video)
• A Quick Look at Impredicativity (video)

Type Inference (Subtyping)

• • Algebraic Subtyping
  • Polymorphism, Subtyping, and Type Inference in MLsub (video)

Unification

• Unification Under a Mixed Prefix

Internals

• System F with Type Equality Coercions
• Generalizing Hindley-Milner Type Inference Algorithms

Copyright

Copyright © Freddy A Cubas, "Superstar64"

Licensed under GPL3 only. See LICENSE for more info.