u/Kyraimionin r/haskell • Recommends
Video: "Some functions on length-indexed vectors require custom GADTs" (Richard Eisenberg); Part 6 in the series on type level programming
0:00 / 0:00
#gadt#length-indexedvectors#ghc
@rae: Some functions on length-indexed vectors require custom GADTs
Tweag by Modus Create
5K subscribers • 25 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Richard Eisenberg
- Linked in the descriptiongoldfirere/video-resources
Advanced. Deep dive for people who know the field.
1.2K views5 years ago1 recommendation
Programming languagesHaskellFunctional programming
Richard Eisenberg demonstrates how to design custom GADTs to implement functions like index and span on length-indexed vectors.
This video is the last in the series on type-level programming with length-indexed vectors. This one covers writing (!!) and span, requiring the design of custom GADTs with just the right setup. There is a longish (but hopefully educational!) diversion down a dead-end -- but, in the end, we all hit dead-ends sometimes. Apologies for the distorted sound -- I know what was wrong and will fix, but had no time to re-record. Code at github.com/goldfirere/video-resources/tree/main/2021-05-18-v… Find me at richarde.dev/ or on Twitter at @RaeHaskellWhy it's here
1 person recommends thisWhat people say. Recommended as the final part of a series on type-level programming with length-indexed vectors in Haskell.