In this blog post I'm going to take a break from Haskell and spread the good word of Dhall. The good news is that it won't be a break from functional programming. We still have all the good stuff in Dhall like: lambdas, products, sums and types! We'll take a look through some of the basics of Dhall and work our way up to defining Either. This will be a two part series and in the second part we'll take the definition of Either and work with it to see some more functional concepts in Dhall.

Introduction to Dhall

One can almost view Dhall as JSON with functions and types, but really it's so much better. There is an excellent tutorial that lives in the library. It goes through the simple usage of Dhall and how you can utilise Dhall files in your Haskell code. I will try summarise here the main points to give you a taste. To really get a feel we can grab the Dhall executable. An easy way to get it is if you have stack, we can run stack install dhall --resolver=lts-12.0; grabbing the dhall package (version 1.16.1) at LTS-12.0.

The native types to Dhall can be enumerated:

• Bool
• Natural
• Integer
• Double
• Text
• List
• Optional
• Unit

Basic Types

So let's take a look at them via the dhall command. Running the following we can see what we can do with Dhall.

Booleans

$ dhall <<< "True && False"
Bool

False

$ dhall <<< "True || False"
Bool

True

Naturals

$ dhall <<< "1"
Natural

1

$ dhall <<< "1 + 1"
Natural

2

Integers and Doubles

$ dhall <<< "-1"
Integer

-1

$ dhall <<< "+1"
Integer

+1

$ dhall <<< "+0"
Integer

+0

$ dhall <<< "-0"
Integer

+0

$ dhall <<< "3.14"
Double

3.14

Note:

There are no built-in operations on Integers or Doubles. For all practical purposes they are opaque values within the Dhall language

Text

$ dhall <<< "\"Fintan <3 Dhall\""
Text

"Fintan <3 Dhall"

$ dhall <<< "\"Hello\" ++ \" World\""
Text

"Hello World"

Lists

$ dhall <<< "[1, 2, 3] # [4, 5, 6]"
List Natural

[ 1, 2, 3, 4, 5, 6 ]

$ dhall <<< "List/fold Bool [True, False, True] Bool (λ(x : Bool) → λ(y : Bool) → x && y) True"
Bool

False

$ dhall <<< "List/length Natural [1, 2, 3]"
Natural

3

Optionals

$ dhall <<< "Optional/fold Text ([\"ABC\"] : Optional Text) Text (λ(t : Text) → t) \"\""
Text

"ABC"

$ dhall <<< "Optional/fold Text ([] : Optional Text) Text (λ(t : Text) → t) \"\""
Text

""

Unit

$ dhall <<< "{=}"
{}

{=}

The Unit type looks like an empty record, which segues us onto our next topic nicely!

Records

On top of all these types we can make records that have named fields. For example let's define a user with a name, age, and email.

Defining Records Types and Values

$ dhall <<< "{ name : Text, age : Natural, email : Text }"
Type

{ name : Text, age : Natural, email : Text }

Notice that we didn't have to bind the record type to a name such as User. Due to the nature of working with directories and files, our file path will be our name.

For these small examples, we will use let and in to bind the type and assert that the value we are constructing is the correct type.

$ dhall <<< "let User = { name : Text, age : Natural, email : Text } in { name = \"Fintan\", age = 25, email = \"fintan dot halpenny at gmail dot com\" } : User"
{ name : Text, age : Natural, email : Text }

{ name = "Fintan", age = 25, email = "fintan dot halpenny at gmail dot com" }

Just to prove to ourselves that Dhall is type checking correctly, let's leave off the email value and see what happens.

$ dhall <<< "let User = { name : Text, age : Natural, email : Text } in { name = \"Fintan\", age = 25 } : User"

Use "dhall --explain" for detailed errors

Error: Expression doesn't match annotation

{ - email : …
, …
}


{ name = "Fintan", age = 25 } : User


(stdin):1:60

Accessing Record Values

We can access one or more record fields use the . accessor.

$ dhall <<< "{ name = \"Fintan\", age = 25 }.age"
Natural

25

$ dhall <<< "{ name = \"Fintan\", age = 25 }.{ age, name }"
{ age : Natural, name : Text }

{ age = 25, name = "Fintan" }

Unions

As well as records we can define union types. For example we can enumerate the days of the week.

Defining Union Types and Construcing Values

$ dhall <<< "
< Monday : {}
| Tuesday : {}
| Wednesday : {}
| Thursday : {}
| Friday : {}
>
"
Type

< Monday : {} | Tuesday : {} | Wednesday : {} | Thursday : {} | Friday : {} >

And construct values of union types using the constructors keyword:

$ dhall <<< "
    let Days =
          < Monday :
              {}
          | Tuesday :
              {}
          | Wednesday :
              {}
          | Thurday :
              {}
          | Friday :
              {}
          >

in  let DaysConstructors = constructors Days

in  DaysConstructors.Monday {=}
"
< Monday : {} | Tuesday : {} | Wednesday : {} | Thurday : {} | Friday : {} >

< Monday = {=} | Tuesday : {} | Wednesday : {} | Thurday : {} | Friday : {} >

Consuming Unions

When we want to collapse union data we use the merge keyword:

$ dhall <<< "
    let Days =
          < Monday :
              {}
          | Tuesday :
              {}
          | Wednesday :
              {}
          | Thurday :
              {}
          | Friday :
              {}
          >

in  let DaysConstructors = constructors Days

in  let doesGarfieldHate =
            λ(day : Days)
          → merge
            { Monday =
                λ(_ : {}) → True
            , Tuesday =
                λ(_ : {}) → False
            , Wednesday =
                λ(_ : {}) → False
            , Thurday =
                λ(_ : {}) → False
            , Friday =
                λ(_ : {}) → False
            }
            day

in        if doesGarfieldHate (DaysConstructors.Monday {=})

    then  \"Garfield hates Mondays...\"

    else  \"Garfield is happy today!\"

Text

"Garfield hates Mondays..."

Either

Ok, so that was a whirlwind tour of Dhall and I'm sure we missed some things along the way but it should be enough to get us writing a self defined Either data type. If we were to go off of the knowledge we covered above, our first attempt at Either would be:

< Left : a | Right : b >

That is to say, we have a Left union entry of type a, and a Right union entry of type b. The question is, where do a and b come from? Well, this is where type functions come in. In Dhall, types are passed along to say what types of things we are working with. Let's see this in action with the full definition of Either:

$ dhall <<< "\(a : Type) -> \(b : Type) -> < Left : a | Right : b >"
∀(a : Type) → ∀(b : Type) → Type

λ(a : Type) → λ(b : Type) → < Left : a | Right : b >

Notice how the output uses ∀, λ, and →. We can format our files to use these symbols, and I strongly recommend you do so. If we put the above definition in a file Either/type and run dhall format --inplace ./Either/type, it will convert all the symbols for us. So pretty 😍.

Let's see our Either in action! Assuming you're following along and have defined the above in Either/type we can try the following:

$ dhall <<< "let E = constructors (./Either/Type Text Natural) in E.Right 2"
< Left : Text | Right : Natural >

< Right = 2 | Left : Text >

dhall <<< "let E = constructors (./Either/Type Text Natural) in E.Left \"Hello\""
< Left : Text | Right : Natural >

< Left = "Hello" | Right : Natural >

    let Either = ./Either/Type Text Natural

in  let E = constructors Either

in  let f =
            λ(e : Either)
          → merge { Right = λ(i : Natural) → i + 2, Left = λ(t : Text) → 42 } e

in  f (E.Right 42)

Just the Starters

We have taken a whirlwind tour of Dhall and filled ourselves with some starters. Going through the types that Dhall supports, defining and creating records and unions, and defining our good ol' friend Either. I'm not sure about you but I'm still hungry, so tune in next time for exploring some more Dhall visiting our familiar friend Functor, and its lesser known yokefellow Yoneda.