From 002ee0418195afccd1a1b500a36cc5b2adc44791 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 16 Jan 2018 22:33:38 -0400 Subject: - Added sub-structural types (for synchronous IO and asynchronous Promise). --- stdlib/source/lux/type/resource.lux | 187 +++++++++++++++++++++++++++++++++ stdlib/test/test/lux/type/resource.lux | 46 ++++++++ 2 files changed, 233 insertions(+) create mode 100644 stdlib/source/lux/type/resource.lux create mode 100644 stdlib/test/test/lux/type/resource.lux diff --git a/stdlib/source/lux/type/resource.lux b/stdlib/source/lux/type/resource.lux new file mode 100644 index 000000000..6da339ea8 --- /dev/null +++ b/stdlib/source/lux/type/resource.lux @@ -0,0 +1,187 @@ +(.module: + lux + (lux (control ["p" parser] + ["ex" exception #+ exception:] + [monad #+ Monad do] + (monad [indexed #+ IxMonad])) + (data [maybe] + [product] + [number] + text/format + (coll [dict #+ Dict] + [set] + [sequence #+ Sequence] + [list "list/" Functor Fold])) + (concurrency [promise #+ Promise]) + [macro] + (macro ["s" syntax #+ Syntax syntax:]) + (type abstract) + [io #+ IO])) + +(type: #export (Procedure monad input output value) + (-> input (monad [output value]))) + +(type: #export (Linear monad value) + (All [keys] + (Procedure monad keys keys value))) + +(type: #export (Affine monad permissions value) + (All [keys] + (Procedure monad keys [permissions keys] value))) + +(type: #export (Relevant monad permissions value) + (All [keys] + (Procedure monad [permissions keys] keys value))) + +(struct: (IxMonad Monad) + (All [m] (-> (Monad m) (IxMonad (Procedure m)))) + + (def: (wrap value) + (function [keys] + (:: Monad wrap [keys value]))) + + (def: (bind f input) + (function [keysI] + (do Monad + [[keysT value] (input keysI)] + ((f value) keysT))))) + +(do-template [ ] + [(def: #export + (IxMonad (Procedure )) + (IxMonad )) + + (def: #export ( procedure) + (All [v] (-> (Linear v) ( v))) + (do + [[_ output] (procedure [])] + (wrap output)))] + + [IxMonad IO io.Monad sync] + [IxMonad Promise promise.Monad async] + ) + +(abstract: #export Ordered {} []) + +(abstract: #export Commutative {} []) + +(abstract: #export (Key mode key) {} + [] + + (do-template [ ] + [(def: + (Ex [k] (-> [] (Key k))) + (|>> @abstraction))] + + [ordered-key Ordered] + [commutative-key Commutative] + )) + +(type: #export OK (Key Ordered)) +(type: #export CK (Key Commutative)) + +(abstract: #export (Res key value) + {#.doc "A value locked by a key."} + value + + (do-template [ ] + [(def: #export ( value) + (All [v] (Ex [k] (-> v (Affine (Key k) (Res k v))))) + (function [keys] + (:: wrap [[( []) keys] (@abstraction value)])))] + + [ordered IO io.Monad Ordered ordered-key] + [ordered! Promise promise.Monad Ordered ordered-key] + [commutative IO io.Monad Commutative commutative-key] + [commutative! Promise promise.Monad Commutative commutative-key]) + + (do-template [ ] + [(def: #export ( resource) + (All [v k m] + (-> (Res k v) (Relevant (Key m k) v))) + (function [[key keys]] + (:: wrap [keys (@representation resource)])))] + + [read IO io.Monad] + [read! Promise promise.Monad])) + +(exception: #export Index-Cannot-Be-Repeated) +(exception: #export Amount-Cannot-Be-Zero) + +(def: indices + (Syntax (List Nat)) + (s.tuple (loop [seen (set.new number.Hash)] + (do p.Monad + [done? s.end?] + (if done? + (wrap (list)) + (do @ + [head s.nat + _ (p.assert (Index-Cannot-Be-Repeated (%n head)) + (not (set.member? seen head))) + tail (recur (set.add head seen))] + (wrap (list& head tail)))))))) + +(def: (no-op Monad) + (All [m] (-> (Monad m) (Linear m Unit))) + (function [context] (:: Monad wrap [context []]))) + +(do-template [ ] + [(syntax: #export ( [swaps ..indices]) + (macro.with-gensyms [g!context] + (case swaps + #.Nil + (wrap (list (` ((~! no-op) )))) + + (#.Cons head tail) + (do macro.Monad + [#let [max-idx (list/fold n/max head tail)] + g!inputs (<| (monad.seq @) (list.repeat (n/inc max-idx)) (macro.gensym "input")) + #let [g!outputs (|> (monad.fold maybe.Monad + (function [from to] + (do maybe.Monad + [input (list.nth from g!inputs)] + (wrap (sequence.add input to)))) + (: (Sequence Code) sequence.empty) + swaps) + maybe.assume + sequence.to-list) + g!inputsT+ (list/map (|>> (~) ..CK (`)) g!inputs) + g!outputsT+ (list/map (|>> (~) ..CK (`)) g!outputs)]] + (wrap (list (` (: (All [(~+ g!inputs) (~ g!context)] + (Procedure (~! ) + [(~+ g!inputsT+) (~ g!context)] + [(~+ g!outputsT+) (~ g!context)] + Unit)) + (function [[(~+ g!inputs) (~ g!context)]] + (:: (~! ) (~' wrap) [[(~+ g!outputs) (~ g!context)] []]))))))))))] + + [exchange IO io.Monad] + [exchange! Promise promise.Monad]) + +(def: amount + (Syntax Nat) + (do p.Monad + [raw s.nat + _ (p.assert (Amount-Cannot-Be-Zero "") + (n/> +0 raw))] + (wrap raw))) + +(do-template [ ] + [(syntax: #export ( [amount amount]) + (macro.with-gensyms [g!context] + (do macro.Monad + [g!keys (<| (monad.seq @) (list.repeat amount) (macro.gensym "keys"))] + (wrap (list (` (: (All [(~+ g!keys) (~ g!context)] + (Procedure (~! ) + [ (~ g!context)] + [ (~ g!context)] + Unit)) + (function [[ (~ g!context)]] + (:: (~! ) (~' wrap) [[ (~ g!context)] []])))))))))] + + [group IO io.Monad (~+ g!keys) [(~+ g!keys)]] + [group! Promise promise.Monad (~+ g!keys) [(~+ g!keys)]] + [un-group IO io.Monad [(~+ g!keys)] (~+ g!keys)] + [un-group! Promise promise.Monad [(~+ g!keys)] (~+ g!keys)] + ) diff --git a/stdlib/test/test/lux/type/resource.lux b/stdlib/test/test/lux/type/resource.lux new file mode 100644 index 000000000..3681a7ce1 --- /dev/null +++ b/stdlib/test/test/lux/type/resource.lux @@ -0,0 +1,46 @@ +(.module: + lux + (lux (control (monad [indexed #+ do])) + [macro] + (type [resource #+ Res]) + [io]) + lux/test) + +(context: "Sub-structural typing." + ($_ seq + (test "Can produce and consume keys in an ordered manner." + (<| (n/= (n/+ +123 +456)) + io.run + resource.sync + (do resource.IxMonad + [res|left (resource.ordered +123) + res|right (resource.ordered +456) + right (resource.read res|right) + left (resource.read res|left)] + (wrap (n/+ left right))))) + + (test "Can exchange commutative keys." + (<| (n/= (n/+ +123 +456)) + io.run + resource.sync + (do resource.IxMonad + [res|left (resource.commutative +123) + res|right (resource.commutative +456) + _ (resource.exchange [+1 +0]) + left (resource.read res|left) + right (resource.read res|right)] + (wrap (n/+ left right))))) + + (test "Can group and un-group keys." + (<| (n/= (n/+ +123 +456)) + io.run + resource.sync + (do resource.IxMonad + [res|left (resource.commutative +123) + res|right (resource.commutative +456) + _ (resource.group +2) + _ (resource.un-group +2) + right (resource.read res|right) + left (resource.read res|left)] + (wrap (n/+ left right))))) + )) -- cgit v1.2.3