.. Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. .. SPDX-License-Identifier: Apache-2.0 Copyright © 2020, `Digital Asset (Switzerland) GmbH `_ and/or its affiliates. All rights reserved. Daml-LF 1 specification ======================= .. contents:: Contents Introduction ^^^^^^^^^^^^ This document specifies version 1 of the Daml-LF language — the language that Daml ledgers execute. Daml compiles to Daml-LF which executes on Daml ledgers, similar to how Java compiles to JVM byte code which executes on the JVM. “LF” in Daml-LF stands for “Ledger Fragment”. Daml-LF is a small, strongly typed, functional language with strict evaluation that includes native representations for core Daml concepts such as templates, updates, and parties. It is primarily intended as a compilation target. How to view and edit this document ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To view this document correctly, we recommend you install the `DejaVu Sans family of fonts `_, which is free (as in freedom) and provide exceptional Unicode coverage. The sphinx style sheets specify DejaVu Sans Mono as the font to use for code, and if you want to view/edit this section you should use it for your editor, too. If you want to edit this section comfortably, we highly recommend using either VS Code' ``latex-input`` extension or Emacs' TeX input mode. In VS Code, you can start typing, say, ``\Gamma`` and the autocompleter will suggest ``Γ``. Similarly ``\to``, ``\->`` and ``\rightarrow`` will all lead to ``→``. You might need to explicitly trigger the autocompleter using ``Ctrl+Space``. All autocompletions are triggered by (one of) their LaTeX names. You can also trigger autocompletions for subscripts by typing ``\_1`` for ``₁``, ``\_i`` for ``ᵢ``, etc. We have have added a couple of extra symbols in ``.vscode/restructuredtext.code-snippets`` file. If you want to add further symbols that's where they could go. If you want to use Emacs' TeX input mode, , you can turn it on using ``M-x set-input-method TeX``, and then you can input symbols as you would in TeX, mostly using ``\symbol-name`` and ``_letter``. If you don't know how to input a character, go over it with your cursor and ``M-x describe-char``. Its TeX code will be listed under ``to input``. Moreover, add the following to your ``~/.emacs`` to enable additional symbols used in this doc:: (with-temp-buffer (activate-input-method "TeX") (let ((quail-current-package (assoc "TeX" quail-package-alist))) (quail-defrule "\\limage" ?⦇ nil t) (quail-defrule "\\rimage" ?⦈ nil t) (quail-defrule "\\rwave" ?↝ nil t) (quail-defrule "\\lwave" ?↜ nil t) (quail-defrule "\\lwbrace" ?⦃ nil t) (quail-defrule "\\rwbrace" ?⦄ nil t))) Version history ~~~~~~~~~~~~~~~ The Daml-LF language is versioned using a major and minor component. Increasing the major component allows us to drop features, change the semantics of existing features, or update the serialization format. Changes to the minor component cannot break backward compatibility, and operate on the same major version of the serialization format in a backward compatible way. This document describes Daml-LF major version 1, including all its minor versions. Starting from SDK 1.0 release, Daml-LF versions older than 1.6 are deprecated. An engine compliant with the present specification must handle all versions newer than or equal to Daml-LF 1.6, no requirement is made on handling older version. Each Daml-LF program is accompanied by the version identifier of the language it was serialized in. This number enables the Daml-LF engine to interpret previous versions of the language in a backward compatibility way. In the following of this document, we will use annotations between square brackets such as *[Available in version < x.y]*, *[Available in versions >= x.y]*, and *[Changed in version x.y]* to emphasize that a particular feature is concerned with a change introduced in Daml x.y version. In addition, we will mark lines within inference rules with annotations of the form ``[Daml-LF < x.y]`` and ``[Daml-LF ≥ x.y]`` to make the respective line conditional upon the Daml-LF version. A *preview* version is an snapshot of the next 1.x version to be released. It is provided for beta testing purpose and may only be changed to include bug fixes. On the other hand, the *development* version is a special staging area for the development of upcoming version 1.x version. It may be used for alpha testing, and can be changed without notice. Compliant implementations are not required to implement any features exclusive to development version, but should take them under advisement as likely elements of the next 1.x version. Below, we list the versions of Daml-LF 1.x that a Daml-LF engine compliant with the present specification must handle, in ascending order. The optional preview version is marked with the tag *(preview)* while the development version is marked with the tag *(development)*. Conventionally development version is call 1.dev. The list comes with a brief description of the changes, and some links to help unfamiliar readers learn about the features involved in the change. One can refer also to the `Serialization` section which is particularly concerned about versioning and backward compatibility. Support for language versions 1.0 to 1.5 was dropped on 2020-11-30. This breaking change does not impact ledgers created with SDK 1.0.0 or later. Version: 1.6 ............ * Introduction date: 2019-07-01 * Description: + Initial version Version: 1.7 ............ * Introduction date: 2019-11-07 * Description: + **Add** Nat kind and Nat type. - add `nat` kind - add `nat` type + **Add** parametrically scaled Numeric type. - add `NUMERIC` primitive type - add `numeric` primitive literal - add numeric builtins, namely `ADD_NUMERIC`, `SUB_NUMERIC`, `MUL_NUMERIC`, `DIV_NUMERIC`, `ROUND_NUMERIC`, `CAST_NUMERIC`, `SHIFT_NUMERIC`, `LEQ_NUMERIC`, `LESS_NUMERIC`, `GEQ_NUMERIC`, `GREATER_NUMERIC`, `FROM_TEXT_NUMERIC`, `TO_TEXT_NUMERIC`, `INT64_TO_NUMERIC`, `NUMERIC_TO_INT64`, `EQUAL_NUMERIC` + **Drop** support for Decimal type. Use Numeric of scale 10 instead. - drop `DECIMAL` primitive type - drop `decimal` primitive literal - drop decimal builtins, namely `ADD_DECIMAL`, `SUB_DECIMAL`, `MUL_DECIMAL`, `DIV_DECIMAL`, `ROUND_DECIMAL`, `LEQ_DECIMAL`, `LESS_DECIMAL`, `GEQ_DECIMAL`, `GREATER_DECIMAL`, `FROM_TEXT_DECIMAL`, `TO_TEXT_DECIMAL`, `INT64_TO_DECIMAL`, `DECIMAL_TO_INT64`, `EQUAL_DECIMAL` + **Add** string interning in external package references. + **Add** name interning in external package references. + **Add** existential ``Any`` type - add `'Any'` primitive type - add `'to_any'` and `'from_any'` expression to convert from/to an arbitrary ground type (i.e. a type with no free type variables) to ``Any``. + **Add** for Type representation. - add `'TypeRep'` primitive type - add `type_rep` expression to reify a arbitrary ground type (i.e. a type with no free type variables) to a value. Version: 1.8 ............ * Introduction date: 2020-03-02 * Description: + **Add** type synonyms. + **Add** package metadata. + **Rename** structural records from ``Tuple`` to ``Struct``. + **Rename** ``Map`` to ``TextMap``. Version: 1.11 ............. * Introduction date: 2020-12-14 * Description: + **Add** generic equality builtin. + **Add** generic order builtin. + **Add** generic map type ``GenMap``. + **Add** ``TO_TEXT_CONTRACT_ID`` builtin. + **Add** `exercise_by_key` Update. + **Add** choice observers. Version: 1.12 ............. * Introduction date: 2021-01-2 * Description: + Drop type constructor in serialized variant and enumeration values. Drop type constructor and field names in serialized record values. See value version 12 in value specification for more details Version: 1.dev (development) ............................ + **Add** exception handling. + **Add** BigDecimal type. - add `BigNumeric` primitive type - add `RoundingMode` primitive type Abstract syntax ^^^^^^^^^^^^^^^ This section specifies the abstract syntax tree of a Daml-LF package. We define identifiers, literals, types, expressions, and definitions. Notation ~~~~~~~~ Terminals are specified as such:: description: symbols ∈ regexp -- Unique identifier Where: * The ``description`` describes the terminal being defined. * The ``symbols`` define how we will refer of the terminal in type rules / operational semantics / .... * The ``regexp`` is a `java regular expression `_ describing the members of the terminal. In particular, we will use the following conventions: * ``\xhh`` matches the character with hexadecimal value ``0xhh``. * ``\n`` matches the carriage return character ``\x0A``, * ``\r`` matches the carriage return ``\x0D``, * ``\"`` matches the double quote character ``\x22``. * ``\$`` match the dollar character ``\x24``. * ``\.`` matches the full stop character ``\x2e\``. * ``\\`` matches the backslash character ``\x5c``. * ``\d`` to match a digit: ``[0-9]``. * The ``Unique identifier`` is a string that uniquely identifies the non-terminal. Sometimes the symbol might be the same as the unique identifier, in the instances where a short symbol is not needed because we do not mention it very often. Non-terminals are specified as such:: Description: symbols ::= non-terminal alternative -- Unique identifier for alternative: description for alternative | ⋮ Where description and symbols have the same meaning as in the terminal rules, and: * each non-terminal alternative is a piece of syntax describing the alternative; * each alternative has a unique identifier (think of them as constructors of a datatype). Note that the syntax defined by the non-terminals is not intended to be parseable or non-ambiguous, rather it is intended to be read and interpreted by humans. However, for the sake of clarity, we enclose strings that are part of the syntax with single quotes. We do not enclose symbols such as ``.`` or ``→`` in quotes for the sake of brevity and readability. Identifiers ~~~~~~~~~~~ In this section, we define the sorts of strings and identifiers that appear in Daml-LF programs. We first define two types of *strings*:: Strings: Str ::= " " -- Str | " StrChars " Sequences of string characters: StrChars ::= StrChar -- StrChars | StrChars StrChar | EscapedStrChar StrChar String chars: StrChar ∈ [^\n\r\"\\] -- StrChar String character escape sequences: EscapedStrChar ∈ \\\n|\\\r|\\\"|\\\\ -- EscapedStrChar *Strings* are possibly empty sequences of legal `Unicode `_ code points where the line feed character ``\n``, the carriage return character ``\r``, the double quote character ``\"``, and the backslash character ``\\`` must be escaped with backslash ``\\``. Daml-LF considers legal `Unicode code point `_ that is not a `Surrogate Code Point `_, in other words any code point with an integer value in the range from ``0x000000`` to ``0x00D7FF`` or in the range from ``0x00DFFF`` to ``0x10FFFF`` (bounds included). Then, we define the so-called *PackageId strings* and *PartyId strings*. Those are non-empty strings built with a limited set of US-ASCII characters (See the rules `PackageIdChar` and `PartyIdChar` below for the exact sets of characters). We use those string in instances when we want to avoid empty identifiers, escaping problems, and other similar pitfalls. :: PackageId strings PackageIdString ::= ' PackageIdChars ' -- PackageIdString Sequences of PackageId character PackageIdChars ::= PackageIdChar -- PackageIdChars | PackageIdChars PackageIdChar PackageId character PackageIdChar ∈ [a-zA-Z0-9\-_ ] -- PackageIdChar PartyId strings PartyIdString ∈ [a-zA-Z0-9:\-_ ]{1,255} -- PartyIdChar PackageName strings PackageNameString ∈ [a-zA-Z0-9:\-_]+ -- PackageNameString PackageVersion strings PackageVersionString ∈ (0|[1-9][0-9]*)(\.(0|[1-9][0-9]*))* – PackageVersionString We can now define a generic notion of *identifier* and *name*:: identifiers: Ident ∈ [a-zA-Z_\$][a-zA-Z0-9_\$] -- Ident names: Name ::= Identifier -- Name | Name \. Identifier Identifiers are standard `java identifiers `_ restricted to US-ASCII while names are sequences of identifiers intercalated with dots. The character ``%`` is reserved for external languages built on Daml-LF as a "not an Ident" notation, so should not be considered for future addition to allowed identifier characters. In the following, we will use identifiers to represent *built-in functions*, term and type *variable names*, record and struct *field names*, *variant constructors* and *template choices*. On the other hand, we will use names to represent *type constructors*, *type synonyms*, *value references*, and *module names*. Finally, we will use PackageId strings as *package identifiers*. :: Expression variables x, y, z ::= Ident -- VarExp Type variables α, β ::= Ident -- VarTy Built-in function names F ::= Ident -- Builtin Record and struct field names f ::= Ident -- Field Variant data constructors V ::= Ident -- VariantCon Enum data constructors E ::= Ident -- EnumCon Template choice names Ch ::= Ident -- ChoiceName Value references W ::= Name -- ValRef Type constructors T ::= Name -- TyCon Type synonym S ::= Name -- TySyn Module names ModName ::= Name -- ModName Package identifiers pid ::= PackageIdString -- PkgId Package names pname ::= PackageNameString -- PackageName Package versions pversion ::= PackageVersionString -- PackageVersion V0 Contract identifiers: cidV0 ∈ #[a-zA-Z0-9\._:-#/ ]{0,254} -- V0ContractId V1 Contract identifiers: cidV1 ∈ 00([0-9a-f][0-9a-f]){32,126} -- V1ContractId Contract identifiers can be created dynamically through interactions with the underlying ledger. See the `operation semantics of update statements `_ for the formal specification of those interactions. Depending on its configuration, a Daml-LF engine can produce V0 or V1 contract identifiers. When configured to produce V0 contract identifiers, a Daml-LF compliant engine must refuse to load any Daml-LF >= 1.11 archives. On the contrary, when configured to produce V1 contract IDs, a Daml-LF compliant engine must accept to load any non-deprecated Daml-LF version. V1 Contract IDs allocation scheme is described in the `V1 Contract ID allocation scheme specification <./contract-id.rst>`_. Also note that package identifiers are typically `cryptographic hash `_ of the content of the package itself. Literals ~~~~~~~~ We now define all the literals that a program can handle:: Nat type literals: -- LitNatType n ∈ \d+ 64-bit integer literals: LitInt64 ∈ (-?)\d+ -- LitInt64 Numeric literals: LitNumeric ∈ ([+-]?)([1-9]\d+|0).\d* -- LitNumeric Date literals: LitDate ∈ \d{4}-\d{2}-\d{2} -- LitDate UTC timestamp literals: LitTimestamp ∈ \d{4}-\d{2}-\d{2}T\d{2}:\d{2}:\d{2}(.\d{1,3})?Z -- LitTimestamp UTF8 string literals: t ::= String -- LitText Party literals: LitParty ::= PartyIdString -- LitParty Contract ID literals: cid ::= cidV0 | cidV1 -- LitCid Rounding Mode Literals: -- LitRoundingMode LitRoundingMode ::= | ROUNDING_UP | ROUNDING_DOWN | ROUNDING_CEILING | ROUNDING_FLOOR | ROUNDING_HALF_UP | ROUNDING_HALF_DOWN | ROUNDING_HALF_EVEN | ROUNDING_UNNECESSARY The literals represent actual Daml-LF values: * A ``LitNatType`` represents a natural number between ``0`` and ``38``, bounds inclusive. * A ``LitInt64`` represents a standard signed 64-bit integer (integer between ``−2⁶³`` to ``2⁶³−1``). * A decimal numbers is a signed number that can be represented as a product `i * 10⁻ˢ` where `i` (the *unscaled value* of the number) is a signed integer without trailing zeros and `s` (the *scale* of the number) is a signed integer. The *precision* of a decimal numbers if the number of digits of its unscaled value (ignoring possible leading zeros). By convention the scale and the precision of zero are 0. Daml-LF distinguishes two kinds of decimal numbers: + A ``LitNumeric`` represents those decimal numbers that have a precision of at most 38 and a scale between ``0`` and ``37`` (bounds inclusive). + A ``LitBigNumeric`` represents those decimal numbers that have at most 2¹⁵ significant digits at the right and the left of the decimal point. Equivalently those are decimal numbers that respect `scale ≤ 2¹⁵` and `precision - scale < 2¹⁵`. * A ``LitDate`` represents the number of day since ``1970-01-01`` with allowed range from ``0001-01-01`` to ``9999-12-31`` and using a year-month-day format. * A ``LitTimestamp`` represents the number of microseconds since ``1970-01-01T00:00:00.000000Z`` with allowed range ``0001-01-01T00:00:00.000000Z`` to ``9999-12-31T23:59:59.999999Z`` using a year-month-day-hour-minute-second-microsecond format. * A ``LitText`` represents a `UTF8 string `_. * A ``LitParty`` represents a *party*. * A ``LitRoundingMode`` represents a *rounding mode* used by numerical operations. .. note:: A literal which is not backed by an actual value is not valid and is implicitly rejected by the syntax presented here. For instance, the literal ``9223372036854775808`` is not a valid ``LitInt64`` since it cannot be encoded as a signed 64-bits integer, i.e. it equals ``2⁶³``. Similarly,``2019-13-28`` is not a valid ``LitDate`` because there are only 12 months in a year. Number-like literals (``LitNatTyp``, ``LitInt64``, ``LitNumeric``, ``LitBigNumeric``, ``LitDate``, ``LitTimestamp``) are ordered by natural ordering. Text-like literals (``LitText``, ``LitParty``, and ``Contract ID``) are ordered lexicographically. Note that in the ASCII encoding, the character ``#`` comes before digits, meaning V0 Contract ID are ordered before V1 Contract ID. In the following we will denote the corresponding (non-strict) order by ``≤ₗ``. RoundingMode literals are ordered as they appear in the definition of ``LitRoundingMode``, e.g. ``ROUNDING_UP`` and ``ROUNDING_UNNECESSARY`` are the smallest and greatest rounding mode. Kinds, types, and expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. TODO We might want to consider changing the syntax for ``Mod``, since in our software we use the colon to separate the module name from the definition name inside the module. Then we can define our kinds, types, and expressions:: Kinds k ::= 'nat' -- KindNat [Daml-LF ≥ 1.7] | ek -- KindErasable Erasable Kind ek ::= ⋆ -- KindStar | k → ek -- KindArrow Module references Mod ::= PkdId:ModName -- ModPackage: module from a package Built-in types BuiltinType ::= 'TArrow' -- BTArrow: Arrow type | 'Int64' -- BTyInt64: 64-bit integer | 'Numeric' -- BTyNumeric: numeric, precision 38, parametric scale between 0 and 37 | 'BigNumeric' -- BTyBigNumeric: arbitrary precision decimal | 'RoundingMode' -- BTyRoundingMode: rounding mode to control BigNumeric operations. | 'Text' -- BTyText: UTF-8 string | 'Date' -- BTyDate | 'Timestamp' -- BTyTime: UTC timestamp | 'Party' -- BTyParty | 'Date' -- BTyDate: year, month, date triple | 'Unit' -- BTyUnit | 'Bool' -- BTyBool | 'List' -- BTyList | 'Optional' -- BTyOptional | 'TextMap' -- BTTextMap: map with string keys | 'GenMap' -- BTGenMap: map with general value keys [Daml-LF ≥ 1.11] | 'ContractId' -- BTyContractId | 'Any' -- BTyAny [Daml-LF ≥ 1.7] | 'TypeRep' -- BTTypeRep [Daml-LF ≥ 1.7] | 'Update' -- BTyUpdate | 'Scenario' -- BTyScenario | 'AnyException' -- BTyAnyException [Daml-LF ≥ 1.dev] | 'GeneralError' -- BTyGeneralError [Daml-LF ≥ 1.dev] | 'ArithmeticError' -- BTyArithmeticError [Daml-LF ≥ 1.dev] | 'ContractError' -- BTyContractError [Daml-LF ≥ 1.dev] Types (mnemonic: tau for type) τ, σ ::= α -- TyVar: Type variable | n -- TyNat: Nat Type [Daml-LF ≥ 1.7] | τ σ -- TyApp: Type application | ∀ α : k . τ -- TyForall: Universal quantification | BuiltinType -- TyBuiltin: Builtin type | Mod:T -- TyCon: type constructor | |Mod:S τ₁ … τₘ| -- TySyn: type synonym [Daml-LF ≥ 1.8] | ⟨ f₁: τ₁, …, fₘ: τₘ ⟩ -- TyStruct: Structural record type Expressions e ::= x -- ExpVar: Local variable | e₁ e₂ -- ExpApp: Application | e @τ -- ExpTyApp: Type application | λ x : τ . e -- ExpAbs: Abstraction | Λ α : k . e -- ExpTyAbs: Type abstraction | 'let' x : τ = e₁ 'in' e₂ -- ExpLet: Let | 'case' e 'of' p₁ → e₁ '|' … '|' pₙ → eₙ -- ExpCase: Pattern matching | () -- ExpUnit | 'True' -- ExpTrue | 'False' -- ExpFalse | LitInt64 -- ExpLitInt64: 64-bit integer literal | LitNumeric -- ExpLitNumeric: Numeric literal | LitBigNumeric -- ExpLitBigNumeric: BigNumeric literal | t -- ExpLitText: UTF-8 string literal | LitDate -- ExpLitDate: Date literal | LitTimestamp -- ExpLitTimestamp: UTC timestamp literal | LitParty -- ExpLitParty: Party literal | cid -- ExpLitContractId: Contract identifiers | LitRoundingMode -- ExpLitRoundingMode: Rounding Mode | F -- ExpBuiltin: Builtin function | Mod:W -- ExpVal: Defined value | Mod:T @τ₁ … @τₙ { f₁ = e₁, …, fₘ = eₘ } -- ExpRecCon: Record construction | Mod:T @τ₁ … @τₙ {f} e -- ExpRecProj: Record projection | Mod:T @τ₁ … @τₙ { e₁ 'with' f = e₂ } -- ExpRecUpdate: Record update | Mod:T:V @τ₁ … @τₙ e -- ExpVariantCon: Variant construction | Mod:T:E -- ExpEnumCon:Enum construction | ⟨ f₁ = e₁, …, fₘ = eₘ ⟩ -- ExpStructCon: Struct construction | e.f -- ExpStructProj: Struct projection | ⟨ e₁ 'with' f = e₂ ⟩ -- ExpStructUpdate: Struct update | 'Nil' @τ -- ExpListNil: Empty list | 'Cons' @τ e₁ e₂ -- ExpListCons: Cons list | 'None' @τ -- ExpOptionalNone: Empty Optional | 'Some' @τ e -- ExpOptionalSome: Non-empty Optional | [t₁ ↦ e₁; …; tₙ ↦ eₙ] -- ExpTextMap | 〚e₁ ↦ e₁; …; eₙ ↦ eₙ'〛 -- ExpGenMap [Daml-LF ≥ 1.11] | 'to_any' @τ e -- ExpToAny: Wrap a value of the given type in Any [Daml-LF ≥ 1.7] | 'from_any' @τ e -- ExpToAny: Extract a value of the given from Any or return None [Daml-LF ≥ 1.7] | 'type_rep' @τ -- ExpToTypeRep: A type representation [Daml-LF ≥ 1.7] | u -- ExpUpdate: Update expression | s -- ExpScenario: Scenario expression | 'throw' @σ @τ e -- ExpThrow: throw exception [Daml-LF ≥ 1.dev] | 'to_any_exception' @τ e -- ExpToAnyException: Turn a concrete exception into an 'AnyException' [Daml-LF ≥ 1.dev] | 'from_any_exception' @τ e -- ExpFromAnyException: Extract a concrete exception from an 'AnyException' [Daml-LF ≥ 1.dev] Patterns p ::= Mod:T:V x -- PatternVariant | Mod:T:E -- PatternEnum | 'Nil' -- PatternNil | 'Cons' xₕ xₜ -- PatternCons | 'None' -- PatternNone | 'Some' x -- PatternSome | 'True' -- PatternTrue | 'False' -- PatternFalse | () -- PatternUnit | _ -- PatternDefault Updates u ::= 'pure' @τ e -- UpdatePure | 'bind' x₁ : τ₁ ← e₁ 'in' e₂ -- UpdateBlock | 'create' @Mod:T e -- UpdateCreate | 'fetch' @Mod:T e -- UpdateFetch | 'exercise' @Mod:T Ch e₁ e₂ e₃ -- UpdateExercise | 'exercise_without_actors' @Mod:T Ch e₁ e₂ -- UpdateExerciseWithoutActors | 'exercise_by_key' @Mod:T Ch e₁ e₂ -- UpdateExerciseByKey [Daml-LF ≥ 1.11] | 'get_time' -- UpdateGetTime | 'fetch_by_key' @τ e -- UpdateFecthByKey | 'lookup_by_key' @τ e -- UpdateLookUpByKey | 'embed_expr' @τ e -- UpdateEmbedExpr | 'try' @τ e₁ 'catch' x. e₂ -- UpdateTryCatch [Daml-LF ≥ 1.dev] Scenario s ::= 'spure' @τ e -- ScenarioPure | 'sbind' x₁ : τ₁ ← e₁ 'in' e₂ -- ScenarioBlock | 'commit' @τ e u -- ScenarioCommit | 'must_fail_at' @τ e u -- ScenarioMustFailAt | 'pass' e -- ScenarioPass | 'sget_time' -- ScenarioGetTime | 'sget_party' e -- ScenarioGetParty | 'sembed_expr' @τ e -- ScenarioEmbedExpr .. note:: The explicit syntax for maps (cases ``ExpTextMap`` and ``ExpGenMap``) is forbidden in serialized programs. It is specified here to ease the definition of `values`_, `operational semantics`_ and `value comparison `_. In practice, `text map functions`_ and `generic map functions`_ are the only way to create and handle those objects. .. note:: The order of entries in maps (cases ``ExpTextMap`` and ``ExpGenMap``) is always significant. For text maps, the entries should be always ordered by keys. On the other hand, the order of entries in generic maps indicate the order in which the keys have been inserted into the map. .. note:: The distinction between kinds and erasable kinds is significant, because erasable kinds have no runtime representation. This affects the operational semantics. The right hand side of an arrow is always erasable. .. note:: The explicit syntax for BigNumeric literal (case ``ExpLitBigNumeric``) is forbidden in serialized programs. It is specified here to ease the definition of `values`_, `operational semantics`_ and `value comparison `_. In practice, `BigNumeric functions`_ are the only way to create and handle those objects. In the following, we will use ``τ₁ → τ₂`` as syntactic sugar for the type application ``('TArrow' τ₁ τ₂)`` where ``τ₁`` and ``τ₂`` are types. Definitions ~~~~~~~~~~~ Expressions and types contain references to definitions in packages available for usage:: Template choice kind ChKind ::= 'consuming' -- ChKindConsuming | 'non-consuming' -- ChKindNonConsuming Template key definition KeyDef ::= 'no_key' | 'key' τ eₖ eₘ Template choice definition ChDef ::= 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e -- ChDef Definitions Def ::= | 'record' T (α₁: k₁)… (αₙ: kₙ) ↦ { f₁ : τ₁, …, fₘ : τₘ } -- DefRecord: Nominal record type | 'variant' T (α₁: k₁)… (αₙ: kₙ) ↦ V₁ : τ₁ | … | Vₘ : τₘ -- DefVariant | 'enum' T ↦ E₁ | … | Eₘ -- DefEnum | 'synonym' S (α₁: k₁)… (αₙ: kₙ) ↦ τ -- DefTypeSynonym | 'val' W : τ ↦ e -- DefValue | 'tpl' (x : T) ↦ -- DefTemplate { 'precondition' e₁ , 'signatories' e₂ , 'observers' e₃ , 'agreement' e₄ , 'choices' { ChDef₁, …, ChDefₘ } , KeyDef } | 'exception' T ↦ { 'message' e } -- DefException [Daml-LF ≥ 1.dev] Module (mnemonic: delta for definitions) Δ ::= ε -- DefCtxEmpty | Def · Δ -- DefCtxCons PackageMetadata PackageMetadata ::= 'metadata' PackageNameString PackageVersionString -- PackageMetadata PackageModules PackageModules ∈ ModName ↦ Δ -- PackageModules Package Package ::= Package PackageModules PackageMetadata – since Daml-LF 1.8 Package ::= Package PackageModules -- until Daml-LF 1.8 Package collection Ξ ∈ pid ↦ Package -- Packages Feature flags ~~~~~~~~~~~~~ Modules are annotated with a set of feature flags. Those flags enables syntactical restrictions and semantics changes on the annotated module. The following feature flags are available: +-------------------------------------------+----------------------------------------------------------+ | Flag | Semantic meaning | +===========================================+==========================================================+ | ForbidPartyLiterals | Party literals are not allowed in a Daml-LF module. | | | (See `Party Literal restriction`_ for more details) | +-------------------------------------------+----------------------------------------------------------+ | DontDivulgeContractIdsInCreateArguments | contract IDs captured in ``create`` arguments are not | | | divulged, ``fetch`` is authorized if and only if the | | | authorizing parties contain at least one stakeholder of | | | the fetched contract ID. | | | The contract ID on which a choice is exercised | | | is divulged to all parties that witness the choice. | +-------------------------------------------+----------------------------------------------------------+ | DontDiscloseNonConsumingChoicesToObservers| When a non-consuming choice of a contract is exercised, | | | the resulting sub-transaction is not disclosed to the | | | observers of the contract. | +-------------------------------------------+----------------------------------------------------------+ Well-formed programs ^^^^^^^^^^^^^^^^^^^^ The section describes the type system of language and introduces some other restrictions over programs that are statically verified at loading. Type system ~~~~~~~~~~~ In all the type checking rules, we will carry around the packages available for usage ``Ξ``. Given a module reference ``Mod`` equals to ``('Package' pid ModName)``, we will denote the corresponding definitions as ``〚Ξ〛Mod`` where ``ModName`` is looked up in package ``Ξ(pid)``; Expressions do also contain references to built-in functions. Any built-in function ``F`` comes with a fixed type, which we will denote as ``𝕋(F)``. See the `Built-in functions`_ section for the complete list of built-in functions and their respective types. Type normalization .................. First, we define the type normalization relation ``↠`` over types, which inlines type synonym definitions, and normalizes struct types to remove dependence on the order of fields :: ——————————————————————————————————————————————— RewriteVar α ↠ α ——————————————————————————————————————————————— RewriteNat n ↠ n ——————————————————————————————————————————————— RewriteBuiltin BuiltinType ↠ BuiltinType ———————————————————————————————————————————————— RewriteTyCon Mod:T ↠ Mod:T 'synonym' S (α₁:k₁) … (αₙ:kₙ) ↦ τ ∈ 〚Ξ〛Mod τ ↠ σ τ₁ ↠ σ₁ ⋯ τₙ ↠ σₙ ——————————————————————————————————————————————— RewriteSynonym |Mod:S τ₁ … τₙ| ↠ σ[α₁ ↦ σ₁, …, αₙ ↦ σₙ] τ₁ ↠ σ₁ ⋯ τₙ ↠ σₙ [f₁, …, fₘ] sorts lexicographically to [fⱼ₁, …, fⱼₘ] ———————————————————————————————————————————————— RewriteStruct ⟨ f₁: τ₁, …, fₘ: τₘ ⟩ ↠ ⟨ fⱼ₁: σⱼ₁, …, fⱼₘ: σⱼₘ ⟩ τ₁ ↠ σ₁ τ₂ ↠ σ₂ ———————————————————————————————————————————————— RewriteApp τ₁ τ₂ ↠ σ₁ σ₂ τ ↠ σ ———————————————————————————————————————————————— RewriteForall ∀ α : k . τ ↠ ∀ α : k . σ Note that the relation ``↠`` defines a partial normalization function over types as soon as: 1. there is at most one definition for a type synonym ``S`` in each module 2. there is no cycles between type synonym definitions. These two properties will be enforced by the notion of `well-formedness `_ defined below. Note ``↠`` is undefined on type contains an undefined type synonym or a type synonym applied to a wrong number. Such types are assumed non well-formed and will be rejected by the Daml-LF type checker. Well-formed types ................. We now formally defined *well-formed types*. :: Type context: Γ ::= ε -- CtxEmpty | α : k · Γ -- CtxVarTyKind | x : τ · Γ -- CtxVarExpType ┌───────────────┐ Well-formed types │ Γ ⊢ τ : k │ └───────────────┘ α : k ∈ Γ ————————————————————————————————————————————— TyVar Γ ⊢ α : k ————————————————————————————————————————————— TyNat Γ ⊢ n : 'nat' Γ ⊢ τ : k₁ → k₂ Γ ⊢ σ : k₁ ————————————————————————————————————————————— TyApp Γ ⊢ τ σ : k₂ α : k · Γ ⊢ τ : ⋆ ————————————————————————————————————————————— TyForall Γ ⊢ ∀ α : k . τ : ⋆ ————————————————————————————————————————————— TyArrow Γ ⊢ 'TArrow' : ⋆ → ⋆ ————————————————————————————————————————————— TyUnit Γ ⊢ 'Unit' : ⋆ ————————————————————————————————————————————— TyBool Γ ⊢ 'Bool' : ⋆ ————————————————————————————————————————————— TyInt64 Γ ⊢ 'Int64' : ⋆ ————————————————————————————————————————————— TyNumeric Γ ⊢ 'Numeric' : 'nat' → ⋆ ————————————————————————————————————————————— TyBigNumeric Γ ⊢ 'BigNumeric' : ⋆ ————————————————————————————————————————————— TyRoundingMode Γ ⊢ 'RoundingMode' : ⋆ ————————————————————————————————————————————— TyText Γ ⊢ 'Text' : ⋆ ————————————————————————————————————————————— TyDate Γ ⊢ 'Date' : ⋆ ————————————————————————————————————————————— TyTimestamp Γ ⊢ 'Timestamp' : ⋆ ————————————————————————————————————————————— TyParty Γ ⊢ 'Party' : ⋆ ————————————————————————————————————————————— TyList Γ ⊢ 'List' : ⋆ → ⋆ ————————————————————————————————————————————— TyOptional Γ ⊢ 'Optional' : ⋆ → ⋆ ————————————————————————————————————————————— TyTextMap Γ ⊢ 'TextMap' : ⋆ → ⋆ ————————————————————————————————————————————— TyGenMap Γ ⊢ 'GenMap' : ⋆ → ⋆ → ⋆ ————————————————————————————————————————————— TyContractId Γ ⊢ 'ContractId' : ⋆ → ⋆ ————————————————————————————————————————————— TyAny Γ ⊢ 'Any' : ⋆ ————————————————————————————————————————————— TyTypeRep Γ ⊢ 'TypeRep' : ⋆ 'record' T (α₁:k₁) … (αₙ:kₙ) ↦ … ∈ 〚Ξ〛Mod ————————————————————————————————————————————— TyRecordCon Γ ⊢ Mod:T : k₁ → … → kₙ → ⋆ 'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … ∈ 〚Ξ〛Mod ————————————————————————————————————————————— TyVariantCon Γ ⊢ Mod:T : k₁ → … → kₙ → ⋆ 'enum' T ↦ … ∈ 〚Ξ〛Mod ————————————————————————————————————————————— TyEnumCon Γ ⊢ Mod:T : ⋆ Γ ⊢ τ₁ : ⋆ … Γ ⊢ τₙ : ⋆ f₁ < … < fₙ lexicographically ————————————————————————————————————————————— TyStruct Γ ⊢ ⟨ f₁: τ₁, …, fₙ: τₙ ⟩ : ⋆ ————————————————————————————————————————————— TyUpdate Γ ⊢ 'Update' : ⋆ → ⋆ ————————————————————————————————————————————— TyScenario Γ ⊢ 'Scenario' : ⋆ → ⋆ ————————————————————————————————————————————— TyAnyException [Daml-LF ≥ 1.dev] Γ ⊢ 'AnyException' : ⋆ ————————————————————————————————————————————— TyGeneralError [Daml-LF ≥ 1.dev] Γ ⊢ 'GeneralError' : ⋆ ————————————————————————————————————————————— TyArithmeticError [Daml-LF ≥ 1.dev] Γ ⊢ 'ArithmeticError' : ⋆ ————————————————————————————————————————————— TyContractError [Daml-LF ≥ 1.dev] Γ ⊢ 'ContractError' : ⋆ Exception types ............... To state the typing rules related to exception handling, we need the notion of *exception types*. As the name suggests, values of these types are the ones that can be thrown and caught by the exception handling mechanism. :: ┌────────┐ Exception types │ ⊢ₑ τ │ └────────┘ 'exception' T ↦ … ∈ 〚Ξ〛Mod ———————————————————————————————————————————————————————————————— ExnTyDefException ⊢ₑ Mod:T ———————————————————————————————————————————————————————————————— ExnTyGeneralError ⊢ₑ 'GeneralError' ———————————————————————————————————————————————————————————————— ExnTyArithmeticError ⊢ₑ 'ArithmeticError' ———————————————————————————————————————————————————————————————— ExnTyContractError ⊢ₑ 'ContractError' Note that ``'AnyException'`` is not an exception type in order to avoid having ``'AnyException'`` wrapped into ``'AnyException'``. Well-formed expression ...................... Then we define *well-formed expressions*. :: ┌───────────────┐ Well-formed expressions │ Γ ⊢ e : τ │ └───────────────┘ x : τ ∈ Γ ——————————————————————————————————————————————————————————————— ExpDefVar Γ ⊢ x : τ Γ ⊢ e₁ : τ₁ → τ₂ Γ ⊢ e₂ : τ₁ ——————————————————————————————————————————————————————————————— ExpApp Γ ⊢ e₁ e₂ : τ₂ τ ↠ τ' Γ ⊢ τ' : k Γ ⊢ e : ∀ α : k . σ ——————————————————————————————————————————————————————————————— ExpTyApp Γ ⊢ e @τ : σ[α ↦ τ'] τ ↠ τ' x : τ' · Γ ⊢ e : σ Γ ⊢ τ' : ⋆ ——————————————————————————————————————————————————————————————— ExpAbs Γ ⊢ λ x : τ . e : τ' → σ α : k · Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— ExpTyAbs Γ ⊢ Λ α : k . e : ∀ α : k . τ τ ↠ τ' Γ ⊢ e₁ : τ' Γ ⊢ τ' : ⋆ x : τ' · Γ ⊢ e₂ : σ ——————————————————————————————————————————————————————————————— ExpLet Γ ⊢ 'let' x : τ = e₁ 'in' e₂ : σ ——————————————————————————————————————————————————————————————— ExpUnit Γ ⊢ () : 'Unit' ——————————————————————————————————————————————————————————————— ExpTrue Γ ⊢ 'True' : 'Bool' ——————————————————————————————————————————————————————————————— ExpFalse Γ ⊢ 'False' : 'Bool' τ ↠ τ' Γ ⊢ τ' : ⋆ ——————————————————————————————————————————————————————————————— ExpListNil Γ ⊢ 'Nil' @τ : 'List' τ' τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ eₕ : τ' Γ ⊢ eₜ : 'List' τ' ——————————————————————————————————————————————————————————————— ExpListCons Γ ⊢ 'Cons' @τ eₕ eₜ : 'List' τ' τ ↠ τ' Γ ⊢ τ' : ⋆ —————————————————————————————————————————————————————————————— ExpOptionalNone Γ ⊢ 'None' @τ : 'Optional' τ' τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ' ——————————————————————————————————————————————————————————————— ExpOptionalSome Γ ⊢ 'Some' @τ e : 'Optional' τ' ∀ i,j ∈ 1, …, n i > j ∨ tᵢ ≤ tⱼ Γ ⊢ e₁ : τ Γ ⊢ eₙ : τ ——————————————————————————————————————————————————————————————— ExpTextMap Γ ⊢ [t₁ ↦ e₁; …; tₙ ↦ eₙ] : 'TextMap' τ Γ ⊢ e₁ : σ Γ ⊢ eₙ : σ Γ ⊢ e₁' : τ Γ ⊢ eₙ' : τ ——————————————————————————————————————————————————————————————— ExpGenMap (*) Γ ⊢ 〚e₁ ↦ e₁'; …; eₙ ↦ eₙ'〛: GenMap σ τ τ contains no quantifiers and no type synonyms ε ⊢ τ : ⋆ Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— ExpToAny Γ ⊢ 'to_any' @τ e : 'Any' τ contains no quantifiers and no type synonyms ε ⊢ τ : ⋆ Γ ⊢ e : 'Any' ——————————————————————————————————————————————————————————————— ExpFromAny Γ ⊢ 'from_any' @τ e : 'Optional' τ τ contains no quantifiers and no type synonyms ε ⊢ τ : ⋆ ——————————————————————————————————————————————————————————————— ExpTypeRep Γ ⊢ 'type_rep' @τ : 'TypeRep' ——————————————————————————————————————————————————————————————— ExpBuiltin Γ ⊢ F : 𝕋(F) ——————————————————————————————————————————————————————————————— ExpLitInt64 Γ ⊢ LitInt64 : 'Int64' n = scale(LitNumeric) ——————————————————————————————————————————————————————————————— ExpLitNumeric Γ ⊢ LitNumeric : 'Numeric' n ——————————————————————————————————————————————————————————————— ExpBigNumeric Γ ⊢ LitBigNumeric : 'BigNumeric' ——————————————————————————————————————————————————————————————— ExpLitText Γ ⊢ t : 'Text' ——————————————————————————————————————————————————————————————— ExpLitDate Γ ⊢ LitDate : 'Date' ——————————————————————————————————————————————————————————————— ExpLitTimestamp Γ ⊢ LitTimestamp : 'Timestamp' ——————————————————————————————————————————————————————————————— ExpLitParty Γ ⊢ LitParty : 'Party' 'tpl' (x : T) ↦ { … } ∈ 〚Ξ〛Mod ——————————————————————————————————————————————————————————————— ExpLitContractId Γ ⊢ cid : 'ContractId' Mod:T ——————————————————————————————————————————————————————————————— ExpLitRoundingMode Γ ⊢ LitRoundingMode : 'RoundingMode' τ ↠ τ' 'val' W : τ ↦ … ∈ 〚Ξ〛Mod ——————————————————————————————————————————————————————————————— ExpVal Γ ⊢ Mod:W : τ' 'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { f₁:τ₁, …, fₘ:τₘ } ∈ 〚Ξ〛Mod σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ' Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ τ₁ ↠ τ₁' Γ ⊢ e₁ : τ₁'[α₁ ↦ σ₁', …, αₙ ↦ σₙ'] ⋮ τₘ ↠ τₘ' Γ ⊢ eₘ : τₘ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ'] ———————————————————————————————————————————————————————————————— ExpRecCon Γ ⊢ Mod:T @σ₁ … @σₙ { f₁ = e₁, …, fₘ = eₘ } : Mod:T σ₁' … σₙ' 'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { …, fᵢ : τᵢ, … } ∈ 〚Ξ〛Mod τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ' Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ Γ ⊢ e : Mod:T σ₁' … σₙ' ——————————————————————————————————————————————————————————————— ExpRecProj Γ ⊢ Mod:T @σ₁ … @σₙ {f} e : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ'] 'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { …, fᵢ : τᵢ, … } ∈ 〚Ξ〛Mod τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ' Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ Γ ⊢ e : Mod:T σ₁' ⋯ σₙ' Γ ⊢ eᵢ : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ'] ———————————————————————————————————————————————————————————————– ExpRecUpdate Γ ⊢ Mod:T @σ₁ … @σₙ { e 'with' fᵢ = eᵢ } : Mod:T σ₁' … σₙ' 'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … | Vᵢ : τᵢ | … ∈ 〚Ξ〛Mod τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ' Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ Γ ⊢ e : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ'] ——————————————————————————————————————————————————————————————— ExpVarCon Γ ⊢ Mod:T:Vᵢ @σ₁ … @σₙ e : Mod:T σ₁' … σₙ' 'enum' T ↦ … | Eᵢ | … ∈ 〚Ξ〛Mod ——————————————————————————————————————————————————————————————— ExpEnumCon Γ ⊢ Mod:T:Eᵢ : Mod:T ⟨ f₁: τ₁, …, fₘ: τₘ ⟩ ↠ σ Γ ⊢ σ : ⋆ Γ ⊢ e₁ : τ₁ ⋯ Γ ⊢ eₘ : τₘ ——————————————————————————————————————————————————————————————— ExpStructCon Γ ⊢ ⟨ f₁ = e₁, …, fₘ = eₘ ⟩ : σ Γ ⊢ e : ⟨ …, fᵢ: τᵢ, … ⟩ ——————————————————————————————————————————————————————————————— ExpStructProj Γ ⊢ e.fᵢ : τᵢ Γ ⊢ e : ⟨ f₁: τ₁, …, fᵢ: τᵢ, …, fₙ: τₙ ⟩ Γ ⊢ eᵢ : τᵢ ——————————————————————————————————————————————————————————————— ExpStructUpdate Γ ⊢ ⟨ e 'with' fᵢ = eᵢ ⟩ : ⟨ f₁: τ₁, …, fₙ: τₙ ⟩ n ≥ 1 Γ ⊢ e : τ Γ ⊢ τ // alt₁ : σ ⋮ Γ ⊢ τ // altₙ : σ τ ⊲ alt₁, …, altₙ ——————————————————————————————————————————————————————————————— ExpCase Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ Γ ⊢ σ : ⋆ ⊢ₑ τ Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— ExpThrow [Daml-LF ≥ 1.dev] Γ ⊢ 'throw' @σ @τ @e : σ ⊢ₑ τ Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— ExpToAnyException [Daml-LF ≥ 1.dev] Γ ⊢ 'to_any_exception' @τ e : 'AnyException' ⊢ₑ τ Γ ⊢ e : 'AnyException' ——————————————————————————————————————————————————————————————— ExpFromAnyException [Daml-LF ≥ 1.dev] Γ ⊢ 'from_any_exception' @τ e : 'Optional' τ Γ ⊢ τ : ⋆ Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— UpdPure Γ ⊢ 'pure' e : 'Update' τ τ₁ ↠ τ₁' Γ ⊢ τ₁' : ⋆ Γ ⊢ e₁ : 'Update' τ₁' x₁ : τ₁' · Γ ⊢ e₂ : 'Update' τ₂ ——————————————————————————————————————————————————————————————— UpdBlock Γ ⊢ 'bind' x₁ : τ₁ ← e₁ 'in' e₂ : 'Update' τ₂ 'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod Γ ⊢ e : Mod:T ——————————————————————————————————————————————————————————————— UpdCreate Γ ⊢ 'create' @Mod:T e : 'Update' ('ContractId' Mod:T) 'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' … ↦ …, … } } ∈ 〚Ξ〛Mod Γ ⊢ e₁ : 'ContractId' Mod:T Γ ⊢ e₂ : 'List' 'Party' Γ ⊢ e₃ : τ ——————————————————————————————————————————————————————————————— UpdExercise Γ ⊢ 'exercise' @Mod:T Ch e₁ e₂ e₃ : 'Update' σ 'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' … ↦ …, … } } ∈ 〚Ξ〛Mod Γ ⊢ e₁ : 'ContractId' Mod:T Γ ⊢ e₂ : τ ——————————————————————————————————————————————————————————————— UpdExerciseWithouActors Γ ⊢ 'exercise_without_actors' @Mod:T Ch e₁ e₂ : 'Update' σ 'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' … ↦ …, … }, 'key' τₖ … } ∈ 〚Ξ〛Mod Γ ⊢ e₁ : τₖ Γ ⊢ e₂ : τ ——————————————————————————————————————————————————————————————— UpdExerciseByKey Γ ⊢ 'exercise_by_key' @Mod:T Ch e₁ e₂ : 'Update' σ 'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod Γ ⊢ e₁ : 'ContractId' Mod:T ——————————————————————————————————————————————————————————————— UpdFetch Γ ⊢ 'fetch' @Mod:T e₁ : 'Update' Mod:T ——————————————————————————————————————————————————————————————— UpdGetTime Γ ⊢ 'get_time' : 'Update' 'Timestamp' 'tpl' (x : T) ↦ { …, 'key' τ …, … } ∈ 〚Ξ〛Mod Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— UpdFetchByKey Γ ⊢ 'fetch_by_key' @Mod:T e : 'Update' ⟨ 'contractId' : 'ContractId' @Mod:T 'contract' : Mod:T ⟩ 'tpl' (x : T) ↦ { …, 'key' τ …, … } ∈ 〚Ξ〛Mod Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— UpdLookupByKey Γ ⊢ 'lookup_by_key' @Mod:T e : 'Update' ('Optional' (ContractId Mod:T)) τ ↠ τ' Γ ⊢ e : 'Update' τ' ——————————————————————————————————————————————————————————————— UpdEmbedExpr Γ ⊢ 'embed_expr' @τ e : 'Update' τ' τ ↠ τ' Γ ⊢ e₁ : 'Update' τ' x : 'AnyException' · Γ ⊢ e₂ : 'Optional' ('Update' τ') ——————————————————————————————————————————————————————————————— UpdTryCatch [Daml-LF ≥ 1.dev] Γ ⊢ 'try' @τ e₁ 'catch' x. e₂ : 'Update' τ' Γ ⊢ τ : ⋆ Γ ⊢ e : τ ——————————————————————————————————————————————————————————————— ScnPure Γ ⊢ 'spure' e : 'Scenario' τ τ₁ ↠ τ₁' Γ ⊢ τ₁' : ⋆ Γ ⊢ e₁ : 'Scenario' τ₁' x₁ : τ₁' · Γ ⊢ e₂ : 'Scenario' τ₂ ——————————————————————————————————————————————————————————————— ScnBlock Γ ⊢ 'sbind' x₁ : τ₁ ← e₁ 'in' e₂ : 'Scenario' τ₂ Γ ⊢ e : 'Party' τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ u : 'Uptate' τ ——————————————————————————————————————————————————————————————— ScnCommit Γ ⊢ 'commit' @τ e u : 'Scenario' τ Γ ⊢ e : 'Party' τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ u : 'Uptate' τ ——————————————————————————————————————————————————————————————— ScnMustFailAt Γ ⊢ 'must_fail_at' @τ e u : 'Scenario' 'Unit' Γ ⊢ e : 'Int64' ——————————————————————————————————————————————————————————————— ScnPass Γ ⊢ 'pass' e : 'Scenario' 'Timestamp' Γ ⊢ e : 'Text' ——————————————————————————————————————————————————————————————— ScnGetParty Γ ⊢ 'get_party' e : 'Scenario' 'Party' τ ↠ τ' Γ ⊢ e : 'Scenario' τ' ——————————————————————————————————————————————————————————————— ScnEmbedExpr Γ ⊢ 'sembed_expr' @τ e : 'Scenario' τ' .. note :: Unlike ``ExpTextMap``, the ``ExpGenMap`` rule does not enforce uniqueness of key. In practice, the uniqueness is enforced by the `builtin functions `_ that are the only way to handle generic maps in a serialized program, the explicit syntax for maps being forbidden in serialized programs. Well-formed case alternatives ............................. Case expressions ``Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ`` require the notion of well-formed case alternatives ``Γ ⊢ τ // alt : σ`` defined here. To simplify the presentation, we omit the assumption that the scrutinee type ``τ`` is well-formed, in the rules below. :: ┌──────────────────┐ Well-formed case alternatives │ Γ ⊢ τ // alt : σ │ └──────────────────┘ 'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … | V : τ | … ∈ 〚Ξ〛Mod τ ↠ τ' x : τ'[α₁ ↦ τ₁, …, αₙ ↦ τₙ] · Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltVariant Γ ⊢ Mod:T τ₁ … τₙ // Mod:T:V x → e : σ 'enum' T ↦ … | E | … ∈ 〚Ξ〛Mod Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltEnum Γ ⊢ Mod:T // Mod:T:E → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltNil Γ ⊢ 'List' τ // 'Nil' → e : σ xₕ ≠ xₜ xₕ : τ · xₜ : 'List' τ · Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltCons Γ ⊢ 'List' τ // 'Cons' xₕ xₜ → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltNone Γ ⊢ 'Optional' τ // 'None' → e : σ x : τ · Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltSome Γ ⊢ 'Optional' τ // 'Some' x → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltTrue Γ ⊢ 'Bool' // 'True' → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltFalse Γ ⊢ 'Bool' // 'False' → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltUnit Γ ⊢ 'Unit' // () → e : σ Γ ⊢ e : σ ——————————————————————————————————————————————————————————————— AltDefault Γ ⊢ τ // _ → e : σ Pattern match exhaustiveness ............................ Case expressions ``Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ`` also require their patterns to be exhaustive, which is defined here. :: ┌─────────────────────┐ Pattern match exhaustiveness │ τ ⊲ alt₁, …, altₙ │ └─────────────────────┘ 'variant' T (α₁:k₁) … (αᵣ:kᵣ) ↦ V₁ : σ₁ | … | Vₘ : σₘ ∈ 〚Ξ〛Mod i₁, i₂, …, iₘ ∈ {1, …, n} altᵢ₁ = Mod:T:V₁ x₁ → e₁ altᵢ₂ = Mod:T:V₂ x₂ → e₂ ⋮ altᵢₘ = Mod:T:Vₘ xₘ → eₘ ——————————————————————————————————————————————————————————————— ExhaustVariant Mod:T τ₁ … τᵣ ⊲ alt₁, …, altₙ 'enum' T ↦ E₁ | … | Eₘ ∈ 〚Ξ〛Mod i₁, i₂, …, iₘ ∈ {1, …, n} altᵢ₁ = Mod:T:E₁ → e₁ altᵢ₂ = Mod:T:E₂ → e₂ ⋮ altᵢₘ = Mod:T:Eₘ → eₘ ——————————————————————————————————————————————————————————————— ExhaustEnum Mod:T ⊲ alt₁, …, altₙ i, j ∈ {1, …, n} altᵢ = 'Nil' → e₁ altⱼ = 'Cons' xₕ xₜ → e₂ ——————————————————————————————————————————————————————————————— ExhaustList 'List' τ ⊲ alt₁, …, altₙ i, j ∈ {1, …, n} altᵢ = 'None' → e₁ altⱼ = 'Some' x → e₂ ——————————————————————————————————————————————————————————————— ExhaustOptional 'Optional' τ ⊲ alt₁, …, altₙ i, j ∈ {1, …, n} altᵢ = 'True' → e₁ altⱼ = 'False' → e₂ ——————————————————————————————————————————————————————————————— ExhaustBool 'Bool' ⊲ alt₁, …, altₙ i ∈ {1, …, n} altᵢ = () → e ——————————————————————————————————————————————————————————————— ExhaustUnit 'Unit' ⊲ alt₁, …, altₙ i ∈ {1, …, n} altᵢ = _ → e ——————————————————————————————————————————————————————————————— ExhaustDefault τ ⊲ alt₁, …, altₙ Serializable types .................. To define the validity of definitions, modules, and packages, we need to first define *serializable* types. As the name suggests, serializable types are the types whose values can be persisted on the ledger. :: ┌────────┐ Serializable types │ ⊢ₛ τ │ └────────┘ ———————————————————————————————————————————————————————————————— STyUnit ⊢ₛ 'Unit' ———————————————————————————————————————————————————————————————— STyBool ⊢ₛ 'Bool' ⊢ₛ τ ———————————————————————————————————————————————————————————————— STyList ⊢ₛ 'List' τ ⊢ₛ τ ———————————————————————————————————————————————————————————————— STyOptional ⊢ₛ 'Optional' τ ———————————————————————————————————————————————————————————————— STyInt64 ⊢ₛ 'Int64' ———————————————————————————————————————————————————————————————— STyNumeric ⊢ₛ 'Numeric' n ———————————————————————————————————————————————————————————————— STyText ⊢ₛ 'Text' ———————————————————————————————————————————————————————————————— STyDate ⊢ₛ 'Date' ———————————————————————————————————————————————————————————————— STyTimestamp ⊢ₛ 'Timestamp' ———————————————————————————————————————————————————————————————— STyParty ⊢ₛ 'Party' ⊢ₛ τ ———————————————————————————————————————————————————————————————— STyCid ⊢ₛ 'ContractId' τ 'record' T α₁ … αₙ ↦ { f₁: σ₁, …, fₘ: σₘ } ∈ 〚Ξ〛Mod ⊢ₛ σ₁[α₁ ↦ τ₁, …, αₙ ↦ τₙ] ⋮ ⊢ₛ σₘ[α₁ ↦ τ₁, …, αₙ ↦ τₙ] ⊢ₛ τ₁ ⋮ ⊢ₛ τₙ ———————————————————————————————————————————————————————————————— STyRecConf ⊢ₛ Mod:T τ₁ … τₙ 'variant' T α₁ … αₙ ↦ V₁: σ₁ | … | Vₘ: σₘ ∈ 〚Ξ〛Mod m ≥ 1 ⊢ₛ σ₁[α₁ ↦ τ₁, …, αₙ ↦ τₙ] ⋮ ⊢ₛ σₘ[α₁ ↦ τ₁, …, αₙ ↦ τₙ] ⊢ₛ τ₁ ⋮ ⊢ₛ τₙ ———————————————————————————————————————————————————————————————— STyVariantCon ⊢ₛ Mod:T τ₁ … τₙ 'enum' T ↦ E₁: σ₁ | … | Eₘ: σₘ ∈ 〚Ξ〛Mod m ≥ 1 ———————————————————————————————————————————————————————————————— STyEnumCon ⊢ₛ Mod:T ———————————————————————————————————————————————————————————————— STyGeneralError ⊢ₛ 'GeneralError' ———————————————————————————————————————————————————————————————— STyArithmeticError ⊢ₛ 'ArithmeticError' ———————————————————————————————————————————————————————————————— STyContractError ⊢ₛ 'ContractError' Note that 1. Structs are *not* serializable. 2. Type synonyms are *not* serializable. 3. Uninhabited variant and enum types are *not* serializable. 4. For a data type to be serializable, *all* type parameters must be instantiated with serializable types, even phantom ones. Well-formed-definitions ....................... Finally, we specify well-formed definitions. Note that these rules work also under a set of packages available for usage ``Ξ``. Moreover, they also have the current module name, ``ModName``, in scope (needed for the ``DefTemplate`` rule). :: ┌────────┐ Well-formed definitions │ ⊢ Def │ └────────┘ τ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆ ⋮ τ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆ ——————————————————————————————————————————————————————————————— DefRec ⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ { f₁: τ₁, …, fₘ: τₘ } τ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆ ⋮ τ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆ ——————————————————————————————————————————————————————————————— DefVariant ⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ V₁: τ₁ | … | Vₘ: τₘ ——————————————————————————————————————————————————————————————— DefEnum ⊢ 'enum' T ↦ E₁ | … | Eₘ τ ↠ τ' (α₁:k₁) … (αₙ:kₙ) · Γ ⊢ τ' : ⋆ ——————————————————————————————————————————————————————————————— DefTypeSynonym ⊢ 'synonym' S (α₁: k₁) … (αₙ: kₙ) ↦ τ τ ↠ τ' ε ⊢ e : τ' ——————————————————————————————————————————————————————————————— DefValue ⊢ 'val' W : τ ↦ e 'record' T ↦ { f₁ : τ₁, …, fₙ : τₙ } ∈ 〚Ξ〛Mod ⊢ₛ Mod:T x : Mod:T ⊢ eₚ : 'Bool' x : Mod:T ⊢ eₛ : 'List' 'Party' x : Mod:T ⊢ eₒ : 'List' 'Party' x : Mod:T ⊢ eₐ : 'Text' x : Mod:T ⊢ ChDef₁ ⋯ x : Mod:T ⊢ ChDefₘ x : Mod:T ⊢ KeyDef ——————————————————————————————————————————————————————————————— DefTemplate ⊢ 'tpl' (x : T) ↦ { 'precondition' eₚ , 'signatories' eₛ , 'observers' eₒ , 'agreement' eₐ , 'choices' { ChDef₁, …, ChDefₘ } , KeyDef } 'record' T ↦ { f₁ : τ₁, …, fₙ : τₙ } ∈ 〚Ξ〛Mod ⊢ₛ Mod:T ⊢ e : Mod:T → 'Text' ——————————————————————————————————————————————————————————————— DefException [Daml-LF ≥ 1.dev] ⊢ 'exception' T ↦ { 'message' e } ┌───────────────────┐ Well-formed choices │ x : Mod:T ⊢ ChDef │ └───────────────────┘ ⊢ₛ τ ⊢ₛ σ y : 'ContractId' Mod:T · z : τ · x : Mod:T ⊢ e : 'Update' σ z : τ · x : Mod:T ⊢ eₚ : 'List' 'Party' z : τ · x : Mod:T ⊢ eₒ : 'List' 'Party' ——————————————————————————————————————————————————————————————— ChDef x : Mod:T ⊢ 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e ┌────────────┐ Valid key │ ⊢ₖ e : τ │ └────────────┘ ——————————————————————————————————————————————————————————————— ExpRecProj ⊢ₖ x ⊢ₖ e ——————————————————————————————————————————————————————————————— ExpRecProj ⊢ₖ Mod:T @τ₁ … @τₙ {f} e ⊢ₖ e₁ ⋯ ⊢ₖ eₘ ———————————————————————————————————————————————————————————————— ExpRecCon ⊢ₖ Mod:T @σ₁ … @σₙ { f₁ = e₁, …, fₘ = eₘ } ┌────────────┐ Well-formed keys │ Γ ⊢ KeyDef │ └────────────┘ ——————————————————————————————————————————————————————————————— KeyDefNone Γ ⊢ 'no_key' ⊢ₛ τ Γ ⊢ eₖ : τ ⊢ₖ eₖ [Daml-LF = 1.3] ε ⊢ eₘ : τ → 'List' 'Party' ——————————————————————————————————————————————————————————————— KeyDefSome Γ ⊢ 'key' τ eₖ eₘ Naturally, we will say that modules and packages are well-formed if all the definitions they contain are well-formed. Template coherence ~~~~~~~~~~~~~~~~~~ Each template definition is paired to a record ``T`` with no type arguments (see ``DefTemplate`` rule). To avoid ambiguities, we want to make sure that each record type ``T`` has at most one template definition associated to it. We term this restriction *template coherence* since it's a requirement reminiscent of the coherence requirement of Haskell type classes. Specifically, a template definition is *coherent* if: * Its argument data type is defined in the same module that the template is defined in; * Its argument data type is not an argument to any other template. Exception coherence ~~~~~~~~~~~~~~~~~~~ The *exception coherence* condition is literally the same as the template coherence condition with "template" replaced by "exception". We further require that no type has a template definition and an exception definition associated to it. Party literal restriction ~~~~~~~~~~~~~~~~~~~~~~~~~ .. TODO I think this is incorrect, and actually before the ``ForbidPartyLiterals`` feature flag party literals were allowed everywhere. The usage of party literals is restricted in Daml-LF. By default, party literals are neither allowed in templates nor in values used in templates directly or indirectly. In practice, this restricted the usage of party literals to test cases written in Daml-LF. Usage of party literals can be completely forbidden thanks to the `feature flag `_ ``ForbidPartyLiterals``. If this flag is on, any occurrence of a party literal anywhere in the module makes the module not well-formed. Name collision restriction ~~~~~~~~~~~~~~~~~~~~~~~~~~ Daml-LF relies on `names and identifiers `_ to refer to different kinds of constructs such as modules, type constructors, variants constructor, and fields. These are relative; type names are relative to modules; field names are relative to type record and so one. They live in different namespaces. For example, the space names for module and type is different. Fully resolved name ................... Daml-LF restricts the way names and identifiers are used within a package. This restriction relies on the notion of *fully resolved name* construct as follows: * The *fully resolved name* of the module ``Mod`` is ``Mod``. * The *fully resolved name* of a record type constructor ``T`` defined in the module ``Mod`` is ``Mod.T``. * The *fully resolved name* of a variant type constructor ``T`` defined in the module ``Mod`` is ``Mod.T``. * The *fully resolved name* of a enum type constructor ``T`` defined in the module ``Mod`` is ``Mod.T``. * The *fully resolved name* of a type synonym ``S`` defined in the module ``Mod`` is ``Mod.S``. * The *fully resolved name* of a field ``fᵢ`` of a record type definition ``'record' T … ↦ { …, fᵢ: τᵢ, … }`` defined in the module ``Mod`` is ``Mod.T.fᵢ`` * The *fully resolved name* of a variant constructor ``Vᵢ`` of a variant type definition ``'variant' T … ↦ … | Vᵢ: τᵢ | …`` defined in the module ``Mod`` is ``Mod.T.Vᵢ``. * The *fully resolved name* of a enum constructor ``Eᵢ`` of a enum type definition ``'enum' T ↦ … | Eᵢ | …`` defined in the module ``Mod`` is ``Mod.T.Eᵢ``. * The *fully resolved name* of a choice ``Ch`` of a template definition ``'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch … ↦ …, … } }`` defined in the module ``Mod`` is ``Mod.T.Ch``. Name collisions ............... A so-called *name collision* occurs if two fully resolved names in a package are equal *ignoring case*. The following are examples of collisions: * A package contains two modules with the same name; * A module defines two types with the same name, one lowercase and the other one uppercase; * A record contains two fields with the same name; * A package contains a module ``A.B`` and a module ``A`` that defines the type ``B``; * A package contains a module ``A.B`` that defines the type ``C`` together with a module ``A`` that defines the type ``B.C``. Note that templates do not have names, and therefore can not cause collisions. Note also that value references are not concerned with collisions as defined here. Also note that while the collision is case-insensitive, name resolution is *not* case-insensitive in Daml-LF. In other words, to refer to a name, one must refer to it with the same case that it was defined with. The case-insensitivity for collisions is in place since we often generate files from Daml-LF packages, and we want to make sure for things to work smoothly when operating in case-insensitive file systems, while at the same time preserving case sensitivity in the language. Name collision condition ........................ In Daml-LF, the only permitted name collisions are those occurring between variant constructors and record types defined in the same module. Every other collision makes the module (and thus the package) not well-formed. For example, a module ``Mod`` can contain the following definitions:: 'variant' Tree (α : ⋆) ↦ Node : Mod:Tree.Node @α | Leaf : Unit 'record' Tree.Node (α : ⋆) ↦ { value: α, left: Mod:Tree α, right: Mod:Tree α } The variant constructor ``Node`` (within the definition of the variant type ``Tree``) and the record type ``Tree.Node`` (within the first record type definition) have the same fully resolved name ``Mod.Tree.Node``. However this package is well-formed. Note that name collisions between a record definition and a variant constructor from different modules are prohibited. We will say that the *name collision condition* holds for a package if the only name collisions within this package are those occurring between variant constructors and record types, as described above. Well-formed packages ~~~~~~~~~~~~~~~~~~~~ Then, a collection of packages ``Ξ`` is well-formed if: * Each definition in ``Ξ`` is `well-formed `_; * Each template in ``Ξ`` is `coherent