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?
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.