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
If you just want to see the progress, check out here
Let's get started!
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:
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.
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
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
You can see a preview of it here:
Thanks for reading! Keep in tune for future posts 😊.
If you liked this, please comment or react in the post ❤️