Quotes



Inductively and Coinductively Defined Types
Inductive types  coinductive types  

Least Fixpoint or initial solution of isomorphism equations.  Greatest Fixpoint or final solution of isomorphism equations.  
Elements may be obtained by a finite composition of its introductory forms.  Elements behave properly in response to a finite composition of elimination forms.  
Recursor  Generator  
Catamorphism  Anamorphism  
An Falgebra is a triple consisting of:
 endofunctor F
 object a (carrier or underlying object)
 morphism F a > a (evaluation function or the structure map)
where F forms expressions and the morphism as evaluates them.
Idris definition of an Falgebra f is now lower case due to programming conventions. 
interface Algebra f a = f a > a 
Algebra for a Functor
An algebra for a functor F is a pair <X, α>
where
 X is a type
 α : F X>X
Example of Lists
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 
What we need is a type where adding an inner type does not change the overall type, like this:
MyList ( MyList x) = MyList x
Where = means 'is the same type as'
This can easily be done with recursive types. We can analyse this by using the concept of a 'fixpoint'.
Fixpoints
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 
We can also have fixpoints between more complicated types.  
Inductivly Defined Type data Expr = Constant Nat  Var String  Add Expr Expr  Mul Expr Expr 
Inductivly defined types can also have fixpoints. 
We have an endofunctor Expr which takes a type and gives us an expression over that type.
We can have an expression over some base:
Expr Base
and we can have an expression over that and so on:
 Base
 Expr Base
 Expr Expr Base
 Expr Expr ExprBase
 ...
The fixpoint is where Expr x = x
Example of Fixpoint on Sets
In order to get some insight I think it helps to look at sets graphically:
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. 

Some endofunctions may not have a fixpoint, in this example there is a loop around C,D,E and F.  
Or, if the set is infinite, there may not be any loops. 
So we can see from this that not every endofunction would have a fixpoint or there could be many fixpoints.
Examples
Functor  Initial Algebra  Coalgebra  

List  X > 1 + A × X  List A = 1 + A × X  
Natural Numbers  X > 1 + X  N = 1 + X  
Binary Tree  X > A + X × X  
Stream  X > A × X  
Fixpoint Combinator using Idris
It would be good to have a function which takes an endofunction and generates a fixpoint from it (If it exists).
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 
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 
Ideally we would like this function to return some special value (such as bottom) if there is no fixpoint. This would be more practical for types.
Existence of Fixpoints  Monotonicity
A fixpoint is guaranteed to exist if the function is monotone (KnasterTarski fixpoint theorem).
That is, if there is an order on the elements and the function preserves the order.
This applies even if the order is a partial order provided there is a bottom element.
This order may be thought of in different ways depending if we are coming from the direction of denotional semantics or category theory:
Denotional Semantics  Category Theory  

Order  Applies to a partially defined function. Lower means less well defined and higher means more defined. 
Lower means toward 'initial' and higher means toward 'final'. 
Bottom Element  Denoted. This means undefined/error/nonterminating computation.  The least fixed point is the fixed point with a morphism to every other morphism. 
The semantics should not just be monotone but also continuous , in which the least fixpoint is the union of all finite iterates.
Functions for which f() =are called strict.
Strictly Positive Functor
An inductive type is defined by a functor but not all functors can be used to define an inductive type.
A functor is strictly positive if it is defined by an expression that only uses constant types, the variable type X and the operators ×, +, >, so that X only occurs to the right of arrows. Arrows (functions) are covarient in codomain and contravarient in domain.
More info on this site and this site.
Fixpoint in Types
What we are more interested in here is fixpoints for functions between types (Type > Type) that is a type that depends on another type such as 'List'.
The intuition behind this definition is that, since we applied f infinitely many times to get Fix f, applying it one more time doesn’t change anything.  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)) 
Algebraic Data Type and Least Fixed Point of a Functor
Algebraic data type  least fixed point of a functor 
data Fix f = Fix (f (Fix f)) 
ffix : (a > a) > a ffix f {a} = x where x : a x = f x 
Discussion on Idris Github
Idris code example from here.  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) 
another example from here  
Strictly Positive Functors  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 (strictlypositive) 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 
Example: Nat  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, ())) 
References  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. 
Computer Implementation of Algebra
More information about algebra and monad on this page.
Requires a carrier type to be defined then we need the algebra to be defined like this:
Monoid 
data MonF a = MEmpty  MAppend a a 
Ring 
data RingF a = RZero  ROne  RNeg a  RAdd a a  Rmull a a 
To make this into an expression we need a recursive definition :
Monoid 
data MonExpr = MEmpty  MAppend Expr Expr 
Ring 
data RingExpr = RZero  ROne  RNeg RingExpr  RAdd RingExpr RingExpr  Rmull RingExpr RingExpr 