Welcome to Alba’s documentation!

Contents:

• 1. Introduction
  • 1.1. Goals of the Language
  • 1.2. Goals for Version 1
• 2. Certified Programming
  • 2.1. Logic
    • 2.1.1. Function Composition
    • 2.1.2. Propositions
    • 2.1.3. Equality
    • 2.1.4. Decisions
    • 2.1.5. Refinement
  • 2.2. Natural Numbers
    • 2.2.1. Basic Definitions
    • 2.2.2. Zero is Different from a Successor
    • 2.2.3. Properties of Addition
    • 2.2.4. Properties of Multiplication
    • 2.2.5. Properties of Order
    • 2.2.6. Order and Predicates
    • 2.2.7. Difference
    • 2.2.8. Wellfounded Recursion
  • 2.3. Binary Natural Numbers
    • 2.3.1. Basic Definitions
  • 2.4. List
    • 2.4.1. Basics
    • 2.4.2. Append Lists
    • 2.4.3. List Reversal
  • 2.5. Vector
    • 2.5.1. Basics
    • 2.5.2. Concatenate Vectors
    • 2.5.3. Reverse Vectors
    • 2.5.4. Random Access
  • 2.6. Parsing
    • 2.6.1. String Parser
    • 2.6.2. Incremental Parsers
    • 2.6.3. Backtracking (DRAFT)
  • 2.7. Printf like Functions
• 3. Language Elements
  • 3.1. Abstract Data Types
  • 3.2. Do Notation
  • 3.3. Functions
    • 3.3.1. Anonymous Functions
    • 3.3.2. Named Functions
    • 3.3.3. Recursive Functions
    • 3.3.4. Mutually Recursive Functions
  • 3.4. Inductive Types
    • 3.4.1. General Inductive Types
    • 3.4.2. Mutually Inductive Types
    • 3.4.3. Nested Inductive Types
    • 3.4.4. Why Positivity?
  • 3.5. Implicit Arguments
  • 3.6. Inspect Expression
  • 3.7. Lexical Structure
    • 3.7.1. Input Format
    • 3.7.2. Wildcard
    • 3.7.3. Punctuation Symbols
    • 3.7.4. Identifiers
    • 3.7.5. Keywords
    • 3.7.6. Operators
    • 3.7.7. Literals
    • 3.7.8. Comments
    • 3.7.9. Whitespace
    • 3.7.10. Allowed UTF-8 Characters
    • 3.7.11. UTF-8 Encoding
  • 3.8. Local Definitions
  • 3.9. Modules
    • 3.9.1. Top Level Modules
    • 3.9.2. Inner Modules
  • 3.10. Namespaces
    • 3.10.1. Declaration of Names
    • 3.10.2. Usage of Names
  • 3.11. Packages
  • 3.12. Pattern Match
    • 3.12.1. Syntax
    • 3.12.2. Type
    • 3.12.3. Rules
    • 3.12.4. Welltyped
    • 3.12.5. Canonical Forms
    • 3.12.6. Reachability
    • 3.12.7. Exhaustiveness
    • 3.12.8. Pattern Match Compiler
    • 3.12.9. Modified Pattern Compiler
  • 3.13. Precedence and Associativity
  • 3.14. Projects
  • 3.15. Records
    • 3.15.1. Simple Records
    • 3.15.2. Dependent Records
  • 3.16. Sections
  • 3.17. Style and Conventions
    • 3.17.1. Generous Spacing
    • 3.17.2. Choosing Names
    • 3.17.3. Identifier Case
  • 3.18. Telescopes / Formal Arguments
  • 3.19. Types
  • 3.20. Universes / Sorts
    • 3.20.1. Basics
    • 3.20.2. Subtyping
    • 3.20.3. Dependent Lists
    • 3.20.4. Heterogeneous Lists
    • 3.20.5. Draft
    • 3.20.6. Russel’s Paradox
• 4. Builtins
  • 4.1. Module: alba.core.general
  • 4.2. Module: alba.core.logic
    • 4.2.1. Axioms and Builtin Definitions
    • 4.2.2. Equality
  • 4.3. Module: alba.core.natural
    • 4.3.1. Builtin Definitions
    • 4.3.2. Recursion and Induction
    • 4.3.3. Addition
    • 4.3.4. Multiplication
    • 4.3.5. Exponentiation
    • 4.3.6. Order Relation
  • 4.4. Module: alba.core.integer
  • 4.5. Module: alba.core.nat
    • 4.5.1. Axioms and Builtin Definitions
    • 4.5.2. Embedding into Natural Numbers
  • 4.6. Module: alba.core.list
  • 4.7. Basic Types
    • 4.7.1. Scalar Types
• 5. Intermediate Representation
  • 5.1. Basics
  • 5.2. Names
• 6. Compilation
  • 6.1. Pattern Match
  • 6.2. Elaboration
    • 6.2.1. Inductive Type
    • 6.2.2. Pattern Match
  • 6.3. Context
  • 6.4. Term Elaboration
  • 6.5. Elaboration Context
  • 6.6. Sorts
  • 6.7. Types
  • 6.8. Products
  • 6.9. Identifier / Operator
  • 6.10. Function Application
  • 6.11. Term
• 7. Platforms
  • 7.1. Browser
    • 7.1.1. Modules
    • 7.1.2. Browser Programs
• 8. Backends
  • 8.1. Javascript
    • 8.1.1. General
    • 8.1.2. Browser
    • 8.1.3. Nodejs
  • 8.2. Rust
  • 8.3. LLVM
    • 8.3.1. Memory Representation
    • 8.3.2. Some Examples
    • 8.3.3. Algebraic Types
• 9. Draft
  • 9.1. Hoare State Monad (Swierstra)
    • 9.1.1. Without Monad
    • 9.1.2. With Monad
    • 9.1.3. Hoare Monad
    • 9.1.4. Certified Relabelling
    • 9.1.5. Some Analysis
    • 9.1.6. Example: Open File Descriptors
    • 9.1.7. Example: Open File Descriptors (2)
    • 9.1.8. Example: Open File Descriptors (3)
  • 9.2. IO
    • 9.2.1. Console Programs
    • 9.2.2. IO Interface
    • 9.2.3. Sinks
    • 9.2.4. Buffers
    • 9.2.5. Appendix
  • 9.3. Effects (Idris)
  • 9.4. Wellfounded Recursion
    • 9.4.1. W Types
    • 9.4.2. Unbounded Search with Bound Function
    • 9.4.3. Merge Sorted Lists
    • 9.4.4. Ackermann Function
    • 9.4.5. Unbounded Search for Natural Numbers
    • 9.4.6. Wellfounded Relations on Inductive Types
  • 9.5. Monad Recursion
    • 9.5.1. Parsing Monad
    • 9.5.2. Monadic Parser with Progress Indicator
    • 9.5.3. State and Continuation Monads and Progress
    • 9.5.4. Progress in IO
  • 9.6. Group Theory
    • 9.6.1. Subgroups
    • 9.6.2. The Integers mod n
    • 9.6.3. Cyclic Subgroups
  • 9.7. Records, Objects, …
    • 9.7.1. Inductive Data Types
    • 9.7.2. Records
  • 9.8. Platforms
    • 9.8.1. Unix Console Applications
    • 9.8.2. Browser Applications
    • 9.8.3. Server Applications
  • 9.9. Pattern Match
    • 9.9.1. Ideas from “Implementation of Functional Languages” of Simon Peyton Jones.
    • 9.9.2. Examples
  • 9.10. Pattern Match Compiler
    • 9.10.1. Basics
    • 9.10.2. ?
    • 9.10.3. Example nodups
    • 9.10.4. Example: Eliminate Duplicates
    • 9.10.5. Examply unwieldy
    • 9.10.6. Example: demo
    • 9.10.7. Example: less equal
    • 9.10.8. Example: greater equal
    • 9.10.9. Example: map2
  • 9.11. Pattern Guard
• 10. Bibliography