What is a correct scope that LiquidHaskell does?

Learn
#1

I stumbled upon LiquidHaskell by chance. This refined type system appears to enhance static checks, thereby providing more robust compile-time validation.

However, I have a question regarding how it verifies the expected range of values statically. The code below illustrates the definition of a take function.

{-@ take' :: xs:[a] -> {i:Int | i < len xs} -> [a] @-}
take' :: [a] -> Int -> [a]
take' _ 0 = []
take' [] _ = []
take' (h:t) s = h : take' t (s - 1)

-- work
ex1 = take' [1,2,3,4,5] 4
-- does not work
ex2 = take' l 4
    where l = take 5 (repeat 3) -- [3,3,3,3,3]

The first example ex1 works, but not the case of ex2.

  1. Could someone clarify the distinctions in the way LiquidHaskell handles ā€˜ex1ā€™ and ā€˜ex2ā€™?
  2. I havenā€™t tested command-line inputs, file inputs, or any external inputs. I assume that external inputs should also fail if they are fed to take function as input. If this assumption is accurate, what is the appropriate context within which LiquidHaskell can be utilized, and what are the expected use cases for it?

Thank you.

1 Like
#2

Liquid Haskell by itself does not know anything about built in functions like take as used in ex2, you need to load the annotations from liquid-base to make it work. I donā€™t know exactly how to do that.

For unknown external inputs like from stdin you can always perform a run-time check, e.g. if n < length xs then Just (take' xs n) else Nothing.

1 Like
#3

I also want to learn about Liquid Haskell myself, so I tried to repro and help out as a way to learn:

I got a minimal working cabal project here liquid-intro Ā· GitHub

The code yields this error:

    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == (4 : int)}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV < len l}
    .
    in the context
      l : {l : [GHC.Num.Integer.Integer] | (not ((5 : int) >= 0) => len l == 0)
                                           && ((5 : int) >= 0 => len l == (if len ?a < (5 : int) then len ?a else (5 : int)))
                                           && len l >= 0}
       
      ?a : {?a : [GHC.Num.Integer.Integer] | len ?a >= 0}
    Constraint id 2

I canā€™t parse it myself, but I did notice if I replace that infinite list of repeat 3 with a concrete list, it works.

Intuitively, it feels like it should work, but the error message kind of makes it seem like the fact that the infinite list has no known length gets the checker ā€œstuckā€ in some way?

I am reading the tutorials now - maybe as I go, it will become clear how to program LH with infinite lists :grin: Iā€™ve worked through a similar-feeling issue in Idris years ago writing take for HList, so this will be a fun example once we figure it out Iā€™m sure!

3 Likes
#4

If Iā€™m interpreting the error correctly it is saying that it canā€™t verify that 4 is indeed less than the length of the list l. And it infers the length of l is if len ?a < (5 : int) then len ?a else (5 : int). But that leaves the possibility of the list being smaller than length 5 (the true branch of the if).

Ah, so I think the problem is that liquid-base has no refinement type for repeat saying that its length is infinite. Youā€™d want something like this:

repeat :: a -> { xs:[a] | forall n. len xs > n }

But I donā€™t think the forall quantifier is supported there. Maybe Liquid Haskell doesnā€™t work very well with inifinite data structures.

Maybe @facundominguez can help?

2 Likes
#5

Adding this makes it work:

{-@ assume repeat :: a -> { xs:[a] | len xs > 0x7FFFFFFFFFFFFFFF } @-}

But unfortunately you have to unsafely ā€œassumeā€ it.

2 Likes
#6

I guess liquid-base could hide those gutsā€¦but I think using MAX_INT here isnā€™t quite the beautiful solution I was hoping for :laughing:

1 Like
#7

Iā€™ve opened an issue about this on the liquidhaskell github repo:

1 Like
#8 
-- Per @facundominguez in this Github issue:
-- https://github.com/ucsd-progsys/liquidhaskell/issues/2218#issuecomment-1715830606
{-@ measure infinite :: Int @-}
{-@ invariant { v:Int | v <= infinite && v+infinite = infinite } @-}

{-@ assume repeat1 :: a -> { v:[a] | infinite = len v } @-}
{-@ lazy repeat1 @-}
repeat1 :: a -> [a]
repeat1 x = x : repeat1 x

^ Using this instead of repeat does work! Iā€™ve updated my gist with it.

2 Likes
#10

I never anticipated that this topic would be so intriguing. Iā€™m grateful for all of your insightful responses.

Now, I need to carefully consider how I can make the most of LiquidHaskellā€™s capabilities, aiming for a 200% improvement.

  • Annotating every function may not be practical in real world
  • LiquidHaskell may be a good contribution to the real world in various domains such as OS, network, interpreter, etc. Maybe I should think and research how it can be integrated with a specific domain, rather than a trivial implementation such as list length check, or list ordering.

Thank you very much

2 Likes
#12

Apparently there is a way! I donā€™t know reflect or --ple do yet, so I have some reading to do :cowboy_hat_face: