Last active
September 23, 2021 15:15
-
-
Save pchiusano/4b6e79f42db5c0e55488d6c9ee249d54 to your computer and use it in GitHub Desktop.
Nondeterminism ability
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
structural ability Split where | |
skip! : x | |
both : a -> a -> a | |
Split! : [a] ->{Split} a | |
Split! = cases | |
[] -> skip! | |
[a] -> a | |
as -> | |
(l,r) = halve as | |
force (both (Split l) (Split r)) | |
Split : [a] -> '{Split} a | |
Split as _ = Split! as | |
Split.toList : '{Split, g} a ->{g} [a] | |
Split.toList s = | |
go = cases | |
{ a } -> [a] | |
{ skip! -> k } -> [] | |
{ both l r -> k } -> | |
(handle k l with go) ++ (handle k r with go) | |
handle !s with go | |
Split.append : '{Split, g} a -> '{Split, g} a -> '{Split, g} a | |
Split.append s1 s2 _ = force (both s1 s2) | |
(Split.append.aliases.<>) = Split.append | |
Split.keep : (a ->{Split,g} Boolean) -> '{Split, g} a -> '{Split, g} a | |
Split.keep f s _ = | |
a = !s | |
if f a then a else skip! | |
Split.map : (a ->{Split,g} b) -> '{Split, g} a -> '{Split, g} b | |
Split.map f s _ = | |
a = !s | |
f a | |
Split.mapSome : (a ->{Split,g} Optional b) -> '{Split, g} a -> '{Split, g} b | |
Split.mapSome f s _ = match f !s with | |
None -> skip! | |
Some b -> b | |
Split.zipSame : '{Split, g} a -> '{Split, g} b -> '{Split, g} (a, b) | |
Split.zipSame sa sb _ = | |
go : '{Split,g2} y -> Request {Split} x ->{Split,g2} (x,y) | |
go sb = cases | |
{ a } -> (a, !sb) | |
{ skip! -> _ } -> skip! | |
{ both la ra -> k } -> | |
handle !sb with cases | |
{ _ } -> skip! | |
{ skip! -> k } -> skip! | |
{ both lb rb -> k2 } -> force ( | |
both (zipSame '(k la) '(k2 lb)) | |
(zipSame '(k ra) '(k2 rb)) | |
) | |
handle !sa with go sb | |
> Split [1,2,3,4] | |
<> Split [5,6,7] | |
|> zipSame (Split (range 1 8)) | |
|> Split.toList | |
> Split.toList <| keep (x -> x `mod` 2 == 0) (Split (range 0 20)) | |
> Split.toList <| mapSome (x -> Some (x + 12)) (Split (range 0 20)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
structural ability Split m where | |
empty! : x | |
both : m -> a -> a -> a | |
structural type Split.Step m a r | |
= Empty | |
| One a | |
| Two m r r | |
Split.metric : Reducer {} a m -> '{Split m,g} a ->{Split m,g} m | |
Split.metric R s = match step s with | |
Empty -> Reducer.zero R | |
One a -> Reducer.inject R a | |
Two m _ _ -> m | |
Split.fromList : Reducer {} a m -> [a] -> '{Split m} a | |
Split.fromList R as _ = match as with | |
[] -> empty! | |
[a] -> a | |
as -> | |
(l,r) = halve as | |
lt = fromList R l | |
rt = fromList R r | |
force (Split.append R lt rt) | |
Split.append! : Reducer {} a m -> '{Split m,g} a -> '{Split m,g} a ->{Split m,g} a | |
Split.append! R s1 s2 = | |
!(both (Reducer.op R (metric R s1) (metric R s2)) s1 s2) | |
Split.append : Reducer {} a m -> '{Split m,g} a -> '{Split m,g} a -> '{Split m,g} a | |
Split.append R s1 s2 _ = append! R s1 s2 | |
Split.toList : '{Split m,g} a ->{g} [a] | |
Split.toList s = | |
go = cases | |
{ a } -> [a] | |
{ empty! -> _ } -> [] | |
{ both _ l r -> k } -> | |
(handle k l with go) ++ (handle k r with go) | |
handle !s with go | |
Split.step : '{Split m,g} a ->{Split m,g} (Step m a ('{Split m,g} a)) | |
Split.step s = | |
go : Request {Split m} a ->{Split m,g} (Step m a ('{Split m,g} a)) | |
go = cases | |
{ a } -> One a | |
{ empty! -> _ } -> Empty | |
{ both m l r -> k } -> Two m ('(k l) : '{Split m,g} a) '(k r) | |
handle !s with go | |
Split.two : m -> '{Split m,g} a -> '{Split m,g} a -> '{Split m,g} a | |
Split.two m s1 s2 _ = !(both m s1 s2) | |
Split.search : (Either m a ->{Split m, g} Ordering) -> '{Split m, g} a -> '{Split m, g} a | |
Split.search f s _ = search! f s | |
Split.search! : (Either m a ->{Split m, g} Ordering) -> '{Split m, g} a ->{Split m, g} a | |
Split.search! f s = match step s with | |
Empty -> empty! | |
One a -> match f (Right a) with | |
Equal -> a | |
_ -> empty! | |
Two m l r -> match f (Left m) with | |
Less -> empty! | |
_ -> search! f (both m l r) | |
Split.map : (a ->{Split m,g} b) -> '{Split m, g} a -> '{Split m, g} b | |
Split.map f s _ = f !s | |
Split.keep : (a ->{Split m,g} Boolean) -> '{Split m, g} a -> '{Split m, g} a | |
Split.keep f s _ = | |
a = !s | |
if f a then a else empty! | |
Split.mapSome : (a ->{Split m,g} (Optional b)) -> '{Split m, g} a -> '{Split m, g} b | |
Split.mapSome f s _ = match f !s with | |
None -> empty! | |
Some b -> b | |
up.Reducer.new : (a ->{g} m) -> m -> (m -> m ->{g} m) -> Reducer g a m | |
up.Reducer.new f z op = Reducer f (Monoid z op) | |
-- > Split.toList <| 'empty! | |
{- | |
Split.innerJoin : (Either a k -> Either b k ->{g} Ordering) -> '{Split k,g} a -> '{Split k,g} b -> '{Split k,g} (a,b) | |
Split.innerJoin overlap s1 s2 _ = match overlap (metric s1) (metric s2) with | |
Equal -> todo "hmm" | |
_ -> empty! | |
-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- structural type T k a = Empty | Leaf a | Branch (T k a) (T k a) | K k (T k a) | |
{- | |
-- This one fuses map, filter, flatMap, can do append, but can't support | |
-- searching, joins, intersection. Should separate key type from the value type | |
structural ability S1 where | |
empty! : x | |
both : a -> a -> a | |
-} | |
-- | |
structural ability Split m where | |
empty! : x | |
both : a -> a -> a | |
summarize : m -> a -> a | |
structural type Split.Step m a r | |
= Empty | |
| One a | |
| Summarize m r | |
| Both r r | |
Split.search : (m ->{Split m,g} Ordering) -> '{Split m,g} a -> '{Split m,g} a | |
Split.search ord ix _ = | |
go : Request {Split m} x ->{Split m,g} x | |
go = cases | |
{ a } -> a | |
{ empty! -> _ } -> empty! | |
{ summarize m a -> resume } -> match ord m with | |
Equal -> handle resume a with go | |
_ -> empty! | |
{ both l r -> resume } -> | |
l' _ = handle resume l with go | |
r' _ = handle resume r with go | |
both l' r' () | |
handle !ix with go | |
Split.first : '{Split m,g} a ->{Split m,g} Optional a | |
Split.first ix = match step ix with | |
Empty -> None | |
One a -> Some a | |
Summarize _ r -> Split.first r | |
Both l _ -> Split.first l | |
Split.last : '{Split m,g} a ->{Split m,g} Optional a | |
Split.last ix = match step ix with | |
Empty -> None | |
One a -> Some a | |
Summarize _ r -> Split.last r | |
Both _ r -> Split.last r | |
Split.one : m -> a -> '{Split m,g} a | |
Split.one m a _ = summarize m a | |
Split.append! : '{Split m,g} a -> '{Split m,g} a ->{Split m,g} a | |
Split.append! ix1 ix2 = both ix1 ix2 () | |
Split.append : '{Split m,g} a -> '{Split m,g} a -> '{Split m,g} a | |
Split.append ix1 ix2 _ = both ix1 ix2 () | |
Split.toList : '{Split m,g} a ->{g} [a] | |
Split.toList ix = | |
go = cases | |
{ a } -> [a] | |
{ empty! -> _ } -> [] | |
{ summarize _ a -> k } -> handle k a with go | |
{ both l r -> k } -> | |
(handle k l with go) List.++ (handle k r with go) | |
handle !ix with go | |
Split.map : (a ->{Split m,g} b) -> '{Split m,g} a -> '{Split m,g} b | |
Split.map f a _ = f !a | |
Split.keepIf : (a ->{Split m,g} Boolean) -> '{Split m,g} a -> '{Split m,g} a | |
Split.keepIf f ix _ = | |
a = !ix | |
if f a then a else empty! | |
Split.aliases.Split.filter = keepIf | |
Split.mapSome : (a ->{Split m,g} Optional b) -> '{Split m,g} a -> '{Split m,g} b | |
Split.mapSome f a _ = match f !a with | |
None -> empty! | |
Some b -> b | |
Split.unstep! : Step m a ('{Split m,g} a) ->{Split m,g} a | |
Split.unstep! = cases | |
Empty -> empty! | |
One a -> a | |
Summarize m r -> summarize m r () | |
Both l r -> both l r () | |
Split.step : '{Split m,g} a ->{Split m,g} (Step m a ('{Split m,g} a)) | |
Split.step s = | |
go : Request {Split m} a ->{Split m,g} (Step m a ('{Split m,g} a)) | |
go = cases | |
{ a } -> One a | |
{ empty! -> _ } -> Empty | |
{ summarize m a -> k } -> Summarize m '(k a) | |
{ both l r -> k } -> Both ('(k l) : '{Split m,g} a) '(k r) | |
handle !s with go | |
Split.summary.root : '{Split m,g} a ->{Split m,g} Optional m | |
Split.summary.root ix = match step ix with | |
Summarize a _ -> Some a | |
_ -> None | |
Split.summary : (m -> m ->{Split m,g} m) -> '{Split m,g} a ->{Split m,g} Optional m | |
Split.summary op ix = match step ix with | |
Empty -> None | |
One _ -> None | |
Summarize m _ -> Some m | |
Both l r -> match (summary op l, summary op r) with | |
(None, None) -> None | |
(Some m1, Some m2) -> Some (op m1 m2) | |
(Some m, _) -> Some m | |
(_, Some m) -> Some m | |
Split.summaries : (m ->{} m ->{Split m,g} m) -> ['{Split m,g} a] ->{Split m,g} Optional m | |
Split.summaries op ixs = match List.somes (List.map (summary op) ixs) with | |
[] -> None | |
h +: t -> Some (List.foldLeft op h t) | |
Split.fromReduce : (a ->{Split m,g} m) -> (m -> m ->{Split m,g} m) -> [a] -> '{Split m,g} a | |
Split.fromReduce inj op as _ = match as with | |
[] -> empty! | |
[a] -> summarize (inj a) a | |
as -> | |
(l,r) = halve as | |
l' = Split.fromReduce inj op l | |
r' : '{Split m,g} a | |
r' = Split.fromReduce inj op r | |
match summaries op [l', r'] with | |
None -> both l' r' () | |
Some m -> summarize m (both l' r') () | |
Split : [a] -> '{Split m} a | |
Split as _ = match as with | |
[] -> empty! | |
[a] -> a | |
as -> | |
(l,r) = halve as | |
both (Split l) (Split r) () | |
Split.unfold : s -> (s ->{g} (Split.Step m a s)) -> '{Split m,g} a | |
Split.unfold s f _ = match f s with | |
Empty -> empty! | |
One a -> a | |
Summarize m s -> summarize m (unfold s f) () | |
Both l r -> both (unfold l f) (unfold r f) () | |
> Split [1,2,3,4,5,6] | |
|> Split.map (x -> x * 100) | |
|> keepIf (x -> x < 500) | |
|> Split.toList | |
Split.withSummary : '{Split m,g} a -> '{Split m,g} (a,Optional m) | |
Split.withSummary ix _ = | |
go : Optional m -> Request {Split m} a ->{Split m,g} (a, Optional m) | |
go m = cases | |
{ a } -> (a, m) | |
{ empty! -> _ } -> empty! | |
{ both l r -> k } -> | |
l' _ = handle k l with go m | |
r' : '{Split m,g} (a,Optional m) | |
r' _ = handle k r with go m | |
both l' r' () | |
{ summarize m a -> k } -> | |
a' _ = handle k a with go (Some m) | |
summarize m a' () | |
handle !ix with go None | |
Split.accumulate : (a ->{g} m) -> (m -> m ->{g} m) -> '{Split m,g} a -> '{Split m,g} a | |
Split.accumulate inj op ix _ = match step ix with | |
Empty -> empty! | |
One a -> summarize (inj a) a | |
Summarize a r -> summarize a r () | |
Both l r -> | |
l' = accumulate inj op l | |
r' : '{Split m,g} a | |
r' = accumulate inj op r | |
match summaries op [l',r'] with | |
None -> both l' r' () | |
Some m -> summarize m () | |
both l' r' () | |
{- | |
Split.joinBy : (m -> m ->{g} Ordering) -> '{Split m,g} a -> '{Split m,g} b -> '{Split m,g} (a, b) | |
Split.joinBy ord ixa ixb _ = | |
go : Boolean | |
-> [(Optional m, '{Split m,g} a)] | |
-> [(Optional m, '{Split m,g} b)] | |
-> {Split m,g} (a,b) | |
go breakA = cases | |
[], _ -> empty! | |
_, [] -> empty! | |
(None,_) +: as, _ +: bs -> go breakA as bs | |
_ +: as, (None,_) +: bs -> go breakA as bs | |
as0@((Some m1, a) +: as), bs0@((Some m2, b) +: bs) -> | |
match ord m1 m2 with | |
Less -> go as bs0 | |
Greater -> go as0 bs | |
Equal -> | |
if breakA then match step a with | |
break : '{Split m,g} x ->{Split m,g} ['(Optional m, '{Split m,g} x)] | |
break ix = match step ix with | |
Empty -> [] | |
One a -> [(None, 'a)] | |
Summarize | |
go [(summary.root ixa, ixa)] [(summary.root ixb, ixb)] | |
- |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment