Fintan Halpenny
10 Sep 2018
β’
4 min read
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.
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
](https://docs.haskellstack.org/en/stable/README# how-to-install), 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:
So let's take a look at them via the dhall
command. Running the following we can see what we
can do with Dhall.
$ dhall <<< "True && False"
Bool
False
$ dhall <<< "True || False"
Bool
True
$ dhall <<< "1"
Natural
1
$ dhall <<< "1 + 1"
Natural
2
$ 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
Integer
s orDouble
s. For all practical purposes they are opaque values within the Dhall language
$ dhall <<< "\"Fintan <3 Dhall\""
Text
"Fintan <3 Dhall"
$ dhall <<< "\"Hello\" ++ \" World\""
Text
"Hello World"
$ 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
$ dhall <<< "Optional/fold Text ([\"ABC\"] : Optional Text) Text (Ξ»(t : Text) β t) \"\""
Text
"ABC"
$ dhall <<< "Optional/fold Text ([] : Optional Text) Text (Ξ»(t : Text) β t) \"\""
Text
""
$ dhall <<< "{=}"
{}
{=}
The Unit type looks like an empty record, which segues us onto our next topic nicely!
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.
$ 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
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" }
As well as records we can define union types. For example we can enumerate the days of the week.
$ 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 : {} >
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..."
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)
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.
Fintan Halpenny
Passionate about Haskell as it is the perfect language to help me be productive but also constantly drives me to learn new things. The day I stop learning is the day I'm no longer on this Earth. I also have an interest in Dhall and helped start a functional library for the language (despite Dhall's original intention of being a config language) https://github.com/FormationAI/dhall-bhat
See other articles by Fintan
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!