@@ -0,0 +1,73 @@
1+{-# LANGUAGE RankNTypes #-}
2+{-# LANGUAGE ConstraintKinds #-}
5+type L f = (Unit f, Concat f)
8+ conc :: f a -> f a -> f a
14+instance Concat [] where
17+instance Unit [] where
22+newtype StringWrapper a = StringWrapper String deriving Show
24+instance Concat StringWrapper where
25+ conc (StringWrapper s1) (StringWrapper s2) =
26+ StringWrapper ("( " ++ s1 ++ " ++ " ++ s2 ++ " )")
28+instance Unit StringWrapper where
29+ unit a = StringWrapper "[val]"
30+ nil = StringWrapper "[]"
32+cons x fa = unit x `conc` fa
38+l1 :: forall f . (Unit f, Concat f) => f Int
39+l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
41+-- Observe the normalisation using l1' @StringWrapper
42+l1' :: forall f . L f => f Int
46+-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
47+-- right associates the cons
49+newtype MapK f a = MapK (f a -> f a)
51+liftMapK :: Concat f => f a -> MapK f a
52+--liftMapK fa = (MapK (`conc` fa)) -- Right Associative
53+liftMapK fa = (MapK (fa `conc`)) -- Left Associative
55+lowerMapK :: Unit f => MapK f a -> f a
56+lowerMapK (MapK fa) = fa nil
58+(<<++>) :: f a -> MapK f a -> f a
59+(<<++>) fa (MapK k) = k fa
61+instance Concat (MapK f) where
62+-- conc fa fb = MapK (\g -> g <<++> fa <<++> fb)
63+ conc (MapK fa) (MapK fb) = MapK (fa . fb)
64+-- unit a = MapK (\fa -> unit a
66+instance L f => (Unit (MapK f)) where
67+ unit a = liftMapK (unit a)
70+type List a = forall f . L f => f a
72+ravel :: List a -> List a
73+ravel fa = lowerMapK fa