[Haskell-cafe] What are Kind errors and how do you fix them?

[Stefan Holdermans]

Alex,

  AJ> Ok, I am still trying to understand kind errors and now have 
  AJ> a very simple class and types:

Okay, let's have a look.

You declare

> class MyClass a b
>   where emptyVal :: a b

In the type signature for emptyVal the type variable a is applied to b. So,
we infer

  a :: k -> l
  b :: k

for kinds k and l. Applying the default binding k = * to k and l (so that k
= * and l = *) yields

  a :: * -> *
  b :: *

So far, so good.

Then you declare

> type MyType a = [a]
> type MyType2 = []

Since [] :: * -> *, we infer

  MyType  :: * -> *
  MyType2 :: * -> *

Then you write

> instance MyClass MyType2 b
>   where emptyVal = []

(For clarity, I write b where you used a.)

Recall that we inferred that the first argument (a) of MyClass should have
kind * -> *, while the second argument (b) should have kind *. Here, you've
substituted MyType2 :: * -> * for a. So the kinds match and everything is
okay.

But then:

> instance MyClass (MyType b) b
>   where emptyVal = []

The second argument (b) should have kind *. Since, no further information is
available, we thus assume b :: *. MyType has kind * -> * and is applied to
b; so, (MyType b) :: *. However, we expected the first argument of MyClass
to have kind * -> *. So, this instance declaration won't compile.

When you write

> instance MyClass MyType b
>   where emptyVal= []

the kinds are okay, but this won't compile since type synonyms are not
allowed to be applied partially.

Finally, assuming FiniteMap :: * -> * -> *, from

> type StringMap a = FiniteMap a String

we infer StringMap :: * -> *. Since, synonyms have to be applied fully, you
can only substitute StringMap for the second argument of MyClass.

HTH,

Stefan


> -----Original Message-----
> From: haskell-cafe-bounces at haskell.org 
> [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of S. 
> Alexander Jacobson
> Sent: Saturday, March 27, 2004 5:09 AM
> To: Jon Fairbairn
> Cc: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] What are Kind errors and how do 
> you fix them? 
> 
> Ok, I am still trying to understand kind errors and now have 
> a very simple class and types:
> 
>    class MyClass a b where emptyVal::a b
> 
>    type MyType a = [a]
>    type MyType2 = []
> 
> I can't figure out why some instance work and others don't.  
> e.g. this one works:
> 
>    instance MyClass MyType2 a where emptyVal=[]
> 
> But this one doesn't:
> 
>    instance MyClass (MyType a) a where emptyVal=[]
> 
> and neither does this one:
> 
>    instance MyClass (MyType) a where emptyVal=[]
> 
> How do I make (MyType a) work?  For example, a real world example is:
> 
>    type MyType a = FiniteMap a String?
> 
> -Alex-
> 
> _________________________________________________________________
> S. Alexander Jacobson                  mailto:me at alexjacobson.com
> tel:917-770-6565                       http://alexjacobson.com
> 
> 
> On Tue, 23 Mar 2004, Jon Fairbairn wrote:
> 
> > On 2004-03-23 at 16:58EST "S. Alexander Jacobson" wrote:
> > > Implementing Reverse from before, I am running into this weird 
> > > error:
> > >
> > >   type ReverseType a string = (string ->(string,a))
> > >   data Reverse a string = Reverse (ReverseType a string)
> > >
> > >   instance Monad (Reverse a s) where
> > > 	return x = Reverse (\text -> (text,x))
> > > 	(Reverse p) >>= k = Reverse p3
> > > 		where
> > > 		p3 s0 = p2 s1
> > > 			where
> > > 			(Reverse p2) = k a
> > > 			(s1,a)=p s0
> > >
> > > Produces the error:
> > >
> > >     Kind error: Expecting kind `* -> *', but `Reverse a 
> s' has kind `*'
> > >     When checking kinds in `Monad (Reverse a s)'
> > >     In the instance declaration for `Monad (Reverse a s)'
> > >
> > > I have no clue what this error message means.
> >
> > Kinds are to types what types are to values. You've 
> declared Reverse 
> > to have two arguments: it takes a type, then another type 
> and returns 
> > a type, so its kind is * -> * -> *. (Reverse a) has kind * -> * and 
> > (Reverse a s) has kind *.
> >
> > Now a monad is something that takes a type as an argument, 
> so has kind 
> > * -> *, for example IO has kind * -> * -- you expect to see IO 
> > Something most places. So (Reverse a) could perhaps be a monad, but 
> > (Reverse a s) cannot be.
> >
> >
> > --
> > Jón Fairbairn                                 
> Jon.Fairbairn at cl.cam.ac.uk
> >
> >
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>