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.

Minimal complete definition

nuMatchingProof

Methods

nuMatchingProof :: MbTypeRepr a

Instances

NuMatching Bool

Methods

nuMatchingProof :: MbTypeRepr Bool

NuMatching Char

Methods

nuMatchingProof :: MbTypeRepr Char

NuMatching Int

Methods

nuMatchingProof :: MbTypeRepr Int

NuMatching Integer

Methods

nuMatchingProof :: MbTypeRepr Integer

NuMatching ()

Methods

nuMatchingProof :: MbTypeRepr ()

NuMatching a => NuMatching [a]

Methods

nuMatchingProof :: MbTypeRepr [a]

NuMatching a => NuMatching (Maybe a)

Methods

nuMatchingProof :: MbTypeRepr (Maybe a)

NuMatching (Name a)

Methods

nuMatchingProof :: MbTypeRepr (Name a)

NuMatching (Closed a)

Methods

nuMatchingProof :: MbTypeRepr (Closed a)

NuMatching (Term a0)

Methods

nuMatchingProof :: MbTypeRepr (Term a0)

NuMatching (Decls a0)

Methods

nuMatchingProof :: MbTypeRepr (Decls a0)

NuMatching (Decl a0)

Methods

nuMatchingProof :: MbTypeRepr (Decl a0)

NuMatching (DTerm a0)

Methods

nuMatchingProof :: MbTypeRepr (DTerm a0)

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

Methods

nuMatchingProof :: MbTypeRepr (a -> b)

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

Methods

nuMatchingProof :: MbTypeRepr (Either a b)

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

Methods

nuMatchingProof :: MbTypeRepr (a, b)

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

Methods

nuMatchingProof :: MbTypeRepr (MapRList f ctx)

NuMatching (Member c a)

Methods

nuMatchingProof :: MbTypeRepr (Member c a)

NuMatching a => NuMatching (Mb ctx a)

Methods

nuMatchingProof :: MbTypeRepr (Mb ctx a)

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

Methods

nuMatchingProof :: MbTypeRepr (a, b, c)

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

Methods

nuMatchingProof :: MbTypeRepr (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

Minimal complete definition

nuMatchingListProof

Methods

nuMatchingListProof :: MapRList NuMatchingObj args

Instances

NuMatchingList (RNil *)

Methods

nuMatchingListProof :: MapRList NuMatchingObj (RNil *)

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

Methods

nuMatchingListProof :: MapRList NuMatchingObj ((* :> args) a)

class NuMatching1 f where

Minimal complete definition

nuMatchingProof1

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.

isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a

Build an MbTypeRepr for type a by using an isomorphism with an already-representable type b. This is useful for building NuMatching instances for, e.g., Integral types, by mapping to and from Integer, without having to define instances for each one in this module.

data NuMatchingObj a

Constructors

NuMatching a => NuMatchingObj ()