Edward, is quite right. Thank you for pointing this out; I hadn’t fully
absorbed the consequences of the three-parameter Has class. This isn’t a
fundep-vs-type-function thing; it’s a tradeoff between polymorphism and
overloading.
There seem to be two alternatives. I’ll use fundep notation just because it’s
better known. Same things happen with functions. Here are two records
data R a = MkR { foo :: a -> a }
data S = MkS { bar :: forall b. b -> b }
Here is Plan A: use fundep (or type function)
class Has r f t | r f -> t where
getFld :: r -> t
instance Has (R a) “foo” (a -> a) where ..
instance Has S “bar” (forall b. b -> b) where ...
Lacking (as we still do) impredicative polymorphism, the S instance declaration
is rejected.
Here is Plan B: no fundep (or type functions)
class Has r f t where
getFld :: r -> t
instance (t ~ a->a) => Has (R a) “foo” t where ..
instance (t ~ b->b) => Has S “bar” t where ...
Now the instance for S works fine. But the ambiguity problem that Edward
describes shows up.
Can you combine A and B?
class Has r f t | r f -> t where
getFld :: r -> t
instance (t ~ b->b) => Has S “bar” t where ...
No: the instance is rejected because the S does not “cover” the free type
variable t. This is #2247 I think. There is a good reason for this (I could
elaborate if reqd).
Notice too that with
data T = MkT { wib :: (forall b. b -> b) -> Int }
the polymorphic type is more deeply buried, and Plan B doesn’t work either. So
Plan B is already a bit of a sticking plaster.
Bottom line: there is a real tension here.
Let’s review the goal:
to allow you to use the same field name in different records.
The current proposal allows you to write
f :: r { foo :: Int } => r -> Int -> Int
which will work on any record with an Int-valued foo field. BUT writing
functions like this was never a goal! We could restrict the proposal: we could
simply *not abstract* over Has constraints, preventing you from writing ‘f’,
but also preventing you from falling over Edward’s problem. (But it would
also be an odd restriction, given that Has is in most ways an ordinary class.)
So I think Plan B (the one we are currently proposing) works just fine for the
declared goal. We just have to acknowledge that it doesn’t do everything you
might possibly want.
Simon
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 01 July 2013 18:21
To: Adam Gundry
Cc: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
Subject: Re: Field accessor type inference woes
On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry
<adam.gun...@strath.ac.uk<mailto:adam.gun...@strath.ac.uk>> wrote:
Hi Edward,
I was envisaging that we might well need a functional dependency
class Has (r :: *) (x :: Symbol) (t :: *) | r x -> t
and, as you point out, composition of polymorphic accessors certainly
motivates this. Isn't that enough, though? I think it works out more
neatly than the type family version, not least because evidence for a
Has constraint is still merely a projection function, and we can still
handle universally quantified fields.
My understanding from a recent interaction with Iavor was that the old
difference between functional dependencies and type families where the fundep
only chose the 'instance' rather than the actual meaning of the arguments has
changed recently, to make the two approaches basically indistinguishable.
This happened as part of the resolution to
http://hackage.haskell.org/trac/ghc/ticket/2247 as I understand it.
In particular this broke similar code that relied on this functionality in lens
and forced a rather large number of patches that had made (ab)use of the old
fundep behavior to be reverted in lens.
Consequently, I don't think you'll find much of a difference between the type
family and the functional depency, except that the latter is forced to infect
more type signatures.
Obviously it will still not allow determining the type of a record from
the type of one of its fields, but that doesn't seem unreasonable to me.
Have you any examples where this will be problematic?
Well, it does have the unfortunate consequence that it dooms the lifted
instance we talked about that could make all field accessors automatically lift
into lenses, as that required inference to flow backwards from the 'field' to
the 'record'.
Moreover, I suggest that Has constraints are only introduced when there
are multiple fields with the same name in scope, so existing code (with
no ambiguity) will work fine.
The awkward part about that is that it becomes impossible to write code that is
polymorphic and have it get the more general signature without putting dummies
in scope just to force conflict.
-Edward
Thanks,
Adam
On 01/07/13 15:48, Edward Kmett wrote:
> It strikes me that there is a fairly major issue with the record
> proposal as it stands.
>
> Right now the class
>
> class Has (r :: *) (x :: Symbol) (t :: *)
>
> can be viewed as morally equivalent to having several classes
>
> class Foo a b where
> foo :: a -> b
>
> class Bar a b where
> bar :: a -> b
>
> for different fields foo, bar, etc.
>
> I'll proceed with those instead because it makes it easier to show the
> issue today.
>
> When we go to compose those field accessors, you very quickly run into a
> problem due to a lack of functional dependencies:
>
> When you go to define
>
> fooBar = foo.bar
>
> which is perfectly cromulent with existing record field accessors you
> get a big problem.
>
> fooBar :: (Foo b c, Bar a b) => a -> c
>
> The b that should occur in the signature isn't on the right hand side,
> and isn't being forced by any fundeps, so fooBar simply can't be written.
>
> Could not deduce (Foo b0 c) arising from a use of `foo' from the context
> (Bar a b, Foo b c)
>
> If you leave off the signature you'll get an ambiguity check error:
>
> Could not deduce (Foo b0 c)
> arising from the ambiguity check for `fooBar'
> from the context (Bar a b, Foo b c)
> bound by the inferred type for `fooBar':
> (Bar a b, Foo b c) => a -> c
>
> It strikes me that punting all functional dependencies in the record
> types to the use of equality constraints has proven insufficient to
> tackle this problem. You may be able to bandaid over it by including a
> functional dependency/type family
>
> class Has (r :: *) (x :: Symbol) where
> type Got r x :: *
> getFld :: r -> Got r x
>
> (or to avoid the need for type applications in the first place!)
>
> class Has (r :: *) (x :: Symbol) where
> type Got r x :: *
> getFld :: p x -> r -> Got r x
>
> This has some annoying consequences though. Type inference can still
> only flow one way through it, unlike the existing record accessors, and
> it would cost the ability to 'cheat' and still define 'Has' for
> universally quantified fields that we might have been able to do with
> the proposal as it stands.
>
> -Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
