[Haskell-cafe] How to deal with type family applications in type equalities?
Jakob Brünker
jakob.bruenker at gmail.com
Thu Feb 18 17:00:53 UTC 2021
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 <lysxia at gmail.com> 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 <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.
> >
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210218/1793a7cb/attachment.html>
More information about the Haskell-Cafe
mailing list