Skip to content

Commit

Permalink
Allow >< as syntax for product types
Browse files Browse the repository at this point in the history
Also update documentation to match.  Closes #333.
  • Loading branch information
byorgey committed Dec 20, 2023
1 parent 22a832d commit c2f750b
Show file tree
Hide file tree
Showing 6 changed files with 32 additions and 18 deletions.
4 changes: 4 additions & 0 deletions disco.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
21 changes: 10 additions & 11 deletions docs/reference/product-type.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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:

::

Expand All @@ -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::
Expand All @@ -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
Expand Down
7 changes: 4 additions & 3 deletions src/Disco/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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@).
Expand Down Expand Up @@ -1241,6 +1241,7 @@ parseType = makeExprParser parseAtomicType table
[
[ infixR "*" (:*:)
, infixR "×" (:*:)
, infixR "><" (:*:)
]
,
[ infixR "+" (:+:)
Expand Down
4 changes: 0 additions & 4 deletions src/Disco/Syntax/Operators.hs
Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

-- |
Expand Down
7 changes: 7 additions & 0 deletions test/types-syntax/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(2, 3)
(2, 3)
(2, 3)
left(4)
left(4)
<ℤ → ℤ>
<ℤ → ℤ>
7 changes: 7 additions & 0 deletions test/types-syntax/input
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit c2f750b

Please sign in to comment.