Opened 4 years ago

Last modified 12 months ago

#10832 new feature request

Generalize injective type families

Reported by: jstolarek Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.11
Keywords: TypeFamilies, InjectiveFamilies Cc: nfrisby, Iceland_jack, RyanGlScott, lexi.lambda
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #6018 Differential Rev(s): Phab:D1287
Wiki Page:

Description

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.

Change History (20)

comment:1 Changed 4 years ago by jstolarek

comment:2 Changed 4 years ago by jstolarek

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.

comment:3 Changed 4 years ago by jstolarek

Differential Rev(s): D1287

comment:4 Changed 4 years ago by jstolarek

Differential Rev(s): D1287Phab:D1287

comment:5 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:6 Changed 3 years ago by carter

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! )

comment:7 Changed 3 years ago by jstolarek

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.

comment:8 Changed 3 years ago by nfrisby

Cc: nfrisby added

comment:9 Changed 3 years ago by simonpj

See comment:119 on #6018 for a use-case example.

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

comment:10 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:11 Changed 3 years ago by simonpj

Keywords: InjectiveFamilies added

comment:12 Changed 2 years ago by Iceland_jack

Possible use-case #13731

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

comment:13 Changed 2 years ago by lexi.lambda

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.)

comment:14 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

comment:15 Changed 2 years ago by simonpj

comment:13 looks like a use-case for injectivity to me.

comment:9 has a fairly well-advanced implementation, just needs completing.

comment:16 Changed 2 years ago by lexi.lambda

Cc: lexi.lambda added

comment:17 Changed 2 years ago by AntC

comment:13 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.

comment:18 Changed 2 years ago by Iceland_jack

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

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:19 Changed 19 months ago by Iceland_jack

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.

Last edited 12 months ago by Iceland_jack (previous) (diff)

comment:20 Changed 18 months ago by jstolarek

Owner: jstolarek deleted
Note: See TracTickets for help on using tickets.