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.
For example:
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.
Thanks,
~Scarlet
1
These are known as Kinds or Type Classes (in some areas, not others) or a few other things. They are defined formally as any other function, except the Type Constructors (another searchable term for parameterized types) use kinds as their signature rather than first level types.
These have been formally defined in the past and proper academic research should provide tons of papers on the subject. Lambda the Ultimate should also have resources to help.
The results will largely be bound to a specific language, since they are very language specific. C++’s implementation specifically precludes such things, so you would need to extend/change the language – probably in ways that other languages have already done.
0