How can I define type-level list indexing amenable to proof?

user_5863987 0
Viewed 113
{-# language GADTs, KindSignatures, DataKinds, TypeApplications, TypeOperators,
    TypeFamilies, PolyKinds, UndecidableInstances, RankNTypes, AllowAmbiguousTypes #-}

import GHC.TypeLits

I would like to index a type-level list with a type-level Nat:

type family Index (xs :: [a]) (k :: Nat) where
    Index (x:xs) 0 = x
    Index (x:xs) k = Index xs (k - 1)

Note that I'm using GHC.TypeLits.Nat instead of, say, data Nat = Z | S Nat, as the actual parameter comes from an SNat and I would like to avoid storing numbers in unary at runtime.

This definition works fine for concrete types:

*Main> :k! Index [Int, Double, String] 1
Index [Int, Double, String] 1 :: *
= Double

However, in some of my functions, I need to prove that Index v n ~ Index (a:v) (n+1). GHC cannot solve this by itself:

prf :: Index v n -> Index (a:v) (n + 1)
prf x = x

    • Couldn't match expected type ‘Index (a : v) (n + 1)’
                  with actual type ‘Index v n’
      NB: ‘Index’ is a non-injective type family
    • In the expression: x
      In an equation for ‘prf’: prf x = x
    • Relevant bindings include
        x :: Index v n (bound at Minimal.hs:11:5)
        prf :: Index v n -> Index (a : v) (n + 1)
          (bound at Minimal.hs:11:1)

Is it possible to prove this type equality? If not, what are my alternatives?

type-families dependent-type haskell
1 Answers

Is it possible to prove this type equality?

Unfortunately, you're out of luck on actually proving anything here, as far as I'm aware. You can perform arithmetic on Nats, but GHC doesn't actually know anything about them. As a simple example of this:

> :k! forall n. n + 1 - 1
forall n. n + 1 - 1 :: Nat
= (n + 1) - 1

In other words, GHC can't tell that n + 1 - 1 ~ n. From that alone, your definition, which uses + while your type family uses - won't work. But, you're actually in even more trouble. Because you're using GHC's Nat and not something unary, you've written your type family as a closed type family:

type family Index (xs :: [a]) (k :: Nat) where
    Index (x:xs) 0 = x
    Index (x:xs) k = Index xs (k - 1)

In order for GHC to use the second case, it has to know, without a doubt, that the second argument is not 0. But remember, GHC doesn't really know anything about the "math" used on Nat. For instance, it doesn't know that n + 1 won't ever end up being 0. That + there isn't really math, it's just a type family, and GHC doesn't understand any logic therein. All GHC knows is that n + 1 is a type family application that can't be reduced, so there's no evidence that n is not 0, so Index can't be reduced.

If not, what are my alternatives?

Well, there's the one you don't like, which is to use data Nat = Z | S Nat. There's no apparent math anymore, just constructors and pattern matching, and you don't even need to close the type family to make it work.

The next thing you can do is use a type-checker plugin that actually knows some math. While I believe this is viable, I don't know of any plugins that actually do this. Maybe someone else can suggest one, or maybe you can write your own.

The last option is to write some mathematical axioms yourself and use unsafeCoerce as your "proof". It's far from elegant, but if it makes your library work the way you want, then go for it.

In this case, you could pretty easily write:

prf :: Index (a:v) (n + 1) -> Index v n
prf = unsafeCoerce

and have pretty high confidence nothing will go wrong. Using the constraints library, you could also try writing something like this:

axiom1 :: forall a v n. Dict (Index (a:v) (n + 1) ~ Index v n)
axiom1 = unsafeCoerce $ Dict @()

prf :: forall a v n. Index (a:v) (n + 1) -> Index v n
prf = case axiom1 @a @v @n of
  Dict -> id

Here, our axiom1 asserts that these two types are equivalent. In prf, we extract that Dict, which gives us our evidence, so we can define prf as id.

user_148023840
Related