18 March 2026

Bootstrapping Data Structures From Fixpoints of Containers

by Andre Videla

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

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 papers456 that should give you a comprehensive view of how descriptions and ornaments work.

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.

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.

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.

NatDataType : Type
NatDataType = Data NatDesc ()

For convenience we add special functions as constructors of the datatype.

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.

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.

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.

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.

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

  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.

  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.

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

  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.

  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.

  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 ↩

  4. 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 ↩

  5. 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 ↩

  6. 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. ↩

tags: containers - poly - idris - data structures