Fixed points of indexed functors

#Introduction

I was lately thinking about fixed points, more or less.

A new version of data-fix was released recently, and also corresponding version of recursion-schemes.

Also I wrote a Fix-ing regular expressions post, about adding fixed points to regular expression.

This post is another exploration: Fixed points of Indexed functors. This is not novel idea at all, but I’m positively surprised this works out quite nicely in modern GHC Haskell. I define a IxFix type and illustrate it with three examples.

Note: The HFix in multirec package is the same as IxFix in this post. I always forget about the existence of multirec.

In the following, the "modern GHC Haskell" is quite conservative, only eight extensions:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

And this literate Haskell script is warning free, with -Wall

{-# OPTIONS_GHC -Wall #-}

On this trip

module IxFix where

we need a handful of imports

-- Type should be added to Prelude
import Data.Kind (Type)

-- Few newtypes
import Data.Functor.Identity (Identity (..))
import Data.Functor.Compose (Compose (..))
import Data.Functor.Const (Const (..))

-- dependently typed programming!
import Data.Fin      (Fin)
import Data.Type.Nat
import Data.Vec.Lazy (Vec (..))

-- magic
import Data.Coerce (coerce)

Before we go further, let me remind you about ordinary fixed points, as defined in data-fix package.

newtype Fix f = Fix { unFix :: f (Fix f) }

foldFix :: Functor f => (f a -> a) -> Fix f -> a
foldFix f = go where go = f . fmap go . unFix

Using Fix we can define recursive types using non-recursive base functors, e.g. for a list we’d have

data ListF a rec = NilF | ConsF a rec

We then use foldFix (or cata and other recursion schemes in recursion-schemes) to decouple "how we recurse" and "what we do at each step". I won’t try to convince you why this separation of concerns might be useful.

Instead I continue directly to the topic: define indexed fixed points. Why we need them? Because Fix is not powerful enough to allow working with Vec or polymorphically recursive types.

-- hello dependently typed world.
data Vec (n :: Nat) (a :: Type) where
    VNil  :: Vec 'Z a
    (:::) :: a -> Vec n a -> Vec ('S n) a

#Fixed points of indexed functors

Before talking about fixed points, we need to figure out what are indexed functors. Recall a normal functor is a thing of kind Type -> Type:

class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

Indexed version is the one with Type replaced with k -> Type, for some index k (it is still a functor, but in different category). We want morphisms to work for all indices, and preserve them. Thus we define a commonly used type alias¹

-- natural, or parametric, transformation
type f ~> g = forall (j :: k). f j -> g j

Using it we can define a Functor variant²: it looks almost the same.

class IxFunctor (f :: (k -> Type) -> (k -> Type)) where
    ixmap :: (a ~> b) -> (f a ~> f b)

With IxFunctor in our toolbox, we can define an IxFix, note how the definition is again almost the same as for unindexed Fix and foldFix:

newtype IxFix f i = IxFix { unIxFix :: f (IxFix f) i }

foldIxFix :: IxFunctor f => (f g ~> g) -> IxFix f ~> g
foldIxFix alg = alg . ixmap (foldIxFix alg) . unIxFix

Does this work? I hope that following examples will convince that IxFix is usable (at least in theory).

#Example: length indexed lists, Vec

The go to example of recursion schemes is a folding a list, The go to example of dependent types is length indexed list, often called Vec. I combine these traditions by defining Vec as an indexed fixed point:

data VecF (a :: Type) rec (n :: Nat) where
    NilF  ::               VecF a rec 'Z
    ConsF :: a -> rec n -> VecF a rec ('S n)

VecF is an IxFunctor:

instance IxFunctor (VecF a) where
    ixmap _ NilF         = NilF
    ixmap f (ConsF x xs) = ConsF x (f xs)

And we can define Vec as fixed point of VecF, with constructors:

type Vec' a n = IxFix (VecF a) n

nil :: Vec' a 'Z
nil = IxFix NilF

cons :: a -> Vec' a n -> Vec' a ('S n)
cons x xs = IxFix (ConsF x xs)

Can we actually use it? Of course! Lets define concatenation³ Vec' a n -> Vec' a m -> Vec' a (Plus n m). We cannot use foldIxFix directly, as Plus n m is not the same index as n, so we need to define an auxiliary newtype to plumb the indices. Another way to think about these kind of newtypes, is that they work around the lack of type-level anonymous functions in nowadays Haskell.

newtype Appended m a n =
    Append { getAppended :: Vec' a m -> Vec' a (Plus n m) }

append :: forall a n m. Vec' a n -> Vec' a m -> Vec' a (Plus n m)
append xs ys = getAppended (foldIxFix alg xs) ys where
    alg :: VecF a (Appended m a) j -> Appended m a j
    alg NilF          = Append id
    alg (ConsF x rec) = Append $ \zs -> cons x (getAppended rec zs)

We can also define a refold function, which doesn’t mention IxFix at all.

ixrefold :: IxFunctor f => (f b ~> b) -> (a ~> f a) -> a ~> b
ixrefold f g = f . ixmap (ixrefold f g) . g

And then, using ixrefold we can define concatenation for Vec from vec package, which isn’t defined using IxFix. Here we need auxiliary newtypes as well.

newtype Swapped f a b =
    Swap { getSwapped :: f b a }
newtype Appended2 m a n =
    Append2 { getAppended2  :: Vec m a -> Vec (Plus n m) a }

append2 :: forall a n m. Vec n a -> Vec m a -> Vec (Plus n m) a
append2 xs ys = getAppended2 (ixrefold f g (Swap xs)) ys where
    -- same as alg in 'append'
    f :: VecF a (Appended2 m a) j -> Appended2 m a j
    f NilF          = Append2 id
    f (ConsF z rec) = Append2 $ \zs -> z :::  (getAppended2 rec zs)

    -- 'project'
    g :: Swapped Vec a j -> VecF a (Swapped Vec a) j
    g (Swap VNil)       = NilF
    g (Swap (z ::: zs)) = ConsF z (Swap zs)

You may note that one can implement append as induction over length, that’s how vec implements them. Theoretically it is not right, and IxFix formulation highlights it:

append3 :: forall a n m. SNatI n
        => Vec' a n -> Vec' a m -> Vec' a (Plus n m)
append3 xs ys = getAppended3 (induction caseZ caseS) xs where
    caseZ :: Appended3 m a 'Z
    caseZ = Append3 (\_ -> ys)

    caseS :: Appended3 m a p -> Appended3 m a ('S p)
    caseS rec = Append3 $ \(IxFix (ConsF z zs)) ->
        cons z (getAppended3 rec zs)

-- Note: this is different than Appended!
newtype Appended3 m a n =
    Append3 { getAppended3 :: Vec' a n -> Vec' a (Plus n m) }

Here we pattern match on IxFix value. If we want to treat it as least fixed point, the only valid elimination is to use foldIxFix!

However, the induction over length is the right approach if Vec is defined as a data or type family:

type family VecFam (a :: Type) (n :: Nat) :: Type where
    VecFam a 'Z     = ()
    VecFam a ('S n) = (a, VecFam a n)

Whether you want to have data or type-family or GADT depends on the application. (Even in Agda or Coq). Family variant doesn’t intristically know its length, which is sometimes a blessing, sometimes a curse. For what it’s worth, vec package provides both variants, with almost the same module interface.

#Example: Polymorphically recursive type

The IxFix can also be used to define polymorphically recursive types like

data Nested a = a :<: (Nested [a]) | Epsilon
infixr 5 :<:

nested :: Nested Int
nested = 1 :<: [2,3,4] :<: [[5,6],[7],[8,9]] :<: Epsilon

A length function defined over this datatype will be polymorphically recursive, as the type of the argument changes from Nested a to Nested [a] in the recursive call:

-- >>> nestedLength nested
-- 3
nestedLength :: Nested a -> Int
nestedLength Epsilon    = 0
nestedLength (_ :<: xs) = 1 + nestedLength xs

We cannot represent Nested as Fix of some functor, and we can not use recursion-schemes either. However, we can redefine Nested as indexed fixed point.

An important observation is that we (often or always?) use polymorphic recursion as a solution to the lack indexed types. My favorite example is de Bruijn indices for well-scoped terms. Compare

data Expr1 a
    = Var1 a
    | App1 (Expr1 a) (Expr1 a)
    | Abs1 (Expr1 (Maybe a))

and

data Expr2 a n
    = Free2 a                -- split free and bound variables
    | Bound2 (Fin n)
    | App2 (Expr2 a n) (Expr2 a n)
    | Abs2 (Expr2 a ('S n))  -- extend bound context by one

Which one is simpler is a really good discussion, but for another time.

In Nested example the single argument is also used for two purposes: the type of an base element (Int) and container type (starts with Identity and increases with extra list layer).

One approach is just use Nat index and have a type family ⁴

type family Container (n :: Nat) :: Type -> Type where
    Container 'Z     = Identity
    Container ('S n) = Compose [] (Container n)

or

data NestedF a rec f
    = f a :<<: rec (Compose [] f)
    | EpsilonF

instance IxFunctor (NestedF a) where
    ixmap _ EpsilonF    = EpsilonF
    ixmap f (x :<<: xs) = x :<<: f xs

We can convert from Nested a to IxFix (NestedF a) Identity and back. We use coerce to help with newtype plumbing.

convert :: Nested a -> IxFix (NestedF a) Identity
convert = aux . coerce where
    aux :: Nested (f a) -> IxFix (NestedF a) f
    aux Epsilon    = IxFix EpsilonF
    aux (x :<: xs) = IxFix (x :<<: aux (coerce xs))

-- back left as an exercise

And then we can write nestedLength as a fold.

-- >>> nestedLength2 (convert nested)
-- 3
nestedLength2 :: IxFix (NestedF a) f -> Int
nestedLength2 = getConst . foldIxFix alg where
    alg :: NestedF a (Const Int) ~> Const Int
    alg EpsilonF         = Const 0
    alg (_ :<<: Const n) = Const (n + 1)

#Non-example: ListF

In the introduction I mentioned an ordinary list, which is a fixed point

where I use notation to represent least fixed points: . Note that we first introduce a type parameter with , and then make a fixed point with .

We can define an ordirinary list using IxFix, by taking a fixed point of a Type -> Type thing, i.e. first , and then .

data ListF1 rec a = NilF1 | ConsF1 a (rec a)
type List1 = IxFix ListF1

fromList1 :: [a] -> List1 a
fromList1 []     = IxFix NilF1
fromList1 (x:xs) = IxFix (ConsF1 x (fromList1 xs))

Compare to Agda code:

-- parameter
data List (A : Set) : Set where
    nil  : List A
    cons : A -> List A -> List A

-- index
data List : Set -> Set where
    nil :  (A : Set) -> List A
    cons : (A : Set) -> A -> List A -> List A

These types are subtly different. See https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices.

This gives a hint why Agda people define Vec (A : Set) : Nat -> Set, i.e. length as the last parameter: because you have to do that way. And Haskellers (usually) define as Vec (n :: Nat) (a :: Type), because then Vec can be given Functor etc instances. In other words, machinery in both languages forces an order of of type arguments.

Finally, we can write parametric version of List using IxFix too. We just use a dummy, boring index.

data ListF2 a rec (unused :: ()) = NilF2 | ConsF2 a (rec unused)
type List2 a = IxFix (ListF2 a) '()

fromList2 :: [a] -> List2 a
fromList2 []     = IxFix NilF2
fromList2 (x:xs) = IxFix (ConsF2 x (fromList2 xs))

IxFix is more general than Fix, but if you don’t need an extra power, maybe you shouldn’t use it.

Do we need something even more powerful than IxFix? I don’t think so. If we need more (dependent) indices, we can pack them all into a single index by tupling (or -mming) them.

#Conclusion

We have seen IxFix, fixed point of indexed functor. I honestly do not think that you should start looking in your code base whether you can use it. I suspect it is more useful as thinking and experimentation tool. It is an interesting gadget.

• 2024-06-24 – hashable arch native
• 2024-05-28 – cabal fields
• 2024-04-21 – A note about coercions
• 2024-04-18 – What makes a good compiler warning?
• 2024-04-12 – Core Inspection

twitter github email linkedin stackoverflow