enumerateConstructors is not good

andrewthad commented 8 years ago

In the Data.Case.Enumerate module, there's a little TH function that can be used to do the same thing on every branch of a pattern match. This is useful for when you are pattern matching on a GADT and all of the branches have different types that satisfy the same typeclasses. A decent example of when to use this is given in the haddocks.

Two bad things. One is that is takes a type name to get the constructors and then implicitly promotes it to the singletonized type for pattern matching. That's kind of bad. Instead, it should use the same type. So, instead of giving it something like ''Bool as the second argument, it would make more sense to give it ''SBool, which is a type synonym for a data instance. I don't how how to work with those in template haskell. Two, it should really be able to infer the type of the thing it's pattern matching on, but I don't know if this is actually possible.

andrewthad commented 8 years ago

@parsonsmatt

andrewthad commented 8 years ago

I really need to check the examples I put in the haddocks. I've added a working example: https://github.com/andrewthad/pringletons/commit/e6bbb1a857f35bcbf76a13f9d55b1fef79f900a1

parsonsmatt commented 8 years ago

Notes so far

Type synonyms can be reified with TH, and give their underlying stuff:

λ> type Foo = Maybe
λ> $(stringE . show =<< reify ''Foo)
"TyConI (TySynD Ghci2.Foo [] (ConT GHC.Base.Maybe))"

Reification of SBool gives:

λ> :i SBool
type SBool = Sing
        -- Defined in ‘singletons-2.0.1:Data.Singletons.Prelude.Instances’
λ> $(stringE . show =<< reify ''SBool)
"TyConI (TySynD Data.Singletons.Prelude.Instances.SBool [] (SigT (ConT Data.Singleto
ns.Sing) (AppT (AppT ArrowT (ConT GHC.Types.Bool)) StarT)))"

SigT t k is the TH rep for (t :: k).

Reification of Sing:

λ> $(stringE . show =<< reify ''Sing)
"FamilyI (FamilyD DataFam Data.Singletons.Sing [KindedTV a_1627411905 (VarT k_1627411904)] (Jus
t StarT)) [DataInstD [] Data.Singletons.Sing [SigT (VarT n_1627517287) (ConT GHC.TypeLits.Symbo
l)] [ForallC [] [AppT (ConT GHC.TypeLits.KnownSymbol) (VarT n_1627517287)] (NormalC Data.Single
tons.TypeLits.Internal.SSym [])] [],DataInstD [] Data.Singletons.Sing [SigT (VarT n_1627517933)
 (ConT GHC.TypeLits.Nat)] [ForallC [] [AppT (ConT GHC.TypeLits.KnownNat) (VarT n_1627517933)] (
NormalC Data.Singletons.TypeLits.Internal.SNat [])] [],DataInstD [] Data.Singletons.Sing [SigT
(VarT z0_1627517291) (TupleT 0)] [ForallC [] [AppT (AppT EqualityT (VarT z0_1627517291)) (ConT
peLits.Internal.SSym [])] [],DataInstD [] Data.Singletons.Sing [SigT (VarT n_1627517933)
 (ConT GHC.TypeLits.Nat)] [ForallC [] [AppT (ConT GHC.TypeLits.KnownNat) (VarT n_1627517933)] (
NormalC Data.Singletons.TypeLits.Internal.SNat [])] [],DataInstD [] Data.Singletons.Sing [SigT
(VarT z0_1627517291) (TupleT 0)] [ForallC [] [AppT (AppT EqualityT (VarT z0_1627517291)) (ConT...

here's a reified data instance for Bool:

DataInstD [] Data.Singletons.Sing [SigT (VarT z0_1627472669) (ConT GHC.Types.Bool)] [ForallC
[] [AppT (AppT EqualityT (VarT z0_1627472669)) (ConT GHC.Types.False)] (NormalC Data.Singletons
.Prelude.Instances.SFalse []),ForallC [] [AppT (AppT EqualityT (VarT z0_1627472669)) (ConT GHC.
Types.True)] (NormalC Data.Singletons.Prelude.Instances.STrue [])] []

-- formatted

DataInstD 
  []
  -- ^ a Cxt or [Pred], the type class context 
  Sing 
  -- ^ The Name of the class/family
  [ SigT (VarT z) (ConT GHC.Types.Bool) ] 
  -- ^ A [Type]. This is (z :: Bool)
  [ ForallC 
    -- ^ has type Con, so is a GADT
      [] 
      -- ^ TyVarBndr
      [AppT (AppT EqualityT (VarT z)) (ConT GHC.Types.False)]
      -- ^ Cxt, list of predicates. in this case, we're asserting that 
      -- `z ~ False`.
      (NormalC Data.Singletons.Prelude.Instances.SFalse [])
      -- ^ Normal constructor.
  , ForallC 
      [] 
      [AppT (AppT EqualityT (VarT z0_1627472669)) (ConT GHC.Types.True)] 
      (NormalC Data.Singletons.Prelude.Instances.STrue [])
  ]
  -- ^ [Con], the constructors we want
  []
  -- ^ [Name] of instances to derive

I'm going to need to dig more into how the reifyInstances works to search by the types.

andrewthad / pringletons

enumerateConstructors is not good #1