Safe Haskell	None

Language.Haskell.FreeTheorems.BasicSyntax

Description

Declares the basic syntax of a Haskell98 subset enriched with higher-ranked functions. Additionally, it defines small convenience functions.

Synopsis

Documentation

data Declaration Source

A Haskell declaration which corresponds to a type, data, newtype, class or type signature declaration.

In type expressions, type variables must not be applied to type expressions. Thus, for example, the functions of the Monad class are not expressible. However, in extension to Haskell98, higher-rank types can be expressed.

This data type does not reflect all information of a declaration. Only the aspects needed by the FreeTheorems library are covered.

Constructors

TypeDecl TypeDeclaration	A `type` declaration.
DataDecl DataDeclaration	A `data` declaration.
NewtypeDecl NewtypeDeclaration	A `newtype` declaration.
ClassDecl ClassDeclaration	A `class` declaration.
TypeSig Signature	A type signature.

Instances

Eq Declaration
Data Declaration
Show Declaration
Typeable Declaration

getDeclarationName :: Declaration -> Identifier Source

Gets the name of the item declared by a declaration. This is the type constructor for data, newtype and type declarations, the name of a class for a class declaration or the name of a type signature.

getDeclarationArity :: Declaration -> Maybe Int Source

Gets the arity of a type constructor or Nothing if this is not a data, newtype or type declaration.

data TypeDeclaration Source

A type declaration for a type synonym.

Constructors

Type
Fields typeName :: Identifier The type constructor name. typeVars :: [TypeVariable] The type variables on the left-hand side. typeRhs :: TypeExpression The type expression on the right-hand side.

Instances

Eq TypeDeclaration
Data TypeDeclaration
Show TypeDeclaration
Typeable TypeDeclaration

data DataDeclaration Source

A data declaration for an algebraic data type.

Note that the context and the deriving parts of a data declaration are ignored.

Constructors

Data
Fields dataName :: Identifier The name of the type constructor. dataVars :: [TypeVariable] The type variables on the left-hand side. dataCons :: [DataConstructorDeclaration] The declarations of the data constructors on the right-hand side.

Instances

Eq DataDeclaration
Data DataDeclaration
Show DataDeclaration
Typeable DataDeclaration

data NewtypeDeclaration Source

A newtype declaration for a type renaming.

Note that the context and the deriving parts of a newtype declaration are ignored.

Constructors

Newtype
Fields newtypeName :: Identifier The name of the type constructor. newtypeVars :: [TypeVariable] The type variables of the left-hand side. newtypeCon :: Identifier The name of the data constructor on the right-hand side. newtypeRhs :: TypeExpression The type expression on the right-hand side.

Instances

Eq NewtypeDeclaration
Data NewtypeDeclaration
Show NewtypeDeclaration
Typeable NewtypeDeclaration

data ClassDeclaration Source

A class declaration for a type class.

Note that, except of type signatures of class methods, all other declarations inside the class are ignored.

Constructors

Class
Fields superClasses :: [TypeClass] The superclasses of this class. className :: Identifier The name of this type class. classVar :: TypeVariable The type variable constrained by this type class. classFuns :: [Signature] The type signatures of the class methods.

Instances

Eq ClassDeclaration
Data ClassDeclaration
Show ClassDeclaration
Typeable ClassDeclaration

data Signature Source

A type signature.

Constructors

Signature
Fields signatureName :: Identifier The name of the signature, i.e. the name of a variable or function. signatureType :: TypeExpression The type expression of the type signature.

Instances

Eq Signature
Data Signature
Show Signature
Typeable Signature

newtype Identifier Source

An identifier. This data type tags every String occurring in a declaration or a type expression.

Constructors

Ident
Fields unpackIdent :: String

Instances

Eq Identifier
Data Identifier
Ord Identifier
Show Identifier
Typeable Identifier

data DataConstructorDeclaration Source

A data constructor declaration.

Constructors

DataCon
Fields dataConName :: Identifier The name of the data constructor. dataConTypes :: [BangTypeExpression] The type arguments of the data constructor.

Instances

Eq DataConstructorDeclaration
Data DataConstructorDeclaration
Show DataConstructorDeclaration
Typeable DataConstructorDeclaration

data BangTypeExpression Source

Indicates whether in an algebraic data type declaration a strictness annotation is used.

Constructors

Banged	A type expression with a strictness flag "`!`".
Fields withoutBang :: TypeExpression
Unbanged	A type expression without a strictness flag.
Fields withoutBang :: TypeExpression

Instances

Eq BangTypeExpression
Data BangTypeExpression
Show BangTypeExpression
Typeable BangTypeExpression

data TypeExpression Source

A Haskell type expression. This data type supports also higher-rank functions. Unlike in Haskell98, a type variable must not be applied to type expressions.

Constructors

TypeVar TypeVariable	A type variable.
TypeCon TypeConstructor [TypeExpression]	A type constructor. This covers algebraic data types, type synonyms, and type renamings as well as predefined standard data types like lists and tuples.
TypeFun TypeExpression TypeExpression	The function type constructor `->`.
TypeFunLab TypeExpression TypeExpression	The function type constructor `->^o` for the non-bottom-reflecting logical relation for functions in the languagesubset with seq for equational theorems.
TypeAbs TypeVariable [TypeClass] TypeExpression	The type abstraction constructor `forall`.
TypeAbsLab TypeVariable [TypeClass] TypeExpression	The type abstraction constructor `forall^o`, allowing non-bottom-reflecting logical relations for types the type variable is instantiated with in the calculus with seq.
TypeExp FixedTypeExpression	A variable representing a fixed type expression.

Instances

Eq TypeExpression
Data TypeExpression
Show TypeExpression
Typeable TypeExpression

data TypeConstructor Source

The data type for type constructors.

Constructors

ConUnit	The unit type constructor `()`.
ConList	The list type constructor `[]`.
ConTuple Int	The tuple type constructors with given arity.
ConInt	The Haskell type `Int`.
ConInteger	The Haskell type `Integer`.
ConFloat	The Haskell type `Float`.
ConDouble	The Haskell type `Double`.
ConChar	The Haskell type `Char`.
Con Identifier	Any other type constructor with a given name.

Instances

Eq TypeConstructor
Data TypeConstructor
Typeable TypeConstructor

newtype TypeClass Source

Identifies a Haskell type class.

Constructors

TC Identifier

Instances

Eq TypeClass
Data TypeClass
Show TypeClass
Typeable TypeClass

newtype TypeVariable Source

Identifies a Haskell type variable

Constructors

TV Identifier

Instances

Eq TypeVariable
Data TypeVariable
Ord TypeVariable
Show TypeVariable
Typeable TypeVariable

newtype FixedTypeExpression Source

Represents an abbreviation for some fixed type expression. It does not occur in Haskell98 source code, but it can occur in generated theorems.

Constructors

TF Identifier

Instances

Eq FixedTypeExpression
Data FixedTypeExpression
Show FixedTypeExpression
Typeable FixedTypeExpression