> |- {v:Count b | count v == count x + count y} <: Count b <>}
Count a <

>) -> Count b <> ;
>> :: x:Count a -> y:Count b -> {v:Count b | count v == count x + count y};
return :: a -> {v:Count a | count v == 0 }
@-}
return x = let r = Count x in assertCount 0 (Count x)
(Count x) >>= f = let r = f x in assertCount (getCount (Count x) + getCount r) r
x >> y = assertCount (getCount x + getCount y) y
fail = error
{-@ assume assertCount :: i:Int -> x:Count a -> {v:Count a | v == x && count v == i } @-}
assertCount :: Int -> Count a -> Count a
assertCount _ x = x
{-@ assume getCount :: x:Count a -> {v:Int | v == count x } @-}
getCount :: Count a -> Int
getCount _ = 0
{-@ makeCount :: x:a -> {v:Count a | v == Count x} @-}
makeCount = Count
{-@ assume incr :: a -> {v:Count a | count v == 1 } @-}
incr :: a -> Count a
incr = Count
{-@ assume unit :: {v:Count () | count v == 0 } @-}
unit = Count ()
{-@ foo :: a -> {v:Count a | count v == 0 } @-}
foo :: a -> Count a
foo y = return y
{-@ test1 :: {v:Count () | count v == 0 } @-}
test1 :: Count ()
test1 = do
unit
unit
unit
{-@ test2 :: {v:Count () | count v == 1 } @-}
test2 = do
unit
y <- incr ()
unit
foo y
unit
{-@ test3 :: {v:Count () | count v == 2 } @-}
test3 = do
unit
unit
incr ()
incr ()
unit