Re: Why not allow empty record updates?
> Another place this problem has come up for me is in wanting to ensure > representation sharing for values constructed by data constructors which > don't make use of their type parameters. A trivial example would be sharing > the representation of Nothing between all the Maybe types, or sharing the > empty list among all the list types. That example isn't especially > motivating, but there are other cases where we can end up with a large > structure for which the type parameters are 'phantom' even though they may > not be phantom in general (because other data constructors make use of > them). That we want type updates for records with phantom types is just a > symptom of the larger issue of wanting type updates for all > quasiphantom/pseudophantom types. I feel like this is similar (or the same) as an issue I've had like: data X a = A a | B Z Z | C Z | D Z Z Z -- | Cast the type by stripping out an A. cast :: X a -> Maybe (X b) cast x = case x of A _ -> Nothing no_a -> Just no_a Except of course that no_a isn't going to work, I have to write case branches for B, C, and D and reconstruct them exactly the same way only with a different type, even though it's a type they don't depend on. I assume sharing is destroyed, but it seems like it should be possible to keep it, just like the various types of Nothing and []. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
On 11/15/11 8:07 PM, wagne...@seas.upenn.edu wrote:
Quoting wren ng thornton :
So far I've just defined helper functions to adjust the phantom
type[1], each of which is implemented by (\x -> x { foo = foo x }).
It's a horrible hack, but at least it's hidden away in library
functions instead of something I have to look at. The annoying part
(a bit tongue-in-cheek, and hence not sent to the mailing list)
Forwarding to the list, because I actually have a serious response :)
As long as we're writing hacks, why not use unsafeCoerce? ;-)
In this particular case I don't care too much about representation
sharing (though I do share Ed's concern), and I generally do my best to
avoid unsafeFoo just so I can minimize my personal proof obligations /
maximize the utility of the compiler's type checking.
Though, yes, in other projects with similar considerations I've also
gone the unsafeCoerce route. Other than invalidating type system
guarantees, it does have the side effect that it can interfere with
rewrite rules firing (since the coercion remains in the System Fc core).
And the times when I really care about representation sharing are often
also the times I really care about rewrite rules firing. Which in turn
means I tend to add additional rewrite rules to push the unsafeCoerce
around in order to get it out of the way so that other rules can fire.
But I see no way of specifying these additional rules in full generality
while retaining correctness--- without some additional mechanism to say
things like "this newtype wrapper is opaque in these contexts (to
preserve the abstract semantics), but is translucent in these other
contexts (to abide by categorical laws like functorality). It's really
unfortunate that these complementary goals of sharing representation and
doing rewrites/fusion are at odds in current Haskell.
I run into similar issues with needing to work around coercions in Coq,
since they impede the evaluator and proofs of value equality due to the
weakness of Coq's case analysis. That the issue shows up in Coq as well
seems to imply that the root of the problem is something deeper than
noone having implemented the convenience. Agda has a stronger case
analysis and so doesn't run into quite the same issues, though I'm not
entirely clear on the exact ways in which Agda's case analysis gains
that extra power, so it's unclear whether we could (meaningfully) add
the power to Haskell without going whole hog into dependent types.
Of course, this all is related to the problem of strong updates; it just
happens that the update is Curry-identical, yet Church-different. Given
the general preference for Church-style lambda calculi, it's not
surprising that this exact problem hasn't been tackled (to my knowledge).
Another place this problem has come up for me is in wanting to ensure
representation sharing for values constructed by data constructors which
don't make use of their type parameters. A trivial example would be
sharing the representation of Nothing between all the Maybe types, or
sharing the empty list among all the list types. That example isn't
especially motivating, but there are other cases where we can end up
with a large structure for which the type parameters are 'phantom' even
though they may not be phantom in general (because other data
constructors make use of them). That we want type updates for records
with phantom types is just a symptom of the larger issue of wanting type
updates for all quasiphantom/pseudophantom types.
--
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Why not allow empty record updates?
| >> Trouble is, what type does this have?
| >> f x = x {}
| >>
| >> Malcolm Wallace wrote:
| > f :: a -> a
| >>
| >> Ian Lynagh wrote:
| That wouldn't help the original poster, as it is incompatible with
| f :: Foo Clean -> Foo Dirty
There are several different things going on in this thread.
1. What does f x = x {} mean? The report
http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-490003.15
says we should treat it like
f x = case x of
C1 a b -> C1 a b
C2 v -> C2 v
but if there are no fields how do we know what C1 and C2 are? The whole
section only makes sense if you know x's type. So Malcolm's suggestion of "f
:: forall a. a -> a" would be non-uniform with the non-empty cases.
When we *do* know the type then the above translation makes sense, and even
allows the
f :: Foo Clean -> Foo Dirty
type-change. Now two further issues arise:
2. When do we "know the type"? If the type is supposed to come from an
enclosing type signature, to specify the type system one would need to specify
the way that type annotations propagate. This isn't impossible (we do it for
higher-rank types), but it seems like a big hammer for this particular nut.
3. Edward wants to maintain sharing, meaning presumably that no fresh record
is allocated. That makes sense, but sadly System FC (GHC's intermediate
language) has no way to express it. We'd need some new axioms claiming that
forall ab. Foo a ~ Foo b. But that's a question for another time. Moreover,
it affects non-record types just as much.
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
I wrote:
>> Yes. The translation of record updates given in the Report
>> makes perfect sense for {}. It is only forbidden by
>> "n >= 1", but no reason is given for that restriction.
d wagner wrote:
> It doesn't make sense to me. The translation explodes a value into a case
> statement over its constructors; what constructors do you use when you don't
> know the type of the value?
> When n >= 1, you know the type of the value by looking where the field came
> from, and hence which constructors to use in the case statement.
Well, yes, you need to know the type. That's why I asked
Simon if there is difficulty with implementation.
I do have an algorithm in mind, but it seemed silly for me
to write it out given that I know near zero about
the implementation details of GHC's type checker.
But if you insist, here is a rough sketch:
Replace each subexpression of the form e {} by
v' and add v = e to the let bindings, where v and v' are
fresh variables. Resolve the type. For any v that resolves
to an ADT (even if the types of its parameters are not
resolved), replace e {} in the original expression by
its case expansion. Repeat until all are resolved,
rejecting the program if an iteration does not resolve
any v. Resolve the final form of the expression one
more time to obtain its type.
Does this make any sense?
Thanks,
Yitz
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
Sent from my iPad
On Nov 15, 2011, at 7:18 PM, wren ng thornton wrote:
> On 11/15/11 12:33 PM, Yitzchak Gale wrote:
>> Simon Peyton-Jones wrote:
>> Trouble is, what type does this have?
>> f x = x {}
>>
>> Malcolm Wallace wrote:
> f :: a -> a
>>
>> Ian Lynagh wrote:
That wouldn't help the original poster, as it is incompatible with
f :: Foo Clean -> Foo Dirty
>>
>> Only because in that expression the type of x is not known.
>>
>> ...the whole feature of type-changing update is (as you know)
>> a bit obscure and not widely used, so it'd be adding
>> complexity to an already-dark corner.
>>
>> To me, at least, that is surprising. The report implies that
>> record updates are just sugar for the given case expression.
>> Whether or not it changes a type parameter seems
>> unimportant.
>>
>> In fact, I would even advocate adding a line of explanation
>> in the Report that this is a convenient way of copying
>> a value from an ADT to itself with a different type
>> as its parameter. I agree with Malcolm that this is
>> analogous to using empty record syntax in a pattern
>> to avoid hard-coding the number of parameter to
>> a constructor.
>>
>> I usually avoid using the combination of type parameters and
>> record syntax altogether, mainly because this obvious syntax
>> doesn't work. Perhaps that's the reason why type-changing
>> update is not widely used.
>>
>> (Admittedly, I didn't think of Herbert's trick. But doesn't
>> that seem like somewhat of an ugly hack?)
>>
>> Are you hesitant because of implementation difficulty,
>> or only because you are worried about the semantics
>> being confusing? In my opinion, it's more confusing
>> the way it is now.
>
> For what it's worth, I do the exact same thing in the project I've been
> working on. The phantom type is a clean/dirty bit even :)
>
> It's an incredibly helpful thing to have for records. Especially for the
> context I'm in: I'm generating summary data over gobs of input, but the input
> can come incrementally. So long as the core of the summary is correct, then I
> don't care about maintaining the cache fields while I'm just shoveling data
> in; but I do want to make sure the caches are valid before I try to get any
> information out. This is exactly the sort of type-level hackery which makes
> Haskell a joy to work in and other languages such a pain.
>
> So far I've just defined helper functions to adjust the phantom type[1], each
> of which is implemented by (\x -> x { foo = foo x }). It's a horrible hack,
> but at least it's hidden away in library functions instead of something I
> have to look at. The annoying part is that when I adjust the members of the
> records, if I remove or rename foo then I have to fix all those coercion
> functions too.
>
My biggest issue is loss of sharing, but you could always use
castFoo = asTypeOf unsafeCoerce $ \x -> x { foo = foo x }
to maximize sharing, but that doesn't help with the code rewriting,
Or less horrifically just carry the phantom in a newtype wrapper wrapped around
your record, and cast by putting it on and taking it off, which also maximizes
sharing in exchange for newtype noise on access.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
On 11/15/11 12:33 PM, Yitzchak Gale wrote:
Simon Peyton-Jones wrote:
Trouble is, what type does this have?
f x = x {}
Malcolm Wallace wrote:
f :: a -> a
Ian Lynagh wrote:
That wouldn't help the original poster, as it is incompatible with
f :: Foo Clean -> Foo Dirty
Only because in that expression the type of x is not known.
...the whole feature of type-changing update is (as you know)
a bit obscure and not widely used, so it'd be adding
complexity to an already-dark corner.
To me, at least, that is surprising. The report implies that
record updates are just sugar for the given case expression.
Whether or not it changes a type parameter seems
unimportant.
In fact, I would even advocate adding a line of explanation
in the Report that this is a convenient way of copying
a value from an ADT to itself with a different type
as its parameter. I agree with Malcolm that this is
analogous to using empty record syntax in a pattern
to avoid hard-coding the number of parameter to
a constructor.
I usually avoid using the combination of type parameters and
record syntax altogether, mainly because this obvious syntax
doesn't work. Perhaps that's the reason why type-changing
update is not widely used.
(Admittedly, I didn't think of Herbert's trick. But doesn't
that seem like somewhat of an ugly hack?)
Are you hesitant because of implementation difficulty,
or only because you are worried about the semantics
being confusing? In my opinion, it's more confusing
the way it is now.
For what it's worth, I do the exact same thing in the project I've been
working on. The phantom type is a clean/dirty bit even :)
It's an incredibly helpful thing to have for records. Especially for the
context I'm in: I'm generating summary data over gobs of input, but the
input can come incrementally. So long as the core of the summary is
correct, then I don't care about maintaining the cache fields while I'm
just shoveling data in; but I do want to make sure the caches are valid
before I try to get any information out. This is exactly the sort of
type-level hackery which makes Haskell a joy to work in and other
languages such a pain.
So far I've just defined helper functions to adjust the phantom type[1],
each of which is implemented by (\x -> x { foo = foo x }). It's a
horrible hack, but at least it's hidden away in library functions
instead of something I have to look at. The annoying part is that when I
adjust the members of the records, if I remove or rename foo then I have
to fix all those coercion functions too.
[1] set bit to Clean, set bit to Dirty, and unsafe set bit to 'a'.
--
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
Quoting Yitzchak Gale :
Yes. The translation of record updates given in the Report
makes perfect sense for {}. It is only forbidden by
"n >= 1", but no reason is given for that restriction.
It doesn't make sense to me. The translation explodes a value into a
case statement over its constructors; what constructors do you use
when you don't know the type of the value?
When n >= 1, you know the type of the value by looking where the field
came from, and hence which constructors to use in the case statement.
~d
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
Simon Peyton-Jones wrote:
Trouble is, what type does this have?
f x = x {}
Malcolm Wallace wrote:
>>> f :: a -> a
Ian Lynagh wrote:
>> That wouldn't help the original poster, as it is incompatible with
>> f :: Foo Clean -> Foo Dirty
Only because in that expression the type of x is not known.
...the whole feature of type-changing update is (as you know)
a bit obscure and not widely used, so it'd be adding
complexity to an already-dark corner.
To me, at least, that is surprising. The report implies that
record updates are just sugar for the given case expression.
Whether or not it changes a type parameter seems
unimportant.
In fact, I would even advocate adding a line of explanation
in the Report that this is a convenient way of copying
a value from an ADT to itself with a different type
as its parameter. I agree with Malcolm that this is
analogous to using empty record syntax in a pattern
to avoid hard-coding the number of parameter to
a constructor.
I usually avoid using the combination of type parameters and
record syntax altogether, mainly because this obvious syntax
doesn't work. Perhaps that's the reason why type-changing
update is not widely used.
(Admittedly, I didn't think of Herbert's trick. But doesn't
that seem like somewhat of an ugly hack?)
Are you hesitant because of implementation difficulty,
or only because you are worried about the semantics
being confusing? In my opinion, it's more confusing
the way it is now.
Thanks,
Yitz
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Why not allow empty record updates?
| > > Trouble is, what type does this have?
| > >
| > > f x = x {}
| >
| > f :: a -> a
|
| That wouldn't help the original poster, as it is incompatible with
| f :: Foo Clean -> Foo Dirty
Ah! *That* is why I said it was awkward. Thanks Ian.
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Why not allow empty record updates?
Hmm yes. Fair enough. Does anyone care enough? I can see (now) that it
wouldn't really be hard.
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Yitzchak Gale
| Sent: 15 November 2011 11:16
| To: Malcolm Wallace
| Cc: GHC-users List
| Subject: Re: Why not allow empty record updates?
|
| Simon Peyton-Jones wrote:
| >> Trouble is, what type does this have?
| >> f x = x {}
|
| Malcolm Wallace wrote:
| > Empty record patterns {} are permitted, even for types
| > that are not declared with named fields.
| > So I don't see why an empty record update should
| > require the type to be declared with named fields either.
|
| Yes. The translation of record updates given in the Report
| makes perfect sense for {}. It is only forbidden by
| "n >= 1", but no reason is given for that restriction.
|
| According to that translation, the type of x {} is
| the type of the case expression it translates to.
|
| Thanks,
| Yitz
|
| ___
| 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: Why not allow empty record updates?
On Tue, Nov 15, 2011 at 08:34:01AM +, Malcolm Wallace wrote:
>
> On 14 Nov 2011, at 22:09, Simon Peyton-Jones wrote:
>
> > Trouble is, what type does this have?
> >
> > f x = x {}
>
> f :: a -> a
That wouldn't help the original poster, as it is incompatible with
f :: Foo Clean -> Foo Dirty
Thanks
Ian
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
Simon Peyton-Jones wrote:
>> Trouble is, what type does this have?
>> f x = x {}
Malcolm Wallace wrote:
> Empty record patterns {} are permitted, even for types
> that are not declared with named fields.
> So I don't see why an empty record update should
> require the type to be declared with named fields either.
Yes. The translation of record updates given in the Report
makes perfect sense for {}. It is only forbidden by
"n >= 1", but no reason is given for that restriction.
According to that translation, the type of x {} is
the type of the case expression it translates to.
Thanks,
Yitz
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
On 14 Nov 2011, at 22:09, Simon Peyton-Jones wrote:
> Trouble is, what type does this have?
>
> f x = x {}
f :: a -> a
Empty record patterns {} are permitted, even for types that are not declared
with named fields. So I don't see why an empty record update should require
the type to be declared with named fields either.
Regards,
Malcolm
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Why not allow empty record updates?
Trouble is, what type does this have?
f x = x {}
In your example the type annotations give the clue, but Haskell is mainly
designed for type annotations to be optional. We require at least one field so
we can figure out, from the field name, which type is being updated.
Yes, something could doubtless be done by following the type annotations, much
like higher-rank types, but it would be somewhat tricky to specify -- and the
whole feature of type-changing update is (as you know) a bit obscure and not
widely used, so it'd be adding complexity to an already-dark corner.
See also the (inconclusive) discussion here, which would involve abolishing the
entire type-changing update mechanism entirely!
http://hackage.haskell.org/trac/ghc/wiki/Records
Simon
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Herbert Valerio Riedel
| Sent: 14 November 2011 14:31
| To: glasgow-haskell-users@haskell.org
| Subject: Why not allow empty record updates?
|
| Hello GHC HQ,
|
| I have been toying with phantom types in combination with "polymorphic"
| record-updates (which is a great feature imho), but stumbled over a
| limitation: GHC doesn't allow empty record updates (see toy example
| below), and I couldn't find a GHC language extension to relax this
| constraint. In the toy-example below it was easy to workaround by
| performing a dummy record update, but for more advanced uses workarounds
| becomes a bit more annoying.
|
| Is there a particular reason why empty record updates are disallowed by
| the Haskell Report? Would it be sensible, to allow empty record updates
| as a GHC language extension?
|
|
| hvr.
|
| ---
| -- empty types for tagging
| data Clean
| data Dirty
|
| data Foo a = Foo { fa :: Int, fb :: String }
| data Bar a = Bar { ba :: Int, bb :: Foo a }
|
| markDirtyFoo :: Foo Clean -> Foo Dirty
| markDirtyFoo foo = foo { } -- rejected with "Empty record update" error
| markDirtyFoo foo = foo { fa = fa foo } -- workaround: dummy update
|
| markDirtyBar :: Bar Clean -> Bar Dirty
| markDirtyBar bar = bar { bb = markDirtyFoo (bb bar) } -- works
|
|
|
|
|
|
| ___
| 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
