Liborator Articles About

Published: 17th October 2026

Understanding dependently-typed filter

Reading introductions to programming with dependent types, one usually encounters a vector. It is a list that also carries information about its length on the type-level. This allows for more precise specification of program behaviour and helps ruling out even more errors during compile time.

Consider following declarations:

-- Forward declaration of 'Vec' type constructor and functions.
-- Data constructors and implementations may be completed later.

-- 'Vec' is a type constructor accepting 2 arguments. First is a natural number
-- and the other is a type.
data Vec : Nat -> Type -> Type

-- Put an item at the end of a vector. (S n) means "Successor of n", so length
-- of the output vector will be 1 more than the input vector.
append  : a -> Vec n a -> Vec (S n) a
-- Concatenate one vector with another.
concat  : Vec m a -> Vec n a -> Vec (m + n) a
-- Return the first element of a vector. It only accepts a vector of length
-- at least 1, which makes the function infallible.
head    : Vec (S n) a -> a
-- Transform each element of a vector by a function.
map     : (a -> b) -> Vec n a -> Vec n b
-- Reverse the vector.
reverse : Vec n a -> Vec n a
-- Given vectors of equal length, return a vector of pairs from the original
-- vectors.
zip     : Vec n a -> Vec n b -> Vec n (a, b)

Even without implementations, we can deduce a plenty of information from the signatures alone, like:

However, one well-known function is usually absent in the introductions:

-- Create a vector of elements that satisfy a predicate from the input vector.
filter : (a -> Bool) -> Vec n a -> ???

In this article, I implement everything from scratch in a lovely programming language Idris 2. By the end, we will understand both how filter works and why it is usually omitted from introductory examples.

Disclaimer: It’s a shame I need to even mention it, but the year is 2026 and folks are trying to cut corners with their (ab)use of generative AI. This article is written by me and me only.

I prompted myself to “Make no mistakes.”. But I am just a guy on the Internet, so double-check everything.

Note on natural numbers in dependently-typed languages

Before we begin though, a quick note on natural numbers, because they are central to dependently-typed programming languages. Their representation in the type system is similar to:

data Natural : Type where
  -- Base case, zero, 0, ...
  Zero : Natural
  -- Step, successor, 1 + _, ...
  Successor : Natural -> Natural

Number 3 then looks like:

threeNatural : Natural
threeNatural = (Successor (Successor (Successor Zero)))

-- The canonical version from Prelude. Reserving one-letter constructors
-- for them saves a bit of typing, since they are used often.
threeNat : Nat
threeNat = (S (S (S Z)))

During runtime, they are normal machine integers, since arithmetic in this (unary) representation, albeit doable, would be hopelessly inefficient.
Having them defined as a data type with Z (for 0 value) and S (for successor function) constructors helps reasoning though. Techniques like mathematical (or more generally structural) induction rely on this representation.

Vec definition and examples

With clarification of the Z and S symbols out of the way, let’s implement the vector data type:

data Vec : Nat -> Type -> Type where
  -- An empty vector.
  Empty : Vec Z a
  -- 'Cons' is a historic name for prepending an item to a list, coming from
  -- Lisp.
  -- This constructor accepts 2 arguments, an item and a vector and returns a
  -- vector of length 1 more than the input vector.
  Cons  : a -> Vec n a -> Vec (S n) a

Vec itself is a type constructor with 2 arguments.
Argument n is a natural number, not a type. It is usually called an “index”, because it varies across data constructors. You can see it is equal to Z for Empty and (S n) for Cons.
Argument a is usually called a “parameter”, because it is uniform across all data constructors. Parameters can be thought of as “generic types” in mainstream languages.

Empty and Cons are the data constructors of Vec. Each data constructor can have different arguments. Calling them constructs values of their respective types - Empty constructs a value of type Vec 0 a and Cons of type Vec (S n) a.

Here are some examples:

v1 : Vec 0 _
v1 = Empty

v2 : Vec 1 Char
v2 = Cons 'x' Empty

v3 : Vec 2 Nat
v3 = Cons 1 (Cons 2 Empty)

failing "Mismatch between: 0 and 1."
  vBad : Vec 1 Nat
  vBad = Empty

Besides few successful instantiations, you can observe a feature of Idris called failing blocks.
It allows a syntactically valid code that does not compile be part of your source code, which I find rather nifty.
The (optional) string after the failing keyword is a part of an error message compiler would have emitted had the code block not been inside failing block, so:

-- failing "Mismatch between: 0 and 1."
vBad : Vec 1 Nat
vBad = Empty

produces:

$ idris2 Vec.idr
...
1/1: Building Vec (Vec.idr)
Error: While processing right hand side of vBad. When unifying:
    Vec 0 Nat
and:
    Vec 1 Nat
Mismatch between: 0 and 1.

Vec:59:8--59:13
 55 | v3 = Cons 1 (Cons 2 Empty)
 56 |
 57 | -- failing "Mismatch between: 0 and 1."
 58 | vBad : Vec 1 Nat
 59 | vBad = Empty
             ^^^^^

The error tells us that during unification (solving a system of type equations), vBad was declared to be of type Vec 1 Nat, but Empty can only be Vec 0 Nat. It is impossible to satisfy both, so a mismatch between 0 and 1 is reported.

Naive implementation of map (that works)

Armed with the definition of Vec, let’s implement our first version of map, called mapNaive:

mapNaive : (a -> b) -> Vec n a -> Vec n b
mapNaive _ Empty = Empty
mapNaive f (Cons x xs) = Cons (f x) (mapNaive f xs)

We can perform pattern matching on the data constructors directly in the function definition.

Empty case:

This is the base case, so no matter the function, Empty must be returned.

Cons case:

Cons means the length of the input vector is at least 1, so S k. Therefore, length of xs is any natural number k. Because the recursive step

mapNaive f xs

is immediately used in the Cons constructor, which increases the length by 1, Idris is able to deduce the overall length of the vector stays the same.

Idris has a nice REPL support, so we can load the file and try few examples.
Note that (\x => x + 123) is an anonymous function syntax.

$ idris2 Vec.idr
...
Vec> mapNaive S (Cons 1 (Cons 2 Empty))
Cons 2 (Cons 3 Empty)
Vec> mapNaive (\x => x + 123) (Cons 1 (Cons 2 Empty))
Cons 124 (Cons 125 Empty)

There is nothing wrong with the implementation per se, the reason I call it “naive” is because it is not tail-recursive. It allocates stack space in proportion to the length of the vector, so calling this function on a vector of length say 1 million will probably get the program terminated. In later installments, we will come back to map and make it tail-recursive.

Naive implementation of filter (that does not work)

Following our success with map, let’s try the same approach with filter. We introduce another index m for the resulting vector length, because we do not know a priori how long it is going to be:

filterBad : (a -> Bool) -> (Vec n a) -> (Vec m a)

That will not type check though.

Empty case:

failing "Mismatch between: 0 and m."
  filterBadEmpty : (a -> Bool) -> (Vec n a) -> (Vec m a)
  filterBadEmpty _ Empty = Empty

The error tells us that during unification, m is required to simultaneously be equal to 0 and be unconstrained. This cannot be satisfied and unification fails.

Cons case:

failing "Mismatch between: S ?m and m."
  filterBadCons : (a -> Bool) -> (Vec n a) -> (Vec m a)
  filterBadCons pred (Cons x xs) =
    let rest := filterBadCons pred xs in  -- `rest` is of type `Vec m a`
      if pred x then
        Cons x rest -- Wrong, since value of type `Vec (S m) a` would be returned!
      else
        rest

Vector rest, which is a result of recursive call to filterBadCons, is declared to be of type Vec m a. So, if x satisfies the predicate pred, prepending it to rest changes the result type to Vec (S m) a.
No natural number satisfies k = k + 1, therefore unification fails.

It seems we are in a pickle. We know there exists m that would be equal to length of the filtered vector. But with our current approach, we have no way to encode this knowledge of existence of m into the type system. The actual value depends on the predicate, which is an information only known at runtime, because different predicates may yield different lengths. And since length is part of the type now, we cannot construct a vector until we know its length!

So … what now?

Flaw of previous approach and a way out

Looking back at the mapNaive function, it does not really care about the value of an index n in Vec n a. It can be anything - 0, 1, 1337, …
mapNaive transforms elements of the vector, length remains fixed.

filter, on the other hand, changes the length of the vector in a way that is impossible to determine at compile time. As mentioned in the previous section, it depends on the predicate. We somehow need to bundle1 a number together with a vector that is guaranteed to have length equal to this number into a single type.

Something like:

import dataclasses
import typing as t

@dataclasses.dataclass(frozen=True, slots=True)
class LengthAwareList[A]:
    n: int
    lst: list[A]

    def __post_init__(self) -> None:
        # `__post_init__` is a special method of data classes that is executed
        # post initialization.
        assert self.n == len(self.lst)

but with a compile time guarantee rather than a runtime check. :)

Solution to our struggles is a construction known as a dependent sum type.

It’s a record (or a tuple) with a twist. Instead of types of its fields being fixed, the distinguishing feature of dependent pair types is that field types defined later in the body can depend on the values of fields already defined.

-- Record is a data type with a single constructor. Fields are named and
-- projections (field accessors) are automatically generated.
record LengthAwareVec (a : Type) where
  constructor MkLengthAwareVec
  len : Nat
  -- Type of 'vec' field depends on the **value** of 'len' field!
  vec : Vec len a

Observe that the len field is referenced in a type annotation of the vec field.

Playing with it a bit:

lav1 : LengthAwareVec Char
lav1 = MkLengthAwareVec 0 Empty

lav2 : LengthAwareVec Char
lav2 = MkLengthAwareVec 1 (Cons 'a' Empty)

failing "Mismatch between: 1 and 0."
  lavBad : LengthAwareVec Char
  lavBad = MkLengthAwareVec 0 (Cons 'a' Empty)

Let’s see if we make any progress with this fancy new feature.

Naive implementation of filter (that finally works)

First, function signature needs to reflect the new type. Again, “naive” is to be understood as not tail-recursive.

filterNaive : (a -> Bool) -> (Vec n a) -> LengthAwareVec a

Empty case:

Filtering an empty vector is the base case and no matter the predicate, Empty vector is returned. Here, it needs to be bundled with Z for length 0.

filterNaive _ Empty = MkLengthCheckedVec Z Empty

Compiler accepts this implementation and also correctly rejects a counting mistake:

failing "Mismatch between: 0 and 1."
  filterNaiveBadEmptyLength : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveBadEmptyLength _ Empty = MkLengthAwareVec 1 Empty

Cons case:

filterNaive pred (Cons x xs) =
    let rest := filterNaive pred xs in
      if pred x then
        MkLengthAwareVec (S rest.len) (Cons x rest.vec)
      else
        rest

And again, implementation is accepted!

In the True branch, you can see that incrementing the length and prepending an item to a vector must be done in a lockstep. Omitting one or the other results in an error:

failing "Can't solve constraint between: S (len rest) and rest .len"
  filterNaiveNoS : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveNoS pred (Cons x xs) =
      let rest := filterNaive pred xs in
        if pred x then
          MkLengthAwareVec rest.len (Cons x rest.vec) -- Forgotten (S rest.len)
        else
          rest

failing "Can't solve constraint between: rest .len and S (rest .len)"
  filterNaiveNoCons : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveNoCons pred (Cons x xs) =
      let rest := filterNaive pred xs in
        if pred x then
          MkLengthAwareVec (S rest.len) rest.vec -- Forgotten (Cons x rest.vec)
        else
          rest

Here are some examples from the REPL:

$ idris2 Vec.idr
...
Vec> filterNaive (\x => x > 2) Empty
MkLengthAwareVec 0 Empty
Vec> filterNaive (\x => x < 2) (Cons 1 (Cons 2 Empty))
MkLengthAwareVec 1 (Cons 1 Empty)
Vec> filterNaive (\x => x <= 2) (Cons 1 (Cons 2 Empty))
MkLengthAwareVec 2 (Cons 1 (Cons 2 Empty))
Vec> filterNaive (\x => x > 2) (Cons 1 (Cons 2 Empty))
MkLengthAwareVec 0 Empty

That’s it! We are done!

Please note that Idris’ standard library already contains Vect data type and common functions acting on it, including filter. However, instead of returning a record, stdlib’s filter returns a dependent tuple. Here is the signature, using the :module (load a module) and :t (show the type of expression) affordances of Idris REPL:

Vec> :module Data.Vect
Imported module Data.Vect
Vec> :t Data.Vect.filter
Data.Vect.filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)

The

(p : Nat ** Vect p elem)

is the dependent tuple syntax. Expressive power of records and tuples is the same, I opted for the record because I find it a bit more readable. Complete program below includes filterNaivePair with dependent tuple for comparison.

To answer the question posed in the introduction of the article, the signature of filter function is:

filter : (a -> Bool) -> Vec n a -> (m : Nat ** Vec m a)

And I also believe all the talk about dependent sums justifies why tutorials omit the filter function, so let me know if I did a good job explaining it. :D

Conclusion and future work

I sincerely hope I did not overwhelm you and you learnt something new today. Dependent types are a fascinating topic bridging type theory, formal methods, programming and others, so they are daunting.

I intend this article to be the first in series of posts exploring dependent types themselves as well as their connections to other topics I find interesting.

Namely:

My implementations of map and filter are not tail-recursive. To correct it, we will need to dip our toes in proving some theorems.

I used phrases like “there exists a length” and “map works for all lengths”. Indeed, dependent sums can model existential quantification, while their duals - dependent products - can model the universal quantification.
I will visit this as well.

Dependent types let us really constrain the values. Properties like:

can be expressed and automatically checked by the compiler. How to leverage them to write safer programs? How to find a balance between type-level “golfing” and runtime checks?

The “Idris book” contains nice examples of using dependent types for modelling state machines. How does that compare to model checking done by eg. TLA+? Encoding a transaction or a network protocol in the type system would be an interesting exercise.

And many more … stay tuned for next installments!

Complete program

To have the complete program at hand, it is provided here in its entirety. You can download it to Vec.idr and launch a REPL, as is done several times in the article.

Program:

module Vec

%default total

-- Forward declaration of 'Vec' type constructor and functions.
-- Data constructors and implementations may be completed later.

-- 'Vec' is a type constructor accepting 2 arguments. First is a natural number
-- and the other is a type.
data Vec : Nat -> Type -> Type

-- Put an item at the end of a vector. (S n) means "Successor of n", so length
-- of the output vector will be 1 more than the input vector.
append  : a -> Vec n a -> Vec (S n) a
-- Concatenate one vector with another.
concat  : Vec m a -> Vec n a -> Vec (m + n) a
-- Return the first element of a vector. It only accepts a vector of length
-- at least 1, which makes the function infallible.
head    : Vec (S n) a -> a
-- Transform each element of a vector by a function.
map     : (a -> b) -> Vec n a -> Vec n b
-- Reverse the vector.
reverse : Vec n a -> Vec n a
-- Given vectors of equal length, return a vector of pairs from the original
-- vectors.
zip     : Vec n a -> Vec n b -> Vec n (a, b)

data Natural : Type where
  -- Base case, zero, 0, ...
  Zero : Natural
  -- Step, successor, 1 + _, ...
  Successor : Natural -> Natural

threeNatural : Natural
threeNatural = (Successor (Successor (Successor Zero)))

-- The canonical version from Prelude. Reserving one-letter constructors
-- for them saves a bit of typing, since they are used often.
threeNat : Nat
threeNat = (S (S (S Z)))

-- 'Vec' accepts 2 arguments. First is a natural number and the other is a type.
-- 'Vec 123 Char' is a 'Type'
-- 'Vec 123' is a type-level function, so 'Type -> Type'
data Vec : Nat -> Type -> Type where
  -- An empty vector.
  Empty : Vec Z a
  -- 'Cons' is a historic name for prepending an item to a list, coming from
  -- Lisp.
  -- This constructor accepts 2 arguments, an item and a vector and returns a
  -- vector of length 1 more than the input vector.
  Cons  : a -> Vec n a -> Vec (S n) a

v1 : Vec 0 _
v1 = Empty

v2 : Vec 1 Char
v2 = Cons 'x' Empty

v3 : Vec 2 Nat
v3 = Cons 1 (Cons 2 Empty)

failing "Mismatch between: 0 and 1."
  vBad : Vec 1 Nat
  vBad = Empty

mapNaive : (a -> b) -> Vec n a -> Vec n b
mapNaive _ Empty = Empty
mapNaive f (Cons x xs) = Cons (f x) (mapNaive f xs)

-- 'mapNaive' specialized for the 'Vec 0 a' case. Observe the function needs
-- to handle only the 'Empty' case, because it is impossible to construct a
-- value of a type 'Vec 0 a' with the 'Cons' constructor!
mapNaiveEmpty : (a -> b) -> Vec 0 a -> Vec 0 b
mapNaiveEmpty _ Empty = Empty

-- 'mapNaive' specialized for the 'Vec (S n) a' case. Again, function handles
-- only the 'Cons' case, because it is impossible to construct a value of type
-- 'Vec (S n) a' with the 'Empty' constructor.
-- However, implementation is a bit uglier. Here, the 'xs' tail of the vector
-- may be 'Empty', which means recursion hit the base case.
mapNaiveCons : (a -> b) -> Vec (S n) a -> Vec (S n) b
mapNaiveCons f (Cons x xs) =
  let y := f x in
    case xs of
      Empty    => Cons y Empty
      Cons _ _ => Cons y (mapNaiveCons f xs)

failing "Mismatch between: 0 and m."
  filterBadEmpty : (a -> Bool) -> (Vec n a) -> (Vec m a)
  filterBadEmpty _ Empty = Empty

failing "Mismatch between: S ?m and m."
  filterBadCons : (a -> Bool) -> (Vec n a) -> (Vec m a)
  filterBadCons pred (Cons x xs) =
    let rest := filterBadCons pred xs in  -- `rest` is of type `Vec m a`
      if pred x then
        Cons x rest -- Wrong, since value of type `Vec (S m) a` would be returned!
      else
        rest

-- Record is a data type with a single constructor. Fields are named and
-- projections (field accessors) are automatically generated.
record LengthAwareVec (a : Type) where
  constructor MkLengthAwareVec
  len : Nat
  -- Type of 'vec' field depends on the **value** of 'len' field!
  vec : Vec len a

lav1 : LengthAwareVec Char
lav1 = MkLengthAwareVec 0 Empty

lav2 : LengthAwareVec Char
lav2 = MkLengthAwareVec 1 (Cons 'a' Empty)

failing "Mismatch between: 1 and 0."
  lavBad : LengthAwareVec Char
  lavBad = MkLengthAwareVec 0 (Cons 'a' Empty)

filterNaive : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
filterNaive _    Empty = MkLengthAwareVec Z Empty
filterNaive pred (Cons x xs) =
    let rest := filterNaive pred xs in
      if pred x then
        MkLengthAwareVec (S rest.len) (Cons x rest.vec)
      else
        rest

failing "Mismatch between: 0 and 1."
  filterNaiveBadEmptyLength : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveBadEmptyLength _ Empty = MkLengthAwareVec 1 Empty

failing "Can't solve constraint between: S (len rest) and rest .len"
  filterNaiveNoS : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveNoS pred (Cons x xs) =
      let rest := filterNaive pred xs in
        if pred x then
          MkLengthAwareVec rest.len (Cons x rest.vec) -- Forgotten (S rest.len)
        else
          rest

failing "Can't solve constraint between: rest .len and S (rest .len)"
  filterNaiveNoCons : (a -> Bool) -> (Vec n a) -> LengthAwareVec a
  filterNaiveNoCons pred (Cons x xs) =
      let rest := filterNaive pred xs in
        if pred x then
          MkLengthAwareVec (S rest.len) rest.vec -- Forgotten (Cons x rest.vec)
        else
          rest

------------
-- EXTRAS --
------------

-- To showcase how inefficient operations on unary representation of natural
-- numbers is. 'plusNatural' performs the following:
-- plusNatural 3 6 = plusNatural 2 7 = plusNatural 1 8 = plusNatural 0 9 = 9
plusNatural : Natural -> Natural -> Natural
plusNatural m n =
  case m of
    Zero => n
    Successor k => plusNatural k (Successor n)

-- We can let Idris prove the equality of 'mapNaive' applying the 'Successor'
-- function 'S'.
-- mapNaive S [1, 2] = [2, 3]
-- More on theorem proving in future articles.
mapNaiveExample : (mapNaive S (Cons 1 (Cons 2 Empty))) = (Cons 2 (Cons 3 Empty))
mapNaiveExample = Refl

-- Instead of defining a custom record, Idris has special syntax for dependent
-- pairs.
-- (Nat, String) is an ordinary type of a pair, (m : Nat ** Vec m a) is the
-- dependent pair.
-- Expressive power of dependent records and pairs is the same, I opted for the
-- former in this article.
filterNaivePair : (a -> Bool) -> (Vec n a) -> (m : Nat ** Vec m a)
filterNaivePair _    Empty = (Z ** Empty)
filterNaivePair pred (Cons x xs) =
    let (k ** rest) := filterNaivePair pred xs in
      if pred x then
        ((S k) ** (Cons x rest))
      else
        (k ** rest)

  1. Word “bundle” was chosen on purpose. There is a concept of a “fiber bundle” in topology. Without going into too much detail, a dependent sum corresponds to an element of a bundle and a dependent product to a section of the bundle.↩︎