Data.Binding.Hobbits.NuMatching

This module defines the typeclass NuMatching a, which allows pattern-matching on the bodies of multi-bindings when their bodies have type a. To ensure adequacy, the actual machinery of how this works is hidden from the user, but, for any given (G)ADT a, the user can use the Template Haskell function mkNuMatching to create a NuMatching instance for a.

Documentation

class NuMatching a where

Instances of the NuMatching a class allow pattern-matching on multi-bindings whose bodies have type a, i.e., on multi-bindings of type Mb ctx a. The structure of this class is mostly hidden from the user; see mkNuMatching to see how to create instances of the NuMatching class.

Methods

nuMatchingProof :: MbTypeRepr a

Instances

NuMatching Char

NuMatching Int

NuMatching Integer

NuMatching ()

NuMatching a => NuMatching [a]

NuMatching (Cl a)

NuMatching (Name a)

NuMatching (Term a)

NuMatching (Decls a)

NuMatching (Decl a)

NuMatching (DTerm a)

(NuMatching a, NuMatching b) => NuMatching (a -> b)

(NuMatching a, NuMatching b) => NuMatching (Either a b)

(NuMatching a, NuMatching b) => NuMatching (a, b)

(NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx)

NuMatching (Member c a)

NuMatching a => NuMatching (Mb ctx a)

(NuMatching a, NuMatching b, NuMatching c) => NuMatching (a, b, c)

(NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a, b, c, d)

mkNuMatching :: Q Type -> Q [Dec]

Template Haskell function for creating NuMatching instances for (G)ADTs. Typical usage is to include the following line in the source file for (G)ADT T (here assumed to have two type arguments):

$(mkNuMatching [t| forall a b . T a b |])

The mkNuMatching call here will create an instance declaration for NuMatching (T a b). It is also possible to include a context in the forall type; for example, if we define the ID data type as follows:

data ID a = ID a

then we can create a NuMatching instance for it like this:

$( mkNuMatching [t| NuMatching a => ID a |])

Note that, when a context is included, the Haskell parser will add the forall a for you.

class NuMatchingList args where

Methods

nuMatchingListProof :: MapRList NuMatchingObj args

Instances

NuMatchingList (RNil *)

(NuMatchingList args, NuMatching a) => NuMatchingList ((:>) * args a)

class NuMatching1 f where

Methods

nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)

data MbTypeRepr a

This type states that it is possible to replace free names with fresh names in an object of type a. This type essentially just captures a representation of the type a as either a Name type, a multi-binding, a function type, or a (G)ADT. In order to be sure that only the "right" proofs are used for (G)ADTs, however, this type is hidden from the user, and can only be constructed with mkNuMatching.