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