u/Kyraimionin r/haskell • Recommends
Video Tutorial: "Existentials and writing functions for length-indexed vectors" (Richard Eisenberg)
0:00 / 0:00
#existentialtypes#length-indexedvectors#ghc
@rae: Existentials and writing functions for length-indexed vectors
Tweag by Modus Create
5K subscribers • 20 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.
2K views5 years ago1 recommendation
Programming languagesHaskellFunctional programming
Richard Eisenberg explains how to use existential types in Haskell to write functions like filter for length-indexed vectors.
This week's entry in the series on length-indexed vectors is about existentials, and how we need them in order to define functions like `filter`, where we cannot know the length of the output from the input. Code at github.com/goldfirere/video-resources/tree/main/2021-05-04-v… Existentials paper at richarde.dev/papers/2021/exists/exists.pdf Find me at richarde.dev/ or on Twitter at @RaeHaskellWhy it's here
1 person recommends thisWhat people say. Recommended as a clear tutorial on using existential types for Haskell vector operations where output length is unknown.