0 | ||| This module is based on the paper
  1 | ||| Dependent Tagless Final
  2 | ||| by Nicoals Biri
  3 |
  4 | module Language.Tagless
  5 |
  6 | import Data.List.Elem
  7 | import Data.List.Quantifiers
  8 |
  9 | %default total
 10 |
 11 | export infixr 0 -#
 12 | public export
 13 | (-#) : Type -> Type -> Type
 14 | a -# b = (0 _ : a) -> b
 15 |
 16 | public export
 17 | BinaryOp : Type -> Type
 18 | BinaryOp a = a -> a -> a
 19 |
 20 | namespace Section3
 21 |
 22 |   interface Base (0 inter : Type -# Type) where
 23 |     int : Int -> inter Int
 24 |     add : BinaryOp (inter Int)
 25 |     mult : BinaryOp (inter Int)
 26 |     and : BinaryOp (inter Bool)
 27 |     or : BinaryOp (inter Bool)
 28 |     eq : Eq a => inter a -> inter a -> inter Bool
 29 |     ite : inter Bool -> BinaryOp (inter a)
 30 |
 31 |   interface Read (0 inter : Type -# Type -# Type) where
 32 |     read : inter r r
 33 |     chain : inter a b -> inter b c -> inter a c
 34 |
 35 |   public export
 36 |   Ctx : Type
 37 |   Ctx = List (String, Type)
 38 |
 39 |   interface Var (0 inter : Ctx -# Type -# Type) where
 40 |     lam : (lbl : String) -> inter ((lbl, a) :: ctx) b -> inter ctx (a -> b)
 41 |     app : inter ctx (a -> b) -> inter ctx a -> inter ctx b
 42 |     get : (lbl : String) -> Elem (lbl, a) ctx -> inter ctx a
 43 |
 44 |   record EvalBase (0 a : Type) where
 45 |     constructor MkBase
 46 |     getValueBase : a
 47 |
 48 |   Base EvalBase where
 49 |     int = MkBase
 50 |     add = MkBase .: (+) `on` getValueBase
 51 |     mult = MkBase .: (*) `on` getValueBase
 52 |     and (MkBase b) (MkBase c) = MkBase (b && c)
 53 |     or (MkBase b) (MkBase c) = MkBase (b || c)
 54 |     eq = MkBase .: (==) `on` getValueBase
 55 |     ite (MkBase b) (MkBase t) (MkBase f) = MkBase (ifThenElse b t f)
 56 |
 57 |   record EvalRead (0 r : Type) (0 a : Type) where
 58 |     constructor MkRead
 59 |     getValueRead : r -> a
 60 |
 61 |   runEvalRead : r -> EvalRead r a -> a
 62 |   runEvalRead r (MkRead f) = f r
 63 |
 64 |   Read EvalRead where
 65 |     read = MkRead id
 66 |     chain (MkRead f) (MkRead g) = MkRead (g . f)
 67 |
 68 |   public export
 69 |   Env : Ctx -> Type
 70 |   Env = All snd
 71 |
 72 |   record EvalVar (0 ctx : Ctx) (0 a : Type) where
 73 |     constructor MkEvalVar
 74 |     getValueVar : Env ctx -> a
 75 |
 76 |   Var EvalVar where
 77 |     lam lbl (MkEvalVar body) = MkEvalVar $ \ env, x => body (x :: env)
 78 |     app (MkEvalVar f) (MkEvalVar t) = MkEvalVar $ \ env => f env (t env)
 79 |     get lbl prf = MkEvalVar $ indexAll prf
 80 |
 81 |   -- Mixing two languages: Read & Base
 82 |   -- We can somewhat save ourselves by adding a constraint
 83 |   -- {0 r : Type} -> Base (inter r)
 84 |   testBaseRead : {0 inter : Type -# Type -# Type} ->
 85 |                  ({0 r : Type} -> Base (inter r)) =>
 86 |                  Read inter =>
 87 |                  inter Int Int
 88 |   testBaseRead = chain (eq read (int 2)) (ite read (int 4) (int 0))
 89 |
 90 |   -- Basically duplicating the (Base EvalBase) work but adding orthogonal
 91 |   -- Reader monad cruft. This is annoyingly verbose...
 92 |   Base (EvalRead r) where
 93 |     int = MkRead . const
 94 |     add m n = MkRead $ \ r => ((+) `on` runEvalRead r) m n
 95 |     mult m n = MkRead $ \ r => ((*) `on` runEvalRead r) m n
 96 |     eq m n = MkRead $ \ r => ((==) `on` runEvalRead r) m n
 97 |     or b c = MkRead $ \ r => runEvalRead r b || runEvalRead r c
 98 |     and b c = MkRead $ \ r => runEvalRead r b && runEvalRead r c
 99 |     ite b t f = MkRead $ \ r => ifThenElse (runEvalRead r b) (runEvalRead r t) (runEvalRead r f)
100 |
101 |   -- But it does work.
102 |   runTest : ([0..3] <&> \ r => runEvalRead r Section3.testBaseRead) === [0,0,4,0]
103 |   runTest = Refl
104 |
105 |   -- How are you supposed to compose Base, Read, and Var though?
106 |   -- The constraints on the type of inter are incompatible.
107 |
108 | namespace Section4
109 |
110 |   -- Solution: index Inter by a notion of context and use mtl-style constraints
111 |   -- on the context type to ensure we have access to the required operations
112 |   -- (cf. ReadContext & Read, or VarContext & Var)
113 |
114 |   Inter : Type -> Type
115 |   Inter context = context -> Type -> Type
116 |
117 |   interface Base (0 context : Type) (0 inter : Inter context)
118 |             | inter where
119 |     using (ctx : context)
120 |       int : Int -> inter ctx Int
121 |       add : BinaryOp (inter ctx Int)
122 |       mult : BinaryOp (inter ctx Int)
123 |       and : BinaryOp (inter ctx Bool)
124 |       or : BinaryOp (inter ctx Bool)
125 |       eq : Eq a => inter ctx a -> inter ctx a -> inter ctx Bool
126 |       ite : inter ctx Bool -> BinaryOp (inter ctx a)
127 |
128 |   interface ReadContext context where
129 |     0 getRead : context -> Type
130 |     0 setRead : Type -> context -> context
131 |     0 getSetId : (ctx : context) -> getRead (setRead a ctx) === a
132 |
133 |   interface Read (0 context : Type) (0 inter : Inter context)
134 |             (0 r : ReadContext context) | inter where
135 |     using (ctx : context)
136 |       read : inter ctx (getRead ctx)
137 |       chain : inter ctx a -> inter (setRead a ctx) b -> inter ctx b
138 |
139 |   interface VarContext context where
140 |     0 getCtx : context -> Ctx
141 |     0 addVar : (String, Type) -> context -> context
142 |     0 getAddCons : (ctx : context) -> getCtx (addVar v ctx) === v :: getCtx ctx
143 |
144 |   interface Var context (0 inter : Inter context)
145 |             (0 v : VarContext context) | inter where
146 |     using (ctx : context)
147 |       lam : (lbl : String) -> inter (addVar (lbl, a) ctx) b -> inter ctx (a -> b)
148 |       app : inter ctx (a -> b) -> inter ctx a -> inter ctx b
149 |       get : (lbl : String) -> Elem (lbl, a) (getCtx ctx) -> inter ctx a
150 |
151 |   -- If we only want a reader
152 |   ReadContext Type where
153 |     getRead = id
154 |     setRead = const
155 |     getSetId _ = Refl
156 |
157 |   -- If we only want a var
158 |   VarContext Ctx where
159 |     getCtx = id
160 |     addVar = (::)
161 |     getAddCons _ = Refl
162 |
163 |   -- If we want both a reader and a var
164 |   record RVCtx where
165 |     constructor MkRVCtx
166 |     cellType : Type
167 |     context : Ctx
168 |
169 |   ReadContext RVCtx where
170 |     getRead = cellType
171 |     setRead r = { cellType := r }
172 |     getSetId (MkRVCtx r ctx) = Refl
173 |
174 |   VarContext RVCtx where
175 |     getCtx = context
176 |     addVar v = { context $= (v ::) }
177 |     getAddCons (MkRVCtx r ctx) = Refl
178 |
179 |   record RVEnv (ctx : RVCtx) where
180 |     constructor MkRVEnv
181 |     cellValue : ctx.cellType
182 |     environment : All Builtin.snd ctx.context
183 |
184 |   record Eval (ctx : RVCtx) (a : Type) where
185 |     constructor MkEval
186 |     getEvalValue : RVEnv ctx -> a
187 |
188 |   runEval : RVEnv ctx -> Eval ctx a -> a
189 |   runEval r (MkEval f) = f r
190 |
191 |   Functor (Eval ctx) where
192 |     map f (MkEval k) = MkEval (f . k)
193 |
194 |   Applicative (Eval ctx) where
195 |     pure = MkEval . const
196 |     MkEval f <*> MkEval t = MkEval (\ r => f r (t r))
197 |
198 |   Section4.Read RVCtx Eval %search where
199 |     read = MkEval cellValue
200 |     chain {ctx = MkRVCtx a ctx} f g = MkEval $ \ r =>
201 |       runEval ({ cellValue := runEval r f } r) g
202 |
203 |   Section4.Var RVCtx Eval %search where
204 |     lam {ctx = MkRVCtx a ctx} lbl body
205 |       = MkEval $ \ (MkRVEnv r env), v => runEval (MkRVEnv r (v :: env)) body
206 |     app f t = [| ($) f t |]
207 |     get x pr = MkEval (indexAll pr . environment)
208 |
209 |   Section4.Base RVCtx Eval where
210 |     int x = pure x
211 |     add m n = [| m + n |]
212 |     mult m n = [| m * n |]
213 |     eq m n = [| m == n |]
214 |     -- annoying eta expansions because of Lazy annotations
215 |     and b c = [| (\ b, c => b && c) b c |]
216 |     or b c = [| (\ b, c => b || c) b c |]
217 |     ite b t f = [| (\ b, t, f => ifThenElse b t f) b t f |]
218 |
219 |   -- why do we need hiding? Shouldn't the interfaces be limited to the
220 |   -- separate namespace?!
221 |   %hide Section3.add
222 |   %hide Section3.lam
223 |   %hide Section3.get
224 |   %hide Section3.read
225 |   %hide Section3.int
226 |
227 |   testExpr : {0 inter : RVCtx -> Type -> Type} ->
228 |              Section4.Base RVCtx inter =>
229 |              Section4.Read RVCtx inter %search =>
230 |              Section4.Var RVCtx inter %search =>
231 |              inter (MkRVCtx Int ctx) (Int -> Int)
232 |   testExpr = lam "x" (add (get "x" Here) (add read (int 5)))
233 |