pchiusano

{{
  ``List.selectBy o k as`` yields the same results as ``List.at k sorted`` 
  where ''sorted'' is a sorted version of ''as'', but in (expected) linear time
  without fully sorting the list.

  ```
  List.selectBy Universal.ordering 2 [4,1,3,2,5]
  ```

  ```

pchiusano

{{ 
  ``task.pure a`` creates a task that returns ''a'' on {Remote.await}. 

  That is, {{docExample 1 '(a -> Remote.await (task.pure a) === a) }}
}}
Remote.task.pure : a -> t a
Remote.task.pure a = 
  t = Remote.empty! 
  task.complete (Right a)
  t

pchiusano

structural ability Split where
  skip! : x
  both : a -> a -> a

Split! : [a] ->{Split} a
Split! = cases
  [] -> skip!
  [a] -> a
  as ->
    (l,r) = halve as

pchiusano

> Async.pure.run 'let
  List.parMap (x -> x*10) [1,2,3,4,5] 

> Async.pure.run 'let
  use Async put fork await empty!
  tr = empty!
  t1 = fork '(await tr + 1)
  t2 = fork '(put 9 tr)
  Async.await t1

pchiusano

unique ability Located d where
  location : d a -> Location {} 

unique ability Storage.Distributed d where
  restore : d a -> a
  save : a -> d a
  saveNear : d x -> a -> d a

unique type Kit d m a
  = Empty

pchiusano

# I version my full namespace tree here, it's a snapshot
# of all my current workstreams. If I need to switch
# computers, I might just push here, then pull on the
# other computer.
# `.> push` will go here.
GitUrl = "git@github.com:pchiusano/unisoncode"

# GitUrl {
# 
#   # Some projects I occasionally make PRs against.

pchiusano

-- splittable RNG type
ability Random where
  nat : Nat
  split : {Random} (forall g a. '{Random,g} a ->{g} a)

{{ ``Random.natIn i j`` generates a {type Nat} between ''i'' and ''j'', 
   not including ''j''.

   If ''j'' is less than or equal to ''i'', throws an error.

pchiusano

ability Each where
  each : [a] -> a

Each.toStream.handler : Request {Each} a ->{Stream a} ()
Each.toStream.handler = cases
  { a } -> Stream.emit a
  { Each.each as -> resume } -> match as with
    [] -> ()
    a +: as ->
      handle resume a with Each.toStream.handler

pchiusano

-- Ability to range over all the elements of a list
ability Each where
  each : [a] -> a

-- Implementation detail - standard early termination ability
ability Abort where abort : x

-- Here's a first usage. `each` lets us traverse multiple lists 
-- elementwise, matching up values at corresponding indices.
> handle 

pchiusano

-- porting https://hackage.haskell.org/package/splitmix-0.1.0.1/docs/src/System.Random.SplitMix.html
-- could use a native popcount / hamming weight instruction

roll : Nat -> Nat ->{Random} Nat
roll n sides =
  Nat.sum (List.replicate n '(Random.natIn sides + 1))

-- example, rolling 3 x d8
> Random.splitmix 10349 '(roll 3 8)