I seem to have gotten a very basic qualified type thing working. still need to noodle with it more, though.
Qualified types introduce a type predicate that needs to be checked after inferring each expression. For example, let's say the signature of '+' is 'a, a -> a' where 'a' is any type. Addition only makes sense for certain types of data, so we can then specify which types are valid with a predicate. For example: where 'a' is a float or an int. Adding two booleans is valid as far as the function signature is concerned, but it will then fail the predicate check.
One limitation of this approach seems to be (meaning I haven't found a paper/article stating otherwise yet) that it cannot express all of the possibilities of function overloading. For example, in GLSL it is valid to multiply a matrix by a vector. It is also valid to multiply a vector by a matrix. Both forms return a matrix, but the signatures are different. The first is 'a, b -> a' and the second is 'b, a -> a'. This would require two differently named functions in a qualified type system.
What might be useful is allowing for a signature like 'a, b -> c' and associate substitutions with predicate conditions. If 'a' is a vector and 'b' is a matrix then substitute 'b' for 'c'. If 'a' is a matrix and 'b' is a vector, substitute 'a' for 'c'.
@dthompson Yeah, this is what I'd try to do.
@zenhack cool, thanks! and thanks for pointing me towards qualified types.
@dthompson You're welcome!