If you think about it for a bit, you'll see that there is no way the type of your listToChain can ever work because it takes in values of (b, Direction) that have no type level information of direction and it should still somehow figure out the direction-indexed type of the resulting Chain at compile time. That's clearly impossible since at run-time the values could be inputted by the user or read from a socket etc.
You need to either skip the intermediate list and build up your chain directly from compile-time verified values or your can wrap the resulting chain in an existential type and perform a run-time check to reify the existential to a more precise type.
So, given an existential wrapper like
data SomeChain a where
SomeChain :: Chain nu nd a -> SomeChain a
you can implement listToChain as
listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = withSome (SomeChain . Add x) (listToChain xs)
listToChain ((x, Up):xs) = withSome (SomeChain . AddUp x) (listToChain xs)
listToChain ((x, Down): xs) = withSome (SomeChain . AddDn x) (listToChain xs)
listToChain ((x, UpDown): xs) = withSome (SomeChain . AddUD x) (listToChain xs)
listToChain _ = SomeChain Nil
using the helper function withSome for more convenient wrapping and unwrapping of the existential.
withSome :: (forall nu nd. Chain nu nd b -> r) -> SomeChain b -> r
withSome f (SomeChain c) = f c
Now we have an existential which we can pass around that hides the precise up and down types. When we want to call a function like lengthChain that expects specific up and down counts we need to validate the contents at run-time. One way to do this is to define a type-class.
class ChainProof pnu pnd where
proveChain :: Chain nu nd b -> Maybe (Chain pnu pnd b)
The proveChain function takes a chain of any nu and nd and tries to prove that it conforms to the specific pnu and pnd. Implementing ChainProof requires a bit of repetitive boilerplate but it can then provide proof for any desired combination of ups and downs in addition to the one-one case we need for lengthChain.
instance ChainProof Zero Zero where
proveChain Nil = Just Nil
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain _ = Nothing
instance ChainProof u Zero => ChainProof (Succ u) Zero where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddUp a rest) = AddUp a <$> proveChain rest
proveChain _ = Nothing
instance ChainProof Zero d => ChainProof Zero (Succ d) where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddDn a rest) = AddDn a <$> proveChain rest
proveChain _ = Nothing
instance (ChainProof u (Succ d), ChainProof (Succ u) d, ChainProof u d) => ChainProof (Succ u) (Succ d) where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddUp a rest) = AddUp a <$> proveChain rest
proveChain (AddDn a rest) = AddDn a <$> proveChain rest
proveChain (AddUD a rest) = AddUD a <$> proveChain rest
proveChain _ = Nothing
The above requires the language extensions MultiParamTypeClasses and FlexibleContexts and I'm using <$> from Control.Applicative.
Now we can use the proving mechanism to create a safe wrapper for any function expecting specific up and down counts
safe :: ChainProof nu nd => (Chain nu nd b -> r) -> SomeChain b -> Maybe r
safe f = withSome (fmap f . proveChain)
This might seem like an unsatisfactory solution since we still need to handle the failure case (i.e. Nothing) but at least the check is only required at the top level. Inside the given f we have static guarantees about the structure of the chain and don't need to do any additional validation.
Alternative solution
The above solution, while simple to implement, has to traverse and re-construct the whole chain every time it is validated. Another option is to store the up and down counts as singleton naturals in the existential.
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data SomeChain a where
SomeChain :: SNat nu -> SNat nd -> Chain nu nd a -> SomeChain a
The SNat type is the value level equivalent of the Nat kind so that for each type of kind Nat there is exactly one value of type SNat which means that even when the type t of SNat t is erased, we can fully recover it by pattern matching on the value. By extension this means that we can recover the full type of Chain in the existential by merely pattern matching on the naturals without having to traverse the chain itself.
Building the chain gets a little bit more verbose
listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = case listToChain xs of
SomeChain u d c -> SomeChain u d (Add x c)
listToChain ((x, Up):xs) = case listToChain xs of
SomeChain u d c -> SomeChain (SSucc u) d (AddUp x c)
listToChain ((x, Down): xs) = case listToChain xs of
SomeChain u d c -> SomeChain u (SSucc d) (AddDn x c)
listToChain ((x, UpDown): xs) = case listToChain xs of
SomeChain u d c -> SomeChain (SSucc u) (SSucc d) (AddUD x c)
listToChain _ = SomeChain SZero SZero Nil
But on the other hand, the proof get shorter (although with somewhat hairy type signatures).
proveChain :: forall pnu pnd b. (ProveNat pnu, ProveNat pnd) => SomeChain b -> Maybe (Chain pnu pnd b)
proveChain (SomeChain (u :: SNat u) (d :: SNat d) c)
= case (proveNat u :: Maybe (Refl u pnu), proveNat d :: Maybe (Refl d pnd)) of
(Just Refl, Just Refl) -> Just c
_ -> Nothing
This uses ScopedTypeVariables to explicitly choose the type-class instances for ProveNat we want to use. If we get proof that the naturals match the requested values then the type-checker is happy to let us return Just c without examining it further.
ProveNat is defined as
{-# LANGUAGE PolyKinds #-}
data Refl a b where
Refl :: Refl a a
class ProveNat n where
proveNat :: SNat m -> Maybe (Refl m n)
The Refl type (reflexivity) is a commonly used pattern to make the type checker unify two unknown types when we pattern match on the Refl constructor (and PolyKinds allows it to be generic to any kind, letting us use it with Nats). So while proveNat accepts forall m. SNat m if we can pattern match on Just Refl afterwards, we (and more importantly, the type-checker) can be sure that m and n are actually the same type.
The instances for ProveNat are pretty simple but require, again, some explicit types to help inference.
instance ProveNat Zero where
proveNat SZero = Just Refl
proveNat _ = Nothing
instance ProveNat n => ProveNat (Succ n) where
proveNat m@(SSucc _) = proveNat' m where
proveNat' :: forall p. ProveNat n => SNat (Succ p) -> Maybe (Refl (Succ p) (Succ n))
proveNat' (SSucc p) = case proveNat p :: Maybe (Refl p n) of
Just Refl -> Just Refl
_ -> Nothing
proveNat _ = Nothing
