Edward Kmett | 1 Jul 16:48 2013
Picon

Field accessor type inference woes

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Adam Gundry | 1 Jul 19:07 2013
Picon
Picon

Re: Field accessor type inference woes

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.

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?

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.

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
Edward Kmett | 1 Jul 19:21 2013
Picon

Re: Field accessor type inference woes

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry <adam.gundry <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 2 Jul 10:57 2013
Picon

RE: Field accessor type inference woes

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:ekmett <at> gmail.com]
Sent: 01 July 2013 18:21
To: Adam Gundry
Cc: Simon Peyton-Jones; glasgow-haskell-users <at> haskell.org
Subject: Re: Field accessor type inference woes

 

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry <adam.gundry <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
AntC | 2 Jul 12:45 2013
Picon

Re: Field accessor type inference woes

> Simon Peyton-Jones <simonpj <at> microsoft.com> writes:
> 
>  ...; it’s a tradeoff between polymorphism and overloading.
>  

Hah! my post crossed with Simon's. This time I'll be succinct.
There's **three** alternatives. ...

>
>           data R a = MkR { foo :: a -> a }
>           data S    = MkS { bar :: forall b. b -> b }
>  

Try Plan C: use a cleverer (associated) type function

    class Has r f t    where
       type GetResult r f t :: *               -- ?? default to t
       getFld :: r -> GetResult r f t

    instance (t ~ a->a) => Has (R a) “foo” t where
       type GetResult (R a) "foo" t = a -> a   -- ?? ignore t
       getFld ...
    instance (t ~ b->b) => Has S “bar” t where 
       type GetResult S "bar" t = t      -- 'improved' t
       getFld ...

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)

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Adam Gundry | 2 Jul 13:12 2013
Picon
Picon

Re: Field accessor type inference woes

Unfortunately, I don't think we get away with this...

On 02/07/13 11:45, AntC wrote:
> There's **three** alternatives. ...
> 
>>
>>           data R a = MkR { foo :: a -> a }
>>           data S    = MkS { bar :: forall b. b -> b }
>>  
> 
> Try Plan C: use a cleverer (associated) type function
> 
>     class Has r f t    where
>        type GetResult r f t :: *               -- ?? default to t
>        getFld :: r -> GetResult r f t
> 
>     instance (t ~ a->a) => Has (R a) “foo” t where
>        type GetResult (R a) "foo" t = a -> a   -- ?? ignore t
>        getFld ...
>     instance (t ~ b->b) => Has S “bar” t where 
>        type GetResult S "bar" t = t      -- 'improved' t
>        getFld ...
> 
> 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)

GetResult isn't necessarily injective (and GHC couldn't tell if it was)
so there is no way to determine `t` from `GetResult r f t`. I tried
prototyping this, and it leads to errors like

    Couldn't match type `GetResult (GetResult a "bar" t1) "foo" t0'
                  with `GetResult (GetResult a "bar" t2) "foo" t'
    NB: `GetResult' is a type function, and may not be injective
    The type variables `t0', `t1' are ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: a -> GetResult (GetResult a "bar" t2) "foo" t
      Actual type: a -> GetResult (GetResult a "bar" t1) "foo" t0

I agree with Simon that we should stick with the current plan, and
accept the fact that composition of polymorphic record selectors isn't
going to work, though this does make me sad. I'm not sure about
restricting quantification over the Has class, because some uses are
perfectly fine (aliasing a selector, for example).

Adam

--

-- 
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Twan van Laarhoven | 2 Jul 16:26 2013
Picon

Re: Field accessor type inference woes

On 02/07/13 10:57, Simon Peyton-Jones wrote:
> 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.

How common are such polymorphic fields in practice? You sometimes see them in 
newtype wrappers and the like. But I think those are not cases where you want 
overlapping names anyway.

So: why not use a Plan A style class, except for polymorphic fields? Perhaps you 
could still have a (less polymorphic) class for bar above,

     class HasBar r where
         getBar :: r -> b -> b

Twan

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
AntC | 4 Jul 13:27 2013
Picon

Re: Field accessor type inference woes

> Simon Peyton-Jones <simonpj <at> microsoft.com> writes:
> 
> Edward, is quite right.  Thank you for pointing this out; I hadn’t fully
> absorbed the consequences of the three-parameter Has class. ...

Thank you Simon, Edward, Adam. There is quite a complex design space 
(and I apologise for trailing a red herring earlier).

Simon/Adam's Plan is (in effect) favouring higher-ranked polymorphism 
over record nesting/chaining.

H-R fields are a limitation because we can't update them either.
So I think it's a fair question 
whether supporting h-r polymorphism is worth the limitations?

Edward pointed out earlier, circumstances where lenses:
>> required inference to flow backwards from the 'field' to the 'record'

So that 'feature' of H98 records we've deliberately abandoned, because:

> Let’s review the goal:
> to allow you to use the same field name in different records.

Therefore we can't have the field determining the record type.

We've also abandoned having the field (alone) determine the field's type.
I can see a genuine use case for (for example) personId is always Int,
irrespective of the record type in which personId appears.

(This is a 'silent' feature of H98, because the field can appear in only 
one record type, so it's moot whether it's the field or field+record 
determining the field's type.)

This would be a strong motivation for overloaded fields refraining 
from generating the fully polymorphic field selector functions.
That is, set -XNoRecordSelectorFunctions, then I could declare:

    personId :: r { personId :: Int } => r -> Int
    personId = getFld

Or perhaps there could be some way to declare that a given field is always 
at a specific type?

Does this help with Edward's chained/nested records example?
Does the field name in the outer record determine the type of the inner?
(I guess we're in trouble if the inner is (parametric) polymorphic?)

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Barney Hilken | 4 Jul 14:47 2013

Re: Field accessor type inference woes

The two points in AntC's message suggest a possible compromise solution. Unless I've missed something,
this allows nested fields, fixed type projections, and HR fields. The only restriction is that HR fields
must be
fixed type, though they can still be used in multiple records.

1. Use an associated type class for Has, to solve the nesting problem:

	class Has (r :: *) (x :: Symbol) where
		type GetField r x :: *
		getField :: r -> GetField r x

(Maybe a fundep would also work, but I'm more used to thinking with associated types.)

2. Introduce a declaration for fixed type fields:

	field bar :: Bar

is translated as:

	class Has_bar r where
		bar :: r -> Bar

	instance Has_bar r => Has r "bar" where
		GetType r "bar" = Bar
		getField = bar

3. Undeclared fields and those declared typeless don't have their own class:

	field bar

is translated as

	bar :: Has r "bar" => r -> GetType r "bar"
	bar = getField

4. Now you can use HR fields, provided you declare them first:

	field bar :: forall b. b -> b

is translated as:

	class Has_bar r where
		bar :: r -> forall b. b -> b

	instance Has_bar r => Has r "bar" where
		GetType r "bar" = forall b. b -> b
		getField = bar

which doesn't look impredicative to me.

Does this work, or have I missed something?

Barney.
Adam Gundry | 4 Jul 21:19 2013
Picon
Picon

Re: Field accessor type inference woes

On 04/07/13 12:27, AntC wrote:
> H-R fields are a limitation because we can't update them either. So I
> think it's a fair question whether supporting h-r polymorphism is
> worth the limitations?

Yes, higher rank polymorphism is bound to cause trouble with polymorphic
projections, and perhaps it won't matter if we limit ourselves to one or
the other.

> Edward pointed out earlier, circumstances where lenses:
>>> required inference to flow backwards from the 'field' to the
>>> 'record'

Crucially, Edward pointed out that this is needed to make polymorphic
record fields into lenses automatically [1], which I'm quite keen on. So
that's an additional reason for sticking with the current story.

> This would be a strong motivation for overloaded fields refraining
> from generating the fully polymorphic field selector functions.
> That is, set -XNoRecordSelectorFunctions, then I could declare:
>
>     personId :: r { personId :: Int } => r -> Int
>     personId = getFld
>
> Or perhaps there could be some way to declare that a given field is
> always at a specific type?
>
> Does this help with Edward's chained/nested records example?
> Does the field name in the outer record determine the type of the inner?
> (I guess we're in trouble if the inner is (parametric) polymorphic?)

In some circumstances, it might well remove ambiguity if we knew that a
field always had a consistent type. I wonder how to declare this. If we
were using the type family version then the user could declare

type instance GetResult r "personId" = Int

independently of any data declarations.

Alas...

On 04/07/13 13:47, Barney Hilken wrote:
| The two points in AntC's message suggest a possible compromise
solution. Unless I've missed something,
| this allows nested fields, fixed type projections, and HR fields. The
only restriction is that HR fields must be
| fixed type, though they can still be used in multiple records.

| [...]

| 	class Has_bar r where
| 		bar :: r -> forall b. b -> b
|
| 	instance Has_bar r => Has r "bar" where
| 		GetType r "bar" = forall b. b -> b
| 		getField = bar
|
| which doesn't look impredicative to me.
|
| Does this work, or have I missed something?

...this associated type declaration isn't legal, because type families
are not allowed to return polymorphic type schemes. (It's far from clear
how one would do type inference for such monsters.)

Adam

[1]
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Plan#Polymorphicrecordupdateforlenses
AntC | 5 Jul 08:11 2013
Picon

Re: Field accessor type inference woes

> Adam Gundry <adam.gundry <at> strath.ac.uk> writes:
>
> > On 04/07/13 12:27, AntC wrote:
> > H-R fields are a limitation because we can't update them either. So I
> > think it's a fair question whether supporting h-r polymorphism is
> > worth the limitations?
> 
> Yes, higher rank polymorphism is bound to cause trouble with polymorphic
> projections, and perhaps it won't matter if we limit ourselves to one or
> the other.
> 

So with h-r fields, let's stratify the requirements:
* The current Plan tries to support holding h-r fields
  in a way backwards-compatible with H98 records.
  Why? We know that OverloadedFields are going to break some stuff.
  It's a question of which stuff is more important to not break.

* I think the real requirement is to hold an h-r value
  in a record, accessible by field name.

Consider TPDORF does this:
(see example based on one in SPJ's SORF 
http://hackage.haskell.org/trac/ghc/wiki/Records/TypePunningDeclaredOverloa
dedRecordFields#Implementation:theHasclasswithmethodsgetandsetandpunnedType
s     at 'Higher-Ranked polymorphic fields' )

  -- must wrap h-r values in a newtype to put them in a record.
    newtype Rev = Rev (forall a. [a] -> [a])
    data HR = HR { rev :: Rev }

  -- Has class takes 2 args, with type family for GetResult
    type instance GetResult r "rev"     = Rev
    instance Has HR "rev"                         where
        getFld HR{ rev = (Rev x) } = Rev x
                    -- can't unwrap here, 'cos can't spec Polymorphic

Then user code must unwrap the newtype at point of applying.

I think this approach also allows update for h-r values (providing they're 
wrapped) -- but I must admit I rather ran out of steam with the prototype.

TPDORF also supported type-changing update for parametric polymorphic 
fields -- but with limitations. To get round those you would have to 
revert to H98 record update -- just as the current Plan.

So I'm tending to the conclusion that cunning though it is to use 
"a functional-dependency-like mechanism (but using equalities) 
for the result type",
that is actually giving too much of a headache.

**bikeshed:
I do like the proposed sugar for constraints (r { f :: t }) => ...
But how does that play if `Has` only needs 2 args?

AntC
AntC | 2 Jul 10:53 2013
Picon

Re: Field accessor type inference woes

> 
> 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
Edward Kmett | 2 Jul 15:51 2013
Picon

Re: Field accessor type inference woes

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane