blob: d4f69504173757f5aee1018820c3dc0dd988c5fe (
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
module Main where
import Data.Kind (Type)
--------------------------------------------------------------------------------
-- Simple generic programming (instant-generics-like library)
--------------------------------------------------------------------------------
data U a = UNIT | SUM (U a) (U a) | PRODUCT (U a) (U a) | REC a
-- GADT interpretation
data I :: U Type -> Type where
Unit :: I UNIT
Inl :: I a -> I (SUM a b)
Inr :: I b -> I (SUM a b)
Product :: I a -> I b -> I (PRODUCT a b)
Rec :: a -> I (REC a)
-- Class embedding types and their generic representation
class Generic (a :: Type) where
type Rep a :: U Type
from :: a -> I (Rep a)
to :: I (Rep a) -> a
-- Generic size on representations
class GSize (a :: U Type) where
gsize :: I a -> Int
instance GSize UNIT where
gsize Unit = 0
instance (GSize a, GSize b) => GSize (SUM a b) where
gsize (Inl x) = gsize x
gsize (Inr x) = gsize x
instance (GSize a, GSize b) => GSize (PRODUCT a b) where
gsize (Product a b) = gsize a + gsize b
instance (Size a) => GSize (REC a) where
gsize (Rec x) = 1 + size x
-- Size on datatypes
class Size (a :: Type) where
size :: a -> Int
default size :: (Generic a, GSize (Rep a)) => a -> Int
size = gsize . from
instance (Size a) => Size [a] -- default
instance Size Char where size _ = 1 -- adhoc
-- Example encoding: lists
instance Generic [a] where
type Rep [a] = SUM UNIT (PRODUCT (REC a) (REC [a]))
from [] = Inl Unit
from (h:t) = Inr (Product (Rec h) (Rec t))
to (Inl Unit) = []
to (Inr (Product (Rec h) (Rec t))) = h:t
-- Testing size
test1 = size "abc"
main = print test1
|
