A simple case where LiquidHaskell works well on the type "Data.String" but not on the type "Data.Text"

Question

The problem

I've been very excited playing with LiquidHaskell, however, I don't know to what extent I need to modify my original Haskell code to meet LiquidHaskell's requirements.

Here is a simple example of how Liquid's specifications work well for String type but not for Text type.

For String type it works well

Example

I define a Liquid type where we say that the values of a tuple cannot be the same:

{-@ type NoRouteToHimself = {v:(_, _) | (fst v) /= (snd v)} @-}

Then, for a String type specification it works well as shown below:

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = ("AA", "AB")

LiquidHaskel Output >> RESULT: SAFE

{-@ strBad :: NoRouteToHimself @-}
strBad :: (String, String)
strBad = ("AA", "AA")

LiquidHaskel Output >> RESULT: UNSAFE

So far so good, let's define the same function for the Text type.

For the Text type it goes wrong

Example

{-# LANGUAGE OverloadedStrings #-}
import qualified Data.Text as Tx

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = ("AA", "AB")

Expected Result: RESULT: SAFE

LiquidHaskell Output: RESULT: UNSAFE

 ..Example.hs:102:3-5: Error: Liquid Type Mismatch
  
 102 |   foo = ("AA", "AB")
         ^^^
  
   Inferred type
     VV : {v : (Data.Text.Internal.Text, Data.Text.Internal.Text) | x_Tuple22 v == ?a
                                                                    && x_Tuple21 v == ?b
                                                                    && snd v == ?a
                                                                    && fst v == ?b}
  
   not a subtype of Required type
     VV : {VV : (Data.Text.Internal.Text, Data.Text.Internal.Text) | fst VV /= snd VV}
  
   In Context
     ?b : Data.Text.Internal.Text
      
     ?a : Data.Text.Internal.Text

Apparently LiquidHaskell cannot evaluate the values of the tuple for this case. Any suggestions?

Answer 1

After some playing around, I have found a way you can do this. I don't know of a way that preserves the polymorphism of NoRouteToHimself, but there is, at least, a way to speak about equality of Data.Text objects.

The technique is to introduce a denotation measure. That is, a Text is really just a fancy way of representing a String, so we should in principle be able to use String reasoning on Text objects. So we introduce a measure to get what the Text represents:

{-@ measure denot :: Tx.Text -> String @-}

When we construct a Text from a String, we need to say that the Text's denotation is the String we passed in (this encodes injectivity, with denot playing the role of the inverse).

{-@ assume fromStringL :: s:String -> { t:Tx.Text | denot t == s } @-}
fromStringL = Tx.pack

Now when we want to compare equality of different Texts in LH, we instead compare their denotations.

{-@ type NoRouteToHimself = v:(_,_) : denot (fst v) /= denot (snd v) @-}

And now we can get the example to pass:

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (fromStringL "AA", fromStringL "AB")

To use other functions of Data.Text in LH, one would need to give denotational specifications to those functions. It is some work, but I think it would be a worthwhile thing to do.

I'm curious if there are ways to make this treatment more polymorphic and reusable. I also wonder if we can overload LH's notion of equality so that we don't have to go through denot. There is much to learn.

Answer 2

Liquid Haskell works by exploiting primitive Haskell constructors. The String code is sugar for

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = (,) ('A':'A':[]) ('A':'B':[])

and Liquid Haskell knows how to unravel / recurse those constructors away. But Data.Text is not defined in terms of Haskell constructors, rather it uses an opaque conversion function – the -XOverloadedStrings extension inserts it:

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (Tx.pack "AA", Tx.pack "AB")

Here, Liquid Haskell doesn't know how Tx.pack works, whether it yields anything deconstructible in its output. A simpler example where it also doesn't succeed is (without -XOverloadedStrings)

{-@ foo :: NoRouteToHimself @-}
foo' :: (String, String)
foo' = (reverse "AA", reverse "AB")

To make this work, LH would need to know at least that Tx.pack and reverse are injective. I don't know enough about LH to tell if it's possible to achive that. Perhaps forcing it to inline the conversion function would do the trick. Short of that, the only option would be to NF the value and call the actual == operator on it – which would work fine in this particular case, but would be impossible for the non-trivial use cases that LH is actually supposed to do.