<p>Using <code>Free</code>, 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 <code>reduce omega</code>.</p>

<pre><code>{-# 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
</code></pre>

CC BY-SA 4.0
2020-02-27T13:30:38.337Z
2020-02-27T13:30:38.337Z
gallais
<p>Using the standard encoding of a free monad in Haskell and its <code>fmap</code> instance:</p>



<pre><code>data Free f a = Pure a
              | Roll (f (Free f a))
</code></pre>

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

<p>Is it possible to cause non-termination with this encoding of a <code>Free</code> monad?</p>

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

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

<p>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.</p>

CC BY-SA 4.0
2020-02-24T07:18:50.787Z
In ["Efficient Mendler-Style Lambda-Encodings in Cedille"](https://arxiv.org/pdf/1803.02473.pdf), 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`.
Labbekak
CC BY-SA 4.0
2020-02-25T08:08:40.513Z
Do you mean `Pure a`?
András Kovács
CC BY-SA 4.0
2020-02-27T22:02:19.047Z
@Nift As for the strictly positive variant of `Free`, I'd suggest reading Dylus' ['One Monad To Prove Them All'](https://arxiv.org/abs/1805.08059)
gallais
<type-theory><dependent-type><monad>
Non-termination, strict positivity and free monads
Ilk
# Non-termination, strict positivity and free monads

(Asked by: username_0 on 2020-02-24)

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.

**Tags:** type-theory, dependent-type, monad
> **Comments:**
> **username_1**: In ["Efficient Mendler-Style Lambda-Encodings in Cedille"](https://arxiv.org/pdf/1803.02473.pdf), 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`.  
> **username_2**: Do you mean `Pure a`?  
> **username_3**: @Nift As for the strictly positive variant of `Free`, I'd suggest reading Dylus' ['One Monad To Prove Them All'](https://arxiv.org/abs/1805.08059)  

---

## 1 answers

### Answer by username_3 on 2020-02-27. Score: 2 | Accepted answer

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


---

