11institutetext: Bloomberg, New York, USA 22institutetext: SUNY - University
at Buffalo , New York, USA

# Putting gradual types to work

Bhargav Shivkumar 1122 0000-0002-8430-9229 Enrique Naudon 11
0000-0001-9878-2781 Lukasz Ziarek 22

###### Abstract

In this paper, we describe our experience incorporating gradual types in a
statically typed functional language with Hindley-Milner style type inference.
Where most gradually typed systems aim to improve static checking in a
dynamically typed language, we approach it from the opposite perspective and
promote dynamic checking in a statically typed language. Our approach provides
a glimpse into how languages like SML and OCaml might handle gradual typing.
We discuss our implementation and challenges faced—specifically how gradual
typing rules apply to our representation of composite and recursive types. We
review the various implementations that add dynamic typing to a statically
typed language in order to highlight the different ways of mixing static and
dynamic typing and examine possible inspirations while maintaining the gradual
nature of our type system. This paper also discusses our motivation for adding
gradual types to our language, and the practical benefits of doing so in our
industrial setting.

###### Keywords:

Gradual typing Type inference Functional programming

##  1 Introduction

Static typing and dynamic typing are two opposing type system paradigms.
Statically typed languages are able to catch more programmer bugs early in the
compilation process, at the expense of a more flexible semantics. On the other
hand, dynamically typed languages allow greater flexibility, while allowing
more bugs at runtime. The proponents of each paradigm often feel very strongly
in favor of their paradigm. Language designers are stranded in the middle of
this dichotomy and left to decide between the two extremes when designing
their languages.

At Bloomberg, we have felt this pain while designing a domain specific
language for programmatically defining financial contracts. For the purposes
of this paper, we will call our language Bloomberg Contract Language (BCL).
BCL is a statically typed functional language with Hindley-Milner style type
inference [4, 17], structural composite types and recursive types. Users of
BCL are split into two groups—end users and language maintainers. End users
are typically financial professionals whose primary programming experience
involves scripting in dynamically typed languages such as Python and MATLAB.
On the other hand, language maintainers are Bloomberg software engineers who
are most at ease programming in statically typed and often functional
languages like OCaml. Whilst it is of paramount importance to provide our end
users with an environment in which they are comfortable, our domain—financial
contracts—is one in which correctness is of extraordinary importance, since
errors can lead to large financial losses. This makes static types appealing,
as they catch many errors that dynamic systems might miss. Even though static
types provide a more error-free runtime, they do require extra effort from our
end users who must learn an unfamiliar system. Our desire to simultaneously
satisfy our end users and our language maintainers led us to gradual typing
[23], which seeks to integrate static and dynamic typing in one system.
Gradual typing in BCL allows language maintainers to stick to static typing
and end users to selectively disable static typing when it interferes with
their ability to work in BCL.

Since its introduction, gradual typing [23] has been making its way into more
mainstream languages [30, 29] and more people have acknowledged the varied
benefits of mixing static and dynamic typing in the same program. As
identified by Siek and Taha [26], there has been considerable interest in
integrating static and dynamic typing, both in academia and in industry. There
has also been a plethora of proposed approaches, from adding a dynamic keyword
[2], to using objects in object-oriented languages [16], to Seik and Taha’s
gradual typing itself [23]. While there seems to be no one-size-fits-all
approach to designing a system that mixes static and dynamic types, Siek and
Taha standardize the guarantees [26] we can expect from such a system. For
language designers, this provides a more methodical way to approach the
integration. Language designers can also draw from a large body of literature
exploring the combination of gradual types with other common features, such as
objects [24] and type inference [25, 5].

While it is typical for dynamically typed languages to go the gradual route in
order to incorporate more static type checking, we go the other way and add
more dynamism to our already static language. Most static languages that
incorporate dynamic typing do so by following in the footsteps of Abadi et.al.
[2]–C# is a prime example of this [9]. Since BCL already supports type
inference and we want to retain the dynamic feel of the language, we implement
the inference algorithm described by Siek and Vachhrajani [25], putting us in
an interesting position. Our approach promotes the use of a ? annotation to
explicitly signify dynamically typed terms while un-annotated terms are
(implicitly) statically typed, much like that of Garcia and Cimini [5]. This
approach provides a simple escape hatch to end users who want to use dynamic
typing as well as avenues to automate this process to ensure backwards
compatibility of BCL with legacy code.

Finally, we feel there is a need to study the adaptation of gradual types to
an existing language with a substantial user base and lots of existing code.
We aim to provide a technical report in this paper that models our design
decisions and implementation details of bringing in gradual types to BCL. Our
primary contributions include:

  * •

A brief review of other statically typed languages that add dynamic types, to
compare and possibly derive inspiration for our own design in Section 2.

  * •

Introduce a new use case that shows how a gradually typed language benefits
different user groups of a language in Section 3.

  * •

An inference algorithm, which is an adaptation of a prominent inference
algorithm to add gradual types to a language with type inference in Section 4.

Note that throughout this paper we use "gradual" to indicate an implementation
that provides gradual guarantees as specified in [26]. While, we do not state
this formally for BCL and leave that to future work, our implementation
supports the smooth evolution of programs from static to dynamic typing as
prescribed for gradually typed systems.

##  2 Background

In this section we briefly survey the existing literature to better
contextualize our design choices. The incorporation of static and dynamic
typing has been extensively studied [28, 15, 23, 26, 8], though usually in the
context of a core calculus instead of a full-featured language. There also
seems to be a juxtaposition of the literature, which generally follows a
static-first approach, and practical implementations, which generally follow a
dynamic-first approach 111Here, static-first refers elaborating a static
surface language to a gradually typed intermediate representation. Conversely,
by dynamic-first we mean the opposite: elaborating a dynamic surface language
to a gradually typed intermediate representation. [7].

Abadi et al [2] has been an inspiration for many static languages looking to
incorporate dynamic typing. This work is a precursor to gradual typing, and
while it does not qualify as gradual à la [23], it is nevertheless a standard
when it comes to adding dynamic checks to a static language. Abadi’s work uses
a dynamic construct to build terms of type Dynamic and a typecase construct to
perform case analysis on the runtime type of an expression of type Dynamic.
This is similar to the typeof() function in dynamic languages like Python,
which resolve the type of an expression at runtime. Siek and Taha observe that
translating from their language of explicit casts to Abadi et al’s language is
not straightforward [23]. Nevertheless we believe that it is worthwhile to
introduce something like the typecase construct in a static language with
gradual types. We identify and discuss some potential applications of this in
Section 5.

Statically typed object oriented languages like C# and Java have worked to
incorporate some form of dynamic typing [6, 16]. C# 4.0 introduced the dynamic
type to declare objects that can bypass static type checking [1]. Although
this achieves dynamic type checking, there is no indication of it being
gradual à la [23]. Moreover, using the dynamic type in a C# program runs the
program on the Dynamic Language Runtime (DLR) which is a separate runtime from
the Common Language Runtime and which supports dynamic checking.

While works like [18, 22] examine gradual type inference from the perspective
of removing dynamic checks by performing type inference at runtime, Garcia and
Cimini [5] (much like BCL) deals with static reasoning about programs, based
on the consistency relation. [5] explores an alternate approach to gradual
type inference and presents a statically typed language and its gradual
counterpart. Instead of inferring gradual types based on type precision [25],
this work limits the inference problem to static types only and requires
consistency constraints between gradual types. An interesting feature of their
language is that they distinguish between static type parameters and gradual
type parameters to tell static parametric polymorphism apart from polymorphism
due to the dynamic type.

Our approach is to adopt the properly gradual system defined by Siek and
Vachchrajani [25]. That work describes the incorporation of gradual typing
into a language with unification-based type inference. Unification-based
inference is a common implementation of the Hindley-Milner type system [17],
and is the implementation that BCL already uses. This makes our integration
work relatively easier and also lets us leverage all the benefits of the
standard for gradual typing laid out by Siek and Taha [26].

###  2.1 Gradual types and unification based inference

(SVAR) |  Γ(x) = τS; Γ⊢x: τ | $None$
---|---|---
(SCNST) |  S;Γ⊢c : _typeof_(c) |
(SAPP) |  S;Γ⊢e_1 : τ_1 |
S;Γ⊢e_2 : τ_2 |  |
S(τ_1) = S(τ_2 →τ_3) S;Γ⊢e_1 e_2 : τ_3 |  |
(SABS) |  S;Γ(x↦τ_1) ⊢e : τ_2 S;Γ⊢λx: τ_1 . e : τ_1 →τ_2 |

(a)

(GVAR) |  Γ(x) = τS;Γ⊢_g x: τ | $None$
---|---|---
(GCNST) |  S;Γ⊢_g c : _typeof_(c) |
(GAPP) |  S;Γ⊢_g e_1 : τ_1 |
S; Γ⊢_g e_2 : τ_2 |  |
S ⊧τ_1 ≃τ_2 →β |  |
(βfresh)S;Γ⊢_g e_1 e_2 : β |  |
(GABS) |  S;Γ(x↦τ_1) ⊢_g e : τ_2S;Γ⊢_g λx:τ_1 . e : τ_1 →τ_2 |

(b)

Figure 1: Simply and gradually typed lambda calculus with type variables
Figure 2: Huet’s unification of
$\\{\alpha\rightarrow\alpha=Int\rightarrow\beta\\}$

Siek and Vachchrajani [25](S&V) propose an innovative solution for performing
gradual type inference which combines gradual typing with type inference.
Their main goal is to allow inference to operate on the statically typed parts
of the code, while leaving the dynamic parts to runtime checks. Furthermore,
the dynamic type must unify with static types and type variables, so that the
static and dynamic portions of code may freely interact. In this section, we
summarize their work.

The work of S&V is based on the gradually typed lambda calculus [23]. The
gradually typed lambda calculus extends the simply typed lambda calculus
($\lambda_{\rightarrow}$) with an unknown type, $?$–pronounced “dynamic”; type
checking for terms of this type is left until runtime. The gradually typed
lambda calculus ($\lambda_{\rightarrow}^{?}$) allows static and dynamic types
to freely mix and satisfies the gradual guarantee [26], ensuring smooth
migration between static and dynamic code while maintaining the correctness of
the program.

Type inconsistencies in $\lambda_{\rightarrow}^{?}$ are caught by a
_consistent_ relation, instead of equality as in $\lambda_{\rightarrow}$. The
_consistent_ relation only compares parts of a type that are statically known;
it is one of the key contributions of $\lambda_{\rightarrow}^{?}$. All type
errors that cannot be statically resolved by the gradual type system are
delegated to runtime checks.

Type inference allows programmers to omit type annotations in their programs
and have the compiler infer the types for them. Hindley-Milner type inference
is often cast as a two step process that consists of generating constraints
and then solving them by a unification algorithm [32, 20, 21]. The inference
algorithm models the typing rules as equations, called constraints, between
type variables, while the unification algorithm computes a substitution $S$,
which is a mapping from type variables to types, such that for each equation
$\tau_{1}=\tau_{2}$, we have $S(\tau_{1})=S(\tau_{2})$.

S&V introduce the gradually typed lambda calculus with type variables (
$\lambda_{\rightarrow}^{?\alpha}$), which is $\lambda_{\rightarrow}^{?}$
extended with type variables, $\alpha$. They define a new relation,
_consistent-equal_ ($\simeq$), which extends the _consistent_ relation from
$\lambda_{\rightarrow}^{?}$ to treatment $\alpha$. Fig. LABEL:fig:lam-dyn-a-ts
compares the typing rules for $\lambda_{\rightarrow}^{\alpha}$, the statically
typed lambda calculus with type variables, to the new type system
$\lambda_{\rightarrow}^{?\alpha}$. S&V also specify a unification algorithm
for $\lambda_{\rightarrow}^{?\alpha}$ which integrates the _consistent-equal_
into Huet’s unification algorithm [10, 14] which is a popular algorithm that
doesn’t rely on substitution.

Huet’s unification algorithm uses a graph representation for types. For
example, a type like $Int\rightarrow\beta$ is represented as a sub graph in
Fig. 2. A node represents a type, ground types, type variables or the function
type ($\rightarrow$), and edges connect the nodes of types belonging to a
$\rightarrow$ type. From this it follows that the unification algorithm is the
amalgamation of two graphs present in a constraint equation following the
rules of the type system. Huet’s algorithm maintains a union find structure
[27] to maintain equivalence classes among nodes and thereby types. When node
$A$ unifies with node $B$ according to the type rules, the merge results in
one of the two nodes becoming the representative of the merge. This signifies
that the representative node is the solution to the constraint being unified.
Fig. 2 shows how the unification of the constraint
$\\{\alpha\rightarrow\alpha=Int\rightarrow\beta\\}$ proceeds.

##  3 Introduction to BCL

Our motivation to explore gradual types for BCL is rooted in several
historical and contextual details, which we discuss in this section. It is
first helpful to understand that BCL is predominantly used to model financial
contracts, by providing end users with programmatic access to a financial
contract library. The library we use is based upon the composable contracts of
Peyton Jones, Eber and Seward [19]. Its internal contract data structure is
used throughout our broader derivatives system to support various downstream
analyses. In this way, BCL serves as an expressive front-end for describing
contracts to our derivatives system.

⬇

let receive currency amount = scale (one currency) amount in

let european_stock_option args =

let first = stock_price args.effective_date args.company in

let last = stock_price args.expiry_date args.company in

let payoff = match args.call_or_put with

| Call -> (last / first - args.strike)

| Put -> (args.strike - last / first)

in

european args.expiry_date (receive args.currency payoff)

in

european_stock_option

{ company = "ABC Co.",

call_or_put = Call,

strike = 100.0,

currency = USD,

effective_date = 2021-01-17,

expiry_date = 2021-01-22 }

Figure 3: European stock option

Let us look at a short illustrative example of BCL code. Fig. 3 provides an
example of the sort of thing for which BCL might be used. The
european_stock_option function produces a Contract which models a European
stock option. European stock options grant their holder the right, but not the
obligation, to buy or sell stock in a company. The “European” in European
stock option refers to the fact that, on one specific date, the holder must
choose whether or not s/he would like to buy (or sell) the stock. This is in
contrast to “American” options, where the holder may choose to buy (or sell)
on any date within a specified range of dates.

This stock option is based on several helper functions, defined in [19], which
we must examine first. The european function constructs a contract which
allows its holder to choose between receiving “something” or nothing on a
specified date. receive constructs a contract that pays the specified amount
of the specified currency passed as arguments andn uses the scale and one
primitives. The scale primitive takes an amount of type $Obs\ Double$–where
type $Obs\ d$ represents a time-varying quantity of type $d$–and a contract as
arguments and multiplies key values in the contract by the amount. Note that
european_stock_option uses - and / operators which are built-ins that operate
on $Obs\ Double$ arguments. stock_price is a primitive for looking up the
price of the specified stock on the specified date.

european_stock_option starts off by using stock_price to look up the price of
the specified company’s stock on the “effective” (contract start) and “expiry”
(contract end) dates. It uses these stock prices to construct the payoff based
on the specified call or put style, and feeds the payoff to receive to
construct a contract that pays it. Finally european_stock_option passes the
result of receive to the european, which allows the holder to choose between
the payoff and nothing. Note that the payoff may well be negative, so the
holder’s choice is not entirely clear. The end of Fig. 3, provides an example
call european_stock_option which constructs a call option on ABC Co. In
practice, functions like european_stock_option would be defined in BCL’s
standard library, and would be called by users who wish to model European
stock options directly or who wish to model contracts that contain such
options as sub-contracts.

###  3.1 Motivation for gradual types

Given that BCL is mostly used to describe financial contracts, it should come
as no surprise that our users are largely financial professionals. In
particular, many are financial engineers or quantitative analysts with some
programming experience in dynamic languages such as Python and MATLAB.
Typically these users need to translate term sheets, plain-English
descriptions of a contract, into BCL for consumption by our system. These
contracts are mostly one-off and, once finished, are unlikely to be reused as
subcontracts to build further contracts. For these reasons, the users of BCL
are primarily concerned with development speed. Ideally, they would like to be
able to translate a term sheet as quickly as possible, so that they may focus
on analyzing the contract’s behavior once it has been ingested by our system.

On the other hand, the maintainers of BCL and its standard library are
software engineers and functional programmers with extensive experience in
OCaml, C++ and other static languages. The main jobs of the BCL maintainers
are implementing language extensions and standard library functions. One of
the significant constraints that they face is preserving backwards
compatibility. All existing user contracts must continue to work as BCL
evolves–even minor changes in behavior are unacceptable! Given the broad reuse
of the features that BCL’s language maintainers implement and the difficulties
involved in rolling back features, correctness is the paramount concern of BCL
maintainers.

Finally, it is important to note that the version of BCL described here is
actually the second version of BCL. The first version of BCL was dynamically
typed, so we will distinguish it from the second version by referring to it as
Dynamic BCL. Dynamic BCL supports only a few primitive data types, as well as
a list composite type; it does not support algebraic types. It also runs only
minimal validation before attempting evaluation. This simplicity makes Dynamic
BCL well suited to our users who seek to quickly feed contracts into our
system, but ill-suited to the library code written by our maintainers.
Additionally, some users who encounter runtime type errors while implementing
particularly complex contracts would turn to the maintainers for assistance,
further increasing the burden on the maintainers. It was in light of these
issues, that we developed (Static) BCL.

To address the issues with Dynamic BCL while remaining useful to our users,
BCL aims to be a static language that feels roughly dynamic. To this end, BCL
supports implicit static types via type inference; we chose Hindley-Milner
style inference so that our users could omit type annotations in almost all
cases. BCL also supports record and variant types, although they are
structural rather than the nominal ones typically seen in OCaml and Haskell.
This choice also lends BCL a more dynamic feel.

The goal of BCL’s design is to retain enough flexibility for our users, while
introducing static types for the benefit of our language maintainers. However,
“enough flexibility” is entirely subjective and some users may well feel that
any amount of static checking results in a system that is too inflexible.
Gradual types address this concern by allowing users to use dynamic types
where they like, while also allowing maintainers to use static types where
they would like. Importantly, gradual types guarantee that fully dynamic code
and fully static code can co-exist, and that static code is never blamed for
runtime type errors. Taken together, these two guarantees satisfy both groups,
and ensure that the type errors that dynamic users see are isolated to the
code that they themselves wrote.

###  3.2 Core calculus

BCL’s core calculus is the lambda calculus extended with structural composite
types and recursive types. Furthermore, BCL is implicitly-typed and supports
Hindley-Milner style type inference. This section describes the types and
terms of this core calculus. Note, however, that the grammars in this section
are abstract representations of BCL’s theoretical underpinnings, and do not
cover the full set of productions in BCL’s grammar.

####  3.2.1 Kinds and Types

$\begin{array}[]{l c l l
cl}\kappa&::=&*\mid\rho\mid\kappa\Rightarrow\kappa&C&::=&\rightarrow\mid\Pi\mid\Sigma\mid...\\\
\tau&::=&\alpha\mid C\mid\tau\ \tau\mid
l:\tau;\tau\mid\epsilon\mid\mu\alpha.\tau&\sigma&::=&\tau\mid\forall\alpha.\sigma\end{array}$

Figure 4: Grammar of types and kinds

The grammar of the types and kinds that describe BCL is given in Fig. 4. Our
kind system is fairly standard and consists of only three forms. The base
kind, $*$, is the kind of “proper” types–$Int$ and $Int\rightarrow Int$, for
example–which themselves describe terms. The row kind, $\rho$, is of course
the kind for rows. The operator kind, $\Rightarrow$, is the kind of type
operators – $Array$ and $\rightarrow$, for example – which take types as
arguments and which do not directly describe terms.

$C$ ranges over type constructors, including the type operators for function
types ($\rightarrow$ of kind $*\Rightarrow*\Rightarrow*$), record types ($\Pi$
of kind $\rho\Rightarrow*$) and variant types ($\Sigma$ of kind
$\rho\Rightarrow*$). $C$ may also include additional constructors for base
types (e.g. $Int$ and $String$) and more type operators (e.g. $Array$) as
desired. However, these additional constructors are not useful for our
purposes here, so we make no further mention of them.

Our type system is stratified into monomorphic types and type schemes, per
[4]. Monomorphic types, $\tau$, consist of type variables, type constructors,
and record, variant and recursive types. Type variables are ranged over by
$\alpha$, $\beta$, $\gamma$, etc., and are explicitly bound by $\mu$ and
$\forall$ types, as described below. Rows are written $l:\tau;\tau^{\prime}$,
indicating that the row has a field labeled $l$ of type $\tau$.
$\tau^{\prime}$ has kind $\rho$ and dictates the other fields that the row may
contain. If $\tau^{\prime}$ is a type variable, the row can contain arbitrary
additional fields; if $\tau^{\prime}$ is the empty row, $\epsilon$, the row
contains no additional fields; finally if $\tau^{\prime}$ is another type of
the form $l:\tau;\tau^{\prime}$, then the row contains exactly the fields
specified therein. Recursive types are written $\mu\alpha.\tau$, where the
variable $\alpha$ represents the point of recursion and is bound within
$\tau$. BCL’s recursive types are equi-recursive, so it does not have explicit
constructs for rolling and unrolling recursive types. Finally, type schemes
have two forms: monomorphic types and universally quantified schemes.
Monomorphic types, $\tau$, are merely the types described above. Universally
quantified schemes, $\forall\alpha.\sigma$, bind the variable $\alpha$ within
the scheme $\sigma$. Naturally, it is through universal quantification that
BCL supports parametric polymorphism.

####  3.2.2 Terms

$\begin{array}[]{l c l}t&::=&x\mid\lambda x.t\mid t\ t\mid{\textbf{let}\
\textbf{rec}\ x=t\ \textbf{in}\ t}\mid
t:\tau\mid\\{\overline{l_{i}:t_{i}}\\}\par\mid t.l\mid l\ t\mid\textbf{match}\
t\ \textbf{with}\ \overline{l_{i}x_{i}\Rightarrow t_{i}}\par\end{array}$

Figure 5: Grammar of terms

The grammar of the terms in BCL is given in Fig. 5. Most of the term forms are
drawn directly from the lambda calculus. Term variables are ranged over by
$x$, $y$, $z$, etc., and are introduced by lambda abstraction, let-bindings
and match-expressions. Lambda abstraction is written $\lambda x.t$ and binds
$x$ within the expression $t$. Lambda abstractions are eliminated by
application, which is denoted by juxtaposition: $t\ t$. Let-bindings are
written $\textbf{let}\ \textbf{rec}\ x=t\ \textbf{in}\ t$. The rec is optional
and, when present, indicates $x$ may be referenced by the expression to the
right of the $=$; $x$ may of course always be referenced by the expression to
the right of the in. Type annotations are written $t:\tau$, and serve to
ensure that $t$ has the they $\tau$.

In addition to the forms described above, BCL supports records and variants.
Record introduction is written $\\{\overline{l_{i}:t_{i}}\\}$ , where $t_{i}$
evaluates to the value stored in the field $l_{i}$. Records are eliminated by
field projection. The projection of the field $l$ from the record $t$ is
written $t.l$. Variant introduction is written $l\ t$, where the label $l$ is
used to tag the variant’s payload, $t$. Variants are eliminated by case
analysis, which is written $\textbf{match}\ t\ \textbf{with}\
\overline{l_{i}x_{i}\Rightarrow t_{i}}$, which evaluates to the branch
specified by the tag associated with the variant $t$.

##  4 Implementation

We identify three main components required to add gradual typing to a
statically typed language with type inference, such as BCL. The first is the
ability to annotate terms with types, as these annotations dictate whether a
term is type-checked statically or dynamically. The second is the addition of
a dynamic type to the existing set of types, and the third is an algorithm to
unify the existing types with the newly added dynamic type. Since our grammar,
shown in Fig. 5, already supports explicit annotation of terms, we have the
means to differentiate between dynamically typed and statically typed code. We
add a dynamic type, ?, to our set of types; it serves to indicate that a term
that will be dynamically typed. BCL’s type inference algorithm statically
infers a type for every term, meaning that by default BCL programs are
completely statically typed. In order to tell the type system to dynamically
type some terms, we must explicitly annotate those terms with the ? type.

For example: a simple increment function can be defined in BCL as follows.

⬇

let incr x = x + 1 in incr

The type system will infer the type $Int\rightarrow Int$ for the incr
function. However, we can instead provide an explicit annotation.

⬇

let incr x = x + 1 in incr : ? -> Int

In this case, the inference algorithm retains the annotated type as the type
of the function. Any type checks on the argument of the incr function would be
put off until runtime. While the type checks pertaining to ? types are
delayed, we still need to complete the inference procedure in order to infer
the types of the un-annotated portions of the program (like the return type of
incr). Siek and Vacchrajani [25](S&V) extend the standard unification-based
inference algorithm to handle the ? type. Their algorithm is based on the
_consistent-equal_ relation which takes into consideration the type variables
that are generated as part of a typical type inference algorithm. Fortunately
for us, their algorithm works well for our implementation with only minor
adaptations.

⬇

maybe_copy_dyns ($\tau_{1}\simeq\tau_{2}$) =

$\tau_{1}^{\prime}$ $\leftarrow$ if was_copied $\tau_{1}$ then $\tau_{1}$ else
copy_dyn $\tau_{1}$

$\tau_{2}^{\prime}$ $\leftarrow$ if was_copied $\tau_{2}$ then $\tau_{2}$ else
copy_dyn $\tau_{2}$

$\tau_{1}^{\prime}\simeq\tau_{2}^{\prime}$

unify $\tau_{1}^{\prime\prime}$ $\tau_{2}^{\prime\prime}$ =

$\tau_{1}$ $\leftarrow$ find $\tau_{1}^{\prime\prime}$

$\tau_{2}$ $\leftarrow$ find $\tau_{2}^{\prime\prime}$

if was_visited $\tau_{1}$ and was_visited $\tau_{2}$ then

()

else case maybe_copy_dyns ($\tau_{1}\simeq\tau_{2}$) of

$\alpha\simeq\tau$ $\mid$ $\tau\simeq\alpha$ $\Rightarrow$ merge $\tau$
$\alpha$ (*Case 1 & 2*)

$\mid$ $?\simeq\tau_{1}\ \rightarrow\tau_{2}$ $\mid$ $\tau_{1}\
\rightarrow\tau_{2}\simeq\ ?$ $\Rightarrow$ (*Case 3 & 4*)

unify $\tau_{1}$ (new $?$)

unify $\tau_{2}$ (new $?$)

$\mid$ $?\simeq\tau$ $\mid$ $\tau\simeq\ ?$ $\Rightarrow$ merge $\tau$ $?$
(*Case 5 & 6*)

$\mid$ $\tau_{11}\ \rightarrow\tau_{12}\simeq\tau_{21}\ \rightarrow\tau_{22}$
$\Rightarrow$ (*Case 7*)

unify $\tau_{11}$ $\tau_{21}$

unify $\tau_{12}$ $\tau_{22}$

$\mid$ $l:\tau_{1};\tau_{2}\simeq
l^{\prime}:\tau_{1}^{\prime};\tau_{2}^{\prime}$ if $l$ = $l^{\prime}$
$\Rightarrow$ (*Case 8*)

unify $\tau_{1}$ $\tau_{1}^{\prime}$

unify $\tau_{2}$ $\tau_{2}^{\prime}$

$\mid$ $l:\tau_{1};\tau_{2}\simeq
l^{\prime}:\tau_{1}^{\prime};\tau_{2}^{\prime}$ $\Rightarrow$ (*Case 9*)

$\alpha$ $\leftarrow$ fresh_type_variable()

unify ($l:\tau_{1};\alpha$) $\tau_{2}^{\prime}$

unify ($l^{\prime}:\tau_{1}^{\prime};\alpha$) $\tau_{2}$

$\mid$ $\mu\alpha.\tau\simeq\tau^{\prime}$ $\mid$
$\tau^{\prime}\simeq\mu\alpha.\tau$ $\Rightarrow$ (*Case 10 & 11*)

mark_visited ($\mu\alpha.\tau$)

unify $\tau[\mu\alpha.\tau/\alpha]$ $\tau^{\prime}$

$\mid$ $\epsilon\simeq\epsilon$ $\Rightarrow$ () (*Case 12*)

$\mid$ _ $\Rightarrow$ error

infer $\Gamma$ $t$ =

case $t$ of

…

$t:\tau$ $\rightarrow$

case (unify (infer $\Gamma$ $t$) $\tau$) of

Error $\Rightarrow$ Error : inconsistent types

$\mid$ _ $\Rightarrow$ $\tau$

Figure 6: Type inference algorithm

Fig. 6 shows an outline of our adaptation of S&V’s inference algorithm. Unlike
the original algorithm by S&V, BCL’s does not separate constraint generation
and constraint solving.222Put another way, our inference algorithm solves each
constraint immediately after generating it, and before generating the next
constraint. This difference is important, as it means that our inference
algorithm does not have access to the whole constraint set prior to
unification. Instead the infer function traverses the term, generating and
solving constraints on the fly. For example, if it encounters an application
$t_{1}\ t_{2}$, it figures out the type of the term from the environment
($\Gamma$) and generates a constraint like
$\\{\tau_{1}\simeq\tau_{2}\rightarrow\alpha\\}$, where $\tau_{1}$ is the type
of term $t_{1}$, $\tau_{2}$ is the type of $t_{2}$ and $\alpha$ is a fresh
type variable. infer sends this constraint to unify, which attempts to satisfy
it or raises an error if the constraint cannot be satisfied.

Fig. 6 shows the infer case for a term $t$ annotated with the type $\tau$.
infer generates a constraint which tries to unify the type inferred for $t$
with the annotated type, $\tau$. We highlight this case for two reasons.
First, the only way we can currently introduce a ? type in BCL is through an
annotation. Therefore, this is the only point where constraints involving the
? type originate. Second it is critically important that this case returns the
annotated type and not the inferred type. Note that in incr the inferred type
$Int\rightarrow Int$ differs from–but is _consistent-equal_ with–the annotated
type $\texttt{?}\rightarrow Int$. We always want the user’s explicit
annotation to take precedence in this situation.

BCL’s unification algorithm is already based on Huet’s unification algorithm,
which makes adopting the changes suggested by S&V easier. The crux of S&V’s
algorithm lies in the way the ? type unifies with other types, and
particularly with type variables. When ? unifies with a type variable, S&V’s
algorithm makes ? the representative node. However, when ? unifies with types
other than type variables, the other type becomes the representative element
of the resulting set. The find and merge functions in Fig. 6 come from the
union-find data structure that underlies Huet’s unification algorithm.
Respectively, they compute a node’s representative element, and union two
nodes’ sets keeping the representative element of the first node’s set.

The first six cases of the unify function handle unification with the ? type
as laid out by S&V. We say first six because Cases 1 and 2 take care of
unifying the ? type with type variables as specified by S&V’s algorithm. Cases
3 and 4 handle an edge case in their algorithm. These two cases simulate the
operational semantics of Siek and Taha [23], which require constraints like
$\\{\texttt{?}\simeq\alpha\rightarrow\beta\\}$ to be treated as
$\\{\texttt{?}\rightarrow\texttt{?}\simeq\alpha\rightarrow\beta\\}$. We use
new to create a new node different from what was passed in to handle this
case.

Cases 8-11 take care of unifying with row and recursive types, neither of
which are covered by S&V’s solution. However, it is our observation that these
types do not require special handling. A constraint like
$\\{x:Int;\epsilon\simeq\texttt{?}\\}$ would be handled by Case 2 and ? would
be merged with the row type $x:Int;\epsilon$. Now suppose the ? is present
inside the row type like in the following constraint
$\\{x:\texttt{?};\epsilon\simeq x:Int;\epsilon\\}$; this will be handled by
Case 8 and then Cases 5 and 12 when we recursively call unify with the types
within the row. The same holds true for unification with the recursive type.
For example, a constraint like $\\{List\ Int\simeq List\ \texttt{?}\\}$ will
have the following successful unification trace:

$\displaystyle\\{List\ Int\simeq List\ \texttt{?}\\}$ (Case 10)
$\displaystyle\rightarrow\\{\Pi(head:Int;tail:List\ Int;\epsilon)\simeq List\
\texttt{?}\\}$ (Case 11) $\displaystyle\rightarrow\\{\Pi(head:Int;tail:List\
Int;\epsilon)\simeq\Pi(head:\texttt{?};tail:List\ \texttt{?};\epsilon)\\}$
(Case 8) $\displaystyle\rightarrow\\{\\{Int\simeq\texttt{?}\\},\\{List\
Int\simeq List\ \texttt{?}\\}\\}$ (Case 6, Case 10)
$\displaystyle\rightarrow\cdots$ $\displaystyle\rightarrow\\{\Pi\
\epsilon\simeq\Pi\ \epsilon\\}$ (Case 8)
$\displaystyle\rightarrow\\{\epsilon\simeq\epsilon\\}\rightarrow()$ (Case 12)

Where $List$ is defined as follows.

$List\ \alpha\equiv\mu
a.\Sigma(Nil:\Pi\epsilon;Cons:\Pi(head:\alpha;tail:a;\epsilon);\epsilon)$ Note
that BCL supports equi-recursive types, as mentioned in Section 3, so unify
tracks the types it visits with mark_visited and was_visited to detect cycles.

####  4.0.1 The copy_dyn conundrum:

The copy_dyn function is a crucial part of the way ? unifies with other types.
In S&V’s presentation, copy_dyn ensures that each ? node in the constraint set
is physically unique. Without this step, multiple types might unify with the
same ? node, and then transitively with each other. This has the potential to
cause spurious failures in unify. S&V’s solution to this is to traverse the
constraint set and duplicate each ? node prior to unification; this is
performed by their implementation of copy_dyn. Unfortunately, we do not have
access to the full constraint set, because our inference algorithm generates
and solves constraints in one step.

Our first attempt at working around this issue was to call copy_dyn as the
first step in unification. However, this leads to over copying. For example,
consider the constraint {
$\texttt{?}\rightarrow\alpha\simeq\alpha\rightarrow\tau$ }. According to Case
7 of unify, when $\alpha$ unifies with the ? node, copy_dyn is called and a
new ? node is created in the union-find structure. But when $\alpha$ then
unifies with $\tau$, find looks up ? as $\alpha$’s representative element, and
copy_dyn is called once more. $\tau$ therefore unifies with the new ? node,
instead of the one which unified with $\alpha$. Thus, we lose the fact that
$\tau$ and $\alpha$ are the same type.

To rectify this, we implement maybe_copy_dyns, which traverses a constraint
and copies each ? node exactly once.333There are many ways to accomplish this.
Our approach was to use one canonical ? node in type annotations, and compare
each ?’s address to the canonical node’s address before copying. The result of
this is the same as originally intended by S&V’s copy_dyn function. That is,
we ensure there is a unique ? node in the union-find structure for every
unique use of ?.

###  4.1 Discussion

In Section 2 we gave an overview of how statically typed languages approach
this problem of promoting dynamic typing. It is our observation that most
statically typed, object-oriented languages approach dynamic typing following
Abadi et al. That is, their dynamic type exploits subtype polymorphism to
bypass static type checking. This is a natural direction for object-oriented
languages which rely heavily on subtyping. In order to inspect the types at
runtime, these languages make use of type reflection. Java is one such
language where work has been done to add dynamic types using reflection,
contracts and mirrors [6]. The Java Virtual Machine supports many dynamic
languages like Jython and JRuby, demonstrating that such runtime constructs
help static languages add more dynamic type checks. However, these
implementations only add dynamic checks, and do not achieve the gradual goal
of a seamless mix of static and dynamic types as in [26]. To our knowledge,
only Featherweight Java [11] has attempted to support proper gradual typing
[12]. In any case, the primary purpose for dynamic types in these languages is
inter-operation with other dynamic languages. This differs from our own
purpose and the end result does not fit our needs well. Thus we conclude that
this approach was not a good design choice for us.

The languages closest to BCL are statically typed functional languages with
type inference, such as SML, OCaml, and Haskell. OCaml has incorporated
dynamic typing at the library level by leveraging its support for generalized
algebraic data types [3]. Similarly, Haskell supports a dynamic type as a
derivative of the Typeable type class, which uses reflection [13] to look at
the runtime representation of types. While these approaches introduce more
dynamism, they lack the simplicity of gradual typing, which hide all the nuts
and bolts of the type system under a simple ? annotation.

Seamless interoperation of static and dynamic types as promised by gradual
typing fits very well with our use case. It lets our end users access both
paradigms without knowledge of specialized types or constructs. Furthermore,
the approach we use—extending unification-based inference with gradual
typing—is a natural extension for languages like BCL, which support static
type inference. The addition of dynamic types to the type system easily boils
down to how we handle this new type in the unification algorithm, and does not
require reworking the entire type system. We attribute this benefit to S&V’s
proposed inference algorithm, which incorporates the essence of the
$\lambda_{\rightarrow}^{?}$ type system. This makes it easier to adapt to an
existing language with similar constructs.

Garcia and Cimini’s work takes a different approach to this problem but their
end goal is the same: gradual type inference in a statically typed language.
The authors of that work feel that S&V’s approach has “complexities that make
it unclear how to adopt, adapt, and extend this approach with modern features
of implicitly typed languages like let-polymorphism, row-polymorphism and
first class polymorphism”. Our experience with S&V’s approach was different:
we found the integration fairly simple without major changes to the original
inference algorithm. We leave a deep dive into the differences between these
two schemes to future work. Based on Garcia and Cimini’s design principle, Xie
et al. [34] introduce an inference algorithm with support for higher-rank
polymorphism, using a _consistent subtyping_ relation. In contrast, BCL only
infers rank-1 polymorphic types and doesn’t support higher-rank polymorphism.

We recognize an added benefit of going from a static to a dynamic language
with explicit ? annotations. Promoting static type checking in a dynamic
language without type inference requires the programmer to add annotations to
all parts of the code that they want statically checked. Needing to add these
annotations is such a burden for the programmer that they often skip some
annotations and miss out on static optimizations. These un-annotated types are
implicitly dynamic, leading to runtime overhead, despite the fact that on many
occasions they could be statically inferred. This in turn has lead to efforts
to making gradual typing more efficient [22].

BCL does not have this issue as it provides static inference by default. It
therefore enjoys the optimizations of static typing and and can skip
unnecessary runtime checks. Moreover, BCL could support a dynamic-by-default
mode with an additional compiler flag that implicitly annotates un-annotated
terms with the ? type. This makes it even more seamless to go from complete
static typing to complete dynamic typing. We might also consider doing this
implicit annotation on a file-level or function-level. In cases where it is
possible to separate dynamic and static components, this could even lead to
cleaner refactoring. These ideas have not yet been implemented in BCL but are
something we intend to do as future work.

##  5 Application of gradual types

Gradual typing enables the quick prototyping common in dynamic languages, as
well as specialized applications that enable simplification of existing code.
In this section, we focus on the latter, due to space constraints. Notice, in
Fig. 3, that the scale combinator [19] is simply multiplication of a contract
by a floating-point _observable_. In a domain specific language like BCL, it
is convenient to reuse the ** multiplication syntax for scale as well. We can
fit this more general _observable_ multiplication operator into the type
system with the gradual type $Obs\
Double\rightarrow\texttt{?}\rightarrow\texttt{?}$. Our new multiplication
operator can delegate to scale when the second argument a $Contract$ at
runtime and continue with _observable_ multiplication, or raise a runtime type
error based on the runtime type of the second argument. With this new
operator, the receive function can be rewritten thus:

⬇

let receive currency amount = one currency ** amount in ...

There are a variety of extensions to Hindley-Milner that enable this sort of
ad-hoc polymorphism statically. Type classes, for example, extend the
signature of overloaded functions with classes [31], which our users would
need to learn. Similarly, modular implicits introduce a separate syntax for
implicit modular arguments [33]. However, these constructs require effort to
educate our end users in their use and detract from the dynamic feel of the
language. Gradual types, by contrast, are much easier for our end users since
they already work in a dynamic environment and it does not require new syntax
(save a ? annotation).

It is worth noting that, while the new multiplication operator can be given a
valid type in BCL, it cannot currently be implemented in BCL; it can only be
implemented as a built-in operator because BCL provides no way to perform case
analysis on the runtime type of a dynamic value. However, addressing this is
actually quite easy if we reuse BCL’s existing support for variants. That is,
we could implement a dynamic_to_type primitive which consumes a dynamic value
and produces a variant describing its runtime type. This would allow us to
then branch on this variant with the existing match construct. Fig. 7 shows a
prototype of a function that achieves this effect assuming the dynamic_to_type
primitive is defined.

⬇

let dyn_obs_mul x y = match dynamic_to_type (y) with

| Obs Double => x ** y

| Contract => scale x y

in

dyn_obs_mul : Obs Double $\rightarrow$ Dyn $\rightarrow$ Dyn

Figure 7: Sample of a dynamic Observable multiplication function

dynamic_to_type is interesting in light of our discussion in Section 2, which
describes dynamic programming as the territory of BCL’s users and not its
maintainers. Clearly, however, the dynamic multiplication operator is
something that would live in BCL’s standard library and be maintained by the
language maintainers. Indeed there are a number of interesting standard
library functions which we might add on top of dynamic_to_type. Another simple
example would be a any_to_string function, which could produce a string
representation for arbitrary types by traversing their runtime type and
delegating to the appropriate type-specific to-string function. Such a
function would be very handy for debugging and quick inspection of values.

The any_to_string example is a function which consumes an arbitrary value.
However, there are equally compelling use cases for producing arbitrary
values. For example, property-based testing frameworks rely on automatically
generating values that conform to certain constraints. We could implement a
simple property-based testing framework with a function which consumes the
output of dynamic_to_type and generates arbitrary values that conform to that
type. Such a framework would be especially useful in a domain such as ours,
where real money is at stake, and where robust testing is absolutely critical.

##  6 Conclusion

Dynamic languages are extremely popular with many users. For users with a
limited computer science background, for whom ease-of-use is the paramount,
this is doubly true. However, despite the flexibility offered by dynamic
typing, the safety offered by static typing is helpful in domains where
correctness is critical. In such an arena, gradual types are a perfect blend
of both paradigms, and they provides a middle ground to please a larger group
of users. Given this, it is important for the literature to speak about
adapting gradual types to existing languages. As a first step towards that, we
write about our experiences adapting gradual typing to our implementation of a
statically typed functional language with type inference. We provide context
in terms of how others in similar situations approached this problem, and we
elaborate our inference algorithm with key insights around what worked for us
and what did not. We identify an interesting use case for gradual types here
at Bloomberg, where we look to harmonize end users and language maintainers
with competing goals. End users want to specify financial contracts without
worrying about static typing demands, while language maintainers need a more
rigorous type system that ensures that libraries that they write are error-
free. Gradual types allow us to satisfy both groups. We also intend to gather
feedback from our end users and maintainers about how gradual types are being
used , which can give insight into possible tweaks to make this system more
amenable to all.

## References

  * [1] Using type dynamic. https://docs.microsoft.com/en-us/dotnet/csharp/programming-guide/types/using-type-dynamic, accessed: 2020-10-02
  * [2] Abadi, M., Cardelli, L., Pierce, B., Plotkin, G.: Dynamic typing in a statically typed language. ACM transactions on programming languages and systems (TOPLAS) 13(2), 237–268 (1991)
  * [3] Balestrieri, F., Mauny, M.: Generic programming in ocaml. Electronic Proceedings in Theoretical Computer Science 285, 59–100 (Dec 2018). https://doi.org/10.4204/eptcs.285.3, http://dx.doi.org/10.4204/EPTCS.285.3
  * [4] Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 207–212 (1982)
  * [5] Garcia, R., Cimini, M.: Principal type schemes for gradual programs. SIGPLAN Not. 50(1), 303–315 (Jan 2015). https://doi.org/10.1145/2775051.2676992, https://doi.org/10.1145/2775051.2676992
  * [6] Gray, K.E., Findler, R.B., Flatt, M.: Fine-grained interoperability through mirrors and contracts. ACM SIGPLAN Notices 40(10), 231–245 (2005)
  * [7] Greenberg, M.: The dynamic practice and static theory of gradual typing. In: 3rd Summit on Advances in Programming Languages (SNAPL 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)
  * [8] Gronski, J., Knowles, K., Tomb, A., Freund, S.N., Flanagan, C.: Sage: Hybrid checking for flexible specifications. In: Scheme and Functional Programming Workshop. vol. 6, pp. 93–104 (2006)
  * [9] Hejlsberg, A.: C# 4.0 and beyond by anders hejlsberg. Microsoft Channel 9 (2010)
  * [10] Huet, G.: A unification algorithm for typed lambda calculus. Theoretical Computer Science 1(1), 27 – 57 (1975). https://doi.org/https://doi.org/10.1016/0304-3975(75)90011-0, http://www.sciencedirect.com/science/article/pii/0304397575900110
  * [11] Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight java: A minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (May 2001). https://doi.org/10.1145/503502.503505, https://doi.org/10.1145/503502.503505
  * [12] Ina, L., Igarashi, A.: Gradual typing for featherweight java. Computer Software 26(2), 18–40 (2009)
  * [13] Jones, S.P., Weirich, S., Eisenberg, R.A., Vytiniotis, D.: A reflection on types. In: A List of Successes That Can Change the World, pp. 292–317. Springer (2016)
  * [14] Knight, K.: Unification: A multidisciplinary survey. ACM Computing Surveys (CSUR) 21(1), 93–124 (1989)
  * [15] Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 31(3), 1–44 (2009)
  * [16] Meijer, E., Drayton, P.: Static typing where possible, dynamic typing when needed: The end of the cold war between programming languages. Citeseer (2004)
  * [17] Milner, R.: A theory of type polymorphism in programming. Journal of computer and system sciences 17(3), 348–375 (1978)
  * [18] Miyazaki, Y., Sekiyama, T., Igarashi, A.: Dynamic type inference for gradual hindley–milner typing. Proc. ACM Program. Lang. 3(POPL) (Jan 2019). https://doi.org/10.1145/3290331, https://doi.org/10.1145/3290331
  * [19] Peyton Jones, S., Eber, J.M., Seward, J.: Composing contracts: An adventure in financial engineering (functional pearl). SIGPLAN Not. 35(9), 280–292 (Sep 2000). https://doi.org/10.1145/357766.351267, https://doi.org/10.1145/357766.351267
  * [20] Pottier, F.: A modern eye on ml type inference: old techniques and recent developments (09 2005)
  * [21] Pottier, F., Rémy, D.: The Essence of ML Type Inference, pp. 389–489 (01 2005)
  * [22] Rastogi, A., Chaudhuri, A., Hosmer, B.: The ins and outs of gradual type inference. SIGPLAN Not. 47(1), 481–494 (Jan 2012). https://doi.org/10.1145/2103621.2103714, https://doi.org/10.1145/2103621.2103714
  * [23] Siek, J., Taha, W.: Gradual typing for functional languages. i: Scheme and functional programming workshop (2006)
  * [24] Siek, J., Taha, W.: Gradual typing for objects. In: European Conference on Object-Oriented Programming. pp. 2–27. Springer (2007)
  * [25] Siek, J.G., Vachharajani, M.: Gradual typing with unification-based inference. In: Proceedings of the 2008 symposium on Dynamic languages. pp. 1–12 (2008)
  * [26] Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T.: Refined Criteria for Gradual Typing. In: Ball, T., Bodik, R., Krishnamurthi, S., Lerner, B.S., Morrisett, G. (eds.) 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 32, pp. 274–293. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015). https://doi.org/10.4230/LIPIcs.SNAPL.2015.274, http://drops.dagstuhl.de/opus/volltexte/2015/5031
  * [27] Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of the ACM (JACM) 22(2), 215–225 (1975)
  * [28] Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: from scripts to programs. In: Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications. pp. 964–974 (2006)
  * [29] Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. ACM SIGPLAN Notices 43(1), 395–406 (2008)
  * [30] Vitousek, M.M., Kent, A.M., Siek, J.G., Baker, J.: Design and evaluation of gradual typing for python. In: Proceedings of the 10th ACM Symposium on Dynamic Languages. p. 45–56. DLS ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2661088.2661101, https://doi.org/10.1145/2661088.2661101
  * [31] Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 60–76. POPL ’89, Association for Computing Machinery, New York, NY, USA (1989). https://doi.org/10.1145/75277.75283, https://doi.org/10.1145/75277.75283
  * [32] Wand, M.: A simple algorithm and proof for type inference (1987)
  * [33] White, L., Bour, F., Yallop, J.: Modular implicits. Electronic Proceedings in Theoretical Computer Science 198, 22–63 (Dec 2015). https://doi.org/10.4204/eptcs.198.2, http://dx.doi.org/10.4204/EPTCS.198.2
  * [34] Xie, N., Bi, X., Oliveira, B.C.D.S., Schrijvers, T.: Consistent subtyping for all. ACM Trans. Program. Lang. Syst. 42(1) (Nov 2019). https://doi.org/10.1145/3310339, https://doi-org.gate.lib.buffalo.edu/10.1145/3310339


# Anatomy of ultrafast quantitative magneto-acoustics in freestanding nickel
thin films

Antonia Ghita1 Tudor-Gabriel Mocioi1 Alexey M. Lomonosov2 Jiwan Kim3 Oleksandr
Kovalenko1 Paolo Vavassori4,5 Vasily V. Temnov1<EMAIL_ADDRESS>1LSI,
Ecole Polytechnique, CEA/DRF/IRAMIS, CNRS, Institut Polytechnique de Paris,
F-91128, Palaiseau, France  2B+W Department, Offenburg University of Applied
Sciences, 77652 Offenburg, Germany  3Department of Physics, Kunsan National
University, 54150 Kunsan, Korea  4CIC nanoGUNE BRTA, E-20018 Donostia-San
Sebastian, Spain  5IKERBASQUE, Basque Foundation for Science, E-48013 Bilbao,
Spain

###### Abstract

We revisit the quantitative analysis of the ultrafast magneto-acoustic
experiment in a freestanding nickel thin film by Kim and Bigot Kim and Bigot
(2017) by applying our recently proposed approach of magnetic and acoustic
eigenmodes decomposition by Vernik et al. Vernik  _et al._ (2022). We show
that the application of our modeling to the analysis of time-resolved
reflectivity measurements allows for the determination of amplitudes and
lifetimes of standing perpendicular acoustic phonon resonances with
unprecedented accuracy. The acoustic damping is found to scale as
$\propto\omega^{2}$ for frequencies up to 80 GHz and the peak amplitudes reach
$10^{-3}$. The experimentally measured magnetization dynamics for different
orientations of an external magnetic field agrees well with numerical
solutions of magneto-elastically driven magnon harmonic oscillators. Symmetry-
based selection rules for magnon-phonon interactions predicted by our modeling
approach allow for the unambiguous discrimination between spatially uniform
and non-uniform modes, as confirmed by comparing the resonantly enhanced
magneto-elastic dynamics simultaneously measured on opposite sides of the
film. Moreover, the separation of time scales for (early) rising and (late)
decreasing precession amplitudes provide access to magnetic (Gilbert) and
acoustic damping parameters in a single measurement.

ultrafast magnetization dynamics, magneto-acoustics, exchange magnons,
nanomagnetism

###### pacs:

Valid PACS appear here

##  I Introduction

Since early experimental studies Scherbakov  _et al._ (2010); Kim  _et al._
(2012); Thevenard  _et al._ (2010), ultrafast magneto-elastic interactions
driven by femtosecond light pulses are conveniently described in the time-
domain: the dynamics of magnetization driven by single or multiple acoustic
pulses with picosecond duration are monitored using the magneto-optical pump-
probe technique. This intuitive picture allows for an elegant description of
magnetization precession amplified by a sequence of acoustic pulses with an
appropriate time interval via the magneto-acoustic coherent control mechanism
Kim  _et al._ (2015); Kim and Bigot (2017). Moreover, the time-domain picture
of ultrafast magneto-acoustics facilitates the interpretation of magnetization
switching Kovalenko  _et al._ (2013); Vlasov  _et al._ (2020), where the
duration of acoustic pulses is shorter than the period of ferromagnetic
resonance (FMR) precession.

An alternative view on ultrafast magneto-acoustics is provided in magneto-
optical transient grating experiments Janušonis  _et al._ (2016a, b); Chang
_et al._ (2017, 2018). Here, the spectrally separated quasi-monochromatic
acoustic excitations allow for observing resonant amplification of FMR
precession induced by each acoustic mode. The dependence of FMR frequency on
the external magnetic field makes it possible to tune the FMR precession in
resonance with an acoustic mode of interest. Very recently we have extended
this approach to ultrafast magneto-acoustic dynamics in free-standing thin
films and multilayers Vernik  _et al._ (2022). Our theoretical approach is
based on eigenmodes decomposition of both acoustic and magnetization dynamics,
which allows for a more insightful analysis of ultrafast magneto-acoustic
dynamics experiments in terms of resonant magneto-elastic interactions between
individual modes of longitudinal acoustic phonons and perpendicular standing
spin wave (magnon) modes Van Kampen  _et al._ (2002). For instance, the
application of such rigorous theoretical analysis to resonant phonon-magnon
interactions in freestanding multilayer structures predicts the key role of
the symmetry of magnetic and acoustic modes in prescribing well-defined
selection rules for individual phonon-magnon interactions. One of the most
relevant conclusions was that in symmetric structures interactions between
magnon and phonon eigenmodes with different symmetries were forbidden.

In this paper, with the purpose of bench-marking the power of our improved
approach, we apply it to reinterpreting the experimental results by Kim and
Bigot Kim and Bigot (2017) obtained for a 300 nm freestanding nickel thin
film. We show that even for such thick structures, where frequencies of
spatially uniform (FMR) and non-uniform (spin wave or magnon) modes cannot be
distinguished using conventional approaches employed so far, our approach
enables the detection of their excitation thanks to the symmetry-dependent
selection rules that govern their resonant interaction with acoustic modes.
The results of this work are multiple: from the one side they demonstrate the
ability of our modeling to retrieve fundamental parameters governing the
complex physics involved in ultrafast magneto-acoustic experiments with an
unprecedented accuracy, from the other side corroborate that the physical
picture embodied in our model is particularly insightful, for example by
highlighting the importance of symmetries in magneto-acoustics.

##  II Experiment

Freestanding nickel membranes in the experiment in Ref. Kim and Bigot (2017)
had a thickness $L$=300 nm and were obtained by depositing Ni on a glass
substrate with a layer of sodium chloride in between them. The layer was
subsequently dissolved in water to leave the Ni film stretched on a sample
holder with a hole. The film was stretched laterally by gluing a silver paste
around the edges of the film, which created a static strain in Nickel upon
drying out.

Figure 1:  (a) Schematic picture of the experiment and acoustic pulse
propagating inside the sample. The shaded exponentially decaying functions
illustrate the optical penetration depth of pump and probe pulses,
respectively. (b) Experimental data for reflectivity and Kerr rotation.

The nickel thin film was optically excited at the front side by a femtosecond
pump pulse (400 nm wavelength, 45 fs pulse duration, 10 kHz repetition rate,
1.5 mJ/cm2 fluence), launching pulses of coherent longitudinal acoustic
phonons with a duration of a few picoseconds propagating inside the sample at
a constant speed $c_{s}$=6 nm/ps (see Fig. 1(a)). Due to the inverse
magnetostrictive effect, these acoustic pulses drove the magnetization
dynamics inside the Ni film. Time-delayed probe pulses of
$800\text{\,}\mathrm{nm}$ detected transient changes in the reflectivity and
magneto-optical Kerr effect (MOKE) rotation both at the front and back sides
of the sample. A rotating permanent magnet positioned on top of the sample
produced a magnetic field with reported magnitude
$\mu_{0}H\sim$0.4\text{\,}\mathrm{T}$$ at a variable angle $\xi$ with respect
to the surface normal. Due to the magnetic anisotropy the equilibrium
direction of magnetization was non-collinear with the external magnetic field
and made an angle $\theta$ with the surface normal.

Fig. 1(b) shows the measured differential reflectivity $\frac{\Delta R}{R}$
and Kerr rotation $\psi$ at the back side of the film for five different
orientations of the external magnetic field: $\xi={15.5}^{\circ}$,
${26}^{\circ}$, ${35}^{\circ}$, ${46.5}^{\circ}$ and ${65}^{\circ}$. The
slowly varying thermal background in reflectivity and Kerr rotation signals
originated from heat diffusion from the front to the back side of the film and
will be subtracted throughout the manuscript in order to facilitate the
quantitative comparison with simulations of rapidly varying elastic and
magneto-elastic transients. Complementary Kerr rotation and reflectivity
measurements have been performed at the front side of the film: these data
will be introduced and discussed in Fig. 2(a) for reflectivity and Fig. 4(a)
for Kerr rotation.

##  III Physical model

Excitation of acoustic and magnetic transients in ferromagnetic nickel with
femtosecond laser pulses can be adequately described by the phenomenological
two-temperature model (TTM) Anisimov  _et al._ (1974), which governs the
phenomena of ultrafast demagnetization on a deeply sub-picosecond time scale
Beaurepaire  _et al._ (1996); Güdde  _et al._ (1999) and generation of
ultrashort acoustic pulses on a picosecond time scale Saito  _et al._ (2003).
In the current paper, we are going to disregard the transient ultrafast
demagnetization and focus on the interaction between fs-laser-generated
acoustic pulses and magnetization dynamics. Within the framework of the TTM,
the non-equilibrium hot electrons are initially generated through the
absorption of an optical pump pulse within its skin depth. Subsequently, they
transport energy into the depth of the sample via electron diffusion and heat
up the cold lattice via electron-phonon scattering. These complex spatio-
temporal dynamics result in the emission of picosecond acoustic pulses caused
by the thermal expansion of rapidly heated lattice. In case of a freestanding
nickel film, these acoustic pulses generated at the front side of the sample,
propagate through the film, are reflected at the back Ni/air interface (with a
reflection coefficient equal to -1), and keep bouncing back and forth between
these two interfaces before they decay due to various phonon scattering
mechanisms.

The magnetization dynamics induced by such ultrashort acoustic pulses can be
adequately described by a phenomenological approach using magneto-elastically
driven Landau-Lifshitz-Gilbert (LLG) equations Scherbakov  _et al._ (2010);
Thevenard  _et al._ (2010); Kim  _et al._ (2012). Adapted to the experimental
geometry in Fig. 1, the phenomenological free energy density
$F=F_{Z}+F_{d}+F_{ex}+F_{me}$ takes into account the Zeeman term
$F_{Z}=-\mu_{0}M_{0}{\bf m}\cdot{\bf H}$ due to the presence of the external
magnetic field ${\bf H}$, the anisotropy energy
$F_{d}=\left(\frac{1}{2}\mu_{0}M_{0}^{2}+K\right)m_{z}^{2}$ consisting of the
thin-film shape anisotropy and the phenomenological anisotropy constant $K$
due to static built-in strains in a stretched nickel membrane, the exchange
energy $F_{ex}=\frac{1}{2}M_{0}^{2}\sum_{i=1}^{3}D\left(\frac{\partial\bf
m}{\partial x_{i}}\right)^{2}$ and the magneto-elastic energy
$F_{me}(t)=b_{1}m_{z}^{2}\varepsilon_{zz}(z,t)$ ($b_{1}\simeq 10^{7}$J/m3 for
Nickel Chikazumi and Graham (1997)) due to the interaction with an acoustic
pulse $\varepsilon_{zz}(z,t)$. The relation between the angle $\xi$ of the
magnetic field and $\theta$ magnetization at equilibrium is given by:

$\sin(\theta-\xi)=\frac{\tilde{M}}{2H}\sin 2\theta\,,$ (1)

where $\tilde{M}=M_{0}+\frac{2K}{\mu_{0}M_{0}}$ and $M_{0}$ is the saturation
magnetization for Ni. The length of the magnetization vector stays constant in
our model (assuming constant temperature), so the magnetization dynamics can
be described with the unit magnetization vector ${\bf m}$ and its precession
${\bf s}(z,t)$:

${\bf m}={\bf m}_{0}+{\bf s}(z,t)\,,$ (2)

which can be represented as a sum of magnetic eigenmodes:

${\bf s}(z,t)=\sum_{n=0}^{\infty}{\bf s}^{(n)}(t)\cos\left(k_{n}z\right)\,.$
(3)

where $k_{n}=\pi n/L$ is the wavevector of the $n$-th magnetic eigenmode and
free boundary conditions for magnetization dynamics are assumed. The $n=0$
magnetic eigenmode with uniform spatial profile corresponds to ferromagnetic
resonance (FMR), while higher-order $n\geq 1$ modes describe spatially non-
uniform modes of exchange magnons.

It has been shown Vernik  _et al._ (2022); Besse  _et al._ (2020) that in the
linear approximation when the acoustic strains are small, the magneto-
elastically driven dynamics for each magnon mode satisfy the equation of a
damped driven harmonic oscillator,

$\frac{d^{2}s_{z}^{(n)}}{dt^{2}}+2\alpha\omega_{n}\frac{ds_{z}^{(n)}}{dt}+\omega_{n}^{2}s^{(n)}_{z}=f_{n}(t)\,,$
(4)

where $\alpha$ is the Gilbert damping parameter and magnon eigenfrequencies
$\omega_{n}$ obey

$\omega_{n}=\gamma\mu_{0}\sqrt{\left(H\cos\xi-\left(\tilde{M}-{\tilde{D}}k_{n}^{2}\right)\cos\theta\right)^{2}+\left(H\sin\xi+{\tilde{D}}k_{n}^{2}\sin\theta\right)\left(H\sin\xi+\left(\tilde{M}+{\tilde{D}}k_{n}^{2}\right)\sin\theta\right)}\,.$
(5)

Here ${\tilde{D}}=D/(\hbar\gamma\mu_{0})$ is the exchange stiffness
($D=$430\text{\,}\mathrm{m}\mathrm{e}\mathrm{V}$\text{\AA}^{2}$ from Ref. Van
Kampen  _et al._ (2002)) and $\gamma$ denotes the gyromagnetic ratio.

Figure 2:  (a) Experimentally measured reflectivity at the front side of the
Ni film, superimposed with its fit as a superposition of 10 decaying
sinusoidal eigenmodes. (b) Color map showing the reconstituted strain inside
the film as a function of position and time. (c) Experimental reflectivity
measurement at the back side of the Ni film, together with its fit.

The external magneto-elastic driving force

$f_{n}(t)=P_{n}({\bf
H})\int_{0}^{L}\varepsilon_{zz}(z,t)\cos\left(k_{n}z\right)dz,\ $ (6)

is proportional to the overlap integral between the magnon eigenmode with the
acoustic strain pulse $\varepsilon_{zz}(z,t)$. For our experimental geometry
the prefactor

$P_{n}({\bf
H})=\frac{\mu_{0}\gamma^{2}b_{1}\sin(2\theta)\left(\tilde{D}k_{n}^{2}\sin{\theta}+H\sin{\xi}\right)}{M_{0}L}\,$
(7)

is proportional to the magnetostriction coefficient $b_{1}$ and depends both
on the magnitude and orientation of an external magnetic field $\bf H$.

Understanding the magneto-elastic dynamics governed by Eq. (4) is facilitated
by decomposing the acoustic strain pulse in its eigenmodes according to

$\varepsilon_{zz}(z,t)=\sum_{p=1}^{\infty}\varepsilon_{zz}^{(p)}(z)e^{-\gamma_{p}t}\cos{(\omega_{p}t+\varphi_{p})}\,.$
(8)

We assume acoustic eigenmodes to oscillate at frequencies
$\omega_{p}=c_{s}k_{p}$ and decay with damping constants $\gamma_{p}$;
$\varphi_{p}$ denote their initial phases. In a freestanding film, the
acoustic eigenmodes obey the free boundary conditions for the acoustic
displacement (corresponding to zero strains at both Ni/air interfaces)
resulting in

$\varepsilon_{zz}^{(p)}(z)=a_{p}\sin\left(k_{p}z\right)\,,$ (9)

where $k_{p}=\pi p/L$ is the wavevector of the $p$-th acoustic eigenmode.
Using the decomposition of the acoustic strain in its respective eigenmodes,
the expression of the magneto-elastic driving force becomes

$f_{n}(t)=P_{n}({\bf
H})\sum_{p=1}^{\infty}I_{np}a_{p}e^{-\gamma_{p}t}\cos(\omega_{p}t+\varphi_{p})\,.$
(10)

Here we have introduced the overlap integral

$I_{np}=\int_{0}^{L}\cos\left(k_{n}z\right)\sin\left(k_{p}z\right)dz$ (11)

between the $n$-th magnetic and $p$-th acoustic eigenmodes.

To sum up this section, after having quantified the acoustic strain and
decomposed it in its eigenmodes, we can use equations (4 \- 5) and (10 \- 11)
to simulate the time evolution of the magnetization precession. To solve Eq.
(4) numerically, we use the 4th-order Runge-Kutta method.

##  IV Analysis of acoustic data

Figure 3:  (a) Fourier Transform of the experimental reflectivity and its fit,
for the backside of the film. (b) Damping as a function of frequency, as
extracted from the fitting procedure. The result follows a quadratic law to a
very good approximation. (c) Amplitudes of the acoustic modes, as extracted
from the fitting procedure. The dashed line represents the acoustic frequency
spectrum according to Eq. (5) in Ref. Saito  _et al._ (2003) for Nickel thin
films excited by weak fs-pump pulses. , amplitudes obtained with Eq. (15)
assuming exponential heating profiles with $h$=20 nm and 60 nm are shown for
comparison (continuous lines).

.

The change in reflectivity measured by the probe pulse after excitation with
the pump pulse is related to the strain inside the film through the
sensitivity function $f(z)$, which depends on the optical constants of Ni.
Their relation (as in Thomsen  _et al._ (1986)) is given by

$\frac{\Delta R(t)}{R}=2\text{Re}\Big{(}\frac{\Delta
r(t)}{r}\Big{)}=\int_{0}^{L}\varepsilon_{zz}(z,t)f(z)\mathrm{d}z\,,$ (12)

where we used the expression for the sensitivity function in the complex
notation Saito  _et al._ (2003):

$f(z)=\frac{16\pi}{\lambda}\text{Re}\left(i\frac{\partial\tilde{n}}{\partial\varepsilon_{zz}}\frac{\tilde{n}}{\tilde{n}^{2}-1}e^{i\frac{4\pi\tilde{n}}{\lambda}z}\right)\,.$
(13)

Here $\tilde{n}=2.48+4.38i$ denotes the complex index of refraction of Ni at
the probe wavelength $\lambda=$800\text{\,}\mathrm{nm}$$ and its derivative
with respect to the applied strain
$\frac{\partial\tilde{n}}{\partial\varepsilon_{zz}}=0.6-1.8i$ Saito  _et al._
(2003) is called the photo-elastic coefficient. The spatial dependence of the
sensitivity function is dominated by the exponential decay $\propto{\rm
exp}(-z/\delta_{skin})$ within the optical penetration depth of the probe
pulse
$\delta_{skin}=\frac{\lambda}{4\pi\text{Im}(\tilde{n})}=$14.5\text{\,}\mathrm{nm}$$.

Using the previous decomposition of strain into eigenmodes, we obtain the
following expression for the measured reflectivity

$\frac{\Delta
R(t)}{R}=\sum_{p=1}^{\infty}a_{p}J_{p}e^{-\gamma_{p}t}\cos{(\omega_{p}t+\varphi_{p})}\,,$
(14)

where we can interpret $J_{p}=\int_{0}^{L}f(z)\sin(k_{p}z)\mathrm{d}z\,$ as
the detection integral of the $p$-th mode. This expression for the transient
reflectivity shows that it can be represented as a sum of damped harmonic
oscillations, suggesting that the Fourier transform of the signal could be
useful in characterizing the acoustic eigenmodes. Panels (a) and (c) in Fig. 2
show the reflectivity signal at the front and back side of the film, while
Fig. 3(a) displays the Fourier transform of the backside reflectivity signal.
The data allows us to distinguish ten peaks in the Fourier transform, so we
carry out the analysis using the first ten acoustic modes.

To obtain the amplitudes, lifetimes, and phases of the respective acoustic
modes, we performed a non-linear least squares fitting (using the Levenberg-
Marquardt algorithm) of the reflectivity data at the back side with Eq. (14),
where $a_{p}$, $\gamma_{p}$, and $\varphi_{p}$ are taken as fit parameters and
frequencies $\omega_{p}$ are extracted from the Fourier spectrum. As an
initial guess for the amplitudes $a_{p}$, we used the integrated intensity of
each peak, and for damping constants $\gamma_{p}$ \- the width of spectral
lines from the Fourier spectrum. It is important to choose a rather precise
initial guess for amplitudes and damping constants as the algorithm is highly
sensitive to them. The results of such fitting in Fig. 2(a,c) and Fig. 3(a)
appear to be in an excellent agreement with experimental data.

Furthermore, panels (b) and (c) in Fig. 3 show the dependence of damping and
amplitudes for the first eight eigenmodes on their frequencies. The second-
degree polynomial fit of damping $\gamma_{p}$ as a function of frequency shows
that the quadratic term dominates. Thus, we can conclude that damping scales
quadratically with frequency up to around $80\text{\,}\mathrm{GHz}$. This
result is consistent with Ref. Zhu  _et al._ (1991), suggesting that the
attenuation mechanism is due to the phonon-phonon scattering.

The straightforward attempt to understand the fitted amplitudes (Fig. 3(c))
within the framework of the TTM failed. Using Eq. (5) and the set of
experimental fit parameters in the low-fluence excitation regime (pump fluence
$\sim$0.01 mJ/cm2) in Nickel thin films Saito  _et al._ (2003) results in the
initial heat penetration depth $h$=20 nm that only slightly exceeds the
optical skin depth of our pump pulses. In terms of the acoustic amplitudes the
results of the TTM are well-approximated by a simplified phenomenological
model assuming an instantaneous heating with an exponential profile
$\propto\exp(-z/h)$ giving rise to

$a_{p}\propto\int_{0}^{L}e^{-z/h}\sin\left(k_{p}z\right)dz\,,$ (15)

The strong disagreement between the theory and the experimental data indicates
that this modeling cannot be applied. In the strong-excitation regime used in
this experiment the parameters of the two-temperature model display strong
dependence on the pump fluence Lin  _et al._ (2008) resulting in larger
electronic heat capacity and weaker electron-phonon coupling. Both effects
favor a larger heat penetration depth mediated by hot electron diffusion
during the increase electron-phonon relaxation time. We can account for this
effect by assuming a larger heat penetration depth $h$=60 nm, which provides a
better approximation to the experimental data. However, it is clear that the
discussed theoretical models represent oversimplifications and a further
systematic study of the strong excitation regime of picosecond acoustic pulses
is necessary.

Using the obtained amplitudes, phases, and damping parameters, we can
reconstruct the strain inside the film as a function of space and time. Figure
2(b) shows an evolution of spatial strain that is in accordance with the
intuitive image of an acoustic echo propagating back and forth, undergoing
reflections at both ends of the film and damping in time. But, in addition to
this intuitive picture, the eigenmode decomposition also helps explaining the
broadening of acoustic echo in time domain, which is due to the frequency-
dependent damping.

##  V Analysis of magnetization dynamics

Figure 4:  Comparison of magnetization dynamics at the front and back side of
the film, as obtained (a) experimentally and (b) from our simulations.

Magnetization dynamics in the Ni film are analyzed by measuring the Kerr
rotation angle. The depth sensitivity function of MOKE becomes important in
case of ultrafast magnetization dynamics, varying within the skin depth of
light due to the presence of spatially non-uniform high-frequency magnons. The
relation between the detected Kerr rotation and the magnetization precession
$s_{z}(z,t)$ inside the film is given by

$\frac{\Delta\psi(t)}{\psi_{s}}=\int_{0}^{L}s_{z}(z,t)g(z)dz$ (16)

where $\psi_{s}$ is the static Kerr rotation angle, $\Delta\psi(t)$ is its
change due to magnetization precession, and $g(z)$ is the depth sensitivity
function for the polar MOKE Traeger  _et al._ (1992):

$g(z)=\frac{4\pi}{\lambda}\text{Re}\Big{(}iQ_{MO}\frac{\tilde{n}^{2}}{1+\tilde{n}^{2}}e^{-i\frac{4\pi\tilde{n}}{\lambda}z}\Big{)}.$
(17)

Here, unlike the acoustical sensitivity function, the magneto-optical response
is valued by the complex magneto-optical (Voigt) constant
$Q_{MO}=i\frac{\tilde{\epsilon}_{xy}}{\tilde{\epsilon}_{xx}}=-(4.9+10.5i)\times
10^{-3}$ Krinchik and Artemjev (1968).

Using our previous decomposition in magnon eigenmodes, we get an expression
that ties the dynamics of individual magnon modes to the Kerr rotation:

$\frac{\Delta\psi(t)}{\psi_{s}}=\sum_{n=0}^{\infty}\tilde{J_{n}}s_{z}^{(n)}(t)\,,$
(18)

where $\tilde{J_{n}}=\int_{z=0}^{L}g(z)\cos\left(k_{n}z\right)dz$ is the
detection integral of the $n$-th magnon mode. Using this expression, we can
fit the results of our magnetization dynamics simulation with those of the
experiment in the next section.

##  VI Resonant phonon-magnon interactions

The experimental data for the back- and front side- Kerr rotation are
presented in Fig. 4(a) for different orientations of the external magnetic
field. We simulate the Kerr rotation by solving Eq. (4) for each magnon and
using the sensitivity function defined in the previous section to obtain the
Kerr rotation from Eq. (18). In order to reach an agreement with experimental
data for all angles $\xi$ in Fig. 4, we have used the values for the
anisotropy constant $K$, magnitude of the magnetic field $H$ and Gilbert
damping $\alpha$ as fit parameters. Using the magnetic field of
$0.3\text{\,}\mathrm{T}$, the anisotropy constant $K=2.05\cdot
10^{5}\text{J/m}^{3}$ and the Gilbert damping $\alpha=0.04$, we achieve the
quantitative agreement between the experimental data and simulations (Fig. 4).
The value of the magnetic field stays within the expected error bar for a
permanent magnet placed on top of the sample. The value of the Gilbert damping
is equal to the one obtained in a recent study of ultrafast magnetization
dynamics in nickel nanomagnets Berk  _et al._ (2019). The simulated Kerr
rotation at the front and back sides are represented in Fig. 4(a,b). We
observe an excellent agreement between the experimental data and simulations,
except for the initial thermal excitation of magnetization at the front side,
which we did not account for in our model.

Given this agreement between experimental data and simulations, we analyze the
peculiarities of the magnetization dynamics at different angles. For $15.5$ ∘,
the magnetization dynamics at the back side is in-phase with that at the
front-side, while for $65$ ∘ they are $\pi$-shifted. Moreover, we notice that
the magnetization precession at $15.5$ and $65$ ∘ lasts longer and is stronger
than at other angles. While at $15.5$ ∘ and $65$ ∘ there are some slowly
varying long-lived dynamics, at angles $26$, $35$, and $46.5$ ∘ we observe
weak, somewhat irregular beating patterns.

Figure 5: (a) Fourier transform of simulated Kerr rotation as a function of
magnetic field angle. The dashed lines indicate the frequencies of phonons and
the continuous white lines are the dispersion curves of magnons. Vertical
cross-sections into the heat map, corresponding to the three angles in panel
b, are shown. (b) Magnetization dynamics inside the film, as a function of
position and time, for three experimental angles. (c) Magnetization profiles,
taken at the times indicated in panel (b) by dashed lines. Figure 6:
Representation of magnonic eigenmodes (along the horizontal axis) and acoustic
eigenmodes (along the axis), with their corresponding overlap integrals.

A complementary perspective is presented in Fig. 5 which show the
reconstructed magnetization dymnamics inside the sample (Fig. 5(b-c)) as a
function of position and time. After the transient regime dies out, the
magnetization profile for $15.5$ ∘ is approximately uniform in space,
suggesting that the dynamics is dominated by the FMR ($n=0$) mode. On the
other hand, the dynamics at $65$ ∘ follow the spatially antisymmetric profile
with respect to the middle of the film, which suggests that in this
configuration the $n=1$ magnon dominates. This conclusion is inline with the
observed $\pi$-phase shift between the data at the front and the backside at
$65$ ∘, see Fig. 4. At an intermediate angle of $35$ ∘, the magnetization
dynamics with a much smaller amplitude are mainly visible at early delays
times. This suggests that in this intermediate regime no magnon modes are
resonantly excited.

All these observations can be explained by a simple theory for a driven
harmonic oscillator. The main result is that the oscillation amplitude is
resonantly enhanced when the natural frequency (here, that of magnons
$\omega_{n}$) equals the driving frequency (in our case, that of phonons
$\omega_{p}$). Away from resonance, the transient regime is characterized by a
beating pattern because of the difference between the natural and driving
frequencies.

Figure 5(a) shows the amplitude of magnetization precession as a function of
its frequency and the angle of the external magnetic field. Two bright spots
are visible: one at the point where the frequency of the first phonon ($p=1$)
matches that of FMR ($n=0$) and another one where the frequency of the second
phonon ($p=2$) matches that of the first magnon ($n=1$).

However, for our symmetric freestanding membrane the overlap integral $I_{np}$
(Fig. 6) is zero when the acoustic modes possess a different symmetry from
that of the magnon modes. This means that symmetric (antisymmetric) acoustic
modes will interact only with symmetric (antisymmetric) magnon modes,
respectively. Therefore, the symmetry-based selection rules become as
important for resonant phonon-magnon interaction as the previously mentionned
frequency matching condition.

These considerations enable us to identify the driving forces of the
magnetization dynamics observed at the three angles shown in Fig. 5. At
$15.5^{\circ}$, the frequency of the first phonon ($p=1$) matches that of the
first few magnons but the symmetry of the modes allows only even magnons to be
excited. Since the overlap integral decays with increasing magnon number, the
dominant magnetic mode at $15^{\circ}$ is the FMR ($n=0$). At $65^{\circ}$,
the second phonon ($p=2$), whose frequency matches the frequencies of the
first few magnons, interacts only with odd magnons. Thus, the dominant mode in
this case is the first magnon ($n=1$). At $35^{\circ}$, the magnon frequencies
are between the frequency of the first ($p=1$) and second ($p=2$) phonon and
exhibit no resonant interaction. Hence, the magnetization precession is
significantly weaker.

Figure 7 illustrates the quantitative agreement between theory and experiment
for the two resonantly driven magnetization dynamics. There are two timescales
involved in such phonon-magnon interactions: excitation (the transient regime)
and decay (the driven regime). When the driving frequency is equal to the
eigenfrequency, the response in the transient regime follows
$(1-e^{-t/\tau_{exc}})\cos{\omega_{p}t}$, where $\omega_{p}$ is the frequency
of the acoustic driving mode and $\tau_{exc}$ is a characteristic relaxation
time of magnetization dynamics, which is related to Gilbert damping as
$\tau_{exc}=(\alpha\omega_{n})^{-1}$, where $\omega_{n}$ is the frequency of
the dominant magnon. On the other hand, the decay of magnetization is a driven
regime when magnetization dynamics follow the acoustic driving force as
$\propto e^{-t/\tau_{decay}}\cos{(\omega_{p}t)}$, where
$\tau_{decay}=1/\gamma_{p}$ is the acoustic mode lifetime. Thus, to a good
approximation, the overall magnetization dynamics fit inside an envelope of
the form

$A(t)\propto(1-e^{-t/\tau_{exc}})e^{-t/\tau_{decay}}\,.$ (19)

We can assign these characteristic relaxation times to the corresponding
acoustic and magnetic eigenmodes, respectively, as shown in Fig. 7. For the
magnetization dynamics at $15.5^{\circ}$, the characteristic time of the
excitation phase is $\tau_{exc}^{(1)}=$0.45\text{\,}\mathrm{ns}$$ and the
decay time is $\tau_{decay}^{(1)}=$1.2\text{\,}\mathrm{ns}$$. We can see a
clear correlation between these two times and the corresponding lifetimes of
the acoustic and magnetic eigenmodes,
$\frac{1}{\gamma_{G}^{(0)}}=$0.44\text{\,}\mathrm{ns}$$ and
$\frac{1}{\gamma_{ac}^{(1)}}=$1.19\text{\,}\mathrm{ns}$$. Similarly, for the
case of magnetization dynamics at $65^{\circ}$, we extract the excitation time
$\tau_{exc}^{(2)}=$0.23\text{\,}\mathrm{ns}$$ and a value of the decay time
$\tau_{decay}^{(2)}=$0.57\text{\,}\mathrm{ns}$$. Again, this value is
consistent with the lifetimes of the first magnon mode
$\frac{1}{\gamma_{G}^{(1)}}=$0.22\text{\,}\mathrm{ns}$$ and of the second
acoustic eigenmode, $\frac{1}{\gamma_{ac}^{(2)}}=$0.56\text{\,}\mathrm{ns}$$.

Figure 7: Long-scan magnetization dynamics at the backside of the film, under
the magnetic field angles (a) $\xi=15.5^{\circ}$ and (b) $\xi=65^{\circ}$.
Experimental data is represented by dots, the simulated curve is a black
continuous line, while the dashed curve denotes the fit envelope $A(t)$. The
separation of timescales is clearly visible in both graphs: the initial growth
governed by the Gilbert damping is followed by the decay due to the acoustic
decay.

This model also allows for extracting quality factors of magnons and phonon
resonances. The magnon quality factor of $Q_{G}=13\simeq 1/(2\alpha)$ does not
depend on the mode number, in agreement with previously reported results on
frequency-independent Gilbert damping $\alpha$ Razdolski  _et al._ (2017);
Salikhov  _et al._ (2019). Acoustic quality factors $Q_{ac}^{(1)}=37$ and
$Q_{ac}^{(2)}=29$ are slightly different due to the observed nonlinear
dependence of acoustic damping on frequency, converging to the approximate
scaling $Q_{ac}(\omega)\propto\omega^{-1}$ for higher-order acoustic modes.
The observed high values of acoustic quality factors $Q_{ac}>Q_{G}$ enable the
separation of time- scales in the excitation and decay phases in the
magnetization dynamics.

Qualitatively similar magnetization dynamics have been observed earlier in
transient grating experiments Janušonis  _et al._ (2016a). However, in the
latter case the conspicuous decay of magnetization dynamics was explained by
the complex spatio-temporal dynamics of the magnitude of the magnetization
vector $M_{z}(x,t)$ on the temperature $T(x,t)$ in the periodically
demagnetized nickel film Janušonis  _et al._ (2016b); Chang  _et al._ (2018).
In this context, our experimental geometry provides an advantage of isolating
resonant phonon-magnon interactions from thermal effects and extracting their
properties from the same measurement.

##  VII Summary and conclusions

In this manuscript, we reported on the quantitative analysis of experimental
data by Kim and Bigot in a free-standing nickel thin film Kim and Bigot (2017)
based on the decomposition of magnetic and acoustic dynamics in phonon and
magnon eigenmodes, respectively. The time-domain fitting of transient
reflectivity data on both sides of the nickel film provides frequencies,
lifetimes and phases of individual acoustic eigenmodes. The latter is shown to
drive the magnetization dynamics, to be in quantitative agreement with time-
resolved MOKE measurements. Notably, the comparison of MOKE signals on both
sides of the sample evidence the in-phase FMR dynamics ($n=0$, with minor
contributions of symmetric magnon eigenmodes $n=2,4,...$) induced by the
lowest order (p=1) symmetric acoustic mode and the opposite-sign magnetization
oscillation of antisymmetric magnon modes ($n=1,3,...$). Being in a
quantitative agreement with a simple theoretical model with tabulated material
parameters, the experimental data clearly evidence the resonantly enhanced
excitation of nonuniform magnon modes. Moreover, accurate fitting of the
magnetization dynamics driven by long-lived $p=1$ (9.8 GHz) and $p=2$ (19.1
GHz) acoustic modes delivers the correct value for magnetic Gilbert damping
$\alpha=0.04$, corresponding to the quality factor $Q_{m}=13$ for magnon
modes. Being smaller than the quality factors of acoustic modes, this magnetic
quality factor assures optimum conditions for resonant phonon-magnon
excitation, the phenomenon to be further explored in the ultrahigh THz-
frequency regime Vernik  _et al._ (2022); Kimel  _et al._ (2022).

###### Acknowledgements.

This article is dedicated to the memory of Jean-Yves Bigot, in whose labs the
reported measurements have been performed. The support of the Physics
Department of École Polytechnique and Institut Polytechnique de Paris within
the framework of a Projet de Recherche en Laboratoire and by the
ANR-21-MRS1-0015-01 ”IRON-MAG” is gratefully acknowledged. P.V. acknowledges
support from the Spanish Ministry of Science and Innovation and the European
Union under the Maria de Maeztu Units of Excellence Programme
(CEX2020-001038-M) and the project PID2021-123943NB-I00 (MICINN/FEDER). J.K.
acknowledges support from Basic Science Research Program through the National
Research Foundation of Korea (NRF) funded by the Ministry of Education
(2022R1I1A3072023) and by the MSIT (2021R1A4A1031920).

## References

  * Kim and Bigot (2017) J.-W. Kim and J.-Y. Bigot, Phys. Rev. B 95, 144422 (2017).
  * Vernik  _et al._ (2022) U. Vernik, A. M. Lomonosov, V. S. Vlasov, L. N. Kotov, D. A. Kuzmin, I. V. Bychkov, P. Vavassori, and V. V. Temnov, Physical Review B 106, 144420 (2022).
  * Scherbakov  _et al._ (2010) A. V. Scherbakov, A. S. Salasyuk, A. V. Akimov, X. Liu, M. Bombeck, C. Brüggemann, D. R. Yakovlev, V. F. Sapega, J. K. Furdyna, and M. Bayer, Phys. Rev. Lett. 105, 117204 (2010).
  * Kim  _et al._ (2012) J.-W. Kim, M. Vomir, and J.-Y. Bigot, Phys. Rev. Lett. 109, 166601 (2012).
  * Thevenard  _et al._ (2010) L. Thevenard, E. Peronne, C. Gourdon, C. Testelin, M. Cubukcu, E. Charron, S. Vincent, A. Lemaître, and B. Perrin, Phys. Rev. B 82, 104422 (2010).
  * Kim  _et al._ (2015) J.-W. Kim, M. Vomir, and J.-Y. Bigot, Scientific reports 5, 8511 (2015).
  * Kovalenko  _et al._ (2013) O. Kovalenko, T. Pezeril, and V. V. Temnov, Phys. Rev. Lett. 110, 266602 (2013).
  * Vlasov  _et al._ (2020) V. S. Vlasov, A. M. Lomonosov, A. V. Golov, L. N. Kotov, V. Besse, A. Alekhin, D. A. Kuzmin, I. V. Bychkov, and V. V. Temnov, Phys. Rev. B 101, 024425 (2020).
  * Janušonis  _et al._ (2016a) J. Janušonis, C. L. Chang, T. Jansma, A. Gatilova, V. S. Vlasov, A. M. Lomonosov, V. V. Temnov, and R. I. Tobey, Phys. Rev. B 94, 024415 (2016a).
  * Janušonis  _et al._ (2016b) J. Janušonis, T. Jansma, C. L. Chang, L. Q., A. Gatilova, A. M. Lomonosov, V. Shalagatskyi, T. Pezeril, V. V. Temnov, and R. I. Tobey, Scientific Reports 6, 29143 (2016b).
  * Chang  _et al._ (2017) C. L. Chang, A. M. Lomonosov, J. Janusonis, V. S. Vlasov, V. V. Temnov, and R. I. Tobey, Phys. Rev. B 95, 060409(R) (2017).
  * Chang  _et al._ (2018) C. L. Chang, S. Mieszczak, M. Zelent, V. Besse, U. Martens, R. R. Tamming, J. Janusonis, P. Graczyk, M. Münzenberg, J. W. Kłos, _et al._ , Physical Review Applied 10, 064051 (2018).
  * Van Kampen  _et al._ (2002) M. Van Kampen, C. Jozsa, J. Kohlhepp, P. LeClair, L. Lagae, W. De Jonge, and B. Koopmans, Phys. Rev. Lett. 88, 227201 (2002).
  * Anisimov  _et al._ (1974) S. Anisimov, B. Kapeliovich, T. Perelman, _et al._ , Zh. Eksp. Teor. Fiz 66, 375 (1974).
  * Beaurepaire  _et al._ (1996) E. Beaurepaire, J.-C. Merle, A. Daunois, and J.-Y. Bigot, Phys. Rev. Lett. 76, 4250 (1996).
  * Güdde  _et al._ (1999) J. Güdde, U. Conrad, V. Jähnke, J. Hohlfeld, and E. Matthias, Physical Review B 59, R6608 (1999).
  * Saito  _et al._ (2003) T. Saito, O. Matsuda, and O. Wright, Physical Review B 67, 205421 (2003).
  * Chikazumi and Graham (1997) S. Chikazumi and C. D. Graham,  _Physics of ferromagnetism_ , 94 (Oxford university press, 1997).
  * Besse  _et al._ (2020) V. Besse, A. V. Golov, V. S. Vlasov, A. Alekhin, D. Kuzmin, I. V. Bychkov, L. N. Kotov, and V. V. Temnov, J. Magn. Magn. Mater. 502, 166320 (2020).
  * Thomsen  _et al._ (1986) C. Thomsen, H. T. Grahn, H. J. Maris, and J. Tauc, Phys. Rev. B 34, 4129 (1986).
  * Zhu  _et al._ (1991) T. C. Zhu, H. J. Maris, and J. Tauc, Phys. Rev. B 44, 4281 (1991).
  * Lin  _et al._ (2008) Z. Lin, L. V. Zhigilei, and V. Celli, Physical Review B 77, 075133 (2008).
  * Traeger  _et al._ (1992) G. Traeger, L. Wenzel, and A. Hubert, physica status solidi (a) 131, 201 (1992).
  * Krinchik and Artemjev (1968) G. S. Krinchik and V. A. Artemjev, Journal of Applied Physics 39, 1276 (1968), https://doi.org/10.1063/1.1656263 .
  * Berk  _et al._ (2019) C. Berk, M. Jaris, W. Yang, S. Dhuey, S. Cabrini, and H. Schmidt, Nature communications 10, 1 (2019).
  * Razdolski  _et al._ (2017) I. Razdolski, A. Alekhin, N. Ilin, J. P. Meyburg, V. Roddatis, D. Diesing, U. Bovensiepen, and A. Melnikov, Nature communications 8, 15007 (2017).
  * Salikhov  _et al._ (2019) R. Salikhov, A. Alekhin, T. Parpiiev, T. Pezeril, D. Makarov, R. Abrudan, R. Meckenstock, F. Radu, M. Farle, H. Zabel, and V. V. Temnov, Phys. Rev. B 99, 104412 (2019).
  * Kimel  _et al._ (2022) A. Kimel, A. Zvezdin, S. Sharma, S. Shallcross, N. De Sousa, A. García-Martín, G. Salvan, J. Hamrle, O. Stejskal, J. McCord, _et al._ , Journal of Physics D: Applied Physics 55, 463003 (2022).