Skip to content
Hallway
0:00 / 0:00

#idris#dependenttypes#printf

Idris: Type safe printf

Brian McKenna

1.4K subscribers • 3 videos on Hallway

YouTube
  • Recommended by 3 people: 2 on Lobsters and 1 in engineering communities.
  • A classic. People kept recommending it from 2014 to 2018.
  • Presented by Brian McKenna

Advanced. Deep dive for people who know the field.

12K views12 years ago3 recommendations

Programming languagesComputer scienceLanguage design and type systemsComputation and complexity

Brian McKenna demonstrates how to implement a compile-time type-safe printf function using the Idris programming language.

Demonstrating creation of a type safe printf function using Idris, a dependently typed programming language. The result is here: gist.github.com/puffnfresh/11202637

Why it's here

3 people recommend this

What people say. Recommended as a classic demonstration of dependent types solving a practical type-safety problem.

u/Tehnixin r/haskell • Recommends

Idris compile checked printf, possible in Haskell soon? (with TypeInType coming up, etc) With the new TypeInType extension coming up in GHC 8.0, and a lot of work going into getting dependent type features in Haskell, I was wondering how far we are from something like this https://gist.github.com/puffnfresh/11202637, which is done in Idris (explanation of the code here link to this video A TL;DR of the link: It's a compile time checked version of printf, where the current Text.Printf gives runtime exceptions on wrong usage, the idris version is able to catch this beforehand.
29View on Reddit

Picnoiron Lobsters • Recommends

Idris: Type safe printf Final code (if you want to skip the video): https://gist.github.com/puffnfresh/11202637
15View on Lobsters

puffnfreshon Lobsters • Recommends

Idris: Type safe printf
14View on Lobsters