TerminationRecordPatternLie.agda

-- 2010-10-05 Andreas

module TerminationRecordPatternLie where

data Empty : Set where

record Unit : Set where

data Bool : Set where
  true false : Bool

T : Bool -> Set
T true = Unit
T false = Empty

-- Thorsten suggests on the Agda list  thread "Coinductive families"
-- to encode lists as records
record List (A : Set) : Set where
  constructor list
  field
    isCons : Bool
    head   : T isCons -> A
    tail   : T isCons -> List A

open List public

-- However, we have to be careful to preserve termination
-- in the presence of a lie

postulate
  lie : {b : Bool} -> T b

-- this function is rejected
f : {A : Set} -> List A -> Empty
f (list b h t) = f (t lie)

-- since its internal representation is
g : {A : Set} -> List A -> Empty
g l = g (tail l lie)

-- however could record constructors still count as structural increase
-- if they cannot be translated away
-- should we accept this?
--   f (list true h t) = f (t _)