This repository was archived by the owner on Oct 4, 2020. It is now read-only.
File tree 2 files changed +31
-0
lines changed
2 files changed +31
-0
lines changed Original file line number Diff line number Diff line change 2
2
3
3
## Module Data.Inject
4
4
5
+
6
+ This module defines a type class ` Inject ` which is useful
7
+ when working with coproducts of functors.
8
+
5
9
#### ` Inject `
6
10
7
11
``` purescript
@@ -10,27 +14,39 @@ class Inject f g where
10
14
prj :: forall a. g a -> Maybe (f a)
11
15
```
12
16
17
+ The ` Inject ` class asserts a coproduct relationship between two functors.
18
+
19
+ Specifically, an instance ` Inject f g ` indicates that ` g ` is isomorphic to
20
+ a coproduct of ` f ` and some third functor.
21
+
22
+ Laws:
23
+
24
+ - ` prj g = Just f ` if and only if ` inj f = g `
13
25
14
26
#### ` injectReflexive `
15
27
16
28
``` purescript
17
29
instance injectReflexive :: Inject f f
18
30
```
19
31
32
+ Any functor is isomorphic to the coproduct of itself with the
33
+ constantly-` Void ` functor.
20
34
21
35
#### ` injectLeft `
22
36
23
37
``` purescript
24
38
instance injectLeft :: Inject f (Coproduct f g)
25
39
```
26
40
41
+ Left injection
27
42
28
43
#### ` injectRight `
29
44
30
45
``` purescript
31
46
instance injectRight :: (Inject f g) => Inject f (Coproduct h g)
32
47
```
33
48
49
+ Right injection
34
50
35
51
36
52
Original file line number Diff line number Diff line change
1
+ -- | This module defines a type class `Inject` which is useful
2
+ -- | when working with coproducts of functors.
3
+
1
4
module Data.Inject
2
5
( Inject
3
6
, inj , prj
@@ -7,18 +10,30 @@ import Data.Either (Either(..))
7
10
import Data.Functor.Coproduct (Coproduct (..), coproduct )
8
11
import Data.Maybe (Maybe (..))
9
12
13
+ -- | The `Inject` class asserts a coproduct relationship between two functors.
14
+ -- |
15
+ -- | Specifically, an instance `Inject f g` indicates that `g` is isomorphic to
16
+ -- | a coproduct of `f` and some third functor.
17
+ -- |
18
+ -- | Laws:
19
+ -- |
20
+ -- | - `prj g = Just f` if and only if `inj f = g`
10
21
class Inject f g where
11
22
inj :: forall a . f a -> g a
12
23
prj :: forall a . g a -> Maybe (f a )
13
24
25
+ -- | Any functor is isomorphic to the coproduct of itself with the
26
+ -- | constantly-`Void` functor.
14
27
instance injectReflexive :: Inject f f where
15
28
inj = id
16
29
prj = Just
17
30
31
+ -- | Left injection
18
32
instance injectLeft :: Inject f (Coproduct f g ) where
19
33
inj = Coproduct <<< Left
20
34
prj = coproduct Just (const Nothing )
21
35
36
+ -- | Right injection
22
37
instance injectRight :: (Inject f g ) => Inject f (Coproduct h g ) where
23
38
inj = Coproduct <<< Right <<< inj
24
39
prj = coproduct (const Nothing ) prj
You can’t perform that action at this time.
0 commit comments