[Haskell-cafe] Question on inductive type-families
lysxia at gmail.com
Wed Aug 21 14:46:25 UTC 2019
The problem is that in the case where `n1` is not equal to `0`, this
unequality is not made available as a constraint solver (whereas in the
case where they are equal, the `Refl` constructor makes the
corresponding equality constraint available).
In fact, there is no built-in "unequality constraint" that acts as a
counterpart to `~` (it does not seem quite straightforward how that
would even work), but there is one way to encode it as a boolean type
family `((n == 0) ~ 'False)`. That requires changing type families to
pattern-match on `n == 0` instead of `n` directly, and possibly
additional gymnastics to reflect the comparison at term-level:
type Index n l = IndexIf (n == 0) n l
type family IndexIf (b :: Bool) (n :: Nat) (l :: [k]) :: k where
IndexIf 'False n (x ': _ ) = x
IndexIf 'True n (_ ': xs) = Index (n - 1) xs
On 8/21/19 9:09 AM, Sylvain Henry wrote:
> 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. ?
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe