idris-lang/Idris-dev
View on GitHub ↗ ★ 3,478 Haskell archived
A Dependently Typed Functional Programming Language
21 mentions on Hacker News by 21 people: 2 stories, 19 comments · first 2014-04-13 · latest 2020-09-12
20082026
-
…) and a massive code base in Haskell. [Agda]( https://github.com/agda/agda ) and [Idris]( https://github.com/idris-lang/Idris-dev ) were mostly written in Haskell as well.
comment by ywei3410 · 2020-09-12 · in What killed Haskell, could kill Rust, too -
…k) (S j) (S i) = rewrite minimumAssociative k j i in Refl [1] Or prelude, or whatever it's called. https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
comment by nickdrozd · 2020-03-12 · in What would Dijkstra do? Proving the associativity of min -
…If you really wanted to, you could prove that `add` is well-formed in Haskell and Haskell-likes: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
comment by mbo · 2020-02-25 · in Implement with types, not your brain (2019) -
…pedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://en.wikipedia.org/wiki/Dependent_type [2] https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...
comment by TheAsprngHacker · 2020-01-26 · in Types Can Be Like Tests -
…anything, a reader who doesn't know can just jump through to the definition, which is a one-liner: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
comment by lmm · 2020-01-20 · in A game in a pure language (part 1): introduction and problems with Idris -
https://github.com/idris-lang/Idris-dev/blob/5965fb16210b184... Idris is not a Lisp and I've never used it, but it has dependent types (types incorporating values) and encodes matrix dimensions into the type system (I think only matrix…
comment by _fbpt · 2019-10-13 · in Show HN: Bel -
…They're both implemented within Idris, as libraries/modules, rather than being compiler magic: - https://github.com/idris-lang/Idris-dev/blob/master/libs/con... - https://github.com/idris-lang/Idris-dev/blob/master/libs/eff... I think it'd…
comment by cinnamonheart · 2019-06-06 · in Why GitHub used Haskell for Semantic -
…in the contrib library (and the book mentions this). For example the preorder interface you need: https://github.com/idris-lang/Idris-dev/blob/master/libs/con...
comment by KirinDave · 2018-09-23 · in The Little Typer -
…2. compile-time evidence that a runtime check will be performed: https://github.com/idris-lang/Idris-dev/blob/master/libs/bas... 3. Most of all, compile-time checking of state machine properties http://docs.idris-lang.org/e
comment by mej10 · 2017-06-16 · in Things that Idris improves things over Haskell -
…The laziness information is carried around in the types: force : Lazy a -> a force a = a https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ#... (purescript-lazy is also a thing, but I think it's not as seamless because of the "no…
comment by mrkgnao · 2017-06-14 · in Rust as a gateway drug to Haskell -
…than the parsers I am currently writing: https://github.com/ekmett/ermine/tree/master/src/Ermine https://github.com/idris-lang/Idris-dev/tree/master/src/Idri... And here is a relevant Reddit thread, which includes a link to Edward Kmett's…
comment by dhess · 2015-08-17 · in State of the Haskell ecosystem -
My Idris installation instructions: https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Window... It's an example of pulling down build tools and libs (well, a lib) with msys2.
comment by kryptiskt · 2015-08-17 · in State of the Haskell ecosystem -
…kind, and allow them to interact with standard types only in limited ways. See, for example, https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type... . I believe http://protz.github.io/mezzo/ is also exploring this design space.
comment by Jweb_Guru · 2015-04-10 · in Fearless concurrency with Rust -
▲ 19
Uniqueness types in Idrisstory by steveklabnik · 2014-10-27 · 0 comments
-
…list: umap : (a -> b) -> UList a -> UList b umap f [] = [] umap f (x :: xs) = f x :: umap f xs 1. https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type... 2. https://github.com/idris-lang/Idris-dev/wiki/Static-Argument... 3.…
comment by logicchains · 2014-10-27 · in Idris 0.9.15 released – partial evaluation and uniqueness types -
▲ 56
Copatterns in Idrisstory by lelf · 2014-09-10 · 13 comments
-
You can sort of do this sometimes. Consider Idris' decidable equality module: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Idris has type classes and it produces a polymorphic total function `decEq` for any type which…
comment by tel · 2014-07-02 · in Dependently Typed Programming -
Idris has a type class that is pretty much this: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Here's an example interaction. There's a difference, though, since + is only for {Num instance,Fin} addition while ++ is…
comment by reycharles · 2014-06-02 · in Brainfuck beware: JavaScript is after you (2012) -
…something new, that both Idris and F* are open source; https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)
comment by tluyben2 · 2014-04-21 · in The Case for Formal Verification (2013)