Feel.Type.Arrows (feel v0.1.0)

Function types as arrows, an overloaded function as the intersection of several (D-171), and the questions about them.

What a function type holds

A function has no values to list. Runtime membership reads its signature metadata: a FEEL closure's declared parameter types and result from Feel.IR.result_spec/1, or a built-in's type for each signature (Feel.Value.Function.types_at/2). An enforced recursive result retains its exact declaration graph; other results use the body's public projection. A value is an instance of function<P> -> R when one signature conforms to it (Feel.Type.Instance, Feel.Type.Conformance: the same number of parameters, each parameter of the type within the parameter of the function, and the result of the function within the result of the type). So a function is a finite set of arrows, and it is in an arrow type when some arrow of its set is within it. That is what instance of answers, so it is the meaning of the type: a narrowing takes its else branch when the run does.

Everything the algebra asks follows from it, and none of it is hard:

An arrow A is within an arrow B (arrow_within?/2): the same number of parameters, B's parameters within A's, A's result within B's. It is the one comparison that is not a set operation, and is the rule of the specification.
A function type that is the intersection of arrows P1 ∧ … ∧ Pn and the negation of some ¬N1 ∧ … ∧ ¬Nm has a function unless some Pi is within some Nj (empty?/2): a function whose set is {P1, …, Pn} is in every Pi, and in no Nj when none of the Pi is within it; and a function that is in Pi has an arrow within Pi, and so within Nj if Pi is. There is no search, and no bound but the number of arrows (overload/2 caps it).
So an intersection P is within a union N1 ∨ … ∨ Nm when some Pi is within some Nj (within?/2), and an arrow is within an intersection when it is within each of its arrows.

The semantic subtyping of Frisch and Castagna says more, because it takes an arrow to be what a function does: (A → B) ∧ (C → D) is within (A ∪ C) → (B ∪ D) there. The run does not say so (abs instance of function<number> -> number is false: the specification gives abs the one parameter that takes all three kinds), and a type that took more than the run does would put a value in an else branch that the type excluded. So the emptiness of an arrow, which is the hard part of that theory, is the one comparison above.

An overload

A function that was declared with several function types is all of them: before is a function<Any, Any> -> boolean and a function<Any, range<Any>> -> boolean, and substring a function of two parameters and one of three. Its type is {:overload, arrows, refinements}:

arrows are those function types. They are what the algebra sees: the value is in each of them, so an overload is within a function type when one of its arrows is, and a function type is within it when it is within each. A reader that does not ask for the exact type (Feel.Type.Union.positive/1) sees them as alternatives, which is the type that a built-in function value had before. A function type holds for any arguments: the result is in its result, or null (a call is null when an argument does not conform, Table 64).
refinements say what a call does for the arguments in their parameters, and nothing of the others. abs is declared function<Any> -> Any (the specification has one parameter for the three kinds it takes), and a call with a duration gives a duration: that is a refinement. It is not a function type of the value, as abs instance of function<duration> -> duration is false, so the algebra does not see it: it is used to type a call and for nothing else (application/2). The function types a narrowing finds a function to be of are refinements as well (meet/2).

Nested arrows and exclusions retain their meaning through normalization. Positive approximations are requested explicitly by readers, rather than rewriting a parameter or an excluded type.

An arrow guarantees a compatible runtime signature; it does not exclude additional signatures on the same value. For example, matches inhabits both a two-argument and a three-argument arrow. Neither a single arrow nor an overload's recorded arrows establish an exhaustive signature list. Readers can use these guarantees to establish acceptance, but cannot infer rejection merely from the absence of a qualifying arrow. Call refinements do not establish runtime signatures at all.

A literal FEEL function also uses an overload when its precise body result differs from that observable result projection. For non-recursive signatures its arrow matches runtime metadata, including nullable results; its refinement carries the precise result for calls. instance of never uses that refinement as an observable arrow.

Recursive signatures require upper bounds in this algebra: an observable result becomes Any | Null, with a structural call bound retained only as a refinement. Recursive domains use an empty lower bound in upper arrows. Graph projection may widen the call bound too. Runtime membership keeps the original descriptors and conservative conformance; inclusion in an analysis projection cannot prove an exact recursive signature. Overlapping runtime signatures' possible results remain alternatives, not conjunctive call refinements.

Summary

Types

application()

The possible result of calling a function of this type, including unrecorded signatures.

arrow()

A function type: its parameters and its result.

t()

A member of a union that is a function type: an arrow, the function of anything, or an overload (its arrows, and what a call of it does for part of what it takes).

Functions

application(arg, types)

The type of the result of calling a function of an overload with arguments of these types, by position.

arrow_within?(arg1, arg2)

Whether one arrow is within another: the same number of parameters, the parameters of the second within those of the first and the result of the first within the result of the second (section 10.3.2.9.2, Feel.Type.Conformance).

arrows(arrow)

The arrows that a function of this type is all of: an arrow is itself, an overload its arrows, and the function of anything none.

empty?(positives, negatives)

Whether the functions that are of every arrow in positives and of none of the negatives are shown to be none: some positive is within some negative.

meet(member, member)

The functions that are of both types, as the members of a union: the one that is within the other if one is, and otherwise the first with the arrows of the second as refinements.

overload(arrows, refinements \\ [])

The type of a function that is all of the arrows and, for the arguments in their parameters, does what the refinements say, as the members of a union: the arrow itself if there is one and no refinement, and the overload otherwise.

overload?(arg1)

Whether a member is an overload.

result(arg, types)

The type of a call of one arrow by position: its result if every argument is within its parameter. Another arity or an uncovered domain gives Any | Null, since the type does not exclude other signatures.

within?(member, other)

Whether every function of the first type is of the second: each arrow of the second has an arrow of the first within it. The function of anything holds every function, and is held by it alone.

Types

application()

@type application() :: {:ok, Feel.Type.Union.t()}

The possible result of calling a function of this type, including unrecorded signatures.

arrow()

@type arrow() :: {:function, [Feel.Type.Union.t()], Feel.Type.Union.t()}

A function type: its parameters and its result.

t()

@type t() :: arrow() | :function | {:overload, [arrow(), ...], [arrow()]}

A member of a union that is a function type: an arrow, the function of anything, or an overload (its arrows, and what a call of it does for part of what it takes).

Functions

application(arg, types)

@spec application({:overload, [arrow(), ...], [arrow()]}, [Feel.Type.Union.t()]) ::
  application()

The type of the result of calling a function of an overload with arguments of these types, by position.

Recorded arrows bound the result only when they take this many arguments and their parameter domains cover all of them. The result is the union of those bounds. If none covers the arguments, the starting bound is Any | Null: another signature can accept them, including at the same arity. Applicable call refinements still narrow that bound.

iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> number = {:function, [[:number, :null]], [:number, :null]}
iex> duration = {:function, [[:days_and_time_duration, :null]], [:days_and_time_duration, :null]}
iex> overload = {:overload, [any], [number, duration]}
iex> Feel.Type.Arrows.application(overload, [[:days_and_time_duration]])
{:ok, [:days_and_time_duration, :null]}
iex> Feel.Type.Arrows.application(overload, [[:any, :null]])
{:ok, [:any, :null]}
iex> Feel.Type.Arrows.application(overload, [[:number], [:number]])
{:ok, [:any, :null]}

arrow_within?(arg1, arg2)

@spec arrow_within?(arrow(), arrow()) :: boolean()

iex> number = {:function, [[:number, :null]], [:number]}
iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> Feel.Type.Arrows.arrow_within?(any, {:function, [[:number, :null]], [:any, :null]})
true
iex> Feel.Type.Arrows.arrow_within?(number, any)
false
iex> Feel.Type.Arrows.arrow_within?(any, number)
false

arrows(arrow)

@spec arrows(t()) :: [arrow()]

The arrows that a function of this type is all of: an arrow is itself, an overload its arrows, and the function of anything none.

iex> Feel.Type.Arrows.arrows(:function)
[]
iex> Feel.Type.Arrows.arrows({:overload, [{:function, [], [:null]}], [{:function, [[:null]], [:null]}]})
[{:function, [], [:null]}]

empty?(positives, negatives)

@spec empty?([arrow()], [t()]) :: boolean()

Whether the functions that are of every arrow in positives and of none of the negatives are shown to be none: some positive is within some negative.

The functions are the ones of the run, a finite set of arrows each, and this is the whole of the question for them (the module says why). The answer is true only when it is shown, as everywhere in the algebra.

iex> number = {:function, [[:number, :null]], [:number, :null]}
iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> Feel.Type.Arrows.empty?([number], [any])
false
iex> Feel.Type.Arrows.empty?([any], [number])
false
iex> Feel.Type.Arrows.empty?([number, any], [{:function, [[:number, :null]], [:any, :null]}])
true

meet(member, member)

@spec meet(t(), t()) :: [t(), ...]

The functions that are of both types, as the members of a union: the one that is within the other if one is, and otherwise the first with the arrows of the second as refinements.

Before overloads the meeting of two function types was the first of them, which holds the functions of both and others, and it still is to the algebra and to a reader that does not ask for the overload. A function that is of the second type does what its arrows say for the arguments in their parameters, though, and a call is typed by it (application/2). What the functions of either are known to do (their refinements) is kept.

iex> number = {:function, [[:number, :null]], [:number, :null]}
iex> string = {:function, [[:string, :null]], [:string, :null]}
iex> Feel.Type.Arrows.meet(number, string)
[{:overload, [number], [string]}]
iex> Feel.Type.Arrows.meet(number, :function)
[number]
iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> Feel.Type.Arrows.meet(any, {:function, [[:any, :null]], [:number, :null]})
[{:function, [[:any, :null]], [:number, :null]}]

overload(arrows, refinements \\ [])

@spec overload([arrow(), ...], [arrow()]) :: [t(), ...]

A refinement that an arrow is within says nothing the arrow did not, and goes. The arrows are kept as they come, for the type that a reader sees without the overload is theirs.

iex> number = {:function, [[:number, :null]], [:number, :null]}
iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> Feel.Type.Arrows.overload([number])
[{:function, [[:number, :null]], [:number, :null]}]
iex> Feel.Type.Arrows.overload([any], [number, any])
[{:overload, [{:function, [[:any, :null]], [:any, :null]}], [{:function, [[:number, :null]], [:number, :null]}]}]

overload?(arg1)

@spec overload?(term()) :: boolean()

Whether a member is an overload.

iex> Feel.Type.Arrows.overload?({:overload, [], []})
true
iex> Feel.Type.Arrows.overload?(:function)
false

result(arg, types)

@spec result(arrow(), [Feel.Type.Union.t()]) :: Feel.Type.Union.t()

iex> arrow = {:function, [[:number, :null]], [:string]}
iex> Feel.Type.Arrows.result(arrow, [[:number]])
[:string]
iex> Feel.Type.Arrows.result(arrow, [[:string]])
[:any, :null]

within?(member, other)

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

Whether every function of the first type is of the second: each arrow of the second has an arrow of the first within it. The function of anything holds every function, and is held by it alone.

iex> number = {:function, [[:number, :null]], [:number, :null]}
iex> any = {:function, [[:any, :null]], [:any, :null]}
iex> overload = {:overload, [any, number], []}
iex> Feel.Type.Arrows.within?(overload, number)
true
iex> Feel.Type.Arrows.within?(number, overload)
false
iex> Feel.Type.Arrows.within?(overload, :function)
true
iex> Feel.Type.Arrows.within?({:overload, [any], [number]}, number)
false