Allow >< as syntax for product types

disco.cabal

@@ -177,6 +177,8 @@ extra-source-files:  stack.yaml, repl/*.hs
                      test/parse-top-term/expected
                      test/parse-top-term/input
                      test/parse-top-term/parse-top-term.disco
+                     test/parse-try/expected
+                     test/parse-try/input
                      test/poly-bad/expected
                      test/poly-bad/input
                      test/poly-infer-sort/expected
@@ -347,6 +349,8 @@ extra-source-files:  stack.yaml, repl/*.hs
                      test/types-squash/input
                      test/types-standalone-ops/expected
                      test/types-standalone-ops/input
+                     test/types-syntax/expected
+                     test/types-syntax/input
                      test/types-toomanypats/expected
                      test/types-toomanypats/input
                      test/types-toomanypats/toomanypats.disco

docs/reference/product-type.rst

@@ -4,14 +4,14 @@ Pair types
 *Pair types*, or *product types*, represent *ordered pairs* of
 values. Suppose ``A`` and ``B`` are :doc:`types <types>`. Then:
 
-- ``A * B`` (also written ``A × B``) is a *pair type* (also known
+- ``A >< B`` (also written ``A × B`` or ``A * B``) is a *pair type* (also known
   as a *product type* or *Cartesian product*).  It represents the set of
   all possible pairs where the first element has type ``A`` and the
   second element has type ``B``.
 
 - A pair is written ``(a, b)`` (where ``a`` and ``b`` can be arbitrary
   :doc:`expressions <expression>`).  Specifically, if ``a : A`` and ``b : B``, then the
-  ordered pair ``(a, b)`` has type ``A * B``.  For example:
+  ordered pair ``(a, b)`` has type ``A >< B``.  For example:
 
     ::
 
@@ -21,35 +21,34 @@ values. Suppose ``A`` and ``B`` are :doc:`types <types>`. Then:
        (-7, -3) : ℤ × ℤ
 
 Pair types are commonly used to represent functions that take multiple
-inputs.  For example, ``f : N * Z -> Q`` means that ``f`` takes a
+inputs.  For example, ``f : N >< Z -> Q`` means that ``f`` takes a
 *pair* of a natural number and an integer as input.  Such functions
 are often defined via :doc:`pattern matching <pattern>` on the pair,
 :doc:`like so <prod-pattern>`:
 
 ::
 
-   f : N * Z -> Z
+   f : (N >< Z) -> Z
    f(n,z) = 3n - z
 
 
 n-tuples and nested pairs
 -------------------------
 
-We have seen that ``A * B`` is a type of *pairs* of values.  What
+We have seen that ``A >< B`` is a type of *pairs* of values.  What
 about triples, quadruples, ... n-tuples of values?  The answer is
 simple:
 
-- triples are written ``(x,y,z)`` and have types like ``A * B * C``;
-- quadruples are written ``(w,x,y,z)`` and have types like ``A * B *
-  C * D``;
+- triples are written ``(x,y,z)`` and have types like ``A >< B >< C``;
+- quadruples are written ``(w,x,y,z)`` and have types like ``A >< B >< C >< D``;
 - and so on.
 
 So, for example, a function taking a quintuple of values could be
 written like this:
 
 ::
 
-   funTaking5Tuple : N * Z * List(N) * Q * Bool -> Int
+   funTaking5Tuple : (N >< Z >< List(N) >< Q >< Bool) -> Int
    funTaking5Tuple(n,z,l,q,b) = ...
 
 .. note::
@@ -59,15 +58,15 @@ written like this:
    convenience, pair types and values both *associate to the right*,
    that is,
 
-   - the type ``A * B * C`` is interpreted as ``A * (B * C)``, and
+   - the type ``A >< B >< C`` is interpreted as ``A >< (B >< C)``, and
    - correspondingly, ``(x, y, z)`` is interpreted as ``(x, (y, z))``.
 
    So, for example, the definition of the function ``funTaking5Tuple``
    from above is really shorthand for
 
    ::
 
-      funTaking5Tuple : N * (Z * (List(N) * (Q * Bool))) -> Int
+      funTaking5Tuple : N >< (Z >< (List(N) >< (Q >< Bool))) -> Int
       funTaking5Tuple(n,(z,(l,(q,b)))) = ...
 
    Typically one can just use triples or 5-tuples or whatever and not

src/Disco/Parser.hs

@@ -304,8 +304,8 @@ ellipsis = label "ellipsis (..)" $ concat <$> ((:) <$> dot <*> some dot)
 lambda :: Parser String
 lambda = symbol "\\" <|> symbol "λ"
 
-forall :: Parser ()
-forall = void (symbol "∀") <|> reserved "forall"
+forAll :: Parser ()
+forAll = void (symbol "∀") <|> reserved "forall"
 
 exists :: Parser ()
 exists = void (symbol "∃") <|> reserved "exists"
@@ -888,7 +888,7 @@ parseQuantified = do
 parseQuantifier :: Parser Quantifier
 parseQuantifier =
   Lam <$ lambda
-    <|> All <$ forall
+    <|> All <$ forAll
     <|> Ex <$ exists
 
 -- | Parse a let expression (@let x1 = t1, x2 = t2, ... in t@).
@@ -1241,6 +1241,7 @@ parseType = makeExprParser parseAtomicType table
     [
       [ infixR "*" (:*:)
       , infixR "×" (:*:)
+      , infixR "><" (:*:)
       ]
     ,
       [ infixR "+" (:+:)

src/Disco/Syntax/Operators.hs

@@ -1,10 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- SPDX-License-Identifier: BSD-3-Clause
 
 -- |

test/types-syntax/expected

@@ -0,0 +1,7 @@
+(2, 3)
+(2, 3)
+(2, 3)
+left(4)
+left(4)
+<ℤ → ℤ>
+<ℤ → ℤ>

test/types-syntax/input

@@ -0,0 +1,7 @@
+(2,3) : N * Z
+(2,3) : N × Z
+(2,3) : N >< Z
+left(4) : N + Z
+left(4) : N ⊎ Z
+(\x. x) : Z -> Z
+(\x. x) : Z → Z