| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
ReWire.Eidos.Types
Description
Type utilities for Eidos: the total synthesizing typeOf, type
substitution (trivially capture-free: Ty has no binders), arrow and
application spines, and type-level-natural evaluation.
typeOf follows the Core-Lint convention: it is total on well-formed
programs (doc/eidos.md §5) and calls error on ill-formed ones, which
the linter rejects with a located diagnostic before any pass consults
types.
Synopsis
- typeOf :: Exp -> Ty
- substTv :: HashMap TyVar Ty -> Ty -> Ty
- instantiate :: Sig -> [Ty] -> Ty
- mkArrow :: Annote -> Ty -> Ty -> Ty
- dstArrow :: Ty -> Maybe (Ty, Ty)
- flattenArrow :: Ty -> ([Ty], Ty)
- flattenTyApp :: Ty -> (Ty, [Ty])
- mkTyApp :: Annote -> Ty -> [Ty] -> Ty
- flattenApp :: Exp -> (Exp, [Arg])
- evalNat :: Ty -> Maybe Natural
- natNorm :: Ty -> Ty
- tyEq :: Ty -> Ty -> Bool
- hasArrow :: Ty -> Bool
- higherOrder :: Ty -> Bool
- fundamental :: Ty -> Bool
- reacOrStateT :: Ty -> Bool
- synthable :: Ty -> Bool
- machineDefn :: Defn -> Bool
Documentation
The type of an expression. Total on lint-clean programs; error (with
the offending annotation) otherwise. Type arguments may only be applied
to Var heads, must precede all term arguments, and must saturate the
head's quantifier list (doc/eidos.md §4.2). One tolerance: a bare
(argument-less) reference to a polymorphic name returns its open
signature type — the linter rejects such references outside
fully-instantiated spines, but the specializer reads them.
substTv :: HashMap TyVar Ty -> Ty -> Ty Source #
Substitution of types for type variables. No renaming is ever needed: types contain no binders.
instantiate :: Sig -> [Ty] -> Ty Source #
Instantiate a signature at type arguments (must saturate the quantifier list; the linter enforces this at occurrences).
flattenTyApp :: Ty -> (Ty, [Ty]) Source #
A type application spine: flattenTyApp (T a b) == (T, [a, b]).
flattenApp :: Exp -> (Exp, [Arg]) Source #
A term application spine: head and arguments, outermost last.
evalNat :: Ty -> Maybe Natural Source #
Evaluate a closed type-level natural: literals and the built-in arithmetic constructors over evaluable operands.
Normalize a type: every type-level-natural subterm is put into a
canonical linear form (a sorted sum of coefficient-scaled atoms plus a
constant), so equal-modulo-arithmetic types — including OPEN ones,
e.g. 0 + m + n vs n + m, whose equality GHC's type-lits plugins
already proved — compare structurally equal. Type equality throughout
the compiler is structural equality after natNorm (annotations are
already ignored by 'Eq Ty'). Subtraction does not distribute (naturals
truncate): a - b normalizes its operands and is otherwise an atom.
tyEq :: Ty -> Ty -> Bool Source #
Structural equality after normalization — the compiler-wide notion of type equality (doc/eidos.md §5).
higherOrder :: Ty -> Bool Source #
A function type with a function-typed parameter or result.
fundamental :: Ty -> Bool Source #
No String, Integer, or list constructors anywhere in the type.
reacOrStateT :: Ty -> Bool Source #
Mentions a reactive-monad-stack constructor.
synthable :: Ty -> Bool Source #
Representable in hardware: first-order, fundamental, and no reactive types in parameter position (the partial evaluator's per-definition goal).
machineDefn :: Defn -> Bool Source #
A definition the machine level keeps and the fold lowers: dotted-named (not a builtin signature carrier, which is undotted), monomorphic, and not reactive-typed (the reactive fragment is consumed by purification).