Skip to content
Hallway
0:00 / 0:00

#typefamilies#dependenttypes#type-levelprogramming

@rae: Type families help define functions over length-indexed vectors

Tweag by Modus Create

5K subscribers • 25 videos on Hallway

YouTube
  • Recommended by 1 person: 1 in engineering communities.
  • Presented by Richard Eisenberg, Haskell researcher
  • Linked in the descriptiongoldfirere/video-resources

Advanced. Deep dive for people who know the field.

1.6K views5 years ago1 recommendation

Programming languagesHaskellLanguage design and type systems

Richard Eisenberg explains how to use Haskell type families to define operations where the output vector length is computed from input lengths.

This is the third installment in a series about exploring type-level programming through length-indexed vectors. This one covers type families, and how we need them to write operations where the output length must be computed from the input length(s). First in the series, focusing on GADTs: youtu.be/PHS3Q-tRjFQ Second in the series, focusing on singletons: youtu.be/WHeBxSBY0fc Finished code to follow along: github.com/goldfirere/video-resources/blob/main/2021-04-27-v… Find me at richarde.dev/ or on Twitter at @RaeHaskell

Why it's here

1 person recommends this

What people say. Recommended as part of a series explaining type-level programming and dependent types in Haskell.

u/Kyraimionin r/haskell • Recommends

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
11View on Reddit

u/Kyraimionin r/haskell • Recommends

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…
10View on Reddit

u/Kyraimionin r/haskell • Recommends

On “Video Tutorial: "How to program in types with length-indexed vectors: Part 1" (Richard Eisenberg)”

Followup videos: * Part2 : Using singleton types to replicate a length-indexed Vector * Part 3: Type families help define functions over length-indexed vectors Also check out the rest of the channel (link to this video Thanks, Richard, for the great videos, they are much appreciated!
6View on Reddit

u/Kyraimionin r/haskell • Recommends

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
4View on Reddit