Append for type-level numbered lists with TypeLits
haskell
Solution
Sure there's a way. It's not a good way, but there's a way.. The entire purpose of putting `unsafeCoerce` in the language is for the case where you know something is correctly typed, but GHC can't figure it out itself. So.. There's a way.
The story is supposed to improve significantly in GHC 7.10. The current plans are to include an SMT solver for working with type-level Nat values.
Edit:
Oh. As for why it's easy with Peano naturals, and hard with type-level literals: With Peano naturals, adding one is applying a type constructor. GHC knows that applying a type constructor is an injective operation. In fact, it's one of the key points underlying GHC's type system. So when you work with Peano naturals, you're working solely with constructs GHC is already well-suited to handle.
In contrast, GHC doesn't know a darned thing about arithmetic. It doesn't know that `(+1)` is an injective function on `Nat`. So it has no way of knowing that it can derive `m ~ n` from `(m + 1) ~ (n + 1)`. It also has no ideas about the basic properties of arithmetic on `Nat`, like the associative, distributive, and commutative properties. The idea behind integrating an SMT solver is that SMT solvers are quite good at working with those sorts of properties.
With GHC 7.8, you can rather painlessly translate type-level literals to Peano naturals, though:
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits
data Z
data S a
type family P (n :: Nat) where
P 0 = Z
P n = S (P (n - 1))
This takes advantage of the new closed type families feature to make a type function `P` for converting from a literal to a Peano representation, as such:
*Main> :t undefined :: P 5
undefined :: P 5 :: S (S (S (S (S Z))))
Problem
Using `GHC.TypeLits`, we can write a simple type-level numbered list (or vector.) ``` > {-# LANGUAGE TypeOperators, KindSignatures, GADTs, DataKinds, ScopedTypeVariables #-} > import GHC.TypeLits > data Vec :: * -> Nat -> * where > VNil :: Vec e 0 > (:-) :: e -> Vec e n -> Vec e (n+1) ``` This is the canonical vector definition with `TypeLits`. The append operation, intuitively, should look as follows: ``` > vecAppend :: Vec e n -> Vec e m -> Vec e (n + m) > vecAppend VNil vec = vec > vecAppend (a :- as) vec = a :- vecAppend as vec ``` But GHC's solver has trouble with the arithmetic: ``` Could not deduce (((n1 + m) + 1) ~ (n + m)) from the context (n ~ (n1 + 1)) ``` Of course, since `n1 + 1 ~ n`, `(n1 + m) + 1 ~ n1 + 1 + m ~ n + m`, but the solver does not seem to know about the commutativity and associativity of `+` (a type function isn't in general commutative or associative!) I know that it is possible if I define type-level Peano naturals, but I wanted to know if there is a way to do it with the current implementation of type nats in GHC (7.8.0 here.) So I tried to help: ``` > vecAppend :: Vec e (n+1) -> Vec e m -> Vec e ((n + 1) + m) > vecAppend VNil vec = vec > vecAppend (a :- as) vec = a :- vecAppend as vec ``` But that just defers the problem to proper instantiation of type variables. ``` Could not deduce (((n1 + 1) + m) ~ ((n + m) + 1)) from the context ((n + 1) ~ (n1 + 1)) bound by a pattern with constructor :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1), in an equation for ‘vecAppend’ NB: ‘+’ is a type function, and may not be injective Expected type: Vec l ((n + 1) + m) Actual type: Vec l ((n + m) + 1) Relevant bindings include l :: Vec l m as :: Vec l n1 vecAppend :: Vec l (n + 1) -> Vec l m -> Vec l ((n + 1) + m) ``` And two more much like this one. So let's scope them. ``` > vecAppend ∷ ∀ e n m. Vec e (n+1) → Vec e m → Vec e (n + 1 + m) > vecAppend VNil l = l > vecAppend ((a :- (as ∷ Vec e n)) ∷ Vec e (n+1)) (l ∷ Vec e m) = a :- (vecAppend as l ∷ Vec e (n+m)) ``` Alas, ``` Could not deduce (n1 ~ n) from the context ((n + 1) ~ (n1 + 1)) bound by a pattern with constructor :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1), in an equation for ‘vecAppend’ ‘n1’ is a rigid type variable bound by a pattern with constructor :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1), in an equation for ‘vecAppend’ ‘n’ is a rigid type variable bound by the type signature for vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m) Expected type: Vec e n1 Actual type: Vec e n Relevant bindings include vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m) In the pattern: as :: Vec e n In the pattern: a :- (as :: Vec e n) In the pattern: (a :- (as :: Vec e n)) :: Vec e (n + 1) ``` Is there a way to do this with the current solver, and without resorting to defining your own Peano nats? I prefer the look of `3` to `Succ (Succ (Succ Zero)))` in my type signatures. EDIT: Since it seems that there is no way to do it currently (until GHC 7.10) I'll rephrase my question: can anybody show my why there is no way? I unfortunately have not yet looked at SMT solvers, so I don't know what is in principle possible or not. The idea is that I'm not very experienced with type-level computations, and I want learn to discern situations where I can rephrase my problem so that it works, and situations where I cannot (this being (for now) an instance of the latter.)