From 785d7569f700d336e7ac7b0044f19ffc5f32984c Mon Sep 17 00:00:00 2001 From: Jashank Jeremy Date: Wed, 29 Apr 2020 17:20:48 +1000 Subject: [PATCH] docs: intro/first-program: working through content. (SQUASH ^{21}) --- docs/introduction/first-program.rst | 111 ++++++++++++++++++++-------- 1 file changed, 82 insertions(+), 29 deletions(-) diff --git a/docs/introduction/first-program.rst b/docs/introduction/first-program.rst index f7d426242..9bf3364c7 100644 --- a/docs/introduction/first-program.rst +++ b/docs/introduction/first-program.rst @@ -3,42 +3,88 @@ ************************************************************************ -The program we are going to walk through is a simple program which adds two -natural numbers up, and prints out the result, or reports an overflow -error. - -|cogent| is a restricted, pure, functional language. For example, |cogent| is -unable to express I/O, memory management, loops or recursions. For this reason, -we only write the core functionality in |cogent|, which adds up two natural numbers, -and check if overflow has happened. To carry the result of the check, we need -a result type:: +The program we are going to walk through is +a simple program which adds two natural numbers up, +and prints out the result, or reports an overflow error. + +|cogent| is a restricted, pure, functional language. +For example, |cogent| is unable to express +input/output operations, memory management, and loops. +For this reason, we will only write +the core functionality in |cogent|, +which adds up two natural numbers, +and check if overflow has happened. +To carry the result of the check, +we need a result type:: type R a b = < Success a | Error b > -It has similar meaning to a sum type in Haskell (or in any functional language):: +It has similar meaning to a sum type in Haskell +(or in any functional language):: + -- in Haskell, we might say: data R a b = Success a | Error b -It says that, the result can be either a ``Success`` or ``Error``, and in each case -you also return the result associated with these tags, namely ``a`` and ``b`` respectively. -Note that ``R a b`` is polymorphic on ``a`` and ``b``. They can be instantiated to any -concrete types. +It says the result may be +either ``Success`` or ``Error`` --- +which are referred to as tags or variants --- +and, in each case, +a value will be associated with a tag: +``Success`` has an associated ``a``, and +``Error`` has an associated ``b``. +Note that ``R a b`` is *polymorphic* on ``a`` and ``b``: +we may replace those *type variables* with any concrete types. + +One notable difference to the Haskell version above is +that the ``type`` keyword only introduces a *type synonym*, +where in Haskell it would introduce a new type. +Thus, wherever an ``R a b`` is needed, +it may be equivalently spelled in full +as ``< Success a | Error b >`` +(which, of course, is more verbose in many cases). + + +Next we define a function ``add``. +As with other strongly-typed functional languages, +we do so by first giving its type signature:: + + add : (U32, U32) -> R U32 () + +``U32`` is a type representing +an unsigned 32-bit integer; +here, we use it to model the natural numbers. +|cogent| has built-in types for +common sizes of unsigned integers: +``U8``, ``U16`` and ``U64`` also exist. -The difference to the Haskell version is that, the ``type`` keyword only introduces a -type synonym, which is to say, wherever an ``R a b`` is needed, it can be alternatively -spelt as ``< Success a | Error b >``, which of course is more verbose in many cases. +Unlike many other functional languages, +a |cogent|'s functions can only take **one argument**. +When we wish to pass two ``U32``\ s, +we make them into a pair (or, more generally, a tuple). -Next we define a function ``add``, which has the following type signature:: +Ignoring, for the moment, the error handling, +our first attempt at writing ``add`` might look like:: add : (U32, U32) -> R U32 () + add (x, y) = Success (x + y) + +Similar to Haskell, +we give a function's definition +by declaring the computation it does: +here, ``add (x, y)`` becomes ``(x + y)``, +wrapped in ``Success``. +Cogent also supports *pattern matching*, +so the names ``x`` and ``y`` bind, +as expected, +to the values of the tuple passed in. + +.. todo: -``U32`` is an unsigned 32-bit integer; we use it to model natural numbers here. |cogent| -also has built-in ``U8``, ``U16`` and ``U64`` for other sizes of unsigned integers. -A |cogent| function only takes **one argument**. When we want to pass in two ``U32``\ s, -we make them into a pair (or a tuple, more generally). + - introduce let/in + - introduce patterns + - full definition -The full definition of the ``add`` function is given below (also includes the previously -given type signature): +Let's have a look at the rest of ``add``'s definition:: .. code-block:: none @@ -48,11 +94,18 @@ given type signature): | True -> Error () | False -> Success sum -|cogent| is a layout sensitive language, like Python or Haskell. In this function, -it binds the value of ``x + y`` to binder ``sum``. In the body of the ``let-in`` -expression, a pattern match is done on the condition ``sum < x || sum < y`` (if -``sum`` is less than ``x`` or it's less than ``y``). If this condition is ``True``, -then we return an ``Error ()``. ``()`` is "unit", the single value of type ``()`` +|cogent| is a layout-sensitive language, like Python or Haskell. +In this function, +we bind the value of ``x + y`` to ``sum``. +In the body of the ``let ... in`` expression, +a pattern match is done +on the condition ``sum < x || sum < y`` --- +that is, if ``sum`` is less than ``x`` +or less than ``y`` --- +and, if this condition is ``True``, +then we return an ``Error``. + +``()`` is "unit", the single value of type ``()`` (also reads "unit"). If the condition is ``False``, which means that overflow didn't happen, then we return ``Success sum``, which carries the summation.