Type on index & examples from assertions

Introduction

Hi there! Today I'm going to tell you some progress made in the project so far, specifically the following features:

Type of files on each index
Examples from assertions

TL-DR

If you just want to see the progress, check out here

https://hydra.dhall-lang.org/build/64022/download/1/docs/

Let's get started!

Type of a dhall file

Usually in typed languages like Dhall or Haskell, the type of any value is more useful than its name. You can get an insight into what a function does with just its type.

In the case of Haskell, this fact is exploited a lot. There is a website similar to "google" that let you search functions that match a type that you defined: http://hoogle.haskell.org/

In another project (firelink) that I was developing, there was a circumstance where I wanted to get the Just values from a list of Maybes, something like this:

f :: [Maybe a] -> [a]

I "hoogled" the type and it showed me catMaybes, which does exactly what I wanted to. Without looking up for the name, just the type.

On Dhall, we have a similar urge: types are more meaningful than the name. So a cool feature that I add was showing the type of the expression on the index page.

Type-checking a dhall expression is something that involves several steps. This can get cumbersome in this context and fact, we (my mentors and I) didn't want to do so (the whole algorithm is described here). The way we extract the type from a dhall file is by analyzing the source code.

The only kind of expressions that this feature supports are let-bindings, which in the internal AST representation are constructed using the following constructor:

-- Let (Binding _ x _  Nothing  _ r) e ~ let x     = r in e
-- Let (Binding _ x _ (Just t ) _ r) e ~ let x : t = r in e
Let (Binding s a) (Expr s a)

Dhall also supports multiple-let bindings, to write code like this:

let a = 1
let b = 2
in a + b

So what we do is check if the last expression in the binding is a variable name, and traverse backward the list of bindings to get the desired one and finally its associated type (which may be absent).

There is a slight modification to support referencing variables with their indexes, for instance:

let x : Bool = True
let x : Natural = 1
in x

... will return Natural as its type because it is the closes lexical binding, but if we change the last line to the following:

in x@1

it will return Bool. The final code for that was the following:

-- The `V` constructor is used to handle name references on
-- Dhall expressions, whereas
extractTypeIfInSource :: Expr Void Import -> Maybe (Expr Void Import)
extractTypeIfInSource expr = do
    V name index <- maybeNameInLet expr
    (Binding _ _ _ (Just (_, exprType)) _ _) <-
        getLetBindingWithIndex index $ getLetBindingsWithName name
    return exprType
    where
    -- | For an expression of the form @let x0 = y0 let x1 = y1 ... in e@
    --   where @e@ is a variable, maybeNameInLet returns the variable name.
    maybeNameInLet :: Expr Void Import -> Maybe Var
    maybeNameInLet (Var v@(V _ _)) = Just v
    maybeNameInLet (Let _ e) = maybeNameInLet e
    maybeNameInLet _ = Nothing

    getLetBindingsWithName :: Text -> [Binding Void Import]
    getLetBindingsWithName name = filter bindName $ reverse $ bindings expr
        where
        bindName (Binding _ x _ _ _ _) = x == name


    getLetBindingWithIndex :: Int -> [Binding Void Import] -> Maybe (Binding Void Import)
    getLetBindingWithIndex i bs =
        case drop i bs of
            [] -> Nothing
            binding : _ -> Just binding

When I get this right I was kind of excited because it was the first time in my life where I used Maybe as a Monad. The code works (thanks tests!) and takes into account the cases with variable indexing.

Here you can see a preview of how it looks like:

Cool right? 😎

Let's get to the next feature.

Examples from assertions

Dhall has a nice feature named assertions. This lets you add unit tests to your files and the type-checking phase will fail if any of these assertions fail.

We wanted a way to get examples of using a Dhall file expression, and the best way to do so was extracting them from the assertions body.

For instance, if we have something like this in a Dhall file:

let example0 = assert : e0
let example1 = assert : e1
...

on the generated documentation you will look e0 and e1 as code examples.

The code manipulates the syntax-tree as the extractTypeFromSource does, but it's more compact and easy:

examplesFromAssertions :: Expr Void Import -> [Expr Void Import]
examplesFromAssertions expr = Maybe.mapMaybe fromAssertion values
    where
    values :: [Expr Void Import]
    values = map value $ bindings expr

    fromAssertion :: Expr Void Import -> Maybe (Expr Void Import)
    fromAssertion (Assert e) =  Just e
    fromAssertion _ = Nothing