Changes between Version 21 and Version 22 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 5:46:10 PM (13 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v21 v22  
    7474  Note that the behavior of `F` depends on the ''kind'' of its argument, `k`. This is an example of a non-parametric type function. Looking at the kind, `k -> k`, one would expect `F` to be the identity; yet, it is not. 
    7575 
    76   Thus, we would want to distinguish `pi k. k -> k` (the kind of `F`) and `forall k. k -> k` (the kind of a type-level 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 type-level 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. 
    7777 
    7878 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 poly-kinded 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 term-level 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. 
    8080 
    8181== Open design questions == 
     
    135135=== Parametric vs. Non-parametric type families === 
    136136 
    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. 
    138138 
    139139= Related work =