Naming function arguments in Dhall

This post showcases some neat Dhall language features for improving the readability of types that I think other languages should steal.

To motivate this post, consider the following Haskell type for Data.Text.replace:

replace :: Text -> Text -> Text -> Text

This function replaces all occurrences of a substring with another substring, but you wouldn’t be able to easily guess which argument is which from the type alone.

Fortunately, the function does have Haddock-level documentation in the form of comments for each function argument:

replace
    :: Text
    -- ^ @needle@ to search for.  If this string is empty, an
    -- error will occur.
    -> Text
    -- ^ @replacement@ to replace @needle@ with.
    -> Text
    -- ^ @haystack@ in which to search.
    -> Text

… but what if you could provide a hint to what each argument does within the type itself?

Naming function arguments using ∀ / forall

Well, in Dhall you can, and here is the equivalent Dhall type:

$ dhall repl
⊢ :type Text/replace

∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text

… or if you prefer ASCII syntax then that is the same as this type:

forall (needle : Text) ->
forall (replacement : Text) ->
forall (haystack : Text) ->
  Text

Here we’ve tagged each function argument with the argument’s name. In fact, you don’t need to do this explicitly. Dhall will automatically infer named function argument types when you create user-defined functions:

⊢ :type λ(name : Text) → "Hello, ${name}"

∀(name : Text) → Text

In many cases these names are “cosmetic”, meaning that they have no effect on type-checking. For example, as far as the type-checker is concerned the following function type:

∀(name : Text) → Text

… is the exact same as the following simpler function type (they are α-equivalent):

Text → Text

However, sometimes these names are not cosmetic! The simplest example is a polymorphic function (a.k.a. a “generic” function), like the following polymorphic identity function:

let identity
      : ∀(a : Type) → a → a
      = λ(a : Type) → λ(x : a) → x

in  identity

Here we’ve used the ∀ to name the first function argument a, which lets us reference that name downstream within the same type.

let identity
       -- We're naming our first function argument `a` …
       -- ↓
      : ∀(a : Type) → a → a
                   -- ↑   ↑
                   -- … so that we can reference the value of the first function
                   -- argument downstream within the same type
      = λ(a : Type) → λ(x : a) → x

in  identity

However, unlike other languages, Dhall also lets us name the second function argument using the exact same syntax, even though our second function argument is not a Type:

let identity
      : ∀(a : Type) → ∀(x : a) → a
      = λ(a : Type) → λ(x : a) → x

In fact, this is actually the type that the interpreter would have inferred if we had omitted the type annotation. The name of this second function argument is cosmetic, though.

Another example where the argument name is not cosmetic is the following hypothetical Dhall type for a safe division function that rejects 0 denominators at type-checking time:

divide
    : ∀(denominator : Natural) →
      ∀(proof : Natural/isZero denominator ≡ False) →
      ∀(numerator : Natural) →
        Natural

This division function takes three arguments instead of the usual two:

• The first argument is the denominator

  … as you may have guessed from the helpful type-level name

• The second function argument requires a proof that denominator is non-zero

  Side note: This proof obligation is satisfied by assert : False ≡ False so long as denominator is not 0

• The third argument is the numerator

By naming the first argument denominator, we can refer to the value of the first argument within the type of the second argument:

divide
    --  We're referring to the value of the first argument …
    --  ↓
    : ∀(denominator : Natural) →
    --                         … within the type of the second argument
    --                         ↓
      ∀(proof : Natural/isZero denominator ≡ False) →
    --  ↑
    --  These names are still cosmetic, though
    --  ↓
      ∀(numerator : Natural) →
        Natural

You might wonder why Dhall uses the ∀ / forall keyword for this purpose, since typically most languages only use forall to create polymorphic (a.k.a. “generic”) functions. This is because Dhall is implemented as a pure type system, meaning that Dhall uniformly handles term-level function arguments and type-level function arguments in the exact same way. They’re both special cases of Π types.

The following paper does a really good job explaining pure type systems and Π types:

• Henk: a typed intermediate language,

… and that’s actually where I stole this trick from.

Really the correct symbol to use is Π and not ∀, but there isn’t a great way to input Π as ASCII. The Henk paper suggests using |~| as the ASCII counterpart to Π, but that didn’t seem right to me. I went with ∀ / forall because there’s already prior art for using those for type arguments.

Anonymous record types

There is another approach to naming function arguments that doesn’t require a pure type system at all: anonymous record types.

For example, we could have changed the Text/replace function to have this type:

{ needle : Text, replacement : Text, haystack : Text } → Text

That’s pretty clear, too, and can be done in any language that supports anonymous record types, including Dhall, F#, PureScript, Elm, and OCaml.

Naming type parameters

You can also use the above two tricks to name type arguments for type constructors, too.

For example, we can define a Map type constructor to be a list of key-value pairs:

let Map =
      λ(key : Type) →
      λ(value : Type) →
        List { mapKey : key, mapValue : value }

… which we would use like this:

⊢ Map Text Natural

List { mapKey : Text, mapValue : Natural }

… and the inferred type names the arguments to our Map type constructor:

⊢ :type Map

∀(key : Type) → ∀(value : Type) → Type

We can also use anonymous records to name type arguments, too! For example, we could have instead defined Map as:

let Map =
      λ(args : { key : Type, value : Type }) →
        List { mapKey : args.key, mapValue : args.value }

… which we would use like this:

⊢ Map { key = Text, value = Natural }

List { mapKey : Text, mapValue : Natural }

… and this latter Map would have an inferred type of:

⊢ :type Map

∀(args : { key : Type, value : Type }) → Type

Pretty neat! Not many languages can pass type constructor arguments as named fields of a record.

Conclusion

Hopefully this gives language designers some ideas for how they can add language support for naming function arguments.

Unfortunately, my favorite language (Haskell) does not exactly support these features, so sometimes people work around this by using newtypes to name function arguments. I’ve never been of fan of this approach, especially if the newtype is not opaque and this post does a good job of explaining why:

• Names are not type safety

However, you can simulate this trick in Haskell using something like what the vulkan package does, which is to use DataKinds and TypeOperators to create a type-level operator that lets you associate arbitrary name data with types:

type (name :: k) ::: a = a

… which the package uses like this:

cmdDraw
    :: forall io . (MonadIO io)
    => -- | @commandBuffer@ is the command buffer into which the command is
       -- recorded.
       CommandBuffer
    -> -- | @vertexCount@ is the number of vertices to draw.
       ("vertexCount" ::: Word32)
    -> -- | @instanceCount@ is the number of instances to draw.
       ("instanceCount" ::: Word32)
    -> -- | @firstVertex@ is the index of the first vertex to draw.
       ("firstVertex" ::: Word32)
    -> -- | @firstInstance@ is the instance ID of the first instance to draw.
       ("firstInstance" ::: Word32)
    -> io ()

These names are ignored by the type-checker, just like the equivalent cosmetic names in Dhall.