Data.Eliminator.TH

Generate dependently typed elimination functions using Template Haskell.

Eliminator generation

Term-level eliminators

deriveElim and deriveElimNamed provide a way to automate the creation of eliminator functions, which are mostly boilerplate. Here is a complete example showing how one might use deriveElim:

$(singletons [d| data MyList a = MyNil | MyCons a (MyList a) |])
$(deriveElim ''MyList)

This will produce an eliminator function that looks roughly like the following:

elimMyList :: forall (a :: Type) (p :: MyList a ~> Type) (l :: MyList a).
              Sing l
           -> Apply p MyNil
           -> (forall (x :: a). Sing x
                -> forall (xs :: MyList a). Sing xs -> Apply p xs
                -> Apply p (MyCons x xs))
           -> Apply p l
elimMyList SMyNil pMyNil _ = pMyNil
elimMyList (SMyCons (x' :: Sing x) (xs' :: Sing xs)) pMyNil pMyCons
  = pMyCons x' xs' (elimMyList @a @p @xs pMyNil pMyCons)

There are some important things to note here:

• Because these eliminators use Sing under the hood, in order for deriveElim to work, the Sing instance for the data type given as an argument must be in scope. Moreover, deriveElim assumes the naming conventions for singled constructors used by the singletons library. (This is why the singletons function is used in the example above).

• There is a convention for the order in which the arguments appear. The quantified type variables appear in this order:

  1. First, the type variables of the data type itself (a, in the above example).
  2. Second, a predicate type variable of kind <Datatype> ~> Type (p, in the above example).
  3. Finally, a type variable of kind <Datatype> (l, in the above example).

The function arguments appear in this order:

1. First, a Sing argument (Sing l, in the above example).
2. Next, there are arguments that correspond to each constructor. More on this in a second.

The return type is the predicate type variable applied to the data type (Apply p (MyCons x xs), the above example).

The type of each constructor argument also follows certain conventions:

1. For each field, there will be a rank-2 type variable whose kind matches the type of the field, followed by a matching Sing type. For instance, in the above example, forall (x :: a). Sing x corresponds to the first field of MyCons.
2. In addition, if the field is a recursive occurrence of the data type, an additional argument will follow the Sing type. This is best explained using the above example. In the MyCons constructor, the second field (of type MyCons a) is a recursive occurrence of MyCons, so that corresponds to the type forall (xs :: MyList a). Sing xs -> Apply p xs, where Apply p xs is only present due to the recursion.
3. Finally, the return type will be the predicate type variable applied to a saturated occurrence of the data constructor (Apply p (MyCons x xs), in the above example).

• You'll need to enable lots of GHC extensions in order for the code generated by deriveElim to typecheck. You'll need at least the following:

  • AllowAmbiguousTypes

  • DataKinds

  • GADTs

  • PolyKinds

  • RankNTypes

  • ScopedTypeVariables

  • TemplateHaskell

  • TypeApplications

• deriveElim doesn't support every possible data type at the moment. It is known not to work for the following:

  • Data types defined using GADTs or ExistentialQuantification
  • Data family instances
  • Data types which use polymorphic recursion (e.g., data Foo a = Foo (Foo a))

deriveElim :: Name -> Q [Dec]

deriveElim dataName generates a top-level elimination function for the datatype dataName. The eliminator will follow these naming conventions:

• If the datatype has an alphanumeric name, its eliminator will have that name with elim prepended.
• If the datatype has a symbolic name, its eliminator will have that name with ~> prepended.

deriveElimNamed :: String -> Name -> Q [Dec]

deriveElimNamed funName dataName generates a top-level elimination function named funName for the datatype dataName.

Type-level eliminators

deriveTypeElim and deriveTypeElimNamed are like deriveElim and deriveElimNamed except that they create type-level eliminators instead of term-level ones. Here is an example showing how one might use deriveTypeElim:

data MyList a = MyNil | MyCons a (MyList a)
$(deriveTypeElim ''MyList)

This will produce an eliminator function that looks roughly like the following:

type ElimMyList :: forall (a :: Type).
                   forall (p :: MyList a ~> Type) (l :: MyList a)
                -> Apply p MyNil
                -> (forall (x :: a) (xs :: MyList a)
                     -> Apply p xs ~> Apply p (MyCons x xs))
                -> Apply p l
type family ElimMyList p l pMyNil pMyCons where
  forall (a :: Type)
         (p :: MyList a ~> Type)
         (pMyNil :: Apply p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> Apply p xs ~> Apply p (MyCons x xs)).
    ElimMyList a p MyNil pMyNil pMyCons =
      pMyNil
  forall (a :: Type)
         (p :: MyList a ~> Type)
         (_pMyNil :: Apply p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> Apply p xs ~> Apply p (MyCons x xs))
         x' xs'.
    ElimMyList a p (MyCons x' xs') pMyNil pMyCons =
      Apply (pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons)

Note the following differences from a term-level eliminator that deriveElim would generate:

• Type-level eliminators do not use Sing. Instead, they use visible dependent quantification. That is, instead of generating forall (x :: a). Sing x -> ... (as a term-level eliminator would do), a type-level eliminator would use forall (x :: a) -> ....
• Term-level eliminators quantify p with an invisible forall, whereas type-level eliminators quantify p with a visible forall. (Really, p ought to be quantified visibly in both forms of eliminator, but GHC does not yet support visible dependent quantification at the term level.)
• Type-level eliminators use (~>) in certain places where (->) would appear in term-level eliminators. For instance, note the use of Apply p xs ~> Apply p (MyCons x xs) in ElimMyList above. This is done to make it easier to use type-level eliminators with defunctionalization symbols (which aren't necessary for term-level eliminators).

This comes with a notable drawback: type-level eliminators cannot support data constructors where recursive occurrences of the data type appear in a position other than the last field of a constructor. In other words, deriveTypeElim works on the MyList example above, but not this variant:

 data SnocList a = SnocNil | SnocCons (SnocList a) a
 

This is because $(deriveTypeElim ''SnocList) would generate an eliminator with the following kind:

 type ElimSnocList :: forall (a :: Type).
                      forall (p :: SnocList a ~> Type) (l :: SnocList a)
                   -> Apply p SnocNil
                   -> (forall (xs :: SnocList a) -> Apply p xs
                         ~> (forall (x :: a) -> Apply p (SnocCons x xs)))
                   -> Apply p l
 

Unfortunately, the kind Apply p xs ~> (forall (x :: a) -> Apply p (SnocCons x xs)) is impredicative.

• In addition to the language extensions that deriveElim requires, you'll need to enable these extensions in order to use deriveTypeElim:

  • StandaloneKindSignatures

  • UndecidableInstances

deriveTypeElim :: Name -> Q [Dec]

deriveTypeElim dataName generates a type-level eliminator for the datatype dataName. The eliminator will follow these naming conventions:

• If the datatype has an alphanumeric name, its eliminator will have that name with Elim prepended.
• If the datatype has a symbolic name, its eliminator will have that name with ~> prepended.

deriveTypeElimNamed :: String -> Name -> Q [Dec]

deriveTypeElimNamed funName dataName generates a type-level eliminator named funName for the datatype dataName.