Field accessor type inference woes

AntC anthony_clayden at clear.net.nz
Tue Jul 2 10:53:24 CEST 2013


> 
> 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?

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.

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.

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)


[**] 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.
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




More information about the Glasgow-haskell-users mailing list