Feel.Type.Recursive (feel v0.1.0)

Copy Markdown View Source

Finite graphs for guarded recursive item declarations.

Runtime unfolding retains references and checks every finite value. Analysis uses an upper approximation, never a proof that a recursive target is satisfied. Cycles without a context member or list element, and cycles through function signatures, are rejected by validate/2. Finite function items may accept or return recursive data. Relations between different recursive descriptors remain conservative; a structural analysis projection is not runtime signature evidence.

Summary

Types

graph()
t()

Functions

contains?(arg1)

Whether a type contains a recursive declaration, without unfolding its graph.

equivalent?(arg1, arg2)

Whether two descriptors have identical reachable declaration graphs up to renaming.

parts(value, root, target, graph)

Materializes occurrences of a declaration, with their concrete paths from the root. Runtime constraint verification traverses incrementally instead: collecting every forward path can require quadratic space for a deep chain.

unfold(arg)

Unfolds one graph node, retaining references as finite recursive descriptors.

upper(type)

A structural upper approximation, bounded by repeated references and a shared node budget.

Types

graph()

@type graph() :: %{
  optional(String.t()) => %{
    type: term(),
    constraints: list(),
    recursive?: boolean(),
    resolved_type: Feel.Type.t() | nil
  }
}

t()

@type t() :: {:recursive, String.t(), graph()}

Functions

contains?(arg1)

@spec contains?(Feel.Type.t()) :: boolean()

Whether a type contains a recursive declaration, without unfolding its graph.

equivalent?(arg1, arg2)

@spec equivalent?(t(), t()) :: boolean()

Whether two descriptors have identical reachable declaration graphs up to renaming.

Import frames can rename references and include unrelated definitions. Compare the rooted graphs with a consistent one-to-one renaming, retaining constructors, constraints and sharing. This does not prove subtyping between different recursive shapes or unfold aliases away.

parts(value, root, target, graph)

@spec parts(Feel.Value.t(), String.t(), String.t(), graph()) :: [
  {Feel.Value.t(), list()}
]

Materializes occurrences of a declaration, with their concrete paths from the root. Runtime constraint verification traverses incrementally instead: collecting every forward path can require quadratic space for a deep chain.

unfold(arg)

@spec unfold(t()) :: Feel.Type.t()

Unfolds one graph node, retaining references as finite recursive descriptors.

upper(type)

@spec upper(Feel.Type.t()) :: Feel.Type.t()

A structural upper approximation, bounded by repeated references and a shared node budget.