Is it possible to have type synonym families for parametrized data such as Data.Param.FSVec?
Ideally, I would like this to compile:
class A e where
type Arg e a
f :: (Arg e a -> b) -> e a -> e b
instance A X where
type Arg X a = Nat size => FSVec size a
f = {- implementation -}
I have tried several workarounds, like wrapping FSVec size a in a newtype, or constraint synonyms, but it seems that I could not get anything reasonable right.
A is a class previously defined (for example) as such:
class OldA e where
f :: (Maybe a -> b) -> [e (Maybe a)] -> [e b]
An example of type inheriting OldA is:
data Y a = Y a
instance Functor Y where
fmap f (Y a) = Y (f a)
instance OldA Y where
f = fmap . fmap
I want to extend this class to be able to express more general function arguments for f. Let's say we have a type X and an associated function fIndependent:
import qualified Data.Param.FSVec as V
import Data.TypeLevel hiding ((==))
data X a = X a deriving Show
fromX (X a) = a
fIndependent :: (Nat size) => (V.FSVec size (Maybe a) -> b) -> [X (Maybe a)] -> [X b]
fIndependent _ [] = []
fIndependent f xs = let x' = (V.reallyUnsafeVector . take c . fmap fromX) xs
xs' = drop c xs
c = V.length x'
in if c == length (V.fromVector x') then X (f x') : fIndependent f xs' else []
fIndependent is sane itself. Testing it with a function
test :: V.FSVec D2 x -> Int
test a = V.length a
will grant the result:
>>> fIndependent test $ map (X . Just) [1,2,3,4,5,6,7,8,9]
[X 2, X 2, X 2, X 2]
Ok, now how to extend OldA? The most "natural" thing that came into my mind is to equip class A with a type synonym family Arg e a as below.
class NewA e where
type Arg e a
f :: (Arg e a -> b) -> [e (Maybe a)] -> [e b]
Converting all existing instances is easy:
instance NewA Y where
type Arg Y a = Maybe a
f = fmap . fmap -- old implementation
To express fIndependent as f is the difficult part, since just adding
instance NewA X where
type Arg X a = (Nat size) => FSVec size (Maybe a) -- wrong!!!
f = {- same as fIndependent -}
does not work. This is what I have trouble with.
Most solutions I saw propose wrapping FSVec inside a newtype. Doing so does not help since the following code:
{-# LANGUAGE RankNTypes #-}
newtype ArgV a = ArgV (forall rate.Nat rate => V.FSVec rate (Maybe a))
instance NewA X where
type Arg X a = ArgV a
g f xs = let x' = (V.reallyUnsafeVector . take c . fmap fromX) xs
xs' = drop c xs
c = V.length x'
in if c == length (V.fromVector x') then X (f $ ArgV x') : g f xs' else []
the type inference system seems to lose the information about size:
Couldn't match type ‘s0’ with ‘rate’ …
because type variable ‘rate’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: Nat rate => V.FSVec rate (Maybe a)
Expected type: V.FSVec rate (Maybe a)
Actual type: V.FSVec s0 (Maybe a)
Relevant bindings include
x' :: V.FSVec s0 (Maybe a)
(bound at ...)
In the first argument of ‘Args’, namely ‘x'’
In the second argument of ‘($)’, namely ‘Args x'’
Compilation failed.
I would appreciate any lead or hint in this matter.
Cirdec's answer explains one of the problems, but its solution given does not exactly answer the question posted. The question asks for an instance X for the class A, with a FSVec type synonym.
The overarching issue here that prevents defining type Arg X = FSVec size a (in any possible configuration) is that type families are not injective. Knowing this and following Cirdec's reasoning, I can think of a workaround to achieve this goal: include a proxy "context" variable in Xs type, to overcome the mentioned issue.
data X c a = X a
instance (Nat n) => A (X n) where
type (X n) a = FSVec n a
f = {- same as fIndependent -}
Of course, this is a quick fix that works for the minimal example (i.e. it answers the question posted), but might not scale well when composing multiple functions like f since there might appear type clashes between the inferred "contexts".
The best solution I can think of would be to add a constraint synonym (as suggested by this answer) for each instance, like:
import qualified Data.Param.FSVec
import Data.TypeLevel
import GHC.Exts -- for Constraint kind
class A e where
type Arg e context a
type Ctx e context :: Constraint
f :: (Ctx e context) => (Arg e context a -> b) -> [e (Maybe a)] -> [e b]
instance A Y where
type Arg Y c a = Maybe a
type Ctx Y c = ()
f = {- same as before -}
instance A X where
type Arg X size a = V.FSVec size (Maybe a)
type Ctx X size = Nat rate
f = {- same as fIndependent -}
But then we would have to deal with the ambiguous types resulted due to the infamous non-injectivity of type families (e.g. Could not deduce: Arg e context0 a ~ Arg e context a). In this case proving injectivity would have to be done manually using the TypeFamilyDependencies extension (based on injective type families) available in GHC 8.0, and define Arg as:
type family Arg (e :: * -> *) context = (r :: * -> *) | r -> context
Of course, this is not possible if the design of the type family is not injective (which is my case), but it is the cleanest solution so far. It is definitely recommended if one can design her type family using the guidelines in the provided paper.