# Non-termination, strict positivity and free monads

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.

• In "Efficient Mendler-Style Lambda-Encodings in Cedille", at the end of Chapter 4.1 they show how having a non-positive functor will lead to inconsistency. I think the same applies to Free. Feb 24, 2020 at 7:18
• Do you mean Pure a? Feb 25, 2020 at 8:08
• @Nift As for the strictly positive variant of Free, I'd suggest reading Dylus' 'One Monad To Prove Them All' Feb 27, 2020 at 22:02

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
`