Idris, a language that will change the way you think about programming (2015)

<p><pre><code> app : Vect n a -&gt; Vect m a -&gt; Vect (n + m) a </code></pre> That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.

If you are interested in Idris, you might also be interested in agda, which is another dependently typed programming language: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Agda_(programming_language)" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Agda_(programming_language)</a>

Idris homepage: <a href="http:&#x2F;&#x2F;www.idris-lang.org&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.idris-lang.org&#x2F;</a><p>Github: <a href="https:&#x2F;&#x2F;github.com&#x2F;idris-hackers" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;idris-hackers</a>

This is actually perfect for a library on algebraic structures I&#x27;ve been trying to make in Haskell. For example, how does one distinguish between elements in the Dihedral group of order 10 vs. Dihedral group on order 16 when obstensibly, they have the same representation. For now, I think Haskell programmers use type-level arithmetic libraries, but this is a much better solution.

Bit disappointed it makes the assumption the reader knows Haskell, that lost me immediately.

I recently had some murky thoughts on my ideal Matlab replacement, and it would have a feature like this. It would be huge for array-oriented programming:<p><pre><code> func train_model(X: [n d], y: [n 1]) </code></pre> So many lines of code are spent verifying that the sizes of two function arguments are compatible.

I haven&#x27;t used Idris, but it sounds like someone I might want. I really want a tool that lets me mix and match operational code with proofs. It&#x27;s common now to write a unit test while debugging something, less common to write a randomized property tester, and rare to see a theorem prover being used.<p>It would be fantastic if I could casually throw in a proof while debugging a hard problem.

Thanks for the link. I was looking into liquid Haskell and refinement types and thought that it&#x27;s a great idea but rued the fact that it wasn&#x27;t built into the language. I am definitely going to try Idris for one of my projects.

But does it allow specifying vectors that has no less than three and no more than seven items? Or vectors with even number of items?<p>More importantly can we possibly implement church numerals in Haskell? &#x2F;rhetorical

Great article and really interesting language!<p>I wonder how Idris is going to be affected when Dependent types come to Haskell as well (announced at last ICFP)

I would suggest to use Python or some other mainstream language instead of Haskell in example to contrast to Idris. People who know Haskell most likely be already familiar with dependent types and for people not familiar with Haskell syntax could be confusing (as some comments indicate).

I don&#x27;t get it. Is it just about rediscovering std::array?

Does anyone know whether Idris is a response to Haskell&#x27;s &#x27;Foldable&#x27; controversy?<p>It looks like it was released in 2012 on hackage but I don&#x27;t know how far back &#x27;Foldable&#x27; was envisioned.

Is Idris related to Idris Elba, the British actor, by any chance?

&quot;Indentation significant syntax&quot;<p>:(<p>in my opinion, one of the worst ideas to plague many new languages<p>brackets are really, seriously, honestly a better visual cue for grouping