Skip to content
Hallway
0:00 / 0:00

#idris#dependenttypes#typetheory

"Idris: Practical Dependent Types with Practical Examples" by Brian McKenna

Strange Loop Conference

88K subscribers • 114 videos on Hallway • Conference channel

YouTube
  • Recommended by 2 people: 2 in engineering communities.
  • Presented by Brian McKenna

Intermediate. Assumes working knowledge.

30K views12 years ago2 recommendations

Programming languagesComputer scienceFunctional programmingLanguage design and type systemsComputation and complexity

Brian McKenna demonstrates practical examples of dependent typing using the Idris programming language.

Dependent types turn types into a first-class language construct and allows types to be predicated upon values. Allowing types to be controlled by ordinary values allows us to prove many more properties about our programs and enables some interesting forms of metaprogramming. We can do interesting things like write a type-safe printf or verify algebraic laws of data structures - but while dependent types are quickly gaining in popularity, it can be tricky to find examples which are both useful and introductory. This talk will demonstrate some practical dependent typing examples (and not sized vectors) using Idris, a language designed for writing executable programs, rather than just proving theorems. by Brian McKenna (@puf nfresh) Brian McKenna is a small contributor to the Idris and PureScript languages. He also makes video tutorials on writing programs in Idris so that others can get started with dependent types. Brian works professionally as a functional programmer at a startup, using tools such as Scala and Haskell to create products for utility companies.

Why it's here

2 people recommend this

What people say. Recommended for its practical examples of dependent types, including proving time complexity and writing type-safe code.

Moments people linked to

u/ephrionin r/compsci • Recommends

On “Functional Programming Myths”

> I like FP so much that I've finally decided to learn Haskell, but I think that this is a myth. Computers are dumb and FP can't change that. > Let's say we want to sort a list of integers. Here's the definition of the problem: > * a list is sorted iff ... > * a permutation of a list is ... > * sort list must return a list L such that L is a permutation of list and L is sorted. Haskell's QuickCheck testing/checking library can be used to make these sorts of assertions. It won't actually write the code for you, of course, but it will do a damn good job figuring out how your code doesn't fit if it doesn't. IIRC, QuickCheck is not easily implementable in other languages because of Haskell's…
6View on Reddit

u/mirpain r/functionalprogramming • Recommends

On “Is there any research related to reasoning about code performance using type systems?”

[video In this video about Idris, Brian McKenna shows how he proves time complexity of some function and writes wrapper that allows running this function while not exceeding certain complexity.
2View on Reddit

u/Condexin r/ProgrammingLanguages • Mentions

On “Do i need to be an expert in type theory to make a PL?”

The Short Answer: No. The Long Answer: I really like static typing and type theory. I think it's the right thing to do. However, I also appreciate that understanding types is a non-trivial exercise. There are different types of type theory and there's different implementations of the same type theories. Take Agda vs Idris for example. They're both dependently typed languages, but Idris uses heterogeneous propositional equality and Agda uses homogeneous propositional equality. I actually don't really understand all of what that means, but apparently it has non-trivial implications as to what you can implement using these languages (Homotopy Type Theory is supposedly incompatible with…
14View on Reddit

u/dalaingin r/haskell • Mentions

On “Utility of dependent types?”

These videos might (or might not) be helpful: * Brian McKenna using Idris to demonstrate some useful things * Ollie Charles with a nice example of something useful with the DT-flavoured GHC extensions Mark Hibberd had a great talk at YOW Lambda Jam in Brisbane on writing Tic Tac Toe in Idris. The video isn't up yet, but the slides are.
12View 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/theindigamerin r/haskell • Mentions

On “[PDF] Stephen Diehl - Reasoning about Program Behavior Algebraically”

While mbw_rdt has written a lot of good explanations for the different points, if you're looking for a complementary explanation, there's a Strange Loop 2017 talk by Stephanie Weirich on dependent types in Haskell which includes singletons, among other things. I've seen the Refl bit in an Idris talk (YouTube - Idris: practical dependent types)
3View on Reddit

u/foBrowsingin r/haskell • Mentions

On “Complexity monad”

I'm afraid it's not in Haskell, but there's this video (starts at 20:59), in Idris, where the computational complexity of a given function is encoded in its type. It uses a monad, though it might not be the same as what you're referring to.
2View on Reddit

u/Roboguy2in r/ProgrammingLanguages • Mentions

On “To Be Turing Complete, Or Not To Be, That is the Question”

Proof assistants (and similar) aside, I do have some sympathy for that point of view, actually. I also think there is at least a bit of practical value in that you can sometimes accidentally write an infinite loop. It's probably easier to accidentally write an infinite loop than to accidentally write a O(n\^n\^n\^n\^n) algorithm when you meant to write an O(n^(2)) algorithm. So, it would at least prevent some of those kinds of errors. On the other side of things, more inline with what you're saying, there is some interesting work: There are some (non-Turing complete) programming languages actually turn out to be restricted to a certain computational complexity class, which is a stronger r…
1View on Reddit