#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