Opened 4 years ago

Closed 2 years ago

#8920 closed feature request (wontfix)

Alternative GADT syntax

Reported by: guest Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Parser) Version: 7.8.1-rc2
Keywords: gadts Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

An alternative syntax for GADTs

Instead of

data Term x where
    K :: Term (a -> b -> a)
    S :: Term ((a -> b -> c)  -> (a -> b) -> a -> c)
    Const :: a -> Term a
    (:@) :: Term (a -> b) -> (Term a) -> Term b

You can write

data Term x = K :: Term (a -> b -> a) 
            | S :: Term ((a -> b -> c)  -> (a -> b) -> a -> c) 
            | Const a :: Term a 
            | (:@) (Term (a -> b)) (Term a) :: Term b

Change History (5)

comment:1 Changed 4 years ago by simonpj

Description: modified (diff)

comment:2 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.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:3 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:4 Changed 2 years ago by strake888

why?

comment:5 Changed 2 years ago by goldfire

Resolution: wontfix
Status: newclosed

In the absence of a person willing to stand up and champion this, I'm closing this ticket.

Note: See TracTickets for help on using tickets.