To alleviate this we’re looking into ways to abstract this away.
To start, we would like do define something like
class Some t where
type SomeT t
useSome :: (forall a. t a -> c) -> SomeT t -> c
This fails when we try to write instance Some Foo because Foo has two type parameters, while, in the definition of Some, t is required to have only one.
We noticed that we could work around this issue by rewriting Foo as
data Foo' (c :: (Type, Type))
but I was wondering if there were more generic way to approach the issue.
I suspect this may be an XY problem. Perhaps if you explain what the code does you can get help to find a simpler implementation?
Regarding your question, you can define a different data type for each number of type variables. Something like this:
data Some1 f = forall a. Some1 (f a)
useSome1 :: (forall a. f a -> r) -> Some1 f -> r
useSome1 k (Some1 f) = k f
data Some2 f = forall a b. Some2 (f a b)
useSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
useSome2 k (Some2 f) = k f
data Some3 ...
data Foo = forall a. Foo a
data Bar = forall b. Bar b
data Baz = forall c. Baz c
stuff :: Foo -> Bar -> Baz -> ()
stuff foo bar baz = runIdentity do
Foo a <- pure foo
Bar b <- pure bar
Baz c <- pure baz
pure ()
If you are not bothered by a slight performance and verbosity overhead, you can try something like this:
{-# LANGUAGE GADTs #-}
module Some
( Some (..),
Uncurry (..),
some2,
fail,
(>>=),
)
where
import Prelude hiding ((>>=))
data Some f = forall a. Some (f a)
(>>=) :: Some f -> (forall a. f a -> r) -> r
(Some x) >>= k = k x
data Uncurry f t where
UC :: {getUncurry :: f a b} -> Uncurry f (a, b)
some2 :: f a b -> Some (Uncurry f)
some2 x = Some (UC x)
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QualifiedDo #-}
import Some
data Foo1 a = Foo1 Int
data Foo2 a b = Foo2 Int
test :: Int
test = Some.do
Foo1 n <- Some (Foo1 1)
UC (Foo2 m) <- some2 (Foo2 2)
n + m
The last thing which I’m not sure how to handle are constraints.
Consider
data Foo a where
Foo :: Bar a => Int -> Foo a
data SomeFoo = forall a. Bar a => SomeFoo (Foo a)
useSomeFoo :: (forall a. Bar a => Foo a -> b) -> SomeFoo -> b
If I used Some and withSome from Data.Some instead, I wouldn’t be able to encode the Bar a constraint.
Is there a way to circumvent this issue and encode the constraint in Some?
The constraint is already provided by Foo; putting it in SomeFoo is just duplication. You can use a constraint-agnostic Some Foo and recover the constraint by pattern matching on Foo i.
This approach with pattern matching works almost perfectly.
There is still one case where I’m not sure how to make it work.
If I have a foo :: Foo a I can retrieve the Bar a constraint just by pattern matching on foo. But if I have a mFoo :: Maybe (Foo a), how can I retrieve the constraint on a? If I pattern match, I can obtain the constraint only for the Just case, and I’m stuck in the Nothing case.
One way out I see is defining something like
data MaybeFoo a where
NothingFoo :: Bar a => MaybeFoo a
JustFoo :: Bar a => Int -> Foo a
It’s not clear to me that the solution to the concrete example is not just to have foo take an explicit IsCurrency to constraint, like convert.
That said, you can always factor out your Bar constraint into another type and pair it up when necessary.
{-# LANGUAGE GHC2021, NoStarIsType, PatternSynonyms #-}
module FooBar where
import Data.Functor.Product
import Data.Functor.Compose
type (.) = Compose
type (*) = Product
infixr 9 .
infixr 8 *
data Some f where
Some :: f a -> Some f
data Sat c a where
Sat :: c a => Sat c a
{-# COMPLETE PS #-}
pattern PS :: () => c a => f a -> (Sat c * f) a
pattern PS fx = Pair Sat fx
{-# COMPLETE PSC #-}
pattern PSC :: () => c a => f (g a) -> (Sat c * f . g) a
pattern PSC fgx = PS (Compose fgx)
class Bar (a :: k)
-- Remove `Bar` constraint from `Foo`.
data Foo (a :: k) where
Foo :: Int -> Foo a
-- Instead pair the `Bar` constraint with whatever transformation of `Foo`.
type FooBar k f = Sat Bar * f . Foo @k
-- The types have the right shape for `Some`.
eg :: Some (FooBar k f) -> (forall (a :: k). Bar a => f (Foo a) -> r) -> r
eg (Some (PSC ffx)) k = k ffx
Edit
Another approach would be to capture a quantified constraint in ExchangeRate:
data ExchangeRate from to where
ER :: (IsCurrency from => IsCurrency to) => ExchangeRate from to
Then neither convert nor foo require IsCurrency constraints.