Prototype: Renamed any/none to unknown/never (#447)

* Renamed any/none to unknown/never
* Pin hackage version
* Update Agda version

.github/workflows/prototyping.yml

@@ -10,15 +10,17 @@ jobs:
   linux:
     strategy:
       matrix:
-        agda: [2.6.2.1]
+        agda: [2.6.2.2]
+        hackageDate: ["2022-04-07"]
+        hackageTime: ["23:06:28"]
     name: prototyping
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v1
     - uses: actions/cache@v2
       with:
         path: ~/.cabal/store
-        key: prototyping-${{ runner.os }}-${{ matrix.agda }}
+        key: "prototyping-${{ runner.os }}-${{ matrix.agda }}-${{ matrix.hackageDate }}-${{ matrix.hackageTime }}"
     - uses: actions/cache@v2
       id: luau-ast-cache
       with:
@@ -28,12 +30,12 @@ jobs:
       run: sudo apt-get install -y cabal-install
     - name: cabal update
       working-directory: prototyping
-      run: cabal update
+      run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z"
     - name: cabal install
       working-directory: prototyping
       run: |
-        cabal install Agda-${{ matrix.agda }}
         cabal install --lib scientific vector aeson --package-env .
+        cabal install --allow-newer Agda-${{ matrix.agda }}
     - name: check targets
       working-directory: prototyping
       run: |

prototyping/Luau/StrictMode.agda

@@ -5,7 +5,7 @@ module Luau.StrictMode where
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt)
+open import Luau.Type using (Type; strict; nil; number; string; boolean; _⇒_; _∪_; _∩_; tgt)
 open import Luau.Subtyping using (_≮:_)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)

prototyping/Luau/Subtyping.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --rewriting #-}
 
-open import Luau.Type using (Type; Scalar; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 open import Properties.Equality using (_≢_)
 
 module Luau.Subtyping where
@@ -29,7 +29,7 @@ data Language where
   left : ∀ {T U t} → Language T t → Language (T ∪ U) t
   right : ∀ {T U u} → Language U u → Language (T ∪ U) u
   _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
-  any : ∀ {t} → Language any t
+  unknown : ∀ {t} → Language unknown t
 
 data ¬Language where
 
@@ -42,7 +42,7 @@ data ¬Language where
   _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
   left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
   right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
-  none : ∀ {t} → ¬Language none t
+  never : ∀ {t} → ¬Language never t
 
 -- Subtyping as language inclusion
 

prototyping/Luau/Type.agda

@@ -9,8 +9,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing)
 data Type : Set where
   nil : Type
   _⇒_ : Type → Type → Type
-  none : Type
-  any : Type
+  never : Type
+  unknown : Type
   boolean : Type
   number : Type
   string : Type
@@ -29,8 +29,8 @@ lhs (T ⇒ _) = T
 lhs (T ∪ _) = T
 lhs (T ∩ _) = T
 lhs nil = nil
-lhs none = none
-lhs any = any
+lhs never = never
+lhs unknown = unknown
 lhs number = number
 lhs boolean = boolean
 lhs string = string
@@ -40,25 +40,25 @@ rhs (_ ⇒ T) = T
 rhs (_ ∪ T) = T
 rhs (_ ∩ T) = T
 rhs nil = nil
-rhs none = none
-rhs any = any
+rhs never = never
+rhs unknown = unknown
 rhs number = number
 rhs boolean = boolean
 rhs string = string
 
 _≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
 nil ≡ᵀ nil = yes refl
 nil ≡ᵀ (S ⇒ T) = no (λ ())
-nil ≡ᵀ none = no (λ ())
-nil ≡ᵀ any = no (λ ())
+nil ≡ᵀ never = no (λ ())
+nil ≡ᵀ unknown = no (λ ())
 nil ≡ᵀ number = no (λ ())
 nil ≡ᵀ boolean = no (λ ())
 nil ≡ᵀ (S ∪ T) = no (λ ())
 nil ≡ᵀ (S ∩ T) = no (λ ())
 nil ≡ᵀ string = no (λ ())
 (S ⇒ T) ≡ᵀ string = no (λ ())
-none ≡ᵀ string = no (λ ())
-any ≡ᵀ string = no (λ ())
+never ≡ᵀ string = no (λ ())
+unknown ≡ᵀ string = no (λ ())
 boolean ≡ᵀ string = no (λ ())
 number ≡ᵀ string = no (λ ())
 (S ∪ T) ≡ᵀ string = no (λ ())
@@ -68,57 +68,57 @@ number ≡ᵀ string = no (λ ())
 (S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
 (S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q))
 (S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q))
-(S ⇒ T) ≡ᵀ none = no (λ ())
-(S ⇒ T) ≡ᵀ any = no (λ ())
+(S ⇒ T) ≡ᵀ never = no (λ ())
+(S ⇒ T) ≡ᵀ unknown = no (λ ())
 (S ⇒ T) ≡ᵀ number = no (λ ())
 (S ⇒ T) ≡ᵀ boolean = no (λ ())
 (S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ())
 (S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ())
-none ≡ᵀ nil = no (λ ())
-none ≡ᵀ (U ⇒ V) = no (λ ())
-none ≡ᵀ none = yes refl
-none ≡ᵀ any = no (λ ())
-none ≡ᵀ number = no (λ ())
-none ≡ᵀ boolean = no (λ ())
-none ≡ᵀ (U ∪ V) = no (λ ())
-none ≡ᵀ (U ∩ V) = no (λ ())
-any ≡ᵀ nil = no (λ ())
-any ≡ᵀ (U ⇒ V) = no (λ ())
-any ≡ᵀ none = no (λ ())
-any ≡ᵀ any = yes refl
-any ≡ᵀ number = no (λ ())
-any ≡ᵀ boolean = no (λ ())
-any ≡ᵀ (U ∪ V) = no (λ ())
-any ≡ᵀ (U ∩ V) = no (λ ())
+never ≡ᵀ nil = no (λ ())
+never ≡ᵀ (U ⇒ V) = no (λ ())
+never ≡ᵀ never = yes refl
+never ≡ᵀ unknown = no (λ ())
+never ≡ᵀ number = no (λ ())
+never ≡ᵀ boolean = no (λ ())
+never ≡ᵀ (U ∪ V) = no (λ ())
+never ≡ᵀ (U ∩ V) = no (λ ())
+unknown ≡ᵀ nil = no (λ ())
+unknown ≡ᵀ (U ⇒ V) = no (λ ())
+unknown ≡ᵀ never = no (λ ())
+unknown ≡ᵀ unknown = yes refl
+unknown ≡ᵀ number = no (λ ())
+unknown ≡ᵀ boolean = no (λ ())
+unknown ≡ᵀ (U ∪ V) = no (λ ())
+unknown ≡ᵀ (U ∩ V) = no (λ ())
 number ≡ᵀ nil = no (λ ())
 number ≡ᵀ (T ⇒ U) = no (λ ())
-number ≡ᵀ none = no (λ ())
-number ≡ᵀ any = no (λ ())
+number ≡ᵀ never = no (λ ())
+number ≡ᵀ unknown = no (λ ())
 number ≡ᵀ number = yes refl
 number ≡ᵀ boolean = no (λ ())
 number ≡ᵀ (T ∪ U) = no (λ ())
 number ≡ᵀ (T ∩ U) = no (λ ())
 boolean ≡ᵀ nil = no (λ ())
 boolean ≡ᵀ (T ⇒ U) = no (λ ())
-boolean ≡ᵀ none = no (λ ())
-boolean ≡ᵀ any = no (λ ())
+boolean ≡ᵀ never = no (λ ())
+boolean ≡ᵀ unknown = no (λ ())
 boolean ≡ᵀ boolean = yes refl
 boolean ≡ᵀ number = no (λ ())
 boolean ≡ᵀ (T ∪ U) = no (λ ())
 boolean ≡ᵀ (T ∩ U) = no (λ ())
 string ≡ᵀ nil = no (λ ())
 string ≡ᵀ (x ⇒ x₁) = no (λ ())
-string ≡ᵀ none = no (λ ())
-string ≡ᵀ any = no (λ ())
+string ≡ᵀ never = no (λ ())
+string ≡ᵀ unknown = no (λ ())
 string ≡ᵀ boolean = no (λ ())
 string ≡ᵀ number = no (λ ())
 string ≡ᵀ string = yes refl
 string ≡ᵀ (U ∪ V) = no (λ ())
 string ≡ᵀ (U ∩ V) = no (λ ())
 (S ∪ T) ≡ᵀ nil = no (λ ())
 (S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
-(S ∪ T) ≡ᵀ none = no (λ ())
-(S ∪ T) ≡ᵀ any = no (λ ())
+(S ∪ T) ≡ᵀ never = no (λ ())
+(S ∪ T) ≡ᵀ unknown = no (λ ())
 (S ∪ T) ≡ᵀ number = no (λ ())
 (S ∪ T) ≡ᵀ boolean = no (λ ())
 (S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V) 
@@ -128,8 +128,8 @@ string ≡ᵀ (U ∩ V) = no (λ ())
 (S ∪ T) ≡ᵀ (U ∩ V) = no (λ ())
 (S ∩ T) ≡ᵀ nil = no (λ ())
 (S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ())
-(S ∩ T) ≡ᵀ none = no (λ ())
-(S ∩ T) ≡ᵀ any = no (λ ())
+(S ∩ T) ≡ᵀ never = no (λ ())
+(S ∩ T) ≡ᵀ unknown = no (λ ())
 (S ∩ T) ≡ᵀ number = no (λ ())
 (S ∩ T) ≡ᵀ boolean = no (λ ())
 (S ∩ T) ≡ᵀ (U ∪ V) = no (λ ())
@@ -151,29 +151,29 @@ data Mode : Set where
   nonstrict : Mode
 
 src : Mode → Type → Type
-src m nil = none
-src m number = none
-src m boolean = none
-src m string = none
+src m nil = never
+src m number = never
+src m boolean = never
+src m string = never
 src m (S ⇒ T) = S
 -- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant
 src strict    (S ∪ T) = (src strict S) ∩ (src strict T)
 src nonstrict (S ∪ T) = (src nonstrict S) ∪ (src nonstrict T)
 src strict    (S ∩ T) = (src strict S) ∪ (src strict T)
 src nonstrict (S ∩ T) = (src nonstrict S) ∩ (src nonstrict T)
-src strict none = any
-src nonstrict none = none
-src strict any = none
-src nonstrict any = any
+src strict never = unknown
+src nonstrict never = never
+src strict unknown = never
+src nonstrict unknown = unknown
 
 tgt : Type → Type
-tgt nil = none
+tgt nil = never
 tgt (S ⇒ T) = T
-tgt none = none
-tgt any = any
-tgt number = none
-tgt boolean = none
-tgt string = none
+tgt never = never
+tgt unknown = unknown
+tgt number = never
+tgt boolean = never
+tgt string = never
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
 

prototyping/Luau/Type/FromJSON.agda

@@ -2,7 +2,7 @@
 
 module Luau.Type.FromJSON where
 
-open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number; string)
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; unknown; never; number; string)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 open import Agda.Builtin.Bool using (true; false)
@@ -42,7 +42,9 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
 
 typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
-typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right unknown -- not quite right
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "unknown") = Right unknown
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "never") = Right never
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "string") = Right string
 typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"

prototyping/Luau/Type/ToString.agda

@@ -1,7 +1,7 @@
 module Luau.Type.ToString where
 
 open import FFI.Data.String using (String; _++_)
-open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; string; _∪_; _∩_; normalizeOptional)
+open import Luau.Type using (Type; nil; _⇒_; never; unknown; number; boolean; string; _∪_; _∩_; normalizeOptional)
 
 {-# TERMINATING #-}
 typeToString : Type → String
@@ -10,8 +10,8 @@ typeToStringᴵ : Type → String
 
 typeToString nil = "nil"
 typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
-typeToString none = "none"
-typeToString any = "any"
+typeToString never = "never"
+typeToString unknown = "unknown"
 typeToString number = "number"
 typeToString boolean = "boolean"
 typeToString string = "string"

prototyping/Luau/TypeCheck.agda

@@ -10,7 +10,7 @@ open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Type using (Type; Mode; nil; any; number; boolean; string; _⇒_; tgt)
+open import Luau.Type using (Type; Mode; nil; unknown; number; boolean; string; _⇒_; tgt)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
@@ -19,9 +19,9 @@ open import Properties.Product using (_×_; _,_)
 src : Type → Type
 src = Luau.Type.src m
 
-orAny : Maybe Type → Type
-orAny nothing = any
-orAny (just T) = T
+orUnknown : Maybe Type → Type
+orUnknown nothing = unknown
+orUnknown (just T) = T
 
 srcBinOp : BinaryOperator → Type
 srcBinOp + = number
@@ -30,8 +30,8 @@ srcBinOp * = number
 srcBinOp / = number
 srcBinOp < = number
 srcBinOp > = number
-srcBinOp == = any
-srcBinOp ~= = any
+srcBinOp == = unknown
+srcBinOp ~= = unknown
 srcBinOp <= = number
 srcBinOp >= = number
 srcBinOp ·· = string
@@ -89,7 +89,7 @@ data _⊢ᴱ_∈_ where
 
   var : ∀ {x T Γ} →
 
-    T ≡ orAny(Γ [ x ]ⱽ) →
+    T ≡ orUnknown(Γ [ x ]ⱽ) →
     ----------------
     Γ ⊢ᴱ (var x) ∈ T