---
key: pl/idris
kind: plang
name: "Idris"
url: https://plangs.page/idris
---

# Idris

> Purely-functional language for Type-Driven Development with dependent types and optional lazy evaluation.

Purely-functional programming language, designed for Type-Driven Development with dependent types, optional lazy evaluation, and features such as a totality checker. It serves as both a general-purpose language and a proof assistant.

## Facts

- Appeared: 2007
- Homepage: https://www.idris-lang.org
- GitHub: https://github.com/idris-lang/Idris2
- Languish ranking: #262

## Relationships

### Paradigms

- [Functional](https://plangs.page/paradigm/functional)

### Platforms

- [Cross-Platform](https://plangs.page/platform/cross)

### Type Systems

- [Algebraic Data Types](https://plangs.page/type-system/algebraic)
- [Dependent](https://plangs.page/type-system/dependent)
- [Inferred](https://plangs.page/type-system/inferred)
- [Static](https://plangs.page/type-system/static)
- [Strong](https://plangs.page/type-system/strong)

### Influenced By

- [Agda](https://plangs.page/agda)
- [Clean](https://plangs.page/clean)
- [Coq](https://plangs.page/coq)
- [F#](https://plangs.page/f-sharp)
- [Haskell](https://plangs.page/haskell)
- [Rust](https://plangs.page/rust)

### Licenses

- [BSD](https://plangs.page/license/bsd)

### Tags

- [Interpreter](https://plangs.page/tag/interpreters)
- [Proof Assistant](https://plangs.page/tag/proofs)