Field accessor type inference woes

[Edward Kmett]

On Tue, Jul 2, 2013 at 4:53 AM, AntC <anthony_clayden at clear.net.nz> wrote:

> >
> > I was envisaging that we might well need a functional dependency
> >
>
> Hi Adam, Edward, (Simon),
>
> I think we should be really careful before introducing FunDeps (or type
> functions).
>
> Can we get to the needed type inference with UndecidableInstances?
> Is that so bad?
>

That doesn't solve this problem. The issue isn't that the it is undecidable
and that it could choose between two overlapping options. The issue is that
there is no 'correct' instance to choose.


> In the original SORF proposal, Simon deliberately avoided type functions,
> and for closely argued reasons:
> "But this approach fails for fields with higher rank types."
> I guess the same would apply for FunDeps.
>

The approach still has issues with higher kinded types when extended to
include setting.


> FWIW in the DORF prototype, I did use type functions.
> I was trying to cover a panoply of HR types, parametric polymorphic
> records, type-changing update [**], and all sorts;
> so probably too big a scope for this project.
>
> If you're interested, it's deep in the bowels of the Implementation notes,
> so I could forgive anybody for tl;dr. See:
> http://hackage.haskell.org/trac/ghc/wiki/Records/DeclaredOverloadedRecordFi
> elds/ImplementorsView#Type-changingupdate
>
> In terms of the current Plan:
>
>     class Has r fld t   where
>         getFld  :: r -> GetResult r fld t
>
> Of course where the record and field do determine the result,
> the GetResult instance can simply ignore its third argument.
> But for HR types, this allows the `Has` instance to
> 'improve' `t` through Eq constraints,
> _and_then_ pass that to GetResult.
>
> In the 'chained' accessors that Edward raises,
> I think the presence of the type function 'fools' type inference into
> thinking there's a dependency.
>

There really is a dependency. If the input record type doesn't determine
the output value type that has to be passed to the next field accessor (or
vice versa) then there is *no* known type for the intermediate value type.
You can't punt it to the use site.


> So (foo . bar) has type (and abusing notation):
>
>     ( Has r "bar" t_bar, Has (GetResult r "bar" t_bar) "foo" t_foo )
>      => r -> (GetResult (GetResult r "bar" t_bar) "foo" t_foo)


The extra parameter actually makes coverage even harder to determine and it
makes instance selection almost impossible as it will in almost all cases
be under-determined, and since we're playing games with type application,
not even manually able to be applied!


> [**] Beware that the DORF approach didn't support type-changing update in
> all cases, for reasons included in the notes for Adam's Plan page.
>
> Also beware that DORF used type families and some sugar around them.
> That had the effect of generating overlapping family instances in some
> cases -- which was OK, because they were confluent.
> But if I understand correctly what Richard E is working on
> http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
> overlapping stand-alone family instances are going to be banished
> -- even if confluent.
>

Even with overlapping type families nothing changes. Coverage is still
violated.


> So today I would approach it by making them associated types,
> and including the GetResult instance inside the `Has`,
> so having a separate (non-overlapping) instance
> for each combination of record and field (Symbol).
>
> HTH. Is Adam regretting taking up the challenge yet? ;-)
>
> AntC
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130702/0799c937/attachment.htm>