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.
Could someone clarify the distinctions in the way LiquidHaskell handles āex1ā and āex2ā?
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?
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.
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 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!
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.
-- 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.
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.