[was ghc-devs] Reasoning backwards with type families

Thu Dec 14 01:33:59 UTC 2017

On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead <redirect at vodafone.co.nz>
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 at clear.net.nz> wrote:
>
>>
>> On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald <redirect at 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 at 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 at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>>
>>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171214/74c3ca40/attachment.html>