- More accurate AllT environment management by using (Maybe TypeEnv) instead of TypeEnv. The performance of the type-checker also improved thanks to that.

2 files changed, 86 insertions, 57 deletions

diff --git a/source/lux.lux b/source/lux.lux
index a005da3da..aab80ed7e 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -22,11 +22,14 @@
 (def' Text (#DataT "java.lang.String"))
 (export' Text)
 
+(def' Void (#VariantT #Nil))
+(export' Void)
+
 ## (deftype (List a)
 ##   (| #Nil
 ##      (#Cons (, a (List a)))))
 (def' List
-  (#AllT [#Nil "List" "a"
+  (#AllT [#None "List" "a"
           (#VariantT (#Cons [["lux;Nil" (#TupleT #Nil)]
                              (#Cons [["lux;Cons" (#TupleT (#Cons [(#BoundT "a")
                                                                   (#Cons [(#AppT [(#BoundT "List") (#BoundT "a")])
@@ -34,6 +37,16 @@
                                      #Nil])]))]))
 (export' List)
 
+## (deftype (Maybe a)
+##   (| #None
+##      (#Some a)))
+(def' Maybe
+  (#AllT [#None "Maybe" "a"
+          (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
+                             (#Cons [["lux;Some" (#BoundT "a")]
+                                     #Nil])]))]))
+(export' Maybe)
+
 ## (deftype #rec Type
 ##   (| #AnyT
 ##      #NothingT
@@ -44,47 +57,36 @@
 ##      (#LambdaT (, Type Type))
 ##      (#BoundT Text)
 ##      (#VarT Int)
-##      (#AllT (, (List (, Text Type)) Text Text Type))
+##      (#AllT (, (Maybe (List (, Text Type))) Text Text Type))
 ##      (#AppT (, Type Type))))
 (def' Type
   (case' (#AppT [(#BoundT "Type") (#BoundT "")])
          Type
          (case' (#AppT [List (#TupleT (#Cons [Text (#Cons [Type #Nil])]))])
                 TypeEnv
-                (#AppT [(#AllT [#Nil "Type" ""
+                (#AppT [(#AllT [#None "Type" ""
                                 (#VariantT (#Cons [["lux;AnyT" (#TupleT #Nil)]
                                                    (#Cons [["lux;NothingT" (#TupleT #Nil)]
                                                            (#Cons [["lux;DataT" Text]
-                                                                   (#Cons [["lux;TupleT" (#AppT [List (#AppT [(#BoundT "Type") (#BoundT "")])])]
+                                                                   (#Cons [["lux;TupleT" (#AppT [List Type])]
                                                                            (#Cons [["lux;VariantT" TypeEnv]
                                                                                    (#Cons [["lux;RecordT" TypeEnv]
                                                                                            (#Cons [["lux;LambdaT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
                                                                                                    (#Cons [["lux;BoundT" Text]
                                                                                                            (#Cons [["lux;VarT" Int]
-                                                                                                                   (#Cons [["lux;AllT" (#TupleT (#Cons [TypeEnv (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))]
+                                                                                                                   (#Cons [["lux;AllT" (#TupleT (#Cons [(#AppT [Maybe TypeEnv]) (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))]
                                                                                                                            (#Cons [["lux;AppT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
                                                                                                                                    #Nil])])])])])])])])])])]))])
                         #NothingT]))))
 (export' Type)
 
-## (deftype (Maybe a)
-##   (| #None
-##      (#Some a)))
-(def' Maybe
-  (:' Type
-     (#AllT [#Nil "Maybe" "a"
-             (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
-                                (#Cons [["lux;Some" (#BoundT "a")]
-                                        #Nil])]))])))
-(export' Maybe)
-
 ## (deftype (Bindings k v)
 ##   (& #counter Int
 ##      #mappings (List (, k v))))
 (def' Bindings
   (:' Type
-     (#AllT [#Nil "Bindings" "k"
-             (#AllT [#Nil "" "v"
+     (#AllT [#None "Bindings" "k"
+             (#AllT [#None "" "v"
                      (#RecordT (#Cons [["lux;counter" Int]
                                        (#Cons [["lux;mappings" (#AppT [List
                                                                        (#TupleT (#Cons [(#BoundT "k")
@@ -99,8 +101,8 @@
 ##      #closure (Bindings k v)))
 (def' Env
   (:' Type
-     (#AllT [#Nil "Env" "k"
-             (#AllT [#Nil "" "v"
+     (#AllT [#None "Env" "k"
+             (#AllT [#None "" "v"
                      (#RecordT (#Cons [["lux;name" Text]
                                        (#Cons [["lux;inner-closures" Int]
                                                (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
@@ -119,8 +121,8 @@
 ##   (| (#Meta (, m v))))
 (def' Meta
   (:' Type
-     (#AllT [#Nil "Meta" "m"
-             (#AllT [#Nil "" "v"
+     (#AllT [#None "Meta" "m"
+             (#AllT [#None "" "v"
                      (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
                                                                      (#Cons [(#BoundT "v")
                                                                              #Nil])]))]
@@ -186,7 +188,7 @@
                    Syntax'List
                    (case' (#TupleT (#Cons [Text (#Cons [Text #Nil])]))
                           Ident
-                          (#AllT [#Nil "Syntax'" "w"
+                          (#AllT [#None "Syntax'" "w"
                                   (#VariantT (#Cons [["lux;Bool" Bool]
                                                      (#Cons [["lux;Int" Int]
                                                              (#Cons [["lux;Real" Real]
@@ -217,8 +219,8 @@
 ##      (#Right r)))
 (def' Either
   (:' Type
-     (#AllT [#Nil "_" "l"
-             (#AllT [#Nil "" "r"
+     (#AllT [#None "_" "l"
+             (#AllT [#None "" "r"
                      (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
                                         (#Cons [["lux;Right" (#BoundT "r")]
                                                 #Nil])]))])])))
@@ -452,7 +454,7 @@
          (#Cons [(#Meta [_ (#Tuple (#Cons [(#Meta [_ (#Symbol ["" arg-name])]) other-args]))])
                  (#Cons [body #Nil])])
          (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Tag ["lux" "AllT"]))
-                                                (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "Nil"]))
+                                                (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "None"]))
                                                                                (#Cons [(_meta (#Text ""))
                                                                                        (#Cons [(_meta (#Text arg-name))
                                                                                                (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "All'"]))
@@ -760,7 +762,7 @@
 ##                           (lambda [body arg]
 ##                             (case' arg
 ##                                    (#Meta [_ (#Symbol [arg-module arg-name])])
-##                                    (` (#AllT (list) "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name]
+##                                    (` (#AllT #None "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name]
 ##                                                                                                       (` (#BoundT (~ (#Text ($ text:++ arg-module ";" arg-name)))))
 ##                                                                                                       body)))))))
 ##                       body
@@ -1596,7 +1598,7 @@
 ##                      (#Symbol ["" arg]))
 ##                    args)
 ##         body' (replace-syntax arg-replacements body)]
-##     (return (list (` (#AllT [#Nil (~ name') (#Tuple (list (~@ args')))
+##     (return (list (` (#AllT [#None (~ name') (#Tuple (list (~@ args')))
 ##                              (~ body')]))))))
 
 ## (def (walk-syntax type)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 35190da27..17db11b43 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -17,18 +17,22 @@
 (def Unit (&/V "lux;TupleT" (&/|list)))
 
 (def List
-  (&/V "lux;AllT" (&/T (&/|table) "List" "a"
-                       (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))
+  (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "List" "a"
+                       (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" Unit)
                                                     (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
                                                                                                (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
                                                                                                                     (&/V "lux;BoundT" "a")))))))))))
 
+(def Maybe
+  (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Maybe" "a"
+                       (&/V "lux;VariantT" (&/|list (&/T "lux;None" Unit)
+                                                    (&/T "lux;Some" (&/V "lux;BoundT" "a")))))))
+
 (def Type
   (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_")))
         TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type))))
-        Unit (&/V "lux;TupleT" (&/|list))
         TypePair (&/V "lux;TupleT" (&/|list Type Type))]
-    (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_"
+    (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Type" "_"
                                               (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit)
                                                                            (&/T "lux;NothingT" Unit)
                                                                            (&/T "lux;DataT" Text)
@@ -38,7 +42,7 @@
                                                                            (&/T "lux;LambdaT" TypePair)
                                                                            (&/T "lux;BoundT" Text)
                                                                            (&/T "lux;VarT" Int)
-                                                                           (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type)))
+                                                                           (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list (&/V "lux;AppT" (&/T Maybe TypeEnv)) Text Text Type)))
                                                                            (&/T "lux;AppT" TypePair)
                                                                            ))))
                          (&/V "lux;NothingT" nil)))))
@@ -154,10 +158,16 @@
       (return (&/V "lux;RecordT" =members)))
 
     [["lux;AllT" [?env ?name ?arg ?body]]]
-    (|do [=env (&/map% (fn [[k v]]
-                         (|do [=v (clean* ?tid v)]
-                           (return (&/T k =v))))
-                       ?env)
+    (|do [=env (matchv ::M/objects [?env]
+                 [["lux;None" _]]
+                 (return ?env)
+
+                 [["lux;Some" ?env*]]
+                 (|do [clean-env (&/map% (fn [[k v]]
+                                           (|do [=v (clean* ?tid v)]
+                                             (return (&/T k =v))))
+                                         ?env*)]
+                   (return (&/V "lux;Some" clean-env))))
           body* (clean* ?tid ?body)]
       (return (&/V "lux;AllT" (&/T =env ?name ?arg body*))))
 
@@ -284,20 +294,27 @@
                      ;;      'NAME [xname yname] (= xname yname)
                      ;;      'ARG (= xarg yarg)
                      ;;      'LENGTH [(&/|length xenv) (&/|length yenv)] (= (&/|length xenv) (&/|length yenv)))
-                   (and (= xname yname)
-                        (= xarg yarg)
-                        (type= xbody ybody)
-                        ;; (= (&/|length xenv) (&/|length yenv))
-                        ;; (&/fold (fn [old bname]
-                        ;;           (and old
-                        ;;                (type= (&/|get bname xenv) (&/|get bname yenv))))
-                        ;;         true
-                        ;;         (&/|keys xenv))
-                        ))
+                     (and (= xname yname)
+                          (= xarg yarg)
+                          ;; (matchv ::M/objects [xenv yenv]
+                          ;;   [["lux;None" _] ["lux;None" _]]
+                          ;;   true
+
+                          ;;   [["lux;Some" xenv*] ["lux;Some" yenv*]]
+                          ;;   (&/fold (fn [old bname]
+                          ;;             (and old
+                          ;;                  (type= (&/|get bname xenv*) (&/|get bname yenv*))))
+                          ;;           (= (&/|length xenv*) (&/|length yenv*))
+                          ;;           (&/|keys xenv*))
+
+                          ;;   [_ _]
+                          ;;   false)
+                          (type= xbody ybody)
+                          ))
 
                  [_ _]
                  (do ;; (prn 'type= (show-type x) (show-type y))
-                   false)
+                     false)
                  )]
     ;; (prn 'type= output (show-type x) (show-type y))
     output))
@@ -343,16 +360,19 @@
     (&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)))
 
     [["lux;AllT" [?local-env ?local-name ?local-arg ?local-def]]]
-    (&/V "lux;AllT" (&/T (&/|merge ?local-env env) ?local-name ?local-arg ?local-def))
+    (matchv ::M/objects [?local-env]
+      [["lux;None" _]]
+      (&/V "lux;AllT" (&/T (&/V "lux;Some" env) ?local-name ?local-arg ?local-def))
+
+      [["lux;Some" _]]
+      type)
 
     [["lux;LambdaT" [?input ?output]]]
     (&/V "lux;LambdaT" (&/T (beta-reduce env ?input) (beta-reduce env ?output)))
 
     [["lux;BoundT" ?name]]
     (if-let [bound (&/|get ?name env)]
-      (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str ""))
-          ;;      (show-type bound))
-          (beta-reduce env bound))
+      (beta-reduce env bound)
       type)
 
     [_]
@@ -372,10 +392,17 @@
   ;; (prn 'apply-type (aget type-fn 0) (aget param 0))
   (matchv ::M/objects [type-fn]
     [["lux;AllT" [local-env local-name local-arg local-def]]]
-    (return (beta-reduce (->> local-env
-                              (&/|put local-name type-fn)
-                              (&/|put local-arg param))
-                         local-def))
+    (let [;; _ (prn 'apply-type/local-env (aget local-env 0) (show-type type-fn))
+          local-env* (matchv ::M/objects [local-env]
+                       [["lux;None" _]]
+                       (&/|table)
+
+                       [["lux;Some" local-env*]]
+                       local-env*)]
+      (return (beta-reduce (->> local-env*
+                                (&/|put local-name type-fn)
+                                (&/|put local-arg param))
+                           local-def)))
 
     [["lux;AppT" [F A]]]
     (|do [type-fn* (apply-type F A)]
@@ -552,7 +579,7 @@
     (|do [_ (check* init-fixpoints input param)]
       (return output))
 
-    [["lux;AllT" [local-env local-name local-arg local-def]]]
+    [["lux;AllT" _]]
     (with-var
       (fn [$var]
         (|do [func* (apply-type func $var)