{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module SomeDictOf
( module SomeDictOf
, module Data.Functor.Identity
, module Data.Proxy
, module Data.Constraint
) where
import Data.Constraint
import Data.Functor.Identity
import Data.Kind
import Data.Proxy
data SomeDictOf (f :: k -> Type) (c :: k -> Constraint) where
SomeDictOf :: c a => f a -> SomeDictOf f c
type SomeDict = SomeDictOf Proxy
someDict :: forall a c. c a => SomeDict c
someDict :: SomeDict c
someDict = Proxy a -> SomeDict c
forall k (c :: k -> Constraint) (a :: k) (f :: k -> *).
c a =>
f a -> SomeDictOf f c
SomeDictOf (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)
fromDict :: forall a c. Dict (c a) -> SomeDict c
fromDict :: Dict (c a) -> SomeDict c
fromDict Dict (c a)
Dict = Proxy a -> SomeDict c
forall k (c :: k -> Constraint) (a :: k) (f :: k -> *).
c a =>
f a -> SomeDictOf f c
SomeDictOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
withSomeDictOf
:: SomeDictOf f c
-> (forall a. c a => f a -> r)
-> r
withSomeDictOf :: SomeDictOf f c -> (forall (a :: k). c a => f a -> r) -> r
withSomeDictOf (SomeDictOf f a
p) forall (a :: k). c a => f a -> r
k =
f a -> r
forall (a :: k). c a => f a -> r
k f a
p
mapSomeDictOf
:: (forall a. c a => f a -> g a)
-> SomeDictOf f c
-> SomeDictOf g c
mapSomeDictOf :: (forall (a :: k). c a => f a -> g a)
-> SomeDictOf f c -> SomeDictOf g c
mapSomeDictOf forall (a :: k). c a => f a -> g a
f (SomeDictOf f a
fa) =
g a -> SomeDictOf g c
forall k (c :: k -> Constraint) (a :: k) (f :: k -> *).
c a =>
f a -> SomeDictOf f c
SomeDictOf (f a -> g a
forall (a :: k). c a => f a -> g a
f f a
fa)
forgetContents
:: forall f c. Functor f
=> SomeDictOf f c
-> f (SomeDictOf Proxy c)
forgetContents :: SomeDictOf f c -> f (SomeDictOf Proxy c)
forgetContents (SomeDictOf (f a
xs :: f a)) =
(a -> SomeDictOf Proxy c) -> f a -> f (SomeDictOf Proxy c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
_ :: a) -> Proxy a -> SomeDictOf Proxy c
forall k (c :: k -> Constraint) (a :: k) (f :: k -> *).
c a =>
f a -> SomeDictOf f c
SomeDictOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)) f a
xs