DataRecordInductive.agda

module DataRecordInductive where

module NotMutual where

  record Nil (A : Set) : Set where
    constructor []

  record Cons (A X : Set) : Set where
    constructor _∷_
    field head : A
          tail : X
  open Cons

  data List (A : Set) : Set where
    nil  : Nil A  → List A
    cons : Cons A (List A) → List A

  -- works
  module Constr where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   [])      = nil []
    map f (cons (x ∷ xs)) = cons (f x ∷ map f xs)

  -- works, since projections are size preserving
  module Proj where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   _) = nil []
    map f (cons  p) = cons (f (head p) ∷ map f (tail p))

module Mutual where

  mutual

    data List (A : Set) : Set where
      nil  : Nil A  → List A
      cons : Cons A → List A

    record Nil (A : Set) : Set where
      constructor []

    -- since Cons is inductive, we are not creating colists
    record Cons (A : Set) : Set where
      inductive
      constructor _∷_
      field head : A
            tail : List A

  open Cons

  -- works
  module Constr where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   [])      = nil []
    map f (cons (x ∷ xs)) = cons (f x ∷ map f xs)

  -- works, since projections of an inductive record are size-preserving
  module Proj where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   _) = nil []
    map f (cons  p) = cons (f (head p) ∷ map f (tail p))