Unsafe type error

[william....@yale.edu]

Hi,

I'm currently learning LH, and encountered an unsafe type error when trying to prove that the following code is correct:

{-@ type IncrList a = [a]<{\h v -> h <= v}> @-}

{-@ mapPlus2 :: IncrList Int -> IncrList Int @-}

mapPlus2 :: [Int] -> [Int]

mapPlus2 [] = []

mapPlus2 (x:xs) = (x + 2):mapPlus2 xs

After a bit more experimentation, I discovered that even the following is not safe:

{-@ id' :: IncrList Int -> IncrList Int @-}

id' :: [Int] -> [Int]

id' [] = []

id' (x:xs) = x:id' xs

However, LH does say that this (very similar) code is safe:

{-@ id'' :: (Ord a) => IncrList a -> IncrList a @-}

id'' :: [a] -> [a]

id'' [] = []

id'' (x:xs) = x:id'' xs

Why is this?  It seems that since Int implements Ord, the the safety of id'' should imply the safety of id' safety?

This code is available online here: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1478898064_17964.hs

Thanks,

Bill

[Ranjit Jhala]

Hi Bill,

this is a very tricky question indeed! I should write up 

a common explanation for this in one place.

The reason that your `id''` is SAFE but your `id'` is UNSAFE is parametricity.

1. In the UNSAFE case, 

```

{-@ id' :: IncrList Int -> IncrList Int @-}

id' :: [Int] -> [Int]

id' [] = []

id' (x:xs) = x:id' xs

```

the code is rejected because the ONLY thing we know about the result of 

the recursive call is that it is SOME `IncrList Int` ; in particular we 

do not know that it is -- the same list of values as `xs` -- and hence,

we do not know that the list comprises values that are LARGER THAN x.

Put another way, to LH, the code above is identical to:

```

{-@ randomIncrList :: IncrList Int -> IncrList Int @-}

randomIncrList xs = ...

{-@ id' :: IncrList Int -> IncrList Int @-}

id' :: [Int] -> [Int]

id' [] = []

id' (x:xs) = x : randomIncrList xs

```

except that for modularity, it ONLY uses the type signature of randomIncrList 

which is not strong enough to prove the property. Indeed `randomIncrList` may 

return the list `[0]` which satisfies the output type but may not be "good enough"

at the call site in `id'`. 

2. In the SAFE case, 

the type signature -- thanks to the "forall a" -- actually ensures that the list 

of values that we put in, is exactly the same as the set that comes out. 

Specifically, in

```

id'' (x:xs) = x : id'' xs

```

we know (from the IncrList) that:

             xs :: [ {v : IncrList a | x <= v} ]

and due to the polymorphism, we deduce that 

        id'' xs :: [ {v : IncrList a | x <= v} ]

which then lets LH prove that 

  (x : id'' xs) :: IncrList a

Your  `mapPlus2` is rejected for the same reason as the `id'` above -- 

however, we've never found a good way to verify that order was preserved

under mapping. (i.e. never found what the "right" type signature is -- that

captures the relevant property, which is perhaps something like the "f" 

being used to map is "monotonic".)

Does that make sense?

@Niki do you think the following could be checked with bounds? (Not clear 

that the instantiation works out ... or does it?

```

bound mono p = \a1 b1 a2 b2 -> a1 <= a2 => (p a1 b1) => (p a2 b2) => b1 <= b2

monoMap :: forall <p :: a -> b -> Prop>. (Mono p) => 

           (Ord a, Ord b) => (x:a -> b<p x>) -> OrdList a -> OrdList b 

monoMap f []     = [] 

monoMap f (x:xs) = f x : monoMap f xs

```

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

[william....@yale.edu]

Great, thanks.  Makes sense.

[Zilin Chen]

Just to confirm my understanding, it is the exact problem your paper "Abstract refinement types" solves.

Is it an implemented feature in LH?

Thanks,
Zilin

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.

[Ranjit Jhala]

Yes -- the abstract refinements stuff *is* implemented in LH..