[GHC] #6018: Injective type families
GHC
ghc-devs at haskell.org
Wed Sep 10 12:16:41 UTC 2014
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies,
Resolution: | Injective
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets: #4259
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by jstolarek):
Replying to [comment:56 heisenbug]:
> Tim Sheard has a nice 2006 paper on how to do it.
What's the title of this paper? I tried to google it but failed.
Replying to [comment:45 simonpj]:
> For closed type classes, can't we infer injectivity, rather than having
to declare it?
I thought about it and I believe this should be possible. But we could
only infer normal injectivity. I believe an algorithm for inferring
injectivity in some of the parameters (ie. things like `result a -> b c`
or `result -> b c` for a 3-arity type family) would be exponential in the
number of arguments. Inferring normal injectivity should be O(n^2^) at
most, where n is the number of equations.
Replying to [comment:57 simonpj]:
> But we have no actual use-caes for anything except Number 1 Goal, for
equalities of form `F t1 ~ F t2`.
It looks like Conal Elliot has a use case for injectivity in only some
arguments: http://www.haskell.org/pipermail/glasgow-haskell-
users/2011-February/020027.html I'll contact him for more details.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:58>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list