Skip to content
Hallway
0:00 / 0:00

#idris#dependenttypes#universepattern

David Christiansen - Coding for Types: The Universe Patern in Idris - Curry On

Curry On!

6.3K subscribers • 21 videos on Hallway

YouTube
  • Recommended by 2 people: 1 in engineering communities and 1 curated list.
  • Presented by David Christiansen

Advanced. Deep dive for people who know the field.

14K views11 years ago2 recommendations

Programming languagesComputer scienceLanguage design and type systemsFunctional programmingComputation and complexity

David Christiansen explains the universe pattern in Idris, showing how to compute types from data for type-safe programming.

Curry On Prague, July 7th 2015 curry-on.org 2015.ecoop.org

Why it's here

2 people recommend this

What people say. Recommended as an excellent explanation of the universe pattern and dependent type programming in Idris.

u/gopher9in r/haskell • Recommends

xpost from /r/idris Coding for Types: The Universe Patern in Idris - Curry On
25View on Reddit

programming-talkscurated list on GitHubRecommends

Under “Idris”

Coding for Types: The Universe Patern in Idris 00:48:04 by **David Christiansen** (2015)
View the list

u/int_indexin r/haskell • Mentions

On “Dependent Haskell vs Idris”

No, it doesn't. You need The Universe Pattern to simulate type families.
3View on Reddit

u/Faucelmein r/haskell • Mentions

On “[blog] Variable-arity zipWith in terms of Applicative ZipList”

Thanks. I seem to remember that Idris can use something called the universe pattern to handle "pattern matching on a type"-like problems, but I don't know if that technique is applicable here.
3View on Reddit

u/htuholain r/ProgrammingLanguages • Mentions

On “How to write a programming language?”

With every programming language having types and values that they manipulate, I'd have thought it's useful to know type theory at least. If you need a book on it, maybe Little Typer? I'm not sure it's enough though. TAPL is usually mentioned as well, I didn't see it this time so I mentioned it now. A Little Taste of Dependent types -video by David Thrane Christiansen I was told this might be interesting as well: Coding for Types: The Universe Patern in Idris.
2View on Reddit