{-# OPTIONS --safe --without-K  #-}

module Lists where

open import Agda.Primitive using (_⊔_)

infixr  _∷_
data List {a} (A : Set a) : Set a where
  [] : List A
  _∷_ : A → List A → List A

module _ {a b} {A : Set a} {B : Set b} where
  foldr : (A → B → B) → B → List A → B
  foldr f b [] = b
  foldr f b (x ∷ xs) = f x (foldr f b xs)

  foldl : (B → A → B) → B → List A → B
  foldl f b [] = b
  foldl f b (x ∷ xs) = foldl f (f b x) xs

record IsList {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  field [_]  : A → List B
open IsList ⦃ ... ⦄ public

instance
  nil : ∀ {a} {A : Set a} → IsList A A
  [_] ⦃ nil ⦄ = _∷ []

infixr  _,_
record Cons {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    head : A
    tail : B

instance
  cons : ∀ {b} {B : Set b} {a} {A : Set a}
    → ⦃ _ : IsList A B ⦄
    → IsList (Cons B A) B
  [_] ⦃ cons ⦄ (x , xs) = x ∷ [ xs ]