@@ -1,119 +0,0 @@
1−{-# LANGUAGE RankNTypes #-}
2−{-# LANGUAGE ConstraintKinds #-}
5−type L f = (Unit f, Concat f, Nil f)
8− conc :: f a -> f a -> f a
16−instance Concat [] where
19−instance Unit [] where
26−newtype StringWrapper a = StringWrapper String deriving Show
28−instance Concat StringWrapper where
29− conc (StringWrapper s1) (StringWrapper s2) =
30− StringWrapper ("( " ++ s1 ++ " ++ " ++ s2 ++ " )")
32−instance Unit StringWrapper where
33− unit a = StringWrapper "[val]"
35−instance Nil StringWrapper where
36− nil = StringWrapper "[]"
38−cons x fa = unit x `conc` fa
45−l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
48−l2 = ((u 1) `conc` (u 2)) `conc` (u 3)
50−-- Observe the normalisation using l1' @StringWrapper
51−l1' :: forall f . L f => f Int
54−l2' :: forall f . L f => f Int
58−-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
59−-- right associates the cons
61−newtype MapK f a = MapK (f a -> f a)
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
67−lowerMapK :: Nil f => MapK f a -> f a
68−lowerMapK (MapK fa) = fa nil
70−(<<++>) :: f a -> MapK f a -> f a
71−(<<++>) fa (MapK k) = k fa
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
78−instance L f => (Unit (MapK f)) where
79− unit a = liftMapK (unit a)
81−instance L f => (Nil (MapK f)) where
84−type List a = forall f . L f => f a
86−ravel :: List a -> List a
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)