blog-static/content/blog/idris_catamorphisms.md

title	date	expirydate	tags	draft
Induction Principles from Base Functors	2022-04-22T12:19:22-07:00	2022-04-22T12:19:22-07:00	Idris	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:

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.

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

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