aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/lux/type/check.lux
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/lux/type/check.lux')
-rw-r--r--stdlib/source/lux/type/check.lux683
1 files changed, 683 insertions, 0 deletions
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
new file mode 100644
index 000000000..7e77b0bb6
--- /dev/null
+++ b/stdlib/source/lux/type/check.lux
@@ -0,0 +1,683 @@
+(.module: {#.doc "Type-checking functionality."}
+ [lux #*
+ [control
+ [functor (#+ Functor)]
+ [apply (#+ Apply)]
+ ["." monad (#+ do Monad)]
+ ["ex" exception (#+ exception:)]]
+ [data
+ ["." maybe]
+ ["." product]
+ ["." error (#+ Error)]
+ ["." number ("nat/." Codec<Text,Nat>)]
+ [text ("text/." Monoid<Text> Equivalence<Text>)]
+ [collection
+ ["." list]
+ ["." set (#+ Set)]]]]
+ ["." // ("type/." Equivalence<Type>)])
+
+(exception: #export (unknown-type-var {id Nat})
+ (nat/encode id))
+
+(exception: #export (unbound-type-var {id Nat})
+ (nat/encode id))
+
+(exception: #export (invalid-type-application {funcT Type} {argT Type})
+ (//.to-text (#.Apply argT funcT)))
+
+(exception: #export (cannot-rebind-var {id Nat} {type Type} {bound Type})
+ (ex.report ["Var" (nat/encode id)]
+ ["Wanted Type" (//.to-text type)]
+ ["Current Type" (//.to-text bound)]))
+
+(exception: #export (type-check-failed {expected Type} {actual Type})
+ (ex.report ["Expected" (//.to-text expected)]
+ ["Actual" (//.to-text actual)]))
+
+(type: #export Var Nat)
+
+(type: #export Assumption
+ {#subsumption [Type Type]
+ #verdict Bit})
+
+(type: #export (Check a)
+ (-> Type-Context (Error [Type-Context a])))
+
+(type: #export Type-Vars
+ (List [Var (Maybe Type)]))
+
+(structure: #export _ (Functor Check)
+ (def: (map f fa)
+ (function (_ context)
+ (case (fa context)
+ (#error.Error error)
+ (#error.Error error)
+
+ (#error.Success [context' output])
+ (#error.Success [context' (f output)])
+ ))))
+
+(structure: #export _ (Apply Check)
+ (def: functor Functor<Check>)
+
+ (def: (apply ff fa)
+ (function (_ context)
+ (case (ff context)
+ (#error.Success [context' f])
+ (case (fa context')
+ (#error.Success [context'' a])
+ (#error.Success [context'' (f a)])
+
+ (#error.Error error)
+ (#error.Error error))
+
+ (#error.Error error)
+ (#error.Error error)
+ )))
+ )
+
+(structure: #export _ (Monad Check)
+ (def: functor Functor<Check>)
+
+ (def: (wrap x)
+ (function (_ context)
+ (#error.Success [context x])))
+
+ (def: (join ffa)
+ (function (_ context)
+ (case (ffa context)
+ (#error.Success [context' fa])
+ (case (fa context')
+ (#error.Success [context'' a])
+ (#error.Success [context'' a])
+
+ (#error.Error error)
+ (#error.Error error))
+
+ (#error.Error error)
+ (#error.Error error)
+ )))
+ )
+
+(open: "check/." Monad<Check>)
+
+(def: (var::get id plist)
+ (-> Var Type-Vars (Maybe (Maybe Type)))
+ (case plist
+ #.Nil
+ #.None
+
+ (#.Cons [var-id var-type]
+ plist')
+ (if (n/= id var-id)
+ (#.Some var-type)
+ (var::get id plist'))
+ ))
+
+(def: (var::new id plist)
+ (-> Var Type-Vars Type-Vars)
+ (#.Cons [id #.None] plist))
+
+(def: (var::put id value plist)
+ (-> Var (Maybe Type) Type-Vars Type-Vars)
+ (case plist
+ #.Nil
+ (list [id value])
+
+ (#.Cons [var-id var-type]
+ plist')
+ (if (n/= id var-id)
+ (#.Cons [var-id value]
+ plist')
+ (#.Cons [var-id var-type]
+ (var::put id value plist')))
+ ))
+
+(def: (var::remove id plist)
+ (-> Var Type-Vars Type-Vars)
+ (case plist
+ #.Nil
+ #.Nil
+
+ (#.Cons [var-id var-type]
+ plist')
+ (if (n/= id var-id)
+ plist'
+ (#.Cons [var-id var-type]
+ (var::remove id plist')))
+ ))
+
+## [[Logic]]
+(def: #export (run context proc)
+ (All [a] (-> Type-Context (Check a) (Error a)))
+ (case (proc context)
+ (#error.Error error)
+ (#error.Error error)
+
+ (#error.Success [context' output])
+ (#error.Success output)))
+
+(def: #export (throw exception message)
+ (All [e a] (-> (ex.Exception e) e (Check a)))
+ (function (_ context)
+ (ex.throw exception message)))
+
+(def: #export existential
+ {#.doc "A producer of existential types."}
+ (Check [Nat Type])
+ (function (_ context)
+ (let [id (get@ #.ex-counter context)]
+ (#error.Success [(update@ #.ex-counter inc context)
+ [id (#.Ex 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))
+ (#error.Success [context <fail>])
+
+ (#.Some (#.Some bound))
+ (#error.Success [context <succeed>])
+
+ #.None
+ (ex.throw unknown-type-var id))))]
+
+ [bound? Bit #0 #1]
+ [read (Maybe Type) #.None (#.Some bound)]
+ )
+
+(def: (peek id)
+ (-> Var (Check Type))
+ (function (_ context)
+ (case (|> context (get@ #.var-bindings) (var::get id))
+ (#.Some (#.Some bound))
+ (#error.Success [context bound])
+
+ (#.Some #.None)
+ (ex.throw unbound-type-var id)
+
+ #.None
+ (ex.throw unknown-type-var id))))
+
+(def: #export (bind type id)
+ (-> Type Var (Check Any))
+ (function (_ context)
+ (case (|> context (get@ #.var-bindings) (var::get id))
+ (#.Some (#.Some bound))
+ (ex.throw cannot-rebind-var [id type bound])
+
+ (#.Some #.None)
+ (#error.Success [(update@ #.var-bindings (var::put id (#.Some type)) context)
+ []])
+
+ #.None
+ (ex.throw unknown-type-var id))))
+
+(def: (update type id)
+ (-> Type Var (Check Any))
+ (function (_ context)
+ (case (|> context (get@ #.var-bindings) (var::get id))
+ (#.Some _)
+ (#error.Success [(update@ #.var-bindings (var::put id (#.Some type)) context)
+ []])
+
+ #.None
+ (ex.throw unknown-type-var id))))
+
+(def: #export var
+ (Check [Var Type])
+ (function (_ context)
+ (let [id (get@ #.var-counter context)]
+ (#error.Success [(|> context
+ (update@ #.var-counter inc)
+ (update@ #.var-bindings (var::new id)))
+ [id (#.Var id)]]))))
+
+(def: get-bindings
+ (Check (List [Var (Maybe Type)]))
+ (function (_ context)
+ (#error.Success [context
+ (get@ #.var-bindings context)])))
+
+(def: (set-bindings value)
+ (-> (List [Var (Maybe Type)]) (Check Any))
+ (function (_ context)
+ (#error.Success [(set@ #.var-bindings value context)
+ []])))
+
+(def: (apply-type! funcT argT)
+ (-> Type Type (Check Type))
+ (case funcT
+ (#.Var func-id)
+ (do Monad<Check>
+ [?funcT' (read func-id)]
+ (case ?funcT'
+ #.None
+ (throw invalid-type-application [funcT argT])
+
+ (#.Some funcT')
+ (apply-type! funcT' argT)))
+
+ _
+ (function (_ context)
+ (case (//.apply (list argT) funcT)
+ #.None
+ (ex.throw invalid-type-application [funcT argT])
+
+ (#.Some output)
+ (#error.Success [context output])))))
+
+(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)
+ (#error.Success [context output])
+ (recur post (set.add post output)))
+
+ _
+ (#error.Success [context empty-ring]))
+
+ (#.Some #.None)
+ (#error.Success [context output])
+
+ #.None
+ (ex.throw unknown-type-var current)))))
+
+(def: #export fresh-context
+ Type-Context
+ {#.var-counter +0
+ #.ex-counter +0
+ #.var-bindings (list)
+ })
+
+(def: (attempt op)
+ (All [a] (-> (Check a) (Check (Maybe a))))
+ (function (_ context)
+ (case (op context)
+ (#error.Success [context' output])
+ (#error.Success [context' (#.Some output)])
+
+ (#error.Error _)
+ (#error.Success [context #.None]))))
+
+(def: #export (fail message)
+ (All [a] (-> Text (Check a)))
+ (function (_ context)
+ (#error.Error message)))
+
+(def: #export (assert message test)
+ (-> Text Bit (Check Any))
+ (function (_ context)
+ (if test
+ (#error.Success [context []])
+ (#error.Error message))))
+
+(def: (either left right)
+ (All [a] (-> (Check a) (Check a) (Check a)))
+ (function (_ context)
+ (case (left context)
+ (#error.Success [context' output])
+ (#error.Success [context' output])
+
+ (#error.Error _)
+ (right context))))
+
+(def: (assumed? [e a] assumptions)
+ (-> [Type Type] (List Assumption) (Maybe Bit))
+ (:: 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] Bit (List Assumption) (List Assumption))
+ (#.Cons [ea status] assumptions))
+
+(def: (if-bind id type then else)
+ (All [a]
+ (-> Var Type (Check a) (-> Type (Check a))
+ (Check a)))
+ ($_ either
+ (do Monad<Check>
+ [_ (..bind 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 (maybe.default (#.Var id) ?bound)))))
+
+(def: (link-2 left right)
+ (-> Var Var (Check Any))
+ (do Monad<Check>
+ [_ (..bind (#.Var right) left)]
+ (..bind (#.Var left) right)))
+
+(def: (link-3 interpose to from)
+ (-> Var Var Var (Check Any))
+ (do Monad<Check>
+ [_ (update (#.Var interpose) from)]
+ (update (#.Var to) interpose)))
+
+(def: (check-vars check' assumptions idE idA)
+ (-> (-> Type Type (List Assumption) (Check (List Assumption)))
+ (List Assumption)
+ Var Var
+ (Check (List Assumption)))
+ (if (n/= idE idA)
+ (check/wrap assumptions)
+ (do Monad<Check>
+ [ebound (attempt (peek idE))
+ abound (attempt (peek 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.Equivalence<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: (with-error-stack on-error check)
+ (All [a] (-> (-> Any Text) (Check a) (Check a)))
+ (function (_ context)
+ (case (check context)
+ (#error.Error error)
+ (#error.Error (case error
+ ""
+ (on-error [])
+
+ _
+ ($_ text/compose
+ (on-error [])
+ "\n\n-----------------------------------------\n\n"
+ error)))
+
+ output
+ output)))
+
+(def: (check-apply check' assumptions [eAT eFT] [aAT aFT])
+ (-> (-> Type Type (List Assumption) (Check (List Assumption))) (List Assumption)
+ [Type Type] [Type Type]
+ (Check (List Assumption)))
+ (case [eFT aFT]
+ (^or [(#.UnivQ _ _) (#.Ex _)] [(#.UnivQ _ _) (#.Var _)])
+ (do Monad<Check>
+ [eFT' (apply-type! eFT eAT)]
+ (check' eFT' (#.Apply aAT aFT) assumptions))
+
+ (^or [(#.Ex _) (#.UnivQ _ _)] [(#.Var _) (#.UnivQ _ _)])
+ (do Monad<Check>
+ [aFT' (apply-type! aFT aAT)]
+ (check' (#.Apply eAT eFT) aFT' assumptions))
+
+ (^or [(#.Ex _) _] [_ (#.Ex _)])
+ (do Monad<Check>
+ [assumptions (check' eFT aFT assumptions)]
+ (check' eAT aAT assumptions))
+
+ [(#.Var id) _]
+ (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)]
+ (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 (List Assumption) (Check (List Assumption)))
+ (if (is? expected actual)
+ (check/wrap assumptions)
+ (with-error-stack
+ (function (_ _) (ex.construct type-check-failed [expected actual]))
+ (case [expected actual]
+ [(#.Var idE) (#.Var idA)]
+ (check-vars check' assumptions idE idA)
+
+ [(#.Var id) _]
+ (if-bind id actual
+ (check/wrap assumptions)
+ (function (_ bound)
+ (check' bound actual assumptions)))
+
+ [_ (#.Var id)]
+ (if-bind id expected
+ (check/wrap assumptions)
+ (function (_ bound)
+ (check' expected bound assumptions)))
+
+ (^template [<fe> <fa>]
+ [(#.Apply A1 <fe>) (#.Apply A2 <fa>)]
+ (check-apply check' assumptions [A1 <fe>] [A2 <fa>]))
+ ([F1 (#.Ex ex)]
+ [(#.Ex ex) F2]
+ [F1 (#.Var id)]
+ [(#.Var id) F2])
+
+ [(#.Apply A F) _]
+ (let [fx-pair [expected actual]]
+ (case (assumed? fx-pair assumptions)
+ (#.Some ?)
+ (if ?
+ (check/wrap assumptions)
+ (fail ""))
+
+ #.None
+ (do Monad<Check>
+ [expected' (apply-type! F A)]
+ (check' expected' actual (assume! fx-pair #1 assumptions)))))
+
+ [_ (#.Apply A F)]
+ (do Monad<Check>
+ [actual' (apply-type! F A)]
+ (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)
+ (n/= (list.size e-params)
+ (list.size a-params)))
+ (do Monad<Check>
+ [assumptions (monad.fold Monad<Check>
+ (function (_ [e a] assumptions) (check' e a assumptions))
+ assumptions
+ (list.zip2 e-params a-params))]
+ (check/wrap assumptions))
+ (fail ""))
+
+ (^template [<compose>]
+ [(<compose> eL eR) (<compose> aL aR)]
+ (do Monad<Check>
+ [assumptions (check' eL aL assumptions)]
+ (check' eR aR assumptions)))
+ ([#.Sum]
+ [#.Product])
+
+ [(#.Function eI eO) (#.Function aI aO)]
+ (do Monad<Check>
+ [assumptions (check' aI eI assumptions)]
+ (check' eO aO assumptions))
+
+ [(#.Ex e!id) (#.Ex a!id)]
+ (if (n/= e!id a!id)
+ (check/wrap assumptions)
+ (fail ""))
+
+ [(#.Named _ ?etype) _]
+ (check' ?etype actual assumptions)
+
+ [_ (#.Named _ ?atype)]
+ (check' expected ?atype assumptions)
+
+ _
+ (fail "")))))
+
+(def: #export (check expected actual)
+ {#.doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
+ (-> Type Type (Check Any))
+ (do Monad<Check>
+ [assumptions (check' expected actual (list))]
+ (wrap [])))
+
+(def: #export (checks? expected actual)
+ {#.doc "A simple type-checking function that just returns a yes/no answer."}
+ (-> Type Type Bit)
+ (case (run fresh-context (check expected actual))
+ (#error.Error error)
+ #0
+
+ (#error.Success _)
+ #1))
+
+(def: #export context
+ (Check Type-Context)
+ (function (_ context)
+ (#error.Success [context context])))
+
+(def: #export (clean inputT)
+ (-> Type (Check Type))
+ (case inputT
+ (#.Primitive name paramsT+)
+ (do Monad<Check>
+ [paramsT+' (monad.map @ clean paramsT+)]
+ (wrap (#.Primitive name paramsT+')))
+
+ (^or (#.Parameter _) (#.Ex _) (#.Named _))
+ (:: Monad<Check> wrap inputT)
+
+ (^template [<tag>]
+ (<tag> leftT rightT)
+ (do Monad<Check>
+ [leftT' (clean leftT)
+ rightT' (clean rightT)]
+ (wrap (<tag> leftT' rightT'))))
+ ([#.Sum] [#.Product] [#.Function] [#.Apply])
+
+ (#.Var id)
+ (do Monad<Check>
+ [?actualT (read id)]
+ (case ?actualT
+ (#.Some actualT)
+ (clean actualT)
+
+ _
+ (wrap inputT)))
+
+ (^template [<tag>]
+ (<tag> envT+ unquantifiedT)
+ (do Monad<Check>
+ [envT+' (monad.map @ clean envT+)]
+ (wrap (<tag> envT+' unquantifiedT))))
+ ([#.UnivQ] [#.ExQ])
+ ))
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-18 04:28:12 +0000