Opened 3 years ago

Last modified 3 months ago

#4466 new feature request

Add extension for type application

Reported by: igloo Owned by:
Priority: low Milestone: 7.6.2
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 Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

In
http://www.haskell.org/pipermail/libraries/2010-October/014761.html
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)

were:

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

comment:1 Changed 3 years ago by igloo

  • Milestone set to 7.2.1

comment:2 Changed 3 years ago by igloo

See also #5296.

comment:3 Changed 2 years ago by igloo

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

comment:4 Changed 2 years ago by WrenThornton

  • Cc wren@… added

comment:5 Changed 20 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:6 Changed 12 months ago by sweirich

  • Cc sweirich@… added

comment:7 Changed 12 months ago by kosmikus

  • Cc mail@… added

comment:8 Changed 9 months ago by Hamidhasan

  • Cc hamidhasan14@… added
  • Difficulty set to Unknown

comment:9 Changed 3 months ago by jstolarek

  • Cc jan.stolarek@… added
Note: See TracTickets for help on using tickets.