Changes between Version 6 and Version 7 of KindSystem


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

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v6 v7  
    2525There are many eugh moments in this code:
    2626
    27 * We first declare two new types ({{{Zero}}} and {{{Succ}}}), and, thanks to the EmpyDataDecls extension, say that they are uninhabited by values (except bottom/error).
     27  * We first declare two new types ({{{Zero}}} and {{{Succ}}}), and, thanks to the EmpyDataDecls extension, say that they are uninhabited by values (except bottom/error).
    2828  * {{{Zero}}} has kind {{{*}}}, and {{{Succ}}} has kind {{{* -> *}}}, so it is perfectly valid to create a haskell function with a signature:
    2929
     
    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 decalare a new data type to hold lists parameterised by their lengths.
     40
    4041  * {{{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.
    4142