I've seen a number of posts in which people
have been arguing over the power of sequent
calculus and the claim that the type theory
of Qi is more powerful than ML or Haskell.
This claim is correct, but to
show why, I've written a short page on
the background of Qi and a sketch of
an application of sequent
calculus to the type theory of interval
arithmetic. Its not meant to be definitive,
but more indicative of what you can do in Qi.
You can find the page at
www.lambdassociates.org/advtypes.htm
Mark
"Mark Tarver" <··········@ukonline.co.uk> writes:
> I've seen a number of posts in which people
> have been arguing over the power of sequent
> calculus and the claim that the type theory
> of Qi is more powerful than ML or Haskell.
>
> This claim is correct, but to
> show why, I've written a short page on
> the background of Qi and a sketch of
> an application of sequent
> calculus to the type theory of interval
> arithmetic. Its not meant to be definitive,
> but more indicative of what you can do in Qi.
>
> You can find the page at
>
> www.lambdassociates.org/advtypes.htm
>
> Mark
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.
Sincerely,
Matthias Blume
PS: By the way, can you prove subject reduction for Qi?
Hello Mark,
"Mark Tarver" <··········@ukonline.co.uk> wrote in message
·····························@g43g2000cwa.googlegroups.com...
> www.lambdassociates.org/advtypes.htm
>
> Mark
>
Interesting stuff.
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).
Rene.
I've gathered together some of the threads both here and in Lambda the
Ultimate to answer some points raised in discussion. You can find my
answers in
www.lambdassociates.org/response.htm
That will be all from me for the time being. I'm moving
home and seeking work and this internet connection will
cease to exist in a couple of weeks. Have a great summer.
Mark