Ticket #1706: TIA-6.8.lhs

File TIA-6.8.lhs, 14.8 KB (added by kahl@…, 7 years ago)

Small example for exponential-time type synonym checking in 6.8

Line 
1\section{|TIA| --- Type-Indexed Aggregates --- ``Type Information Awareness''}
2
3This module provides aggregates of type-indexed constructions,
4somewhat inpired by the heterogeneous list data type |HList| of
5\cite{Kiselyov-Laemmel-Schupke-2004}.
6
7\begin{code}
8{-# LANGUAGE ScopedTypeVariables, KindSignatures, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, TypeSynonymInstances, FunctionalDependencies, UndecidableInstances, Rank2Types, TypeOperators, PartiallyAppliedClosedTypeSynonyms #-}
9module TIA where
10
11import Control.Monad.Error
12import BinaryNumber hiding (succ)
13\end{code}
14
15%{{{ \subsection{The Type-Class |TIA| for Type-Indexed Aggregates}
16\subsection{The Type-Class |TIA| for Type-Indexed Aggregates}
17
18In order to ease providing construction functions,
19I separate the flag type (typically phantom)
20from the flag container,
21and make only the container a parameter of the class |TIA|:
22
23\begin{code}
24class LENGTH r n => LENGTH2 r n
25instance LENGTH r n => LENGTH2 r n
26
27
28class TIA (r :: (* -> *) -> *) where
29  tiaFold :: (forall i . c i -> (a -> a)) -> r c -> (a -> a)
30  tiaMap :: (forall i . c i -> d i) -> r c -> r d
31--  |tiaCons ::  (Nat0E n, Nat0E n1, TIA r1, LENGTH2 r n, LENGTH2 r1 n1, Succ n n1) => c i -> r c -> r1 c|
32--  |isEmpty :: r c -> Bool|
33--  |isSingleton :: Bool|
34--  |headTIA :: r c -> i|
35
36class  (TIA r, TIA r1) => TIACons r r1 a | r1 -> r a where 
37    tiaCons :: c a -> r c -> r1 c
38instance TIACons TiaNil (Tia a) a where
39    tiaCons a _ = Tia a
40instance TIACons  (Tia i) (a ::: Tia i) a where
41   tiaCons a i = a ::: i
42instance (TIA r) => TIACons (i ::: r) (a ::: i ::: r) a where
43   tiaCons a i = a ::: i
44
45-- |class (TIA r) => TIAEmpty r where|
46--    |tiaEmpty :: r|
47-- |instance TIAEmpty|
48\end{code}
49
50\begin{code}
51tiaLength :: (TIA r) => r c -> Int
52tiaLength  r = tiaFold (const succ) r 0
53
54tiaLength2 :: forall r n c . (LENGTH r n) => r c -> Int
55tiaLength2 _ = toInt (undefined :: n)
56\end{code}
57
58\begin{code}
59tiaToList :: forall r c a . (TIA r) => (forall i . c i -> a) -> r c -> [a]
60tiaToList f r = tiaFold f' r []
61    where
62      f' :: forall i . c i -> [a] -> [a]
63      f' = (:) . f
64\end{code}
65
66\begin{code}
67tiaZipWithList :: (TIA r) => (forall i . c i -> a -> b) -> r c -> [a] -> [b]
68tiaZipWithList f r xs = tiaFold (f' xs) r []
69  where
70    f' []  n ys = ys
71    f' (x : xs) n ys = f n x : ys
72\end{code}
73
74\begin{code}
75tiaFoldWithList :: (TIA r) => (forall i . c i -> a -> b -> b) -> r c -> [a] -> b -> b
76tiaFoldWithList f r xs y = tiaFold (f' xs) r y
77  where
78    f' []  n y = y
79    f' (x : xs) n ys = f n x y
80\end{code}
81%}}}
82
83%{{{ Length Class
84\begin{code}
85class (TIA r, Nat0E n) => LENGTH r n | r -> n where
86--    typeLength :: r -> Int
87instance LENGTH TiaNil N0 
88instance LENGTH (Tia i) N1
89instance (LENGTH r n, Succ n n') => LENGTH (i ::: r) n'
90\end{code}
91%}}}
92
93%{{{ \subsection{Instances}
94\subsection{Instances}
95
96\begin{code}
97data TiaNil (c :: * -> *) = TiaNil
98newtype Tia i c = Tia {unTia :: c i}
99data (:::) i r c = c i ::: r c
100data (:*:) r1 r2 (c :: * -> *) = r1 c :*:  r2 c
101\end{code}
102
103\edcomm{WK}{Do we want to have different precedences here?}
104\begin{code}
105infixr 5 :::
106infixr 5 :*:
107\end{code}
108
109Type-level replication is occasionally useful ---
110we provide hard-coded factors as demand arises.
111
112\begin{code}
113type TIACons1 = (:::)
114type TIACons2 t x = TIACons1 t (TIACons1 t x)
115type TIACons3 t x = TIACons2 t (TIACons1 t x)
116type TIACons4 t x = TIACons2 t (TIACons2 t x)
117type TIACons7 t x = TIACons4 t (TIACons3 t x)
118type TIACons8 t x = TIACons4 t (TIACons4 t x)
119type TIACons15 t x = TIACons8 t (TIACons7 t x)
120type TIACons16 t x = TIACons8 t (TIACons8 t x)
121type TIACons31 t x = TIACons16 t (TIACons15 t x)
122type TIACons32 t x = TIACons16 t (TIACons16 t x)
123type TIACons47 t x = TIACons32 t (TIACons15 t x)
124type TIACons48 t x = TIACons32 t (TIACons16 t x)
125\end{code}
126
127The irrefutable patterns are justified
128since presence of a constructor does not really carry any information ---
129it follows from the type.
130
131\begin{code}
132instance TIA TiaNil where
133  tiaMap _ _ = TiaNil
134  tiaFold _ _ = id
135--  tiaCons = (:::)
136--  isEmpty = True
137--  isSingleton = False
138--  headTIA = undefined
139
140instance TIA (Tia i) where
141  tiaFold f (Tia n) = f n
142  tiaMap f (Tia n) = Tia (f n)
143
144instance (TIA r) => TIA (i ::: r) where
145  tiaFold f ~(n ::: r) = f n . tiaFold f r
146  tiaMap f ~(n ::: r) = f n ::: tiaMap f r
147\end{code}
148
149Let's see how far we get with a pair instance:
150
151\begin{code}
152instance (TIA r1, TIA r2) => TIA (r1 :*: r2) where
153  tiaFold f ~(r1 :*: r2) = tiaFold f r1 . tiaFold f r2
154  tiaMap f ~(r1 :*: r2) = tiaMap f r1 :*: tiaMap f r2
155\end{code}
156%}}}
157
158%{{{ \subsection{List-Based Conversions}
159\subsection{List-Based Conversions}
160
161The following are intended to be used in function compositions:
162
163\begin{verbatim}
164{-
165tiaSingleton n = n .*. TiaNil
166tia2Tuple (n1, n2) = n1 .*. n2 .*. TiaNil
167tia3Tuple (n1, n2, n3) = n1 .*. n2 .*. n3 .*. TiaNil
168tia4Tuple (n1, n2, n3, n4) = n1 .*. n2 .*. n3 .*. n4 .*. TiaNil
169-}
170\end{verbatim}
171
172\begin{code}
173tiaSingleton n = Tia n
174tia2Tuple (n1, n2) = n1 ::: Tia n2
175tia3Tuple (n1, n2, n3) = n1 ::: n2 ::: Tia n3
176tia4Tuple (n1, n2, n3, n4) = n1 ::: n2 ::: n3 ::: Tia n4
177tia5Tuple (n1, n2, n3, n4, n5) = n1 ::: n2 ::: n3 ::: n4 ::: Tia n5
178tia6Tuple (n1, n2, n3, n4, n5, n6) = n1 ::: n2 ::: n3 ::: n4 ::: n5 ::: Tia n6
179\end{code}
180
181\begin{code}
182wrapBin :: (c i -> c j -> c k) -> ((Tia i :*: Tia j) c -> Tia k c)
183wrapBin f (Tia x :*: Tia y) = Tia (f x y)
184\end{code}
185
186%{{{ tiaConst, tiaUncurry
187\begin{code}
188tiaConst :: a -> (TiaNil c -> a)
189tiaConst = const
190
191tiaAtom :: (c i -> b) -> Tia i c -> b
192tiaAtom f (Tia n) = f n
193
194tiaUncurry :: (TIA r) => (c i -> r c -> b) -> (i ::: r) c -> b
195tiaUncurry f (n ::: r) = f n r
196\end{code}
197%}}}
198
199%{{{ tiaFunX
200\begin{code}
201tiaFun1 :: (c i -> b) -> Tia i c -> b
202-- |tiaFun1 f = tiaUncurry (tiaConst . f)|
203tiaFun1 = tiaAtom
204\end{code}
205
206\begin{code}
207tiaFun2 :: (c i1 -> c i2 -> b) -> (i1 ::: Tia i2) c -> b
208tiaFun2 f = tiaUncurry (tiaFun1 . f)
209\end{code}
210
211\begin{code}
212tiaFun3 :: (c i1 -> c i2 -> c i3 -> b) -> (i1 ::: i2 ::: Tia i3) c -> b
213tiaFun3 f = tiaUncurry (tiaFun2 . f)
214\end{code}
215
216\begin{code}
217tiaFun4 :: (c i1 -> c i2 -> c i3 -> c i4 -> b)
218  -> (i1 ::: i2 ::: i3 ::: Tia i4) c -> b
219tiaFun4 f = tiaUncurry (tiaFun3 . f)
220\end{code}
221
222\begin{code}
223tiaFun5 :: (c i1 -> c i2 -> c i3 -> c i4 -> c i5 -> b)
224  -> (i1 ::: i2 ::: i3 ::: i4 ::: Tia i5) c -> b
225tiaFun5 f = tiaUncurry (tiaFun4 . f)
226\end{code}
227
228\begin{code}
229tiaFun6 :: (c i1 -> c i2 -> c i3 -> c i4 -> c i5 -> c i6 -> b)
230  -> (i1 ::: i2 ::: i3 ::: i4 ::: i5 ::: Tia i6) c -> b
231tiaFun6 f = tiaUncurry (tiaFun5 . f)
232\end{code}
233%}}}
234%}}}
235
236%{{{ \subsection{|HomTIA|}
237\subsection{|HomTIA|}
238
239%{{{ class HomTIA
240Sometimes we know that all elements have the same type ---
241the following is an experiment to see
242whether we can capture this appropriately.
243Since we list the index among the class arguments,
244this cannot work for |TiaNil|,
245and we have to base these lists on |Tia|.
246
247\begin{code}
248class (TIA r) => HomTIA r i | r -> i where
249  homTIAtoList :: r c -> [c i]
250
251  homTIAparse :: forall m c . (MonadError String m) => [c i] -> m (r c, [c i])
252
253  homTIAfromList :: forall m c . (MonadError String m) => [c i] -> m (r c)
254  homTIAfromList = liftM fst . homTIAparse
255
256instance HomTIA (Tia i) i where
257  homTIAtoList (Tia n) = [n]
258  homTIAparse [] = throwError "Tia.homTIAparse []"
259  homTIAparse (n : ns) = return (Tia n, ns)
260
261instance (HomTIA r i) => HomTIA (i ::: r) i where
262  homTIAtoList ~(n ::: r) = n : homTIAtoList r
263  homTIAparse [] = throwError ":::.homTIAparse []"
264  homTIAparse (n : ns) = case homTIAparse ns of
265    Left e -> fail $ ":::." ++ e
266    Right (r, ns') -> return (n ::: r, ns')
267\end{code}
268
269\begin{code}
270instance (HomTIA r1 i, HomTIA r2 i) => HomTIA (r1 :*: r2) i where
271  homTIAtoList ~(r1 :*: r2) = homTIAtoList r1 ++ homTIAtoList r2
272  homTIAparse cs = case homTIAparse cs of
273    Left e -> throwError $ ":*:1." ++ e
274    Right (r1, cs') -> case homTIAparse cs' of
275      Left e -> throwError $ ":*:2." ++ e
276      Right (r2, cs'') -> return (r1 :*: r2, cs'')
277\end{code}
278%}}}
279%}}}
280
281%{{{ \subsection{Inactive Material}
282\subsection{Inactive Material}
283
284%{{{ class TIAAppend
285\edcomm{WK}{I leave |TIAAppend| commented out for the time being
286since it is not yet clear whether we really need it.
287}
288\begin{verbatim}
289{-
290class TIAAppend r1 r2 r | r1 r2 -> r where
291  tiaAppend :: r1 c -> r2 c -> r c
292  tiaCutPrefix :: r1 c -> r c -> r2 c
293  tiaUnAppend :: r c -> (r1 c, r2 c)  -- type-driven
294
295instance TIA r => TIAAppend TiaNil r r where
296  tiaAppend TiaNil = id
297  tiaCutPrefix _ x = x
298  tiaUnAppend x = (TiaNil, x)
299
300instance TIA r => TIAAppend (Tia n) r (TiaCons n r) where
301  tiaAppend (Tia n) = (n :::)
302  tiaCutPrefix ~(Tia _) (_ ::: r) = r
303  tiaUnAppend (n ::: r) = (Tia n, r)
304
305instance (TIA r1, TIAAppend r1 r2 r) => TIAAppend (TiaCons n r1) r2 (TiaCons n r) where
306  tiaAppend (n ::: r) = (n :::) . tiaAppend r
307  tiaCutPrefix ~(_n ::: r) (_n' ::: r') = tiaCutPrefix r r'
308  tiaUnAppend (n ::: r) = case tiaUnAppend r of (r', x) -> (n ::: r', x)
309-}
310\end{verbatim}
311%}}}
312
313%{{{ class TIAZip
314We let zipping work only for lists of the same length,
315and the same index structure:
316
317\begin{verbatim}
318class TIAZip r1 r2 where
319  tiaZipWith1     ::  (forall i . c i -> d i -> c i) -> r1 c -> r2 d -> r1 c
320  tiaMap2         ::  (forall n1 n2 . c1 n1 -> c2 n2 -> (c1 n1, c2 n2))
321                  ->  r1 -> r2 -> (r1, r2)
322  tiaZip3bWith1   ::  (forall n1 n2 . c1 n1 -> c2 n2 -> c2 n2 -> c1 n1)
323                  ->  r1 -> r2 -> r2 -> r1
324
325instance TIAZip (TiaNil c1) c1 (TiaNil c2) c2 where
326  tiaZipWith1 _ _ _ = TiaNil
327  tiaMap2 _ _ _ = (TiaNil, TiaNil)
328  tiaZip3bWith1 _ _ _ _ = TiaNil
329
330instance  TIAZip (Tia c1 n1) c1 (Tia c2 n2) c2 where
331  tiaZipWith1 f (Tia n1) (Tia n2) = Tia (f (n1 :: c1 n1) (n2 :: c2 n2))
332  tiaMap2 f (Tia n1) (Tia n2) = (Tia n1', Tia n2')
333    where
334      (n1', n2') = f (n1 :: c1 n1) (n2 :: c2 n2) :: (c1 n1, c2 n2)
335  tiaZip3bWith1 f (Tia n1) (Tia n2) (Tia n3) = Tia (f (n1 :: c1 n1) (n2 :: c2 n2) (n3 :: c2 n2))
336
337instance  (TIAZip r1 c1 r2 c2)
338          => TIAZip (TiaCons c1 n1 r1) c1 (TiaCons c2 n2 r2) c2 where
339  tiaZipWith1 f (TiaCons n1 r1) (TiaCons n2 r2) =
340      TiaCons (f (n1 :: c1 n1) (n2 :: c2 n2)) (tiaZipWith1 f r1 r2 :: r1)
341  tiaMap2 f (TiaCons n1 r1) (TiaCons n2 r2) = (TiaCons n1' r1', TiaCons n2' r2')
342    where
343      (n1', n2') = f (n1 :: c1 n1) (n2 :: c2 n2) :: (c1 n1, c2 n2)
344      (r1', r2') = tiaMap2 f r1 r2 :: (r1, r2)
345  tiaZip3bWith1 f (TiaCons n1 r1) (TiaCons n2 r2) (TiaCons n3 r3) =
346      TiaCons (f (n1 :: c1 n1) (n2 :: c2 n2) (n3 :: c2 n2)) (tiaZip3bWith1 f r1 r2 r3 :: r1)
347\end{verbatim}
348
349Again, let us see how far we get with a pair instance:
350
351\begin{verbatim}
352instance (TIAZip r1 c1 r2 c2, TIAZip r1' c1 r2' c2)
353   => TIAZip (r1, r1') c1 (r2, r2') c2 where
354  tiaZipWith1 f (r1, r1') (r2, r2') = (tiaZipWith1 f r1 r2, tiaZipWith1 f r1' r2')
355  tiaMap2 f (r1, r1') (r2, r2') = ((s1, s1'), (s2, s2'))
356    where
357      (s1, s2) = tiaMap2 f r1 r2 :: (r1, r2)
358      (s1', s2') = tiaMap2 f r1' r2' :: (r1', r2')
359  tiaZip3bWith1 f (r1, r1') (r2, r2') (r3, r3') =
360    ((tiaZip3bWith1 f r1 r2 r3 :: r1), (tiaZip3bWith1 f r1' r2' r3' :: r1'))
361\end{verbatim}
362%}}}
363
364%{{{ class TIAZip3
365\begin{verbatim}
366class TIAZip3 r1 c1 r2 c2 r3 c3 | r1 -> c1, r2 -> c2, r3 -> c3 where
367  tiaZip3With1  :: (forall n1 n2 n3 . c1 n1 -> c2 n2 -> c3 n3 -> c1 n1)
368                -> r1 -> r2 -> r3 -> r1
369
370instance TIAZip3 (TiaNil c1) c1 (TiaNil c2) c2 (TiaNil c3) c3 where
371  tiaZip3With1 _ _ _ _ = TiaNil
372
373instance  (TIAZip3 r1 c1 r2 c2 r3 c3)
374          => TIAZip3 (TiaCons c1 n1 r1) c1 (TiaCons c2 n2 r2) c2 (TiaCons c3 n3 r3) c3 where
375  tiaZip3With1 f (TiaCons n1 r1) (TiaCons n2 r2) (TiaCons n3 r3) =
376        TiaCons (f (n1 :: c1 n1) (n2 :: c2 n2) (n3 :: c3 n3)) (tiaZip3With1 f r1 r2 r3 :: r1)
377\end{verbatim}
378
379\begin{verbatim}
380instance (TIAZip3 r1 c1 r2 c2 r3 c3, TIAZip3 r1' c1 r2' c2 r3' c3)
381   => TIAZip3 (r1, r1') c1 (r2, r2') c2 (r3, r3') c3 where
382  tiaZip3With1 f (r1, r1') (r2, r2') (r3, r3') =
383    ((tiaZip3With1 f r1 r2 r3 :: r1), (tiaZip3With1 f r1' r2' r3' :: r1'))
384\end{verbatim}
385%}}}
386
387%{{{ class HomTIAZip
388If both partners of the zip are homogeneous,
389we do not need polymorphic zipping functions:
390
391\begin{verbatim}
392{-
393class (HomTIA c1 r1 n1, HomTIA c2 r2 n2)
394   => HomTIAZip r1 c1 n1 r2 c2 n2
395   | r1 -> c1 n1
396   , r2 -> c2 n2
397   , c1 r1 n1 c2 n2 -> r2
398   , c1 n1 c2 r2 n2 -> r1
399    where
400  homTiaZipWith1 :: (c1 n1 -> c2 n2 -> c1 n1) -> r1 -> r2 -> r1
401  homTiaMap2 :: (c1 n1 -> c2 n2 -> (c1 n1, c2 n2)) -> r1 -> r2 -> (r1, r2)
402  homTiaZip3bWith1 :: (c1 n1 -> c2 n2 -> c2 n2 -> c1 n1) -> r1 -> r2 -> r2 -> r1
403
404instance  HomTIAZip (Tia c1 n1) c1 n1 (Tia c2 n2) c2 n2 where
405  homTiaZipWith1 f (Tia n1) (Tia n2) = Tia (f (n1 :: c1 n1) (n2 :: c2 n2))
406  homTiaMap2 f (Tia n1) (Tia n2) = (Tia n1', Tia n2')
407    where
408      (n1', n2') = f (n1 :: c1 n1) (n2 :: c2 n2) :: (c1 n1, c2 n2)
409  homTiaZip3bWith1 f (Tia n1) (Tia n2) (Tia n3) =
410       Tia (f (n1 :: c1 n1) (n2 :: c2 n2) (n3 :: c2 n2))
411
412instance  (HomTIAZip r1  c1 n1 r2 c2 n2)
413          => HomTIAZip (TiaCons c1 n1 r1) c1 n1 (TiaCons c2 n2 r2) c2 n2 where
414  homTiaZipWith1 f (TiaCons n1 r1) (TiaCons n2 r2) =
415      TiaCons (f (n1 :: c1 n1) (n2 :: c2 n2)) (homTiaZipWith1 f r1 r2 :: r1)
416  homTiaMap2 f (TiaCons n1 r1) (TiaCons n2 r2) = (TiaCons n1' r1', TiaCons n2' r2')
417    where
418      (n1', n2') = f (n1 :: c1 n1) (n2 :: c2 n2) :: (c1 n1, c2 n2)
419      (r1', r2') = homTiaMap2 f r1 r2 :: (r1, r2)
420  homTiaZip3bWith1 f (TiaCons n1 r1) (TiaCons n2 r2) (TiaCons n3 r3) =
421       TiaCons (f (n1 :: c1 n1) (n2 :: c2 n2) (n3 :: c2 n2)) (homTiaZip3bWith1 f r1 r2 r3 :: r1)
422\end{verbatim}
423
424Again, let us see how far we get with a pair instance:
425
426\begin{verbatim}
427instance (HomTIAZip r1 c1 n1 r2 c2 n2, HomTIAZip r1' c1 n1 r2' c2 n2)
428   => HomTIAZip (r1, r1') c1 n1 (r2, r2') c2 n2 where
429  homTiaZipWith1 f (r1, r1') (r2, r2') = (homTiaZipWith1 f r1 r2, homTiaZipWith1 f r1' r2')
430  homTiaMap2 f (r1, r1') (r2, r2') = ((s1, s1'), (s2, s2'))
431    where
432      (s1, s2) = homTiaMap2 f r1 r2 :: (r1, r2)
433      (s1', s2') = homTiaMap2 f r1' r2' :: (r1', r2')
434  homTiaZip3bWith1 f (r1, r1') (r2, r2') (r3, r3') =
435    ((homTiaZip3bWith1 f r1 r2 r3 :: r1), (homTiaZip3bWith1 f r1' r2' r3' :: r1'))
436\end{verbatim}
437%}}}
438
439%{{{ HNat
440\begin{verbatim}
441class HNat n where
442  hNat :: n -> Int
443
444withHNat :: (forall n . HNat n => n -> a) -> Int -> a
445withHNat f 0 = f HZero
446withHNat f k = withHNat (\ n -> f (HSucc n)) $ pred k
447
448
449data HZero = HZero
450data HSucc n = HSucc n
451
452instance HNat HZero where
453  hNat _ = 0
454instance HNat n => HNat (HSucc n) where
455  hNat (HSucc n)= succ (hNat n)
456\end{verbatim}
457%}}}
458
459%{{{ TIAReplicate
460\begin{verbatim}
461class TIAReplicate n r rr where
462  tiaReplicate :: n -> (forall n . HNat n => n -> r) -> rr
463
464instance TIAReplicate HZero r (TiaNil c) where
465  tiaReplicate _ _ = TiaNil
466
467instance forall n r rr rr' .
468  (HNat n, TIAReplicate n r rr, TIAAppend r rr rr') => TIAReplicate (HSucc n) r rr' where
469  tiaReplicate n@(HSucc n') f = tiaAppend (f n) (tiaReplicate n' f :: rr)
470-}
471\end{verbatim}
472%}}}
473%}}}
474
475
476%{{{ EMACS lv
477% Local Variables:
478% folded-file: t
479% fold-internal-margins: 0
480% eval: (fold-set-marks "%{{{ " "%}}}")
481% eval: (fold-whole-buffer)
482% end:
483%}}}