1 files changed, 193 insertions, 0 deletions
diff --git a/source/lux/meta/type.lux b/source/lux/meta/type.lux
new file mode 100644
index 000000000..0938d104d
--- /dev/null
+++ b/source/lux/meta/type.lux
@@ -0,0 +1,193 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;import lux
+         (lux (control show
+                       eq
+                       monad)
+              (data (char #as c)
+                    (text #as t #open ("text:" Text/Monoid Text/Eq))
+                    (number/int #open ("int:" Int/Number Int/Ord Int/Show))
+                    maybe
+                    (list #refer #all #open ("list:" List/Monad List/Monoid List/Fold)))
+              ))
+
+(open List/Fold)
+
+## [Utils]
+(def (unravel-fun type)
+  (-> Type (, Type (List Type)))
+  (case type
+    (#;LambdaT in out')
+    (let [[out ins] (unravel-fun out')]
+      [out (@list& in ins)])
+
+    _
+    [type (@list)]))
+
+(def (unravel-app type)
+  (-> Type (, Type (List Type)))
+  (case type
+    (#;AppT left' right)
+    (let [[left rights] (unravel-app left')]
+      [left (list:++ rights (@list right))])
+
+    _
+    [type (@list)]))
+
+## [Structures]
+(defstruct #export Type/Show (Show Type)
+  (def (show type)
+    (case type
+      (#;DataT name params)
+      (case params
+        #;Nil
+        ($ text:++ "(^ " name ")")
+
+        _
+        ($ text:++ "(^ " name " " (|> params (list:map show) (interpose " ") (list:foldL text:++ "")) ")"))
+
+      (#;TupleT members)
+      (case members
+        #;Nil
+        "(,)"
+
+        _
+        ($ text:++ "(, " (|> members (list:map show) (interpose " ") (foldL text:++ "")) ")"))
+
+      (#;VariantT members)
+      (case members
+        #;Nil
+        "(|)"
+
+        _
+        ($ text:++ "(| " (|> members (list:map show) (interpose " ") (foldL text:++ "")) ")"))
+
+      (#;LambdaT input output)
+      (let [[out ins] (unravel-fun type)]
+        ($ text:++  "(-> " (|> ins (list:map show) (interpose " ") (foldL text:++ "")) " " (show out) ")"))
+
+      (#;VarT id)
+      ($ text:++ "⌈" (int:show id) "⌋")
+
+      (#;BoundT idx)
+      (int:show idx)
+
+      (#;ExT id)
+      ($ text:++ "⟨" (int:show id) "⟩")
+
+      (#;AppT fun param)
+      (let [[type-fun type-args] (unravel-app type)]
+        ($ text:++  "(" (show type-fun) " " (|> type-args (list:map show) (interpose " ") (foldL text:++ "")) ")"))
+
+      (#;UnivQ env body)
+      ($ text:++ "(All " (show body) ")")
+
+      (#;ExQ env body)
+      ($ text:++ "(Ex " (show body) ")")
+
+      (#;NamedT [module name] type)
+      ($ text:++ module ";" name)
+      )))
+
+(defstruct #export Type/Eq (Eq Type)
+  (def (= x y)
+    (case [x y]
+      [(#;DataT xname xparams) (#;DataT yname yparams)]
+      (and (text:= xname yname)
+           (int:= (size xparams) (size yparams))
+           (foldL (lambda [prev [x y]]
+                    (and prev (= x y)))
+                  true
+                  (zip2 xparams yparams)))
+
+      (\or [(#;VarT xid) (#;VarT yid)]
+       [(#;ExT xid) (#;ExT yid)]
+       [(#;BoundT xid) (#;BoundT yid)])
+      (int:= xid yid)
+
+      (\or [(#;LambdaT xleft xright) (#;LambdaT yleft yright)]
+       [(#;AppT xleft xright) (#;AppT yleft yright)])
+      (and (= xleft yleft)
+           (= xright yright))
+
+      [(#;NamedT [xmodule xname] xtype) (#;NamedT [ymodule yname] ytype)]
+      (and (text:= xmodule ymodule)
+           (text:= xname yname)
+           (= xtype ytype))
+
+      (\or [(#;TupleT xmembers) (#;TupleT ymembers)]
+       [(#;VariantT xmembers) (#;VariantT ymembers)])
+      (and (int:= (size xmembers) (size ymembers))
+           (foldL (lambda [prev [x y]]
+                    (and prev (= x y)))
+                  true
+                  (zip2 xmembers ymembers)))
+
+      (\or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)]
+       [(#;ExQ xenv xbody) (#;ExQ yenv ybody)])
+      (and (int:= (size xenv) (size yenv))
+           (foldL (lambda [prev [x y]]
+                    (and prev (= x y)))
+                  (= xbody ybody)
+                  (zip2 xenv yenv)))
+
+      _
+      false
+      )))
+
+## [Functions]
+(def #export (beta-reduce env type)
+  (-> (List Type) Type Type)
+  (case type
+    (\template [<tag>]
+     [(<tag> members)
+      (<tag> (list:map (beta-reduce env) members))])
+    [[#;VariantT]
+     [#;TupleT]]
+
+    (\template [<tag>]
+     [(<tag> left right)
+      (<tag> (beta-reduce env left) (beta-reduce env right))])
+    [[#;LambdaT]
+     [#;AppT]]
+
+    (\template [<tag>]
+     [(<tag> env def)
+      (case env
+        #;Nil
+        (<tag> env def)
+
+        _
+        type)])
+    [[#;UnivQ]
+     [#;ExQ]]
+    
+    (#;BoundT idx)
+    (? type (@ idx env))
+    
+    (#;NamedT name type)
+    (beta-reduce env type)
+
+    _
+    type
+    ))
+
+(def #export (apply-type type-fun param)
+  (-> Type Type (Maybe Type))
+  (case type-fun
+    (#;UnivQ env body)
+    (#;Some (beta-reduce (@list& type-fun param env) body))
+
+    (#;AppT F A)
+    (do Maybe/Monad
+      [type-fn* (apply-type F A)]
+      (apply-type type-fn* param))
+
+    (#;NamedT name type)
+    (apply-type type param)
+    
+    _
+    #;None))