---
title: "Induction Principles from Base Functors"
date: 2022-04-22T12:19:22-07:00
expirydate: 2022-04-22T12:19:22-07:00
tags: ["Idris"]
draft: true
---
In the [Haskell catamorphisms article]({{< relref "haskell_catamorphisms" >}}), we looked
at how base functors and functions of the type `F a -> a` can be used to
derive "fold" functions on inductive data types. This formulation allows for
one more interesting trick, one that I found to be extremely interesting and
worth covering. However, this trick requires a more powerful type system
than Haskell provides us; it requires depdendent types.

This article assumes a working knowledge of dependent types. I will not
spend time explaining dependent types, nor the syntax for them in Idris,
which is the language I'll use in this article. Below are a few resources
that should help you get up to speed.

{{< todo >}}List resources{{< /todo >}}

We've seen that, given a function `F a -> a`, we can define a function
`B -> a`, if `F` is a base functor of the type `B`. However, what if
the goal is to define a function in which the return type `a` depends
on the value of `B`? In other words, what if we want to define a function
with type:
```Idris
someFunction : (b : B) -> P b
```
How might we achieve such a thing? Unlike the generic type `a`, we can't
simply place `P` into the base functor `F`; the following is completely
invalid.
```Idris
-- Completely bogus
argType : Type
argType = F P -> P
```
In our case, `P` is a type family, rather than a type; in order to use it as
a parameter to the base functor, we need to feed it an argument (of type `B`).
Well, we've already seen one way to get a value `b` of type `B` at the type
level: we can use a dependent function. This too is not correct, but it does get us a little bit closer to the goal.
```Idris
-- Still bogus
argType : Type
argType = (b : B) -> F (P b) -> P b
```
Recall that the base functor `F` effectively denotes a single layer of a data
structure, with recursive