docs/surface.rst - 3p/nicta/cogent - Git at Google

 =====================
 Cogent Surface Syntax
 =====================

 .. note:: For new users of this language, this section is not intended to be a
           tutorial for the language. It merely introduces its surface syntax and
           should be used as a reference while using the language.

 .. note:: As described in `#324 <https://github.com/NICTA/cogent/issues/324>`_,
           we are in the progress of revising the surface sytnax. So it's subject
           to change in near future.


 Types
 =====

 All type names must begin with an uppercase letter. Tuple, Function,
 Record and Variant types have special syntax.

 Record types
 ------------

 Now indicated by a series of typing declarations inside braces, e.g

 ::

     {x : A, y : B}

 If a field ``f`` is removed by ``take``, the postfix type operator
 ``take f`` may be used:

 ::

     {x : A, y : B} take x

 This works, even if the type on the LHS is a type synonym (c.f. :ref:`typedefs`).

 Sugar: Taking multiple fields:

 ::

     {x : A, y : B} take (x,y) -- parens mandatory

 ::

     {x : A, y : B} take (..)  -- parens mandatory

 This ``(..)`` sugar means to take all currently untaken fields (if any).

 Similarly, we can write ``put`` instead of ``take`` with the same
 syntax. ``put`` is dual to ``take``. One common usage would be

 ::

     ({x : A, y : B, z : C, u : D, w : E} take (..)) put x

 Note that the parentheses around the record and first ``take`` is mandatory.
 Arbitrary many levels of nestings is possible.

 Unboxed records
 ---------------

 Unboxed records are pretty much like regular records, except that their
 wrappers (i.e. the unboxed container) are lightweight that no allocation
 is required.

 The syntax is simple, just a prefixing ``#`` on its counterpart record
 type. ``take``, ``put`` operations (and punning) and member extraction
 are of exactly the same syntax as regular records. As a consequence of
 its lightweightness, we can construct and deconstruct (by means of
 pattern matching) unboxed records, just as what we do on tuples (see
 :ref:`product-types` for tuples).

 E.g.,

 ::

     #{x : A, y : B}    -- type
     #{x = e1, y = e2}  -- expression or pattern
     a.x                -- member
     a {x = f}          -- take and put, same as regular records

 About its *permission* rules (see :ref:`permissions`):
 the wrapper per se is non-linear (i.e. shareable
 and discardable). If
 any linear fields are present (untaken), then the unboxed record becomes
 linear. Member operation can only be used if there're no linear
 fields inside, or the unboxed record is banged (``!``).

 Unboxed abstract types
 ----------------------

 The ``#`` sigil is not used in the declaration of an unboxed abstract
 type. Instead, we attach the ``#`` sigil when the type is used. E.g.:

 ::

     type A
     type T = {a : #A, b : A}

 In the above case, field ``a`` is unboxed, whereas ``b`` is not. When
 generating C code, boxed abstract types will be pointers, unboxed are
 not. It's the users' responsibility to keep the C code consistent, as
 these types are abstract.

 Bang (``!``)
 ------------

 Record types and abstract types have *sigils*, but outwardly, a *Write*
 sigil is just a plain record type / abstract type, and an *Observe* (or *Readonly*) sigil
 would be indicated with a postfix bang, for example: ``{x : A, y : B}!``, ``C!``.

 The postfix bang operator can be applied to any type, which converts all
 write sigils to readonly sigils internally (and any type variables to
 readonly type variables).

 To bang a parametric type, the type must be surrounded by parentheses,
 otherwise ``!`` will be applied to the type parameter right before the
 ``!`` symbol.

 .. _product-types:

 Product Types
 -------------

 Nameless, unboxed tuples may be used everywhere you like. Their syntax
 is identical to Haskell. A unit type (which is freely discardable and
 not linear) also exists, ``()`` with a value ``()``. Tuples are not
 associative, namely ``(a, b, c, d) /= (a, (b, (c, d)))`` and
 ``(a, b, c, d) /= (((a, b), c), d)``, just as in Haskell.

 Variant Types
 -------------

 Variant types look like this.

 ::

     < Ok (Obj, Heap) | Fail Heap >

 They can be constructed using ``Ok (obj,h)``, or ``Fail e``.

 We can determine from context if ``Identifier`` (``Ok`` and ``Fail`` in
 the example above) is a type or a data constructor, much like Haskell.
 We will have to do a little bit of inference to determine which variant
 type the thing actually belongs to.

 They can have as many alternatives as you like, and there is no
 restriction on what goes inside a variant type. Each alternative can
 take any number of arguments (0 or more). They will be desugared to
 tuples of all the arguments. E.g.:

 ::

     <Ok Obj U8 | Fail >  -- equiv to <Ok (Obj, U8) | Fail ()>

 Polymorphic types
 -----------------

 Types can contain variables. Functions may be declared as having
 polymorphic type.

 ::

     size : all (k, v). Map k v -> U32

 Monomorphic functions are first class, but to get a monomorphic function
 from a polymorphic function requires instantiation, e.g ``length[Int]``.
 Since Cogent-2.0.9, explicit type applications are not mandatory,
 although in some cases they must be supplied to guide the type inference
 engine. Type applications can be partial, or with type holes. For
 example, ``foo [_, A, B]``; ``foo [S, T, _]`` is equivalent to ``foo [S,T]``.

 A type variable under observation (i.e ``let!``-ed) is annotated with a
 prefix bang (e.g ``!a``)

 .. _permissions:

 Permissions
 ~~~~~~~~~~~

 *Permissions* (they used to be called "kinds") are provided for
 polymorphic signatures as follows:

 ::

     length : all (a :< k). Array a -> U32

 Permissions are internally a set of three booleans: whether or not the
 type can be:

 -  ``D`` for Discard (i.e by weakening)
 -  ``S`` for Share   (i.e by contraction)
 -  ``E`` for Escape  (i.e returned from ``let!``)

 The permission signature on a type variable is more like a constraint.
 They are some combination of those three letters. If no permission
 is provided, it is assumed that none of those permissions are required,
 and the value will be linear and cannot escape a ``let!``.

 .. _typedefs:

 Type synonyms
 =============

 Type synonyms may be provided using the ``type`` keyword as follows:

 ::

     type X a b = { foo : a, bar : b, baz : Int }

 The type synonym ``X`` must always be fully saturated with its two
 arguments wherever it is used, however.

 Abstract types (defined in C) may also be declared, and they also may
 take parameters. This corresponds to a family of types in C.

 ::

     type Buffer
     type Array a

 Constants and top-level definitions
 ===================================

 Constants are mono-typed.

 ::

     abc : U8
     abc = 3

 But the right hand side can be much more expressive now, with let
 bindings and whatnot. We must be able to prevent users from doing
 side-effects like allocation in the top-level---see :ref:`effects`.

 To make the syntax easier to parse, a function or constant's body must
 be indented by at least one space. This means that any non-indented
 bareword is the start of a new definition or signature.

 .. _effects:

 Effects
 =======

 Most effects are currently (successfully) modelled via linear types. For
 allocation, Cogent does not know anything about it. Memory management
 involves the heap. I propose modelling the heap as an explicit linear
 value, just as with any other state.

 Allocation functions must take and return a linear heap, as they
 modify it:

 ::

     allocateObj : Heap -> < Ok Obj Heap | Fail Heap >

 Special syntax for allocation functions and automating heap-threading
 are nice to have, so I welcome proposals.


 Expression language
 ===================

 Matching and Error Handling
 ---------------------------

 Matching may be accomplished by the following syntax:

 ::

     f : Heap -> < Ok Obj Heap | Fail Heap >
     f h = allocateobj h
         | Ok obj h => allocateobj h
             | Ok obj' h => Ok (mergeObj (obj, obj')) h
             | Fail h -> let () = free obj in Fail h
         | Fail h -> Fail h

 This is an alignment-based syntax, grouping determined based on the
 alignment of the bars.

 The rightward arrows for each case can either be ``=>`` or ``->``.
 ``=>`` indicates that that branch is likely, to enable compiler
 optimisations. ``~>`` can also be used to indicate an unlikely branch.

 A pattern may be ``_`` but only if the kind of the value allows it to be
 discarded.

 Biased pattern matching
 -----------------------

 The syntax above poses a problem if many levels of nestings occur---you
 will end up with cascading matches which indent a lot. To solve this
 problem, we allow a syntax for early exit, which is inspired by `Idris <https://www.idris-lang.org/>`_.
 The syntax looks like:

 ::

     f : Heap -> <Ok Obj Heap | Fail Heap>
     f h = let Ok obj  h <= allocateobj h |> Fail h -> Fail h
           and Ok obj' h <= allocateobj h |> Fail h -> let _ = free obj in Fail h
            in Ok (mergeObj (obj, obj')) h

 This piece of code is semantically identical to the one above. ``<=``
 matches the major case, and ``|>`` bails out with the minor case.

 Patterns
 --------

 Patterns may be refutable (could fail, e.g ``Ok a`` or ``43``) or
 irrefutable (always match, e.g ``(a,b)`` or ``_``). Refutable patterns
 can be used in a matching block only, but they can only nest irrefutable
 patterns. So, unlike in Haskell, you can't go:

 ::

     f x = foo x
       | Ok (Alt1 3) -> bar
       | _ -> baz

 As this nests a refutable pattern (``3``) inside another refutable
 pattern (``Alt1 3``) inside another refutable pattern (``Ok (Alt1 3)``).

 This is forbidden to make compilation much more straightforward in the
 presence of linear types.

 Let-binding
 -----------

 Let expressions take the form of ML. They are not ever recursive.
 Multiple let-bindings can be introduced by separating them with ``and``:

 ::

     f () = let x = 3
            and y = 4
             in foo (x,y)

 Is equivalent to:

 ::

     f () = let x = 3
             in let y = 4
                 in foo (x,y)

 Irrefutable single patterns may occur on the left hand side of let-binding, but
 refutable patterns must use regular pattern matching.

 To force inference to go the way you want, a type signature can be
 provided for a let binding:

 ::

     f () = let x : U8 = 3
             in let y : U16 = 4
                 in foo (x,y)

 Observation and ``let!``
 ------------------------

 Variables may be observed using ``!``:

 ::

     f (x, y) = let (a,b) = foo (x, y) !x !y
                 in bar (a, b)

 Prefix ``!`` annotations can be used inline with pattern matching also:

 ::

     f (x,y) = foo(x,y) !x !y
               | Blah x  => bar x
               | Blorp z -> baz z

 If
 --

 Conditionals can be expressed in the form of if-expressions. They are in
 the form of ``if c !v1 !v2 ... then e1 else e2``. The ``!v``\ s are
 similar to the ``!`` syntax introduced above, allowing for temporary
 access to linear objects in the condition.

 Apart from the normal if-then-else syntax, Cogent offers a multi-way if
 syntax, inspired by GHC/Haskell. For example,

 ::

     if | cond_1 -> expr_1
        | cond_2 -> expr_2
        | ...
        | else   -> expr_n

 In the code snippet above, the conditions are Boolean **expressions**,
 instead of patterns as one might think. The final ``else`` is part of
 the syntax. The pipes have to be aligned. The arrows, as usual, can be
 any of ``=>``, ``->`` or ``~>``, which have the same semantics as used
 in alternatives. Prefix ``!``\ s can be added after each condition (but
 not after the ``else`` keyword), like ``| cond_1 !v1 !v2 => e``.

 Sequencing
 ----------

 Occasionally, it is useful to free a bunch of things, and using ``let`` for
 this purpose can be somewhat annoying:

 ::

     f : (Obj, Obj) -> Int
     f (a, b) = let _ = free a
                and _ = free b
                 in 42

 So, a little sugar is added for a series of discarding let bindings:

 ::

     f : (Obj, Obj) -> Int
     f (a, b) = free a; free b; 42

 These two expressions are equivalent.


 Records
 --------
 Unboxed records are initialized as follows:

 ::
     #{x = e1, y = e2}

 Boxed records are allocated on the heap. They are typically initialized by
 first calling the external C malloc function and then updating the record
 using the put operation.

 Take/put
 --------

 There is pattern syntax for ``take``, and a similar expression syntax
 for ``put``:

 ::

     f : {a : Foo, b : Bar} -> {a : Foo, b : Bar}
     f (r {a = ra, b = rb}) = r {a = ra, b = rb}

 .. note:: ``take`` is always in patterns (i.e. LHS of ``=``), whereas
           ``put`` is always in expressions (i.e. RHS of ``=``).

 Punning is also allowed:

 ::

     f : {a : Foo, b : Bar} -> {a : Foo, b : Bar}
     f (r {a, b}) = r {a, b}

 (where just ``a`` is equivalent to ``a = a``)

 Arithmetic and comparison operators
 -----------------------------------

 Currently Cogent will use the smallest type possible for integer
 literals and generate upcasts (but not downcasts) automatically when
 used in a context where they are required. For non-literals, an explicit
 ``upcast`` primitive may be needed.

 Type annotations
 ----------------

 To guide the type inference engine, the user can give type annotations
 to any expressions. The syntax is ``e : t``.


 Experimental features
 =====================

 .. warning:: Experimental features, as they are called, are indeed experimental,
              which means they are not stable, and may fail, terribly. Don't rely on them
              until they become stable.

 .. _static-arrays:

 Static arrays
 -------------

 .. note:: This feature is not implemented on the ``master`` branch. It's implemented
           on the ``array`` branch and needs to be enabled by the ``--builtin-arrays`` flag
           (see :ref:`optional-features` for more information on how to do that).

 Array literals can be introduced using square brackets, like
 ``[a, b, c]``. This syntax can also be used as patterns. Array types can
 be defined like ``U8[3]``, similar to C. Indexing can be made with the
 ``@`` operator. E.g.: ``arr @ 3``. Arrays can also be ``take``\ n and ``put``.
 The type-level ``take`` and ``put`` operators are spelt as ``@take`` and ``@put``
 respectively. On the term level, it's written as ``arr @{ @idx = val }``---
 just prefix the open bracket and the indices with ``@`` symbols, and the rest
 are the same as those for records.


 Lambda expressions
 ------------------

 We only allow for a very limited form of lambda expressions. A lambda
 expression has the syntax ``\irref => exp``, where ``irref`` is an
 irrefutable pattern, and ``exp`` is an expression which does not refer
 to any variables outside the lambda binding (no free variables). The
 bound variables have to be non-linear.
	=====================
	Cogent Surface Syntax
	=====================

	.. note:: For new users of this language, this section is not intended to be a
	tutorial for the language. It merely introduces its surface syntax and
	should be used as a reference while using the language.

	.. note:: As described in `#324 <https://github.com/NICTA/cogent/issues/324>`_,
	we are in the progress of revising the surface sytnax. So it's subject
	to change in near future.


	Types
	=====

	All type names must begin with an uppercase letter. Tuple, Function,
	Record and Variant types have special syntax.

	Record types
	------------

	Now indicated by a series of typing declarations inside braces, e.g

	::

	{x : A, y : B}

	If a field ``f`` is removed by ``take``, the postfix type operator
	``take f`` may be used:

	::

	{x : A, y : B} take x

	This works, even if the type on the LHS is a type synonym (c.f. :ref:`typedefs`).

	Sugar: Taking multiple fields:

	::

	{x : A, y : B} take (x,y) -- parens mandatory

	::

	{x : A, y : B} take (..) -- parens mandatory

	This ``(..)`` sugar means to take all currently untaken fields (if any).

	Similarly, we can write ``put`` instead of ``take`` with the same
	syntax. ``put`` is dual to ``take``. One common usage would be

	::

	({x : A, y : B, z : C, u : D, w : E} take (..)) put x

	Note that the parentheses around the record and first ``take`` is mandatory.
	Arbitrary many levels of nestings is possible.

	Unboxed records
	---------------

	Unboxed records are pretty much like regular records, except that their
	wrappers (i.e. the unboxed container) are lightweight that no allocation
	is required.

	The syntax is simple, just a prefixing ``#`` on its counterpart record
	type. ``take``, ``put`` operations (and punning) and member extraction
	are of exactly the same syntax as regular records. As a consequence of
	its lightweightness, we can construct and deconstruct (by means of
	pattern matching) unboxed records, just as what we do on tuples (see
	:ref:`product-types` for tuples).

	E.g.,

	::

	#{x : A, y : B} -- type
	#{x = e1, y = e2} -- expression or pattern
	a.x -- member
	a {x = f} -- take and put, same as regular records

	About its permission rules (see :ref:`permissions`):
	the wrapper per se is non-linear (i.e. shareable
	and discardable). If
	any linear fields are present (untaken), then the unboxed record becomes
	linear. Member operation can only be used if there're no linear
	fields inside, or the unboxed record is banged (``!``).

	Unboxed abstract types
	----------------------

	The ``#`` sigil is not used in the declaration of an unboxed abstract
	type. Instead, we attach the ``#`` sigil when the type is used. E.g.:

	::

	type A
	type T = {a : #A, b : A}

	In the above case, field ``a`` is unboxed, whereas ``b`` is not. When
	generating C code, boxed abstract types will be pointers, unboxed are
	not. It's the users' responsibility to keep the C code consistent, as
	these types are abstract.

	Bang (``!``)
	------------

	Record types and abstract types have sigils, but outwardly, a Write
	sigil is just a plain record type / abstract type, and an Observe (or Readonly) sigil
	would be indicated with a postfix bang, for example: ``{x : A, y : B}!``, ``C!``.

	The postfix bang operator can be applied to any type, which converts all
	write sigils to readonly sigils internally (and any type variables to
	readonly type variables).

	To bang a parametric type, the type must be surrounded by parentheses,
	otherwise ``!`` will be applied to the type parameter right before the
	``!`` symbol.

	.. _product-types:

	Product Types
	-------------

	Nameless, unboxed tuples may be used everywhere you like. Their syntax
	is identical to Haskell. A unit type (which is freely discardable and
	not linear) also exists, ``()`` with a value ``()``. Tuples are not
	associative, namely ``(a, b, c, d) /= (a, (b, (c, d)))`` and
	``(a, b, c, d) /= (((a, b), c), d)``, just as in Haskell.

	Variant Types
	-------------

	Variant types look like this.

	::

	< Ok (Obj, Heap) \| Fail Heap >

	They can be constructed using ``Ok (obj,h)``, or ``Fail e``.

	We can determine from context if ``Identifier`` (``Ok`` and ``Fail`` in
	the example above) is a type or a data constructor, much like Haskell.
	We will have to do a little bit of inference to determine which variant
	type the thing actually belongs to.

	They can have as many alternatives as you like, and there is no
	restriction on what goes inside a variant type. Each alternative can
	take any number of arguments (0 or more). They will be desugared to
	tuples of all the arguments. E.g.:

	::

	<Ok Obj U8 \| Fail > -- equiv to <Ok (Obj, U8) \| Fail ()>

	Polymorphic types
	-----------------

	Types can contain variables. Functions may be declared as having
	polymorphic type.

	::

	size : all (k, v). Map k v -> U32

	Monomorphic functions are first class, but to get a monomorphic function
	from a polymorphic function requires instantiation, e.g ``length[Int]``.
	Since Cogent-2.0.9, explicit type applications are not mandatory,
	although in some cases they must be supplied to guide the type inference
	engine. Type applications can be partial, or with type holes. For
	example, ``foo [_, A, B]``; ``foo [S, T, _]`` is equivalent to ``foo [S,T]``.

	A type variable under observation (i.e ``let!``-ed) is annotated with a
	prefix bang (e.g ``!a``)

	.. _permissions:

	Permissions
	~~~~~~~~~~~

	Permissions (they used to be called "kinds") are provided for
	polymorphic signatures as follows:

	::

	length : all (a :< k). Array a -> U32

	Permissions are internally a set of three booleans: whether or not the
	type can be:

	- ``D`` for Discard (i.e by weakening)
	- ``S`` for Share (i.e by contraction)
	- ``E`` for Escape (i.e returned from ``let!``)

	The permission signature on a type variable is more like a constraint.
	They are some combination of those three letters. If no permission
	is provided, it is assumed that none of those permissions are required,
	and the value will be linear and cannot escape a ``let!``.

	.. _typedefs:

	Type synonyms
	=============

	Type synonyms may be provided using the ``type`` keyword as follows:

	::

	type X a b = { foo : a, bar : b, baz : Int }

	The type synonym ``X`` must always be fully saturated with its two
	arguments wherever it is used, however.

	Abstract types (defined in C) may also be declared, and they also may
	take parameters. This corresponds to a family of types in C.

	::

	type Buffer
	type Array a

	Constants and top-level definitions
	===================================

	Constants are mono-typed.

	::

	abc : U8
	abc = 3

	But the right hand side can be much more expressive now, with let
	bindings and whatnot. We must be able to prevent users from doing
	side-effects like allocation in the top-level---see :ref:`effects`.

	To make the syntax easier to parse, a function or constant's body must
	be indented by at least one space. This means that any non-indented
	bareword is the start of a new definition or signature.

	.. _effects:

	Effects
	=======

	Most effects are currently (successfully) modelled via linear types. For
	allocation, Cogent does not know anything about it. Memory management
	involves the heap. I propose modelling the heap as an explicit linear
	value, just as with any other state.

	Allocation functions must take and return a linear heap, as they
	modify it:

	::

	allocateObj : Heap -> < Ok Obj Heap \| Fail Heap >

	Special syntax for allocation functions and automating heap-threading
	are nice to have, so I welcome proposals.


	Expression language
	===================

	Matching and Error Handling
	---------------------------

	Matching may be accomplished by the following syntax:

	::

	f : Heap -> < Ok Obj Heap \| Fail Heap >
	f h = allocateobj h
	\| Ok obj h => allocateobj h
	\| Ok obj' h => Ok (mergeObj (obj, obj')) h
	\| Fail h -> let () = free obj in Fail h
	\| Fail h -> Fail h

	This is an alignment-based syntax, grouping determined based on the
	alignment of the bars.

	The rightward arrows for each case can either be ``=>`` or ``->``.
	``=>`` indicates that that branch is likely, to enable compiler
	optimisations. ``~>`` can also be used to indicate an unlikely branch.

	A pattern may be ``_`` but only if the kind of the value allows it to be
	discarded.

	Biased pattern matching
	-----------------------

	The syntax above poses a problem if many levels of nestings occur---you
	will end up with cascading matches which indent a lot. To solve this
	problem, we allow a syntax for early exit, which is inspired by `Idris <https://www.idris-lang.org/>`_.
	The syntax looks like:

	::

	f : Heap -> <Ok Obj Heap \| Fail Heap>
	f h = let Ok obj h <= allocateobj h \|> Fail h -> Fail h
	and Ok obj' h <= allocateobj h \|> Fail h -> let _ = free obj in Fail h
	in Ok (mergeObj (obj, obj')) h

	This piece of code is semantically identical to the one above. ``<=``
	matches the major case, and ``\|>`` bails out with the minor case.

	Patterns
	--------

	Patterns may be refutable (could fail, e.g ``Ok a`` or ``43``) or
	irrefutable (always match, e.g ``(a,b)`` or ``_``). Refutable patterns
	can be used in a matching block only, but they can only nest irrefutable
	patterns. So, unlike in Haskell, you can't go:

	::

	f x = foo x
	\| Ok (Alt1 3) -> bar
	\| _ -> baz

	As this nests a refutable pattern (``3``) inside another refutable
	pattern (``Alt1 3``) inside another refutable pattern (``Ok (Alt1 3)``).

	This is forbidden to make compilation much more straightforward in the
	presence of linear types.

	Let-binding
	-----------

	Let expressions take the form of ML. They are not ever recursive.
	Multiple let-bindings can be introduced by separating them with ``and``:

	::

	f () = let x = 3
	and y = 4
	in foo (x,y)

	Is equivalent to:

	::

	f () = let x = 3
	in let y = 4
	in foo (x,y)

	Irrefutable single patterns may occur on the left hand side of let-binding, but
	refutable patterns must use regular pattern matching.

	To force inference to go the way you want, a type signature can be
	provided for a let binding:

	::

	f () = let x : U8 = 3
	in let y : U16 = 4
	in foo (x,y)

	Observation and ``let!``
	------------------------

	Variables may be observed using ``!``:

	::

	f (x, y) = let (a,b) = foo (x, y) !x !y
	in bar (a, b)

	Prefix ``!`` annotations can be used inline with pattern matching also:

	::

	f (x,y) = foo(x,y) !x !y
	\| Blah x => bar x
	\| Blorp z -> baz z

	If
	--

	Conditionals can be expressed in the form of if-expressions. They are in
	the form of ``if c !v1 !v2 ... then e1 else e2``. The ``!v``\ s are
	similar to the ``!`` syntax introduced above, allowing for temporary
	access to linear objects in the condition.

	Apart from the normal if-then-else syntax, Cogent offers a multi-way if
	syntax, inspired by GHC/Haskell. For example,

	::

	if \| cond_1 -> expr_1
	\| cond_2 -> expr_2
	\| ...
	\| else -> expr_n

	In the code snippet above, the conditions are Boolean expressions,
	instead of patterns as one might think. The final ``else`` is part of
	the syntax. The pipes have to be aligned. The arrows, as usual, can be
	any of ``=>``, ``->`` or ``~>``, which have the same semantics as used
	in alternatives. Prefix ``!``\ s can be added after each condition (but
	not after the ``else`` keyword), like ``\| cond_1 !v1 !v2 => e``.

	Sequencing
	----------

	Occasionally, it is useful to free a bunch of things, and using ``let`` for
	this purpose can be somewhat annoying:

	::

	f : (Obj, Obj) -> Int
	f (a, b) = let _ = free a
	and _ = free b
	in 42

	So, a little sugar is added for a series of discarding let bindings:

	::

	f : (Obj, Obj) -> Int
	f (a, b) = free a; free b; 42

	These two expressions are equivalent.


	Records
	--------
	Unboxed records are initialized as follows:

	::
	#{x = e1, y = e2}

	Boxed records are allocated on the heap. They are typically initialized by
	first calling the external C malloc function and then updating the record
	using the put operation.

	Take/put
	--------

	There is pattern syntax for ``take``, and a similar expression syntax
	for ``put``:

	::

	f : {a : Foo, b : Bar} -> {a : Foo, b : Bar}
	f (r {a = ra, b = rb}) = r {a = ra, b = rb}

	.. note:: ``take`` is always in patterns (i.e. LHS of ``=``), whereas
	``put`` is always in expressions (i.e. RHS of ``=``).

	Punning is also allowed:

	::

	f : {a : Foo, b : Bar} -> {a : Foo, b : Bar}
	f (r {a, b}) = r {a, b}

	(where just ``a`` is equivalent to ``a = a``)

	Arithmetic and comparison operators
	-----------------------------------

	Currently Cogent will use the smallest type possible for integer
	literals and generate upcasts (but not downcasts) automatically when
	used in a context where they are required. For non-literals, an explicit
	``upcast`` primitive may be needed.

	Type annotations
	----------------

	To guide the type inference engine, the user can give type annotations
	to any expressions. The syntax is ``e : t``.


	Experimental features
	=====================

	.. warning:: Experimental features, as they are called, are indeed experimental,
	which means they are not stable, and may fail, terribly. Don't rely on them
	until they become stable.

	.. _static-arrays:

	Static arrays
	-------------

	.. note:: This feature is not implemented on the ``master`` branch. It's implemented
	on the ``array`` branch and needs to be enabled by the ``--builtin-arrays`` flag
	(see :ref:`optional-features` for more information on how to do that).

	Array literals can be introduced using square brackets, like
	``[a, b, c]``. This syntax can also be used as patterns. Array types can
	be defined like ``U8[3]``, similar to C. Indexing can be made with the
	``@`` operator. E.g.: ``arr @ 3``. Arrays can also be ``take``\ n and ``put``.
	The type-level ``take`` and ``put`` operators are spelt as ``@take`` and ``@put``
	respectively. On the term level, it's written as ``arr @{ @idx = val }``---
	just prefix the open bracket and the indices with ``@`` symbols, and the rest
	are the same as those for records.


	Lambda expressions
	------------------

	We only allow for a very limited form of lambda expressions. A lambda
	expression has the syntax ``\irref => exp``, where ``irref`` is an
	irrefutable pattern, and ``exp`` is an expression which does not refer
	to any variables outside the lambda binding (no free variables). The
	bound variables have to be non-linear.