How to declare polymorphic instances for higher-kinded types?
Hello *, For simple-kinded type variables, instances of the type instance NFData a => NFData [a] instance NFData a => NFData (Maybe a) instance (NFData a, NFData b) => NFData (a, b) are common and can be defined effortless; now I wanted do something similiar for a type with a phantom type parameter: {-# LANGUAGE KindSignatures, TypeSynonymInstances #-} import Control.Applicative import Control.Monad data DataBase = DataBase -- specific type not relevant here data Res data Unres -- provides operation to transform an unresolved `Foo_ Unres` to a resolved `Foo_ Res` class Resolvable (e :: * -> *) where resolve :: DataBase -> e Unres -> Either String (e Res) -- trivial /resolvable/ type data Foo_ r = Foo instance Resolvable Foo_ where resolve _ x = return Foo ...it was no problem to define the polymorphic operations outside of an instance: -- Maybe (polymorphic 0 or 1 element container) resolveMaybe :: Resolvable e => DataBase -> Maybe (e Unres) -> Either String (Maybe (e Res)) resolveMaybe db (Just x) = Just <$> resolve db x resolveMaybe db Nothing = pure Nothing -- Pairs resolvePair :: (Resolvable e0, Resolvable e1) => DataBase -> (e0 Unres, e1 Unres) -> Either String (e0 Res, e1 Res) resolvePair db (x,y) = (,) <$> resolve db x <*> resolve db y ...but when I tried to wrap those into polymorphic instances in the style of the instances at the beginning of this mail, I wasn't able to convince GHC: The following attempts wouldn't work: instance Resolvable e => Resolvable (Maybe e) where resolve = resolveMaybe -- GHC fails with: -- Expecting one more argument to `e' -- In the instance declaration for `Resolvable (Maybe e)' Fair enough, but trying to workaround this by defining a type-synonym to get an (*->*)-kinded expression didn't work either, as currying doesn't seem to be supported at the type-level (is there a language-extension for that?): type Maybe_ e r = Maybe (e r) instance Resolvable e => Resolvable (Maybe_ e) where resolve = resolveMaybe -- GHC fails with: -- Type synonym `Maybe_' should have 2 arguments, but has been given 1 -- In the instance declaration for `Resolvable (Maybe_ e)' So, am I really out of luck here, wanting to define polymorphic instances in combination with phantom-types, or is there a trick I haven't thought of yet? PS: while experimenting, I accidentally triggered the following GHC exception: *** Exception: compiler/rename/RnSource.lhs:429:14-81: Irrefutable pattern failed for pattern Data.Maybe.Just (inst_tyvars, _, SrcLoc.L _ cls, _) ...alas I lost the Haskell-code causing this; is this a known issue? Should I try harder to reproduce it again? cheers, hvr --
Hi. Here's a way that seems to work for me. I haven't tested in detail. There may be problems, or also easier ways to achieve the same. The DataKinds extension isn't essential. I've just used it for fun. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
Andres Löh
Here's a way that seems to work for me. I haven't tested in detail. There may be problems, or also easier ways to achieve the same. The DataKinds extension isn't essential. I've just used it for fun.
looks interesting If I get it right, the trick is to use a *-kinded (instead of a *->*-kinded) argument for the class & instances and have a "type function" that is able to phantom-retag an already applied type-constructor `Foo_ Unres` to a differently applied type-constructor `Foo_ Res`. The only thing that disturbs me is that I have to define explicit boilerplate type family declarations for all twenty or so non-polymorphic instances which'd look always the same, i.e. type ResFun (t r) a = t a type ResArg (t r) a = t ~ a ...could that be defined as an override-able default somehow? cheers, hvr --
Hi.
If I get it right, the trick is to use a *-kinded (instead of a *->*-kinded) argument for the class & instances and have a "type function" that is able to phantom-retag an already applied type-constructor `Foo_ Unres` to a differently applied type-constructor `Foo_ Res`.
Yes.
The only thing that disturbs me is that I have to define explicit boilerplate type family declarations for all twenty or so non-polymorphic instances which'd look always the same, i.e.
type ResFun (t r) a = t a type ResArg (t r) a = t ~ a
...could that be defined as an override-able default somehow?
The only way I can quickly think of that might work is to go via another type family. However, this requires "UndecidableInstances": type family GetF e :: Resolved -> * type instance GetF (f x) = f -- provides operation to transform an unresolved `Foo_ Unres` to a resolved `Foo_ Res` class Resolvable e where type ResFun e (a :: Resolved) :: * type ResFun e a = GetF e a type ResArg e (a :: Resolved) :: Constraint type ResArg e a = GetF e a ~ e ... Then, for types like Foo, you can just write: instance Resolvable (Foo_ r) where resolve _ x = return Foo I.e., you shouldn't need the type family declarations. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
Here's another alternative.
newtype Comp f g a = Comp {unComp :: f (g a)}
instance Resolvable e => Resolvable (Maybe `Comp` e) where resolve db = fmap Comp . resolveMaybe db . unComp
One disadvantage of this approach is that it requires you to pepper
your types with explicit compositions of *->* types via Comp.
On Mon, Mar 5, 2012 at 3:14 AM, Herbert Valerio Riedel
Fair enough, but trying to workaround this by defining a type-synonym to get an (*->*)-kinded expression didn't work either, as currying doesn't seem to be supported at the type-level (is there a language-extension for that?):
The Comp newtype provides the type-level currying you were after, which cannot be done with type synonyms. There is no language-extension for that that I'm aware of. If you want to venture down that rabbit hole, maybe take a look at Her. https://personal.cis.strath.ac.uk/~conor/pub/she/ The other disadvantage of this approach is that Comp only works for a fixed number of arguments. Thus *->*->* types, like pairs, requires Comp2.
newtype Comp2 f g h a = Comp2 {unComp2 :: f (g a) (h a)}
instance (Resolvable e0, Resolvable e1) => Resolvable (Comp2 (,) e0 e1) where resolve db = fmap Comp2 . resolvePair db . unComp2
So, if you don't mind adding types like Comp, Comp2, etc throughout the types in your program/library, this let's you keep Resolvable's parameter as (* -> *) and avoids the type families and constraint kinds. I personally prefer the implicitness and generality of Löh's approach, but I also know that some people (perhaps your users) are shy to the newer type extensions. HTH
participants (3)
-
Andres Löh -
Herbert Valerio Riedel -
Nicolas Frisby