aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/meta/type/check.lux372
-rw-r--r--stdlib/test/test/lux/meta/type/check.lux115
2 files changed, 369 insertions, 118 deletions
diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux
index 296aee11a..920eb876c 100644
--- a/stdlib/source/lux/meta/type/check.lux
+++ b/stdlib/source/lux/meta/type/check.lux
@@ -1,36 +1,38 @@
-(;module: {#;doc "Type-checking functionality.
-
- Very useful for writing advanced macros."}
+(;module: {#;doc "Type-checking functionality."}
lux
(lux (control [functor #+ Functor]
[applicative #+ Applicative]
- [monad #+ do Monad])
+ [monad #+ do Monad]
+ ["ex" exception #+ exception:])
(data [text "text/" Monoid<Text> Eq<Text>]
[number "nat/" Codec<Text,Nat>]
maybe
[product]
- (coll [list])
- ["E" error])
+ (coll [list]
+ [set #+ Set])
+ ["e" error])
(meta [type "type/" Eq<Type>])
))
+(type: #export Var Nat)
+
(type: #export Assumptions (List [[Type Type] Bool]))
(type: #export (Check a)
- (-> Type-Context (E;Error [Type-Context a])))
+ (-> Type-Context (e;Error [Type-Context a])))
(type: #export Type-Vars
- (List [Nat (Maybe Type)]))
+ (List [Var (Maybe Type)]))
(struct: #export _ (Functor Check)
(def: (map f fa)
(function [context]
(case (fa context)
- (#E;Error error)
- (#E;Error error)
+ (#e;Error error)
+ (#e;Error error)
- (#E;Success [context' output])
- (#E;Success [context' (f output)])
+ (#e;Success [context' output])
+ (#e;Success [context' (f output)])
))))
(struct: #export _ (Applicative Check)
@@ -38,21 +40,21 @@
(def: (wrap x)
(function [context]
- (#E;Success [context x])))
+ (#e;Success [context x])))
(def: (apply ff fa)
(function [context]
(case (ff context)
- (#E;Success [context' f])
+ (#e;Success [context' f])
(case (fa context')
- (#E;Success [context'' a])
- (#E;Success [context'' (f a)])
+ (#e;Success [context'' a])
+ (#e;Success [context'' (f a)])
- (#E;Error error)
- (#E;Error error))
+ (#e;Error error)
+ (#e;Error error))
- (#E;Error error)
- (#E;Error error)
+ (#e;Error error)
+ (#e;Error error)
)))
)
@@ -62,23 +64,23 @@
(def: (join ffa)
(function [context]
(case (ffa context)
- (#E;Success [context' fa])
+ (#e;Success [context' fa])
(case (fa context')
- (#E;Success [context'' a])
- (#E;Success [context'' a])
+ (#e;Success [context'' a])
+ (#e;Success [context'' a])
- (#E;Error error)
- (#E;Error error))
+ (#e;Error error)
+ (#e;Error error))
- (#E;Error error)
- (#E;Error error)
+ (#e;Error error)
+ (#e;Error error)
)))
)
(open Monad<Check> "check/")
(def: (var::get id plist)
- (-> Nat Type-Vars (Maybe (Maybe Type)))
+ (-> Var Type-Vars (Maybe (Maybe Type)))
(case plist
#;Nil
#;None
@@ -91,7 +93,7 @@
))
(def: (var::put id value plist)
- (-> Nat (Maybe Type) Type-Vars Type-Vars)
+ (-> Var (Maybe Type) Type-Vars Type-Vars)
(case plist
#;Nil
(list [id value])
@@ -106,7 +108,7 @@
))
(def: (var::remove id plist)
- (-> Nat Type-Vars Type-Vars)
+ (-> Var Type-Vars Type-Vars)
(case plist
#;Nil
#;Nil
@@ -121,96 +123,100 @@
## [[Logic]]
(def: #export (run context proc)
- (All [a] (-> Type-Context (Check a) (E;Error a)))
+ (All [a] (-> Type-Context (Check a) (e;Error a)))
(case (proc context)
- (#E;Error error)
- (#E;Error error)
+ (#e;Error error)
+ (#e;Error error)
- (#E;Success [context' output])
- (#E;Success output)))
+ (#e;Success [context' output])
+ (#e;Success output)))
(def: (apply-type! t-func t-arg)
(-> Type Type (Check Type))
(function [context]
(case (type;apply (list t-arg) t-func)
#;None
- (#E;Error ($_ text/compose "Invalid type application: " (type;to-text t-func) " on " (type;to-text t-arg)))
+ (#e;Error ($_ text/compose "Invalid type application: " (type;to-text t-func) " on " (type;to-text t-arg)))
(#;Some output)
- (#E;Success [context output]))))
+ (#e;Success [context output]))))
(def: #export existential
{#;doc "A producer of existential types."}
(Check [Nat Type])
(function [context]
(let [id (get@ #;ex-counter context)]
- (#E;Success [(update@ #;ex-counter n.inc context)
+ (#e;Success [(update@ #;ex-counter n.inc context)
[id (#;Ex id)]]))))
+(exception: #export Unknown-Type-Var)
+(exception: #export Unbound-Type-Var)
+(exception: #export Improper-Ring)
+
(def: #export (bound? id)
- (-> Nat (Check Bool))
+ (-> Var (Check Bool))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some _))
- (#E;Success [context true])
+ (#e;Success [context true])
(#;Some #;None)
- (#E;Success [context false])
+ (#e;Success [context false])
#;None
- (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (ex;throw Unknown-Type-Var (nat/encode id)))))
(def: #export (read id)
- (-> Nat (Check Type))
+ (-> Var (Check Type))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some type))
- (#E;Success [context type])
+ (#e;Success [context type])
(#;Some #;None)
- (#E;Error ($_ text/compose "Unbound type-var: " (nat/encode id)))
+ (ex;throw Unbound-Type-Var (nat/encode id))
#;None
- (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (ex;throw Unknown-Type-Var (nat/encode id)))))
-(def: #export (write id type)
- (-> Nat Type (Check Unit))
+(def: #export (write type id)
+ (-> Type Var (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some bound))
- (#E;Error ($_ text/compose "Cannot rebind type-var: " (nat/encode id) " | Current type: " (type;to-text bound)))
+ (#e;Error ($_ text/compose "Cannot re-bind type-var: " (nat/encode id) " | Current type: " (type;to-text bound)))
(#;Some #;None)
- (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
- (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (ex;throw Unknown-Type-Var (nat/encode id)))))
-(def: (update id type)
- (-> Nat Type (Check Unit))
+(def: (update type id)
+ (-> Type Var (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
- (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (ex;throw Unknown-Type-Var (nat/encode id)))))
(def: #export (clear id)
- (-> Nat (Check Unit))
+ (-> Var (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#E;Success [(update@ #;var-bindings (var::put id #;None) context)
+ (#e;Success [(update@ #;var-bindings (var::put id #;None) context)
[]])
#;None
- (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (ex;throw Unknown-Type-Var (nat/encode id)))))
(def: #export (clean t-id type)
- (-> Nat Type (Check Type))
+ (-> Var Type (Check Type))
(case type
(#;Var id)
(if (n.= t-id id)
@@ -232,12 +238,12 @@
[_ (clear id)]
(wrap type))
(do Monad<Check>
- [_ (update id ==type)]
+ [_ (update ==type id)]
(wrap type)))
_
(do Monad<Check>
- [_ (update id ==type)]
+ [_ (update ==type id)]
(wrap type))))
(wrap type))))
@@ -271,34 +277,97 @@
))
(def: #export create
- (Check [Nat Type])
+ (Check [Var Type])
(function [context]
(let [id (get@ #;var-counter context)]
- (#E;Success [(|> context
+ (#e;Success [(|> context
(update@ #;var-counter n.inc)
(update@ #;var-bindings (var::put id #;None)))
[id (#;Var id)]]))))
(def: get-bindings
- (Check (List [Nat (Maybe Type)]))
+ (Check (List [Var (Maybe Type)]))
(function [context]
- (#E;Success [context
+ (#e;Success [context
(get@ #;var-bindings context)])))
(def: (set-bindings value)
- (-> (List [Nat (Maybe Type)]) (Check Unit))
+ (-> (List [Var (Maybe Type)]) (Check Unit))
(function [context]
- (#E;Success [(set@ #;var-bindings value context)
+ (#e;Success [(set@ #;var-bindings value context)
[]])))
-(def: #export (delete id)
- (-> Nat (Check Unit))
+(def: (pre-link id)
+ (-> Var (Check (Maybe Var)))
+ (function [context]
+ (loop [current id]
+ (case (|> context (get@ #;var-bindings) (var::get current))
+ (#;Some (#;Some type))
+ (case type
+ (#;Var post)
+ (if (n.= id post)
+ (#e;Success [context (#;Some current)])
+ (recur post))
+
+ _
+ (if (n.= current id)
+ (#e;Success [context #;None])
+ (ex;throw Improper-Ring (nat/encode id))))
+
+ (#;Some #;None)
+ (#e;Success [context #;None])
+
+ #;None
+ (ex;throw Unknown-Type-Var (nat/encode current))))))
+
+(type: #export Ring (Set Var))
+
+(def: empty-ring Ring (set;new number;Hash<Nat>))
+
+(def: #export (ring id)
+ (-> Var (Check Ring))
+ (function [context]
+ (loop [current id
+ output (set;add id empty-ring)]
+ (case (|> context (get@ #;var-bindings) (var::get current))
+ (#;Some (#;Some type))
+ (case type
+ (#;Var post)
+ (if (n.= id post)
+ (#e;Success [context output])
+ (recur post (set;add post output)))
+
+ _
+ (#e;Success [context empty-ring]))
+
+ (#;Some #;None)
+ (#e;Success [context output])
+
+ #;None
+ (ex;throw Unknown-Type-Var (nat/encode current))))))
+
+(def: (delete' id)
+ (-> Var (Check Unit))
(function [context]
- (#E;Success [(update@ #;var-bindings (var::remove id) context)
+ (#e;Success [(update@ #;var-bindings (var::remove id) context)
[]])))
+(def: #export (delete id)
+ (-> Var (Check Unit))
+ (do Monad<Check>
+ [?link (pre-link id)]
+ (case ?link
+ #;None
+ (delete' id)
+
+ (#;Some pre)
+ (do @
+ [post (read id)
+ _ (update post pre)]
+ (delete' id)))))
+
(def: #export (with k)
- (All [a] (-> (-> [Nat Type] (Check a)) (Check a)))
+ (All [a] (-> (-> [Var Type] (Check a)) (Check a)))
(do Monad<Check>
[[id var] create
output (k [id var])
@@ -316,16 +385,23 @@
(All [a] (-> (Check a) (Check (Maybe a))))
(function [context]
(case (op context)
- (#E;Success [context' output])
- (#E;Success [context' (#;Some output)])
+ (#e;Success [context' output])
+ (#e;Success [context' (#;Some output)])
- (#E;Error _)
- (#E;Success [context #;None]))))
+ (#e;Error _)
+ (#e;Success [context #;None]))))
(def: #export (fail message)
(All [a] (-> Text (Check a)))
(function [context]
- (#E;Error message)))
+ (#e;Error message)))
+
+(def: #export (assert message test)
+ (-> Text Bool (Check Unit))
+ (function [context]
+ (if test
+ (#e;Success [context []])
+ (#e;Error message))))
(def: (fail-check expected actual)
(All [a] (-> Type Type (Check a)))
@@ -337,10 +413,10 @@
(All [a] (-> (Check a) (Check a) (Check a)))
(function [context]
(case (left context)
- (#E;Success [context' output])
- (#E;Success [context' output])
+ (#e;Success [context' output])
+ (#e;Success [context' output])
- (#E;Error _)
+ (#e;Error _)
(right context))))
(def: (assumed? [e a] assumptions)
@@ -357,14 +433,104 @@
(def: (on id type then else)
(All [a]
- (-> Nat Type (Check a) (-> Type (Check a))
+ (-> Var Type (Check a) (-> Type (Check a))
(Check a)))
- (either (do Monad<Check>
- [_ (write id type)]
- then)
- (do Monad<Check>
- [bound (read id)]
- (else bound))))
+ ($_ either
+ (do Monad<Check>
+ [_ (write type id)]
+ then)
+ (do Monad<Check>
+ [ring (ring id)
+ _ (assert "" (n.> +1 (set;size ring)))
+ _ (monad;map @ (update type) (set;to-list ring))]
+ then)
+ (do Monad<Check>
+ [bound (read id)]
+ (else bound))))
+
+(def: (link-2 left right)
+ (-> Var Var (Check Unit))
+ (do Monad<Check>
+ [_ (write (#;Var right) left)]
+ (write (#;Var left) right)))
+
+(def: (link-3 interpose to from)
+ (-> Var Var Var (Check Unit))
+ (do Monad<Check>
+ [_ (update (#;Var interpose) from)]
+ (update (#;Var to) interpose)))
+
+(def: (check-vars check' assumptions idE idA)
+ (-> (-> Type Type Assumptions (Check Assumptions))
+ Assumptions
+ Var Var
+ (Check Assumptions))
+ (if (n.= idE idA)
+ (check/wrap assumptions)
+ (do Monad<Check>
+ [ebound (attempt (read idE))
+ abound (attempt (read idA))]
+ (case [ebound abound]
+ ## Link the 2 variables circularily
+ [#;None #;None]
+ (do @
+ [_ (link-2 idE idA)]
+ (wrap assumptions))
+
+ ## Interpose new variable between 2 existing links
+ [(#;Some etype) #;None]
+ (case etype
+ (#;Var targetE)
+ (do @
+ [_ (link-3 idA targetE idE)]
+ (wrap assumptions))
+
+ _
+ (check' etype (#;Var idA) assumptions))
+
+ ## Interpose new variable between 2 existing links
+ [#;None (#;Some atype)]
+ (case atype
+ (#;Var targetA)
+ (do @
+ [_ (link-3 idE targetA idA)]
+ (wrap assumptions))
+
+ _
+ (check' (#;Var idE) atype assumptions))
+
+ [(#;Some etype) (#;Some atype)]
+ (case [etype atype]
+ [(#;Var targetE) (#;Var targetA)]
+ (do @
+ [ringE (ring idE)
+ ringA (ring idA)]
+ (if (:: set;Eq<Set> = ringE ringA)
+ (wrap assumptions)
+ ## Fuse 2 rings
+ (do @
+ [_ (monad;fold @ (function [interpose to]
+ (do @
+ [_ (link-3 interpose to idE)]
+ (wrap interpose)))
+ targetE
+ (set;to-list ringA))]
+ (wrap assumptions))))
+
+ [(#;Var targetE) _]
+ (do @
+ [ring (ring idE)
+ _ (monad;map @ (update atype) (set;to-list ring))]
+ (wrap assumptions))
+
+ [_ (#;Var targetA)]
+ (do @
+ [ring (ring idA)
+ _ (monad;map @ (update etype) (set;to-list ring))]
+ (wrap assumptions))
+
+ _
+ (check' etype atype assumptions))))))
(def: #export (check' expected actual assumptions)
{#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
@@ -372,34 +538,18 @@
(if (is expected actual)
(check/wrap assumptions)
(case [expected actual]
- [(#;Var e-id) (#;Var a-id)]
- (if (n.= e-id a-id)
- (check/wrap assumptions)
- (do Monad<Check>
- [ebound (attempt (read e-id))
- abound (attempt (read a-id))]
- (case [ebound abound]
- [#;None #;None]
- (do @
- [_ (write e-id actual)]
- (wrap assumptions))
-
- [(#;Some etype) #;None]
- (check' etype actual assumptions)
-
- [#;None (#;Some atype)]
- (check' expected atype assumptions)
-
- [(#;Some etype) (#;Some atype)]
- (check' etype atype assumptions))))
+ [(#;Var idE) (#;Var idA)]
+ (check-vars check' assumptions idE idA)
[(#;Var id) _]
- (on id actual (check/wrap assumptions)
+ (on id actual
+ (check/wrap assumptions)
(function [bound]
(check' bound actual assumptions)))
[_ (#;Var id)]
- (on id expected (check/wrap assumptions)
+ (on id expected
+ (check/wrap assumptions)
(function [bound]
(check' expected bound assumptions)))
@@ -529,13 +679,13 @@
{#;doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bool)
(case (run fresh-context (check expected actual))
- (#E;Error error)
+ (#e;Error error)
false
- (#E;Success _)
+ (#e;Success _)
true))
(def: #export get-context
(Check Type-Context)
(function [context]
- (#E;Success [context context])))
+ (#e;Success [context context])))
diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux
index 5fb207cec..21eed2f72 100644
--- a/stdlib/test/test/lux/meta/type/check.lux
+++ b/stdlib/test/test/lux/meta/type/check.lux
@@ -1,14 +1,17 @@
(;module:
lux
(lux [io]
- (control [monad #+ do Monad])
- (data [text "text/" Monoid<Text> Eq<Text>]
- text/format
+ (control [monad #+ do Monad]
+ [pipe #+ case>])
+ (data [product]
+ [maybe]
[number]
- maybe
- (coll [list]))
+ [text "text/" Monoid<Text> Eq<Text>]
+ text/format
+ (coll [list "list/" Functor<List>]
+ [set]))
["r" math/random]
- (meta [type]
+ (meta [type "type/" Eq<Type>]
["@" type/check]))
lux/test)
@@ -162,7 +165,7 @@
(and (type-checks? (@;with (function [[id var]] (@;check var #;Unit))))
(type-checks? (@;with (function [[id var]] (@;check #;Unit var))))))
- (test "Can't rebind already bound type-vars."
+ (test "Cannot rebind already bound type-vars."
(not (type-checks? (@;with (function [[id var]]
(do @;Monad<Check>
[_ (@;check var #;Unit)]
@@ -180,3 +183,101 @@
[_ (@;check var Bottom)]
(@;check #;Unit var))))))
))
+
+(def: (build-ring num-connections)
+ (-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]]))
+ (do @;Monad<Check>
+ [[head-id head-type] @;create
+ ids+types (monad;seq @ (list;repeat num-connections @;create))
+ [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]]
+ (do @
+ [_ (@;check head-type tail-type)]
+ (wrap [tail-id tail-type])))
+ [head-id head-type]
+ ids+types)]
+ (wrap [[head-id head-type] ids+types [tail-id tail-type]])))
+
+(context: "Rings."
+ (<| (times +100)
+ (do @
+ [num-connections (|> r;nat (:: @ map (n.% +100)))
+ bound (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true))))
+ pick-pcg (r;seq r;nat r;nat)]
+ ($_ seq
+ (test "Can create rings of variables."
+ (type-checks? (do @;Monad<Check>
+ [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
+ #let [ids (list/map product;left ids+types)]
+ headR (@;ring head-id)
+ tailR (@;ring tail-id)]
+ (@;assert ""
+ (let [same-rings? (:: set;Eq<Set> = headR tailR)
+ expected-size? (n.= (n.inc num-connections) (set;size headR))
+ same-vars? (|> (set;to-list headR)
+ (list;sort n.<)
+ (:: (list;Eq<List> number;Eq<Nat>) = (list;sort n.< (#;Cons head-id ids))))]
+ (and same-rings?
+ expected-size?
+ 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)
+ #let [ids (list/map product;left ids+types)]
+ _ (@;check head-type bound)
+ 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))]
+ (@;assert ""
+ (and rings-were-erased?
+ same-types?))))))
+ (test "Can delete variables from rings."
+ (type-checks? (do @;Monad<Check>
+ [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
+ #let [ids (list/map product;left ids+types)
+ all-ids (#;Cons head-id ids)
+ num-all-ids (list;size all-ids)
+ [_ idx] (r;run (r;pcg-32 pick-pcg)
+ (|> r;nat (:: r;Monad<Random> map (n.% num-all-ids))))]
+ #let [pick (maybe;assume (list;nth idx all-ids))]
+ _ (@;delete pick)]
+ (if (n.= +0 num-connections)
+ (wrap [])
+ (do @
+ [ring (@;ring (if (n.= head-id pick)
+ tail-id
+ head-id))
+ #let [without-removal (|> (list (list;take idx all-ids)
+ (list;drop (n.inc idx) all-ids))
+ list;concat
+ (list;sort n.<))]]
+ (let [missing-link? (n.= (n.dec num-all-ids) (set;size ring))
+ ids-match? (|> (set;to-list ring)
+ (list;sort n.<)
+ (:: (list;Eq<List> number;Eq<Nat>) = without-removal))]
+ (@;assert ""
+ (and missing-link?
+ ids-match?)))))
+ )))
+ (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)
+ headRL-pre (@;ring head-idL)
+ headRR-pre (@;ring head-idR)
+ _ (@;check head-typeL head-typeR)
+ headRL-post (@;ring head-idL)
+ headRR-post (@;ring head-idR)]
+ (@;assert ""
+ (let [same-rings? (:: set;Eq<Set> = headRL-post headRR-post)
+ expected-size? (n.= (n.* +2 (n.inc num-connections))
+ (set;size headRL-post))
+ union? (:: set;Eq<Set> = headRL-post (set;union headRL-pre headRR-pre))]
+ (and same-rings?
+ expected-size?
+ union?))))))
+ ))
+ ))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 15:02:15 +0000