From 50f626ab2dc6e4b6ae6755969c7213b28456fe7d Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 1 Dec 2018 18:36:22 -0800 Subject: [PATCH 01/36] Add back draft langref from before --- docs/langref/relay/expressions.rst | 162 +++++++++++++++++++++++++ docs/langref/relay/index.rst | 16 +++ docs/langref/relay/intro.rst | 182 +++++++++++++++++++++++++++++ docs/langref/relay/type_system.rst | 157 +++++++++++++++++++++++++ 4 files changed, 517 insertions(+) create mode 100644 docs/langref/relay/expressions.rst create mode 100644 docs/langref/relay/index.rst create mode 100644 docs/langref/relay/intro.rst create mode 100644 docs/langref/relay/type_system.rst diff --git a/docs/langref/relay/expressions.rst b/docs/langref/relay/expressions.rst new file mode 100644 index 000000000000..f9644d30d7ff --- /dev/null +++ b/docs/langref/relay/expressions.rst @@ -0,0 +1,162 @@ +=========== +Expressions +=========== + +The Relay IR is a pure, expression-oriented language with distinct dataflow +and control flow language fragments. Although Relay uses abstract syntax trees to represent programs, +the dataflow fragments of a program can be considered as a graph when writing and expressing transformations. + +The below sections make an attempt to clearly split the expressions that +are pure dataflow (equivalent to traditional computation graphs) from +the extended expressions that contain control flow. + +================= +Dataflow Fragment +================= + +First we will cover the set of expressions which do not involve control flow; +this fragment of the language is semantically equivalent to pure computation graphs +without control flow. + +Constants +~~~~~~~~~ + +Relay programs can contain constant tensor values. This node represents +a constant tensor value (see :py:mod:~tvm.relay.Value for more details). +The constants are represented as :py:class:`~tvm.NDArray`, allowing us to utilize +TVM operators for constant evaluation. + +See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation. + +Tuple +~~~~~ + +The tuple node builds a finite (that is, of statically known size) sequence of heterogeneous data. +These tuples match Python's closely. Their fixed length allows for efficient projection of their +members. + +.. code-block:: python + + (a, b, c) : Tuple + + (a + b + c, d) : Tuple, Tensor> + +See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. + +Function +~~~~~~~~ + +A function node represents a function; it contains a sequence of +parameters, a return type, and a body. + +.. code-block:: python + + fun (x : Float, y: Float) -> Float { x + y } + +Functions are first-class in Relay and can be used in any expression +position. Function expressions are the same as global functions, but do not +have a globally unique name. You can use a function in conjunction with a let +binding to define locally recursive functions. + +.. code-block:: python + + let fact = fun (x : Float) -> Float { + if (x == 0) { + 0 + } else { + x * fact(x - 1) + } + }; + fact(10) + +See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. + +Variables +~~~~~~~~~ + +Both global variables and local variables are valid expressions; one may use them +anywhere an expression may appear. + +For example, the below fragment of code is a valid expression. + +.. code-block:: python + %ret = @global(op_name, %local) + +See :py:class:`~tvm.relay.expr.LocalVar` and :py:class:`~tvm.expr.GlobalVar` for its definition +and documentation. + +Let Binding +~~~~~~~~~~~ + +A let binding is an immutable variable binding, allowing the user +to bind an expression to a name. A let binding contains a local variable, +an optional type annotation, a value, and a body expression +that may reference the bound identifier. + +We will first introduce a single binding without +type annotations: + +.. code-block:: python + let %x = %a + %b; + x + +The value of a let binding is the value of the final expression +after evaluating the bindings it depends on. + +A sequence of let bindings can be considered as a dataflow graph, +where the bindings are a series of sub-graphs connected +by bound variables. Since these binding sequences are +pure, we can evaluate them in any order according to the program +dataflow. + +For example the below Relay program is equivalent to the +below NNVM program. + +.. code-block:: python + let %y_pred = %x * %w + %b; + let %loss = pow(%y - %y_pred, 2); + ret %loss + +.. code-block:: python + TODO + +See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. + +======================= +Control Flow Expression +======================= + +Control flow expressions enable network topology to change based +based on the value of previously executed expressions. + +Call +~~~~ + +Expressions with function types in Relay are "callable," meaning that they can be +invoked via a function call. + +All Relay functions are typed with function types, as are all Relay operators. + +For example, we can call the previously defined `fact` because it has a function +type: + +.. code-block:: python + fact(10) + +See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. + +If-Then-Else +~~~~~~~~~~~~ + +Relay has a simple if-then-else expression that allows programs to branch +on a single value of type :code:`bool`, i.e., a zero-rank +tensor of booleans (:code:`Tensor[(), bool]`). + +.. code-block:: python + if (sum(equal(t, u))) { + return x: + } else { + return y; + } + +See :py:class:`~tvm.relay.expr.If` for its definition and documentation. diff --git a/docs/langref/relay/index.rst b/docs/langref/relay/index.rst new file mode 100644 index 000000000000..1b05697cbb03 --- /dev/null +++ b/docs/langref/relay/index.rst @@ -0,0 +1,16 @@ +Relay Language Reference +======================== + +This document is a work in progress language reference describing +Relay, TVM's high-level intermediate representation. The name is an +allusion to interneurons, which are often referred to as intermediate +or relay neurons. + +As we evolve the new IR, we will update this document accordingly. + +.. toctree:: + :maxdepth: 2 + + intro + expressions + type_system diff --git a/docs/langref/relay/intro.rst b/docs/langref/relay/intro.rst new file mode 100644 index 000000000000..9f5a9cab4b2c --- /dev/null +++ b/docs/langref/relay/intro.rst @@ -0,0 +1,182 @@ +============ +Introduction +============ + +Relay is a differentiable programming language with support for +closures, control flow, and recursion. It has an advanced +static type system specifically designed for programs written +by machine learning practitioners and researchers. Relay is intended to replace +the computation graph-based intermediate representations currently employed by deep +learning frameworks and compilers. + +The deep learning community has organically evolved a representation of machine learning +models that was useful for the form of computation originally desired, i.e., a directed +acyclic graph of primitive functions. Computation graphs also serve a dual purpose as both a +compile-time and run-time data structure. While computation graphs are a good fit +for models with a static topology, they make it tricky to incorporate control flow and +abstraction. Additionally, the conflation of the description of a computation, the +representation used for optimizing it, and the data structure used to execute it unnecessarily +hamper the goals of machine learning frameworks. We believe having a high-level, expressive language +designed for writing compiler optimizations is essential to the future of an end-to-end +deep learning compiler stack. + +Relay's design is influenced by the authors' experience building advanced optimizing compilers +for high-level languages, as well as by challenges presented by the current version of the +TVM stack, and NNVM's IR. We address a few important challenges with Relay's design. +Relay is an IR with closures, control-flow, recursion, and an advanced type system supporting +complex shape relationships and symbolic dimensions. We define a series of +automatic differentiation rules over the language, with the goal of enabling higher-order +differentiation of programs with control flow and closures. + +================== +Language +================== + +Relay is a purely functional, differentiable intermediate representation. + +================== +IR Reference +================== + +The IR has a global environment that stores the set of definitions, +constants, options, and attributes, and provides access to features +including type inferecnce, constant evaluation, and more. + +~~~~~~~~~~ +Relay Node +~~~~~~~~~~ + +The fundamental unit of the IR is the node, which only contains a Span. + +.. code-block:: python + + class Node: + span: Span + +================== +Variables +================== + +Relay has two notions of variables: local and global. +Our design draws inspiration from LLVM, which differentiates between identifier types. +This enables writers of optimizations to know precisely what an identifier references without needing +information beyond the kind of identifier. + +Globals are written with `@`, locals are written with `%`, and variables written without a +sigil name the corresponding operator. The distinction between global and local identifiers +makes certain kinds of transformation easier. For example, inlining a global definition +requires no analysis, as you can write a pass that directly inlines the definitions. +Ensuring there is no spooky action at a distance; introducing a new identifier return +type is omitted we will infer the return type based on the text of the program. + + +Global Variable +~~~~~~~~~~~~~~~~~~ + +Global identifiers are prefixed by the `@` sigil. A global identifier always +references a globally visibly definition contained in the environment. You +can write a global identifier as `@global`. + +Local Variable +~~~~~~~~~~~~~~~~~ + +Local identifiers are prefixed by the :code:`%` sigil. A local identifier always +references a parameter, or let bound expression. You can write a local +identifier as :code:`%local`. + + +================ +Global Functions +================ + +A function definition consists of a name, parameters, type parameters, and an optional return +type. A global function is no different from a procedure or function in a typical programming +language and generalizes the concept of a named subgraph. + +A definition minimally consists of an identifier :code:`@id`, an empty set of +parameters, and a body expression contained by curly braces. + +.. code-block:: python + + def @id() { body } + +A definition may also contain any number of parameters. For example, a +simple function which just adds two tensors: + +.. code-block:: python + + def @add(%x, %y) { %x + %y } + +It is also possible for us to annotate explicit types on definitions. For example, +we can restrict the above definition to only work on certain types: + +.. code-block:: python + + def @add(%x: Tensor, %y: Tensor) -> Tensor { + %x + %y + } + +A parameter is just a pairing of a :py:class:`~tvm.relay.expr.LocalVar` and optional :py:class:`~tvm.relay.ty.Type`. They represent +the formal parameters of functions and definitions, and are written as :code:`%x : T`. + +Parameters may only appear in function literals and definitions and have no relation +to parameters in the machine learning. + +When the type information is omitted, we will attempt to infer the most general type +for the users. This property is known as generalization: for a definition without +explicit annotations, we will attempt to assign the most general type. When the +return type is omitted, we will infer the return type based on the text of the +program. + +Finally, we can directly construct type-polymorphic definitions by writing down +a set of type parameters for a definition. For example, one can definte a +polymorphic identity function for tensors as follows: +:: + def @id(%x: Tensor) { + %x + } + +Notice we can omit the return type and it will still be inferred. + +.. *Note: this is not yet implemented.* + +.. Finally we allow a definition be prefixed by metadata, which adds +extra properties to the definition. + +.. It is important to be able to annotate metadata that is external to +the computational behavior of a definition. For example, we can use +this to add an `inline` or `noinline` attribute that the compiler +can consider when performing inlining. + +.. For example we can set the attributes for :code:`@id_real`.:: + + +.. attributes id_real { + inline: true + } + +.. def id_real(%x:Real) { ret %x } + + +========= +Operators +========= + +An operator is a primitive operation that is not defined in the Relay language but is provided +externally. Currently we back these operator's registrations with the operators +exposed by TVM's TOPI. An operator requires a user to provide an implementation +of the operator, its type, and various required attributes. + +The input methods for Relay programs do not provide a way to describe operators in +Relay; they must be explicitly registered in the global environment via Python or C++. +Operators are rendered without a sigil (e.g :code:`add`, :code:`subtract`) when pretty- +printing Relay programs. Operators are explicitly contained in the program and are uniquely +identifiable by pointer during a run of the Relay compiler. + +Programs +~~~~~~~~ + +Now that we have presented both global functions and operators, we have +everything in hand to describe a complete Relay program. A Relay program consists of a +registry of operators, one or more functions, as well as the global configuration +stored in the environment. diff --git a/docs/langref/relay/type_system.rst b/docs/langref/relay/type_system.rst new file mode 100644 index 000000000000..bb66d866e935 --- /dev/null +++ b/docs/langref/relay/type_system.rst @@ -0,0 +1,157 @@ +=========== +Type System +=========== + +We have briefly introduced types while detailing the the expression language +of Relay, but have not yet described the type system. Relay is +a statically typed and type-inferred language, allowing programs to +be typed with a minimal requirement of explicit type information. + +Static types are useful because they enable efficient layout, memory reuse, and +code generation. They aid in debugging program transformations, but can also give us the +expressivity afforded by more dynamic languages. + +We are able to omit these type annotations by a process known as type inference. +Type inference is a technique that has its roots in the programming language +community, and can be viewed as a method for generalizing shape inference to +run over arbitrary user programs containing control flow and recursion. + +Static types are useful when performing compiler optimizations because they +communicate properties about the data we manipulate, such as runtime shape, +data layout, and storage without needing to run the program. + +Most current IRs use "shape inference" to recover tensor dimensions from the user +provided program. Machine learning users have enjoyed shape inference for +tensors because it allows them to generate performant code without giving up +on the expressivity of the input language. Because Relay is intended as an IR, we +require *some* type information to provide full inference. We don't believe this to be +an issue, as many of the IR builder interfaces require some type information or can +generate IR based on their own higher-level inferences. + +We view this limited shape inference as a simpler form of type +inference. Instead of relying on an ad hoc procedure for recovering type +information from a potentially dynamic program, we apply ideas from compiler +and IR design. Below, we briefly discuss the different kinds of types in Relay. + +===== +Types +===== + +Relay's type system has a "language of types" which enables one to write down the type of +a Relay program. Below we detail the language of types and how we assign types to Relay +expressions. + +Type +~~~~ + +The base type for all Relay types. All Relay types are sub-classes of this base type. + +See :py:class:`~tvm.relay.ty.Type` for its definition and documentation. + +Tensor Type +~~~~~~~~~~~ + +A concrete TensorType in Relay, see `tvm/relay/type.h` for more details. + +This is the type assigned to tensor's with a known dtype and shape. For +example a tensor of `float32` and `(5, 5)`. The data type must be a base +type as enforced by the kind checking rules described below. +The shape may be any valid Relay shape as described in the below section on shapes. + +See :py:class:`~tvm.relay.ty.TensorType` for its definition and documentation. + +Kind +~~~~ + +The kind of a type parameter, representing a variable shape, +base type, type, or dimension. + +This controls what a type parameter is allowed to be instantiated +with. For example one's of kind BaseType can only be `float32`, +`int32`, and so on. + +See :py:class:`~tvm.relay.ty.Kind` for its definition and documentation. + +Type Parameter +~~~~~~~~~~~~~~ + +A type parameter used for generic types in Relay, +see `tvm/relay/type.h` for more details. + +A type parameter represents a type placeholder that will +be filled in later on. This allows the user to write +functions that are generic over types. + +See :py:class:`~tvm.relay.ty.TypeParam` for its definition and documentation. + +Type Constraint +~~~~~~~~~~~~~~~ + +Abstract class representing a type constraint, to be elaborated +upon in further releases. + +See :py:class:`~tvm.relay.ty.TypeConstraint` for its definition and documentation. + +Function Type +~~~~~~~~~~~~~ +A function type in Relay, see `tvm/relay/type.h` for more details. + +This is the type assigned to functions in Relay. A function type consists of +a list of type parameters, a set of type constraints, a sequence of argument +types, and a return type. + +We informally write them as: +`forall (type_params), (arg_types) -> ret_type where type_constraints` + +See :py:class:`~tvm.relay.ty.FuncType` for its definition and documentation. + +Type Relation +~~~~~~~~~~~~~ + +A type relation is the most exotic type system feature in Relay. It allows +users to extend type inference with new rules. We use type relations to type operators with +"hard" types such as broadcasting operators, or :code:`flatten`. + +A type relation :code:`R` is an n-ary input, single-output relation over +types. To unpack that, it allows us to specify a relationship between +a set of input and output types. + +For example we can define the identity relation to be: + +.. code-block:: prolog + Identity(I, I) :- true + +Or we can define the relation for flatten: + +.. code-block:: prolog + Flatten(Tensor(sh, bt), O) :- + O = Tensor(sh[0], prod(sh[1:])) + +The above examples are written in Prolog-like syntax, but currently the relations +must be implemented by users in C++ or Python. + +If we have a relation such as :code:`Broadcast` it becomes possible to type things +like :code:`elemwise_add`: + +.. code-block:: python + elemwise_add : forall (Lhs : Type) (Rhs : Type), (Lhs, Rhs) -> Broadcast(Lhs, Rhs) + +You might ask why we write the relation in the return type. We use it as a +notational convenience for: + +.. code-block:: python + elemwise_add : forall (Lhs : Type) (Rhs : Type) (Out : Type), Broadcast(Lhs, Rhs, Out) => (Lhs, Rhs) -> Out + +That is, the user may pick the type of the :code:`Lhs`, :code:`Rhs`, and :code:`Out` as long as we can +show :code:`Broadcast(Lhs, Rhs, Out)` holds. + +See :py:class:`~tvm.relay.ty.TypeRelation` for its definition and documentation. + +Incomplete Type +~~~~~~~~~~~~~~~ + +A type or portion of a type that is not yet known. Only used during type inference. + +.. note:: Known as a "type variable" in the type checking literature. + +See :py:class:`~tvm.relay.ty.IncompleteType` for its definition and documentation. From fd4ae4d147cbb0c7b474548402047d03b04c08de Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 3 Dec 2018 17:48:06 -0800 Subject: [PATCH 02/36] Move relay docs to top-level langref dir --- docs/langref/index.rst | 7 +++- docs/langref/relay/index.rst | 16 -------- .../{relay/expressions.rst => relay_expr.rst} | 0 .../{relay/intro.rst => relay_intro.rst} | 37 ++++++------------- .../{relay/type_system.rst => relay_type.rst} | 0 5 files changed, 17 insertions(+), 43 deletions(-) delete mode 100644 docs/langref/relay/index.rst rename docs/langref/{relay/expressions.rst => relay_expr.rst} (100%) rename docs/langref/{relay/intro.rst => relay_intro.rst} (75%) rename docs/langref/{relay/type_system.rst => relay_type.rst} (100%) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index 22ca00f7faa5..4120dd4004c1 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -1,10 +1,13 @@ Language Reference ================== -This document provide references to -embedded languages in TVM stack. +This document provides references to +embedded languages in the TVM stack. .. toctree:: :maxdepth: 2 + relay_intro + relay_expr + relay_type relay_op hybrid_script diff --git a/docs/langref/relay/index.rst b/docs/langref/relay/index.rst deleted file mode 100644 index 1b05697cbb03..000000000000 --- a/docs/langref/relay/index.rst +++ /dev/null @@ -1,16 +0,0 @@ -Relay Language Reference -======================== - -This document is a work in progress language reference describing -Relay, TVM's high-level intermediate representation. The name is an -allusion to interneurons, which are often referred to as intermediate -or relay neurons. - -As we evolve the new IR, we will update this document accordingly. - -.. toctree:: - :maxdepth: 2 - - intro - expressions - type_system diff --git a/docs/langref/relay/expressions.rst b/docs/langref/relay_expr.rst similarity index 100% rename from docs/langref/relay/expressions.rst rename to docs/langref/relay_expr.rst diff --git a/docs/langref/relay/intro.rst b/docs/langref/relay_intro.rst similarity index 75% rename from docs/langref/relay/intro.rst rename to docs/langref/relay_intro.rst index 9f5a9cab4b2c..bc09a5a253e0 100644 --- a/docs/langref/relay/intro.rst +++ b/docs/langref/relay_intro.rst @@ -2,31 +2,18 @@ Introduction ============ -Relay is a differentiable programming language with support for -closures, control flow, and recursion. It has an advanced -static type system specifically designed for programs written -by machine learning practitioners and researchers. Relay is intended to replace -the computation graph-based intermediate representations currently employed by deep -learning frameworks and compilers. - -The deep learning community has organically evolved a representation of machine learning -models that was useful for the form of computation originally desired, i.e., a directed -acyclic graph of primitive functions. Computation graphs also serve a dual purpose as both a -compile-time and run-time data structure. While computation graphs are a good fit -for models with a static topology, they make it tricky to incorporate control flow and -abstraction. Additionally, the conflation of the description of a computation, the -representation used for optimizing it, and the data structure used to execute it unnecessarily -hamper the goals of machine learning frameworks. We believe having a high-level, expressive language -designed for writing compiler optimizations is essential to the future of an end-to-end -deep learning compiler stack. - -Relay's design is influenced by the authors' experience building advanced optimizing compilers -for high-level languages, as well as by challenges presented by the current version of the -TVM stack, and NNVM's IR. We address a few important challenges with Relay's design. -Relay is an IR with closures, control-flow, recursion, and an advanced type system supporting -complex shape relationships and symbolic dimensions. We define a series of -automatic differentiation rules over the language, with the goal of enabling higher-order -differentiation of programs with control flow and closures. +Relay is a functional, differentiable programming language that has been +designed to be an expressive intermediate representation for machine +learning systems. It features support for closures, control flow, and +recursion, thus allowing for representing more complex models directly +in Relay. Relay also includes a form of dependent typing using type +relations in order to handle to shape analysis + + +Additionally, Relay is designed to be easily extensible by +machine learning researchers and practitioners in order to facilitate +the inclusion and development of new large-scale program transformations +and optimizations. ================== Language diff --git a/docs/langref/relay/type_system.rst b/docs/langref/relay_type.rst similarity index 100% rename from docs/langref/relay/type_system.rst rename to docs/langref/relay_type.rst From 65fbaaa5f73414522774e5d6d2dbc1be8ba0c399 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 3 Dec 2018 21:36:32 -0800 Subject: [PATCH 03/36] Pass over expression documentation --- docs/langref/relay_expr.rst | 376 ++++++++++++++++++++++++++++------- docs/langref/relay_intro.rst | 166 +--------------- 2 files changed, 313 insertions(+), 229 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index f9644d30d7ff..4c6cccd3531e 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -1,30 +1,210 @@ -=========== -Expressions -=========== +==================== +Expressions in Relay +==================== -The Relay IR is a pure, expression-oriented language with distinct dataflow -and control flow language fragments. Although Relay uses abstract syntax trees to represent programs, -the dataflow fragments of a program can be considered as a graph when writing and expressing transformations. +The Relay IR is a pure, expression-oriented language with distinct +dataflow and control flow language fragments. +The dataflow fragments of a program (i.e., those without +calls to recursive functions or branching) can be considered +as a more traditional computation graph when writing and +expressing transformations. -The below sections make an attempt to clearly split the expressions that -are pure dataflow (equivalent to traditional computation graphs) from -the extended expressions that contain control flow. +The below sections describe the different expressions in Relay +as well as give details of their semantics. + +Variables +========= + +Relay allows for local and global variables. Our design is based on +that of LLVM, which differentiates between identifier types; a writer of +optimizations can thus determine a lot of information about what a +variable references simply by knowing the kind of identifier. + +Global variables are written with `@`, local variables are written +with `%`, and variables written without a sigil correspond to operator +names. + +The distinction between global and local identifiers +makes certain kinds of transformation easier. For example, +inlining a global definition requires no analysis: simply inlining +the definitions suffices. + +Global Variable +~~~~~~~~~~~~~~~~~~ + +Global identifiers are prefixed by the `@` sigil, such as "`@global`". +A global identifier always references a globally visibly definition contained in the environment. The names of global identifiers must be unique. + +See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation +and documentation. + +Local Variable +~~~~~~~~~~~~~~~~~ + +Local identifiers are prefixed by the :code:`%` sigil, +such as ":code:`%local`". A local identifier always references +a function argument or a variable bound in a `let` expression. +A local variable will be scoped to the function where it +appears or the `let` expression where it is bound, respectively. + +Suppose the local variable :code:`%a` has been defined in a scope +and within that scope, a `let` expression binding to a variable +:code:`%a` appears. This is permitted, as in most functional languages. +In the scope of the `let` expression (the inner scope), +the name :code:`%a` is "shadowed," meaning all references to +:code:`%a` in the inner scope refer to the later defintion, while +references to :code:`%a` in the outer scope continue to refer to +the previous one. + +(Note that in Relay's implemetnation, each definition of a local variable +creates a new :py:class:`~tvm.relay.expr.Var`, so a shadowed local variable, +despite having the same name as one in an outer scope, will be a different +object. This allows for comparing local variables by pointer identity with the +knowledge that the same local variable object corresponds to a different binding site.) + +See :py:class:`~tvm.relay.expr.Var` for its implementation +and documentation. + +Global Functions +================ + +A function is no different from a procedure or function in a +typical programming language and generalizes the concept of a +named subgraph. +A function definition consists of a name, arguments, return type, +type parameters, and any applicable type relations. +A function's return type and the types of parameters may be omitted; +Relay will attempt to infer the most general types where types +are omitted. + +Functions defined in the manner described in this subsection are +of global scope; anonymous functions will be discussed later, though +their mechanics are nearly identical. Note that global functions may be +recursive; that is, within the function's body, the function's +identifier refers back to the function unless it is shadowed in a `let` +expression. + +A definition minimally consists of an identifier :code:`@id`, an empty set of +parameters, and a body expression (:py:class:`~tvm.relay.expr.Expr`) +contained by curly braces. + +.. code-block:: python + + def @id() { body } + +A definition may contain any number of parameters. For example, a +simple function that invokes the `add` operator: + +.. code-block:: python + + def @plus(%x, %y) { add(%x, %y) } + +Notice that within the function's body, the parameters are local +variables, just like those bound in a `let` expression. + +It is also possible for us to annotate explicit types on definitions. +For example, we can restrict the above definition to only work +on certain types: + +.. code-block:: python + + def @add(%x: Tensor, %y: Tensor) -> Tensor { + %x + %y + } + +A parameter is just a pairing of a :py:class:`~tvm.relay.expr.LocalVar` and optional :py:class:`~tvm.relay.ty.Type`. They represent +the formal parameters of functions and definitions and are written as :code:`%x : T`. + +Parameters may only appear in function literals and definitions +and have no relation to parameters in the machine learning. + +When the type information is omitted, we will attempt to infer the most general type +for the users. This property is known as generalization: for a definition without +explicit annotations, we will attempt to assign the most general type. When the +return type is omitted, we will infer the return type based on the text of the +program. + +We can directly construct type-polymorphic definitions by writing down +a set of type parameters for a definition. For example, one can define a +polymorphic identity function for tensors as follows: +:: + def @id(%x: Tensor) { + %x + } + +Notice that the return type is omitted and will be inferred. + +.. *Note: polymorphism is not yet implemented.* + +A function may also be subject to one or more type relations, such as in +the following: + +.. code-block:: python + + def @plus(%x, %y) where Broadcast { add(%x, %y) } + +In the above definition, the types of `%x` and `%y` and the return type +are subject to the `Broadcast` relation, meaning all three must be tensors +and their shapes follow the elementwise broadcast relation. As with +operators, the definitions of relations are not transparent to Relay +and they are instead implemented externally. + +As in the case of `Broadcast`, relations are used to express complicated +constraints on types (especially tensor shapes). +All function relations must hold at all call sites; +type checking is thus treated as a constraint-solving problem. +For more detail on type relations and their implementations, +please see the documentation on typing in Relay. + +See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of function nodes. + +Operators +========= + +An operator is a primitive operation that is not defined in the Relay +language but is registered in the global environment in either Python +or C++. Implementations of operators are typically backed by TVM's TOPI. + +An operator requires a user to provide an implementation +of the operator, its type, and any other desired metadata. +The operator registry is simply a column-based store where +operators are keys, so any metadata (which might be referenced +by optimization passes) may be registered as a new column. + +From the perspective of Relay's type system, an operator is a function, +so operators may be called like any other function and have function +types. In particular, operator types are registered using a single +type relation (see the above subsection), typically a relation +specialized to that operator. For example, the :code:`add` operator +is registered with the `Broadcast` relation, indicating that the +arguments of :code:`add` must be tensors and that the return type +is a tensor whose shape depends on those of its arguments. + +Operators are rendered without a sigil (e.g :code:`add`, :code:`subtract`) +when pretty-printing Relay programs. +Operators are explicitly contained in the program and are uniquely +identifiable by pointer during a run of the Relay compiler. + +See :py:class:`~tvm.relay.op.Op` for the definition and documentation +of operator nodes, demonstrating the infrastructure for registering +operator metadata. The other files in :py:class:`~tvm.relay.op` give +handles for generating a call to various pre-registered operators. -================= Dataflow Fragment ================= -First we will cover the set of expressions which do not involve control flow; -this fragment of the language is semantically equivalent to pure computation graphs -without control flow. +This subsection covers the set of Relay expressions that do not involve +control flow. That is, any portion of a program comprised only of these +expressions corresponds to a pure computation graph without control flow. +Note that global and local variables are also part of the dataflow fragment. Constants ~~~~~~~~~ -Relay programs can contain constant tensor values. This node represents -a constant tensor value (see :py:mod:~tvm.relay.Value for more details). -The constants are represented as :py:class:`~tvm.NDArray`, allowing us to utilize -TVM operators for constant evaluation. +This node represents a constant tensor value +(see :py:mod:~tvm.relay.Value for more details). +The constants are represented as :py:class:`~tvm.NDArray`, +allowing Relay to utilize TVM operators for constant evaluation. See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation. @@ -43,82 +223,113 @@ members. See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. -Function -~~~~~~~~ +Tuple Projection +~~~~~~~~~~~~~~~~ -A function node represents a function; it contains a sequence of -parameters, a return type, and a body. +A tuple must be indexed by an integer constant in order to extract a +particular member of the tuple. Projections are 0-indexed. + +For example, the below projection evaluates to :code:`b`: .. code-block:: python - fun (x : Float, y: Float) -> Float { x + y } + (a, b, c).1 + +See :py:class:`~tvm.relay.expr.TupleGetItem` for its definition and documentation. -Functions are first-class in Relay and can be used in any expression -position. Function expressions are the same as global functions, but do not -have a globally unique name. You can use a function in conjunction with a let -binding to define locally recursive functions. +Function Expressions +~~~~~~~~~~~~~~~~~~~~ + +Functions are first class in Relay and can be used in any expression +position. Function expressions are the same as global functions and +use nearly the same syntax (besides not including a name), but do +not have a globally unique name. .. code-block:: python - let fact = fun (x : Float) -> Float { - if (x == 0) { - 0 - } else { - x * fact(x - 1) - } - }; - fact(10) + fun (%x : Tensor, y: Tensor + -> Tensor { add(%x, %y) } -See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. +Note that function expressions evaluate to closure values. Closures +store values for all free variables in their body. A free variable +is a variable defined outside the scope of the function's body, +which means that if a function expression references a local variable +in the outer scope that is not shadowed by the parameters, +the closure will store the value for that local variable and +use that value when the function is called, even if original +local variable has gone out of scope. -Variables -~~~~~~~~~ +For example, in the below example, :code:`%z` will evaluate to a tensor +of zero values because the closure for :code:`%f` stores the value of +:code:`%x` at the pointer where :code:`%f` was defined. + +.. code-block:: -Both global variables and local variables are valid expressions; one may use them -anywhere an expression may appear. + let %g = fun () { + let %x = Constant(0, float32, (10, 10)); + # x is a free variable in the below function + fun (%y) { multiply(%y, %x) } + }; + # the %x in %g's body is not in scope anymore + # %f is a closure where %x maps to Constant(0, float32, (10, 10)) + let %f = %g(); + let %x = Constant(1, float32, (10, 10)); + let %z = %f(%x) -For example, the below fragment of code is a valid expression. +A recursive function expression can be defined using a `let` binding, +as here: .. code-block:: python - %ret = @global(op_name, %local) -See :py:class:`~tvm.relay.expr.LocalVar` and :py:class:`~tvm.expr.GlobalVar` for its definition -and documentation. + let %fact = fun (%x : Tensor) -> Tensor { + if (equal(%x, Constant(1, float32, (10, 10))) { + Constant(0, float32, (10, 10)) + } else { + multiply(%x, %fact(subtract(%x, Constant(1, float32, (10, 10)))) + } + }; + %fact(10) + +See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. Let Binding ~~~~~~~~~~~ -A let binding is an immutable variable binding, allowing the user -to bind an expression to a name. A let binding contains a local variable, +A `let` binding is an immutable local variable binding, +allowing the user to bind an expression to a name. + +A `let` binding contains a local variable, an optional type annotation, a value, and a body expression -that may reference the bound identifier. +that may reference the bound identifier. If a type annotation +on the bound variable is omitted, Relay attempts to infer the +most general type permitted for the variable. -We will first introduce a single binding without -type annotations: +The bound variable in a `let` expression is scoped to the let +expression's body. Note that the bound variable can only be +recursively referenced in the value in the case of a function +expression, as in the above subsection. -.. code-block:: python - let %x = %a + %b; - x +The value of a `let` binding is the value of the final expression +after evaluating the bindings it depends on. For example, in the +following example the entire expression evaluates to a tensor +of shape (10, 10) where all elements are 2: -The value of a let binding is the value of the final expression -after evaluating the bindings it depends on. +.. code-block:: python + let %x : Tensor = Consantt(1, float32, (10, 10)); + add(%x, %x) -A sequence of let bindings can be considered as a dataflow graph, +A sequence of `let` bindings can be considered as a dataflow graph, where the bindings are a series of sub-graphs connected by bound variables. Since these binding sequences are -pure, we can evaluate them in any order according to the program -dataflow. - -For example the below Relay program is equivalent to the -below NNVM program. - -.. code-block:: python - let %y_pred = %x * %w + %b; - let %loss = pow(%y - %y_pred, 2); - ret %loss +pure, they can be evaluated in any order according to the program +dataflow. For example, the first and second `let` bindings below +may be evaluated in either order because neither has a dataflow +dependency on the other: .. code-block:: python - TODO + let %x = add(%a, %b); + let %y = add(%c, %d); + multiply(%x, %y) See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. @@ -126,22 +337,33 @@ See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. Control Flow Expression ======================= -Control flow expressions enable network topology to change based +Control flow expressions allow the network topology to change based on the value of previously executed expressions. Call ~~~~ -Expressions with function types in Relay are "callable," meaning that they can be -invoked via a function call. - -All Relay functions are typed with function types, as are all Relay operators. +Expressions with function types in Relay are "callable," +meaning that they can be invoked via a function call. These consist of +any expression that evaluates to a closure (i.e., function expressions +or global functions) and Relay operators. -For example, we can call the previously defined `fact` because it has a function -type: +For example, we can call the previously defined `%fact` because it +has a function type: .. code-block:: python - fact(10) + %fact(10) + +A type-polymorphic function can also include type arguments at a call +site. The type arguments are substituted for type parameters when +type checking. + +.. *Note: polymorphism is not yet implemented.* + +Note that all type relations in the function type must hold at each +call site. Because relations are checked at call sites, this means that +the relations are checked against the types of the particular arguments +at that call site, so this is also allows for a form of polymorphism. See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. @@ -150,7 +372,7 @@ If-Then-Else Relay has a simple if-then-else expression that allows programs to branch on a single value of type :code:`bool`, i.e., a zero-rank -tensor of booleans (:code:`Tensor[(), bool]`). +tensor of booleans (:code:`Tensor`). .. code-block:: python if (sum(equal(t, u))) { @@ -159,4 +381,10 @@ tensor of booleans (:code:`Tensor[(), bool]`). return y; } +Since if-then-else branches are expressions, they may appear inline +wherever any other expression may be expected, like invocations of +the ternary operator in C-like languages. The if-then-else expression +evaluates to the value of the "then" branch if the condition value is +`True` and evaluates to the value of the "else" branch otherwise. + See :py:class:`~tvm.relay.expr.If` for its definition and documentation. diff --git a/docs/langref/relay_intro.rst b/docs/langref/relay_intro.rst index bc09a5a253e0..ad9d1a5236db 100644 --- a/docs/langref/relay_intro.rst +++ b/docs/langref/relay_intro.rst @@ -1,169 +1,25 @@ -============ -Introduction -============ +===================== +Introduction to Relay +===================== Relay is a functional, differentiable programming language that has been designed to be an expressive intermediate representation for machine learning systems. It features support for closures, control flow, and recursion, thus allowing for representing more complex models directly in Relay. Relay also includes a form of dependent typing using type -relations in order to handle to shape analysis - +relations in order to handle shape analysis for operators with complex +requirements on argument shapes. Additionally, Relay is designed to be easily extensible by machine learning researchers and practitioners in order to facilitate the inclusion and development of new large-scale program transformations and optimizations. -================== -Language -================== - -Relay is a purely functional, differentiable intermediate representation. - -================== -IR Reference -================== - -The IR has a global environment that stores the set of definitions, -constants, options, and attributes, and provides access to features -including type inferecnce, constant evaluation, and more. - -~~~~~~~~~~ -Relay Node -~~~~~~~~~~ - -The fundamental unit of the IR is the node, which only contains a Span. - -.. code-block:: python - - class Node: - span: Span - -================== -Variables -================== - -Relay has two notions of variables: local and global. -Our design draws inspiration from LLVM, which differentiates between identifier types. -This enables writers of optimizations to know precisely what an identifier references without needing -information beyond the kind of identifier. - -Globals are written with `@`, locals are written with `%`, and variables written without a -sigil name the corresponding operator. The distinction between global and local identifiers -makes certain kinds of transformation easier. For example, inlining a global definition -requires no analysis, as you can write a pass that directly inlines the definitions. -Ensuring there is no spooky action at a distance; introducing a new identifier return -type is omitted we will infer the return type based on the text of the program. - - -Global Variable -~~~~~~~~~~~~~~~~~~ - -Global identifiers are prefixed by the `@` sigil. A global identifier always -references a globally visibly definition contained in the environment. You -can write a global identifier as `@global`. - -Local Variable -~~~~~~~~~~~~~~~~~ - -Local identifiers are prefixed by the :code:`%` sigil. A local identifier always -references a parameter, or let bound expression. You can write a local -identifier as :code:`%local`. - - -================ -Global Functions -================ - -A function definition consists of a name, parameters, type parameters, and an optional return -type. A global function is no different from a procedure or function in a typical programming -language and generalizes the concept of a named subgraph. - -A definition minimally consists of an identifier :code:`@id`, an empty set of -parameters, and a body expression contained by curly braces. - -.. code-block:: python - - def @id() { body } - -A definition may also contain any number of parameters. For example, a -simple function which just adds two tensors: - -.. code-block:: python - - def @add(%x, %y) { %x + %y } - -It is also possible for us to annotate explicit types on definitions. For example, -we can restrict the above definition to only work on certain types: - -.. code-block:: python - - def @add(%x: Tensor, %y: Tensor) -> Tensor { - %x + %y - } - -A parameter is just a pairing of a :py:class:`~tvm.relay.expr.LocalVar` and optional :py:class:`~tvm.relay.ty.Type`. They represent -the formal parameters of functions and definitions, and are written as :code:`%x : T`. - -Parameters may only appear in function literals and definitions and have no relation -to parameters in the machine learning. - -When the type information is omitted, we will attempt to infer the most general type -for the users. This property is known as generalization: for a definition without -explicit annotations, we will attempt to assign the most general type. When the -return type is omitted, we will infer the return type based on the text of the -program. - -Finally, we can directly construct type-polymorphic definitions by writing down -a set of type parameters for a definition. For example, one can definte a -polymorphic identity function for tensors as follows: -:: - def @id(%x: Tensor) { - %x - } - -Notice we can omit the return type and it will still be inferred. - -.. *Note: this is not yet implemented.* - -.. Finally we allow a definition be prefixed by metadata, which adds -extra properties to the definition. - -.. It is important to be able to annotate metadata that is external to -the computational behavior of a definition. For example, we can use -this to add an `inline` or `noinline` attribute that the compiler -can consider when performing inlining. - -.. For example we can set the attributes for :code:`@id_real`.:: - - -.. attributes id_real { - inline: true - } - -.. def id_real(%x:Real) { ret %x } - - -========= -Operators -========= - -An operator is a primitive operation that is not defined in the Relay language but is provided -externally. Currently we back these operator's registrations with the operators -exposed by TVM's TOPI. An operator requires a user to provide an implementation -of the operator, its type, and various required attributes. - -The input methods for Relay programs do not provide a way to describe operators in -Relay; they must be explicitly registered in the global environment via Python or C++. -Operators are rendered without a sigil (e.g :code:`add`, :code:`subtract`) when pretty- -printing Relay programs. Operators are explicitly contained in the program and are uniquely -identifiable by pointer during a run of the Relay compiler. +The below pages describe the grammar, type system, and operators in Relay, respectively. -Programs -~~~~~~~~ +.. toctree:: + :maxdepth: 2 -Now that we have presented both global functions and operators, we have -everything in hand to describe a complete Relay program. A Relay program consists of a -registry of operators, one or more functions, as well as the global configuration -stored in the environment. + relay_expr + relay_type + relay_op From 37ef0d7d442417cbefb917b6b9388041f562ca54 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 4 Dec 2018 17:56:39 -0800 Subject: [PATCH 04/36] Corrections to examples, etc., in expr docs --- docs/langref/relay_expr.rst | 24 +++- docs/langref/relay_type.rst | 213 +++++++++++++++++++++++------------- 2 files changed, 153 insertions(+), 84 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 4c6cccd3531e..b852ed7d3926 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -127,7 +127,8 @@ program. We can directly construct type-polymorphic definitions by writing down a set of type parameters for a definition. For example, one can define a polymorphic identity function for tensors as follows: -:: + +.. code-block:: python def @id(%x: Tensor) { %x } @@ -219,7 +220,7 @@ members. (a, b, c) : Tuple - (a + b + c, d) : Tuple, Tensor> + (add(add(a, b), c), d) : Tuple, Tensor> See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. @@ -315,6 +316,7 @@ following example the entire expression evaluates to a tensor of shape (10, 10) where all elements are 2: .. code-block:: python + let %x : Tensor = Consantt(1, float32, (10, 10)); add(%x, %x) @@ -327,9 +329,10 @@ may be evaluated in either order because neither has a dataflow dependency on the other: .. code-block:: python - let %x = add(%a, %b); - let %y = add(%c, %d); - multiply(%x, %y) + + let %x = add(%a, %b); + let %y = add(%c, %d); + multiply(%x, %y) See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. @@ -348,11 +351,19 @@ meaning that they can be invoked via a function call. These consist of any expression that evaluates to a closure (i.e., function expressions or global functions) and Relay operators. +When a closure is called, the body is evaluated in the closure's stored +environment (i.e., using the stored values for free variables) with +local variable bindings added for each argument; the final value +obtained by evaluating the body is the call's return value. +In the case of operators, the implementation is opaque to Relay, +so the result is left up to the registered TVM implementation. + For example, we can call the previously defined `%fact` because it has a function type: .. code-block:: python - %fact(10) + + %fact(10) A type-polymorphic function can also include type arguments at a call site. The type arguments are substituted for type parameters when @@ -375,6 +386,7 @@ on a single value of type :code:`bool`, i.e., a zero-rank tensor of booleans (:code:`Tensor`). .. code-block:: python + if (sum(equal(t, u))) { return x: } else { diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index bb66d866e935..565fea7ddb1e 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -1,45 +1,36 @@ -=========== -Type System -=========== +=================== +Relay's Type System +=================== We have briefly introduced types while detailing the the expression language of Relay, but have not yet described the type system. Relay is a statically typed and type-inferred language, allowing programs to be typed with a minimal requirement of explicit type information. -Static types are useful because they enable efficient layout, memory reuse, and -code generation. They aid in debugging program transformations, but can also give us the -expressivity afforded by more dynamic languages. - -We are able to omit these type annotations by a process known as type inference. -Type inference is a technique that has its roots in the programming language -community, and can be viewed as a method for generalizing shape inference to -run over arbitrary user programs containing control flow and recursion. - Static types are useful when performing compiler optimizations because they communicate properties about the data we manipulate, such as runtime shape, -data layout, and storage without needing to run the program. - -Most current IRs use "shape inference" to recover tensor dimensions from the user -provided program. Machine learning users have enjoyed shape inference for -tensors because it allows them to generate performant code without giving up -on the expressivity of the input language. Because Relay is intended as an IR, we -require *some* type information to provide full inference. We don't believe this to be -an issue, as many of the IR builder interfaces require some type information or can -generate IR based on their own higher-level inferences. - -We view this limited shape inference as a simpler form of type -inference. Instead of relying on an ad hoc procedure for recovering type -information from a potentially dynamic program, we apply ideas from compiler -and IR design. Below, we briefly discuss the different kinds of types in Relay. +data layout, and storage without needing to run the program. Additionally, +static typing is useful for determining the + +Relay's type system features a form of depending typing for shapes to +replace the dynamic shape inference used in NNVM and most other machine +learning IRs. Treating tensor shapes as types allows Relay to perform +more powerful reasoning at compile time; in particular, Relay can statically +reason about operations whose output shapes vary based on the input shapes +in complex ways. Statically reasoning about shapes in this manner allows +Relay to be ahead-of-time compiled and provides much more information about +tensors for optimizations furhter in the compilation pipeline. + +Reasoning about tensor types in Relay is encoded using type relations, which means +that the bulk of type checking in Relay is constraint solving (ensuring that all +type relations are satisfied at call sites). Type relations offer a flexible and +relatively simple way of making the power of dependent typing available in Relay +without greatly increasing the complexity of Relay's type AST. -===== Types ===== -Relay's type system has a "language of types" which enables one to write down the type of -a Relay program. Below we detail the language of types and how we assign types to Relay -expressions. +Below we detail the language of types in Relay and how they are assigned to Relay expressions. Type ~~~~ @@ -51,36 +42,71 @@ See :py:class:`~tvm.relay.ty.Type` for its definition and documentation. Tensor Type ~~~~~~~~~~~ -A concrete TensorType in Relay, see `tvm/relay/type.h` for more details. +A concrete TensorType in Relay. + +Tensors are typed according to data type and shape. At present, these use TVM's +data types and shapes, but in the future, Relay may include a separate AST for +shapes. In particular, data types include `bool`, `float32`, `int8` and various +other bit widths. Shapes are given as tuples of dimensions (TVM `IndexExpr`), +such as `(5, 5)`; note, though, that TVM shapes can also include variables and +arithmetic expressions including variables, so Relay's constraint solving phase +will attempt to find assignments to all shape variables to ensure all shapes will +be concrete before running a program. -This is the type assigned to tensor's with a known dtype and shape. For -example a tensor of `float32` and `(5, 5)`. The data type must be a base -type as enforced by the kind checking rules described below. -The shape may be any valid Relay shape as described in the below section on shapes. +For example, here is a simple concrete tensor type corresponding to a 10-by-10 tensor of 32-bit floats: + +.. code-block:: python + + Tensor See :py:class:`~tvm.relay.ty.TensorType` for its definition and documentation. -Kind -~~~~ +Tuple Type +~~~~~~~~~~ -The kind of a type parameter, representing a variable shape, -base type, type, or dimension. +A type of a tuple in Relay. -This controls what a type parameter is allowed to be instantiated -with. For example one's of kind BaseType can only be `float32`, -`int32`, and so on. +Just as a tuple is simply a sequence of values of statically known length, the type +of the tuple consists of a sequence of types corresponding to the type of each member +of the tuple. -See :py:class:`~tvm.relay.ty.Kind` for its definition and documentation. +Because a tuple type is of statically known size, the type of a tuple projection +is simply the corresponding index into the tuple type. + +For example, in the below code, :code:`%t` is of type +`Tuple, Tensor>` +and :code:`%c` is of type `Tensor`. + +.. code-block:: python + let %t = (Constant(0, bool, ()), Constant(1, float32, (10, 10))); + let %c = %t.1 + +See :py:class:`~tvm.relay.ty.TupleType` for its definition and documentation. Type Parameter ~~~~~~~~~~~~~~ -A type parameter used for generic types in Relay, -see `tvm/relay/type.h` for more details. +.. *note*: Type parameters are not yet implemented + +Type parameters represent placeholder types used for polymorphism in functions. +Type parameters are specified according to *kind*: Kinds include general types +(such as tensor types and tuple types), shapes, and data types. Relay enforces +that types can only appear where their kind permits them; for instance, a +shape or data type can only appear inside a tensor type, while only general types +may appear inside a tensor or for a function's return and argument types. + +Type parameters will be substituted with a concrete type at call sites. + +For example, `s` below is a type paramter of kind `Shape` and it will +be substituted for `(10, 10)` at the call site below: + +.. code-block:: python -A type parameter represents a type placeholder that will -be filled in later on. This allows the user to write -functions that are generic over types. + def @plus(%t1 : Tensor, %t2 : Tensor) { + add(%t1, %t2) + } + plus<(10, 10)>(%a, %b) + See :py:class:`~tvm.relay.ty.TypeParam` for its definition and documentation. @@ -88,7 +114,8 @@ Type Constraint ~~~~~~~~~~~~~~~ Abstract class representing a type constraint, to be elaborated -upon in further releases. +upon in further releases. Currently, type relations are the only +type constraints provided; they are discussed below. See :py:class:`~tvm.relay.ty.TypeConstraint` for its definition and documentation. @@ -96,61 +123,91 @@ Function Type ~~~~~~~~~~~~~ A function type in Relay, see `tvm/relay/type.h` for more details. -This is the type assigned to functions in Relay. A function type consists of -a list of type parameters, a set of type constraints, a sequence of argument -types, and a return type. +This is the type assigned to functions in Relay. A function type +consists of a list of type parameters, a set of type constraints, +a sequence of argument types, and a return type. -We informally write them as: -`forall (type_params), (arg_types) -> ret_type where type_constraints` +We informally write function types as: +`fun(arg_types) -> ret_type where type_constraints` + +A type parameter in the function type may appear in the argument +types or the return types. Additionally, each of the type constraints +must hold at every call site of the function. The type constraints +typically take the function's argument types and the function's return +type as arguments, but may take a subset instead. See :py:class:`~tvm.relay.ty.FuncType` for its definition and documentation. Type Relation ~~~~~~~~~~~~~ -A type relation is the most exotic type system feature in Relay. It allows -users to extend type inference with new rules. We use type relations to type operators with -"hard" types such as broadcasting operators, or :code:`flatten`. +A type relation is the most complex type system feature in Relay. +It allows users to extend type inference with new rules. +We use type relations to define types for operators that work with +tensor shapes in complex ways, such as broadcasting operators or +:code:`flatten`, allowing Relay to statically reason about the shapes +in these cases. -A type relation :code:`R` is an n-ary input, single-output relation over -types. To unpack that, it allows us to specify a relationship between -a set of input and output types. +A type relation :code:`R` is an n-ary-input, single-output relation over +types. Namely, :code:`R` specifies a relationship between its argument +types and outputs either `true` if the relationship holds and `false` +if it fails to hold. Types given to a relation may be incomplete or +include shape variables, so it may be possible to assign values to +incomplete types and shape variables such that a relation can hold. -For example we can define the identity relation to be: +For example we can define an identity relation to be: .. code-block:: prolog Identity(I, I) :- true -Or we can define the relation for flatten: +Or we can define the relation for :code:`flatten`: .. code-block:: prolog Flatten(Tensor(sh, bt), O) :- O = Tensor(sh[0], prod(sh[1:])) -The above examples are written in Prolog-like syntax, but currently the relations -must be implemented by users in C++ or Python. - -If we have a relation such as :code:`Broadcast` it becomes possible to type things -like :code:`elemwise_add`: - -.. code-block:: python - elemwise_add : forall (Lhs : Type) (Rhs : Type), (Lhs, Rhs) -> Broadcast(Lhs, Rhs) - -You might ask why we write the relation in the return type. We use it as a -notational convenience for: +If we have a relation like :code:`Broadcast` it becomes possible +to type operators like :code:`add`: .. code-block:: python - elemwise_add : forall (Lhs : Type) (Rhs : Type) (Out : Type), Broadcast(Lhs, Rhs, Out) => (Lhs, Rhs) -> Out - -That is, the user may pick the type of the :code:`Lhs`, :code:`Rhs`, and :code:`Out` as long as we can -show :code:`Broadcast(Lhs, Rhs, Out)` holds. + add : fun(t1, t2) -> t3 + where Broadcast + +The inclusion of :code:`Broadcast` above indicates that the argument +types and the return type must be tensors where the shape of `t3` is +the broadcast of the shapes of `t1` and `t2`. The type system will +accept any argument types and return type so long as they fulfill +:code:`Broadcast`. Hence, it is usually convenient to type operators +in Relay by defining a relation specific to that operator that +encodes all the necessary constraints on the argument types +and the return type. + +Note that the above example relations are written in Prolog-like syntax, +but currently the relations must be implemented by users in C++ +or Python. More specifically, Relay's type system uses an *ad hoc* solver +for type relations in which type relations are actually implemented as +C++ or Python functions that check whether the relation holds and +imperatively update any shape variables or incomplete types. The +functions are run as needed (if an input is updated) until one of the following holds: + +1. All relations hold (typechecking succeeds). +2. A relation fails to hold (a type error). +3. A fixpoint is reached where shape variables or incomplete types +remain (either a type error or more type annotations may be needed). + +Presently all of the relations used in Relay are implemented in C++. +See the files in `src/relay/op` for examples of relations implemented +in C++. See :py:class:`~tvm.relay.ty.TypeRelation` for its definition and documentation. Incomplete Type ~~~~~~~~~~~~~~~ -A type or portion of a type that is not yet known. Only used during type inference. +A type or portion of a type that is not yet known. +Only used during type inference: any omitted type annotation is +replaced by an incomplete type, which will be replaced by another +type at a later point. .. note:: Known as a "type variable" in the type checking literature. From e7c5a046a39cadfa80c7481d9a8c9b9017241ea4 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 10 Dec 2018 14:52:17 -0800 Subject: [PATCH 05/36] Incorporate jroesch's specific suggestions --- docs/langref/relay_expr.rst | 85 ++++++++++++++++++------------------- docs/langref/relay_type.rst | 2 +- 2 files changed, 43 insertions(+), 44 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index b852ed7d3926..eb3a597ecc0e 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -5,8 +5,8 @@ Expressions in Relay The Relay IR is a pure, expression-oriented language with distinct dataflow and control flow language fragments. The dataflow fragments of a program (i.e., those without -calls to recursive functions or branching) can be considered -as a more traditional computation graph when writing and +calls to recursive functions or branching) can be +viewed as a traditional computation graph when writing and expressing transformations. The below sections describe the different expressions in Relay @@ -17,8 +17,8 @@ Variables Relay allows for local and global variables. Our design is based on that of LLVM, which differentiates between identifier types; a writer of -optimizations can thus determine a lot of information about what a -variable references simply by knowing the kind of identifier. +optimizations can thus determine what a variable references +simply by knowing the kind of identifier. Global variables are written with `@`, local variables are written with `%`, and variables written without a sigil correspond to operator @@ -27,13 +27,14 @@ names. The distinction between global and local identifiers makes certain kinds of transformation easier. For example, inlining a global definition requires no analysis: simply inlining -the definitions suffices. +the definition suffices. Global Variable ~~~~~~~~~~~~~~~~~~ Global identifiers are prefixed by the `@` sigil, such as "`@global`". -A global identifier always references a globally visibly definition contained in the environment. The names of global identifiers must be unique. +A global identifier always references a globally visibly definition contained in the environment. +Global identifiers must be unique. See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation and documentation. @@ -43,14 +44,14 @@ Local Variable Local identifiers are prefixed by the :code:`%` sigil, such as ":code:`%local`". A local identifier always references -a function argument or a variable bound in a `let` expression. +a function argument or a variable bound in a :code:`let` expression. A local variable will be scoped to the function where it -appears or the `let` expression where it is bound, respectively. +appears or the :code:`let` expression where it is bound, respectively. Suppose the local variable :code:`%a` has been defined in a scope -and within that scope, a `let` expression binding to a variable +and within that scope, a :code:`let` expression binding to a variable :code:`%a` appears. This is permitted, as in most functional languages. -In the scope of the `let` expression (the inner scope), +In the scope of the :code:`let` expression (the inner scope), the name :code:`%a` is "shadowed," meaning all references to :code:`%a` in the inner scope refer to the later defintion, while references to :code:`%a` in the outer scope continue to refer to @@ -68,20 +69,21 @@ and documentation. Global Functions ================ -A function is no different from a procedure or function in a -typical programming language and generalizes the concept of a -named subgraph. A function definition consists of a name, arguments, return type, type parameters, and any applicable type relations. -A function's return type and the types of parameters may be omitted; +A function's return type and parameter types may be omitted; Relay will attempt to infer the most general types where types are omitted. +Functions in Relay act similarly to procedures or functions in +other programming language and serve to generalize the concept +of a named subgraph. + Functions defined in the manner described in this subsection are of global scope; anonymous functions will be discussed later, though their mechanics are nearly identical. Note that global functions may be recursive; that is, within the function's body, the function's -identifier refers back to the function unless it is shadowed in a `let` +identifier refers back to the function unless it is shadowed in a :code:`let` expression. A definition minimally consists of an identifier :code:`@id`, an empty set of @@ -100,9 +102,9 @@ simple function that invokes the `add` operator: def @plus(%x, %y) { add(%x, %y) } Notice that within the function's body, the parameters are local -variables, just like those bound in a `let` expression. +variables, just like those bound in a :code:`let` expression. -It is also possible for us to annotate explicit types on definitions. +One may also annotate explicit types on definitions. For example, we can restrict the above definition to only work on certain types: @@ -112,11 +114,8 @@ on certain types: %x + %y } -A parameter is just a pairing of a :py:class:`~tvm.relay.expr.LocalVar` and optional :py:class:`~tvm.relay.ty.Type`. They represent -the formal parameters of functions and definitions and are written as :code:`%x : T`. - -Parameters may only appear in function literals and definitions -and have no relation to parameters in the machine learning. +A parameter is just a local variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally annotated +with a type. Parameters are written as :code:`%x : T`. When the type information is omitted, we will attempt to infer the most general type for the users. This property is known as generalization: for a definition without @@ -148,7 +147,7 @@ In the above definition, the types of `%x` and `%y` and the return type are subject to the `Broadcast` relation, meaning all three must be tensors and their shapes follow the elementwise broadcast relation. As with operators, the definitions of relations are not transparent to Relay -and they are instead implemented externally. +and they are instead implemented externally in either C++ or Python. As in the case of `Broadcast`, relations are used to express complicated constraints on types (especially tensor shapes). @@ -162,13 +161,17 @@ See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of Operators ========= -An operator is a primitive operation that is not defined in the Relay -language but is registered in the global environment in either Python +An operator is a primitive operation not defined in the Relay +language. Operators are declaredi n the global operator +registry in C++. Many common operators are backed by TVM's +Tensor Operator Inventory (`TOPI `__). + +but registered in the global environment in either Python or C++. Implementations of operators are typically backed by TVM's TOPI. An operator requires a user to provide an implementation of the operator, its type, and any other desired metadata. -The operator registry is simply a column-based store where +The operator registry is a column-based store where operators are keys, so any metadata (which might be referenced by optimization passes) may be registered as a new column. @@ -184,7 +187,7 @@ is a tensor whose shape depends on those of its arguments. Operators are rendered without a sigil (e.g :code:`add`, :code:`subtract`) when pretty-printing Relay programs. Operators are explicitly contained in the program and are uniquely -identifiable by pointer during a run of the Relay compiler. +identifiable by pointer. See :py:class:`~tvm.relay.op.Op` for the definition and documentation of operator nodes, demonstrating the infrastructure for registering @@ -203,7 +206,7 @@ Constants ~~~~~~~~~ This node represents a constant tensor value -(see :py:mod:~tvm.relay.Value for more details). +(see :py:mod:`~tvm.relay.Value` for more details). The constants are represented as :py:class:`~tvm.NDArray`, allowing Relay to utilize TVM operators for constant evaluation. @@ -251,14 +254,10 @@ not have a globally unique name. fun (%x : Tensor, y: Tensor -> Tensor { add(%x, %y) } -Note that function expressions evaluate to closure values. Closures -store values for all free variables in their body. A free variable -is a variable defined outside the scope of the function's body, -which means that if a function expression references a local variable -in the outer scope that is not shadowed by the parameters, -the closure will store the value for that local variable and -use that value when the function is called, even if original -local variable has gone out of scope. +Note that function expressions evaluate to a closure. Closures +are values that are represented as a pair of a local environment +(storing the values for all variables defined outside the scope +of the function's body) and the function itself. For example, in the below example, :code:`%z` will evaluate to a tensor of zero values because the closure for :code:`%f` stores the value of @@ -277,7 +276,7 @@ of zero values because the closure for :code:`%f` stores the value of let %x = Constant(1, float32, (10, 10)); let %z = %f(%x) -A recursive function expression can be defined using a `let` binding, +A recursive function expression can be defined using a :code:`let` binding, as here: .. code-block:: python @@ -296,21 +295,21 @@ See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. Let Binding ~~~~~~~~~~~ -A `let` binding is an immutable local variable binding, +A :code:`let` binding is an immutable local variable binding, allowing the user to bind an expression to a name. -A `let` binding contains a local variable, +A :code:`let` binding contains a local variable, an optional type annotation, a value, and a body expression that may reference the bound identifier. If a type annotation on the bound variable is omitted, Relay attempts to infer the most general type permitted for the variable. -The bound variable in a `let` expression is scoped to the let +The bound variable in a :code:`let` expression is scoped to the let expression's body. Note that the bound variable can only be recursively referenced in the value in the case of a function expression, as in the above subsection. -The value of a `let` binding is the value of the final expression +The value of a :code:`let` binding is the value of the final expression after evaluating the bindings it depends on. For example, in the following example the entire expression evaluates to a tensor of shape (10, 10) where all elements are 2: @@ -320,11 +319,11 @@ of shape (10, 10) where all elements are 2: let %x : Tensor = Consantt(1, float32, (10, 10)); add(%x, %x) -A sequence of `let` bindings can be considered as a dataflow graph, +A sequence of :code:`let` bindings can be considered as a dataflow graph, where the bindings are a series of sub-graphs connected by bound variables. Since these binding sequences are pure, they can be evaluated in any order according to the program -dataflow. For example, the first and second `let` bindings below +dataflow. For example, the first and second :code:`let` bindings below may be evaluated in either order because neither has a dataflow dependency on the other: diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index 565fea7ddb1e..f99b2845f882 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -42,7 +42,7 @@ See :py:class:`~tvm.relay.ty.Type` for its definition and documentation. Tensor Type ~~~~~~~~~~~ -A concrete TensorType in Relay. +A concrete tensor type in Relay. Tensors are typed according to data type and shape. At present, these use TVM's data types and shapes, but in the future, Relay may include a separate AST for From 3d30695ba4c9f63cac7dc2b11f3eecc1c6a11c7a Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 10 Dec 2018 14:57:59 -0800 Subject: [PATCH 06/36] Deduplicate text in function description --- docs/langref/relay_expr.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index eb3a597ecc0e..6aff6781f931 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -246,8 +246,7 @@ Function Expressions Functions are first class in Relay and can be used in any expression position. Function expressions are the same as global functions and -use nearly the same syntax (besides not including a name), but do -not have a globally unique name. +use nearly the same syntax, but do not have a globally unique name. .. code-block:: python From 1451e6dec8dc93bab70e6ecad21d514f6c64f466 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 10 Dec 2018 14:59:56 -0800 Subject: [PATCH 07/36] Remove note about polymorphism not being implemented; it is! --- docs/langref/relay_expr.rst | 4 ---- docs/langref/relay_type.rst | 4 +--- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 6aff6781f931..81c4735ab074 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -134,8 +134,6 @@ polymorphic identity function for tensors as follows: Notice that the return type is omitted and will be inferred. -.. *Note: polymorphism is not yet implemented.* - A function may also be subject to one or more type relations, such as in the following: @@ -367,8 +365,6 @@ A type-polymorphic function can also include type arguments at a call site. The type arguments are substituted for type parameters when type checking. -.. *Note: polymorphism is not yet implemented.* - Note that all type relations in the function type must hold at each call site. Because relations are checked at call sites, this means that the relations are checked against the types of the particular arguments diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index f99b2845f882..e52910dd0d66 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -86,8 +86,6 @@ See :py:class:`~tvm.relay.ty.TupleType` for its definition and documentation. Type Parameter ~~~~~~~~~~~~~~ -.. *note*: Type parameters are not yet implemented - Type parameters represent placeholder types used for polymorphism in functions. Type parameters are specified according to *kind*: Kinds include general types (such as tensor types and tuple types), shapes, and data types. Relay enforces @@ -108,7 +106,7 @@ be substituted for `(10, 10)` at the call site below: plus<(10, 10)>(%a, %b) -See :py:class:`~tvm.relay.ty.TypeParam` for its definition and documentation. +See :py:class:`~tvm.relay.ty.TypeVar` for its definition and documentation. Type Constraint ~~~~~~~~~~~~~~~ From ad9c30c42ba175c606a0f280651955bba7f41a64 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 10 Dec 2018 16:13:56 -0800 Subject: [PATCH 08/36] Mistake in example code --- docs/langref/relay_type.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index e52910dd0d66..1b24c9541d62 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -78,8 +78,9 @@ For example, in the below code, :code:`%t` is of type and :code:`%c` is of type `Tensor`. .. code-block:: python - let %t = (Constant(0, bool, ()), Constant(1, float32, (10, 10))); - let %c = %t.1 + let %t = (Constant(0, bool, (10, 10)), Constant(1, float32, (10, 10))); + let %c = %t.1; + %c See :py:class:`~tvm.relay.ty.TupleType` for its definition and documentation. From 1aabbc5e2c10034812b180c08cb829e88bc2da0d Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Mon, 10 Dec 2018 16:46:41 -0800 Subject: [PATCH 09/36] Shape should precede dt in all examples --- docs/langref/relay_expr.rst | 44 ++++++++++++++++++------------------- docs/langref/relay_type.rst | 10 ++++----- 2 files changed, 27 insertions(+), 27 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 81c4735ab074..cd975a6c55a8 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -110,25 +110,25 @@ on certain types: .. code-block:: python - def @add(%x: Tensor, %y: Tensor) -> Tensor { - %x + %y + def @plus(%x: Tensor<(10, 10), float32>, %y: Tensor<(10, 10), float32>) + -> Tensor<(10, 10), float32> { + add(%x, %y) } -A parameter is just a local variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally annotated -with a type. Parameters are written as :code:`%x : T`. +A function parameter is just a local variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally +annotated with a type. Parameters are written as :code:`%x : T`. When the type information is omitted, we will attempt to infer the most general type for the users. This property is known as generalization: for a definition without explicit annotations, we will attempt to assign the most general type. When the -return type is omitted, we will infer the return type based on the text of the -program. +return type is omitted, we will infer the return type based on the function body. We can directly construct type-polymorphic definitions by writing down a set of type parameters for a definition. For example, one can define a polymorphic identity function for tensors as follows: .. code-block:: python - def @id(%x: Tensor) { + def @id(%x: Tensor) { %x } @@ -221,7 +221,7 @@ members. (a, b, c) : Tuple - (add(add(a, b), c), d) : Tuple, Tensor> + (add(add(a, b), c), d) : Tuple, Tensor<(100, 100), float32>> See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. @@ -248,8 +248,8 @@ use nearly the same syntax, but do not have a globally unique name. .. code-block:: python - fun (%x : Tensor, y: Tensor - -> Tensor { add(%x, %y) } + fun (%x : Tensor<(10, 10), float32>, y: Tensor<(10, 10), float32> + -> Tensor<(10, 10), float32> { add(%x, %y) } Note that function expressions evaluate to a closure. Closures are values that are represented as a pair of a local environment @@ -263,14 +263,14 @@ of zero values because the closure for :code:`%f` stores the value of .. code-block:: let %g = fun () { - let %x = Constant(0, float32, (10, 10)); + let %x = Constant(0, (10, 10), float32); # x is a free variable in the below function fun (%y) { multiply(%y, %x) } }; # the %x in %g's body is not in scope anymore - # %f is a closure where %x maps to Constant(0, float32, (10, 10)) + # %f is a closure where %x maps to Constant(0, (10, 10), float32) let %f = %g(); - let %x = Constant(1, float32, (10, 10)); + let %x = Constant(1, (10, 10), float32); let %z = %f(%x) A recursive function expression can be defined using a :code:`let` binding, @@ -278,11 +278,11 @@ as here: .. code-block:: python - let %fact = fun (%x : Tensor) -> Tensor { - if (equal(%x, Constant(1, float32, (10, 10))) { - Constant(0, float32, (10, 10)) + let %fact = fun (%x : Tensor<(10, 10), float32>) -> Tensor<(10, 10), float32> { + if (equal(%x, Constant(1, (10, 10), float32)) { + Constant(0, (10, 10), float32) } else { - multiply(%x, %fact(subtract(%x, Constant(1, float32, (10, 10)))) + multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32))) } }; %fact(10) @@ -313,7 +313,7 @@ of shape (10, 10) where all elements are 2: .. code-block:: python - let %x : Tensor = Consantt(1, float32, (10, 10)); + let %x : Tensor<(10, 10), float32> = Constant(1, (10, 10), float32); add(%x, %x) A sequence of :code:`let` bindings can be considered as a dataflow graph, @@ -377,14 +377,14 @@ If-Then-Else Relay has a simple if-then-else expression that allows programs to branch on a single value of type :code:`bool`, i.e., a zero-rank -tensor of booleans (:code:`Tensor`). +tensor of booleans (:code:`Tensor<(), bool>`). .. code-block:: python - if (sum(equal(t, u))) { - return x: + if (equal(%t, %u)) { + %t } else { - return y; + %u } Since if-then-else branches are expressions, they may appear inline diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index 1b24c9541d62..38a7862307ae 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -57,7 +57,7 @@ For example, here is a simple concrete tensor type corresponding to a 10-by-10 t .. code-block:: python - Tensor + Tensor<(10, 10), float32> See :py:class:`~tvm.relay.ty.TensorType` for its definition and documentation. @@ -74,11 +74,11 @@ Because a tuple type is of statically known size, the type of a tuple projection is simply the corresponding index into the tuple type. For example, in the below code, :code:`%t` is of type -`Tuple, Tensor>` -and :code:`%c` is of type `Tensor`. +`Tuple, Tensor<(10, 10), float32>>` +and :code:`%c` is of type `Tensor<(10, 10), float32>`. .. code-block:: python - let %t = (Constant(0, bool, (10, 10)), Constant(1, float32, (10, 10))); + let %t = (Constant(0, (), bool), Constant(1, (10, 10), float32)); let %c = %t.1; %c @@ -101,7 +101,7 @@ be substituted for `(10, 10)` at the call site below: .. code-block:: python - def @plus(%t1 : Tensor, %t2 : Tensor) { + def @plus(%t1 : Tensor, %t2 : Tensor) { add(%t1, %t2) } plus<(10, 10)>(%a, %b) From 8e97f2ad6123d4e378d9c1e878cc616cef742729 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 20 Dec 2018 13:58:40 -0800 Subject: [PATCH 10/36] Bring if-else, tuple type, and tensor type syntax in line with text format --- docs/langref/relay_expr.rst | 37 ++++++++++++++++++------------------- docs/langref/relay_type.rst | 8 ++++---- 2 files changed, 22 insertions(+), 23 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index cd975a6c55a8..7866b6272eb4 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -110,8 +110,8 @@ on certain types: .. code-block:: python - def @plus(%x: Tensor<(10, 10), float32>, %y: Tensor<(10, 10), float32>) - -> Tensor<(10, 10), float32> { + def @plus(%x: Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32]) + -> Tensor[(10, 10), float32] { add(%x, %y) } @@ -128,7 +128,7 @@ a set of type parameters for a definition. For example, one can define a polymorphic identity function for tensors as follows: .. code-block:: python - def @id(%x: Tensor) { + def @id(%x: Tensor[s, bt]) { %x } @@ -219,9 +219,10 @@ members. .. code-block:: python - (a, b, c) : Tuple + (a, b, c) : (Tensor[(10, 10), float32], Tensor[(10, 10), float32], Tensor[(10, 10), float32]) + d : Tensor[(100, 100), float32] - (add(add(a, b), c), d) : Tuple, Tensor<(100, 100), float32>> + (add(add(a, b), c), d) : (Tensor[(10, 10), float32], Tensor[(100, 100), float32]) See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. @@ -248,8 +249,8 @@ use nearly the same syntax, but do not have a globally unique name. .. code-block:: python - fun (%x : Tensor<(10, 10), float32>, y: Tensor<(10, 10), float32> - -> Tensor<(10, 10), float32> { add(%x, %y) } + fn (%x : Tensor[(10, 10), float32], y: Tensor[(10, 10), float32] + -> Tensor[(10, 10), float32] { add(%x, %y) } Note that function expressions evaluate to a closure. Closures are values that are represented as a pair of a local environment @@ -262,10 +263,10 @@ of zero values because the closure for :code:`%f` stores the value of .. code-block:: - let %g = fun () { + let %g = fn () { let %x = Constant(0, (10, 10), float32); # x is a free variable in the below function - fun (%y) { multiply(%y, %x) } + fn (%y) { multiply(%y, %x) } }; # the %x in %g's body is not in scope anymore # %f is a closure where %x maps to Constant(0, (10, 10), float32) @@ -278,12 +279,11 @@ as here: .. code-block:: python - let %fact = fun (%x : Tensor<(10, 10), float32>) -> Tensor<(10, 10), float32> { - if (equal(%x, Constant(1, (10, 10), float32)) { + let %fact = fun (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { + if (equal(%x, Constant(1, (10, 10), float32)) Constant(0, (10, 10), float32) - } else { - multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32))) - } + else + multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32))) }; %fact(10) @@ -313,7 +313,7 @@ of shape (10, 10) where all elements are 2: .. code-block:: python - let %x : Tensor<(10, 10), float32> = Constant(1, (10, 10), float32); + let %x : Tensor[(10, 10), float32] = Constant(1, (10, 10), float32); add(%x, %x) A sequence of :code:`let` bindings can be considered as a dataflow graph, @@ -377,15 +377,14 @@ If-Then-Else Relay has a simple if-then-else expression that allows programs to branch on a single value of type :code:`bool`, i.e., a zero-rank -tensor of booleans (:code:`Tensor<(), bool>`). +tensor of booleans (:code:`Tensor[(), bool]`). .. code-block:: python - if (equal(%t, %u)) { + if (equal(%t, %u)) %t - } else { + else %u - } Since if-then-else branches are expressions, they may appear inline wherever any other expression may be expected, like invocations of diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index 38a7862307ae..042c79973a99 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -57,7 +57,7 @@ For example, here is a simple concrete tensor type corresponding to a 10-by-10 t .. code-block:: python - Tensor<(10, 10), float32> + Tensor[(10, 10), float32] See :py:class:`~tvm.relay.ty.TensorType` for its definition and documentation. @@ -74,8 +74,8 @@ Because a tuple type is of statically known size, the type of a tuple projection is simply the corresponding index into the tuple type. For example, in the below code, :code:`%t` is of type -`Tuple, Tensor<(10, 10), float32>>` -and :code:`%c` is of type `Tensor<(10, 10), float32>`. +`(Tensor[(), bool], Tensor[(10, 10), float32])` +and :code:`%c` is of type `Tensor[(10, 10), float32]`. .. code-block:: python let %t = (Constant(0, (), bool), Constant(1, (10, 10), float32)); @@ -101,7 +101,7 @@ be substituted for `(10, 10)` at the call site below: .. code-block:: python - def @plus(%t1 : Tensor, %t2 : Tensor) { + def @plus(%t1 : Tensor[s, float32], %t2 : Tensor[s, float32]) { add(%t1, %t2) } plus<(10, 10)>(%a, %b) From b7f25eff33bd1046b0fbb09a23439270ca14dd91 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 20 Dec 2018 14:04:15 -0800 Subject: [PATCH 11/36] Typo --- docs/langref/relay_expr.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 7866b6272eb4..5307e75cef8d 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -57,7 +57,7 @@ the name :code:`%a` is "shadowed," meaning all references to references to :code:`%a` in the outer scope continue to refer to the previous one. -(Note that in Relay's implemetnation, each definition of a local variable +(Note that in Relay's implementation, each definition of a local variable creates a new :py:class:`~tvm.relay.expr.Var`, so a shadowed local variable, despite having the same name as one in an outer scope, will be a different object. This allows for comparing local variables by pointer identity with the From 1a2e89dca9bcec9995da14f9ba8711e9bdec7e8f Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 20 Dec 2018 15:35:59 -0800 Subject: [PATCH 12/36] Typo pass in relay_expr --- docs/langref/relay_expr.rst | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 5307e75cef8d..5b86709a8449 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -33,7 +33,7 @@ Global Variable ~~~~~~~~~~~~~~~~~~ Global identifiers are prefixed by the `@` sigil, such as "`@global`". -A global identifier always references a globally visibly definition contained in the environment. +A global identifier always references a globally visible definition contained in the environment. Global identifiers must be unique. See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation @@ -160,13 +160,10 @@ Operators ========= An operator is a primitive operation not defined in the Relay -language. Operators are declaredi n the global operator +language. Operators are declared in the global operator registry in C++. Many common operators are backed by TVM's Tensor Operator Inventory (`TOPI `__). -but registered in the global environment in either Python -or C++. Implementations of operators are typically backed by TVM's TOPI. - An operator requires a user to provide an implementation of the operator, its type, and any other desired metadata. The operator registry is a column-based store where @@ -368,7 +365,7 @@ type checking. Note that all type relations in the function type must hold at each call site. Because relations are checked at call sites, this means that the relations are checked against the types of the particular arguments -at that call site, so this is also allows for a form of polymorphism. +at that call site, so this also allows for a form of polymorphism. See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. From 5344b791f56d1ad5b6cdfaaa3c0ce44c2efc40b8 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 20 Dec 2018 16:25:58 -0800 Subject: [PATCH 13/36] Correct typos and rephrasing some descriptions in relay_type --- docs/langref/relay_type.rst | 57 +++++++++++++++++++++---------------- 1 file changed, 33 insertions(+), 24 deletions(-) diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index 042c79973a99..cbd71cd93734 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -5,27 +5,33 @@ Relay's Type System We have briefly introduced types while detailing the the expression language of Relay, but have not yet described the type system. Relay is a statically typed and type-inferred language, allowing programs to -be typed with a minimal requirement of explicit type information. +be typed with a minimal requirement of explicit type annotations. Static types are useful when performing compiler optimizations because they -communicate properties about the data we manipulate, such as runtime shape, -data layout, and storage without needing to run the program. Additionally, -static typing is useful for determining the - -Relay's type system features a form of depending typing for shapes to -replace the dynamic shape inference used in NNVM and most other machine -learning IRs. Treating tensor shapes as types allows Relay to perform -more powerful reasoning at compile time; in particular, Relay can statically -reason about operations whose output shapes vary based on the input shapes -in complex ways. Statically reasoning about shapes in this manner allows +communicate properties about the data a program manipulates, such as runtime +shape, data layout, and storage, without needing to run the program. + +Relay's type system features a form of dependent typing for shapes. Treating tensor +shapes as types allows Relay to perform more powerful reasoning at compile time; +in particular, Relay can statically reason about operations whose output shapes +vary based on the input shapes in complex ways. Casting shape inference as a type +inference problem allows Relay to infer the shapes of all tensors at compile time, +including in programs that use branching and function calls. + +Statically reasoning about shapes in this manner allows Relay to be ahead-of-time compiled and provides much more information about -tensors for optimizations furhter in the compilation pipeline. +tensors for optimizations further in the compilation pipeline. Such optimizations +can be implemented as passes, which are Relay-to-Relay AST transformations, and +may use the inferred types (e.g., shape information) for making decisions about +program transformations. For instance, `src/relay/pass/fuse_ops.cc` gives +an implementation of a pass that uses inferred tensor shapes to replace invocations +of operators in a Relay program with fused operator implementations. Reasoning about tensor types in Relay is encoded using type relations, which means that the bulk of type checking in Relay is constraint solving (ensuring that all type relations are satisfied at call sites). Type relations offer a flexible and relatively simple way of making the power of dependent typing available in Relay -without greatly increasing the complexity of Relay's type AST. +without greatly increasing the complexity of Relay's type system. Types ===== @@ -48,10 +54,12 @@ Tensors are typed according to data type and shape. At present, these use TVM's data types and shapes, but in the future, Relay may include a separate AST for shapes. In particular, data types include `bool`, `float32`, `int8` and various other bit widths. Shapes are given as tuples of dimensions (TVM `IndexExpr`), -such as `(5, 5)`; note, though, that TVM shapes can also include variables and -arithmetic expressions including variables, so Relay's constraint solving phase -will attempt to find assignments to all shape variables to ensure all shapes will -be concrete before running a program. +such as `(5, 5)`; scalars are also given tuple types and have a shape of `()`. + +Note, though, that TVM shapes can also include variables and arithmetic expressions +including variables, so Relay's constraint solving phase will attempt to find +assignments to all shape variables to ensure all shapes will be concrete before +running a program. For example, here is a simple concrete tensor type corresponding to a 10-by-10 tensor of 32-bit floats: @@ -67,8 +75,7 @@ Tuple Type A type of a tuple in Relay. Just as a tuple is simply a sequence of values of statically known length, the type -of the tuple consists of a sequence of types corresponding to the type of each member -of the tuple. +of the tuple consists of a sequence of the types corresponding to each member of the tuple. Because a tuple type is of statically known size, the type of a tuple projection is simply the corresponding index into the tuple type. @@ -105,7 +112,7 @@ be substituted for `(10, 10)` at the call site below: add(%t1, %t2) } plus<(10, 10)>(%a, %b) - + See :py:class:`~tvm.relay.ty.TypeVar` for its definition and documentation. @@ -120,6 +127,7 @@ See :py:class:`~tvm.relay.ty.TypeConstraint` for its definition and documentatio Function Type ~~~~~~~~~~~~~ + A function type in Relay, see `tvm/relay/type.h` for more details. This is the type assigned to functions in Relay. A function type @@ -127,7 +135,7 @@ consists of a list of type parameters, a set of type constraints, a sequence of argument types, and a return type. We informally write function types as: -`fun(arg_types) -> ret_type where type_constraints` +`fn(arg_types) -> ret_type where type_constraints` A type parameter in the function type may appear in the argument types or the return types. Additionally, each of the type constraints @@ -149,10 +157,11 @@ in these cases. A type relation :code:`R` is an n-ary-input, single-output relation over types. Namely, :code:`R` specifies a relationship between its argument -types and outputs either `true` if the relationship holds and `false` +types and outputs `true` if the relationship holds and `false` if it fails to hold. Types given to a relation may be incomplete or -include shape variables, so it may be possible to assign values to -incomplete types and shape variables such that a relation can hold. +include shape variables, so type inference must assign appropriate +values to incomplete types and shape variables for necessary relations +to hold, if such values exist. For example we can define an identity relation to be: From 7509d0136ce3b36c7e49ab16f9cb9c427c1ae978 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Fri, 21 Dec 2018 14:11:15 -0800 Subject: [PATCH 14/36] If blocks should have braces --- docs/langref/relay_expr.rst | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 5b86709a8449..30f9a4e8cd7f 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -277,10 +277,11 @@ as here: .. code-block:: python let %fact = fun (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { - if (equal(%x, Constant(1, (10, 10), float32)) + if (equal(%x, Constant(1, (10, 10), float32)) { Constant(0, (10, 10), float32) - else - multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32))) + } else { + multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32)))) + } }; %fact(10) @@ -378,10 +379,11 @@ tensor of booleans (:code:`Tensor[(), bool]`). .. code-block:: python - if (equal(%t, %u)) + if (equal(%t, %u)) { %t - else + } else { %u + } Since if-then-else branches are expressions, they may appear inline wherever any other expression may be expected, like invocations of From 8faa741fd3ab9480ad5bd4518f6f331f348056d2 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Fri, 21 Dec 2018 14:19:12 -0800 Subject: [PATCH 15/36] Include Relay intro in the section index --- docs/langref/index.rst | 34 ++++++++++++++++++++++++++++++++-- docs/langref/relay_intro.rst | 25 ------------------------- 2 files changed, 32 insertions(+), 27 deletions(-) delete mode 100644 docs/langref/relay_intro.rst diff --git a/docs/langref/index.rst b/docs/langref/index.rst index 4120dd4004c1..00952b174138 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -3,11 +3,41 @@ Language Reference This document provides references to embedded languages in the TVM stack. +Hybrid Script +------------- + +The below page describes the TVM hybrid script front-end, +which uses software emulation to support some constructs not +officially supported in TVM. + +.. toctree:: + :maxdepth: 2 + + hybrid_script + + + +Introduction to Relay +--------------------- + +Relay is a functional, differentiable programming language that has been +designed to be an expressive intermediate representation for machine +learning systems. It features support for closures, control flow, and +recursion, thus allowing for representing more complex models directly +in Relay. Relay also includes a form of dependent typing using type +relations in order to handle shape analysis for operators with complex +requirements on argument shapes. + +Additionally, Relay is designed to be easily extensible by +machine learning researchers and practitioners in order to facilitate +the inclusion and development of new large-scale program transformations +and optimizations. + +The below pages describe the grammar, type system, and operators in Relay, respectively. + .. toctree:: :maxdepth: 2 - relay_intro relay_expr relay_type relay_op - hybrid_script diff --git a/docs/langref/relay_intro.rst b/docs/langref/relay_intro.rst deleted file mode 100644 index ad9d1a5236db..000000000000 --- a/docs/langref/relay_intro.rst +++ /dev/null @@ -1,25 +0,0 @@ -===================== -Introduction to Relay -===================== - -Relay is a functional, differentiable programming language that has been -designed to be an expressive intermediate representation for machine -learning systems. It features support for closures, control flow, and -recursion, thus allowing for representing more complex models directly -in Relay. Relay also includes a form of dependent typing using type -relations in order to handle shape analysis for operators with complex -requirements on argument shapes. - -Additionally, Relay is designed to be easily extensible by -machine learning researchers and practitioners in order to facilitate -the inclusion and development of new large-scale program transformations -and optimizations. - -The below pages describe the grammar, type system, and operators in Relay, respectively. - -.. toctree:: - :maxdepth: 2 - - relay_expr - relay_type - relay_op From 853fb70d955f0e155fc86045c56f0d8803cdd81b Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Fri, 21 Dec 2018 15:33:37 -0800 Subject: [PATCH 16/36] Add subsection on Relay graph bindings --- docs/langref/relay_expr.rst | 45 +++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 30f9a4e8cd7f..3d1ff809e62d 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -330,6 +330,51 @@ dependency on the other: See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. +Graph Bindings +~~~~~~~~~~~~~~ + +A :code:`let` binding creates a named variable that is bound to the given value +and scoped to the subsequent expression. By contrast, a graph binding allows for +explicitly constructing dataflow graphs in a Relay program by binding an expression +(graph node) directly to a temporary variable, which is not scoped. This has the +semantics of substituting the expression wherever the variable appears, even though +the graph node will only be evaluated once by the compiled program. + +These bindings allow for a style of programming that corresponds to that already +employed by NNVM and other dataflow graph-based input formats. The fact that the variables +are not scoped offers some flexibility in evaluation order compared to :code:`let` +bindings, though this can also introduce some ambiguity in programs (`this developer +page`__ includes more detailed discussion of +this nuance). + +In Relay's text format, a graph binding can be written as below (note the lack of a +:code:`let` keyword and a semicolon): + +.. code-block:: python + + %1 = add(%a, %b) + %2 = add(%1, %1) + multiply(%2, %2) + +Graph bindings are not represented as an AST node in Relay, but rather as meta-variables set +to reference AST nodes. For example, a program like the above could be constructed in Relay's +Python front-end by setting *Python variables* equal to the corresponding Relay AST node and +using the variables repeatedly, as below (a C++ program using the corresponding API bindings +could accomplish the same thing): + +.. code-block:: python + + sum1 = relay.add(a, b) + sum2 = relay.add(sum1, sum1) + relay.multiply(sum2, sum2) + +For development purposes and to enable certain optimizations, Relay includes passes to +convert between dataflow graphs defined using graph bindings and programs with :code:`let` +bindings in A-normal form, employed by many compiler optimizations from the functional +programming community (see `"The Essence of Compiling with Continuations" by +Flanagan *et al*`__ for a discussion +of the A-normal form). + ======================= Control Flow Expression ======================= From 2c8efbf6f14297dc4c6c99e24d738575da236348 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 22 Dec 2018 12:24:14 -0800 Subject: [PATCH 17/36] Add internal hyperlinks to Relay dev guide and operator tutorial --- docs/langref/relay_expr.rst | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 3d1ff809e62d..9ed6c3f3867c 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -188,6 +188,10 @@ See :py:class:`~tvm.relay.op.Op` for the definition and documentation of operator nodes, demonstrating the infrastructure for registering operator metadata. The other files in :py:class:`~tvm.relay.op` give handles for generating a call to various pre-registered operators. +The `tutorial on adding operators to Relay`__ shows how to add further +operators into the language. + +__ `Adding an Operator to Relay`_ Dataflow Fragment ================= @@ -336,16 +340,19 @@ Graph Bindings A :code:`let` binding creates a named variable that is bound to the given value and scoped to the subsequent expression. By contrast, a graph binding allows for explicitly constructing dataflow graphs in a Relay program by binding an expression -(graph node) directly to a temporary variable, which is not scoped. This has the +(graph node) directly to a temporary variable, which is not scoped. Each reference +to the variable corresponds to an edge in the dataflow graph. This has the semantics of substituting the expression wherever the variable appears, even though the graph node will only be evaluated once by the compiled program. These bindings allow for a style of programming that corresponds to that already employed by NNVM and other dataflow graph-based input formats. The fact that the variables are not scoped offers some flexibility in evaluation order compared to :code:`let` -bindings, though this can also introduce some ambiguity in programs (`this developer -page`__ includes more detailed discussion of -this nuance). +bindings, though this can also introduce some ambiguity in programs (the +`developer introduction to the Relay IR`__ includes more detailed discussion +of this nuance). + +__ `Introduction to Relay IR`_ In Relay's text format, a graph binding can be written as below (note the lack of a :code:`let` keyword and a semicolon): From 2a59e6dfdca9af5ae577b02f3617183a2488dbe0 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 22 Dec 2018 21:07:01 -0800 Subject: [PATCH 18/36] Incorporate @joshpoll's suggestions in relay_expr --- docs/langref/relay_expr.rst | 83 ++++++++++++++++++++++--------------- 1 file changed, 50 insertions(+), 33 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 9ed6c3f3867c..a75bf824a21a 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -15,24 +15,19 @@ as well as give details of their semantics. Variables ========= -Relay allows for local and global variables. Our design is based on -that of LLVM, which differentiates between identifier types; a writer of -optimizations can thus determine what a variable references -simply by knowing the kind of identifier. +Inspired by LLVM, Relay explicitly distinguishes between local and +global variables both in the AST and in the text format. In the text format, +global and local variables are distinguished by prefixes, or sigils. +Global variables are prefixed with :code:`@` and local variables with :code:`%`. -Global variables are written with `@`, local variables are written -with `%`, and variables written without a sigil correspond to operator -names. - -The distinction between global and local identifiers -makes certain kinds of transformation easier. For example, -inlining a global definition requires no analysis: simply inlining -the definition suffices. +This explicit distinction makes certain optimizations easier to implement. +For example, inlining a global definition requires no analysis: simply +substituting the definition suffices. Global Variable ~~~~~~~~~~~~~~~~~~ -Global identifiers are prefixed by the `@` sigil, such as "`@global`". +Global identifiers are prefixed by the :code:`@` sigil, such as ":code:`@global`". A global identifier always references a globally visible definition contained in the environment. Global identifiers must be unique. @@ -40,22 +35,27 @@ See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation and documentation. Local Variable -~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~ Local identifiers are prefixed by the :code:`%` sigil, such as ":code:`%local`". A local identifier always references -a function argument or a variable bound in a :code:`let` expression. -A local variable will be scoped to the function where it -appears or the :code:`let` expression where it is bound, respectively. - -Suppose the local variable :code:`%a` has been defined in a scope -and within that scope, a :code:`let` expression binding to a variable -:code:`%a` appears. This is permitted, as in most functional languages. -In the scope of the :code:`let` expression (the inner scope), -the name :code:`%a` is "shadowed," meaning all references to -:code:`%a` in the inner scope refer to the later defintion, while +a function argument or a variable bound in a :code:`let` expression, +and will be scoped to the function where it appears or the :code:`let` +expression where it is bound, respectively. + +In the below code segment, notice that :code:`%a` is defined twice. This is +permitted, as in most functional languages; in the scope of the second +:code:`let` expression, the name :code:`%a` is "shadowed," meaning all +references to :code:`%a` in the inner scope refer to the later defintion, while references to :code:`%a` in the outer scope continue to refer to -the previous one. +the first one. + +.. code-block:: python + def @f(%a) { + let %b = %a; + let %a = add(%a, %a); + multiply(%a, %b) + } (Note that in Relay's implementation, each definition of a local variable creates a new :py:class:`~tvm.relay.expr.Var`, so a shadowed local variable, @@ -76,11 +76,11 @@ Relay will attempt to infer the most general types where types are omitted. Functions in Relay act similarly to procedures or functions in -other programming language and serve to generalize the concept +other programming languages and serve to generalize the concept of a named subgraph. -Functions defined in the manner described in this subsection are -of global scope; anonymous functions will be discussed later, though +Functions defined in the manner described in this subsection have +global scope; anonymous functions will be discussed later, though their mechanics are nearly identical. Note that global functions may be recursive; that is, within the function's body, the function's identifier refers back to the function unless it is shadowed in a :code:`let` @@ -120,12 +120,27 @@ annotated with a type. Parameters are written as :code:`%x : T`. When the type information is omitted, we will attempt to infer the most general type for the users. This property is known as generalization: for a definition without -explicit annotations, we will attempt to assign the most general type. When the -return type is omitted, we will infer the return type based on the function body. +explicit annotations, we will attempt to assign the most general type to the +parameters and return type based on the function body and call sites. + +.. *Note: type parameter syntax is not yet supported in the text format.* + +A function may also be given a set of type parameters, which can be +substituted for specific types at call sites. Functions with +type parameters are *type polymorphic*; their return type or the types +of arguments they will accept can vary based on the type arguments +given at call sites. -We can directly construct type-polymorphic definitions by writing down -a set of type parameters for a definition. For example, one can define a -polymorphic identity function for tensors as follows: +For example, one can define a polymorphic identity function for +any Relay type as follows: + +.. code-block:: python + def @id(%x : t) -> t { + %x + } + +The below definition is also polymorphic, but restricts its +arguments to tensor types: .. code-block:: python def @id(%x: Tensor[s, bt]) { @@ -134,6 +149,8 @@ polymorphic identity function for tensors as follows: Notice that the return type is omitted and will be inferred. +.. *Note: :code:`where` syntax is not yet supported in the text format.* + A function may also be subject to one or more type relations, such as in the following: From 1c535ad73a6f84aeebb5eac3a5867f09c2575fbc Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 22 Dec 2018 21:09:16 -0800 Subject: [PATCH 19/36] Incorporate @joshpoll's suggestions in the langref index --- docs/langref/index.rst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index 00952b174138..a565b5a54218 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -23,15 +23,14 @@ Introduction to Relay Relay is a functional, differentiable programming language that has been designed to be an expressive intermediate representation for machine learning systems. It features support for closures, control flow, and -recursion, thus allowing for representing more complex models directly -in Relay. Relay also includes a form of dependent typing using type -relations in order to handle shape analysis for operators with complex +recursion, allowing Relay to directly represent more complex models. +Relay also includes a form of dependent typing using *type relations* +in order to handle shape analysis for operators with complex requirements on argument shapes. -Additionally, Relay is designed to be easily extensible by -machine learning researchers and practitioners in order to facilitate -the inclusion and development of new large-scale program transformations -and optimizations. +Relay is extensible by design and makes it easy for machine learning +researchers and practitioners to develop new large-scale program +transformations and optimizations. The below pages describe the grammar, type system, and operators in Relay, respectively. From c6b6b46a2b0987249af8f52c3d7b3db38561bf47 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 22 Dec 2018 21:15:03 -0800 Subject: [PATCH 20/36] Further edit in introduction to relay_expr --- docs/langref/relay_expr.rst | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index a75bf824a21a..41c8cb3d7146 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -4,10 +4,9 @@ Expressions in Relay The Relay IR is a pure, expression-oriented language with distinct dataflow and control flow language fragments. -The dataflow fragments of a program (i.e., those without -calls to recursive functions or branching) can be -viewed as a traditional computation graph when writing and -expressing transformations. +Each dataflow fragment of a program (i.e., the portions of the +program without recursive calls or branching) can be viewed as a +traditional computation graph when writing and expressing transformations. The below sections describe the different expressions in Relay as well as give details of their semantics. From cf7919c6d669d54517ce2c12dd591851954ae7b4 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Sat, 22 Dec 2018 21:17:58 -0800 Subject: [PATCH 21/36] A couple of further edits to the langref index suggested by @joshpoll --- docs/langref/index.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index a565b5a54218..c8ac577f5f2d 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -20,9 +20,9 @@ officially supported in TVM. Introduction to Relay --------------------- -Relay is a functional, differentiable programming language that has been +Relay is a functional, differentiable programming language designed to be an expressive intermediate representation for machine -learning systems. It features support for closures, control flow, and +learning systems. It supports for closures, control flow, and recursion, allowing Relay to directly represent more complex models. Relay also includes a form of dependent typing using *type relations* in order to handle shape analysis for operators with complex From 32331925aef5bf7d827b556ac955ab299bb0cb68 Mon Sep 17 00:00:00 2001 From: Josh Pollock Date: Tue, 25 Dec 2018 00:06:01 -0500 Subject: [PATCH 22/36] Apply numerous corrections by @joshpoll Co-Authored-By: slyubomirsky --- docs/langref/index.rst | 2 +- docs/langref/relay_expr.rst | 34 +++++++++++++++++----------------- docs/langref/relay_type.rst | 30 +++++++++++++++--------------- 3 files changed, 33 insertions(+), 33 deletions(-) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index c8ac577f5f2d..19327048a632 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -22,7 +22,7 @@ Introduction to Relay Relay is a functional, differentiable programming language designed to be an expressive intermediate representation for machine -learning systems. It supports for closures, control flow, and +learning systems. It supports closures, control flow, and recursion, allowing Relay to directly represent more complex models. Relay also includes a form of dependent typing using *type relations* in order to handle shape analysis for operators with complex diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 41c8cb3d7146..f69a2a9424bf 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -157,13 +157,13 @@ the following: def @plus(%x, %y) where Broadcast { add(%x, %y) } -In the above definition, the types of `%x` and `%y` and the return type -are subject to the `Broadcast` relation, meaning all three must be tensors +In the above definition, the types of :code:`%x` and :code:`%y` and the return type +are subject to the :code:`Broadcast` relation, meaning all three must be tensors and their shapes follow the elementwise broadcast relation. As with operators, the definitions of relations are not transparent to Relay and they are instead implemented externally in either C++ or Python. -As in the case of `Broadcast`, relations are used to express complicated +As in the case of :code:`Broadcast`, relations are used to express complicated constraints on types (especially tensor shapes). All function relations must hold at all call sites; type checking is thus treated as a constraint-solving problem. @@ -175,12 +175,12 @@ See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of Operators ========= -An operator is a primitive operation not defined in the Relay +An operator is a primitive operation, such as :code:`add` or :code:`conv2d`, not defined in the Relay language. Operators are declared in the global operator registry in C++. Many common operators are backed by TVM's Tensor Operator Inventory (`TOPI `__). -An operator requires a user to provide an implementation +To register an operator a user must provide an implementation of the operator, its type, and any other desired metadata. The operator registry is a column-based store where operators are keys, so any metadata (which might be referenced @@ -191,7 +191,7 @@ so operators may be called like any other function and have function types. In particular, operator types are registered using a single type relation (see the above subsection), typically a relation specialized to that operator. For example, the :code:`add` operator -is registered with the `Broadcast` relation, indicating that the +is registered with the :code:`Broadcast` relation, indicating that the arguments of :code:`add` must be tensors and that the return type is a tensor whose shape depends on those of its arguments. @@ -217,12 +217,12 @@ control flow. That is, any portion of a program comprised only of these expressions corresponds to a pure computation graph without control flow. Note that global and local variables are also part of the dataflow fragment. -Constants +Constant ~~~~~~~~~ This node represents a constant tensor value (see :py:mod:`~tvm.relay.Value` for more details). -The constants are represented as :py:class:`~tvm.NDArray`, +A constant is represented as a :py:class:`~tvm.NDArray`, allowing Relay to utilize TVM operators for constant evaluation. See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation. @@ -249,24 +249,24 @@ Tuple Projection A tuple must be indexed by an integer constant in order to extract a particular member of the tuple. Projections are 0-indexed. -For example, the below projection evaluates to :code:`b`: +For example, the below projection evaluates to :code:`%b`: .. code-block:: python - (a, b, c).1 + (%a, %b, %c).1 See :py:class:`~tvm.relay.expr.TupleGetItem` for its definition and documentation. Function Expressions ~~~~~~~~~~~~~~~~~~~~ -Functions are first class in Relay and can be used in any expression -position. Function expressions are the same as global functions and +Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples. +Function expressions are the same as global functions and use nearly the same syntax, but do not have a globally unique name. .. code-block:: python - fn (%x : Tensor[(10, 10), float32], y: Tensor[(10, 10), float32] + fn (%x : Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32] -> Tensor[(10, 10), float32] { add(%x, %y) } Note that function expressions evaluate to a closure. Closures @@ -289,7 +289,7 @@ of zero values because the closure for :code:`%f` stores the value of # %f is a closure where %x maps to Constant(0, (10, 10), float32) let %f = %g(); let %x = Constant(1, (10, 10), float32); - let %z = %f(%x) + %f(%x) // evaluates to `Constant(1, (10, 10), float32) A recursive function expression can be defined using a :code:`let` binding, as here: @@ -379,7 +379,7 @@ In Relay's text format, a graph binding can be written as below (note the lack o %2 = add(%1, %1) multiply(%2, %2) -Graph bindings are not represented as an AST node in Relay, but rather as meta-variables set +Unlike a let binding, a graph binding is not represented as an AST node in Relay, but rather as a meta-variable referencing its AST node value. to reference AST nodes. For example, a program like the above could be constructed in Relay's Python front-end by setting *Python variables* equal to the corresponding Relay AST node and using the variables repeatedly, as below (a C++ program using the corresponding API bindings @@ -399,10 +399,10 @@ Flanagan *et al*`__ for a d of the A-normal form). ======================= -Control Flow Expression +Control Flow Expressions ======================= -Control flow expressions allow the network topology to change +Control flow expressions allow the graph topology to change based on the value of previously executed expressions. Call diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index cbd71cd93734..826c01888244 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -2,16 +2,16 @@ Relay's Type System =================== -We have briefly introduced types while detailing the the expression language -of Relay, but have not yet described the type system. Relay is +We briefly introduced types while detailing Relay's expression language +, but have not yet described its type system. Relay is a statically typed and type-inferred language, allowing programs to -be typed with a minimal requirement of explicit type annotations. +be fully typed while requiring just a few explicit type annotations. Static types are useful when performing compiler optimizations because they communicate properties about the data a program manipulates, such as runtime shape, data layout, and storage, without needing to run the program. -Relay's type system features a form of dependent typing for shapes. Treating tensor +Relay's type system features a form of *dependent typing* for shapes. That is, its type system keeps track of the shapes of tensors in a Relay program. Treating tensor shapes as types allows Relay to perform more powerful reasoning at compile time; in particular, Relay can statically reason about operations whose output shapes vary based on the input shapes in complex ways. Casting shape inference as a type @@ -27,11 +27,11 @@ program transformations. For instance, `src/relay/pass/fuse_ops.cc` gives an implementation of a pass that uses inferred tensor shapes to replace invocations of operators in a Relay program with fused operator implementations. -Reasoning about tensor types in Relay is encoded using type relations, which means +Reasoning about tensor types in Relay is encoded using *type relations*, which means that the bulk of type checking in Relay is constraint solving (ensuring that all type relations are satisfied at call sites). Type relations offer a flexible and relatively simple way of making the power of dependent typing available in Relay -without greatly increasing the complexity of Relay's type system. +without greatly increasing the complexity of its type system. Types ===== @@ -75,7 +75,7 @@ Tuple Type A type of a tuple in Relay. Just as a tuple is simply a sequence of values of statically known length, the type -of the tuple consists of a sequence of the types corresponding to each member of the tuple. +of a tuple consists of a sequence of the types corresponding to each member of the tuple. Because a tuple type is of statically known size, the type of a tuple projection is simply the corresponding index into the tuple type. @@ -85,7 +85,7 @@ For example, in the below code, :code:`%t` is of type and :code:`%c` is of type `Tensor[(10, 10), float32]`. .. code-block:: python - let %t = (Constant(0, (), bool), Constant(1, (10, 10), float32)); + let %t = (False, Constant(1, (10, 10), float32)); let %c = %t.1; %c @@ -101,9 +101,9 @@ that types can only appear where their kind permits them; for instance, a shape or data type can only appear inside a tensor type, while only general types may appear inside a tensor or for a function's return and argument types. -Type parameters will be substituted with a concrete type at call sites. +Like normal parameters, concrete arguments must be given for type parameters at call sites. -For example, `s` below is a type paramter of kind `Shape` and it will +For example, `s` below is a type parameter of kind `Shape` and it will be substituted for `(10, 10)` at the call site below: .. code-block:: python @@ -155,9 +155,9 @@ tensor shapes in complex ways, such as broadcasting operators or :code:`flatten`, allowing Relay to statically reason about the shapes in these cases. -A type relation :code:`R` is an n-ary-input, single-output relation over -types. Namely, :code:`R` specifies a relationship between its argument -types and outputs `true` if the relationship holds and `false` +A type relation :code:`R` describes a relationship between the inputs and output types of a Relay function. +Namely, :code:`R` is a function on types that +outputs `true` if the relationship holds and `false` if it fails to hold. Types given to a relation may be incomplete or include shape variables, so type inference must assign appropriate values to incomplete types and shape variables for necessary relations @@ -178,7 +178,7 @@ If we have a relation like :code:`Broadcast` it becomes possible to type operators like :code:`add`: .. code-block:: python - add : fun(t1, t2) -> t3 + add : fn(t1, t2) -> t3 where Broadcast The inclusion of :code:`Broadcast` above indicates that the argument @@ -213,7 +213,7 @@ Incomplete Type ~~~~~~~~~~~~~~~ A type or portion of a type that is not yet known. -Only used during type inference: any omitted type annotation is +This is only used during type inference. Any omitted type annotation is replaced by an incomplete type, which will be replaced by another type at a later point. From a61ebca464dd2d855abc3a2cb601e45117b7cae0 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 00:21:06 -0500 Subject: [PATCH 23/36] Further clarification in langref index --- docs/langref/index.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index 19327048a632..58d41d9fe379 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -22,8 +22,9 @@ Introduction to Relay Relay is a functional, differentiable programming language designed to be an expressive intermediate representation for machine -learning systems. It supports closures, control flow, and -recursion, allowing Relay to directly represent more complex models. +learning systems. Relay supports closures, control flow, and +recursion, allowing it to directly represent more complex models +than can computation graph-based IRs. Relay also includes a form of dependent typing using *type relations* in order to handle shape analysis for operators with complex requirements on argument shapes. From 36fe8120da1fb898d86f1e3475518c862483bcc2 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 01:03:13 -0500 Subject: [PATCH 24/36] More small corrections to relay_expr --- docs/langref/relay_expr.rst | 116 +++++++++++++++++++++++------------- 1 file changed, 75 insertions(+), 41 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index f69a2a9424bf..9f24c18cdac6 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -5,7 +5,7 @@ Expressions in Relay The Relay IR is a pure, expression-oriented language with distinct dataflow and control flow language fragments. Each dataflow fragment of a program (i.e., the portions of the -program without recursive calls or branching) can be viewed as a +program without recursive calls, calls to recursive functions, or branching) can be viewed as a traditional computation graph when writing and expressing transformations. The below sections describe the different expressions in Relay @@ -50,11 +50,10 @@ references to :code:`%a` in the outer scope continue to refer to the first one. .. code-block:: python - def @f(%a) { - let %b = %a; - let %a = add(%a, %a); - multiply(%a, %b) - } +let %a = 1; +let %b = 2 * %a; // %b = 2 +let %a = %a + %a; // %a = 2. %a is shadowed +%a + %b // has value 2 + 2 = 4 (Note that in Relay's implementation, each definition of a local variable creates a new :py:class:`~tvm.relay.expr.Var`, so a shadowed local variable, @@ -195,11 +194,15 @@ is registered with the :code:`Broadcast` relation, indicating that the arguments of :code:`add` must be tensors and that the return type is a tensor whose shape depends on those of its arguments. -Operators are rendered without a sigil (e.g :code:`add`, :code:`subtract`) +Operators are rendered without a sigil (e.g :code:`conv2d`, :code:`flatten`) when pretty-printing Relay programs. Operators are explicitly contained in the program and are uniquely identifiable by pointer. +Note that common arithmetic operators such as :code:`add` and :code:`multiply` +may be written using the corresponding arithmetic operators in the text format +(e.g., :code:`+` or :code:`*`) as syntactic sugar. + See :py:class:`~tvm.relay.op.Op` for the definition and documentation of operator nodes, demonstrating the infrastructure for registering operator metadata. The other files in :py:class:`~tvm.relay.op` give @@ -215,7 +218,8 @@ Dataflow Fragment This subsection covers the set of Relay expressions that do not involve control flow. That is, any portion of a program comprised only of these expressions corresponds to a pure computation graph without control flow. -Note that global and local variables are also part of the dataflow fragment. +Note that global and local variables are also part of the dataflow fragment, +as are calls to non-recursive functions and operators. Constant ~~~~~~~~~ @@ -225,6 +229,11 @@ This node represents a constant tensor value A constant is represented as a :py:class:`~tvm.NDArray`, allowing Relay to utilize TVM operators for constant evaluation. +This node can also represent scalar constants, since +scalars are tensors with a shape of :code:`()`. In the text format, numerical +and boolean literals are thus syntactic sugar for constants encoding a +tensor type with a rank-zero shape. + See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation. Tuple @@ -236,10 +245,10 @@ members. .. code-block:: python - (a, b, c) : (Tensor[(10, 10), float32], Tensor[(10, 10), float32], Tensor[(10, 10), float32]) - d : Tensor[(100, 100), float32] - - (add(add(a, b), c), d) : (Tensor[(10, 10), float32], Tensor[(100, 100), float32]) +fn (%a : Tensor[(10, 10), float32], %b : float32, %c : Tensor[(100, 100), float32]) { + let %tup = (%a, %b); // type: (Tensor[(10, 10), float32], float32) + ((%tup.0 + %tup.1), %c) // type: (Tensor[(10, 10), float32], Tensor[(100, 100), float32]) +} See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. @@ -278,15 +287,15 @@ For example, in the below example, :code:`%z` will evaluate to a tensor of zero values because the closure for :code:`%f` stores the value of :code:`%x` at the pointer where :code:`%f` was defined. -.. code-block:: +.. code-block:: python let %g = fn () { let %x = Constant(0, (10, 10), float32); - # x is a free variable in the below function + // x is a free variable in the below function fn (%y) { multiply(%y, %x) } }; - # the %x in %g's body is not in scope anymore - # %f is a closure where %x maps to Constant(0, (10, 10), float32) + // the %x in %g's body is not in scope anymore + // %f is a closure where %x maps to Constant(0, (10, 10), float32) let %f = %g(); let %x = Constant(1, (10, 10), float32); %f(%x) // evaluates to `Constant(1, (10, 10), float32) @@ -296,14 +305,14 @@ as here: .. code-block:: python - let %fact = fun (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { - if (equal(%x, Constant(1, (10, 10), float32)) { - Constant(0, (10, 10), float32) + let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { + if (%x == Constant(0, (10, 10), float32)) { + Constant(1, (10, 10), float32) } else { - multiply(%x, %fact(subtract(%x, Constant(1, (10, 10), float32)))) + %x * %fact(%x - Constant(1, (10, 10), float32)) } }; - %fact(10) + %fact(Constant(10, (10, 10), float32)) See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. @@ -319,10 +328,11 @@ that may reference the bound identifier. If a type annotation on the bound variable is omitted, Relay attempts to infer the most general type permitted for the variable. -The bound variable in a :code:`let` expression is scoped to the let -expression's body. Note that the bound variable can only be -recursively referenced in the value in the case of a function -expression, as in the above subsection. +The bound variable in a :code:let expression is only in scope +in its body, except when the variable defines a function expression. +When a :code:let expression creates a function, the variable is also +in scope in its value to allow for recursively defined functions +(see the previous subsection). The value of a :code:`let` binding is the value of the final expression after evaluating the bindings it depends on. For example, in the @@ -332,7 +342,7 @@ of shape (10, 10) where all elements are 2: .. code-block:: python let %x : Tensor[(10, 10), float32] = Constant(1, (10, 10), float32); - add(%x, %x) + %x + %x A sequence of :code:`let` bindings can be considered as a dataflow graph, where the bindings are a series of sub-graphs connected @@ -344,9 +354,9 @@ dependency on the other: .. code-block:: python - let %x = add(%a, %b); - let %y = add(%c, %d); - multiply(%x, %y) + let %x = %a + %b); + let %y = %c + %d); + %x * %y See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. @@ -375,9 +385,9 @@ In Relay's text format, a graph binding can be written as below (note the lack o .. code-block:: python - %1 = add(%a, %b) - %2 = add(%1, %1) - multiply(%2, %2) + %1 = %a + %b) + %2 = %1 + %1 + %2 * %2 Unlike a let binding, a graph binding is not represented as an AST node in Relay, but rather as a meta-variable referencing its AST node value. to reference AST nodes. For example, a program like the above could be constructed in Relay's @@ -394,9 +404,9 @@ could accomplish the same thing): For development purposes and to enable certain optimizations, Relay includes passes to convert between dataflow graphs defined using graph bindings and programs with :code:`let` bindings in A-normal form, employed by many compiler optimizations from the functional -programming community (see `"The Essence of Compiling with Continuations" by -Flanagan *et al*`__ for a discussion -of the A-normal form). +programming community (see `"A-Normalization: Why and How" by +Matt Might`__ for an introduction +to the A-normal form). ======================= Control Flow Expressions @@ -427,14 +437,38 @@ has a function type: %fact(10) +.. *Note: type parameters are not yet supported in the text format.* + A type-polymorphic function can also include type arguments at a call site. The type arguments are substituted for type parameters when -type checking. +type checking. If a function is type-polymorphic and type arguments are not +given, type inference will attempt to infer type arguments if possible. +The following code gives examples of explicit and inferred type arguments: + +.. code-block:: python + + // %f : fn(a, b) -> c + let %x1 = f(True, False); + // %x1 is of type Tensor[(), bool] + let %x2 : () = f(%x1, %x1) + // the type arguments in the second call are inferred to be Note that all type relations in the function type must hold at each -call site. Because relations are checked at call sites, this means that -the relations are checked against the types of the particular arguments -at that call site, so this also allows for a form of polymorphism. +call site. Specifically, this means that the relation will be checked +against the specific types of the arguments at a given call site. This +is also a form of polymorphism, since there may be multiple valid +assignments of argument types and a return type so long as the relation +is satisfied. + +For example, if we have a function :code:`%f` that takes tensor arguments +and has the :code:`Broadcast` relation, then there are many different +shapes that the arguments in the below call could have that would satisfy +the type annotation: + +.. code-block:: python + + let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, $c); + %x See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. @@ -456,7 +490,7 @@ tensor of booleans (:code:`Tensor[(), bool]`). Since if-then-else branches are expressions, they may appear inline wherever any other expression may be expected, like invocations of the ternary operator in C-like languages. The if-then-else expression -evaluates to the value of the "then" branch if the condition value is -`True` and evaluates to the value of the "else" branch otherwise. +evaluates to the value of the "then" branch if the condition value +evaluates to `True` and evaluates to the value of the "else" branch otherwise. See :py:class:`~tvm.relay.expr.If` for its definition and documentation. From 7f6a13fd46d545fca47f193c8fda4c70c1755336 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 01:47:09 -0500 Subject: [PATCH 25/36] Further tweaks and more examples in relay_expr --- docs/langref/relay_expr.rst | 43 +++++++++++++++++++++++-------------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 9f24c18cdac6..7cf7833a3974 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -81,8 +81,7 @@ Functions defined in the manner described in this subsection have global scope; anonymous functions will be discussed later, though their mechanics are nearly identical. Note that global functions may be recursive; that is, within the function's body, the function's -identifier refers back to the function unless it is shadowed in a :code:`let` -expression. +identifier refers back to the function. A definition minimally consists of an identifier :code:`@id`, an empty set of parameters, and a body expression (:py:class:`~tvm.relay.expr.Expr`) @@ -298,7 +297,7 @@ of zero values because the closure for :code:`%f` stores the value of // %f is a closure where %x maps to Constant(0, (10, 10), float32) let %f = %g(); let %x = Constant(1, (10, 10), float32); - %f(%x) // evaluates to `Constant(1, (10, 10), float32) + %f(%x) // evaluates to `Constant(0, (10, 10), float32) A recursive function expression can be defined using a :code:`let` binding, as here: @@ -354,8 +353,8 @@ dependency on the other: .. code-block:: python - let %x = %a + %b); - let %y = %c + %d); + let %x = %a + %b; + let %y = %c + %d; %x * %y See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. @@ -380,17 +379,19 @@ of this nuance). __ `Introduction to Relay IR`_ +.. *Note: Graph bindings are not currently parsed by the text format.* + In Relay's text format, a graph binding can be written as below (note the lack of a :code:`let` keyword and a semicolon): .. code-block:: python - %1 = %a + %b) + %1 = %a + %b %2 = %1 + %1 %2 * %2 Unlike a let binding, a graph binding is not represented as an AST node in Relay, but rather as a meta-variable referencing its AST node value. -to reference AST nodes. For example, a program like the above could be constructed in Relay's +For example, a program like the above could be constructed in Relay's Python front-end by setting *Python variables* equal to the corresponding Relay AST node and using the variables repeatedly, as below (a C++ program using the corresponding API bindings could accomplish the same thing): @@ -423,19 +424,29 @@ meaning that they can be invoked via a function call. These consist of any expression that evaluates to a closure (i.e., function expressions or global functions) and Relay operators. -When a closure is called, the body is evaluated in the closure's stored -environment (i.e., using the stored values for free variables) with -local variable bindings added for each argument; the final value -obtained by evaluating the body is the call's return value. -In the case of operators, the implementation is opaque to Relay, -so the result is left up to the registered TVM implementation. +In terms of computation graphs, since a function corresponds to a named +subgraph, a function call effectively inserts the subgraph. Calls to +Relay operators or non-recursive functions are still dataflow expressions, +since the graph topology does not change based on their values, but recursive +calls are indeed control edges. -For example, we can call the previously defined `%fact` because it -has a function type: +The syntax of calls follows that used in C-like languages, demonstrated in the +example below: .. code-block:: python - %fact(10) + let c = 1; + let f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; + %f(10, 11) + +When a closure is called (see `Function Expressions`_ for a discussion of closures), +the closure's body is evaluated in the stored environment +(i.e., using the stored values for free variables) with +local variable bindings added for each argument; the final value +obtained by evaluating the body is the call's return value. +Thus, in the above example, the call evaluates to 22. +In the case of operators, the implementation is opaque to Relay, +so the result is left up to the registered TVM implementation. .. *Note: type parameters are not yet supported in the text format.* From c0c351f6ea456c19e0b5e0dd8649bb18ea862348 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 02:15:02 -0500 Subject: [PATCH 26/36] More tweaks and incorporated suggestions in relay_type --- docs/langref/relay_type.rst | 50 ++++++++++++++++++++++++------------- 1 file changed, 33 insertions(+), 17 deletions(-) diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index 826c01888244..aef830711c75 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -53,7 +53,7 @@ A concrete tensor type in Relay. Tensors are typed according to data type and shape. At present, these use TVM's data types and shapes, but in the future, Relay may include a separate AST for shapes. In particular, data types include `bool`, `float32`, `int8` and various -other bit widths. Shapes are given as tuples of dimensions (TVM `IndexExpr`), +other bit widths and numbers of lanes. Shapes are given as tuples of dimensions (TVM `IndexExpr`), such as `(5, 5)`; scalars are also given tuple types and have a shape of `()`. Note, though, that TVM shapes can also include variables and arithmetic expressions @@ -95,14 +95,23 @@ Type Parameter ~~~~~~~~~~~~~~ Type parameters represent placeholder types used for polymorphism in functions. -Type parameters are specified according to *kind*: Kinds include general types -(such as tensor types and tuple types), shapes, and data types. Relay enforces -that types can only appear where their kind permits them; for instance, a -shape or data type can only appear inside a tensor type, while only general types -may appear inside a tensor or for a function's return and argument types. +Type parameters are specified according to *kind*, corresponding to the types +those parameters are allowed to replace: + +- :code:`Type`, corresponding to top-level Relay types like tensor types, tuple types, and function types +- :code:`BaseType`, corresponding to the base type of a tensor (e.g., :code:`float32`, :code:`bool`) +- :code:`Shape`, corresponding to a tensor shape +- :code:`ShapeVar`, corresponding to variables within a tensor shape + +Relay's type system enforces that type parameters are only allowed to appear where their kind permits them, +so if type variable :code:`t` is of kind :code:`Type`, :code:`Tensor[t, float32]` is not a valid type. + +.. *Note: At present, only type parameters of kind :code:`Type` are supported.* Like normal parameters, concrete arguments must be given for type parameters at call sites. +.. *Note: type parameter syntax is not yet supported in the text format.* + For example, `s` below is a type parameter of kind `Shape` and it will be substituted for `(10, 10)` at the call site below: @@ -113,13 +122,12 @@ be substituted for `(10, 10)` at the call site below: } plus<(10, 10)>(%a, %b) - See :py:class:`~tvm.relay.ty.TypeVar` for its definition and documentation. Type Constraint ~~~~~~~~~~~~~~~ -Abstract class representing a type constraint, to be elaborated +This is an abstract class representing a type constraint, to be elaborated upon in further releases. Currently, type relations are the only type constraints provided; they are discussed below. @@ -168,7 +176,10 @@ For example we can define an identity relation to be: .. code-block:: prolog Identity(I, I) :- true -Or we can define the relation for :code:`flatten`: +It is usually convenient to type operators +in Relay by defining a relation specific to that operator that +encodes all the necessary constraints on the argument types +and the return type. For example, we can define the relation for :code:`flatten`: .. code-block:: prolog Flatten(Tensor(sh, bt), O) :- @@ -185,20 +196,22 @@ The inclusion of :code:`Broadcast` above indicates that the argument types and the return type must be tensors where the shape of `t3` is the broadcast of the shapes of `t1` and `t2`. The type system will accept any argument types and return type so long as they fulfill -:code:`Broadcast`. Hence, it is usually convenient to type operators -in Relay by defining a relation specific to that operator that -encodes all the necessary constraints on the argument types -and the return type. +:code:`Broadcast`. Note that the above example relations are written in Prolog-like syntax, but currently the relations must be implemented by users in C++ or Python. More specifically, Relay's type system uses an *ad hoc* solver for type relations in which type relations are actually implemented as C++ or Python functions that check whether the relation holds and -imperatively update any shape variables or incomplete types. The -functions are run as needed (if an input is updated) until one of the following holds: +imperatively update any shape variables or incomplete types. In the current +implementation, the functions implementing relations should return :code:`False` +if the relation fails to hold and :code:`True` if the relation holds or if +there is not enough information to determine whether it holds or not. + +The functions for all the relations are run as needed (if an input is updated) +until one of the following conditions holds: -1. All relations hold (typechecking succeeds). +1. All relations hold and no incomplete types remain (typechecking succeeds). 2. A relation fails to hold (a type error). 3. A fixpoint is reached where shape variables or incomplete types remain (either a type error or more type annotations may be needed). @@ -217,6 +230,9 @@ This is only used during type inference. Any omitted type annotation is replaced by an incomplete type, which will be replaced by another type at a later point. -.. note:: Known as a "type variable" in the type checking literature. +Incomplete types are known as "type variables" or "type holes" in the programming languages +literature. We use the name "incomplete type" in order to more clearly distinguish them from type +parameters: Type parameters must be bound to a function and are replaced with concrete type arguments (instantiated) +at call sites, whereas incomplete types may appear anywhere in the program and are filled in during type inference. See :py:class:`~tvm.relay.ty.IncompleteType` for its definition and documentation. From 4b45cd885abe41baa951a7885663d797e0216600 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 02:18:23 -0500 Subject: [PATCH 27/36] Typo in example --- docs/langref/relay_expr.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 7cf7833a3974..1ed1b54c9692 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -478,7 +478,7 @@ the type annotation: .. code-block:: python - let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, $c); + let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, %c); %x See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. From f26eeacb0dc18eee9f2237d1697f489ca46d037d Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 02:28:46 -0500 Subject: [PATCH 28/36] Further clarification on calls and control flow --- docs/langref/relay_expr.rst | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 1ed1b54c9692..95b527a1496b 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -218,7 +218,8 @@ This subsection covers the set of Relay expressions that do not involve control flow. That is, any portion of a program comprised only of these expressions corresponds to a pure computation graph without control flow. Note that global and local variables are also part of the dataflow fragment, -as are calls to non-recursive functions and operators. +as are calls to operators and functions whose bodies are also entirely in +the dataflow fragment. Constant ~~~~~~~~~ @@ -424,11 +425,12 @@ meaning that they can be invoked via a function call. These consist of any expression that evaluates to a closure (i.e., function expressions or global functions) and Relay operators. -In terms of computation graphs, since a function corresponds to a named -subgraph, a function call effectively inserts the subgraph. Calls to -Relay operators or non-recursive functions are still dataflow expressions, -since the graph topology does not change based on their values, but recursive -calls are indeed control edges. +In terms of dataflow graphs, if a function corresponds to a named +subgraph, a function call inserts the subgraph. This means that if a function's +body contains control flow, calling that function affects the graph topology based +on the values of the executed expressions, as does a recursive call. However, +calls to operators and functions whose bodies do not contain recursive calls +or control flow are still dataflow expressions. The syntax of calls follows that used in C-like languages, demonstrated in the example below: From ffef4c8aa840b123e3bb3092f043df73a676f4b6 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 02:52:52 -0500 Subject: [PATCH 29/36] Make dataflow vs control a section, reorganize relay_expr --- docs/langref/relay_expr.rst | 318 ++++++++++++++++++------------------ 1 file changed, 159 insertions(+), 159 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 95b527a1496b..7d6a3005a962 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -2,14 +2,36 @@ Expressions in Relay ==================== -The Relay IR is a pure, expression-oriented language with distinct -dataflow and control flow language fragments. -Each dataflow fragment of a program (i.e., the portions of the -program without recursive calls, calls to recursive functions, or branching) can be viewed as a -traditional computation graph when writing and expressing transformations. +The Relay IR is a pure, expression-oriented language. The below sections +describe the different expressions in Relay and give details of their semantics. + +Dataflow and Control Fragments +============================== + +For the purposes of comparing Relay to traditional computational graph-based IRs, it +can be useful to consider Relay exrpessions in terms of dataflow and control fragments. +Each portion of a Relay program containing expressions that only affect the dataflow can +be viewed as a traditional comptuation graph when writing and expressing transformations. + +The dataflow fragment covers the set of Relay expressions that do not involve +control flow. That is, any portion of a program containing only the following +constructs corresponds to a pure computation graph: +- `Variables`_ +- Tuple `Construction`_ and `Projection`_ +- `Let Bindings`_ +- `Graph Bindings`_ +- Calls to `Operators`_ -The below sections describe the different expressions in Relay -as well as give details of their semantics. +Control flow expressions allow the graph topology to change +based on the value of previously executed expressions. The control +fragment in Relay includes the following constructs: +- `If-Then-Else`_ Expressions +- Recursive Calls in Functions + +Because a function can be viewed as a subgraph from the point of view of computational graphs, +a call effectively substitutes in the subgraph. Thus, if a function's body is entirely within +the dataflow fragment, a call to that function is in the dataflow fragment; conversely, if the +function's body contains control flow, a call to that function is not part of the dataflow fragment. Variables ========= @@ -64,23 +86,26 @@ knowledge that the same local variable object corresponds to a different binding See :py:class:`~tvm.relay.expr.Var` for its implementation and documentation. +Functions +========= + +Functions in Relay act similarly to procedures or functions in +other programming languages and serve to generalize the concept +of a named subgraph. + +See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of function nodes. + Global Functions -================ +~~~~~~~~~~~~~~~~ -A function definition consists of a name, arguments, return type, +A global function definition consists of a name, arguments, return type, type parameters, and any applicable type relations. A function's return type and parameter types may be omitted; Relay will attempt to infer the most general types where types are omitted. -Functions in Relay act similarly to procedures or functions in -other programming languages and serve to generalize the concept -of a named subgraph. - Functions defined in the manner described in this subsection have -global scope; anonymous functions will be discussed later, though -their mechanics are nearly identical. Note that global functions may be -recursive; that is, within the function's body, the function's +global scope and may be recursive; that is, within the function's body, the function's identifier refers back to the function. A definition minimally consists of an identifier :code:`@id`, an empty set of @@ -168,7 +193,53 @@ type checking is thus treated as a constraint-solving problem. For more detail on type relations and their implementations, please see the documentation on typing in Relay. -See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of function nodes. +Function Expressions +~~~~~~~~~~~~~~~~~~~~ + +Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples. +Function expressions behave identically to global functions and use nearly the same syntax, +but do not have a globally unique name. + +.. code-block:: python + + fn (%x : Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32] + -> Tensor[(10, 10), float32] { add(%x, %y) } + +Note that function expressions evaluate to a closure. Closures +are values that are represented as a pair of a local environment +(storing the values for all variables defined outside the scope +of the function's body) and the function itself. + +For example, in the below example, :code:`%z` will evaluate to a tensor +of zero values because the closure for :code:`%f` stores the value of +:code:`%x` at the pointer where :code:`%f` was defined. + +.. code-block:: python + + let %g = fn () { + let %x = Constant(0, (10, 10), float32); + // x is a free variable in the below function + fn (%y) { multiply(%y, %x) } + }; + // the %x in %g's body is not in scope anymore + // %f is a closure where %x maps to Constant(0, (10, 10), float32) + let %f = %g(); + let %x = Constant(1, (10, 10), float32); + %f(%x) // evaluates to `Constant(0, (10, 10), float32) + +A recursive function expression can be defined using a :code:`let` binding, +as here: + +.. code-block:: python + + let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { + if (%x == Constant(0, (10, 10), float32)) { + Constant(1, (10, 10), float32) + } else { + %x * %fact(%x - Constant(1, (10, 10), float32)) + } + }; + %fact(Constant(10, (10, 10), float32)) Operators ========= @@ -211,18 +282,69 @@ operators into the language. __ `Adding an Operator to Relay`_ -Dataflow Fragment -================= +Call +==== + +Expressions with function types in Relay are "callable," +meaning that they can be invoked via a function call. These consist of +any expression that evaluates to a closure (i.e., function expressions +or global functions) and Relay operators. + +The syntax of calls follows that used in C-like languages, demonstrated in the +example below: + +.. code-block:: python + + let c = 1; + let f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; + %f(10, 11) + +When a closure is called (see `Function Expressions`_ for a discussion of closures), +the closure's body is evaluated in the stored environment +(i.e., using the stored values for free variables) with +local variable bindings added for each argument; the final value +obtained by evaluating the body is the call's return value. +Thus, in the above example, the call evaluates to 22. +In the case of operators, the implementation is opaque to Relay, +so the result is left up to the registered TVM implementation. -This subsection covers the set of Relay expressions that do not involve -control flow. That is, any portion of a program comprised only of these -expressions corresponds to a pure computation graph without control flow. -Note that global and local variables are also part of the dataflow fragment, -as are calls to operators and functions whose bodies are also entirely in -the dataflow fragment. +.. *Note: type parameters are not yet supported in the text format.* + +A type-polymorphic function can also include type arguments at a call +site. The type arguments are substituted for type parameters when +type checking. If a function is type-polymorphic and type arguments are not +given, type inference will attempt to infer type arguments if possible. +The following code gives examples of explicit and inferred type arguments: + +.. code-block:: python + + // %f : fn(a, b) -> c + let %x1 = f(True, False); + // %x1 is of type Tensor[(), bool] + let %x2 : () = f(%x1, %x1) + // the type arguments in the second call are inferred to be + +Note that all type relations in the function type must hold at each +call site. Specifically, this means that the relation will be checked +against the specific types of the arguments at a given call site. This +is also a form of polymorphism, since there may be multiple valid +assignments of argument types and a return type so long as the relation +is satisfied. + +For example, if we have a function :code:`%f` that takes tensor arguments +and has the :code:`Broadcast` relation, then there are many different +shapes that the arguments in the below call could have that would satisfy +the type annotation: + +.. code-block:: python + + let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, %c); + %x + +See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. Constant -~~~~~~~~~ +======== This node represents a constant tensor value (see :py:mod:`~tvm.relay.Value` for more details). @@ -236,8 +358,11 @@ tensor type with a rank-zero shape. See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation. -Tuple -~~~~~ +Tuples +====== + +Construction +~~~~~~~~~~~~ The tuple node builds a finite (that is, of statically known size) sequence of heterogeneous data. These tuples match Python's closely. Their fixed length allows for efficient projection of their @@ -252,8 +377,8 @@ fn (%a : Tensor[(10, 10), float32], %b : float32, %c : Tensor[(100, 100), float3 See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. -Tuple Projection -~~~~~~~~~~~~~~~~ +Projection +~~~~~~~~~~ A tuple must be indexed by an integer constant in order to extract a particular member of the tuple. Projections are 0-indexed. @@ -266,58 +391,8 @@ For example, the below projection evaluates to :code:`%b`: See :py:class:`~tvm.relay.expr.TupleGetItem` for its definition and documentation. -Function Expressions -~~~~~~~~~~~~~~~~~~~~ - -Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples. -Function expressions are the same as global functions and -use nearly the same syntax, but do not have a globally unique name. - -.. code-block:: python - - fn (%x : Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32] - -> Tensor[(10, 10), float32] { add(%x, %y) } - -Note that function expressions evaluate to a closure. Closures -are values that are represented as a pair of a local environment -(storing the values for all variables defined outside the scope -of the function's body) and the function itself. - -For example, in the below example, :code:`%z` will evaluate to a tensor -of zero values because the closure for :code:`%f` stores the value of -:code:`%x` at the pointer where :code:`%f` was defined. - -.. code-block:: python - - let %g = fn () { - let %x = Constant(0, (10, 10), float32); - // x is a free variable in the below function - fn (%y) { multiply(%y, %x) } - }; - // the %x in %g's body is not in scope anymore - // %f is a closure where %x maps to Constant(0, (10, 10), float32) - let %f = %g(); - let %x = Constant(1, (10, 10), float32); - %f(%x) // evaluates to `Constant(0, (10, 10), float32) - -A recursive function expression can be defined using a :code:`let` binding, -as here: - -.. code-block:: python - - let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { - if (%x == Constant(0, (10, 10), float32)) { - Constant(1, (10, 10), float32) - } else { - %x * %fact(%x - Constant(1, (10, 10), float32)) - } - }; - %fact(Constant(10, (10, 10), float32)) - -See :py:class:`~tvm.relay.expr.Function` for its definition and documentation. - -Let Binding -~~~~~~~~~~~ +Let Bindings +============ A :code:`let` binding is an immutable local variable binding, allowing the user to bind an expression to a name. @@ -361,7 +436,7 @@ dependency on the other: See :py:class:`~tvm.relay.expr.Let` for its definition and documentation. Graph Bindings -~~~~~~~~~~~~~~ +============== A :code:`let` binding creates a named variable that is bound to the given value and scoped to the subsequent expression. By contrast, a graph binding allows for @@ -410,83 +485,8 @@ programming community (see `"A-Normalization: Why and How" by Matt Might`__ for an introduction to the A-normal form). -======================= -Control Flow Expressions -======================= - -Control flow expressions allow the graph topology to change -based on the value of previously executed expressions. - -Call -~~~~ - -Expressions with function types in Relay are "callable," -meaning that they can be invoked via a function call. These consist of -any expression that evaluates to a closure (i.e., function expressions -or global functions) and Relay operators. - -In terms of dataflow graphs, if a function corresponds to a named -subgraph, a function call inserts the subgraph. This means that if a function's -body contains control flow, calling that function affects the graph topology based -on the values of the executed expressions, as does a recursive call. However, -calls to operators and functions whose bodies do not contain recursive calls -or control flow are still dataflow expressions. - -The syntax of calls follows that used in C-like languages, demonstrated in the -example below: - -.. code-block:: python - - let c = 1; - let f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; - %f(10, 11) - -When a closure is called (see `Function Expressions`_ for a discussion of closures), -the closure's body is evaluated in the stored environment -(i.e., using the stored values for free variables) with -local variable bindings added for each argument; the final value -obtained by evaluating the body is the call's return value. -Thus, in the above example, the call evaluates to 22. -In the case of operators, the implementation is opaque to Relay, -so the result is left up to the registered TVM implementation. - -.. *Note: type parameters are not yet supported in the text format.* - -A type-polymorphic function can also include type arguments at a call -site. The type arguments are substituted for type parameters when -type checking. If a function is type-polymorphic and type arguments are not -given, type inference will attempt to infer type arguments if possible. -The following code gives examples of explicit and inferred type arguments: - -.. code-block:: python - - // %f : fn(a, b) -> c - let %x1 = f(True, False); - // %x1 is of type Tensor[(), bool] - let %x2 : () = f(%x1, %x1) - // the type arguments in the second call are inferred to be - -Note that all type relations in the function type must hold at each -call site. Specifically, this means that the relation will be checked -against the specific types of the arguments at a given call site. This -is also a form of polymorphism, since there may be multiple valid -assignments of argument types and a return type so long as the relation -is satisfied. - -For example, if we have a function :code:`%f` that takes tensor arguments -and has the :code:`Broadcast` relation, then there are many different -shapes that the arguments in the below call could have that would satisfy -the type annotation: - -.. code-block:: python - - let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, %c); - %x - -See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. - If-Then-Else -~~~~~~~~~~~~ +============ Relay has a simple if-then-else expression that allows programs to branch on a single value of type :code:`bool`, i.e., a zero-rank From 90bed3a3ff967e997326acd6a7b792105ee06aaa Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 25 Dec 2018 15:44:26 -0500 Subject: [PATCH 30/36] Subsection on TempExpr --- docs/langref/relay_expr.rst | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 7d6a3005a962..a981d1becac3 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -507,3 +507,21 @@ evaluates to the value of the "then" branch if the condition value evaluates to `True` and evaluates to the value of the "else" branch otherwise. See :py:class:`~tvm.relay.expr.If` for its definition and documentation. + +TempExprs +========= + +Program transformations (passes) in Relay may require inserting temporary +state into the program AST to guide further transformations. The +:code:`TempExpr` node is provided as a utility to developers for this purpose; +nodes inheriting from :code:`TempExpr` cannot appear directly in user-provided +code but may be inserted in a pass. Any :code:`TempExpr`s created in a pass +should ideally be eliminated before the pass is complete, as +:code:`TempExpr`s only store internal state and have no semantics of their own. + +For an example of :code:`TempExpr`s being used in a pass, +see :code:`src/relay/pass/alter_op_layout.cc`, which uses :code:`TempExpr` nodes +to store information about operator layouts as the pass tries to rearrange operator +calls. + +See :py:class:`~tvm.relay.expr.TempExpr` for its definition and documentation. From a1c8a3a615c529db03dcd30a67e9333156231197 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Wed, 26 Dec 2018 13:54:16 -0500 Subject: [PATCH 31/36] Move Relay in index to before Hybrid Script --- docs/langref/index.rst | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/docs/langref/index.rst b/docs/langref/index.rst index 58d41d9fe379..f89d29d9218d 100644 --- a/docs/langref/index.rst +++ b/docs/langref/index.rst @@ -1,21 +1,7 @@ Language Reference ================== This document provides references to -embedded languages in the TVM stack. - -Hybrid Script -------------- - -The below page describes the TVM hybrid script front-end, -which uses software emulation to support some constructs not -officially supported in TVM. - -.. toctree:: - :maxdepth: 2 - - hybrid_script - - +embedded languages and IRs in the TVM stack. Introduction to Relay --------------------- @@ -41,3 +27,15 @@ The below pages describe the grammar, type system, and operators in Relay, respe relay_expr relay_type relay_op + +Hybrid Script +------------- + +The below page describes the TVM hybrid script front-end, +which uses software emulation to support some constructs not +officially supported in TVM. + +.. toctree:: + :maxdepth: 2 + + hybrid_script From d73a0bc2695c1076ee4f076fce0778ac68f2ef71 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Wed, 26 Dec 2018 15:41:24 -0500 Subject: [PATCH 32/36] Reorganize function discussion, add module section --- docs/langref/relay_expr.rst | 173 +++++++++++++++++++++--------------- 1 file changed, 99 insertions(+), 74 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index a981d1becac3..8a8ac460729f 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -93,35 +93,30 @@ Functions in Relay act similarly to procedures or functions in other programming languages and serve to generalize the concept of a named subgraph. -See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of function nodes. - -Global Functions -~~~~~~~~~~~~~~~~ +Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples. +Additionally, functions in Relay are higher-order, which means that a function can be passed as an argument to a +function or returned by a function, as function expressions evaluate to closures (see the `Closures`_ subsection), +which are values like tensors and tuples. -A global function definition consists of a name, arguments, return type, -type parameters, and any applicable type relations. -A function's return type and parameter types may be omitted; -Relay will attempt to infer the most general types where types -are omitted. +See :py:class:`~tvm.relay.expr.Function` for the definition and documentation of function nodes. -Functions defined in the manner described in this subsection have -global scope and may be recursive; that is, within the function's body, the function's -identifier refers back to the function. +Syntax +~~~~~~ -A definition minimally consists of an identifier :code:`@id`, an empty set of +A definition minimally consists of the keyword :code:`fn`, an empty set of parameters, and a body expression (:py:class:`~tvm.relay.expr.Expr`) contained by curly braces. .. code-block:: python - def @id() { body } + fn() { body } A definition may contain any number of parameters. For example, a simple function that invokes the `add` operator: .. code-block:: python - def @plus(%x, %y) { add(%x, %y) } + fn(%x, %y) { add(%x, %y) } Notice that within the function's body, the parameters are local variables, just like those bound in a :code:`let` expression. @@ -132,19 +127,62 @@ on certain types: .. code-block:: python - def @plus(%x: Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32]) + fn(%x: Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { add(%x, %y) } -A function parameter is just a local variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally -annotated with a type. Parameters are written as :code:`%x : T`. +The above function only takes arguments of type :code:`Tensor[(10, 10), float32]` and returns a value of +type :code:`Tensor[(10, 10), float32]`. A function parameter is just a local +variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally annotated with a type, written as :code:`%x : T`. -When the type information is omitted, we will attempt to infer the most general type +When the type information is omitted, Relay attempts to infer the most general type for the users. This property is known as generalization: for a definition without -explicit annotations, we will attempt to assign the most general type to the +explicit annotations, Relay attempts to assign the most general type to the parameters and return type based on the function body and call sites. +A recursive function expression can be defined using a :code:`let` binding, +as here: + +.. code-block:: python + + let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { + if (%x == Constant(0, (10, 10), float32)) { + Constant(1, (10, 10), float32) + } else { + %x * %fact(%x - Constant(1, (10, 10), float32)) + } + }; + %fact(Constant(10, (10, 10), float32)) + +Closures +~~~~~~~~ + +Function expressions evaluate to a closure. Closures +are values that are represented as a pair of a local environment +(storing the values for all variables defined outside the scope +of the function's body) and the function itself. + +For example, in the below example, the final result will be +a tensor of zero values because the closure for :code:`%f` stores the value of +:code:`%x` at the pointer where :code:`%f` was defined. + +.. code-block:: python + + let %g = fn () { + let %x = Constant(0, (10, 10), float32); + // x is a free variable in the below function + fn (%y) { multiply(%y, %x) } + }; + // the %x in %g's body is not in scope anymore + // %f is a closure where %x maps to Constant(0, (10, 10), float32) + let %f = %g(); + let %x = Constant(1, (10, 10), float32); + %f(%x) // evaluates to `Constant(0, (10, 10), float32) + +Polymorphism and Type Relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + .. *Note: type parameter syntax is not yet supported in the text format.* A function may also be given a set of type parameters, which can be @@ -157,7 +195,7 @@ For example, one can define a polymorphic identity function for any Relay type as follows: .. code-block:: python - def @id(%x : t) -> t { + fn(%x : t) -> t { %x } @@ -165,7 +203,7 @@ The below definition is also polymorphic, but restricts its arguments to tensor types: .. code-block:: python - def @id(%x: Tensor[s, bt]) { + fn(%x: Tensor[s, bt]) { %x } @@ -178,7 +216,7 @@ the following: .. code-block:: python - def @plus(%x, %y) where Broadcast { add(%x, %y) } + fn(%x, %y) where Broadcast { add(%x, %y) } In the above definition, the types of :code:`%x` and :code:`%y` and the return type are subject to the :code:`Broadcast` relation, meaning all three must be tensors @@ -191,55 +229,7 @@ constraints on types (especially tensor shapes). All function relations must hold at all call sites; type checking is thus treated as a constraint-solving problem. For more detail on type relations and their implementations, -please see the documentation on typing in Relay. - -Function Expressions -~~~~~~~~~~~~~~~~~~~~ - -Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples. -Function expressions behave identically to global functions and use nearly the same syntax, -but do not have a globally unique name. - -.. code-block:: python - - fn (%x : Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32] - -> Tensor[(10, 10), float32] { add(%x, %y) } - -Note that function expressions evaluate to a closure. Closures -are values that are represented as a pair of a local environment -(storing the values for all variables defined outside the scope -of the function's body) and the function itself. - -For example, in the below example, :code:`%z` will evaluate to a tensor -of zero values because the closure for :code:`%f` stores the value of -:code:`%x` at the pointer where :code:`%f` was defined. - -.. code-block:: python - - let %g = fn () { - let %x = Constant(0, (10, 10), float32); - // x is a free variable in the below function - fn (%y) { multiply(%y, %x) } - }; - // the %x in %g's body is not in scope anymore - // %f is a closure where %x maps to Constant(0, (10, 10), float32) - let %f = %g(); - let %x = Constant(1, (10, 10), float32); - %f(%x) // evaluates to `Constant(0, (10, 10), float32) - -A recursive function expression can be defined using a :code:`let` binding, -as here: - -.. code-block:: python - - let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { - if (%x == Constant(0, (10, 10), float32)) { - Constant(1, (10, 10), float32) - } else { - %x * %fact(%x - Constant(1, (10, 10), float32)) - } - }; - %fact(Constant(10, (10, 10), float32)) +please see the documentation on `Relay's Type System`_. Operators ========= @@ -258,7 +248,7 @@ by optimization passes) may be registered as a new column. From the perspective of Relay's type system, an operator is a function, so operators may be called like any other function and have function types. In particular, operator types are registered using a single -type relation (see the above subsection), typically a relation +type relation (see `Polymorphism and Type Relations`_), typically a relation specialized to that operator. For example, the :code:`add` operator is registered with the :code:`Broadcast` relation, indicating that the arguments of :code:`add` must be tensors and that the return type @@ -299,7 +289,7 @@ example below: let f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; %f(10, 11) -When a closure is called (see `Function Expressions`_ for a discussion of closures), +When a closure is called (see `Closures`_), the closure's body is evaluated in the stored environment (i.e., using the stored values for free variables) with local variable bindings added for each argument; the final value @@ -343,6 +333,41 @@ the type annotation: See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. +Module and Global Functions +=========================== + +Relay keeps a global data structure known as a "module" (often called an "environment" in other +functional programming languages) to keep track of the definitions of global functions. +In particular, the module keeps a globally accessible mapping of global variables to the +function expressions they denote. The utility of the module is that it allows global functions +to recursively refer to themselves or any other global function (e.g., as in mutual recursion). + +Note Relay's module is analogous to data structures for keeping track of subgraphs in computation +graph-based IRs. + +Global functions in Relay behave identically to the function expressions defined in `Functions`_, +but have syntactic sugar in the text format to enter their definitions into the module. Namely, +a global function definition includes a global identifier and is allowed to recursively refer to +that identifier in the body, as in the following example: + +.. code-block:: python + + def @ackermann(%m : Tensor[(), int32], %n : Tensor[(), int32]) -> Tensor[(), int32] { + if (%m == 0) { + %n + 1 + } else if (%m > 0 && n == 0) { + @ackermann(%m - 1, 1) + } else { + @ackermann(%m - 1, @ackermann(%m, %n - 1)) + } + } + +This definition would result in a module entry mapping the identifier :code:`@ackermann` to a function expression +with the parameters, return type, and body above. Any reference to the identifier :code:`@ackermann` elsewhere in the +code could then look up the identifier in the module and replace the function definition as needed. + +See :py:class:`~tvm.relay.Module` for the definition and documentation of a module. + Constant ======== From 12ad89a2b9e734ba41238d86bfabc26835d30a13 Mon Sep 17 00:00:00 2001 From: Josh Pollock Date: Thu, 27 Dec 2018 17:48:54 -0500 Subject: [PATCH 33/36] Numerous corrections and clarifications by @joshpoll Co-Authored-By: slyubomirsky --- docs/langref/relay_expr.rst | 66 ++++++++++++++++++------------------- docs/langref/relay_type.rst | 18 +++++----- 2 files changed, 42 insertions(+), 42 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 8a8ac460729f..6dfddfb37d6e 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -28,9 +28,9 @@ fragment in Relay includes the following constructs: - `If-Then-Else`_ Expressions - Recursive Calls in Functions -Because a function can be viewed as a subgraph from the point of view of computational graphs, -a call effectively substitutes in the subgraph. Thus, if a function's body is entirely within -the dataflow fragment, a call to that function is in the dataflow fragment; conversely, if the +From the point of view of a computation graph, a function is a subgraph and a function call inlines the subgraph, substituting its arguments for the free variables in the subgraph with corresponding names. +Thus if a function's body uses only dataflow constructs +, a call to that function is in the dataflow fragment; conversely, if the function's body contains control flow, a call to that function is not part of the dataflow fragment. Variables @@ -38,7 +38,7 @@ Variables Inspired by LLVM, Relay explicitly distinguishes between local and global variables both in the AST and in the text format. In the text format, -global and local variables are distinguished by prefixes, or sigils. +global and local variables are distinguished by prefixes, or *sigils*. Global variables are prefixed with :code:`@` and local variables with :code:`%`. This explicit distinction makes certain optimizations easier to implement. @@ -112,7 +112,7 @@ contained by curly braces. fn() { body } A definition may contain any number of parameters. For example, a -simple function that invokes the `add` operator: +simple function that invokes the :code:`add` operator: .. code-block:: python @@ -121,13 +121,13 @@ simple function that invokes the `add` operator: Notice that within the function's body, the parameters are local variables, just like those bound in a :code:`let` expression. -One may also annotate explicit types on definitions. -For example, we can restrict the above definition to only work +One may also annotate explicit types on functions. +For example, we can restrict the above function to only work on certain types: .. code-block:: python - fn(%x: Tensor[(10, 10), float32], %y: Tensor[(10, 10), float32]) + fn(%x : Tensor[(10, 10), float32], %y : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { add(%x, %y) } @@ -146,7 +146,7 @@ as here: .. code-block:: python - let %fact = fn (%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { + let %fact = fn(%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] { if (%x == Constant(0, (10, 10), float32)) { Constant(1, (10, 10), float32) } else { @@ -158,7 +158,7 @@ as here: Closures ~~~~~~~~ -Function expressions evaluate to a closure. Closures +A function expression evaluates to a closure. Closures are values that are represented as a pair of a local environment (storing the values for all variables defined outside the scope of the function's body) and the function itself. @@ -169,16 +169,16 @@ a tensor of zero values because the closure for :code:`%f` stores the value of .. code-block:: python - let %g = fn () { + let %g = fn() { let %x = Constant(0, (10, 10), float32); - // x is a free variable in the below function - fn (%y) { multiply(%y, %x) } + // %x is a free variable in the below function + fn(%y) { %y * %x } }; // the %x in %g's body is not in scope anymore // %f is a closure where %x maps to Constant(0, (10, 10), float32) let %f = %g(); let %x = Constant(1, (10, 10), float32); - %f(%x) // evaluates to `Constant(0, (10, 10), float32) + %f(%x) // evaluates to Constant(0, (10, 10), float32) Polymorphism and Type Relations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -195,7 +195,7 @@ For example, one can define a polymorphic identity function for any Relay type as follows: .. code-block:: python - fn(%x : t) -> t { + fn(%x : t) -> t { %x } @@ -203,7 +203,7 @@ The below definition is also polymorphic, but restricts its arguments to tensor types: .. code-block:: python - fn(%x: Tensor[s, bt]) { + fn(%x : Tensor[s, bt]) { %x } @@ -285,8 +285,8 @@ example below: .. code-block:: python - let c = 1; - let f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; + let %c = 1; + let %f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c }; %f(10, 11) When a closure is called (see `Closures`_), @@ -309,9 +309,9 @@ The following code gives examples of explicit and inferred type arguments: .. code-block:: python // %f : fn(a, b) -> c - let %x1 = f(True, False); + let %x1 = %f(True, False); // %x1 is of type Tensor[(), bool] - let %x2 : () = f(%x1, %x1) + let %x2 : () = %f(%x1, %x1) // the type arguments in the second call are inferred to be Note that all type relations in the function type must hold at each @@ -328,7 +328,7 @@ the type annotation: .. code-block:: python - let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b, %c); + let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b); %x See :py:class:`~tvm.relay.expr.Call` for its definition and documentation. @@ -355,7 +355,7 @@ that identifier in the body, as in the following example: def @ackermann(%m : Tensor[(), int32], %n : Tensor[(), int32]) -> Tensor[(), int32] { if (%m == 0) { %n + 1 - } else if (%m > 0 && n == 0) { + } else if (%m > 0 && %n == 0) { @ackermann(%m - 1, 1) } else { @ackermann(%m - 1, @ackermann(%m, %n - 1)) @@ -390,15 +390,15 @@ Construction ~~~~~~~~~~~~ The tuple node builds a finite (that is, of statically known size) sequence of heterogeneous data. -These tuples match Python's closely. Their fixed length allows for efficient projection of their +These tuples match Python's closely, and their fixed length allows for efficient projection of their members. .. code-block:: python -fn (%a : Tensor[(10, 10), float32], %b : float32, %c : Tensor[(100, 100), float32]) { - let %tup = (%a, %b); // type: (Tensor[(10, 10), float32], float32) - ((%tup.0 + %tup.1), %c) // type: (Tensor[(10, 10), float32], Tensor[(100, 100), float32]) -} + fn(%a : Tensor[(10, 10), float32], %b : float32, %c : Tensor[(100, 100), float32]) { + let %tup = (%a, %b); // type: (Tensor[(10, 10), float32], float32) + ((%tup.0 + %tup.1), %c) // type: (Tensor[(10, 10), float32], Tensor[(100, 100), float32]) + } See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation. @@ -428,16 +428,16 @@ that may reference the bound identifier. If a type annotation on the bound variable is omitted, Relay attempts to infer the most general type permitted for the variable. -The bound variable in a :code:let expression is only in scope +The bound variable in a :code:`let` expression is only in scope in its body, except when the variable defines a function expression. -When a :code:let expression creates a function, the variable is also +When a :code:`let` expression creates a function, the variable is also in scope in its value to allow for recursively defined functions (see the previous subsection). The value of a :code:`let` binding is the value of the final expression after evaluating the bindings it depends on. For example, in the following example the entire expression evaluates to a tensor -of shape (10, 10) where all elements are 2: +of shape :code:`(10, 10)` where all elements are 2: .. code-block:: python @@ -508,7 +508,7 @@ convert between dataflow graphs defined using graph bindings and programs with : bindings in A-normal form, employed by many compiler optimizations from the functional programming community (see `"A-Normalization: Why and How" by Matt Might`__ for an introduction -to the A-normal form). +to A-normal form). If-Then-Else ============ @@ -519,7 +519,7 @@ tensor of booleans (:code:`Tensor[(), bool]`). .. code-block:: python - if (equal(%t, %u)) { + if (%t == %u) { %t } else { %u @@ -540,7 +540,7 @@ Program transformations (passes) in Relay may require inserting temporary state into the program AST to guide further transformations. The :code:`TempExpr` node is provided as a utility to developers for this purpose; nodes inheriting from :code:`TempExpr` cannot appear directly in user-provided -code but may be inserted in a pass. Any :code:`TempExpr`s created in a pass +code but may be inserted in a pass. Any :code:`TempExpr`s created in a pass should ideally be eliminated before the pass is complete, as :code:`TempExpr`s only store internal state and have no semantics of their own. diff --git a/docs/langref/relay_type.rst b/docs/langref/relay_type.rst index aef830711c75..48df988df85f 100644 --- a/docs/langref/relay_type.rst +++ b/docs/langref/relay_type.rst @@ -23,7 +23,7 @@ Relay to be ahead-of-time compiled and provides much more information about tensors for optimizations further in the compilation pipeline. Such optimizations can be implemented as passes, which are Relay-to-Relay AST transformations, and may use the inferred types (e.g., shape information) for making decisions about -program transformations. For instance, `src/relay/pass/fuse_ops.cc` gives +program transformations. For instance, :code:`src/relay/pass/fuse_ops.cc` gives an implementation of a pass that uses inferred tensor shapes to replace invocations of operators in a Relay program with fused operator implementations. @@ -52,9 +52,9 @@ A concrete tensor type in Relay. Tensors are typed according to data type and shape. At present, these use TVM's data types and shapes, but in the future, Relay may include a separate AST for -shapes. In particular, data types include `bool`, `float32`, `int8` and various -other bit widths and numbers of lanes. Shapes are given as tuples of dimensions (TVM `IndexExpr`), -such as `(5, 5)`; scalars are also given tuple types and have a shape of `()`. +shapes. In particular, data types include :code:`bool`, :code:`float32`, :code:`int8` and various +other bit widths and numbers of lanes. Shapes are given as tuples of dimensions (TVM :code:`IndexExpr`), +such as :code:`(5, 5)`; scalars are also given tuple types and have a shape of :code:`()`. Note, though, that TVM shapes can also include variables and arithmetic expressions including variables, so Relay's constraint solving phase will attempt to find @@ -112,8 +112,8 @@ Like normal parameters, concrete arguments must be given for type parameters at .. *Note: type parameter syntax is not yet supported in the text format.* -For example, `s` below is a type parameter of kind `Shape` and it will -be substituted for `(10, 10)` at the call site below: +For example, :code:`s` below is a type parameter of kind :code:`Shape` and it will +be substituted with :code:`(10, 10)` at the call site below: .. code-block:: python @@ -143,7 +143,7 @@ consists of a list of type parameters, a set of type constraints, a sequence of argument types, and a return type. We informally write function types as: -`fn(arg_types) -> ret_type where type_constraints` +:code:`fn(arg_types) -> ret_type where type_constraints` A type parameter in the function type may appear in the argument types or the return types. Additionally, each of the type constraints @@ -163,7 +163,7 @@ tensor shapes in complex ways, such as broadcasting operators or :code:`flatten`, allowing Relay to statically reason about the shapes in these cases. -A type relation :code:`R` describes a relationship between the inputs and output types of a Relay function. +A type relation :code:`R` describes a relationship between the input and output types of a Relay function. Namely, :code:`R` is a function on types that outputs `true` if the relationship holds and `false` if it fails to hold. Types given to a relation may be incomplete or @@ -225,7 +225,7 @@ See :py:class:`~tvm.relay.ty.TypeRelation` for its definition and documentation. Incomplete Type ~~~~~~~~~~~~~~~ -A type or portion of a type that is not yet known. +An incomplete type is a type or portion of a type that is not yet known. This is only used during type inference. Any omitted type annotation is replaced by an incomplete type, which will be replaced by another type at a later point. From 342e7db5a54dec6637bf6fc208e94e23e3a68bd6 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 27 Dec 2018 18:04:04 -0500 Subject: [PATCH 34/36] Add references to module, kinds, and type relations --- docs/langref/relay_expr.rst | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 6dfddfb37d6e..81ae21538821 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -49,9 +49,12 @@ Global Variable ~~~~~~~~~~~~~~~~~~ Global identifiers are prefixed by the :code:`@` sigil, such as ":code:`@global`". -A global identifier always references a globally visible definition contained in the environment. +A global identifier always references a globally visible definition contained in the +globally visible environment, known as the `module`__. Global identifiers must be unique. +__ `Module and Global Functions`_ + See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation and documentation. @@ -191,6 +194,14 @@ type parameters are *type polymorphic*; their return type or the types of arguments they will accept can vary based on the type arguments given at call sites. +Type parameters are classified by *kind* and can +only appear in parts of the type signature where their kind is appropriate +(e.g., type parameters of kind :code:`Shape` can only appear where a shape +would be expected in a tensor type); for a full discussion, +see `the documentation on type parameters`__. + +__ `Type Parameter`_ + For example, one can define a polymorphic identity function for any Relay type as follows: @@ -248,12 +259,14 @@ by optimization passes) may be registered as a new column. From the perspective of Relay's type system, an operator is a function, so operators may be called like any other function and have function types. In particular, operator types are registered using a single -type relation (see `Polymorphism and Type Relations`_), typically a relation +type relation (see `the documentation on type relations`__), typically a relation specialized to that operator. For example, the :code:`add` operator is registered with the :code:`Broadcast` relation, indicating that the arguments of :code:`add` must be tensors and that the return type is a tensor whose shape depends on those of its arguments. +__ `Type Relation`_ + Operators are rendered without a sigil (e.g :code:`conv2d`, :code:`flatten`) when pretty-printing Relay programs. Operators are explicitly contained in the program and are uniquely From e2e4df8e91303b4a82deaf885dc6b090e0b15fab Mon Sep 17 00:00:00 2001 From: Josh Pollock Date: Tue, 1 Jan 2019 19:20:49 -0500 Subject: [PATCH 35/36] Note on reordering let bindings from @joshpoll Co-Authored-By: slyubomirsky --- docs/langref/relay_expr.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index 81ae21538821..ba4374dec945 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -460,8 +460,8 @@ of shape :code:`(10, 10)` where all elements are 2: A sequence of :code:`let` bindings can be considered as a dataflow graph, where the bindings are a series of sub-graphs connected by bound variables. Since these binding sequences are -pure, they can be evaluated in any order according to the program -dataflow. For example, the first and second :code:`let` bindings below +pure, a pair of bindings where neither depends on the other can be safely reordered. +For example, the first and second :code:`let` bindings below may be evaluated in either order because neither has a dataflow dependency on the other: From fadf3b5acd748b832188a61ced2daf4184514b77 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Tue, 1 Jan 2019 19:25:09 -0500 Subject: [PATCH 36/36] Clarify semantics of if-then-else --- docs/langref/relay_expr.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/langref/relay_expr.rst b/docs/langref/relay_expr.rst index ba4374dec945..f28527d9bf51 100644 --- a/docs/langref/relay_expr.rst +++ b/docs/langref/relay_expr.rst @@ -542,7 +542,8 @@ Since if-then-else branches are expressions, they may appear inline wherever any other expression may be expected, like invocations of the ternary operator in C-like languages. The if-then-else expression evaluates to the value of the "then" branch if the condition value -evaluates to `True` and evaluates to the value of the "else" branch otherwise. +evaluates to :code:`True` and evaluates to the value of the "else" branch if the +condition value evaluates to :code:`False`. See :py:class:`~tvm.relay.expr.If` for its definition and documentation.