From e550029ac3ca8eecade4705020b9cf24312227f5 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sat, 21 Jul 2018 00:49:34 -0400 Subject: Moved "lux/language/type/*" to "lux/type/*". --- stdlib/source/lux/data/collection/set/multi.lux | 4 +- stdlib/source/lux/data/text/format.lux | 3 +- stdlib/source/lux/host.jvm.lux | 8 +- .../source/lux/language/compiler/analysis/case.lux | 69 +-- .../lux/language/compiler/analysis/function.lux | 19 +- .../lux/language/compiler/analysis/inference.lux | 17 +- .../lux/language/compiler/analysis/reference.lux | 3 - .../lux/language/compiler/analysis/structure.lux | 26 +- .../source/lux/language/compiler/analysis/type.lux | 7 +- .../lux/language/compiler/default/repl/type.lux | 5 +- .../compiler/extension/analysis/common.lux | 32 +- .../compiler/extension/analysis/host.jvm.lux | 5 +- .../source/lux/language/compiler/meta/archive.lux | 4 +- stdlib/source/lux/language/type.lux | 391 ------------ stdlib/source/lux/language/type/check.lux | 685 --------------------- stdlib/source/lux/macro/poly.lux | 6 +- stdlib/source/lux/macro/poly/equivalence.lux | 6 +- stdlib/source/lux/macro/poly/functor.lux | 3 +- stdlib/source/lux/macro/poly/json.lux | 6 +- stdlib/source/lux/type.lux | 391 ++++++++++++ stdlib/source/lux/type/abstract.lux | 3 +- stdlib/source/lux/type/check.lux | 683 ++++++++++++++++++++ stdlib/source/lux/type/implicit.lux | 5 +- stdlib/source/lux/type/object/interface.lux | 5 +- stdlib/source/lux/type/quotient.lux | 4 +- stdlib/source/lux/type/refinement.lux | 4 +- 26 files changed, 1181 insertions(+), 1213 deletions(-) delete mode 100644 stdlib/source/lux/language/type.lux delete mode 100644 stdlib/source/lux/language/type/check.lux create mode 100644 stdlib/source/lux/type.lux create mode 100644 stdlib/source/lux/type/check.lux (limited to 'stdlib/source') diff --git a/stdlib/source/lux/data/collection/set/multi.lux b/stdlib/source/lux/data/collection/set/multi.lux index c4d67b8fe..eb8e914e3 100644 --- a/stdlib/source/lux/data/collection/set/multi.lux +++ b/stdlib/source/lux/data/collection/set/multi.lux @@ -5,9 +5,7 @@ [equivalence (#+ Equivalence)] [hash (#+ Hash)]] ["." function] - [language - [type (#+ :share)]] - [type + [type (#+ :share) abstract]] [//// ["." maybe]] diff --git a/stdlib/source/lux/data/text/format.lux b/stdlib/source/lux/data/text/format.lux index acab4c72b..7592b7b28 100644 --- a/stdlib/source/lux/data/text/format.lux +++ b/stdlib/source/lux/data/text/format.lux @@ -22,8 +22,7 @@ ["." macro ["." code] ["s" syntax (#+ syntax: Syntax)]] - [language - ["." type]]]) + ["." type]]) ## [Syntax] (syntax: #export (format {fragments (p.many s.any)}) diff --git a/stdlib/source/lux/host.jvm.lux b/stdlib/source/lux/host.jvm.lux index fe72467bf..a3f8a82c4 100644 --- a/stdlib/source/lux/host.jvm.lux +++ b/stdlib/source/lux/host.jvm.lux @@ -4,8 +4,6 @@ ["." monad (#+ do Monad)] ["." enum] ["p" parser]] - ["." io] - function [data ["." maybe] ["." product] @@ -16,12 +14,12 @@ format] [collection ["." list ("list/." Monad Fold Monoid)]]] + function + ["." type ("type/." Equivalence)] ["." macro (#+ with-gensyms Functor Monad) ["." code] ["s" syntax (#+ syntax: Syntax)]] - [language - ["." type ("type/." Equivalence)]] - ]) + ["." io]]) (do-template [ ] [(def: #export ( value) diff --git a/stdlib/source/lux/language/compiler/analysis/case.lux b/stdlib/source/lux/language/compiler/analysis/case.lux index 09a045e8c..841173629 100644 --- a/stdlib/source/lux/language/compiler/analysis/case.lux +++ b/stdlib/source/lux/language/compiler/analysis/case.lux @@ -11,6 +11,8 @@ format] [collection ["." list ("list/." Fold Monoid Functor)]]] + ["." type + ["." check]] ["." macro ["." code]]] ["." // (#+ Pattern Analysis Operation Compiler) @@ -18,25 +20,22 @@ ["//." type] ["." structure] ["/." // - ["." extension] - [// - ["." type - ["tc" check]]]]] + ["." extension]]] [/ ["." coverage]]) -(exception: #export (cannot-match-type-with-pattern {type Type} {pattern Code}) +(exception: #export (cannot-match-with-pattern {type Type} {pattern Code}) (ex.report ["Type" (%type type)] ["Pattern" (%code pattern)])) -(exception: #export (sum-type-has-no-case {case Nat} {type Type}) +(exception: #export (sum-has-no-case {case Nat} {type Type}) (ex.report ["Case" (%n case)] ["Type" (%type type)])) (exception: #export (unrecognized-pattern-syntax {pattern Code}) (%code pattern)) -(exception: #export (cannot-simplify-type-for-pattern-matching {type Type}) +(exception: #export (cannot-simplify-for-pattern-matching {type Type}) (%type type)) (do-template [] @@ -63,7 +62,7 @@ ## type-variables or quantifications. ## This function makes it easier for "case" analysis to properly ## type-check the input with respect to the patterns. -(def: (simplify-case-type caseT) +(def: (simplify-case caseT) (-> Type (Operation Type)) (loop [envs (: (List (List Type)) (list)) @@ -72,13 +71,13 @@ (#.Var id) (do ///.Monad [?caseT' (//type.with-env - (tc.read id))] + (check.read id))] (.case ?caseT' (#.Some caseT') (recur envs caseT') _ - (///.throw cannot-simplify-type-for-pattern-matching caseT))) + (///.throw cannot-simplify-for-pattern-matching caseT))) (#.Named name unnamedT) (recur envs unnamedT) @@ -89,7 +88,7 @@ (#.ExQ _) (do ///.Monad [[ex-id exT] (//type.with-env - tc.existential)] + check.existential)] (recur envs (maybe.assume (type.apply (list exT) caseT)))) (#.Apply inputT funcT) @@ -97,14 +96,14 @@ (#.Var funcT-id) (do ///.Monad [funcT' (//type.with-env - (do tc.Monad - [?funct' (tc.read funcT-id)] + (do check.Monad + [?funct' (check.read funcT-id)] (.case ?funct' (#.Some funct') (wrap funct') _ - (tc.throw cannot-simplify-type-for-pattern-matching caseT))))] + (check.throw cannot-simplify-for-pattern-matching caseT))))] (recur envs (#.Apply inputT funcT'))) _ @@ -113,7 +112,7 @@ (recur envs outputT) #.None - (///.throw cannot-simplify-type-for-pattern-matching caseT))) + (///.throw cannot-simplify-for-pattern-matching caseT))) (#.Product _) (|> caseT @@ -130,7 +129,7 @@ (//.with-cursor cursor (do ///.Monad [_ (//type.with-env - (tc.check inputT type)) + (check.check inputT type)) outputA next] (wrap [output outputA])))) @@ -178,23 +177,23 @@ [cursor (#.Tuple sub-patterns)] (//.with-cursor cursor (do ///.Monad - [inputT' (simplify-case-type inputT)] + [inputT' (simplify-case inputT)] (.case inputT' (#.Product _) - (let [sub-types (type.flatten-tuple inputT') - num-sub-types (maybe.default (list.size sub-types) - num-tags) + (let [subs (type.flatten-tuple inputT') + num-subs (maybe.default (list.size subs) + num-tags) num-sub-patterns (list.size sub-patterns) - matches (cond (n/< num-sub-types num-sub-patterns) - (let [[prefix suffix] (list.split (dec num-sub-patterns) sub-types)] + matches (cond (n/< num-subs num-sub-patterns) + (let [[prefix suffix] (list.split (dec num-sub-patterns) subs)] (list.zip2 (list/compose prefix (list (type.tuple suffix))) sub-patterns)) - (n/> num-sub-types num-sub-patterns) - (let [[prefix suffix] (list.split (dec num-sub-types) sub-patterns)] - (list.zip2 sub-types (list/compose prefix (list (code.tuple suffix))))) + (n/> num-subs num-sub-patterns) + (let [[prefix suffix] (list.split (dec num-subs) sub-patterns)] + (list.zip2 subs (list/compose prefix (list (code.tuple suffix))))) - ## (n/= num-sub-types num-sub-patterns) - (list.zip2 sub-types sub-patterns))] + ## (n/= num-subs num-sub-patterns) + (list.zip2 subs sub-patterns))] (do @ [[memberP+ thenA] (list/fold (: (All [a] (-> [Type Code] (Operation [(List Pattern) a]) @@ -213,7 +212,7 @@ thenA]))) _ - (///.throw cannot-match-type-with-pattern [inputT pattern]) + (///.throw cannot-match-with-pattern [inputT pattern]) ))) [cursor (#.Record record)] @@ -221,7 +220,7 @@ [record (structure.normalize record) [members recordT] (structure.order record) _ (//type.with-env - (tc.check inputT recordT))] + (check.check inputT recordT))] (analyse-pattern (#.Some (list.size members)) inputT [cursor (#.Tuple members)] next)) [cursor (#.Tag tag)] @@ -231,14 +230,14 @@ (^ [cursor (#.Form (list& [_ (#.Nat idx)] values))]) (//.with-cursor cursor (do ///.Monad - [inputT' (simplify-case-type inputT)] + [inputT' (simplify-case inputT)] (.case inputT' (#.Sum _) (let [flat-sum (type.flatten-variant inputT') size-sum (list.size flat-sum) num-cases (maybe.default size-sum num-tags)] (.case (list.nth idx flat-sum) - (^multi (#.Some case-type) + (^multi (#.Some caseT) (n/< num-cases idx)) (do ///.Monad [[testP nextA] (if (and (n/> num-cases size-sum) @@ -247,15 +246,15 @@ (type.variant (list.drop (dec num-cases) flat-sum)) (` [(~+ values)]) next) - (analyse-pattern #.None case-type (` [(~+ values)]) next))] + (analyse-pattern #.None caseT (` [(~+ values)]) next))] (wrap [(//.sum-pattern num-cases idx testP) nextA])) _ - (///.throw sum-type-has-no-case [idx inputT]))) + (///.throw sum-has-no-case [idx inputT]))) _ - (///.throw cannot-match-type-with-pattern [inputT pattern])))) + (///.throw cannot-match-with-pattern [inputT pattern])))) (^ [cursor (#.Form (list& [_ (#.Tag tag)] values))]) (//.with-cursor cursor @@ -263,7 +262,7 @@ [tag (extension.lift (macro.normalize tag)) [idx group variantT] (extension.lift (macro.resolve-tag tag)) _ (//type.with-env - (tc.check inputT variantT))] + (check.check inputT variantT))] (analyse-pattern (#.Some (list.size group)) inputT (` ((~ (code.nat idx)) (~+ values))) next))) _ diff --git a/stdlib/source/lux/language/compiler/analysis/function.lux b/stdlib/source/lux/language/compiler/analysis/function.lux index cc431f9b6..d12880afa 100644 --- a/stdlib/source/lux/language/compiler/analysis/function.lux +++ b/stdlib/source/lux/language/compiler/analysis/function.lux @@ -9,10 +9,9 @@ format] [collection ["." list ("list/." Fold Monoid Monad)]]] - ["." macro] - [language - ["." type - ["tc" check]]]] + ["." type + ["." check]] + ["." macro]] ["." // (#+ Analysis Operation Compiler) ["." scope] ["//." type] @@ -57,13 +56,13 @@ (do @ [[_ instanceT] (//type.with-env )] (recur (maybe.assume (type.apply (list instanceT) expectedT))))) - ([#.UnivQ tc.existential] - [#.ExQ tc.var]) + ([#.UnivQ check.existential] + [#.ExQ check.var]) (#.Var id) (do @ [?expectedT' (//type.with-env - (tc.read id))] + (check.read id))] (case ?expectedT' (#.Some expectedT') (recur expectedT') @@ -71,12 +70,12 @@ ## Inference _ (do @ - [[input-id inputT] (//type.with-env tc.var) - [output-id outputT] (//type.with-env tc.var) + [[input-id inputT] (//type.with-env check.var) + [output-id outputT] (//type.with-env check.var) #let [functionT (#.Function inputT outputT)] functionA (recur functionT) _ (//type.with-env - (tc.check expectedT functionT))] + (check.check expectedT functionT))] (wrap functionA)) )) diff --git a/stdlib/source/lux/language/compiler/analysis/inference.lux b/stdlib/source/lux/language/compiler/analysis/inference.lux index e068f073a..160978d39 100644 --- a/stdlib/source/lux/language/compiler/analysis/inference.lux +++ b/stdlib/source/lux/language/compiler/analysis/inference.lux @@ -9,10 +9,9 @@ format] [collection ["." list ("list/." Functor)]]] - ["." macro]] - [//// ["." type - ["tc" check]]] + ["." check]] + ["." macro]] ["." /// ("operation/." Monad) ["." extension]] [// (#+ Tag Analysis Operation Compiler)] @@ -87,7 +86,7 @@ (Operation Type) (do ///.Monad [cursor (extension.lift macro.cursor) - [ex-id _] (//type.with-env tc.existential)] + [ex-id _] (//type.with-env check.existential)] (wrap (named-type cursor ex-id)))) ## Type-inference works by applying some (potentially quantified) type @@ -112,23 +111,23 @@ (#.UnivQ _) (do ///.Monad - [[var-id varT] (//type.with-env tc.var)] + [[var-id varT] (//type.with-env check.var)] (general analyse (maybe.assume (type.apply (list varT) inferT)) args)) (#.ExQ _) (do ///.Monad - [[var-id varT] (//type.with-env tc.var) + [[var-id varT] (//type.with-env check.var) output (general analyse (maybe.assume (type.apply (list varT) inferT)) args) bound? (//type.with-env - (tc.bound? var-id)) + (check.bound? var-id)) _ (if bound? (wrap []) (do @ [newT new-named-type] (//type.with-env - (tc.check varT newT))))] + (check.check varT newT))))] (wrap output)) (#.Apply inputT transT) @@ -156,7 +155,7 @@ (#.Var infer-id) (do ///.Monad - [?inferT' (//type.with-env (tc.read infer-id))] + [?inferT' (//type.with-env (check.read infer-id))] (case ?inferT' (#.Some inferT') (general analyse inferT' args) diff --git a/stdlib/source/lux/language/compiler/analysis/reference.lux b/stdlib/source/lux/language/compiler/analysis/reference.lux index 4fdbde5c2..bb78a32fb 100644 --- a/stdlib/source/lux/language/compiler/analysis/reference.lux +++ b/stdlib/source/lux/language/compiler/analysis/reference.lux @@ -4,9 +4,6 @@ monad ["ex" exception (#+ exception:)]] ["." macro] - [language - [type - ["tc" check]]] [data [text ("text/." Equivalence) format]]] diff --git a/stdlib/source/lux/language/compiler/analysis/structure.lux b/stdlib/source/lux/language/compiler/analysis/structure.lux index 77a0487c5..b2eb5dc17 100644 --- a/stdlib/source/lux/language/compiler/analysis/structure.lux +++ b/stdlib/source/lux/language/compiler/analysis/structure.lux @@ -13,6 +13,8 @@ [collection ["." list ("list/." Functor)] ["dict" dictionary (#+ Dictionary)]]] + ["." type + ["." check]] ["." macro ["." code]]] ["." // (#+ Tag Analysis Operation Compiler) @@ -21,9 +23,7 @@ ["." inference] ["/." // ["." extension] - ["//." // - ["." type - ["tc" check]]]]]) + ["//." //]]]) (exception: #export (invalid-variant-type {type Type} {tag Tag} {code Code}) (ex.report ["Type" (%type type)] @@ -105,7 +105,7 @@ (#.Var id) (do @ [?expectedT' (//type.with-env - (tc.read id))] + (check.read id))] (case ?expectedT' (#.Some expectedT') (//type.with-type expectedT' @@ -124,14 +124,14 @@ [[instance-id instanceT] (//type.with-env )] (//type.with-type (maybe.assume (type.apply (list instanceT) expectedT)) (sum analyse tag valueC)))) - ([#.UnivQ tc.existential] - [#.ExQ tc.var]) + ([#.UnivQ check.existential] + [#.ExQ check.var]) (#.Apply inputT funT) (case funT (#.Var funT-id) (do @ - [?funT' (//type.with-env (tc.read funT-id))] + [?funT' (//type.with-env (check.read funT-id))] (case ?funT' (#.Some funT') (//type.with-type (#.Apply inputT funT') @@ -207,7 +207,7 @@ (#.Var id) (do @ [?expectedT' (//type.with-env - (tc.read id))] + (check.read id))] (case ?expectedT' (#.Some expectedT') (//type.with-type expectedT' @@ -219,8 +219,8 @@ [membersTA (monad.map @ (|>> analyse //type.with-inference) membersC) _ (//type.with-env - (tc.check expectedT - (type.tuple (list/map product.left membersTA))))] + (check.check expectedT + (type.tuple (list/map product.left membersTA))))] (wrap (//.product-analysis (list/map product.right membersTA)))))) (^template [ ] @@ -229,14 +229,14 @@ [[instance-id instanceT] (//type.with-env )] (//type.with-type (maybe.assume (type.apply (list instanceT) expectedT)) (product analyse membersC)))) - ([#.UnivQ tc.existential] - [#.ExQ tc.var]) + ([#.UnivQ check.existential] + [#.ExQ check.var]) (#.Apply inputT funT) (case funT (#.Var funT-id) (do @ - [?funT' (//type.with-env (tc.read funT-id))] + [?funT' (//type.with-env (check.read funT-id))] (case ?funT' (#.Some funT') (//type.with-type (#.Apply inputT funT') diff --git a/stdlib/source/lux/language/compiler/analysis/type.lux b/stdlib/source/lux/language/compiler/analysis/type.lux index 8bc0bd53b..3eb574986 100644 --- a/stdlib/source/lux/language/compiler/analysis/type.lux +++ b/stdlib/source/lux/language/compiler/analysis/type.lux @@ -5,10 +5,9 @@ [data ["." error]] ["." function] - ["." macro] - [language - [type - ["tc" check]]]] + [type + ["tc" check]] + ["." macro]] [// (#+ Operation) ["/." // ["." extension]]]) diff --git a/stdlib/source/lux/language/compiler/default/repl/type.lux b/stdlib/source/lux/language/compiler/default/repl/type.lux index 4b2b8dc02..635624e67 100644 --- a/stdlib/source/lux/language/compiler/default/repl/type.lux +++ b/stdlib/source/lux/language/compiler/default/repl/type.lux @@ -19,11 +19,10 @@ [duration (#+ Duration)] [date (#+ Date)]] ["." function] + ["." type] ["." macro ["." code] - ["." poly (#+ Poly)]] - [language - ["." type]]]) + ["." poly (#+ Poly)]]]) (exception: #export (cannot-represent-value {type Type}) (ex.report ["Type" (%type type)])) diff --git a/stdlib/source/lux/language/compiler/extension/analysis/common.lux b/stdlib/source/lux/language/compiler/extension/analysis/common.lux index 7f3c4d947..201616ac9 100644 --- a/stdlib/source/lux/language/compiler/extension/analysis/common.lux +++ b/stdlib/source/lux/language/compiler/extension/analysis/common.lux @@ -13,9 +13,9 @@ ["." list ("list/." Functor)] ["." array] ["dict" dictionary (#+ Dictionary)]]] - ["." language - [type - ["tc" check]]] + [type + ["." check]] + ["." language] [io (#+ IO)]] ["." //// ["." analysis (#+ Analysis Handler Bundle) @@ -64,7 +64,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((binary varT varT Bit extension-name) analyse args)))) @@ -76,7 +76,7 @@ (case args (^ (list opC)) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var) + [[var-id varT] (typeA.with-env check.var) _ (typeA.infer (type (Either Text varT))) opA (typeA.with-type (type (IO varT)) (analyse opC))] @@ -210,7 +210,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((binary (type (Array varT)) Nat (type (Maybe varT)) extension-name) analyse args)))) @@ -218,7 +218,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((trinary (type (Array varT)) Nat varT (type (Array varT)) extension-name) analyse args)))) @@ -226,7 +226,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((binary (type (Array varT)) Nat (type (Array varT)) extension-name) analyse args)))) @@ -269,7 +269,7 @@ (case args (^ (list initC)) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var) + [[var-id varT] (typeA.with-env check.var) _ (typeA.infer (type (Atom varT))) initA (typeA.with-type varT (analyse initC))] @@ -282,7 +282,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((unary (type (Atom varT)) varT extension-name) analyse args)))) @@ -290,7 +290,7 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var)] + [[var-id varT] (typeA.with-env check.var)] ((trinary (type (Atom varT)) varT varT Bit extension-name) analyse args)))) @@ -309,7 +309,7 @@ (case args (^ (list initC)) (do ////.Monad - [[var-id varT] (typeA.with-env tc.var) + [[var-id varT] (typeA.with-env check.var) _ (typeA.infer (type (All [!] (Box ! varT)))) initA (typeA.with-type varT (analyse initC))] @@ -322,8 +322,8 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[thread-id threadT] (typeA.with-env tc.var) - [var-id varT] (typeA.with-env tc.var)] + [[thread-id threadT] (typeA.with-env check.var) + [var-id varT] (typeA.with-env check.var)] ((unary (type (Box threadT varT)) varT extension-name) analyse args)))) @@ -331,8 +331,8 @@ Handler (function (_ extension-name analyse args) (do ////.Monad - [[thread-id threadT] (typeA.with-env tc.var) - [var-id varT] (typeA.with-env tc.var)] + [[thread-id threadT] (typeA.with-env check.var) + [var-id varT] (typeA.with-env check.var)] ((binary varT (type (Box threadT varT)) Any extension-name) analyse args)))) diff --git a/stdlib/source/lux/language/compiler/extension/analysis/host.jvm.lux b/stdlib/source/lux/language/compiler/extension/analysis/host.jvm.lux index 24d3948b0..0edd20d2b 100644 --- a/stdlib/source/lux/language/compiler/extension/analysis/host.jvm.lux +++ b/stdlib/source/lux/language/compiler/extension/analysis/host.jvm.lux @@ -15,11 +15,10 @@ ["." list ("list/." Fold Functor Monoid)] ["." array] ["." dictionary (#+ Dictionary)]]] + ["." type + ["." check]] ["." macro ["s" syntax]] - [language - ["." type - ["." check]]] ["." host]] [// ["." common] diff --git a/stdlib/source/lux/language/compiler/meta/archive.lux b/stdlib/source/lux/language/compiler/meta/archive.lux index 570221385..9feaf523f 100644 --- a/stdlib/source/lux/language/compiler/meta/archive.lux +++ b/stdlib/source/lux/language/compiler/meta/archive.lux @@ -11,9 +11,7 @@ format] [collection ["dict" dictionary (#+ Dictionary)]]] - [language - [type (#+ :share)]] - [type + [type (#+ :share) abstract] [world [file (#+ File)]]] diff --git a/stdlib/source/lux/language/type.lux b/stdlib/source/lux/language/type.lux deleted file mode 100644 index 9d774198d..000000000 --- a/stdlib/source/lux/language/type.lux +++ /dev/null @@ -1,391 +0,0 @@ -(.module: {#.doc "Basic functionality for working with types."} - [lux (#- function) - [control - [equivalence (#+ Equivalence)] - [monad (#+ do Monad)] - ["p" parser]] - [data - ["." text ("text/." Monoid Equivalence)] - [ident ("ident/." Equivalence Codec)] - [number ("nat/." Codec)] - ["." maybe] - [collection - ["." list ("list/." Functor Monoid Fold)]]] - ["." macro - ["." code] - ["s" syntax (#+ Syntax syntax:)]]]) - -## [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) - - _ - ( (list/map (beta-reduce env) old-env) def))) - ([#.UnivQ] - [#.ExQ]) - - (#.Parameter idx) - (maybe.default (error! (text/compose "Unknown type var: " (nat/encode idx))) - (list.nth idx env)) - - _ - type - )) - -## [Structures] -(structure: #export _ (Equivalence 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))) - #1 - (list.zip2 xparams yparams))) - - (^template [] - [( xid) ( yid)] - (n/= yid xid)) - ([#.Var] [#.Ex] [#.Parameter]) - - (^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))) - #1 - (list.zip2 xenv yenv))) - - _ - #0 - ))) - -## [Values] -(do-template [ ] - [(def: #export ( type) - (-> Type [Nat Type]) - (loop [num-args +0 - type type] - (case type - ( env sub-type) - (recur (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-code type) - (-> Type Code) - (case type - (#.Primitive name params) - (` (#.Primitive (~ (code.text name)) - (.list (~+ (list/map to-code params))))) - - (^template [] - ( idx) - (` ( (~ (code.nat idx))))) - ([#.Var] [#.Ex] [#.Parameter]) - - (^template [] - ( left right) - (` ( (~ (to-code left)) - (~ (to-code right))))) - ([#.Sum] [#.Product] [#.Function] [#.Apply]) - - (#.Named name sub-type) - (code.symbol name) - - (^template [] - ( env body) - (` ( (.list (~+ (list/map to-code env))) - (~ (to-code 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 "")) ")")) - - (^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) ")")) - - (#.Parameter 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 Nothing #.Sum] - [tuple Any #.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 - _ (|> body ( (dec size)) ( (list)))))] - - [univ-q #.UnivQ] - [ex-q #.ExQ] - ) - -(def: #export (quantified? type) - (-> Type Bit) - (case type - (#.Named [module name] _type) - (quantified? _type) - - (#.Apply A F) - (maybe.default #0 - (do maybe.Monad - [applied (apply (list A) F)] - (wrap (quantified? applied)))) - - (^or (#.UnivQ _) (#.ExQ _)) - #1 - - _ - #0)) - -(def: #export (array level elem-type) - (-> Nat Type Type) - (case level - +0 elem-type - _ (|> elem-type (array (dec level)) (list) (#.Primitive "#Array")))) - -(syntax: #export (:log! {input (p.alt s.symbol - s.any)}) - (case input - (#.Left valueN) - (do @ - [cursor macro.cursor - valueT (macro.find-type valueN) - #let [_ (log! ($_ text/compose - ":log!" " @ " (.cursor-description cursor) "\n" - (ident/encode valueN) " : " (..to-text valueT) "\n"))]] - (wrap (list (' [])))) - - (#.Right valueC) - (macro.with-gensyms [g!value] - (wrap (list (` (.let [(~ g!value) (~ valueC)] - (..:log! (~ g!value))))))))) - -(def: type-parameters - (Syntax (List Text)) - (s.tuple (p.some s.local-symbol))) - -(syntax: #export (:cast {type-vars type-parameters} - input - output - {value (p.maybe s.any)}) - (let [casterC (` (: (All [(~+ (list/map code.local-symbol type-vars))] - (-> (~ input) (~ output))) - (|>> :assume)))] - (case value - #.None - (wrap (list casterC)) - - (#.Some value) - (wrap (list (` ((~ casterC) (~ value)))))))) - -(type: Typed - {#type Code - #expression Code}) - -(def: typed - (Syntax Typed) - (s.record (p.seq s.any s.any))) - -(syntax: #export (:share {type-vars type-parameters} - {exemplar typed} - {computation typed}) - (macro.with-gensyms [g!_] - (let [shareC (` (: (All [(~+ (list/map code.local-symbol type-vars))] - (-> (~ (get@ #type exemplar)) - (~ (get@ #type computation)))) - (.function ((~ g!_) (~ g!_)) - (:assume (~ (get@ #expression computation))))))] - (wrap (list (` ((~ shareC) (~ (get@ #expression exemplar))))))))) diff --git a/stdlib/source/lux/language/type/check.lux b/stdlib/source/lux/language/type/check.lux deleted file mode 100644 index 3f9812d0b..000000000 --- a/stdlib/source/lux/language/type/check.lux +++ /dev/null @@ -1,685 +0,0 @@ -(.module: {#.doc "Type-checking functionality."} - [lux #* - [control - [functor (#+ Functor)] - [apply (#+ Apply)] - ["." monad (#+ do Monad)] - ["ex" exception (#+ exception:)]] - [data - ["." maybe] - ["." product] - ["e" error] - ["." number ("nat/." Codec)] - [text ("text/." Monoid Equivalence)] - [collection - ["." list] - ["." set (#+ Set)]]] - [language - ["." type ("type/." Equivalence)]] - ]) - -(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}) - (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" (type.to-text type)] - ["Current Type" (type.to-text bound)])) - -(exception: #export (type-check-failed {expected Type} {actual Type}) - (ex.report ["Expected" (type.to-text expected)] - ["Actual" (type.to-text actual)])) - -(type: #export Var Nat) - -(type: #export Assumption - {#subsumption [Type Type] - #verdict Bit}) - -(type: #export (Check a) - (-> Type-Context (e.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) - (#e.Error error) - (#e.Error error) - - (#e.Success [context' output]) - (#e.Success [context' (f output)]) - )))) - -(structure: #export _ (Apply Check) - (def: functor Functor) - - (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) - ))) - ) - -(structure: #export _ (Monad Check) - (def: functor Functor) - - (def: (wrap x) - (function (_ context) - (#e.Success [context x]))) - - (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: "check/." Monad) - -(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) (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 [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)] - (#e.Success [(update@ #.ex-counter 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 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)) - (#e.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) - (#e.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 _) - (#e.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)] - (#e.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) - (#e.Success [context - (get@ #.var-bindings context)]))) - -(def: (set-bindings value) - (-> (List [Var (Maybe Type)]) (Check Any)) - (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 [funcT argT]) - - (#.Some funcT') - (apply-type! funcT' argT))) - - _ - (function (_ context) - (case (type.apply (list argT) funcT) - #.None - (ex.throw invalid-type-application [funcT argT]) - - (#.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 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 Bit (Check Any)) - (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 Bit)) - (:: 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] 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 - [_ (..bind 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 Any)) - (do Monad - [_ (..bind (#.Var right) left)] - (..bind (#.Var left) right))) - -(def: (link-3 interpose to from) - (-> Var Var Var (Check Any)) - (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.Equivalence = 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) - (#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 [(#.UnivQ _ _) (#.Ex _)] [(#.UnivQ _ _) (#.Var _)]) - (do Monad - [eFT' (apply-type! eFT eAT)] - (check' eFT' (#.Apply aAT aFT) assumptions)) - - (^or [(#.Ex _) (#.UnivQ _ _)] [(#.Var _) (#.UnivQ _ _)]) - (do Monad - [aFT' (apply-type! aFT aAT)] - (check' (#.Apply eAT eFT) aFT' assumptions)) - - (^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 (_ _) (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 [ ] - [(#.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 #1 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 [] - [( eL eR) ( aL aR)] - (do Monad - [assumptions (check' eL aL assumptions)] - (check' eR aR assumptions))) - ([#.Sum] - [#.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 Any)) - (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 Bit) - (case (run fresh-context (check expected actual)) - (#e.Error error) - #0 - - (#e.Success _) - #1)) - -(def: #export 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 (#.Parameter _) (#.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/macro/poly.lux b/stdlib/source/lux/macro/poly.lux index 96d806c81..964f857a1 100644 --- a/stdlib/source/lux/macro/poly.lux +++ b/stdlib/source/lux/macro/poly.lux @@ -25,10 +25,8 @@ [common ["csr" reader] ["csw" writer]]]] - [language - ["." type ("type/." Equivalence) - ["." check]]] - ]) + ["." type ("type/." Equivalence) + ["." check]]]) (type: #export Env (Dictionary Nat [Type Code])) diff --git a/stdlib/source/lux/macro/poly/equivalence.lux b/stdlib/source/lux/macro/poly/equivalence.lux index 1dd8757e4..ae910874c 100644 --- a/stdlib/source/lux/macro/poly/equivalence.lux +++ b/stdlib/source/lux/macro/poly/equivalence.lux @@ -29,10 +29,8 @@ [syntax (#+ syntax: Syntax) ["." common]] ["." poly (#+ poly:)]] - [type - ["." unit]] - [language - ["." type]]]) + ["." type + ["." unit]]]) ## [Derivers] (poly: #export Equivalence diff --git a/stdlib/source/lux/macro/poly/functor.lux b/stdlib/source/lux/macro/poly/functor.lux index 45cf169f7..90a2ecde0 100644 --- a/stdlib/source/lux/macro/poly/functor.lux +++ b/stdlib/source/lux/macro/poly/functor.lux @@ -15,8 +15,7 @@ [syntax (#+ syntax: Syntax) ["." common]] ["." poly (#+ poly:)]] - [language - ["." type]]]) + ["." type]]) (poly: #export Functor (do @ diff --git a/stdlib/source/lux/macro/poly/json.lux b/stdlib/source/lux/macro/poly/json.lux index 66014ae56..596d24b18 100644 --- a/stdlib/source/lux/macro/poly/json.lux +++ b/stdlib/source/lux/macro/poly/json.lux @@ -30,10 +30,8 @@ ["s" syntax (#+ syntax:)] ["." code] ["." poly (#+ poly:)]] - [type - ["." unit]] - [language - ["." type]]]) + ["." type + ["." unit]]]) (def: tag (-> Nat Frac) diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux new file mode 100644 index 000000000..9d774198d --- /dev/null +++ b/stdlib/source/lux/type.lux @@ -0,0 +1,391 @@ +(.module: {#.doc "Basic functionality for working with types."} + [lux (#- function) + [control + [equivalence (#+ Equivalence)] + [monad (#+ do Monad)] + ["p" parser]] + [data + ["." text ("text/." Monoid Equivalence)] + [ident ("ident/." Equivalence Codec)] + [number ("nat/." Codec)] + ["." maybe] + [collection + ["." list ("list/." Functor Monoid Fold)]]] + ["." macro + ["." code] + ["s" syntax (#+ Syntax syntax:)]]]) + +## [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) + + _ + ( (list/map (beta-reduce env) old-env) def))) + ([#.UnivQ] + [#.ExQ]) + + (#.Parameter idx) + (maybe.default (error! (text/compose "Unknown type var: " (nat/encode idx))) + (list.nth idx env)) + + _ + type + )) + +## [Structures] +(structure: #export _ (Equivalence 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))) + #1 + (list.zip2 xparams yparams))) + + (^template [] + [( xid) ( yid)] + (n/= yid xid)) + ([#.Var] [#.Ex] [#.Parameter]) + + (^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))) + #1 + (list.zip2 xenv yenv))) + + _ + #0 + ))) + +## [Values] +(do-template [ ] + [(def: #export ( type) + (-> Type [Nat Type]) + (loop [num-args +0 + type type] + (case type + ( env sub-type) + (recur (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-code type) + (-> Type Code) + (case type + (#.Primitive name params) + (` (#.Primitive (~ (code.text name)) + (.list (~+ (list/map to-code params))))) + + (^template [] + ( idx) + (` ( (~ (code.nat idx))))) + ([#.Var] [#.Ex] [#.Parameter]) + + (^template [] + ( left right) + (` ( (~ (to-code left)) + (~ (to-code right))))) + ([#.Sum] [#.Product] [#.Function] [#.Apply]) + + (#.Named name sub-type) + (code.symbol name) + + (^template [] + ( env body) + (` ( (.list (~+ (list/map to-code env))) + (~ (to-code 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 "")) ")")) + + (^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) ")")) + + (#.Parameter 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 Nothing #.Sum] + [tuple Any #.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 + _ (|> body ( (dec size)) ( (list)))))] + + [univ-q #.UnivQ] + [ex-q #.ExQ] + ) + +(def: #export (quantified? type) + (-> Type Bit) + (case type + (#.Named [module name] _type) + (quantified? _type) + + (#.Apply A F) + (maybe.default #0 + (do maybe.Monad + [applied (apply (list A) F)] + (wrap (quantified? applied)))) + + (^or (#.UnivQ _) (#.ExQ _)) + #1 + + _ + #0)) + +(def: #export (array level elem-type) + (-> Nat Type Type) + (case level + +0 elem-type + _ (|> elem-type (array (dec level)) (list) (#.Primitive "#Array")))) + +(syntax: #export (:log! {input (p.alt s.symbol + s.any)}) + (case input + (#.Left valueN) + (do @ + [cursor macro.cursor + valueT (macro.find-type valueN) + #let [_ (log! ($_ text/compose + ":log!" " @ " (.cursor-description cursor) "\n" + (ident/encode valueN) " : " (..to-text valueT) "\n"))]] + (wrap (list (' [])))) + + (#.Right valueC) + (macro.with-gensyms [g!value] + (wrap (list (` (.let [(~ g!value) (~ valueC)] + (..:log! (~ g!value))))))))) + +(def: type-parameters + (Syntax (List Text)) + (s.tuple (p.some s.local-symbol))) + +(syntax: #export (:cast {type-vars type-parameters} + input + output + {value (p.maybe s.any)}) + (let [casterC (` (: (All [(~+ (list/map code.local-symbol type-vars))] + (-> (~ input) (~ output))) + (|>> :assume)))] + (case value + #.None + (wrap (list casterC)) + + (#.Some value) + (wrap (list (` ((~ casterC) (~ value)))))))) + +(type: Typed + {#type Code + #expression Code}) + +(def: typed + (Syntax Typed) + (s.record (p.seq s.any s.any))) + +(syntax: #export (:share {type-vars type-parameters} + {exemplar typed} + {computation typed}) + (macro.with-gensyms [g!_] + (let [shareC (` (: (All [(~+ (list/map code.local-symbol type-vars))] + (-> (~ (get@ #type exemplar)) + (~ (get@ #type computation)))) + (.function ((~ g!_) (~ g!_)) + (:assume (~ (get@ #expression computation))))))] + (wrap (list (` ((~ shareC) (~ (get@ #expression exemplar))))))))) diff --git a/stdlib/source/lux/type/abstract.lux b/stdlib/source/lux/type/abstract.lux index bf17562da..7dd65b106 100644 --- a/stdlib/source/lux/type/abstract.lux +++ b/stdlib/source/lux/type/abstract.lux @@ -16,8 +16,7 @@ [common ["csr" reader] ["csw" writer]]]] - [language - [type (#+ :cast)]]]) + [type (#+ :cast)]]) (def: (get k plist) (All [a] 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 ("text/." Monoid Equivalence)] + [collection + ["." list] + ["." set (#+ Set)]]]] + ["." // ("type/." Equivalence)]) + +(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) + + (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) + + (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) + +(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 [ ] + [(def: #export ( id) + (-> Var (Check )) + (function (_ context) + (case (|> context (get@ #.var-bindings) (var::get id)) + (^or (#.Some (#.Some (#.Var _))) + (#.Some #.None)) + (#error.Success [context ]) + + (#.Some (#.Some bound)) + (#error.Success [context ]) + + #.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 + [?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)) + +(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 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 + [_ (..bind 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 Any)) + (do Monad + [_ (..bind (#.Var right) left)] + (..bind (#.Var left) right))) + +(def: (link-3 interpose to from) + (-> Var Var Var (Check Any)) + (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.Equivalence = 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 + [eFT' (apply-type! eFT eAT)] + (check' eFT' (#.Apply aAT aFT) assumptions)) + + (^or [(#.Ex _) (#.UnivQ _ _)] [(#.Var _) (#.UnivQ _ _)]) + (do Monad + [aFT' (apply-type! aFT aAT)] + (check' (#.Apply eAT eFT) aFT' assumptions)) + + (^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 (_ _) (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 [ ] + [(#.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 #1 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 [] + [( eL eR) ( aL aR)] + (do Monad + [assumptions (check' eL aL assumptions)] + (check' eR aR assumptions))) + ([#.Sum] + [#.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 Any)) + (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 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 + [paramsT+' (monad.map @ clean paramsT+)] + (wrap (#.Primitive name paramsT+'))) + + (^or (#.Parameter _) (#.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/type/implicit.lux b/stdlib/source/lux/type/implicit.lux index c4f025f4f..f8be1a83f 100644 --- a/stdlib/source/lux/type/implicit.lux +++ b/stdlib/source/lux/type/implicit.lux @@ -16,9 +16,8 @@ ["." macro (#+ Monad) ["." code] ["s" syntax (#+ syntax: Syntax)]] - [language - ["." type - ["." check (#+ Check)]]]]) + ["." type + ["." check (#+ Check)]]]) (def: (find-type-var id env) (-> Nat Type-Context (Meta Type)) diff --git a/stdlib/source/lux/type/object/interface.lux b/stdlib/source/lux/type/object/interface.lux index 94d42a28a..cb92c7253 100644 --- a/stdlib/source/lux/type/object/interface.lux +++ b/stdlib/source/lux/type/object/interface.lux @@ -12,6 +12,7 @@ [collection ["." list ("list/." Functor Fold Monoid)] ["." set (#+ Set)]]] + ["." type] ["." macro (#+ Monad) ("meta/." Monad) ["." code] ["s" syntax (#+ syntax:)] @@ -19,9 +20,7 @@ ["cs" common] [common ["csr" reader] - ["csw" writer]]]] - [language - ["." type]]]) + ["csw" writer]]]]]) ## [Common] (type: Declaration diff --git a/stdlib/source/lux/type/quotient.lux b/stdlib/source/lux/type/quotient.lux index 63d022a31..8f22f4702 100644 --- a/stdlib/source/lux/type/quotient.lux +++ b/stdlib/source/lux/type/quotient.lux @@ -5,9 +5,7 @@ ["p" parser]] [data ["e" error (#+ Error)]] - [language - ["." type]] - [type + ["." type abstract] ["." macro ["s" syntax (#+ syntax:)] diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux index 670a3101e..dd8664236 100644 --- a/stdlib/source/lux/type/refinement.lux +++ b/stdlib/source/lux/type/refinement.lux @@ -6,9 +6,7 @@ ["p" parser]] [data ["e" error (#+ Error)]] - [language - ["." type ("type/." Equivalence)]] - [type + ["." type ("type/." Equivalence) abstract] ["." macro ["s" syntax (#+ syntax:)] -- cgit v1.2.3