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

Learn
#8

I see how you can map current record notation to it.
How does it look with deeply nested fields, plain updates, deeply nested updates and multiple updates?

type This =
      '{ "foo" := Char
       , "bar" := Bool
       , "baz" := Float
       }

type That =
      '{ "foo" := Char
       , "bar" := Bool
       , "baz" := Float
       }

type Thing =
      '{ "foo" := Char
       , "bar" := Bool
       }

-- this gives ambiguous errors?
f = new
    . cons @"baz" (5 :: Float)
    . cons @"bar" True
    . cons @"foo" 'a'
    $ nil

-- this gives ambiguous errors?
result r = index @"bar" r
#9

For the code snippet, they’re all just types, so you’d get

f :: Rec '{ "bar" := Bool, "baz" := Float, "foo" := Char }

result :: (Find "bar" xs v, Index "bar" xs n) => Rec xs -> v

Single-level updates don’t make sense in the immutable version, you’d need to convert it to a mutable record, apply the changes and convert back. Or, if you’re writing imperative code you can just keep mutating the mutable version directly.

Nesting, as said, can be a completely separate thing, because updating "foo.bar.baz" is the same as accessing "foo", then accessing "baz", then updating "bar". This will be different for every single type, e.g. for FFI nested anything merely requires adding offsets together.

#10

You are right, thank you.

I was thinking of composing index, cons and new to return a new immutable record like how it’s done with current records.
Basically reimplementing

rec.foo.bar
rec { foo = a, bar = b }
rec { foo.bar.baz = a, bar = b, foo.quux = c }
rec { foo = a, ..}

in this notation to see how ergonomic it is and the errors it gives in different scenarios.

1 Like
#11

; > laughs maniacally <

2004 HList. (See the pdf from that link.) Originally used FunDeps, now upgraded to use TFs. So not just a proposal but an implementation. I don’t find enough in your sketch to tell whether it’s significantly different to HList.

Yeah. Perhaps there’s a reason those “more knowledgable” maybe wouldn’t agree that “this doesn’t need any complex proposals”.

#12

One problem I don’t recalling seeing mentioned very often is that if all the fields of a data type are exposed via names, the type isn’t abstract - all those names can then be used to make public duplicates of values with the original data type.

Others have made similar laments e.g:

…which I have commented on here:

…with this being my final post there:

Type abstraction in face of field labels
#13

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.

#14

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.

2 Likes
#15

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?

#16

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.

#17

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.

#18

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.

1 Like
#19

I take this opportunity to shill inline-c, for lurkers.
And a recent example.
Love this package.

1 Like
#20

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.

1 Like
#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.