Changes between Version 9 and Version 10 of KindSystem

Timestamp:

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

Author:

simonpj

Comment:

--

KindSystem

@@ -87 +87 @@
 }}}
 
+
+
+== Interaction with normal functions ==
+
+Functions cannot have arguments of a non * kind.  So the following would be disallowed:
+
+{{{
+bad :: Zero -> Bool   -- Zero has kind Nat
+}}}
+
+This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes
+
+Type variables may however be inferred to have non-* kinds.  E.g.
+
+{{{
+#!text/x-haskell
+data NatRep :: Nat -> * where
+  ZeroRep :: NatRep Zero
+  SuccRep :: (NatRep n) -> NatRep (Succ n)
+
+tReplicate :: forall n a . NatRep n -> a -> List a n
+...
+}}}
+
+In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}.
+
 == Interaction with GADTs ==
 
@@ -105 +131 @@
 GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described below), but may also collect constraints for the kind inference system.
 
-== Interaction with normal functions ==
-
-Functions cannot have arguments of a non * kind.  So the following would be disallowed:
-
-{{{
-bad :: Zero -> Bool   -- Zero has kind Nat
-}}}
-
-This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes
-
-Type variables may however be inferred to have non-* kinds.  E.g.
-
-{{{
-#!text/x-haskell
-data NatRep :: Nat -> * where
-  ZeroRep :: NatRep Zero
-  SuccRep :: (NatRep n) -> NatRep (Succ n)
-
-tReplicate :: forall n a . NatRep n -> a -> List a n
-...
-}}}
-
-In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}.
-
 === Ambiguous cases ===
 
@@ -149 +151 @@
 instance LessThanOrEqual Zero Zero
 instance LessThanOrEqual n m => LessThanOrEqual n (Succ m)
-
-class Bad x y            -- \
-instance Bad True Int    --  |
-instance Bad Int String  --   > Together this would require argument x :: forall kind k . k, 
-                         --  |  see PolymorphicKinds
-                         -- /
+}}}
+This example is ill-kinded though:
+{{{
+class Bad x           -- Defaults to x::*
+instance Bad Int   -- OK
+instance Bad Zero  -- BAD: ill-kinded 
 }}}