Maths - Recursive Types

• Algebraic data type is least fixed point of a functor.

• Least fixed points are closely related to free algebras (site here).

Idris definition of an F-algebra

f is now lower case due to programming conventions.

interface Algebra f a = f a -> a

In most languages we can construct lists, for example here is a list of integers:

Idris> [1,2]
[1, 2] : List Integer

We can also nest lists, here is a list of lists of integers:

Idris> [[1,2],[3,4]]
[[1, 2], [3, 4]] : List (List Integer)

Sometimes we may need to have different depths in different parts of the list. This can be a problem as in this case:

Idris> [[1,2],3]
List Integer is not a numeric type

endofunction

example

int -> int 

Functions from a type to an element of the same type (endofunctions) can have fixpoints.

More information about fixpoints on this page.

endofunctor

example

 Expr ->Expr

Inductivly Defined Type

data Expr = Constant Nat
          | Var String
          | Add Expr Expr
          | Mul Expr Expr

These examples show the action of an endofunction 'f' on some set. For example 'f' sends 'A' to 'C', 'C' to 'D' and 'D' to itself.

So 'D' is a fixpoint.

So, this would be the signature of such a function:

ffix : (a -> a) -> a

Here is an implementation:

It looks like this function would try to construct an infinite sequence of function calls
f (f (f (f (f ...))))
and we would expect the program to run out of memory and crash.

ffix : (a -> a) -> a
ffix f {a} = x
  where
    x : a
    x = f x

However, if the language can support lazy (as opposed to eager) types then, when the parameter is not used, the function will terminate.

*fixPoint> ffix (const 3)
3 : Integer

In this example we give it 'Id' which we would expect to cause an infinite loop. With this Idris example, it sometimes seems to detect this and to go into lazy mode:

*fixPoint> ffix Id
Fix.ffix, x Type Id : Type

and this is also lazy. If returns a function instead of trying to evaluate an infinite loop.

*fixPoint> ffix (+2)
prim__addBigInt
         (Fix.ffix, x Integer (
            \ARG => prim__addBigInt ARG 2))
                2 : Integer

Applies to a partially defined function.

Lower means less well defined and higher means more defined.

Fix f = f (Fix f)

In Haskell library it is defined like this:

Both type name and constuctor are called Fix

In Idris we need to make it lazy.

||| Fix only has one constructor
||| (newtype in Haskell)
||| this is a recursive definition
data Fix f = Fix (f (Fix f))

data Fix f = Fix (f (Fix f))

ffix : (a -> a) -> a
ffix f {a} = x
  where
    x : a
    x = f x

module Main

fix : (|(x: a) -> a) -> a
fix f = x
  where
    x = f (lazy x)

foo : |(x: Int -> Int) -> Int -> Int
foo _ 0 = 0
foo f n = f (n - 1)

main : IO
main = print ((fix foo) 12)

When using Idris how can we ensure that the base functor of the datatype is strictly positive? Strictly positive functors can be represent by defining a universe or by containers.

-- A universe of positive functor
data Desc : Type where
  ||| sigma type
  Sig : (a : Type) -> (a -> Desc) -> Desc
  ||| a (strictly-positive) position for a recursive substructure
  Rec : Desc -> Desc
  ||| nothing
  End : Desc


-- The decoding as a Type -> Type function
desc : Desc -> Type -> Type
desc (Sig a d) x = (v : a ** desc (d v) x)
desc (Rec d)   x = (x, desc d x)
desc End       x = ()

From this universe of functors, which are guaranteed to be strictly positive, we can take their least fixpoint:

-- The least fixpoint of such a positive functor
data Mu : Desc -> Type where
  In : desc d (Mu d) -> Mu d

Start with a sum type.

data NatC = ZERO | SUCC

We then define the strictly positive base functor by storing the constructor tag in a sigma and computing the rest of the description based on the tag value. The ZERO tag is associated to End (there is nothing else to store in a zero constructor) whilst the SUCC one requires a Rec End, that is to say one recursive substructure corresponding to the Nat's predecessor.

natD : Desc
natD = Sig NatC $ \ c => case c of
  ZERO => End
  SUCC => Rec End

Inductive type by taking the fixpoint of the description:

nat : Type
nat = Mu natD

Recover the constructors:

zero : nat
zero = In (ZERO ** ())

succ : nat -> nat
succ n = In (SUCC ** (n, ()))

This specific universe is taken from 'Ornamental Algebras, Algebraic Ornaments' by McBride but you can find more details in 'The Gentle Art of Levitation' by Chapman, Dagand, McBride, and Morris.

Monoid

data MonF a = MEmpty | MAppend a a 

Ring

data RingF a = RZero | ROne | RNeg a | RAdd a a | Rmull a a 

Monoid

data MonExpr = MEmpty | MAppend Expr Expr 

Ring

data RingExpr = RZero | ROne | RNeg RingExpr | 
	          RAdd RingExpr RingExpr | Rmull RingExpr RingExpr