Changes between Version 8 and Version 9 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 8:04:26 AM (6 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v8 v9  
    55== Rationale == 
    66 
    7 Haskell has a very powerful and expressive static type system.  The problem is when you come to do any programming at the type level, that is typed by an unsatisfactorily inexpressive kind system.  We propose to make it just a little bit stronger. 
     7Haskell has a very powerful and expressive static type system.  The problem is when you come to do any programming at the type level, that is typed by an unsatisfactorily inexpressive kind system.    We propose to make it just a little bit stronger. 
    88 
    99Note: the aim here initially is to implement a small useful extension to Haskell, and not to retrofit the entirety of e.g. [http://web.cecs.pdx.edu/~sheard/Omega/index.html Omega] into GHC yet ;)) 
     
    6161 
    6262 
    63 * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} and {{{Succ}}}.  Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any haskell values (including undefined/bottom).  So the {{{ foo :: Zero -> Succ Zero -> Bool }}} type signature from earlier would be rejected by the compiler. 
    64  
    65 * We then declare the type {{{List}}}, but we now say the second argument to {{{List}}} has to be a type of kind {{{Nat}}}.  With this extra information, the compiler can statically detect our erroneous {{{Cons}}} declaration and would also reject silly types like {{{List Int Int}}}. 
     63  * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} and {{{Succ}}}.  Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any haskell values (including undefined/bottom).  So the {{{ foo :: Zero -> Succ Zero -> Bool }}} type signature from earlier would be rejected by the compiler. 
     64 
     65  * We then declare the type {{{List}}}, but we now say the second argument to {{{List}}} has to be a type of kind {{{Nat}}}.  With this extra information, the compiler can statically detect our erroneous {{{Cons}}} declaration and would also reject silly types like {{{List Int Int}}}. 
    6666 
    6767