Are type family instance proofs possible?

Question

First, I started with some typical type-level natural number stuff.

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

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

So I wanted to create a data type representing an n-dimensional grid. (A generalization of what is found at Evaluating cellular automata is comonadic.)

data U (n :: Nat) x where
  Point     :: x                           -> U Z     x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

The idea is that the type U num x is the type of a num-dimensional grid of xs, which is "focused" on a particular point in the grid.

So I wanted to make this a comonad, and I noticed that there's this potentially useful function I can make:

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r
ufold f (Point x) = f x
ufold f (Dimension ls mid rs) =
  Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs)

We can now implement a "dimension join" that turns an n-dimensional grid of m-dimensional grids into an (n+m)-dimensional grid, in terms of this combinator. This will come in handy when dealing with the result of cojoin which will produce grids of grids.

dimJoin :: U n (U m x) -> U (Plus n m) x
dimJoin = ufold id

So far so good. I also noticed that the Functor instance can be written in terms of ufold.

instance Functor (U n) where
  fmap f = ufold (\x -> Point (f x))

However, this results in a type error.

Couldn't match type `n' with `Plus n 'Z'

But if we whip up some copy pasta, then the type error goes away.

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f (Dimension ls mid rs) =
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs)

Well I hate the taste of copy pasta, so my question is this. How can I tell the type system that Plus n Z is equal to n? And the catch is this: you can't make a change to the type family instances that would cause dimJoin to produce a similar type error.

Answer 1

What you need is a nice propositional equality type:

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

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

data (:=) :: k -> k -> * where
  Refl :: a := a

data Natural (n :: Nat) where
  Zero :: Natural Z
  Suc  :: Natural n -> Natural (S n)

plusZero :: Natural n -> n := (n `Plus` Z)
plusZero Zero = Refl
plusZero (Suc n) | Refl <- plusZero n = Refl

This allows you to prove arbitrary things about your types and bring that knowledge into scope locally by pattern matching on the Refl.

One annoying thing is that my plusZero proof requires induction over the natural in question, which you won't be able to do by default (since it doesn't exist at runtime). A typeclass for generating Natural witnesses would be easy, though.

Another option for your particular case might be just to invert the arguments to plus in your type definition so that you get the Z on the left and it reduces automagically. It's often a good first step to make sure your types are as simple as you can make them, but then you'll often need propositional equality for more complicated things, regardless.