If you think about this a bit, you will see that the type of your listToChain cannot work, because it takes values (b, Direction) that do not have information about the type of direction level, and this should still somehow determine the type of index with the direction index of the resulting Chain at compile time. This is clearly impossible, because at run time, values can be entered by the user or read from the socket, etc.
You either need to skip the intermediate list, or create a chain directly from the verified compilation time values, or you can wrap the resulting chain with an existential type and perform a run time check to confirm the existential more accurate type.
So, given the existential shell of type
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 withSome helper function to more conveniently package and deploy the existential.
withSome :: (forall nu nd. Chain nu nd b -> r) -> SomeChain b -> r withSome f (SomeChain c) = fc
Now we have an existential one that we can get around that hides the exact types up and down. When we want to call a function of type lengthChain that expects specific counts up and down, we need to check the contents at runtime. 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 matches specific pnu and pnd . The ChainProof implementation requires a slightly repeating pattern, but then can provide proof for any desired combination of ups and downs in addition to the 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 ud) => 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
This requires an extension of the MultiParamTypeClasses and FlexibleContexts language, and I use <$> from Control.Applicative .
Now we can use the verification mechanism to create a secure shell for any function that expects specific counts up and down
safe :: ChainProof nu nd => (Chain nu nd b -> r) -> SomeChain b -> Maybe r safe f = withSome (fmap f . proveChain)
This may seem like an unsatisfactory solution, since we still need to handle the case of a failure (i.e. Nothing ), but at least validation is only required at the top level. Inside the given f we have static guarantees regarding the structure of the chain and do not need additional verification.
Alternative solution
The above solution, although simple to implement, must go through and rebuild the whole chain each time it is tested. Another option is to keep the counters up and down as solitary existentials.
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
Type SNat is the level equivalent of a value of type Nat , so for each type of type Nat there is exactly one value of type SNat , which means that even when the type t of SNat t is erased, we can completely restore it by matching patterns by value. By extension, this means that we can restore the full type of Chain to existential by simply matching patterns in natural languages without going through the chain itself.
Chaining is getting a little more detailed
listToChain :: [(b, Direction)] -> SomeChain b listToChain ((x, Center): xs) = case listToChain xs of SomeChain udc -> SomeChain ud (Add xc) listToChain ((x, Up):xs) = case listToChain xs of SomeChain udc -> SomeChain (SSucc u) d (AddUp xc) listToChain ((x, Down): xs) = case listToChain xs of SomeChain udc -> SomeChain u (SSucc d) (AddDn xc) listToChain ((x, UpDown): xs) = case listToChain xs of SomeChain udc -> SomeChain (SSucc u) (SSucc d) (AddUD xc) listToChain _ = SomeChain SZero SZero Nil
But, on the other hand, the proof is getting 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
In this case, ScopedTypeVariables used to explicitly select the type-type instances for ProveNat that we want to use. If we get proof that naturals match the requested values, then type checking would happily allow us to return Just c without having to examine it further.
ProveNat defined as
{-# LANGUAGE PolyKinds #-} data Refl ab where Refl :: Refl aa class ProveNat n where proveNat :: SNat m -> Maybe (Refl mn)
The Refl type is a commonly used pattern to force type checking to unify two unknown types when we map the pattern to the Refl constructor (and PolyKinds allows it to be common to any type, allowing us to use it with Nat s). Therefore, if ProveNat takes forall m. SNat m forall m. SNat m , if after that we can match the Just Refl pattern, we (and, more importantly, the checking type) can be sure that m and n are actually the same type.
The instances for ProveNat pretty simple, but they also require some explicit types to help make a conclusion.
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 pn) of Just Refl -> Just Refl _ -> Nothing proveNat _ = Nothing