0 | module Data.Linear.Interface
 1 |
 2 | import Data.Linear.Notation
 3 | import Data.Linear.Bifunctor
 4 | import public Data.Linear.Copies
 5 |
 6 | %default total
 7 |
 8 | ||| An interface for consumable types
 9 | public export
10 | interface Consumable a where
11 |   consume : a -@ ()
12 |
13 | ||| Void and the unit type are trivially consumable
14 | export
15 | Consumable Void where consume v impossible
16 |
17 | export
18 | Consumable () where consume u = u
19 |
20 | ||| Unions can be consumed by pattern matching
21 | export
22 | Consumable Bool where
23 |   consume True = ()
24 |   consume False = ()
25 |
26 | export
27 | Consumable (!* a) where
28 |   consume (MkBang v) = ()
29 |
30 | ||| We can cheat to make built-in types consumable
31 | export
32 | Consumable Int where
33 |   consume = believe_me (\ 0 i : Int => ())
34 |
35 | -- But crucially we don't have `Consumable World` or `Consumable Handle`.
36 |
37 | export infixr 5 `seq`
38 | ||| We can sequentially compose a computation returning a value that is
39 | ||| consumable with another computation. This is done by first consuming
40 | ||| the result of the first computation and then returning the second one.
41 | export
42 | seq : Consumable a => a -@ b -@ b
43 | a `seq` b = let 1 () = consume a in b
44 |
45 | public export
46 | interface Duplicable a where
47 |   duplicate : (1 v : a) -> 2 `Copies` v
48 |
49 | export
50 | Duplicable Void where
51 |   duplicate v impossible
52 |
53 | export
54 | Duplicable () where
55 |   duplicate () = [(), ()]
56 |
57 | export
58 | Duplicable Bool where
59 |   duplicate True  = [True, True]
60 |   duplicate False = [False, False]
61 |
62 | export
63 | Duplicable (!* a) where
64 |   duplicate (MkBang v) = [MkBang v, MkBang v]
65 |
66 | ||| Comonoid is the dual of Monoid, it can consume a value linearly and duplicate a value linearly
67 | ||| `comult` returns a pair instead of 2 copies, because we do not guarantee that the two values
68 | ||| are identical, unlike with `duplicate`. For example if we build a comonoid out of a group, with
69 | ||| comult returning both the element given and its inverse:
70 | ||| comult x = x # inverse x
71 | ||| It is not necessarily the case that x equals its inverse. For example the finite group of size
72 | ||| 3, has 1 and 2 as inverses of each other wrt to addition, but are not the same.
73 | public export
74 | interface Comonoid a where
75 |   counit : a -@ ()
76 |   comult : a -@ LPair a a
77 |
78 | ||| If a value is consumable and duplicable we can make an instance of Comonoid for it
79 | export
80 | [AutoComonoid] Consumable a => Duplicable a => Comonoid a where
81 |   counit = consume
82 |   comult x = pair (duplicate x)
83 |
84 | export
85 | Comonoid (!* a) where
86 |   counit (MkBang _) = ()
87 |   comult (MkBang v) = MkBang v # MkBang v
88 |