Skip to content

Instantly share code, notes, and snippets.

@PkmX
Last active March 30, 2016 19:50
Show Gist options
  • Save PkmX/6edadd8e1699ba97dc0b4225c1d818e4 to your computer and use it in GitHub Desktop.
Save PkmX/6edadd8e1699ba97dc0b4225c1d818e4 to your computer and use it in GitHub Desktop.
DynT

This utility module provides DynT, a dynamically-typed value that restricts the injected value to be a Functor. It can be considered an improved Data.Dynamic.Dynamic.

Below we will refer the Dynamic provided by base as Base.Dynamic:

import qualified Data.Dynamic as Base
import Data.DynT

Motivation

Let's say we have a list of Base.Dynamic, where each value wrapped inside must be actually of type [a]:

let dyns :: [Base.Dynamic]
    dyns = [ Base.toDyn [True, False]
           , Base.toDyn "abcdefghijklmnopqrstuvwxyz"
           , Base.toDyn ([] :: [Int])
           , Base.toDyn (["abc", "def"] ^? ix 0)
           ]

We can unwrap a Base.Dynamic with Base.fromDynamic or Base.fromDyn:

λ> Base.fromDynamic (dyns !! 0) :: Maybe [Bool]
Just [True,False]

However, it is also completely possible to accidentally write:

λ> Base.fromDynamic (dyns !! 2) :: Maybe (Vector Int)
Nothing

Oops!

The problem is that the interface of Data.Dynamic:

Base.toDyn       :: Typeable a => a            -> Base.Dynamic
Base.fromDynamic :: Typeable a => Base.Dynamic -> Maybe a

doesn't really restrict what a could be. Ideally, we would like to a restricted version of Data.Dynamic that captures the "static" part of the structure inside a dynamically-typed value, and the conversion functions should respect said structure.

By the way, did you notice that dyns !! 3 is actually a Maybe String instead of a String? The type checker didn't catch that either.

DynT

DynT transforms a Functor so that it maps over a dynamically-typed value.

data DynT :: (* -> *) -> * where
  DynT :: f Any -> TypeRep -> DynT f
  
toDynT   :: (Functor f, Typeable a) => f a    -> DynT f
fromDynT :: (Functor f, Typeable a) => DynT f -> Maybe (f a)

dynTypeRep :: DynT f -> TypeRep

Now, the example above won't compile:

let dyns :: [DynT []]
    dyns = [ toDynT [True, False]
           , toDynT "abcdefghijklmnopqrstuvwxyz"
           , toDynT ([] :: [Int])
           , toDynT $ ["abc", "def"] ^? ix 0
           ]

    Couldn't match type Maybe with []
    Expected type: DynT []
      Actual type: DynT Maybe
    In the expression: toDynT $ ["abc", "def"] ^? ix 0

Removing the offending element, and we may now convert a DynT [] back with fromDynT:

λ> fromDynT (dyns !! 0) :: Maybe [Bool]
Just [True,False]

Attempting to convert a DynT [] to something that is not a list results in a type error:

λ> fromDynT (dyns !! 2) :: Maybe (Vector Int)

    Couldn't match type [] with Vector
    Expected type: [DynT Vector]
      Actual type: [DynT []]

Dyn

type Dyn = DynT Identity

toDyn   :: Typeable a => a   -> Dyn
fromDyn :: Typeable a => Dyn -> Maybe a

Dyn is functionally equivalent to Data.Dynamic.Dynamic. Note that it isn't a drop-in replacement however.

Base.fromDynamic = fromDyn
Base.fromDyn dyn def = fromMaybe def $ fromDyn dyn

Utility functions

runDynT :: Functor f => DynT f -> f Dyn

Convert a DynT f to a plain Dyn wrapped under f.

wrapDyn     :: (Alternative m, Monad m) => m Dyn -> TypeRep -> DynT m
wrapDynFail :: Monad m                  => m Dyn -> TypeRep -> DynT m

Convert an existing Dyn under a m to DynT m. Unfortunately, it isn't possible to access the TypeRep under m Dyn without m being Copointed, so users must supply the correct TypeRep manually. These two functions differ in how they report the error when the supplied TypeRep does not match the actual TypeRep inside Dyn. wrapDyn returns an empty, and wrapDynFail reports the mismatch with fail.

An example could be passing a DynT f to a function of type DynT f -> f Dyn where you would like to wrap the result back to DynT f again:

  let f :: DynT f -> f Dyn
      
      foo :: (Alternative f, Monad f) => DynT f -> DynT f
      foo d = wrapDyn (f d) (dynTypeRep d)
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Data.DynT where
import Control.Applicative
import Control.Monad
import Data.Functor.Identity
import Data.Maybe
import Data.Typeable
import GHC.Prim (Any)
import Unsafe.Coerce
import Prelude hiding (any)
data DynT :: (* -> *) -> * where
DynT :: f Any -> TypeRep -> DynT f
instance Typeable f => Show (DynT f) where
show (DynT _ tr) = let (tc, trs) = splitTyConApp (typeRep (Proxy :: Proxy f))
in "<<" ++ show (mkTyConApp tc (trs ++ [tr])) ++ ">>"
dynAny :: DynT f -> f Any
dynAny (DynT fany _) = fany
dynTypeRep :: DynT f -> TypeRep
dynTypeRep (DynT _ tr) = tr
toDynT :: forall f a. (Functor f, Typeable a) => f a -> DynT f
toDynT fa = DynT (unsafeCoerce <$> fa) (typeRep (Proxy :: Proxy a))
fromDynT :: forall f a. (Functor f, Typeable a) => DynT f -> Maybe (f a)
fromDynT (DynT fany tr) | typeRep (Proxy :: Proxy a) == tr = Just $ fmap unsafeCoerce fany
| otherwise = Nothing
fromDynM :: forall m a. (Monad m, Typeable a) => DynT m -> m a
fromDynM = fromMaybe (fail "fromDynM") . fromDynT
type Dyn = DynT Identity
instance {-# OVERLAPPING #-} Show Dyn where
show (Dyn _ tr) = "<<" ++ show tr ++ ">>"
pattern Dyn any tr = DynT (Identity any) tr
toDyn :: Typeable a => a -> Dyn
toDyn = toDynT . Identity
fromDyn :: Typeable a => Dyn -> Maybe a
fromDyn = fmap runIdentity . fromDynT
runDynT :: Functor f => DynT f -> f Dyn
runDynT (DynT fany tr) = (`Dyn` tr) <$> fany
wrapDyn :: (Alternative m, Monad m) => m Dyn -> TypeRep -> DynT m
wrapDyn mdyn tr = flip DynT tr $ do
(Dyn any tr') <- mdyn
guard $ tr == tr'
pure any
wrapDynFail :: Monad m => m Dyn -> TypeRep -> DynT m
wrapDynFail mdyn tr = flip DynT tr $ do
(Dyn any tr') <- mdyn
if tr == tr' then pure any else fail "wrapDynFail"
unsafeWrapDynT :: Functor f => f Dyn -> TypeRep -> DynT f
unsafeWrapDynT fdyn = DynT (unsafeCoerce . dynAny <$> fdyn)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment