838155242cebf2b69411a07503f90292d45be9aa
[ghc.git] / testsuite / tests / dependent / should_compile / dynamic-paper.hs
1 {- This is the code extracted from "A reflection on types", by Simon PJ,
2 Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
3
4 -- NB: it includes a negative-recursive function (see delta1), and
5 -- so will give "simplifer ticks exhausted", at least with -O
6
7 {-# LANGUAGE RankNTypes, PolyKinds, TypeOperators,
8 ScopedTypeVariables, GADTs, FlexibleInstances,
9 UndecidableInstances, RebindableSyntax,
10 DataKinds, MagicHash, AutoDeriveTypeable, TypeInType #-}
11 {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-}
12 {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
13 -- Because we define a local Typeable class and have
14 -- instance Data.Typeable.Typeable a => Typeable a
15
16 module Dynamic where
17
18 import Data.Map ( Map )
19 import qualified Data.Map as Map
20 import Unsafe.Coerce ( unsafeCoerce )
21 import Control.Monad ( (<=<) )
22 import Prelude hiding ( lookup, fromInteger, replicate )
23 import qualified Prelude
24 import qualified Data.Typeable
25 import qualified Data.Data
26 import Data.Kind
27
28 lookupMap = Map.lookup
29 insertMap = Map.insert
30
31 -- let's ignore overloaded numbers
32 fromInteger :: Integer -> Int
33 fromInteger = Prelude.fromInteger
34
35 insertStore = undefined
36 schema = undefined
37 withTypeable = undefined
38 throw# = undefined
39
40 toDynamicST = undefined
41 fromDynamicST = undefined
42
43 extendStore :: Typeable a => STRef s a -> a -> Store -> Store
44 lookupStore :: Typeable a => STRef s a -> Store -> Maybe a
45
46 type Key = Int
47 data STRef s a = STR Key
48 type Store = Map Key Dynamic
49
50 extendStore (STR k) v s = insertMap k (toDynamicST v) s
51 lookupStore (STR k) s = case lookupMap k s of
52 Just d -> fromDynamicST d
53 Nothing -> Nothing
54
55 toDynamicST :: Typeable a => a -> Dynamic
56 fromDynamicST :: Typeable a => Dynamic -> Maybe a
57
58 eval = undefined
59 data Term
60
61 data DynamicSilly = DIntSilly Int
62 | DBoolSilly Bool
63 | DCharSilly Char
64 | DPairSilly DynamicSilly DynamicSilly
65
66
67 toDynInt :: Int -> DynamicSilly
68 toDynInt = DIntSilly
69
70 fromDynInt :: DynamicSilly -> Maybe Int
71 fromDynInt (DIntSilly n) = Just n
72 fromDynInt _ = Nothing
73
74 toDynPair :: DynamicSilly -> DynamicSilly -> DynamicSilly
75 toDynPair = DPairSilly
76
77 dynFstSilly :: DynamicSilly -> Maybe DynamicSilly
78 dynFstSilly (DPairSilly x1 x2) = Just x1
79 dynFstSilly _ = Nothing
80
81 eval :: Term -> DynamicSilly
82
83 eqT = undefined
84
85 instance Typeable (->)
86 instance Typeable Maybe
87 instance Typeable Bool
88 instance Typeable Int
89 instance (Typeable a, Typeable b) => Typeable (a b)
90 instance Typeable (,)
91
92 instance Eq TypeRepX
93
94 data Dynamic where
95 Dyn :: TypeRep a -> a -> Dynamic
96
97 toDynamic :: Typeable a => a -> Dynamic
98 toDynamic x = Dyn typeRep x
99
100 eqTNoKind = undefined
101
102 eqTNoKind :: TypeRep a -> TypeRep b -> Maybe (a :***: b)
103 -- Primitive; implemented by compiler
104
105 data a :***: b where
106 ReflNoKind :: a :***: a
107
108 fromDynamic :: forall d. Typeable d => Dynamic -> Maybe d
109 fromDynamic (Dyn (ra :: TypeRep a) (x :: a))
110 = case eqT ra (typeRep :: TypeRep d) of
111 Nothing -> Nothing
112 Just Refl -> Just x
113
114 fromDynamicMonad :: forall d. Typeable d => Dynamic -> Maybe d
115
116 fromDynamicMonad (Dyn ra x)
117 = do Refl <- eqT ra (typeRep :: TypeRep d)
118 return x
119
120 cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
121 cast x = do Refl <- eqT (typeRep :: TypeRep a)
122 (typeRep :: TypeRep b)
123 return x
124
125 gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
126 gcast x = do Refl <- eqT (typeRep :: TypeRep a)
127 (typeRep :: TypeRep b)
128 return x
129
130 data SameKind :: k -> k -> *
131 type CheckAppResult = SameKind AppResult AppResultNoKind
132 -- not the most thorough check
133 foo :: AppResult x -> AppResultNoKind x
134 foo (App y z) = AppNoKind y z
135
136 splitApp :: TypeRep a -> Maybe (AppResult a)
137 splitApp = undefined
138 splitAppNoKind = undefined
139 splitAppNoKind :: TypeRep a -> Maybe (AppResultNoKind a)
140 -- Primitive; implemented by compiler
141
142 data AppResultNoKind t where
143 AppNoKind :: TypeRep a -> TypeRep b -> AppResultNoKind (a b)
144
145 dynFstNoKind :: Dynamic -> Maybe Dynamic
146 dynFstNoKind (Dyn rpab x)
147 = do AppNoKind rpa rb <- splitAppNoKind rpab
148 AppNoKind rp ra <- splitAppNoKind rpa
149 Refl <- eqT rp (typeRep :: TypeRep (,))
150 return (Dyn ra (fst x))
151
152 dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
153 dynApply (Dyn rf f) (Dyn rx x) = do
154 App ra rt2 <- splitApp rf
155 App rtc rt1 <- splitApp ra
156 Refl <- eqT rtc (typeRep :: TypeRep (->))
157 Refl <- eqT rt1 rx
158 return (Dyn rt2 (f x))
159
160 data TypeRepAbstract (a :: k) -- primitive, indexed by type and kind
161
162 class Typeable (a :: k) where
163 typeRep :: TypeRep a
164
165 data AppResult (t :: k) where
166 App :: forall k1 k (a :: k1 -> k) (b :: k1).
167 TypeRep a -> TypeRep b -> AppResult (a b)
168
169 dynFst :: Dynamic -> Maybe Dynamic
170 dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
171
172 = do App (rpa :: TypeRep pa ) (rb :: TypeRep b) <- splitApp rpab
173 -- introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|
174
175 App (rp :: TypeRep p ) (ra :: TypeRep a) <- splitApp rpa
176 -- introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|
177
178 Refl <- eqT rp (typeRep :: TypeRep (,))
179 -- introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|
180
181 return (Dyn ra (fst x))
182
183 eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)
184
185 data (a :: k1) :~: (b :: k2) where
186 Refl :: forall k (a :: k). a :~: a
187
188 castDance :: (Typeable a, Typeable b) => a -> Maybe b
189 castDance = castR typeRep typeRep
190
191 withTypeable :: TypeRep a -> (Typeable a => r) -> r
192
193 castR :: TypeRep a -> TypeRep b -> a -> Maybe b
194 castR ta tb = withTypeable ta (withTypeable tb castDance)
195
196 cmpT = undefined
197 compareTypeRep = undefined
198
199 data TypeRepX where
200 TypeRepX :: TypeRep a -> TypeRepX
201
202 type TyMapLessTyped = Map TypeRepX Dynamic
203
204 insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
205 insertLessTyped x = Map.insert (TypeRepX (typeRep :: TypeRep a)) (toDynamic x)
206
207 lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a
208 lookupLessTyped = fromDynamic <=< Map.lookup (TypeRepX (typeRep :: TypeRep a))
209
210 instance Ord TypeRepX where
211 compare (TypeRepX tr1) (TypeRepX tr2) = compareTypeRep tr1 tr2
212
213 compareTypeRep :: TypeRep a -> TypeRep b -> Ordering -- primitive
214
215 data TyMap = Empty | Node Dynamic TyMap TyMap
216
217 lookup :: TypeRep a -> TyMap -> Maybe a
218 lookup tr1 (Node (Dyn tr2 v) left right) =
219 case compareTypeRep tr1 tr2 of
220 LT -> lookup tr1 left
221 EQ -> castR tr2 tr1 v -- know this cast will succeed
222 GT -> lookup tr1 right
223 lookup tr1 Empty = Nothing
224
225 cmpT :: TypeRep a -> TypeRep b -> OrderingT a b
226 -- definition is primitive
227
228 data OrderingT a b where
229 LTT :: OrderingT a b
230 EQT :: OrderingT t t
231 GTT :: OrderingT a b
232
233 data TypeRep (a :: k) where
234 TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
235 TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k)
236
237 data TyCon = TyCon { tc_module :: Module, tc_name :: String }
238 data Module = Module { mod_pkg :: String, mod_name :: String }
239
240 tcMaybe :: TyCon
241 tcMaybe = TyCon { tc_module = Module { mod_pkg = "base"
242 , mod_name = "Data.Maybe" }
243 , tc_name = "Maybe" }
244
245 rt = undefined
246
247 delta1 :: Dynamic -> Dynamic
248 -- NB: this function behaves like a negative-recursive data type
249 -- and hence leads compiler into an infinite inlining loop,
250 -- and we get "simplifier ticks exhausted".
251 -- See Section 7 of the paper "A reflection on types"
252 delta1 dn = case fromDynamic dn of
253 Just f -> f dn
254 Nothing -> dn
255 loop1 = delta1 (toDynamic delta1)
256
257 data Rid = MkT (forall a. TypeRep a -> a -> a)
258 rt :: TypeRep Rid
259 delta :: forall a. TypeRep a -> a -> a
260 delta ra x = case (eqT ra rt) of
261 Just Refl -> case x of MkT y -> y rt x
262 Nothing -> x
263 loop = delta rt (MkT delta)
264
265 throw# :: SomeException -> a
266
267 data SomeException where
268 SomeException :: Exception e => e -> SomeException
269
270 class (Typeable e, Show e) => Exception e where { }
271
272 data Company
273 data Salary
274 incS :: Float -> Salary -> Salary
275 incS = undefined
276
277 -- some impedance matching with SYB
278 instance Data.Data.Data Company
279 instance {-# INCOHERENT #-} Data.Typeable.Typeable a => Typeable a
280
281 mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a
282 mkT f x = case (cast f) of
283 Just g -> g x
284 Nothing -> x
285
286 data Expr a
287 frontEnd = undefined
288
289 data DynExp where
290 DE :: TypeRep a -> Expr a -> DynExp
291
292 frontEnd :: String -> DynExp
293
294 data TyConOld
295
296 typeOf = undefined
297 eqTOld = undefined
298 funTcOld = undefined :: TyConOld
299 splitTyConApp = undefined
300 mkTyCon3 = undefined
301 boolTcOld = undefined
302 tupleTc = undefined
303 mkTyConApp = undefined
304 instance Eq TypeRepOld
305 instance Eq TyConOld
306
307 data TypeRepOld -- Abstract
308
309 class TypeableOld a where
310 typeRepOld :: proxy a -> TypeRepOld
311
312 data DynamicOld where
313 DynOld :: TypeRepOld -> a -> DynamicOld
314
315 data Proxy a = Proxy
316
317 fromDynamicOld :: forall d. TypeableOld d => DynamicOld -> Maybe d
318 fromDynamicOld (DynOld trx x)
319 | typeRepOld (Proxy :: Proxy d) == trx = Just (unsafeCoerce x)
320 | otherwise = Nothing
321
322 dynApplyOld :: DynamicOld -> DynamicOld -> Maybe DynamicOld
323 dynApplyOld (DynOld trf f) (DynOld trx x) =
324 case splitTyConApp trf of
325 (tc, [t1,t2]) | tc == funTcOld && t1 == trx ->
326 Just (DynOld t2 ((unsafeCoerce f) x))
327 _ -> Nothing
328
329 data DynamicClosed where
330 DynClosed :: TypeRepClosed a -> a -> DynamicClosed
331
332 data TypeRepClosed (a :: *) where
333 TBool :: TypeRepClosed Bool
334 TFun :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
335 TProd :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
336
337
338 lookupPil = undefined
339
340 lookupPil :: Typeable a => [Dynamic] -> Maybe a
341
342 data Dyn1 = Dyn1 Int
343 | DynFun (Dyn1 -> Dyn1)
344 | DynPair (Dyn1, Dyn1)
345
346 data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
347 data Schema = Object [Schema] |
348 Field TypeEnum |
349 Array Schema
350
351 schema :: Typeable a => a -> Schema