[Haskell-cafe] Question on inductive type-families

Sylvain Henry sylvain at haskus.fr
Wed Aug 21 13:09:15 UTC 2019


Suppose I have the following type family:

type family Index (n :: Nat) (l :: [k]) = (r :: k) where
    Index 0 (x ': _ ) = x
    Index n (_ ': xs) = Index (n-1) xs

I'm using it to define a Variant type:

data V2 (vs :: [k]) where
    V2 :: forall vs (n :: Nat). KnownNat n => Proxy n -> Index n vs -> V2 vs

Now I want to match on the Variant retrieving either the head or the 
tail (another Variant):

splitV2 :: forall v vs. V2 (v:vs) -> Either v (V2 vs)
splitV2 = \case
    V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0) of
          Just Refl -> Left v
          Nothing   -> Right (V2 (Proxy @(n-1)) v)

It fails to typecheck with:

Couldn't match type ‘Index n (v : vs)’ with ‘Index (n - 1) vs’
Expected type: Index (n - 1) vs
Actual type: Index n vs1
NB: ‘Index’ is a non-injective type family

Is there a way to make this work?

This is highly speculative as I'm not very familiar with type-checking: 
would it be sound to make the inductive Index family "weakly" injective? 
I.e. somehow produce a typing rule for the type family:

   forall n n' x xs xs'.
     Solving: Index n (x ': xs) ~ Index (n'-1) xs'
     Is equivalent to solving: if n /= 0 then (n ~ n', xs ~ xs') else (x 
~ Index (n'-1) xs')

Here we could know that "n /= 0" thanks to the match on "sameNat n1 
(Proxy @0)".

("weakly" because we have some form of injectivity on the shape of the 
list but not on its contents)

Any pointer on this kind of stuff in research papers, Coq, Agda, etc. ?


More information about the Haskell-Cafe mailing list