Idris-dev

Idris‑dev is the development version of Idris 1, a general-purpose functional programming language featuring full dependent types, designed for writing type-safe programs and proofs within the language itself. It compiles to C and JavaScript (for Node.js and browsers), and supports code generation via substitute backends. This repository represents the latest development version of the language, and may contain bugs that are being actively worked on. For those who wish to use a more stable version of Idris please consider installing the latest version that has been released on Hackage. Installation instructions for various platforms can be found on the Idris Wiki. Idris has support for external code generators. Supplied with the distribution is a C code generator to compile executables, and a JavaScript code generator with support for node.js and browser JavaScript.

Features

Full dependent types allowing values to appear in types
Totality checking to ensure functions are complete and terminating
Code generators for C and JavaScript (browser and Node.js)
Supports external backends (e.g., JVM, CIL, LLVM) via community contributions
Strong type-driven development inspired by proof assistants like Agda and Coq
Actively maintained in parallel with Idris 2 development

Project Samples

Project Activity

See All Activity >

License

MIT License

Follow Idris-dev

Idris-dev Web Site

Other Useful Business Software

Auth0 for AI Agents now in GA

Ready to implement AI with confidence (without sacrificing security)?

Connect your AI agents to apps and data more securely, give users control over the actions AI agents can perform and the data they can access, and enable human confirmation for critical agent actions.

Start building today

Rate This Project

User Reviews

Be the first to post a review of Idris-dev!

Additional Project Details

Operating Systems

Linux, Mac, Windows

Programming Language

Haskell

Related Categories

Haskell Programming Languages

Registered

2025-09-04

Similar Business Software

Nim

Nim is a statically typed compiled systems programming language. It combines successful concepts from mature languages like Python, Ada and Modula. Nim generates native dependency-free executables, not dependent on a virtual machine, which are small and allow easy redistribution. Nim's memory...

See Software
Java

The Java™ Programming Language is a general-purpose, concurrent, strongly typed, class-based object-oriented language. It is normally compiled to the bytecode instruction set and binary format defined in the Java Virtual Machine Specification. In the Java programming language, all source code is...

See Software
Visual Basic

Visual Basic is an object-oriented programming language developed by Microsoft. Using Visual Basic makes it fast and easy to create type-safe .NET apps. Visual Basic focuses on supplying more of the features of the Visual Basic Runtime (microsoft.visualbasic.dll) to .NET Core and is the first...

See Software
Zig

Zig is a general-purpose programming language and toolchain for maintaining robust, optimal and reusable software. Focus on debugging your application rather than debugging your programming language knowledge. A fresh approach to metaprogramming based on compile-time code execution and...

See Software
C#

C# (also known as C Sharp, pronounced "See Sharp") is a modern, object-oriented, and type-safe programming language. C# enables developers to build many types of secure and robust applications that run in .NET. C# has its roots in the C family of languages and will be immediately familiar to C,...

See Software
QML

QML is a declarative language that allows user interfaces to be described in terms of their visual components and how they interact and relate with one another. It is a highly readable language that was designed to enable components to be interconnected in a dynamic manner, and it allows...

See Software

Report inappropriate content