DOCSEARCHbyAlgolia
Submit Docs

Idris 2 Documentation

repository·main·Indexed 25 days ago

https://github.com/idris-lang/idris2

Idris 2 is a purely functional programming language featuring first-class types, designed for high-assurance software development through type-driven design. This documentation covers the use of the pack package manager, the Control.App module for managing state and exceptions, and the Idris2 UNIX benchmark suite for measuring performance across backends such as chez, refc, racket, and gambit.

Tokens
55K
Snippets
193
Records
316
Agent score
84%

What's inside Idris 2

  2. Overview of Idris 2 Prelude and Base Libraries

    main

    The Idris 2 Prelude is intentionally minimal, containing only functions required by almost any non-trivial program. Most utility functions previously found in the Idris 1 Prelude have been moved to the base libraries.

    Included in Prelude:

    • Desugaring primitives (tuples, (), =)
    • Basic types (Bool, Nat, List, Stream, Dec, Maybe, Either)
    • Core utilities (id, the, composition)
    • Arithmetic interfaces and implementations
    • Char and String manipulation
    • Typeclass implementations (Show, Eq, Ord, Semigroup, Monoid, Functor, Applicative, Monad, Foldable, Alternative, Traversable)
    • Range for list syntax
    • Console IO

    Commonly used modules in base:

    • Data.List, Data.Nat
    • Data.Maybe, Data.Either
    • System.File, System.Directory (File management)
    • Decidable.Equality

  3. Understand the Idris 2 Core Language (TT)

    main

    The core language of Idris 2 is TT, defined in Core.TT. It is based on Quantitative Type Theory (QTT), where binders have multiplicities: *0*, *1*, or unlimited.

    Key architectural components:

    • Terms: Indexed over names in scope to ensure they are always well-scoped.
    • Values: Defined as NF (Normal Form) in Core.Value. Constructors do not evaluate arguments until requested.
    • Elaboration: The process of translating a high-level language (TTImp) into the core TT. This involves desugaring operators, do notation, and handling implicit arguments and proof search.
    • Linearity Check: Performed after elaboration in Core.LinearCheck to update hole types and multiplicities.

  4. Understand Totality in Idris 2

    main

    Idris distinguishes between total and partial functions:

    • Total functions: Either terminate for all possible inputs or produce a non-empty, finite prefix of a possibly infinite result. Total functions are safe to evaluate during type checking.
    • Partial functions: May crash or enter an infinite loop. While they can be used in types, they are not evaluated during type checking to prevent the type checker from failing to terminate.

    Understanding this distinction is critical because only total functions are guaranteed to be evaluated by the compiler during the type-checking process.

  5. Understand the concept of Dependent Types in Idris 2

    main

    In Idris 2, types are first-class language constructs that can depend on values. This allows you to encode properties directly into types. A common example is the Vect n a type, where n is a value representing the length of the list and a is the element type. This enables functions to specify precise properties in their type signatures, such as the app function which concatenates two vectors and guarantees the resulting length is the sum of the input lengths.

    app : Vect n a -> Vect m a -> Vect (n + m) a

  6. Understand Erasure and Multiplicity

    main

    Idris 2 uses multiplicity annotations (RigCount) for all binders to support linear types.

    • Erasure: Unbound implicits are assigned a multiplicity of 0.
    • Runtime Behavior: Arguments with 0 multiplicity are erased at runtime.
    • Compiler Safety: The elaboration and case tree compiler ensure that 0-multiplicity arguments are never inspected in case trees.
      • For constructors, 0-multiplicity arguments are removed completely.
      • For functions, 0-multiplicity arguments are replaced with a placeholder erased value.

  9. Use named implementations for interfaces

    main

    If you need multiple implementations of the same interface for a single type (e.g., different sorting orders or printing formats), you can name them using the [name] syntax.

    To call a specific named implementation, use the @{name} syntax. This is useful for overriding default behavior in specific function calls.

    [myord] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{myord} x y

-- Usage:
-- sort @{myord} testList

  10. Handle function calls and partial application

    main

    Custom backends must handle four types of function calls:

    • Saturated: All arguments are present.
    • Under-applied: Some arguments are missing (supported by ANF and Lifted via the UnderApp constructor).
    • Primitive: Necessarily saturated (PrimFn constructor).
    • Foreign: Referred to by name.

    If your host language does not natively support partial application (like Scheme does), you must simulate closures. A common approach is to create a special object that stores the function and its currently applied values, waiting until all arguments are received before evaluation.

  11. Implement a well-typed interpreter

    main

    An interpreter can be implemented as a function interp that takes an Env (environment) and an Expr (expression) and returns a concrete Idris value.

    • Environment: Define an Env indexed by the same Vect n Ty as the expression context. Use lookup with a HasType proof to retrieve values.
    • Evaluation: The interp function pattern matches on the Expr constructors:
      • Var: Uses lookup in the environment.
      • Val: Returns the literal value.
      • Lam: Returns an Idris lambda that extends the environment.
      • App: Interprets the function and argument, then applies them.
      • Op: Applies the provided Idris operator to the interpreted operands.
      • If: Uses Idris's if...then...else to evaluate the appropriate branch lazily.
    data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)

lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop    (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

interp : Env ctxt -> Expr ctxt t -> interpTy t
interp env (Var i)     = lookup i env
interp env (Val x)     = x
interp env (Lam sc)    = \x => interp (x :: env) sc
interp env (App f s)   = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e)  = if interp env x then interp env t
                                         else interp env e

  12. Migrate 'Type-Driven Development with Idris' code to Idris 2

    main
    The code in the book Type-Driven Development with Idris by Edwin Brady requires small changes to work in Idris 2. If you are a beginner, it is recommended to work through the first 3-4 chapters using Idris 1 to avoid these changes. For later chapters, refer to the specific updates required for each chapter in this document. Updated code is also available in the Idris 2 test suite under tests/typedd-book.