Opened 3 weeks ago

Last modified 11 days 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:
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 (3)

comment:1 Changed 3 weeks 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 12 days 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 11 days 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).

Note: See TracTickets for help on using tickets.