Changes between Version 6 and Version 7 of KindSystem

Timestamp:

10/17/08 01:03:01 (5 years ago)

Author:

simonpj

Comment:

--

KindSystem

@@ -25 +25 @@
 There are many eugh moments in this code:
 
-* 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).
+  * 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).
   * {{{Zero}}} has kind {{{*}}}, and {{{Succ}}} has kind {{{* -> *}}}, so it is perfectly valid to create a haskell function with a signature:
 
@@ -37 +37 @@
   * {{{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.
 
-* We then decalare a new data type to hold lists parameterised by their lengths.
+  * We then decalare a new data type to hold lists parameterised by their lengths.
+
   * {{{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.