Changes between Version 7 and Version 8 of KindSystem


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

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v7 v8  
    3737  * {{{Succ}}} has kind {{{* -> *}}}, whereas really the programmer wants to enforce that the argument to {{{Succ}}} will only ever consist of {{{Zero}}}s or {{{Succ}}}s.  i.e. the {{{* -> *}}} kind given to {{{Succ}}} is far to relaxed. 
    3838 
    39   * We then decalare a new data type to hold lists parameterised by their lengths. 
     39  * We then declare a new data type to hold lists parameterised by their lengths. 
    4040 
    4141  * {{{List}}} has kind {{{* -> * -> *}}}, which really doesn't tell us anything other than its arity.  An alternative definition could have been: {{{data List item len where ... }}}, although this adds only pedagogical information, and nothing new that the compiler can statically check. 
    4242 
    43   * The {{{Cons}}} constructor actually has a mistake in it.  The second argument ({{{List n a}}}) has the names to the type parameters flipped.  The compiler cannot detect this, and the error will become apparant at use sites which are at a distance from this declaration site. 
     43  * The {{{Cons}}} constructor actually has a mistake in it.  The second argument ({{{List n a}}}) has the names to the type parameters flipped.  The compiler cannot detect this, and the error will become apparent at use sites which are at a distance from this declaration site. 
    4444 
    4545  * Nothing stops a user creating the silly type {{{List Int Int}}} even though the intention is that the second argument is structured out of {{{Succ}}}s and {{{Zero}}}s. 
     46 
     47== Proposal == 
    4648 
    4749We propose to add new base kinds other than {{{*}}} using a simple notation.  The above example ''could'' become: 
     
    6365* 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}}}. 
    6466 
    65 == Declaration Syntax == 
     67 
    6668 
    6769=== ADT syntax ===