Disclaimer
My knowledge on the topic is rather limited. I don’t know if this suggestion makes sense when it comes to type theory, and whether it is easy or even possible to implement. Also, maybe there is a better alternative. However, I would still like to share the idea. We discussed this briefly with @natefaubion and @jy14898 on slack.
Background
Purescript records have a lot of benefits.
However, one question that seems to repeatedly come up is whether one should use records with or without newtype wrappers. One typical answer seems to be that one should normally use records without wrappers and create wrappers when necessary (for example, when one needs to define a type class instance).
I would like to propose an idea that could potentially let us have one type that supports dot syntax, type class instances, and also improved type safety without the need for wrappers.
Named records
The idea is to allow defining named records, for example, PersonRecord or CompanyRecord, that behave just like Record.
This gives us a combination of nominal and structural typing: PersonRecord (name :: String | others) unifies with PersonRecord (name :: String), but not with CompanyRecord (name :: String).
Let’s consider an example.
Currently we can write:
person :: Record (name :: String)
person = { name : "John" }
I would like to be able to write:
person :: PersonRecord (name :: String)
person = { name : "John" }
The code above assumes that there is a way to define named records like PersonRecord, and also, as @natefaubion suggested, that we have something like OverloadedRecords, so that we can use normal record construction syntax to construct a named record.
Benefits:
- We can allow defining instances for records, as
PersonRecord (name :: String)andCompanyRecord (name :: String)are different types. - There is no need for newtypes and wrapping / unwrapping.
- Normal dot notation can be used for accessing nested records.
- Improved type safety when necessary (for example, we cannot use
CompanyRecord (name :: String)wherePersonRecord (name :: String)is expected. - Named records can be extended in the same way as anonymous records, so, if a function expects
PersonRecord (name :: String | others), it can takePersonRecord (name :: String).
The important thing here is that we get one type that supports all of the functionality, without the need for wrappers. And of course, we could still use anonymous records if we prefer that.
Comparison to other languages
I don’t know any languages that support this kind of records.
Haskell:
Normal records in Haskell are nominally typed:
data PersonRecord = PersonRecord
{
name :: String,
age :: Int
}
There are several libraries that support structurally typed records, but I couldn’t find any libraries that support named structurally typed records.
Here is an example with row-types:
class Greet a where
greet :: a -> String
type Person = Rec ("name" .== String)
instance (person ~ Person) => Greet person where
greet person = "Hi, " ++ person .! #name
person :: Person
person = #name .== "John"
This is very similar to Purescript. In addition, we can make Person an instance of Greet type class, but I don’t think that such usage is ideal, because:
- If we define
type Company = Rec ("name" .== String), it is now automatically an instance of theGreettype class. - We can quickly run into the problem with overlapping instances.
Idris
Normal records in Idris are also nominally typed:
record Person where
constructor MkPerson
name : String
age : Int
Elm
Elm records seem to be very similar to Purescript: anonymous and structurally typed. But as long as Elm does not have type classes, there is also less need for newtype wrappers.
type alias Person =
{
name : String,
age : Int
}
