Is family type proof possible?

Question

First, I started with some typical natural type number.

{-# 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 nm) 

So, I wanted to create a data type representing an n-dimensional grid. (A generalization of what is on the assessment of cellular automata is comonadic .)

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

The idea is that the type U num x is a type of num dimensional grid x s that is "focused" on a specific point on the grid.

So, I wanted to do this comonad, and I noticed that this is a potentially useful function that I can do:

 ufold :: (x -> U mr) -> U nx -> U (Plus nm) r ufold f (Point x) = fx ufold f (Dimension ls mid rs) = Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs) 

Now we can implement a “dimensional union”, which turns an n-dimensional grid of m-dimensional grids into an (n + m) -dimensional grid in terms of this combinator. This is useful when working with the result of cojoin , which will create meshes of meshes.

 dimJoin :: U n (U mx) -> U (Plus nm) 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 (fx)) 

However, this leads to a type error.

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

But if we whip some pasta, then the type error disappears.

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

Well, I hate the taste of pasta copies, so my question is this. How can I tell the type system that Plus n Z is n ? And this is a trick: you cannot make changes to instances of a type family that will cause dimJoin create a similar type error.

Answer 1

What you need is a good type of equality of sentences:

 {-# 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 nm) 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 inject this knowledge into the field locally by matching patterns in Refl .

It is unfortunate that my plusZero proof requires induction on the natural question under consideration, which you cannot do by default (since it does not exist at run time). However, the Natural Witness Creation Class would be easy.

Another option for your particular case may be to simply invert the arguments to plus in the definition of your type so that you get Z on the left and automatically reduce it. This is often a good first step to make sure your types are simple, how you can make them, but then you will often need propositional equality for more complex things, regardless.