On 27-Mar-2000, Jan Brosius <[EMAIL PROTECTED]> wrote:
> Hi,
>
> Suppose a denotes a type variable.
>
> 1.Can I then say: Bool is of type a ?
No. That would be a category error. `Bool' _is a_ type, but it doesn't
_have a_ type.
Only _values_ have types, but `Bool' is a type, not a value, and types don't
have types.
Instead, types and type constructors have "kinds"; you could for example say
`Bool' has kind `*' (the kind of all types), as oppose to `List', which has
kind `* -> *' (the kind of type constructors which take a type as their
parameter and give you back a type). Note that Haskell doesn't have any
explicit syntax for kinds; the syntax using asterisks (`*') is used in the
Haskell Report, but it is not part of Haskell syntax and cannot be used in
Haskell programs. Nor does Haskell have any kind variables.
> 2. I suppose I can say that True is of type Bool.
Yes.
> However True is not itself a type, isn't it?
That's correct.
> I suppose that I cannot say that True is of type a, isn't it ?
Well, you can certainly say that `True' is of type `Bool',
and in certain circumstances you can also say that `True'
is of type `a' -- this would imply that `a' was bound to `Bool'.
> So True is a "value" but not a "type value" , isn't?
Right.
> 3. Now consider the type of state transformers ST s a : in the
> above s is a type variable that ranges over the values(?) of type
> State .
No; s is a type variable that ranges over the _types_ of kind `*'.
> Since IO a = ST RealWorld a , I deduce that RealWorld
> is not a type variable (because the first letter is a capital) but a
> very specific type
Correct.
> : i.e. RealWorld is of type State
No, RealWorld is a type of kind `*'.
I'm not sure where `State' came from.
> and RealWorld itself contains values
Yes; at very least, it must contain bottom.
> but not of type State ;
Indeed, the values in the `RealWorld' type are of type `RealWorld',
not of type `State'.
> shouldn't I then say
> that s ranges over "type values " of type state instead of
> "values" of type State.
You should say that s ranges of types of kind `*'.
> 4. Consider the type f :: a -> b -> c.
Since you're asking about terminology:
`f :: a -> b -> c' is not a type, it is a _type signature_.
`a -> b -> c' is a type and `f :: a -> b -> c' is a type signature
which declares `f' to have the type `forall a,b,c . a -> b -> c'.
> Can I say that f is of type a -> b
> since b is a more general type than the type b -> c
The short answer is no.
There are several issues here. One is that you need to be careful about the
scopes of type variables; if `f' has type `a -> b -> c', then that type is
_not_ an instance of the type `a -> b' if `a' and `b' denote the same
type variables in both types.
Another issue is that a type signature such as `f :: a -> b -> c'
declares `f' to have the polymorphic type `forall a,b,c . a -> b -> c',
which is different from the polymorphic type `forall a,b . a -> b'.
Every instance of the former is an instance of the latter, but
not vice versa.
> And if this is true I suppose that "being of type " is a transitive relation
>among types, isn't?
No. It doesn't even make sense to say that a type "is of type" some other type.
However, you can say that a type is an instance of some other type,
meaning that you can obtain the first type by some binding of the
type variables in the second type. This "instance of" relation is transitive.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
