Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
research:software:haskellaop:ghc-extensions [2012/09/26 22:59] – [ImpredicativeTypes] ifiguero | research:software:haskellaop:ghc-extensions [2012/12/06 16:57] (current) – [MultiParamTypeClasses] ifiguero | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== GHC Type Extensions ====== | ====== 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 [[http://www.haskell.org/haskellwiki/Haskell|Haskell | + | This is a brief introduction to the GHC Haskell type system extensions used in [[http://pleiad.dcc.uchile.cl/research/software/ |
==== ScopedTypeVariables ==== | ==== ScopedTypeVariables ==== | ||
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, | 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, | ||
Line 9: | Line 8: | ||
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. | 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 [[http:// | + | 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 [[http:// |
- | We use this extension to define | + | We use this extension to define |
- | * OpenApp, for overloaded uses of #. | + | * OpenApp, for overloaded uses of #. |
- | * MonadDeploy, | + | * MonadDeploy, |
- | * LeastGen', | + | * LeastGen', |
Multi-parameter type classes can introduce ambiguity in type inference, and are usually used in conjunction with the FunctionalDependencies extension [[http:// | Multi-parameter type classes can introduce ambiguity in type inference, and are usually used in conjunction with the FunctionalDependencies extension [[http:// | ||
==== FunctionalDependencies ==== | ==== FunctionalDependencies ==== | ||
- | 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. [[http:// | + | 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. [[http:// |
==== FlexibleInstances ==== | ==== FlexibleInstances ==== | ||
- | 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 [[http:// | + | 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 [[http:// |
==== FlexibleContexts ==== | ==== FlexibleContexts ==== | ||
- | 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 [[Ref|http:// | + | 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:// |
==== TemplateHaskell ==== | ==== TemplateHaskell ==== | ||
- | This language extension allows the use of TemplateHaskell in a module [[Ref|http:// | + | This language extension allows the use of TemplateHaskell in a module. It is necessary to use our macro expansions for advising bounded polymorphic functions. |
- | ==== TypeSynonimInstances | + | ==== TypeSynonymInstances |
- | 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, | + | 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, |
==== DeriveDataTypeable ==== | ==== DeriveDataTypeable ==== | ||
- | When defining a type using data, a " | + | When defining a type using data, a " |
==== GeneralizedNewtypeDeriving ==== | ==== GeneralizedNewtypeDeriving ==== | ||
Line 42: | Line 41: | ||
==== KindSignatures ==== | ==== KindSignatures ==== | ||
- | 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. [[http:// | + | 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. [[http:// |
==== ConstraintKinds ==== | ==== ConstraintKinds ==== | ||
Line 58: | Line 57: | ||
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. | 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. [[http:// | + | We use this extensions to express the parametricity property of the non-interfering aspects, pointcuts and advices. [[http:// |
==== ImpredicativeTypes ==== | ==== ImpredicativeTypes ==== | ||
- | This extension allows to call a polymorphic function at a polymorphic type, and parameterise data structures over polymorphic types. [[http:// | + | This extension allows to call a polymorphic function at a polymorphic type, and parameterise data structures over polymorphic types. [[http:// |
+ | |||
+ | ==== OverlappingInstances and IncoherentInstances ==== | ||
+ | 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, | ||
+ | |||
+ | 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. | ||
+ | |||
+ | [[http:// | ||
+ | [[http:// | ||
- | ==== IncoherentInstances ==== | ||
==== UndecidableInstances ==== | ==== UndecidableInstances ==== | ||
+ | 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. [[http:// | ||
+ | |||
+ | |||
==== TypeFamilies ==== | ==== TypeFamilies ==== | ||
- | | + | 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. [[http:// |
- | ==== OverlappingInstances ==== | + | |
- | ==== IncoherentInstances ==== | + | |
- | ==== NoMonomorphismRestriction ==== | + | 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. |
+ | ==== NoMonomorphismRestriction ==== | ||
+ | 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 [[http:// | ||
- | Data constructor `Jp' has existential | + | 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 |
- | (Use -XExistentialQuantification or -XGADTs to allow this) | + |