[GHC] #9840: Permit empty closed type families

[GHC]

#9840: Permit empty closed type families
-------------------------------------+-------------------------------------
        Reporter:  adamgundry        |                   Owner:
            Type:  feature request   |                  Status:  patch
        Priority:  normal            |               Milestone:
       Component:  Compiler (Type    |                 Version:  7.8.3
  checker)                           |                Keywords:
      Resolution:                    |            Architecture:
Operating System:  Unknown/Multiple  |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:  #8028             |  Differential Revisions:  Phab:D841
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Replying to [comment:5 adamgundry]:
 > > What Adam really wants here is the ability to create new type-level
 constants at arbitrary kind.
 >
 > Is it?

 Yes. :) But you don't know it yet.

 After posting this morning, I thought more about this. The more I thought
 about it, the more I liked it.

 The key idea (for me) is that currently Haskell has many different forms
 of type-level symbol declaration (`data`, `newtype`, `type family`, `data
 family`, `type`, `class`, maybe more?), but perhaps these can all be
 rolled into one, more flexible type of declaration. (I'm not necessarily
 proposing to expose this to users as such, but to think of it this way.)
 At the moment, I'm concerned only with how these type-level symbol
 declarations behave in types, completely forgetting about any term-level
 behavior. I'm also forgetting about FC for the moment, concentrating only
 on Haskell.

 * `data`: Declares generative, injective constants whose result kind must
 be `*`. Can be pattern-matched. When considered as a kind, the set of
 inhabitants is closed and always known.
 * `newtype`: Identical to `data`, except that `newtype`s are neither
 generative nor injective under representational equality.
 * `type family`: Not generative, not injective. Accordingly, must appear
 always saturated. (GHC's type variable application operation in types --
 that is, `a b` where `a` and `b` are type variables -- assumes that the
 function is generative & injective. Anything that isn't must always be
 saturated.) These have a limited reduction behavior known to GHC. Closed
 type families have a fixed reduction behavior; open type families'
 reduction behavior can be extended. Cannot be pattern-matched against.
 * `data family`: Generative & injective. When considered as a kind (in the
 future with kind equalities) the set of inhabitants is open, but each
 extension of this set requires parameters to be apart from previous sets.
 Can be pattern-matched against.
 * `type`: Like a `type family`, but with even more limited behavior.
 * `class`: Like `data`, but the result kind must be `Constraint`.

 Phab:D202 extends this collection with injective type families, which are
 like type families, but allow injectivity in some subset of its
 parameters.

 I have wanted the following:
 * A generative, injective type constant, whose result kind is `*`. When
 considered as a kind, the set of inhabitants is open. Can be pattern-
 matched against.

   This is like `*`, but still distinguished from `*`. One may argue that
 this is like `Symbol`, but I want to be able to hook into GHC's module
 system to disambiguate identically-named inhabitants. I wanted this for
 `units`, where I settle for declaring my extensible set of units in kind
 `*`. This leads to worse error messages than would be possible if I could
 declare a new, open kind.

 * A generative, injective type constant that can '''not''' be pattern-
 matched against.

   This is the right place for `Any`.

 Adam seems to want:

 * A non-generative, non-injective type-level symbol with reduction
 behavior unknown to GHC. This cannot be pattern-matched against.

   The reduction behavior is implemented in a plugin. This type of
 declaration is also the correct characterization of the type-lits
 operators.

 So it seems that there are several characteristics each type-level
 declaration varies in:
 * Generativity (possibly different choices for nominal vs.
 representational equality)
 * Injectivity (possibly different choice for nominal vs. representational
 equality, and per argument)
 * Matchability (if something is matchable, it had better be generative and
 injective, too!)
 * Open/closed

 In addition, GHC blesses type families (and type synonyms) with a limited
 form of reduction.

 -------------------

 I'm not totally sure where all of this goes, but somehow classifying this
 menagerie seems meaningful. It also helps to identify missing spots and to
 understand what is going on better. Perhaps using empty closed type
 families for Adam's needs and for type-lits is OK, but it isn't really
 what we want, according to these classifications: these type-level symbols
 have an unknown reduction behavior, in contrast to empty closed type
 families, which have a known (vacuous) reduction behavior.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9840#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler