#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): Dominic, do throw in thoughts at any time. My patch will be ready Real Soon Now but after the merge there will be room for further development of this feature. I will not comment on the proposal of having a separate kind for injective type families. I don't have sufficient knowledge of typechecker to judge whether this would make things easier. Perhaps Simon or Richard can offer some insight here. Regarding your proposed new syntax I believe it does not offer anything new compared to the syntax we decided to use (unless I missed something?). These pairs of definitions would be equivalent: {{{#!hs type family Id a = result | result -> a where {...} type family (Id :: * >-> *) a where {...} type family F a b c = d | d -> a b c type family (F :: * >-> * >->) a b c type family G a b c = foo | foo -> a b where type family (G :: * >-> * -> *) a b c }}} Your syntax however does not extend to injectivity where knowing the result and some of the arguments allows to determine some other arguments: {{{#!hs type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a where type family H a b c = xyz | xyz a -> b c, xyz b -> a c }}} This kind of injectivity is not implemented in my patch but we want to leave the door open for such a possibility in the future. I'm also not sure if I like how your proposed syntax interacts with PolyKinds: it seems that there would be two alternative places to specify kinds. David, what do you mean by injectivity lemmas? At the moment I don't have a solid stance on the subject of calling type families in the RHS of injective type families. When I started this work it seemed to me that this is not possible. Now I have some more experience so I plan to revisit my earlier decisions. Incidentally, now it seems to me that self-recursion might actually be doable. Calling other type families in the RHS still seems very problematic. First of all called families would have to be injective to declare that a type family that calls them is also injective*. This implies that type families would have to be typechecked in dependency order, which sounds lika a non-trivial technical obstacle. Of course this would prevent type families that form cycles (including mutual recursion) from being injective. Another problem is issue of overlap: {{{#!hs type family Foo a = r | r -> a where Foo (Bar a) = X a Foo (Baz a b) = Y a b }}} To determine whether `Foo` is injective or not we must know whether `X a` and `Y a b` can have identical values (well, types not values). Given that `X` and `Y` can also call other type families I don't see a simple way of checking this. Anyway, the ice here seems very thin and I don't feel confident proceeding further with calling type families by injective type families without formal proof. *) This is a simplifying assumption. It is possible to write a type family that is injective despite calling non-injective type families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:107 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler