How do I prove type-level list properties in haskell?

Question

I have these type families:

type family xs ++ ys where
  '[]      ++ ys = ys
  (x : xs) ++ ys = x : (xs ++ ys)

type family Drop n xs where
  Drop  O         xs  = xs
  Drop (S n) (_ : xs) = Drop n xs

type family Length xs where
  Length '[] = O
  Length  (x : xs) = S (Length xs)

At some point, GHC wants a proof that

forall a. Drop (Length a) (a ++ c) ~ c

I've used to shove that into context of some constructor.

How do I prove this property universally?

Answer 1

Okay, so your type families are fine and your property is almost right.

What you want to prove is this:

proof :: Drop (Length a) (a ++ c) :~: c

Except you don't really know what a and c are. They are implicitly quantified. You want them to be explicit so we can do induction over them.

proof :: (a :: [ k ]) -> (c :: [ k ]) -> Drop (Length a) (a ++ c) :~: c

You'll realise this is not going to type check because Haskell doesn't have real dependent types, but there is a way around: singleton types. The idea is to create an indexed type so that each term corresponds to one term of a different type that is used as the type index. I know this sounds a bit confusing, but example should clarify it.

You can use the singletons library or build them from scratch that's what I'll do here.

data family Sing (x :: k)

data SList xs where
  SNil  :: SList '[]
  SCons :: Sing x -> SList xs -> SList (x ': xs)

Here Sing is a data family so that I can generically refer to things that have singletons. SList is the singleton version of the list type and as you can see the SNil constructor corresponds to the type-level []. Similarly, SCons reflects :.

Then (assuming you also have a definition of data Nat = O | S Nat somewhere) the signature of the proof you are after is

proof :: SList a -> SList c -> Drop (Length a) (a ++ c) :~: c

Notice that I changed your ~ into a :~: that's a type operator available in Data.Type.Equality. It's only constructor is Refl which you can only assert if its two operands are exactly the same.

Now we just need to prove it. Luckily, this is a super simple property to prove, you just need to do induction over SList a

In the base case SList a is SNil, so you are really trying to prove Drop (Length '[]) ('[] '++ c) :~: c. Because you used type families, the type checker will immediately reduce this to c :~: c. Since both operands are the same we can use the Refl constructor to prove this case.

proof SNil _ = Refl

Now comes the inductive case. We'll pattern match again and this time learn that SList a is of the form SCons a as with a :: Sing x and as :: Sing xs. This means what we need to prove is Drop (Length (x ': xs)) ((x : xs) ++ c) :~: c. Again your type families will immediately start doing computation and reduce this goal to Drop (Length xs) (xs ++ c) :~: c because it doesn't really need to know what x is to do the evaluation.

As it turns out, proof as c (nb. I use as instead of SCons a as) has exactly the required type, so we use that to prove the property.

Here's the full proof.

proof :: SList a -> SList c -> Drop (Length a) (a ++ c) :~: c
proof SNil _ = Refl
proof (SCons a as) cs = proof as cs

For these to work, you'll need all of these language extensions:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}