Inferring general typeclass instance from a series of smaller ones?
the title of this is admittedly not very descriptive, but I don't know how else to describe this in a short title. I'd appreciate any recommendations!
I'm going to be presenting a very simplified version of my issue :)
So I have a typeclass
class Known f a where
known :: f a
That is supposed to be able to generate the canonical construction of a given type at a certain index, useful for working with GADT's and stuff. I'm giving a simplified version of this, with the relavant parts.
So there's obviously an instance for Proxy :
instance Known Proxy a where
known = Proxy
Which we can use:
> known :: Proxy Monad
Proxy
But there's also an instance for this HList-like type:
data Prod f :: [k] -> * where
PNil :: Prod f '[]
(:<) :: f a -> Prod f as -> Prod f (a ': as)
infixr 5 (:<)
Where a Prod f '[a,b,c] would be roughly equivalent to a (fa, fb, fc) tuple. Same Functor, different types.
Writing the instance is decently straightforward:
instance Known (Prod f) '[] where
known = PNil
instance (Known f a, Known (Prod f) as) => Known (Prod f) (a ': as) where
known = known :< known
Which works out pretty well: (assuming a Show instance)
> known :: Prod Proxy '[1,2,3]
Proxy :< Proxy :< Proxy :< PNil
But, I'm in the case where I need to make a "polymorphic" function on all as ...but GHC is not liking it.
asProds :: forall as. Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as
It comes up with this error:
No instance for (Known (Prod f) as)
arising from a use of 'known'
Which I guess is saying that GHC can't show that there will be an instance it will pick that will work for any as , or, it doesn't have a strategy to construct known for that instance.
I as a human know that this is the case, but is there any way I can get this to work? The instances are all "in scope" and available...but how can I tell GHC how to construct it in a way that it is satisfied?
If there's no constraint for a class, you can't use its methods. Just add the constraint:
asProds :: forall as. Known (Prod Proxy) as => Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as
Note that GHC can infer this type:
asProds (_ :: Proxy as) = known :: Prod Proxy as
-- inferred constraint
Since types are erased, there's nothing from which instances could be built runtime in the absence of a dictionary to begin with. It might well be logically true that there exists instances for all inhabitants of a kind, but for programs we need dictionaries - constructive proofs - to run.
Writing out the constraints shouldn't bother us much, since if we have instances for all cases, then when we need an instance, we can usually get one, with not-too-frequent exceptions. The exception is when we want instances for an open type with type family applications. In that case we have to write functions that explicitly build instances at the desired type from other known instances.
链接地址: http://www.djcxy.com/p/43540.html下一篇: 从一系列较小的类推出一般的类型类实例？