aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux.lux10
-rw-r--r--stdlib/source/lux/control/effect.lux2
-rw-r--r--stdlib/source/lux/macro/poly.lux4
-rw-r--r--stdlib/source/lux/type.lux47
-rw-r--r--stdlib/source/lux/type/auto.lux59
-rw-r--r--stdlib/source/lux/type/check.lux16
-rw-r--r--stdlib/test/test/lux/type.lux164
-rw-r--r--stdlib/test/test/lux/type/auto.lux28
-rw-r--r--stdlib/test/test/lux/type/check.lux162
-rw-r--r--stdlib/test/tests.lux16
10 files changed, 427 insertions, 81 deletions
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index de985db95..b834649e8 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -3254,8 +3254,8 @@
_
(list type)))]
- [flatten-sum #;SumT]
- [flatten-prod #;ProdT]
+ [flatten-variant #;SumT]
+ [flatten-tuple #;ProdT]
[flatten-lambda #;LambdaT]
[flatten-app #;AppT]
)
@@ -3264,7 +3264,7 @@
(-> Type (Maybe (List Type)))
(case type
(#ProdT _)
- (#Some (flatten-prod type))
+ (#Some (flatten-tuple type))
(#AppT fun arg)
(do Monad<Maybe>
@@ -4059,10 +4059,10 @@
"Unit"
(#SumT _)
- ($_ Text/append "(| " (|> (flatten-sum type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
+ ($_ Text/append "(| " (|> (flatten-variant type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
(#ProdT _)
- ($_ Text/append "[" (|> (flatten-prod type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]")
+ ($_ Text/append "[" (|> (flatten-tuple type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]")
(#LambdaT _)
($_ Text/append "(-> " (|> (flatten-lambda type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
diff --git a/stdlib/source/lux/control/effect.lux b/stdlib/source/lux/control/effect.lux
index 16605e1c7..379a28d76 100644
--- a/stdlib/source/lux/control/effect.lux
+++ b/stdlib/source/lux/control/effect.lux
@@ -300,7 +300,7 @@
(if (tc;checks? (clean-effect effect) eff0)
(#;Some idx)
#;None))
- (|> unfoldT1 type;flatten-sum (List/map un-apply) list;enumerate))
+ (|> unfoldT1 type;flatten-variant (List/map un-apply) list;enumerate))
(#;Some idx)])
(wrap (list (` (#;;Effect (:: (~ g!functor) (~' map) (~' wrap) ((~ (ast;int (nat-to-int idx)))
(~ (ast;symbol var))))))))
diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux
index 0973eece6..8c3a5b288 100644
--- a/stdlib/source/lux/macro/poly.lux
+++ b/stdlib/source/lux/macro/poly.lux
@@ -91,8 +91,8 @@
(:: compiler;Monad<Lux> wrap members)
(compiler;fail (format "Not a " ($AST$ <tag>) " type: " (%type :type:)))))))]
- [sum sum+ type;flatten-sum #;SumT]
- [prod prod+ type;flatten-prod #;ProdT]
+ [sum sum+ type;flatten-variant #;SumT]
+ [prod prod+ type;flatten-tuple #;ProdT]
)
(def: #export func
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index c16c8217b..91b44bfd8 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -128,11 +128,11 @@
_
[(list) type]))
-(def: #export (flatten-apply type)
+(def: #export (flatten-application type)
(-> Type [Type (List Type)])
(case type
(#;AppT left' right)
- (let [[left rights] (flatten-apply left')]
+ (let [[left rights] (flatten-application left')]
[left (List/append rights (list right))])
_
@@ -148,8 +148,8 @@
_
(list type)))]
- [flatten-sum #;SumT]
- [flatten-prod #;ProdT]
+ [flatten-variant #;SumT]
+ [flatten-tuple #;ProdT]
)
(def: #export (apply-type type-fun param)
@@ -197,8 +197,8 @@
(^template [<tag> <macro> <flattener>]
(<tag> left right)
(` (<macro> (~@ (List/map to-ast (<flattener> type))))))
- ([#;SumT | flatten-sum]
- [#;ProdT & flatten-prod])
+ ([#;SumT | flatten-variant]
+ [#;ProdT & flatten-tuple])
(#;NamedT name sub-type)
(ast;symbol name)
@@ -236,8 +236,8 @@
(list;interpose " ")
(List/fold Text/append ""))
<close>))
- ([#;SumT "(| " ")" flatten-sum]
- [#;ProdT "[" "]" flatten-prod])
+ ([#;SumT "(| " ")" flatten-variant]
+ [#;ProdT "[" "]" flatten-tuple])
(#;LambdaT input output)
(let [[ins out] (flatten-function type)]
@@ -259,7 +259,7 @@
($_ Text/append "⟨e:" (Nat/encode id) "⟩")
(#;AppT fun param)
- (let [[type-fun type-args] (flatten-apply type)]
+ (let [[type-fun type-args] (flatten-application type)]
($_ Text/append "(" (to-text type-fun) " " (|> type-args (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")"))
(#;UnivQ env body)
@@ -306,3 +306,32 @@
[variant Void #;SumT]
[tuple Unit #;ProdT]
)
+
+(def: #export (function inputs output)
+ (-> (List Type) Type Type)
+ (case inputs
+ #;Nil
+ output
+
+ (#;Cons input inputs')
+ (#;LambdaT input (function inputs' output))))
+
+(def: #export (application quant params)
+ (-> Type (List Type) Type)
+ (case params
+ #;Nil
+ quant
+
+ (#;Cons param params')
+ (application (#;AppT quant param) params')))
+
+(do-template [<name> <tag>]
+ [(def: #export (<name> size body)
+ (-> Nat Type Type)
+ (case size
+ +0 body
+ _ (<tag> (list) (<name> (n.dec size) body))))]
+
+ [univq #;UnivQ]
+ [exq #;ExQ]
+ )
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index f33314ac1..c22434e9f 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -20,6 +20,37 @@
(type ["tc" check #+ Check Monad<Check>])
))
+(def: (find-type-var id env)
+ (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+ (case (list;find (|>. product;left (n.= id))
+ (get@ #;mappings env))
+ (#;Some [_ (#;Some type)])
+ (case type
+ (#;VarT id')
+ (find-type-var id' env)
+
+ _
+ (:: Monad<Lux> wrap type))
+
+ (#;Some [_ #;None])
+ (compiler;fail (format "Unbound type-var " (%n id)))
+
+ #;None
+ (compiler;fail (format "Unknown type-var " (%n id)))
+ ))
+
+(def: (resolve-type var-name)
+ (-> Ident (Lux Type))
+ (do Monad<Lux>
+ [raw-type (compiler;find-type var-name)
+ compiler compiler;get-compiler]
+ (case raw-type
+ (#;VarT id)
+ (find-type-var id (get@ #;type-vars compiler))
+
+ _
+ (wrap raw-type))))
+
(def: (find-member-type idx sig-type)
(-> Nat Type (Check Type))
(case sig-type
@@ -84,8 +115,12 @@
(do Monad<Lux>
[this-module-name compiler;current-module-name
imp-mods (compiler;imported-modules this-module-name)
- export-batches (mapM @ compiler;exports imp-mods)]
- (wrap (prepare-defs this-module-name (List/join export-batches)))))
+ export-batches (mapM @ (lambda [imp-mod]
+ (do @
+ [exports (compiler;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))
@@ -123,7 +158,7 @@
(lambda [compiler]
(let [type-vars (get@ #;type-vars compiler)
context (|> tc;fresh-context
- (set@ #tc;var-id (get@ #;counter type-vars))
+ (set@ #tc;var-counter (get@ #;counter type-vars))
(set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
(#;Right [compiler context]))))
@@ -135,7 +170,7 @@
(list;filter (lambda [[alt-name alt-type]]
(case (tc;run context
(do Monad<Check>
- [_ (tc;check sig-type 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)))
(#;Left error)
@@ -171,23 +206,23 @@
(All [a] (-> [a a] (List a)))
(list l r))
-(syntax: #export (::: {member s;symbol}
- {args (s;alt (s;some s;symbol)
- (s;some s;any))})
+(syntax: #export (::: [member s;symbol]
+ [args (s;alt (s;some s;symbol)
+ (s;some s;any))])
(case args
(#;Left args)
(do @
[[member-idx sig-type] (resolve-member member)
- input-types (mapM @ compiler;find-type args)
+ input-types (mapM @ resolve-type args)
output-type compiler;expected-type
chosen-ones (find-alternatives sig-type member-idx input-types output-type)]
(case chosen-ones
#;Nil
- (compiler;fail (format "No structure option could be found for member " (%ident member)))
+ (compiler;fail (format "No structure option could be found for member: " (%ident member)))
(#;Cons chosen #;Nil)
(wrap (list (` (:: (~ (ast;symbol chosen))
- (~ (ast;symbol member))
+ (~ (ast;local-symbol (product;right member)))
(~@ (List/map ast;symbol args))))))
_
@@ -205,7 +240,3 @@
#let [retry (` (let [(~@ (|> (list;zip2 labels args-to-bind) (List/map join-pair) List/join))]
(;;::: (~ (ast;symbol member)) (~@ labels))))]]
(wrap (list retry)))))
-
-(comment
- (::: map i.inc (list 0 1 2 3 4))
- )
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 951586bb0..b9a1301bc 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -24,8 +24,8 @@
(type: #export Fixpoints (List [[Type Type] Bool]))
(type: #export Context
- {#var-id Id
- #ex-id Id
+ {#var-counter Id
+ #ex-counter Id
#bindings (dict;Dict Id (Maybe Type))
#fixpoints Fixpoints
})
@@ -111,8 +111,8 @@
(def: #export existential
(Check [Id Type])
(lambda [context]
- (let [id (get@ #ex-id context)]
- (#;Right [(update@ #ex-id n.inc context)
+ (let [id (get@ #ex-counter context)]
+ (#;Right [(update@ #ex-counter n.inc context)
[id (#;ExT id)]]))))
(def: (bound? id)
@@ -241,9 +241,9 @@
(def: #export create-var
(Check [Id Type])
(lambda [context]
- (let [id (get@ #var-id context)]
+ (let [id (get@ #var-counter context)]
(#;Right [(|> context
- (update@ #var-id n.inc)
+ (update@ #var-counter n.inc)
(update@ #bindings (dict;put id #;None)))
[id (#;VarT id)]]))))
@@ -307,8 +307,8 @@
(def: #export fresh-context
Context
- {#var-id +0
- #ex-id +0
+ {#var-counter +0
+ #ex-counter +0
#bindings (dict;new number;Hash<Nat>)
#fixpoints (list)
})
diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux
index 8fa871e70..0e203f376 100644
--- a/stdlib/test/test/lux/type.lux
+++ b/stdlib/test/test/lux/type.lux
@@ -1,41 +1,137 @@
+## 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/.
+
(;module:
lux
(lux (codata [io])
(control monad)
(data [text "Text/" Monoid<Text>]
- [number])
- type
- (codata function))
+ text/format
+ [number]
+ maybe
+ (struct [list]))
+ (math ["R" random])
+ pipe
+ ["&" type])
lux/test)
-(test: "lux/type exports"
- (let% [<eq-tests> (do-template [<type>]
- [(match true (:: Eq<Type> = <type> <type>))]
-
- [(#;HostT "java.util.List" (list Int))]
- [#;UnitT]
- [#;VoidT]
- [(#;VarT +123)]
- [(#;ExT +123)]
- [(#;BoundT +123)]
- [(#;LambdaT Bool Int)]
- [(#;AppT List Int)]
- [(#;NamedT ["" "Int-List"] (#;AppT List Int))]
- [(#;SumT Bool Int)]
- [(#;ProdT Bool Int)]
- [(#;UnivQ (list) (#;ProdT Bool (#;BoundT +1)))]
- [(#;ExQ (list) (#;ProdT Bool (#;BoundT +1)))]
- )]
- (test-all <eq-tests>
- (match (^=> (#;Some _type) (:: Eq<Type> = _type (#;ProdT Bool Int)))
- (apply-type (type (Meta Bool)) Int))
- (match #;None (apply-type Text Bool))
- (match true
- (:: Eq<Type> =
- (#;NamedT ["" "a"]
- (#;ProdT Bool Int))
- (un-alias (#;NamedT ["" "c"]
- (#;NamedT ["" "b"]
- (#;NamedT ["" "a"]
- (#;ProdT Bool Int)))))))
- )))
+## [Utils]
+(def: gen-name
+ (R;Random Text)
+ (do R;Monad<Random>
+ [size (|> R;nat (:: @ map (n.% +10)))]
+ (R;text size)))
+
+(def: gen-ident
+ (R;Random Ident)
+ (R;seq gen-name gen-name))
+
+(def: gen-type
+ (R;Random Type)
+ (let [(^open "R/") R;Monad<Random>]
+ (R;rec (lambda [gen-type]
+ ($_ R;alt
+ (R;seq gen-name (R/wrap (list)))
+ (R/wrap [])
+ (R/wrap [])
+ (R;seq gen-type gen-type)
+ (R;seq gen-type gen-type)
+ (R;seq gen-type gen-type)
+ R;nat
+ R;nat
+ R;nat
+ (R;seq (R/wrap (list)) gen-type)
+ (R;seq (R/wrap (list)) gen-type)
+ (R;seq gen-type gen-type)
+ (R;seq gen-ident gen-type)
+ )))))
+
+## [Tests]
+(test: "Types"
+ [sample gen-type]
+ (assert "Every type is equal to itself."
+ (:: &;Eq<Type> = sample sample)))
+
+(test: "Type application"
+ (assert "Can apply quantified types (universal and existential quantification)."
+ (and (default false
+ (do Monad<Maybe>
+ [partial (&;apply-type Meta Bool)
+ full (&;apply-type partial Int)]
+ (wrap (:: &;Eq<Type> = full (#;ProdT Bool Int)))))
+ (|> (&;apply-type Text Bool)
+ (case> #;None true _ false)))))
+
+(test: "Naming"
+ (let [base (#;NamedT ["" "a"] (#;ProdT Bool Int))
+ aliased (#;NamedT ["" "c"]
+ (#;NamedT ["" "b"]
+ base))]
+ ($_ seq
+ (assert "Can remove aliases from an already-named type."
+ (:: &;Eq<Type> =
+ base
+ (&;un-alias aliased)))
+
+ (assert "Can remove all names from a type."
+ (and (not (:: &;Eq<Type> =
+ base
+ (&;un-name aliased)))
+ (:: &;Eq<Type> =
+ (&;un-name base)
+ (&;un-name aliased)))))))
+
+(test: "Type construction [structs]"
+ [size (|> R;nat (:: @ map (n.% +3)))
+ members (seqM @ (list;repeat size gen-type))
+ #let [(^open "&/") &;Eq<Type>
+ (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+ (let% [<struct-tests> (do-template [<desc> <ctor> <dtor> <unit>]
+ [(assert (format "Can build and tear-down " <desc> " types.")
+ (let [flat (|> members <ctor> <dtor>)]
+ (or (n.= (list;size members) (list;size flat))
+ (and (n.= +0 (list;size members))
+ (n.= +1 (list;size flat))
+ (|> flat list;head (default (undefined)) (&/= <unit>))))))]
+
+ ["variant" &;variant &;flatten-variant #;VoidT]
+ ["tuple" &;tuple &;flatten-tuple #;UnitT]
+ )]
+ ($_ seq
+ <struct-tests>
+ )))
+
+(test: "Type construction [parameterized]"
+ [size (|> R;nat (:: @ map (n.% +3)))
+ members (seqM @ (list;repeat size gen-type))
+ extra gen-type
+ #let [(^open "&/") &;Eq<Type>
+ (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+ ($_ seq
+ (assert "Can build and tear-down function types."
+ (let [[inputs output] (|> (&;function members extra) &;flatten-function)]
+ (n.= (list;size members) (list;size inputs))))
+
+ (assert "Can build and tear-down application types."
+ (let [[tfunc tparams] (|> members (&;application extra) &;flatten-application)]
+ (n.= (list;size members) (list;size tparams))))
+ ))
+
+(test: "Type construction [higher order]"
+ [size (|> R;nat (:: @ map (n.% +3)))
+ extra gen-type
+ #let [(^open "&/") &;Eq<Type>]]
+ (let% [<quant-tests> (do-template [<desc> <ctor> <dtor>]
+ [(assert (format "Can build and tear-down " <desc> " types.")
+ (let [[flat-size flat-body] (|> extra (<ctor> size) <dtor>)]
+ (and (n.= size flat-size)
+ (&/= extra flat-body))))]
+
+ ["universally-quantified" &;univq &;flatten-univq]
+ ["existentially-quantified" &;exq &;flatten-exq]
+ )]
+ ($_ seq
+ <quant-tests>
+ )))
diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux
new file mode 100644
index 000000000..ef69961cd
--- /dev/null
+++ b/stdlib/test/test/lux/type/auto.lux
@@ -0,0 +1,28 @@
+## 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/.
+
+(;module:
+ lux
+ (lux (codata [io])
+ (control monad
+ [eq])
+ (data [text "Text/" Monoid<Text>]
+ text/format
+ [number]
+ [bool "B/" Eq<Bool>]
+ maybe
+ (struct [list]))
+ (math ["R" random])
+ pipe
+ [type]
+ type/auto)
+ lux/test)
+
+(test: "Automatic structure selection"
+ [x R;nat
+ y R;nat]
+ (assert "Can automatically select first-order structures."
+ (B/= (:: number;Eq<Nat> = x y)
+ (::: eq;= x y))))
diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux
new file mode 100644
index 000000000..273dbad4c
--- /dev/null
+++ b/stdlib/test/test/lux/type/check.lux
@@ -0,0 +1,162 @@
+## 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/.
+
+(;module:
+ lux
+ (lux (codata [io])
+ (control monad)
+ (data [text "Text/" Monoid<Text>]
+ text/format
+ [number]
+ maybe
+ (struct [list]))
+ (math ["R" random])
+ pipe
+ [type]
+ ["&" type/check])
+ lux/test)
+
+## [Utils]
+(def: gen-name
+ (R;Random Text)
+ (do R;Monad<Random>
+ [size (|> R;nat (:: @ map (n.% +10)))]
+ (R;text size)))
+
+(def: gen-ident
+ (R;Random Ident)
+ (R;seq gen-name gen-name))
+
+(def: gen-type
+ (R;Random Type)
+ (let [(^open "R/") R;Monad<Random>]
+ (R;rec (lambda [gen-type]
+ ($_ R;alt
+ (R;seq gen-name (R/wrap (list)))
+ (R/wrap [])
+ (R/wrap [])
+ (R;seq gen-type gen-type)
+ (R;seq gen-type gen-type)
+ (R;seq gen-type gen-type)
+ R;nat
+ R;nat
+ R;nat
+ (R;seq (R/wrap (list)) gen-type)
+ (R;seq (R/wrap (list)) gen-type)
+ (R;seq gen-type gen-type)
+ (R;seq gen-ident gen-type)
+ )))))
+
+(def: (type-checks? input)
+ (-> (&;Check []) Bool)
+ (case (&;run &;fresh-context input)
+ (#;Right [])
+ true
+
+ (#;Left error)
+ false))
+
+## [Tests]
+(test: "Top and Bottom"
+ [sample gen-type]
+ ($_ seq
+ (assert "Top is the super-type 0f everything."
+ (&;checks? Top sample))
+
+ (assert "Bottom is the sub-type 0f everything."
+ (&;checks? sample Bottom))
+ ))
+
+(test: "Simple type-checking."
+ ($_ seq
+ (assert "Unit and Void match themselves."
+ (and (&;checks? Void Void)
+ (&;checks? Unit Unit)))
+
+ (assert "Existential types only match with themselves."
+ (and (type-checks? (do &;Monad<Check>
+ [[id ex] &;existential]
+ (&;check ex ex)))
+ (not (type-checks? (do &;Monad<Check>
+ [[lid lex] &;existential
+ [rid rex] &;existential]
+ (&;check lex rex))))))
+
+ (assert "Names don't affect type-checking."
+ (and (type-checks? (do &;Monad<Check>
+ [[id ex] &;existential]
+ (&;check (#;NamedT ["module" "name"] ex)
+ ex)))
+ (type-checks? (do &;Monad<Check>
+ [[id ex] &;existential]
+ (&;check ex
+ (#;NamedT ["module" "name"] ex))))
+ (type-checks? (do &;Monad<Check>
+ [[id ex] &;existential]
+ (&;check (#;NamedT ["module" "name"] ex)
+ (#;NamedT ["module" "name"] ex))))))
+
+ (assert "Can type-check functions."
+ (and (&;checks? (#;LambdaT Bottom Top)
+ (#;LambdaT Top Bottom))
+ (not (&;checks? (#;LambdaT Top Bottom)
+ (#;LambdaT Bottom Top)))))
+ ))
+
+(test: "Type application"
+ [meta gen-type
+ data gen-type]
+ (assert "Can type-check type application."
+ (and (&;checks? (#;AppT (#;AppT Meta meta) data)
+ (type;tuple (list meta data)))
+ (&;checks? (type;tuple (list meta data))
+ (#;AppT (#;AppT Meta meta) data)))))
+
+(test: "Host types"
+ [nameL gen-name
+ nameR gen-name
+ paramL gen-type
+ paramR gen-type]
+ ($_ seq
+ (assert "Host types match when they have the same name and the same parameters."
+ (&;checks? (#;HostT nameL (list paramL))
+ (#;HostT nameL (list paramL))))
+
+ (assert "Names matter to host types."
+ (&;checks? (#;HostT nameL (list paramL))
+ (#;HostT nameR (list paramL))))
+
+ (assert "Parameters matter to host types."
+ (&;checks? (#;HostT nameL (list paramL))
+ (#;HostT nameL (list paramR))))
+ ))
+
+(test: "Type-vars"
+ ($_ seq
+ (assert "Type-vars check against themselves."
+ (type-checks? (&;with-var (lambda [[id var]] (&;check var var)))))
+
+ (assert "Can bind unbound type-vars by type-checking against them."
+ (and (type-checks? (&;with-var (lambda [[id var]] (&;check var #;UnitT))))
+ (type-checks? (&;with-var (lambda [[id var]] (&;check #;UnitT var))))))
+
+ (assert "Can't rebind already bound type-vars."
+ (not (type-checks? (&;with-var (lambda [[id var]]
+ (do &;Monad<Check>
+ [_ (&;check var #;UnitT)]
+ (&;check var #;VoidT)))))))
+
+ (assert "If the type bound to a var is a super-type to another, then the var is also a super-type."
+ (type-checks? (&;with-var (lambda [[id var]]
+ (do &;Monad<Check>
+ [_ (&;check var Top)]
+ (&;check var #;UnitT))))))
+
+ (assert "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
+ (type-checks? (&;with-var (lambda [[id var]]
+ (do &;Monad<Check>
+ [_ (&;check var Bottom)]
+ (&;check #;UnitT var))))))
+ ))
diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux
index e225e1f28..ef94dca90 100644
--- a/stdlib/test/tests.lux
+++ b/stdlib/test/tests.lux
@@ -59,17 +59,17 @@
(macro ["_;" ast]
["_;" syntax]
["_;" template])
- ## [type]
- ## (type [check] [auto])
- ## (control ...)
+ ["_;" type]
+ (type ["_;" check]
+ ["_;" auto])
+ ## (control [effect])
)
)
## (lux (codata [cont])
- ## (macro [poly]
- ## (poly ["poly_;" eq]
- ## ["poly_;" text-encoder]
- ## ["poly_;" functor]))
- ## (control [effect]))
+ ## (macro [poly]
+ ## (poly ["poly_;" eq]
+ ## ["poly_;" text-encoder]
+ ## ["poly_;" functor])))
)
## [Program]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 03:08:58 +0000