'D' is for Darn it, I have to write a blog entry!

eheh, eheh, eheh!

So, eek! Fifteen minutes left to today, and I have yet to complete my entry on 'D' is for dependent types.

*sigh*

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.

Well:

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?

Clarity.

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:

'D' is for Dependent Type

We're all familiar with types, right? They're classes, or classifiers, telling us what something in (into which class it belongs).  One example is this weekend I'm going to be running a 5k with my family, which is a very different thing than running a 5 miler or running just 5 feet. Kilometers, miles, feet, these are units of measure, and they type or classify what we're talking about. 'Units of measure,' also, in fact, is a type, so the types 'kilometers,' 'miles' and 'feet' all fall into the type 'units of measure.' Just like our pets are a type of animal: cats. 'Cats' is a type, and itself is a type of something else: 'animal,' or 'pet,' ... depending.

Programming with types is an on-again off-again kind of thing, some programming languages require all things/objects to be typed, some languages require none to be typed and some fall in the middle somewhere between those extremes.

And, as you may guess, different programming languages have different kinds of types or different ways of typing things or different ways of creating types.

What do types give you?

Some say they give you a pain in the ... neck, and nothing more; others say that, by putting things into categories, they provide a distinction of objects operated on, so you know what you can do, and can't do, with the object at hand, simplifying the programming task.

Me, I'm a typeful person, if you hadn't surmised this from the title of the blog which contains this entry. Types are wonderful! They provide a way for me to declare what things are, and, from simply knowing the types of the data I'm working with, I now know a lot about the system and what it does and what its usefulness is.