aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/lux/type/implicit.lux
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/lux/type/implicit.lux')
-rw-r--r--stdlib/source/lux/type/implicit.lux363
1 files changed, 363 insertions, 0 deletions
diff --git a/stdlib/source/lux/type/implicit.lux b/stdlib/source/lux/type/implicit.lux
new file mode 100644
index 000000000..54fec2626
--- /dev/null
+++ b/stdlib/source/lux/type/implicit.lux
@@ -0,0 +1,363 @@
+(;module:
+ lux
+ (lux (control ["M" monad #+ do Monad]
+ [eq]
+ ["p" parser])
+ (data [text "Text/" Eq<Text>]
+ text/format
+ [number]
+ (coll [list "List/" Monad<List> Fold<List>]
+ [dict])
+ [bool]
+ [product]
+ [maybe])
+ [meta #+ Monad<Meta>]
+ (meta [code]
+ ["s" syntax #+ syntax: Syntax])
+ (lang [type]
+ (type ["tc" check #+ Check Monad<Check>]))
+ ))
+
+(def: (find-type-var id env)
+ (-> Nat Type-Context (Meta Type))
+ (case (list;find (|>. product;left (n.= id))
+ (get@ #;var-bindings env))
+ (#;Some [_ (#;Some type)])
+ (case type
+ (#;Var id')
+ (find-type-var id' env)
+
+ _
+ (:: Monad<Meta> wrap type))
+
+ (#;Some [_ #;None])
+ (meta;fail (format "Unbound type-var " (%n id)))
+
+ #;None
+ (meta;fail (format "Unknown type-var " (%n id)))
+ ))
+
+(def: (resolve-type var-name)
+ (-> Ident (Meta Type))
+ (do Monad<Meta>
+ [raw-type (meta;find-type var-name)
+ compiler meta;get-compiler]
+ (case raw-type
+ (#;Var id)
+ (find-type-var id (get@ #;type-context compiler))
+
+ _
+ (wrap raw-type))))
+
+(def: (find-member-type idx sig-type)
+ (-> Nat Type (Check Type))
+ (case sig-type
+ (#;Named _ sig-type')
+ (find-member-type idx sig-type')
+
+ (#;Apply arg func)
+ (case (type;apply (list arg) func)
+ #;None
+ (tc;fail (format "Cannot apply type " (%type func) " to type " (%type arg)))
+
+ (#;Some sig-type')
+ (find-member-type idx sig-type'))
+
+ (#;Product left right)
+ (if (n.= +0 idx)
+ (:: Monad<Check> wrap left)
+ (find-member-type (n.dec idx) right))
+
+ _
+ (if (n.= +0 idx)
+ (:: Monad<Check> wrap sig-type)
+ (tc;fail (format "Cannot find member type " (%n idx) " for " (%type sig-type))))))
+
+(def: (find-member-name member)
+ (-> Ident (Meta Ident))
+ (case member
+ ["" simple-name]
+ (meta;either (do Monad<Meta>
+ [member (meta;normalize member)
+ _ (meta;resolve-tag member)]
+ (wrap member))
+ (do Monad<Meta>
+ [this-module-name meta;current-module-name
+ imp-mods (meta;imported-modules this-module-name)
+ tag-lists (M;map @ meta;tag-lists imp-mods)
+ #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join)
+ candidates (list;filter (. (Text/= simple-name) product;right)
+ tag-lists)]]
+ (case candidates
+ #;Nil
+ (meta;fail (format "Unknown tag: " (%ident member)))
+
+ (#;Cons winner #;Nil)
+ (wrap winner)
+
+ _
+ (meta;fail (format "Too many candidate tags: " (%list %ident candidates))))))
+
+ _
+ (:: Monad<Meta> wrap member)))
+
+(def: (resolve-member member)
+ (-> Ident (Meta [Nat Type]))
+ (do Monad<Meta>
+ [member (find-member-name member)
+ [idx tag-list sig-type] (meta;resolve-tag member)]
+ (wrap [idx sig-type])))
+
+(def: (prepare-defs this-module-name defs)
+ (-> Text (List [Text Def]) (List [Ident Type]))
+ (|> defs
+ (list;filter (function [[name [def-type def-anns def-value]]]
+ (meta;struct? def-anns)))
+ (List/map (function [[name [def-type def-anns def-value]]]
+ [[this-module-name name] def-type]))))
+
+(def: local-env
+ (Meta (List [Ident Type]))
+ (do Monad<Meta>
+ [local-batches meta;locals
+ #let [total-locals (List/fold (function [[name type] table]
+ (dict;put~ name type table))
+ (: (dict;Dict Text Type)
+ (dict;new text;Hash<Text>))
+ (List/join local-batches))]]
+ (wrap (|> total-locals
+ dict;entries
+ (List/map (function [[name type]] [["" name] type]))))))
+
+(def: local-structs
+ (Meta (List [Ident Type]))
+ (do Monad<Meta>
+ [this-module-name meta;current-module-name
+ defs (meta;defs this-module-name)]
+ (wrap (prepare-defs this-module-name defs))))
+
+(def: import-structs
+ (Meta (List [Ident Type]))
+ (do Monad<Meta>
+ [this-module-name meta;current-module-name
+ imp-mods (meta;imported-modules this-module-name)
+ export-batches (M;map @ (function [imp-mod]
+ (do @
+ [exports (meta;exports imp-mod)]
+ (wrap (prepare-defs imp-mod exports))))
+ imp-mods)]
+ (wrap (List/join export-batches))))
+
+(def: (apply-function-type func arg)
+ (-> Type Type (Check Type))
+ (case func
+ (#;Named _ func')
+ (apply-function-type func' arg)
+
+ (#;UnivQ _)
+ (do Monad<Check>
+ [[id var] tc;var]
+ (apply-function-type (maybe;assume (type;apply (list var) func))
+ arg))
+
+ (#;Function input output)
+ (do Monad<Check>
+ [_ (tc;check input arg)]
+ (wrap output))
+
+ _
+ (tc;fail (format "Invalid function type: " (%type func)))))
+
+(def: (concrete-type type)
+ (-> Type (Check [(List Nat) Type]))
+ (case type
+ (#;UnivQ _)
+ (do Monad<Check>
+ [[id var] tc;var
+ [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))]
+ (wrap [(#;Cons id ids)
+ final-output]))
+
+ _
+ (:: Monad<Check> wrap [(list) type])))
+
+(def: (check-apply member-type input-types output-type)
+ (-> Type (List Type) Type (Check []))
+ (do Monad<Check>
+ [member-type' (M;fold Monad<Check>
+ (function [input member]
+ (apply-function-type member input))
+ member-type
+ input-types)]
+ (tc;check output-type member-type')))
+
+(type: #rec Instance
+ {#constructor Ident
+ #dependencies (List Instance)})
+
+(def: (test-provision provision context dep alts)
+ (-> (-> Compiler Type-Context Type (Check Instance))
+ Type-Context Type (List [Ident Type])
+ (Meta (List Instance)))
+ (do Monad<Meta>
+ [compiler meta;get-compiler]
+ (case (|> alts
+ (List/map (function [[alt-name alt-type]]
+ (case (tc;run context
+ (do Monad<Check>
+ [[tvars alt-type] (concrete-type alt-type)
+ #let [[deps alt-type] (type;flatten-function alt-type)]
+ _ (tc;check dep alt-type)
+ context' tc;get-context
+ =deps (M;map @ (provision compiler context') deps)]
+ (wrap =deps)))
+ (#;Left error)
+ (list)
+
+ (#;Right =deps)
+ (list [alt-name =deps]))))
+ List/join)
+ #;Nil
+ (meta;fail (format "No candidates for provisioning: " (%type dep)))
+
+ found
+ (wrap found))))
+
+(def: (provision compiler context dep)
+ (-> Compiler Type-Context Type (Check Instance))
+ (case (meta;run compiler
+ ($_ meta;either
+ (do Monad<Meta> [alts local-env] (test-provision provision context dep alts))
+ (do Monad<Meta> [alts local-structs] (test-provision provision context dep alts))
+ (do Monad<Meta> [alts import-structs] (test-provision provision context dep alts))))
+ (#;Left error)
+ (tc;fail error)
+
+ (#;Right candidates)
+ (case candidates
+ #;Nil
+ (tc;fail (format "No candidates for provisioning: " (%type dep)))
+
+ (#;Cons winner #;Nil)
+ (:: Monad<Check> wrap winner)
+
+ _
+ (tc;fail (format "Too many candidates for provisioning: " (%type dep) " --- " (%list (. %ident product;left) candidates))))
+ ))
+
+(def: (test-alternatives sig-type member-idx input-types output-type alts)
+ (-> Type Nat (List Type) Type (List [Ident Type]) (Meta (List Instance)))
+ (do Monad<Meta>
+ [compiler meta;get-compiler
+ context meta;type-context]
+ (case (|> alts
+ (List/map (function [[alt-name alt-type]]
+ (case (tc;run context
+ (do Monad<Check>
+ [[tvars alt-type] (concrete-type alt-type)
+ #let [[deps alt-type] (type;flatten-function alt-type)]
+ _ (tc;check alt-type sig-type)
+ member-type (find-member-type member-idx alt-type)
+ _ (check-apply member-type input-types output-type)
+ context' tc;get-context
+ =deps (M;map @ (provision compiler context') deps)]
+ (wrap =deps)))
+ (#;Left error)
+ (list)
+
+ (#;Right =deps)
+ (list [alt-name =deps]))))
+ List/join)
+ #;Nil
+ (meta;fail (format "No alternatives for " (%type (type;function input-types output-type))))
+
+ found
+ (wrap found))))
+
+(def: (find-alternatives sig-type member-idx input-types output-type)
+ (-> Type Nat (List Type) Type (Meta (List Instance)))
+ (let [test (test-alternatives sig-type member-idx input-types output-type)]
+ ($_ meta;either
+ (do Monad<Meta> [alts local-env] (test alts))
+ (do Monad<Meta> [alts local-structs] (test alts))
+ (do Monad<Meta> [alts import-structs] (test alts)))))
+
+(def: (var? input)
+ (-> Code Bool)
+ (case input
+ [_ (#;Symbol _)]
+ true
+
+ _
+ false))
+
+(def: (join-pair [l r])
+ (All [a] (-> [a a] (List a)))
+ (list l r))
+
+(def: (instance$ [constructor dependencies])
+ (-> Instance Code)
+ (case dependencies
+ #;Nil
+ (code;symbol constructor)
+
+ _
+ (` ((~ (code;symbol constructor)) (~@ (List/map instance$ dependencies))))))
+
+(syntax: #export (::: [member s;symbol]
+ [args (p;alt (p;seq (p;some s;symbol) s;end!)
+ (p;seq (p;some s;any) s;end!))])
+ {#;doc (doc "Automatic structure selection (for type-class style polymorphism)."
+ "This feature layers type-class style polymorphism on top of Lux's signatures and structures."
+ "When calling a polymorphic function, or using a polymorphic constant,"
+ "this macro will check the types of the arguments, and the expected type for the whole expression"
+ "and it will search in the local scope, the module's scope and the imports' scope"
+ "in order to find suitable structures to satisfy those requirements."
+ "If a single alternative is found, that one will be used automatically."
+ "If no alternative is found, or if more than one alternative is found (ambiguity)"
+ "a compile-time error will be raised, to alert the user."
+ "Examples:"
+ "Nat equality"
+ (:: number;Eq<Nat> = x y)
+ (::: = x y)
+ "Can optionally add the prefix of the module where the signature was defined."
+ (::: eq;= x y)
+ "(List Nat) equality"
+ (::: =
+ (list;n.range +1 +10)
+ (list;n.range +1 +10))
+ "(Functor List) map"
+ (::: map n.inc (list;n.range +0 +9))
+ "Caveat emptor: You need to make sure to import the module of any structure you want to use."
+ "Otherwise, this macro will not find it.")}
+ (case args
+ (#;Left [args _])
+ (do @
+ [[member-idx sig-type] (resolve-member member)
+ input-types (M;map @ resolve-type args)
+ output-type meta;expected-type
+ chosen-ones (find-alternatives sig-type member-idx input-types output-type)]
+ (case chosen-ones
+ #;Nil
+ (meta;fail (format "No structure option could be found for member: " (%ident member)))
+
+ (#;Cons chosen #;Nil)
+ (wrap (list (` (:: (~ (instance$ chosen))
+ (~ (code;local-symbol (product;right member)))
+ (~@ (List/map code;symbol args))))))
+
+ _
+ (meta;fail (format "Too many options available: "
+ (|> chosen-ones
+ (List/map (. %ident product;left))
+ (text;join-with ", "))
+ " --- for type: " (%type sig-type)))))
+
+ (#;Right [args _])
+ (do @
+ [labels (M;seq @ (list;repeat (list;size args)
+ (meta;gensym "")))
+ #let [retry (` (let [(~@ (|> (list;zip2 labels args) (List/map join-pair) List/join))]
+ (;;::: (~ (code;symbol member)) (~@ labels))))]]
+ (wrap (list retry)))
+ ))
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 05:44:18 +0000