So, eek! Fifteen minutes left to today, and I have yet to complete my entry on 'D' is for dependent types.
SO, 'D' is now for 'Darn it, I have to write a blog entry!'
AND, since this is a math blog, I darn well tootin' better write some math in it.
1 + 1 = 2.
And, okay, here's a taste of dependent types.
Types tell us what kind of objects are in that set of like-things.
The type, or class, of chickens in the coop lay eggs.
But dependent types go one further: the type depends on the thing it describes.
So the dependent type of even-numbered things are the sets of things that only have even numbers of things in them. How do we know the type? The type depends on the things. How do we know the things? The things are described by the type.
What do dependent types give us, beside circularity?
If I know I have an even number of things I'm working with, I don't need to as is_even. Or if I do, I know my answer, from the type itself.
For the type of even-numbered things, is_even always is true and is_odd is always false.
So, one thing I don't need to do is to check what I'm working with, or how many I have, odd or even, because I already know from the type itself.
Dependent types are from a new kind of logic called intuitionistic logic developed by Per Martin-Löf. The math for it is rather heady, and using dependent types in programming is 'harder' at the get-go than using ordinary types, but, being very restrictive, they also give a much stronger correlation between knowing that your program is correct: that it's doing what it's supposed to be doing, or what you want it to be doing, and, with dependent types, I find I am able to express things, correctly and safely that I am not able to do (correctly and safely) using ordinary types.
My working draft for this blog entry had started out as follows: