Re: Fixing imports for and namespaces (was: Simon's H98 Notes)

[Fergus Henderson]

On 24-Oct-1998, David Barton <[EMAIL PROTECTED]> wrote:
> Fergus Henderson writes:
> 
> >  No, different uids don't work fine in the multiprogrammer case.
> >  The programmer that is compiling the source code needs read access
> >  to all of it (for using tools like `grep', if nothing else).  Once
> >  he has that read access, nothing prevents him from violating the
> >  encapsulation.
> 
> Let's see here --- you want him to be able to do reads like grep
> but not refer to the units directly?

The programmer should be able to read the source code;
the code that he writes, however, should not be allowed to
violate encapsulation by accessing private parts of other modules.

> You ask too much of *any* mechanism [...]
> Either you can trust the programmer to follow conventions, or you
> restrict any kind of read access; without that restriction, he or she
> can always make a local copy and do what he or she wills.

Making a local copy doesn't violate encapsulation.

One of the big advantages of language-enforced encapsulation
is that I can change the representation of private data and
I can be sure that this won't break code in other modules
or other packages.  Making local copies ("cut-and-paste" reuse)
doesn't invalidate that guarantee.

> But even *if* you decide that some more sophisticated mechanism of
> version control is necessary, it is properly an operating system
> function, *not* a language function.

I need the guarantee that encapsulation provides -- the guarantee that I
can change private implementation details without breaking code in
other modules -- to hold across *all* operating systems.
Otherwise someone might be using my library on a system which doesn't
enforce the encapsulation, and my change could break their code.

> It all boils down to: access control to files is the responsibility of
> the operating system, *not* a programming language.

The entities that I want to protect are not _files_.
The entities that I want to protect are language-level entities
(functions, type definitions, etc.) so I think it is quite appropriate
for access control to these entities to be enforced by the language.

> >  > 2) The compiler can (and should) be intelligent enough to detect
> >  >the importation of symbols only through non-functional
> >  >(gather) modules.  This is not a big test to perform.
> >
> >  So the compiler should enforce this convention?
>
> No; detect it and take advantage of it.

If the convention is optional, then it is much more difficult
for the compiler to take advantage of it -- detection requires
global analysis, which means for example that you can't take
advantage of the convention when doing separate compilation.

> Most of the below is variations on a theme, which make lots of sense
> if you accept the basic assumption that enforcing access control
> conventions is properly a function of the language feature; under that
> assumption, I agree with most of it.

Yep, that is our key difference of opinion.

>Every programmer on the team may need
>to modify any file (in order to fix a bug, for example).  So all
>programmers need write access to every file.
> 
> This does not correspond to any configuration controlled project that
> I have ever worked on, so I am at sea.  In my world, if you need a
> file that is outside your own package, you need to go to the
> configuration manager (who may or may not be the project manager) for
> permission to check out the file to make the change.  This may be as
> simple as an Email, or it may even require review.  Allowing the
> programmer to just do it, on his own hook, is well outside any kind of
> configuration control guidelines I have ever worked under.

Basically the way our system works is that you get permission
to commit the change (i.e. to check the modified file back in,
after you have already checked it out and modified it), not
permission to check out the file in the first place.

But programmers are also allowed to make changes without
getting permission, if they are confident that they changes
are going to be OK.  Very occaisionally, this will mean that
permission is sometimes retracted retrospectively, by backing
out a change that has already been committed.  However, this
happens only on very rare occaisions, and any disruption in
those cases is more than compensated for by the decrease in
the time lost by programmers waiting for permission.

> We work in very different environments!

Indeed. 

Above I have explained in more detail above how the environment
that I work in operates.  I hope that you can see how this sort
of environment could work, and that you will take my word for
it that it does seem to work pretty well for us.

>Yes, you may be right.  But I don't think a language should require
>the use of a particular configuration management style.  And
>therefore I'm not keen on any solution which relies on the
>configuration management style rather than the language to enforce
> 

Re: type error, why?

[Peter Thiemann]

Alex> In other words, you are saying that I want a feature, first class
Alex> polymorphism, that is now available in Hugs1.3c and from the docs,
Alex> GHC4.0?.

Yes.

Alex> Since I am doing development in Hugs 1.4, I guess the question is when
Alex> will Hugs1.4  have this feature and is this feature
Alex> compatible with Derive?

As far as I know, the Hugs 1.4 folks are working on it. Derive is only 
a preprocessor for data type declarations, I don't know whether it
works with existentially typed or polymorphic constructor
arguments. If you don't have these, then I don't see any problems.

Alex> Alternatively, since GHC 4.0 is there a way to run just the type-checker
Alex> part of GHC 4.0 without waiting for it to compile everything?

Alex> Also, has anyone manageed to build GHC4.0 for win32?

Sorry, beats me.

-Peter

Re: type error, why?

[Peter Thiemann]

> "Alex" == S Alexander Jacobson <[EMAIL PROTECTED]> writes:


Alex> I wrote the following function that attempts to generalize show by
Alex> allowing the user to choose the function to stringify constructor
Alex> arguments.

>> stringArgs' sep stringer1 (MyFoo x i s) = 
>> x' ++sep++i' ++ sep ++ s'
>> where 
>> x'=stringer' x
>> i'=stringer'' i
>> s'=stringer''' s
>> stringer' o=stringer o
>> stringer'' o=stringer o
>> stringer''' o =stringer o
>> stringer o=stringer1 o --!! replacing stringer1 w/ show works!

Alex> This function generates a type error because stringer is being used as
Int-> Char and as Char->Char.  But, if I replace stringer1 in the last
Alex> line, with the function `show`, hugs allows this function.

OK, show :: forall a . Show a => a -> String [if my memory serves correctly]
so it is polymorphic in the type a.
However, the parameters of a function cannot (currently) have a
polymorphic type. So when you want to pass show to stringArgs you will 
have to use one particular instance of this type. In the present case, 
you get Show a => a -> String [note that the forall is gone], but you
cannot resolve the overloading because you do not know what a is. Hence

Alex> However, if I use show and attempt to call this function using foo:

>> foo x = stringArgs "\n" show (MyFoo "asd" 12 "asd")

Alex> I get an ambiguous type signature error.

the ambiguity. If Haskell included first-class polymorphism (which is
on the list for Haskell 2 and which is present in some form in Hugs
1.3c) and you provided an explicit signature, then your function and
your example would work out. Modulo syntax, this is what is would look 
like:

stringArgs' :: String -> (forall a . Show a => a -> String) -> MyFooType -> String
stringArgs' sep stringer (MyFoo x i s) =
x' ++sep++i' ++ sep ++ s'
  where 
x'=stringer x
i'=stringer i
s'=stringer s

And your function call would look just like the one above.

-Peter

Re: Haskell 98

[Peter Thiemann]

> "Hans" == Hans Aberg <[EMAIL PROTECTED]> writes:

>> It's not different logical entities, all occurrences of f are variables.

Hans>   Different occurrences of f have different semantic meaning (that is, the
Hans> "f" in one place is not the same as the "f" in another place).

All I'm saying is in "f f = f", the first occurrence of f is a binding
occurrence, the second one is also a binding one, and the third one is 
an occurrence of f bound to the second binding.

>> It's not Haskell that's causing the confusion if any, it's the lambda
>> calculus, more precisely: alpha-conversion.

Hans>   The original question was this: What is the meaning of "f(f) = f"? I
Hans> remarked that in this case Haskell has a very good strategy, namely
Hans> interpreting it as the expression f := f |-> f, or "f is assigned the
Hans> expression  lambda f f" if you so want; the lack of such a good strategy
Hans> seemed to cause the other problems discussed in this thread.

There is no assignment in "f f = f", it's just binding of names. Using 
any notion of assignment in this context is misleading IMHO.

Hans>   Otherwise, the naming of functions is not part of the lambda calculus;

I disagree on that one: the meaning of 

letrec f = \f -> f in e
is
(\f -> e) (fix \f -> \f -> f)

[plug in any fixpoint combinator for fix]

-Peter

Re: Haskell 98

[Hans Aberg]

At 14:30 + 98/10/26, Peter Thiemann wrote:
>> Haskell translates  f f = f  into  f := f |-> f; on the right hand side
>>"f" is a bound variable, on the left hand side "f" is a name. Suppose I
>> f := \f |-> \f
>>> or f(\f) := \f.
>
>I don't really understand your remark. f f = f  as a toplevel
>definition is equivalent to (in this special case)
>
>letrec ...
>   f = \f -> f
>   ...

  I just avoid using Haskell notation in order to not get the notation
confused as Haskell does.

>It's not different logical entities, all occurrences of f are variables.

  Different occurrences of f have different semantic meaning (that is, the
"f" in one place is not the same as the "f" in another place).

>It's not Haskell that's causing the confusion if any, it's the lambda
>calculus, more precisely: alpha-conversion.

  The original question was this: What is the meaning of "f(f) = f"? I
remarked that in this case Haskell has a very good strategy, namely
interpreting it as the expression f := f |-> f, or "f is assigned the
expression  lambda f f" if you so want; the lack of such a good strategy
seemed to cause the other problems discussed in this thread.

  Otherwise, the naming of functions is not part of the lambda calculus;
one must add an interpretation of this lambda calculus in order to arrive
at a meaning of an assignment in the computer sense. (For example, if I
define \f to denote a free variable, I could assign f := \f + 1, and later
bind this \f by the assignment f := \f |-> f, which would work out to the
increment function. In this example, free variables and symbol table names
have a distinctly different behavior.)

  Hans Aberg
  * Email: Hans Aberg 
  * Home Page: 
  * AMS member listing: 

LOPSTR'99: call-for-papers

[Annalisa Bossi]

___

Our apologies if you receive multiple copies.
___


 CALL FOR PAPERS

LOPSTR'99
  9th International Workshop on
 Logic-based Program Synthesis and Transformation

  Venezia, Italia, 22 - 24 September 1999


LOPSTR'99 is the ninth in a series of international workshops on
logic-based  program synthesis and transformation.  In 1999, it will be
held in parallel to the Symposium on Static Analysis (SAS'99).

OBJECTIVES
LOPSTR'99 will continue the tradition of being a lively and friendly forum
for presenting recent and current research as well as discussing future
trends in the synthesis and transformation of programs.
The scope includes any computational-logic-based techniques, languages, and
tools for the interactive or automated development of programs, with no
preference for a specific language.  Also, papers discussing
programming-in-the-large issues, or presenting practical applications, or
convincingly arguing for the practical applicability of given theoretical
results are encouraged.

PROCEEDINGS AND EDITING POLICY
The  _mode_of_operation_ is as follows.  Based upon submitted extended
abstracts, the programme committee will invite authors to present their
research at the  workshop.  Pre-proceedings with the accepted extended
abstracts will be available at the workshop as a technical report.  Shortly
after the workshop, the programme committee will invite the authors of the
most promising abstracts and presentations to submit full papers.  After
another round of refereeing, the best full papers will be included in the
post-workshop proceedings.

At this point, extended abstracts of at most eight pages are thus solicited
about, but not limited to, the following topics:

specification  analysis
synthesis  verification
compositionreuse
transformation  schemas
specialization  industrial applications

Every submission must clearly exhibit the relationship to the scope of the
workshop, and must really be an extended abstract. It must thus be a
miniature research paper with the key motivations and ideas, with outlines
of the proofs of the key theorems, with references and comparisons to
related work, but without full details of proofs or implemented systems,
without the description of future work, without ramifications that are
irrelevant to the key ideas. 

IMPORTANT DATES
 Submission of extended abstracts   1 May 1999
 Notification to authors10 June 1999
 Submission of full papers  31 October 1999
 Notification to authors20 December 1999

PROGRAM COMMITTEE
 Annalisa Bossi, University of Venice, Italy (programme chair)
 Yves Deville, Universite' Catholique de Louvain, Belgium 
 Mireille Ducasse, IRISA, Rennes , France 
 Sandro Etalle, Universiteit Maastricht , The Netherlands 
 Pierre Flener, Uppsala University, Sweden
 Patricia Hill, University of Leeds, UK
 Kung-Kiu Lau, University of Manchester, UK
 Baudouin Le Charlier?, University of Namur , Belgium
 Michael Leuschel, Universityof Southampton, UK
 Michael Lowry, NASA Ames, USA
 Ali Mili, Institute for Software Research, USA, and University of Tunis II,
Tunisia
 Lee Naish, Melbourne University, Australia
 Alberto Pettorossi, University of Rome II, Italy
 Dave Robertson, University of Edinburgh, UK

SUBMISSIONS
Electronic submissions are strongly encouraged. Address all correspondence
(email preferred: uuencoded, compressed, postscript file) to: 

 Annalisa Bossi "[EMAIL PROTECTED]" 
 Dipartimento di Matematica Applicata e Informatica 
 Universita' "Ca' Foscari" di Venezia 
 Via Torino 155, 30173 Venezia Mestre, Italy 
 Tel: (39) 41 2908421 Fax: (39) 41 2908419 

Re: Haskell 98

[Peter Thiemann]

>> 
>> f f = f
>> 

Hans>   Haskell translates  f f = f  into  f := f |-> f; on the right hand side
Hans> "f" is a bound variable, on the left hand side "f" is a name. Suppose I
Hans> inidicate variables with a slash, then the formula would read
Hans> f := \f |-> \f
Hans> or f(\f) := \f.

I don't really understand your remark. f f = f  as a toplevel
definition is equivalent to (in this special case)

letrec ...
f = \f -> f
   ...

Hans>   So Haskell allows different logical entities have the same name dependent
Hans> on the context, which causes the confusion.

It's not different logical entities, all occurrences of f are variables.
It's not Haskell that's causing the confusion if any, it's the lambda
calculus, more precisely: alpha-conversion. 

-Peter

Re: type error, why?

[S. Alexander Jacobson]

In other words, you are saying that I want a feature, first class
polymorphism, that is now available in Hugs1.3c and from the docs,
GHC4.0?.

Since I am doing development in Hugs 1.4, I guess the question is when
will Hugs1.4  have this feature and is this feature
compatible with Derive?

Alternatively, since GHC 4.0 is there a way to run just the type-checker
part of GHC 4.0 without waiting for it to compile everything?

Also, has anyone manageed to build GHC4.0 for win32?

-Alex-

___
S. Alexander Jacobson   i2x Media  
1-212-697-0184 voice1-212-697-1427 fax


On Mon, 26 Oct 1998, Peter Thiemann wrote:

> > "Alex" == S Alexander Jacobson <[EMAIL PROTECTED]> writes:
> 
> 
> Alex> I wrote the following function that attempts to generalize show by
> Alex> allowing the user to choose the function to stringify constructor
> Alex> arguments.
> 
> >> stringArgs' sep stringer1 (MyFoo x i s) = 
> >> x' ++sep++i' ++ sep ++ s'
> >> where 
> >> x'=stringer' x
> >> i'=stringer'' i
> >> s'=stringer''' s
> >> stringer' o=stringer o
> >> stringer'' o=stringer o
> >> stringer''' o =stringer o
> >> stringer o=stringer1 o --!! replacing stringer1 w/ show works!
> 
> Alex> This function generates a type error because stringer is being used as
> Int-> Char and as Char->Char.  But, if I replace stringer1 in the last
> Alex> line, with the function `show`, hugs allows this function.
> 
> OK, show :: forall a . Show a => a -> String [if my memory serves correctly]
> so it is polymorphic in the type a.
> However, the parameters of a function cannot (currently) have a
> polymorphic type. So when you want to pass show to stringArgs you will 
> have to use one particular instance of this type. In the present case, 
> you get Show a => a -> String [note that the forall is gone], but you
> cannot resolve the overloading because you do not know what a is. Hence
> 
> Alex> However, if I use show and attempt to call this function using foo:
> 
> >> foo x = stringArgs "\n" show (MyFoo "asd" 12 "asd")
> 
> Alex> I get an ambiguous type signature error.
> 
> the ambiguity. If Haskell included first-class polymorphism (which is
> on the list for Haskell 2 and which is present in some form in Hugs
> 1.3c) and you provided an explicit signature, then your function and
> your example would work out. Modulo syntax, this is what is would look 
> like:
> 
> stringArgs' :: String -> (forall a . Show a => a -> String) -> MyFooType -> String
> stringArgs' sep stringer (MyFoo x i s) =
>   x' ++sep++i' ++ sep ++ s'
>   where 
> x'=stringer x
> i'=stringer i
> s'=stringer s
> 
> And your function call would look just like the one above.
> 
> -Peter
> 

Re: topdelcs / decls

[Johannes Waldmann]

Felix Schroeter wrote:

> newtype IntFunnilyOrdered = IFO Int
> instance Ord IntFunnilyOrdered where compare ...
> int_from_ifo (IFO x) = x

>   map int_from_ifo $ sort $ map IFO l

> Ideally, the compiler should figure out that map IFO and map
> int_from_ifo are essentially noops, except changing the class
> instances to use.

right. but i'd like to have an even more clever compiler,
in order to not have to write all those type coercions explicitely.

> If you use the instances once, I think using something like sortWith
> instead will be more elegant.

it depends. the design question then is 
how to pass the argument (<=) to sort: 
visibly (sortBy) or invisibly (as an Ord instance).

> foo = let 
> instance Ord T where compare ... = ... 
>   in 
> sort (something::[T])

> There's no Ord instance visible in the definition of sort.

i think there is (or should be). we have two different meanings of T here:
one is just T, the other is T with the Ord instance.
the last one should apply for the declaration of `something'
(because it is visible at that point).

perhaps this should better be written as
"type T' is instance Ord T where ..."

> somelist :: [T]
> somelist = let instance Ord T where ... in (generate some list of values in T)

the Ord instance here is local, and thus not available later in the program.

> sortedlist :: [T]
> sortedlist = let instance Ord T where [different from the above instance] in
>   sort somelist

somelist's type is implicitely propagated from "just T" to
"T with the instance decl just given".
alternatively, we could require explicit propagation.

> That somehow twists my mind :-)

indeed, i'm not saying the proposal is fully thought out,
or easily implementable. 

-- 
Dr. Johannes Waldmann Institut fur InformatikUniversitat Leipzig
[EMAIL PROTECTED] http://www.informatik.uni-leipzig.de/~joe/
Augustusplatz, D-04109 Leipzig, Germany, Tel/Fax (+49) 341 97 32 204/209

type error, why?

[S. Alexander Jacobson]

I wrote the following function that attempts to generalize show by
allowing the user to choose the function to stringify constructor
arguments.

> stringArgs' sep stringer1 (MyFoo x i s) = 
>x' ++sep++i' ++ sep ++ s'
>  where 
>   x'=stringer' x
>   i'=stringer'' i
>   s'=stringer''' s
>   stringer' o=stringer o
>   stringer'' o=stringer o
>   stringer''' o =stringer o
>   stringer o=stringer1 o --!! replacing stringer1 w/ show works!

This function generates a type error because stringer is being used as
Int->Char and as Char->Char.  But, if I replace stringer1 in the last
line, with the function `show`, hugs allows this function.

However, if I use show and attempt to call this function using foo:

> foo x = stringArgs "\n" show (MyFoo "asd" 12 "asd")

I get an ambiguous type signature error.

What am I doing wrong?

-Alex-

___
S. Alexander Jacobson   i2x Media  
1-212-697-0184 voice1-212-697-1427 fax

Re: Haskell 98

[Hans Aberg]

At 14:15 + 98/10/24, Simon Marlow wrote:
>Simon Peyton-Jones <[EMAIL PROTECTED]> writes:
>
>> Consider the function
>>
>>  t :: T a => T a -> T a
>>
>> I think that it's far from clear what each of the T's mean!
>> Worse, in Haskell 2 we'll also have
>>
>>  t :: T T => T a -> T a
>>
>> In (T T) one is class and the other is a type constructor.
>
>I'm not convinced by the argument "this allows you to write obfuscated
>Haskell".  After all, Haskell is already a wonderful language for
>writing obfuscated code; eg. what does the following definition mean
>
>   f f = f
>
>is it a static error (re-use of 'f'), a type error, or a definition of
>the identity function?  (it's the latter).
>
>Here's to cleaning up the language, and to more exciting obfuscated
>Haskell competitions!

  Haskell translates  f f = f  into  f := f |-> f; on the right hand side
"f" is a bound variable, on the left hand side "f" is a name. Suppose I
inidicate variables with a slash, then the formula would read
f := \f |-> \f
or f(\f) := \f.

  So Haskell allows different logical entities have the same name dependent
on the context, which causes the confusion.

  Now, I think the problems you have with the original discussion is that
you fail to properly define the underlying semantics, specifically, the
general principles on which it depends.

  Hans Aberg
  * Email: Hans Aberg 
  * Home Page: 
  * AMS member listing: 

Re: topdelcs / decls

[Michael Hobbs]

Felix Schroeter wrote:
> > for instance, i could want to sort a list,
> > according to two different criteria,
> > using two different instances of Ord.
> 
> newtype IntFunnilyOrdered = IFO Int
> instance Ord IntFunnilyOrdered where
>   compare (IFO x) (IFO y) | even x && even y = compare x y
>   | even x && odd y  = LT
>   | odd x && even y  = GT
>   | otherwise= compare x y
> int_from_ifo (IFO x) = x
> 
> newtype IntReverse = IR Int
> instance Ord IntReverse where
>   compare (IR x) (IR y) = compare y x
> int_from_ir (IR x) = x
> 
> Now, you can do
>   map int_from_ir $ sort $ map IR l
> or
>   map int_from_ifo $ sort $ map IFO l

Trust me, if you have more than just a few ways to order, this method
gets real complicated real fast. You have to keep track of which list is
based on which 'newtype' and then constantly convert the newtype
back-and-forth to/from the original type when you add or retrieve an
element. The 'map' trick is a nifty work-around for this particular
instance, but it doesn't work well in general for "Bag" ADTs. That is
because the resulting list has lost all of its sorting information. In
order to insert a new element, the list would have to be converted back
into the newtype, insert the element, then convert list back to original
type. I'll be honest and admit that I haven't thought real hard about
how much the efficency will be affected by constantly mapping
back-and-forth with lazy evaluation, but my gut feel is that the
overhead of such a scheme will be expensive for any large Bag.

Re: Fixing imports for and namespaces (was: Simon's H98 Notes)

[David Barton]

One more quick comment, and then I think I (at least) am done (to the
extent that the difference in opinion is clearly defined).

Fergus Henderson writes:

   > And, again IMHO, it is the task of the language to *define* the
   > encapsuation (or to allow that encapsulation to be defined), and
   > the job of the operating system or programming environment to
   > enforce it (or to trust to convention, depending).

   There's not much difference between "language implementation" and
   "programming environment", is there?

No; however, there is a world of difference between "language
implementation" and "language definition".  The two are *very*
distinct in my mind.  Note that I said (above) the job of the language
is to define; you morphed that into "language implementation".

   Above you say it is the job of the OS or programming environment to
   enforce encapsulation.  I think it should be the language
   implementation's job, but the OS should be considered a part of the
   language implementation, so letting the OS handle it would be one
   way for the language implementation to do the enforcement.

I am happy to make it part of the language implementation as long as
it does not impinge on the language definition, leaving other
implementations free to do it other ways.  Pragmas may be one way to
do this.  I simply object (and will continue to object) to making one
mechanism of encapsulation enformement part of the definition,
imposing it on all implementors.  To repeat: defining the
encapsulation is the job of the language defintion, but enforcing it
is not (and should not be).  All IMHO, of course.

Dave Barton <*>
[EMAIL PROTECTED] )0(
http://www.averstar.com/~dlb

Re: Haskell 98

[Philip Wadler]

> Consider the function
> 
>   t :: T a => T a -> T a
> 
> I think that it's far from clear what each of the T's mean!
> Worse, in Haskell 2 we'll also have
> 
>   t :: T T => T a -> T a
> 
> In (T T) one is class and the other is a type constructor.

Let's leave the language as it is: class names and type names must be
distinct.  Rationale: the above examples show that a change might have
questionable consequences.  Recall that the change requires adding the
label `class' to signatures, but not adding the label `type'; it feels
more like a convenient hack than a well-rounded design.  Rather than
make a questionable change now, let's leave it for Haskell 2 and get it
right there.  -- P

Re: monad type errors in class definition?

[Pablo E. Martinez Lopez]

> > class MetaData a where
> >  constructorName::a->String
> >  mapArgs::(MetaData b,MonadPlus c) => (b->c)->a->[c]
> 
> results in the error
> Illegal type "[c]" in constructor application
> 
> If I replace MonadPlus with Show or Num there is no error.
> (Replacing MonadPlus with Monad also result in an error)
> 
> What is so special about MonadPlus and Monad that they result in an error,
> but Show or Num don't.

The problem is that MonadPlus expects a type constructor and Show
expects just a type.
As your variable c is not applied in the right hand side, it is
considered to be a variable for a type, and not for a type constructor.
You should say something as

mapArgs::(MetaData b,MonadPlus c) => (b->c a)->a->[c a]

or similar.
In the paper 

Functional Programming with Overloading and Higher-Order Polymorphism,
Mark P. Jones, First International Spring School on Advanced Functional
Programming Techniques, B{\aa}stad, Sweden, Springer-Verlag Lecture
Notes in Computer Science 925, May 1995.

you can find a very good explanation of this stuff (about kinds, and
kind inference). It is available at
http://www.cs.nott.ac.uk/~mpj/springschool.html

Fidel.