I would be interested in formally defining (and consequently demonstrating) a "type system" for, well, a type system. More specifically, I would like to explore the idea of what C++ calls concepts for my bachelor's thesis. How would one go about defining such system (formally) ? It's basically a meta-language for generic programming I suppose, but all the material I've found so far is basically bound to syntax of a specific programming language.
The basic idea is to provide an interface for parametric types.
An argument for the function
foo(T) is some (unfortunately any) T. (This type is known statically.) And, I would like to define an interface for such type, so that this T is actually not any T, but some type that complies to an interface, such as: "In order for this type to be legal for the function foo, it needs to comply to: This and that concept / interface to statically check against."
Concepts would define related, meaningful "interfaces" that would constrain the type T. Currently, the language C++ doesn't do any such checks, it simply tries to do whatever it is that
foo(T) does on any type and hopes it works. If it doesn't the error message is of length of a decent novel, as the error is detected too late and the compiler needs to "spit out" the entire process of how it got to an error.
I would eventually like to show the concept (errm, idea, sorry for the ambiguity) on the C++ specifically, if that's any relevant.