Optionally present fields: is it possible?

[dhall-lang]

Optionally present fields: is it possible?

[Gabriella439]

@geigerzaehler: I agree that there probably should be some language feature that provides type inference in the non-empty case

Here's one idea: add language support for Some and None keywords. Some performs type inference so that you can write Some "value", whereas None still requires a type argument (i.e. None Text). Would that work for you?

[Gabriella439]

@f-f: Mainly separation of concerns. dhall format should in theory never change the syntax tree

[Gabriella439]

Alright, then I'll try to open a proposal this weekend (ETA: Sunday)

[f-f]

@Gabriel439 I have the feeling there might be some value in having a different syntax for Optional and List, in that we wouldn't have to worry about the compulsory type signature on Optional anymore.

The Some and None in the Prelude go in this direction, but as you said it would be even better to add language support for inferring the type in Some.

What I'm trying to say here is that I think it would be beneficial to replace the Optional syntax from [] to Some/None.
It would be a pretty breaking change, but I'd compare it to the Natural-Integer change which was very good. In this case it would be much easier, since for some time we could support both to have time to migrate.

[Gabriella439]

@f-f: We can do this in two steps: first introduce Some/None and then in a separate release remove support for list-like syntax? That way people have a smooth migration path. Also, that would give us a chance to add dhall lint support for migrating people onto the new syntax.

[AlexeyRaga]

I have found a way to make it a bit less noisy.

With this expression

let nothing = \(a: Type) -> ([] : Optional a)
in  nothing

I can now write

{ cpus = ./Nothing Double
, memoryMb = ./Nothing Double
, diskMb = ./Nothing Double
, numPorts = ./Nothing Integer
} : ./Resources

But is there a way to avoid specifying a type parameter every time so I could just write ./Nothing?

[Gabriella439]

Usually the way I do this is to provide the user with a default record which they can override or extend using ⫽, like this:

    let defaults =
          { cpus =
              [] : Optional Double
          , memoryMb =
              [] : Optional Double
          , diskMb =
              [] : Optional Double
          , numPorts =
              [] : Optional Integer
          }

in  defaults ⫽ { cpus = [ 1 ] : Optional Integer }

Judging by #114 it looks like that is already your current approach so I'll address how to deal with overriding recursive types separately in that ticket. I need some more time to think about that one.

Also, dhall-json could definitely be extended to provide a flag to omit null fields of a record. Could you open a ticket against that repository?

[gromakovsky]

I think it would be more convenient to write defaults // { cpus = 1 } so that in the resulting type cpus would still be Optional Double (i. e. the same type as in defaults).
Does it make sense? Is it possible at all?
If it makes sense and is possible, maybe it's worth adding a new operator with this behavior?

[Gabriella439]

@gromakovsky: I would like to keep it the way it is. The issues with your proposal are that:

• The // operator is no longer associative (i.e. (x // y) // z is not the same as x // (y // z))

• The field can no longer be set to the empty value through the use of the // operator (i.e. there is no way to set cpus to the empty Optional value)

[geigerzaehler]

I feel @AlexeyRaga’s pain. I think having a way to write a Some value without providing the types would be nice. It would for instance free you from importing complex type. Maybe the following syntax could work: (! "value") instead of [ "value" ] : Optional Text and Some Text "value". (Of course one would need to provide the type for Nothing`

A more advanced step, but a huge help, could be a builtin function liftSome that takes a record and returns a record with the same labels but every value is lifted with Some. E.g.

liftSome { foo = "foo", bar = 1 } : { foo : Text, bar : Natural }

evaluates to

{ foo = [ "foo" ] : Optional Text, bar = [ 1 ] : Optional Text }

[geigerzaehler]

Here's one idea: add language support for Some and None keywords.

That would be great!

[quasicomputational]

Not having weird corner cases like dhall-lang/dhall-haskell#414 is also a nice advantage in my book, so +1 for making a change.

[Gabriella439]

@quasicomputational: Note that changing the syntax for Optionals would not fix the issue described in dhall-lang/dhall-haskell#414. That issue has to do with the fact that the List token in the type annotation is part of the grammar and fixing that requires a change to the semantics.

That said, I'm still liking the idea of changing the syntax for Optional anyway

[f-f]

@Gabriel439 +1 for doing the transition in two steps and for facilitating the transition with dhall lint (why not also dhall-format?)

[Gabriella439]

Just an update that there is a delay on this while I finish the work on standardizing serialization. Once that is done then I will proceed with standardizing this

[Gabriella439]

Sorry for the delay on this, but I have time to standardize this now. There are two ideas that I would like to suggest in the meantime while I am implementing and standardizing this.

The first suggestion is possibly using Present/Absent instead of Some/None. They are a little longer but I think they are more clear to people not steeped in programming naming conventions and they read more closely to english (i.e. "Present 1" reads like "a present 1" and "Absent Integer" reads like "an absent integer") and the words themselves have a nice duality to them. The disadvantage to Present/Absent is that there is no prior art for them in other programming languages.

The second suggestion is possibly lowercasing them (i.e. some and none). The reason why is that so far Dhall used uppercase identifiers for reserved built-ins and lowercase identifiers for keywords. However, Some is technically not a built-in because it is not typeable in isolation (although None is fine). This leads me to wonder if we should treat Some as keyword instead of a built-in and lowercase it (also lowercasing None just for consistency with Some).

[Gabriella439]

Another thing to mention: the simplest way to do this is to make Some and None the normal form and have [] : Optional T / [ t ] : Optional T normalize to None T and Some t, respectively.

The reason why is that it's simple to rewrite [ t ] : Optional T to Some t since it's just discarding the type, but it's not simple to go the other direction because you'd have to infer the type as part of the normalization phase.

This also slightly simplifies migration because any expression in normal form is already migrated (although expressions not in normal form still need to be explicitly migrated via dhall lint)

[Gabriella439]

Alright, I have a pull request up based on the Some/None names: #227

We can continue the discussion there

[Gabriella439]

Alright, I will go ahead and close this since I think None/Some simplify the original example. The new default record would be:

{ cpus     = None Double
, memoryMb = None Double
, numPorts = None Integer
}

... and you can override it like this:

./defaults ⫽ { cpus = Some 1 }