[Replaced type lists with the new Data.List1.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305000632] hunk ./MultiComposition.agda 17
+open import Data.List1
hunk ./MultiComposition.agda 20
--- Type vectors
+-- Turning a list of types into a function type
hunk ./MultiComposition.agda 22
-infixr 5 _∷_ _++_
+-- Fun (a ∷₁ b ∷₁ c ∷₁ []₁) d ≡₁ a -> b -> c -> d.
hunk ./MultiComposition.agda 24
-data TypeList : Set1 where
-  []  : TypeList
-  _∷_ : Set -> TypeList -> TypeList
-
-Fun : TypeList -> Set -> Set
-Fun []       b = b
-Fun (a ∷ as) b = a -> Fun as b
-
-_++_ : TypeList -> TypeList -> TypeList
-[]       ++ bs = bs
-(a ∷ as) ++ bs = a ∷ (as ++ bs)
+Fun : [ Set ]₁ -> Set -> Set
+Fun []₁       b = b
+Fun (a ∷₁ as) b = a -> Fun as b
hunk ./MultiComposition.agda 29
-        Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++ ts₂) a
-lemma []        = ≡₁-refl
-lemma (t ∷ ts₁) = ≡₁-ext \_ -> lemma ts₁
+        Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++₁ ts₂) a
+lemma []₁        = ≡₁-refl
+lemma (t ∷₁ ts₁) = ≡₁-ext \_ -> lemma ts₁
hunk ./MultiComposition.agda 41
-        (a -> b) -> (ts : TypeList) -> Fun ts a -> Fun ts b
-f ⟪ []     ⟫ g = f g
-f ⟪ a ∷ as ⟫ g = \x -> f ⟪ as ⟫ g x
+        (a -> b) -> (ts : [ Set ]₁) -> Fun ts a -> Fun ts b
+f ⟪ []₁     ⟫ g = f g
+f ⟪ a ∷₁ as ⟫ g = \x -> f ⟪ as ⟫ g x
hunk ./MultiComposition.agda 47
-             (ts : TypeList) {g₁ g₂ : Fun ts a} -> g₁ ≡ g₂ ->
+             (ts : [ Set ]₁) {g₁ g₂ : Fun ts a} -> g₁ ≡ g₂ ->
hunk ./MultiComposition.agda 54
-        Fun ts₁ (Fun ts₂ a) -> Fun (ts₁ ++ ts₂) a
-merge []        f = f
-merge (t ∷ ts₁) f = \x -> merge ts₁ (f x)
+        Fun ts₁ (Fun ts₂ a) -> Fun (ts₁ ++₁ ts₂) a
+merge []₁        f = f
+merge (t ∷₁ ts₁) f = \x -> merge ts₁ (f x)
hunk ./MultiComposition.agda 59
-        Fun (ts₁ ++ ts₂) a -> Fun ts₁ (Fun ts₂ a)
-split []        f = f
-split (t ∷ ts₁) f = \x -> split ts₁ (f x)
+        Fun (ts₁ ++₁ ts₂) a -> Fun ts₁ (Fun ts₂ a)
+split []₁        f = f
+split (t ∷₁ ts₁) f = \x -> split ts₁ (f x)
hunk ./MultiComposition.agda 64
-              (f : a -> b) (g : Fun (t ∷ ts₂) a) (h : Fun ts₁ t) ->
-              (f ⟪ t ∷ ts₂ ⟫ g) ⟪ ts₁ ⟫ h ≡
-              split ts₁ (f ⟪ ts₁ ++ ts₂ ⟫ (merge ts₁ (g ⟪ ts₁ ⟫ h)))
-right-assoc []         ts₂ f g h = ≡-refl
-right-assoc (t₁ ∷ ts₁) ts₂ f g h =
+              (f : a -> b) (g : Fun (t ∷₁ ts₂) a) (h : Fun ts₁ t) ->
+              (f ⟪ t ∷₁ ts₂ ⟫ g) ⟪ ts₁ ⟫ h ≡
+              split ts₁ (f ⟪ ts₁ ++₁ ts₂ ⟫ (merge ts₁ (g ⟪ ts₁ ⟫ h)))
+right-assoc []₁         ts₂ f g h = ≡-refl
+right-assoc (t₁ ∷₁ ts₁) ts₂ f g h =
hunk ./Wand.agda 23
+open import Data.List1
hunk ./Wand.agda 34
+  -- Wand's simple expression language with variables:
+
hunk ./Wand.agda 52
+  -- The semantics, in continuation-passing style (I would have chosen
+  -- something more easily digestible, but monads weren't available to
+  -- CS people in the early eighties):
+
hunk ./Wand.agda 101
-      E e₁ ⟪ K ∷ [] ⟫ (\κ v₁ -> E e₂ (\v₂ -> κ (v₁ + v₂)))
+      E e₁ ⟪ K ∷₁ []₁ ⟫ (\κ v₁ -> E e₂ (\v₂ -> κ (v₁ + v₂)))
hunk ./Wand.agda 103
-      E e₁ ⟪ K ∷ [] ⟫ (E e₂ ⟪ K ∷ V ∷ [] ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
-        ≡⟨ proof (E'P e₁) ⟪ K ∷ [] ⟫-cong
-             (proof (E'P e₂) ⟪ K ∷ V ∷ [] ⟫-cong ≡-refl) ⟩
-      E' e₁ ⟪ K ∷ [] ⟫ (E' e₂ ⟪ K ∷ V ∷ [] ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
+      E e₁ ⟪ K ∷₁ []₁ ⟫ (E e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
+        ≡⟨ proof (E'P e₁) ⟪ K ∷₁ []₁ ⟫-cong
+             (proof (E'P e₂) ⟪ K ∷₁ V ∷₁ []₁ ⟫-cong ≡-refl) ⟩
+      E' e₁ ⟪ K ∷₁ []₁ ⟫ (E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
hunk ./Wand.agda 108
-      E' e₁ ⟪ K ∷ [] ⟫ (E' e₂ ⟪ K ∷ V ∷ [] ⟫ add)
+      E' e₁ ⟪ K ∷₁ []₁ ⟫ (E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ add)
hunk ./Wand.agda 125
-      E e ⟪ [] ⟫ (\v σ -> v)
-        ≡⟨ proof (E'P e) ⟪ [] ⟫-cong ≡-refl ⟩
-      E' e ⟪ [] ⟫ halt
+      E e ⟪ []₁ ⟫ (\v σ -> v)
+        ≡⟨ proof (E'P e) ⟪ []₁ ⟫-cong ≡-refl ⟩
+      E' e ⟪ []₁ ⟫ halt
hunk ./Wand.agda 155
-  comp [ e₁ + e₂ ] = B (K ∷ []) (comp e₁) (B (K ∷ V ∷ []) (comp e₂) add)
+  comp [ e₁ + e₂ ] =
+    B (K ∷₁ []₁) (comp e₁) (B (K ∷₁ V ∷₁ []₁) (comp e₂) add)
hunk ./Wand.agda 197
-      {witness = B (K ∷ []) (comp' e₁) (B (K ∷ V ∷ []) (comp' e₂) add)}
+      {witness = B (K ∷₁ []₁) (comp' e₁) (B (K ∷₁ V ∷₁ []₁) (comp' e₂) add)}
hunk ./Wand.agda 199
-        Step₁.E' e₁ ⟪ K ∷ [] ⟫ (Step₁.E' e₂ ⟪ K ∷ V ∷ [] ⟫ Step₁.add)
+        Step₁.E' e₁ ⟪ K ∷₁ []₁ ⟫ (Step₁.E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ Step₁.add)
hunk ./Wand.agda 204
-        ⟦ B (K ∷ []) (comp' e₁) (B (K ∷ V ∷ []) (comp' e₂) add) ⟧
+        ⟦ B (K ∷₁ []₁) (comp' e₁) (B (K ∷₁ V ∷₁ []₁) (comp' e₂) add) ⟧
hunk ./Wand.agda 218
--- Another option is to index the Exp' type on the semantics of
--- expressions:
-
hunk ./Wand.agda 222
+  -- Step₂ can be simplified by indexing the Exp' type on the
+  -- semantics of expressions:
+
hunk ./Wand.agda 241
-  comp [ e₁ + e₂ ] = B (K ∷ []) (comp e₁) (B (K ∷ V ∷ []) (comp e₂) add)
+  comp [ e₁ + e₂ ] =
+    B (K ∷₁ []₁) (comp e₁) (B (K ∷₁ V ∷₁ []₁) (comp e₂) add)