Henrik Nilsson
Hi,
Just checking my understanding here as I have not followed this thread in all its details.
So, with both DORF ''', am I correct in understanding that polymorphic fields, be it universally quantified as in
Good question Henrik! It's explicitly answered in the wiki, because it's a tricky area. Briefly: - both of those varieties of poly fields are possible - both can be declared in records - both can be extracted and applied in polymorphic contexts - DORF supports updating the universally quantified, including changing the type of the field and therefore of the record. (Also there's a Quasifunctor proposal for SORF to do that.) - Neither approach supports updating the existential/higher-ranked variety. (There are all the complexities you discuss in detail. They are solved (with quite a bit of complexity behind the scenes), except for updating h-r types.) You can still use explicit data constructurs to pattern match and update h-r fields. Question for you: (you've already given an example of wanting to update a universally quant'd field and change its type) Do you want to update a h-r field? If so, what's the use case? AntC
data ARecordType a = C1 { ..., fieldX :: a, ..., fieldY :: a -> a, ... }
or existentially quantified as in:
data AnotherRecordType = forall a . C2 { ..., fieldU :: a, ..., fieldV :: a -> Int, ... }
would no longer be possible?
Note that the type variable a in both cases scope just over the constructor(s) of the data type in question. So any attempt at declaring the types of the fields outside of this context, be it explicitly with the fieldLabel notation, or implicitly as per your proposal, would not be possible. E.g.
fieldLabel fieldY :: a -> a
would presumably mean
fieldLabel fieldY :: forall a . a -> a
resulting in ARecordType becoming second-order polymorphic where the value of fieldY would *have* to be a polymorphic function, which is very different from the original definition.
Similarly, the whole point with the existentially quantification is to allow a number of fields to share some specific but arbitrary type, which again means that any attempt to type these fields outside of the context of the datatype to which they belong would result in something different.
Note that fieldU and fieldV cannot be used as projection functions due to escaped type variables, but that field selection by pattern matching is perfectly fine.
Both constructions above are very useful and, I'd argue that a design that rules them out actually is a rather poor fit for a language like Haskell.
To be completely honest, I, at least, would be much happier keeping working around the present limitations of Haskell's named fields by picking my field names carefully, than losing the above.
Or am I missing something? E.g. is the idea that sharing of fields only applies to fields of monomorphic type, i.e. whose type can be declared globally?
Best,
/Henrik