<div dir="ltr"><div>*sigh* sorry, disregard part of this, I missed something obvious. I just need to replace
`MaxSIsSMaxEQ o` with `Sym (MaxSIsSMaxEQ o)`, and then it works.</div><div><br></div><div>However, I'm still somewhat confused - the reason why I thought the type family application was the problem to begin with is that I tried this:</div><div><br></div><div> type Foo :: Max n (S m) :~: S (Max n m) -> ()<br> type family Foo p where<br> Foo Refl = '()</div><div><br></div><div>and it results in the error</div><div><br></div><div> • 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’</div><div><br></div><div>What is the reason I can't pattern match on Refl here? I would expect it to simply being the constraint `Max n (S m) ~ S (Max n m)` into scope.<br></div><div><br></div><div>Thanks,</div><div>Jakob<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Feb 18, 2021 at 5:52 AM Jakob Brünker <<a href="mailto:jakob.bruenker@gmail.com">jakob.bruenker@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"><div dir="ltr"><div>Imagine you want to have a type level function that calculates the element-wise OR on two bitstrings, encoded as length-indexed vectors filled with Bools (this is a simplification of something I need for a project). The vectors should be "aligned to the right" as it were, such that the new right-most value is True if the right-most value of the first vector OR the right-most value of the second vector was True.<br></div><div><br></div><div>Example (replacing True and False with 1 and 0 for readability):</div><div>ElementwiseOr [1,0,1,1] [0,1,1,0,0,0,0,1]</div><div>= [0,1,1,0,1,0,1,1]<br></div><div><br></div><div>Its type would be something like</div><div>ElementwiseOr :: Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool<br></div><div><br></div><div>I have written the following code:</div><div><br></div><div>---------------------------------------------------------------------------</div><div>{-# 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)</div><div>
<div><br></div><div>-- The reason for this slightly convoluted Ordering type is that it seems</div><div>-- to make the "right-alignment" easier.<br></div><div>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</div>
<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) 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</div><div>---------------------------------------------------------------------------</div><div><br></div><div>To me, the equation at the end marked with XXX seems like it should work. However, it produces the following error:</div><div><br></div><div> • 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)’</div><div><br></div><div>So it expects something of kind `S (Max n m) :~: S (Max n m)` - it seems like Refl fits that bill, but that doesn't work either, because replacing (MaxSIsSMaxEQ o) with Refl means that TransportVec returns a type of the wrong kind, producing a very similar error.<br><br></div><div>I suspect the reason this doesn't work is because type equality isn't equipped to properly handle type family applications. I could potentially work around this if I defined Max as<br><br></div><div>data Max n m r where</div><div> MaxZZ :: Max Z Z Z</div><div> MaxSZ :: Max (S n) Z (S n)</div><div> MaxZS :: Max Z (S m) (S m)</div><div> MaxSS :: Max n m r -> Max (S n) (S m) (S r)<br></div><div><br></div><div>However, dealing with a proof object like this is a lot less convenient than just being able to use a type family for most purposes, so I'd like to avoid this if possible.</div><div><br></div><div>Is there a way to make this work while sticking with type families?</div><div><br></div><div>Thanks</div><div><br></div><div>Jakob<br></div></div>
</blockquote></div>