On 18-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> OK, I'm curious. Two people replied that C++ has undecidable type
> checking. I was not aware of this (although I can't say I'm too
> surprised); do you have a reference?
Not really. I believe this has been mentioned on comp.std.c++,
but I did not succeed in finding the revelant articles with the
quick DejaNews search that I did.
But basically the relevant feature is templates and template
specialization. Templates give you recursion at compile time,
and template specialization gives you the equivalent of if-then-else,
and that's about all you need. I've included below an example which
computes factorials at compile time, using successor arithmetic in the
type system. I believe it would be straight-forward, albeit tedious, to
extend this example to compute arbitrary recursive functions on natural
numbers.
The relevant part of the C++ standard is Annex B:
| -1- Because computers are finite, C++ implementations are inevitably
| limited in the size of the programs they can successfully process.
| Every implementation shall document those limitations where known.
| This documentation may cite fixed limits where they exist, say how to
| compute variable limits as a function of available resources, or say
| that fixed limits do not exist or are unknown.
|
| -2- The limits may constrain quantities that include those described
| below or others. The bracketed number following each quantity is
| recommended as the minimum for that quantity. However, these
| quantities are only guidelines and do not determine compliance.
...
| * Recursively nested template instantiations [17].
Here's the example code. Note that to compile this, you will
need a compiler that supports much more than 17 recursively
nested template instantiations.
// successor arithmetic:
struct Zero {
typedef Zero check_is_zero;
};
template <class T> struct Succ {
typedef T pred;
};
typedef Succ<Zero> One;
typedef Succ<One> Two;
typedef Succ<Two> Three;
typedef Succ<Three> Four;
typedef Succ<Four> Five;
// some examples of recursion with if-the-else:
// addition
template <class T1, class T2>
struct Sum {
typedef typename Sum<typename T1::pred, Succ<T2> >::t t;
};
template <class T2>
struct Sum<Zero, T2> {
typedef T2 t;
};
// multiplication
template <class T1, class T2>
struct Prod {
typedef typename Sum<T2,
typename Prod<typename T1::pred,T2>::t>::t t;
};
template <class T2>
struct Prod<Zero, T2> {
typedef Zero t;
};
typedef Prod<Two, Five>::t Ten;
typedef Prod<Two, Ten>::t Twenty;
typedef Prod<Ten, Ten>::t Hundred;
typedef Prod<Ten, Hundred>::t Thousand;
// factorial
template <class T>
struct Factorial {
typedef typename Prod<T,
typename Factorial<typename T::pred>::t>::t t;
};
template <>
struct Factorial<Zero> {
typedef One t;
};
// equality
template <class T1, class T2>
struct ZeroIfEqual {
typedef typename ZeroIfEqual<typename T1::pred,
typename T2::pred>::t t;
};
template <>
struct ZeroIfEqual<Zero, Zero> {
typedef Zero t;
};
template <class T1>
struct ZeroIfEqual<T1, Zero> {
typedef One t;
};
template <class T2>
struct ZeroIfEqual<Zero, T2> {
typedef One t;
};
// now some examples where the type-correctness of the program
// depends on the results of the arithmetic
// check that 2! == 2
typedef typename ZeroIfEqual<typename Factorial<Two>::t, Two>::t res;
typedef typename res::check_is_zero checkme;
// check that 5! == 120
typedef typename Sum<Hundred, Twenty>::t HundredAndTwenty;
typedef typename ZeroIfEqual<typename Factorial<Five>::t,
HundredAndTwenty>::t res2;
typedef typename res2::check_is_zero checkme2;
--
Fergus Henderson <[EMAIL PROTECTED]> | "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh> | but source code lives forever"
PGP: finger [EMAIL PROTECTED] | -- leaked Microsoft memo.
