[TYPES] Functors and free theorems

[Thorsten Altenkirch]

Hi Tim,

just a quick remark: using parametricity you can show that for
any functor, any function inhabiting the map function can be obtained by 
composing the morphism part of the functor with a natural 
transformation. E.g. for any m: Pi X,Y.(X -> Y) -> (F X) -> (F Y)
there is a natural transformation a : Pi X.(F X) -> (F X) s.t.

    m X Y f = (a Y) o (T f)

(You can also shift the nat tfn to the other since of the Tf).

That is the type of the map function almost achieves your goal already.
A typical exception is the twisted map on TX = XxX which is defined
as
      twist f (x,y) = (f y,f x).

However, the result above implies that it is enough to check the first 
functor law (F1 = 1), the other one follows automagically as a "free" 
theorem.

Cheers,
Thorsten

P.S. I proved and used the equation in my CSL 98 paper
"Logical relations and inductive/coinductive types"
see http://www.cs.nott.ac.uk/~txa/publ/

Tim Sweeney wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> A covariant functor is an operator F:type->type paired with a function
> Map:(t->u)->(F(t)->F(u)) such that Map(id(t))=id(F(t)) and
> Map(f.g)=Map(f).Map(g) where "." is function composition and id(t) is the
> identity function over type t.
> 
> Given a functor's Map function, since Map(id(t))=id(F(t)), we can at least
> in concept recover a functor's operator F from its Map function by
> translating the resulting identity arrow id(F(t)) back to its unique type.
> So a Map function obeying the two laws above is sufficient to define a
> functor.
> 
> Question:
> 
> Are there type systems where the type of all such a Map functions (for all
> possible functors) can be expressed precisely?
> 
> I realize that in a type system supporting proofs-as-programs and equality
> types, it is possible to express the types of the proofs of
> Map(id(t))=id(F(t)) and Map(f.g)=Map(f).Map(g) directly.  But this takes the
> form of a product of a function and two relatively verbose proofs about it.
> Is there a way to do this more directly?
> 
> I'm looking for something similar in spirit to the guarantee that in the
> Hindley-Milner type system, every function inhabiting the type
> ForAll(t:type).t->t is an identity function.  Is there a way to express the
> type of Map functions such that a parametricity-derived free theorem
> guarantees that it is inhabited exactly by those functions that are correct
> Map functions of functors?  A solution in any type theory whatsoever (not
> just Hindley-Milner) would be of interest.
> 
> Tim Sweeney
> 


-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham