Idris2 Alternatives

Idris2 reviews and mentions

• Idris2: A purely functional programming language with first class types
  1 project | news.ycombinator.com | 6 Nov 2023
• Lean4 helped Terence Tao discover a small bug in his recent paper
  10 projects | news.ycombinator.com | 27 Oct 2023

  Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming.

  Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.

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

• How to Keep Lambda Calculus Simple
  1 project | news.ycombinator.com | 8 Jul 2023

  The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.)

  In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct:

  https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...

• What are the current hot topics in type theory and static analysis?
  15 projects | /r/ProgrammingLanguages | 8 May 2023

  Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

• New video! 2022 in Programming Languages
  8 projects | /r/contextfree | 28 Jan 2023
• How to avoid right intendation?
  2 projects | /r/haskell | 17 Jan 2023

  Idris2 has a great syntax for this, see e.g. node018:

• Data types with Negation
  2 projects | /r/ProgrammingLanguages | 16 Jan 2023

  I asked because it just baffles me any time I see a dependently typed language using unary numbers. I think to myself, "are these people even educated? Do they know about number systems?" I mean, cavemen were the last group using unary number system as their mainstay, and that was during the Paleolithic. Then they have issues open like this when they discuss optimizing those damn unaries. But this shouldn't even have been a problem for anyone even remotely related to programming! It's giving a terrible impression of dependently-typed languages. Getting rid of those should be the first step of popularizing them.

• I've learned this from Conor McBride on an SPLV'19 bus ride. A literary reference would be welcome.
  1 project | /r/programmingcirclejerk | 12 Jan 2023
• Altering behavior of runElab and macros outside of source code
  1 project | /r/Idris | 11 Jan 2023

  addOne : Int -> EitherT String IO Int addOne x = pure $ x + 1 add : Int -> Int -> EitherT String IO Int add x y = pure $ x + y main : IO () main = do exportFn `{add} the (IO ()) $ exportFn `{addOne} -- `the (IO ())` is needed due to issue https://github.com/idris-lang/Idris2/issues/2851

• Managing world state for a imperative language with pure functions
  1 project | /r/ProgrammingLanguages | 6 Dec 2022

  The idea of world state is an attraction of the state that side effects change. I got the idea from Idris internals: https://github.com/idris-lang/Idris2/blob/main/libs/prelude/PrimIO.idr

• A note from our sponsor - SaaSHub
  www.saashub.com | 17 Mar 2025

  SaaSHub helps you find the best software and product alternatives Learn more →