#3632: lift restrictions on records with existential fields, especially in the
presence of class constraints
----------------------------------------------------+-----------------------
Reporter: eflister | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.10.4
Severity: normal | Resolution:
Keywords: existential records accessor update | Difficulty: Unknown
Testcase: | Os:
Unknown/Multiple
Architecture: Unknown/Multiple |
----------------------------------------------------+-----------------------
Comment (by eflister):
wow, thanks for getting back to me so fast!
> 1. if a record had two existential fields (e.g. `dur1,dur2::x`), you'd
have to update them both simultaneously.
ah, i see what you mean. 'dur1,dur2::x', is an assertion that dur1 and
dur2 have the same type, even if that type is not concretely known (only
that it is in class NoteDur). but if this were written 'dur1::x,dur2::y',
with 'forall x y. NoteDur x, NoteDur y', then they could be independently
updated, right, even though there are two existential fields?
> 2. Either I misunderstand you, or this is unsound. Remember, the type
'x' is unknown, so it can't be supplied by the caller. So, as far as I can
see this is a non-starter.
i know you know what your'e talking about -- so i'm just not seeing
something! :) but don't lots of functions have a type like this? all
the caller needs to do is restrict itself to using methods of class
SomeClass, it never has to know the underlying type.
> 3. This is already possible
> {{{
> data ModDur where
> Dotted :: NoteDur x => x -> ModDur
> Triplet :: DurBase -> ModDur
> }}}
oh ok, sorry, that worked! i hadn't seen that way (i don't fully grok
GADTs). but it still seems like the following form would be more
uniform/natural.
{{{
data ModDur = NoteDur x => Dotted x | Triplet DurBase
}}}
and what about line 107? following the same approach you suggested, maybe
something like:
{{{
data Note where
Note :: NoteDur x => x -> Note
...
}}}
but i don't see where to go from there, or a nice way to have multiple
existential fields, etc. the following feels very natural to me, just
omitting the forall (implicit universal quantification seems to already be
present in the first place):
{{{
data Note = NoteDur x => Note {
midiNum :: Int -- 0-255
, vel :: Int -- 0-255
, chan :: Int -- 0-15
, measure :: Integral a => a
, beat :: Int
, subdiv :: RealFrac a => a -- % of beat
, dur :: x
}
}}}
although i think it is tricky to find a way to communicate the difference
between class constraints expressed inside vs. outside the Note
constructor. it's something like compile-time vs. runtime polymorphism,
right? but for such a big difference, this difference in expression
doesn't make that clear at all.
> 4. I don't understand this at all. In your example
> {{{
> quarters (x y) = quarters y * case x of
> }}}
> what are you expecting 'x' to be bound to? The constructor itself?
If so, you are way beyond Haskell. Check out [http://www-
staff.it.uts.edu.au/~cbj/patterns/ Barry Jay's excellent work].
right -- don't we pattern match on constructors frequently? would binding
them leak out of this kind of application and cause ambiguous problems in
other situations? the reference looks very relevant -- are those ideas
not amenable to inclusion in haskell? in this example, i wasn't just
playing golf -- i was trying to express the idea that the 'quarters' part
of the function is constant, only the factor 3/2 vs. 2/3 is sensitive to
the input. is there a natural way to do this in haskell that i'm missing?
> 5. I have no idea what you mean here.
sorry. :) note in the example:
{{{
class NoteDur a where
beats :: (Real x, Floating x) => a -> x
-- beats d = (quarters d) / (quarters $ unit timeSig) -- want to factor
out the application of quarters
-- beats d = uncurry (/) $ join (***) quarters (d, unit timeSig) --
join (***) from Saizan_ @ #haskell, but isn't existentially polymorphic
beats d = uncurry (/) $ both quarters (d, unit timeSig)
where both (f :: forall a b. (NoteDur a, Real b, Floating b) => a ->
b) (x, y) = (f x, f y) -- lame that this has to be class specific
(copumpkin @ #haskell says a 'forall classes' would be nice)
}}}
again, i wanted to factor out the application of quarters to the nominator
and denominator, to show that it is not a free choice. but i couldn't
find a natural way to express this -- since the nominator and denominator
are different types, it is hard to find a way to map the application of
'quarters' over them in a way that interacts nicely with expressing that
there must be exactly two (one denominator and one nominator, so we can
later divide them). i wind up having to define 'both' -- which already is
a bit unnatural. but what makes it really unsatisfying is that both has
to be defined just to operate on these specific classes -- there's no way
that i could find to express "apply some class method to exactly N class
instances" without *specifying* the classes involved. then copumpkin
mentioned that he had run into similar situations and thought a "forall
classes" construct would give you the desired polymorphism here. so
something like:
{{{
both :: (forall p q a b. (p a, q b) => a -> b) -> (a,a) -> (b,b)
}}}
but what is really wanted is some kind of existential tuple map -- one
shouldn't have to write 'both' manually and specifically for each N...
{{{
mapTup'' :: (forall p q a b. (p a, q b) => a -> b) -> (a,a) -> (b,b)
mapTup''' :: (forall p q a b. (p a, q b) => a -> b) -> (a,a,a) -> (b,b,b)
...
}}}
maybe if every tuple were a functor, fmap could be defined like this? as
long as it worked existentially...
> 6. Quite possible, along the lines of tuple sections. The
complexity/benefit ratio is debatable; my nose says "not quite worth it"
but I'd be interested to know what others think.
yeah i hear you. it was from the perspective of someone new to haskell
trying to internalize its philosophy and apply it consistently, it's just
kind of a nasty surprise when it doesn't work.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3632#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
