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.

Sign up for GitHub

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

added some category theory into FunctionK document #1636

Merged
merged 7 commits into from
May 17, 2017
Merged

added some category theory into FunctionK document #1636

Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
f48450d
added some category theory into FunctionK document
kailuowang Apr 25, 2017
64ac09c
correct name
kailuowang Apr 25, 2017
1a4a36c
feedback
kailuowang Apr 25, 2017
c825740
Update functionk.md
kailuowang May 12, 2017
78ded9d
address feedback
kailuowang May 15, 2017
d579487
Merge branch 'master' into improve-functionK-doc
kailuowang May 17, 2017
5a3e63d
Merge branch 'improve-functionK-doc' of github.com:kailuowang/cats in…
kailuowang May 17, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions docs/src/main/tut/datatypes/functionk.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,3 +121,24 @@ type ErrorOr[A] = Either[String, A]
val errorOrFirst: FunctionK[List, ErrorOr] =
λ[FunctionK[List, ErrorOr]](_.headOption.toRight("ERROR: the list was empty!"))
```

## Natural Transformation

In category theory, a [Natural Transformation](https://en.wikipedia.org/wiki/Natural_transformation) provides a morphism between Functors while preserving the internal structure. It's one of the most fundamental notions of category theory.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ncatlab might be a better reference than Wikipedia for such a subject :-) https://ncatlab.org/nlab/show/natural+transformation


If we have two `Functor`s: `F` and `G`, then, being parametric polymorphic, `FunctionK[F, G]` is automatically a Natural Transformation between them. That is, if we have a `fk: F ~> G`, then for any combination of `A`, `B` and function `f: A => B`, the following two functions are equivalent:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps drop the colon, and use 'parametricity', e.g.

If we have two Functors F and G, FunctionK[F, G] is a natural transformation via parametricity. That is, given fk: FunctionK[F, G], for all functions A => B the following are equivalent:

```Scala
(fa:F[A]) => fK(F.map(fa)(f))
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor inconsistency: fK and fk.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This has fK where is is defined above as fk

```
and
```Scala
(fa: F[A]) => G.map(fk(fa))(f)
````

We don't need to write a law to test the implementation of the `fk` for the above to be true. It's automatically given by its parametric polymorphism.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

by parametricity


This is why a parametric polymorphic function `FunctionK[F, G]` is sometimes referred as a Natural Transformation. However, they are two different concepts.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor: is there a particular reason that you capitalized "Natural Transformation" here?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably don't need to capitalize

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line could use some elaboration.. maybe say something about how FunctionK is more powerful than natural transformations, or natural transformations can be implemented in terms of FunctionK (I prefer the latter)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We had a discussion about this on gitter, and @edmundnoble pointed out that natural transformation could be deemed as more powerful in some ways. My intuition is that FunctionK is more powerful in one category but natural transformation is a concept that could involve two categories. Maybe when we restrict natural transformation to endofunctors we can say something about it. In conclusion we feel it's too complex a thing to include here.


Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not entirely sure this is worth including unless we can give an explanation as to how do they differ

For more details, Bartosz Milewski has written a great blog post titled
["Parametricity: Money for Nothing and Theorems for Free"](https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/).