0 | module Control.Linear.LIO
  1 |
  2 | import public Data.Linear.Notation
  3 | import System
  4 |
  5 | ||| Like `Monad`, but the action and continuation must be run exactly once
  6 | ||| to ensure that the computation is linear.
  7 | public export
  8 | interface LinearBind io where
  9 |   bindL : io a -@ (a -> io b) -@ io b
 10 |
 11 | export
 12 | LinearBind IO where
 13 |   bindL = io_bind
 14 |
 15 | ||| Required usage on the result value of a computation
 16 | public export
 17 | data Usage = None | Linear | Unrestricted
 18 |
 19 | -- Not sure about this, it is a horrible hack, but it makes the notation
 20 | -- a bit nicer
 21 | public export
 22 | fromInteger : (x : Integer) -> {auto _ : Either (x = 0) (x = 1)} -> Usage
 23 | fromInteger 0 = None
 24 | fromInteger 1 = Linear
 25 | fromInteger x = Unrestricted
 26 |
 27 | public export
 28 | 0 ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
 29 |
 30 | ||| A wrapper which allows operations to state the multiplicity of the value
 31 | ||| they return. For example, `L IO {use=1} File` is an IO operation which
 32 | ||| returns a file that must be used exactly once.
 33 | -- This is uglier than I'd like. Perhaps multiplicity polymorphism would make
 34 | -- it neater, but we don't have that (yet?), and fortunately none of this
 35 | -- horror has to be exposed to the user!
 36 | export
 37 | data L : (io : Type -> Type) ->
 38 |          {default Unrestricted use : Usage} ->
 39 |          (ty : Type) -> Type where
 40 |      [search ty]
 41 |      -- Three separate Pures, because we need to distinguish how they are
 42 |      -- used, and this is neater than a continuation.
 43 |      Pure0 : (0 _ : a) -> L io {use=0} a
 44 |      Pure1 : (1 _ : a) -> L io {use=1} a
 45 |      PureW : a -> L io a
 46 |      -- The action is always run once, and the type makes an assertion about
 47 |      -- how often it's safe to use the result.
 48 |      Action : (1 _ : io a) -> L io {use} a
 49 |      Bind : {u_act : _} ->
 50 |             (1 _ : L io {use=u_act} a) ->
 51 |             (1 _ : ContType io u_act u_k a b) ->
 52 |             L io {use=u_k} b
 53 |
 54 | public export
 55 | L0 : (io : Type -> Type) -> (ty : Type) -> Type
 56 | L0 io ty = L io {use = 0} ty
 57 |
 58 | public export
 59 | L1 : (io : Type -> Type) -> (ty : Type) -> Type
 60 | L1 io ty = L io {use = 1} ty
 61 |
 62 | ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
 63 | ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
 64 | ContType io Unrestricted u_k a b = a -> L io {use=u_k} b
 65 |
 66 | RunCont : Usage -> Type -> Type -> Type
 67 | RunCont None t b = (0 _ : t) -> b
 68 | RunCont Linear t b = (1 _ : t) -> b
 69 | RunCont Unrestricted t b = t -> b
 70 |
 71 | -- The repetition here is annoying, but necessary because we don't have
 72 | -- multiplicity polymorphism. We need to look at the usage to know what the
 73 | -- concrete type of the continuation is.
 74 | runK : {use : _} ->
 75 |        LinearBind io =>
 76 |        L io {use} a -@ RunCont use a (io b) -@ io b
 77 | runK (Pure0 x) k = k x
 78 | runK (Pure1 x) k = k x
 79 | runK (PureW x) k = k x
 80 | runK {use = None} (Action x) k = bindL x $ \x' => k x'
 81 | runK {use = Linear} (Action x) k = bindL x $ \x' => k x'
 82 | runK {use = Unrestricted} (Action x) k = bindL x $ \x' => k x'
 83 | runK (Bind {u_act = None} act next) k = runK act (\x => runK (next x) k)
 84 | runK (Bind {u_act = Linear} act next) k = runK act (\x => runK (next x) k)
 85 | runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)
 86 |
 87 | ||| Run a linear program exactly once, with unrestricted return value in the
 88 | ||| underlying context
 89 | export
 90 | run : Applicative io => LinearBind io =>
 91 |       L io a -@ io a
 92 | run prog = runK prog pure
 93 |
 94 | export
 95 | Functor io => Functor (L io) where
 96 |   map fn act = Bind act $ \a' => PureW (fn a')
 97 |
 98 | export
 99 | Applicative io => Applicative (L io) where
100 |   pure = PureW
101 |   (<*>) f a
102 |       = f `Bind` \f' =>
103 |         a `Bind` \a' =>
104 |         PureW (f' a')
105 |
106 | export
107 | (Applicative m, LinearBind m) => Monad (L m) where
108 |   (>>=) a k = Bind a k
109 |
110 | -- prioritise this one for concrete LIO, so we get the most useful
111 | -- linearity annotations.
112 | export %inline
113 | (>>=) : {u_act : _} ->
114 |         LinearBind io =>
115 |         L io {use=u_act} a -@
116 |         ContType io u_act u_k a b -@ L io {use=u_k} b
117 | (>>=) = Bind
118 |
119 | export
120 | delay : {u_act : _} -> L io {use=u_k} b -@ ContType io u_act u_k () b
121 | delay mb = case u_act of
122 |   None => \ _ => mb
123 |   Linear => \ () => mb
124 |   Unrestricted => \ _ => mb
125 |
126 | export %inline
127 | (>>) : {u_act : _} ->
128 |         LinearBind io =>
129 |         L io {use=u_act} () -@
130 |         L io {use=u_k} b -@ L io {use=u_k} b
131 | ma >> mb = ma >>= delay mb
132 |
133 | export %inline
134 | pure0 : (0 x : a) -> L io {use=0} a
135 | pure0 = Pure0
136 |
137 | export %inline
138 | pure1 : a -@ L io {use=1} a
139 | pure1 = Pure1
140 |
141 | ||| Shuffling around linearity annotations: a computation of an
142 | ||| unrestricted value can be seen as a computation of a linear
143 | ||| value that happens to be unrestricted.
144 | export %inline
145 | bang : L IO t -@ L1 IO (!* t)
146 | bang io = io >>= \ a => pure1 (MkBang a)
147 |
148 | export
149 | (LinearBind io, HasLinearIO io) => HasLinearIO (L io) where
150 |   liftIO1 p = Action (liftIO1 p)
151 |
152 | public export
153 | LinearIO : (Type -> Type) -> Type
154 | LinearIO io = (LinearBind io, HasLinearIO io)
155 |
156 | ||| Linear version of `die`
157 | export
158 | die1 : LinearIO io => String -> L1 io a
159 | die1 err = do
160 |   x <- die err
161 |   pure1 x
162 |