dynamic-paper.hs 10 KB
Newer Older
1 2 3
{- This is the code extracted from "A reflection on types", by Simon PJ,
Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}

4
-- NB: it includes a negative-recursive function (see delta1), and
Gabor Greif's avatar
Gabor Greif committed
5
-- so will give "simplifier ticks exhausted", at least with -O
6

7 8 9 10
{-#  LANGUAGE RankNTypes, PolyKinds, TypeOperators,
             ScopedTypeVariables, GADTs, FlexibleInstances,
             UndecidableInstances, RebindableSyntax,
             DataKinds, MagicHash, AutoDeriveTypeable, TypeInType  #-}
11 12 13 14
{-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
  -- Because we define a local Typeable class and have
  --   instance Data.Typeable.Typeable a => Typeable a
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247

module Dynamic where

import Data.Map ( Map )
import qualified Data.Map as Map
import Unsafe.Coerce ( unsafeCoerce )
import Control.Monad ( (<=<) )
import Prelude hiding ( lookup, fromInteger, replicate )
import qualified Prelude
import qualified Data.Typeable
import qualified Data.Data
import Data.Kind

lookupMap = Map.lookup
insertMap = Map.insert

--  let's ignore overloaded numbers
fromInteger :: Integer -> Int
fromInteger = Prelude.fromInteger

insertStore = undefined
schema = undefined
withTypeable = undefined
throw# = undefined

toDynamicST = undefined
fromDynamicST = undefined

extendStore  :: Typeable a => STRef s a -> a -> Store -> Store
lookupStore  :: Typeable a => STRef s a -> Store -> Maybe a

type Key = Int
data STRef s a = STR Key
type Store = Map Key Dynamic

extendStore (STR k) v  s =  insertMap k (toDynamicST v) s
lookupStore (STR k)    s =  case lookupMap k s of
                              Just d   -> fromDynamicST d
                              Nothing  -> Nothing

toDynamicST    :: Typeable a => a -> Dynamic
fromDynamicST  :: Typeable a => Dynamic -> Maybe a

eval = undefined
data Term

data DynamicSilly  =  DIntSilly  Int
              |  DBoolSilly Bool
              |  DCharSilly Char
              |  DPairSilly DynamicSilly DynamicSilly


toDynInt :: Int -> DynamicSilly
toDynInt = DIntSilly

fromDynInt :: DynamicSilly -> Maybe Int
fromDynInt (DIntSilly n)  = Just n
fromDynInt _         = Nothing

toDynPair :: DynamicSilly -> DynamicSilly -> DynamicSilly
toDynPair = DPairSilly

dynFstSilly :: DynamicSilly -> Maybe DynamicSilly
dynFstSilly (DPairSilly x1 x2) = Just x1
dynFstSilly _             = Nothing

eval :: Term -> DynamicSilly

eqT = undefined

instance Typeable (->)
instance Typeable Maybe
instance Typeable Bool
instance Typeable Int
instance (Typeable a, Typeable b) => Typeable (a b)
instance Typeable (,)

instance Eq TypeRepX

data Dynamic where
   Dyn :: TypeRep a -> a -> Dynamic

toDynamic :: Typeable a => a -> Dynamic
toDynamic x = Dyn typeRep x

eqTNoKind = undefined

eqTNoKind :: TypeRep a -> TypeRep b -> Maybe (a :***: b)
   --  Primitive; implemented by compiler

data a :***: b where
  ReflNoKind :: a :***: a

fromDynamic :: forall d. Typeable d => Dynamic -> Maybe d
fromDynamic (Dyn (ra :: TypeRep a) (x :: a))
  =  case eqT ra (typeRep :: TypeRep d) of
       Nothing    -> Nothing
       Just Refl  -> Just x

fromDynamicMonad :: forall d. Typeable d => Dynamic -> Maybe d

fromDynamicMonad (Dyn ra x)
  = do  Refl <- eqT ra (typeRep :: TypeRep d)
        return x

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast x = do  Refl <- eqT  (typeRep :: TypeRep a)
                          (typeRep :: TypeRep b)
             return x

gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
                           (typeRep :: TypeRep b)
              return x

data SameKind :: k -> k -> *
type CheckAppResult = SameKind AppResult AppResultNoKind
  --  not the most thorough check
foo :: AppResult x -> AppResultNoKind x
foo (App y z) = AppNoKind y z

splitApp :: TypeRep a -> Maybe (AppResult a)
splitApp = undefined
splitAppNoKind = undefined
splitAppNoKind :: TypeRep a -> Maybe (AppResultNoKind a)
   --  Primitive; implemented by compiler

data AppResultNoKind t where
  AppNoKind :: TypeRep a -> TypeRep b -> AppResultNoKind (a b)

dynFstNoKind :: Dynamic -> Maybe Dynamic
dynFstNoKind (Dyn rpab x)
  = do  AppNoKind rpa rb  <- splitAppNoKind rpab
        AppNoKind rp  ra  <- splitAppNoKind rpa
        Refl        <- eqT rp (typeRep :: TypeRep (,))
        return (Dyn ra (fst x))

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dyn rf f) (Dyn rx x) = do
    App ra rt2   <- splitApp rf
    App rtc rt1  <- splitApp ra
    Refl         <- eqT rtc (typeRep :: TypeRep (->))
    Refl         <- eqT rt1 rx
    return (Dyn rt2 (f x))

data TypeRepAbstract (a :: k)  --  primitive, indexed by type and kind

class Typeable (a :: k) where
   typeRep :: TypeRep a

data AppResult (t :: k) where
  App ::  forall k1 k (a :: k1 -> k) (b :: k1).
          TypeRep a -> TypeRep b -> AppResult (a b)

dynFst :: Dynamic -> Maybe Dynamic
dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))

  = do  App (rpa  :: TypeRep pa ) (rb :: TypeRep b)  <- splitApp rpab
            --  introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|

        App (rp   :: TypeRep p  ) (ra :: TypeRep a)  <- splitApp rpa
            --  introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|

        Refl       <- eqT rp (typeRep :: TypeRep (,))
            --  introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|

        return (Dyn ra (fst x))

eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)

data (a :: k1) :~: (b :: k2) where
  Refl :: forall k (a :: k). a :~: a

castDance :: (Typeable a, Typeable b)  => a -> Maybe b
castDance = castR typeRep typeRep

withTypeable :: TypeRep a -> (Typeable a => r) -> r

castR :: TypeRep a -> TypeRep b -> a -> Maybe b
castR ta tb = withTypeable ta (withTypeable tb castDance)

cmpT = undefined
compareTypeRep = undefined

data TypeRepX where
   TypeRepX :: TypeRep a -> TypeRepX

type TyMapLessTyped = Map TypeRepX Dynamic

insertLessTyped    ::  forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
insertLessTyped x  =   Map.insert (TypeRepX (typeRep :: TypeRep a)) (toDynamic x)

lookupLessTyped  ::  forall a. Typeable a => TyMapLessTyped -> Maybe a
lookupLessTyped  =   fromDynamic <=< Map.lookup (TypeRepX (typeRep :: TypeRep a))

instance Ord TypeRepX where
  compare (TypeRepX tr1) (TypeRepX tr2) = compareTypeRep tr1 tr2

compareTypeRep :: TypeRep a -> TypeRep b -> Ordering  --  primitive

data TyMap = Empty | Node Dynamic TyMap TyMap

lookup :: TypeRep a -> TyMap -> Maybe a
lookup tr1 (Node (Dyn tr2 v) left right) =
  case compareTypeRep tr1 tr2 of
    LT  -> lookup tr1 left
    EQ  -> castR tr2 tr1 v   --  know this cast will succeed
    GT  -> lookup tr1 right
lookup tr1 Empty = Nothing

cmpT :: TypeRep a -> TypeRep b -> OrderingT a b
  --  definition is primitive

data OrderingT a b where
  LTT  :: OrderingT a b
  EQT  :: OrderingT t t
  GTT  :: OrderingT a b

data TypeRep (a :: k) where
  TrApp    :: TypeRep a -> TypeRep b -> TypeRep (a b)
  TrTyCon  :: TyCon -> TypeRep k -> TypeRep (a :: k)

data TyCon = TyCon { tc_module :: Module, tc_name :: String }
data Module = Module { mod_pkg :: String, mod_name :: String }

tcMaybe  :: TyCon
tcMaybe  = TyCon  { tc_module  = Module  { mod_pkg   = "base"
                                               , mod_name  = "Data.Maybe" }
                        , tc_name    = "Maybe" }

rt = undefined

delta1 :: Dynamic -> Dynamic
248 249 250 251
-- NB: this function behaves like a negative-recursive data type
-- and hence leads compiler into an infinite inlining loop,
-- and we get "simplifier ticks exhausted".
-- See Section 7 of the paper "A reflection on types"
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351
delta1 dn = case fromDynamic dn of
             Just f   -> f dn
             Nothing  -> dn
loop1 = delta1 (toDynamic delta1)

data Rid = MkT (forall a. TypeRep a -> a -> a)
rt :: TypeRep Rid
delta :: forall a. TypeRep a -> a -> a
delta ra x = case (eqT ra rt) of
             Just Refl  -> case x of MkT y -> y rt x
             Nothing    -> x
loop = delta rt (MkT delta)

throw# :: SomeException -> a

data SomeException where
  SomeException :: Exception e => e -> SomeException

class (Typeable e, Show e) => Exception e where {   }

data Company
data Salary
incS :: Float -> Salary -> Salary
incS = undefined

--  some impedance matching with SYB
instance Data.Data.Data Company
instance {-#  INCOHERENT  #-} Data.Typeable.Typeable a => Typeable a

mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT f x = case (cast f) of
            Just g   -> g x
            Nothing  -> x

data Expr a
frontEnd = undefined

data DynExp where
  DE :: TypeRep a -> Expr a -> DynExp

frontEnd :: String -> DynExp

data TyConOld

typeOf = undefined
eqTOld = undefined
funTcOld = undefined :: TyConOld
splitTyConApp = undefined
mkTyCon3 = undefined
boolTcOld = undefined
tupleTc = undefined
mkTyConApp = undefined
instance Eq TypeRepOld
instance Eq TyConOld

data TypeRepOld       --  Abstract

class TypeableOld a where
  typeRepOld :: proxy a -> TypeRepOld

data DynamicOld where
   DynOld :: TypeRepOld -> a -> DynamicOld

data Proxy a = Proxy

fromDynamicOld :: forall d. TypeableOld d => DynamicOld -> Maybe d
fromDynamicOld (DynOld trx x)
 | typeRepOld (Proxy :: Proxy d) == trx  = Just (unsafeCoerce x)
 | otherwise                          = Nothing

dynApplyOld :: DynamicOld -> DynamicOld -> Maybe DynamicOld
dynApplyOld (DynOld trf f) (DynOld trx x) =
  case splitTyConApp trf of
      (tc, [t1,t2]) | tc == funTcOld && t1 == trx ->
          Just (DynOld t2 ((unsafeCoerce f) x))
      _ -> Nothing

data DynamicClosed where
  DynClosed :: TypeRepClosed a -> a -> DynamicClosed

data TypeRepClosed (a :: *) where
  TBool  :: TypeRepClosed Bool
  TFun   :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
  TProd  :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)


lookupPil = undefined

lookupPil :: Typeable a => [Dynamic] -> Maybe a

data Dyn1 = Dyn1 Int
         | DynFun (Dyn1 -> Dyn1)
         | DynPair (Dyn1, Dyn1)

data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
data Schema = Object [Schema] |
              Field TypeEnum |
              Array Schema

schema :: Typeable a => a -> Schema