Has anyone tried tracking the symbol directly on the type? Try using Ptr that way

#1

I was trying to use Haskell’s Ptr recently, and I found that I could directly track Ptr’s maclloc, poke, peek on the type. Here is a demo.

The idea of ​​this demo is to track the creation, update, and free of Ptr symbol directly on the type. This seems to be a good idea. Has anyone tried it before?


type DM = Map Symbol (Maybe Symbol)

data MMP (s :: Symbol) = MMP (Ptr (Ptr Void))

data MKey (ia :: DM -> Type) (b :: DM) where
  MReturn :: ia c -> MKey ia c
  NewKey :: Proxy (s :: Symbol) -> (At (MMP s) (Insert s Nothing dm) ~> MKey ia) -> MKey ia dm
  UpdateKey :: MMP s -> MMP v -> MKey ia (InsertOverwriting s (Just v) dm) -> MKey ia dm
  FreeKey :: MMP s -> MKey ia (DeleteVal s (Delete s dm)) -> MKey ia dm
  LiftM :: IO (MKey ia dm) -> MKey ia dm

instance IFunctor MKey where
  imap f = \case
    MReturn ia -> MReturn (f ia)
    NewKey st cont -> NewKey st (imap f . cont)
    UpdateKey s v cont -> UpdateKey s v (imap f cont)
    FreeKey ak cont -> FreeKey ak (imap f cont)
    LiftM imk -> LiftM (fmap (imap f) imk)

instance IMonad MKey where
  ireturn = MReturn
  ibind f = \case
    MReturn ia -> f ia
    NewKey st cont -> NewKey st (ibind f . cont)
    UpdateKey s v cont -> UpdateKey s v (ibind f cont)
    FreeKey ak cont -> FreeKey ak (ibind f cont)
    LiftM imk -> LiftM (fmap (ibind f) imk)

liftm :: IO a -> MKey (At () dm) dm
liftm io = LiftM (io >> pure (returnAt ()))

newkey :: forall (s :: Symbol) -> MKey (At (MMP s) (Insert s Nothing dm)) dm
newkey s = NewKey (Proxy @s) ireturn

updatekey :: MMP s -> MMP v -> MKey (At () (InsertOverwriting s (Just v) dm)) dm
updatekey s v = UpdateKey s v (returnAt ())

type family LookupI (s :: k) (i :: [k :-> Maybe v]) :: v where
  LookupI k '[] = TypeError (Text "can't get key: " :<>: ShowType k)
  LookupI k ((k ':-> Nothing) ': _) = TypeError (Text "can't get val of key: " :<>: ShowType k)
  LookupI k ((k ':-> Just a) ': _) = a
  LookupI k (_ ': b) = LookupI k b

readkey :: (k ~ (LookupI s dm)) => MMP s -> MKey (At (MMP k) dm) dm
readkey (MMP ptr) =
  LiftM $ do
    t <- peek ptr
    pure $ returnAt (MMP $ castPtr t)

freekey :: MMP s -> MKey (At () (DeleteVal s (Delete s dm))) dm
freekey mmp = FreeKey mmp (returnAt ())

tt :: MKey (At () '[]) '[]
tt = I.do
  At k1 <- newkey "k1"
  At k2 <- newkey "k2"
  At k3 <- newkey "k3"
  liftm $ print (k1, k2, k3)
  updatekey k1 k2
  updatekey k2 k1
  freekey k3
  At k2v <- readkey k2
  liftm $ print k2v
  freekey k1
  freekey k2


runtt :: IO ()
runtt = runMyKey tt

This can achieve some very strange effects.

For example,
pt1 → [pt2]
pt2 → [pt1]

If pt1 is freed, the value of pt2 is null, and the value of pt2 cannot be accessed. The type system can detect this error.

6 Likes
#3

Why does this require indexed monads to work?

#4

I try to keep track of the notation of pointers referencing each other on types, which requires the Indexed Monad.This is more than just keeping track of the types of pointers.

3 Likes