2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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
| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.