From 53ccae1625d46cf57247b9fb1cb9f4c28b0a0ad4 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 15 Nov 2017 22:04:44 -0400 Subject: - Moved "/type" and "/type/check" from "lux/meta" to "lux/lang". --- stdlib/source/lux/concurrency/actor.lux | 28 +- stdlib/source/lux/data/format/json.lux | 4 +- stdlib/source/lux/data/text/format.lux | 4 +- stdlib/source/lux/host.jvm.lux | 4 +- stdlib/source/lux/lang/type.lux | 354 ++++++++++++++++ stdlib/source/lux/lang/type/check.lux | 666 +++++++++++++++++++++++++++++++ stdlib/source/lux/meta/poly.lux | 4 +- stdlib/source/lux/meta/poly/eq.lux | 2 +- stdlib/source/lux/meta/poly/functor.lux | 4 +- stdlib/source/lux/meta/poly/json.lux | 8 +- stdlib/source/lux/meta/type.lux | 354 ---------------- stdlib/source/lux/meta/type/check.lux | 666 ------------------------------- stdlib/source/lux/meta/type/implicit.lux | 4 +- stdlib/source/lux/meta/type/object.lux | 4 +- 14 files changed, 1053 insertions(+), 1053 deletions(-) create mode 100644 stdlib/source/lux/lang/type.lux create mode 100644 stdlib/source/lux/lang/type/check.lux delete mode 100644 stdlib/source/lux/meta/type.lux delete mode 100644 stdlib/source/lux/meta/type/check.lux (limited to 'stdlib/source') diff --git a/stdlib/source/lux/concurrency/actor.lux b/stdlib/source/lux/concurrency/actor.lux index c09cde8bc..fea0ca422 100644 --- a/stdlib/source/lux/concurrency/actor.lux +++ b/stdlib/source/lux/concurrency/actor.lux @@ -5,7 +5,7 @@ ["ex" exception #+ exception:]) [io #- run "io/" Monad] (data text/format - (coll [list "L/" Monoid Monad Fold]) + (coll [list "list/" Monoid Monad Fold]) [product]) [meta #+ with-gensyms Monad] (meta [code] @@ -13,8 +13,8 @@ (syntax ["cs" common] (common ["csr" reader] ["csw" writer])) - [type] - (type opaque))) + (type opaque)) + (lang [type])) (.. ["A" atom] ["P" promise "P/" Monad] ["T" task] @@ -229,7 +229,7 @@ g!behavior (code;local-symbol (behavior-name _name)) g!actor (code;local-symbol _name) g!new (code;local-symbol (new-name _name)) - g!vars (L/map code;local-symbol _vars)]] + g!vars (list/map code;local-symbol _vars)]] (wrap (list (` (type: (~@ (csw;export export)) ((~ g!type) (~@ g!vars)) (~ state-type))) (` (type: (~@ (csw;export export)) ((~ g!actor) (~@ g!vars)) @@ -313,29 +313,29 @@ [actor-name (resolve-actor actor-name) #let [g!type (code;symbol (product;both id state-name actor-name)) g!message (code;local-symbol (get@ #name signature)) - g!actor-vars (L/map code;local-symbol actor-vars) + g!actor-vars (list/map code;local-symbol actor-vars) g!actor (` ((~ (code;symbol actor-name)) (~@ g!actor-vars))) - g!all-vars (|> (get@ #vars signature) (L/map code;local-symbol) (L/compose g!actor-vars)) - g!inputsC (|> (get@ #inputs signature) (L/map (|>. product;left code;local-symbol))) - g!inputsT (|> (get@ #inputs signature) (L/map product;right)) + g!all-vars (|> (get@ #vars signature) (list/map code;local-symbol) (list/compose g!actor-vars)) + g!inputsC (|> (get@ #inputs signature) (list/map (|>. product;left code;local-symbol))) + g!inputsT (|> (get@ #inputs signature) (list/map product;right)) g!state (|> signature (get@ #state) code;local-symbol) g!self (|> signature (get@ #self) code;local-symbol) g!actor-refs (: (List Code) (if (list;empty? actor-vars) (list) (|> actor-vars list;size n.dec - (list;n.range +0) (L/map (|>. code;nat (~) ($) (`)))))) + (list;n.range +0) (list/map (|>. code;nat (~) ($) (`)))))) ref-replacements (|> (if (list;empty? actor-vars) (list) (|> actor-vars list;size n.dec - (list;n.range +0) (L/map (|>. code;nat (~) ($) (`))))) + (list;n.range +0) (list/map (|>. code;nat (~) ($) (`))))) (: (List Code)) (list;zip2 g!all-vars) (: (List [Code Code]))) - g!outputT (L/fold (function [[g!var g!ref] outputT] - (code;replace g!var g!ref outputT)) - (get@ #output signature) - ref-replacements)]] + g!outputT (list/fold (function [[g!var g!ref] outputT] + (code;replace g!var g!ref outputT)) + (get@ #output signature) + ref-replacements)]] (wrap (list (` (def: (~@ (csw;export export)) ((~ g!message) (~@ g!inputsC) (~ g!self)) (~ (|> annotations (with-message actor-name) diff --git a/stdlib/source/lux/data/format/json.lux b/stdlib/source/lux/data/format/json.lux index 899cd652a..8f664d6ea 100644 --- a/stdlib/source/lux/data/format/json.lux +++ b/stdlib/source/lux/data/format/json.lux @@ -20,8 +20,8 @@ [meta #+ Monad with-gensyms] (meta ["s" syntax #+ syntax:] [code] - [poly #+ poly:] - [type]) + [poly #+ poly:]) + (lang [type]) )) (do-template [ ] diff --git a/stdlib/source/lux/data/text/format.lux b/stdlib/source/lux/data/text/format.lux index 323ce1efb..161288d86 100644 --- a/stdlib/source/lux/data/text/format.lux +++ b/stdlib/source/lux/data/text/format.lux @@ -14,8 +14,8 @@ [date]) [meta] (meta [code] - ["s" syntax #+ syntax: Syntax] - [type]))) + ["s" syntax #+ syntax: Syntax]) + (lang [type]))) ## [Syntax] (def: #hidden _compose_ diff --git a/stdlib/source/lux/host.jvm.lux b/stdlib/source/lux/host.jvm.lux index 6c3f18b19..1b77e3016 100644 --- a/stdlib/source/lux/host.jvm.lux +++ b/stdlib/source/lux/host.jvm.lux @@ -13,8 +13,8 @@ [bool "bool/" Codec]) [meta #+ with-gensyms Functor Monad] (meta [code] - ["s" syntax #+ syntax: Syntax] - [type]) + ["s" syntax #+ syntax: Syntax]) + (lang [type]) )) (do-template [ ] diff --git a/stdlib/source/lux/lang/type.lux b/stdlib/source/lux/lang/type.lux new file mode 100644 index 000000000..9d6ed5162 --- /dev/null +++ b/stdlib/source/lux/lang/type.lux @@ -0,0 +1,354 @@ +(;module: {#;doc "Basic functionality for working with types."} + [lux #- function] + (lux (control [eq #+ Eq] + [monad #+ do Monad]) + (data [text "text/" Monoid Eq] + [ident "ident/" Eq] + [number "nat/" Codec] + [maybe] + (coll [list #+ "list/" Monad Monoid Fold])) + (meta [code]) + )) + +## [Utils] +(def: (beta-reduce env type) + (-> (List Type) Type Type) + (case type + (#;Primitive name params) + (#;Primitive name (list/map (beta-reduce env) params)) + + (^template [] + ( left right) + ( (beta-reduce env left) (beta-reduce env right))) + ([#;Sum] [#;Product] + [#;Function] [#;Apply]) + + (^template [] + ( old-env def) + (case old-env + #;Nil + ( env def) + + _ + type)) + ([#;UnivQ] + [#;ExQ]) + + (#;Bound idx) + (maybe;default (error! (text/compose "Unknown type var: " (nat/encode idx))) + (list;nth idx env)) + + _ + type + )) + +## [Structures] +(struct: #export _ (Eq Type) + (def: (= x y) + (case [x y] + [(#;Primitive xname xparams) (#;Primitive yname yparams)] + (and (text/= xname yname) + (n.= (list;size yparams) (list;size xparams)) + (list/fold (;function [[x y] prev] (and prev (= x y))) + true + (list;zip2 xparams yparams))) + + (^template [] + [ ] + true) + ([#;Void] [#;Unit]) + + (^template [] + [( xid) ( yid)] + (n.= yid xid)) + ([#;Var] [#;Ex] [#;Bound]) + + (^or [(#;Function xleft xright) (#;Function yleft yright)] + [(#;Apply xleft xright) (#;Apply yleft yright)]) + (and (= xleft yleft) + (= xright yright)) + + [(#;Named xname xtype) (#;Named yname ytype)] + (and (ident/= xname yname) + (= xtype ytype)) + + (^template [] + [( xL xR) ( yL yR)] + (and (= xL yL) (= xR yR))) + ([#;Sum] [#;Product]) + + (^or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)] + [(#;ExQ xenv xbody) (#;ExQ yenv ybody)]) + (and (n.= (list;size yenv) (list;size xenv)) + (= xbody ybody) + (list/fold (;function [[x y] prev] (and prev (= x y))) + true + (list;zip2 xenv yenv))) + + _ + false + ))) + +## [Values] +(do-template [ ] + [(def: #export ( type) + (-> Type [Nat Type]) + (loop [num-args +0 + type type] + (case type + ( env sub-type) + (recur (n.inc num-args) sub-type) + + _ + [num-args type])))] + + [flatten-univ-q #;UnivQ] + [flatten-ex-q #;ExQ] + ) + +(def: #export (flatten-function type) + (-> Type [(List Type) Type]) + (case type + (#;Function in out') + (let [[ins out] (flatten-function out')] + [(list& in ins) out]) + + _ + [(list) type])) + +(def: #export (flatten-application type) + (-> Type [Type (List Type)]) + (case type + (#;Apply arg func') + (let [[func args] (flatten-application func')] + [func (list/compose args (list arg))]) + + _ + [type (list)])) + +(do-template [ ] + [(def: #export ( type) + (-> Type (List Type)) + (case type + ( left right) + (list& left ( right)) + + _ + (list type)))] + + [flatten-variant #;Sum] + [flatten-tuple #;Product] + ) + +(def: #export (apply params func) + (-> (List Type) Type (Maybe Type)) + (case params + #;Nil + (#;Some func) + + (#;Cons param params') + (case func + (^template [] + ( env body) + (|> body + (beta-reduce (list& func param env)) + (apply params'))) + ([#;UnivQ] [#;ExQ]) + + (#;Apply A F) + (apply (list& A params) F) + + (#;Named name unnamed) + (apply params unnamed) + + _ + #;None))) + +(def: #export (to-ast type) + (-> Type Code) + (case type + (#;Primitive name params) + (` (#;Primitive (~ (code;text name)) + (list (~@ (list/map to-ast params))))) + + (^template [] + + (` )) + ([#;Void] [#;Unit]) + + (^template [] + ( idx) + (` ( (~ (code;nat idx))))) + ([#;Var] [#;Ex] [#;Bound]) + + (^template [] + ( left right) + (` ( (~ (to-ast left)) + (~ (to-ast right))))) + ([#;Function] [#;Apply]) + + (^template [ ] + ( left right) + (` ( (~@ (list/map to-ast ( type)))))) + ([#;Sum | flatten-variant] + [#;Product & flatten-tuple]) + + (#;Named name sub-type) + (code;symbol name) + + (^template [] + ( env body) + (` ( (list (~@ (list/map to-ast env))) + (~ (to-ast body))))) + ([#;UnivQ] [#;ExQ]) + )) + +(def: #export (to-text type) + (-> Type Text) + (case type + (#;Primitive name params) + (case params + #;Nil + ($_ text/compose "(primitive " name ")") + + _ + ($_ text/compose "(primitive " name " " (|> params (list/map to-text) list;reverse (list;interpose " ") (list/fold text/compose "")) ")")) + + #;Void + "Void" + + #;Unit + "Unit" + + (^template [ ] + ( _) + ($_ text/compose + (|> ( type) + (list/map to-text) + list;reverse + (list;interpose " ") + (list/fold text/compose "")) + )) + ([#;Sum "(| " ")" flatten-variant] + [#;Product "[" "]" flatten-tuple]) + + (#;Function input output) + (let [[ins out] (flatten-function type)] + ($_ text/compose "(-> " + (|> ins + (list/map to-text) + list;reverse + (list;interpose " ") + (list/fold text/compose "")) + " " (to-text out) ")")) + + (#;Bound idx) + (nat/encode idx) + + (#;Var id) + ($_ text/compose "⌈v:" (nat/encode id) "⌋") + + (#;Ex id) + ($_ text/compose "⟨e:" (nat/encode id) "⟩") + + (#;Apply param fun) + (let [[type-func type-args] (flatten-application type)] + ($_ text/compose "(" (to-text type-func) " " (|> type-args (list/map to-text) list;reverse (list;interpose " ") (list/fold text/compose "")) ")")) + + (^template [ ] + ( env body) + ($_ text/compose "(" " {" (|> env (list/map to-text) (text;join-with " ")) "} " (to-text body) ")")) + ([#;UnivQ "All"] + [#;ExQ "Ex"]) + + (#;Named [module name] type) + ($_ text/compose module ";" name) + )) + +(def: #export (un-alias type) + (-> Type Type) + (case type + (#;Named _ (#;Named ident type')) + (un-alias (#;Named ident type')) + + _ + type)) + +(def: #export (un-name type) + (-> Type Type) + (case type + (#;Named ident type') + (un-name type') + + _ + type)) + +(do-template [ ] + [(def: #export ( types) + (-> (List Type) Type) + (case types + #;Nil + + + (#;Cons type #;Nil) + type + + (#;Cons type types') + ( type ( types'))))] + + [variant Void #;Sum] + [tuple Unit #;Product] + ) + +(def: #export (function inputs output) + (-> (List Type) Type Type) + (case inputs + #;Nil + output + + (#;Cons input inputs') + (#;Function input (function inputs' output)))) + +(def: #export (application params quant) + (-> (List Type) Type Type) + (case params + #;Nil + quant + + (#;Cons param params') + (application params' (#;Apply param quant)))) + +(do-template [ ] + [(def: #export ( size body) + (-> Nat Type Type) + (case size + +0 body + _ ( (list) ( (n.dec size) body))))] + + [univ-q #;UnivQ] + [ex-q #;ExQ] + ) + +(def: #export (quantified? type) + (-> Type Bool) + (case type + (#;Named [module name] _type) + (quantified? _type) + + (#;Apply A F) + (maybe;default false + (do maybe;Monad + [applied (apply (list A) F)] + (wrap (quantified? applied)))) + + (^or (#;UnivQ _) (#;ExQ _)) + true + + _ + false)) + +(def: #export (array level elem-type) + (-> Nat Type Type) + (case level + +0 elem-type + _ (#;Primitive "#Array" (list (array (n.dec level) elem-type))))) diff --git a/stdlib/source/lux/lang/type/check.lux b/stdlib/source/lux/lang/type/check.lux new file mode 100644 index 000000000..cbf31ac08 --- /dev/null +++ b/stdlib/source/lux/lang/type/check.lux @@ -0,0 +1,666 @@ +(;module: {#;doc "Type-checking functionality."} + lux + (lux (control [functor #+ Functor] + [applicative #+ Applicative] + [monad #+ do Monad] + ["ex" exception #+ exception:]) + (data [text "text/" Monoid Eq] + [number "nat/" Codec] + [maybe] + [product] + (coll [list] + [set #+ Set]) + ["e" error]) + (lang [type "type/" Eq]) + )) + +(exception: #export Unknown-Type-Var) +(exception: #export Unbound-Type-Var) +(exception: #export Improper-Ring) +(exception: #export Invalid-Type-Application) +(exception: #export Cannot-Rebind-Var) +(exception: #export Type-Check-Failed) + +(type: #export Var Nat) + +(type: #export Assumption + {#subsumption [Type Type] + #verdict Bool}) + +(type: #export (Check a) + (-> Type-Context (e;Error [Type-Context a]))) + +(type: #export Type-Vars + (List [Var (Maybe Type)])) + +(struct: #export _ (Functor Check) + (def: (map f fa) + (function [context] + (case (fa context) + (#e;Error error) + (#e;Error error) + + (#e;Success [context' output]) + (#e;Success [context' (f output)]) + )))) + +(struct: #export _ (Applicative Check) + (def: functor Functor) + + (def: (wrap x) + (function [context] + (#e;Success [context x]))) + + (def: (apply ff fa) + (function [context] + (case (ff context) + (#e;Success [context' f]) + (case (fa context') + (#e;Success [context'' a]) + (#e;Success [context'' (f a)]) + + (#e;Error error) + (#e;Error error)) + + (#e;Error error) + (#e;Error error) + ))) + ) + +(struct: #export _ (Monad Check) + (def: applicative Applicative) + + (def: (join ffa) + (function [context] + (case (ffa context) + (#e;Success [context' fa]) + (case (fa context') + (#e;Success [context'' a]) + (#e;Success [context'' a]) + + (#e;Error error) + (#e;Error error)) + + (#e;Error error) + (#e;Error error) + ))) + ) + +(open 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::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) (e;Error a))) + (case (proc context) + (#e;Error error) + (#e;Error error) + + (#e;Success [context' output]) + (#e;Success output))) + +(def: #export (throw exception message) + (All [a] (-> ex;Exception Text (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)] + (#e;Success [(update@ #;ex-counter n.inc context) + [id (#;Ex id)]])))) + +(do-template [ ] + [(def: #export ( id) + (-> Var (Check )) + (function [context] + (case (|> context (get@ #;var-bindings) (var::get id)) + (^or (#;Some (#;Some (#;Var _))) + (#;Some #;None)) + (#e;Success [context ]) + + (#;Some (#;Some bound)) + (#e;Success [context ]) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id)))))] + + [bound? Bool false true] + [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)) + (#e;Success [context bound]) + + (#;Some #;None) + (ex;throw Unbound-Type-Var (nat/encode id)) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id))))) + +(def: #export (write type id) + (-> Type Var (Check Unit)) + (function [context] + (case (|> context (get@ #;var-bindings) (var::get id)) + (#;Some (#;Some bound)) + (ex;throw Cannot-Rebind-Var + ($_ text/compose + " Var: " (nat/encode id) "\n" + " Wanted Type: " (type;to-text type) "\n" + "Current Type: " (type;to-text bound))) + + (#;Some #;None) + (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) + []]) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id))))) + +(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) + []]) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id))))) + +(def: #export var + (Check [Var Type]) + (function [context] + (let [id (get@ #;var-counter context)] + (#e;Success [(|> context + (update@ #;var-counter n.inc) + (update@ #;var-bindings (var::put id #;None))) + [id (#;Var id)]])))) + +(def: get-bindings + (Check (List [Var (Maybe Type)])) + (function [context] + (#e;Success [context + (get@ #;var-bindings context)]))) + +(def: (set-bindings value) + (-> (List [Var (Maybe Type)]) (Check Unit)) + (function [context] + (#e;Success [(set@ #;var-bindings value context) + []]))) + +(def: (apply-type! funcT argT) + (-> Type Type (Check Type)) + (case funcT + (#;Var func-id) + (do Monad + [?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] + (case (type;apply (list argT) funcT) + #;None + (ex;throw Invalid-Type-Application (type;to-text (#;Apply argT funcT))) + + (#;Some output) + (#e;Success [context output]))))) + +(type: #export Ring (Set Var)) + +(def: empty-ring Ring (set;new number;Hash)) + +(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: #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) + (#e;Success [context' output]) + (#e;Success [context' (#;Some output)]) + + (#e;Error _) + (#e;Success [context #;None])))) + +(def: #export (fail message) + (All [a] (-> Text (Check a))) + (function [context] + (#e;Error message))) + +(def: #export (assert message test) + (-> Text Bool (Check Unit)) + (function [context] + (if test + (#e;Success [context []]) + (#e;Error message)))) + +(def: (either left right) + (All [a] (-> (Check a) (Check a) (Check a))) + (function [context] + (case (left context) + (#e;Success [context' output]) + (#e;Success [context' output]) + + (#e;Error _) + (right context)))) + +(def: (assumed? [e a] assumptions) + (-> [Type Type] (List Assumption) (Maybe Bool)) + (:: maybe;Monad 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 (List Assumption) (List Assumption)) + (#;Cons [ea status] assumptions)) + +(def: (on id type then else) + (All [a] + (-> Var Type (Check a) (-> Type (Check a)) + (Check a))) + ($_ either + (do Monad + [_ (write type id)] + then) + (do Monad + [ring (ring id) + _ (assert "" (n.> +1 (set;size ring))) + _ (monad;map @ (update type) (set;to-list ring))] + then) + (do Monad + [?bound (read id)] + (else (maybe;default (#;Var id) ?bound))))) + +(def: (link-2 left right) + (-> Var Var (Check Unit)) + (do Monad + [_ (write (#;Var right) left)] + (write (#;Var left) right))) + +(def: (link-3 interpose to from) + (-> Var Var Var (Check Unit)) + (do Monad + [_ (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 + [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;Eq = 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] (-> (-> Unit Text) (Check a) (Check a))) + (function [context] + (case (check context) + (#e;Error error) + (#e;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 [(#;Ex _) _] [_ (#;Ex _)]) + (do Monad + [assumptions (check' eFT aFT assumptions)] + (check' eAT aAT assumptions)) + + [(#;Var id) _] + (do Monad + [?rFT (read id)] + (case ?rFT + (#;Some rFT) + (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions) + + _ + (do Monad + [assumptions (check' eFT aFT assumptions) + e' (apply-type! aFT eAT) + a' (apply-type! aFT aAT)] + (check' e' a' assumptions)))) + + [_ (#;Var id)] + (do Monad + [?rFT (read id)] + (case ?rFT + (#;Some rFT) + (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions) + + _ + (do Monad + [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 [_] (Type-Check-Failed + ($_ text/compose + "Expected: " (type;to-text expected) "\n\n" + " Actual: " (type;to-text actual)))) + (case [expected actual] + [(#;Var idE) (#;Var idA)] + (check-vars check' assumptions idE idA) + + [(#;Var id) _] + (on id actual + (check/wrap assumptions) + (function [bound] + (check' bound actual assumptions))) + + [_ (#;Var id)] + (on id expected + (check/wrap assumptions) + (function [bound] + (check' expected bound assumptions))) + + (^template [ ] + [(#;Apply A1 ) (#;Apply A2 )] + (check-apply check' assumptions [A1 ] [A2 ])) + ([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 + [expected' (apply-type! F A)] + (check' expected' actual (assume! fx-pair true assumptions))))) + + [_ (#;Apply A F)] + (do Monad + [actual' (apply-type! F A)] + (check' expected actual' assumptions)) + + (^template [ ] + [( _) _] + (do Monad + [[_ paramT] + expected' (apply-type! expected paramT)] + (check' expected' actual assumptions))) + ([#;UnivQ ;;existential] + [#;ExQ ;;var]) + + (^template [ ] + [_ ( _)] + (do Monad + [[_ paramT] + 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 + [assumptions (monad;fold Monad + (function [[e a] assumptions] (check' e a assumptions)) + assumptions + (list;zip2 e-params a-params))] + (check/wrap assumptions)) + (fail "")) + + (^template [ ] + [ ] + (check/wrap assumptions) + + [( eL eR) ( aL aR)] + (do Monad + [assumptions (check' eL aL assumptions)] + (check' eR aR assumptions))) + ([#;Void #;Sum] + [#;Unit #;Product]) + + [(#;Function eI eO) (#;Function aI aO)] + (do Monad + [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 Unit)) + (do Monad + [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 Bool) + (case (run fresh-context (check expected actual)) + (#e;Error error) + false + + (#e;Success _) + true)) + +(def: #export get-context + (Check Type-Context) + (function [context] + (#e;Success [context context]))) + +(def: #export (clean inputT) + (-> Type (Check Type)) + (case inputT + (#;Primitive name paramsT+) + (do Monad + [paramsT+' (monad;map @ clean paramsT+)] + (wrap (#;Primitive name paramsT+'))) + + (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _)) + (:: Monad wrap inputT) + + (^template [] + ( leftT rightT) + (do Monad + [leftT' (clean leftT) + rightT' (clean rightT)] + (wrap ( leftT' rightT')))) + ([#;Sum] [#;Product] [#;Function] [#;Apply]) + + (#;Var id) + (do Monad + [?actualT (read id)] + (case ?actualT + (#;Some actualT) + (clean actualT) + + _ + (wrap inputT))) + + (^template [] + ( envT+ unquantifiedT) + (do Monad + [envT+' (monad;map @ clean envT+)] + (wrap ( envT+' unquantifiedT)))) + ([#;UnivQ] [#;ExQ]) + )) diff --git a/stdlib/source/lux/meta/poly.lux b/stdlib/source/lux/meta/poly.lux index c374e585c..432d9385a 100644 --- a/stdlib/source/lux/meta/poly.lux +++ b/stdlib/source/lux/meta/poly.lux @@ -18,8 +18,8 @@ ["s" syntax #+ syntax: Syntax] (syntax ["cs" common] (common ["csr" reader] - ["csw" writer])) - [type] + ["csw" writer]))) + (lang [type] (type [check])) )) diff --git a/stdlib/source/lux/meta/poly/eq.lux b/stdlib/source/lux/meta/poly/eq.lux index 38386a6c8..a57a9e5de 100644 --- a/stdlib/source/lux/meta/poly/eq.lux +++ b/stdlib/source/lux/meta/poly/eq.lux @@ -24,8 +24,8 @@ [syntax #+ syntax: Syntax] (syntax [common]) [poly #+ poly:] - [type] (type [unit])) + (lang [type]) )) ## [Derivers] diff --git a/stdlib/source/lux/meta/poly/functor.lux b/stdlib/source/lux/meta/poly/functor.lux index 7dc20edaf..0e140e9e4 100644 --- a/stdlib/source/lux/meta/poly/functor.lux +++ b/stdlib/source/lux/meta/poly/functor.lux @@ -11,8 +11,8 @@ (meta [code] [syntax #+ syntax: Syntax] (syntax [common]) - [poly #+ poly:] - [type]) + [poly #+ poly:]) + (lang [type]) )) (poly: #export Functor diff --git a/stdlib/source/lux/meta/poly/json.lux b/stdlib/source/lux/meta/poly/json.lux index 0569d03d5..703bbf109 100644 --- a/stdlib/source/lux/meta/poly/json.lux +++ b/stdlib/source/lux/meta/poly/json.lux @@ -10,7 +10,7 @@ (text ["l" lexer]) [number "frac/" Codec "nat/" Codec] maybe - ["E" error] + ["e" error] [sum] [product] (coll [list "list/" Fold Monad] @@ -24,8 +24,8 @@ (meta ["s" syntax #+ syntax:] [code] [poly #+ poly:] - [type] (type [unit])) + (lang [type]) )) (def: #hidden _map_ @@ -63,7 +63,7 @@ (struct: #hidden _ (Codec JSON Int) (def: encode (|>. int-to-nat (:: Codec encode))) (def: decode - (|>. (:: Codec decode) (:: E;Functor map nat-to-int)))) + (|>. (:: Codec decode) (:: e;Functor map nat-to-int)))) (def: #hidden (nullable writer) {#;doc "Builds a JSON generator for potentially inexistent values."} @@ -78,7 +78,7 @@ (def: encode (|>. unit;out (:: Codec encode))) (def: decode - (|>. (:: Codec decode) (:: E;Functor map (unit;in carrier))))) + (|>. (:: Codec decode) (:: e;Functor map (unit;in carrier))))) (poly: #hidden Codec//encode (with-expansions diff --git a/stdlib/source/lux/meta/type.lux b/stdlib/source/lux/meta/type.lux deleted file mode 100644 index 9d6ed5162..000000000 --- a/stdlib/source/lux/meta/type.lux +++ /dev/null @@ -1,354 +0,0 @@ -(;module: {#;doc "Basic functionality for working with types."} - [lux #- function] - (lux (control [eq #+ Eq] - [monad #+ do Monad]) - (data [text "text/" Monoid Eq] - [ident "ident/" Eq] - [number "nat/" Codec] - [maybe] - (coll [list #+ "list/" Monad Monoid Fold])) - (meta [code]) - )) - -## [Utils] -(def: (beta-reduce env type) - (-> (List Type) Type Type) - (case type - (#;Primitive name params) - (#;Primitive name (list/map (beta-reduce env) params)) - - (^template [] - ( left right) - ( (beta-reduce env left) (beta-reduce env right))) - ([#;Sum] [#;Product] - [#;Function] [#;Apply]) - - (^template [] - ( old-env def) - (case old-env - #;Nil - ( env def) - - _ - type)) - ([#;UnivQ] - [#;ExQ]) - - (#;Bound idx) - (maybe;default (error! (text/compose "Unknown type var: " (nat/encode idx))) - (list;nth idx env)) - - _ - type - )) - -## [Structures] -(struct: #export _ (Eq Type) - (def: (= x y) - (case [x y] - [(#;Primitive xname xparams) (#;Primitive yname yparams)] - (and (text/= xname yname) - (n.= (list;size yparams) (list;size xparams)) - (list/fold (;function [[x y] prev] (and prev (= x y))) - true - (list;zip2 xparams yparams))) - - (^template [] - [ ] - true) - ([#;Void] [#;Unit]) - - (^template [] - [( xid) ( yid)] - (n.= yid xid)) - ([#;Var] [#;Ex] [#;Bound]) - - (^or [(#;Function xleft xright) (#;Function yleft yright)] - [(#;Apply xleft xright) (#;Apply yleft yright)]) - (and (= xleft yleft) - (= xright yright)) - - [(#;Named xname xtype) (#;Named yname ytype)] - (and (ident/= xname yname) - (= xtype ytype)) - - (^template [] - [( xL xR) ( yL yR)] - (and (= xL yL) (= xR yR))) - ([#;Sum] [#;Product]) - - (^or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)] - [(#;ExQ xenv xbody) (#;ExQ yenv ybody)]) - (and (n.= (list;size yenv) (list;size xenv)) - (= xbody ybody) - (list/fold (;function [[x y] prev] (and prev (= x y))) - true - (list;zip2 xenv yenv))) - - _ - false - ))) - -## [Values] -(do-template [ ] - [(def: #export ( type) - (-> Type [Nat Type]) - (loop [num-args +0 - type type] - (case type - ( env sub-type) - (recur (n.inc num-args) sub-type) - - _ - [num-args type])))] - - [flatten-univ-q #;UnivQ] - [flatten-ex-q #;ExQ] - ) - -(def: #export (flatten-function type) - (-> Type [(List Type) Type]) - (case type - (#;Function in out') - (let [[ins out] (flatten-function out')] - [(list& in ins) out]) - - _ - [(list) type])) - -(def: #export (flatten-application type) - (-> Type [Type (List Type)]) - (case type - (#;Apply arg func') - (let [[func args] (flatten-application func')] - [func (list/compose args (list arg))]) - - _ - [type (list)])) - -(do-template [ ] - [(def: #export ( type) - (-> Type (List Type)) - (case type - ( left right) - (list& left ( right)) - - _ - (list type)))] - - [flatten-variant #;Sum] - [flatten-tuple #;Product] - ) - -(def: #export (apply params func) - (-> (List Type) Type (Maybe Type)) - (case params - #;Nil - (#;Some func) - - (#;Cons param params') - (case func - (^template [] - ( env body) - (|> body - (beta-reduce (list& func param env)) - (apply params'))) - ([#;UnivQ] [#;ExQ]) - - (#;Apply A F) - (apply (list& A params) F) - - (#;Named name unnamed) - (apply params unnamed) - - _ - #;None))) - -(def: #export (to-ast type) - (-> Type Code) - (case type - (#;Primitive name params) - (` (#;Primitive (~ (code;text name)) - (list (~@ (list/map to-ast params))))) - - (^template [] - - (` )) - ([#;Void] [#;Unit]) - - (^template [] - ( idx) - (` ( (~ (code;nat idx))))) - ([#;Var] [#;Ex] [#;Bound]) - - (^template [] - ( left right) - (` ( (~ (to-ast left)) - (~ (to-ast right))))) - ([#;Function] [#;Apply]) - - (^template [ ] - ( left right) - (` ( (~@ (list/map to-ast ( type)))))) - ([#;Sum | flatten-variant] - [#;Product & flatten-tuple]) - - (#;Named name sub-type) - (code;symbol name) - - (^template [] - ( env body) - (` ( (list (~@ (list/map to-ast env))) - (~ (to-ast body))))) - ([#;UnivQ] [#;ExQ]) - )) - -(def: #export (to-text type) - (-> Type Text) - (case type - (#;Primitive name params) - (case params - #;Nil - ($_ text/compose "(primitive " name ")") - - _ - ($_ text/compose "(primitive " name " " (|> params (list/map to-text) list;reverse (list;interpose " ") (list/fold text/compose "")) ")")) - - #;Void - "Void" - - #;Unit - "Unit" - - (^template [ ] - ( _) - ($_ text/compose - (|> ( type) - (list/map to-text) - list;reverse - (list;interpose " ") - (list/fold text/compose "")) - )) - ([#;Sum "(| " ")" flatten-variant] - [#;Product "[" "]" flatten-tuple]) - - (#;Function input output) - (let [[ins out] (flatten-function type)] - ($_ text/compose "(-> " - (|> ins - (list/map to-text) - list;reverse - (list;interpose " ") - (list/fold text/compose "")) - " " (to-text out) ")")) - - (#;Bound idx) - (nat/encode idx) - - (#;Var id) - ($_ text/compose "⌈v:" (nat/encode id) "⌋") - - (#;Ex id) - ($_ text/compose "⟨e:" (nat/encode id) "⟩") - - (#;Apply param fun) - (let [[type-func type-args] (flatten-application type)] - ($_ text/compose "(" (to-text type-func) " " (|> type-args (list/map to-text) list;reverse (list;interpose " ") (list/fold text/compose "")) ")")) - - (^template [ ] - ( env body) - ($_ text/compose "(" " {" (|> env (list/map to-text) (text;join-with " ")) "} " (to-text body) ")")) - ([#;UnivQ "All"] - [#;ExQ "Ex"]) - - (#;Named [module name] type) - ($_ text/compose module ";" name) - )) - -(def: #export (un-alias type) - (-> Type Type) - (case type - (#;Named _ (#;Named ident type')) - (un-alias (#;Named ident type')) - - _ - type)) - -(def: #export (un-name type) - (-> Type Type) - (case type - (#;Named ident type') - (un-name type') - - _ - type)) - -(do-template [ ] - [(def: #export ( types) - (-> (List Type) Type) - (case types - #;Nil - - - (#;Cons type #;Nil) - type - - (#;Cons type types') - ( type ( types'))))] - - [variant Void #;Sum] - [tuple Unit #;Product] - ) - -(def: #export (function inputs output) - (-> (List Type) Type Type) - (case inputs - #;Nil - output - - (#;Cons input inputs') - (#;Function input (function inputs' output)))) - -(def: #export (application params quant) - (-> (List Type) Type Type) - (case params - #;Nil - quant - - (#;Cons param params') - (application params' (#;Apply param quant)))) - -(do-template [ ] - [(def: #export ( size body) - (-> Nat Type Type) - (case size - +0 body - _ ( (list) ( (n.dec size) body))))] - - [univ-q #;UnivQ] - [ex-q #;ExQ] - ) - -(def: #export (quantified? type) - (-> Type Bool) - (case type - (#;Named [module name] _type) - (quantified? _type) - - (#;Apply A F) - (maybe;default false - (do maybe;Monad - [applied (apply (list A) F)] - (wrap (quantified? applied)))) - - (^or (#;UnivQ _) (#;ExQ _)) - true - - _ - false)) - -(def: #export (array level elem-type) - (-> Nat Type Type) - (case level - +0 elem-type - _ (#;Primitive "#Array" (list (array (n.dec level) elem-type))))) diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux deleted file mode 100644 index 91e8f3bdf..000000000 --- a/stdlib/source/lux/meta/type/check.lux +++ /dev/null @@ -1,666 +0,0 @@ -(;module: {#;doc "Type-checking functionality."} - lux - (lux (control [functor #+ Functor] - [applicative #+ Applicative] - [monad #+ do Monad] - ["ex" exception #+ exception:]) - (data [text "text/" Monoid Eq] - [number "nat/" Codec] - [maybe] - [product] - (coll [list] - [set #+ Set]) - ["e" error]) - (meta [type "type/" Eq]) - )) - -(exception: #export Unknown-Type-Var) -(exception: #export Unbound-Type-Var) -(exception: #export Improper-Ring) -(exception: #export Invalid-Type-Application) -(exception: #export Cannot-Rebind-Var) -(exception: #export Type-Check-Failed) - -(type: #export Var Nat) - -(type: #export Assumption - {#subsumption [Type Type] - #verdict Bool}) - -(type: #export (Check a) - (-> Type-Context (e;Error [Type-Context a]))) - -(type: #export Type-Vars - (List [Var (Maybe Type)])) - -(struct: #export _ (Functor Check) - (def: (map f fa) - (function [context] - (case (fa context) - (#e;Error error) - (#e;Error error) - - (#e;Success [context' output]) - (#e;Success [context' (f output)]) - )))) - -(struct: #export _ (Applicative Check) - (def: functor Functor) - - (def: (wrap x) - (function [context] - (#e;Success [context x]))) - - (def: (apply ff fa) - (function [context] - (case (ff context) - (#e;Success [context' f]) - (case (fa context') - (#e;Success [context'' a]) - (#e;Success [context'' (f a)]) - - (#e;Error error) - (#e;Error error)) - - (#e;Error error) - (#e;Error error) - ))) - ) - -(struct: #export _ (Monad Check) - (def: applicative Applicative) - - (def: (join ffa) - (function [context] - (case (ffa context) - (#e;Success [context' fa]) - (case (fa context') - (#e;Success [context'' a]) - (#e;Success [context'' a]) - - (#e;Error error) - (#e;Error error)) - - (#e;Error error) - (#e;Error error) - ))) - ) - -(open 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::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) (e;Error a))) - (case (proc context) - (#e;Error error) - (#e;Error error) - - (#e;Success [context' output]) - (#e;Success output))) - -(def: #export (throw exception message) - (All [a] (-> ex;Exception Text (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)] - (#e;Success [(update@ #;ex-counter n.inc context) - [id (#;Ex id)]])))) - -(do-template [ ] - [(def: #export ( id) - (-> Var (Check )) - (function [context] - (case (|> context (get@ #;var-bindings) (var::get id)) - (^or (#;Some (#;Some (#;Var _))) - (#;Some #;None)) - (#e;Success [context ]) - - (#;Some (#;Some bound)) - (#e;Success [context ]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id)))))] - - [bound? Bool false true] - [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)) - (#e;Success [context bound]) - - (#;Some #;None) - (ex;throw Unbound-Type-Var (nat/encode id)) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) - -(def: #export (write type id) - (-> Type Var (Check Unit)) - (function [context] - (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some (#;Some bound)) - (ex;throw Cannot-Rebind-Var - ($_ text/compose - " Var: " (nat/encode id) "\n" - " Wanted Type: " (type;to-text type) "\n" - "Current Type: " (type;to-text bound))) - - (#;Some #;None) - (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) - []]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) - -(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) - []]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) - -(def: #export var - (Check [Var Type]) - (function [context] - (let [id (get@ #;var-counter context)] - (#e;Success [(|> context - (update@ #;var-counter n.inc) - (update@ #;var-bindings (var::put id #;None))) - [id (#;Var id)]])))) - -(def: get-bindings - (Check (List [Var (Maybe Type)])) - (function [context] - (#e;Success [context - (get@ #;var-bindings context)]))) - -(def: (set-bindings value) - (-> (List [Var (Maybe Type)]) (Check Unit)) - (function [context] - (#e;Success [(set@ #;var-bindings value context) - []]))) - -(def: (apply-type! funcT argT) - (-> Type Type (Check Type)) - (case funcT - (#;Var func-id) - (do Monad - [?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] - (case (type;apply (list argT) funcT) - #;None - (ex;throw Invalid-Type-Application (type;to-text (#;Apply argT funcT))) - - (#;Some output) - (#e;Success [context output]))))) - -(type: #export Ring (Set Var)) - -(def: empty-ring Ring (set;new number;Hash)) - -(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: #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) - (#e;Success [context' output]) - (#e;Success [context' (#;Some output)]) - - (#e;Error _) - (#e;Success [context #;None])))) - -(def: #export (fail message) - (All [a] (-> Text (Check a))) - (function [context] - (#e;Error message))) - -(def: #export (assert message test) - (-> Text Bool (Check Unit)) - (function [context] - (if test - (#e;Success [context []]) - (#e;Error message)))) - -(def: (either left right) - (All [a] (-> (Check a) (Check a) (Check a))) - (function [context] - (case (left context) - (#e;Success [context' output]) - (#e;Success [context' output]) - - (#e;Error _) - (right context)))) - -(def: (assumed? [e a] assumptions) - (-> [Type Type] (List Assumption) (Maybe Bool)) - (:: maybe;Monad 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 (List Assumption) (List Assumption)) - (#;Cons [ea status] assumptions)) - -(def: (on id type then else) - (All [a] - (-> Var Type (Check a) (-> Type (Check a)) - (Check a))) - ($_ either - (do Monad - [_ (write type id)] - then) - (do Monad - [ring (ring id) - _ (assert "" (n.> +1 (set;size ring))) - _ (monad;map @ (update type) (set;to-list ring))] - then) - (do Monad - [?bound (read id)] - (else (maybe;default (#;Var id) ?bound))))) - -(def: (link-2 left right) - (-> Var Var (Check Unit)) - (do Monad - [_ (write (#;Var right) left)] - (write (#;Var left) right))) - -(def: (link-3 interpose to from) - (-> Var Var Var (Check Unit)) - (do Monad - [_ (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 - [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;Eq = 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] (-> (-> Unit Text) (Check a) (Check a))) - (function [context] - (case (check context) - (#e;Error error) - (#e;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 [(#;Ex _) _] [_ (#;Ex _)]) - (do Monad - [assumptions (check' eFT aFT assumptions)] - (check' eAT aAT assumptions)) - - [(#;Var id) _] - (do Monad - [?rFT (read id)] - (case ?rFT - (#;Some rFT) - (check' (#;Apply eAT rFT) (#;Apply aAT aFT) assumptions) - - _ - (do Monad - [assumptions (check' eFT aFT assumptions) - e' (apply-type! aFT eAT) - a' (apply-type! aFT aAT)] - (check' e' a' assumptions)))) - - [_ (#;Var id)] - (do Monad - [?rFT (read id)] - (case ?rFT - (#;Some rFT) - (check' (#;Apply eAT eFT) (#;Apply aAT rFT) assumptions) - - _ - (do Monad - [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 [_] (Type-Check-Failed - ($_ text/compose - "Expected: " (type;to-text expected) "\n\n" - " Actual: " (type;to-text actual)))) - (case [expected actual] - [(#;Var idE) (#;Var idA)] - (check-vars check' assumptions idE idA) - - [(#;Var id) _] - (on id actual - (check/wrap assumptions) - (function [bound] - (check' bound actual assumptions))) - - [_ (#;Var id)] - (on id expected - (check/wrap assumptions) - (function [bound] - (check' expected bound assumptions))) - - (^template [ ] - [(#;Apply A1 ) (#;Apply A2 )] - (check-apply check' assumptions [A1 ] [A2 ])) - ([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 - [expected' (apply-type! F A)] - (check' expected' actual (assume! fx-pair true assumptions))))) - - [_ (#;Apply A F)] - (do Monad - [actual' (apply-type! F A)] - (check' expected actual' assumptions)) - - (^template [ ] - [( _) _] - (do Monad - [[_ paramT] - expected' (apply-type! expected paramT)] - (check' expected' actual assumptions))) - ([#;UnivQ ;;existential] - [#;ExQ ;;var]) - - (^template [ ] - [_ ( _)] - (do Monad - [[_ paramT] - 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 - [assumptions (monad;fold Monad - (function [[e a] assumptions] (check' e a assumptions)) - assumptions - (list;zip2 e-params a-params))] - (check/wrap assumptions)) - (fail "")) - - (^template [ ] - [ ] - (check/wrap assumptions) - - [( eL eR) ( aL aR)] - (do Monad - [assumptions (check' eL aL assumptions)] - (check' eR aR assumptions))) - ([#;Void #;Sum] - [#;Unit #;Product]) - - [(#;Function eI eO) (#;Function aI aO)] - (do Monad - [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 Unit)) - (do Monad - [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 Bool) - (case (run fresh-context (check expected actual)) - (#e;Error error) - false - - (#e;Success _) - true)) - -(def: #export get-context - (Check Type-Context) - (function [context] - (#e;Success [context context]))) - -(def: #export (clean inputT) - (-> Type (Check Type)) - (case inputT - (#;Primitive name paramsT+) - (do Monad - [paramsT+' (monad;map @ clean paramsT+)] - (wrap (#;Primitive name paramsT+'))) - - (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _)) - (:: Monad wrap inputT) - - (^template [] - ( leftT rightT) - (do Monad - [leftT' (clean leftT) - rightT' (clean rightT)] - (wrap ( leftT' rightT')))) - ([#;Sum] [#;Product] [#;Function] [#;Apply]) - - (#;Var id) - (do Monad - [?actualT (read id)] - (case ?actualT - (#;Some actualT) - (clean actualT) - - _ - (wrap inputT))) - - (^template [] - ( envT+ unquantifiedT) - (do Monad - [envT+' (monad;map @ clean envT+)] - (wrap ( envT+' unquantifiedT)))) - ([#;UnivQ] [#;ExQ]) - )) diff --git a/stdlib/source/lux/meta/type/implicit.lux b/stdlib/source/lux/meta/type/implicit.lux index a2013d3b1..54fec2626 100644 --- a/stdlib/source/lux/meta/type/implicit.lux +++ b/stdlib/source/lux/meta/type/implicit.lux @@ -13,8 +13,8 @@ [maybe]) [meta #+ Monad] (meta [code] - ["s" syntax #+ syntax: Syntax] - [type] + ["s" syntax #+ syntax: Syntax]) + (lang [type] (type ["tc" check #+ Check Monad])) )) diff --git a/stdlib/source/lux/meta/type/object.lux b/stdlib/source/lux/meta/type/object.lux index 43b563122..0eb354242 100644 --- a/stdlib/source/lux/meta/type/object.lux +++ b/stdlib/source/lux/meta/type/object.lux @@ -14,8 +14,8 @@ ["s" syntax #+ syntax:] (syntax ["cs" common] (common ["csr" reader] - ["csw" writer])) - [type]))) + ["csw" writer]))) + (lang [type]))) ## [Common] (type: Declaration -- cgit v1.2.3