atacratic

-- Aim is to make a handler for https://share.unison-lang.org/latest/types/distributed/up/async/Async
-- that works for tests and docs, so, a pure scheduler.

-- Key problem is how to make the types work in scheduleHandler.
-- - the awaitCompletion case is producing a 'resume' value - the continuation for 
--   how some task will resume after its call to tryAwait completes
-- - the completeTask case is producing a 'result' value - the output of some task, 
--   let's say one that another task is waiting on.
-- The latter has type 'Either Failure a', for some type a matching the return type
-- of the task.  The former wants to consume an 'Either Failure a'.  So it's 'just'

atacratic

-- Contains a piece of state which can be written and read from different tasks.
type Cell a = Cell (Channel (CellProto a))

type CellProto a = Read (Channel a) | Write a

example = 'let
  c = Cell.new 1
  f = 'let
    Cell.write 2 c
  g = 'let

atacratic

-- Sketch of algebraic laws property testing, using explicit encoding for typeclass instances (Unison language)

type base.Monoid a = {
  mempty : a,
  mplus : a -> a -> a
}

type base.Monoid.Laws a = {
  leftIdentity : Monoid a -> a -> Boolean,
  rightIdentity : Monoid a -> a -> Boolean,

atacratic

-- An example multihandler.
-- Pipe messages out of the first argument computation into the second.
pipe : Request (Send m) () -> Request (Receive m) a ->{Abort} a
pipe sender receiver =
  case receiver of
    { Receive.receive -> kr } ->
      case sender of
        { Send.send m -> ks } -> pipe (step ks) (step '(kr m))
        { _ } -> Abort.abort
    { a } -> a

atacratic

This tutorial explains how Unison handles 'effectful' computations, like storing state or performing I/O, using abilities. It assumes you haven't come across abilities before, and covers everything from the ground up.

This is an unofficial tutorial, written before the one on unisonweb.org/docs. The approach taken here is slow and methodical. Your first stop should be the official tutorial, if you haven't seen it already.

This doc is a Unison transcript - the source is here.

Terminology note: other languages with ability systems typically call them 'effect handlers' or 'algebraic effects', but many of the ideas are the same.

Introducing abilities

atacratic

chris@chris-ubuntu:~/unison$ git difftool HEAD HEAD^1

This message is displayed because 'diff.tool' is not configured.
See 'git difftool --tool-help' or 'git help config' for more details.
'git difftool' will now attempt to use one of the following tools:
meld opendiff kdiff3 tkdiff xxdiff kompare gvimdiff diffuse diffmerge ecmerge p4merge araxis bc codecompare emerge vimdiff

Viewing (1/1): 'parser-typechecker/src/Unison/Codebase/TranscriptParser.hs'
Launch 'bc' [Y/n]? Y
The diff tool bc is not available as 'bcompare'

atacratic

This is a case that might help motivate support in Unison for ability sets where multiple abilities share the same head type constructor.

In a nutshell the point is that ability sets like {Exception Foo, Exception Bar} arise naturally when composing functions. So weak support for those ability sets bakes a barrier to compositionality into the language.

Let's suppose we're using the Exception ability.

ability Exception e where
  throw : e -> a

atacratic

-- This gist demonstrates a prototype IO proxy handler for record/replay.  
-- The hope is to get some version of this into unisonbase someday.  
--
-- More motivation and explanation is at https://github.com/unisonweb/unison/issues/258.
--
-- It currently only handles a few IO primitives - there's a bunch of boilerplate code 
-- needed to handle the rest.  And see 'Limitations' below for issues coming out of this
-- prototyping.  
-- 
-- The aim is to provide the following:

atacratic

reviewing Unison's LanguageReference.md master@81b65b, i.e. this

Overall:

• This doc is awesome: nicely written, thorough, not trying to be too formal, nice use of examples.
• It needs a table of contents to give the reader an overview.

In ‘type signature’:

• say that Nat means natural number, and that that means whole numbers starting at zero
• ‘meets’->’matches’?

atacratic

Here's a question on using the Unison language.

I wanted to play around with defining APIs for data sources/sinks/feeds etc, but I hit a wall. I don't know how I should define an API in unison without tying down the underlying datatype used to implement it.

As a example, consider the following bit of Haskell.

-- let's ignore for the purposes of this discussion whether this is a wise definition of a stream...
class StreamT s where
 get :: s a -> (a, s a)