Church datatype encoding in Agda

Church.agda

-- Make Agda as unsafe as Haskell is
{-# OPTIONS
  --type-in-type
  --no-termination-check #-}

-- `type-in-type` for impredicative Π-types (Set → Set : Set)
-- `no-termination-check` for blowing up

module Church where

-- {-
-- Standard library
open import Data.Nat using (ℕ ; _+_ ; zero) renaming (suc to succ)
open import Function using (_∘_ ; _$_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-- -}

-- Maybe
Maybe : Set → Set
Maybe A = (X : Set) → (A → X) → X → X

just : {A : Set} → A → Maybe A
just a = λ _ f z → f a

nothing : {A : Set} → Maybe A
nothing = λ _ f z → z

maybe-e : {A X : Set} → (A → X) → X → Maybe A → X
maybe-e f z m = m _ f z

-- Product
infixr 5 _×_
_×_   : Set → Set → Set
A × B = (X : Set) → (A → B → X) → X

infixr 5 _,_
_,_ : {A B : Set} → A → B → A × B
a , b = λ _ f → f a b

fst : {A B : Set} → A × B → A
fst p = p _ (λ a b → a)

snd : {A B : Set} → A × B → B
snd p = p _ (λ a b → b)

×-e : {A B X : Set} → (A → B → X) → A × B → X
×-e f p = p _ f

-- List
List : Set → Set
List A = (X : Set) → (A → X → X) → X → X
  
list-e : {A X : Set} → (A → X → X) → X → List A → X
list-e {A} {X} f z as = as X f z
  
nil : {A : Set} → List A
nil X f z = z
  
cons : {A : Set} → A → List A → List A
cons a as X f z = f a (as X f z)

-- Using Kleene hack
break : {A : Set} → List A → Maybe (A × List A)
break {A} as = fst (list-e (λ a → ×-e (λ x y → just (a , y) , cons a y)) (nothing , nil) as)

-- Note that
--   reverse as = foldr (λ a f → f ∘ cons a) id as []
-- this term uses the same trick.
zip : {A B : Set} → List A → List B → List (A × B)
zip {A} {B} as′ bs′ =
    fst (list-e
      (λ _ → ×-e (λ rev → ×-e (λ as bs → body as bs rev)))
      ((λ x → x) , as′ , bs′) -- 
      as′) -- Theoretically we need the longer list here,
           -- but zip stops at the end of the shorter list,
           -- so both as′ and bs′ would work.
    nil
  where
  body : List A → List B → (List (A × B) → List (A × B))
       → ((List (A × B) → List (A × B)) × List A × List B)
{-
  case₂ ea eb =
    case ea of
      (a ∷ as) → case eb of
        (b ∷ bs) → bothOk   -- FV = {a , as , b , bs}
        nil → ebIsNil       -- FV = {a , as}
      nil → eaIsNil         -- FV = {}
-}
  body ea eb rev =
    maybe-e
      (×-e (λ a as → maybe-e
        (×-e (λ b bs → bothOk a as b bs))
        (ebIsNil a as)
        (break eb)))
      eaIsNil
      (break ea)
    where
    eaIsNil = rev , nil , nil
    ebIsNil = λ a as → rev , nil , nil
    bothOk = λ a as b bs → rev ∘ cons (a , b) , as , bs

zipWith : {A B C : Set} → (A → B → C) → List A → List B → List C
zipWith f as = list-e (λ p rest → ×-e (λ a b → cons (f a b) rest) p) nil ∘ zip as

infixr 5 _∷_
data DList (A : Set) : Set where
  [] : DList A
  _∷_ : A → DList A → DList A

fromD : {A : Set} → DList A → List A
fromD [] = nil
fromD (a ∷ as) = cons a (fromD as)

toD : {A : Set} → List A → DList A
toD as = list-e _∷_ [] as

take : {A : Set} → ℕ → DList A → DList A
take zero     _        = []
take (succ n) []       = []
take (succ n) (a ∷ as) = a ∷ (take n as)

zipWith′ : {A B C : Set} → (A → B → C) → DList A → DList B → DList C
zipWith′ f as bs = toD (zipWith f (fromD as) (fromD bs))

-- Work:
test₁ : zipWith′ _+_ (1 ∷ 2 ∷ []) (1 ∷ 2 ∷ 3 ∷ []) ≡ 2 ∷ 4 ∷ []
test₁ = refl

ones : DList ℕ
ones = 1 ∷ ones

test₂ = take 1 ones

test₃ = take 1 ∘ toD ∘ fromD $ ones

-- Blows up:
testBlowMe = take 1 $ zipWith′ _+_ ones (1 ∷ 2 ∷ 3 ∷ [])