interface.tex

\chapter{Interface or Type Relationships}\label{interface-or-type-relationships}

A class or component, e.g.\ denoted \lstinline!A!, can in some cases be used at a
location designed for another class or component, e.g.\ denoted \lstinline!B!. In
Modelica this is the case for replaceable classes (see \cref{redeclaration}) and
for \lstinline!inner!/\lstinline!outer! elements (see \cref{instance-hierarchy-name-lookup-of-inner-declarations}).
Replaceable classes are the
primary mechanism to create very flexible models. In this chapter, the
precise rules are defined when \lstinline!A! can be used at a location designed for
\lstinline!B!. The restrictions are defined in terms of compatibility rules
(\cref{interface-compatibility-or-subtyping} and \cref{plug-compatibility-or-restricted-subtyping}) between ``interfaces'' (\cref{the-concepts-of-type-interface-and-subtype}); this can
also be viewed as sub-typing (\cref{the-concepts-of-type-interface-and-subtype}).

\section{Interface Terminology}\label{interface-terminology}
In this chapter, two kinds of terminology is used for identical concepts
to get better understanding (e.g.\ by both engineers and computer
scientists). A short summary of the terms is given in the following
table. The details are defined in the rest of this chapter.

\begin{definition}[Type \emph{or} interface]\index{type!interface}\index{interface}
The ``essential'' part of the public declaration sections of a class
that is needed to decide whether \lstinline!A! can be used instead of \lstinline!B!.
\par
\begin{nonnormative*}
E.g.\ a declaration \lstinline!Real x! is part of the type (also called \emph{interface}), but \lstinline!import A! is not.
\end{nonnormative*}
\end{definition}

\begin{definition}[Class type \emph{or} inheritance interface]\index{class type}\index{type!class}\index{inheritance interface}\index{interface!inheritance}
The ``essential'' part of the public \emph{and protected} declaration sections of a class that is needed to decide whether \lstinline!A! can be used instead of \lstinline!B!. The class type, also
called inheritance interface, is needed when inheritance takes place, since then the protected declarations have to be taken into account.
\end{definition}

\begin{definition}[Subtype \emph{or} compatible interface]\index{subtype}\index{compatible interface}\index{interface!compatible}
\lstinline!A! is a subtype of \lstinline!B!, or equivalently, the interface of \lstinline!A! is compatible to the interface of \lstinline!B!, if the ``essential'' part of the public declaration
sections of \lstinline!B! is also available in \lstinline!A!.
\par
\begin{nonnormative*}
E.g., if \lstinline!B! has a declaration \lstinline!Real x!, this declaration must also be present in \lstinline!A!.  If \lstinline!A! has a declaration \lstinline!Real y!, this declaration must
not be present in \lstinline!B!.
\end{nonnormative*}
\end{definition}

If \lstinline!A! is a subtype of \lstinline!B!, then \lstinline!B! is said to be a \firstuse{supertype}\index{supertype} of \lstinline!A!.

\begin{definition}[Restricted subtype \emph{or} plug compatible interface]\index{restricted subtype}\index{subtype!restricted}\index{plug compatible interface}\index{interface!plug compatible}
\lstinline!A! is a restricted subtype of \lstinline!B!, or equivalently, the interface of \lstinline!A! is plug compatible to the interface of \lstinline!B!, if \lstinline!A! is a subtype of
\lstinline!B! and if connector components in \lstinline!A! that are not in \lstinline!B!, are default connectable.
\begin{nonnormative}
E.g.\ it is not allowed that these connectors have variables with the \lstinline!input! prefix, because then they must be connected.
\end{nonnormative}
A model or block \lstinline!A! cannot be used instead of \lstinline!B!, if the particular situation does not allow to make a connection to these additional connectors. In such a case the stricter
\emph{plug compatible} is required for a redeclaration.
\end{definition}

\begin{definition}[Function subtype \emph{or} function compatible interface]\index{function subtype}\index{subtype!function}\index{function compatible interface}\index{interface!function compatible}
\lstinline!A! is a function subtype of \lstinline!B!, or equivalently, the interface of \lstinline!A! is function compatible to the interface of \lstinline!B!, if \lstinline!A! is a subtype of
\lstinline!B! and if the additional arguments of function \lstinline!A! that are not in function \lstinline!B! are defined in such a way, that \lstinline!A! can be called at places where
\lstinline!B! is called.
\par
\begin{nonnormative*}
E.g.\ an additional argument must have a default value.
\end{nonnormative*}
\end{definition}

\section{The Concepts of Type, Interface and Subtype}\label{the-concepts-of-type-interface-and-subtype}

A \emph{type} can conceptually be viewed as a \emph{set of values}. When
we say that the variable \lstinline!x! has the type \lstinline!Real!, we mean that the value of
\lstinline!x! belongs to the set of values represented by the type \lstinline!Real! i.e.,
roughly the set of floating point numbers representable by \lstinline!Real!, for the
moment ignoring the fact that \lstinline!Real! is also viewed as a class with
certain attributes. Analogously, the variable \lstinline!b! having \lstinline!Boolean! type
means that the value of \lstinline!b! belongs to the set of values \{\lstinline!false!, \lstinline!true!\}.
The built-in types \lstinline!Real!, \lstinline!Integer!, \lstinline!String!,
\lstinline!Boolean! are considered to be
distinct types.

The \emph{subtype} relation between types is analogous to the subset
relation between sets. A type \lstinline!A1! being a subtype of type \lstinline!A! means that
the set of values corresponding to type \lstinline!A1! is a subset of the set of
values corresponding to type \lstinline!A!.

The type \lstinline!Integer! is not a subtype of \lstinline!Real! in Modelica even though the
set of primitive integer values is a subset of the primitive real values
since there are some attributes of \lstinline!Real! that are not part of \lstinline!Integer!
(\cref{predefined-types-and-classes}).

The concept of \emph{interface} as defined in \cref{interface-or-type} and used in
this document is equivalent to the notion of type based on sets in the
following sense:

An element is characterized by its interface defined by some attributes
(\cref{interface-or-type}). The \emph{type} of the element is the set of values
having the same interface, i.e.\ the same attributes.

A \emph{subtype} \lstinline!A1! in relation to another type \lstinline!A!, means that the
elements of the set corresponding to \lstinline!A1! is a subset of the set
corresponding to \lstinline!A!, characterized by the elements of that subset having
additional properties.

\begin{example}
A record \lstinline!R!: \lstinline!record R Boolean b; Real x; end R;!

Another record called \lstinline!R2!: \lstinline!R2 Boolean b; Real x; Real y; end R2;!

An instance \lstinline!r!: \lstinline!R r;!

An instance \lstinline!r2!: \lstinline!R2 r2;!

The type \lstinline!R! of \lstinline!r! can be viewed as the set of all record values having the attributes defined by the interface of \lstinline!R!, e.g.\ the infinite set \{\lstinline!R(b=false, x=1.2)!, \lstinline!R(b=false, x=3.4)!, \lstinline!R(b=true, x=1.2)!, \lstinline!R(b=true, x=1.2, y=2)!, \lstinline!R(b=true, x=1.2, a=2)!, $\ldots$\}.
The statement that \lstinline!r! has the type (or interface) \lstinline!R! means that the value of \lstinline!r! s to this infinite set.

The type \lstinline!R2! is a subtype of \lstinline!R! since its instances
fulfill the additional property of having the component \lstinline!Real y;!
in all its values.

\begin{figure}[H]
  \begin{center}
    \includegraphics{subtype}
  \end{center}
  \caption{The type \lstinline!R! can be defined as the set of record values containing \lstinline!x! and \lstinline!b!.  The subtype \lstinline!R2! is the subset of values that all contain
  \lstinline!x!, \lstinline!b!, and \lstinline!y!.}
\end{figure}
\end{example}

\section{Interface or Type}\label{interface-or-type}

Based on a flattened class or component we can construct an interface for that flattened class or component.
The \firstuse{interface}\index{interface} or \firstuse{type}\index{type} (the terms \emph{interface} and \emph{type} are equivalent and can be used interchangeably, and are different from \emph{inheritance interface} and \emph{class type}) is defined as the following information about the flattened element itself:
\begin{itemize}
\item
  Whether it is replaceable or not.
\item
  Whether the class itself or the class of the component is transitively
  non-replaceable (\cref{transitively-non-replaceable}), and if not, the reference to the
  replaceable class it refers to.
\item
  Whether it is a component or a class.
\item
  Additional information about the element:
  \begin{itemize}
  \item
    The \lstinline!flow! or \lstinline!stream! prefix.
  \item
    Declared variability (\lstinline!constant!, \lstinline!parameter!, \lstinline!discrete!).
  \item
    The prefixes \lstinline!input! and \lstinline!output!.
  \item
    The prefixes \lstinline!inner! and/or \lstinline!outer!.
  \item
    Whether the declaration is \lstinline!final!, and in that case its semantics
    contents.
  \item
    Array sizes (if any).
  \item
    Condition of conditional components (if any).
  \item
    Which kind of specialized class.
  \item
    For an enumeration type or component of enumeration type the names
    of the enumeration literals in order.
  \item
    Whether it is a built-in type and the built-in type (\lstinline!RealType!,
    \lstinline!IntegerType!, \lstinline!StringType! or \lstinline!BooleanType!).
  \end{itemize}
\item
  Only for an \lstinline!operator record! class and classes derived from \lstinline!ExternalObject!: the full name of the operator record base-class
  (i.e.\  the one containing the operations), or the derived class.  See \cref{overloaded-operators} and \cref{external-objects}.

  The following item does not apply for an \lstinline!operator record! class or class derived from \lstinline!ExternalObject!, since the type is already
  uniquely defined by the full name.
\item
  For each named public element of the class or component (including
  both local and inherited named elements) a tuple comprised of:
  \begin{itemize}
  \item
    Name of the element.
  \item
    Interface or type of the element.
    \begin{nonnormative}
    This might have been modified by modifiers and is thus not necessarily identical to the interface of the original declaration.
    \end{nonnormative}
  \end{itemize}
\end{itemize}

The corresponding \emph{constraining} interface is constructed based on the \emph{constraining} type (\cref{constraining-type}) of the declaration (if replaceable -- otherwise same as actual
type) and with the \emph{constraining} interface for the named elements.

In a class all references to elements of that class should be limited to their constraining interface.

\begin{nonnormative}
The \emph{constraining interface} consists of only the public elements, and if the declaration is replaceable the element is limited to the constraining interface.
\end{nonnormative}

\begin{nonnormative}
The public interface does not contain all of the information about the class or component.  When using a class as a base-class we also need protected elements, and
for internal type-checking we need e.g.\ import-elements.  However, the information is sufficient for checking compatibility and for using the class to flatten components.
\end{nonnormative}

\subsection{Transitively non-Replaceable}\label{transitively-non-replaceable}

\begin{nonnormative}
In several cases it is important that no new elements can be added to the interface of a class, especially considering short class definitions.
Such classes are defined as \willintroduce{transitively non-replaceable}.
\end{nonnormative}

A class reference is \firstuse{transitively non-replaceable}\index{transitively non-replaceable} iff (i.e.\ \emph{if and only if}) all parts of the name satisfy the following:
\begin{itemize}
\item
  If the class definition is long it is transitively non-replaceable if
  not declared replaceable.
\item
  If the class definition is short (i.e.\ \lstinline!class A = P.B!) it is
  transitively non-replaceable if it is non-replaceable and equal to
  class reference (\lstinline!P.B!) that is transitively non-replaceable.
\end{itemize}

\begin{nonnormative}
According to \cref{restrictions-on-base-classes-and-constraining-types-to-be-transitively-non-replaceable}, for a hierarchical name all
parts of the name must be transitively non-replaceable, i.e.\ in \lstinline!extends A.B.C! this implies that \lstinline!A.B.C! must be transitively
non-replaceable, as well as \lstinline!A! and \lstinline!A.B!, with the exception of the \emph{class
extends redeclaration mechanism} see \cref{the-class-extends-redeclaration-mechanism}.
\end{nonnormative}

\subsection{Inheritance Interface or Class Type}\label{inheritance-interface-or-class-type}

For inheritance, the interface also must include protected elements; this is the only change compared to above.

Based on a flattened class we can construct an \firstuse{inheritance interface}\index{inheritance interface}\index{interface!inheritance} or \firstuse{class type}\index{class type}\index{type!class} for that flattened class.
The inheritance interface or class type is defined as the following information about the flattened element itself:
\begin{itemize}
\item
  Whether it is replaceable or not.
\item
  Whether the class itself or the class of the component is transitively
  non-replaceable (\cref{transitively-non-replaceable}), and if not the reference to
  replaceable class it refers to.
\item
  For each named element of the class (including both local and
  inherited named elements) a tuple comprised of:
  \begin{itemize}
  \item
    Name of the element.
  \item
    Whether the element is component or a class.
  \item
    For elements that are classes: Inheritance interface or class type of the element.
    \begin{nonnormative}
    This might have been modified by modifiers and is thus not necessarily identical to the interface of the original declaration.
    \end{nonnormative}
  \item
    For elements that are components: interface or type of the element.
    \begin{nonnormative}
    This might have been modified by modifiers and is thus not necessarily identical to the interface of the original declaration.
    \end{nonnormative}
  \end{itemize}
\item
  Additional information about the element:
  \begin{itemize}
  \item
    The \lstinline!flow! or \lstinline!stream! prefix.
  \item
    Declared variability (\lstinline!constant!, \lstinline!parameter!, \lstinline!discrete!).
  \item
    The prefixes \lstinline!input! and \lstinline!output!.
  \item
    The prefixes \lstinline!inner! and/or \lstinline!outer!.
  \item
    Whether the declaration is \lstinline!final!, and in that case its semantics
    contents.
  \item
    Array sizes (if any).
  \item
    Condition of conditional components (if any).
  \item
    Which kind of specialized class.
  \item
    For an enumeration type or component of enumeration type the names
    of the enumeration literals in order.
  \item
    Whether it is a built-in type and the built-in type (\lstinline!RealType!,
    \lstinline!IntegerType!, \lstinline!StringType! or \lstinline!BooleanType!).
  \item
    Visibility (\lstinline!public! or \lstinline!protected!).
  \end{itemize}
\end{itemize}

\section{Interface Compatibility or Subtyping}\label{interface-compatibility-or-subtyping}

An interface of a class or component \lstinline!A! is compatible with an interface
of a class or component \lstinline!B! (or the constraining interface of \lstinline!B!), or
equivalently that the type of \lstinline!A! is a subtype of the type of \lstinline!B!, iff:
\begin{itemize}
\item
  \lstinline!A! is a class if and only if \lstinline!B! is a class (and thus: \lstinline!A! is a component
  if and only if \lstinline!B! is a component).
\item
  If \lstinline!A! has an \lstinline!operator record! base-class then \lstinline!B! must also have one and
  it must be the same. If \lstinline!A! does not have an operator record base-class
  then \lstinline!B! shall not have one. See \cref{overloaded-operators}.
\item
  If \lstinline!A! is derived from \lstinline!ExternalObject!, then \lstinline!B! must also be derived from
  \lstinline!ExternalObject! and have the same full name. If \lstinline!A! is not derived from
  \lstinline!ExternalObject! then \lstinline!B! shall not be derived from \lstinline!ExternalObject!. See
  \cref{external-objects}.
\item
  If \lstinline!B! is not replaceable then \lstinline!A! shall not be replaceable.
\item
  If \lstinline!B! is transitively non-replaceable then \lstinline!A! must be transitively
  non-replaceable (\cref{transitively-non-replaceable}). For all elements of the inheritance
  interface of \lstinline!B! there must exist a compatible element with the same
  name and visibility in the inheritance interface of \lstinline!A!. The interface
  of \lstinline!A! shall not contain any other elements.
  \begin{nonnormative}
  We might even extend this to say that \lstinline!A! and \lstinline!B! should have the same contents, as in the additional restrictions below.
  \end{nonnormative}
\item
  If \lstinline!B! is replaceable then for all elements of the component interface
  of \lstinline!B! there must exist a plug-compatible element with the same name in
  the component interface of \lstinline!A!.
\item
  If \lstinline!B! is neither transitively non-replaceable nor replaceable then \lstinline!A!
  must be linked to the same class, and for all elements of the
  component interface of \lstinline!B! there must thus exist a plug-compatible
  element with the same name in the component interface of \lstinline!A!.
\item
  Additional restrictions on the additional information.  These elements should either match or have a natural total order:
  \begin{itemize}
  \item
    If \lstinline!B! is a non-replaceable long class definition \lstinline!A! must also be a
    long class definition.
  \item
    The \lstinline!flow! or \lstinline!stream! prefix should be matched for compatibility.
  \item
    Declared variability is ordered \lstinline!constant! \textless{} \lstinline!parameter! \textless{} \lstinline!discrete! \textless{} continuous-time (\lstinline!Real! without prefix), and \lstinline!A! is only compatible with \lstinline!B! if the declared variability in \lstinline!A! is less than or equal the variability in \lstinline!B!.
    \begin{nonnormative}
    For a redeclaration of an element the variability prefix is as default inherited by the redeclaration (i.e.\ no need to repeat \lstinline!parameter! when redeclaring a parameter).
    \end{nonnormative}
  \item
    The \lstinline!input! and \lstinline!output! prefixes must be matched.  This ensures that the rules regarding inputs/outputs for matching connectors and (non-connector inputs) are preserved, as well as the restriction on blocks.
    \begin{nonnormative}
    For a redeclaration of an element the \lstinline!input! or \lstinline!output! prefix is inherited from the original declaration.
    \end{nonnormative}
  \item
    The \lstinline!inner! and/or \lstinline!outer! prefixes should be matched.
    \begin{nonnormative}
    For a redeclaration of an element the \lstinline!inner! and/or \lstinline!outer! prefixes are inherited from the original declaration (since it is not
    possible to have \lstinline!inner! and/or \lstinline!outer! as part of a redeclare).
    \end{nonnormative}
  \item
    If \lstinline!B! is final \lstinline!A! must also be final and have the same semantic
    contents.
  \item
    The number of array dimensions in \lstinline!A! and \lstinline!B! must be matched.
  \item
    Conditional components are only compatible with conditional components.  The conditions must have equivalent contents (similar to array sizes, except there is no \lstinline!:! for conditional
    components).
    \begin{nonnormative}
    For a redeclaration of an element the conditional part is inherited from the original.
    \end{nonnormative}
  \item
    A \lstinline!function! class is only compatible with a \lstinline!function! class, a \lstinline!package! class only compatible with a \lstinline!package! class, a \lstinline!connector! class only with a \lstinline!connector! class, a \lstinline!model! or \lstinline!block! class only compatible with a \lstinline!model! or \lstinline!block! class, and a \lstinline!type! or \lstinline!record! class only compatible with a \lstinline!type! or \lstinline!record! class.
  \item
    If \lstinline!B! is an enumeration type \lstinline!A! must also be an enumeration type and
    vice versa. If \lstinline!B! is an enumeration type not defined as \lstinline!(:)! then \lstinline!A!
    must have the same enumeration literals in the same order; if \lstinline!B! is
    an enumeration type defined as \lstinline!(:)! then there is no restriction on
    the enumeration type \lstinline!A!.
  \item
    If \lstinline!B! is a built-in type then \lstinline!A! must also be of the same built-in
    type and vice versa.
  \end{itemize}
\end{itemize}

\begin{nonnormative}
Intuitively, that the type \lstinline!A! is a subtype of the type of \lstinline!B! means that all important elements of \lstinline!B! are be present in \lstinline!A!.
\end{nonnormative}

Plug-compatibility is a further restriction of compatibility (subtyping)
defined in \cref{plug-compatibility-or-restricted-subtyping}, and further restricted for functions, see
\cref{function-compatibility-or-function-subtyping-for-functions}. For a replaceable declaration or modifier the default class
must be compatible with the constraining class.

For a modifier the following must apply:
\begin{itemize}
\item
  The modified element should exist in the element being modified.
\item
  The modifier should be compatible with the element being modified, and
  in most cases also plug-compatible, \cref{plug-compatibility-or-restricted-subtyping}.
\end{itemize}

\begin{nonnormative}
If the original constraining flat class is legal (no references to unknown elements and no illegal use of class/component), and modifiers legal as above, then the resulting flat class will be legal
(no references to unknown elements and no illegal use of class/component and compatible with original constraining class) and references refer to similar entities.
\end{nonnormative}

\section{Plug-Compatibility or Restricted Subtyping}\label{plug-compatibility-or-restricted-subtyping}

\begin{nonnormative}
If a sub-component is redeclared, see \cref{redeclaration}, it is impossible to connect to any new connector.  A connector with \lstinline!input! prefix must be connected to, and since one cannot connect across hierarchies, one should not be allowed to introduce such a connector at a level where a connection is not possible.  Therefore all public components present in the interface \lstinline!A! that are not present in \lstinline!B! must be connected by default.
\end{nonnormative}

\begin{definition}[Plug-compatibility (= restricted subtyping)]%
\index{plug-compatibility}\index{restricted subtype|seealso{plug-compatibility}}%
An interface \lstinline!A! is plug-compatible with (a restricted subtype of) an
interface \lstinline!B! (or the constraining interface of \lstinline!B!) iff:
\begin{itemize}
\item
  \lstinline!A! is compatible with (subtype of) \lstinline!B!.
\item
  All public components present in \lstinline!A! but not in \lstinline!B! must be
  default-connectable (as defined below).
\end{itemize}
\end{definition}

\begin{definition}[Default connectable]\index{default connectable}
A component of an interface is default-connectable iff:
\begin{itemize}
\item
  All of its components are default connectable.
\item
  A connector component must not be an \lstinline!input!.
  \begin{nonnormative}
  Otherwise a connection to the input will be missing.
  \end{nonnormative}
\item
  A connector component must not be of an expandable connector class.
  \begin{nonnormative}
  The expandable connector does potentially have inputs.
  \end{nonnormative}
\item
  A parameter, constant, or non-connector input must either have a
  binding equation or all of its sub-components must have binding
  equations.
\end{itemize}
\end{definition}

Based on the above definitions, there are the following restrictions:
\begin{itemize}
\item
  A redeclaration of an inherited top-level component must be
  \emph{compatible} \emph{with} (subtype of) the constraining interface
  of the element being redeclared.
\item
  In all other cases redeclarations must be \emph{plug-compatible} with
  the constraining interface of the element being redeclared.
\end{itemize}

\begin{nonnormative}
The reason for the difference is that for an inherited
top-level component it is possible to connect to the additional
connectors, either in this class or in a derived class.

Example:
\begin{lstlisting}[language=modelica]
partial model TwoFlanges
  Modelica.Mechanics.Rotational.Interfaces.Flange_a flange_a;
  Modelica.Mechanics.Rotational.Interfaces.Flange_b flange_b;
end TwoFlanges;

partial model FrictionElement
  extends TwoFlanges;
  $\ldots$
end FrictionElement;

model Clutch "compatible - but not plug-compatible with FrictionElement"
  Modelica.Blocks.Interfaces.RealInput pressure;
  extends FrictionElement;
  $\ldots$
end Clutch;

model DriveLineBase
  extends TwoFlanges;
  Inertia J1;
  replaceable FrictionElement friction;
equation
  connect(flange_a, J1.flange_a);
  connect(J1.flange_b, friction.flange_a);
  connect(friction.flange_b, flange_b);
end DriveLineBase;

model DriveLine
  extends DriveLineBase(redeclare Clutch friction);
  Constant const;
equation
  connect(const.y, frition.pressure);
  // Legal connection to new input connector.
end DriveLine;

model UseDriveLine "illegal model"
  DriveLineBase base(redeclare Clutch friction);
  // Cannot connect to friction.pressure
end UseDriveLine;
\end{lstlisting}

If a subcomponent is redeclared, it is impossible to connect to any new connector.  Thus any new connectors must work without being connected, i.e., the default connection of flow variables.  That fails for inputs (and expandable connectors may contain inputs).  For parameters and non-connector inputs it would be possible to provide bindings in a derived class, but that would require hierarchical modifiers and it would be bad modeling practice that a hierarchical modifier must be used in order to make a model valid.  A replaceable class might be used as the class for a sub-component, therefore plug-compatibility is required not only for replaceable sub-components, but also for replaceable classes.
\end{nonnormative}

\section{Function-Compatibility or Function-Subtyping for Functions}\label{function-compatibility-or-function-subtyping-for-functions}

\begin{nonnormative}
Functions may be called with either named or positional
arguments, and thus both the name and order is significant. If a
function is redeclared, see \cref{redeclaration}, any new arguments must
have defaults (and be at the end) in order to preserve the meaning of
existing calls.
\end{nonnormative}

\begin{definition}[Function-compatibility or function-subtyping for functions]\label{function-compatibility}\index{function-compatibility}\index{subtype!functions}
A \lstinline!function! class \lstinline!A! is \emph{function-compatible with or a function subtype of} \lstinline!function! class \lstinline!B! iff (the terms \emph{function-compatible} and \emph{function subtype} of are synonyms and used interchangeably):
\begin{itemize}
\item
  \lstinline!A! is compatible to (subtype of) \lstinline!B!.
\item
  All public input components of \lstinline!B! have correspondingly named public
  input components of \lstinline!A! in the same order and preceding any additional
  public input components of \lstinline!A!.
\item
  All public output components of \lstinline!B! have correspondingly named public
  output components of \lstinline!A! in the same order and preceding any additional
  public output components of \lstinline!A!.
\item
  A public input component of \lstinline!A! must have a binding assignment if the
  corresponding named element has a binding assignment in \lstinline!B!.
\item
  A public input component of \lstinline!A! not present in \lstinline!B! must have a binding
  assignment.
\item
  If \lstinline!A! is impure, then \lstinline!B! must also be impure, compare \cref{pure-modelica-functions}.
\end{itemize}
\end{definition}

Based on the above definition the following restriction holds:
\begin{itemize}
\item
  The interface of a redeclared function must be
  \emph{function-compatible with or a function subtype of} the
  constraining interface of the function being redeclared.
\end{itemize}

Note that function-compatibilty does currently not ensure that the function call has the correct variability, and that must then be checked after re-declaration - due the possibility of default arguments with higher variability.
\begin{nonnormative}
Thus any call of a function that is replaceable will need to be checked after redeclarations.
\end{nonnormative}

\begin{example}
Demonstrating a redeclaration using a function-compatible function
\begin{lstlisting}[language=modelica]
function GravityInterface
  input Modelica.Units.SI.Position position[3];
  output Modelica.Units.SI.Acceleration acceleration[3];
end GravityInterface;

function PointMassGravity
  extends GravityInterface;
  input Modelica.Units.SI.Mass m;
algorithm
  acceleration := -Modelica.Constants.G*m*position/(position*position)^1.5;
end PointMassGravity;

model Body
  model UseDriveLine "illegal model"
    DriveLineBase base(redeclare Clutch friction);
    // Cannot connect to friction.pressure
  end UseDriveLine;
  Modelica.Mechanics.MultiBody.Interface.Frame_a frame_a;
  replaceable function gravity = GravityInterface;
  constant Real failed[:]=gravity({1,0,0}); // May fail
equation
  frame_a.f = gravity(frame_a.r0);
  // or gravity(position=frame_a.r0);
  frame_a.t = zeros(3);
end Body;

model PlanetSimulation
  parameter Modelica.Units.SI.Mass mSun=2e30;
  function sunGravity = PointMassGravity (m=mSun);
  Body planet1(redeclare function gravity = sunGravity);
  Body planet2(redeclare function gravity = PointMassGravity (m=2e30));
  $\ldots$
end PlanetSimulation;
\end{lstlisting}

Note: \lstinline!PointMassGravity! is not function-compatible with
\lstinline!GravityInterface! (no default for \lstinline!m!), but \lstinline!sunGravity!
inside \lstinline!PlanetSimulation! is function-compatible with
\lstinline!GravityInterface!.

The constant failed in \lstinline!planet1!, will violate variability constraints, whereas it will work in \lstinline!planet2!.
The call \lstinline!gravity(frame_a.r0)! will work in both of them.
\end{example}

\section{Type Compatible Expressions}\label{type-compatible-expressions}

Certain expressions consist of an operator applied to two or more type
compatible sub-expressions (\lstinline!A! and \lstinline!B!), including binary operators, e.g.
\lstinline!A + B!, if-expressions, e.g.\ \lstinline!if x then A else B!, and array expressions,
e.g.\ \lstinline!{A, B}!. The resulting type of the expression in case of two type
compatible subexpressions \lstinline!A! and \lstinline!B! is defined as follows:
\begin{itemize}
\item
  If \lstinline!A! is a record-expression \lstinline!B! must also be a record-expression with
  the same named elements. The type compatible expression is a record
  comprised of named elements that are compatible with the corresponding
  named elements of both \lstinline!A! and \lstinline!B!.
  In an array expression the two records may contain elements with different sizes, but apart from that they must be of compatible types.
  That generates a heterogenous array of records, see \cref{arrays}.
\item
  If \lstinline!A! is an array expression then \lstinline!B! must also be an array expression, and \lstinline!ndims(A)! = \lstinline!ndims(B)!.  The type compatible expression is an array expression with elements compatible with the elements of both \lstinline!A! and \lstinline!B!.  If both \lstinline!size(A)! and \lstinline!size(B)! are known and \lstinline!size(A)! = \lstinline!size(B)! then this defines the size of the type compatible expression, otherwise the size of the expression is not known until the expression is about to be evaluated.  In case of an if-expression the size of the type compatible expression is defined based on the branch selected, and for other cases \lstinline!size(A)! = \lstinline!size(B)! must hold at this point.
\item
  If \lstinline!A! is a scalar expression of a simple type \lstinline!B! must also be a scalar
  expression of a simple type.
\item
  If \lstinline!A! is a \lstinline!Real! expression then \lstinline!B! must be a \lstinline!Real! or \lstinline!Integer! expression
  and the type compatible expression is \lstinline!Real!, compare \cref{standard-type-coercion}.
\item
  If \lstinline!A! is an \lstinline!Integer! expression then \lstinline!B! must be a \lstinline!Real! or \lstinline!Integer!
  expression. For exponentiation and division the type compatible
  expression is \lstinline!Real! (even if both \lstinline!A! and \lstinline!B! are \lstinline!Integer!) see \cref{exponentiation-of-scalars-of-numeric-elements}
  and \cref{division-of-scalars-or-numeric-arrays-by-numeric-scalars}, in
  other cases the type compatible expression is \lstinline!Real! or \lstinline!Integer! (same as
  \lstinline!B!), compare \cref{standard-type-coercion}.
\item
  If \lstinline!A! is a \lstinline!Boolean! expression then \lstinline!B! must be a \lstinline!Boolean! expression and
  the type compatible expression is \lstinline!Boolean!.
\item
  If \lstinline!A! is a \lstinline!String! expression then \lstinline!B! must be a \lstinline!String! expression and the
  type compatible expression is \lstinline!String!.
\item
  If \lstinline!A! is an enumeration expression then \lstinline!B! must be an enumeration
  expression and the type compatible expression is enumeration
  expression, and all enumeration expressions must be defined in terms
  of an enumeration type with the same enumeration literals in the same
  order.
\item
  If \lstinline!A! has an \lstinline!operator record! base-class then \lstinline!B! must also have an
  \lstinline!operator record! base-class, and it must be the same, and otherwise
  neither \lstinline!A! nor \lstinline!B! may have an \lstinline!operator record! base-class. This is also
  the \lstinline!operator record! base-class for the expression e.g.\ for
  \lstinline!if (cond) then A else B!.
\item
  If \lstinline!A! is derived from \lstinline!ExternalObject! then \lstinline!B! must also be derived from
  \lstinline!ExternalObject! and they must have the same full name; and otherwise
  neither \lstinline!A! nor \lstinline!B! may be derived from \lstinline!ExternalObject!. The common full
  name also defines the type of the expression, e.g.\ for \lstinline!if (cond) then A else B!.
\end{itemize}