normalize package:dhall

Reduce an expression to its normal form, performing beta reduction normalize does not type-check the expression. You may want to type-check expressions before normalizing them since normalization can convert an ill-typed expression into a well-typed expression. normalize can also fail with error if you normalize an ill-typed expression

Normalize an expression, using the supplied InputSettings

Access the custom normalizer.

Reduce an expression to its normal form, performing beta reduction and applying any custom definitions. normalizeWith is designed to be used with function typeWith. The typeWith function allows typing of Dhall functions in a custom typing context whereas normalizeWith allows evaluating Dhall expressions in a custom context. To be more precise normalizeWith applies the given normalizer when it finds an application term that it cannot reduce by other means. Note that the context used in normalization will determine the properties of normalization. That is, if the functions in custom context are not total then the Dhall language, evaluated with those functions is not total either. normalizeWith can fail with an error if you normalize an ill-typed expression

This function generalizes normalizeWith by allowing the custom normalizer to use an arbitrary Monad normalizeWithM can fail with an error if you normalize an ill-typed expression

Lens from a Status to its _normalizer field

An variation on NormalizerM for pure normalizers

Use this to wrap you embedded functions (see normalizeWith) to make them polymorphic enough to be used.

A reified Normalizer, which can be stored in structures without running into impredicative polymorphism.

α-normalize an expression by renaming all bound variables to "_" and using De Bruijn indices to distinguish them

>>> mfb = Syntax.makeFunctionBinding

>>> alphaNormalize (Lam mempty (mfb "a" (Const Type)) (Lam mempty (mfb "b" (Const Type)) (Lam mempty (mfb "x" "a") (Lam mempty (mfb "y" "b") "x"))))
Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1)))))

α-normalization does not affect free variables:

>>> alphaNormalize "x"
Var (V "x" 0)

Quickly check if an expression is in normal form Given a well-typed expression e, isNormalized e is equivalent to e == normalize e. Given an ill-typed expression, isNormalized may fail with an error, or evaluate to either False or True!

Check if an expression is in a normal form given a context of evaluation. Unlike isNormalized, this will fully normalize and traverse through the expression. It is much more efficient to use isNormalized. isNormalizedWith can fail with an error if you check an ill-typed expression

Render the difference between the normal form of two expressions

This is only used by the FromDhall instance for functions in order to normalize the function input before marshaling the input into a Dhall expression.

Default normalization-related settings (no custom normalization)

genericAutoWithInputNormalizer is like genericAutoWith, but instead of using the defaultInputNormalizer it expects an custom InputNormalizer.

genericToDhallWithInputNormalizer is like genericToDhallWith, but instead of using the defaultInputNormalizer it expects an custom InputNormalizer.