Yesterday someone asked on Reddit how one might define GHC's OrdList in a way that statically enforces its three key invariants. The accepted solution required rewriting OrdList as a GADT indexed by a proof of emptiness (which is essentially created by a run-time check), and used the new Closed Type Families extension in GHC 7.8 to define a type-level join of the Emptiness index.

Today, let's see a somewhat more direct way of tackling this problem in LiquidHaskell, in which we need not change a single line of code (well.. maybe one), and need not perform any dynamic checks.

## The OrdList Type¶

The OrdList type is defined as follows:

54: data OrdList a
55:   = None
56:   | One a
57:   | Many [a]        -- Invariant: non-empty
58:   | Cons a (OrdList a)
59:   | Snoc (OrdList a) a
60:   | Two (OrdList a) -- Invariant: non-empty
61:         (OrdList a) -- Invariant: non-empty

As indicated by the comments the key invariants are that:

• Many should take a non-empty list,
• Two takes two non-empty OrdLists.

## What is a Non-Empty OrdList?¶

To proceed, we must tell LiquidHaskell what non-empty means. We do this with a measure that describes the number of elements in a structure. When this number is strictly positive, the structure is non-empty.

We've previously seen how to measure the size of a list.

77: measure len :: [a] -> Int
78: len ([])   = 0
79: len (x:xs) = 1 + (len xs)

We can use the same technique to measure the size of an OrdList.

85: {-@ measure olen :: OrdList a -> Int
86:     olen (None)      = 0
87:     olen (One x)     = 1
88:     olen (Many xs)   = (len xs)
89:     olen (Cons x xs) = 1 + (olen xs)
90:     olen (Snoc xs x) = 1 + (olen xs)
91:     olen (Two x y)   = (olen x) + (olen y)
92:   @-}
93:
94: {-@ invariant {v:OrdList a | (olen v) >= 0} @-}

Now, we can use the measures to define aliases for non-empty lists and OrdLists.

100: {-@ type ListNE    a = {v:[a]       | (len v)  > 0} @-}
101: {-@ type OrdListNE a = {v:OrdList a | (olen v) > 0} @-}

## Capturing the Invariants In a Refined Type¶

Let's return to the original type, and refine it with the above non-empty variants to specify the invariants as part of the data declaration

110: {-@ data OrdList [olen] a
111:       = None
112:       | One  (x  :: a)
113:       | Many (xs :: ListNE a)
114:       | Cons (x  :: a)           (xs :: OrdList a)
115:       | Snoc (xs :: OrdList a)   (x  :: a)
116:       | Two  (x  :: OrdListNE a) (y  :: OrdListNE a)
117:   @-}

Notice immediately that LiquidHaskell can use the refined definition to warn us about malformed OrdList values.

124: (OrdList.OrdList {VV : (GHC.Integer.Type.Integer) | (VV > 0)})ok     = x1:{x6 : [{x9 : (GHC.Integer.Type.Integer) | (x9 > 0)}] | ((len x6) > 0)}
-> {x2 : (OrdList.OrdList {x9 : (GHC.Integer.Type.Integer) | (x9 > 0)}) | ((olen x2) == (len x1))}Many {x5 : [{x11 : (GHC.Integer.Type.Integer) | (x11 > 0)}]<\x9 VV -> (x8 > 0) && (x8 > x9)> | (((null x5)) <=> false) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}[1,2,3]
125: forall a.
{VV : (OrdList.OrdList {VV : a | false}) | ((olen VV) == 0)}bad    = x1:{x4 : [{VV : a | false}] | ((len x4) > 0)}
-> {x2 : (OrdList.OrdList {VV : a | false}) | ((olen x2) == (len x1))}Many {x8 : [{VV : a | false}]<\_ VV -> false> | (((null x8)) <=> true) && ((len x8) == 0) && ((olens x8) == 0) && ((sumLens x8) == 0) && ((len x8) >= 0) && ((olens x8) >= 0) && ((sumLens x8) >= 0)}[]
126: {VV : (OrdList.OrdList {VV : (GHC.Integer.Type.Integer) | (VV > 0)}) | ((olen VV) == (olen OrdList.ok))}badder = x1:{x10 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x10) > 0)}
-> x2:{x6 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x6) > 0)}
-> {x2 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x2) == ((olen x1) + (olen x2)))}Two {x3 : (OrdList.OrdList {x4 : (GHC.Integer.Type.Integer) | false}) | ((olen x3) == 0) && ((olen x3) >= 0)}None {x3 : (OrdList.OrdList {x5 : (GHC.Integer.Type.Integer) | (x5 > 0)}) | (x3 == OrdList.ok) && ((olen x3) >= 0)}ok

All of the above are accepted by GHC, but only the first one is actually a valid OrdList. Happily, LiquidHaskell will reject the latter two, as they violate the invariants.

## Basic Functions¶

Now let's look at some of the functions!

First, we'll define a handy alias for OrdLists of a given size:

142: {-@ type OrdListN a N = {v:OrdList a | (olen v) = N} @-}

Now, the nilOL constructor returns an empty OrdList:

148: {-@ nilOL :: OrdListN a {0} @-}
149: forall a. {v : (OrdList.OrdList a) | ((olen v) == 0)}nilOL = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None

the unitOL constructor returns an OrdList with one element:

155: {-@ unitOL :: a -> OrdListN a {1} @-}
156: forall a. a -> {v : (OrdList.OrdList a) | ((olen v) == 1)}unitOL aas = {VV : a | (VV == as)}
-> {x2 : (OrdList.OrdList {VV : a | (VV == as)}) | ((olen x2) == 1)}One {VV : a | (VV == as)}as

and snocOL and consOL return outputs with precisely one more element:

162: {-@ snocOL :: xs:OrdList a -> a -> OrdListN a {1 + (olen xs)} @-}
163: forall a.
xs:(OrdList.OrdList a)
-> a -> {v : (OrdList.OrdList a) | ((olen v) == (1 + (olen xs)))}snocOL (OrdList.OrdList a)as ab = x1:(OrdList.OrdList a)
-> a -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x1)))}Snoc {x3 : (OrdList.OrdList a) | (x3 == as) && ((olen x3) >= 0)}as {VV : a | (VV == b)}b
164:
165: {-@ consOL :: a -> xs:OrdList a -> OrdListN a {1 + (olen xs)} @-}
166: forall a.
a
-> xs:(OrdList.OrdList a)
-> {v : (OrdList.OrdList a) | ((olen v) == (1 + (olen xs)))}consOL aa (OrdList.OrdList a)bs = a
-> x2:(OrdList.OrdList a)
-> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x2)))}Cons {VV : a | (VV == a)}a {x3 : (OrdList.OrdList a) | (x3 == bs) && ((olen x3) >= 0)}bs

Note: The OrdListN a {e} syntax just lets us use LiquidHaskell expressions e as a parameter to the type alias OrdListN.

## Appending OrdLists¶

The above functions really aren't terribly interesting, however, since their types fall right out of the definition of olen.

So how about something that takes a little thinking?

190: {-@ appOL :: xs:OrdList a -> ys:OrdList a
191:           -> OrdListN a {(olen xs) + (olen ys)}
192:   @-}
193: None  forall a.
xs:(OrdList.OrdList a)
-> ys:(OrdList.OrdList a)
-> {v : (OrdList.OrdList a) | ((olen v) == ((olen xs) + (olen ys)))}`appOL` (OrdList.OrdList a)b     = {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b
194: a     `appOL` None  = {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a
195: One a `appOL` b     = {VV : a | (VV == a) && (VV > a) && (VV < a)}
-> x2:(OrdList.OrdList {VV : a | (VV == a) && (VV > a) && (VV < a)})
-> {x2 : (OrdList.OrdList {VV : a | (VV == a) && (VV > a) && (VV < a)}) | ((olen x2) == (1 + (olen x2)))}Cons {VV : a | (VV == a)}a {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b
196: a     `appOL` One b = x1:(OrdList.OrdList {VV : a | (VV == b) && (VV > b) && (VV < b)})
-> {VV : a | (VV == b) && (VV > b) && (VV < b)}
-> {x2 : (OrdList.OrdList {VV : a | (VV == b) && (VV > b) && (VV < b)}) | ((olen x2) == (1 + (olen x1)))}Snoc {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a {VV : a | (VV == b)}b
197: a     `appOL` b     = x1:{x6 : (OrdList.OrdList a) | ((olen x6) > 0)}
-> x2:{x4 : (OrdList.OrdList a) | ((olen x4) > 0)}
-> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}Two {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b

appOL takes two OrdLists and returns a list whose length is the sum of the two input lists. The most important thing to notice here is that we haven't had to insert any extra checks in appOL, unlike the GADT solution.

LiquidHaskell uses the definition of olen to infer that in the last case of appOL, a and b must be non-empty, so they are valid arguments to Two.

We can prove other things about OrdLists as well, like the fact that converting an OrdList to a Haskell list preserves length

211: {-@ toOL :: xs:[a] -> OrdListN a {(len xs)} @-}
212: forall a.
xs:[a] -> {v : (OrdList.OrdList a) | ((olen v) == (len xs))}toOL [] = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None
213: toOL xs = x1:{x4 : [a] | ((len x4) > 0)}
-> {x2 : (OrdList.OrdList a) | ((olen x2) == (len x1))}Many {x4 : [a] | ((len x4) >= 0) && ((olens x4) >= 0) && ((sumLens x4) >= 0)}xs

as does mapping over an OrdList

219: {-@ mapOL :: (a -> b) -> xs:OrdList a -> OrdListN b {(olen xs)} @-}
220: forall a b.
(b -> a)
-> x3:(OrdList.OrdList b)
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL _ None        = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None
221: mapOL f (One x)     = a -> {x2 : (OrdList.OrdList a) | ((olen x2) == 1)}One (a -> bf {VV : a | (VV == x)}x)
222: mapOL f (Cons x xs) = a
-> x2:(OrdList.OrdList a)
-> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x2)))}Cons (a -> bf {VV : a | (VV == x)}x) (forall a b.
(b -> a)
-> x3:(OrdList.OrdList b)
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs)
223: mapOL f (Snoc xs x) = x1:(OrdList.OrdList a)
-> a -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x1)))}Snoc (forall a b.
(b -> a)
-> x3:(OrdList.OrdList b)
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) (a -> bf {VV : a | (VV == x)}x)
224: mapOL f (Two x y)   = x1:{x6 : (OrdList.OrdList a) | ((olen x6) > 0)}
-> x2:{x4 : (OrdList.OrdList a) | ((olen x4) > 0)}
-> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}Two (forall a b.
(b -> a)
-> x3:(OrdList.OrdList b)
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x4 : (OrdList.OrdList a) | (x4 == x) && ((olen x4) > 0) && ((olen x4) >= 0)}x) (forall a b.
(b -> a)
-> x3:(OrdList.OrdList b)
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x4 : (OrdList.OrdList a) | (x4 == y) && ((olen x4) > 0) && ((olen x4) >= 0)}y)
225: mapOL f (Many xs)   = x1:{x4 : [a] | ((len x4) > 0)}
-> {x2 : (OrdList.OrdList a) | ((olen x2) == (len x1))}Many ((a -> b) -> x3:[a] -> {x2 : [b] | ((len x2) == (len x3))}map a -> bf {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs)

as does converting a Haskell list to an OrdList.

231: {-@ type ListN a N = {v:[a] | (len v) = N} @-}
232:
233: {-@ fromOL :: xs:OrdList a -> ListN a {(olen xs)} @-}
234: forall a.
xs:(OrdList.OrdList a) -> {v : [a] | ((len v) == (olen xs))}fromOL (OrdList.OrdList a)a = x1:(OrdList.OrdList a)
-> x2:{x4 : [a] | ((len x4) == 0)}
-> {x2 : [a] | ((len x2) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == a) && ((olen x3) >= 0)}a {x8 : [{VV : a | false}]<\_ VV -> false> | (((null x8)) <=> true) && ((len x8) == 0) && ((olens x8) == 0) && ((sumLens x8) == 0) && ((len x8) >= 0) && ((olens x8) >= 0) && ((sumLens x8) >= 0)}[]
235:   where
236:     {-@ go :: xs:_ -> ys:_
237:            -> {v:_ | (len v) = (olen xs) + (len ys)}
238:       @-}
239:     x1:(OrdList.OrdList a)
-> x2:{VV : [a] | ((len VV) >= 0)}
-> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go None       {VV : [a] | ((len VV) >= 0)}acc = {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc
240:     go (One a)    acc = {VV : a | (VV == a)}a forall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}: {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc
241:     go (Cons a b) acc = {VV : a | (VV == a)}a forall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}: x1:(OrdList.OrdList a)
-> x2:{VV : [a] | ((len VV) >= 0)}
-> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc
242:     go (Snoc a b) acc = x1:(OrdList.OrdList a)
-> x2:{VV : [a] | ((len VV) >= 0)}
-> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == a) && ((olen x3) >= 0)}a ({VV : a | (VV == b)}bforall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}:{x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc)
243:     go (Two a b)  acc = x1:(OrdList.OrdList a)
-> x2:{VV : [a] | ((len VV) >= 0)}
-> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x4 : (OrdList.OrdList a) | (x4 == a) && ((olen x4) > 0) && ((olen x4) >= 0)}a (x1:(OrdList.OrdList a)
-> x2:{VV : [a] | ((len VV) >= 0)}
-> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x4 : (OrdList.OrdList a) | (x4 == b) && ((olen x4) > 0) && ((olen x4) >= 0)}b {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc)
244:     go (Many xs)  acc = {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs x1:[a]
-> x2:[a] -> {x2 : [a] | ((len x2) == ((len x1) + (len x2)))}++ {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc

There's nothing super interesting to say about the foldOLs but I'll include them here for completeness' sake.

268: foldrOL :: (a->b->b) -> b -> OrdList a -> b
269: forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL _ az None        = {VV : a | (VV == z)}z
270: foldrOL k z (One x)     = a -> b -> bk {VV : a | (VV == x)}x {VV : a | (VV == z)}z
271: foldrOL k z (Cons x xs) = a -> b -> bk {VV : a | (VV == x)}x (forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk {VV : a | (VV == z)}z {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs)
272: foldrOL k z (Snoc xs x) = forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk (a -> b -> bk {VV : a | (VV == x)}x {VV : a | (VV == z)}z) {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs
273: foldrOL k z (Two b1 b2) = forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk (forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk {VV : a | (VV == z)}z {x4 : (OrdList.OrdList a) | (x4 == b2) && ((olen x4) > 0) && ((olen x4) >= 0)}b2) {x4 : (OrdList.OrdList a) | (x4 == b1) && ((olen x4) > 0) && ((olen x4) >= 0)}b1
274: foldrOL k z (Many xs)   = (a -> b -> b) -> b -> [a] -> bfoldr a -> b -> bk {VV : a | (VV == z)}z {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs
275:
276: foldlOL :: (b->a->b) -> b -> OrdList a -> b
277: forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL _ az None        = {VV : a | (VV == z)}z
278: foldlOL k z (One x)     = a -> b -> ak {VV : a | (VV == z)}z {VV : a | (VV == x)}x
279: foldlOL k z (Cons x xs) = forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak (a -> b -> ak {VV : a | (VV == z)}z {VV : a | (VV == x)}x) {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs
280: foldlOL k z (Snoc xs x) = a -> b -> ak (forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak {VV : a | (VV == z)}z {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) {VV : a | (VV == x)}x
281: foldlOL k z (Two b1 b2) = forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak (forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak {VV : a | (VV == z)}z {x4 : (OrdList.OrdList a) | (x4 == b1) && ((olen x4) > 0) && ((olen x4) >= 0)}b1) {x4 : (OrdList.OrdList a) | (x4 == b2) && ((olen x4) > 0) && ((olen x4) >= 0)}b2
282: foldlOL k z (Many xs)   = (a -> b -> a) -> a -> [b] -> afoldl a -> b -> ak {VV : a | (VV == z)}z {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs

## Concatenatation: Nested Measures¶

Now, the astute readers will have probably noticed that I'm missing one function, concatOL, which glues a list of OrdLists into a single long OrdList.

With LiquidHaskell we can give concatOL a super precise type, which states that the size of the output list equals the sum-of-the-sizes of the input OrdLists.

298: {-@ concatOL :: xs:[OrdList a] -> OrdListN a {(olens xs)} @-}
299: forall a.
x1:[(OrdList.OrdList a)]
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olens x1))}concatOL []       = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None
300: concatOL (ol:ols) = {x3 : (OrdList.OrdList a) | (x3 == ol) && ((olen x3) >= 0)}ol x1:(OrdList.OrdList a)
-> x2:(OrdList.OrdList a)
-> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}`appOL` forall a.
x1:[(OrdList.OrdList a)]
-> {VV : (OrdList.OrdList a) | ((olen VV) == (olens x1))}concatOL {x5 : [(OrdList.OrdList a)] | (x5 == ols) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}ols

The notion of sum-of-the-sizes of the input lists is specifed by the measure

306: {-@ measure olens :: [OrdList a] -> Int
307:     olens ([])     = 0
308:     olens (ol:ols) = (olen ol) + (olens ols)
309:   @-}
310:
311: {-@ invariant {v:[OrdList a] | (olens v) >= 0} @-}

LiquidHaskell is happy to verify the above signature, again without requiring any explict proofs.

## Conclusion¶

The above illustrates the flexibility provided by LiquidHaskell measures.

Instead of having to bake particular invariants into a datatype using indices or phantom types (as in the GADT approach), we are able to split our properties out into independent views of the datatype, yielding an approach that is more modular as

• we didn't have to go back and change the definition of [] to talk about OrdLists,
• we didn't have to provide explict non-emptiness witnesses,
• we obtained extra information about the behavior of API functions like concatOL.
Eric Seidel
2014-02-11