level constraints in instances of type families
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.
Context + minimal working example
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 ea 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.
Try-outs
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.
It appears that you are using a class Nat :: k -> Constraint and a data type FSVec :: k -> * -> * . The data type is constrained with the old DatatypeContexts extension.
{-# LANGUAGE DatatypeContexts #-}
class Nat n
data Nat n => FSVec n a = FSVec -- ...
You have an existing class A :: (* -> *) -> Constraint which you'd like to write an FSVec instance for.
class A e where
--- ...
f :: ( {- ... -} b) -> e a -> e b
But FSVec can never have an A instance, because it's a kind mismatch. The class A requires a type argument with the kind * -> * but FSVec has the kind k -> * -> * . You've already run into a problem, and aren't even using the type family yet. If you try to do this (hand waving away what the type family argument is for now)
data X = X
instance A (FSVec) where
type Arg FSVec a = X
f = undefined
You get a compiler error.
Expecting one more argument to `FSVec'
The first argument of `A' should have kind `* -> *',
but `FSVec' has kind `* -> * -> *'
In the instance declaration for `A (FSVec)'
Everything before here, including the compiler error, is useful information for communicating the problem you are having and is useful in asking for help.
Fortunately it's a really easy problem to fix. If you pick some natural number n , then FSVec n has the kind * -> * , which matches the kind of the type argument to A . You can start writing an instance A (FSVec n)
instance A (FSVec n) where
f = -- ...
When you reintroduce the complete class definition with type families
{-# LANGUAGE TypeFamilies #-}
class A e where
type Arg e a
f :: (Arg e a -> b) -> e a -> e b
The solution is still to write an A instance for FSVec n instead of for FSVec . Now that n has moved into the instance declaration, there's an obvious place to capture the needed Nat n context.
instance Nat n => A (FSVec n) where
type Arg (FSVec n) a = FSVec n a
f = undefined -- ...
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 X s 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 (ie 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 (eg 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.
链接地址: http://www.djcxy.com/p/66630.html上一篇: 数据族vs内射型家族
下一篇: 类型家族情况下的级别约束