patternModerate
What is the relation between functors in SML and Category theory?
Viewed 0 times
thewhattheorycategoryfunctorssmlbetweenandrelation
Problem
Along the same thinking as this statement by Andrej Bauer in this answer
The Haskell community has developed a number of techniques inspired by
category theory, of which monads are best known but should not be
confused with monads.
What is the relation between functors in SML and functors in Category theory?
Since I don't know about the details of functors in other languages such as Haskell or OCaml, if there is info of value then please also add sections for other languages.
The Haskell community has developed a number of techniques inspired by
category theory, of which monads are best known but should not be
confused with monads.
What is the relation between functors in SML and functors in Category theory?
Since I don't know about the details of functors in other languages such as Haskell or OCaml, if there is info of value then please also add sections for other languages.
Solution
Categories form a (large) category whose objects are the (small) categories and whose morphisms are functors between small categories. In this sense functors in category theory are "higher size morphisms".
ML functors are not functors in the categorical sense of the word. But they are "higher size functions" in a type-theoretic sense.
Think of concrete datatypes in a typical programming language as "small". Thus
We may collect all the datatypes into a large collection called
An ML functor is just a slightly more complicated large function: it accepts as an argument several small things and it returns several small things. "Several small things put together" is known as structure in ML. In terms of Martin-Löf type theory we have a universe
Now we can draw an analogy between ML and categories, under which functors correspond to functors. But we also notice that datatypes in ML are like "small categories without morphisms", in other words they are like sets more than they are like categories. We could use an analogy between ML and set theory then:
ML functors are not functors in the categorical sense of the word. But they are "higher size functions" in a type-theoretic sense.
Think of concrete datatypes in a typical programming language as "small". Thus
int, bool, int -> int, etc are small, classes in java are small, as well structs in C.We may collect all the datatypes into a large collection called
Type. A type constructor, such as list or array is a function from Type to Type. So it is a "large" function.An ML functor is just a slightly more complicated large function: it accepts as an argument several small things and it returns several small things. "Several small things put together" is known as structure in ML. In terms of Martin-Löf type theory we have a universe
Type of small types. The large types are usually called kinds. So we have:- values are elements of types (example:
42 : int)
- types are elements of
Type(example:int : Type)
- ML signatures are kinds (example:
OrderedType)
- type constructors are elements of kinds (example:
list : Type -> Type)
- ML stuctures are elements of kinds (example:
String : OrderedType)
- ML functors are functions between kinds (example:
Map.Make : Map.OrderedType -> Make.S)
Now we can draw an analogy between ML and categories, under which functors correspond to functors. But we also notice that datatypes in ML are like "small categories without morphisms", in other words they are like sets more than they are like categories. We could use an analogy between ML and set theory then:
- datatypes are like sets
- kinds are like set-theoretic classes
- functors are like class-sized functions
Context
StackExchange Computer Science Q#9769, answer score: 16
Revisions (0)
No revisions yet.