Representing implicit parameters about dhall-haskell

[Gabriella439]

I recently added support for this by introducing a new // operator in dhall-1.3.0 which does a right-biased and non-recursive record merge. You can use this operator to implement option defaulting by first defining a record containing default options like this:

$ cat ./defaults
{ foo = 1, bar = "ABC", baz = True }

... and then you can override those defaults using //, like this:

$ dhall <<< './defaults // { foo = 2 }'
{ bar : Text, baz : Bool, foo : Integer }

{ bar = "ABC", baz = True, foo = 2 }

[bosu]

Yes, it looks like // operator solves the problem for the flat records.

What do you think can be done for the nested records, e.g. div tag can have other tags as children?

[Gabriella439]

For nested records you would have to do something like this:

    λ(defaults : { foo : { bar : Integer }, baz : Bool })
→   defaults // { foo = defaults.foo // { bar = 1 } }

[bosu]

I am afraid this defaults solution looks a bit verbose :(

Do you think, having some implicit field construct in the language is overkill?

Anyhow, thanks for your answers! Feel free to close the issue if you think that nothing can be done.

[Gabriella439]

The main reason why Dhall does not have implicit parameters is because Dhall has a firm "no subtyping" rule to keep the language easy to teach. Implicit parameters are one form of subtyping, because multiple record types would be able to type check as valid arguments to the same function. For example:

-- This would be valid:
(λ(r : { foo = 1 }) → r) {=}

-- ... and so would this:
(λ(r : { foo = 1 }) → r) { foo = 2 }

In order for the above type-application to work we'd need to:

• add subtyping rules so that {} ⊂ { foo = 1 }, { foo : Integer } ⊂ { foo = 1 }
• teach new users how to reason about these new subtyping rules, which is difficult (I'm not even sure I understand what they should be)

... and now a subexpression {=} would no longer have a unique type or even a principal type

Reducing verbosity is very intentionally not one of the design priorities of the language. You can find the list of design priorities here:

• https://github.com/Gabriel439/Haskell-Dhall-Library#design-philosophy

Also, in this specific case it conflicts with two other priorities which are:

• Beginner friendliness - Adding this makes it more difficult to teach beginners how to reason about Dhall's type-checking semantics so that they can understand type errors
• Consistency - Now there would be two separate ways of doing the same thing (providing defaults). One being the (//) operator and the other being default fields

[bosu]

This makes perfect sense. Thanks!