recursion via data-types or references makes termination checker unsound

[nikivazou]

It seems that we can encode the fixpoint or the Y combinator (ie, recursion) with data types[1]:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x))) 

Since y is not a recursive function liquidHaskell will trivially assume that y always terminates.

With y we can define our unsound example (see tests/todo/Recursion.hs):

{-@ foo :: n:Nat -> {v:Nat | v < n} @-}
foo :: Int -> Int
foo = y go
  where go f n = if n > 0 then n-1 else f n

prop = let x = 0 in
       liquidAssert ((\n -> 0==1) (foo 0))

So, maybe in the termination checker we should reason about data types like Rec,
ie recursive types that appear in negative positions. Concretely, functions that open such types should be considered as diverging.

[1] http://en.wikipedia.org/wiki/Fixed-point_combinator

[ranjitjhala]

Aargh. Yes, negative-mu’s are always a hassle (also with plain sub typing since one cannot be covariant…)

Good catch. Will have to deal with this…

On December 2, 2013 at 6:04:36 PM, Niki Vazou (notifications@github.com) wrote:

It seems that we can encode the fixpoint or the Y combinator (ie, recursion) with data types[1]:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))

Since y is not a recursive function liquidHaskell will trivially assume that y always terminates.

With y we can define our unsound example (see tests/todo/Recursion.hs):

{-@ foo :: n:Nat -> {v:Nat | v < n} @-}
foo :: Int -> Int
foo = y go
where go f n = if n > 0 then n-1 else f n

prop = let x = 0 in
liquidAssert ((\n -> 0==1) (foo 0))

So, maybe in the termination checker we should reason about data types like Rec,
ie recursive types that appear in negative positions. Concretely, functions that open such types should be considered as diverging.

[1] http://en.wikipedia.org/wiki/Fixed-point_combinator

---

Reply to this email directly or view it on GitHub:
#159

[nikivazou]

Another (maybe extreme?) example where our termination checker is unsound is in recursion via references:
tests/todo/Recursion1.hs is SAFE, but function f may diverge, where

f n = unsafePerformIO $ (unsafePerformIO bar) n

bar :: IO (Int -> IO Int)
bar  = do f <- newIORef (\_ -> return 0)
          writeIORef f (foo f)
          readIORef f

foo     :: (IORef (Int -> IO Int)) -> Int -> IO Int
foo f n  | n > 0     = return $ n-1 
         | otherwise = readIORef f >>= \g -> g n 

The credits for both the above sources of unsound termination checking go to Daan Leijen.

[gridaphobe]

That does seem quite extreme, as you'd have to infer that foo f == g before
adding the decreasing arguments constraint.

On Wednesday, December 4, 2013, Niki Vazou wrote:

Another (maybe extreme?) example where our termination checker is unsound
is in recursion via references:
tests/todo/Recursion1.hs is SAFE, but function f may diverge, where

f n = unsafePerformIO $ (unsafePerformIO bar) n

bar :: IO (Int -> IO Int)
bar = do f <- newIORef (_ -> return 0)
writeIORef f (foo f)
readIORef f

foo :: (IORef (Int -> IO Int)) -> Int -> IO Int
foo f n | n > 0 = return $ n-1
| otherwise = readIORef f >>= \g -> g n

The credits for both the above sources of unsound termination checking go
to Daan Leijen.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/159#issuecomment-29877470
.

[ranjitjhala]

Haha interesting! Surprised that LH does not crash on this program... :)

On Dec 4, 2013, at 11:45 PM, Niki Vazou notifications@github.com wrote:

Another (maybe extreme?) example where our termination checker is unsound is in recursion via references:
tests/todo/Recursion1.hs is SAFE, but function f may diverge, where

f n = unsafePerformIO $ (unsafePerformIO bar) n

bar :: IO (Int -> IO Int)
bar = do f <- newIORef (_ -> return 0)
writeIORef f (foo f)
readIORef f

foo :: (IORef (Int -> IO Int)) -> Int -> IO Int
foo f n | n > 0 = return $ n-1
| otherwise = readIORef f >>= \g -> g n
The credits for both the above sources of unsound termination checking go to Daan Leijen.

—
Reply to this email directly or view it on GitHub.

[nikivazou]

Actually my first attempt to implement it crashed, but was fixed after @gridaphobe 's edit for partial application of TyCon.

It is extreme, but I added this example mostly to document a source of unsoundness.
I suspect that IO and especially unsafePerformIO could lead to more unsound results...:(

[ranjitjhala]

I agree this is extremely good to know. Actually I would also add a link to this in the README...

On Dec 5, 2013, at 8:53 AM, Niki Vazou notifications@github.com wrote:

Actually my first attempt to implement it crashed, but was fixed after @gridaphobe 's edit for partial application of TyCon.

It is extreme, but I added this example mostly to document a source of unsoundness.
I suspect that IO and especially unsafePerformIO could lead to more unsound results...:(

—
Reply to this email directly or view it on GitHub.

[gridaphobe]

I would actually suggest splitting the IO example into a separate issue, I suspect it will be much more difficult to resolve than the negative-Mu business. I agree though that a link in the README would be good :)

[nikivazou]

I updated the title of the issue for now. It is not clear to me how to resolve any of them.
As, for the negative mu we have to propagate the no-terminating information: y opens Rec and foo diverges

[ranjitjhala]

This seems related to the covariant/contravariant discussion from earlier today?

[nomeata]

Is there a plan here? Does LH currently have a concept of unsafe types that it rejects? I guess you only want to reject these types in proofs, but not in all programs, or something...

BTW, higher rank polymorphism can also lead to recursion, so a plain positivity-checker is not sufficient.

[nikivazou]

No current plan. I think Rustan has worked around this in Dafny, but as far as I know, has not published his technique.

An idea is to always generate termination error when you have negative or higher rank types?

[nomeata]

Yeah, that’d be the conservative approach. But it is a policy decision on your (i.e. the Liquid Haskell authors) to weigh soundness-in-all-cases vs, practicality. If you document that “Liquid Haskell is not sound in the presence of negative types and higher rank types”, then there is no bug at least, and people who shoot in their foot are welcome to do so :-)

[ranjitjhala]

The conservative approach sounds good to me. We can have some mechanism to “relax” the checks for such cases if the programmer so desires?

…

On Tue, Apr 3, 2018 at 2:06 PM Joachim Breitner ***@***.***> wrote: Yeah, that’d be the conservative approach. But it is a policy decision on your (i.e. the Liquid Haskell authors) to weigh soundness-in-all-cases vs, practicality. If you document that “Liquid Haskell is not sound in the presence of negative types and higher rank types”, then there is no bug at least, and people who shoot in their foot are welcome to do so :-) — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#159 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOCvpNeRZtvVm1kiYnWK00gAA2nqiks5tk-OugaJpZM4BRVE1> .

[mgree]

We independently ran into this (per email); posting the file here for posterity. A negative occurrence check would rule out the following program:

module Omega where

import qualified Data.Map as Map
import Data.Map (Map, (!))

-- | Standard domain for LC + Bool
data D = B Bool | L (D -> D) | Wrong

instance Show D where
  show (B b) = show b
  show (L _) = "<function>"
  show Wrong = "oops"

-- | Syntax for Lambda calculus
type VarName = String
data LC =
    Var VarName
  | App LC LC
  | Lam VarName LC
  | Bool Bool
  | If LC LC LC
  deriving (Eq, Ord, Show)
{-@ data LC [size] @-}

-- | Simple size measure
--
-- >>> size (Var "x")
-- 1
-- >>> size littleOmega
-- 4
-- >>> size omega
-- 9
size :: LC -> Int
size (Var _) = 1
size (App e1 e2) = 1 + size e1 + size e2
size (Lam x e) = 1 + size e
size (Bool _) = 1
size (If e1 e2 e3) = 1 + size e1 + size e2 + size e3
{-@ measure size @-}
{-@ size :: e:LC -> {v : Nat | v = size e} @-}

type Env = Map VarName D

-- | Standard denotational model of LC + Bool
--
-- >>> eval Map.empty (Lam "x" (Var "x"))
-- <function>
-- >>> eval Map.empty (App (Lam "x" (Var "x")) (Bool True))
-- True
{-@ eval :: Env -> e:LC -> D / [ size e ] @-}
eval :: Env -> LC -> D
eval env (Var x) = env ! x
eval env (App e1 e2) =
  case eval env e1 of
    L f -> f $ eval env e2
    _ -> Wrong
eval env (Lam x e) = L $ \v -> eval (Map.insert x v env) e
eval _   (Bool b) = B b
eval env (If e1 e2 e3) =
  case eval env e1 of
    B b -> eval env (if b then e2 else e3)
    _ -> Wrong

-- | We go off the rails... Liquid Haskell said we'd be safe! :(
littleOmega, omega :: LC
littleOmega = Lam "x" (App (Var "x") (Var "x"))
omega = App littleOmega littleOmega

oops = eval Map.empty omega

[ranjitjhala]

High time we buttoned down and implemented this... [thanks for bumping it up @mgree !]

[mgree]

Side note: that file passes as safe when I use the github version, but Ron's version from cabal breaks with a bunch of weird subtype errors.

[ranjitjhala]

Adding super simple example due to Gan Shen on slack: https://liquidhaskell.slack.com/archives/C54QAL9RR/p1615244385057800

module Evil where

data Evil a = Very (Evil a -> a)

{-@ type Bot = {v: () | false} @-}

{-@ bad :: Evil Bot -> Bot @-}
bad :: Evil () -> ()
bad (Very f) = f (Very f)

{-@ worse :: Bot @-}
worse :: ()
worse = bad (Very bad)

[ranjitjhala]

@nikivazou I think it should be easy to add @mgree 's suggestion: reject datatypes with negative occurrences (maybe with an escape hatch to allow it e.g. lazy Evil or similar?