Opened 6 years ago

Closed 8 months ago

#4466 closed feature request (duplicate)

Add extension for type application

Reported by: igloo Owned by:
Priority: low Milestone: 8.0.1
Component: Compiler Version: 6.12.3
Keywords: Cc: wren@…, sweirich@…, mail@…, hamidhasan14@…, jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #5296 Differential Rev(s):
Wiki Page:


In we discussed adding an extension for explicit type application.

The main stumbling block is syntax.

For example, we would like to be able to write something to the effect of

(Just @ Char) 'a'

and also to be able to pattern match types, e.g.

f ((Just @ t) x) = (Right @ String @ t) x

For a more useful example:

data T where
    MkT :: forall a. a -> (a -> Int) -> T

f (MkT @ a x g) = g (x::a)

Possible suggested syntaxes to make something of type

Maybe (forall a. a->a)


Just @ (forall a. a->a) id    (@ has another meaning in patterns)
Just[forall a. a->a] id       (pvs, opal, HasCASL with paramterized modules; conflicts with Haskell list syntax)
Just {forall a. a->a} id      (Agda)
#Just (forall a. a->a) id
@Just (forall a. a->a) id     (coq)

In the last 2 cases we would presumably have something like

Just :: forall a . a -> Maybe a
Just :: Char -> Maybe Char
#Just :: /\ a . a -> Maybe a
#Just Char :: Char -> Maybe Char

and similarly

#map :: /\ a b . (a -> b) -> [a] -> [b]

Change History (13)

comment:1 Changed 6 years ago by igloo

  • Milestone set to 7.2.1

comment:2 Changed 5 years ago by igloo

See also #5296.

comment:3 Changed 4 years ago by igloo

  • Milestone changed from 7.4.1 to 7.6.1
  • Priority changed from normal to low

comment:4 Changed 4 years ago by WrenThornton

  • Cc wren@… added

comment:5 Changed 4 years ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:6 Changed 3 years ago by sweirich

  • Cc sweirich@… added

comment:7 Changed 3 years ago by kosmikus

  • Cc mail@… added

comment:8 Changed 3 years ago by Hamidhasan

  • Cc hamidhasan14@… added
  • difficulty set to Unknown

comment:9 Changed 2 years ago by jstolarek

  • Cc jan.stolarek@… added

comment:10 Changed 23 months ago by thoughtpolice

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:11 Changed 17 months ago by thoughtpolice

  • Milestone changed from 7.10.1 to 7.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:12 Changed 9 months ago by thoughtpolice

  • Milestone changed from 7.12.1 to 8.0.1

Milestone renamed

comment:13 Changed 8 months ago by jstolarek

  • Cc jstolarek added; jan.stolarek@… removed
  • Resolution set to duplicate
  • Status changed from new to closed

Clearly this has been duplicated by #5296 but since all the discussion is happening there I will close this ticket.

Note: See TracTickets for help on using tickets.