Opened 3 years ago

Last modified 2 years ago

#12717 new feature request

Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)

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


Suppose I write in a signature:

data Type = TArrow t1 t2 | TApp String [Type]

But it turns out that the real data type only has TApp (and uses "->" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this "concrete abstract data type" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.

The converse might be useful too:

data Type
pattern TArrow :: Type -> Type -> Type
pattern TInt :: Type

These patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)

Change History (1)

comment:1 Changed 2 years ago by ocharles

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