diff options
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/case.lux | 23 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/common.lux | 12 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/function.lux | 24 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/inference.lux | 80 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/procedure/common.lux | 36 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux | 12 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/structure.lux | 41 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/translation.lux | 40 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/translation/statement.jvm.lux | 2 | ||||
| -rw-r--r-- | stdlib/source/lux/meta/type/check.lux | 225 | ||||
| -rw-r--r-- | stdlib/test/test/lux/meta/type/check.lux | 59 |
11 files changed, 233 insertions, 321 deletions
diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux index 5bf2e8ed1..ee4d4fcfa 100644 --- a/new-luxc/source/luxc/lang/analysis/case.lux +++ b/new-luxc/source/luxc/lang/analysis/case.lux @@ -47,13 +47,13 @@ (case caseT (#;Var id) (do meta;Monad<Meta> - [? (&;with-type-env - (tc;concrete? id))] - (if ? - (do @ - [caseT' (&;with-type-env - (tc;read id))] - (simplify-case-type caseT')) + [?caseT' (&;with-type-env + (tc;read id))] + (case ?caseT' + (#;Some caseT') + (simplify-case-type caseT') + + _ (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))) (#;Named name unnamedT) @@ -71,9 +71,12 @@ (do meta;Monad<Meta> [funcT' (&;with-type-env (do tc;Monad<Check> - [? (tc;concrete? funcT-id)] - (if ? - (tc;read funcT-id) + [?funct' (tc;read funcT-id)] + (case ?funct' + (#;Some funct') + (wrap funct') + + _ (tc;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))))] (simplify-case-type (#;Apply inputT funcT'))) diff --git a/new-luxc/source/luxc/lang/analysis/common.lux b/new-luxc/source/luxc/lang/analysis/common.lux index b14524559..968ebd2ea 100644 --- a/new-luxc/source/luxc/lang/analysis/common.lux +++ b/new-luxc/source/luxc/lang/analysis/common.lux @@ -11,14 +11,12 @@ (lang analysis))) (def: #export (with-unknown-type action) - (All [a] (-> (Meta Analysis) (Meta [Type Analysis]))) + (All [a] (-> (Meta a) (Meta [Type a]))) (do meta;Monad<Meta> - [[var-id var-type] (&;with-type-env tc;var) - analysis (&;with-expected-type var-type - action) - analysis-type (&;with-type-env - (tc;clean var-id var-type))] - (wrap [analysis-type analysis]))) + [[_ varT] (&;with-type-env tc;var) + analysis (&;with-expected-type varT + action)] + (wrap [varT analysis]))) (exception: #export Variant-Tag-Out-Of-Bounds) diff --git a/new-luxc/source/luxc/lang/analysis/function.lux b/new-luxc/source/luxc/lang/analysis/function.lux index 2a9826683..6a4a33e48 100644 --- a/new-luxc/source/luxc/lang/analysis/function.lux +++ b/new-luxc/source/luxc/lang/analysis/function.lux @@ -50,29 +50,21 @@ (#;Var id) (do @ - [? (&;with-type-env - (tc;concrete? id))] - (if ? - (do @ - [expectedT' (&;with-type-env - (tc;read id))] - (recur expectedT')) + [?expectedT' (&;with-type-env + (tc;read id))] + (case ?expectedT' + (#;Some expectedT') + (recur expectedT') + + _ ## Inference (do @ [[input-id inputT] (&;with-type-env tc;var) [output-id outputT] (&;with-type-env tc;var) #let [funT (#;Function inputT outputT)] funA (recur funT) - funT' (&;with-type-env - (tc;clean output-id funT)) - concrete-input? (&;with-type-env - (tc;concrete? input-id)) - funT'' (if concrete-input? - (&;with-type-env - (tc;clean input-id funT')) - (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT')))) _ (&;with-type-env - (tc;check expectedT funT''))] + (tc;check expectedT funT))] (wrap funA)) )) diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux index 5152de0b6..8b04ac2b7 100644 --- a/new-luxc/source/luxc/lang/analysis/inference.lux +++ b/new-luxc/source/luxc/lang/analysis/inference.lux @@ -14,50 +14,22 @@ (analysis ["&;" common])))) (exception: #export Cannot-Infer) +(def: (cannot-infer type args) + (-> Type (List Code) Text) + (format " Type: " (%type type) "\n" + "Arguments:" + (|> args + list;enumerate + (list/map (function [[idx argC]] + (format "\n " (%n idx) " " (%code argC)))) + (text;join-with "")))) + (exception: #export Cannot-Infer-Argument) (exception: #export Smaller-Variant-Than-Expected) (exception: #export Invalid-Type-Application) (exception: #export Not-A-Record-Type) (exception: #export Not-A-Variant-Type) -## When doing inference, type-variables often need to be created in -## order to figure out which types are present in the expression being -## inferred. -## If a type-variable never gets bound/resolved to a type, then that -## means the expression can be generalized through universal -## quantification. -## When that happens, the type-variable must be replaced by an -## argument to the universally-quantified type. -(def: #export (replace-var var-id bound-idx type) - (-> Nat Nat Type Type) - (case type - (#;Primitive name params) - (#;Primitive name (list/map (replace-var var-id bound-idx) params)) - - (^template [<tag>] - (<tag> left right) - (<tag> (replace-var var-id bound-idx left) - (replace-var var-id bound-idx right))) - ([#;Sum] - [#;Product] - [#;Function] - [#;Apply]) - - (#;Var id) - (if (n.= var-id id) - (#;Bound bound-idx) - type) - - (^template [<tag>] - (<tag> env quantified) - (<tag> (list/map (replace-var var-id bound-idx) env) - (replace-var var-id (n.+ +2 bound-idx) quantified))) - ([#;UnivQ] - [#;ExQ]) - - _ - type)) - (def: (replace-bound bound-idx replacementT type) (-> Nat Type Type Type) (case type @@ -110,18 +82,8 @@ (#;UnivQ _) (do meta;Monad<Meta> - [[var-id varT] (&;with-type-env tc;var) - [outputT argsA] (general analyse (maybe;assume (type;apply (list varT) inferT)) args)] - (do @ - [? (&;with-type-env - (tc;concrete? var-id)) - ## Quantify over the type if genericity/parametricity - ## is discovered. - outputT' (if ? - (&;with-type-env - (tc;clean var-id outputT)) - (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))] - (wrap [outputT' argsA]))) + [[var-id varT] (&;with-type-env tc;var)] + (general analyse (maybe;assume (type;apply (list varT) inferT)) args)) (#;ExQ _) (do meta;Monad<Meta> @@ -155,14 +117,18 @@ (analyse argC)))] (wrap [outputT' (list& argA args'A)])) + (#;Var infer-id) + (do meta;Monad<Meta> + [?inferT' (&;with-type-env (tc;read infer-id))] + (case ?inferT' + (#;Some inferT') + (general analyse inferT' args) + + _ + (&;throw Cannot-Infer (cannot-infer inferT args)))) + _ - (&;throw Cannot-Infer (format " Type: " (%type inferT) "\n" - "Arguments:" - (|> args - list;enumerate - (list/map (function [[idx argC]] - (format "\n " (%n idx) " " (%code argC)))) - (text;join-with ""))))) + (&;throw Cannot-Infer (cannot-infer inferT args))) )) ## Turns a record type into the kind of function type suitable for inference. diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux index fff5de504..3965e78ba 100644 --- a/new-luxc/source/luxc/lang/analysis/procedure/common.lux +++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux @@ -141,42 +141,6 @@ [lux//check typeA;analyse-check] [lux//coerce typeA;analyse-coerce]) -(def: (clean-type inputT) - (-> Type (tc;Check Type)) - (case inputT - (#;Primitive name paramsT+) - (do tc;Monad<Check> - [paramsT+' (monad;map @ clean-type paramsT+)] - (wrap (#;Primitive name paramsT+'))) - - (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _)) - (:: tc;Monad<Check> wrap inputT) - - (^template [<tag>] - (<tag> leftT rightT) - (do tc;Monad<Check> - [leftT' (clean-type leftT) - rightT' (clean-type rightT)] - (wrap (<tag> leftT' rightT')))) - ([#;Sum] [#;Product] [#;Function] [#;Apply]) - - (#;Var id) - (do tc;Monad<Check> - [? (tc;concrete? id)] - (if ? - (do @ - [actualT (tc;read id)] - (clean-type actualT)) - (wrap inputT))) - - (^template [<tag>] - (<tag> envT+ unquantifiedT) - (do tc;Monad<Check> - [envT+' (monad;map @ clean-type envT+)] - (wrap (<tag> envT+' unquantifiedT)))) - ([#;UnivQ] [#;ExQ]) - )) - (def: (lux//check//type proc) (-> Text Proc) (function [analyse eval args] diff --git a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux index 39ca0eb43..cd5fdc7bb 100644 --- a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux +++ b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux @@ -305,9 +305,9 @@ _ (&;infer varT) arrayA (&;with-expected-type (type (Array varT)) (analyse arrayC)) - elemT (&;with-type-env - (tc;read var-id)) - [elemT elem-class] (box-array-element-type elemT) + ?elemT (&;with-type-env + (tc;read var-id)) + [elemT elem-class] (box-array-element-type (maybe;default varT ?elemT)) idxA (&;with-expected-type Nat (analyse idxC))] (wrap (la;procedure proc (list (code;text elem-class) idxA arrayA)))) @@ -325,9 +325,9 @@ _ (&;infer (type (Array varT))) arrayA (&;with-expected-type (type (Array varT)) (analyse arrayC)) - elemT (&;with-type-env - (tc;read var-id)) - [valueT elem-class] (box-array-element-type elemT) + ?elemT (&;with-type-env + (tc;read var-id)) + [valueT elem-class] (box-array-element-type (maybe;default varT ?elemT)) idxA (&;with-expected-type Nat (analyse idxC)) valueA (&;with-expected-type valueT diff --git a/new-luxc/source/luxc/lang/analysis/structure.lux b/new-luxc/source/luxc/lang/analysis/structure.lux index e1f4de1d7..1f1ef15d7 100644 --- a/new-luxc/source/luxc/lang/analysis/structure.lux +++ b/new-luxc/source/luxc/lang/analysis/structure.lux @@ -1,17 +1,13 @@ (;module: lux (lux (control [monad #+ do] - ["ex" exception #+ exception:] - pipe) - [function] - (concurrency ["A" atom]) + ["ex" exception #+ exception:]) (data [ident] [number] [product] [maybe] (coll [list "list/" Functor<List>] [dict #+ Dict]) - [text] text/format) [meta] (meta [code] @@ -63,20 +59,21 @@ (#;Var id) (do @ - [concrete? (&;with-type-env - (tc;concrete? id))] - (if concrete? - (do @ - [expectedT' (&;with-type-env - (tc;read id))] - (&;with-expected-type expectedT' - (analyse-sum analyse tag valueC))) + [?expectedT' (&;with-type-env + (tc;read id))] + (case ?expectedT' + (#;Some expectedT') + (&;with-expected-type expectedT' + (analyse-sum analyse tag valueC)) + + _ ## Cannot do inference when the tag is numeric. ## This is because there is no way of knowing how many ## cases the inferred sum type would have. (&;throw Cannot-Infer-Numeric-Tag (format " Tag: " (%n tag) "\n" "Value: " (%code valueC) "\n" - " Type: " (%type expectedT))))) + " Type: " (%type expectedT))) + )) (^template [<tag> <instancer>] (<tag> _) @@ -166,14 +163,14 @@ (#;Var id) (do @ - [concrete? (&;with-type-env - (tc;concrete? id))] - (if concrete? - (do @ - [expectedT' (&;with-type-env - (tc;read id))] - (&;with-expected-type expectedT' - (analyse-product analyse membersC))) + [?expectedT' (&;with-type-env + (tc;read id))] + (case ?expectedT' + (#;Some expectedT') + (&;with-expected-type expectedT' + (analyse-product analyse membersC)) + + _ ## Must do inference... (do @ [membersTA (monad;map @ (|>. analyse &common;with-unknown-type) diff --git a/new-luxc/source/luxc/lang/translation.lux b/new-luxc/source/luxc/lang/translation.lux index cf3137aff..6726470cc 100644 --- a/new-luxc/source/luxc/lang/translation.lux +++ b/new-luxc/source/luxc/lang/translation.lux @@ -8,6 +8,7 @@ text/format (coll [dict])) [meta] + (meta (type ["tc" check])) [host] [io] (world [file #+ File])) @@ -35,6 +36,43 @@ (exception: #export Macro-Expansion-Failed) (exception: #export Unrecognized-Statement) +(def: (clean inputT) + (-> Type (tc;Check Type)) + (case inputT + (#;Primitive name paramsT+) + (do tc;Monad<Check> + [paramsT+' (monad;map @ clean paramsT+)] + (wrap (#;Primitive name paramsT+'))) + + (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _)) + (:: tc;Monad<Check> wrap inputT) + + (^template [<tag>] + (<tag> leftT rightT) + (do tc;Monad<Check> + [leftT' (clean leftT) + rightT' (clean rightT)] + (wrap (<tag> leftT' rightT')))) + ([#;Sum] [#;Product] [#;Function] [#;Apply]) + + (#;Var id) + (do tc;Monad<Check> + [?actualT (tc;read id)] + (case ?actualT + (#;Some actualT) + (clean actualT) + + _ + (wrap inputT))) + + (^template [<tag>] + (<tag> envT+ unquantifiedT) + (do tc;Monad<Check> + [envT+' (monad;map @ clean envT+)] + (wrap (<tag> envT+' unquantifiedT)))) + ([#;UnivQ] [#;ExQ]) + )) + (def: (translate code) (-> Code (Meta Unit)) (case code @@ -55,6 +93,8 @@ (wrap [Type valueA])) (commonA;with-unknown-type (analyse valueC)))) + valueT (&;with-type-env + (clean valueT)) valueI (expressionT;translate (expressionS;synthesize valueA)) _ (&;with-scope (statementT;translate-def def-name valueT valueI metaI (:! Code metaV)))] diff --git a/new-luxc/source/luxc/lang/translation/statement.jvm.lux b/new-luxc/source/luxc/lang/translation/statement.jvm.lux index 2a2173fa9..1cef99c76 100644 --- a/new-luxc/source/luxc/lang/translation/statement.jvm.lux +++ b/new-luxc/source/luxc/lang/translation/statement.jvm.lux @@ -76,7 +76,7 @@ tags (&module;declare-tags tags (meta;export? metaV) (:! Type valueV))) (wrap [])) - #let [_ (log! (format "DEF " current-module ";" def-name))]] + #let [_ (log! (format "DEF " (%ident [current-module def-name])))]] (commonT;record-artifact bytecode-name bytecode))) (def: #export (translate-program program-args programI) diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux index d6589760e..74c5a2a90 100644 --- a/stdlib/source/lux/meta/type/check.lux +++ b/stdlib/source/lux/meta/type/check.lux @@ -6,7 +6,7 @@ ["ex" exception #+ exception:]) (data [text "text/" Monoid<Text> Eq<Text>] [number "nat/" Codec<Text,Nat>] - maybe + [maybe] [product] (coll [list] [set #+ Set]) @@ -24,7 +24,9 @@ (type: #export Var Nat) -(type: #export Assumptions (List [[Type Type] Bool])) +(type: #export Assumption + {#subsumption [Type Type] + #verdict Bool}) (type: #export (Check a) (-> Type-Context (e;Error [Type-Context a]))) @@ -152,42 +154,35 @@ (#e;Success [(update@ #;ex-counter n.inc context) [id (#;Ex id)]])))) -(def: #export (bound? id) - (-> Var (Check Bool)) - (function [context] - (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some (#;Some bound)) - (#e;Success [context true]) - - (#;Some #;None) - (#e;Success [context false]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) - -(def: #export (concrete? id) - (-> Var (Check Bool)) - (function [context] - (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some (#;Some bound)) - (#e;Success [context (case bound (#;Var _) false _ true)]) - - (#;Some #;None) - (#e;Success [context false]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) +(do-template [<name> <outputT> <fail> <succeed>] + [(def: #export (<name> id) + (-> Var (Check <outputT>)) + (function [context] + (case (|> context (get@ #;var-bindings) (var::get id)) + (^or (#;Some (#;Some (#;Var _))) + (#;Some #;None)) + (#e;Success [context <fail>]) + + (#;Some (#;Some bound)) + (#e;Success [context <succeed>]) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id)))))] + + [bound? Bool false true] + [read (Maybe Type) #;None (#;Some bound)] + ) -(def: #export (read id) +(def: (peek id) (-> Var (Check Type)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some (#;Some type)) - (#e;Success [context type]) + (#;Some (#;Some bound)) + (#e;Success [context bound]) (#;Some #;None) (ex;throw Unbound-Type-Var (nat/encode id)) - + #;None (ex;throw Unknown-Type-Var (nat/encode id))))) @@ -220,51 +215,6 @@ #;None (ex;throw Unknown-Type-Var (nat/encode id))))) -(def: #export (clean t-id type) - (-> Var Type (Check Type)) - (case type - (#;Var id) - (do Monad<Check> - [? (concrete? id)] - (if ? - (if (n.= t-id id) - (read id) - (do Monad<Check> - [=type (read id) - ==type (clean t-id =type) - _ (update ==type id)] - (wrap type))) - (wrap type))) - - (#;Primitive name params) - (do Monad<Check> - [=params (monad;map @ (clean t-id) params)] - (wrap (#;Primitive name =params))) - - (^template [<tag>] - (<tag> left right) - (do Monad<Check> - [=left (clean t-id left) - =right (clean t-id right)] - (wrap (<tag> =left =right)))) - ([#;Function] - [#;Apply] - [#;Product] - [#;Sum]) - - (^template [<tag>] - (<tag> env body) - (do Monad<Check> - [=env (monad;map @ (clean t-id) env) - =body (clean t-id body)] ## TODO: DO NOT CLEAN THE BODY - (wrap (<tag> =env =body)))) - ([#;UnivQ] - [#;ExQ]) - - _ - (:: Monad<Check> wrap type) - )) - (def: #export var (Check [Var Type]) (function [context] @@ -291,12 +241,13 @@ (case funcT (#;Var func-id) (do Monad<Check> - [? (concrete? func-id)] - (if ? - (do @ - [funcT' (read func-id)] - (apply-type! funcT' argT)) - (throw Invalid-Type-Application (type;to-text (#;Apply argT funcT))))) + [?funcT' (read func-id)] + (case ?funcT' + #;None + (throw Invalid-Type-Application (type;to-text (#;Apply argT funcT))) + + (#;Some funcT') + (apply-type! funcT' argT))) _ (function [context] @@ -373,15 +324,15 @@ (right context)))) (def: (assumed? [e a] assumptions) - (-> [Type Type] Assumptions (Maybe Bool)) - (:: Monad<Maybe> map product;right + (-> [Type Type] (List Assumption) (Maybe Bool)) + (:: maybe;Monad<Maybe> map product;right (list;find (function [[[fe fa] status]] (and (type/= e fe) (type/= a fa))) assumptions))) (def: (assume! ea status assumptions) - (-> [Type Type] Bool Assumptions Assumptions) + (-> [Type Type] Bool (List Assumption) (List Assumption)) (#;Cons [ea status] assumptions)) (def: (on id type then else) @@ -398,8 +349,8 @@ _ (monad;map @ (update type) (set;to-list ring))] then) (do Monad<Check> - [bound (read id)] - (else bound)))) + [?bound (read id)] + (else (maybe;default (#;Var id) ?bound))))) (def: (link-2 left right) (-> Var Var (Check Unit)) @@ -414,15 +365,15 @@ (update (#;Var to) interpose))) (def: (check-vars check' assumptions idE idA) - (-> (-> Type Type Assumptions (Check Assumptions)) - Assumptions + (-> (-> Type Type (List Assumption) (Check (List Assumption))) + (List Assumption) Var Var - (Check Assumptions)) + (Check (List Assumption))) (if (n.= idE idA) (check/wrap assumptions) (do Monad<Check> - [ebound (attempt (read idE)) - abound (attempt (read idA))] + [ebound (attempt (peek idE)) + abound (attempt (peek idA))] (case [ebound abound] ## Link the 2 variables circularily [#;None #;None] @@ -504,9 +455,9 @@ output))) (def: (check-apply check' assumptions [eAT eFT] [aAT aFT]) - (-> (-> Type Type Assumptions (Check Assumptions)) Assumptions + (-> (-> Type Type (List Assumption) (Check (List Assumption))) (List Assumption) [Type Type] [Type Type] - (Check Assumptions)) + (Check (List Assumption))) (case [eFT aFT] (^or [(#;Ex _) _] [_ (#;Ex _)]) (do Monad<Check> @@ -514,31 +465,39 @@ (check' eAT aAT assumptions)) [(#;Var id) _] - (either (do Monad<Check> - [rFT (read id)] - (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions)) - (do Monad<Check> - [assumptions (check' (#;Var id) aFT assumptions) - e' (apply-type! aFT eAT) - a' (apply-type! aFT aAT)] - (check' e' a' assumptions))) + (do Monad<Check> + [?rFT (read id)] + (case ?rFT + (#;Some rFT) + (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions) + + _ + (do Monad<Check> + [assumptions (check' eFT aFT assumptions) + e' (apply-type! aFT eAT) + a' (apply-type! aFT aAT)] + (check' e' a' assumptions)))) [_ (#;Var id)] - (either (do Monad<Check> - [rFT (read id)] - (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions)) - (do Monad<Check> - [assumptions (check' eFT (#;Var id) assumptions) - e' (apply-type! eFT eAT) - a' (apply-type! eFT aAT)] - (check' e' a' assumptions))) + (do Monad<Check> + [?rFT (read id)] + (case ?rFT + (#;Some rFT) + (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions) + + _ + (do Monad<Check> + [assumptions (check' eFT aFT assumptions) + e' (apply-type! eFT eAT) + a' (apply-type! eFT aAT)] + (check' e' a' assumptions)))) _ (fail ""))) (def: #export (check' expected actual assumptions) {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."} - (-> Type Type Assumptions (Check Assumptions)) + (-> Type Type (List Assumption) (Check (List Assumption))) (if (is expected actual) (check/wrap assumptions) (with-error-stack @@ -588,33 +547,23 @@ [actual' (apply-type! F A)] (check' expected actual' assumptions)) - [(#;UnivQ _) _] - (do Monad<Check> - [[ex-id ex] existential - expected' (apply-type! expected ex)] - (check' expected' actual assumptions)) - - [_ (#;UnivQ _)] - (do Monad<Check> - [[var-id var] ;;var - actual' (apply-type! actual var) - assumptions (check' expected actual' assumptions) - _ (clean var-id expected)] - (check/wrap assumptions)) - - [(#;ExQ e!env e!def) _] - (do Monad<Check> - [[var-id var] ;;var - expected' (apply-type! expected var) - assumptions (check' expected' actual assumptions) - _ (clean var-id actual)] - (check/wrap assumptions)) - - [_ (#;ExQ a!env a!def)] - (do Monad<Check> - [[ex-id ex] existential - actual' (apply-type! actual ex)] - (check' expected actual' assumptions)) + (^template [<tag> <instancer>] + [(<tag> _) _] + (do Monad<Check> + [[_ paramT] <instancer> + expected' (apply-type! expected paramT)] + (check' expected' actual assumptions))) + ([#;UnivQ ;;existential] + [#;ExQ ;;var]) + + (^template [<tag> <instancer>] + [_ (<tag> _)] + (do Monad<Check> + [[_ paramT] <instancer> + actual' (apply-type! actual paramT)] + (check' expected actual' assumptions))) + ([#;UnivQ ;;var] + [#;ExQ ;;existential]) [(#;Primitive e-name e-params) (#;Primitive a-name a-params)] (if (and (text/= e-name a-name) diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux index b1239fa43..127e02cbd 100644 --- a/stdlib/test/test/lux/meta/type/check.lux +++ b/stdlib/test/test/lux/meta/type/check.lux @@ -76,7 +76,7 @@ false)) ## [Tests] -(context: "Top and Bottom" +(context: "Top and Bottom." (<| (times +100) (do @ [sample (|> gen-type (r;filter valid-type?))] @@ -96,35 +96,35 @@ (test "Existential types only match with themselves." (and (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check ex ex))) + [[_ exT] @;existential] + (@;check exT exT))) (not (type-checks? (do @;Monad<Check> - [[lid lex] @;existential - [rid rex] @;existential] - (@;check lex rex)))))) + [[_ exTL] @;existential + [_ exTR] @;existential] + (@;check exTL exTR)))))) - (test "Names don't affect type-checking." + (test "Names do not affect type-checking." (and (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check (#;Named ["module" "name"] ex) - ex))) + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + exT))) (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check ex - (#;Named ["module" "name"] ex)))) + [[_ exT] @;existential] + (@;check exT + (#;Named ["module" "name"] exT)))) (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check (#;Named ["module" "name"] ex) - (#;Named ["module" "name"] ex)))))) + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + (#;Named ["module" "name"] exT)))))) - (test "Can type-check functions." + (test "Functions are covariant on inputs and contravariant on outputs." (and (@;checks? (#;Function Bottom Top) (#;Function Top Bottom)) (not (@;checks? (#;Function Top Bottom) (#;Function Bottom Top))))) )) -(context: "Type application" +(context: "Type application." (<| (times +100) (do @ [meta gen-type @@ -135,7 +135,7 @@ (@;checks? (type;tuple (list meta data)) (|> Ann (#;Apply meta) (#;Apply data)))))))) -(context: "Primitive types" +(context: "Primitive types." (<| (times +100) (do @ [nameL gen-name @@ -156,7 +156,7 @@ (#;Primitive nameL (list paramR))))) )))) -(context: "Type-vars" +(context: "Type variables." ($_ seq (test "Type-vars check against themselves." (type-checks? (do @;Monad<Check> @@ -203,11 +203,11 @@ ids+types)] (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) -(context: "Rings." +(context: "Rings of type variables." (<| (times +100) (do @ [num-connections (|> r;nat (:: @ map (n.% +100))) - bound (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) + boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) pick-pcg (r;seq r;nat r;nat)] ($_ seq (test "Can create rings of variables." @@ -227,26 +227,29 @@ same-vars?)))))) (test "When a var in a ring is bound, all the ring is bound." (type-checks? (do @;Monad<Check> - [[[head-id head-type] ids+types tail-type] (build-ring num-connections) + [[[head-id headT] ids+types tailT] (build-ring num-connections) #let [ids (list/map product;left ids+types)] - _ (@;check head-type bound) + _ (@;check headT boundT) head-bound (@;read head-id) tail-bound (monad;map @ @;read ids) headR (@;ring head-id) tailR+ (monad;map @ @;ring ids)] (let [rings-were-erased? (and (set;empty? headR) (list;every? set;empty? tailR+)) - same-types? (list;every? (type/= bound) (list& head-bound tail-bound))] + same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) + (list/map (function [[tail-id ?tailT]] + (maybe;default (#;Var tail-id) ?tailT)) + (list;zip2 ids tail-bound))))] (@;assert "" (and rings-were-erased? same-types?)))))) (test "Can merge multiple rings of variables." (type-checks? (do @;Monad<Check> - [[[head-idL head-typeL] ids+typesL [tail-idL tail-typeL]] (build-ring num-connections) - [[head-idR head-typeR] ids+typesR [tail-idR tail-typeR]] (build-ring num-connections) + [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) + [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) headRL-pre (@;ring head-idL) headRR-pre (@;ring head-idR) - _ (@;check head-typeL head-typeR) + _ (@;check headTL headTR) headRL-post (@;ring head-idL) headRR-post (@;ring head-idR)] (@;assert "" |