blob: 6af86e96a4b0355d4dd89e2bcb9bbc6acb79fb8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import GHC.Exts (Any, withDict)
import GHC.TypeLits
import Type.Reflection (TypeRep, typeRep, withTypeable)
-----
-- reflection
-----
class Reifies s a | s -> a where
reflect :: proxy s -> a
instance KnownNat n => Reifies n Integer where
reflect = natVal
reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
{-# NOINLINE reify #-} -- See Note [NOINLINE someNatVal] in GHC.TypeNats
reify a k = withDict @(forall (proxy :: Type -> Type). proxy Any -> a)
@(Reifies (Any @Type) a)
(const a) (k @Any) Proxy
class Given a where
given :: a
withGift :: forall a b.
(Given a => Proxy a -> b)
-> a -> Proxy a -> b
withGift f x y = withDict @a @(Given a) x f y
give :: forall a r. a -> (Given a => r) -> r
give a k = withGift (\_ -> k) a Proxy
foo :: Given Int => Bool -> Int
foo True = 42
foo False = given
-----
-- singletons
-----
type family Sing :: k -> Type
data SBool :: Bool -> Type where
SFalse :: SBool False
STrue :: SBool True
deriving instance Show (SBool z)
type instance Sing @Bool = SBool
class SingI a where
sing :: Sing a
data SingInstance (a :: k) where
SingInstance :: SingI a => SingInstance a
singInstance :: forall k (a :: k). Sing a -> SingInstance a
singInstance s = with_sing_i SingInstance
where
with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
with_sing_i si = withDict @(Sing a) @(SingI a) s si
withSingI :: Sing n -> (SingI n => r) -> r
withSingI sn r =
case singInstance sn of
SingInstance -> r
-----
main :: IO ()
main = do
-- Type.Reflection
let f :: forall a. TypeRep a -> IO ()
f tr = withTypeable tr $ print $ typeRep @a
in f $ typeRep @Int
-- GHC.TypeLits
print $ someCharVal 'a'
print $ someNatVal 42
print $ someSymbolVal "Hello World"
-- reflection
print $ reify 6 (\p -> reflect p + reflect p)
print $ give (23 :: Int) foo True
-- singletons
print $ withSingI SFalse (sing @False)
|
