[Haskell-cafe] Question on inductive type-families
Sylvain Henry
sylvain at haskus.fr
Wed Aug 21 13:09:15 UTC 2019
Hi,
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. ?
Thanks,
Sylvain
More information about the Haskell-Cafe
mailing list