Chris Gibbs 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

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'

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

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’?

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 -&gt; (a, s a)

	-- 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'

	-- 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

	-- 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,

	-- 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

	-- 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: