[Haskell-cafe] Specific to General to Specific

[Ivan Lazar Miljenovic]

On 19 August 2010 08:11, Edward Z. Yang <ezyang at mit.edu> 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 at gmail.com
IvanMiljenovic.wordpress.com