Copyright | (c) Sebastian Graf 2017-2020 |
---|---|

License | ISC |

Maintainer | sgraf1337@gmail.com |

Portability | portable |

Safe Haskell | None |

Language | Haskell2010 |

This is the top-level, import-all, kitchen sink module.

Look at Datafix.Tutorial for a tour guided by use cases.

## Synopsis

- module Datafix.Common
- module Datafix.Denotational
- module Datafix.Explicit
- module Datafix.NodeAllocator
- module Datafix.FrameworkBuilder
- type family MonoMap k = (r :: * -> *) | r -> k
- type family Apply (t :: Function k l -> *) (u :: k) :: l
- data Constant1 :: * -> Function b a -> *
- data Constant0 :: Function a (Function b a -> *) -> *
- data Function :: * -> * -> *
- class Currying as b where
- type family ReturnType' (t :: *) :: * where ...
- type family ReturnType (t :: *) :: * where ...
- type family ParamTypes' (t :: *) :: [*] where ...
- type family ParamTypes (t :: *) :: [*] where ...
- type family IsBase (t :: *) :: Bool where ...
- type family Products (as :: [*]) where ...
- type Arrows (as :: [*]) (r :: *) = Foldr (->) r as
- type family Constant (b :: l) (as :: [k]) :: [l] where ...
- data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
- data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
- type family Foldr' (c :: Function k (Function l l -> *) -> *) (n :: l) (as :: [k]) :: l where ...
- type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where ...
- type family If (b :: Bool) (l :: k) (r :: k) :: k where ...
- type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where ...
- arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func
- module Datafix.Worklist

# Documentation

module Datafix.Common

module Datafix.Denotational

module Datafix.Explicit

module Datafix.NodeAllocator

module Datafix.FrameworkBuilder

type family MonoMap k = (r :: * -> *) | r -> k Source #

The particular ordered map implementation to use for the key type `k`

.

The default implementation delegates to `POMap`

.

type family Apply (t :: Function k l -> *) (u :: k) :: l Source #

## Instances

type Apply (Constant1 a :: Function k Type -> Type) (b :: k) Source # | |

type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) Source # | |

type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) Source # | |

type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) Source # | |

class Currying as b where Source #

`Currying as b`

witnesses the isomorphism between `Arrows as b`

and `Products as -> b`

. It is defined as a type class rather
than by recursion on a singleton for `as`

so all of that these
conversions are inlined at compile time for concrete arguments.

type family ReturnType' (t :: *) :: * where ... Source #

ReturnType' (a -> t) = ReturnType t |

type family ReturnType (t :: *) :: * where ... Source #

ReturnType t = If (IsBase t) t (ReturnType' t) |

type family ParamTypes' (t :: *) :: [*] where ... Source #

ParamTypes' (a -> t) = a ': ParamTypes t |

type family ParamTypes (t :: *) :: [*] where ... Source #

Using `IsBase`

we can define notions of `ParamTypes`

and `ReturnTypes`

which *reduce* under positive information `IsBase t ~ 'True`

even
though the shape of `t`

is not formally exposed

ParamTypes t = If (IsBase t) '[] (ParamTypes' t) |

type family IsBase (t :: *) :: Bool where ... Source #

`IsBase t`

is `'True`

whenever `t`

is *not* a function space.

type family Products (as :: [*]) where ... Source #

`Products []`

corresponds to `()`

,
`Products [a]`

corresponds to `a`

,
`Products [a1,..,an]`

corresponds to `(a1, (..,( an)..))`

.

So, not quite a right fold, because we want to optimize for the empty, singleton and pair case.

type Arrows (as :: [*]) (r :: *) = Foldr (->) r as Source #

`Arrows [a1,..,an] r`

corresponds to `a1 -> .. -> an -> r`

type family Foldr' (c :: Function k (Function l l -> *) -> *) (n :: l) (as :: [k]) :: l where ... Source #

Version of `Foldr`

taking a defunctionalised argument so
that we can use partially applied functions.

type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where ... Source #

`All p as`

ensures that the constraint `p`

is satisfied by
all the `types`

in `as`

.
(Types is between scare-quotes here because the code is
actually kind polymorphic)

arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func Source #

module Datafix.Worklist