u/mttdin r/ProgrammingLanguages • Recommends
Idris 2 - Type-driven Development of Idris - Curry On 2019 - Edwin Brady
0:00 / 0:00
Edwin Brady - Idris 2 - Type-driven Development of Idris
Curry On!
6.3K subscribers • 21 videos on Hallway
- Recommended by 6 people: 4 on Hacker News and 2 in engineering communities.
- A classic. People kept recommending it from 2019 to 2023.
- Presented by Edwin Brady, creator of Idris
Advanced. Deep dive for people who know the field.
19K views7 years ago6 recommendations
Programming languagesComputer scienceLanguage design and type systemsFunctional programmingComputation and complexity
Edwin Brady presents Idris 2 and demonstrates how its dependent type system assists developers by generating code from type specifications.
The uploader added no description.Why it's here
6 people recommend thisWhat people say. Highly recommended for its mind-expanding demonstration of how a compiler can interactively write code for you using dependent types.
Moments people linked to
u/dharmatechin r/ProgrammingLanguages • Recommends
Edwin Brady on Chez Scheme
From this video at the 25:22 mark:
> As things stand, the executable it generates is in Scheme.
> This is running via Chez Scheme.
> Chez Scheme is something that's been developed over decades at Cisco, recently open sourced.
> And I thought, ok that will be a good stop gap. It turns out that Chez Scheme is astonishingly fast. So even from source, the Chez Scheme generated version for the small set of benchmarks I've tried has run faster than the Idris 1 which goes via C.
> So I guess spending 30 years of knowing what you're doing is quite good if you're writing a runtime system.
lapinoton Hacker News • Recommends
On “CLUI: Building a Graphical Command Line”
I really like the general idea of bridging the gap between graphical and text-based interfaces, abstracting away the differences and be able to use a mixture of both. In the realm of interactive programming (eg heavily ide assisted), people with some functional and statically typed programming background would be interested in this magnificent talk about idris2: Edwin Brady - Idris 2 - Type-driven Development of Idris link to this video
chonglion Hacker News • Recommends
On “Dependent Haskell Is the Future (2018)”
Every single one of your claims is addressed by the programming language Idris 1, which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims. 1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do. Moreover, Idris (and other dependently typed languages) can perform implementation inference , something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the…
pjmlpon Hacker News • Recommends
On “It's not what programming languages do, it's what they shepherd you to (2020)”
Not quite what you mean, but still, you might find interesting the talks on how to approach coding in languages like Idris, where the compiler is able to support the editor in type suggestions. link to this video
adamgordonbellon Hacker News • Recommends
On “Idris: A Language for Type-Driven Development”
The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube: link to this video The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.
u/erdesztin r/haskell • Mentions
On “Is there an IDE that can use Holes and Hoogle and Types to help me synthesize code fragments?”
Both Idris and Agda supports it through editor plugins(I use it with vs code). Here's a video showing some of the capabilities of Idris.
ghc-mod was also able to do case split and basic hole refinement(https://github.com/DanielG/ghc-mod/blob/v5.1.1.0/src/GHCMod.hs#L109) but I think that functionality is now moving over to haskell-ide-engine and I'm not sure about the status.
u/sullyj3in r/haskell • Mentions
On “Dependent Types are a Runtime Maybe”
Edwin has demonstrations of this in some of his talks:
[video
valenterryon Hacker News • Mentions
On “Immutability is not enough (2016)”
…d depending on the programming language it is actually surprisingly easy. Not only that, with a good typesystem, you not only prevent invalid state from occurring, you even get a lot of support from your IDE due to the extra information it has. Here's an example how that can look like for matrices and functions to manipulate them (like transpose): link to this video The syntax might be alien to you, but I hope it still shows what's possible at compile-time before even running the program with modern languages today.…
u/PurpleYoshiEggin r/ProgrammingLanguages • Mentions
On “Does Rust prevent more logic bugs than statically-typed pure FP languages?”
I think with improvements in dependently-typed languages, certain classes of logic errors could be detectable (e.g., if you have a withdraw function, you can make your type depend on the fact that the output balance must be less than or equal to the original balance. If this invariant is violated, the compiler will error). I believe that we are still a long way off from such a thing being useful, and I am not sure for such an example that the gains are quite worth it.
See this Idris type example for how vectors' lengths are built into the type system. You would be able to put a balance into a type here, as well.
This also wholly depends on whatever specification (if it exists) being co…