Lets type unit tests
Maybe this is plain stupidity, but hey it's different from the usual path.
If you have full control of the type system, what can we do?
Well type is a flow of information so basically here you have the possibility to do meta tracking.
But lets consider another idea. Assume that we make an abstract class, with no implementation.
(class stack A Abstract (clear )->NIL (push A)->NIL (pop )-> A)
This follow sort of the standard specification used in Java C++ C# etc.
Now consider another "concrete" class
(class mycl A Impl (clear )->NIL (push A)->NIL (pop )-> A))
Then typically you subclass mycl from stack and you go. The idea now is that in order to be able to subclass mycl from the abstract class you would have to pass a unit test e.g.
(class mycl) => (class stack) if (stack-unit-test mycl)Customizing the type theory adding these tests with cashing would be .... different.
As a side note, this is how I view object orientation abstractly. You have a set of code snippets in the form of different function implementations and object orientations just put names on subsets and makes arrows between the snippets, now the process of making subclasses is just rules that makes arrows and rules how to select which code to evaluate or the context to evaluate a function when using one or several name references.
If we all looked nice and same, the ugliest person would become attractive