Ok so I keep having the same idea over and over again. Maybe that means I like it.
This time I'm phrasing it like this: combining spencertipping's perl objects with functional ideals and distributed references a la Udon. These objects can have computational content (like perl objects, unlike Udon) and are defined in terms of an explicit abstract basis (unlike both).
Having tried to write this several times, I really want to be minimal about it. Not minimal as in perfect and beautiful -- minimal as in a small amount of work. I can give it water and sunlight later.
But first, as with all my recent projects, I have to determine what I mean by an abstract basis. I'm beginning to believe the idea is not reliant upon, but connected to the idea of types. A basis without types is just made of names, which are sufficiently ambiguous that they cannot be methodically searched or computationally combined (nor is their usage clear without examining their definition). Types allow the computer to see what is going on so it can help. I think that, with sufficient coqesque sectioning, polymorphism won't get in the way (I may be wrong).
Let's say a basis for naturals looks like this:
Nat : *
0 : Nat
S : Nat -> Nat
Whatever is defined in terms of this basis can be instantiated for any values of type Nat, 0, and S that match those signatures. Note that, aside from ->, this is self-contained. That's the point -- every object declares the basis upon which it is built, so that there are no true globals and it's always clear in what ways code can be reused. I'm not saying it is up to the user to type the basis every time, definitely not! This is an interactive system, and I'm picturing the basis being inferred (perhaps simply, eg. you do somewhere declare these things, and then the interactive system just notices which ones you need).
I'm considering being weird and not asserting the existence of any disconnected types. Eg. the trivial instantiation, where every object has the same implementation, is possible. I think this will contribute to constructive reasoning over platonic reasoning, which is more fit for computational systems.
Then there is the age-old problem of stitching. How is something actually defined, and in particular, how is code reused? Must anything to be reused be given a type and in theory be substitutable with anything else of that type? Though false, I suppose that is the ideal. Ideally, tight abstraction bounds allow us to express even more in the type than we are used to in Haskell. In other words, the ideal I'm expressing is that code does not reference other code directly, it always abstracts.