[was ghc-devs] Reasoning backwards with type families

Clinton Mead clintonmead at gmail.com
Thu Dec 14 02:57:05 UTC 2017 

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 at clear.net.nz> wrote:

>
> 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/25296012/attachment-0001.html>

More information about the Glasgow-haskell-users mailing list