forked from ajnsit/purescript-typeable
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Dynamic.purs
24 lines (19 loc) · 876 Bytes
/
Dynamic.purs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
module Data.Dynamic where
import Data.Exists (Exists, mkExists, runExists)
import Data.Function ((#))
import Data.Functor (map)
import Data.Leibniz (runLeibniz)
import Data.Maybe (Maybe)
import Data.Typeable (class Typeable, TypeRep, eqT, typeRep)
-- | A `Dynamic` holds a value `a` in a context `t`
-- | and forgets the type of `a`
data Dynamic' :: forall k. (k -> Type) -> k -> Type
data Dynamic' t a = Dynamic' (TypeRep a) (t a)
data Dynamic :: forall k. (k -> Type) -> Type
data Dynamic t = Dynamic (Exists (Dynamic' t))
-- | Wrap a value into a dynamic
dynamic :: forall t a. Typeable a => t a -> Dynamic t
dynamic a = Dynamic (mkExists (Dynamic' typeRep a))
-- | Extract a value from a dynamic
unwrapDynamic :: forall t a. TypeRep a -> Dynamic t -> Maybe (t a)
unwrapDynamic ta (Dynamic e) = e # runExists \(Dynamic' ti v) -> map (\w -> runLeibniz w v) (eqT ti ta)