Home » forums » LtU Forum

Advanced Types in Qi

This website claim: "Qi has the most powerful type theory of any language that will ever be invented."

Frankly I don't understand the first thing in this write-up but I'm sure others will find it interesting.

Also, I read somewhere that while Lisp reflects programming language theory of old, Haskell represents PLT thinking of the 90s (poorly paraphrased from memory). I've always assumed Haskell's type system and pattern matching are what's supposed to be '90s thinking,' so where does that put Qi?

By shahbaz at 2005-05-13 22:51 | LtU Forum | previous forum topic | next forum topic | other blogs | 13082 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Extensible type checker?

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.

By Kannan Goundan at Fri, 2005-05-13 23:11 | login or register to post comments

Type tarpit

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.

By Andris Birkmanis at Sat, 2005-05-14 05:31 | login or register to post comments

Halting problem?

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 complete.

On a more prosaic level... what's the point of a turing-complete type system? We use types to help us write turing complete code. If the type declarations themselves are turing complete, will we need type-types to help us write types?

By nat at Mon, 2005-05-16 16:03 | login or register to post comments

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.

By Paul Snively at Mon, 2005-05-16 22:27 | login or register to post comments

Type types

On a more prosaic level... what's the point of a turing-complete type system? We use types to help us write turing complete code. If the type declarations themselves are turing complete, will we need type-types to help us write types?

If I'm not mistaken, this suggestion is far from farcical. Haskell's type system, while certainly not Turing complete, does provide a very simple sort of typing for types. The type types are called ‘kinds’.

By L Spice at Sun, 2009-08-02 17:00 | login or register to post comments