Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / PolyKinds09.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE TypeFamilies #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE FlexibleContexts #-}
6
7 module Main where
8
9 --------------------------------------------------------------------------------
10 -- Simple generic programming (instant-generics-like library)
11 --------------------------------------------------------------------------------
12 data U a = UNIT | SUM (U a) (U a) | PRODUCT (U a) (U a) | REC a
13
14 -- GADT interpretation
15 data I :: U * -> * where
16 Unit :: I UNIT
17 Inl :: I a -> I (SUM a b)
18 Inr :: I b -> I (SUM a b)
19 Product :: I a -> I b -> I (PRODUCT a b)
20 Rec :: a -> I (REC a)
21
22 -- Class embedding types and their generic representation
23 class Generic (a :: *) where
24 type Rep a :: U *
25 from :: a -> I (Rep a)
26 to :: I (Rep a) -> a
27
28 -- Generic size on representations
29 class GSize (a :: U *) where
30 gsize :: I a -> Int
31
32 instance GSize UNIT where
33 gsize Unit = 0
34
35 instance (GSize a, GSize b) => GSize (SUM a b) where
36 gsize (Inl x) = gsize x
37 gsize (Inr x) = gsize x
38
39 instance (GSize a, GSize b) => GSize (PRODUCT a b) where
40 gsize (Product a b) = gsize a + gsize b
41
42 instance (Size a) => GSize (REC a) where
43 gsize (Rec x) = 1 + size x
44
45 -- Size on datatypes
46 class Size (a :: *) where
47 size :: a -> Int
48 default size :: (Generic a, GSize (Rep a)) => a -> Int
49 size = gsize . from
50
51 instance (Size a) => Size [a] -- default
52 instance Size Char where size _ = 1 -- adhoc
53
54 -- Example encoding: lists
55 instance Generic [a] where
56 type Rep [a] = SUM UNIT (PRODUCT (REC a) (REC [a]))
57 from [] = Inl Unit
58 from (h:t) = Inr (Product (Rec h) (Rec t))
59 to (Inl Unit) = []
60 to (Inr (Product (Rec h) (Rec t))) = h:t
61
62 -- Testing size
63 test1 = size "abc"
64
65 main = print test1