Record Subtyping / Union Types? about dhall-haskell

[Gabriella439]

I probably will not add support for record subtyping (or subtyping in general), partly because Dhall is an experiment in designing a language without any subtyping at all. For example, this is the same reason that Dhall requires explicit type abstraction and type application.

However, I would be open to adding language features that make it easier to explicitly convert between records where a subtyping relationship could exist. For example, Nix has this sort of feature with the inherit keyword that lets you easily project out a subset of fields and Dhall could add something similar.

I also like the idea of a type-level record union operator, although I would like to reserve the symbol \/ for use with sum types.

[markus1189]

Okay I wholeheartedly support the idea of avoiding all forms of subtyping as an experiment :)

If I understand inherit correctly, that does not solve the use case of having a larger config file where additional fields are ignored, right? The use case I have in mind is something like:

$ cat > config
{ 
  one = 1,
  two = 2,
  three = 3
}

Now imagine this config file as being shared by two libraries that use dhall to configure themself.

However, both of them need only a subset of the actual config:

$ cat > schema1
{ one : Integer, two: Integer }
$ cat schema2
{ two : Integer, three : Integer }

It would be cool, if there was something that allows you to have config as-is, where it represents a set of all required attributes, without forcing you to split them.

I think I'll have to think about something that makes this possible without subtyping.

[markus1189]

Anyhow, I'll think a bit about this, I close this for now, cheers!

[Gabriella439]

You should check out "row polymorphism" which is a solution that works very well for modeling extensible records in languages with type inference. In languages without type inference (like Dhall) it is a little trickier but still possible and I'll sketch one approach of how it might be done in Dhall.

The basic idea is that a function that only depends on a subset of fields would like something like this:

-- example
λ(fields : Fields) → λ(record : { foo : Natural, bar : Natural | fields }) → record.foo + record.bar

... where Fields would be a new kind (i.e. Fields : Kind) and fields would be a set of field types. For example, if you wanted to apply this function to a record of type { foo : Natural, bar : Natural, baz : Bool } then you would do something like:

./example {{ baz : Bool }} { foo = +2, bar = +2, baz = True }

... where {{ baz : Bool }} is a hypothetical new syntax for specifying additional fields.

You might wonder why we don't use a hypothetical type-level union operator like the one your proposed to accomplish the same thing. The issue is that you get something like this:

-- Here I'm overloading `∧` as type-level union, too
λ(fields : Type) → λ(record : { foo : Natural, bar : Natural } ∧ fields) → record.foo + record.bar

... which should not type-check because the compiler can't verify that the fields argument will be the type of a record.

So I think it is possible to implement something like this in Dhall if you don't mind having to explicitly specify unused fields. However, I'd probably prefer providing a way to project out desired fields since then you only have to specify the fields you want to keep instead of the fields you want to ignore.