Re: [Haskell-cafe] Specific to General to Specific

18 Aug 2010

      On 19 August 2010 08:11, Edward Z. Yang  wrote:
...
Imagine that I have the following type-class:
   class (Monad (m n)) => NetworkMonad m n
   data NT n a
   instance NetworkMonad NT n
   data NQ n a
   instance NetworkMonad NQ n
   monadicValue :: NetworkMonad m n => m n ()
It defines some family of phantom monads, in this case NT n and NQ n, and
permits some values to inhabit either monad (resolved by the surrounding code).
Suppose, however, that there are multiple possible implementations for the pair
(NT, NQ).  Then we might like to generalize this typeclass with an associated
type.  (Suppose that our old implementation was g = Int.)
   {-# LANGUAGE TypeFamilies #-}
   {-# LANGUAGE MultiParamTypeClasses #-}
   {-# LANGUAGE FlexibleContexts #-}
   class Network g where
       data GNT g :: * -> * -> *
       data GNQ g :: * -> * -> *
   class (Monad (m g n)) => GenericNetworkMonad g m n
   type NT n a = GNT Int n a
   type NQ n a = GNQ Int n a
   genericMonadicValue :: GenericNetworkMonad g m n => m g n ()
   genericMonadicValue = undefined
   monadicValue :: GenericNetworkMonad Int m n => m Int n ()
   monadicValue = undefined
My question is, how can I write a specialized typeclass NetworkMonad
that recaptures the original simple interface?
   monadicValue' :: NetworkMonad m n => m n ()
   monadicValue' = undefined
I've tried something like this:
   type family GetM (x :: * -> * -> *) :: (* -> * -> * -> *)
   type instance GetM (m g) = m
   type family GetG (x :: * -> * -> *) :: *
   type instance GetG (m g) = g
   class (GenericNetworkMonad (GetG mg) (GetM mg) n) => NetworkMonad mg n where
But this doesn't seem to be enough information to do inference with:
   monadicValue'' :: NetworkMonad m n => m n ()
   monadicValue'' = genericMonadicValue
gives the type error:
   Test.hs:28:17:
       Could not deduce (GenericNetworkMonad g m n)
         from the context (NetworkMonad m1 n)
         arising from a use of `genericMonadicValue' at Test.hs:28:17-35
       Possible fix:
         add (GenericNetworkMonad g m n) to the context of
           the type signature for `monadicValue'''
       In the expression: genericMonadicValue
       In the definition of `monadicValue''':
           monadicValue'' = genericMonadicValue
   Test.hs:28:17:
       Couldn't match expected type `m1' against inferred type `m g'
         `m1' is a rigid type variable bound by
              the type signature for `monadicValue''' at Test.hs:27:31
       In the expression: genericMonadicValue
       In the definition of `monadicValue''':
           monadicValue'' = genericMonadicValu
Am I out of luck without superclass equality constraints?
If I understand what you're wanting correctly, then something like
this might work:

class Foo c v | c -> v where
  ...

class (Foo (c v) v) => Bar c v where
  ...

I've used this to "simulate" superclass equality constraints, with the
expectation of dumping MPTCs+FunDeps as soon as real superclass
equality constraints are available with type families.

-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic@gmail.com
IvanMiljenovic.wordpress.com