Sum types

CHANGES.md

@@ -2,6 +2,24 @@
 
 ## Language changes
 
+* Cryptol now supports *enum* declarations. An enum is a named typed which is
+  defined by one or more constructors. Enums correspond to the notion of
+  algebraic data types, which are commonly found in other programming
+  languages.  See the [manual
+  section](https://galoisinc.github.io/cryptol/master/TypeDeclarations.html#enums)
+  for more information.
+
+* Add two enum declarations to the Cryptol standard library:
+
+  ```
+  enum Option a = None | Some a
+
+  enum Result t e = Ok t | Err e
+  ```
+
+  These types are useful for representing optional values (`Option`) or values
+  that may fail in some way (`Result`).
+
 * `foreign` functions can now have an optional Cryptol implementation, which by
   default is used when the foreign implementation cannot be found, or if the FFI
   is unavailable. The `:set evalForeign` REPL option controls this behavior.

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -617,8 +617,7 @@ readBack ty val =
         TVTuple{} -> "tuple"
         TVRec{} -> "record"
         TVFun{} -> "fun"
-        TVNewtype nt _ _ -> identText $ nameIdent $ TC.ntName nt
-        TVAbstract{} -> "abstract"
+        TVNominal nt _ _ -> identText $ nameIdent $ TC.ntName nt
 
 
 -- | Given a suggested `name` and a type and value, attempt to bind the value

cryptol-remote-api/src/CryptolServer/Data/Type.hs

@@ -20,7 +20,10 @@ import Cryptol.Parser.Position (emptyRange)
 import Cryptol.Parser.Selector (ppSelector)
 import Cryptol.Utils.RecordMap (recordFromFields)
 import Cryptol.TypeCheck.PP (NameMap, emptyNameMap, ppWithNames)
-import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf)
+import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..),
+          TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf,
+          NominalType(..), NominalTypeDef(..)
+          )
 import Cryptol.Utils.Ident (mkIdent)
 import Cryptol.Utils.PP (pp)
 import Cryptol.Utils.RecordMap (canonicalFields)
@@ -213,8 +216,14 @@ instance JSON.ToJSON JSONType where
         , "name" .= show (ppWithNames ns v)
         ]
       convert (TUser _n _args def) = convert def
-      convert (TNewtype _nt _ts) =
-        JSON.object [ "type" .= T.pack "newtype" ]
+      convert (TNominal nt ts) =
+        JSON.object [ "type" .= case ntDef nt of
+                                  Struct {} -> T.pack "newtype"
+                                  Enum {}   -> T.pack "enum"
+                                  Abstract  -> T.pack "primitive"
+                    , "name" .= show (pp (ntName nt))
+                    , "arguments" .= map (JSONType ns) ts
+                    ]
       convert (TRec fields) =
         JSON.object
         [ "type" .= T.pack "record"

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -791,7 +791,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:885:14--885:20
+  (Cryptol::@) called at Cryptol:904:14--904:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9

docs/RefMan/TypeDeclarations.rst

@@ -51,3 +51,185 @@ of newtypes to extract the values in the body of the type.
   > sum x.seq
   6
 
+Enums
+-----
+
+.. code-block:: cryptol
+
+  enum Maybe a = Nothing | Just a
+
+An ``enum`` declaration introduces a new named type, which is defined by a
+collection of *constructors*. ``enum`` declarations correspond to the notion of
+*algebraic data types*, which are commonly found in other programming
+languages. Each named ``enum`` type is treated like a separate type, even if it
+has the exact same constructors as another ``enum`` type---in this way ``enum``
+is similar to ``newtype`` and unlike ``type`` synonyms.
+
+**Constructors.** The only way to create a value of an ``enum`` type is to
+use one of its constructors.   When used in an expression, the constructors
+behave like an ordinary function, which has one parameter for each field of the
+constructor.  For example, the constructor ``Just`` has a type like this:
+
+.. code-block:: cryptol
+
+   Just: {a} a -> Maybe a
+
+Constructors may have 0 or multiple fields, and values created with different
+constructors are always distinct.
+
+**Case Expressions.** The only way to examine a value of an ``enum`` type is
+with a ``case`` expression, which are similar to ``if`` expressions:
+
+.. code-block:: cryptol
+
+  case e of
+    Nothing -> 0
+    Just a  -> a + 1
+
+In this example, ``e`` is an expression of type ``Maybe``:
+
+  * if it was created with the ``Nothing`` constructor,
+    then we'll use the first branch of the ``case`` expression, and
+    the result of the whole expression would be 0;
+
+  * if, ``e`` was created by applying the ``Just`` constructor to some
+    value (e.g, ``Just 2``), then we'll use the second branch of the ``case``
+    expression, and the variable ``a`` will be bound to the value of the field
+    (e.g., ``2``), and the whole expression will evaluate to ``a + 1``
+    (e.g., ``3``).
+
+It is also possible to use just a variable (or ``_``) in a case expression
+to define a catch-all clause---if a value does not match any of the previous
+cases, then this branch will be used:
+
+.. code-block:: cryptol
+
+  isNothing x =
+    case x of
+      Nothing -> True
+      _       -> False
+
+**``Option`` and ``Result``.** Currently, Cryptol defines two ``enum``
+declarations in the Cryptol standard library: ``Option`` and ``Result``:
+
+.. code-block:: cryptol
+
+  enum Option a = None | Some a
+
+  enum Result t e = Ok t | Err e
+
+The ``Option a`` type represents an optional value, which can either be a value
+of type ``a`` (``Some``) or no value at all ``None``. A value of type ``Result
+t e`` can either be a successful value of type ``t`` (``Ok``) or an error value
+of type ``e`` (``Err``).
+
+``Option`` and ``Result`` values are commonly used to model the return type of
+partial functions, i.e., functions that are not defined for all inputs. For
+instance, if a function ``f`` is not defined on the input ``42``, then one
+could model this with ``Option``:
+
+.. code-block:: cryptol
+
+  f : [8] -> Option [8]
+  f x =
+    if x == 42
+       then None
+       else Some (x+1)
+
+One could also model this with ``Result``:
+
+.. code-block:: cryptol
+
+  f : [8] -> Result [8] (String [8])
+  f x =
+    if x == 42
+       then Err "`f 42` not defined"
+       else Ok (x+1)
+
+With either result type, one can gracefully recover from ``f 42`` erroring by
+matching on ``None`` or ``Err`` in a ``case`` expression.
+
+**Upper Case Restriction.**
+The names of the constructors in an ``enum`` declarations
+need to start with an upper-case letter.  This restriction makes it possible
+to distinguish between constructors and variable
+bindings in ``case`` patterns (e.g., between ``Just`` and ``a`` in the
+previous example).
+
+**Non Recursive.** The fields in a constructor may be of any value type,
+as long as this type does not depend on the type to which the constructor
+belongs.  This means that we do not support defining recursive types,
+such as linked lists.
+
+**No Nested Constructor Patterns.**  For simplicity, only non-constructor
+patterns may be used in the fields of a constructor pattern.  For example,
+``Just (a,b)`` and ``Just (a # b)`` are OK, however, ``Just (Just a)``
+will be rejected.  This is a restriction that we may lift in the future.
+
+**No Overlapping Patterns.** For simplicity, all patterns in a
+``case`` expression must be disjoint. In particular, this means that:
+
+  * No two patterns in a ``case`` expression can match the same constructor.
+    This means that Cryptol will reject the following example:
+
+    .. code-block:: cryptol
+
+      isNothing x =
+        case x of
+          Nothing -> True
+          Nothing -> False
+
+  * If a ``case`` expression uses a catch-all clause, then that clause must
+    occur last in the expression. It is an error to match on additional
+    patterns after the catch-all clause. For instance, Cryptol will reject the
+    following example:
+
+    .. code-block:: cryptol
+
+      isNothing x =
+        case x of
+          Just _  -> False
+          _       -> True
+          Nothing -> False
+
+**Patterns Must Be Exhaustive.** The patterns in a ``case`` expression must
+cover all constructors in the ``enum`` type being matched on. For example,
+Cryptol will reject the following example, as it does not cover the ``Just``
+constructor:
+
+.. code-block:: cryptol
+
+  isNothing x =
+    case x of
+      Nothing -> True
+
+**The Matched Expression Must Have a Known Enum Type.** Cryptol will reject
+the following definition of ``f``, where ``f`` lacks a type signature:
+
+.. code-block:: cryptol
+
+  f x =
+    case x of
+      _ -> ()
+
+This is because it is not clear what the type of ``x`` (the expression being
+matched) should be. The only pattern is a catch-all case, which does not reveal
+anything about the type of ``x``. It would be incorrect to give ``f`` this type:
+
+.. code-block:: cryptol
+
+  f : {a} a -> ()
+
+This is because ``f`` is not really polymorphic in its argument type, as the
+only values that can be matched in a ``case`` expression are those whose type
+was declared as an ``enum``. As such, Cryptol rejects this example.
+
+Cryptol will also reject this definition, where the type of the value
+being matched is not an ``enum`` type:
+
+.. code-block:: cryptol
+
+  g : Integer -> ()
+  g x =
+    case x of
+      _ -> ()

docs/RefMan/_build/html/.buildinfo

@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 49d6d89345e8bba027ef627e0adeb689
+config: 41758cdb8fafe65367e2aa727ac7d826
 tags: 645f666f9bcd5a90fca523b33c5a78b7