Opened 7 months ago

Last modified 3 months ago

#14478 new feature request

Abstract pattern synonyms (for hsig and hs-boot)

Reported by: ezyang Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: backpack Cc: lelf
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Most declaration forms (data types, values, type families, etc) support forward declaration in hs-boot/hsig files. However, pattern synonyms do not. This seems like a major omission!

Some problems to solve:

  • The obvious syntax pattern Foo :: pat_ty is insufficient to specify whether or not a pattern is bidirectional or unidirectional. How should this be represented syntactically?
  • What is the interaction with bundling? Should it be possible to export a bundle of abstract pattern synonyms, with the intent that this means an implementation must also have bundled them together
  • See also #12717; abstract pattern synonym should be implementable with a plain old constructor

Change History (4)

comment:1 Changed 7 months ago by ezyang

OK, so there is a major wrinkle: pattern-synonym signature splitting. The problem is described in this note:

Note [The pattern-synonym signature splitting rule]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given a pattern signature, we must split
     the kind-generalised variables, and
     the implicitly-bound variables
into universal and existential.  The rule is this
(see discussion on Trac #11224):

     The universal tyvars are the ones mentioned in
          - univ_tvs: the user-specified (forall'd) universals
          - req_theta
          - res_ty
     The existential tyvars are all the rest

For example

   pattern P :: () => b -> T a
   pattern P x = ...

Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
how do we split the arg_tys from req_ty?  Consider

   pattern Q :: () => b -> S c -> T a
   pattern Q x = ...

This is an odd example because Q has only one syntactic argument, and
so presumably is defined by a view pattern matching a function.  But
it can happen (Trac #11977, #12108).

We don't know Q's arity from the pattern signature, so we have to wait
until we see the pattern declaration itself before deciding res_ty is,
and hence which variables are existential and which are universal.

And that in turn is why TcPatSynInfo has a separate field,
patsig_implicit_bndrs, to capture the implicitly bound type variables,
because we don't yet know how to split them up.

It's a slight compromise, because it means we don't really know the
pattern synonym's real signature until we see its declaration.  So,
for example, in hs-boot file, we may need to think what to do...
(eg don't have any implicitly-bound variables).

One way we could manage this without introducing a new syntactic construct is to have a user specify both pattern synonym signature AND a stub declaration, literally writing something like:

pattern P :: () => b -> T a
pattern P x = ...

That's a literal ..., because if we introduce this syntax, we now can also solve the problem of unidirectional versus bidirectional; to declare only a unidirectional pattern is required, you write:

pattern P :: () => b -> T a
pattern P x <- ...

It's annoyingly asymmetric with how we do regular value signatures, but the alternative seems worse (inventing a new signature syntax which builds in the arity somehow.)

comment:2 Changed 7 months ago by simonpj

We also need to know arity because, type system aside, we still need to know how many arguments the pattern synonym should be applied to in a pattern. Eg

       f (P x)
vs
       f (P x y)

comment:3 Changed 7 months ago by goldfire

I actually like the proposed syntax with the ellipsis. I would just vote for .. (two dots), because that's already a lexeme (and is what closed type families use).

comment:4 Changed 3 months ago by lelf

Cc: lelf added
Note: See TracTickets for help on using tickets.