Some thoughts on dependent types
Tags: functional, webdev
Published: 2021-03-06 20:20:01

---
title: Some thoughts on dependent types
published: true
description: What I think dependent types might be, how they're helpful, and a real-world dependent-types library
tags: functional, webdev
cover_image: https://images.unsplash.com/reserve/LJIZlzHgQ7WPSh5KVTCB_Typewriter.jpg?ixlib=rb-1.2.1&ixid=MXwxMjA3fDB8MHxwaG90by1wYWdlfHx8fGVufDB8fHw%3D&auto=format&fit=crop&w=641&q=80
---

According to [Wikipedia](https://en.wikipedia.org/wiki/Dependent_type):

> In computer science and logic, a dependent type is a type whose definition depends on a value.

Let's think about what that means from a programming perspective.  Say you're writing a microservice and you're expecting the input to be of a certain format, ie `Array Int`. If the format is correct, the computation can safely continue with the input value cast to `Array Int`. Otherwise, the server should respond immediately with a `400 Bad Request` error. The type's definition, which is roughly "succeed with an array of integers or fail with a 400 status code", depends on a value. It's a "dependent type."

# Coproducts

This sort of situation is usually described in code with something called a coproduct. Coproducts have two branches. In practice, one branch is often reserved for a failure case and one for a success case. Callbacks and promises in JavaScript emulate coproducts.

In a way, _all_ dependent types are coproducts in some shape or form. When you're dealing with a coproduct, the answer to the question "what's the type of this thing?" is "it depends", and coproducts are a way to answer "it depends" with a type.

# More intricate dependencies

Where dependent types get interesting is when the type needs to describe complex properties of a term.  A term could be, for example, a pair of arrays with the same length. The values `([1],[5])`, `([4,4,4],[3,2,1])`, and `([],[])` all fall into this category.

Several different types could represent this value.  For the remaining code examples in this article, unless otherwise noted, I'll be writing them in PureScript, a member of the Haskell family that compiles to JavaScript and is used mostly for web and Node applications.  Let's list some candidates for our (PureScript) type in order of specificity, from most general to most specific.

| Type | Comment |
| ---- | ------- |
| `forall a. a` | Trivial, saying "this value could by anything." |
| `forall a b. Tuple a b` | Slightly more useful, we know this is a tuple. |
| `forall a. Tuple a a` | Even more useful, we know this is a tuple where both sides have the same type. |
| `Tuple (Array Int) (Array Int)` | We usually stop here, and in a lot of cases this is fine. We have a tuple of arrays of integers. |
| `forall (s :: Nat). Tuple (Vec s Int) (Vec s Int)` | Even better! We now have a sized vector. Here, `s` is of [`kind Nat`](https://en.wikipedia.org/wiki/Kind_(type_theory)) and can be any non-negative integer. |

We'll extend this table with one more row later in the article, but for now, let's stop there.

As a next step, let's drop everything with a `forall` from the table. That's because, when we're dealing with a coproduct where the success branch has a `forall` in it, we have to treat it like a blob because it could be _anything_.  All we know is that it exists, and folks often call it an [_existential type_](https://medium.com/@stephenebly/an-introduction-to-existential-types-25c130ba61a4#:~:text=Existential%20types%20allow%20us%20to,in%20terms%20of%20other%20types.). That means we can only pass the "existential" blob to functions that [accept anything](https://github.com/illacceptanything/illacceptanything). Some examples are `\x -> x` (the identity function) and `_ -> 5` (a function that returns 5). In our microservice, we're not going to get very far with either of those functions.  The table now becomes:

| Type | Comment |
| ---- | ------- |
| `Tuple (Array Int) (Array Int)` | We usually stop here, and in a lot of cases this is fine. We have a tuple of arrays of integers. |

Yikes, that's a steep drop-off. Thankfully, we have a pretty useful type left. We can do a lot with two arrays of integers, but what we can't do is invoke a function that consume two vectors of equal length.  From here on out, when I say "vector", I mean an array or list where the size is built into the type.

One common function that consumes two vectors of equal length is `zip`.  `zip` takes the values of two arrays and performs some operation on them. For example, `zip (+) [1,2,3] [4,5,6]` would equal `[5,7,9]`. We really only have two options if we want to use `zip` on arrays/lists instead of vectors:

1. Build a runtime validator into our zip function that raises an error if the two lists/arrays being zipped are not of equal length.
1. Lob off values if one list/array is bigger than the other.

Neither of these are great options:

1. When you push runtime validation deep into the innards of code, you risk needing to roll back transactions like purchases and DB writes that happen beforehand. As a panacea, programmers often wind up wrapping these functions in nested `try/catch/finally` blocs, which makes silent failures more likely and makes the code harder to read and maintain.
1. When you truncate arrays to make a calculation work, it may make sense, but if the business outcome you're seeking relies on two arrays being the same length (ie collated lists of client data), you don't wanna just chop some data off.

There are several solutions to this problem, though, and the one I'll discuss in this article touches on the ontology of types and of programming. But first, a word on typeclasses. [Typeclasses](https://en.wikipedia.org/wiki/Type_class) will ultimately be part of our answer, but in the next section, I'd like to discuss how they are part of the problem.

# Application code versus library code

One of the most important distinctions in software is whether something is an application or a library. Libraries can remain open-ended because they exist to be used by some other library or application. Applications, on the other hand, are "batteries included". That means that they must have all the information they need to execute.

If a function is polymorphic (`forall`) in a library, it will be instantiated for a specific type in by the compiler in an application.  For example, take the `identity` function. It's fine in a library, but in an application, we have:

```haskell
main = do
  log $ identity "foo"
```

There, in the application, `identity` is no longer `forall a. a -> a`. It is determined by the compiler to be `String -> String`.

The same is true for polymorphic functions/values constrained by one or more typeclasses (ie `forall a. Show a => a -> String`).

```haskell
main = do
  log $ show 1
  log $ show true
```

In the example above, `show` is split by the compiler in to two different functions - one with the signature `Int -> String` and one with the signature `Boolean -> String`. They are different functions.

An application can have libraries or utilities within it, but once it is fully compiled, its types must be fully determined. Most compilers, like `ghc` and `purs`, even erase or partially erase the types from executable code because they are no longer necessary to run the program.

When I first learned strongly-typed languages with typeclasses like Haskell, Scala or PureScript, one mistake I made more times than I'd care to admit was (is 🤦) working with typeclass instances as if they "came alive" at runtime.

For example, if I wrote the following code:

```haskell
data Foo = Foo
instance showFoo :: Show Foo where
  show _ = "Foo"
```

I imagined the executable firing up, looking for an instance of `show` that would turn `Foo` into a string, producing a string, and continuing along its merry way. While this is sort of correct, it's not precise enough. When I'm looking for my keys or looking for hummus in the fridge, there's a chance I won't find either of them. But when an instance of typeclass is retrieved at runtime, it is _guaranteed_ to be there because the compiler found it at compile time. It'd be like if I could always find my keys or always find hummus in my fridge because someone made sure it was there for me (this is why, incidentally, I wish I lived in a world where typeclasses were real).

The truth is that the presence of typeclasses is _never_ determined at runtime.  Otherwise, there is a chance they wouldn't be there and the executable would crash. The closest that can happen is JIT compilation, where a runtime environment compiles a portion of a program once it receives enough information for the types to be fully determined. But even then, we're talking about compilation, as it happens _before_ execution.

I write all this because, going back to the table above, we could make the mistake of trying to use typeclasses to make our existential types more specific. For example, we could write:

> `forall s. Number s => Tuple (Vec s Int) (Vec s Int)`

And then, later downstream as we are manipulating the vector (ie appending new items, concatenating vectors), we could continue expressing those relationships through the constraint system. A concatenation function, for example, could look like this:

> `concat :: forall a b c x. Number a => Number b => Number c => Plus a b c => Vec a x -> Vec b x -> Vec c x`

The problem is that, while this code will compile just fine when you're working on a library, it will _not_ compile in an application because the compiler can't determine correct instance of `Number` or `Plus` to use. I have made this mistake many, many times.

That's not to say, however, that typeclasses are useless when working with dependent types. They're actually the only thing that can make the "two arrays of the same size" challenge work, as we'll see below. But they _won't_ work when left open-ended if you're writing application code. Your code will either refuse to compile or refuse to execute.

# Typeclasses to the rescue

So if typeclasses can't be precise about types that are imprecise, how can they be useful? In the world of dependent types, _typeclasses are useful when they are precise about types that are precisely imprecise._

So how can types be precisely imprecise? Let's zoom out for a second and consider what types _are_. This is a thorny subject because there are many mutually-reinforcing, and sometimes contradictory, definitions of the word "type". I tend to think of a type as a _representation_. For example, when I use `gcc` to compile C code, types represent how much space is needed to correctly access and read from memory.

In functional languages, types perform double-duty. They act as representations to the compiler, but they _also_ act as representations to those writing and reading the code. It would be natural to assume, then, that types represent things that matter to these people. One thing that matters is the code executing, and to that end, types represent things a processor will orchestrate, like sending TCP packets or emitting photons or moving a robot's arm.  Another thing that matters is code _not_ executing, like preventing code from making an automated payment more times than necessary. Both the presence and absence of an outcome can be represented, and in the case of absence, the fact that a type may be inhabited by a value (ie `Int` inhabited by `1`, `Unit` inhabited by `unit`) is incidental because it will never be processed by anything other than the compiler.

Insofar as types are representations, they can represent whatever we want them to represent so long as we agree on the representation. For example, so long as you and I agree that `Int` represents `...,-2,-1,0,1,2,...`, we can read, write, compile, and execute code using the `Int` type and have a shared understanding of what's supposed to happen.  So what can be represented? _Anything_ that humans understand can be represented by humans for humans, and because we humans understand what imprecision is, imprecision can be represented and types can represent imprecision.  And here is where typeclasses come back: for our dependent types, restating what I said above, _typeclasses are useful when they are precise about types that are precisely imprecise._

So what does that look like in code?  Let's create a type called `Unk'`. `Unk'` will represent something that's unknown.

```haskell
data Unk'
```

So long as you and I agree that `Unk'` represents "a value that is not known yet and may never be", we're good.  Now, we will likely have to deal with a bunch of things that are unknown, so let's create types for all of those things.

```haskell
data Unk0'
data Unk1'
data Unk2'
```

That's getting a bit tedious, so let's create a family of types (aka a `kind`) so that these `Unk`-s can be created ad libitum.

```haskell
data Unk'
foreign import data Unk0' :: Unk'
foreign import data UnkX' :: Unk' -> Unk'
```

This representation of unknowns (or more precisely, borrowing from Donald Rumsfeld, known-unknowns) has the same signature as the Peano representation of natural numbers.  I'm no expert on the cardinality of unknown things, but my intuition says that unknowns in calculations (and in life!) increment one by one. They are not fractional, nor are they negative.

Let's compare, now, one of the existentially qualified types from the table a few sections ago with one of our `Unk'`-s.

| Type | Comment |
| ---- | ------- |
| `forall a. a` | Existentially qualified type |
| `forall (u :: Unk'). u` | Also an existentially qualified type, but of `kind Unk'`. |

So far, `forall (u :: Unk'). u`  is just as unappealing as `forall a. a` - they both represent a blob.  But the crucial difference is that, when compiling a program, we can fill in our first `Unk'` with `Unk0'`, our second `Unk'` with `UnkX' Unk0'`, our third with `UnkX' (UnkX' Unk0')` and so forth and so on. By the end of the compilation process, we will know exactly which `Unk'` we are dealing with because the compiler will have filled them in one after the other.  In other words, the `forall (u :: Unk'). u` is guaranteed to turn into `Unk0'`, `UnkX' Unk0'`, or some other `Unk'`.

How can we get the compiler to dole out `Unk'`-s? In general, anytime we want to do something in an order, a monad is a good candidate because its order of execution is guaranteed.  So we can stash our current `Unk'` inside a monad, get the current `Unk'` when we need one, increment it, and put it back.

There's one problem, however. Monads stash stuff away at runtime. `Reader` stashes an environment, `Writer` stashes a log, `State` stashes a state, etc. But we need to stash our `Unk'`-s at _compile time_. So what type acts like a monad at compile time? The answer is an _indexed monad_.

An [indexed monad](https://qiita.com/kimagure/items/a0ee7313e8c7690bf3f5) has two additional parameters to represent the typelevel monadic context, traditionally called `i` and `o`. The full signature is `m i o a`, where `m` is the indexed monad, `i` is the input context, `o` is the output context and `a` is the value being "wrapped" just like in a garden-variety monad (from monad fame like `Maybe a`, `List a`, `Effect a` etc). The reason that the typelevel context is represented by _two_ parameters instead of just one is because, in order to enforce the contract of the indexed monad, the `o` of step _n - 1_ has to equal the `i` of step _n_. That way, we are sure that the context persists through every step.  The types may proceed like this in an indexed `do` bloc:

```haskell
m foo bar Unit
m bar baz Unit
m baz raz Unit
```

The next step is making this automated so that `Unk'`-s go from one `Unk'` to the next in automated fashion. Here's a small program that increments our `Unk'` counter four times and exits.

```haskell
module Data.DT.Unk where

import Prelude
import Control.Applicative.Indexed (class IxApplicative, class IxApply, class IxFunctor, ipure)
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Indexed (class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.Identity (Identity(..))
import Data.Newtype (class Newtype, unwrap)

data Unk'

foreign import data UnkX' :: Unk' -> Unk'

foreign import data Unk0' :: Unk'

newtype Unk (u :: Unk') a
  = Unk (Identity a)

newtype MUnk :: forall k1 k2. k1 -> k2 -> Type -> Type
newtype MUnk i o a
  = MUnk (Identity a)

derive instance newtypeUnk :: Newtype (MUnk i o a) _
derive newtype instance functorMUnk :: Functor (MUnk i o)
derive newtype instance applicativeMUnk :: Applicative (MUnk i o)

derive newtype instance applyMUnk :: Apply (MUnk i o)

instance freeProgramIxFunctor :: IxFunctor MUnk where
  imap f (MUnk a) = MUnk (f <$> a)

instance freeProgramIxApplicative :: IxApply MUnk where
  iapply (MUnk f) (MUnk a) = MUnk (f <*> a)

instance freeProgramIxApply :: IxApplicative MUnk where
  ipure a = MUnk $ pure a

instance freeProgramIxBind :: IxBind MUnk where
  ibind (MUnk monad) function = MUnk (monad >>= (unwrap <<< function))

instance freeProgramIxMonad :: IxMonad MUnk

unk' :: forall m (u :: Unk'). Applicative (m u (UnkX' u)) => m u (UnkX' u) (Unk u Unit)
unk' = pure $ Unk $ Identity unit

-- the type cast at the beginning is the equivalent
-- of a "thunk", starting the unks at 0
-- our `unk'` then kicks in, doing the incrementing
-- automatically thanks to the type  signature
prog = Ix.do
  _ <- unk' :: MUnk Unk0' (UnkX' Unk0') (Unk Unk0' Unit)
  _ <- unk'
  _ <- unk'
  _ <- unk'
  ipure unit
```

So now that we're doling out `Unk'`-s one after the other, the next thing to do is to consume them somehow.  _That's_ where typeclasses come back in.

Recall that, in the previous section, we had temporarily banished typeclasses when working with existential types because we could not nail down a precise type needed for a typeclass lookup. But now that the `Unk'`-s are precise, we can always nail down the precise typeclass to retrieve.

For kicks, let's create a function that asserts two `Unk'` values are equal and another function that consumes equal `Unk`-s. "Equal `Unk'`-s" here can be whatever we want it to be. In this case, we'll make it trivial - if you ask, they're equal, but if you don't, they're not. That's not unlike how I dole out money for candy at my house: I've never been known to say no, but you gotta ask.

```haskell
module Data.DT.Unk where

import Prelude
import Control.Applicative.Indexed (ipure)
import Control.Monad.Indexed (class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.Identity (Identity(..))
import Data.Tuple.Nested ((/\), type (/\))

data Unk'

foreign import data UnkX' :: Unk' -> Unk'

foreign import data Unk0' :: Unk'

newtype Unk (u :: Unk') a
  = Unk (Identity a)

derive newtype instance eqUnk :: Eq a => Eq (Unk s a)

derive newtype instance functorUnk :: Functor (Unk s)

derive newtype instance applicativeUnk :: Applicative (Unk s)

derive newtype instance applyUnk :: Apply (Unk s)

unk' :: forall m (u :: Unk'). Applicative (m u (UnkX' u)) => m u (UnkX' u) (Unk u Unit)
unk' = pure $ Unk $ Identity unit

assertEq :: forall (m :: Type -> Type) (j :: Unk') (k :: Unk'). Applicative m => (Unk j Unit /\ Unk k Unit) -> m (Unk j Unit /\ Unk j Unit)
assertEq _ = pure $ (Unk $ Identity unit) /\ (Unk $ Identity unit)

consumeEq :: forall (j :: Unk'). Unk j Unit -> Unk j Unit -> Unk j Unit
consumeEq _ = identity

prog ::
  forall m (u :: Unk').
  IxMonad m =>
  Applicative (m u (UnkX' u)) =>
  Applicative (m (UnkX' u) (UnkX' (UnkX' u))) =>
  Applicative (m (UnkX' (UnkX' u)) (UnkX' (UnkX' u))) =>
  m u (UnkX' (UnkX' u)) Unit
prog = Ix.do
  u0 <- unk'
  u1 <- unk'
  l /\ r <- assertEq (u0 /\ u1)
  let
    e = consumeEq l r
  ipure unit
```

Let's see how that looks in the IDE:

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/1jo0jesit4oef430xif6.png)
And now let's see how that looks if I consume two equal `Unk'`-s that don't have an equality assertion.

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

The compiler is behaving exactly how we want it.

Note that, in the example above, I made the indexedmonad polymorphic so that you can see its signature.  The signature will is pretty hairy, so in a real library, we'd create a type alias using the `type` keyword that encapsulates that complexity.

`Unk'` doesn't have to be just `Unk'`, just like `Int` doesn't have to be just `Int`. It can be `List Int`, `Maybe Int`, `Effect Int`, etc. Similarly, our `Unk'` can be part of some larger structure.  In the case of the library I'll talk about below, `Unk` is part of a type that represents an algebraic expression, ie `Plus Unk0' Zero'` would be `x + 0` at the term-level.

The more one works with types, the more one gets used to the fact that we often write little programs at the type level for the compiler to execute at compile time.  The typelevel program above that gates access to `consumeEq` is like the runtime program below:

```haskell
if a /= b then throwError else consumeEq a b
```

So what sorts of programs can you write at the type-level? The answer, amazingly, is anything you can write at the term level so long as it does not require any I/O - I know of no compiler (yet) that lets types write to the file system or make a network call. Which brings us to the question: what type of program are we writing with our `Unk'`-s?  Well, what type of program keeps track of unknown variables, makes computations when it can, and raises assertions when things fail?  It's called a _compiler_. Meaning that, when we work with dependent types in this manner, we write a compiler at the type-level.

# Pushing the unknown

We can extend our reasoning about known-unknowns even further. Let's go back to my statement:

> When an instance of a typeclass is retrieved at runtime, it is _guaranteed_ to be there because the compiler found it at compile time.

In this statement, the word "it" is used twice, and it refers to a typeclass. Crucially, it does _not_ refer to a type. That means that the compiler can find a _precise_ typeclass _without_ knowing the precise type on which it will be operating. When I realized this, I felt several neurons break in my brain, and it took writing this article to mend them.

Going back to the analogy about my keys or my hummus, it is as if the compiler guaranteed that hummus will be in the fridge without knowing what hummus is. We are on the razor's edge here between typeclasses and constrained existential types.  Let's summarize the difference here.

| Thing | Example | Comment |
| ----- | ------- | ------- |
| Constrained existential type | `forall a. Show a => Effect Unit` | Compiler has no clue what to do with this. Barfs. |
| Typeclass instance with constraint | `instance myTC :: Show a => TC Unit` | Totally fine, no complaints. |

Let's give a constrained existential type to our poor old compiler and watch it struggle. I do this with no joy, but "you can't make an omelette...".

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/8eiq9gimabgsq2xnojym.png)

Now, let's operate purely in the realm of typeclass instances with constraints. We'll create several - one to reflect a type as a string via a proxy (`TLShow`) and one to recursively increment an index on an indexed type (`IxRec`), similar to `unk'` above but written as a typeclass.

We'll start with foreign code that hides an array. This array will be fetched at runtime.

```javascript
// Main.js for the foreign import
// Main.js for the foreign import
exports.arr0 = function () {
  return [1, 2, 3, 4, 5];
};
```

Then, in the PureScript, it will appear as if a type is being created for each element in the array.

```haskell
module Test.Main where

import Prelude

import Control.Monad.Indexed (class IxApplicative, class IxApply, class IxBind, class IxFunctor, class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.List (List(..), fromFoldable)
import Data.Newtype (class Newtype, unwrap)
import Effect (Effect)
import Effect.Class (class MonadEffect)
import Effect.Class.Console (log)
import Type.Proxy (Proxy(..))

data Unk

foreign import data Unk0 :: Unk

foreign import data UnkX :: Unk -> Unk
newtype MUnk (i :: Unk) (o :: Unk) a
  = MUnk (Effect a)

derive instance newtypeUnk :: Newtype (MUnk i o a) _

derive newtype instance functorMUnk :: Functor (MUnk i o)

derive newtype instance applicativeMUnk :: Applicative (MUnk i o)

derive newtype instance applyMUnk :: Apply (MUnk i o)
derive newtype instance bindMUnk :: Bind (MUnk i o)
derive newtype instance monadMUnk :: Monad (MUnk i o)
derive newtype instance monadEffectMUnk :: MonadEffect (MUnk i o)

instance freeProgramIxFunctor :: IxFunctor MUnk where
  imap f (MUnk a) = MUnk (f <$> a)

instance freeProgramIxApplicative :: IxApply MUnk where
  iapply (MUnk f) (MUnk a) = MUnk (f <*> a)

instance freeProgramIxApply :: IxApplicative MUnk where
  ipure a = MUnk $ pure a

instance freeProgramIxBind :: IxBind MUnk where
  ibind (MUnk monad) function = MUnk (monad >>= (unwrap <<< function))

instance freeProgramIxMonad :: IxMonad MUnk

class TLShow :: ∀ (k ∷ Type). k → Constraint
class TLShow i where
  tlShow :: Proxy i -> String

instance tlShowUnk0 :: TLShow Unk0 where
  tlShow _ = "Unk0"

instance tlShowUnkX :: TLShow x => TLShow (UnkX x) where
  tlShow _ = "UnkX (" <> tlShow (Proxy :: Proxy x) <> ")"

class IxRec m where
  next :: forall (i :: Unk) a. Show a => TLShow i => a -> m i (UnkX i) a
  done :: forall (i :: Unk). m i Unk0 Unit

iFor_ :: forall (i :: Unk) m a. Show a => TLShow i => IxRec m => IxMonad m => List a -> m i Unk0 Unit
iFor_ Nil = done
iFor_ (Cons a b) = Ix.do
  _ <- next a
  iFor_ b

printMUnk :: forall (i :: Unk). TLShow i => MUnk i i Unit
printMUnk = Ix.do
  log $ tlShow (Proxy :: Proxy i)

instance ixRec :: IxRec MUnk where
  next a = Ix.do
    printMUnk
    log $ show a
    pure a
  done = pure unit

foreign import arr0 :: Effect (Array Int)

main :: Effect Unit
main = do
  list0 <- fromFoldable <$> arr0
  let (MUnk o) = (iFor_ :: List Int -> MUnk Unk0 Unk0 Unit) list0
  o
```

The output when we run `npx spago test` is 🥁

```bash
08:19 meeshkan-abel@Abel:~/mike/delete-me-dt$ npx spago test
[info] Build succeeded.
Unk0
1
UnkX (Unk0)
2
UnkX (UnkX (Unk0))
3
UnkX (UnkX (UnkX (Unk0)))
4
UnkX (UnkX (UnkX (UnkX (Unk0))))
5
[info] Tests succeeded.
```

So, even though the compiler has no clue at compile-time that it will eventually deal with an `UnkX (UnkX (UnkX (UnkX (Unk0))))`,
 it knows that it will need a typeclass instance to act on this type and it has a strategy, [mathematical induction](https://en.wikipedia.org/wiki/Mathematical_induction), to find it. Namely, it finds the correct instance of `tlShow` because it knows that the first `tlShow` corresponds to the instance `tlShowUnk0` and the next `tlShow`-s all must, via induction, to `tlShowUnkX`.

For me, this is as mystical as programming gets. The question is "where is the type?" A library with a polymorphic function can just pass the buck to an executable, saying "someone else will determine the type later down the line." But when we're in the land of executables, we can't pass the buck. So the compiler doesn't know the type, the programmer doesn't know the type, and the runtime doesn't know the type. And yet it exists and, as we see above, is printed out on the screen. So what in life exists but cannot be known? I'll leave it to the reader to answer that question...

# purescript-vec-dt

Shameless plug: I wrote a lil' library called [`purescript-vec-dt`](https://github.com/mikesol/purescript-vec-dt) to solve the array-of-equal-length challenge I presented above. Let's look at a bit of application code written with the library.

In this example, the I/O operation is reading two arrays from JavaScript files.  Here is our JS:

```javascript
exports.arr0 = function () {
  return [1, 2, 3];
};
exports.arr1 = function () {
  return [100, 200, 300];
};
```

And here is the PureScript using `purescript-vec-dt`:

```haskell
module Test.Main where

import Prelude

import Control.Applicative.Indexed (class IxApplicative, ipure)
import Control.Apply.Indexed (class IxApply)
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Error.Class (class MonadThrow)
import Control.Monad.Indexed (class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.DT.Vec (assertEq, toList, vec', zipWithE)
import Data.Functor.Indexed (class IxFunctor)
import Data.List (fromFoldable)
import Data.Newtype (class Newtype, unwrap)
import Data.Tuple.Nested ((/\))
import Effect (Effect)
import Effect.Class.Console (log)
import Effect.Exception (Error, error)

foreign import arr0 :: Effect (Array Int)
foreign import arr1 :: Effect (Array Int)

newtype Ctxt :: forall k1 k2. k1 -> k2 -> Type -> Type
newtype Ctxt i o a
  = Ctxt (Effect a)
derive instance newtypeCtxt :: Newtype (Ctxt i o a) _
derive newtype instance freeProgramFunctor :: Functor (Ctxt i o)
derive newtype instance freeProgramApply :: Apply (Ctxt i o)
derive newtype instance freeProgramBind :: Bind (Ctxt i o)
derive newtype instance freeProgramApplicative :: Applicative (Ctxt i o)
derive newtype instance freeProgramMonad :: Monad (Ctxt i o)
derive newtype instance freeProgramMonadThrow :: MonadThrow Error (Ctxt i o)
instance freeProgramIxFunctor :: IxFunctor Ctxt where
  imap f (Ctxt a) = Ctxt (f <$> a)
instance freeProgramIxApplicative :: IxApply Ctxt where
  iapply (Ctxt f) (Ctxt a) = Ctxt (f <*> a)
instance freeProgramIxApply :: IxApplicative Ctxt where
  ipure a = Ctxt $ pure a
instance freeProgramIxBind :: IxBind Ctxt where
  ibind (Ctxt monad) function = Ctxt (monad >>= (unwrap <<< function))
instance freeProgramIxMonad :: IxMonad Ctxt

main :: Effect Unit
main = do
  list0 <- fromFoldable <$> arr0
  list1 <- fromFoldable <$> arr1
  let 
    (Ctxt toPrint) = Ix.do
          v0 <- vec' list0
          v1 <- vec' list1
          l /\ r <- assertEq (error "not eq") (v0 /\ v1)
          ipure $ zipWithE (+) l r
  toPrint >>= log <<< show <<< toList
```

And here's the output:

```bash
(101 : 202 : 303 : Nil)
```

Under the hood, the mechanics are the same as the `Unk'` example above. We are making an assertion that two lists are of equal size (`assertEq`) and, once that assertion is made, we can consume them with a `zipWithE` function that only operates on vectors of equal size.

We can see that it typechecks fine in the IDE, which is my sparring partner when I'm working in PureScript.

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

Let's see a variation where we concatate vectors. Because concatenation increments the unknown value by the same amount on both sides, the equality assertion still holds.

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


One thing to note in the example above is that the indexed monad starts with a "thunk" in the form of `ipure unit`. Previously, this was not necessary because the indexed monad did not have any inner computations, meaning the `i` and `o` never had to change. When there are intermediary values, the compiler needs a "thunk" to know where to start.

Assertions are also transitive.

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

Now, let's break the compilation by trying to operate on vectors of unequal length.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/16erra3lm6wbn8k56wkl.png)

And cuz breaking things is fun, let's break it by operating on vectors without first asserting their equality.

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

I've started to weave this library into the Meeshkan code base whenever we consume JSON or DB rows that eventually need to be zipped. It has afforded me two things:

- I can do all my assertions in the first 4-5 lines of the main function and they remain valid for the whole program. When I get incorrect input, the program exits immediately.
- In a context where I use `zipWithE` several times in a row, I don't have to worry about remembering to assert equality.  The compiler enforces it for me. 

Mind you, in none of these cases do we know the actual length of the vectors we're working with. We can only deal with known-unknowns, but that's all we need. The answer to the question "how long is the vector" is "it depends", which, coming back where we started, is why these are called "dependent types."