使用 Homebrew, apk, dnf, MacPorts, Nix 安装 idris2

项目链接

• 主页
• 仓库

命令和别名

• idris2

项目历史

Idris development is led by Edwin Brady at the University of St Andrews, and the Idris site presents the language as a vehicle for type-driven development: types are treated as plans that guide construction of programs. Idris 2 grew out of that project as a new version of the dependently typed language rather than a small revision of Idris 1.

The Idris 2 paper submitted in 2021 describes the language as a new version of Idris with a core based on Quantitative Type Theory. The official migration documentation emphasizes the practical consequence: every variable has a quantity, so the compiler can distinguish erased values, exactly-once values, and ordinary unrestricted values.

The public Idris2 repository records release tags beginning with v0.2.0 in 2020 and continuing through later 0.x releases. The README also points users to Idris 2 talks from the late 2010s, the official documentation, the Pack package manager, curated community libraries, and idris2-lsp.

采用历史

Adoption has centered on the functional programming, dependent-types, theorem-proving, and programming-language-research communities. The project deliberately preserves a path for Idris 1 users through documentation about language differences and book updates, while also advertising Idris 2 specific learning material and talks.

Package-manager adoption reflects that Idris 2 became installable outside its research niche. The supplied package metadata lists Homebrew, Alpine, Fedora, MacPorts, and Nix package names, giving users a route to the compiler without building the full language stack manually.

使用方式

Users run the idris2 compiler and REPL to write dependently typed programs, explore holes interactively, compile programs, and build packages described by .ipkg files. The README describes Pack as the common way to install Idris packages and work with compatible package collections.

The language is commonly used for examples where types express program invariants: length-indexed data, proof-carrying code, safe protocols, and resource-aware APIs. Idris 2's QTT-based quantities make erasure and linear usage visible to programmers instead of leaving them as compiler-only implementation details.

为什么软件包爱好者会关心

Idris 2 is a package-nerd marker for the point where dependently typed programming moved from papers and conference demos into reproducible command-line tooling. Installing it from Homebrew or Nix pulls a language whose central design is tied directly to contemporary type theory.

It is also interesting because its ecosystem has package metadata of its own. The README's .ipkg and Pack discussion makes Idris 2 both a package in Unix package managers and a language with a nested package culture.

时间线

• 2018: Public Idris 2 talks appear in the official README resource list.
• 2020: Public Idris2 release tags begin with v0.2.0.
• 2021: Edwin Brady's Idris 2: Quantitative Type Theory in Practice paper is submitted and appears at ECOOP 2021.
• 2022: v0.6.0 release tag marks another packaged compiler milestone.
• 2023: v0.7.0 release tag is recorded in the upstream repository.
• 2025: v0.8.0 release tag is recorded in the upstream repository.

Related projects

• Idris 1 is the direct predecessor and remains the context for much of the teaching material, including Type-Driven Development with Idris and the official migration notes.
• Pack, idris2-pack-db, idris2-lsp, the idris-community organization, and the Idris Zulip form much of the surrounding tooling and community infrastructure.

来源

• https://arxiv.org/abs/2104.00480
• https://formulae.brew.sh/formula/idris2
• https://github.com/idris-lang/Idris2
• https://idris2.readthedocs.io/en/latest/updates/updates.html
• https://www.idris-lang.org/