pi-dual/Trees.hs at master · JacquesCarette/pi-dual · GitHub

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
module Trees where

{--

Our objects are n-dimensional cubes represented as complete binary trees of
different heights.

--}

-- plain types: the names are for testing
data T = Zero | One | Plus T T | Times T T | Name String
  deriving Show

data NCube = Leaf T
           | Node NCube NCube -- left is plus; right is minus
  deriving Show

-- examples

-- zeroth level types

t1 = Leaf (Plus One One)
t2 = Leaf One
t3 = Leaf (Times One (Plus One One))
t4 = Leaf (Plus One (Plus One One))

-- first level types (a-b)

tt1 = Node t1 t2
tt2 = Node t3 t4

-- second level types ((a-b)-(c-d))

ttt1 = Node tt1 tt2

-- multiplication

times :: NCube -> NCube -> NCube
times (Leaf t1) (Leaf t2) = Leaf (Times t1 t2)
times (Leaf t) (Node o1 o2) = Node (times (Leaf t) o1) (times (Leaf t) o2)
times (Node o1 o2) o = Node (times o1 o) (times o2 o)

test1 = times
          (Node (Leaf (Name "x+")) (Leaf (Name "y-")))
          (Node (Node (Leaf (Name "a+")) (Leaf (Name "b-")))
                (Node (Leaf (Name "c-")) (Leaf (Name "d+"))))

{--
Node (Node
       (Node (Leaf (Times (Name "x+") (Name "a+")))
             (Leaf (Times (Name "x+") (Name "b-"))))
       (Node (Leaf (Times (Name "x+") (Name "c-")))
             (Leaf (Times (Name "x+") (Name "d+")))))
     (Node
       (Node (Leaf (Times (Name "y-") (Name "a+")))
             (Leaf (Times (Name "y-") (Name "b-"))))
       (Node (Leaf (Times (Name "y-") (Name "c-")))
             (Leaf (Times (Name "y-") (Name "d+")))))
--}

-- addition (extend the shorter tree)

add :: NCube -> NCube -> NCube
add (Leaf t1) (Leaf t2) = Leaf (Plus t1 t2)
add (Leaf t) (Node o1 o2) = add (Node (Leaf t) (Leaf Zero)) (Node o1 o2)
add (Node o1 o2) (Leaf t) = add (Node o1 o2) (Node (Leaf t) (Leaf Zero))
add (Node o1 o2) (Node o3 o4) = Node (add o1 o3) (add o2 o4)

test2 = add
          (Node (Leaf (Name "x+")) (Leaf (Name "y-")))
          (Node (Node (Leaf (Name "a+")) (Leaf (Name "b-")))
                (Node (Leaf (Name "c-")) (Leaf (Name "d+"))))

{--

Node (Node (Leaf (Plus (Name "x+") (Name "a+")))
           (Leaf (Plus Zero (Name "b-"))))
     (Node (Leaf (Plus (Name "y-") (Name "c-")))
           (Leaf (Plus Zero (Name "d+"))))

--}

-- What are the morphisms between these cubes?

{--

mor :: NCube -> NCube -> NMorphism
mor (Leaf t1) (Leaf t2) = Base (t1 :<=> t2)
mor (Node o1 o2) (Node o3 o4) = mor (Either o1 o4) (Either o3 o2)

--}