Exhaustive record field matching

#1

I’m wondering whether we can have an exhaustiveness checks for records, similar to merge checking that every case is handled.

e.g. if I have

let Foo = { bar: Text, baz: Text }

let fooToText = \(foo: Foo) -> "${foo.bar} ${foo.baz} :)"

in fooToText { bar = "4", baz: "abc" }

and I add a field to Foo, say quux : Natural, I want to be reminded by dhall that I need to adjust the fooToText function because I’m missing a field.

In Rust I can use the normal pattern matching facility for that:

struct Foo {
  bar: String,
  baz: String,
}

…
let f = Foo { bar = "abc".to_string(), baz = "bcd".to_string() };
match f {
  { bar, baz } => println!("{} {} :)", bar, baz)
}

which will lead to a compile error if not all fields are matched (and to warnings when a matched field is not used).

1 Like
#2

@Profpatsch: You probably want to standardize this feature:

… with one modification: require a … when not unpacking all of the fields, so the omission of the … would perform the check that you are requesting.