Ticket #1706: TIATest.lhs

File TIATest.lhs, 2.4 KB (added by kahl@…, 7 years ago)

This is really the small example --- please ignore TIA-6.8

Line 
1\section{|TIA| --- Type-Indexed Aggregates --- ``Type Information Awareness''}
2
3The original |TIA| 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, PartiallyAppliedClosedTypeSynonyms #-}
9-- Original module requires more:
10-- {-# LANGUAGE ScopedTypeVariables, KindSignatures, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, TypeSynonymInstances, FunctionalDependencies, UndecidableInstances, Rank2Types, TypeOperators #-}
11module TIATest where
12\end{code}
13
14\begin{code}
15data TIACons1 (i :: *) (r :: (* -> *) -> *) (c :: * -> *) = c i ::: r c
16\end{code}
17
18Type-level replication is occasionally useful ---
19we provide hard-coded factors as demand arises.
20
21\begin{code}
22type TIACons2 t x = TIACons1 t (TIACons1 t x)
23type TIACons3 t x = TIACons2 t (TIACons1 t x)
24type TIACons4 t x = TIACons2 t (TIACons2 t x)
25type TIACons7 t x = TIACons4 t (TIACons3 t x)
26type TIACons8 t x = TIACons4 t (TIACons4 t x)
27type TIACons15 t x = TIACons8 t (TIACons7 t x)
28type TIACons16 t x = TIACons8 t (TIACons8 t x)
29type TIACons31 t x = TIACons16 t (TIACons15 t x)
30type TIACons32 t x = TIACons16 t (TIACons16 t x)
31type TIACons47 t x = TIACons32 t (TIACons15 t x)
32type TIACons48 t x = TIACons32 t (TIACons16 t x)
33{-
34-}
35\end{code}
36%}}}
37
38Up to 8:
39
40real    0m0.375s
41user    0m0.284s
42sys     0m0.067s
43-rw------- 1 kahl users 2176 Sep 14 16:39 Utils/TIATest.o
44-rw------- 1 kahl users  779 Sep 14 16:39 Utils/TIATest.hi
45
46Up to 15:
47
48real    0m0.374s
49user    0m0.290s
50sys     0m0.065s
51-rw------- 1 kahl users 2176 Sep 14 16:39 Utils/TIATest.o
52-rw------- 1 kahl users  883 Sep 14 16:39 Utils/TIATest.hi
53
54Up to 16:
55
56real    0m0.368s
57user    0m0.298s
58sys     0m0.064s
59-rw------- 1 kahl users 2176 Sep 14 16:40 Utils/TIATest.o
60-rw------- 1 kahl users  961 Sep 14 16:40 Utils/TIATest.hi
61
62Up to 31:
63
64real    0m7.386s
65user    0m7.139s
66sys     0m0.118s
67-rw------- 1 kahl users 2176 Sep 14 16:41 Utils/TIATest.o
68-rw------- 1 kahl users 1065 Sep 14 16:41 Utils/TIATest.hi
69
70
71Up to 32:
72
73real    0m18.570s
74user    0m18.301s
75sys     0m0.188s
76-rw------- 1 kahl users 2176 Sep 14 16:42 Utils/TIATest.o
77-rw------- 1 kahl users 1143 Sep 14 16:42 Utils/TIATest.hi
78
79
80
81%{{{ EMACS lv
82% Local Variables:
83% folded-file: t
84% fold-internal-margins: 0
85% eval: (fold-set-marks "%{{{ " "%}}}")
86% eval: (fold-whole-buffer)
87% end:
88%}}}