Add specification for type synonyms in DAML-LF (#3635)

* Add specification for type synonyms in DAML-LF * Fix identifiers for type synonyms * Use S for type synonyms * Address review comments * Split up TyTypeSynonym and DefTypeSynonym
digital-asset · Nov 26, 2019 · f402acf · f402acf
1 parent 06b7a10
commit f402acf
Showing 1 changed file with 25 additions and 2 deletions.
diff --git a/daml-lf/spec/daml-lf-1.rst b/daml-lf/spec/daml-lf-1.rst
@@ -267,6 +267,8 @@ Version: 1.dev
 
   * **Rename** ``Map`` to ``TextMap``
 
+  * **Add** type synonyms.
+
 Abstract syntax
 ^^^^^^^^^^^^^^^
 
@@ -474,8 +476,8 @@ 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 tuple *field
-names*, *variant constructors*, and *template choices*. On the other
-hand, we will use names to represent *type constructors*, *value
+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*.  ::
 
@@ -506,6 +508,9 @@ strings as *package identifiers*.  ::
   Type constructors
               T ::= Name                            -- TyConName
 
+  Type synonym names
+              S ::= Name                            -- TypeSynonym
+
   Module names
         ModName ::= Name                            -- ModName
 
@@ -676,6 +681,7 @@ available for usage::
        |  '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₁
@@ -846,6 +852,13 @@ First, we formally defined *well-formed types*. ::
     ————————————————————————————————————————————— TyTuple
       Γ  ⊢  ⟨ f₁: τ₁, …, fₙ: τₙ ⟩  :  ⋆
 
+      'synonym' S (α₁:k₁) … (αₙ:kₙ) ↦ τ ∈ 〚Ξ〛Mod
+      Γ  ⊢  τ₁ : k₁  …  Γ  ⊢  τₙ : kₙ
+    ————————————————————————————————————————————— TyTypeSynonym
+      Γ  ⊢  S τ₁ … τₙ  :  ⋆
+
+
+
 
 Well-formed expression
 ......................
@@ -982,6 +995,12 @@ Then we define *well-formed expressions*. ::
     ——————————————————————————————————————————————————————————————— ExpEnumCon
       Γ  ⊢  Mod:T:Eᵢ  :  Mod:T
 
+      'synonym' S (α₁:k₁) … (αₙ:kₙ) ↦ τ
+      Γ  ⊢  τ₁ : k₁    ⋯     Γ  ⊢  τₙ : kₙ
+      Γ  ↦  e : τ[α₁ ↦ τ₁, …, α₁ ↦ τₙ]
+    ——————————————————————————————————————————————————————————————— ExpTypeSynonym
+      Γ  ⊢  e : Mod:S τ₁ … τₙ
+
       Γ  ⊢  e₁  :  τ₁      …      Γ  ⊢  eₘ  :  τₘ
     ——————————————————————————————————————————————————————————————— ExpTupleCon
       Γ  ⊢  ⟨ f₁ = e₁, …, fₘ = eₘ ⟩  :  ⟨ f₁: τ₁, …, fₘ: τₘ ⟩
@@ -1219,6 +1238,10 @@ for the ``DefTemplate`` rule). ::
   ——————————————————————————————————————————————————————————————— DefEnum
     ⊢  'enum' T  ↦ E₁ | … | Eₘ
 
+    (α₁:k₁) … (αₙ:kₙ) · Γ  ⊢  τ  :  ⋆
+  ——————————————————————————————————————————————————————————————— DefTypeSynonym
+    ⊢  'synonym' S (α₁: k₁) … (αₙ: kₙ) ↦ τ
+
     ε  ⊢  e  :  τ
   ——————————————————————————————————————————————————————————————— DefValue
     ⊢  'val' W : τ ↦ e