Could not parse the left-hand side (m + 1) * n

user_1973793 0
Viewed 219

I just started learning Agda reading Programming Language Foundations in Agda. Right in the first chapter there's a definition of multiplication with one of the cases being (suc m) * n = n + (m * n). I assumed it could be nicer expressed as (m + 1) * n = n + (m * n), but apparently this is not the case. The following program:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

{-# BUILTIN NATURAL ℕ #-}

_*_ : ℕ → ℕ → ℕ
zero * n = zero
-- This is fine:
-- (suc m) * n = n + (m * n)
-- This is not:
(m + 1) * n = n + (m * n)

fails with:

Could not parse the left-hand side (m + 1) * n
Operators used in the grammar:
  * (infix operator, level 20) [_*_ (/Users/proxi/Documents/Projekty/Agda/multiply.agda:11,1-4)]
  + (infix operator, level 20) [_+_ (/Users/proxi/Documents/Projekty/Agda/multiply.agda:5,1-4)] 
when scope checking the left-hand side (m + 1) * n in the
definition of _*_

I believe in Agda terms one could say that definition using constructor works fine, but definition using operator does not. Why is that so? Is this never possible, or does it depend on how operator (function) is defined?

agda
2 Answers

Using functions in patterns is not supported.

Note also that if functions were allowed in patterns, it would be (1 + m) * n rather than (m + 1) * n, because _+_ is defined by pattern matching on its first argument, so 1 + m reduces to suc m and m + 1 is stuck.

user_32374650

As has been pointed out, you cannot just use a function to pattern-match. However, it is possible to declare pattern-matching extensions that express nearly the same thing:

open import Data.Nat.Base as Nat
  using (ℕ; zero) renaming (suc to 1+_)
pattern 2+_ n = 1+ 1+ n

Then you can use (1+ m) * n, and even (2+ m).

user_19356310
Related