on master help sign in
DList normalised
112c35cMatthew Pickering
DList.hsnew file+73
@@ -0,0 +1,73 @@
1+{-# LANGUAGE RankNTypes #-}
2+{-# LANGUAGE ConstraintKinds #-}
3+module DList where
4+
5+type L f = (Unit f, Concat 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+ nil :: f a
13+
14+instance Concat [] where
15+ conc = (++)
16+
17+instance Unit [] where
18+ unit a = [a]
19+ nil = []
20+
21+
22+newtype StringWrapper a = StringWrapper String deriving Show
23+
24+instance Concat StringWrapper where
25+ conc (StringWrapper s1) (StringWrapper s2) =
26+ StringWrapper ("( " ++ s1 ++ " ++ " ++ s2 ++ " )")
27+
28+instance Unit StringWrapper where
29+ unit a = StringWrapper "[val]"
30+ nil = StringWrapper "[]"
31+
32+cons x fa = unit x `conc` fa
33+
34+u :: L f => a -> f a
35+u = unit
36+
37+
38+l1 :: forall f . (Unit f, Concat f) => f Int
39+l1 = ((u 1) `conc` (u 2)) `conc` ((u 3) `conc` (u 4))
40+
41+-- Observe the normalisation using l1' @StringWrapper
42+l1' :: forall f . L f => f Int
43+l1' = ravel l1
44+
45+
46+-- Goal: Define a data type Norm such that Norm f a ~ f a but Norm
47+-- right associates the cons
48+
49+newtype MapK f a = MapK (f a -> f a)
50+
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
54+
55+lowerMapK :: Unit f => MapK f a -> f a
56+lowerMapK (MapK fa) = fa nil
57+
58+(<<++>) :: f a -> MapK f a -> f a
59+(<<++>) fa (MapK k) = k fa
60+
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
65+
66+instance L f => (Unit (MapK f)) where
67+ unit a = liftMapK (unit a)
68+ nil = liftMapK nil
69+
70+type List a = forall f . L f => f a
71+
72+ravel :: List a -> List a
73+ravel fa = lowerMapK fa