unison/unison-src/demo/3.u

type Future a = Future ('{Remote} a)

-- A simple distributed computation ability
ability Remote where

  -- Spawn a new node
  spawn : {Remote} Node

  -- Start evaluating a computation on another node
  at : Node -> '{Remote} a ->{Remote} Future a

type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair

force : Future a ->{Remote} a
force f = case f of Future.Future r -> !r

-- Let's test out this beast! do we need to deploy our code to some EC2 instances??
-- Gak, no not yet, we just want to test locally, let's write a handler
-- for the `Remote` ability that simulates everything locally!

Remote.runLocal : '{Remote} a -> a
Remote.runLocal r =
  use Future Future
  step nid r = case r of
    {Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
    {Remote.at _ t -> k} -> handle (step nid) in k (Future t)
    {a} -> a -- the pure case
  handle (step (Node.Node 0)) in !r

use Optional None Some
use Monoid Monoid
use Sequence ++

Sequence.map : (a ->{e} b) -> [a] ->{e} [b]
Sequence.map f as =
  go f acc as i = case at i as of
    None -> acc
    Some a -> go f (acc `snoc` f a) as (i + 1)
  go f [] as 0

type Monoid a = Monoid (a -> a -> a) a

Monoid.zero m = case m of Monoid.Monoid op z -> z
Monoid.op   m = case m of Monoid.Monoid op z -> op

Monoid.orElse m a = case a of
  None -> Monoid.zero m
  Some a -> a

uncons : [a] -> Optional (a, [a])
uncons as = case at 0 as of
  None -> None
  Some hd -> Some (hd, drop 1 as)

dreduce : Monoid a -> [a] ->{Remote} a
dreduce m a =
  if size a < 2 then Monoid.orElse m (Sequence.at 0 a)
  else
    l = Remote.at Remote.spawn '(dreduce m (take (size a / 2) a))
    r = Remote.at Remote.spawn '(dreduce m (drop (size a / 2) a))
    Monoid.op m (force l) (force r)

dmapReduce : (a ->{Remote} b) -> Monoid b -> [a] ->{Remote} b
dmapReduce f m as = dreduce m (Sequence.map f as)

dsort2 : (a -> a -> Boolean) -> [a] ->{Remote} [a]
dsort2 lte as =
  dreduce (Monoid (merge lte) [])
          (Sequence.map (a -> [a]) as)

halve : [a] -> ([a], [a])
halve s = splitAt (size s / 2) s

splitAt : Nat -> [a] -> ([a], [a])
splitAt n as = (take n as, drop n as)

Node.increment : Node -> Node
Node.increment n =
  use Node.Node -- the constructor
  case n of Node n -> Node (n + 1)

merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
merge lte a b =
  go out a b = case (uncons a, uncons b) of
    (None,_) -> out ++ b
    (_,None) -> out ++ a
    (Some (hA, tA), Some (hB, tB)) ->
      if hA `lte` hB then go (out `snoc` hA) tA b
      else go (out `snoc` hB) a tB
  go [] a b

> merge (<) [1,3,4,99,504,799] [0,19,22,23]

sort : (a -> a -> Boolean) -> [a] -> [a]
sort lte as =
  if size as < 2 then as
  else case halve as of (left, right) ->
    l = sort lte left
    r = sort lte right
    merge lte l r

dsort : (a -> a -> Boolean) -> [a] ->{Remote} [a]
dsort lte as =
  use Remote at spawn
  if size as < 2 then as
  else case halve as of (left, right) ->
    r1 = at spawn '(dsort lte left)
    r2 = at spawn '(dsort lte right)
    merge lte (force r1) (force r2)

> sort (<) [1,2,3,234,6,2,4,66,2,33,4,2,57]

> Remote.runLocal '(dsort (<) [1,2,3,234,6,2,4,66,2,33,4,2,57])