Slogans about Mainstream Dependent Types
I find it can be hard for programmers to talk about dependent types, since we don't always have the same idea of what they are and they have a reputation of being hard to understand and implement. I want to share these slogans to (hopefully) make the conversation easier.
I wrote this in a hurry and would welcome comments with examples of "mainstream dependent types" - and any relevant corrections and links.
Note: "mainstream" is a moving target
- "A dependent type is a type whose definition depends on a value."