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 Int
s, 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 fun
s must be productive rather than otherwise continuous/partial in a weird way).
So my questions are:
- 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 likefun
with negative occurrences. - Perhaps one that is a compositional extension of the usual definition of coinductive data types+guarded recursion?
- And that allows
good
(unless it is not as well-defined as I think) and rejects bad, of course?