According to Wikipedia:

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.

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. That means we can only pass the "existential" blob to functions that accept anything. 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:

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.
2. 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.
2. 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 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:

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).

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:

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.

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.

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.

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.

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

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.

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.

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:

And now let's see how that looks if I consume two equal Unk'-s that don't have an equality assertion.

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:

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.

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...".

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.

// 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.

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 🥁

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, 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 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:

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

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

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:

(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.

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.

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.

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

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

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."