0 | module Data.Linear.Token
  1 |
  2 | import public Data.Linear
  3 |
  4 | %default total
  5 |
  6 | ||| An empty type for tagging linear computations that can be wrapped in `IO`
  7 | public export
  8 | data World : Type where
  9 |
 10 | --------------------------------------------------------------------------------
 11 | -- T1
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| A linear token used in computations with mutable linear state.
 15 | |||
 16 | ||| The idea is that mutable state (mutable references, arrays, pointers,
 17 | ||| and so on) can only be accessed in the presence of the linear token
 18 | ||| that was used to create the mutable resource.
 19 | |||
 20 | ||| The advantage of using linear types over the `ST` monad: They come
 21 | ||| without the (significant) performance overhead of monadic code in
 22 | ||| Idris. Like the `ST` monad, this provides safe resource handling, because
 23 | ||| the function for running linear computations over a `T1` (function
 24 | ||| `run1`) must work with function argument `f` of type
 25 | ||| `forall s . (1 t : T1 s) -> R1 s a`, that is, mutable references cannot
 26 | ||| leak out of the linear computation and remain usable.
 27 | export %noinline %tcinline
 28 | 0 T1 : (s : Type) -> Type
 29 | T1 s = %World
 30 |
 31 | ||| The result of a stateful linear computation.
 32 | |||
 33 | ||| It pairs the result value with a new linear token.
 34 | public export
 35 | data R1 : (s,a : Type) ->  Type where
 36 |   (#) : (v : a) -> (1 tok : T1 s) -> R1 s a
 37 |
 38 | ||| `R1` is a functor, but since `map` does not have the correct
 39 | ||| quantities, this is what we use instead.
 40 | export %inline
 41 | mapR1 : (a -> b) -> (1 r : R1 s a) -> R1 s b
 42 | mapR1 f (v # t) = f v # t
 43 |
 44 | ||| A linear computation operating on resources `rs` that produces a
 45 | ||| result of type `a` with a new token operating on resources `ss`.
 46 | public export
 47 | 0 F1 : (s : Type) -> (a : Type) -> Type
 48 | F1 s a = (1 t : T1 s) -> R1 s a
 49 |
 50 | ||| Convenience alias for `F1 s ()`.
 51 | public export
 52 | 0 F1' : (s : Type) -> Type
 53 | F1' s = F1 s ()
 54 |
 55 | ||| The dummy action that performs no effect at all.
 56 | export %inline
 57 | unit1 : F1' s
 58 | unit1 = (() # )
 59 |
 60 | ||| `F1` is a functor, but since it is a function type, we cannot
 61 | ||| implement an interface for it (but see `Control.Monad.Pure`).
 62 | export %inline
 63 | mapF1 : (a -> b) -> F1 s a -> F1 s b
 64 | mapF1 f act t = mapR1 f (act t)
 65 |
 66 | ||| Runs a linear computation by providing it with its own linear token.
 67 | |||
 68 | ||| Since this is universally quantified over `s`, it is impossible that
 69 | ||| callers can freely choose the tag for the state thread and thus reuse
 70 | ||| their mutable references.
 71 | |||
 72 | ||| It is also not possible that the linear token paired with the
 73 | ||| corresponding mutable state leaks into the outer world, because
 74 | ||| the result value must have quantity omega (see the definition of `R1`).
 75 | export %noinline
 76 | run1 : (forall s . F1 s a) -> a
 77 | run1 f = let v # _ := f {s = ()} %MkWorld in v
 78 |
 79 | ||| Runs a linear computation tagged with `[World]` as a primitive
 80 | ||| `IO` action.
 81 | export %inline
 82 | primRun : F1 World a -> PrimIO a
 83 | primRun f w = let v # w := f w in MkIORes v w
 84 |
 85 | ||| Convenience wrapper around `primRun`.
 86 | export %inline
 87 | runIO : HasIO io => F1 World a -> io a
 88 | runIO f = primIO $ primRun f
 89 |
 90 | ||| Safely uses a primitive `IO` action in `F1 [World]`.
 91 | export %inline
 92 | toF1 : PrimIO a -> F1 World a
 93 | toF1 f w = let MkIORes v w := f w in v # w
 94 |
 95 | ||| Safely uses an `IO` action in `F1 [World]`.
 96 | export %inline
 97 | ioToF1 : IO a -> F1 World a
 98 | ioToF1 io = toF1 (toPrim io)
 99 |
100 | ||| Run the given stateful computation if the boolean value is `True`.
101 | export
102 | when1 : Bool -> Lazy (F1' s) -> F1' s
103 | when1 True  f t = f t
104 | when1 False _ t = () # t
105 |
106 | ||| Run a stateful computation `n` times
107 | export
108 | forN : Nat -> F1' s -> F1' s
109 | forN 0     f t = () # t
110 | forN (S k) f t =
111 |   let _ # t := f t
112 |    in forN k f t
113 |
114 | --------------------------------------------------------------------------------
115 | -- FFI
116 | --------------------------------------------------------------------------------
117 |
118 | ||| Use this to convert a primitive FFI call to a linear function
119 | ||| of type `F1 rs a`.
120 | |||
121 | ||| This is typically used for running effectful computations that
122 | ||| do not produce an interesting result.
123 | ||| See `Data.Linear.Ref1.prim__writeRef` and
124 | ||| the corresponding `Data.Linear.Ref1.write1` for a usage example.
125 | export %inline
126 | ffi : PrimIO a -> F1 s a
127 | ffi prim w = let MkIORes v w := prim w in v # w
128 |
129 | --------------------------------------------------------------------------------
130 | -- Lift1
131 | --------------------------------------------------------------------------------
132 |
133 | ||| An interface for wrapping linear computations in a monadic context.
134 | |||
135 | ||| This allows us to deal with pure as well as effectful computations.
136 | ||| Effectful computations should use `World` as the tag for `s`, while
137 | ||| pure computations should use universal quantification.
138 | public export
139 | interface Monad f => Lift1 (0 s : Type) (0 f : Type -> Type) | f where
140 |   lift1 : F1 s a -> f a
141 |
142 | export %inline
143 | Lift1 World IO where
144 |   lift1 = runIO
145 |
146 | public export
147 | 0 IO1 : Type -> Type
148 | IO1 = F1 World
149 |
150 | ||| Convenience alias for `Lift1 World`
151 | public export
152 | 0 LIO : (f : Type -> Type) -> Type
153 | LIO = Lift1 World
154 |
155 | --------------------------------------------------------------------------------
156 | -- Debugging
157 | --------------------------------------------------------------------------------
158 |
159 | public export
160 | data DebugFlag : Type where
161 |   [noHints]
162 |   NoDebugging : DebugFlag
163 |   Debugging   : DebugFlag
164 |
165 | ||| This is a utility for debugging complex linear algorithms
166 | ||| similar to but more convenient than the one find in module
167 | ||| `Debug.Trace`.
168 | |||
169 | ||| Strictly speaking, using this breaks referential transparency.
170 | export %inline
171 | debug1 : String -> F1' s
172 | debug1 s t = let MkIORes u t := toPrim (putStrLn s) t in u # t
173 |
174 | ||| Like `debug1` but can be conveniently turned on and off via an
175 | ||| auto-implicit flag.
176 | export %inline
177 | debugIf1 : {auto debug : DebugFlag} -> String -> F1' s
178 | debugIf1 {debug = NoDebugging} s t = () # t
179 | debugIf1 {debug = Debugging}   s t = debug1 s t
180 |