Question on inductive type-families

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Question on inductive type-families

Sylvain Henry-2
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Question on inductive type-families

Li-yao Xia-2
Hi Sylvain,

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


Cheers,
Li-yao

On 8/21/19 9:09 AM, Sylvain Henry wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Question on inductive type-families

Sylvain Henry-2

Hi Li-yao,

Thanks for your answer. Sadly I haven't managed to make it work this way neither.

In addition I need a "KnownNat (n-1)" while I only have "KnownNat n" (and the knowledge that n > 0). For the record, it works with an unsafeCoerce:

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

splitV2 :: forall v vs. V2 (v:vs) -> Either (V2 vs) v
{-# INLINE splitV2 #-}
splitV2 = \case
    V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0) of
       Just Refl -> Right v
       Nothing   -> case someNatVal (natVal n1 - 1) of
         SomeNat (n2 :: Proxy n') -> case unsafeCoerce Refl :: Index n (v:vs) :~: Index n' vs of
            Refl -> Left (V2 n2 v)

instance Show (V2 '[]) where
   {-# INLINABLE show #-}
   show = undefined

instance (Show x, Show (V2 xs)) => Show (V2 (x ': xs)) where
   {-# INLINABLE show #-}
   show v = case splitV2 v of
      Right x -> show x
      Left xs -> show xs

test :: V2 '[Int,Word,String] -> String
test v = show v

However the generated Core isn't as pretty as with the previous representation (which uses unsafeCoerce for the value, not for the index):

data Variant (types :: [*]) = Variant {-# UNPACK #-} !Word Any

I'll stick to this one for now.

Sylvain


On 21/08/2019 16:46, Li-yao Xia wrote:
Hi Sylvain,

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


Cheers,
Li-yao

On 8/21/19 9:09 AM, Sylvain Henry wrote:
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Question on inductive type-families

Brandon Allbery
There are some plugins like natnormalise that help with this kind of thing. ghc itself is not so good at these kinds of deductions.

On Thu, Aug 22, 2019 at 4:33 AM Sylvain Henry <[hidden email]> wrote:

Hi Li-yao,

Thanks for your answer. Sadly I haven't managed to make it work this way neither.

In addition I need a "KnownNat (n-1)" while I only have "KnownNat n" (and the knowledge that n > 0). For the record, it works with an unsafeCoerce:

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

splitV2 :: forall v vs. V2 (v:vs) -> Either (V2 vs) v
{-# INLINE splitV2 #-}
splitV2 = \case
    V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0) of
       Just Refl -> Right v
       Nothing   -> case someNatVal (natVal n1 - 1) of
         SomeNat (n2 :: Proxy n') -> case unsafeCoerce Refl :: Index n (v:vs) :~: Index n' vs of
            Refl -> Left (V2 n2 v)

instance Show (V2 '[]) where
   {-# INLINABLE show #-}
   show = undefined

instance (Show x, Show (V2 xs)) => Show (V2 (x ': xs)) where
   {-# INLINABLE show #-}
   show v = case splitV2 v of
      Right x -> show x
      Left xs -> show xs

test :: V2 '[Int,Word,String] -> String
test v = show v

However the generated Core isn't as pretty as with the previous representation (which uses unsafeCoerce for the value, not for the index):

data Variant (types :: [*]) = Variant {-# UNPACK #-} !Word Any

I'll stick to this one for now.

Sylvain


On 21/08/2019 16:46, Li-yao Xia wrote:
Hi Sylvain,

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


Cheers,
Li-yao

On 8/21/19 9:09 AM, Sylvain Henry wrote:
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


--
brandon s allbery kf8nh

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.