on master help sign in
Extend example to eliminate empty list
5106556Matthew Pickering
DList.hs+50−4
@@ -2,13 +2,15 @@
2{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE ConstraintKinds #-}
3module DList where
3module DList where
4
4
5−type L f = (Unit f, Concat f)
5+type L f = (Unit f, Concat f, Nil f)
6
6
7class Concat f where
7class Concat f where
8 conc :: f a -> f a -> f a
8 conc :: f a -> f a -> f a
9
9
10class Unit f where
10class Unit f where
11 unit :: a -> f a
11 unit :: a -> f a
12+
13+class Nil f where
12 nil :: f a
14 nil :: f a
13
15
14instance Concat [] where
16instance Concat [] where
@@ -16,6 +18,8 @@ instance Concat [] where
16
18
17instance Unit [] where
19instance Unit [] where
18 unit a = [a]
20 unit a = [a]
21+
22+instance Nil [] where
19 nil = []
23 nil = []
20
24
21
25
@@ -27,6 +31,8 @@ instance Concat StringWrapper where
27
31
28instance Unit StringWrapper where
32instance Unit StringWrapper where
29 unit a = StringWrapper "[val]"
33 unit a = StringWrapper "[val]"
34+
35+instance Nil StringWrapper where
30 nil = StringWrapper "[]"
36 nil = StringWrapper "[]"
31
37
32cons x fa = unit x `conc` fa
38cons x fa = unit x `conc` fa
@@ -35,13 +41,19 @@ u :: L f => a -> f a
35u = unit
41u = unit
36
42
37
43
38−l1 :: forall f . (Unit f, Concat f) => f Int
44+l1 :: List Int
39l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
45l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
40
46
47+l2 :: List Int
48+l2 = ((u 1) `conc` (u 2)) `conc` (u 3)
49+
41-- Observe the normalisation using l1' @StringWrapper
50-- Observe the normalisation using l1' @StringWrapper
42l1' :: forall f . L f => f Int
51l1' :: forall f . L f => f Int
43l1' = ravel l1
52l1' = ravel l1
44
53
54+l2' :: forall f . L f => f Int
55+l2' = ravel l2
56+
45
57
46-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
58-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
47-- right associates the cons
59-- right associates the cons
@@ -52,7 +64,7 @@ liftMapK :: Concat f => f a -> MapK f a
52--liftMapK fa = (MapK (`conc` fa)) -- Right Associative
64--liftMapK fa = (MapK (`conc` fa)) -- Right Associative
53liftMapK fa = (MapK (fa `conc`)) -- Left Associative
65liftMapK fa = (MapK (fa `conc`)) -- Left Associative
54
66
55−lowerMapK :: Unit f => MapK f a -> f a
67+lowerMapK :: Nil f => MapK f a -> f a
56lowerMapK (MapK fa) = fa nil
68lowerMapK (MapK fa) = fa nil
57
69
58(<<++>) :: f a -> MapK f a -> f a
70(<<++>) :: f a -> MapK f a -> f a
@@ -65,9 +77,43 @@ instance Concat (MapK f) where
65
77
66instance L f => (Unit (MapK f)) where
78instance L f => (Unit (MapK f)) where
67 unit a = liftMapK (unit a)
79 unit a = liftMapK (unit a)
80+
81+instance L f => (Nil (MapK f)) where
68 nil = liftMapK nil
82 nil = liftMapK nil
69
83
70type List a = forall f . L f => f a
84type List a = forall f . L f => f a
71
85
72ravel :: List a -> List a
86ravel :: 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+