2

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?

dbanas
  • 1,707
  • 14
  • 24
  • Well, it must be another existential type, mustn't it? Presumably `(SomeMat a, (Orig, a))`. I don't think the singletons make much difference here. — Anyways I find it dubious that you're using dependently-typed dimensions here: since the origin isn't fixed, different `Wind`s won't necessarily match even if they have the same type. – leftaroundabout Nov 14 '18 at 19:24

0 Answers0