Embrace -XTypeInType, add -XStarIsType
[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 "simplifier ticks exhausted", at least with -O
6
7 {-# LANGUAGE RankNTypes, PolyKinds, TypeOperators,
8 ScopedTypeVariables, GADTs, FlexibleInstances,
9 UndecidableInstances, RebindableSyntax,
10 DataKinds, MagicHash, AutoDeriveTypeable #-}
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 SomeTypeRep
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 -> Type
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 -> Type|, |b :: k2|
174
175 App (rp :: TypeRep p ) (ra :: TypeRep a) <- splitApp rpa
176 -- introduces kind |k1|, and types |p :: k1 -> k2 -> Type|,
177 -- |a :: k1|
178
179 Refl <- eqT rp (typeRep :: TypeRep (,))
180 -- introduces |p ~ (,)| and
181 -- |(k1 -> k2 -> Type) ~ (Type -> Type -> Type)|
182
183 return (Dyn ra (fst x))
184
185 eqT :: forall k1 k2 (a :: k1) (b :: k2).
186 TypeRep a -> TypeRep b -> Maybe (a :~: b)
187
188 data (a :: k1) :~: (b :: k2) where
189 Refl :: forall k (a :: k). a :~: a
190
191 castDance :: (Typeable a, Typeable b) => a -> Maybe b
192 castDance = castR typeRep typeRep
193
194 withTypeable :: TypeRep a -> (Typeable a => r) -> r
195
196 castR :: TypeRep a -> TypeRep b -> a -> Maybe b
197 castR ta tb = withTypeable ta (withTypeable tb castDance)
198
199 cmpT = undefined
200 compareTypeRep = undefined
201
202 data SomeTypeRep where
203 SomeTypeRep :: TypeRep a -> SomeTypeRep
204
205 type TyMapLessTyped = Map SomeTypeRep Dynamic
206
207 insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
208 insertLessTyped x
209 = Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x)
210
211 lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a
212 lookupLessTyped
213 = fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))
214
215 instance Ord SomeTypeRep where
216 compare (SomeTypeRep tr1) (SomeTypeRep tr2) = compareTypeRep tr1 tr2
217
218 compareTypeRep :: TypeRep a -> TypeRep b -> Ordering -- primitive
219
220 data TyMap = Empty | Node Dynamic TyMap TyMap
221
222 lookup :: TypeRep a -> TyMap -> Maybe a
223 lookup tr1 (Node (Dyn tr2 v) left right) =
224 case compareTypeRep tr1 tr2 of
225 LT -> lookup tr1 left
226 EQ -> castR tr2 tr1 v -- know this cast will succeed
227 GT -> lookup tr1 right
228 lookup tr1 Empty = Nothing
229
230 cmpT :: TypeRep a -> TypeRep b -> OrderingT a b
231 -- definition is primitive
232
233 data OrderingT a b where
234 LTT :: OrderingT a b
235 EQT :: OrderingT t t
236 GTT :: OrderingT a b
237
238 data TypeRep (a :: k) where
239 TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
240 TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k)
241
242 data TyCon = TyCon { tc_module :: Module, tc_name :: String }
243 data Module = Module { mod_pkg :: String, mod_name :: String }
244
245 tcMaybe :: TyCon
246 tcMaybe = TyCon { tc_module = Module { mod_pkg = "base"
247 , mod_name = "Data.Maybe" }
248 , tc_name = "Maybe" }
249
250 rt = undefined
251
252 delta1 :: Dynamic -> Dynamic
253 -- NB: this function behaves like a negative-recursive data type
254 -- and hence leads compiler into an infinite inlining loop,
255 -- and we get "simplifier ticks exhausted".
256 -- See Section 7 of the paper "A reflection on types"
257 delta1 dn = case fromDynamic dn of
258 Just f -> f dn
259 Nothing -> dn
260 loop1 = delta1 (toDynamic delta1)
261
262 data Rid = MkT (forall a. TypeRep a -> a -> a)
263 rt :: TypeRep Rid
264 delta :: forall a. TypeRep a -> a -> a
265 delta ra x = case (eqT ra rt) of
266 Just Refl -> case x of MkT y -> y rt x
267 Nothing -> x
268 loop = delta rt (MkT delta)
269
270 throw# :: SomeException -> a
271
272 data SomeException where
273 SomeException :: Exception e => e -> SomeException
274
275 class (Typeable e, Show e) => Exception e where { }
276
277 data Company
278 data Salary
279 incS :: Float -> Salary -> Salary
280 incS = undefined
281
282 -- some impedance matching with SYB
283 instance Data.Data.Data Company
284 instance {-# INCOHERENT #-} Data.Typeable.Typeable a => Typeable a
285
286 mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a
287 mkT f x = case (cast f) of
288 Just g -> g x
289 Nothing -> x
290
291 data Expr a
292 frontEnd = undefined
293
294 data DynExp where
295 DE :: TypeRep a -> Expr a -> DynExp
296
297 frontEnd :: String -> DynExp
298
299 data TyConOld
300
301 typeOf = undefined
302 eqTOld = undefined
303 funTcOld = undefined :: TyConOld
304 splitTyConApp = undefined
305 mkTyCon3 = undefined
306 boolTcOld = undefined
307 tupleTc = undefined
308 mkTyConApp = undefined
309 instance Eq TypeRepOld
310 instance Eq TyConOld
311
312 data TypeRepOld -- Abstract
313
314 class TypeableOld a where
315 typeRepOld :: proxy a -> TypeRepOld
316
317 data DynamicOld where
318 DynOld :: TypeRepOld -> a -> DynamicOld
319
320 data Proxy a = Proxy
321
322 fromDynamicOld :: forall d. TypeableOld d => DynamicOld -> Maybe d
323 fromDynamicOld (DynOld trx x)
324 | typeRepOld (Proxy :: Proxy d) == trx = Just (unsafeCoerce x)
325 | otherwise = Nothing
326
327 dynApplyOld :: DynamicOld -> DynamicOld -> Maybe DynamicOld
328 dynApplyOld (DynOld trf f) (DynOld trx x) =
329 case splitTyConApp trf of
330 (tc, [t1,t2]) | tc == funTcOld && t1 == trx ->
331 Just (DynOld t2 ((unsafeCoerce f) x))
332 _ -> Nothing
333
334 data DynamicClosed where
335 DynClosed :: TypeRepClosed a -> a -> DynamicClosed
336
337 data TypeRepClosed (a :: Type) where
338 TBool :: TypeRepClosed Bool
339 TFun :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
340 TProd :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
341
342
343 lookupPil = undefined
344
345 lookupPil :: Typeable a => [Dynamic] -> Maybe a
346
347 data Dyn1 = Dyn1 Int
348 | DynFun (Dyn1 -> Dyn1)
349 | DynPair (Dyn1, Dyn1)
350
351 data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
352 data Schema = Object [Schema] |
353 Field TypeEnum |
354 Array Schema
355
356 schema :: Typeable a => a -> Schema