Refinement Types via SMT and Predicate Abstraction

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 `OrdList`s.

## 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 `OrdList`s.

```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 `OrdList`s 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 `OrdList`s

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 `OrdList`s 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 `OrdList`s 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 `foldOL`s 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 `OrdList`s 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 `OrdList`s,
• we didn’t have to provide explict non-emptiness witnesses,
• we obtained extra information about the behavior of API functions like `concatOL`.