A liquid type alias not refining a Haskell type alias

[Rob Stewart]

Hi,

This is my first attempt to tip my toe into liquid haskell. Here's my code:

import Data.Array
import Data.Array.IArray
import Data.Int

-- this liquid type alias does not appear to refine the Haskell type alias below.
{-@ type Image = Array (Int,Int) {p:Int | p <= 255} @-}
type Image = Array (Int,Int) Int

{-@ brighten :: Image -> Image @-}
brighten :: Image -> Image
brighten image = amap brightenPixel image

{-@ brightenPixel :: pIn:{Int | pIn <= 255} ->  {pOut:Int | (pOut >= pIn && pOut <= 255) } @-}
brightenPixel :: Int  -> Int
brightenPixel pixel = min 255 (pixel + 50)

What I want to prove is that the input and returned arrays for the `brighten` function holds element values never greater than 255. However, the liquid haskell error I'm getting is:

**** RESULT: UNSAFE ************************************************************

 src/Lib.hs:13:18-41: Error: Liquid Type Mismatch
 
 13 | brighten image = amap brightenPixel image
                       ^^^^^^^^^^^^^^^^^^^^^^^^
   Inferred type
     VV : GHC.Types.Int
 
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV <= 255}
 
   In Context

 src/Lib.hs:13:23-35: Error: Liquid Type Mismatch
 
 13 | brighten image = amap brightenPixel image
                            ^^^^^^^^^^^^^
   Inferred type
     VV : GHC.Types.Int
 
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV <= 255}
 
   In Context

Where am I going wrong, and what liquid haskell annotations am I missing?

Thanks,

--

Rob

[Niki Vazou]

Well, you are not doing anything wrong, it has to do with type class constrains. 

Here is a version that works 

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1484736747_22226.hs

The problem is that in your initial version the type of `amap` is 

amap :: (IArray a e', IArray a e, Ix i) => (e' -> e) -> a i e' -> a i e

For (soundness of) Liquid Haskell, the fact that the type variables e and e' are constraint by class constrains means that `amap` could create arbitrary values of type `e` and thus Liquid Haskell does not instantiate `e` with your desired refinement type {Int | pIn <= 255}. 

The "fix"  in the link above is to create a `mapArray` instance of `amap` without class constrains on `e`, that is (in the above link)

mapArray ::(Ix a) =>  (e' -> e) -> Array a e' -> Array a e  

mapArray = amap 

The above type holds  _for any_ types `e` and `e'`. In your code both `e` and `e'` will get instantiated in your desired refinement type {Int | pIn <= 255} and verification succeeds. 

If you want to learn more about this problem you can take a look at pg 4, paragraph "Parametric Invariants and Type Classes" of http://goto.ucsd.edu/~rjhala/liquid/abstract_refinement_types.pdf 

Best,

Niki

 

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Niki