Changes between Version 16 and Version 17 of NoSubKinds


Ignore:
Timestamp:
Feb 24, 2016 6:45:51 PM (3 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NoSubKinds

    v16 v17  
    11This page is to track the design of a plan, originally Simon PJ's idea, to get rid of GHC's sub-kinding story. Richard E. has volunteered to implement.
     2
     3'''NB:''' This is implemented. See toward the bottom of the page for what actually happened.
    24
    35== The current story ==
     
    150152 * The body of a type forall should have kind `Type l` for some levity `l`, and that is the kind of the forall.  That is, the body cannot have kind `* -> *`, and certainly not `k`.  This makes `forall k (a::k). a` ill-kinded.  (Cf #10114.)
    151153
     154= Implementation =
     155
     156'''Feb 24, 2016'''
     157
     158This general idea is implemented for 8.0. But it turned out to be a bit more subtle. The subtlety all started when we realized that something like
     159
     160{{{
     161type family F a where
     162  F Int# = Int
     163}}}
     164
     165seemed sensible enough. That is, type families could work with unlifted types.
     166
     167But then, what about
     168
     169{{{
     170type family G a :: k where
     171  G Int = Int#
     172  G Bool = Int
     173
     174foo :: G a -> ...
     175}}}
     176
     177The kind of `G a` there is `TYPE r` for some `r`... but that means that we don't know the width of the argument to `foo`: disaster. Even if we know that `k` is `#`, it's still a disaster, because of the many different width of unboxed things.
     178
     179So, we do this:
     180
     181{{{
     182data RuntimeRep = PtrRepLifted | PtrRepUnlifted | IntRep | VoidRep | ...
     183TYPE :: RuntimeRep -> *
     184type * = TYPE 'PtrRepLifted
     185}}}
     186
     187This is just like the idea above, but using `RuntimeRep` instead of levity. Now, from a type's kind, we always know the values' widths. Huzzah! The actual definition is in `GHC.Types`.
     188
     189We still must ensure that all bound variables have a fixed width. This is most easily done during zonking, because it's possible that constraint-solving will inform `RuntimeRep`s. So, after zonking a binder, we simply check that its width is known, and issue an error otherwise.
     190
     191=== Alternative `RuntimeRep` choice ===
     192
     193An alternative to the `RuntimeRep` above is this:
     194
     195{{{
     196data RuntimeRep = PtrRep Levity | VoidRep | IntRep | ...
     197data Levity = Lifted | Unlifted
     198}}}
     199
     200Now we can say that a certain type is boxed without giving its levity. This is nice, because polymorphism over boxed unlifted things is a sensible thing to think about. It also allows us to give a more restrictive type to `unsafeCoerce#` that prevents it from going between boxed and unboxed things (which would be a horror). (If we did this, we would introduce `reallyUnsafeCoerce#` or perhaps `unsafeCoerce##` that was truly unrestricted.) However, this many-layered approach had measurable performance implications (several percent in some programs) because of the need to pointer-chase when unrolling `*`. When we have unpacked sums, we can revisit, because this alternative is better from a theory standpoint.