Injective Type Families are at the core of my "Freelude" ( https://hackage.haskell.org/package/freelude) package, which allows many more types to be defined as Categories, Functors, Applicatives and Monads. For example you can define a tuple of categories as a category and then: (f1, f2) . (g1 . g2) = (f1 . g1, f2 . g2) as one would expect. Also one can define symmetric versions on tuples "fmap", for example: fmap (*2) (3,4,5) = (6,8,10) The library is currently basically a proof of concept but it wouldn't be possible without Injective Type Families. What would also be helpful is if injectivity of type C as mentioned on the page (https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies) but unfortunately this is currently not implemented so I've worked around this where possible (this is largely the reason why the library splits "Functors" and "ExoFunctors"). Cheers, Clinton On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald wrote:

...

This was / perhaps still is one goal of injective type families too! I’m not sure why the current status is, but it’s defjnitely related

Thanks Carter, yes this sort of injectiviy (semi-injectivity? partial injectivity?) is noted as future work in the 2015 paper. But I'm not seeing a lot of hollerin' for it(?) Or am I looking in the wrong places?

The classic example is for Nats in length-indexed vectors: if we know the length of appending two vectors, and one of the arguments, infer the length of the other. (Oleg provided a solution using FunDeps more than a decade ago.) But GHC has special handling for type-level Nats (or rather Ints), hence no need to extend injectivity.

Come to that, the original work that delivered Injective Type Families failed to find many use cases -- so the motivation was more keep-up-with-the-Jones's to provide equivalence to FunDeps.

There were lots of newbie mistakes when Type Families first arrived, of thinking they were injective, because a TF application looks like a type constructor application `F Int` cp `T Int`. But perhaps that misunderstanding didn't represent genuine use cases?

Is anybody out there using Injective Type Families currently? What for?

AntC

...

On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

...

...

On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:

(Moving to ghc-users, there's nothing particularly dev-y.)

...

Sometimes it woulld be useful to be able to reason backwards about type families.

Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type families compared to FunDeps.

...

For example, we have

type family a && b where 'False && b = 'False 'True && b = b a && 'False = 'False a && 'True = a a && a = a

...

... if we know something about the *result*, GHC doesn't give us any way to learn anything about the arguments.

You can achieve the improvement you want today.

You'll probably find Oleg has a solution With FunDeps and superclass constraints, it'll go like this

class (OnResult r a b, OnResult r b a) => And a b r | a b -> r

instance And 'False b 'False -- etc, as you'd expect following the tf equations -- the instances are overlapping but confluent

class OnResult r a b | r a -> b instance OnResult 'True a 'True instance OnResult 'False 'True 'False

You could equally make `OnResult` a type family.

If you can trace backwards to where `&&` is used, you might be able to add suitable constraints there.

So there's a couple of futures: * typechecker plugins, using an SMT solver * injective type families the next phase is supposed to allow

type family a && b = r | r a -> b, r b -> a where ...

That will help with some type families (such as addition of Nats), plug1 https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness- guards.rst#injective-type-families

but I don't see it helping here. plug2 (this example) https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness- guards.rst#type-family-coincident-overlap

Because (for example) if you unify the first two equations, (that is, looking for coincident overlap)

'False && 'False = 'False 'True && 'False = 'False

That's inconsistent on dependency ` r b -> a`.

And you can't fix it by re-ordering the closed equations.

...

For (&&), the obvious things you'd want are ...

There's nothing inherently impossible about this sort of reasoning.

No-ish but. It relies on knowing kind `Bool` is closed. And GHC doesn't pay attention to that. So you need to bring type family `Not` into the reasoning; hence a SMT solver.

...

... I wouldn't necessarily expect GHC to be able to work something like this out on its own.

That's a relief ;-)

...

But it seems like there should be some way to allow the user to guide it to a proof.

Yes, an SMT solver with a model for kind `Bool`. (And a lot of hard work to teach it, by someone.)

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Hi AntC I've panicked GHC enough whilst developing Freelude so whilst I'm not sure exactly what you're saying I'd be hestiant about exploiting anything bogus (8.2 btw seems far more stable than 8.0 btw). The trick is teaching GHC to do all the type trickery it needs so you can write things like: ((f1,g1), Just h1, [x1,x2]) . ((f2,g2), Nothing. [y1,y2,y3]) Under Freelude this should happily compile (assuming all the bits are categories themselves such as functions). Pairs of categories is a category, Maybe of a category is a category, and a list of categories is a category, and finally a triple of categories is a category. So composition should be defined. I'm no expert in the GHC type system (I don't really know any type theory at all) but from what I observed injectivity allows the compiler to "dig" all the way down this chain whilst still leaving some breadcrumbs to find it's way back up. It's the two way equivalence that seems to help, GHC can jump back and forth. I've tried this with non injective type families and just making "inverse" type families but it just seems to end in tears and a mass of type mismatches. Although, I'd love people to look at the code, play with it and suggest improvements. Clinton On Thu, Dec 14, 2017 at 12:33 PM, Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead wrote:

...

Injective Type Families are at the core of my "Freelude" package, which allows many more types to be defined as Categories, Functors, Applicatives and Monads.

Cool!

...

What would also be helpful is if injectivity of type C as mentioned on the page ...

OK. That's as per the type-level addition of Nats I mentioned. Did you consider using FunDeps instead of Injective Type Families?

(I see lower down that page, type C is described as 'generalized' injectivity.)

The variety of injectivity David F's o.p. talked about is orthogonal across types A, B, C. We might call it 'partial injectivity' as in partial function: * some values of the result determine (some of) the arguments; and/or * some values of the result with some values of some arguments determine other arguments; but * for some values of the result and/or some arguments, we can't determine the other arguments.

You can kinda achieve that now using FunDeps with overlapping instances with UndecidableInstances exploiting GHC's bogus consistency check on FunDeps https://ghc.haskell.org/trac/ghc/ticket/10675#comment:15.

Or maybe with (Closed) Type Families if you put a bogus catch-all at the end of the sequence of equations:

...

type family F a where ... F a = F a

(But then it can't be injective, so you have to stitch it together with type classes and superclass equality constraints and who-knows-what.)

None of it is sound or complete or rugged, in particular you can't risk orphan instances -- unless plug3: https://github.com/ghc- proposals/ghc-proposals/pull/56#issuecomment-351289722

AntC

...

On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

...

On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald < redirect@vodafone.co.nz> wrote:

...

This was / perhaps still is one goal of injective type families too! I’m not sure why the current status is, but it’s defjnitely related

Thanks Carter, yes this sort of injectiviy (semi-injectivity? partial injectivity?) is noted as future work in the 2015 paper. But I'm not seeing a lot of hollerin' for it(?) Or am I looking in the wrong places?

The classic example is for Nats in length-indexed vectors: if we know the length of appending two vectors, and one of the arguments, infer the length of the other. (Oleg provided a solution using FunDeps more than a decade ago.) But GHC has special handling for type-level Nats (or rather Ints), hence no need to extend injectivity.

Come to that, the original work that delivered Injective Type Families failed to find many use cases -- so the motivation was more keep-up-with-the-Jones's to provide equivalence to FunDeps.

There were lots of newbie mistakes when Type Families first arrived, of thinking they were injective, because a TF application looks like a type constructor application `F Int` cp `T Int`. But perhaps that misunderstanding didn't represent genuine use cases?

Is anybody out there using Injective Type Families currently? What for?

AntC

...

On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

...

...

On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:

(Moving to ghc-users, there's nothing particularly dev-y.)

...

Sometimes it woulld be useful to be able to reason backwards about type families.

Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type families compared to FunDeps.

...

For example, we have

type family a && b where 'False && b = 'False 'True && b = b a && 'False = 'False a && 'True = a a && a = a

...

... if we know something about the *result*, GHC doesn't give us any way to learn anything about the arguments.

You can achieve the improvement you want today.

You'll probably find Oleg has a solution With FunDeps and superclass constraints, it'll go like this

class (OnResult r a b, OnResult r b a) => And a b r | a b -> r

instance And 'False b 'False -- etc, as you'd expect following the tf equations -- the instances are overlapping but confluent

class OnResult r a b | r a -> b instance OnResult 'True a 'True instance OnResult 'False 'True 'False

You could equally make `OnResult` a type family.

If you can trace backwards to where `&&` is used, you might be able to add suitable constraints there.

So there's a couple of futures: * typechecker plugins, using an SMT solver * injective type families the next phase is supposed to allow

type family a && b = r | r a -> b, r b -> a where ...

That will help with some type families (such as addition of Nats), plug1 https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness- guards.rst#injective-type-families

but I don't see it helping here. plug2 (this example) https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness- guards.rst#type-family-coincident-overlap

Because (for example) if you unify the first two equations, (that is, looking for coincident overlap)

'False && 'False = 'False 'True && 'False = 'False

That's inconsistent on dependency ` r b -> a`.

And you can't fix it by re-ordering the closed equations.

...

For (&&), the obvious things you'd want are ...

There's nothing inherently impossible about this sort of reasoning.

No-ish but. It relies on knowing kind `Bool` is closed. And GHC doesn't pay attention to that. So you need to bring type family `Not` into the reasoning; hence a SMT solver.

...

... I wouldn't necessarily expect GHC to be able to work something like this out on its own.

That's a relief ;-)

...

But it seems like there should be some way to allow the user to guide it to a proof.

Yes, an SMT solver with a model for kind `Bool`. (And a lot of hard work to teach it, by someone.)

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Happy to go with the bogusness if it works better than injective types, feel free to submit a patch. :) On Thu, 14 Dec 2017 at 9:08 pm, Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

On Thu, 14 Dec 2017 at 4:13 PM, Clinton Mead wrote:

...

I've panicked GHC enough whilst developing Freelude so whilst I'm not sure exactly what you're saying I'd be hestiant about exploiting anything bogus (8.2 btw seems far more stable than 8.0 btw).

;-) Fair enough.

"bogus" is SPJ's way of saying: it works, but it isn't supported by deep type theory. 'C'est brutal mais ca marche.'

And that particular exploit has been stable since 2004 at least: the HList library totally relied on it until Closed Type Families arrived.

AntC

On Thu, 14 Dec 2017 at 3:19 PM, David Feuer wrote:

I still haven't really digested what you've written, but I wish to pick a nit (below)

Thanks David. Heh, heh. I think we might be agreeing about the phenomenon, but picking different nits to 'blame'.

On Nov 20, 2017 3:44 AM, "Anthony Clayden" wrote:

...

On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:

...

...

For (&&), the obvious things you'd want are ...

There's nothing inherently impossible about this sort of reasoning.

No-ish but. It relies on knowing kind `Bool` is closed. And GHC doesn't pay attention to that. So you need to bring type family `Not` into the reasoning; hence a SMT solver.

I don't think this is entirely correct. The fact that Bool is closed does not seem relevant. The key fact, I believe, is that (&&) is closed.

Hmm. I wonder what you think "closed" amounts to? Equation 1 `'False && b = 'False` is consistent with `[b ~ Foo]` (unless GHC were to reason about closed kinds) Equation 2 `'True && b = b ` is consistent with `[b ~ Foo]` And so on. The last equation `a && a = a` is consistent with `[a ~ Foo]`. Furthermore it's *inconsistent* with a putative backwards FunDep ` r a -> b` on `'False && 'True ~ 'False`. I think it would be better to omit that equation all together. Then when your o.p. reasons:

...

...

... we can calculate (Not a || Not b) as 'True for each of these LHSes.

What will it calculate for (Not Foo)? Asking GHC to reason like this about open type families smells much harder,

but maybe my sense of smell is off.

Hmm. Your o.p. said

...

...

In order for the constraint (a && b) ~ 'True to hold, the type family application *must have reduced* using one of its equations.

I think that's smelly logic: if you want to reason backwards, then you can't make assumptions about what "must" have reduced if GHC were reasoning forward. That is, unless you're expecting GHC to behave like an SMT solver over closed kinds. Remember that the logic for selecting Closed Type Family equations works from top to bottom *ignoring anything known about the result*. So not only must it have reduced using one of the equations; it must have rejected equations above the one it selected; and it must have seen evidence for rejecting them. (It's more complicated than that in practice: if there's coincident overlap, GHC will pick some equation eagerly. And your `&&` equations exhibit coincident overlap, apart from the last.) If you want it to benefit from something known about the result, you won't (in general) find the same top-to-bottom sequence helps with type improvement. With the FunDep inconsistency in your last equation for `&&`, I suspect that equation-selection will get 'stuck' looking for evidence to reject earlier equations. If we do expect GHC to behave like an SMT solver over closed kinds, then it can reason just as well for an open type family; on the proviso that it can see all the equations. For a bit of history: during discussions around Injective Type Families, one suggestion was to infer injectivity by examining the equations given -- along the lines you're positing. That was rejected on grounds the equations might exhibit injectivity 'by accident'. Also that the programmer might intend injectivity, but their equations be inconsistent. So it was decided there must be explicit declaration; and the equations must be consistent with that declaration. No equations for `&&` could be consistent that way. AntC