compdata-0.5.3: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerPatrick Bahr <paba@diku.dk>
Safe HaskellSafe-Infered

Data.Comp.Term

Description

This module defines the central notion of terms and its generalisation to contexts.

Synopsis

Documentation

data Cxt whereSource

This data type represents contexts over a signature. Contexts are terms containing zero or more holes. The first type parameter is supposed to be one of the phantom types Hole and NoHole. The second parameter is the signature of the context. The third parameter is the type of the holes.

Constructors

Term :: f (Cxt h f a) -> Cxt h f a 
Hole :: a -> Cxt Hole f a 

Instances

(Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a) 
Functor f => Monad (Context f) 
ArbitraryF f => Arbitrary (Term f)

This lifts instances of ArbitraryF to instances of Arbitrary for the corresponding term type.

ArbitraryF f => ArbitraryF (Context f)

This lifts instances of ArbitraryF to instances of ArbitraryF for the corresponding context functor.

Functor f => Functor (Cxt h f) 
Foldable f => Foldable (Cxt h f) 
Traversable f => Traversable (Cxt h f) 
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a)

This lifts instances of ArbitraryF to instances of Arbitrary for the corresponding context type.

(Functor f, ShowF f) => ShowF (Cxt h f) 
EqF f => EqF (Cxt h f) 
OrdF f => OrdF (Cxt h f) 
HasVars f v => HasVars (Cxt h f) v 
(EqF f, Eq a) => Eq (Cxt h f a)

From an EqF functor an Eq instance of the corresponding term type can be derived.

(OrdF f, Ord a) => Ord (Cxt h f a)

From an OrdF functor an Ord instance of the corresponding term type can be derived.

(Functor f, ShowF f, Show a) => Show (Cxt h f a) 
(NFDataF f, NFData a) => NFData (Cxt h f a) 

data Hole Source

Phantom type that signals that a Cxt might contain holes.

Instances

Functor f => Monad (Context f) 
ArbitraryF f => ArbitraryF (Context f)

This lifts instances of ArbitraryF to instances of ArbitraryF for the corresponding context functor.

(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a)

This lifts instances of ArbitraryF to instances of Arbitrary for the corresponding context type.

data NoHole Source

Phantom type that signals that a Cxt does not contain holes.

Instances

ArbitraryF f => Arbitrary (Term f)

This lifts instances of ArbitraryF to instances of Arbitrary for the corresponding term type.

type Term f = Cxt NoHole f ()Source

A term is a context with no holes.

type PTerm f = forall h a. Cxt h f aSource

Polymorphic definition of a term. This formulation is more natural than Term, it leads to impredicative types in some cases, though.

type Const f = f ()Source

unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)Source

This function unravels the given term at the topmost layer.

simpCxt :: Functor f => f a -> Context f aSource

Convert a functorial value into a context.

toCxt :: Functor f => Term f -> Cxt h f aSource

Cast a term over a signature to a context over the same signature.

constTerm :: Functor f => Const f -> Term fSource

This function converts a constant to a term. This assumes that the argument is indeed a constant, i.e. does not have a value for the argument type of the functor f.