Link Details

In many languages you have type constructors; given a type A and a type constructor Lift, you get a new type Lift>. A functor is a type constructor together with a function lift: (A -> B) -> (Lift> -> Lift>) that preserves composition and identities. If h is the composition of two other functions g and f h (a) = g (f (a)), then lift (h) is the composition of lift (g) and lift (f) lift (h) (la) = lift (g) (lift (f) (la)). Similarly, if h is the identity function on variables of type A h (a: A) = a, then lift (h) will be the identity on variables of type Lift> lift (h) (la : Lift>) = la.