operadsFirstThings/DocCode.hs at master · danielri1011101/operadsFirstThings · 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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
data MoveTree n where
  Leaf :: MoveTree One
  Fan :: Trees n -> MoveTree n

data Trees n where
  NilT :: Trees Z
  (:+) :: (Move, MoveTree a) -> Trees b -> Trees (a+b)

class (Graded f) Operad where
  ident :: f One
  compose :: f n -> Forest f m n -> fm

data Forest f m n where
  Nil :: Forest f Z Z
  Cons :: f i1 -> Forest f i2 n -> Forest f (i1+i2) (S n)

splitForest :: forall f a b z q. SNat a -> SNat b ->
  Forest f q (a+b) ->
  (
   forall j j'. (j+j') ~ q =>
   (Forest f j a, Forest f j' b) -> z
  ) -> z
splitForest (SS (sl :: SNat l))
            (sk :: SNat k)
            (Cons (t :: f j1) (frt :: Forest f j2 (l+k)))
            c =
  splitForest sl sk frt $
    (
     \((lrdr :: Forest f j2' l),(krdr :: Forest f j2'' k)) ->
        case plusAssoc (j1 :: Proxy j1)
                       (j2' :: Proxy j2')
                       (j2'' :: Proxy j2'') of
        Dict -> c (Cons t lrdr , krdr)
    )

instance Operad MoveTree where
  ident = Leaf
  compose Leaf (Cons (t :: MoveTree m) Nil) =
    case plusZ :: Dict (m ~ (m + Z)) of Dict -> t
  compose (Fan ((mv, t) :+ ts)) frt =
    let ans = splitForest (grade t) (grade ts) frt lambda
        lambda = \(mst1, mst2) -> Fan ((mv,tree) :+ trees)
        tree = compose t mst1
        (Fan trees) = compose (Fan ts) mst2
    in ans
  compose _ _ = error "Composition undefined!"

class Functor w => Comonad w where
  extract :: w a -> a
  duplicate :: w a -> w (w a)

class Functor m => Monad m where
  return :: a -> m a
  join :: m (m a) -> m a

data M f a where
  M :: f n -> Vec n a -> M f a

newtype W f a = W {runW :: forall n. f n -> Vec n a}

-- drbr predicts:
runW :: W -> forall n. f n -> Vec n a
--    Polymorphic, I guess.
--    Not what comes out in ghci, sorry.

-- ghci says:
runW :: W f a -> forall (n :: Nat). f n -> Vec n a
-- meaning _n of Nat kind_, I.g.

-- drbr predicts:
W :: (forall (n :: Nat). f n -> Vec n a) -> W f a
-- i.e. W is a placeholder for a tree-to-vector device...
-- Coincides with ghci's answer.

-- Logging dialog with ghci:

:k W
> (Nat -> *) -> * -> *

instance Functor (Vec n) where
  fmap f VNil = VNil
  fmap f (VCons a vs) = VCons (f a) (fmap f vs)

instance Functor (W f) where
  fmap g (W k) =
    W (
       \ f_n -> fmap g (k f_n)
      )

extract :: W f a -> a
extract (W k) = case k ident of VCons a0 VNil -> a0

duplicate' :: W f a -> W f (W f a)

-- take a value and a vector, and replace the vector's coefficients with
-- the value.
replycate :: b -> Vec n a -> Vec n b
replycate b0 VNil = VNil
replycate b0 (VCons a0 as) = VCons b0 (replycate b0 as)

-- trying out a naive duplicate:
duplicate' :: W f a -> W f (W f a)
duplicate' (W k) =
  W (
     \ t_n -> replycate (W k) (k t_n)
    )

instance Operad f => Comonad (W f) where
extract = extract'
duplicate = duplicate'

plusZ :: forall n. Dict (n ~ (n + Z))
plusZ = unsafeCoerce (Dict :: Dict (n ~ n))

plusZ' :: x n -> Dict (n ~ (n + Z))
plusZ' _  = unsafeCoerce (Dict :: Dict (n ~ n))

plusAssoc :: p a -> q b -> r c -> Dict (((a + b) + c) ~ (a + (b + c)))
plusAssoc _ _ _ = unsafeCoerce (Dict :: Dict (a ~ a))

plusAssoc' :: forall a b c. Dict (((a + b) + c) ~ (a + (b + c)))
plusAssoc' = unsafeCoerce (Dict :: Dict (a ~ a))