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". --- new-luxc/source/luxc/lang.lux | 4 +- new-luxc/source/luxc/lang/analysis/case.lux | 4 +- new-luxc/source/luxc/lang/analysis/common.lux | 2 +- new-luxc/source/luxc/lang/analysis/expression.lux | 2 +- new-luxc/source/luxc/lang/analysis/function.lux | 4 +- new-luxc/source/luxc/lang/analysis/inference.lux | 2 +- new-luxc/source/luxc/lang/analysis/primitive.lux | 4 +- .../source/luxc/lang/analysis/procedure/common.lux | 4 +- .../luxc/lang/analysis/procedure/host.jvm.lux | 4 +- new-luxc/source/luxc/lang/analysis/reference.lux | 4 +- new-luxc/source/luxc/lang/analysis/structure.lux | 4 +- new-luxc/source/luxc/lang/analysis/type.lux | 2 +- new-luxc/source/luxc/lang/translation.lux | 4 +- new-luxc/source/luxc/module/descriptor/type.lux | 2 +- new-luxc/test/test/luxc/lang/analysis/case.lux | 4 +- new-luxc/test/test/luxc/lang/analysis/function.lux | 4 +- .../test/test/luxc/lang/analysis/primitive.lux | 4 +- .../test/luxc/lang/analysis/procedure/common.lux | 4 +- .../test/luxc/lang/analysis/procedure/host.jvm.lux | 4 +- .../test/test/luxc/lang/analysis/reference.lux | 2 +- .../test/test/luxc/lang/analysis/structure.lux | 4 +- new-luxc/test/test/luxc/lang/analysis/type.lux | 4 +- 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 +- stdlib/test/test/lux/lang/type.lux | 165 +++++ stdlib/test/test/lux/lang/type/check.lux | 264 ++++++++ stdlib/test/test/lux/meta/type.lux | 165 ----- stdlib/test/test/lux/meta/type/check.lux | 264 -------- stdlib/test/test/lux/meta/type/implicit.lux | 19 +- stdlib/test/tests.lux | 8 +- 42 files changed, 1532 insertions(+), 1535 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 create mode 100644 stdlib/test/test/lux/lang/type.lux create mode 100644 stdlib/test/test/lux/lang/type/check.lux delete mode 100644 stdlib/test/test/lux/meta/type.lux delete mode 100644 stdlib/test/test/lux/meta/type/check.lux diff --git a/new-luxc/source/luxc/lang.lux b/new-luxc/source/luxc/lang.lux index 844cc6755..45a8b1860 100644 --- a/new-luxc/source/luxc/lang.lux +++ b/new-luxc/source/luxc/lang.lux @@ -9,8 +9,8 @@ text/format (coll [list])) [meta] - (meta (type ["tc" check]) - ["s" syntax #+ syntax:])) + (meta ["s" syntax #+ syntax:]) + (lang (type ["tc" check]))) (luxc (lang ["la" analysis]))) (type: #export Eval diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux index ff328b9de..69a975b52 100644 --- a/new-luxc/source/luxc/lang/analysis/case.lux +++ b/new-luxc/source/luxc/lang/analysis/case.lux @@ -12,8 +12,8 @@ text/format (coll [list "list/" Fold Monoid Functor])) [meta] - (meta [code] - [type] + (meta [code]) + (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang ["&;" scope] diff --git a/new-luxc/source/luxc/lang/analysis/common.lux b/new-luxc/source/luxc/lang/analysis/common.lux index 95355d62f..b67e8e268 100644 --- a/new-luxc/source/luxc/lang/analysis/common.lux +++ b/new-luxc/source/luxc/lang/analysis/common.lux @@ -5,7 +5,7 @@ (data text/format [product]) [meta] - (meta [type] + (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang analysis))) diff --git a/new-luxc/source/luxc/lang/analysis/expression.lux b/new-luxc/source/luxc/lang/analysis/expression.lux index afc347248..98addd197 100644 --- a/new-luxc/source/luxc/lang/analysis/expression.lux +++ b/new-luxc/source/luxc/lang/analysis/expression.lux @@ -6,7 +6,7 @@ [product] text/format) [meta] - (meta [type] + (lang [type] (type ["tc" check])) [host]) (luxc ["&" lang] diff --git a/new-luxc/source/luxc/lang/analysis/function.lux b/new-luxc/source/luxc/lang/analysis/function.lux index 611e5c8a4..7f2787e6f 100644 --- a/new-luxc/source/luxc/lang/analysis/function.lux +++ b/new-luxc/source/luxc/lang/analysis/function.lux @@ -7,8 +7,8 @@ text/format (coll [list "list/" Fold Monoid Monad])) [meta] - (meta [code] - [type] + (meta [code]) + (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang ["&;" scope] diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux index cccaa774a..910d5093a 100644 --- a/new-luxc/source/luxc/lang/analysis/inference.lux +++ b/new-luxc/source/luxc/lang/analysis/inference.lux @@ -7,7 +7,7 @@ text/format (coll [list "list/" Functor])) [meta "meta/" Monad] - (meta [type] + (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang ["la" analysis #+ Analysis] diff --git a/new-luxc/source/luxc/lang/analysis/primitive.lux b/new-luxc/source/luxc/lang/analysis/primitive.lux index 792d607c3..2a0fbfbe5 100644 --- a/new-luxc/source/luxc/lang/analysis/primitive.lux +++ b/new-luxc/source/luxc/lang/analysis/primitive.lux @@ -2,8 +2,8 @@ lux (lux (control monad) [meta] - (meta [code] - (type ["tc" check]))) + (meta [code]) + (lang (type ["tc" check]))) (luxc ["&" lang] (lang ["la" analysis #+ Analysis]))) diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux index a643cb76a..a394c554c 100644 --- a/new-luxc/source/luxc/lang/analysis/procedure/common.lux +++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux @@ -9,8 +9,8 @@ [array] [dict #+ Dict])) [meta] - (meta [code] - (type ["tc" check])) + (meta [code]) + (lang (type ["tc" check])) [io]) (luxc ["&" lang] (lang ["la" analysis] diff --git a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux index 8f5382d2b..827f3213d 100644 --- a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux +++ b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux @@ -16,8 +16,8 @@ [dict #+ Dict])) [meta "meta/" Monad] (meta [code] - ["s" syntax] - [type] + ["s" syntax]) + (lang [type] (type ["tc" check])) [host]) (luxc ["&" lang] diff --git a/new-luxc/source/luxc/lang/analysis/reference.lux b/new-luxc/source/luxc/lang/analysis/reference.lux index 6ba0325df..c3ff3456b 100644 --- a/new-luxc/source/luxc/lang/analysis/reference.lux +++ b/new-luxc/source/luxc/lang/analysis/reference.lux @@ -2,8 +2,8 @@ lux (lux (control monad) [meta] - (meta [code] - (type ["tc" check]))) + (meta [code]) + (lang (type ["tc" check]))) (luxc ["&" lang] (lang ["&;" scope] ["la" analysis #+ Analysis] diff --git a/new-luxc/source/luxc/lang/analysis/structure.lux b/new-luxc/source/luxc/lang/analysis/structure.lux index 76b5a3a42..70744ba5b 100644 --- a/new-luxc/source/luxc/lang/analysis/structure.lux +++ b/new-luxc/source/luxc/lang/analysis/structure.lux @@ -10,8 +10,8 @@ [dict #+ Dict]) text/format) [meta] - (meta [code] - [type] + (meta [code]) + (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang ["&;" scope] diff --git a/new-luxc/source/luxc/lang/analysis/type.lux b/new-luxc/source/luxc/lang/analysis/type.lux index eb3de08de..c91fdab38 100644 --- a/new-luxc/source/luxc/lang/analysis/type.lux +++ b/new-luxc/source/luxc/lang/analysis/type.lux @@ -2,7 +2,7 @@ lux (lux (control monad) [meta] - (meta (type ["tc" check]))) + (lang (type ["tc" check]))) (luxc ["&" lang] (lang ["la" analysis #+ Analysis]))) diff --git a/new-luxc/source/luxc/lang/translation.lux b/new-luxc/source/luxc/lang/translation.lux index 88fc25d3a..1e631205d 100644 --- a/new-luxc/source/luxc/lang/translation.lux +++ b/new-luxc/source/luxc/lang/translation.lux @@ -8,8 +8,8 @@ text/format (coll [dict])) [meta] - (meta (type ["tc" check])) - (lang [syntax]) + (lang [syntax] + (type ["tc" check])) [host] [io] (world [file #+ File])) diff --git a/new-luxc/source/luxc/module/descriptor/type.lux b/new-luxc/source/luxc/module/descriptor/type.lux index 2f5b8667b..58e29c39e 100644 --- a/new-luxc/source/luxc/module/descriptor/type.lux +++ b/new-luxc/source/luxc/module/descriptor/type.lux @@ -8,7 +8,7 @@ [number] ["e" error] (coll [list "L/" Functor])) - (meta [type "type/" Eq])) + (lang [type "type/" Eq])) ["&" ../common]) (do-template [ ] diff --git a/new-luxc/test/test/luxc/lang/analysis/case.lux b/new-luxc/test/test/luxc/lang/analysis/case.lux index 6d34ef4c5..bffa99bce 100644 --- a/new-luxc/test/test/luxc/lang/analysis/case.lux +++ b/new-luxc/test/test/luxc/lang/analysis/case.lux @@ -13,8 +13,8 @@ ["S" set])) ["r" math/random "r/" Monad] [meta #+ Monad] - (meta [code] - [type "type/" Eq] + (meta [code]) + (lang [type "type/" Eq] (type ["tc" check])) test) (luxc ["&" lang] diff --git a/new-luxc/test/test/luxc/lang/analysis/function.lux b/new-luxc/test/test/luxc/lang/analysis/function.lux index 6cddfebd2..5b84d3dd0 100644 --- a/new-luxc/test/test/luxc/lang/analysis/function.lux +++ b/new-luxc/test/test/luxc/lang/analysis/function.lux @@ -11,8 +11,8 @@ (coll [list "list/" Functor])) ["r" math/random "r/" Monad] [meta] - (meta [code] - [type "type/" Eq]) + (meta [code]) + (lang [type "type/" Eq]) test) (luxc ["&" lang] (lang ["@;" module] diff --git a/new-luxc/test/test/luxc/lang/analysis/primitive.lux b/new-luxc/test/test/luxc/lang/analysis/primitive.lux index 8e1329eb6..b4dc1a63d 100644 --- a/new-luxc/test/test/luxc/lang/analysis/primitive.lux +++ b/new-luxc/test/test/luxc/lang/analysis/primitive.lux @@ -13,8 +13,8 @@ (coll [list "L/" Functor Fold])) ["r" math/random] [meta #+ Monad] - (meta [code] - [type "type/" Eq]) + (meta [code]) + (lang [type "type/" Eq]) test) (luxc ["&" lang] (lang ["&;" module] diff --git a/new-luxc/test/test/luxc/lang/analysis/procedure/common.lux b/new-luxc/test/test/luxc/lang/analysis/procedure/common.lux index 3420ebb4d..f5b1feb71 100644 --- a/new-luxc/test/test/luxc/lang/analysis/procedure/common.lux +++ b/new-luxc/test/test/luxc/lang/analysis/procedure/common.lux @@ -10,8 +10,8 @@ (coll [array])) ["r" math/random "r/" Monad] [meta #+ Monad] - (meta [code] - [type "type/" Eq]) + (meta [code]) + (lang [type "type/" Eq]) test) (luxc ["&" lang] (lang ["&;" scope] diff --git a/new-luxc/test/test/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/test/test/luxc/lang/analysis/procedure/host.jvm.lux index 783174777..b82eb8206 100644 --- a/new-luxc/test/test/luxc/lang/analysis/procedure/host.jvm.lux +++ b/new-luxc/test/test/luxc/lang/analysis/procedure/host.jvm.lux @@ -14,8 +14,8 @@ [dict])) ["r" math/random "r/" Monad] [meta #+ Monad] - (meta [code] - [type]) + (meta [code]) + (lang [type]) test) (luxc ["&" lang] (lang ["&;" scope] diff --git a/new-luxc/test/test/luxc/lang/analysis/reference.lux b/new-luxc/test/test/luxc/lang/analysis/reference.lux index 15e5af44f..16cfb9a38 100644 --- a/new-luxc/test/test/luxc/lang/analysis/reference.lux +++ b/new-luxc/test/test/luxc/lang/analysis/reference.lux @@ -6,7 +6,7 @@ (data ["e" error]) ["r" math/random] [meta #+ Monad] - (meta [type "type/" Eq]) + (lang [type "type/" Eq]) test) (luxc (lang ["&;" scope] ["&;" module] diff --git a/new-luxc/test/test/luxc/lang/analysis/structure.lux b/new-luxc/test/test/luxc/lang/analysis/structure.lux index 8cc95fd88..cc31622a1 100644 --- a/new-luxc/test/test/luxc/lang/analysis/structure.lux +++ b/new-luxc/test/test/luxc/lang/analysis/structure.lux @@ -13,8 +13,8 @@ ["S" set])) ["r" math/random "r/" Monad] [meta] - (meta [code] - [type "type/" Eq] + (meta [code]) + (lang [type "type/" Eq] (type ["tc" check])) test) (luxc ["&" lang] diff --git a/new-luxc/test/test/luxc/lang/analysis/type.lux b/new-luxc/test/test/luxc/lang/analysis/type.lux index 6d89582e8..ed75f4d6c 100644 --- a/new-luxc/test/test/luxc/lang/analysis/type.lux +++ b/new-luxc/test/test/luxc/lang/analysis/type.lux @@ -13,8 +13,8 @@ (coll [list "list/" Functor Fold])) ["r" math/random "r/" Monad] [meta #+ Monad] - (meta [code] - [type "type/" Eq]) + (meta [code]) + (lang [type "type/" Eq]) test) (luxc ["&" lang] (lang ["&;" module] 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 diff --git a/stdlib/test/test/lux/lang/type.lux b/stdlib/test/test/lux/lang/type.lux new file mode 100644 index 000000000..a592df312 --- /dev/null +++ b/stdlib/test/test/lux/lang/type.lux @@ -0,0 +1,165 @@ +(;module: + lux + (lux [io] + (control ["M" monad #+ do Monad] + pipe) + (data [text "Text/" Monoid] + text/format + [number] + [maybe] + (coll [list])) + ["r" math/random] + (lang ["&" type])) + lux/test) + +## [Utils] +(def: gen-name + (r;Random Text) + (do r;Monad + [size (|> r;nat (:: @ map (n.% +10)))] + (r;text size))) + +(def: gen-ident + (r;Random Ident) + (r;seq gen-name gen-name)) + +(def: gen-type + (r;Random Type) + (let [(^open "R/") r;Monad] + (r;rec (function [gen-type] + ($_ r;alt + (r;seq gen-name (R/wrap (list))) + (R/wrap []) + (R/wrap []) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + r;nat + r;nat + r;nat + (r;seq (R/wrap (list)) gen-type) + (r;seq (R/wrap (list)) gen-type) + (r;seq gen-type gen-type) + (r;seq gen-ident gen-type) + ))))) + +## [Tests] +(context: "Types" + (<| (times +100) + (do @ + [sample gen-type] + (test "Every type is equal to itself." + (:: &;Eq = sample sample))))) + +(context: "Type application" + (test "Can apply quantified types (universal and existential quantification)." + (and (maybe;default false + (do maybe;Monad + [partial (&;apply (list Bool) Ann) + full (&;apply (list Int) partial)] + (wrap (:: &;Eq = full (#;Product Bool Int))))) + (|> (&;apply (list Bool) Text) + (case> #;None true _ false))))) + +(context: "Naming" + (let [base (#;Named ["" "a"] (#;Product Bool Int)) + aliased (#;Named ["" "c"] + (#;Named ["" "b"] + base))] + ($_ seq + (test "Can remove aliases from an already-named type." + (:: &;Eq = + base + (&;un-alias aliased))) + + (test "Can remove all names from a type." + (and (not (:: &;Eq = + base + (&;un-name aliased))) + (:: &;Eq = + (&;un-name base) + (&;un-name aliased))))))) + +(context: "Type construction [structs]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + members (|> gen-type + (r;filter (function [type] + (case type + (^or (#;Sum _) (#;Product _)) + false + + _ + true))) + (list;repeat size) + (M;seq @)) + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [flat (|> members )] + (or (L/= members flat) + (and (L/= (list) members) + (L/= (list ) flat)))))] + + ["variant" &;variant &;flatten-variant Void] + ["tuple" &;tuple &;flatten-tuple Unit] + )] + ($_ seq + + ))))) + +(context: "Type construction [parameterized]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + members (M;seq @ (list;repeat size gen-type)) + extra (|> gen-type + (r;filter (function [type] + (case type + (^or (#;Function _) (#;Apply _)) + false + + _ + true)))) + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + ($_ seq + (test "Can build and tear-down function types." + (let [[inputs output] (|> (&;function members extra) &;flatten-function)] + (and (L/= members inputs) + (&/= extra output)))) + + (test "Can build and tear-down application types." + (let [[tfunc tparams] (|> extra (&;application members) &;flatten-application)] + (n.= (list;size members) (list;size tparams)))) + )))) + +(context: "Type construction [higher order]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + extra (|> gen-type + (r;filter (function [type] + (case type + (^or (#;UnivQ _) (#;ExQ _)) + false + + _ + true)))) + #let [(^open "&/") &;Eq]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [[flat-size flat-body] (|> extra ( size) )] + (and (n.= size flat-size) + (&/= extra flat-body))))] + + ["universally-quantified" &;univ-q &;flatten-univ-q] + ["existentially-quantified" &;ex-q &;flatten-ex-q] + )] + ($_ seq + + ))))) diff --git a/stdlib/test/test/lux/lang/type/check.lux b/stdlib/test/test/lux/lang/type/check.lux new file mode 100644 index 000000000..32f7e832b --- /dev/null +++ b/stdlib/test/test/lux/lang/type/check.lux @@ -0,0 +1,264 @@ +(;module: + lux + (lux [io] + (control [monad #+ do Monad] + [pipe #+ case>]) + (data [product] + [maybe] + [number] + [text "text/" Monoid Eq] + text/format + (coll [list "list/" Functor] + [set])) + ["r" math/random] + (lang [type "type/" Eq] + ["@" type/check])) + lux/test) + +## [Utils] +(def: gen-name + (r;Random Text) + (do r;Monad + [size (|> r;nat (:: @ map (n.% +10)))] + (r;text size))) + +(def: gen-ident + (r;Random Ident) + (r;seq gen-name gen-name)) + +(def: gen-type + (r;Random Type) + (let [(^open "r/") r;Monad] + (r;rec (function [gen-type] + ($_ r;alt + (r;seq gen-name (r/wrap (list))) + (r/wrap []) + (r/wrap []) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + r;nat + r;nat + r;nat + (r;seq (r/wrap (list)) gen-type) + (r;seq (r/wrap (list)) gen-type) + (r;seq gen-type gen-type) + (r;seq gen-ident gen-type) + ))))) + +(def: (valid-type? type) + (-> Type Bool) + (case type + (#;Primitive name params) + (list;every? valid-type? params) + + (^or #;Void #;Unit (#;Ex id)) + true + + (^template [] + ( left right) + (and (valid-type? left) (valid-type? right))) + ([#;Sum] [#;Product] [#;Function]) + + (#;Named name type') + (valid-type? type') + + _ + false)) + +(def: (type-checks? input) + (-> (@;Check []) Bool) + (case (@;run @;fresh-context input) + (#;Right []) + true + + (#;Left error) + false)) + +## [Tests] +(context: "Top and Bottom." + (<| (times +100) + (do @ + [sample (|> gen-type (r;filter valid-type?))] + ($_ seq + (test "Top is the super-type of everything." + (@;checks? Top sample)) + + (test "Bottom is the sub-type of everything." + (@;checks? sample Bottom)) + )))) + +(context: "Simple type-checking." + ($_ seq + (test "Unit and Void match themselves." + (and (@;checks? Void Void) + (@;checks? Unit Unit))) + + (test "Existential types only match with themselves." + (and (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check exT exT))) + (not (type-checks? (do @;Monad + [[_ exTL] @;existential + [_ exTR] @;existential] + (@;check exTL exTR)))))) + + (test "Names do not affect type-checking." + (and (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + exT))) + (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check exT + (#;Named ["module" "name"] exT)))) + (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + (#;Named ["module" "name"] exT)))))) + + (test "Functions are covariant on inputs and contravariant on outputs." + (and (@;checks? (#;Function Bottom Top) + (#;Function Top Bottom)) + (not (@;checks? (#;Function Top Bottom) + (#;Function Bottom Top))))) + )) + +(context: "Type application." + (<| (times +100) + (do @ + [meta gen-type + data gen-type] + (test "Can type-check type application." + (and (@;checks? (|> Ann (#;Apply meta) (#;Apply data)) + (type;tuple (list meta data))) + (@;checks? (type;tuple (list meta data)) + (|> Ann (#;Apply meta) (#;Apply data)))))))) + +(context: "Primitive types." + (<| (times +100) + (do @ + [nameL gen-name + nameR (|> gen-name (r;filter (. not (text/= nameL)))) + paramL gen-type + paramR (|> gen-type (r;filter (|>. (@;checks? paramL) not)))] + ($_ seq + (test "Primitive types match when they have the same name and the same parameters." + (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameL (list paramL)))) + + (test "Names matter to primitive types." + (not (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameR (list paramL))))) + + (test "Parameters matter to primitive types." + (not (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameL (list paramR))))) + )))) + +(context: "Type variables." + ($_ seq + (test "Type-vars check against themselves." + (type-checks? (do @;Monad + [[id var] @;var] + (@;check var var)))) + + (test "Can bind unbound type-vars by type-checking against them." + (and (type-checks? (do @;Monad + [[id var] @;var] + (@;check var #;Unit))) + (type-checks? (do @;Monad + [[id var] @;var] + (@;check #;Unit var))))) + + (test "Cannot rebind already bound type-vars." + (not (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var #;Unit)] + (@;check var #;Void))))) + + (test "If the type bound to a var is a super-type to another, then the var is also a super-type." + (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var Top)] + (@;check var #;Unit)))) + + (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." + (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var Bottom)] + (@;check #;Unit var)))) + )) + +(def: (build-ring num-connections) + (-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]])) + (do @;Monad + [[head-id head-type] @;var + ids+types (monad;seq @ (list;repeat num-connections @;var)) + [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]] + (do @ + [_ (@;check head-type tail-type)] + (wrap [tail-id tail-type]))) + [head-id head-type] + ids+types)] + (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) + +(context: "Rings of type variables." + (<| (times +100) + (do @ + [num-connections (|> r;nat (:: @ map (n.% +100))) + boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) + pick-pcg (r;seq r;nat r;nat)] + ($_ seq + (test "Can create rings of variables." + (type-checks? (do @;Monad + [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) + #let [ids (list/map product;left ids+types)] + headR (@;ring head-id) + tailR (@;ring tail-id)] + (@;assert "" + (let [same-rings? (:: set;Eq = headR tailR) + expected-size? (n.= (n.inc num-connections) (set;size headR)) + same-vars? (|> (set;to-list headR) + (list;sort n.<) + (:: (list;Eq number;Eq) = (list;sort n.< (#;Cons head-id ids))))] + (and same-rings? + expected-size? + same-vars?)))))) + (test "When a var in a ring is bound, all the ring is bound." + (type-checks? (do @;Monad + [[[head-id headT] ids+types tailT] (build-ring num-connections) + #let [ids (list/map product;left ids+types)] + _ (@;check headT boundT) + head-bound (@;read head-id) + tail-bound (monad;map @ @;read ids) + headR (@;ring head-id) + tailR+ (monad;map @ @;ring ids)] + (let [rings-were-erased? (and (set;empty? headR) + (list;every? set;empty? tailR+)) + same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) + (list/map (function [[tail-id ?tailT]] + (maybe;default (#;Var tail-id) ?tailT)) + (list;zip2 ids tail-bound))))] + (@;assert "" + (and rings-were-erased? + same-types?)))))) + (test "Can merge multiple rings of variables." + (type-checks? (do @;Monad + [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) + [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) + headRL-pre (@;ring head-idL) + headRR-pre (@;ring head-idR) + _ (@;check headTL headTR) + headRL-post (@;ring head-idL) + headRR-post (@;ring head-idR)] + (@;assert "" + (let [same-rings? (:: set;Eq = headRL-post headRR-post) + expected-size? (n.= (n.* +2 (n.inc num-connections)) + (set;size headRL-post)) + union? (:: set;Eq = headRL-post (set;union headRL-pre headRR-pre))] + (and same-rings? + expected-size? + union?)))))) + )) + )) diff --git a/stdlib/test/test/lux/meta/type.lux b/stdlib/test/test/lux/meta/type.lux deleted file mode 100644 index abddcc033..000000000 --- a/stdlib/test/test/lux/meta/type.lux +++ /dev/null @@ -1,165 +0,0 @@ -(;module: - lux - (lux [io] - (control ["M" monad #+ do Monad] - pipe) - (data [text "Text/" Monoid] - text/format - [number] - [maybe] - (coll [list])) - ["r" math/random] - (meta ["&" type])) - lux/test) - -## [Utils] -(def: gen-name - (r;Random Text) - (do r;Monad - [size (|> r;nat (:: @ map (n.% +10)))] - (r;text size))) - -(def: gen-ident - (r;Random Ident) - (r;seq gen-name gen-name)) - -(def: gen-type - (r;Random Type) - (let [(^open "R/") r;Monad] - (r;rec (function [gen-type] - ($_ r;alt - (r;seq gen-name (R/wrap (list))) - (R/wrap []) - (R/wrap []) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - r;nat - r;nat - r;nat - (r;seq (R/wrap (list)) gen-type) - (r;seq (R/wrap (list)) gen-type) - (r;seq gen-type gen-type) - (r;seq gen-ident gen-type) - ))))) - -## [Tests] -(context: "Types" - (<| (times +100) - (do @ - [sample gen-type] - (test "Every type is equal to itself." - (:: &;Eq = sample sample))))) - -(context: "Type application" - (test "Can apply quantified types (universal and existential quantification)." - (and (maybe;default false - (do maybe;Monad - [partial (&;apply (list Bool) Ann) - full (&;apply (list Int) partial)] - (wrap (:: &;Eq = full (#;Product Bool Int))))) - (|> (&;apply (list Bool) Text) - (case> #;None true _ false))))) - -(context: "Naming" - (let [base (#;Named ["" "a"] (#;Product Bool Int)) - aliased (#;Named ["" "c"] - (#;Named ["" "b"] - base))] - ($_ seq - (test "Can remove aliases from an already-named type." - (:: &;Eq = - base - (&;un-alias aliased))) - - (test "Can remove all names from a type." - (and (not (:: &;Eq = - base - (&;un-name aliased))) - (:: &;Eq = - (&;un-name base) - (&;un-name aliased))))))) - -(context: "Type construction [structs]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - members (|> gen-type - (r;filter (function [type] - (case type - (^or (#;Sum _) (#;Product _)) - false - - _ - true))) - (list;repeat size) - (M;seq @)) - #let [(^open "&/") &;Eq - (^open "L/") (list;Eq &;Eq)]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [flat (|> members )] - (or (L/= members flat) - (and (L/= (list) members) - (L/= (list ) flat)))))] - - ["variant" &;variant &;flatten-variant Void] - ["tuple" &;tuple &;flatten-tuple Unit] - )] - ($_ seq - - ))))) - -(context: "Type construction [parameterized]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - members (M;seq @ (list;repeat size gen-type)) - extra (|> gen-type - (r;filter (function [type] - (case type - (^or (#;Function _) (#;Apply _)) - false - - _ - true)))) - #let [(^open "&/") &;Eq - (^open "L/") (list;Eq &;Eq)]] - ($_ seq - (test "Can build and tear-down function types." - (let [[inputs output] (|> (&;function members extra) &;flatten-function)] - (and (L/= members inputs) - (&/= extra output)))) - - (test "Can build and tear-down application types." - (let [[tfunc tparams] (|> extra (&;application members) &;flatten-application)] - (n.= (list;size members) (list;size tparams)))) - )))) - -(context: "Type construction [higher order]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - extra (|> gen-type - (r;filter (function [type] - (case type - (^or (#;UnivQ _) (#;ExQ _)) - false - - _ - true)))) - #let [(^open "&/") &;Eq]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [[flat-size flat-body] (|> extra ( size) )] - (and (n.= size flat-size) - (&/= extra flat-body))))] - - ["universally-quantified" &;univ-q &;flatten-univ-q] - ["existentially-quantified" &;ex-q &;flatten-ex-q] - )] - ($_ seq - - ))))) diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux deleted file mode 100644 index 127e02cbd..000000000 --- a/stdlib/test/test/lux/meta/type/check.lux +++ /dev/null @@ -1,264 +0,0 @@ -(;module: - lux - (lux [io] - (control [monad #+ do Monad] - [pipe #+ case>]) - (data [product] - [maybe] - [number] - [text "text/" Monoid Eq] - text/format - (coll [list "list/" Functor] - [set])) - ["r" math/random] - (meta [type "type/" Eq] - ["@" type/check])) - lux/test) - -## [Utils] -(def: gen-name - (r;Random Text) - (do r;Monad - [size (|> r;nat (:: @ map (n.% +10)))] - (r;text size))) - -(def: gen-ident - (r;Random Ident) - (r;seq gen-name gen-name)) - -(def: gen-type - (r;Random Type) - (let [(^open "r/") r;Monad] - (r;rec (function [gen-type] - ($_ r;alt - (r;seq gen-name (r/wrap (list))) - (r/wrap []) - (r/wrap []) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - r;nat - r;nat - r;nat - (r;seq (r/wrap (list)) gen-type) - (r;seq (r/wrap (list)) gen-type) - (r;seq gen-type gen-type) - (r;seq gen-ident gen-type) - ))))) - -(def: (valid-type? type) - (-> Type Bool) - (case type - (#;Primitive name params) - (list;every? valid-type? params) - - (^or #;Void #;Unit (#;Ex id)) - true - - (^template [] - ( left right) - (and (valid-type? left) (valid-type? right))) - ([#;Sum] [#;Product] [#;Function]) - - (#;Named name type') - (valid-type? type') - - _ - false)) - -(def: (type-checks? input) - (-> (@;Check []) Bool) - (case (@;run @;fresh-context input) - (#;Right []) - true - - (#;Left error) - false)) - -## [Tests] -(context: "Top and Bottom." - (<| (times +100) - (do @ - [sample (|> gen-type (r;filter valid-type?))] - ($_ seq - (test "Top is the super-type of everything." - (@;checks? Top sample)) - - (test "Bottom is the sub-type of everything." - (@;checks? sample Bottom)) - )))) - -(context: "Simple type-checking." - ($_ seq - (test "Unit and Void match themselves." - (and (@;checks? Void Void) - (@;checks? Unit Unit))) - - (test "Existential types only match with themselves." - (and (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check exT exT))) - (not (type-checks? (do @;Monad - [[_ exTL] @;existential - [_ exTR] @;existential] - (@;check exTL exTR)))))) - - (test "Names do not affect type-checking." - (and (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check (#;Named ["module" "name"] exT) - exT))) - (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check exT - (#;Named ["module" "name"] exT)))) - (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check (#;Named ["module" "name"] exT) - (#;Named ["module" "name"] exT)))))) - - (test "Functions are covariant on inputs and contravariant on outputs." - (and (@;checks? (#;Function Bottom Top) - (#;Function Top Bottom)) - (not (@;checks? (#;Function Top Bottom) - (#;Function Bottom Top))))) - )) - -(context: "Type application." - (<| (times +100) - (do @ - [meta gen-type - data gen-type] - (test "Can type-check type application." - (and (@;checks? (|> Ann (#;Apply meta) (#;Apply data)) - (type;tuple (list meta data))) - (@;checks? (type;tuple (list meta data)) - (|> Ann (#;Apply meta) (#;Apply data)))))))) - -(context: "Primitive types." - (<| (times +100) - (do @ - [nameL gen-name - nameR (|> gen-name (r;filter (. not (text/= nameL)))) - paramL gen-type - paramR (|> gen-type (r;filter (|>. (@;checks? paramL) not)))] - ($_ seq - (test "Primitive types match when they have the same name and the same parameters." - (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameL (list paramL)))) - - (test "Names matter to primitive types." - (not (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameR (list paramL))))) - - (test "Parameters matter to primitive types." - (not (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameL (list paramR))))) - )))) - -(context: "Type variables." - ($_ seq - (test "Type-vars check against themselves." - (type-checks? (do @;Monad - [[id var] @;var] - (@;check var var)))) - - (test "Can bind unbound type-vars by type-checking against them." - (and (type-checks? (do @;Monad - [[id var] @;var] - (@;check var #;Unit))) - (type-checks? (do @;Monad - [[id var] @;var] - (@;check #;Unit var))))) - - (test "Cannot rebind already bound type-vars." - (not (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var #;Unit)] - (@;check var #;Void))))) - - (test "If the type bound to a var is a super-type to another, then the var is also a super-type." - (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var Top)] - (@;check var #;Unit)))) - - (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." - (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var Bottom)] - (@;check #;Unit var)))) - )) - -(def: (build-ring num-connections) - (-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]])) - (do @;Monad - [[head-id head-type] @;var - ids+types (monad;seq @ (list;repeat num-connections @;var)) - [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]] - (do @ - [_ (@;check head-type tail-type)] - (wrap [tail-id tail-type]))) - [head-id head-type] - ids+types)] - (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) - -(context: "Rings of type variables." - (<| (times +100) - (do @ - [num-connections (|> r;nat (:: @ map (n.% +100))) - boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) - pick-pcg (r;seq r;nat r;nat)] - ($_ seq - (test "Can create rings of variables." - (type-checks? (do @;Monad - [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) - #let [ids (list/map product;left ids+types)] - headR (@;ring head-id) - tailR (@;ring tail-id)] - (@;assert "" - (let [same-rings? (:: set;Eq = headR tailR) - expected-size? (n.= (n.inc num-connections) (set;size headR)) - same-vars? (|> (set;to-list headR) - (list;sort n.<) - (:: (list;Eq number;Eq) = (list;sort n.< (#;Cons head-id ids))))] - (and same-rings? - expected-size? - same-vars?)))))) - (test "When a var in a ring is bound, all the ring is bound." - (type-checks? (do @;Monad - [[[head-id headT] ids+types tailT] (build-ring num-connections) - #let [ids (list/map product;left ids+types)] - _ (@;check headT boundT) - head-bound (@;read head-id) - tail-bound (monad;map @ @;read ids) - headR (@;ring head-id) - tailR+ (monad;map @ @;ring ids)] - (let [rings-were-erased? (and (set;empty? headR) - (list;every? set;empty? tailR+)) - same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) - (list/map (function [[tail-id ?tailT]] - (maybe;default (#;Var tail-id) ?tailT)) - (list;zip2 ids tail-bound))))] - (@;assert "" - (and rings-were-erased? - same-types?)))))) - (test "Can merge multiple rings of variables." - (type-checks? (do @;Monad - [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) - [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) - headRL-pre (@;ring head-idL) - headRR-pre (@;ring head-idR) - _ (@;check headTL headTR) - headRL-post (@;ring head-idL) - headRR-post (@;ring head-idR)] - (@;assert "" - (let [same-rings? (:: set;Eq = headRL-post headRR-post) - expected-size? (n.= (n.* +2 (n.inc num-connections)) - (set;size headRL-post)) - union? (:: set;Eq = headRL-post (set;union headRL-pre headRR-pre))] - (and same-rings? - expected-size? - union?)))))) - )) - )) diff --git a/stdlib/test/test/lux/meta/type/implicit.lux b/stdlib/test/test/lux/meta/type/implicit.lux index 8c05b01af..6d2344120 100644 --- a/stdlib/test/test/lux/meta/type/implicit.lux +++ b/stdlib/test/test/lux/meta/type/implicit.lux @@ -4,15 +4,12 @@ (control [monad #+ do Monad] functor [eq]) - (data [text "Text/" Monoid] - text/format - [number] - [bool "B/" Eq] + (data [number] + [bool "bool/" Eq] maybe (coll [list])) ["r" math/random] - (meta [type] - type/implicit)) + (meta type/implicit)) lux/test) (context: "Automatic structure selection" @@ -22,11 +19,11 @@ y r;nat] ($_ seq (test "Can automatically select first-order structures." - (let [(^open "L/") (list;Eq number;Eq)] - (and (B/= (:: number;Eq = x y) - (::: = x y)) - (L/= (list;n.range +1 +10) - (::: map n.inc (list;n.range +0 +9))) + (let [(^open "list/") (list;Eq number;Eq)] + (and (bool/= (:: number;Eq = x y) + (::: = x y)) + (list/= (list;n.range +1 +10) + (::: map n.inc (list;n.range +0 +9))) ))) (test "Can automatically select second-order structures." diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index d4e038774..3e1d6b5f3 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -66,11 +66,11 @@ ["_;" syntax] (poly ["poly_;" eq] ["poly_;" functor]) - ["_;" type] - (type ["_;" check] - ["_;" implicit] + (type ["_;" implicit] ["_;" object])) - (lang ["lang_;" syntax]) + (lang ["lang_;" syntax] + ["_;" type] + (type ["_;" check])) (world ["_;" blob] ["_;" file] (net ["_;" tcp] -- cgit v1.2.3