Generalize injective type families

With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:

data Nat = Zero | Succ a

class Add a b r | a b -> r, r a -> b
instance                Add Zero     b b
instance (Add a b r) => Add (Succ a) b (Succ r)

Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:

type family AddTF a b = r | r a -> b where
     AddTF Zero     b = b
     AddTF (Succ a) b = Succ (AddTF a b)

But we want to be able to say that.

Trac metadata

Trac field	Value
Version	7.11
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #6018 (closed)

changed weight to 5

added Tfeature request Trac import typechecker labels

Trac metadata

Trac field	Value
Related	- → #6018 (closed)

For anyone interested, the development of this feature is happening here:

https://github.com/jstolarek/ghc/tree/T10832-generalized-injectivity

At the moment it just compiles but I hope this implementation becomes usable Real Soon Now.

Trac metadata

Trac field	Value
Differential revisions	- → D1287

I've hit needing this feature for what I was hoping would be pretty elementary code :(

type family ReverseTC (a :: [ k ]) (res :: [ k ] )  = result    where
    ReverseTC '[] res = res
    ReverseTC (a ': bs ) res = ReverseTC bs (a ':  res)

type family Reverse  (a :: [k]) =  (result  :: [k])     where
  Reverse a = ReverseTC a '[]

I would like to explain to GHC that if i know a and result , or res and result, i know the remaining variable, so that my "stack safe" Reverse computation can also be treated as Injective (which it is! )

Carter, can you upload a self-contained piece of code? When we were working on injective type families we had a really hard time finding real-world examples where injectivity was necessary. Many people in the past claimed that they needed it but when we finally had the feature implemented few people could remember their use cases from the past.

See #10832 on #6018 (closed) for a use-case example.

I think the latest version of all this is in the main repo, on branch wip/T10832-generalised-injectivity

added 1 deleted label

mentioned in issue #13731

Possible use-case #13731

type family ExtensionType ext a = res | res -> ext a
data ListExtension
type instance ExtensionType ListExtension a = [a]

I might have a use case for this, but I’m not smart enough to understand if my problem would be solved by this feature or not. Basically, I have a type family for type-level append:

type family xs :++: ys where
  '[]  :++: ys = ys
  (x ': xs) :++: ys = x ': (xs :++: ys)

This family is not injective, but if you know the result and one of the two inputs, you can deduce the other one. Therefore, I would like to be able to write the dependency annotation r xs -> ys, r ys -> xs.

I have written a function that uses :++: in its type signature, which currently looks like this:

forall g r a f. (forall v. f v -> Eff (g :++: r) v) -> Eff (f ': r) a -> Eff (g :++: r) a

Currently, this signature is ambiguous. However, notably, we know r, and in the location this function is used, we also know g :++: r. Therefore, my hope is that with this feature, I could use this function, and g could be inferred. Currently, however, I have to use TypeApplications to pick g explicitly, even though the type seems “obvious” to the programmer at its use site (since it very explicitly duplicates type information in an adjacent top-level annotation).

I don’t know enough to know if such an annotation would actually allow such a thing or not, or if this is even applicable in my use case, but I thought I would offer the example anyway, since it sounds like this feature is in need of motivating examples. (I can also try and come up with a smaller, self-contained example if I’m not totally off base and that would, in fact, be relevant/helpful.)

ticket:10832#comment:138779 looks like a use-case for injectivity to me.

ticket:10832#comment:125483 has a fairly well-advanced implementation, just needs completing.

Trac metadata

Trac field	Value
CC	Iceland_jack, RyanGlScott, nfrisby → Iceland_jack, RyanGlScott, lexi.lambda, nfrisby

ticket:10832#comment:138779 is asking for injectivity from result with either argument to the other.

Notice the O.P. for AddTF only considers result & first argument -> second arg.

I see a problem. In instances

type family xs :++: ys = r | r xs -> ys, r ys -> xs where  -- both injectivities
  '[]       :++: ys = ys
  (x ': xs) :++: ys = x ': (xs :++: ys)

Under the injection r ys -> xs, I think GHC will not be able to see the 'apartness' in the two equations. That is, it won't be able to disprove ys ~ (x ': (xs :++: ys)). Yes we know they can't unify, but GHC sees :++: as a Type Function, not a (proto-)constructor.

Speculative remedy proposed here, for the AddTF example.

Are we exploring avenues like head-injectivity or partial injectivity? Richard's example tells us a ~ Just b if F a ~ True

type family 
  F a where
  F (Just a) = True
  F Nothing  = False

but similarly

type family
  G a where
  G (Just a) = (a,   a)
  G Nothing  = (Int, Int)

means a ~ Int if G (Just a) ~ (Int, Int) — is that useful?

• *Edit**: I guess G would be equivalent to writing

type family
  GJust a = res | res -> a where
  GJust a = (a, a)

type family
  G a where
  G (Just a) = GJust a
  G Nothing  = (Int, Int)

This might be useless

mentioned in issue #14164

I haven't found so many uses for this, but I wanted to try this lately

-- Free   :: (Type -> Constraint) -> (Type -> Type)
-- Forget :: (Type -> Constraint) -> (Type -> Type)

newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx)

type family
  Forget cls free = res | res cls -> free where
  Forget cls (Free cls a) = a

edit: Generic Programming of All Kinds, (I think) this can be given the annotation

data Ctx :: Type -> Type where
  Nil   :: Ctx(Type)
  (:&:) :: k -> Ctx(ks) -> Ctx(k -> ks)

type family
  Apply kind (f :: kind) (a :: Ctx(kind)) = (res :: Type) | res kind -> a where
  Apply(Type)    a Nil      = a
  Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as

Edit: More suggestions go to this gist.

added injective type families label

added Pnormal label

mentioned in issue #13797

marked this issue as related to #13797

mentioned in issue #17927 (closed)

Key post: When this is done, add annotations to type families in GHC.TypeLits as appropriate, as suggested in #17927 (closed).

mentioned in issue #18851