Type on index & examples from assertions
Published: 2020-07-08 19:05:17

# 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 `Maybe`s, something like this:

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

I ["hoogled"](https://hoogle.haskell.org/?hoogle=%5BMaybe+a%5D+-%3E+%5Ba%5D) 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](https://docs.dhall-lang.org/tutorials/Language-Tour.html#introduction)). 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:

```haskell
-- 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:

```haskell
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:

```haskell
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:

```haskell
in x@1
```

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

```haskell
-- 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:

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/kd8zwen82k6b292o68oz.png)

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:

```haskell
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:

```haskell
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
```

You can see a preview of it here:

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/kszd5limmm8e6mmnqdla.png)

Neat 💥

## If you read this...

Thanks for reading! Keep in tune for future posts 😊.

If you liked this, please comment or react in the post ❤️

[firelink]: https://github.com/aitorres/firelink