@@ -2,13 +2,15 @@
22{-# LANGUAGE ConstraintKinds #-}
33module DList where
44
5−type L f = (Unit f, Concat f)
5+type L f = (Unit f, Concat f, Nil f)
66
77class Concat f where
88 conc :: f a -> f a -> f a
99
1010class Unit f where
1111 unit :: a -> f a
12+
13+class Nil f where
1214 nil :: f a
1315
1416instance Concat [] where
@@ -16,6 +18,8 @@ instance Concat [] where
1618
1719instance Unit [] where
1820 unit a = [a]
21+
22+instance Nil [] where
1923 nil = []
2024
2125
@@ -27,6 +31,8 @@ instance Concat StringWrapper where
2731
2832instance Unit StringWrapper where
2933 unit a = StringWrapper "[val]"
34+
35+instance Nil StringWrapper where
3036 nil = StringWrapper "[]"
3137
3238cons x fa = unit x `conc` fa
@@ -35,13 +41,19 @@ u :: L f => a -> f a
3541u = unit
3642
3743
38−l1 :: forall f . (Unit f, Concat f) => f Int
44+l1 :: List Int
3945l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
4046
47+l2 :: List Int
48+l2 = ((u 1) `conc` (u 2)) `conc` (u 3)
49+
4150-- Observe the normalisation using l1' @StringWrapper
4251l1' :: forall f . L f => f Int
4352l1' = ravel l1
4453
54+l2' :: forall f . L f => f Int
55+l2' = ravel l2
56+
4557
4658-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
4759-- right associates the cons
@@ -52,7 +64,7 @@ liftMapK :: Concat f => f a -> MapK f a
5264--liftMapK fa = (MapK (`conc` fa)) -- Right Associative
5365liftMapK fa = (MapK (fa `conc`)) -- Left Associative
5466
55−lowerMapK :: Unit f => MapK f a -> f a
67+lowerMapK :: Nil f => MapK f a -> f a
5668lowerMapK (MapK fa) = fa nil
5769
5870(<<++>) :: f a -> MapK f a -> f a
@@ -65,9 +77,43 @@ instance Concat (MapK f) where
6577
6678instance L f => (Unit (MapK f)) where
6779 unit a = liftMapK (unit a)
80+
81+instance L f => (Nil (MapK f)) where
6882 nil = liftMapK nil
6983
7084type List a = forall f . L f => f a
7185
7286ravel :: List a -> List a
73−ravel fa = lowerMapK fa
87+ravel fa = lower fa
88+
89+-- First reassociate as this introduces a nil
90+-- then remove the nil to demonstrate the second pass
91+-- This is cool!
92+lower :: L f => MapK (PureK f) a -> f a
93+lower = lowerPureK . lowerMapK
94+
95+-- xs ++ [] == xs
96+
97+data PureK f a = Pure | Dirty (f a)
98+
99+liftPureK :: f a -> PureK f a
100+liftPureK = Dirty
101+
102+lowerPureK :: L f => PureK f a -> f a
103+lowerPureK Pure = nil
104+lowerPureK (Dirty fa) = fa
105+
106+instance Nil (PureK f) where
107+ nil = Pure
108+
109+instance Concat f => (Concat (PureK f)) where
110+ conc Pure fa = fa
111+ conc fa Pure = fa
112+ conc (Dirty fa) (Dirty fb) = Dirty (fa `conc` fb)
113+
114+instance Unit f => (Unit (PureK f)) where
115+ unit a = Dirty (unit a)
116+
117+
118+
119+