On Tue, Jul 2, 2013 at 4:53 AM, AntC <span dir="ltr"><<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">><br>
> I was envisaging that we might well need a functional dependency<br>
><br>
<br>
</div>Hi Adam, Edward, (Simon),<br>
<br>
I think we should be really careful before introducing FunDeps (or type<br>
functions).<br>
<br>
Can we get to the needed type inference with UndecidableInstances?<br>
Is that so bad?<br></blockquote><div><br></div><div>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.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
In the original SORF proposal, Simon deliberately avoided type functions,<br>
and for closely argued reasons:<br>
"But this approach fails for fields with higher rank types."<br>
I guess the same would apply for FunDeps.<br></blockquote><div><br></div><div>The approach still has issues with higher kinded types when extended to include setting. </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
FWIW in the DORF prototype, I did use type functions.<br>
I was trying to cover a panoply of HR types, parametric polymorphic<br>
records, type-changing update [**], and all sorts;<br>
so probably too big a scope for this project.<br>
<br>
If you're interested, it's deep in the bowels of the Implementation notes,<br>
so I could forgive anybody for tl;dr. See:<br>
<a href="http://hackage.haskell.org/trac/ghc/wiki/Records/DeclaredOverloadedRecordFi
elds/ImplementorsView#Type-changingupdate" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/Records/DeclaredOverloadedRecordFi<br>
elds/ImplementorsView#Type-changingupdate</a><br>
<br>
In terms of the current Plan:<br>
<br>
class Has r fld t where<br>
getFld :: r -> GetResult r fld t<br>
<br>
Of course where the record and field do determine the result,<br>
the GetResult instance can simply ignore its third argument.<br>
But for HR types, this allows the `Has` instance to<br>
'improve' `t` through Eq constraints,<br>
_and_then_ pass that to GetResult.<br>
<br>
In the 'chained' accessors that Edward raises,<br>
I think the presence of the type function 'fools' type inference into<br>
thinking there's a dependency.<br></blockquote><div><br></div><div>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 <b>no</b> known type for the intermediate value type. You can't punt it to the use site.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
So (foo . bar) has type (and abusing notation):<br>
<br>
( Has r "bar" t_bar, Has (GetResult r "bar" t_bar) "foo" t_foo )<br>
=> r -> (GetResult (GetResult r "bar" t_bar) "foo" t_foo) </blockquote><div><br></div><div>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!</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
[**] Beware that the DORF approach didn't support type-changing update in<br>
all cases, for reasons included in the notes for Adam's Plan page.<br>
<br>
Also beware that DORF used type families and some sugar around them.<br>
That had the effect of generating overlapping family instances in some<br>
cases -- which was OK, because they were confluent.<br>
But if I understand correctly what Richard E is working on<br>
<a href="http://hackage.haskell.org/trac/ghc/wiki/NewAxioms" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/NewAxioms</a><br>
overlapping stand-alone family instances are going to be banished<br>
-- even if confluent.<br></blockquote><div><br></div><div>Even with overlapping type families nothing changes. Coverage is still violated.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
So today I would approach it by making them associated types,<br>
and including the GetResult instance inside the `Has`,<br>
so having a separate (non-overlapping) instance<br>
for each combination of record and field (Symbol).<br>
<br>
HTH. Is Adam regretting taking up the challenge yet? ;-)<br>
<br>
AntC<br>
<br>
<br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div><br>