Skip to content
Hallway
0:00 / 0:00

#idris#dependenttypes#printf

Idris: Type safe printf

Brian McKenna

1.4K subscribers • 4 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.

Moments people linked to

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

u/CodeBlockin r/haskell • Mentions

On “Verifying the monoid laws using Idris”

Another neat example of dependent types is demonstrated with another video that Brian put up a few weeks back where he made a type-safe printf function in Idris as well. It clearly shows how the type of the function is determined by the value passed to it (in this case, a format string).
6View on Reddit

u/tyrionitein r/haskell • Mentions

On “Examples of real-world haskell usage where correctness is important (not just type-safety)”

Have you looked at Idris? * http://www.idris-lang.org/ * link to this video * link to this video
6View on Reddit

u/paf31in r/haskell • Mentions

On “Compile Time TDD Coverage”

> The printf & scanf example (and proof of their inverse relation) I saw recently is one such example IMHO This one? I modified the printf bit from puffnfresh's idris demo.
4View on Reddit

u/chrisdonerin r/haskell • Mentions

On “Necessity/utility of dependent types?”

> how could you possibly validate or invalidate something which doesn't exist yet? That logic cannot possibly disappear at runtime. Supposing you write `validEmail "foo@bar" :: Maybe Email`, you now have to handle a case which will never happen, despite knowing as a programmer right now that this is correct. Dependent types can let you run your validation function at compile-time on the string `chrisdone@gmail.com`. Thus the logic disappeared at runtime. Simplifying with a type like: data NameChar = F | O data DomainChar = B | A | R | M U data NonEmpty a = Cons a a data Email = Email (NonEmpty NameChar) (NoneEmpty DomainChar) That's a grammar for a very limited set of e…
4View on Reddit

u/maerwaldin r/haskell • Mentions

On “Why does Haskell, in your opinion, suck?”

Pretty simple example: typesafe printf _without_ additional syntax, TH magic or type wrappers. Also see link to this video
3View on Reddit

u/Volsandin r/haskell • Mentions

On “Practical examples of how dependent types are going to help Haskellers who don't know anyhting about dependent types”

Another one would be a type-safe printf library like this
3View on Reddit