I'd like to use existentially sized image windows for a couple of reasons:
- I'd like to pack different size windows into the same list.
- I'd like to make a
Zip
instance for my window type.
I'm using this code to do this:
-- | A "matrix" represented as a composition of sized vectors.
type Mat h w = Vector h :.: Vector w
-- | A handy alias for locating a window in the 2D plane.
type Orig = (Integer,Integer)
-- | An attempt at using `singletons` to define windows.
data Wind :: Nat -> Nat -> Type -> Type where -- height -> width
Wind
:: (KnownNat h, KnownNat w)
=> { img :: Mat h w a -- ^ image data matrix
, ll :: Orig -- ^ position of lower-left corner
, dflt :: a -- ^ out-of-bounds value
} -> Wind h w a
data SomeWind a :: Type where
MkSomeWind :: Sing h -> Sing w -> Wind h w a -> SomeWind a
Now, I need to make a HasRep
instance for my SomeWind
type:
import qualified ConCat.Rep as R
instance R.HasRep (SomeWind a) where
type Rep (SomeWind a) = ???
repr (MkSomeWind _ _ (Wind im orig def)) = (im, (orig, def))
abst (im :: (Vector h :.: Vector w) a, (orig, def)) =
MkSomeWind (SNat :: Sing h) (SNat :: Sing w) (Wind im orig def)
I have a nagging hunch that I ought to be able to use the singletons library to help me replace the "???" above with a correct definition, but I can't figure out how.
Can anyone help?