From 1a6f5e061bf86d692e1a0fba50369014a79e5533 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 29 Jan 2023 21:00:22 -0800
Subject: [PATCH] Add a very rough draft of the idris catemorphisms article I
 found lying around

---
 content/blog/idris_catamorphisms.md | 47 +++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 content/blog/idris_catamorphisms.md

diff --git a/content/blog/idris_catamorphisms.md b/content/blog/idris_catamorphisms.md
new file mode 100644
index 0000000..6298228
--- /dev/null
+++ b/content/blog/idris_catamorphisms.md
@@ -0,0 +1,47 @@
+---
+title: "Induction Principles from Base Functors"
+date: 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