PolymorphicContainers

What are polymorphic containers

In Haskell parametrized data types can serve as polymorphic containers. The best known examples are lists (builtin syntax [a] for homogeneous linked lists) and Maybe for containers holding up to a single element.

How to diff lists.

The Fam data type must mention the two list constructors [] and (:):

data Fam t ts
  Nil' :: Fam [a] Nil
  Cons' :: Fam a ts -> Fam [a] (a `Cons` [a] `Cons` Nil)

The Family instance is straightforward:

instance Family Fam where
  Nil'  `decEq` Nil' = Just (unsafeCoerce Refl, Refl) -- TRUST ME!
  Cons' l `decEq` Cons' r = do (Refl, Refl) <- l `decEq` r; Just (Refl, Refl)

  fields (Cons' _) (a : as) = return $ a `CCons` as `CCons` CNil
  fields Nil' [] = return CNil

  string Nil' = "[]"
  string (Cons' d) = "[" ++ G.string d ++ "]"

It remains to define how we can have a list of constructor descriptors for [a] given known descriptors for the constructors of a:

instance (Type Fam a) => Type Fam [a] where
  constructors = Concr Nil' : [Abstr $ \(a : _) -> Cons' cc | Concr cc :: Con Fam a <- constructors]
                           ++ [Abstr $ \(a : _) -> Cons' $ f a | Abstr f :: Con Fam a <- constructors]