[Haskell-cafe] How to deal with type family applications in type equalities?

[Li-yao Xia]

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 <jakob.bruenker at gmail.com 
> <mailto:jakob.bruenker at 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.
>