<div dir="ltr">There are some plugins like natnormalise that help with this kind of thing. ghc itself is not so good at these kinds of deductions.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 22, 2019 at 4:33 AM Sylvain Henry <<a href="mailto:sylvain@haskus.fr">sylvain@haskus.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<p>Hi Li-yao,</p>
<p>Thanks for your answer. Sadly I haven't managed to make it work
this way neither.</p>
<p>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:</p>
<p><tt>data V2 (vs :: [k]) where</tt><tt><br>
</tt><tt> V2 :: forall vs (n :: Nat). KnownNat n => Proxy n
-> Index n vs -> V2 vs</tt><tt><br>
</tt><tt><br>
</tt><tt>splitV2 :: forall v vs. V2 (v:vs) -> Either (V2 vs) v</tt><tt><br>
</tt><tt>{-# INLINE splitV2 #-}</tt><tt><br>
</tt><tt>splitV2 = \case</tt><tt><br>
</tt><tt> V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0)
of</tt><tt><br>
</tt><tt> Just Refl -> Right v</tt><tt><br>
</tt><tt> Nothing -> case someNatVal (natVal n1 - 1) of</tt><tt><br>
</tt><tt> SomeNat (n2 :: Proxy n') -> case unsafeCoerce
Refl :: Index n (v:vs) :~: Index n' vs of</tt><tt><br>
</tt><tt> Refl -> Left (V2 n2 v)</tt><tt><br>
</tt><tt><br>
</tt><tt>instance Show (V2 '[]) where</tt><tt><br>
</tt><tt> {-# INLINABLE show #-}</tt><tt><br>
</tt><tt> show = undefined</tt><tt><br>
</tt><tt><br>
</tt><tt>instance (Show x, Show (V2 xs)) => Show (V2 (x ': xs))
where</tt><tt><br>
</tt><tt> {-# INLINABLE show #-}</tt><tt><br>
</tt><tt> show v = case splitV2 v of</tt><tt><br>
</tt><tt> Right x -> show x</tt><tt><br>
</tt><tt> Left xs -> show xs</tt></p>
<p><tt>test :: V2 '[Int,Word,String] -> String</tt><tt><br>
</tt><tt>test v = show v</tt><br>
</p>
<p>However the generated Core isn't as pretty as with the previous
representation <span class="gmail-m_-6418842020346594588kt">(which uses unsafeCoerce for the
value, not for the index)</span>:</p>
<pre><span class="gmail-m_-6418842020346594588kr">data</span> <span class="gmail-m_-6418842020346594588kt">Variant</span> <span class="gmail-m_-6418842020346594588p">(</span><span class="gmail-m_-6418842020346594588n">types</span> <span class="gmail-m_-6418842020346594588ow">::</span> <span class="gmail-m_-6418842020346594588p">[</span><span class="gmail-m_-6418842020346594588o">*</span><span class="gmail-m_-6418842020346594588p">])</span> <span class="gmail-m_-6418842020346594588ow">=</span> <span class="gmail-m_-6418842020346594588kt">Variant</span> <span class="gmail-m_-6418842020346594588cm">{-# UNPACK #-}</span> <span class="gmail-m_-6418842020346594588o">!</span><span class="gmail-m_-6418842020346594588kt">Word</span> <span class="gmail-m_-6418842020346594588kt">Any
</span></pre>
<span class="gmail-m_-6418842020346594588kt">I'll stick to this one for now.<br>
</span><br>
Sylvain<br>
<span class="gmail-m_-6418842020346594588kt"></span>
<p><br>
</p>
<div class="gmail-m_-6418842020346594588moz-cite-prefix">On 21/08/2019 16:46, Li-yao Xia wrote:<br>
</div>
<blockquote type="cite">Hi
Sylvain,
<br>
<br>
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).
<br>
<br>
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:
<br>
<br>
<br>
type Index n l = IndexIf (n == 0) n l
<br>
<br>
type family IndexIf (b :: Bool) (n :: Nat) (l :: [k]) :: k where
<br>
IndexIf 'False n (x ': _ ) = x
<br>
IndexIf 'True n (_ ': xs) = Index (n - 1) xs
<br>
<br>
<br>
Cheers,
<br>
Li-yao
<br>
<br>
On 8/21/19 9:09 AM, Sylvain Henry wrote:
<br>
<blockquote type="cite">Hi,
<br>
<br>
Suppose I have the following type family:
<br>
<br>
type family Index (n :: Nat) (l :: [k]) = (r :: k) where
<br>
Index 0 (x ': _ ) = x
<br>
Index n (_ ': xs) = Index (n-1) xs
<br>
<br>
I'm using it to define a Variant type:
<br>
<br>
data V2 (vs :: [k]) where
<br>
V2 :: forall vs (n :: Nat). KnownNat n => Proxy n ->
Index n vs -> V2 vs
<br>
<br>
Now I want to match on the Variant retrieving either the head or
the tail (another Variant):
<br>
<br>
splitV2 :: forall v vs. V2 (v:vs) -> Either v (V2 vs)
<br>
splitV2 = \case
<br>
V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0) of
<br>
Just Refl -> Left v
<br>
Nothing -> Right (V2 (Proxy @(n-1)) v)
<br>
<br>
It fails to typecheck with:
<br>
<br>
Couldn't match type ‘Index n (v : vs)’ with ‘Index (n - 1) vs’
<br>
Expected type: Index (n - 1) vs
<br>
Actual type: Index n vs1
<br>
NB: ‘Index’ is a non-injective type family
<br>
<br>
<br>
Is there a way to make this work?
<br>
<br>
<br>
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:
<br>
<br>
forall n n' x xs xs'.
<br>
Solving: Index n (x ': xs) ~ Index (n'-1) xs'
<br>
Is equivalent to solving: if n /= 0 then (n ~ n', xs ~ xs')
else (x ~ Index (n'-1) xs')
<br>
<br>
Here we could know that "n /= 0" thanks to the match on "sameNat
n1 (Proxy @0)".
<br>
<br>
("weakly" because we have some form of injectivity on the shape
of the list but not on its contents)
<br>
<br>
Any pointer on this kind of stuff in research papers, Coq, Agda,
etc. ?
<br>
<br>
Thanks,
<br>
Sylvain
<br>
<br>
_______________________________________________
<br>
Haskell-Cafe mailing list
<br>
To (un)subscribe, modify options or view archives go to:
<br>
<a class="gmail-m_-6418842020346594588moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
<br>
Only members subscribed via the mailman list are allowed to
post.
<br>
</blockquote>
</blockquote>
</div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>brandon s allbery kf8nh</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a></div></div></div></div></div>