Skip to content
Hallway
0:00 / 0:00

#dependenttypes#type-levelprogramming#formalproofs

@rae: Using proofs to make functions faster 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.8K views5 years ago1 recommendation

Programming languagesComputer scienceHaskellAlgorithmsLanguage design and type systems

Richard Eisenberg shows how to write a linear-time reverse function over length-indexed vectors in Haskell using type-level proofs.

Defining `reverse` over a length-indexed vector leads to a quadratic algorithm if done naively. But doing it linearly is hard and requires several proofs, as this video demonstrates. Code available at github.com/goldfirere/video-resources/tree/main/2021-05-11-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

Video Tutorial: "Using proofs to make functions faster over length-indexed vectors" (Richard Eisenberg)
21View 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