Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Functors are maps for categories #217

Open
MostAwesomeDude opened this issue Jul 4, 2022 · 3 comments
Open

Functors are maps for categories #217

MostAwesomeDude opened this issue Jul 4, 2022 · 3 comments

Comments

@MostAwesomeDude
Copy link

The central idea behind a functor is that it is a map between categories; for every arrow in the source category, the functor designates an arrow in the target category, such that identity and composition (the algebraic laws for categories) are preserved. This central idea isn't covered.

@CrossEye
Copy link
Contributor

CrossEye commented Jul 8, 2022

@MostAwesomeDude::

I think of this repo as a resource for those not steeped in FP to learn what unfamiliar terms mean. That means that although there have to be some cross-references, these definitions should mostly stand on their own.

How would you cast this suggestion into language which supports that?

Right now, it seems to me that the Functor section meets this. How would you add Categories and Arrows to that definition without making it too complex for FP beginners? Note that I think this would be quite challenging, but I'd be thrilled to be proven wrong. Do you have a suggested rewording of the section?

(This applies to several other recent suggestions you've made as well. But perhaps we could start here.)

@MostAwesomeDude
Copy link
Author

Oh, if I had concrete suggestions for improving wording, I would open a PR. I wouldn't do that to you, just opening issues without planning to eventually resolve them.

My main concern is that the given definitions of "category" and "functor" do not actually line up; we should expect that a "functor" is a map between "categories", but that is not the case. The underlying issue here (and in other issues I've opened) is that there are two situations where a category shows up in a programming context:

  • The category's objects are the types of the programming language, and the arrows are (total/partial/etc.) functions between types
  • The category's objects are the elements of some chosen type, and the arrows are merely skeletal (that is, the category mainly records whether there exists an arrow from one object to another, and not which arrow it might be)

There's no commonly-accepted jargon or nomenclature for this distinction. We might argue that the latter categories are "internal categories", and then by analogy we might call the former category the "external category" for a given language.

Then, the main problem is easy to state: the repo currently documents internal categories and external functors. Worse, the external functors are limited to endofunctors, but the limitation isn't justified.

@CrossEye
Copy link
Contributor

I still think most of this is beyond the scope of this document. The category-theoretical view is interesting, but I think it's mostly a distraction here. However I'm mostly just a viewer here and not a core contributor; someone closer to the work may disagree.

Worse, the external functors are limited to endofunctors, but the limitation isn't justified.

That is absolutely true, and I think there should be examples of other functors. Even str => str.length would help.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants