[Haskell-cafe] Question on inductive type-families

[Sylvain Henry]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190822/3ab2fc8e/attachment.html>