added Notes

Notes.md

@@ -0,0 +1,28 @@
+# Notes
+
+## PHOAS
+
+The following comments were collected on the Agda mailing list.
+
+* Nils Anders Danielsson <nad@cse.gu.se>
+  + cites Chlipala, who uses binary parametricity
+    - http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html 
+    - http://adam.chlipala.net/cpdt/html/Intensional.html
+
+* Roman <effectfully@gmail.com>
+  + (similar to my solution)
+    - https://github.com/effectfully/random-stuff/blob/master/Normalization/PHOAS.agda
+    - https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda
+  + also cites Abel's habilitation
+    -  http://www.cse.chalmers.se/~abela/habil.pdf
+
+* András Kovács <kovacsahun@hotmail.com>
+  + applies unary parametricity
+    - http://lpaste.net/363029
+
+* Ulf Norell <ulf.norell@gmail.com>
+  + helped with deriving Eq
+
+* David Darais (not on mailing list)
+  + suggests Scoped PHOAS
+    - https://plum-umd.github.io/darailude-agda/SF.PHOAS.html

src/Lists.lagda

@@ -85,23 +85,29 @@ cons respectively, allowing a more efficient representation of lists.
 
 We can write lists more conveniently by introducing the following definitions.
 \begin{code}
-[_] : ∀ {A : Set} → A → List A
+-- [_] : ∀ {A : Set} → A → List A
-[ z ] = z ∷ []
+-- pattern [ z ] = z ∷ []
+pattern [_] z = z ∷ []
 
-[_,_] : ∀ {A : Set} → A → A → List A
+-- [_,_] : ∀ {A : Set} → A → A → List A
-[ y , z ] = y ∷ z ∷ []
+-- pattern [ y , z ] = y ∷ z ∷ []
+pattern [_,_] y z = y ∷ z ∷ []
 
-[_,_,_] : ∀ {A : Set} → A → A → A → List A
+-- [_,_,_] : ∀ {A : Set} → A → A → A → List A
-[ x , y , z ] = x ∷ y ∷ z ∷ []
+-- pattern [ x , y , z ] = x ∷ y ∷ z ∷ []
+pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
 
-[_,_,_,_] : ∀ {A : Set} → A → A → A → A → List A
+-- [_,_,_,_] : ∀ {A : Set} → A → A → A → A → List A
-[ w , x , y , z ] = w ∷ x ∷ y ∷ z ∷ []
+-- pattern [ w , x , y , z ] = w ∷ x ∷ y ∷ z ∷ []
+pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
 
-[_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → List A
+-- [_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → List A
-[ v , w , x , y , z ] = v ∷ w ∷ x ∷ y ∷ z ∷ []
+-- pattern [ v , w , x , y , z ] = v ∷ w ∷ x ∷ y ∷ z ∷ []
+pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
 
-[_,_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → A → List A
+-- [_,_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → A → List A
-[ u , v , w , x , y , z ] = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
+-- pattern [ u , v , w , x , y , z ] = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
+pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
 \end{code}
 Agda recognises that this is a bracketing notation,
 and hence we can write things like `length [ 0 , 1 , 2 ]`
@@ -129,8 +135,8 @@ tail the same as the tail of the first list appended to the second list.
 Here is an example, showing how to compute the result
 of appending two lists.
 \begin{code}
-ex₁ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ]
+_ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ]
-ex₁ =
+_ =
   begin
     0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []
   ≡⟨⟩
@@ -240,8 +246,8 @@ is one greater than the length of the tail of the list.
 
 Here is an example showing how to compute the length of a list.
 \begin{code}
-ex₂ : length [ 0 , 1 , 2 ] ≡ 3
+_ : length [ 0 , 1 , 2 ] ≡ 3
-ex₂ =
+_ =
   begin
     length (0 ∷ 1 ∷ 2 ∷ [])
   ≡⟨⟩
@@ -316,8 +322,8 @@ containing its head.
 
 Here is an example showing how to reverse a list.
 \begin{code}
-ex₃ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
+_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
-ex₃ =
+_ =
   begin
     reverse (0 ∷ 1 ∷ 2 ∷ [])
   ≡⟨⟩