From c2f750b3404826bbe3b71340cf2589706cd96c8f Mon Sep 17 00:00:00 2001 From: Brent Yorgey Date: Wed, 20 Dec 2023 15:26:56 -0600 Subject: [PATCH] Allow `><` as syntax for product types Also update documentation to match. Closes #333. --- disco.cabal | 4 ++++ docs/reference/product-type.rst | 21 ++++++++++----------- src/Disco/Parser.hs | 7 ++++--- src/Disco/Syntax/Operators.hs | 4 ---- test/types-syntax/expected | 7 +++++++ test/types-syntax/input | 7 +++++++ 6 files changed, 32 insertions(+), 18 deletions(-) create mode 100644 test/types-syntax/expected create mode 100644 test/types-syntax/input diff --git a/disco.cabal b/disco.cabal index dc457880..2d839571 100644 --- a/disco.cabal +++ b/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 diff --git a/docs/reference/product-type.rst b/docs/reference/product-type.rst index 67dbeb07..19bc62cd 100644 --- a/docs/reference/product-type.rst +++ b/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 `. 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 `). 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,27 +21,26 @@ values. Suppose ``A`` and ``B`` are :doc:`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 ` on the pair, :doc:`like so `: :: - 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 @@ -49,7 +48,7 @@ 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,7 +58,7 @@ 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`` @@ -67,7 +66,7 @@ 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)))) = ... Typically one can just use triples or 5-tuples or whatever and not diff --git a/src/Disco/Parser.hs b/src/Disco/Parser.hs index 196c274e..8f403c7f 100644 --- a/src/Disco/Parser.hs +++ b/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 "+" (:+:) diff --git a/src/Disco/Syntax/Operators.hs b/src/Disco/Syntax/Operators.hs index 6d0c90ca..d40b52a7 100644 --- a/src/Disco/Syntax/Operators.hs +++ b/src/Disco/Syntax/Operators.hs @@ -1,10 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} ------------------------------------------------------------------------------ - ------------------------------------------------------------------------------ - -- SPDX-License-Identifier: BSD-3-Clause -- | diff --git a/test/types-syntax/expected b/test/types-syntax/expected new file mode 100644 index 00000000..e6ba6946 --- /dev/null +++ b/test/types-syntax/expected @@ -0,0 +1,7 @@ +(2, 3) +(2, 3) +(2, 3) +left(4) +left(4) +<ℤ → ℤ> +<ℤ → ℤ> diff --git a/test/types-syntax/input b/test/types-syntax/input new file mode 100644 index 00000000..2d3d895e --- /dev/null +++ b/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