Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

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

share|improve this question
    
You might find this book useful. –  World Engineer Jun 1 '13 at 1:12
    
Perfect, book ordered. Thanks. –  ScarletAmaranth Jun 1 '13 at 1:23
add comment

1 Answer

up vote 2 down vote accepted

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.

share|improve this answer
    
Thank you very much kind sir. –  ScarletAmaranth Jun 1 '13 at 1:23
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.