post(typoclassopedia): Applicative Laws
theme(monospace): use Mononoki for code
This commit is contained in:
parent
87efe12fd4
commit
0e3d5a990f
@ -6,7 +6,7 @@
|
|||||||
<title>{% if page.title %}{{ page.title }}{% else %}{{ site.title }}{% endif %}</title>
|
<title>{% if page.title %}{{ page.title }}{% else %}{{ site.title }}{% endif %}</title>
|
||||||
<meta name="description" content="{% if page.excerpt %}{{ page.excerpt | strip_html | strip_newlines | truncate: 160 }}{% else %}{{ site.description }}{% endif %}">
|
<meta name="description" content="{% if page.excerpt %}{{ page.excerpt | strip_html | strip_newlines | truncate: 160 }}{% else %}{{ site.description }}{% endif %}">
|
||||||
|
|
||||||
<link href="https://fonts.googleapis.com/css?family=Secular+One|Nunito|Ubuntu+Mono" rel="stylesheet">
|
<link href="https://fonts.googleapis.com/css?family=Secular+One|Nunito|Mononoki" rel="stylesheet">
|
||||||
<link rel="stylesheet" href="{{ "/css/main.css" | prepend: site.baseurl }}">
|
<link rel="stylesheet" href="{{ "/css/main.css" | prepend: site.baseurl }}">
|
||||||
<link rel="canonical" href="{{ page.url | replace:'index.html','' | prepend: site.baseurl | prepend: site.url }}">
|
<link rel="canonical" href="{{ page.url | replace:'index.html','' | prepend: site.baseurl | prepend: site.url }}">
|
||||||
<link rel="alternate" type="application/rss+xml" title="{{ site.title }}" href="{{ "/feed.xml" | prepend: site.baseurl | prepend: site.url }}" />
|
<link rel="alternate" type="application/rss+xml" title="{{ site.title }}" href="{{ "/feed.xml" | prepend: site.baseurl | prepend: site.url }}" />
|
||||||
|
@ -275,3 +275,55 @@ The Functor section links to [Category Theory](https://en.wikibooks.org/wiki/Has
|
|||||||
fmap (f . g) (Just x) = Just ((f . g) x) = Just (f (g x))
|
fmap (f . g) (Just x) = Just ((f . g) x) = Just (f (g x))
|
||||||
fmap f (fmap g (Just x)) = Just (f (g x)) = Just ((f . g) x)
|
fmap f (fmap g (Just x)) = Just (f (g x)) = Just ((f . g) x)
|
||||||
```
|
```
|
||||||
|
|
||||||
|
Applicative
|
||||||
|
===========
|
||||||
|
|
||||||
|
## Laws
|
||||||
|
|
||||||
|
1. The identity law:
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
pure id <*> v = v
|
||||||
|
```
|
||||||
|
|
||||||
|
2. Homomorphism:
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
pure f <*> pure x = pure (f x)
|
||||||
|
```
|
||||||
|
|
||||||
|
Intuitively, applying a non-effectful function to a non-effectful argument in an effectful context is the same as just applying the function to the argument and then injecting the result into the context with pure.
|
||||||
|
|
||||||
|
3. Interchange:
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
u <*> pure y = pure ($ y) <*> u
|
||||||
|
```
|
||||||
|
|
||||||
|
Intuitively, this says that when evaluating the application of an effectful function to a pure argument, the order in which we evaluate the function and its argument doesn't matter.
|
||||||
|
|
||||||
|
4. Composition:
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
|
||||||
|
```
|
||||||
|
|
||||||
|
This one is the trickiest law to gain intuition for. In some sense it is expressing a sort of associativity property of (`<*>`). The reader may wish to simply convince themselves that this law is type-correct.
|
||||||
|
|
||||||
|
### Exercises
|
||||||
|
|
||||||
|
(Tricky) One might imagine a variant of the interchange law that says something about applying a pure function to an effectful argument. Using the above laws, prove that
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
pure f <*> x = pure (flip ($)) <*> x <*> pure f
|
||||||
|
```
|
||||||
|
|
||||||
|
**Solution**:
|
||||||
|
|
||||||
|
```haskell
|
||||||
|
pure f <*> x = pure (($) f) <*> x -- identical
|
||||||
|
pure f <*> x = pure ($) <*> pure f <*> x -- homomorphism
|
||||||
|
pure f <*> x = pure (flip ($)) <*> x <*> pure f -- flip arguments
|
||||||
|
```
|
||||||
|
|
||||||
|
@ -224,7 +224,11 @@ pre {
|
|||||||
font-family: 'Ubuntu Light';
|
font-family: 'Ubuntu Light';
|
||||||
src: url(fonts/Ubuntu-Light_gdi.woff);
|
src: url(fonts/Ubuntu-Light_gdi.woff);
|
||||||
}
|
}
|
||||||
|
//@font-face {
|
||||||
|
//font-family: 'Ubuntu Mono';
|
||||||
|
//src: url(fonts/UbuntuMono-Regular_gdi.woff);
|
||||||
|
//}
|
||||||
@font-face {
|
@font-face {
|
||||||
font-family: 'Ubuntu Mono';
|
font-family: Mononoki;
|
||||||
src: url(fonts/UbuntuMono-Regular_gdi.woff);
|
src: url(fonts/mononoki-Regular.woff);
|
||||||
}
|
}
|
||||||
|
@ -5,7 +5,7 @@
|
|||||||
/* ----------------------------------------------------------*/
|
/* ----------------------------------------------------------*/
|
||||||
|
|
||||||
pre, code {
|
pre, code {
|
||||||
font-family: 'Ubuntu Mono';
|
font-family: 'Mononoki';
|
||||||
font-size: 11pt;
|
font-size: 11pt;
|
||||||
overflow-x: auto;
|
overflow-x: auto;
|
||||||
}
|
}
|
||||||
|
BIN
css/fonts/mononoki-Regular.ttf
Normal file
BIN
css/fonts/mononoki-Regular.ttf
Normal file
Binary file not shown.
BIN
css/fonts/mononoki-Regular.woff
Normal file
BIN
css/fonts/mononoki-Regular.woff
Normal file
Binary file not shown.
Loading…
Reference in New Issue
Block a user