Opened 3 years ago
Last modified 3 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 3 years ago by
Related Tickets: | → #6018 |
---|
comment:2 Changed 3 years ago by
comment:3 Changed 3 years ago by
Differential Rev(s): | → D1287 |
---|
comment:4 Changed 3 years ago by
Differential Rev(s): | D1287 → Phab:D1287 |
---|
comment:5 Changed 3 years ago by
Keywords: | TypeFamilies added |
---|
comment:6 Changed 3 years ago by
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
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 2 years ago by
Cc: | nfrisby added |
---|
comment:9 Changed 2 years ago by
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 2 years ago by
Cc: | Iceland_jack added |
---|
comment:11 Changed 21 months ago by
Keywords: | InjectiveFamilies added |
---|
comment:12 Changed 20 months ago by
Possible use-case #13731
type family ExtensionType ext a = res | res -> ext a data ListExtension type instance ExtensionType ListExtension a = [a]
comment:13 Changed 19 months ago by
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 19 months ago by
Cc: | RyanGlScott added |
---|
comment:15 Changed 19 months ago by
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 19 months ago by
Cc: | lexi.lambda added |
---|
comment:17 Changed 19 months ago by
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 19 months ago by
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
comment:19 Changed 10 months ago by
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.
comment:20 Changed 9 months ago by
Owner: | jstolarek deleted |
---|
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.