Open srid opened 4 years ago
I see. This is somewhat tricky.
In a special case of when Bar
has only one such GADT field,
and all fields are finite we could generate code as below:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -ddump-splices #-}
import Data.Some
import Data.Universe
import Data.Universe.Some
import Data.Universe.Helpers
import Data.Universe.Some.TH
import Data.GADT.Show
data Foo a where
MkFoo :: Ordering -> Foo Bool
deriving instance Show (Foo a)
instance GShow Foo where gshowsPrec = showsPrec
data Bar a where
MkBar :: Foo a -> Bool -> Ordering -> Bar a
deriving instance Show (Bar a)
instance GShow Bar where gshowsPrec = showsPrec
deriveUniverseSome ''Foo
instance FiniteSome Foo
-- deriveUniverseSome ''Bar
instance UniverseSome Bar where
universeSome =
withSomeM universeFSome $ \x ->
universeF >>= \y ->
universeF >>= \z ->
[mkSome $ MkBar x y z]
instance FiniteSome Bar where
universeFSome = universeSome
-- prints
-- Some (MkBar (MkFoo LT) False LT)
-- Some (MkBar (MkFoo LT) False EQ)
-- Some (MkBar (MkFoo LT) False GT)
-- Some (MkBar (MkFoo LT) True LT)
-- Some (MkBar (MkFoo LT) True EQ)
-- Some (MkBar (MkFoo LT) True GT)
-- Some (MkBar (MkFoo EQ) False LT)
-- Some (MkBar (MkFoo EQ) False EQ)
-- Some (MkBar (MkFoo EQ) False GT)
-- Some (MkBar (MkFoo EQ) True LT)
-- Some (MkBar (MkFoo EQ) True EQ)
-- Some (MkBar (MkFoo EQ) True GT)
-- Some (MkBar (MkFoo GT) False LT)
-- Some (MkBar (MkFoo GT) False EQ)
-- Some (MkBar (MkFoo GT) False GT)
-- Some (MkBar (MkFoo GT) True LT)
-- Some (MkBar (MkFoo GT) True EQ)
-- Some (MkBar (MkFoo GT) True GT)
--
main :: IO ()
main = mapM_ print (universeSome :: [Some Bar])
There are two points:
Finiteness allows us to write universeSome
using withSomeM
and >>=
,
as we don't need to go in diagonals.
There can be at most one GADT field (i.e Field of type f x
such that f
has FiniteSome
instance),
because if we have many, like in
data Quu a where
MkQuu :: Foo a -> Bar a -> Quu a
instance UniverseSome Quu where
universeSome =
withSomeM universeFSome $ \x ->
withSomeM universeFSome $ \y ->
[mkSome $ MkQuu x y]
we'll run into problem that indexes don't match.
Even in this case we can manually show that Foo a
and Bar b
have
always index Int
so the above makes sense, it's tedious and probably
not common to enough to do that.
So I could add deriveFiniteSome
to universe-some
, which would
derive UniverseSome
and FiniteSome
as outlined above.
Will that be enough?
@srid Could you check https://github.com/dmwit/universe/pull/54, whether it solves your issue.
This works:
But if you replace that
MkBar
's argument (Int
) withFoo a
, it will fail:The compile error being:
I'd think it should be using the
SomeUniverse Foo
(orUniverse (Some Foo)
) instance instead?