GHC Type Extensions

This is a brief introduction to the GHC Haskell type system extensions used in our implementation of pointcut-advice AOP in Haskell, with pointers to the relevant documentation.

This extension allows free type variables (in the type signature of the function) to be re-used in the scope of a function. For examples and more documentation, see here.

We use this extension mostly when declaring instances of Typeable1 for the AOT transformers. It is also used in the implementation of the ELT transformer, in particular when declaring ELT as an instance of MonadDeploy.

By default, type classes in Haskell can only have one type parameter. This extension allows a type class to take one or more arguments, thus becoming a relation between types.

The standard monadic libraries depend on this extension. For instance, the MonadState is parameterized by the state type s, and the monad m, and implies that in m one can manipulate a state of type s using the get and put operations See Reference.

We use this extension to define the following multi-parameter type classes:

• OpenApp, for overloaded uses of #.
• MonadDeploy, to specify the semantics of aspect deployment.
• LeastGen', LeastGen, and LessGen,which define the anti-unification algorithm.

Multi-parameter type classes can introduce ambiguity in type inference, and are usually used in conjunction with the FunctionalDependencies extension see here for a detailed discussion.

Multi-parameter typeclasses can introduce ambiguities that prevent type inference from deducing a type. Functional dependencies are a mechanism to more precisely control type inference. A functional dependency states that one of the parameters of a type class can be uniquely determined from the values of other parameters. We use this extension to define the typeclasses for our anti-unification algorithm. See Reference.

In Haskell 98, the form of an instance declaration is restricted to a type constructor applied to zero or more different type variables. This extension relaxes the form of instances, and is pervasively used in the standard monad library. We use it mainly for integration with this library See Reference.

This extension relaxes the form of the contexts of type signatures, newtype, and data declarations. It is usually used in conjunction with MultiParamTypeClasses and FlexibleInstances See Reference.

This language extension allows the use of TemplateHaskell in a module. It is necessary to use our macro expansions for advising bounded polymorphic functions. See Reference.

Instance declarations only allow type constructors defined using data or newtype. This extension allows to use type synonyms in instance declarations. This extension is used mainly for convenience, since type synonyms are just textual replacements performed in the compilation process. This extension is used typically with FlexibleInstances or UndecidableInstances See Reference.

When defining a type using data, a “deriving” clause is used to specify that this type is automatically declared as instance of some type classes. By default, a type can only automatically derive the standard classes Eq, Ord, Enum, Ix, Bounded, Read, and Show. This extension allows to derive the Typeable and Data types. We use it to automatically derive Typeable instances, since our approach is based on PolyTypeable, which extends Typeable. See Reference.

A newtype declaration renames and wraps an existing type. It has some performance advantages because the internal representation is exactly the same of the wrapped type. The deriving clause is also available when defining newtypes, however by default it is limited to Eq, Ord, Enum, and Bounded. With this extension it is possible to use the deriving clause in the same way as with the 'data' type constructor.

We use this extension to define specific AOT transformers, like AOT_cflow, which thanks to this extension automatically becomes an instance of Monad, OpenApp, AOPMonad, and MonadJpStack.

As types are assigned to values, when using type variables it can be necessary to distinguish the arity of type constructors. Haskell by default assigns kinds to types, and uses this information during typechecking. This extension allows the programmer to explicitly state the kind of type arguments. A nullary kind is denoted *, that is, a type constructor with arity 0, like Int or Float. A unary kind is denoted (* → *) and so on. See Reference 1, See Reference 2.

This extension defines a new kind named Constraint. It allows an arbitrary type to be registered as kind, which can then be used in the context of a type class or a function. We use this extension to allow arbitrary, and different constraints in the overloading of the pcAnd pointcut combinator. For an excellent explanation see here

By default, in a type declaration all the type variables used on the right-hand side must appear on the left-hand side of the declaration. Existential quantification provides a mean to hide the type variables on the right-hand side of a type declaration. It is not possible to (safely) assign a specific type to values that were existentially quantified. A good introduction can be found here.

We use this extension to manage an homogeneous aspect environment, using the type EAspect which only has a reference to the underlying monad m. Because we hide the types of poincuts and advices, we need to use unsafeCoerce to cast the values to the proper types in each case. In Section 4 we proved this operation is always safe in our model.

Regular Haskell type variables are universally quantified. A signature a → b → a is equivalent to forall a b. a → b → a, which in turn is equivalent to forall a. a → (forall b. b → a). However, nested forall expressions cannot be moved from the right of an → to the left, because the resulting type is not equivalent. A RankN type indicates a type where N is the number of nested foralls that canot be merged with a previous one.

RankN types are related to existential quantification because the only way to unpack an existential type is to use a function that works on any type that could be stored in the existential.

We use this extensions to express the parametricity property of the non-interfering aspects, pointcuts and advices. See Reference.

This extension allows to call a polymorphic function at a polymorphic type, and parameterise data structures over polymorphic types. See Reference.

GHC by default requires that it be unambigous which instance declaration should be used to resolve a typeclass constraint. These two extensions allow to modify this behavior.

Using OverlappingInstances, instances are allowed to overlap as long as there is a most specific one in any case. An instance X is more specific than an instance Y if X could match Y, but not vice versa. However in certain cases, the compiler cannot commit to one instance because the most specific one can be different in different applications of a function. For these cases, using IncoherentInstances tells GHC to arbitrarily pick one of these instances.

We use these extensions, along with UndecidableInstances in the implementation of the anti-unification algorithm using type classes. These three extensions are also used in the standard monad library.

See Reference on OverlappingInstances. See Reference on IncoherentInstances.

This extension is a more powerful version of FlexibleInstances. When enabled, there are no restrictions on the form of instance declarations. It is up to implementors to ensure that constraint resolution works. See Reference.

This extension allows ad-hoc overloading of data types. That is, types families are parametric types that can be assigned specialized representations based on the type parameters they are instantiated with. They are the type analogue of type classes, used for function overloading according to the types of the arguments. See Reference.

We use this extension to implement our anti-unification typeclass, and also to define a typeclass for the pcAnd pointcut combinator. In this type class, each instance can use a different context, using also the ConstraintKinds extension.

This extension turns off the Monomorphism Restriction (MR), which is on by default on all Haskell modules. Lifting the MR means that all bindings are polymorphic unless constrained by a type signature. A good discussion on the MR can be found here.

We use this extension in some examples to decrease the quantity of type annotations. In general, the influence of the MR during typechecking can be avoided by using explicit type signatures.