I see, thank you for the explanation, Li-yao. I suppose my TransportVec ended up being quite similar to Rewrite. Cheers, Jakob On Thu, Feb 18, 2021 at 3:29 PM Li-yao Xia wrote:

Hi Jakob,

For some reason the mental model that "pattern-matching brings constraints into scope" does not apply to type families (I think that's because "constraints" aren't really a thing at that level). Without such a feature, you can only pattern-match on preceding variables to make patterns type-check beforehand. In your example the only other variables are n and m so you have to split those.

type family Foo n m (p :: Max n (S m) :~: S (Max n m)) :: () where Foo O O Refl = '() Foo O (S m) Refl = '() Foo (S n) m p = '() -- nontrival because of recursion in the type of p

Under those draconian constraints, it is convenient to first define general eliminators for various constructs such as (:~:):

-- type-level equivalent of Data.Type.Equality.castWith type family Rewrite (p :: a :~: b) (x :: f a) :: f b where Rewrite Refl x = x

then you can apply such eliminators in situations where pattern-matching is actually not feasible or practical:

type Foo :: Max n (S m) :~: S (Max n m) -> f (Max n (S m)) -> f (S (Max n m)) type family Foo (p :: Max n (S m) :~: S (Max n m)) (x :: f (Max n (S m))) :: f (S (Max n m)) where Foo p x = Rew p x -- Good luck doing that by pattern-matching on n and m...

Note that Rewrite looks like what you'd write at the term level, but it is actually best thought of as working backwards: first, pattern-match on a and b (doing an equality test) and then, if they are equal, pattern-match on Refl (at which point this is really redundant). This means that Rewrite is *a priori* partial because it does not handle the case where a and b are distinct; we only know otherwise because there is no Refl in that case. In contrast, the function castWith uses a primitive notion of pattern-matching on GADTs, you split (p :: a :~: b) and there is only once case by definition of (:~:) (before knowing anything about a and b), where you get handed the underlying equality constraint.

Cheers, Li-yao

On 2/18/2021 12:36 AM, Jakob Brünker wrote:

...

*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.

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:

type Foo :: Max n (S m) :~: S (Max n m) -> () type family Foo p where Foo Refl = '()

and it results in the error

• Couldn't match kind: Max n ('S m) with: 'S (Max n m) Expected kind ‘Max n ('S m) :~: 'S (Max n m)’, but ‘Refl’ has kind ‘Max n ('S m) :~: Max n ('S m)’ • In the first argument of ‘Foo’, namely ‘Refl’ In the type family declaration for ‘Foo’

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.

Thanks, Jakob

On Thu, Feb 18, 2021 at 5:52 AM Jakob Brünker mailto:jakob.bruenker@gmail.com> wrote:

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.

Example (replacing True and False with 1 and 0 for readability): ElementwiseOr [1,0,1,1] [0,1,1,0,0,0,0,1] = [0,1,1,0,1,0,1,1]

Its type would be something like ElementwiseOr :: Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool

I have written the following code:

---------------------------------------------------------------------------

...

{-# LANGUAGE TypeFamilies, GADTs, DataKinds,

StandaloneKindSignatures,

...

PolyKinds, TypeOperators, RankNTypes, TypeApplications, UndecidableInstances #-}

import Data.Kind import Data.Type.Equality

data Nat = Z | S Nat

infixr 5 :<

type Vec :: Nat -> Type -> Type data Vec n a where Nil :: Vec Z a (:<) :: a -> Vec n a -> Vec (S n) a

type Cong :: forall f -> a :~: b -> f a :~: f b type family Cong f p where Cong f Refl = Refl

type Max :: Nat -> Nat -> Nat type family Max n m where Max Z m = m Max n Z = n Max (S n) (S m) = S (Max n m)

-- The reason for this slightly convoluted Ordering type is that it seems -- to make the "right-alignment" easier. type NatOrdering :: Ordering -> Nat -> Nat -> Type data NatOrdering o n m where NOLTE :: NatOrdering EQ n m -> NatOrdering LT n (S m) NOLTS :: NatOrdering LT n m -> NatOrdering LT n (S m) NOEQZ :: NatOrdering EQ Z Z NOEQS :: NatOrdering EQ n m -> NatOrdering EQ (S n) (S m) NOGTE :: NatOrdering EQ n m -> NatOrdering GT (S n) m NOGTS :: NatOrdering GT n m -> NatOrdering GT (S n) m

type MaxSIsSMaxEQ :: forall n m . NatOrdering EQ n m -> Max n (S m) :~: S (Max n m) type family MaxSIsSMaxEQ o where MaxSIsSMaxEQ NOEQZ = Refl MaxSIsSMaxEQ (NOEQS o) = Cong S (MaxSIsSMaxEQ o)

type TransportVec :: n :~: m -> Vec n a -> Vec m a type family TransportVec p v where TransportVec Refl v = v

type ElementwiseOr :: NatOrdering o n m -> Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool type family ElementwiseOr o u v where ElementwiseOr (NOLTE o) u (s :< v) = TransportVec (MaxSIsSMaxEQ o) (s :< ElementwiseOr o u v) -- XXX -- other equations ommitted

---------------------------------------------------------------------------

...

To me, the equation at the end marked with XXX seems like it should work. However, it produces the following error:

• Couldn't match kind: Max n ('S m) with: 'S (Max n m) Expected kind ‘'S (Max n m) :~: 'S (Max n m)’, but ‘MaxSIsSMaxEQ o’ has kind ‘Max n ('S m) :~: 'S (Max n

m)’

...

• In the first argument of ‘TransportVec’, namely ‘(MaxSIsSMaxEQ o)’

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.

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

data Max n m r where MaxZZ :: Max Z Z Z MaxSZ :: Max (S n) Z (S n) MaxZS :: Max Z (S m) (S m) MaxSS :: Max n m r -> Max (S n) (S m) (S r)

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.

Is there a way to make this work while sticking with type families?

Thanks

Jakob

_______________________________________________ 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.