|In Response to My Critics|
From my page load information, I can see that the Qi announcements have gathered a fair amount of comment on various threads in different groups. I left some of these threads to mature, to gather the best sample of user response I could get and to give people the time to make a measured response. I've constructed this page to bring together some of the discussion on those threads.
Qi has the most powerful type theory of any language that will ever be invented.
Should not people stop to use illy-defined terms when talking on CS topics? :-)
Seriously, I would say that usual PL comparison considerations apply. There are zillions of languages that are Turing complete, but only zealots can say that makes them the most powerful (or expressive) PLs "that will ever be invented". There are zillions of criteria to differentiate PLs in power and expressivity even within this class of Turing completeness. Why should not the same reasoning apply to type systems?
And no, I didn't look at Qi yet, so I may have more substantial arguments, but I think even this generic one is good enough.
No it is not. There are a few things wrong here. The phrase 'most powerful' in the context of the discussion of Qi, refers to the Turing-equivalent nature of the type notation of Qi versus the less-than-Turing-equivalent type notation of (e.g) ML. This claim has a precise and provable meaning which is well-established in the literature. See John Lloyd, Theorem 9.6 in 'Foundations of Logic Programming' for a proof that pure Horn clause logic is Turing-equivalent. Qi sequent calculus can represent any pure Horn clause program.
The second thing that is wrong with this argument is that the Turing-equivalence of Qi has been contrasted with ML only in respect of the type notation, not w.r.t. the programming body of the languages themselves. So 'zillions of languages are Turing complete' misses the point.
There is another sense of 'powerful' which is implicit in your post; the sort where we say 'Lisp is more powerful than assembly'. This is a valid though hard-to-define use of the word. In this sense it is not possible to sensibly assert that Qi or any language is the most powerful that can be invented. This vaguer use of 'power' is probably bound up with how much space it takes to encode some algorithm. In this sense, Qi is still very 'powerful' type-theoretically, since Gentzen's notation has been with us for 60 years and I don't see a better one. But it is perfectly possible someone will claim they have a more compact notation than sequent calculus.
I'm no expert either, but it looks like Qi simply lets you define your own type rules in a Turing-complete language. Therefore, technically, you can create any type system you want. This would make it a convenient vehicle for experimenting with new type systems.
An excellent summary of the facts.
If the Qi type system is
turing complete, surely that means that, because of the
halting problem, type checking is not guaranteed to
complete, and that it's impossible to determine if the
type checking for any particular program will or will not
Used in its native state (i.e. without any user-defined types) Qi type checking is guaranteed to terminate. This is shown by the proof of the AB theorem in Functional Programming in Qi. However it is true that it is possible to add type rules that create non-terminating computations. One such rule for union types is discussed in chapter 13.
There are several responses here.
1. The first is that, practically, unless you're venturing into the deep waters of type theory, you're not likely to run into this problem. Generally non-terminating type rules are fairly rare because most programmers will paddle in the shallows. I cannot recall ever having been caught out by this problem even in the hairiest problems.
2. Second, if you were to use them, the effects are generally pretty quick to show. Qi has a nice trace package (enter (spy +) to the top level) for tracing type checking so you can see what is going on if you get lost.
3. Third, in some cases (including the case cited in chapter 13 of FPQi), infinite regresses are not the end of the world. They can in some cases be plugged.
4. Fourth, it would be possible to augment Qi with the sort of termination check used in the Boyer-Moore ATP. This would provide a sufficient (though not necessary) automatic check of termination which could be employed to reassure people that their type theory would terminate. This is a topic for research.
Type-checking your type rules? It could happen. By Paul Snively
C++ Templates...are also a Turing-complete metalanguage, and C++ compilers, in practice, have a flag that limits "template instantiation depth" precisely in order to ensure that the C++ compiler terminates. However, C++'s type system still isn't as expressive as the dependent type systems that you usually see exhibiting Turing-completeness, so it's not clear what the win there is. Still, you can do amazing things with C++'s template system, as a quick look at boost::spirit or Loki's Gen...Hierarchy tools reveal.
Well, to be strictly accurate, I compared Qi only to other functional programming languages in my announcement.
Yes, of course you can make a language whose type theory is as powerful as Qi. All you have to do is to create your own Turing-equivalent type notation or twiddle my source code and create your own Qi. I did not mean to imply that the power of Qi type notation could not be equalled. Only that it could not be surpassed.
I'm not enough of a C++ programmer to comment on the power of C++ templates vs. sequent calculus. My view on C - expressed in FPQi chapter 1 - is that C was a very good portable assembly language for UNIX that got out of hand and was used for all sorts of things that it was not really designed to tackle. I see C++ as an attempt to patch the deficiencies of C by retrofitting some desirable features onto C. This does not answer the question perhaps, but it may explain why I'm not the right person to make a judgement.
Rene de Visser
Is it possible to do pattern matching based on type (as in Haskell)?
Is it possible to define immutable types in Qi? (Or is Qi already Applicative?)
Is it possible to define lazy types in Qi? (Though I am not sure whether this question is so well defined, as there seems to be some debate as to whether lazyness should be considered as a property of a type).
Yes; associating types with patterns is in Qi. The difference is that in Qi you don't have constructor functions. See Chapter 11 in FPQi for how to do this. Chapters 14-17 use this all the time.
I looked up 'immutable types' on the Internet. Not a lot of material, but here were two accounts.
Whereas an immutable type cannot be modified after construction, a mutable type can have its value changed.
Imutable [sic] objects never change once they are created. When one wishes to modify an immutable object, one is compelled to create a whole new object that reflects the modification.
The phrase seems to be associated with the C++/Java/Python school. If I've got this right then the following is an answer.
The basic type theory of Qi detailed in chapter 13 of FPQi cannot be changed without changing the source. "Hello World" will always be a string. But it can be added to. You can add a type theory called FOO say, and then add to or overwrite FOO. If you overwrite FOO Qi will complain at you because this can invalidate the type security of previously loaded code, but Qi will accept the change. You can set (strong-warning +) to turn a warning into an error message and block this sort of move.
In general there are no immutable types in Qi because any type can be extended. If you wanted to make string an immutable type, without hacking source, the best way to do so would be to use the macroexpansion command in appendix B of FPQi. This allows you to change Qi syntax and its behaviour to suit your style.
Lazy types. In Qi II - yes.
By Matthias Blume
You claim that Qi's type system is the "most powerful possible" because its type language is Turing-equivalent. But to me, that's not an asset, it is a liability. It is a great *weakness* of such a "type system", because it makes type checking undecidable.
The art of designing a good type system is in balancing expressiveness ("strength" in your sense) with simplicity and tractability.
That's why I continue to find your claims about Qi more than just a bit hyperbolic.
PS: By the way, can you prove subject reduction for Qi?
In and of itself, non-termination and being able to collapse the type system are not assets, but it are the inevitable by-product of expressiveness, which is an asset. So to form a judgement on the relative merits of ML/Haskell vs. Qi requires a value judgement. Its not possible to assert the superiority of either paradigm without commiting the prescriptive fallacy.
The arguments for and against Turing-equivalence in type checking are very similar to the arguments for and against Turing-equivalence in programming. You can buy guaranteed program termination in programming at the cost of accepting weak programming languages (loss of expressive power). Most programmers do not want to do this, otherwise by now weak programming languages would be the norm.
Programmers are happier to buy into weak type systems though, because programmers have very dim idea of what this extra expressive power buys for them. What you've never had, you never miss. Also, until now, there was not much real choice; weak type systems like ML and Haskell were all that you could buy. Maybe that will change now. But which you prefer requires a value judgement.
Yes, subject reduction holds in Qi. See Functional Programming in Qi for a proof.
all I have time for now.
(c) 2005, Mark Tarver