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 • 20 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.