[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 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]). But, there is some subtlety.

 GHC assumes all function types (that is, types with kinds that are headed
 by `->`) are ''generative'' and ''injective''. Generativity means that,
 given `a b ~ c d`, you can conclude `a ~ c`. Injectivity means that, given
 `a b ~ a d`, you can conclude `b ~ d`. Indeed, putting these together and
 assuming `a b ~ c d`, you can conclude `b ~ d`. Thus, the kind `->`
 denotes a generative, injective function.

 We could imagine a new classifier `~>` that denotes an ordinary function,
 with no assumptions. GHC would then be careful not to decompose such
 things. This is exactly the situation today with type families. Note that,
 short of GHCi's `:kind` command, there is no way to work with the kind of
 an unapplied type family. If I say `type family F (a :: *) :: *`, we often
 colloquially say that `F :: * -> *`, but there is no way to use this
 knowledge in a Haskell program, because `F` can never appear unsaturated.
 Thus, it is more accurate to say that `F` is just ill-formed, and `F a ::
 *` as long as `a :: *`.

 All of this is to say that the new arrow would have to denote
 ''non''-injective functions. And, I could easy say that GHC today supports
 such a thing, because there's no way to take advantage of it anyway.

 What we really need in this direction is unsaturated type functions, but
 that's a story for another day. (A story I'd love to think more about...
 on that other day!)

 So, taking all of this into account, dorchard's proposal is a different
 syntax for denoting injectivity, and I personally prefer the functional-
 dependency-like one more.

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