0 | ||| This module is based on the content of the functional pearl
 1 | ||| How to Take the Inverse of a Type
 2 | ||| by Daniel Marshall and Dominic Orchard
 3 |
 4 | module Data.Linear.Communications
 5 |
 6 | import Data.Linear
 7 | import Data.Linear.Inverse
 8 |
 9 | %default total
10 |
11 | -- Communicating with Inverses
12 |
13 | -- Session type
14 | public export
15 | data Protocol : Type where
16 |   Send : Type -> Protocol -> Protocol
17 |   Recv : Type -> Protocol -> Protocol
18 |   End : Protocol
19 |
20 | public export
21 | Dual : Protocol -> Protocol
22 | Dual (Send x s) = Recv x (Dual s)
23 | Dual (Recv x s) = Send x (Dual s)
24 | Dual End = End
25 |
26 | export
27 | data LChan : Protocol -> Type where
28 |   MkLChan : {- pointer or something  -@ -} LChan p
29 |
30 | parameters
31 |   -- Assuming we have these primitives acting on channels
32 |   (send : forall s, a. LChan (Send a s) -@ a -@ LChan s)
33 |   (recv : forall s, a. LChan (Recv a s) -@ LPair a (LChan s))
34 |   (close : LChan End -@ ())
35 |   -- Fork relates inverse & duality
36 |   (fork : (0 s : Protocol) -> Inverse (LChan s) -@ LChan (Dual s))
37 |
38 |   -- We can write double negation elimination by communicating
39 |   involOp : Inverse (Inverse a) -@ a
40 |   involOp k =
41 |     let 0 P : Protocol
42 |         P = Send a End
43 |         1 r : LChan (Dual P)
44 |             := fork P $ mkInverse $ \ s =>
45 |                 (`divide` k) $ mkInverse $
46 |                 \ x => let 1 c = send s x in close c
47 |         (x # c') := recv r
48 |         () := close c'
49 |      in x
50 |