Changes between Version 21 and Version 22 of DependentHaskell
 Timestamp:
 May 27, 2014 5:46:10 PM (14 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

DependentHaskell
v21 v22 74 74 Note that the behavior of `F` depends on the ''kind'' of its argument, `k`. This is an example of a nonparametric type function. Looking at the kind, `k > k`, one would expect `F` to be the identity; yet, it is not. 75 75 76 Thus, we would want to distinguish `pi k. k > k` (the kind of `F`) and `forall k. k > k` (the kind of a typelevel polymorphic identity). This distinction does not affect erasure or phase, but it does affect how a quantifiee can be used. Furthermore, this keeps term classifiers more in line with type classifiers. 76 Thus, we would want to distinguish `pi k. k > k` (the kind of `F`) and `forall k. k > k` (the kind of a typelevel polymorphic identity). This distinction does not affect erasure or phase, but it does affect how a quantifiee can be used. Furthermore, this keeps term classifiers more in line with type classifiers. Note that this means all current type/data families are properly classified with `pi`, not `forall`. This won't cause code breakage, though, because it is impossible to write a kind quantification (with any syntax) in today's Haskell. 77 77 78 78 Datatypes:: 79 How is the kind of a datatype classified? (stub)79 How is the kind of a datatype classified? After some debate, Stephanie and RAE thought that a polykinded datatype should be quantified with `pi`, not `forall`. For example, consider `data Proxy (k :: *) (a :: k) = Proxy`. Is its kind `forall (k :: *). k > *` or `pi (k :: *). k > *`. Let's consider the former type as if it classified a termlevel function. That function would have to be a constant function, by parametricity. Yet, we do ''not'' want `Proxy * Bool` to be the same as `Proxy Nat Zero`. So, we choose the latter classifier. For now, we don't see the need to introduce a way for programmers to declare datatypes classified by `forall`, but there doesn't seem to be anything broken by allowing such an extension. 80 80 81 81 == Open design questions == … … 135 135 === Parametric vs. Nonparametric type families === 136 136 137 * Concrete syntax? (stub)137 * We must have a concrete syntax to declare both of these sorts of type and data families. There are no current proposals for this. 138 138 139 139 = Related work =