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 • 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.
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.
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/Noughtmarein r/haskell • Mentions
On “Monthly Hask Anything (August 2021)”
The difference between existential and universal quantification is about the location of the `forall`, I think it is unfortunate that GHC reuses the syntax in this way. You have already written the existential version of `Obj`:
data Obj = forall a . Show a => Obj a
And this is the universal version:
data Obj = Obj (forall a. Show a => a)
You can write the universal version directly in a type signature without the `Obj` wrapper, but you cannot write the existential version directly in a type signature.
There are some ambitions to make existential quantification first-class like universal quantification is now, but it is still at the very early stages. I don't know how much effort…