matFromList solution using measure and possible bug with Applicative

[Alexandru Sorodoc]

Hello everyone.

I was going through the Dimension Safe Matrix API chapter of the book and I encountered a problem with the matFromList exercise. In order to solve it I have to ensure that all the rows have the same number of colums (<=> all the sublists in the input have the same length) and there is a hint about using a measure. Here is a MWE:

module MatMult where

{-@ type Pos = {v:Int | 0 < v} @-}

{-@ measure size @-}
{-@ size    :: xs:[a] -> {v:Nat | v = size xs} @-}
size :: [a] -> Int
size []     = 0
size (_:rs) = 1 + size rs

type List a = [a]

{-@ type ListN a N = {v:List a | size v = N} @-}
{-@ type ListX a X = ListN a {size X}        @-}

{-@ map'      :: (a -> b) -> xs:List a -> ListX b xs @-}
map' _ []     = []
map' f (x:xs) = f x : map' f xs

{-@ data Vector a = V { vDim :: Nat , vElts :: ListN a vDim } @-}
data Vector a = V { vDim :: Int, vElts :: [a] } deriving (Eq, Show)

{-@ vDim :: x:_ -> {v:Nat | v = vDim x} @-}
{-@ type VectorNE a  = {v:Vector a | vDim v > 0} @-}
{-@ type VectorN a N = {v:Vector a | vDim v = N} @-}
{-@ type VectorX a X = VectorN a {vDim X}        @-}

{-@ data Matrix a =
      M { mRow  :: Pos
        , mCol  :: Pos
        , mElts :: VectorN (VectorN a mCol) mRow
        }
  @-}
data Matrix a = M
  { mRow :: Int
  , mCol :: Int
  , mElts :: Vector (Vector a)
  } deriving (Eq, Show)

{-@ type MatrixN a R C   = {v:Matrix a | Dims v R C } @-}
{-@ predicate Dims M R C = mRow M = R && mCol M = C   @-}

{-@ matFromList :: xss:[[a]] -> Maybe (MatrixN a (size xss) (??)) @-}
matFromList      :: [[a]] -> Maybe (Matrix a)
matFromList []   = Nothing
matFromList xss@(xs:_)
  | ok           = Just (M r c vs)
  | otherwise    = Nothing
  where
    r            = size xss
    c            = size xs
    ok           = r > 0 && c > 0
    vs           = undefined

{-@ mat23 :: Maybe (MatrixN Integer 2 2) @-}
mat23     = matFromList [ [1, 2]
                        , [3, 4] ]

My first though was to write a measure for [[a]] that would determine if all the sublists have the same length, something like the following, but it produces an error:

{-@ measure columns @-}
columns :: [[a]] -> Int
columns [] = -1
columns (x:xs) = if r == -1 || c == r then c else -2
  where
    c = size x
    r = columns xs

{-@ matFromList :: xss:[[a]] -> Maybe (MatrixN a (size xss) (columns xss)) @-}
matFromList      :: [[a]] -> Maybe (Matrix a)
matFromList []   = Nothing
matFromList xss@(xs:_)
  | ok           = Just (M r c vs)
  | otherwise    = Nothing
  where
    r            = size xss
    c            = size xs
    ok           = r > 0 && c > 0 && columns xss > 0
    vs           = V r $ map' (V c) xss

**** RESULT: ERROR *************************************************************


 <no source information>:0:0: Error: Illegal type specification for `constructor GHC.Types.:`
     constructor GHC.Types.: :: head:a -> tail:[{VV : a | true}] -> {VV : [a] | columns VV == (if columns tail == (-1)
                                                                                                  || size head == columns tail then size head else -2)
                                                                                && size VV == 1 + size tail
                                                                                && len VV == 1 + len tail
                                                                                && tail VV == tail
                                                                                && head VV == head}
     Sort Error in Refinement: {VV : [a##11] | ((((MatMult.columns VV == (if MatMult.columns tail##GHC.Types.: == (-1)
                                                                             || MatMult.size head##GHC.Types.: == MatMult.columns tail##GHC.Types.: then MatMult.size head##GHC.Types.: else -2)
                                                   && MatMult.size VV == 1 + MatMult.size tail##GHC.Types.:)
                                                  && len VV == 1 + len tail##GHC.Types.:)
                                                 && tail VV == tail##GHC.Types.:)
                                                && head VV == head##GHC.Types.:)}
     Cannot unify a##11 with [@(42)] in expression: MatMult.columns VV << ceq2 >>


 <no source information>:0:0: Error: Illegal type specification for `constructor GHC.Types.[]`
     constructor GHC.Types.[] :: {VV : [a] | columns VV == (-1)
                                             && size VV == 0
                                             && len VV == 0}
     Sort Error in Refinement: {VV : [a##11] | ((MatMult.columns VV == (-1)
                                                 && MatMult.size VV == 0)
                                                && len VV == 0)}
     Cannot unify a##11 with [@(42)] in expression: MatMult.columns VV << ceq2 >>

I don't know if this error is expected or not. I tried all sorts of things using measures but none worked. My question is: for what data structure should the measure be written?

I eventually found a solution that avoids using a measure and that works, but it has a small quirk:

{-@ test :: n:Nat -> xs:[[a]] -> Maybe (ListX (ListN a n) xs) / [size xs] @-}
test :: Int -> [[a]] -> Maybe [[a]]
test _ [] = Just []
test c (x:xs) = if size x == c then (x:) <$> (test c xs) else Nothing

{-@ matFromList :: xss:[[a]] -> Maybe (MatrixN a (size xss) (size (head xss))) @-}
matFromList      :: [[a]] -> Maybe (Matrix a)
matFromList []   = Nothing
matFromList xss@(xs:_)
  | ok           = M r c <$> vs
  | otherwise    = Nothing
  where
    r            = size xss
    c            = size xs
    ok           = r > 0 && c > 0
    vs           = V r . map' (V c) <$> test c xss


I want to bring your attention to the last line. The first time I wrote it, it was:

    vs           = V r <$> map' (V c) <$> test c xss

Which caused this ugly error:

**** RESULT: ERROR *************************************************************


 /home/alex/uni/disertatie-master/liquid-haskell-test/app/matmult.hs:76:20-52: Error: Uh oh.

 76 |     vs           = V r <$> map' (V c) <$> test c xss
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

     addC: malformed constraint:
{lq_tmp$x##6268 : lq_tmp$x##6272:[{lq_tmp$x##6255 : [{lq_tmp$x##6252 : a^"lq_tmp$x##6116" | $k_##6115[VV##6121:=lq_tmp$x##6255][lq_tmp$x##6110:=lq_anf$##7205759403792803473##d2zf][lq_tmp$x##6124:=lq_tmp$x##6252][lq_tmp$x##6101:=lq_tmp$x##6261][lq_tmp$x##6127:=lq_tmp$x##6255][VV##6114:=lq_tmp$x##6252]}]^"lq_tmp$x##6123" | $k_##6122[VV##6121:=lq_tmp$x##6255][lq_tmp$x##6110:=lq_anf$##7205759403792803473##d2zf][lq_tmp$x##6101:=lq_tmp$x##6261][lq_tmp$x##6127:=lq_tmp$x##6255]}] -> {lq_tmp$x##6267 : [{lq_tmp$x##6263 : (Vector {lq_tmp$x##6262 : a^"lq_tmp$x##6130" | $k_##6129[VV##6131:=lq_tmp$x##6263][VV##6128:=lq_tmp$x##6262][lq_tmp$x##6134:=lq_tmp$x##6262][lq_tmp$x##6135:=lq_tmp$x##6263][lq_tmp$x##6110:=lq_anf$##7205759403792803473##d2zf][lq_tmp$x##6111:=lq_tmp$x##6272][lq_tmp$x##6105:=lq_tmp$x##6267]})^"lq_tmp$x##6133" | $k_##6132[VV##6131:=lq_tmp$x##6263][lq_tmp$x##6135:=lq_tmp$x##6263][lq_tmp$x##6110:=lq_anf$##7205759403792803473##d2zf][lq_tmp$x##6111:=lq_tmp$x##6272][lq_tmp$x##6105:=lq_tmp$x##6267]}] | MatMult.size lq_tmp$x##6267 == MatMult.size lq_tmp$x##6272} | lq_tmp$x##6268 == lq_anf$##7205759403792803474##d2zg}
 <:
(-> LiftedRep LiftedRep [[a]] {lq_tmp$x##6209 : [{lq_tmp$x##6205 : (Vector {lq_tmp$x##6204 : a^"lq_tmp$x##6190" | $k_##6189[lq_tmp$x##6163:=lq_anf$##7205759403792803472##d2ze][lq_tmp$x##6162:=lq_anf$##7205759403792803471##d2zd][VV##6188:=lq_tmp$x##6204][VV##6201:=lq_tmp$x##6209][VV##6191:=lq_tmp$x##6205]})^"lq_tmp$x##6193" | $k_##6192[lq_tmp$x##6163:=lq_anf$##7205759403792803472##d2ze][lq_tmp$x##6162:=lq_anf$##7205759403792803471##d2zd][VV##6201:=lq_tmp$x##6209][VV##6191:=lq_tmp$x##6205]}]^"lq_tmp$x##6203" "lq_tmp$x##135" | $k_##6202[lq_tmp$x##6163:=lq_anf$##7205759403792803472##d2ze][lq_tmp$x##6162:=lq_anf$##7205759403792803471##d2zd][VV##6201:=lq_tmp$x##6209]})

Chaning it to one of the following avoids that error:

V r . map' (V c) <$> test c xss
V r <$> (map' (V c) <$> test c xss)

All 3 variants are functionally equivalent, so I assume this is a bug in LH?

[Ranjit Jhala]

Hi Alexandru, 

yes that is definitely a bug! I suspect the crashing variant generates some GHC core (with the LiftedRep) that causes the problem. Could you please post that minimal example as an issue in the LH repo?

 The “test” solution is indeed the one I had in mind, so I’m very glad you found that :)

Unfortunately one cannot use a measure here, due to a weird bug in the implementation of measures ... still the error message is terrible, and I’d be very grateful if you could post that as a separate issue too!

Many Thanks!

- Ranjit.

--
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]

Hello Ranjit,

Thanks for the reply! I will see if I can minimize the examples more and post the issues on github.