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 2 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
22 changes: 22 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,25 @@ 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 structures. It's one of the most fundamental notions of category theory.
Copy link
Contributor

@SystemFw SystemFw Apr 25, 2017 •
edited
Loading

Choose a reason for hiding this comment

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

while preserving the internal structures

A few comments as requested on Gitter: I think the internal structure is slightly better. It refers to the composition of morphisms (similarly to what a functor does)


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 sometime referred as a Natural Transformation.
Copy link
Contributor

Choose a reason for hiding this comment

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

Pedantry warning (sorry): it should be sometimes, not sometime. :)

However, they are two different concepts. `FunctionK` is a stronger and stricter construction than Natural Transformation.

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/).