@@ -2,13 +2,15 @@
2{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE ConstraintKinds #-}
3module DList where
3module DList where
5−type L f = (Unit f, Concat f)
5+type L f = (Unit f, Concat f, Nil f)
7class Concat f where
7class Concat f where
8 conc :: f a -> f a -> f a
8 conc :: f a -> f a -> f a
10class Unit f where
10class Unit f where
11 unit :: a -> f a
11 unit :: a -> f a
12 nil :: f a
14 nil :: f a
14instance Concat [] where
16instance Concat [] where
@@ -16,6 +18,8 @@ instance Concat [] where
17instance Unit [] where
19instance Unit [] where
18 unit a = [a]
20 unit a = [a]
@@ -27,6 +31,8 @@ instance Concat StringWrapper where
28instance Unit StringWrapper where
32instance Unit StringWrapper where
29 unit a = StringWrapper "[val]"
33 unit a = StringWrapper "[val]"
35+instance Nil StringWrapper where
30 nil = StringWrapper "[]"
36 nil = StringWrapper "[]"
32cons x fa = unit x `conc` fa
38cons x fa = unit x `conc` fa
@@ -35,13 +41,19 @@ u :: L f => a -> f a
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))
48+l2 = ((u 1) `conc` (u 2)) `conc` (u 3)
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
54+l2' :: forall f . L f => f Int
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
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
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
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)
81+instance L f => (Nil (MapK f)) where
68 nil = liftMapK nil
82 nil = liftMapK nil
70type List a = forall f . L f => f a
84type List a = forall f . L f => f a
72ravel :: List a -> List a
86ravel :: List a -> List a
73−ravel fa = lowerMapK fa
87+ravel fa = lower fa
89+-- First reassociate as this introduces a nil
90+-- then remove the nil to demonstrate the second pass
92+lower :: L f => MapK (PureK f) a -> f a
93+lower = lowerPureK . lowerMapK
97+data PureK f a = Pure | Dirty (f a)
99+liftPureK :: f a -> PureK f a
102+lowerPureK :: L f => PureK f a -> f a
103+lowerPureK Pure = nil
104+lowerPureK (Dirty fa) = fa
106+instance Nil (PureK f) where
109+instance Concat f => (Concat (PureK f)) where
112+ conc (Dirty fa) (Dirty fb) = Dirty (fa `conc` fb)
114+instance Unit f => (Unit (PureK f)) where
115+ unit a = Dirty (unit a)