Safe Haskell | None |
---|---|

Language | Haskell2010 |

- data Term src ss ts vs t where
- typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
- data TermT src ss ts vs = TermT (Term src ss ts vs t)
- data TermVT src ss ts = TermVT (Term src ss ts vs t)
- liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
- data TermAVT src ss = TermAVT (forall ts. Term src ss ts vs t)
- newtype TeSym ss ts t = TeSym (forall term. Syms ss term => Sym_Lambda term => QualOf t => CtxTe term ts -> term (UnQualOf t))
- teSym :: forall s ss ts t. Inj_Sym ss s => (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) -> TeSym ss ts t
- type family QualOf (t :: Type) :: Constraint where ...
- type family UnQualOf (t :: Type) :: Type where ...
- unQualTy :: Source src => Type src vs (t :: Type) -> (TypeK src vs Constraint, TypeK src vs Type)
- unQualsTy :: Source src => Type src vs (t :: kt) -> TypeK src vs kt
- data CtxTe term hs where
- type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t
- type family Sym (s :: Type) :: (Type -> Type) -> Constraint
- type family Syms (ss :: [Type]) (term :: Type -> Type) :: Constraint where ...
- type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
- inj_Sym :: forall s ss ts t. Inj_Sym ss s => TeSym '[Proxy s] ts t -> TeSym ss ts t
- class Inj_SymP p ss s where
- class Sym_Lambda term where
- lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)
- lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)
- lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e)

# Type `Term`

data Term src ss ts vs t where Source #

AllocVars Type (Term src ss ts) Source # | |

Inj_Source (TermT src ss ts vs) src => TypeOf Type (Term src ss ts vs) Source # | |

Source src => Eq (Term src ss ts vs t) Source # | |

Source src => Show (Term src ss ts vs t) Source # | |

Source src => Sourced (Term src ss ts vs t) Source # | |

LenVars (Term src ss ts vs t) Source # | |

ExpandFam (Term src ss ts vs t) Source # | |

ConstsOf (Term src ss ts vs t) Source # | |

type SourceOf (Term src ss ts vs t) Source # | |

type VarsOf (Term src ss ts vs t) Source # | |

## Type `TermT`

## Type `TermVT`

liftTermVT :: TermVT src ss '[] -> TermVT src ss ts Source #

## Type `TermAVT`

# Type `TeSym`

teSym :: forall s ss ts t. Inj_Sym ss s => (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) -> TeSym ss ts t Source #

## Type family `QualOf`

type family QualOf (t :: Type) :: Constraint where ... Source #

Qualification

QualOf (q #> t) = q | |

QualOf t = (() :: Constraint) |

## Type family `UnQualOf`

unQualTy :: Source src => Type src vs (t :: Type) -> (TypeK src vs Constraint, TypeK src vs Type) Source #

Return `Constraint`

and `Type`

part of given `Type`

.

unQualsTy :: Source src => Type src vs (t :: kt) -> TypeK src vs kt Source #

Remove `Constraint`

s from given `Type`

.

# Type `CtxTe`

data CtxTe term hs where Source #

GADT for an *interpreting context*:
accumulating at each *lambda abstraction*
the `term`

of the introduced variable.

## Type `TermDef`

type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t Source #

Convenient type alias for defining `Term`

.

## Type family `Sym`

## Type family `Syms`

## Type `Inj_Sym`

### Class `Inj_SymP`

# Class `Sym_Lambda`

class Sym_Lambda term where Source #

apply :: term ((a -> b) -> a -> b) Source #

*Function application*.

apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b) Source #

*Function application*.

app :: term (a -> b) -> term a -> term b infixr 0 Source #

*Lambda application*.

app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res infixr 0 Source #

*Lambda application*.

lam :: (term a -> term b) -> term (a -> b) Source #

*Lambda abstraction*.

lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res) Source #

*Lambda abstraction*.

let_ :: term var -> (term var -> term res) -> term res Source #

lam1 :: (term a -> term b) -> term (a -> b) Source #

*Lambda abstraction* beta-reducable without duplication
(i.e. whose variable is used once at most),
mainly useful in compiled `Term`

s
whose symantics are not a single `term`

but a function between `term`

s,
which happens because those are more usable when used as an embedded DSL.

lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b) Source #

*Lambda abstraction* beta-reducable without duplication
(i.e. whose variable is used once at most),
mainly useful in compiled `Term`

s
whose symantics are not a single `term`

but a function between `term`

s,
which happens because those are more usable when used as an embedded DSL.

qual :: proxy q -> term t -> term (q #> t) Source #

*Qualification*.

Workaround used in `readTermWithCtx`

.

qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t) Source #

*Qualification*.

Workaround used in `readTermWithCtx`

.

Sym_Lambda View Source # | |

Sym_Lambda Eval Source # | |

Sym_Lambda term => Sym_Lambda (BetaT term) Source # | |

(Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) Source # | |

lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c) Source #

lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d) Source #

lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e) Source #