4 ms·
Not really, mathematically a functor is really two "functions," one mapping objects to objects and one mapping morphisms to morphisms, along with some condition
by thinkharderdev 5y ago
Not really, mathematically a functor is really two "functions," one mapping objects to objects and one mapping morphisms to morphisms, along with some conditions that make sure the functor is "structure preserving." It is fundamentally a type level construct because, as it is applied to programming, the category in question is the category of types (which is not technically a category due to the halting problem but we sort of hand-wave that away).
- contravariant 5y agoSure a functor satisfies more conditions but that doesn't make it less of a function. Heck if you restrict it to mapping a single set of objects or a particular Homset it is a function, you just can't extend this to the whole category if the objects form a proper class (which happens fairly often). The whole distinction between value-level or type-level is meaningless in general categories. Sure there's a distinction between morphisms between objects and functors between categories but you've also got the category of categories where the morphisms are functors between categories. Edit: I'll have to concede that the article confuses them too much though, you can't just pick a random function and declare it to be a functor, especially when it's not clear between which categories.