woehr/open-adt

Open algebraic data types. Reuse constructors in different types; add and remove constructors from values.

open-adt's Issues

example of overlappable instance ?

The tutorial says:

These situations can be handled with the type class approach just discussed with overlappable instances.

Could you give an example for those of us not expert in type hackery ? I have some difficulty writing the Overlappable instance. A draft would be something like:

instance {-# OVERLAPPABLE #-} ( OpenAlg r ?? ?? (OpenADT r)) => OverList a a' r ?? where
  fmapList' _ ?? = ??

Thanks !

Ord (OpenADT xs) would be nice to have

Assuming that all xs are Ord.

signatures could be simpler.

Here is a sample code:

  replaceVariable :: ( OpenAlg xs "atomF" AtomF (OpenADT xs)
            , (ApplyRow (OpenADT xs) xs .- "atomF") ~ ApplyRow (OpenADT xs) (xs .- "atomF")
            , ((xs .- "atomF") .\/ 'R '["atomF" ':-> AtomF]) ~ xs
            , (ApplyRow (OpenADT xs) (xs .- "atomF") .\/ 'R '["atomF" ':-> AtomF (Fix (VarF xs))])
              ~ ApplyRow (OpenADT xs) xs
            , (Forall (xs .- "atomF") Functor)
            )
      => Text -> Term -> OpenADT xs -> OpenADT xs
  replaceVariable variable value formula =
    case trialF (unfix formula) #atomF of
      Right other -> other & (fmap (replaceVariable variable value)) & diversifyF @("atomF" .== AtomF) & Fix
      Left (AtomF' α name terms) -> Atom α name $ fmap go terms
        where go t =
                case t of
                  GText text -> if text == variable then value else t
                  _ -> t

Some of the constraints in the signature seem to be stating the obvious.