Is there a formalism of "coinductive" data types with negative occurrences?

Question

Consider the following program in Haskell:

data T = T { num :: Int, fun :: (T -> T), tl :: T }

repeat' :: (T -> T) -> T
repeat' f = T 0 f (repeat' f)

check :: Int -> T -> Bool
check 0 t = even (num t)
check n t = not (check (n-1) (tl t))

good :: T -> T
good t
  | check 2 t = T 0 (\_ -> t') t'
  | otherwise = T 1 good (fun t t')
  where t' = tl t

bad :: T -> T
bad t
  | check 2 (fun t t) = T 0 (\_ -> t') t'
  | otherwise         = T 1 bad (fun t t')
  where t' = tl t

-- main = print $ num (tl (tl (good (repeat' good))))
main = print $ num (bad (repeat' bad))

(test with: runghc test.hs)

T is "nearly" a plain coinductive Stream of Ints, except for an infamous negative occurrence in the fun field.

good and bad are functions that differ only in what check (implementation quite irrelevant, other than it looks at the supplied T) is passed.

Both are "nearly" defined by guarded recursion if you ignore the unapplied occurrences in the otherwise clauses.

Of course, "nearly" is not quite good enough for a well-defined definition and bad goes into infinite regress while good is productive. Although both call the fun field of the input with (part of) its input, the red flag is that bad calls the fun of its input before producing a constructor, I believe.

As the call to check demonstrates (and as is compatible with the definition of guarded recursion I found here), it is OK to look at num or tl before producing. Of course, the definition of guarded recursion is not concerned about a "nearly" coinductive type like T; plus the unapplied recursive occurrence would likely be rejected anyway.

I have a function like good in practice and would like to wiggle around the domain theory excursion that's necessary to prove its well-definedness on well-defined inputs (e.g., all funs must be productive rather than otherwise continuous/partial in a weird way).

So my questions are:

1. Is there literature on "nearly" coinductive data types such as T together with a refined definition of what constitutes a definition by guarded recursion on these types? E.g., allow unapplied guarded recursive occurrences and conservatively reject unguarded uses of fields like fun with negative occurrences.
2. Perhaps one that is a compositional extension of the usual definition of coinductive data types+guarded recursion?
3. And that allows good (unless it is not as well-defined as I think) and rejects bad, of course?

---

Edit: I think guarded recursive type theory / guarded computational type theory might go a long way to relax the syntactic guardedness restriction.

Following Atkey and McBride, I came up with the following, well-typed and runnable Haskell (test with GHC >= 9.0, runghc test.hs), which unfortunately is able to type bad as well. I think the force combinator + negative types destroy totality (unfortunately I discovered quite late that they have the same positivity restriction). Nevertheless, here's what I've got.

Note that the program uses unsafeCoerce in unT for the "eta" conversion

forall k. (Int, k :|> (T -> T' k), k :|> T' k)
=>
(Int, forall k. (T -> T' k), T)

which is allowed in Atkey and McBride's system via use of (problematic) force (see deStreamCons on the bottom right of page 3).

It makes good use of some language extensions, so I'm afraid it is not for the faint of heart. It would be much simpler to do this in a language with better support for type applications and lambdas. Note that k :|> a is the $\triangleright^k$ operator, the "later" modality. The type of good is a bit awkardly putting the forall k. first rather than after the T parameter for manageable type inference.

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveFunctor #-}

import Data.Kind
import Unsafe.Coerce

data Clock
data (k :: Clock) :|> a = L a

type T = forall k. T' k
data T' (k :: Clock) where
  T' :: forall k. Int -> k :|> (T -> T' k) -> k :|> T' k -> T' k

fix' :: forall k. forall a. ((k :|> a) -> a) -> a
fix' f = x where x = f (L x)

repeat' :: forall k. (forall k'. T -> T' k') -> T' k
repeat' f = fix' (T' 0 (L f))

unT :: T -> (Int, forall k. T -> T' k, T)
unT t = unsafeCoerce (val @_ t)
  -- Currently don't see how to implement just `force` via unsafeCoerce
  where
    val :: forall k. T' k -> (Int, T -> T' k, T' k)
    val (T' num (L fun) (L tl)) = (num, fun, tl)

check :: Int -> T -> Bool
check n t
  | n == 0    = even num
  | otherwise = not (check (n-1) t')
  where (num,_,t' :: T) = unT t

good :: forall k. T -> T' k
good = fix' f
  where
    f :: k :|> (T  -> T' k) -> T -> T' k
    f good t
      | check 2 t = T' @k 0 (L (\_ -> t' @k)) (L (t' @k))
      | otherwise = T' @k 1 good (L (fun t'))
      where (_,fun,t') = unT t

bad :: forall k. T -> T' k
bad = fix' f
  where
    f :: forall k. k :|> (T  -> T' k) -> T -> T' k
    f bad t
      | check 2 (fun t) = T' @k 0 (L (\_ -> t' @k)) (L (t' @k))
      | otherwise       = T' @k 1 bad (L (fun t'))
      where (_,fun,t') = unT t

main = do
  let (num, _, _) = unT (bad (repeat' bad))
  print num

So it seems that a guarded recursive type theory is more useful than the usual notion of strictly positive coinductive types. Unfortunately, I can well-type bad as well. Bother.

Answer 1

Your datatype is a variant of the domain equation for the untyped lambda calculus. Verifying that an arbitrary untyped lambda term is normalizing is an undecidable problem, but there are undecidable type systems that can be used, specifically intersection types in the sense of Coppo and Dezani. For instance see here for how it relates to strong normalization.