Feel.Type.Conformance (feel v0.1.0)

Copy Markdown View Source

How types relate to each other (DMN 1.6, sections 10.3.2.9.1 and 10.3.2.9.2).

Two relations are defined. Equivalence means two types can be used interchangeably. Conformance, written T <: S, means an instance of T can be used wherever an instance of S is expected. The rules for acyclic model types are structural: names are resolved to shapes. Guarded recursive descriptors accept identical reachable declaration graphs up to consistent renaming (Feel.Type.Recursive.equivalent?/2) and the applicable ordinary lattice rules, without general recursive subtyping or equivalence. A negative answer can therefore mean that a recursive relation was not proved. Structural analysis projections must not be substituted for exact recursive function result declarations.

  • Null <: T <: Any for every type T; Any conforms only to Any.
  • A primitive type conforms only to itself. In particular date does not conform to date and time, and the two durations are unrelated.
  • list<T> <: list<S> and range<T> <: range<S> when T <: S.
  • context<M> <: context<N> when every member of N is in M with a conforming type. Extra members in M are allowed, so the context {id, name, age} conforms to {id, name} but not the other way round.
  • function<P> -> R <: function<Q> -> S when the arities are equal, each parameter of Q conforms to the parameter of P (contravariant), and R <: S (covariant). Parameter names are not part of the type.

A type marked {:non_null, T} (D-48, number!) is T without Null, which is under every other type:

  • T! <: T, and T! <: S! and T! <: S when T <: S.
  • Null is not under a marked type, and neither is a type that can be Null: number is not under number!.
  • The join of two marked types is marked; the join of a marked type and another is the join of the types without the mark.

A type that is {:not, T} or {:union, [T, ...]} (D-178, Feel.Type.Composite) is not in the lattice, which has no union and no negation. A relation that has one is asked of the unions the two types make (Feel.Type.Union.subtype?/2, sound, and the same answer as the rules above for the types the rules can answer).

All of these work on resolved types: a {:named, name} type is related only to itself, to Any, and (as Null) from Null. Resolve model-defined types first with Feel.Type.resolve/2.

Summary

Functions

conforms?(type, target)

Returns true when the first type conforms to the second.

equivalent?(type, other)

Returns true when two types are equivalent.

join(type, other)

Returns a conservative common supertype: the type of a list with elements of these two types. This need not be the least expressible supertype for functions or composite declarations.

Functions

conforms?(type, target)

@spec conforms?(Feel.Type.t(), Feel.Type.t()) :: boolean()

Returns true when the first type conforms to the second.

iex> Feel.Type.Conformance.conforms?(:null, {:list, :number})
true
iex> Feel.Type.Conformance.conforms?(:null, {:non_null, :number})
false
iex> Feel.Type.Conformance.conforms?({:non_null, :number}, :number)
true
iex> Feel.Type.Conformance.conforms?(:number, {:non_null, :number})
false
iex> Feel.Type.Conformance.conforms?(:date, :date_and_time)
false
iex> Feel.Type.Conformance.conforms?({:context, %{"id" => :number, "age" => :number}}, {:context, %{"id" => :number}})
true

equivalent?(type, other)

@spec equivalent?(Feel.Type.t(), Feel.Type.t()) :: boolean()

Returns true when two types are equivalent.

Equal terms are equivalent. Composite declarations can have different terms for the same type (for example, a union's alternatives in another order), so otherwise both directions of conformance must hold.

iex> Feel.Type.Conformance.equivalent?(
...>   {:context, %{"a" => :number, "b" => :string}},
...>   {:context, %{"b" => :string, "a" => :number}}
...> )
true
iex> Feel.Type.Conformance.equivalent?({:list, :number}, {:list, :any})
false

join(type, other)

@spec join(Feel.Type.t(), Feel.Type.t()) :: Feel.Type.t()

Returns a conservative common supertype: the type of a list with elements of these two types. This need not be the least expressible supertype for functions or composite declarations.

  • Null is absorbed: the join of Null and T is T.
  • If one type conforms to the other, the join is the upper one.
  • Lists and ranges join their element types, and two contexts join to the members they share, each with the join of its types.
  • Anything else, such as number and string, joins to Any.

Examples

iex> Feel.Type.Conformance.join(:number, :null)
:number
iex> Feel.Type.Conformance.join({:list, :number}, {:list, :string})
{:list, :any}
iex> Feel.Type.Conformance.join(:number, :string)
:any