Search code examples
haskelltypesprogramming-languagescomputer-sciencecategory-theory

Do all the function types form a subcategory of `Hask`?

In Haskell, all the types form a category named Hask.

Function types are types. Do all the function types form a subcategory of Hask?

Do all the non-function types form a subcategory of Hask?

I think both answers are yes. But I dont know if I am right.

Solution

  • Let C be any category having class O for its objects.

    If O' is any subclass of O we can define a category C' taking O' as the objects, and keeping all the morphisms in C which still "make sense", i.e. which have source and target object in O'. Composition and identities are the same (restricted to O').

    C' is a subcategory of C. (A full subcategory, to be precise.)

    You should check this claim yourself, by expanding all the definitions.

    The examples you mention simply pick some special cases for O', so they are subcategories.