I disagree heavily here. That proposal’s goal is to alter ADTs, which are a fundamental part of the language, into something quite outlandish with far-reaching implications. It wouldn’t even solve the issue I have, since binding that monstrocity to an existing chunk of memory would be impossible.
Using mutable things unsafely across threads is a design decision that users can already make. This proposal would merely allow people to use mutable things as records, that’s it.
I’m requesting a single new type-level type with a shred of new syntax that could be reneged upon later if it’s implemented as an extension. It, in my estimation, would allow for things that are otherwise excruciatingly painful to do in the language. If this is too tall of an ask to even entertain in a research language, then I think something is amiss.
Why should it? In a future parallel-by-default Haskell, trying to use any shared mutable data risks either:
queueing up all those parallel calls to each have their turn to modify that data, making said parallelism practically useless;
or letting all all those parallel calls occur in any random order, which incurs non-determinism.
So why add another (mis)feature which only “works” for sequential Haskell?
This entire discussion is about type-level dictionaries, it has nothing to do with the execution semantics of resulting data implementations. Yes, you would be able to create a mutable array with a type-level dictionary attached, use it across multiple threads with no synchronization and thus get data races; this is in no way different from what currently exists, where you can create a mutable array with no dictionary and do the exact same thing.
Your initial post says
Mutability surely is to do with execution semantics?
All data in Haskell is immutable, and always has been. (Well OK there are MVars and icky low-level stuff using unsafes: they’re not really part of the language/they’re snuck inside IO.)
The “decade of work … poured into figuring out a good solution to extend the record syntax for ADTs” isn’t aimed at changing anything about execution semantics.
So I’m not seeing why this is a ‘problem’ in Haskell. We just don’t do “low-level programming” – except by callouts to low-level interfaces from within IO.
My motivation for creating this topic is that the current record system is insufficient to tackle certain types of problems. I choose to express it through mutable records because I enjoy low-level programming, but if I enjoyed different things I could as well have done this with immutable arrays (coming from problems with compiling large ADTs, hence the existence of packages like large-records) or pure dictionaries (which at times could use the same record guarantees, e.g. in JWTs or when parsing the Vulkan spec).
On top of that I find the idea of nested record updates for immutable data weird, something I’ve expressed in one of my comments on New notation for records?, so juxtaposing the two makes the most sense in my mind.
And, of course, there’s the fundamental issue that not all C structs are properly convertable to and from ADTs due to potential ambiguities and bit fields, so there simply is no existing solution for that issue.
I will most probably never touch that library. Clumsily parsing C (can’t do it any other way) in Template Haskell and then slapping the words “seamless” and “No FFI” is just too much for me.
I have to say that by now I’ve no idea why “records” is in the title of this topic:
Int or Char variable is just as immutable.Either (Maybe String) (Maybe (Either Int Char))
Int or Char again.If you’re continuing to claim “this doesn’t need any complex proposals” (for some value of “this”), perhaps you could re-state the absolute minimum of your proposal without mention of these collateral concerns?
This makes no sense. Type information is erased when generating object code. Record content must be present at run-time. Perhaps “record data” there means not “data” but “structure”? But again what’s “storing” got to do with it?
Good idea, there’s definitely a more concise way to lay it out.
The baseline proposal is to extend the DataKinds type-level machinery, which currently includes Symbols, Chars and Naturals, with a specialized dictionary, called Fields.
data Field a = Symbol := a
data Fields a
Fields is an ordered dictionary from unique Symbols to types. It is housed in a separate module, GHC.TypeFields, which also provides at least the following set of type families:
type family Empty :: Fields a
-- Fails on duplicate insertion.
-- Should only allow a subset of characters in `Symbol`s to support
-- nested access.
type family Insert (k :: Symbol) (v :: a) (xs :: Fields a) :: Fields a
type family Lookup (k :: Symbol) (v :: a) (xs :: Fields a) :: Maybe a
type family Size (xs :: Fields a) :: Nat
-- Fails when no such symbol exists.
type family Index (k :: Symbol) (xs :: Field a) :: Nat
For construction and display of Fields an additional bit of type-level syntax is necessary, which can mirror standard type-level lists . For future compatibility it could be gated behind an extension.
'{} -- On construction same as `Empty`
'{a := b, c := d} -- On construction same as `Insert a b (Insert c d Empty)`
Users would then be able to create their own datatypes outside of base that use said dictionary to enforce certain type-level expectations.
“records” in the topic name comes from the fact that using an immutable array this way fully overlaps with Haskell98 record syntax feature-wise. Nesting is described to show that dot-notation and the like can be added on top on demand, which is superior to the current approach of creating entire language extensions to the record syntax. Anything involving mutation (including FFI) is too “yet another thing this approach does right”, since it requires no runtime conversions.
And yes, this is pretty much a blind retread of the Row Polymorphism proposal. From my perspective it just doesn’t look like something that needs changes to the type resolution (unless of course writing built-in type families is a whole journey I’m unaware of).
How does it go with Eq for records? Or in general for instances of user-defined classes? Do I have to define an instance for each possible combination of fields (Symbols)?
(For comparison, Hugs/Trex auto-derives Eq for records, but the form of the derived instances are not legal if you wanted to define them for your own class.) I’d be interested to know if/how purescript supports instances for user-defined classes over records.
Since the type-level dictionary is ordered, you can simply get the list of fields and traverse that.
type family ToList (xs :: Fields a) :: [(Symbol, a)]
For some data representations, like a data level dictionary with no unknown fields, equality of data representations yields the same result as traversing all fields.
So once again it would seem like this is a feature that can be built on top completely separately.
There may be a complex example I’m missing here, but in my experience with records coupling what instances do with the total list of fields only works well for simple types.
I think there’s a simple example you’re missing. Please give the instance decls for ToList. And look at all the instances before pressing ‘Send’. Hint: HasField uses FunDeps, not type family for a reason.
-- Built-in
type family MinView (xs :: Fields a) :: Maybe (Field a, Fields a)
type ToList xs = ToList' (MinView xs)
type family ToList' (xs :: Maybe (Field a, Fields a)) :: [Field a] where
ToList' ('Just '(x, xs)) = x ': ToList' (MinView xs)
ToList' 'Nothing = '[]
(although I would expect ToList itself to be built-in, since performance is the goal and MinView by itself isn’t all that useful)
Functional Dependencies section of the the HasField proposal does not claim type families are unfit for the job, merely that functional dependencies both look nicer and using them requires less complexity. The only feature-wise difference between the two I know of is the evidence part and I don’t think that matters in this case.
well then, instances for MinView, since you’re moving the goalposts. And/or perhaps I mean instances for Eq/user-defined classes that (presumably) have to be written over [Field a].
Remember with HasField the user can write their own instances. Which is why I’m asking about instances – that is, the whole set of them.
This has to be built-in and this is why Insert is a function and not a constructor. This is why I say the dictionary must be [strictly totally] ordered, because there must exist an unambiguous way to break it apart, similar to Data.Map.Strict.minView.
My expectation is that in some glorious future it will be possible to efficiently construct a type-level datatype like this directly in Haskell, at which point compiler magic will no longer be required for this.
newtype Rec (xs :: Fields Type) = Rec (SmallArray Any)
instance RecEq xs (ToList xs) => Eq (Rec xs) where
Rec arr == Rec brr = recEq @xs @(ToList xs) arr brr
-- Assumes the given key type instead of looking it up.
unsafeIndex :: forall k xs v n. Index k xs n => Rec xs -> v
class RecEq (ys :: Fields Type) (xs :: [Field Type]) where
recEq :: SmallArray Any -> SmallArray Any -> Bool
instance (Index k ys n, Eq v, RecEq ys xs) => RecEq ys ((k := v) ': xs) where
recEq arr brr = unsafeIndex @k @ys @v (Rec arr) == unsafeIndex @k @ys @v (Rec brr)
&& recEq @ys @xs arr brr
instance RecEq ys '[] where
recEq _ _ = True
This makes sense because ADTs are endowed with unique names, type-level dictionaries do not have that privilege/burden. You can still make a Symbol -> Symbol function to alias names, but built-in functions must only work with names present in the dictionary.
So for an approach that started by dissing type families (3.1 in first post), we now have rather a lot of TFs – most of them recursive at that, plus some built-in magic, plus unsafes. And you’ve ended up somewhere that from a end-user experience is not greatly different from vinyl or purescript’s records or the 2018 proposal or indeed Hugs/Trex.
instances for records have to be defined using something that doesn’t at all look like record syntax. And you appear to be exposing the unsafes to the end-user. (Hugs/Trex 1996 does a lot better here.)
I’ve poked enough inside Hugs/Trex to see there’s plenty of complexity and built-ins and magic – although it uses only FunDeps.
As I stated at the very beginning, the point is not to solve row polymorphism in Haskell once and for all, it’s to get across a bare minimum reasonably-efficient solution that does most of the job.
When I describe type families for the proposal I explicitly mean built-in, as I assume those would incur no recursion penalties. Beyond base I expect everything be built with functional dependencies.
ToList should definitely be built-in, because there’s no other reason to deconstruct a dictionary. FromList could be added for efficient construction with the curly brackets.
Also “rather a lot” seems on par with the rest of the type literal modules, we’re talking 5-8.
There is no syntax for dictionaries in the language right now at all: containers has to Show its dictionaries as fromList [(.. , ..)]. My thought in using curly brackets as a “list” of fields is that it directly mirrors an already possible construct that is a list of fields, and it leaves future space for other kinds of dictionaries, e.g. one where keys are integers.
This is not a hill I care about and I’ll support any other working solution.
Which part of it is unsafe? It’s all type-level. Exposing unsafeIndex would be a maintainer’s choice, in their library where they implement the datatype. (and in my example it’s only used to skip an unnecessary Find)
Thank god, let’s please implement this and get the goodness of anon records into haskell. 
I think you’ll have to wait for the maintainer of the original Row Polymorphism proposal to finish his PhD (that is to say snooze til 2027 and hope whatever the chosen solution will be makes it into GHC before year 2030).
This entire topic sums up to pretty much a single Adam Gundry comment on that same proposal from six years ago. That proposal had far wider community coverage, so I feel confident in saying if enough people wanted a working thing, it would be a part of GHC years ago.