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

Language | Haskell2010 |

## Synopsis

- data Term src ss ts vs (t :: Type) 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 :: Type) = TeSym (forall term. Syms ss term => Sym_Lambda term => QualOf t => CtxTe term ts -> term (UnQualOf t))
- teSym :: forall s ss ts t. SymInj ss s => (forall term. Sym 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 :: Type -> Type) (hs :: [Type]) where
- type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
- type family Sym (s :: k) :: (Type -> Type) -> Constraint
- type family Syms (ss :: [Type]) (term :: Type -> Type) :: Constraint where ...
- type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s
- symInj :: forall s ss ts t. SymInj ss s => TeSym '[Proxy s] ts t -> TeSym ss ts t
- class SymInjP 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 :: Type) where Source #

## Instances

AllocVars (Term src ss ts :: [Type] -> Type -> Type) Source # | |

Defined in Language.Symantic.Compiling.Term | |

SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs :: Type -> Type) Source # | |

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

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

Source src => Sourceable (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 # | |

Defined in Language.Symantic.Compiling.Term | |

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

Defined in Language.Symantic.Compiling.Term |

## Type

`TermT`

## Type

`TermVT`

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

## Type

`TermAVT`

# Type

`TeSym`

teSym :: forall s ss ts t. SymInj ss s => (forall term. Sym 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 :: Type -> Type) (hs :: [Type]) 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 => SymInj ss s => Term src ss ts vs t Source #

Convenient type alias to define a `Term`

.

## Type family

`Sym`

## Type family

`Syms`

## Type

`SymInj`

type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s Source #

Convenient type synonym wrapping `SymPInj`

applied on the correct `Index`

.

### Class `SymPInj`

# Class

`Sym_Lambda`

class Sym_Lambda term where Source #

Nothing

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`

.

## Instances

Sym_Lambda Eval Source # | |

Defined in Language.Symantic.Compiling.Term | |

Sym_Lambda View Source # | |

Defined in Language.Symantic.Compiling.Term | |

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

Defined in Language.Symantic.Transforming.Beta apply :: BetaT term ((a -> b) -> a -> b) Source # app :: BetaT term (a -> b) -> BetaT term a -> BetaT term b Source # lam :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b) Source # let_ :: BetaT term var -> (BetaT term var -> BetaT term res) -> BetaT term res Source # lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b) Source # qual :: proxy q -> BetaT term t -> BetaT term (q #> t) Source # | |

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

Defined in Language.Symantic.Compiling.Term apply :: Dup r1 r2 ((a -> b) -> a -> b) Source # app :: Dup r1 r2 (a -> b) -> Dup r1 r2 a -> Dup r1 r2 b Source # lam :: (Dup r1 r2 a -> Dup r1 r2 b) -> Dup r1 r2 (a -> b) Source # let_ :: Dup r1 r2 var -> (Dup r1 r2 var -> Dup r1 r2 res) -> Dup r1 r2 res Source # lam1 :: (Dup r1 r2 a -> Dup r1 r2 b) -> Dup r1 r2 (a -> b) Source # qual :: proxy q -> Dup r1 r2 t -> Dup r1 r2 (q #> t) 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 #