A question I've thought about far too much:
In a programming environment which only gives you "data structures", "types", "functions" or "objects", what's the best way of recording "assertions"?
ie statements of logical fact like:
* A is a B
* A has property C
* A and B implies C
* A asserts that B asserts C
etc.
My feeling is that assertions are very small things, from which other much bigger things like types, functions and objects can be made. But it can be hard to make small out of big.
The idea I've thought about too much is 'can't you just record assertions as functions? Everything computable is a function ultimately right?'
and yes you probably can BUT
there's probably a reason that 'types' were invented as a second kind of thing and tacked on to functions, and it might be that because raw functions on their own get tricky, they run away on you if you give them too much power.
But if you for some reason wanted a computing environment and/or theory that didn't start out at its foundations with 'two kinds of things' that didn't quite mesh together, then you might either try to drop Functions or drop Types, OR you might drop both and try a third option.
The Gradual Typing and Dependent Type people seem to be trying the first approach, slowly extending the idea of the Type until it trespasses on the turf of the Function.
I wonder if there might be another way though.
That's something that bother me too.
Types are logical predicates over memory areas (and maybe other resources).
They can be true or false and they can be kept true at compile time, checked at runtime or both.
Ultimately, inheritance is just implication: if A extends B, then all predicates that are true for a memory area of type B must be true for a memory area of type A too, so A => B.
Liskow substitution principle is just plain implication.
