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?

Decathlon

I think you need a spec file that defines some required axioms of Data.Text. I doubt liquidhaskell knows anything about Data.Text, for example fromString might not even be injective. Unfortunately I'm still digging to find out what exactly a spec file is and how to use it (I just started playing with LH today, so don't despair) – Intramuscular

Some things are said about specs and assumptions in part 4 of the tutorial. – Intramuscular

@luqui, Indeed, a file-level specification "include/Data/String.spec" must be declared, I contacted Ranjit Jhala and suggested creating a PR with this refinement in the function "Data.String.fromString". At the moment, the LH statement "{-@ assume Data.String.fromString :: x:_ -> {v:_ | v ~~ x} @-}" is sufficient. I prefer this option because it does not require altering the native haskell code. – Decathlon

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.

Intramuscular

The answer is correct, however, the declaration of denot is not necessary. {-@ assume Data.String.fromString :: x:_ -> {v:_ | v ~~ x} @-} is sufficient. – Decathlon

@RacielH, interesting, now you are teaching me. What is ~~ ? – Intramuscular

@RacielH, oh, from a little research, it looks like ~~ is supposed to be heterogeneous equality. This makes me uncomfortable, I guess I feel like although fromString s represents s, they are still not equal. However I can't come up with an example of a contradiction, and it may well be consistent as long as fromString is injective. But to me this needs to be justified -- the assumption you have given here feels very strong and should be handled carefully. – Intramuscular

Hi, @luqui. I understand your concern. If you look closely at LH the ~~ operator is widely used, for example, the specification of -- include/GHC/CString.spec includes this operator as well. Heterogeneous equality is available in GHC and is used when you are not sure that the types being compared are the same. Now, your question is very interesting considering the safety of type refinement in LH. – Decathlon

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.

Piss

this answer is also correct, however, an option that does not alter the original Haskell code is preferable. Thank you very much. – Decathlon