i spent some time at the blackboard tonight and found that while this is a beguiling approach, it cannot quite work in its current form. The problem stems from the fact that I am attempting to compose modules like this:
(((Thy1 Thy2) Thy3) Thy4)
But this actually leads to plenty of cases where it is not possible to implement the proper fall-through logic. I think that a typechecker of this kind of inherently not quite compositional, since the only way to build one modularly appears to be not incrementally/compositionally as I attempted to demonstrate, but rather all at once in the end. So we can go on having separate modules Thy1, Thy2, Thy3, Thy4, but they will need to be assembled into a typechecker all at once:
[Thy1 Thy2 Thy3 Thy4]
So I'll probably have to resort to lists of first class modules. It'll be modular, but not compositional. Perhaps compositionality was too much to hope for! I don't think I have ever seen a compositional one (in the sense that I have described) in the literature, so it may have just been a rookie mistake.
i spent some time at the blackboard tonight and found that while this is a beguiling approach, it cannot quite work in its current form. The problem stems from the fact that I am attempting to compose modules like this:
But this actually leads to plenty of cases where it is not possible to implement the proper fall-through logic. I think that a typechecker of this kind of inherently not quite compositional, since the only way to build one modularly appears to be not incrementally/compositionally as I attempted to demonstrate, but rather all at once in the end. So we can go on having separate modules
Thy1, Thy2, Thy3, Thy4, but they will need to be assembled into a typechecker all at once:So I'll probably have to resort to lists of first class modules. It'll be modular, but not compositional. Perhaps compositionality was too much to hope for! I don't think I have ever seen a compositional one (in the sense that I have described) in the literature, so it may have just been a rookie mistake.