Idris
  • Introduction
    • Intended Audience
    • Example Code
  • Getting Started
    • Prerequisites
    • Downloading and Installing
    • The Interactive Environment
  • Types and Functions
    • Primitive Types
    • Data Types
    • Functions
      • where clauses
    • Dependent Types
      • Vectors
      • The Finite Sets
      • Implicit Arguments
      • “using” notation
      • Note: Declaration Order and mutual blocks
    • I/O
    • “do” notation
    • Laziness
    • Useful Data Types
      • List and Vect
      • Aside: Anonymous functions and operator sections
      • Maybe
      • Tuples and Dependent Pairs
      • Dependent Pairs
    • More Expressions
      • let bindings
      • List comprehensions
      • case expressions
    • Dependent Records
      • Nested record update
      • Parameters and Fields
  • Type Classes
    • Default Definitions
    • Extending Classes
    • Functors and Applicatives
    • Monads and do-notation
      • !-notation
      • Monad comprehensions
    • Idiom brackets
      • An error-handling interpreter
    • Named Instances
    • Determining Parameters
  • Modules and Namespaces
    • Export Modifiers
    • Explicit Namespaces
    • Parameterised blocks
  • Packages
    • Package Descriptions
    • Using Package files
  • Example: The Well-Typed Interpreter
    • Representing Languages
    • Writing the Interpreter
    • Testing
    • Running
      • Aside: cast
  • Views and the “with” rule
    • Dependent pattern matching
    • The with rule — matching intermediate values
  • Theorem Proving
    • Equality
    • The Empty Type
    • Simple Theorems
    • Totality Checking
      • Directives and Compiler Flags for Totality
      • Totality checking issues
      • Hints for totality
  • Provisional Definitions
    • Provisional definitions
    • Suspension of Disbelief
    • Example: Binary numbers
  • Interactive Editing
    • Editing at the REPL
    • Editing Commands
      • :addclause
      • :casesplit
      • :addmissing
      • :proofsearch
      • :makewith
    • Interactive Editing in Vim
  • Syntax Extensions
    • syntax rules
    • dsl notation
  • Miscellany
    • Auto implicit arguments
    • Implicit conversions
    • Literate programming
    • Foreign function calls
      • Include and linker directives
      • Testing foreign function calls
    • Type Providers
    • C Target
    • JavaScript Target
      • Code Generation
      • Using the FFI
      • Including external JavaScript files
      • Including NodeJS modules
      • Shrinking down generated JavaScript
    • Cumulativity
  • Further Reading
  • Frequently Asked Questions
    • What are the differences between Agda and Idris?
    • Is Idris production ready?
    • Why does Idris use eager evaluation rather than lazy?
    • How can I make lazy control structures?
    • Evaluation at the REPL doesn’t behave as I expect. What’s going on?
    • When will Idris be self-hosting?
    • Does Idris have Universe Polymorphism? What is the type of Type?
    • Why does Idris use Float and Double instead of Float32 and Float64?
    • What is -ffreestanding?
    • What does the name ‘Idris’ mean?
    • Where can I find more answers?
  • Introduction
    • Hello world
    • Outline
  • State
    • First attempt
    • Introducing Effects
    • Effects and Resources
    • Labelled Effects
    • !-notation
    • Syntactic Sugar and Eff
  • Simple Effects
    • Console I/O
      • Examples
      • Aside: Resource Types
    • Exceptions
      • Example
    • Random Numbers
      • Example
    • Non-determinism
      • Example
    • vadd revisited
    • Example: An Expression Calculator
  • Dependent Effects
    • Dependent States
    • Result-dependent Effects
    • File Management
    • Pattern-matching bind
  • Creating New Effects
    • State
      • Summary
    • Console I/O
    • Exceptions
    • Non-determinism
    • File Management
  • Example: A “Mystery Word” Guessing Game
    • Step 1: Game State
    • Step 2: Game Rules
    • Step 3: Implement Rules
    • Step 4: Implement Interface
    • Discussion
  • Further Reading
  • Effects Summary
    • EXCEPTION
    • FILE_IO
    • RND
    • SELECT
    • STATE
    • STDIO
    • SYSTEM
  • Running example: Addition of Natural Numbers
    • Equality Proofs
      • Type checking equality proofs
    • Heterogeneous Equality
    • Properties of plus
  • Inductive Proofs
  • Pattern Matching Proofs
    • Creating a Definition
    • Base Case
    • Inductive Step
  • Interactive Theorem Proving
  • Documenting Idris Code
    • Comments
    • Inline Documentation
  • Uniqueness Types
    • Using Uniqueness
      • Borrowed Types
      • Problems/Disadvantages/Still to do...
  • New Foreign Function Interface
    • The IO' monad, and main
    • FFI descriptors
    • Foreign calls
      • FFI implementation
    • Compiling foreign calls
    • JavaScript FFI descriptor
  • Erasure By Usage Analysis
    • Motivation
      • Binary numbers
      • U-views of lists
    • Changes to Idris
    • Changes to the language
    • What it means
    • How to use it
    • Benchmarks
    • Shortcomings
    • Planned features
    • Troubleshooting
      • My program is slower
      • Usage warnings are unhelpful
      • There should be no warnings in this function
      • The compiler refuses to recognise this thing as erased
    • How to read and resolve erasure warnings
      • Example 1
      • Example 2
    • References
  • The IDE Protocol
    • Protocol Overview
    • Output Highlighting
    • Source Code Highlighting
  • Type Providers in Idris
    • The use case
    • A simple example
    • Foreign Functions
      • mkForeign
      • Caveats of mkForeign
      • Running foreign functions
      • In the interpreter
      • In an executable
    • Putting it all together
 
Idris
  • Docs »
  • Documentation for the Idris Language
  • Edit on GitHub

Documentation for the Idris Language¶

Note

The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, The Idris Community has waived all copyright and related or neighboring rights to Documentation for Idris.

More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

  • The Idris Tutorial
  • The Effects Tutorial
  • Frequently Asked Questions
  • Theorem Proving
  • Language Reference
  • Tutorials on the Idris Language

The Idris Tutorial¶

  • Introduction
  • Getting Started
  • Types and Functions
  • Type Classes
  • Modules and Namespaces
  • Packages
  • Example: The Well-Typed Interpreter
  • Views and the “with” rule
  • Theorem Proving
  • Provisional Definitions
  • Interactive Editing
  • Syntax Extensions
  • Miscellany
  • Further Reading

Frequently Asked Questions¶

  • Frequently Asked Questions

Learning Effects¶

  • Introduction
  • State
  • Simple Effects
  • Dependent Effects
  • Creating New Effects
  • Example: A “Mystery Word” Guessing Game
  • Further Reading
  • Effects Summary

Theorem Proving¶

  • Running example: Addition of Natural Numbers
  • Inductive Proofs
  • Pattern Matching Proofs
  • Interactive Theorem Proving

Language Reference¶

  • Documenting Idris Code
  • Uniqueness Types
  • New Foreign Function Interface
  • Erasure By Usage Analysis
  • The IDE Protocol

Short Guides¶

  • Type Providers in Idris
Next

© Copyright 2015, The Idris Community.

Built with Sphinx using a theme provided by Read the Docs.