Haskell: Specify the function satisfying a typeclass will take some specific type satisfying a constraint

Question

I think I want to effectively do something like this:

class (forall z. ListZip z) => PlaneZip p where... --functions using z excluded

In short, but more precisely, I want to have

class A p where ... --definition excluded
class C p where
  foo :: (A z) => p (z a) -> a
data Alpha a = ...definition excluded
data Beta a = ...definition excluded
instance A Alpha where --definition excluded
bar :: Beta (Alpha a) -> a
instance C Beta where
  foo = bar

This is impossible, since foo must allow for z to be anything which is an A, not Alpha specifically. How do I make it possible, enforcing that foo must take some A but not any A?

In more detail, I have numerous list zippers which I want to make instances of Comonad. Instead of creating a list zipper type and making lots of wrappers around it, I decided to make a class ListZip, and make multiple types which are instances of it. That is,

class (Functor z) => ListZip z where
    leftMv :: z a -> z a
    rightMv :: z a -> z a --further functions excluded

data ListZipInf a = ListZipInf ([a]) a ([a]) deriving (Show)
instance ListZip ListZipInf where... --functions excluded
data ListZipTorus a = ListZipTorus [a] a [a] deriving (Show)
instance ListZip ListZipTorus where.. --functions excluded

Now I want to make similar zippers for 2d lists - plane zippers -

data PlaneZipInf a = PlaneZipInf (ListZipInf (ListZipInf a)) deriving (Show)
data PlaneZipTorus a = PlaneZipTorus (ListZipTorus (ListZipTorus a)) deriving (Show)

And finally, I want to make a similar plane zipper typeclass, which will allow me to have a default implementation for a way to pull a single element, the 'focus' out of this list zipper, given a way to 'unwrap' the plane zipper constructor:

class PlaneZip p where
  unwrap :: (ListZip z) => p (z (z a)) -> z (z a)
  counit :: (ListZip z, Comonad z) => p (z (z a)) -> a
  counit p =
    let zs = unwrap p
      in extract $ extract zs

This however doesn't work, in particular

instance PlaneZip PlaneZipInf where
    unwrap (PlaneZipInf zs) = zs

Gives me an error - Could not deduce a ~ (ListZipInf (ListZipInf a)) It expects a function that works for any ListZip, but I gave it a function that provides a particular one.

How could I express that I want unwrap to take a type p (z (z a)), where z is some type which is an instance of ListZip, and produce a (z (z a))?

Thanks

It seems like you want an associated type in the PlaneZip class, and a superclass constraint in PlaneZip stating that type must be an instance of ListZip. Maybe you even want z to be existentially quantified. I'm not sure that p (z (z a)) -> z (z a) is correct, however, because \(PlaneZipInf zs) -> zs has type PlaneZipInf a -> ListZipInf (ListZipInf a) which doesn't match the above type. — user2407038

Alec Alec · Accepted Answer · 2016-10-02T06:14:52

I may be misunderstanding your question, but in your case it seems that you will always end up creating plane zippers from nesting list zippers. If that is the case, it seems more advisable to simply do something like the following:

{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}

data PlaneZip z a = PlaneZipInf (z (z a))
deriving instance (Show a, Show (z a), Show (z (z a))) => Show (PlaneZip z a)

type PlaneZipInf a = PlaneZip ListZipInf a
type PlaneZipTorus a = PlaneZip ListZipTorus a

unwrap :: PlaneZip z a -> z (z a)
unwrap (PlaneZip zs) = zs

counit :: Comonad z => PlaneZip z a -> a
counit p =
    let zs = unwrap p
      in extract $ extract zs

If you really want to be sure that the z in PlaneZip z a is always a ListZip, you can use the following GADT instead

{-# LANGUAGE GADTs #-}
data PlaneZip z a where
  PlaneZip :: ListZip z => z (z a) -> PlaneZip z a

If this is not the case, feel free to reply - I believe there is also something else that could be done here with associated type families, but the solution above is much better.

Haskell: Specify the function satisfying a typeclass will take some specific type satisfying a constraint

2 Answers