Refinement type of where-bound function is not inferred with real solver

[plaidfinch]

The following function computes a symbolic convolution between the two halves of its (even-length) input list. That is, convolveHalves [1,2,3,4,5,6] = [(1,6),(2,5),(3,4)]. This algorithm is described in "There and Back Again" by Danvy & Goldberg (ICFP 2002).

{-@ LIQUID "--real" @-}
{-@ convolveHalves :: as : { [a] | (len as) mod 2 = 0 }
                   -> { pairs : [(a,a)] | len pairs = len as / 2 } @-}
convolveHalves :: [a] -> [(a,a)]
convolveHalves as =
  case walk as as of
      (r, []) -> r
  where
      -- why is this not inferred?
      {-@ walk :: as : _ -> _ -> ({ pairs : _ | len pairs = len as / 2 }, _) @-}
      walk          []       xs  = ([], xs)
      walk (_ : _ : us) (x : xs) =
        case walk us xs of
            (r, y : ys) -> ((x,y) : r, ys)

While playing with this example, @nikivazou and I realized that the --real solver flag is required to check the refinement types we needed to express. The above refinement-type-checks, but if the annotation on walk is removed, it does not. Note that we've used type holes to pare down the annotation so it includes only the pieces which are necessary to get LH to accept it. It seems that this annotation should not be necessary—it is of the exact same form as a portion of the function's top-level refinement type: shouldn't it be tried as an instantiation during inference?

A similar but slightly simpler example does not require such annotation:

{-@ convolve ::      as:[a]
             -> {    bs:[b]     | len bs    = len as }
             -> { pairs:[(a,b)] | len pairs = len as } @-}
convolve :: [a] -> [b] -> [(a,b)]
convolve xs ys =
   case walk xs of
      (r, []) -> r
   where
      walk      []  = ([], ys)
      walk (a : as) =
         case walk as of
            (r, b : bs) -> ((a,b) : r, bs)

[ranjitjhala]

Interesting example, thanks! The reason its not getting inferred is that the two as have different types, namely [(a, a)] and [t] -- one is a list of pairs and the other is just a list. Currently the way the qualifiers are generated for inference/instantiation they are only "matched" or instantiated for variables of similar (unifiable) types. Here, we cannot "instantiate" forall a. [(a, a)] to obtain [t] hence the pattern/qualifier is not tried.

Thus, the following works fine, as the pattern is generalized.

{-@ LIQUID "--real" @-}
{-@ convolveHalves :: as : { [a] | (len as) mod 2 = 0 }
                   -> { pairs : [(a,a)] | len pairs = len as / 2 } @-}
convolveHalves :: [a] -> [(a,a)]
convolveHalves as =
  case walk as as of
      (r, []) -> r
  where
      -- Now this _is_ inferred
      walk          []       xs  = ([], xs)
      walk (_ : _ : us) (x : xs) =
        case walk us xs of
            (r, y : ys) -> ((x,y) : r, ys)

-- added to get qualifier
{-@ dummy :: xs:[a] -> {v : _ | len v = len xs / 2 } @-}
dummy :: [a] -> [b]
dummy = undefined

At any rate, this is a great example -- it should be possible for us to "generalize" the types of binders appearing in the refinements to not have to write dummy, and make the pattern extraction more robust. Thanks!

[nikivazou]

Thanks @kwf!

I though the type of convolve was convolve :: [a] -> [a] -> [(a,a)], it is always called with same types right?

BTW, I suggest we make the --real the default behavior!

[ranjitjhala]

@nikivazou -- sure, can you see how that affects the regrtests? Thanks!

On Mon, Feb 8, 2016 at 3:51 PM, Niki Vazou notifications@github.com wrote:

Thanks @kwf https://github.com/kwf!

I though the type of convolve was convolve :: [a] -> [a] -> [(a,a)], it is always called with same types right?

BTW, I suggest we make the --real the default behavior!

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/609#issuecomment-181629373 .

[plaidfinch]

You're welcome! If I get a chance, I'll see what it takes to code up some of the even more complex patterns from that paper in LH—there are some fun ones that end up in "triangular" lists-of-lists and such.

@ranjitjhala: That makes a lot of sense. And, that generalization would totally be a neat feature—I bet it's not the only natural place where inference could benefit from that technique.

@nikivazou: convolve doesn't need to have type [a] -> [a] -> [(a,a)]; it can take two differently-typed lists. But convolveHalves needs to have type [a] -> [(a,a)], because it convolves one half of a list with the other half.

[ranjitjhala]

@nikivazou this should be "easy" with the generalize in fixpoint. Start with a qual, give each param a fresh tyvar, then do sort-check and use the inferred types as the actual parameters.