| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
ReWire.Eidos.Lint
Description
Well-formedness checking for Eidos programs (doc/eidos.md §4): global binder uniqueness, scoping, the spine discipline, bidirectional (synthesis-plus-comparison) type checking, the join point discipline, and the definition and program rules — all with located diagnostics.
The linter runs in one of three cumulative modes (LintMode),
corresponding to the pipeline's invariant stages (§4.1); the machine
level's rules are ReWire.Synolon.Lint's, built on the expression
checker exported here:
LintPoly(post-bridge): the rules of §4.2–§4.4.LintMono(post-specialization): additionally, every definition signature is monomorphic and every type is nat-closed. Datatypes stay parametric through specialization (§3.6), so constructor signatures are exempt from the mono rules;Conoccurrences carry instantiated types, which are not. Builtin-named definitions (rwPrim*) are the builtins' type assumptions riding as polymorphic signature carriers and check in poly mode. Value binders may still be higher-order here: first-orderization is the partial evaluator's job, downstream of specialization, so the first-order rule belongs to mono+ANF.LintMonoANF(purify's input contract): additionally, value binders are first-order and reactive definition bodies are in the ANF shape of §6 (let chains over simple right-hand sides; the reactive fragment — purify's input skeleton — is exempt from naming, and pure definition bodies are exempt entirely — the fold lowers them in any shape).
There is no inference and no unification anywhere: every binder carries
its type, so every expression synthesizes, and checking an expression
against a type is synthesis followed by structural comparison after
natNorm. This is the monadic, located-diagnostic twin of
typeOf, which is total on programs this module
accepts.
TODO(eidos): mono+ANF mode does not yet enforce the full
representable-closure type grammar of §4.1 (a permit-list of type
constructors — Vec, Finite, Bool, (), tuples, monomorphic ADTs,
Integer, Proxy, String in literal positions — plus
ReacT/StateT/Identity until purification); it checks the ANF shape,
first-order value binders, no-polymorphism, and nat-closure. The
Synolon lint enforces representability at a fixed bit width through
envRepr.
TODO(eidos): type arguments and constructor fields are not kind-checked
(there is no kind table for built-in type constructors); type-variable
occurrences are checked against their binders' kinds.
TODO(eidos): the builtin signature check (ReWire.Eidos.BuiltinSigs)
is partial on type-level arithmetic: scheme subterms like
Vec ((i + n) + m) a become deferred equations, checked only when
nat-closed on both sides after substitution. Shape and everything
matching binds directly are always checked.
Synopsis
- data LintMode
- lint :: MonadError AstError m => LintMode -> Program -> m ()
- lintDefn :: MonadError AstError m => LintMode -> Program -> Defn -> m ()
- data Env = Env {}
- envFromDecls :: LintMode -> [DataDefn] -> [Defn] -> Env
- bindVar :: Id -> Env -> Env
- nonTail :: Env -> Env
- checkExp :: MonadError AstError m => Env -> Exp -> m Ty
- checkAgainst :: MonadError AstError m => Env -> Exp -> Ty -> m ()
- checkTy :: MonadError AstError m => Env -> Annote -> Ty -> m ()
- checkRepr :: MonadError AstError m => Env -> Annote -> Text -> Ty -> m ()
- checkValueBinder :: MonadError AstError m => Env -> Annote -> Text -> Id -> m ()
- checkOccSig :: MonadError AstError m => Annote -> Id -> Id -> m ()
- checkDistinct :: forall k m. (MonadError AstError m, Eq k, Hashable k) => [(k, Annote, Text)] -> m ()
- checkDataDefn :: MonadError AstError m => Env -> DataDefn -> m ()
- checkDefn :: MonadError AstError m => Env -> Defn -> m ()
- lookupCon :: MonadError AstError m => Env -> Annote -> DataConId -> m (TyConId, Sig)
- dconFieldTys :: MonadError AstError m => Annote -> DataConId -> TyConId -> Sig -> Ty -> m [Ty]
- data LitRep
- litRep :: Ty -> LitRep
- fitsRep :: LitRep -> Integer -> Bool
- declSites :: [DataDefn] -> [Defn] -> [(Uniq, Annote, Text)]
- expSites :: Exp -> [(Uniq, Annote, Text)]
- idSite :: Annote -> Text -> Id -> (Uniq, Annote, Text)
- tvSite :: Annote -> Text -> TyVar -> (Uniq, Annote, Text)
Documentation
The linter's mode: which stage of the pipeline's cumulative static discipline to enforce (doc/eidos.md §4.1). Modes are ordered by strength.
Constructors
| LintPoly | |
| LintMono | |
| LintMonoANF |
lint :: MonadError AstError m => LintMode -> Program -> m () Source #
Check a whole program in the given mode; succeeds exactly when every rule of the mode holds.
lintDefn :: MonadError AstError m => LintMode -> Program -> Defn -> m () Source #
Check a single definition against a program's global context: every
rule except the whole-program ones (global binder uniqueness, global
name distinctness, datatype well-formedness, and the top rule).
The expression-level checker, for reuse by other checkers
Constructors
| Env | |
Fields
| |
envFromDecls :: LintMode -> [DataDefn] -> [Defn] -> Env Source #
The checking environment over a datatype and definition table: the whole-program scope every rule starts from.
nonTail :: Env -> Env Source #
Entering a non-tail position: no join is jumpable from here (they stay visible, for diagnostics), though joins bound inside are jumpable within their own scopes.
checkExp :: MonadError AstError m => Env -> Exp -> m Ty Source #
Check an expression and return its type — the located, monadic twin of
typeOf.
checkAgainst :: MonadError AstError m => Env -> Exp -> Ty -> m () Source #
Check an expression against an expected type: synthesize and compare
after natNorm.
checkTy :: MonadError AstError m => Env -> Annote -> Ty -> m () Source #
Scoping (every type variable bound, at its binder's kind) plus, in
mono mode, closedness; at the machine level (envBanReactive), the
reactive types are out of the grammar entirely (doc/eidos.md §4.1).
checkRepr :: MonadError AstError m => Env -> Annote -> Text -> Ty -> m () Source #
Representability at a fixed bit width, when the environment carries
the representable closure (envRepr: the machine level).
checkValueBinder :: MonadError AstError m => Env -> Annote -> Text -> Id -> m () Source #
A local *value* binder (parameter, lambda/let/case/pattern binder): additionally first-order in mono+ANF mode (higher-order binders survive specialization; the partial evaluator eliminates them before the ANF stage). Join point labels are exempt — a label's signature is its continuation's function type, and a label is not a value.
checkOccSig :: MonadError AstError m => Annote -> Id -> Id -> m () Source #
An occurrence's signature equals its binder's: the same quantified
variables (uniques and kinds) over natNorm-structurally equal types.
checkDistinct :: forall k m. (MonadError AstError m, Eq k, Hashable k) => [(k, Annote, Text)] -> m () Source #
Fold a list of keyed sites, reporting the first duplicate with both locations.
checkDataDefn :: MonadError AstError m => Env -> DataDefn -> m () Source #
The datatype's kind constructs * from its parameter kinds; every
constructor quantifies exactly the datatype's parameters (the same
type variables, in the same order, across all constructors) and
constructs exactly the datatype applied to them.
checkDefn :: MonadError AstError m => Env -> Defn -> m () Source #
Parameters match a prefix of the signature's arrow spine; the body
checks against the remainder. In mono mode the signature quantifies
nothing — except the builtin-named definitions (rwPrim*), which are
the builtins' type assumptions riding to the Eidos-to-Hyle fold as
polymorphic signature carriers (error-stub bodies, never referenced
as variables); they check in poly mode. In mono+ANF mode the body
must additionally be in the ANF shape of doc/eidos.md §6
(checkANF).
dconFieldTys :: MonadError AstError m => Annote -> DataConId -> TyConId -> Sig -> Ty -> m [Ty] Source #
The instantiated field types of a constructor at a fully-applied
datatype type T ts (the scrutinee's type, or a Con occurrence's
result type).
declSites :: [DataDefn] -> [Defn] -> [(Uniq, Annote, Text)] Source #
Every binding site of the datatype-and-definition fragment, in deterministic order.