GHC Type Extensions

This is a brief introduction to the GHC Haskell type system extensions used in our implementation. Most of the documentation comes from the Haskell Wiki, although we exemplify how we use the extension in our implementation.

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, and implies that in m one can manipulate a state of type s using the get and put operations Ref.

We use this extension to define three 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. Ref. We use this extension to define the typeclasses for our anti-unification algorithm.

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 Ref.

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 http://hackage.haskell.org/trac/haskell-prime/wiki/FlexibleContexts.

This language extension allows the use of TemplateHaskell in a module http://www.haskell.org/ghc/docs/latest/html/users_guide/template-haskell.html.

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 Ref.

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. Ref

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. Ref, Ref2.

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. Ref.



Data constructor `Jp' has existential type variables, a context, or a specialised result type

    (Use -XExistentialQuantification or -XGADTs to allow this)