Field accessor type inference woes

[Edward Kmett]

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

Re: Field accessor type inference woes

[Adam Gundry]

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


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Edward Kmett]

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry 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

Re: Field accessor type inference woes

[AntC]

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


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Field accessor type inference woes

[Simon Peyton-Jones]

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

Re: Field accessor type inference woes

[AntC]

> Simon Peyton-Jones  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 twhere
   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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Adam Gundry]

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 twhere
>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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Edward Kmett]

On Tue, Jul 2, 2013 at 4:53 AM, AntC  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@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Twan van Laarhoven]

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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[AntC]

> Simon Peyton-Jones  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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Barney Hilken]

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.


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[Adam Gundry]

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

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Field accessor type inference woes

[AntC]

> Adam Gundry  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



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users