Couldn't records be solved entirely at the type level?

Learn
#21

I have to say that by now I’ve no idea why “records” is in the title of this topic:

  • Mutability is not specific to records: an Int or Char variable is just as immutable.
  • Deep nesting is not specific to records: Either (Maybe String) (Maybe (Either Int Char))
  • ‘Updating’ deeply inside that nested structure is not different to updating inside nested records. (Not that ‘updating’ in the sense in procedural languages reassignment is really a helpful way to think about it. It’s returning a entirely new value for the whole structure.)
  • Low-level programming is not specific to records: Int or Char again.
  • C structs have what to do with your proposal?

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?

#22

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).

#23

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.

#24

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.

#25

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.

#26 
-- 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.

#27

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.

#28

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.

1 Like
#29

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.

#30

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)

1 Like
#31

Thank god, let’s please implement this and get the goodness of anon records into haskell. :slight_smile:

#32

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.

1 Like