Code Sync
5 HN recommenders · recommended in 9 months, 2018–2024
43:23 · 20K views · Dec 2, 2018
Edwin Brady presents Idris 2, a rewrite of the Idris dependently typed language, and shows type-driven development in practice. The demos show the compiler filling in whole functions from their types.
HN points to it as a good introduction to Idris 2 and a striking demonstration of what dependent types enable.
11 comments from Hacker News
Until yesterday it was officially called "Blodwen" a "prototype successor to Idris", so I assume the fact that it's now officially being called a "pre-alpha implementation of Idris 2" means it's somewhat closer to being ready, but is there some specific announcement about the exact significance of it being officially called Idris 2 now? Edit: Never mind, I found the official announcement on the Idris mailing list: [LINK] He says "No doubt I'll say more about this over the next few weeks," so it sounds like he's planning on making a more detailed announcement later. Edit 2: Also, as someone who hasn't been following Blodwen or how it's different from Idris 1, this looks like a good introduction: this video
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1. Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive. [1] this video
I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: this video (Type Driven Development with Idris 2) Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature.
You don't need the tests. You need only the types. And especially you don't need "artificial dumbness", which does not understand code, and therefore won't produce correct results, but just an advanced programming language. Say hello to Idris! :-) this video
Idris lang seems awesome with the atom plugin. :) Did not use it yet but I hope it will get more attention. this video