Something like measures but for types?

[Alexandru Sorodoc]

Hello,

Is there a way to define measures that have different values for different data types? For example, I want a measure to encode the size in bytes of an integer type. I though of something like this:

data Storable a where
  sizeOf :: a -> Int

{-@ measure sizeOf :: (Storable a) => a -> Int @-}

{-@ instance Storable Word8 where
      sizeOf :: Word8 -> {v:Int | v == 1}
  @-}
instance Storable Word8 where
  sizeOf _ = 1

{-@ instance Storable Word16 where
      sizeOf :: Word16 -> {v:Int | v == 2}
  @-}
instance Storable Word16 where
  sizeOf _ = 2

LH actually checks if each instance of Storable verifies its refinement. When I actually try to use sizeOf in a refinement it seems to not evaluate:

{-@ test :: (Storable a) => n:Int -> {v:a | sizeOf v == n} -> {v:Bool | v}  @-}
test :: (Storable a) => Int -> a -> Bool
test _ _ = True

f = test 1 (0 :: Word8)

f = test 1 (0 :: Word8)
            ^
   Inferred type
     VV : {v : Word8 | v == ?c
                       && v == ?b}

   not a subtype of Required type
     VV : {VV : Word8 | sizeOf VV == ?a}

   In Context
     ?c : {?c : Integer | ?c == 0}

     ?b : {?b : Word8 | ?b == ?c}

     ?a : {?a : Int | ?a == (1 : int)}

I tried using using generic measures:

{-@ class measure sizeOf :: (Storable a) => a -> Int @-}

{-@ instance measure sizeOf :: Word8 -> Int
      sizeOf (_) = 1
  @-}
instance Storable Word8 where
  sizeOf _ = 5

But fails, probably because int types are special compared to other data types:

Error: Malformed refined data constructor `()`

 154 |       sizeOf (_) = 1
             ^^^^^^^
 Requires 0 fields but given 1

[Ranjit Jhala]

Hmm the trouble is that measures are associated with data constructors and so don’t work directly on types...

It may be possible to use the “reflect” mechanism — to just use a plain fu crop . can you give an example of the program (ie some place where you want to check some constraint on sizeof) you would like to check and we can see if reflect might work?

--
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 liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Alexandru Sorodoc]

I want to write a smarted Foreign.Storable that enforces a lower bound on pointer length based on the type you are trying to read. Something like this:

import Data.Word
import Foreign.Marshal.Alloc (allocaBytes)
import qualified Foreign.Ptr as P
import qualified Foreign.Storable as S

{-@ class (S.Storable a) => Storable a where
      sizeOf :: a -> {v:Int | v > 0}
      psizeOf :: P.Ptr a -> {v:Int | v > 0}
  @-}
class (S.Storable a) => Storable a where
  sizeOf :: a -> Int
  psizeOf :: P.Ptr a -> Int

{-@ measure sizeOf :: (Storable a) => a -> {v:Int | v > 0} @-}
{-@ measure psizeOf :: (Storable a) => P.Ptr a -> {v:Int | v > 0} @-}

{-@ instance Storable Word8 where

      sizeOf :: Word8 -> {v:Int | v == 1} ;
      psizeOf :: P.Ptr Word8 -> {v:Int | v == 1}

  @-}
instance Storable Word8 where
  sizeOf _ = 1

  psizeOf _ = 1

{-@ instance Storable Word16 where

      sizeOf :: Word16 -> {v:Int | v == 2} ;
      psizeOf :: P.Ptr Word16 -> {v:Int | v == 2}

  @-}
instance Storable Word16 where
  sizeOf _ = 2

  psizeOf _ = 2

{-@ peek :: (Storable a) => p:{v:(P.Ptr a) | plen v > 0 && psizeOf v <= plen v} -> IO a @-}
peek :: (Storable a) => P.Ptr a -> IO a
peek = S.peek

test = allocaBytes 1 $ \p -> do
  -- should pass
  a <- (peek (P.castPtr p) :: IO Word8)

  -- should fail
  b <- (peek (P.castPtr p) :: IO Word16)

  return ()

Reflecting doesn't work on sizeOf/psizeOf.