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