Typed pattern synonyms

[andreasabel]

Roman writes:

Hi, I'm doing some generic programming and defining lots of pattern synonyms, but they are not equivalent to constructors due to their untyped nature. E.g. I have

    pattern _∷_ x xs = cons₁ (x , xs , lrefl)

Clearly, Agda can't infer that _∷_ has type ∀ {α} {A : Set α} -> A -> List A -> List A, so the inferred type of 2 ∷ [] is μ (_Ds_57 x xs) (_j_58 x xs) instead of List ℕ, i.e. completely unspecified. It means that I need both a pattern _∷_ and an operator

    _∷′_ : ∀ {α} {A : Set α} -> A -> List A -> List A
    _∷′_ = _∷_

to use on the RHS. It's rather inconvenient to have a pattern and a function instead of just one constructor, especially in my case as I want to figure out whether it's possible to type check existing code after changing data definitions to their generic counterparts.
Ideally, I would like to write

    pattern
      _∷_ : ∀ {α} {A : Set α} -> A -> List A -> List A
      x ∷ xs = cons₁ (x , xs , lrefl)

Is it possible to implement such a feature? Or maybe something else that would allow to use pattern synonyms as genuine constructors?

[andreasabel]

Typed pattern synoyms could be overloaded (and overload constructors), this would be handy. However, this would probably then defeat your purpose, Roman, as they will be only checkable, not inferable. Only for non-ambiguous pattern synonyms one could get inference, like for unambiguous constructors now.

[effectfully]

Thanks for considering the request.

I don't expect pattern synonyms (or constructors) to be both inferrable and overloaded at the same time (is it even possible without adding something like union types to the language?). For my use case I need pattern synonyms to be equal in power to constructors (because I want to replace constructors in existing code with corresponding pattern synonyms), i.e. either inferrable or overloaded.

It seems pattern synonyms are not equivalent to constructors even as checkable terms currently. Here is a file which defines the List data type as the fixed point of a description. If I change the _∷′_ typed operator used in several places to the _∷_ pattern synonym, there remain unsolved level metavariables after type checking e.g. the reverse function (copied verbatim from Data.List.Base)

reverse : ∀ {a} {A : Set a} → List A → List A
reverse = foldl (λ rev x → x ∷ rev) []

-- _a_337 : Level
-- _b_338 : Level

[UlfNorell]

I haven't run into the need for inferrable pattern synonyms, but I've often wished for overloadable ones. Here's a common design pattern I'm using:

data D (i : I) : Set where
  c : ∀ {j} → A → i ≡ f j → D i

pattern c! x = c x refl

It's really annoying that I can reuse the c constructor for another datatype but not the c! synonym.

One might consider deferring name resolution in pattern synonyms to the use site, allowing the single definition of c! to serve both constructors, but that would only work if they had the same number of arguments.

[andreasabel]

@effectfully : What you actually want is functions that you can also use on the left hand side.
Your proposal is not far from allowing functions in patterns, like allowing the addition function + there.

eq : Nat -> Nat -> Bool
eq 0 0 = true
eq (1 + x) (1 + y) = eq x y
eq _ _ = false

Agda could evaluate the second clause to

eq (suc x) (suc y) = eq x y

and then do pattern matching as usual.

In general, I think your proposed typed pattern synonyms require an entirely different mechanism than the current pattern synonyms, which are basically macros expanded by the scope checker before we reach the type checker.

[effectfully]

@andreasabel, is it easier to allow functions on lhs than to adjust the meaning of patterns on rhs? Stuff like

pattern
  suc2 : Nat -> Nat
  suc2 x = suc (suc x)

can be processed as follows: first, suc2 is type checked against its signature. If it's alright, then all instances of suc2 x on lhs are syntactically substituted by suc (suc x), but on rhs suc2 is treated as a regular function. Patterns are non-recursive and pattern marching is not allowed in them, so this special treatment of patterns on rhs should be easier to implement than general functions on lhs. These then would be typed bidirectional patterns synonyms which Haskell has.

Though, I like the idea of having functions on lhs. I needed this a few times.

[gallais]

Patterns are non-recursive and pattern marching is not allowed in them (...) Though, I like the idea of having functions on lhs. I needed this a few times.

Being able to write [1..10] ++ z would indeed be pretty convenient. A distinct but related thing: when defining a constructor for the datatype D it is already possible to use a computation that will deliver a ... -> D type after being fully evaluated rather than something syntactically equal to ... -> D. E.g.

module Nary where

open import Agda.Builtin.Nat

N-ary : Nat → Set → Set
N-ary 0       A = A
N-ary (suc n) A = A → N-ary n A

data Nat' : Set where
  zero : N-ary 0 Nat'
  succ : N-ary 1 Nat'

We could imagine these "typed patterns synonyms" to similarly be any well-typed expression as long as it evaluates to something that qualifies as a pattern.

[uhbif19]

Should not definitional injectivity for INJECTIVITY pragma cover this usecase as well?

#4106 (comment)