Sometimes I do difficult stuff, sometimes I don't. Got a bit bored with it so I fixed some stuff to make it somewhat easier to debug. Thinking about typing and combinators again.
One of the things I want is that a list of type "list (?t => ::I t => t)," a list made out of arbitrary elements implementing interface I is accepted by "!t => list t". I should try some type derivations to see if that works, assuming naive semantics for a HM style checker.
Thing is, I don't care too much if all most general types for functions are automatically derivable; it is a property lost in most higher-ranked systems anyway. Though, it is a nice property to have, since it hints that your type system is complete. I should see how far I can trivialize the type checker by not having it generalize local definitions, and just check the instantiation constraints for applications. Just to see if that makes it possible to get away with higher-ranked types trivially. [1]
Not sure yet, didn't write anything down, didn't look at code, but my gut feeling is that I just need a more fine-grained type checker, where types are not instantiated in one rewrite, but in a series of rewrites where deemed necessary during the unification process.
Next thing, I have been looking at the code for the document generator. It is overly complex, and I can think of several manners to reformulate it, none of them very good. It boils down between choices of functional style, combinatorial style, even monadic style, and whether, in the end, you want to treat the generation of data as the generation of a stream or a tree. Best would be if, on the specification side, you would be oblivious to the underlying representation but it always seems to boil up to the surface.
[1] That might actually be a neat trick. Generalization is a cumbersome computationally intensive procedure, having no generalization may just do it.
No comments:
Post a Comment