Skip to content
Hallway
0:00 / 0:00

#singletons#dependenttypes#type-levelprogramming

@rae: Using singleton types to replicate a length-indexed Vector

Tweag by Modus Create

5K subscribers • 25 videos on Hallway

YouTube
  • Recommended by 2 people: 2 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.8K views5 years ago2 recommendations

Programming languagesHaskellLanguage design and type systems

Richard Eisenberg demonstrates how to use singleton types in Haskell to implement a replicate function for length-indexed vectors.

This second video in my series on type-level programming with length-indexed vectors shows how fancy types help us to avoid programming errors. We also encounter the first time we need a singleton type to make progress, in the type of replicate. Previous video: youtu.be/PHS3Q-tRjFQ Final version of code in video: github.com/goldfirere/video-resources/tree/main/2021-04-20-v… Find me at richarde.dev/ or on Twitter at @RaeHaskell

Why it's here

2 people recommend this

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

u/clinton84in r/haskell • Recommends

Hacking Richard Eisenberg's Haskell "dependently typed" example. Some follow up questions?... Richard Eisenberg recently posted the video @rae: Using singleton types to replicate a length-indexed Vector. The full code in Richard's talk is at here. My modified version, of which snippets are in this post, is here. I asked the question in the YouTube comments about whether we could call `replicate` with an `Int` argument and Richard kindly answered and pointed out that as Haskell doesn't have existential types this doesn't work. But then I thought, Haskell kind of does have existential types, just by hiding type variables in the type constructor. Below is the exploration of that idea,…
15View on Reddit

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