u/Kyraimionin r/haskell • Recommends
Video Tutorial: "How to program in types with length-indexed vectors: Part 1" (Richard Eisenberg)
0:00 / 0:00
#gadt#type-levelprogramming#haskell
@rae: How to program in types with length-indexed vectors: Part 1
Tweag by Modus Create
5K subscribers • 25 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Richard Eisenberg, language designer
- Linked in the descriptiongoldfirere/video-resources
Advanced. Deep dive for people who know the field.
2.3K views5 years ago1 recommendation
Programming languagesComputer scienceHaskellLanguage design and type systemsData structures
Richard Eisenberg demonstrates how to use GADTs and length-indexed vectors in Haskell to turn partial functions into safe, total functions.
This video is the start of a series covering the translation of the Data.List functions to work on the length-indexed vector GADT. This will be an exploration of many aspects of type-level programming, in small bite-sized chunks. This week: GADT basics, and how a type signature can make a partial-looking function -- the dreaded 'head' function of the Prelude -- into a nice, safe total function. Data.List documentation: hackage.haskell.org/package/base-4.15.0.0/docs/Data-List.htm… Companion source repo: github.com/goldfirere/video-resources/tree/main/2021-04-13-v… Further reading about touchable variables: microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-…. See Section 5. Find me at richarde.dev/ or on Twitter at @RaeHaskellWhy it's here
1 person recommends thisWhat people say. Recommended as an excellent tutorial on type-level programming in Haskell by Richard Eisenberg.
u/Kyraimionin r/haskell • Mentions
On “Video Tutorial: "Existentials and writing functions for length-indexed vectors" (Richard Eisenberg)”
This is part 4 in his series, if you haven't seen them, you can find the other parts here:
* Part 1: "How to program in types with length-indexed vectors"
* Part 2: Using singleton types to replicate a length-indexed Vector
* Part 3: Type families help define functions over length-indexed vectors
Also check out Richard's other videos on Tweag's youtube channel
u/Kyraimionin r/haskell • Mentions
On “Video: "Some functions on length-indexed vectors require custom GADTs" (Richard Eisenberg); Part 6 in the series on type level programming”
This is the 6th and last part in his series on type level programming. You can find the other parts here:
* Part 1: How to program in types with length-indexed vectors
* Part 2: Using singleton types to replicate a length-indexed Vector
* Part 3: Type families help define functions over length-indexed vectors
* Part 4: Existentials and writing functions for length-indexed vectors
* Part 5: Using proofs to make functions faster over length-indexed vectors
If you find this style of programming interesting or confusing and you want to learn more, there's an excellent introduction using Coq, the dependently typed programming language and proof assistant: Software Foundations; It shou…
u/Kyraimionin r/haskell • Mentions
On “Video Tutorial: "Using proofs to make functions faster over length-indexed vectors" (Richard Eisenberg)”
This is part 5 in his series on type level programming. You can find the other parts here:
* Part 1: How to program in types with length-indexed vectors
* Part 2: Using singleton types to replicate a length-indexed Vector
* Part 3: Type families help define functions over length-indexed vectors
* Part 4: Existentials and writing functions for length-indexed vectors
Also check out Richard's other videos on Tweag's youtube channel
u/SureSun5678in r/haskell • Mentions
On “A sized array type along with a concatenation function?”
There is a really detailed video series by Richard Eisenberg (from Tweag) on YouTube about how to implement something like this yourself. All episodes together are over hour, but if you have the time, I really recommend the watch!
First episode: link to this video
u/agentultrain r/haskell • Mentions
On “Structural Induction Resources ?”
You learn it fairly early on in Lean: https://leanprover.github.io/theorem\_proving\_in\_lean/induction\_and\_recursion.html but I would read the whole thing from the beginning if you're not familiar with Lean.
Richard Eisengberg's series here: [video touches upon it in Haskell.