representation of its meaning. For a language of arithmetic expression, the
"meaning" of an expression is just a number (the result of simplifying the expression).
For a language of booleans, <code>and</code>, and <code>or</code>, the "meaning" is a boolean
for the same reason. Since an expression in the language can be ill-formed (like
<code>list(5)</code> in Python), the "meaning" (<em>semantic domain</em>) of a
complicated language tends to include the possibility of errors.
{{</sidenote>}} I should be able to make my function be of type `Expr -> Val`, and not
`Expr -> Maybe Val`!
Unfortunately, this is not quite true. It is true that if the student's type checking
function is correct, then there will be no way for a type error to occur during
the evaluation of an expression "validated" by said function. The issue is, though,
that __the type system does not know about the expression's type-correctness__. Haskell
doesn't know that an expression has been type checked; worse, since the function's type
indicates that it accepts `Expr`, it must handle invalid expressions to avoid being [partial](https://wiki.haskell.org/Partial_functions). In short, even if we __know__ that the
expressions we give to a function are type safe, we have no way of enforcing this.
A potential solution offered in class was to separate the expressions into several
data types, `BoolExpr`, `ArithExpr`, and finally, a more general `Expr'` that can
be constructed from the first two. Operations such as `and` and `or`
will then only be applicable to boolean expressions:
```Haskell
data BoolExpr = BoolLit Bool | And BoolExpr BoolExpr | Or BoolExpr BoolExpr
```
It will be a type error to represent an expression such as `true or 5`. Then,
`Expr'` may have a constructor such as `IfElse` that only accepts a boolean
expression as the first argument:
```Haskell
data Expr' = IfElse BoolExpr Expr' Expr' | ...
```
All seems well. Now, it's impossible to have a non-boolean condition, and thus,
this error has been eliminated from the evaluator. Maybe we can even have
our type checking function translate an unsafe, potentially incorrect `Expr` into
a more safe `Expr'`:
```Haskell
typecheck :: Expr -> Either TypeError (Expr', ExprType)
We'll be copying functionality back and forth, and our code will suffer. Wouldn't it be
nice if we could somehow tag our expressions with the type they produce? Instead of
`BoolExpr` and `ArithExpr`, we would be able to have `Expr BoolType` and `Expr IntType`,
which would share the `IfElse` constructor...
It's not easy to do this in canonical Haskell, but it can be done in Idris!
### Enter Dependent Types
Idris is a language with support for [dependent types](https://en.wikipedia.org/wiki/Dependent_type). Wikipedia gives the following definition for "dependent type":
> In computer science and logic, a dependent type is a type whose definition depends on a value.
This is exactly what we want. In Idris, we can define the possible set of types in our
In this post, we learned that type checking can be used to translate an expression into
a more strongly-typed data type, which can be (more) safe to evaluate. To help
strengthen the types of our expression language, we used the Idris language and
its support for dependent types and Generalized Algebraic Data Types (GADTs).
I this was interesting!
As usual, you can find the code for this post in this website's Git repository. The
source file we went through today is found [here](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntr.idr).