aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/lang/analysis/case.lux23
-rw-r--r--new-luxc/source/luxc/lang/analysis/common.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/function.lux24
-rw-r--r--new-luxc/source/luxc/lang/analysis/inference.lux80
-rw-r--r--new-luxc/source/luxc/lang/analysis/procedure/common.lux36
-rw-r--r--new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/structure.lux41
-rw-r--r--new-luxc/source/luxc/lang/translation.lux40
-rw-r--r--new-luxc/source/luxc/lang/translation/statement.jvm.lux2
-rw-r--r--stdlib/source/lux/meta/type/check.lux225
-rw-r--r--stdlib/test/test/lux/meta/type/check.lux59
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 ""