Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module provides a generalized implementation of data types à la carte [1]. It supports (higher-order) functors with 0 or more functorial parameters and additional non-functorial parameters, all with a uniform interface.
[1] W. Swierstra. Data Types à la Carte. Journal of Functional Programming, 18(4):423-436, 2008, http://dx.doi.org/10.1017/S0956796808006758.
(This module is preferably used with the GHC extensions DataKinds
and
PolyKinds
.)
Usage
Compared to traditional data types à la carte, an extra poly-kinded parameter
has been added to :+:
and to the parameters of :<:
. Standard data types à
la carte is obtained by setting this parameter to ()
. That gives us the
following type for Inl
:
Inl
:: h1 () a -> (h1:+:
h2) () a
Here, h1 ()
and (h1
are functors.:+:
h2) ()
By setting the extra parameter to a functor f :: * -> *
, we obtain this
type:
Inl
:: h1 f a -> (h1:+:
h2) f a
This makes h1
and (h1
higher-order functors.:+:
h2)
Finally, by setting the parameter to a type-level pair of functors
'(f,g) :: (* -> *, * -> *)
, we obtain this type:
Inl
:: h1 '(f,g) a -> (h1:+:
h2) '(f,g) a
This makes h1
and (h1
higher-order bi-functors.:+:
h2)
Alternatively, we can represent all three cases above using heterogeneous
lists of functors constructed using '(,)
and terminated by ()
:
Inl
:: h1 () a -> (h1:+:
h2) () a -- functorInl
:: h1 '(f,()) a -> (h1:+:
h2) '(f,()) a -- higher-order functorInl
:: h1 '(f,'(g,())) a -> (h1:+:
h2) '(f,'(g,())) a -- higher-order bi-functor
This view is taken by the classes HFunctor
and HBifunctor
. An HFunctor
takes a parameter of kind (* -> *, k)
; i.e. it has at least one
functorial parameter. A HBiFunctor
takes a parameter of kind
(* -> *, (* -> *, k))
; i.e. it has at least two functorial parameters.
Aliases for parameter lists
To avoid ugly types such as '(f,'(g,()))
, this module exports the synonyms
Param0
, Param1
, Param2
, etc. for parameter lists up to size 4. These
synonyms allow the module to be used without the DataKinds
extension.
Extra type parameters
Recall that an HFunctor
takes a parameter of kind (* -> *, k)
, and an
HBifunctor
takes a parameter of kind (* -> *, (* -> *, k))
. Since k
is
polymorphic, it means that it is possible to add extra parameters in place of
k
.
For example, a user can define the following type representing addition in some language:
data Add fs a where Add :: (Num
a, pred a) => f a -> f a -> Add (Param2
f pred) a instanceHFunctor
Add wherehfmap
f (Add a b) = Add (f a) (f b)
Here, Add
has a functorial parameter f
, and an extra non-functorial
parameter pred
that provides a constraint for the type a
.
An obvious alternative would have been to just make pred
a separate
parameter to Add
:
data Add pred fs a where Add :: (Num
a, pred a) => f a -> f a -> Add pred (Param1
f) a instanceHFunctor
(Add pred) wherehfmap
f (Add a b) = Add (f a) (f b)
However, this has the disadvantage of being hard to use together with the
:<:
class. For example, we might want to define the following "smart
constructor" for Add
:
mkAdd :: (Num
a, pred a, Add pred:<:
h) => f a -> f a -> h (Param1
f) a mkAdd a b =inj
(Add a b)
Unfortunately, the above type is ambiguous, because pred
is completely
free. Assuming that h
is a type of the form (...
,
we would like to infer :+:
Add Show
:+:
...)(pred ~
, but this would require extra
machinery, such as a type family that computes Show
)pred
from h
.
By putting pred
in the parameter list, we avoid the above problem. We also
get the advantage that the same pred
parameter is distributed to all types
in a sum constructed using :+:
. This makes it easier to, for example,
change the pred
parameter uniformly throughout an expression.
- data (h1 :+: h2) fs a
- class sub :<: sup where
- class HFunctor h where
- hfmap :: (forall b. f b -> g b) -> h `(f, fs)` a -> h `(g, fs)` a
- class HFunctor h => HBifunctor h where
- type Param0 = ()
- type Param1 a = `(a, Param0)`
- type Param2 a b = `(a, Param1 b)`
- type Param3 a b c = `(a, Param2 b c)`
- type Param4 a b c d = `(a, Param3 b c d)`
Documentation
data (h1 :+: h2) fs a infixr 9 Source
Coproducts
(HBifunctor k k1 k2 h1, HBifunctor k k1 k2 h2) => HBifunctor k k k ((:+:) ((,) (* -> *) ((,) (k -> *) k)) k h1 h2) Source | |
(HFunctor k k1 k2 h1, HFunctor k k1 k2 h2) => HFunctor k k k ((:+:) ((,) (k -> *) k) k h1 h2) Source | |
(:<:) k k1 f h => (:<:) k k f ((:+:) k k g h) Source | |
(:<:) k k f ((:+:) k k f g) Source | |
(Reexpressible k k1 i1 instr, Reexpressible k k1 i2 instr) => Reexpressible k k ((:+:) ((,) (* -> *) ((,) (k -> *) k)) * i1 i2) instr Source | |
(InterpBi k k1 i1 m fs, InterpBi k k1 i2 m fs) => InterpBi k k ((:+:) ((,) (k -> *) ((,) (k -> *) k)) k i1 i2) m fs Source | |
(Interp k k1 i1 m fs, Interp k k1 i2 m fs) => Interp k k ((:+:) ((,) (k -> *) k) k i1 i2) m fs Source | |
(Functor (h1 fs), Functor (h2 fs)) => Functor ((:+:) k * h1 h2 fs) Source |
class sub :<: sup where Source
A constraint f
expresses that the signature :<:
gf
is subsumed by
g
, i.e. f
can be used to construct elements in g
.
Higher-order functors
class HFunctor h => HBifunctor h where Source
Higher-order bi-functors
hbimap :: (Functor f, Functor g) => (forall b. f b -> g b) -> (forall b. i b -> j b) -> h `(f, `(i, fs)`)` a -> h `(g, `(j, fs)`)` a Source
Higher-order "bimap"
(HBifunctor k k1 k2 h1, HBifunctor k k1 k2 h2) => HBifunctor k k k ((:+:) ((,) (* -> *) ((,) (k -> *) k)) k h1 h2) Source |