<div dir="ltr"><div>I see, thank you for the explanation, Li-yao. I suppose my TransportVec ended up being quite similar to Rewrite.</div><div><br></div><div>Cheers,</div><div><br></div><div>Jakob<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Feb 18, 2021 at 3:29 PM Li-yao Xia <<a href="mailto:lysxia@gmail.com">lysxia@gmail.com</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">Hi Jakob,<br>
<br>
For some reason the mental model that "pattern-matching brings <br>
constraints into scope" does not apply to type families (I think that's <br>
because "constraints" aren't really a thing at that level). Without such <br>
a feature, you can only pattern-match on preceding variables to make <br>
patterns type-check beforehand. In your example the only other variables <br>
are n and m so you have to split those.<br>
<br>
type family Foo n m (p :: Max n (S m) :~: S (Max n m)) :: () where<br>
Foo O O Refl = '()<br>
Foo O (S m) Refl = '()<br>
Foo (S n) m p = '() -- nontrival because of recursion in the type of p<br>
<br>
Under those draconian constraints, it is convenient to first define <br>
general eliminators for various constructs such as (:~:):<br>
<br>
-- type-level equivalent of Data.Type.Equality.castWith<br>
type family Rewrite (p :: a :~: b) (x :: f a) :: f b where<br>
Rewrite Refl x = x<br>
<br>
then you can apply such eliminators in situations where pattern-matching <br>
is actually not feasible or practical:<br>
<br>
type Foo :: Max n (S m) :~: S (Max n m) -> f (Max n (S m)) -> f (S (Max <br>
n m))<br>
type family Foo (p :: Max n (S m) :~: S (Max n m)) (x :: f (Max n (S <br>
m))) :: f (S (Max n m)) where<br>
Foo p x = Rew p x<br>
-- Good luck doing that by pattern-matching on n and m...<br>
<br>
Note that Rewrite looks like what you'd write at the term level, but it <br>
is actually best thought of as working backwards: first, pattern-match <br>
on a and b (doing an equality test) and then, if they are equal, <br>
pattern-match on Refl (at which point this is really redundant). This <br>
means that Rewrite is *a priori* partial because it does not handle the <br>
case where a and b are distinct; we only know otherwise because there is <br>
no Refl in that case. In contrast, the function castWith uses a <br>
primitive notion of pattern-matching on GADTs, you split (p :: a :~: b) <br>
and there is only once case by definition of (:~:) (before knowing <br>
anything about a and b), where you get handed the underlying equality <br>
constraint.<br>
<br>
Cheers,<br>
Li-yao<br>
<br>
On 2/18/2021 12:36 AM, Jakob Brünker wrote:<br>
> *sigh* sorry, disregard part of this, I missed something obvious. I just <br>
> need to replace `MaxSIsSMaxEQ o` with `Sym (MaxSIsSMaxEQ o)`, and then <br>
> it works.<br>
> <br>
> However, I'm still somewhat confused - the reason why I thought the type <br>
> family application was the problem to begin with is that I tried this:<br>
> <br>
> type Foo :: Max n (S m) :~: S (Max n m) -> ()<br>
> type family Foo p where<br>
> Foo Refl = '()<br>
> <br>
> and it results in the error<br>
> <br>
> • Couldn't match kind: Max n ('S m)<br>
> with: 'S (Max n m)<br>
> Expected kind ‘Max n ('S m) :~: 'S (Max n m)’,<br>
> but ‘Refl’ has kind ‘Max n ('S m) :~: Max n ('S m)’<br>
> • In the first argument of ‘Foo’, namely ‘Refl’<br>
> In the type family declaration for ‘Foo’<br>
> <br>
> What is the reason I can't pattern match on Refl here? I would expect it <br>
> to simply being the constraint `Max n (S m) ~ S (Max n m)` into scope.<br>
> <br>
> Thanks,<br>
> Jakob<br>
> <br>
> On Thu, Feb 18, 2021 at 5:52 AM Jakob Brünker <<a href="mailto:jakob.bruenker@gmail.com" target="_blank">jakob.bruenker@gmail.com</a> <br>
> <mailto:<a href="mailto:jakob.bruenker@gmail.com" target="_blank">jakob.bruenker@gmail.com</a>>> wrote:<br>
> <br>
> Imagine you want to have a type level function that calculates the<br>
> element-wise OR on two bitstrings, encoded as length-indexed vectors<br>
> filled with Bools (this is a simplification of something I need for<br>
> a project). The vectors should be "aligned to the right" as it were,<br>
> such that the new right-most value is True if the right-most value<br>
> of the first vector OR the right-most value of the second vector was<br>
> True.<br>
> <br>
> Example (replacing True and False with 1 and 0 for readability):<br>
> ElementwiseOr [1,0,1,1] [0,1,1,0,0,0,0,1]<br>
> = [0,1,1,0,1,0,1,1]<br>
> <br>
> Its type would be something like<br>
> ElementwiseOr :: Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool<br>
> <br>
> I have written the following code:<br>
> <br>
> ---------------------------------------------------------------------------<br>
> {-# LANGUAGE TypeFamilies, GADTs, DataKinds, StandaloneKindSignatures,<br>
> PolyKinds, TypeOperators, RankNTypes, TypeApplications,<br>
> UndecidableInstances #-}<br>
> <br>
> import Data.Kind<br>
> import Data.Type.Equality<br>
> <br>
> data Nat = Z | S Nat<br>
> <br>
> infixr 5 :<<br>
> <br>
> type Vec :: Nat -> Type -> Type<br>
> data Vec n a where<br>
> Nil :: Vec Z a<br>
> (:<) :: a -> Vec n a -> Vec (S n) a<br>
> <br>
> type Cong :: forall f -> a :~: b -> f a :~: f b<br>
> type family Cong f p where<br>
> Cong f Refl = Refl<br>
> <br>
> type Max :: Nat -> Nat -> Nat<br>
> type family Max n m where<br>
> Max Z m = m<br>
> Max n Z = n<br>
> Max (S n) (S m) = S (Max n m)<br>
> <br>
> -- The reason for this slightly convoluted Ordering type is that it<br>
> seems<br>
> -- to make the "right-alignment" easier.<br>
> type NatOrdering :: Ordering -> Nat -> Nat -> Type<br>
> data NatOrdering o n m where<br>
> NOLTE :: NatOrdering EQ n m -> NatOrdering LT n (S m)<br>
> NOLTS :: NatOrdering LT n m -> NatOrdering LT n (S m)<br>
> NOEQZ :: NatOrdering EQ Z Z<br>
> NOEQS :: NatOrdering EQ n m -> NatOrdering EQ (S n) (S m)<br>
> NOGTE :: NatOrdering EQ n m -> NatOrdering GT (S n) m<br>
> NOGTS :: NatOrdering GT n m -> NatOrdering GT (S n) m<br>
> <br>
> type MaxSIsSMaxEQ<br>
> :: forall n m . NatOrdering EQ n m -> Max n (S m) :~: S (Max n m)<br>
> type family MaxSIsSMaxEQ o where<br>
> MaxSIsSMaxEQ NOEQZ = Refl<br>
> MaxSIsSMaxEQ (NOEQS o) = Cong S (MaxSIsSMaxEQ o)<br>
> <br>
> type TransportVec :: n :~: m -> Vec n a -> Vec m a<br>
> type family TransportVec p v where<br>
> TransportVec Refl v = v<br>
> <br>
> type ElementwiseOr<br>
> :: NatOrdering o n m -> Vec n Bool -> Vec m Bool -> Vec (Max n m)<br>
> Bool<br>
> type family ElementwiseOr o u v where<br>
> ElementwiseOr (NOLTE o) u (s :< v) =<br>
> TransportVec (MaxSIsSMaxEQ o) (s :< ElementwiseOr o u v) -- XXX<br>
> -- other equations ommitted<br>
> ---------------------------------------------------------------------------<br>
> <br>
> To me, the equation at the end marked with XXX seems like it should<br>
> work. However, it produces the following error:<br>
> <br>
> • Couldn't match kind: Max n ('S m)<br>
> with: 'S (Max n m)<br>
> Expected kind ‘'S (Max n m) :~: 'S (Max n m)’,<br>
> but ‘MaxSIsSMaxEQ o’ has kind ‘Max n ('S m) :~: 'S (Max n m)’<br>
> • In the first argument of ‘TransportVec’, namely<br>
> ‘(MaxSIsSMaxEQ o)’<br>
> <br>
> So it expects something of kind `S (Max n m) :~: S (Max n m)` - it<br>
> seems like Refl fits that bill, but that doesn't work either,<br>
> because replacing (MaxSIsSMaxEQ o) with Refl means that TransportVec<br>
> returns a type of the wrong kind, producing a very similar error.<br>
> <br>
> I suspect the reason this doesn't work is because type equality<br>
> isn't equipped to properly handle type family applications. I could<br>
> potentially work around this if I defined Max as<br>
> <br>
> data Max n m r where<br>
> MaxZZ :: Max Z Z Z<br>
> MaxSZ :: Max (S n) Z (S n)<br>
> MaxZS :: Max Z (S m) (S m)<br>
> MaxSS :: Max n m r -> Max (S n) (S m) (S r)<br>
> <br>
> However, dealing with a proof object like this is a lot less<br>
> convenient than just being able to use a type family for most<br>
> purposes, so I'd like to avoid this if possible.<br>
> <br>
> Is there a way to make this work while sticking with type families?<br>
> <br>
> Thanks<br>
> <br>
> Jakob<br>
> <br>
> <br>
> _______________________________________________<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.<br>
> <br>
_______________________________________________<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>