Opened 8 months ago

Last modified 8 months ago

#13042 new feature request

Allow type annotations / visible type application in pattern synonyms

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeApplications, PatternSynonyms 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

data Lift f a = Pure a | Other (f a)
data V0 a

To make a pattern synonym for a -> Lift V0 a I would like to be able to write either

pattern A a = Pure @V0 a

or

pattern B a = (Pure :: _ -> _ V0 _) a 

to be equivalent to

pattern C :: a -> Lift V0 a
pattern C a = Pure a

Change History (2)

comment:1 Changed 8 months ago by mpickering

Is this not a duplicate of your other ticket about type application in patterns? How is it different?

comment:2 Changed 8 months ago by goldfire

This is different. In my typical understanding of type application in patterns (forgetting about pattern synonyms for a moment), I think of type arguments only for existential type parameters. For example:

foo (Just @a x) = (x :: a)  -- NO! `a` is universally bound
bar (Just @Int x) = x       -- NO! This looks like it's doing runtime type matching

data E where
  MkE :: a -> E
baz (MkE @a x) = ...        -- OK. `a` is existential

The implicit proposal above includes visible type application for universals... but with different typing behavior than I had considered. I always thought that a pattern like Just @Int x would be some abominable pattern that matched against Maybe a, but then checked whether a was in fact Int. (This is just like how Just True only matches when the payload is in fact True.) For universals, though, there is a different typing interpretation: Just @Int x is a pattern against Maybe Int, and only Maybe Int. Trying to match something of type Maybe a against Just @Int x is a straightforward type error.

What's challenging here is that modern patterns have arguments that go in both directions (that is, required vs provided). Normally, everything in a pattern is an output -- that is, something that is bound upon a successful pattern match. The one exception to this rule has been constructors, which are inputs. (View patterns are another way of providing inputs, which is why they are so interesting in the context of pattern synonyms.) Above is proposed adding universal type applications as inputs... an idea I think I like.

A beautiful thing about adding universal type applications as inputs is that it greatly simplifies the design of type applications in patterns. I had been thinking that we allow type applications only for existential variables (as in my example above), but then the ordering of type applications might have a different meaning in a constructor expression than it would in a constructor pattern, which is very confusing. (See comment:1:ticket:11638 for further thoughts, as well as #11350 for the ticket about type applications in patterns in general.)

Or have I utterly misunderstood the original post?

Note: See TracTickets for help on using tickets.