Non-termination, strict positivity and free monads

Question

Using the standard encoding of a free monad in Haskell and its fmap instance:

data Free f a = Pure a
              | Roll (f (Free f a))

Writing an equivalent to this in a dependently typed theory gets rejected because of the strict positivity condition.

Is it possible to cause non-termination with this encoding of a Free monad?

If this isn't the case does it point to some known relaxation of the strict positivity condition?

If this is the case is there a strictly positive datatype which acts as Free for strictly positive functors?

I don't specify the exact type theory I am working in, as some might allow addition of features to allow this. The base theory might be something like Coq's CoC.

Answer 1

Using Free, you can have a HOAS embedding of the untyped lambda calculus. And then write a structurally recursive function firing the top-level redex again and again. Good luck trying to normalise reduce omega.

{-# NO_POSITIVITY_CHECK #-}
data Free (f : Set → Set) (a : Set) : Set where
  Pure : a → Free f a
  Roll : f (Free f a) → Free f a

data LAMF (T : Set) : Set where
  App : T → T → LAMF T
  Lam : (T → T) → LAMF T

LAM : Set → Set
LAM = Free LAMF

pattern `lam b   = Roll (Lam b)
pattern `app f t = Roll (App f t)

data ⊥ : Set where

-- Type of closed term: LAM ⊥

delta : LAM ⊥
delta = `lam λ x → `app x x

omega : LAM ⊥
omega = `app delta delta

reduce : ∀ {A} → LAM A → LAM A
reduce (`app (`lam b) t) = reduce (b t)
reduce t = t