lift restrictions on records with existential fields, especially in the presence of class constraints

[eflister]

the attached file demos the use of a record with an existential field with a class constraint. it shows several cases where lifting the current restrictions on accessing and updating this field would be both well-defined and useful.

here is the record definition; the dur field is existential, but constrained to be in class NoteDur.

data Note = forall x . 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
    }

here is a walk through of places in the code where the current restrictions are unnecessary and intrusive:

1. lines 64-95 -- these functions wouldn't be necessary if record update syntax were enabled for both existential and non-existential fields. i know 6.12 introduces it for non-existentials, but i don't see why it isn't also possible for existential fields (even without a class constraint). lines 33-35 and 60 show how much nicer it is to use regular updater syntax in this case.

2. Line 142. The same is true for existential accessors when there is a class constraint -- there's no need to restrict this situation because the accessor can have type:

   fieldName :: (SomeClass x) => Record -> x
   

   line 142 shows a case where this would be very nice to have.

3. line 100 + 107 -- the foralls could be implicit (maybe offer an extention that would allow them to be implicit)

4. lines 134-136 compared to 138-139 show how additional factoring could be achieved if one were allowed to pattern match on the type of an existential with class constraints.

5. lines 124-127 show how it would be nice to have existential classes

6. lastly, allow curried updater functions: (rec {field = }) 5 instead of (\x -> (rec {field = x})) 5

[simonpj]

Brief responses.

1. It's not all that simple; if a record had two existential fields (e.g. dur1,dur2::x), you'd have to update them both simultaneously. But the rule could, and probably should, be: if the desugared version typechecks, so should the record-update form. So, yes.

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.

3. This is already possible

   data ModDur where
     Dotted :: NoteDur x => x -> ModDur
     Triplet :: DurBase -> ModDur
   

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 ​Barry Jay's excellent work.

5. I have no idea what you mean here.

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.

So for me (1) is the thing that would be worth fixing. I remember spending a while thinking about doing this a year ago, but I didn't do it for some reason. I think it might have been to do with generating sensible error messages.

Simon

[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 ​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.

[thoughtpolice]

Moving to 7.10.1.

[thoughtpolice]

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

[thoughtpolice]

Milestone renamed