Opened 5 years ago

Last modified 7 months ago

#4466 new feature request

Add extension for type application

Reported by: igloo Owned by:
Priority: low Milestone: 7.12.1
Component: Compiler Version: 6.12.3
Keywords: Cc: wren@…, sweirich@…, mail@…, hamidhasan14@…, jan.stolarek@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:


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 (11)

comment:1 Changed 5 years ago by igloo

  • Milestone set to 7.2.1

comment:2 Changed 4 years ago by igloo

See also #5296.

comment:3 Changed 3 years ago by igloo

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

comment:4 Changed 3 years ago by WrenThornton

  • Cc wren@… added

comment:5 Changed 3 years ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:6 Changed 2 years ago by sweirich

  • Cc sweirich@… added

comment:7 Changed 2 years ago by kosmikus

  • Cc mail@… added

comment:8 Changed 2 years ago by Hamidhasan

  • Cc hamidhasan14@… added
  • difficulty set to Unknown

comment:9 Changed 18 months ago by jstolarek

  • Cc jan.stolarek@… added

comment:10 Changed 13 months ago by thoughtpolice

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:11 Changed 7 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.

Note: See TracTickets for help on using tickets.