# 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 equivalent_[^2]. 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 list*[^1]. 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. ## 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. - Containers & their fixpoints ```idris record Container where constructor (!>) shape : Type position : shape -> Type Fix : (Container -> Container) -> Container Fix f = (fw : FixFw f) !> FixBw f fw ``` Fixpoints are particularly subtle and in we plan to publish a future post dedicated to them. For now we are going to assume they exist and explore what we can do with them. - Coproducts ```idris (+) : Container -> Container -> Container (+) c1 c2 = (x : Either c1.shape c2.shape) !> either (c1.position) (c2.position) x ``` - Cartesian product ```idris (*) : Container -> Container -> Container (*) c1 c2 = (x : Pair c1.shape c2.shape) !> Either (c1.position (fst x)) (c2.position (snd x)) -- Neutral for catesian product One : Container One = (_: Unit) !> Void ``` - Tensor product ```idris -- read "parallel" (//) : Container -> Container -> Container (//) c1 c2 = (x : Pair c1.shape c2.shape) !> Pair (c1.position (fst x)) (c2.position (snd x)) -- neutral for tensor I : Container I = (_: Unit) !> Unit ``` Finally, we need to define the extension of containers that lift containers into endofunctors in $Set$. ```idris 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$. ```idris 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`. ```idris 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 ```idris 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. ```idris 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 ```idris 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: ```idris 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: ```idris 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. ```idris 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: ```idris 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 ```idris 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 ```idris 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! ```idris 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 `Nat`[^3], 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: - What's the relationship between fixpoints in containers and the extension? - We got a functor in container for `List/Any` but can we get the pair `List/All`? We can it's `I + a ⊗ _`! What else can we get? - There are other ways to achieve the same thing with container, what's wrong with them? 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]: 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. [^2]: 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](https://www.semanticscholar.org/paper/The-Derivative-of-a-Regular-Type-is-its-Type-of-McBride/4286bcc299ab34b0581cbd62d6241794fc9052de) [^3]: We did but through a fixpoint in containers not in Set [^desc]: J. Chapman, P.-É. Dagand, C. McBride, and P. Morris, ‘The gentle art of levitation’. Association for Computing Machinery, Sep. 27, 2010. Accessed: Sep. 18, 2020. [Online]. Available: https://doi.org/10.1145/1932681.1863547 [^orn]: C. McBride, ‘Ornamental Algebras, Algebraic Ornaments’, 2014. Accessed: Mar. 22, 2023. [Online]. Available: https://www.semanticscholar.org/paper/Ornamental-Algebras%2C-Algebraic-Ornaments-McBride/e16519d681e959d3919c4c256a5cd36853075697 [^across]: P.-E. Dagand and C. McBride, ‘Transporting functions across ornaments’, SIGPLAN Not., vol. 47, no. 9, pp. 103–114, Oct. 2012, doi: 10.1145/2398856.2364544.