I see a lot of libraries coming out that don’t use them, people really aren’t sure about what they are, and I’d like to give a little introduction and show how you can use these things without being scared about them.
He begins by letting you know what he means by path-dependent types, and dependent types, then he dives into the juicy stuff. I’ll quote from his abstract, "It's been said before that we can program guided only by the types and the things we'd like to do with those types. But what happens if we make the types depend on the context? [...] In the process of exploring these questions we'll get more comfortable with dependent types, what they are and gain insights into our every day code."
There’s also some awesome allusions to a particular book by Lewis Carroll. Here’s a little snippet as to how it fits in,
“One of my favorite children’s books has got to be Through The Looking-Glass. One of the things that I like about it, and that’s so entertaining, is that the author decided to take a lot of the rules that people are used to… and just throw them out.”
Not completely, he adds (like losing your head, for example, everyone knows that's bad), but the types of things that you wouldn't nessesarily expect, that if someone were to say 'oh, that's my perspective,' then you could might agree that the way "I feel" is equally absurd.
Find out how all this applies to dependent types in Owein's talk.