18 March 2026

Bootstrapping Data Structures

by Andre Videla

Bootstrapping Data Structures from Almost Nothing

A lot of our research at Glaive relies on the theory around Containers & Lenses. But before we used them for theorem proving, they were used for data structures, providing insight into catamorphisms, folds, initial algebras, interface derivation, and more. One of the most striking examples of containers for data types are the fact that the derivative of a container is its one-holed context equivalent1. That is to say, you can take the derivative (in the algebraic sense, like $\delta(x^2) = 2x$) of a type like List and obtain pointers in a list2.

In this post, we will show we we can generate common algebraic data types from nothing but basic properties on containers. What’s more we are also going to define common indexed data structures that carry valuable information in the types.

This blog post is also Idris 2 literate file that you can run and inspect you can find the raw version of it here.

Our Foundation

We rely on the category of containers to provide everything we need. In particular, we need fixpoints and a couple of monoidal products.

Finally, we need to define the extension of containers that lift containers into endofunctors in $Set$.

Ex : Container -> Type -> Type
Ex c ty = DPair c.shape (\b => c.position b -> ty)

Equipped with this, we’re ready to bootstrap all the types we usually use in programming, and even some dependent types! Let’s start simple, with Maybe and List.

Defining Maybe and List the Usual Way

We start by showing how we traditionally use containers to define data structures, using the extension. One of the most basic types to define is Maybe, a type that either wraps a value, or returns an empty value:

-- The default Maybe type
data Maybe a = Nothing | Just a

The Maybe container is given by taking the coproduct of 1 and I, and its extension gives us the maybe functor in $Set$.

MaybeType : Type -> Type
MaybeType = Ex (One + I)
`MaybeType ~ Maybe` isomorphism ```idris %unbound_implicits off parameters {0 a : Type} toMaybeType : Maybe a -> MaybeType a toMaybeType Nothing = MkDPair (Left ()) absurd toMaybeType (Just x) = MkDPair (Right ()) (const x) fromMaybeType : MaybeType a -> Maybe a fromMaybeType (Left x ** snd) = Nothing fromMaybeType (Right x ** snd) = Just (snd ()) fromToMaybeType : (x : Maybe a) -> (fromMaybeType . toMaybeType) x === x fromToMaybeType Nothing = Refl fromToMaybeType (Just x) = Refl toFromMaybeType : (x : MaybeType a) -> (toMaybeType . fromMaybeType) x === x toFromMaybeType ((Left () ** snd)) = cong (MkDPair (Left ())) (funExt $ \x => absurd x) toFromMaybeType ((Right () ** snd)) = cong (MkDPair (Right ())) (funExt $ \() => Refl) %unbound_implicits on ```

We can take this idea further and generate complex inductive types like List by taking the extension of the container Nat !> Fin.

ListEx : Type -> Type
ListEx = Ex ((n : Nat) !> Fin n)
`ListEx ~ List` isomorphism ```idris %unbound_implicits off parameters {0 a : Type} toListEx : List a -> ListEx a toListEx [] = (Z ** absurd) toListEx (x :: xs) = let rest : ListEx a rest = toListEx xs in (S rest.fst ** (\case FZ => x FS n => rest.snd n)) fromListEx : ListEx a -> List a fromListEx (0 ** snd) = [] fromListEx ((S k) ** snd) = snd FZ :: fromListEx (k ** snd . FS) fromToListEx : (x : List a) -> (fromListEx . toListEx) x === x fromToListEx [] = Refl fromToListEx (x :: xs) = cong (x ::) (trans (cong fromListEx sigmaEta) (fromToListEx xs)) toFromListEx : (x : ListEx a) -> (toListEx . fromListEx) x === x toFromListEx ((0 ** snd)) = cong (MkDPair Z) (funExt $ \x => absurd x) toFromListEx (((S k) ** snd)) with (toFromListEx (k ** snd . FS)) _ | rr = rewrite rr in cong (MkDPair (S k)) $ funExt $ \case FZ => Refl ; FS n => rewrite rr in Refl %unbound_implicits on ```

However, this feels strange. It’s not surprising that we can define inductive types if we already have access to Nat. And where does Fin come from? isn’t it cheating that to define List we need to already have access to indexed types and inductive types?

We can do better. Instead of relying on Nat, or its definition as a fixpoint in $Set$, we are going to be working purely in $Cont$, the category of containers, and only drop down into $Set$ whenever we want to extract the types to use in our programs. As we will see, this approach will also allow us to derive indexed types in addition to plain types or functors.

Defining Nat in $Cont$

We know that the type Nat can be derived from the fixpoint of the 1 + _ functor in $Set$. Does this hold true for containers as well? Let’s try

NatFix : Container
NatFix = Fix (One +)

This is now a container with shapes and positions, but unlike maybe, we do not want to generate a functor, we want a plain Type. It happens that if you project out the shape of this container, you obtain the Nat type.

NatTy : Type
NatTy = NatFix .shape
`NatTy ~ Nat` Isomorphism ```idris %unbound_implicits off toNatTy : Nat -> NatTy toNatTy 0 = MkFixFw (Left ()) toNatTy (S k) = MkFixFw (Right (toNatTy k)) fromNatTy : NatTy -> Nat fromNatTy (MkFixFw (Left x)) = 0 fromNatTy (MkFixFw (Right x)) = S (fromNatTy x) fromToNatTy : (x : Nat) -> (fromNatTy . toNatTy) x === x fromToNatTy 0 = Refl fromToNatTy (S k) = cong S (fromToNatTy k) toFromNatTy : (x : NatTy) -> (toNatTy . fromNatTy) x === x toFromNatTy (MkFixFw (Left ())) = Refl toFromNatTy (MkFixFw (Right x)) = cong (MkFixFw . Right) (toFromNatTy x) %unbound_implicits on ```

This works because the fixpoint in $Cont$ secretly implements a fixpoint in $Set$ in the shapes!

A curious fact about this construction is that the position projection is empty

NatPosEmpty : NatTy -> Type
NatPosEmpty = NatFix .position

natPosEmpty : {n : _} -> NatPosEmpty n -> Void
natPosEmpty {n = MkFixFw (Left x)} (y) = y
natPosEmpty {n = MkFixFw (Right x)} (y) = natPosEmpty {n = x} y

That looks strange at first but there is a very clear explanation. If we write down the values of Fix (1 + _) we get 1 + (1 + (1 + ...)), and if we expand the definition of 1 as a container, we see that the position of the container is never inhabited (1, 0) + ((1, 0) + ((1 + 0) + ...)), and therefore, taking the position if such a container is equivalent of asking “what are the inhabitants of 0 + 0 + 0 + ...”, there is no inhabitant for this term.

So we defined Nat but without Fin we cannot define List from first principles, is there another way to define List without passing through the (Nat !> Fin) container?

Generating List in $Cont$

In $Set$ the type List is obtained by taking the fixpoint of the functor ` 1 + a * _), where a` represents the type of values in the list. We are going to use the same functor and fixpoint but in the category of containers:

ListF : Container -> Container
ListF a = Fix (\x => One + a * x)

This is now a functor in the category of containers, it’s type is Container -> Container. Addionally, we can turn it back into a functor in $Set$ by giving in argument a container with empty positions, and extract its shapes. This way we obtain the list functor again:

ListType : Type -> Type
ListType a = (ListF ((_: a) !> Void)).shape
Show `ListType ~ List` Isomorphism ```idris %unbound_implicits off parameters {0 a : Type} toListType : List a -> ListType a toListType [] = MkFixFw (Left ()) toListType (x :: xs) = let rest : ListType a rest = toListType xs in MkFixFw (Right (x, rest)) fromListType : ListType a -> List a fromListType (MkFixFw (Left x)) = [] fromListType (MkFixFw (Right x)) = fst x :: fromListType (snd x) fromToListType : (x : List a) -> (fromListType . toListType) x === x fromToListType [] = Refl fromToListType (x :: xs) = cong (x ::) (fromToListType xs) toFromListType : (x : ListType a) -> (toListType . fromListType) x === x toFromListType (MkFixFw (Left ())) = Refl toFromListType (MkFixFw (Right x)) = toFromListType (MkFixFw (Right x)) %unbound_implicits on ```

Thanks to fixpoints in containers we completely skipped the need to define Nat and Fin and obtained the List functor in $Set$ anyways. But now that we have access to a container we can also ask “what happens if we project out the positions”?

Well at first it seems not much happens.

ListEmptyPos : (a : Type) -> ListType a -> Type
ListEmptyPos a = (ListF ((_: a) !> Void)) .position

listEmptyPos : (a : Type) -> (ls : ListType a) -> ListEmptyPos a ls -> Void
listEmptyPos a (MkFixFw (Left y)) x = absurd x
listEmptyPos a (MkFixFw (Right y)) (Left x) = absurd x
listEmptyPos a (MkFixFw (Right (_, y))) (Right x) = listEmptyPos a y x

This seems disappointing, are we back in the same situation as with Nat where the positions are always empty?

With careful squinting we see that this pain is purely self-inflicted. When we defined the List functor, we were not interested in the positions so we picked empty positions. But if we pick a non-trivial position we get a much more interesting type:

ListAny : (a : Type) -> (p : a -> Type) -> (ListF ((x : a) !> p x)).shape -> Type
ListAny a p = (ListF ((x : a) !> p x)).position

This gives us the type of predicates at a certain position in a given list. People familiar with the Data.List.Quantifiers module will recognise this type as being the Any predicate on List.

`ListAny ~ Any` Isomorphism ```idris %unbound_implicits off parameters {0 a : Type} {0 a' : a -> Type} 0 ListBase : Type ListBase = (ListF ((x : a) !> a' x)).shape 0 ListPos : ListBase -> Type ListPos = (ListF ((x : a) !> a' x)).position toListBase : List a -> ListBase toListBase [] = MkFixFw (Left ()) toListBase (x :: xs) = let rest : ListBase rest = toListBase xs in MkFixFw (Right (x, rest)) fromListBase : ListBase -> List a fromListBase (MkFixFw (Left x)) = [] fromListBase (MkFixFw (Right x)) = fst x :: fromListBase (snd x) fromToListBase : (x : List a) -> (fromListBase . toListBase) x === x fromToListBase [] = Refl fromToListBase (x :: xs) = cong (x ::) (fromToListBase xs) toFromListBase : (x : ListBase) -> (toListBase . fromListBase) x === x toFromListBase (MkFixFw (Left ())) = Refl toFromListBase (MkFixFw (Right x)) = toFromListBase (MkFixFw (Right x)) toListPos : (ls : List a) -> Any a' ls -> ListPos (toListBase ls) toListPos [] (Here x) impossible toListPos [] (There x) impossible toListPos (y :: xs) (Here x) = Left x toListPos (y :: xs) (There x) = Right (toListPos xs x) fromListPos : (ls : List a) -> ListPos (toListBase ls) -> Any a' ls fromListPos [] x = absurd x fromListPos (y :: xs) (Left x) = Here x fromListPos (y :: xs) (Right x) = There (fromListPos xs x) fromToListPos : (ls : List a) -> (xs : Any a' ls) -> (fromListPos ls . toListPos ls) xs === xs fromToListPos [] xs = absurd xs fromToListPos (x :: ys) (Here y) = Refl fromToListPos (x :: ys) (There y) = cong There (fromToListPos ys y) toFromListPos : (ls : List a) -> (xs : ListPos (toListBase ls)) -> (toListPos ls . fromListPos ls) xs === xs toFromListPos [] xs = absurd xs toFromListPos (x :: ys) (Left y) = Refl toFromListPos (x :: ys) (Right y) = cong Right (toFromListPos ys y) %unbound_implicits on ```

What is more, this type is very close to the Fin type! In essence, the Fin type is nothing but a trivial predicate for a list filled with unit values.

∀ xs : List (). Fin (length xs) ~ Any (const ()) (length xs)

Additionally, this is also using the fact that Nat is isomorphic to List (), could it be that his idea works for containers too?

Deriving Nat and Fin at the Same Time

Now that we have lists as a functor in the category of containers, we can use our Nat intuition in the land of containers. Here is what we get

NatCont : Container
NatCont = ListF I

This is defining a container by applying our list functor to the I container, if we apply what we learned for lists, the base of this container should return the type of natural numbers

NatType : Type
NatType = NatCont .shape

This is the same as taking the ListType from above and applying it to (), and as a result this type is isomorphic to ListType () which is isomorphic to Nat.

`NatType ~ Nat` isomorphism ```idris %unbound_implicits off toNatType : Nat -> NatType toNatType 0 = MkFixFw (Left ()) toNatType (S k) = MkFixFw (Right ((), toNatType k)) fromNatType : NatType -> Nat fromNatType (MkFixFw (Left x)) = 0 fromNatType (MkFixFw (Right x)) = (S (fromNatType (snd x))) fromToNatType : (x : Nat) -> (fromNatType . toNatType) x === x fromToNatType 0 = Refl fromToNatType (S k) = cong S (fromToNatType k) toFromNatType : (x : NatType) -> (toNatType . fromNatType) x === x toFromNatType (MkFixFw (Left ())) = Refl toFromNatType (MkFixFw (Right ((), x))) = cong (MkFixFw . Right . MkPair ()) (toFromNatType x) %unbound_implicits on ```

But the magic happens when we take the positions of this container, we finally get our coveted Fin type!

FinType : NatType -> Type
FinType = NatCont .position
`FinType ~ Fin` isomorphism ```idris %unbound_implicits off toFinType : (n : Nat) -> Fin n -> FinType (toNatType n) toFinType 0 x = absurd x toFinType (S k) FZ = Left () toFinType (S k) (FS x) = Right (toFinType k x) fromFinType : (n : Nat) -> FinType (toNatType n) -> Fin n fromFinType 0 x = absurd x fromFinType (S k) (Left x) = FZ fromFinType (S k) (Right x) = FS (fromFinType k x) fromToFinType : (n : Nat) -> (x : Fin n) -> (fromFinType n . toFinType n) x === x fromToFinType 0 x = absurd x fromToFinType (S k) FZ = Refl fromToFinType (S k) (FS x) = cong FS (fromToFinType k x) toFromFinType : (n : Nat) -> (x : FinType (toNatType n)) -> (toFinType n . fromFinType n) x === x toFromFinType 0 x = absurd x toFromFinType (S k) (Left ()) = Refl toFromFinType (S k) (Right x) = cong Right (toFromFinType k x) %unbound_implicits on ```

What an interesting path we took to arrive here. We defined Fin without using indexed containers, without induction on Nat3, or any additional technology besides the category of containers. One fascinating outcome from this result is that the functor we need to iterate to obtain Nat and Fin is 1 + (I * _) which we wouldn’t have known without our detour through the List functor.

As any good result, it raises just as many questions as it answered:

We’ve been going for long enough, so we will leave the answer to those questions for a future publication. However, for our curious readers, we have two bonus sections showing how to get Nat and Fin using ornaments and indexed containers. I hope you enjoy.

Nat and Fin via descritpions and ornaments ## Generating `Nat` and `Fin` from Ornaments One of the best tool to leverage containers as data descriptors is the description/ornament pair of concepts. A description is a nicer syntax for a container that give direct control over what constructors and how the data is laid out for each of them. ```idris data Desc : (i : Type) -> Type where Say : i -> Desc i Sig : (s : Type) -> (d : s -> Desc i) -> Desc i Ask : i -> Desc i -> Desc i Interp : Desc i -> (i -> Type) -> i -> Type Interp (Say x) f y = x === y Interp (Sig s d) f y = DPair s $ \s' => Interp (d s') f y Interp (Ask x z) f y = DPair (f x) (\_ => Interp z f y) ``` We're not going to explain exactly how it works because it's not the goal of this post, but we are going to refer to three papers[^desc][^orn][^across] that should give you a comprehensive view of how descriptions and ornaments work. ```idris data Inverse : {i, j : Type} -> (j -> i) -> i -> Type where Ok : (jval : j) -> Inverse m (m jval) namespace Ornaments public export data Orn : (j : Type) -> (j -> i) -> Desc i -> Type where Say : Inverse e i -> Orn j e (Say i) Sig : (s : Type) -> {d : s -> Desc i} -> ((sv : s) -> Orn j e (d sv)) -> Orn j e (Sig s d) Ask : Inverse e i -> Orn j e d -> Orn j e (Ask i d) Del : (s : Type) -> (s -> Orn j e d) -> Orn j e d extractDesc : {0 d : Desc i} -> Orn j f d -> Desc j extractDesc {d = .(Say _)} (Say (Ok x)) = Say x extractDesc {d = .(Sig s d)} (Sig s g) = Sig s (\xs => extractDesc (g xs)) extractDesc {d = .(Ask _ d)} (Ask (Ok x) y) = Ask x (extractDesc y) extractDesc {d = d} (Del s g) = Sig s (\xs => extractDesc (g xs)) ``` What's important to understand from the above is that ornaments modify a description and we can extract that modified description from an ornaments. It remains to create data types from our descriptions and we can start building the type of natural numbers. ```idris data Data : Desc i -> i -> Type where Val : Interp d (Data d) iv -> Data d iv ``` Natural numbers are characterised by two constructors `Z` for "zero" and `S` for "successor". For each of those constructor, the values held are unit and another nat, respectively. ```idris NatDesc : Desc () NatDesc = Sig (#["Z", "S"]) $ \case "Z" => Say () "S" => Ask () (Say ()) ``` The above makes use of _tags_ in idris, lists of singleton strings with a nice pattern-matching syntax. First we declare the constructors as a list of tags `#["Z", "S"]` and then, for each tag, we provide descriptions for the values associated with the tag. Obtaining the `Nat` type is done via the `Data` type which maps a description into a type in Idris. ```idris NatDataType : Type NatDataType = Data NatDesc () ``` For convenience we add special functions as constructors of the datatype. ```idris Z : NatDataType Z = Val ("Z" ** Refl) S : NatDataType -> NatDataType S n = Val ("S" ** n ** Refl) fromNat : Nat -> NatDataType fromNat 0 = Z fromNat (S k) = S (fromNat k) toNat : NatDataType -> Nat toNat (Val ((("Z") ** snd))) = Z toNat (Val ((("S") ** snd))) = S (toNat snd.fst) ``` Equipped with natural numbers, we can _adorn_ them with an index, which happens to be the `Nat` type itself emerging from the description. The ornament will modify each constructor to say that in the case of `Z`, our index is a successor, and the value is a unit. And for the successor case `S` the index is also a successor, but we hold a recursive value as data. ```idris FinOrnament : Orn (Data NatDesc ()) (const ()) NatDesc FinOrnament = Sig (#["Z", "S"]) $ \case "Z" => Del NatDataType (\xn => Say (Ok (S xn))) "S" => Del NatDataType (\xn => Ask (Ok xn) (Say (Ok (S xn)))) ``` We can extract the indexed description from this ornament, and then use `Data` to derive the `Fin` type. ```idris FinDesc : Desc NatDataType FinDesc = extractDesc FinOrnament public export FinDataType : NatDataType -> Type FinDataType = Data FinDesc ``` We also build constructors for the Fin Type and we can ensure they are in isomorphism with the built-in `Fin` type. ```idris public export FZ : (n : NatDataType) -> FinDataType (S n) FZ n = Val ("Z" ** n ** Refl) public export FS : (n : NatDataType) -> FinDataType n -> FinDataType (S n) FS n fn = Val ("S" ** n ** fn ** Refl) fromFin : {n : _} -> Fin n -> FinDataType (fromNat n) fromFin {n = 0} x = absurd x fromFin {n = (S k)} FZ = FZ (fromNat k) fromFin {n = (S k)} (FS x) = FS (fromNat k) (fromFin x) toFin : {n : _} -> FinDataType (fromNat n) -> Fin (n) toFin {n = 0} (Val ("Z" ** x2)) with (valEta x2.snd) _ | _ impossible toFin {n = 0} (Val ("S" ** x2)) with (valEta x2.snd.snd) _ | _ impossible toFin {n = (S k)} (Val (("Z" ** snd))) = FZ toFin {n = (S k)} (Val (("S" ** snd))) = FS (toFin $ let ss = snd.snd in ?aiso) ``` This is quite nice, we managed to define both `Fin` and `Nat` from the same description, what's more `Fin` is an ornament of `Nat` using itself as its index which is a very pleasing fact about `Fin`. The main drawback of this approach is that descriptions and ornaments create a gap away from containers that is hard to reconcilliate without advanced knowledge in the topic. Ideally, we would like to make obvious that we are using containers, rather than using an encoding.
Nat and Fin via indexed containers ## Nat and Fin via indexed containers Yet another way to define Nat and Fin is via indexed containers. Indexed containers generalise containrs by giving indexing them by a type, and asking to implement a _reindexing_ function that will produce a new index given a shape/position pair at a previous index. ```idris namespace IxCont record IxCont (i : Type) where constructor MkIxCont s : i -> Type p : (j : i) -> s j -> Type r : (j : i) -> (sh : s j) -> p j sh -> i ``` Just like regular containers, indexed containers have a extension, except instead of mapping containers to a functor in set, it maps between indexed types, so it's a map `(i -> Type) -> (i -> Type)`. ```idris record Ext (cont : IxCont i) (f : i -> Type) (j : i) where constructor MkIEx exShape : cont.s j exPos : (pos : cont.p j exShape) -> f (cont.r j exShape pos) ``` Finally, indexed containers also admit a notion of W-type such that we can extract an indexed type `i -> Type` by taking a fixpoint. ```idris data W : (cont : IxCont i) -> i -> Type where MkW : {j : i} -> (sh : cont.s j) -> ((pos : cont.p j sh) -> W cont (cont.r j sh pos)) -> W cont j ``` With this we can define the container for natural numbers, this is in fact the same data as non-indexed containers because we chose to ignore the index. ```idris NatCont : IxCont () NatCont = MkIxCont (const Bool) (\_, b => if b then Unit else Void) (\_, _, _ => ()) ``` Like before, we can take its W-type and obtain the type of natural numbers in $Set$. ```idris IxNat : Type IxNat = W NatCont () IxZ : IxNat IxZ = MkW False absurd IxS : IxNat -> IxNat IxS x = MkW True (const x) IxNatToNat : IxNat -> Nat IxNatToNat (MkW False f) = Z IxNatToNat (MkW True f) = S (IxNatToNat (f ())) NatToIxNat : Nat -> IxNat NatToIxNat 0 = IxZ NatToIxNat (S k) = IxS (NatToIxNat k) ``` Using the definition of Nat we can build the type `Fin` as a container indxed by `IxNat`. ```idris FinCont : IxCont IxNat FinCont = MkIxCont (\case (MkW False _) => Void ; _ => Bool) -- 1 (\case (MkW False _) => absurd -- 2 ; (MkW True _) => \case False => Void ; True => Unit) (\case (MkW False _) => \x => absurd x -- 3 (MkW True n) => \case False => absurd True => const (n ())) ``` This definition is quite a bit more complex so we're going to explain it carefully. 1. First we define the shapes, those are indexed by `IxNat`, the shapes are going to define the number of constructors for each value of the index. When the index is `0` there are no constructors, hence the use of `Void` for the `MkW False` branch `(MkW False _) => Void`. Whenever the index is greater than 1, we have a choice of two constructor, indicated by the type `Bool` for the catch-all case `_ => Bool`. 2. Then we define the values for each constructor and each index. - For the case where the index is zero, there are no values so we don't need to think about them, this is `(MkW False _) => absurd`. - When the index is greater than one, we have two constrcutors - The first one contains no values and so the we return `Void`: `False => Void`. - For the second constructor we have one recusive constructor and that's indicated by the use of `Unit` in `True => Unit`. 3. Finally we need to explain how the index changes for each pair of constructor and values. - When the index is zero we aren't changing the index because we don't even have a constructor to work with, that's the first case `(MkW False _) => \x => absurd x`. - When the index is greater than zero we have to explain how the index change for each constructor - For the zero case, there are no further values so we can ignore the index, that's given by `False => absurd` - For the successor case we return the index of the nested value indicating that the argument to `FS` has index `n` when its own index is `S n`. This was a bit complicated but are necessary steps to properly encode the values and constructors that characterise the `Fin` type. We can reap the benefits of our effort once we define `FinTy` as the indexed W-type of the contained `FinCont`. ```idris FinTy : IxNat -> Type FinTy = W FinCont FZero : {n : IxNat} -> FinTy (IxS n) FZero = MkW False (\x => absurd x) FSucc : {n : IxNat} -> FinTy n -> FinTy (IxS n) FSucc m = MkW True (\_ => m) ``` And we can even check that it's isomorphic to our builtin `Fin` type. ``` fromFin : (n : IxNat) -> Fin (IxNatToNat n) -> FinTy n fromFin (MkW False _) x = absurd x fromFin (MkW True k) FZ = MkW False (\x => absurd x) fromFin (MkW True k) (FS x) = let ff = fromFin (k ()) x in MkW True (const ff) toFin : (n : Nat) -> FinTy (NatToIxNat n) -> Fin n toFin 0 (MkW sh f) = absurd sh toFin (S k) (MkW False f) = FZ toFin (S k) (MkW True f) = FS (toFin k (f ())) ``` This approach works fine but my personal opinion is that it comes with two big drawbacks. The first is that the indexed container is quite big and powerful which make the whole operation feel very overkill. It also moves the semantics of containers away from endofunctors in $Set$ and into endofunctors of the slice category $Set/i$ which is not always the category we want to work in.


  1. C. McBride, ‘The Derivative of a Regular Type is its Type of One-Hole Contexts’, 2001. Accessed: Oct. 17, 2023. [Online]. Available: https://www.semanticscholar.org/paper/The-Derivative-of-a-Regular-Type-is-its-Type-of-McBride/4286bcc299ab34b0581cbd62d6241794fc9052de ↩

  2. Concretely, the derivative of the List type is pairs of lists (List, List) carrying the information of the elements before the current position, and the elements after the current position. ↩

  3. We did but through a fixpoint in containers not in Set ↩

tags: containers - poly - idris - data structures