Module Smyth.Type

equal tau1 tau2 determines if tau1 and tau2 have the same abstract syntax tree.

The "wildcard" type.

matches tau1 tau2 determines if tau1 and tau2 have the same abstract syntax tree modulo any wildcards.

is_base tau returns determines if tau is a base type.

domain_of_codomain ~codomain root looks for codomain on the right-hand side of a type arrow in root that is not on the left-hand side of any type arrow and, if found, returns the left-hand side of that type arrow.

For example, suppose tau = a -> (b -> (c -> d)). Then:

domain_of_codomain ~codomain:d tau = Some c
domain_of_codomain ~codomain:(c -> d) tau = Some b
domain_of_codomain ~codomain:(b -> (c -> d)) tau = Some a
domain_of_codomain ~codomain:(a -> (b -> (c -> d))) tau = None

Also:

domain_of_codomain ~codomain:a a = None
domain_of_codomain ~codomain:a (() -> a) = Some ()

bind_spec gamma e returns the computed binding specification of e with respect to gamma. In particular:

• Projections decrease the binding specification of their argument
• Variables are looked up in gamma

sub_bind_spec b "decreases" the binding specification b. In particular, if b is a binding specification for the argument of some function, then sub_bind_spec b will be a binding specification for decreasing on that function.

structurally_decreasing_bind_spec ~head_spec ~arg_spec determines if arg_spec is decreasing on head_spec. If head_spec is not a binding specification for a recursive function, then structurally_decreasing ~head_spec ~arg_spec will return true.

structurally_decreasing gamma ~head ~arg determines if arg is structurally decreasing on head in the context gamma.

matches_dec (Some f) bind_spec determines if bind_spec is structurally decreasing on the recursive function f. matches_dec None bind_spec will always return true.

Peels all outer universal quantifiers on a type into a list. For example:

peel_forall (forall a . forall b . a * b) = (["a", "b"], a * b)
peel_forall a = ([], a)
peel_forall (int * int) = ([], int * int)
peel_forall (forall c . int) = (["c"], int)
peel_forall (forall c . d) = (["c"], d)

substitute ~before ~after tau substitutes replaces free occurrences of before in tau with after.

Performs many substitutions one after another; see substitute.

Type-checking errors.

Bidirectional type "checking".

Bidirectional type "inference" or "synthesis".