Help with type error using operator //

#1

Hi,
In my organization I’m prototyping Dhall for our configurations. I am almost done converting our old yaml spec to Dhall, but I have one more thing to fix. I have been struggling with a type error that I don’t understand. I’ve minimized it as far as I could from an example using OpenShift shown at the end. It may be about the // operator, but I don’t know. There seems to be something about the type system that I don’t understand.

The following code type-checks and works:

let Config : Type =
      { name : Text
      , metadata : { labels : Text }
      }

let makeConfig
    : Text -> Text -> Text -> Config =
    \(app : Text) -> \(name : Text) -> \(host : Text) ->
    {
    , name
    , metadata.labels = app
    }

let replaceLabels
    : Text -> Config -> Config =
    \(app : Text) -> \(r : Config) ->
    r // { metadata.labels = app }

let generate
    : Config =
    let r = makeConfig "testapp" "testname" "testhost"
    in replaceLabels "newapp" r

in generate

But adding an optional dummy field to Config breaks it.

let Config : Type =
      { name : Text
      , metadata : { dummy : Optional Text, labels : Text }
      }

let makeConfig
    : Text -> Text -> Text -> Config =
    \(app : Text) -> \(name : Text) -> \(host : Text) ->
    {
    , name
    , metadata = {
      , labels = app
      , dummy = None Text
      }
    }

let replaceLabels
    : Text -> Config -> Config =
    \(app : Text) -> \(r : Config) ->
    r // { metadata.labels = app }

let generate
    : Config =
    let r = makeConfig "testapp" "testname" "testhost"
    in replaceLabels "newapp" r

in generate

Error:

You or the interpreter annotated this expression:

↳ λ(app : Text) → λ(r : Config) → r ⫽ { metadata.labels = app }

... with this type or kind:

↳ Text →
  { metadata : { dummy : Optional Text, labels : Text }, name : Text } →
    { metadata : { dummy : Optional Text, labels : Text }, name : Text }

... but the inferred type or kind of the expression is actually:

↳ ∀(app : Text) →
  ∀(r : { metadata : { dummy : Optional Text, labels : Text }, name : Text }) →
    { metadata : { labels : Text }, name : Text }

A small initial example using OpenShift is this one, but I am not sure I have minimized it correctly:

let OpenShift =
      https://raw.githubusercontent.com/TristanCacqueray/dhall-openshift/master/package.dhall
      sha256:a6883f73597b7dfbded7638222562c2fb0b96d30089fa8e32fa4ea43a487b32e

let makeConfig
    : Text -> Text -> Text -> OpenShift.Route.Type =
    \(app : Text) -> \(name : Text) -> \(host : Text) ->
    OpenShift.Route::{
    , metadata = OpenShift.ObjectMeta::{
      , name = Some name
      , labels = Some (toMap { app = app })
      }
    , spec = OpenShift.RouteSpec::{
      , host = host
      , to = OpenShift.RouteTargetReference::{
        , kind = "Service"
        , name = name
        , weight = 100
        }
      }
    }

let replaceLabels
    : Text -> OpenShift.Route.Type -> OpenShift.Route.Type =
    \(app : Text) -> \(r : OpenShift.Route.Type) ->
    r // { metadata.labels = Some (toMap { app = app }) }

let generate
    : OpenShift.Route.Type =
    let r = makeConfig "testapp" "testname" "testhost"
    in replaceLabels "newapp" r

in generate

With the type error:

You or the interpreter annotated this expression:

↳ λ(app : Text) →
  λ(r : OpenShift.Route.Type) →
    r ⫽ { metadata.labels = Some (toMap { app }) }

... with this type or kind:

↳ Text →
  { apiVersion : Text
  , kind : Text
  , metadata :
      { annotations : Optional (List { mapKey : Text, mapValue : Text })
      ...
    }

... but the inferred type or kind of the expression is actually:

↳ ∀(app : Text) →
  ∀ ( r
    : { apiVersion : Text
      , kind : Text
      , metadata :
          { annotations : Optional (List { mapKey : Text, mapValue : Text })
          ...
    }

Can someone explain my type errors?

#2

I think you want

r with metadata.labels = app

not

r // {metadata.labels = app}

if I understand correctly.

e.g. your minimal example would be:

let OpenShift =
      https://raw.githubusercontent.com/TristanCacqueray/dhall-openshift/master/package.dhall sha256:a6883f73597b7dfbded7638222562c2fb0b96d30089fa8e32fa4ea43a487b32e

let makeConfig
    : Text -> Text -> Text -> OpenShift.Route.Type
    = \(app : Text) ->
      \(name : Text) ->
      \(host : Text) ->
        OpenShift.Route::{
        , metadata = OpenShift.ObjectMeta::{
          , name = Some name
          , labels = Some (toMap { app })
          }
        , spec = OpenShift.RouteSpec::{
          , host
          , to = OpenShift.RouteTargetReference::{
            , kind = "Service"
            , name
            , weight = 100
            }
          }
        }

let replaceLabels
    : Text -> OpenShift.Route.Type -> OpenShift.Route.Type
    = \(app : Text) ->
      \(r : OpenShift.Route.Type) ->
        r
        with metadata.labels = Some (toMap { app })

let generate
    : OpenShift.Route.Type
    = let r = makeConfig "testapp" "testname" "testhost"

      in  replaceLabels "newapp" r

in  generate
1 Like
#3

Thanks! Using with worked, but I don’t understand the difference. Isn’t both the with-expression and the //-expression creating a record? Then why does the type error say that replaceLabels is of this type?

∀(app : Text) → ∀ ( r : record)

There is something about the forall part that I don’t get. I understand it in logics but I don’t see the difference between:

Text →
and
∀(app : Text) →

Aren’t those types the same?

#4

They work differently. with is essentially a record update that “descends” into the structure to update a field. // overrides a top level field, so you can’t use // to update a nested field.

This example might make things more clear:

{ a = { b = 1, c = 2 } } // { a.b = 2 }

{ a.b = 2 }

vs

{ a = { b = 1, c = 2 } } with a.b = 2

{ a = { b = 2, c = 2 } }

r // { a.b = 2 } means replace whatever is in the a field of r with the record { b = 2 }. r with a.b = 2 means update the b field of the record stored in the a field to the value of 2.

If you look at the type error in your dummy example:

You or the interpreter annotated this expression:

↳ λ(app : Text) → λ(r : Config) → r ⫽ { metadata.labels = app }

... with this type or kind:

↳ Text →
  { metadata : { dummy : Optional Text, labels : Text }, name : Text } →
    { metadata : { dummy : Optional Text, labels : Text }, name : Text }

... but the inferred type or kind of the expression is actually:

↳ ∀(app : Text) →
  ∀(r : { metadata : { dummy : Optional Text, labels : Text }, name : Text }) →
    { metadata : { labels : Text }, name : Text }

and pull out what differs between the two, you can see that the final value of the first is
{ metadata : { dummy : Optional Text, labels : Text }, name : Text } while the second is { metadata : { labels : Text }, name : Text }. You’ll notice that the dummy field is missing in the second, because the dummyfield here is like the c field in my example; it’s getting “erased” by the usage of // because // overrides the entire value of the metadata field, rather than doing a nested update.

2 Likes
#5

Thanks for explaining. Now I understand the records part of the language tour when I read it, which I didn’t fully understand before.

+1 for the Dhall community, it has been very friendly and helpful for a Dhall-noob like me.

3 Likes