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:
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
You can see a preview of it here:
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 ❤️
Top comments (2)
This is amazing!
Thanks!