[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
        Reporter:  lunaris           |                   Owner:  jstolarek
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.4.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |  TypeFamilies, Injective
 Type of failure:  None/Unknown      |            Architecture:
      Blocked By:                    |  Unknown/Multiple
 Related Tickets:  #4259             |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D202
-------------------------------------+-------------------------------------

Comment (by jstolarek):

 Replying to [comment:108 goldfire]:
 > Replying to [comment:105 dorchard]:
 > >  what about adding a kind of injectives `>->`? e.g.`* >-> *`is the
 kind of injective type functions
 >
 > This is very much along the lines of what Jan and I proposed in our
 "Promoting Functions to Type Families" paper
 ([http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf
 here]).
 Not exactly, I think. At the moment `->` kind classifies term-level
 functions (non-injective, non-generative, can be partially applied), type
 constructors (injective, generative, can be partially applied) and type
 families (non-injective, non-generative, cannot be partially applied). In
 our paper we proposed a new kind to classify type functions (families)
 that are still non-injective and non-generative but can be partially
 applied just like term-level functions. We addressed the problem of
 partial application, not injectivity.

 > GHC assumes all function types (that is, types with kinds that are
 headed by `->`) are ''generative'' and ''injective''. (...) Thus, the kind
 `->` denotes a generative, injective function.
 Are you sure? I would say this is true only for type constructors but
 perhaps I'm missing something. (I am assuming that also `->` classifies
 type families although, as you point out, this is not entirely accurate.)

 Anyway, I can imagine introducing a new kind to distinguish between
 injective and non-injective applications but, given that we might want a
 new kind to distinguish between things that can and can't be partially
 applied at the type level, this does not seem like a good choice.

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