Re: more closed-world chatter

On May 8, 12:48 am, Marshall <marshall.spi..._at_gmail.com> wrote:
> On May 7, 12:34 am, David BL <davi..._at_iinet.net.au> wrote:

[snip]

> > My concern is that if types can be manipulated as values at run time,
> > then we have the means to solve complex problems using just the type
> > system. In that case why make a distinction between types and values?
>
> Why indeed?
>
> The type theory world is busy struggling with this question, and
> the concern you mention above, which some people consider
> a virtue. Oh, I guess I'm one of those people, by the way.
>
> Why not have a Turing complete type system?
>
> The usual answer is that it means that type checking may
> not halt. In fact, all the troubles of runtime are then added
> to compile time. However I believe this may not be such
> a big issue as it might seem.

You may be right.

BTW are you aware of the claim that C++ templates are Turing complete? I've used a fair amount of template meta-programming in the past few years and can vouch for the power than one can achieve. Interestingly, the infinite regress problem of types of types is avoided very simply by completely avoiding any typing of template parameters. This seems very justifiable because successful compilation implies that 1) halting problem didn't occur and 2) templates must have instantiated sensibly in order to satisfy strong typing consistency.

Nevertheless it seems to me that a functional programming style would be more satisfying for compile time "expansion" of code - kind of like macro expansion on steroids. Haskell's unification approach to avoid if-then-else statements would be similar to template specialisation.

[snip] Received on Tue May 08 2007 - 14:59:52 CEST